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/Constant_prop/index.html
Module Jasmin.Constant_prop
val e2bool : Expr.pexpr -> bool Utils0.execval e2int : Expr.pexpr -> BinNums.coq_Z Utils0.execval e2word : Wsize.wsize -> Expr.pexpr -> Ssralg.GRing.ComRing.sort Utils0.execval of_expr : Type.stype -> Expr.pexpr -> Sem_type.sem_t Utils0.execval to_expr : Type.stype -> Sem_type.sem_t -> Expr.pexpr Utils0.execval ssem_sop1 : Expr.sop1 -> Expr.pexpr -> Expr.pexprval ssem_sop2 : Expr.sop2 -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval snot : Expr.pexpr -> Expr.pexprval sneg_int : Expr.pexpr -> Expr.pexprval s_op1 : Expr.sop1 -> Expr.pexpr -> Expr.pexprval sbeq : Expr.pexpr -> Expr.pexpr -> Expr.pexprval sand : Expr.pexpr -> Expr.pexpr -> Expr.pexprval sor : Expr.pexpr -> Expr.pexpr -> Expr.pexprval sadd_int : Expr.pexpr -> Expr.pexpr -> Expr.pexprval sadd_w : Wsize.wsize -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval sadd : Expr.op_kind -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval ssub_int : Expr.pexpr -> Expr.pexpr -> Expr.pexprval ssub_w : Wsize.wsize -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval ssub : Expr.op_kind -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval smul_int : Expr.pexpr -> Expr.pexpr -> Expr.pexprval smul_w : Wsize.wsize -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval smul : Expr.op_kind -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval s_eq : Expr.op_kind -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval sneq : Expr.op_kind -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval is_cmp_const : Expr.cmp_kind -> Expr.pexpr -> BinNums.coq_Z optionval slt : Expr.cmp_kind -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval sle : Expr.cmp_kind -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval sgt : Expr.cmp_kind -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval sge : Expr.cmp_kind -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval s_op2 : Expr.sop2 -> Expr.pexpr -> Expr.pexpr -> Expr.pexprval app_sopn :
Type.stype list ->
'a1 Utils0.exec Sem_type.sem_prod ->
Expr.pexpr list ->
'a1 Utils0.execval s_opN :
Flag_combination.coq_FlagCombinationParams ->
Expr.opN ->
Expr.pexpr list ->
Expr.pexprval s_if : Type.stype -> Expr.pexpr -> Expr.pexpr -> Expr.pexpr -> Expr.pexprtype const_v = | Cbool of bool| Cint of BinNums.coq_Z| Cword of Wsize.wsize * Ssralg.GRing.ComRing.sort
val const_v_eq_axiom : const_v Eqtype.eq_axiomval coq_HB_unnamed_factory_1 : const_v Eqtype.Coq_hasDecEq.axioms_val constant_prop_const_v__canonical__eqtype_Equality :
Eqtype.Equality.coq_typeval const : const_v -> Expr.pexprtype globals = (Var0.Var.var -> Global.glob_value option) optionval const_prop_e :
Flag_combination.coq_FlagCombinationParams ->
globals ->
const_v Var0.Mvar.t ->
Expr.pexpr ->
Expr.pexprval empty_cpm : const_v Var0.Mvar.tval empty_const_prop_e :
Flag_combination.coq_FlagCombinationParams ->
Expr.pexpr ->
Expr.pexprval merge_cpm :
const_v Var0.Mvar.t ->
const_v Var0.Mvar.t ->
const_v Var0.Mvar.tval remove_cpm :
const_v Var0.Mvar.t ->
Var0.SvExtra.Sv.t ->
const_v Var0.Mvar.tval const_prop_rv :
Flag_combination.coq_FlagCombinationParams ->
globals ->
const_v Var0.Mvar.t ->
Expr.lval ->
const_v Var0.Mvar.t * Expr.lvalval const_prop_rvs :
Flag_combination.coq_FlagCombinationParams ->
globals ->
const_v Var0.Mvar.t ->
Expr.lval list ->
const_v Var0.Mvar.t * Expr.lval listval wsize_of_stype : Type.stype -> Wsize.wsizeval add_cpm :
const_v Var0.Mvar.t ->
Expr.lval ->
Expr.assgn_tag ->
Type.stype ->
Expr.pexpr ->
const_v Var0.Mvar.tval const_prop :
'a1 Sopn.asmOp ->
(const_v Var0.Mvar.t ->
'a1 Expr.instr ->
const_v Var0.Mvar.t * 'a1 Expr.instr list) ->
const_v Var0.Mvar.t ->
'a1 Expr.instr list ->
const_v Var0.Mvar.t * 'a1 Expr.instr listval is_update_imm :
'a1 Sopn.asmOp ->
Expr.lval list ->
'a1 Sopn.sopn ->
Expr.pexpr list ->
((Expr.lval * bool) * Expr.pexpr) optionval const_prop_i :
Flag_combination.coq_FlagCombinationParams ->
Wsize.coq_MSFsize ->
'a1 Sopn.asmOp ->
Global.glob_decl list ->
const_v Var0.Mvar.t ->
'a1 Expr.instr ->
const_v Var0.Mvar.t * 'a1 Expr.instr listval const_prop_fun :
Flag_combination.coq_FlagCombinationParams ->
Wsize.coq_MSFsize ->
'a1 Sopn.asmOp ->
Expr.progT ->
Global.glob_decl list ->
'a1 Expr.fundef ->
('a1, Expr.extra_fun_t) Expr._fundefval const_prop_prog :
Flag_combination.coq_FlagCombinationParams ->
Wsize.coq_MSFsize ->
'a1 Sopn.asmOp ->
Expr.progT ->
'a1 Expr.prog ->
'a1 Expr.prog