package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2026.03.0.tar.bz2
sha256=dec62a3cd0cd42cfe96ec64b3cd3961e0e8a09fb92ceb64175cffb54fde50e40
doc/jasmin.jasmin/Jasmin/Warray_/WArray/index.html
Module Warray_.WArray
type array = Word0.word Gen_map.Mz.tval arr_data : BinNums.positive -> array -> Word0.word 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, Word0.word) Utils0.resultval set8 :
BinNums.positive ->
array ->
BinNums.coq_Z ->
Word0.word ->
(Utils0.error, array) Utils0.resultval valid8P :
BinNums.positive ->
array ->
BinNums.coq_Z ->
Word0.word ->
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 ->
Word0.word Utils0.execval set :
BinNums.positive ->
Wsize.wsize ->
array ->
Memory_model.aligned ->
arr_access ->
BinNums.coq_Z ->
Word0.word ->
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_aux :
BinNums.positive ->
Word0.word list ->
(BinNums.coq_Z * array) Utils0.execval fill : BinNums.positive -> Word0.word list -> array Utils0.execval get_sub_data :
arr_access ->
Wsize.wsize ->
BinNums.positive ->
Word0.word Gen_map.Mz.t ->
BinNums.coq_Z ->
Word0.word 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 ->
Word0.word Gen_map.Mz.t ->
BinNums.coq_Z ->
Word0.word Gen_map.Mz.t ->
Word0.word 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 -> Word0.word list -> arrayval is_uincl : BinNums.positive -> BinNums.positive -> array -> array -> boolval is_uinclP :
BinNums.positive ->
BinNums.positive ->
array ->
array ->
Bool.reflect