Core (soteria-rust.Soteria_rust_lib.Interp.Make.Core)

val cmp : 
  signed:bool ->
  [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t ->
  [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint ] Typed.t, 'a, 'b) Rust_val.raw

val equality_check : 
  ([< `NonZero | `Ptr | `Zero ] as 'a) Typed.t ->
  'a Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint ] Soteria.Bv_values.Typed.t, 'b)
    StateM.t

val normalise_shift_r : 
  Charon.Expressions.binop ->
  'a Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint ] as 'b) Typed.t ->
  'b Typed.t

val eval_lit_binop : 
  Charon.Expressions.binop ->
  Charon.Types.literal_type ->
  [< Soteria__Bv_values__Typed.T.sint ] Typed.t ->
  [ `NonZero | `Zero ] Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint_ovf ] Typed.t, 'e) StateM.t

val eval_checked_lit_binop : 
  Charon.Expressions.binop ->
  Charon.Types.literal_type ->
  [< Soteria_rust_lib.Typed.T.any ] Typed.t ->
  [< Soteria_rust_lib.Typed.T.any ] Typed.t ->
  (([> Soteria__Bv_values__Typed.T.sint ] Soteria.Bv_values.Typed.t, 'a, 'b)
     Rust_val.raw,
    'c)
    StateM.t

val meta_as_int : 
  (Soteria_rust_lib.Typed.T.sint Typed.t, StateM.Sptr.t) Rust_val.meta_raw ->
  (Soteria_rust_lib.Typed.T.sint Typed.t option, 'a) StateM.t

val eval_meta_eq : 
  (Soteria_rust_lib.Typed.T.sint Typed.t, StateM.Sptr.t) Rust_val.meta_raw ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, StateM.Sptr.t) Rust_val.meta_raw ->
  ([> Typed.sbool ] Typed.t, 'a) StateM.t

val eval_ptr_binop : 
  Charon.Expressions.binop ->
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    Soteria_rust_lib.Typed.T.sfloat Typed.t,
    StateM.Sptr.t)
    Rust_val.raw ->
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    Soteria_rust_lib.Typed.T.sfloat Typed.t,
    StateM.Sptr.t)
    Rust_val.raw ->
  ([> Soteria__Bv_values__Typed.T.sint ] Typed.t, 'a) StateM.t

val transmute : 
  from_ty:Charon.Types.ty ->
  to_ty:Charon.Types.ty ->
  StateM.rust_val ->
  (StateM.rust_val, 'a) StateM.t

val zero_valid : ty:Charon.Types.ty -> (bool, 'a) StateM.t