Intrinsics (soteria-rust.Soteria_rust_lib.Analyses.Wpst.Interp.Std

val abort : (unit, unit) StateM.t

val add_with_overflow : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val aggregate_raw_ptr : 
  p:Charon.Types.ty ->
  d:Charon.Types.ty ->
  m:Charon.Types.ty ->
  data:StateM.Sptr.t Rust_val.t ->
  meta:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val align_of : 
  t:Charon.Types.ty ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val align_of_val : 
  t:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val arith_offset : 
  t:Charon.Types.ty ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  offset:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (StateM.Sptr.t Rust_val.full_ptr, unit) StateM.t

val assert_inhabited : t:Charon.Types.ty -> (unit, unit) StateM.t

val assert_mem_uninitialized_valid : t:Charon.Types.ty -> (unit, unit) StateM.t

val assert_zero_valid : t:Charon.Types.ty -> (unit, unit) StateM.t

val assume : 
  b:[< Soteria_rust_lib.Typed.T.sbool ] Typed.t ->
  (unit, unit) StateM.t

val atomic_and : 
  t:Charon.Types.ty ->
  u:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_cxchg : 
  t:Charon.Types.ty ->
  ord_succ:Charon.Types.constant_expr ->
  ord_fail:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  old:StateM.Sptr.t Rust_val.t ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_cxchgweak : 
  t:Charon.Types.ty ->
  ord_succ:Charon.Types.constant_expr ->
  ord_fail:Charon.Types.constant_expr ->
  _dst:StateM.Sptr.t Rust_val.full_ptr ->
  _old:StateM.Sptr.t Rust_val.t ->
  _src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_fence : ord:Charon.Types.constant_expr -> (unit, unit) StateM.t

val atomic_load : 
  t:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  src:StateM.Sptr.t Rust_val.full_ptr ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_max : 
  t:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_min : 
  t:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_nand : 
  t:Charon.Types.ty ->
  u:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_or : 
  t:Charon.Types.ty ->
  u:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_singlethreadfence : 
  ord:Charon.Types.constant_expr ->
  (unit, unit) StateM.t

val atomic_store : 
  t:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  val_:StateM.Sptr.t Rust_val.t ->
  (unit, unit) StateM.t

val atomic_umax : 
  t:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_umin : 
  t:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_xadd : 
  t:Charon.Types.ty ->
  u:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_xchg : 
  t:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_xor : 
  t:Charon.Types.ty ->
  u:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val atomic_xsub : 
  t:Charon.Types.ty ->
  u:Charon.Types.ty ->
  ord:Charon.Types.constant_expr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val autodiff : 
  t_f:Charon.Types.ty ->
  g:Charon.Types.ty ->
  t:Charon.Types.ty ->
  r:Charon.Types.ty ->
  f:StateM.Sptr.t Rust_val.t ->
  df:StateM.Sptr.t Rust_val.t ->
  args:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val bitreverse : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val black_box : 
  t:Charon.Types.ty ->
  dummy:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val breakpoint : (unit, unit) StateM.t

val bswap : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val caller_location : (StateM.Sptr.t Rust_val.full_ptr, unit) StateM.t

val carrying_mul_add : 
  t:Charon.Types.ty ->
  u:Charon.Types.ty ->
  multiplier:StateM.Sptr.t Rust_val.t ->
  multiplicand:StateM.Sptr.t Rust_val.t ->
  addend:StateM.Sptr.t Rust_val.t ->
  carry:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val catch_unwind : 
  (Common.Fun_kind.t ->
    StateM.Sptr.t Rust_val.t list ->
    (StateM.Sptr.t Rust_val.t, unit) StateM.t) ->
  _try_fn:StateM.Sptr.t Rust_val.full_ptr ->
  _data:StateM.Sptr.t Rust_val.full_ptr ->
  _catch_fn:StateM.Sptr.t Rust_val.full_ptr ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val ceilf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val ceilf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val ceilf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val ceilf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val cold_path : (unit, unit) StateM.t

val compare_bytes : 
  left:StateM.Sptr.t Rust_val.full_ptr ->
  right:StateM.Sptr.t Rust_val.full_ptr ->
  bytes:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val const_deallocate : 
  _ptr:StateM.Sptr.t Rust_val.full_ptr ->
  _size:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  _align:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (unit, unit) StateM.t

val const_eval_select : 
  arg:Charon.Types.ty ->
  f:Charon.Types.ty ->
  g:Charon.Types.ty ->
  ret:Charon.Types.ty ->
  _arg:StateM.Sptr.t Rust_val.t ->
  _called_in_const:StateM.Sptr.t Rust_val.t ->
  _called_at_rt:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val const_make_global : 
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  (StateM.Sptr.t Rust_val.full_ptr, unit) StateM.t

val contract_check_ensures : 
  c:Charon.Types.ty ->
  t_ret:Charon.Types.ty ->
  cond:StateM.Sptr.t Rust_val.t ->
  ret:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val contract_check_requires : 
  c:Charon.Types.ty ->
  cond:StateM.Sptr.t Rust_val.t ->
  (unit, unit) StateM.t

val copy : 
  t:Charon.Types.ty ->
  src:StateM.Sptr.t Rust_val.full_ptr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  count:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (unit, unit) StateM.t

val copy_nonoverlapping : 
  t:Charon.Types.ty ->
  src:StateM.Sptr.t Rust_val.full_ptr ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  count:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (unit, unit) StateM.t

val copysignf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val copysignf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val copysignf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val copysignf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val cosf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val cosf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val cosf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val cosf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val ctlz : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val ctlz_nonzero : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val ctpop : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val cttz : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val cttz_nonzero : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val discriminant_value : 
  t:Charon.Types.ty ->
  v:StateM.Sptr.t Rust_val.full_ptr ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val disjoint_bitor : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val exact_div : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val exp2f128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val exp2f16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val exp2f32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val exp2f64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val expf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val expf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val expf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val expf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fabsf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fabsf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fabsf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fabsf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fadd_algebraic : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val fadd_fast : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val fdiv_algebraic : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val fdiv_fast : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val float_to_int_unchecked : 
  float:Charon.Types.ty ->
  int:Charon.Types.ty ->
  value:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val floorf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val floorf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val floorf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val floorf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fmaf128 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  b:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  c:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fmaf16 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  b:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  c:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fmaf32 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  b:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  c:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fmaf64 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  b:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  c:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fmul_algebraic : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val fmul_fast : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val fmuladdf128 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  b:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  c:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fmuladdf16 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  b:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  c:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fmuladdf32 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  b:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  c:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val fmuladdf64 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  b:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  c:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val forget : 
  t:Charon.Types.ty ->
  arg:StateM.Sptr.t Rust_val.t ->
  (unit, unit) StateM.t

val frem_algebraic : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val frem_fast : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val fsub_algebraic : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val fsub_fast : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val is_val_statically_known : 
  t:Charon.Types.ty ->
  _arg:StateM.Sptr.t Rust_val.t ->
  (Soteria_rust_lib.Typed.T.sbool Typed.t, unit) StateM.t

val likely : 
  b:[< Soteria_rust_lib.Typed.T.sbool ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sbool Typed.t, unit) StateM.t

val log10f128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val log10f16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val log10f32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val log10f64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val log2f128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val log2f16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val log2f32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val log2f64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val logf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val logf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val logf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val logf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val maximumf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val maximumf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val maximumf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val maximumf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val maxnumf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val maxnumf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val maxnumf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val maxnumf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val minimumf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val minimumf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val minimumf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val minimumf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val minnumf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val minnumf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val minnumf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val minnumf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  y:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val mul_with_overflow : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val needs_drop : 
  t:Charon.Types.ty ->
  (Soteria_rust_lib.Typed.T.sbool Typed.t, unit) StateM.t

val nontemporal_store : 
  t:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  val_:StateM.Sptr.t Rust_val.t ->
  (unit, unit) StateM.t

val offset : 
  ptr:Charon.Types.ty ->
  delta:Charon.Types.ty ->
  dst:StateM.Sptr.t Rust_val.t ->
  offset:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val offset_of : 
  t:Charon.Types.ty ->
  variant:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  field:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val overflow_checks : (Soteria_rust_lib.Typed.T.sbool Typed.t, unit) StateM.t

val powf128 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val powf16 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val powf32 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val powf64 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val powif128 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  x:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val powif16 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  x:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val powif32 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  x:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val powif64 : 
  a:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  x:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val prefetch_read_data : 
  t:Charon.Types.ty ->
  locality:Charon.Types.constant_expr ->
  data:StateM.Sptr.t Rust_val.full_ptr ->
  (unit, unit) StateM.t

val prefetch_read_instruction : 
  t:Charon.Types.ty ->
  locality:Charon.Types.constant_expr ->
  data:StateM.Sptr.t Rust_val.full_ptr ->
  (unit, unit) StateM.t

val prefetch_write_data : 
  t:Charon.Types.ty ->
  locality:Charon.Types.constant_expr ->
  data:StateM.Sptr.t Rust_val.full_ptr ->
  (unit, unit) StateM.t

val prefetch_write_instruction : 
  t:Charon.Types.ty ->
  locality:Charon.Types.constant_expr ->
  data:StateM.Sptr.t Rust_val.full_ptr ->
  (unit, unit) StateM.t

val ptr_guaranteed_cmp : 
  t:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  other:StateM.Sptr.t Rust_val.full_ptr ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val ptr_mask : 
  t:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  mask:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (StateM.Sptr.t Rust_val.full_ptr, unit) StateM.t

val ptr_metadata : 
  p:Charon.Types.ty ->
  m:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val ptr_offset_from : 
  t:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  base:StateM.Sptr.t Rust_val.full_ptr ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val ptr_offset_from_unsigned : 
  t:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  base:StateM.Sptr.t Rust_val.full_ptr ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val raw_eq : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.full_ptr ->
  b:StateM.Sptr.t Rust_val.full_ptr ->
  (Soteria_rust_lib.Typed.T.sbool Typed.t, unit) StateM.t

val read_via_copy : 
  t:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val rotate_left : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  shift:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val rotate_right : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  shift:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val round_ties_even_f128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val round_ties_even_f16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val round_ties_even_f32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val round_ties_even_f64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val roundf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val roundf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val roundf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val roundf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val rustc_peek : 
  t:Charon.Types.ty ->
  arg:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val saturating_add : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val saturating_sub : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val select_unpredictable : 
  t:Charon.Types.ty ->
  b:[< Soteria_rust_lib.Typed.T.sbool ] Typed.t ->
  true_val:StateM.Sptr.t Rust_val.t ->
  false_val:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val sinf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val sinf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val sinf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val sinf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val size_of : 
  t:Charon.Types.ty ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val size_of_val : 
  t:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val slice_get_unchecked : 
  itemptr:Charon.Types.ty ->
  sliceptr:Charon.Types.ty ->
  t:Charon.Types.ty ->
  slice_ptr:StateM.Sptr.t Rust_val.t ->
  index:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val sqrtf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val sqrtf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val sqrtf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val sqrtf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val sub_with_overflow : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val three_way_compare : 
  t:Charon.Types.ty ->
  lhs:StateM.Sptr.t Rust_val.t ->
  rhss:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val transmute : 
  t_src:Charon.Types.ty ->
  dst:Charon.Types.ty ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val transmute_unchecked : 
  t_src:Charon.Types.ty ->
  dst:Charon.Types.ty ->
  src:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val truncf128 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val truncf16 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val truncf32 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val truncf64 : 
  x:[< Soteria_rust_lib.Typed.T.sfloat ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sfloat Typed.t, unit) StateM.t

val type_id : t:Charon.Types.ty -> (StateM.Sptr.t Rust_val.t, unit) StateM.t

val type_id_eq : 
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (Soteria_rust_lib.Typed.T.sbool Typed.t, unit) StateM.t

val type_name : 
  t:Charon.Types.ty ->
  (StateM.Sptr.t Rust_val.full_ptr, unit) StateM.t

val typed_swap_nonoverlapping : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.full_ptr ->
  y:StateM.Sptr.t Rust_val.full_ptr ->
  (unit, unit) StateM.t

val ub_checks : (Soteria_rust_lib.Typed.T.sbool Typed.t, unit) StateM.t

val unaligned_volatile_load : 
  t:Charon.Types.ty ->
  src:StateM.Sptr.t Rust_val.full_ptr ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unaligned_volatile_store : 
  t:Charon.Types.ty ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  val_:StateM.Sptr.t Rust_val.t ->
  (unit, unit) StateM.t

val unchecked_add : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unchecked_div : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unchecked_funnel_shl : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  shift:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unchecked_funnel_shr : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  shift:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unchecked_mul : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unchecked_rem : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unchecked_shl : 
  t:Charon.Types.ty ->
  u:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unchecked_shr : 
  t:Charon.Types.ty ->
  u:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unchecked_sub : 
  t:Charon.Types.ty ->
  x:StateM.Sptr.t Rust_val.t ->
  y:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val unlikely : 
  b:[< Soteria_rust_lib.Typed.T.sbool ] Typed.t ->
  (Soteria_rust_lib.Typed.T.sbool Typed.t, unit) StateM.t

val unreachable : (unit, unit) StateM.t

val va_arg : 
  t:Charon.Types.ty ->
  ap:StateM.Sptr.t Rust_val.full_ptr ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val va_copy : 
  dest:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.full_ptr ->
  (unit, unit) StateM.t

val va_end : ap:StateM.Sptr.t Rust_val.full_ptr -> (unit, unit) StateM.t

val variant_count : 
  t:Charon.Types.ty ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val volatile_copy_memory : 
  t:Charon.Types.ty ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.full_ptr ->
  count:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (unit, unit) StateM.t

val volatile_copy_nonoverlapping_memory : 
  t:Charon.Types.ty ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  src:StateM.Sptr.t Rust_val.full_ptr ->
  count:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (unit, unit) StateM.t

val volatile_load : 
  t:Charon.Types.ty ->
  src:StateM.Sptr.t Rust_val.full_ptr ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val volatile_set_memory : 
  t:Charon.Types.ty ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  val_:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  count:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (unit, unit) StateM.t

val volatile_store : 
  t:Charon.Types.ty ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  val_:StateM.Sptr.t Rust_val.t ->
  (unit, unit) StateM.t

val vtable_align : 
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val vtable_size : 
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, unit) StateM.t

val wrapping_add : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val wrapping_mul : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val wrapping_sub : 
  t:Charon.Types.ty ->
  a:StateM.Sptr.t Rust_val.t ->
  b:StateM.Sptr.t Rust_val.t ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t

val write_bytes : 
  t:Charon.Types.ty ->
  dst:StateM.Sptr.t Rust_val.full_ptr ->
  val_:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  count:[< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (unit, unit) StateM.t

val write_via_move : 
  t:Charon.Types.ty ->
  ptr:StateM.Sptr.t Rust_val.full_ptr ->
  value:StateM.Sptr.t Rust_val.t ->
  (unit, unit) StateM.t

val eval_fun : 
  string ->
  (Common.Fun_kind.t ->
    StateM.Sptr.t Rust_val.t list ->
    (StateM.Sptr.t Rust_val.t, unit) StateM.t) ->
  Charon.Types.generic_args ->
  StateM.Sptr.t Rust_val.t list ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t