Encoder (soteria-rust.Soteria_rust_lib.Builtins.Intrinsics

val encode : 
  offset:Soteria_rust_lib.Typed.T.sint Typed.t ->
  rust_val ->
  Charon.Types.ty ->
  ((rust_val * Soteria_rust_lib.Typed.T.sint Typed.t)
     Soteria.Soteria_std.Iter.t,
    'env)
    monad

val cast_literal : 
  from_ty:Charon.Values.literal_type ->
  to_ty:Charon.Values.literal_type ->
  [< Soteria_rust_lib.Typed.T.cval ] Typed.t ->
  rust_val

val nondet_valid : Charon.Types.ty -> (rust_val, 'env) monad

val apply_attributes : 
  rust_val ->
  Charon.Meta.attribute list ->
  (unit, 'env) monad

val ref_tys_in : 
  ?include_ptrs:bool ->
  rust_val ->
  Charon.Types.ty ->
  (full_ptr * Charon.Types.ty) list

val update_ref_tys_in : 
  f:('acc -> full_ptr -> Charon.Types.ty -> (full_ptr * 'acc, 'env) monad) ->
  init:'acc ->
  rust_val ->
  Charon.Types.ty ->
  (rust_val * 'acc, 'env) monad