WArray (p.jasmin.2026.03.0.doc.jasmin.jasmin.Jasmin.Warray

type array = Word0.word Gen_map.Mz.t

val arr_data : BinNums.positive -> array -> Word0.word Gen_map.Mz.t

val empty : BinNums.positive -> array

val coq_PointerZ : Memory_model.pointer_op

val in_bound : BinNums.positive -> array -> BinNums.coq_Z -> bool

val in_boundP : BinNums.positive -> array -> BinNums.coq_Z -> Bool.reflect

val is_init : BinNums.positive -> array -> BinNums.coq_Z -> bool

val get8 : 
  BinNums.positive ->
  array ->
  BinNums.coq_Z ->
  (Utils0.error, Word0.word) Utils0.result

val set8 : 
  BinNums.positive ->
  array ->
  BinNums.coq_Z ->
  Word0.word ->
  (Utils0.error, array) Utils0.result

val valid8P : 
  BinNums.positive ->
  array ->
  BinNums.coq_Z ->
  Word0.word ->
  Bool.reflect

val array_CM : BinNums.positive -> array Memory_model.coreMem

val in_range : BinNums.positive -> BinNums.coq_Z -> Wsize.wsize -> bool

val in_rangeP : 
  BinNums.positive ->
  BinNums.coq_Z ->
  Wsize.wsize ->
  Bool.reflect

val get : 
  BinNums.positive ->
  Memory_model.aligned ->
  arr_access ->
  Wsize.wsize ->
  array ->
  BinNums.coq_Z ->
  Word0.word Utils0.exec

val set : 
  BinNums.positive ->
  Wsize.wsize ->
  array ->
  Memory_model.aligned ->
  arr_access ->
  BinNums.coq_Z ->
  Word0.word ->
  array Utils0.exec

val fcopy : 
  Wsize.wsize ->
  BinNums.positive ->
  array ->
  array ->
  BinNums.coq_Z ->
  BinNums.coq_Z ->
  (Utils0.error, array) Utils0.result

val copy : 
  Wsize.wsize ->
  BinNums.positive ->
  array ->
  (Utils0.error, array) Utils0.result

val fill_aux : 
  BinNums.positive ->
  Word0.word list ->
  (BinNums.coq_Z * array) Utils0.exec

val fill : BinNums.positive -> Word0.word list -> array Utils0.exec

val get_sub_data : 
  arr_access ->
  Wsize.wsize ->
  BinNums.positive ->
  Word0.word Gen_map.Mz.t ->
  BinNums.coq_Z ->
  Word0.word Gen_map.Mz.t

val get_sub : 
  BinNums.positive ->
  arr_access ->
  Wsize.wsize ->
  BinNums.positive ->
  array ->
  BinNums.coq_Z ->
  array Utils0.exec

val set_sub_data : 
  arr_access ->
  Wsize.wsize ->
  BinNums.positive ->
  Word0.word Gen_map.Mz.t ->
  BinNums.coq_Z ->
  Word0.word Gen_map.Mz.t ->
  Word0.word Gen_map.Mz.t

val set_sub : 
  BinNums.positive ->
  arr_access ->
  Wsize.wsize ->
  BinNums.positive ->
  array ->
  BinNums.coq_Z ->
  array ->
  array Utils0.exec

val cast : 
  BinNums.positive ->
  BinNums.positive ->
  array ->
  (Utils0.error, array) Utils0.result

val of_list : Wsize.wsize -> Word0.word list -> array

val is_uincl : BinNums.positive -> BinNums.positive -> array -> array -> bool

val is_uinclP : 
  BinNums.positive ->
  BinNums.positive ->
  array ->
  array ->
  Bool.reflect