package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa
doc/jasmin.jasmin/Jasmin/Slh_lowering/index.html
Module Jasmin.Slh_lowering
module E : sig ... endmodule Env : sig ... endval check_e_msf :
Expr.instr_info ->
Env.t ->
Expr.pexpr ->
(Compiler_util.pp_error_loc, unit) Utils0.resultval check_lv :
Expr.instr_info ->
Expr.lval ->
(Compiler_util.pp_error_loc, Var0.Var.var option) Utils0.resultval check_lv_msf :
Wsize.coq_MSFsize ->
Expr.instr_info ->
Expr.lval ->
(Compiler_util.pp_error_loc, Var0.Var.var option) Utils0.resultval check_slho :
Wsize.coq_MSFsize ->
Flag_combination.coq_FlagCombinationParams ->
Expr.instr_info ->
Expr.lval list ->
Slh_ops.slh_op ->
Expr.pexpr list ->
Env.t ->
Env.t Compiler_util.cexecval check_f_arg :
Expr.instr_info ->
Env.t ->
Expr.pexpr ->
slh_t ->
(Compiler_util.pp_error_loc, unit) Utils0.resultval check_f_args :
Expr.instr_info ->
Env.t ->
Expr.pexpr list ->
slh_t list ->
(Compiler_util.pp_error_loc, unit list) Utils0.resultval check_f_lv :
Wsize.coq_MSFsize ->
Expr.instr_info ->
Env.t ->
Expr.lval ->
slh_t ->
(Compiler_util.pp_error_loc, Env.t) Utils0.resultval check_f_lvs :
Wsize.coq_MSFsize ->
Expr.instr_info ->
Env.t ->
Expr.lval list ->
slh_t list ->
(Compiler_util.pp_error_loc, Env.t) Utils0.resultval init_fun_env :
Wsize.coq_MSFsize ->
Env.t ->
Expr.var_i list ->
Type.stype list ->
slh_t list ->
(Compiler_util.pp_error_loc, Env.t) Utils0.resultval check_res :
Wsize.coq_MSFsize ->
Env.t ->
Expr.var_i list ->
Type.stype list ->
slh_t list ->
(Compiler_util.pp_error_loc, unit) Utils0.resultval check_for :
Expr.instr_info ->
Var0.Var.var ->
(Env.t -> Env.t Compiler_util.cexec) ->
Datatypes.nat ->
Env.t ->
Env.t Compiler_util.cexecval check_while :
Flag_combination.coq_FlagCombinationParams ->
Expr.instr_info ->
Expr.pexpr ->
(Env.t -> Env.t Compiler_util.cexec) ->
(Env.t -> Env.t Compiler_util.cexec) ->
Datatypes.nat ->
Env.t ->
Env.t Compiler_util.cexectype 'asm_op sh_params =
Expr.lval list ->
Slh_ops.slh_op ->
Expr.pexpr list ->
((Expr.lval list * 'asm_op Sopn.sopn) * Expr.pexpr list) optionval check_i :
'a1 Sopn.asmOp ->
Wsize.coq_MSFsize ->
Flag_combination.coq_FlagCombinationParams ->
(Var0.funname -> slh_t list * slh_t list) ->
'a1 Expr.instr ->
Env.t ->
Env.t Compiler_util.cexecval check_cmd :
'a1 Sopn.asmOp ->
Wsize.coq_MSFsize ->
Flag_combination.coq_FlagCombinationParams ->
(Var0.funname -> slh_t list * slh_t list) ->
Env.t ->
'a1 Expr.instr list ->
Env.t Compiler_util.cexecval check_fd :
'a1 Sopn.asmOp ->
Wsize.coq_MSFsize ->
Flag_combination.coq_FlagCombinationParams ->
Expr.progT ->
(Var0.funname -> slh_t list * slh_t list) ->
Var0.funname ->
'a1 Expr.fundef ->
unit Compiler_util.cexecval lower_slho :
'a1 Sopn.asmOp ->
'a1 sh_params ->
Expr.instr_info ->
Expr.lval list ->
Expr.assgn_tag ->
Slh_ops.slh_op ->
Expr.pexpr list ->
'a1 Expr.instr_r Compiler_util.cexecval lower_i :
'a1 Sopn.asmOp ->
'a1 sh_params ->
'a1 Expr.instr ->
'a1 Expr.instr Compiler_util.cexecval lower_cmd :
'a1 Sopn.asmOp ->
'a1 sh_params ->
'a1 Expr.instr list ->
'a1 Expr.instr list Compiler_util.cexecval lower_fd :
'a1 Sopn.asmOp ->
Wsize.coq_MSFsize ->
Flag_combination.coq_FlagCombinationParams ->
Expr.progT ->
'a1 sh_params ->
(Var0.funname -> slh_t list * slh_t list) ->
Var0.funname ->
'a1 Expr.fundef ->
(Compiler_util.pp_error_loc, ('a1, Expr.extra_fun_t) Expr._fundef)
Utils0.resultval is_shl_none : slh_t -> boolval lower_slh_prog :
'a1 Sopn.asmOp ->
Wsize.coq_MSFsize ->
Flag_combination.coq_FlagCombinationParams ->
Expr.progT ->
'a1 sh_params ->
(Var0.funname -> slh_t list * slh_t list) ->
Var0.funname list ->
'a1 Expr.prog ->
'a1 Expr.prog Compiler_util.cexec