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

type array = Ssralg.GRing.ComRing.sort Gen_map.Mz.t

val arr_data : 
  BinNums.positive ->
  array ->
  Ssralg.GRing.ComRing.sort 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, Ssralg.GRing.Nmodule.sort) Utils0.result

val set8 : 
  BinNums.positive ->
  array ->
  BinNums.coq_Z ->
  Ssralg.GRing.ComRing.sort ->
  (Utils0.error, array) Utils0.result

val valid8P : 
  BinNums.positive ->
  array ->
  BinNums.coq_Z ->
  Ssralg.GRing.ComRing.sort ->
  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 ->
  Ssralg.GRing.ComRing.sort Utils0.exec

val set : 
  BinNums.positive ->
  Wsize.wsize ->
  array ->
  Memory_model.aligned ->
  arr_access ->
  BinNums.coq_Z ->
  Ssralg.GRing.ComRing.sort ->
  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 : 
  BinNums.positive ->
  Ssralg.GRing.ComRing.sort list ->
  array Utils0.exec

val get_sub_data : 
  arr_access ->
  Wsize.wsize ->
  BinNums.positive ->
  Ssralg.GRing.ComRing.sort Gen_map.Mz.t ->
  BinNums.coq_Z ->
  Ssralg.GRing.ComRing.sort 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 ->
  Ssralg.GRing.ComRing.sort Gen_map.Mz.t ->
  BinNums.coq_Z ->
  Ssralg.GRing.ComRing.sort Gen_map.Mz.t ->
  Ssralg.GRing.ComRing.sort 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 -> Ssralg.GRing.ComRing.sort list -> array