package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.2.tar.bz2
sha256=aa0d21f532c1560a0939244cfd1c8414ba2b42c9d1403960f458500446cb1ebb
doc/jasmin.jasmin/Jasmin/Warray_/WArray/index.html
Module Warray_.WArray
type array = Ssralg.GRing.ComRing.sort Gen_map.Mz.tval arr_data :
BinNums.positive ->
array ->
Ssralg.GRing.ComRing.sort Gen_map.Mz.tval empty : BinNums.positive -> arrayval coq_PointerZ : Memory_model.pointer_opval in_bound : BinNums.positive -> array -> BinNums.coq_Z -> boolval in_boundP : BinNums.positive -> array -> BinNums.coq_Z -> Bool.reflectval is_init : BinNums.positive -> array -> BinNums.coq_Z -> boolval get8 :
BinNums.positive ->
array ->
BinNums.coq_Z ->
(Utils0.error, Ssralg.GRing.Nmodule.sort) Utils0.resultval set8 :
BinNums.positive ->
array ->
BinNums.coq_Z ->
Ssralg.GRing.ComRing.sort ->
(Utils0.error, array) Utils0.resultval valid8P :
BinNums.positive ->
array ->
BinNums.coq_Z ->
Ssralg.GRing.ComRing.sort ->
Bool.reflectval array_CM : BinNums.positive -> array Memory_model.coreMemval in_range : BinNums.positive -> BinNums.coq_Z -> Wsize.wsize -> boolval in_rangeP :
BinNums.positive ->
BinNums.coq_Z ->
Wsize.wsize ->
Bool.reflectval get :
BinNums.positive ->
Memory_model.aligned ->
arr_access ->
Wsize.wsize ->
array ->
BinNums.coq_Z ->
Ssralg.GRing.ComRing.sort Utils0.execval set :
BinNums.positive ->
Wsize.wsize ->
array ->
Memory_model.aligned ->
arr_access ->
BinNums.coq_Z ->
Ssralg.GRing.ComRing.sort ->
array Utils0.execval fcopy :
Wsize.wsize ->
BinNums.positive ->
array ->
array ->
BinNums.coq_Z ->
BinNums.coq_Z ->
(Utils0.error, array) Utils0.resultval copy :
Wsize.wsize ->
BinNums.positive ->
array ->
(Utils0.error, array) Utils0.resultval fill :
BinNums.positive ->
Ssralg.GRing.ComRing.sort list ->
array Utils0.execval 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.tval get_sub :
BinNums.positive ->
arr_access ->
Wsize.wsize ->
BinNums.positive ->
array ->
BinNums.coq_Z ->
array Utils0.execval 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.tval set_sub :
BinNums.positive ->
arr_access ->
Wsize.wsize ->
BinNums.positive ->
array ->
BinNums.coq_Z ->
array ->
array Utils0.execval cast :
BinNums.positive ->
BinNums.positive ->
array ->
(Utils0.error, array) Utils0.resultval of_list : Wsize.wsize -> Ssralg.GRing.ComRing.sort list -> array