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/Psem_defs/index.html
Module Jasmin.Psem_defs
val sem_sop1 : Operators.sop1 -> Values.value -> Values.value Utils0.execval sem_sop2 :
Operators.sop2 ->
Values.value ->
Values.value ->
Values.value Utils0.execval sem_opN :
Flag_combination.coq_FlagCombinationParams ->
Operators.opN ->
Values.values ->
Values.value Utils0.execval get_global_value :
Global.glob_decl list ->
Var0.Var.var ->
Global.glob_value optionval gv2val : Global.glob_value -> Values.valueval get_global :
Global.glob_decl list ->
Var0.Var.var ->
Values.value Utils0.exectype 'syscall_state estate = {escs : 'syscall_state;emem : Low_memory.Memory.mem;evm : Varmap.Vm.t;
}val escs :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
'a1 estate ->
'a1val emem :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
'a1 estate ->
Low_memory.Memory.memval evm :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
'a1 estate ->
Varmap.Vm.tval get_gvar :
Sem_type.coq_WithSubWord ->
bool ->
Global.glob_decl list ->
Varmap.Vm.t ->
Expr.gvar ->
(Utils0.error, Values.value) Utils0.resultval get_var_is :
Sem_type.coq_WithSubWord ->
bool ->
Varmap.Vm.t ->
Expr.var_i list ->
(Utils0.error, Values.value list) Utils0.resultval on_arr_var :
Values.value Utils0.exec ->
(BinNums.positive -> Warray_.WArray.array -> 'a1 Utils0.exec) ->
(Utils0.error, 'a1) Utils0.resultval with_vm :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
'a1 estate ->
Varmap.Vm.t ->
'a1 estateval with_mem :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
'a1 estate ->
Low_memory.Memory.mem ->
'a1 estateval with_scs :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
'a1 estate ->
'a1 ->
'a1 estateval sem_pexpr :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
Sem_params.coq_SemPexprParams ->
bool ->
Global.glob_decl list ->
'a1 estate ->
Expr.pexpr ->
Values.value Utils0.execval sem_pexprs :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
Sem_params.coq_SemPexprParams ->
bool ->
Global.glob_decl list ->
'a1 estate ->
Expr.pexpr list ->
(Utils0.error, Values.value list) Utils0.resultval write_var :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
bool ->
Expr.var_i ->
Values.value ->
'a1 estate ->
'a1 estate Utils0.execval write_vars :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
bool ->
Expr.var_i list ->
Values.value list ->
'a1 estate ->
(Utils0.error, 'a1 estate) Utils0.resultval write_none :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
bool ->
'a1 estate ->
Type.ctype ->
Values.value ->
(Utils0.error, 'a1 estate) Utils0.resultval write_lval :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
Sem_params.coq_SemPexprParams ->
bool ->
Global.glob_decl list ->
Expr.lval ->
Values.value ->
'a1 estate ->
'a1 estate Utils0.execval write_lvals :
Sem_type.coq_WithSubWord ->
'a1 Sem_params.coq_EstateParams ->
Sem_params.coq_SemPexprParams ->
bool ->
Global.glob_decl list ->
'a1 estate ->
Expr.lval list ->
Values.value list ->
(Utils0.error, 'a1 estate) Utils0.resultval exec_sopn :
'a2 Sem_params.coq_EstateParams ->
'a1 Sopn.asmOp ->
'a1 Sopn.sopn ->
Values.values ->
Values.values Utils0.execval sem_sopn :
Sem_type.coq_WithSubWord ->
'a2 Sem_params.coq_EstateParams ->
Sem_params.coq_SemPexprParams ->
'a1 Sopn.asmOp ->
Global.glob_decl list ->
'a1 Sopn.sopn ->
'a2 estate ->
Expr.lval list ->
Expr.pexpr list ->
(Utils0.error, 'a2 estate) Utils0.resultval syscall_sem__ :
'a1 Syscall.syscall_sem ->
Wsize.coq_PointerData ->
'a1 Syscall.syscall_state_t ->
Low_memory.Memory.mem ->
(Wsize.wsize * BinNums.positive) Syscall_t.syscall_t ->
Values.values ->
(('a1 Syscall.syscall_state_t * Low_memory.Memory.mem) * Values.values)
Utils0.exec