Wint_int (p.jasmin.2026.09.0.doc.jasmin.jasmin.Jasmin.Wint

module E : sig ... end

val sc_op1 : Operators.sop1 -> Expr.pexpr -> Expr.pexpr list

val sc_op2 : Operators.sop2 -> Expr.pexpr -> Expr.pexpr -> Expr.pexpr list

val wi2i_op2 : Operators.sop2 -> Operators.sop2

val wi2i_op1_e : Operators.sop1 -> Expr.pexpr -> Expr.pexpr

val wi2i_op2_e : Operators.sop2 -> Expr.pexpr -> Expr.pexpr -> Expr.pexpr

val wi2i_var : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.Var.var ->
  Var0.Var.var

val in_FV_var : Var0.SvExtra.Sv.t -> Var0.Var.var -> bool

val wi2i_vari : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc, Expr.var_i) Utils0.result

val wint_contract_condition : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  Expr.var_i ->
  (Compiler_util.pp_error_loc, (string * Expr.eassert) list) Utils0.result

val wi2i_gvar : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  Expr.gvar ->
  (Compiler_util.pp_error_loc, Expr.gvar) Utils0.result

val wi2i_type : Wsize.signedness option -> Type.atype -> Type.atype

type safety_cond = Expr.pexpr list

val wi2i_es : 
  (Expr.pexpr -> (safety_cond * Expr.pexpr) Compiler_util.cexec) ->
  Expr.pexpr list ->
  (safety_cond * Expr.pexpr list) Compiler_util.cexec

val wi2i_e : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  Expr.pexpr ->
  (safety_cond * Expr.pexpr) Compiler_util.cexec

val wi2i_lvar : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  BinNums.coq_Z Type.extended_type ->
  Expr.var_i ->
  Expr.var_i Compiler_util.cexec

val wi2i_lv : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  BinNums.coq_Z Type.extended_type ->
  Expr.lval ->
  (safety_cond * Expr.lval) Compiler_util.cexec

val wi2i_lvs : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  string ->
  bool ->
  BinNums.coq_Z Type.extended_type list ->
  Expr.lval list ->
  (Compiler_util.pp_error_loc, Expr.pexpr list * Expr.lval list) Utils0.result

val wi2i_eassert : 
  Wsize.coq_PointerData ->
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  Expr.eassert ->
  (safety_cond * Expr.eassert) Compiler_util.cexec

val wi2i_a_and : 
  Wsize.coq_PointerData ->
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  Expr.assertion ->
  (Compiler_util.pp_error_loc, Utils0.assertion_label * Expr.eassert)
    Utils0.result

val get_sig : 
  (Var0.funname ->
    (BinNums.coq_Z Type.extended_type list
     * BinNums.coq_Z Type.extended_type list)
      option) ->
  Var0.funname ->
  (Compiler_util.pp_error_loc,
    BinNums.coq_Z Type.extended_type list
    * BinNums.coq_Z Type.extended_type list)
    Utils0.result

val wi2i_c : 
  'a1 Sopn.asmOp ->
  ('a1 Expr.instr -> 'a1 Expr.instr list Compiler_util.cexec) ->
  'a1 Expr.instr list ->
  (Compiler_util.pp_error_loc, 'a1 Expr.instr list) Utils0.result

type is_Polymorphic_op =

| IsSpill of Pseudo_operator.spill_op * Type.atype list
| IsSwap of Type.atype
| IsDeclassify of Type.atype
| IsOther

val is_polymorphic_op : 'a1 Sopn.asmOp -> 'a1 Sopn.sopn -> is_Polymorphic_op

val wi2i_ir : 
  'a1 Sopn.asmOp ->
  Wsize.coq_PointerData ->
  Wsize.coq_MSFsize ->
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  (Var0.funname ->
    (BinNums.coq_Z Type.extended_type list
     * BinNums.coq_Z Type.extended_type list)
      option) ->
  'a1 Expr.instr_r ->
  (safety_cond * 'a1 Expr.instr_r) Compiler_util.cexec

val wi2i_i : 
  'a1 Sopn.asmOp ->
  Wsize.coq_PointerData ->
  Wsize.coq_MSFsize ->
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  (Var0.funname ->
    (BinNums.coq_Z Type.extended_type list
     * BinNums.coq_Z Type.extended_type list)
      option) ->
  'a1 Expr.instr ->
  'a1 Expr.instr list Compiler_util.cexec

val wi2i_ci : 
  Wsize.coq_PointerData ->
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  Expr.fun_contract ->
  (BinNums.coq_Z Type.extended_type list
   * BinNums.coq_Z Type.extended_type list) ->
  (Compiler_util.pp_error_loc, Expr.fun_contract) Utils0.result

val wi2i_fun : 
  'a1 Sopn.asmOp ->
  Wsize.coq_PointerData ->
  Wsize.coq_MSFsize ->
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  (Var0.funname ->
    (BinNums.coq_Z Type.extended_type list
     * BinNums.coq_Z Type.extended_type list)
      option) ->
  Var0.funname ->
  'a1 Expr.fundef ->
  ('a1, Expr.extra_fun_t) Expr._fundef Compiler_util.cexec

val build_sig : 
  'a1 Sopn.asmOp ->
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  (Var0.funname * 'a1 Expr.fundef) ->
  Var0.funname
  * (BinNums.coq_Z Type.extended_type list
     * BinNums.coq_Z Type.extended_type list)

val build_info : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.SvExtra.Sv.t ->
  (Compiler_util.pp_error_loc,
    Eqtype.Equality.sort ->
    (Wsize.signedness * Var0.Var.var) option)
    Utils0.result

val wi2i_prog : 
  'a1 Sopn.asmOp ->
  Wsize.coq_PointerData ->
  Wsize.coq_MSFsize ->
  ('a1 Expr._uprog ->
    Var0.SvExtra.Sv.t
    * (Var0.Var.var ->
    (Wsize.signedness * Var0.Var.var) option)) ->
  'a1 Expr._uprog ->
  'a1 Expr._uprog Compiler_util.cexec