Module Jasmin.Memory_model

type __ = Obj.t
module LE : sig ... end
type 'core_mem coreMem = {
  1. get : 'core_mem -> Eqtype.Equality.sort -> Ssralg.GRing.ComRing.sort Utils0.exec;
  2. set : 'core_mem -> Eqtype.Equality.sort -> Ssralg.GRing.ComRing.sort -> 'core_mem Utils0.exec;
  3. valid8 : 'core_mem -> Eqtype.Equality.sort -> bool;
  4. valid8P : 'core_mem -> Eqtype.Equality.sort -> Ssralg.GRing.ComRing.sort -> Bool.reflect;
}
type aligned =
  1. | Unaligned
  2. | Aligned
val aligned_tag : aligned -> BinNums.positive
type box_aligned_Unaligned =
  1. | Box_aligned_Unaligned
type aligned_fields_t = __
val aligned_fields : aligned -> aligned_fields_t
val aligned_eqb_fields : (aligned -> aligned -> bool) -> BinNums.positive -> aligned_fields_t -> aligned_fields_t -> bool
val aligned_eqb : aligned -> aligned -> bool
val aligned_eqb_OK : aligned -> aligned -> Bool.reflect
val coq_HB_unnamed_factory_1 : aligned Eqtype.Coq_hasDecEq.axioms_
val memory_model_aligned__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val aligned_le : aligned -> aligned -> bool
module CoreMem : sig ... end
val coq_PointerW : Wsize.coq_PointerData -> pointer_op
type 'mem memory = {
  1. stack_root : 'mem -> Ssralg.GRing.ComRing.sort;
  2. stack_limit : 'mem -> Ssralg.GRing.ComRing.sort;
  3. frames : 'mem -> Ssralg.GRing.ComRing.sort list;
  4. alloc_stack : 'mem -> Wsize.wsize -> BinNums.coq_Z -> BinNums.coq_Z -> BinNums.coq_Z -> 'mem Utils0.exec;
  5. free_stack : 'mem -> 'mem;
  6. init : (Ssralg.GRing.ComRing.sort * BinNums.coq_Z) list -> Ssralg.GRing.ComRing.sort -> 'mem Utils0.exec;
}
module type MemoryT = sig ... end