Finish eval_correct proof

5 files changed, 1043 insertions, 248 deletions

diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v
index bef9f3d..1b7d2e0 100644
--- a/src/hls/DMemorygen.v
+++ b/src/hls/DMemorygen.v
@@ -1,6 +1,6 @@
 (*
  * Vericert: Verified high-level synthesis.
- * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2021-2023 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 7dd1c97..34ba238 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -207,8 +207,6 @@ Fixpoint from_predicated_inv (a: predicated pred_expression): pred_op :=
 Definition simpl_combine {A: Type} (a b: option (@Predicate.pred_op A)) :=
   Option.map simplify (combine_pred a b).
 
-Definition dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default T p.
-
 Definition assert_ (b: bool): option unit :=
   if b then Some tt else None.
 
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 1bc0fd5..e9061a5 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -33,6 +33,11 @@ Require Import vericert.hls.Verilog.
 Require Import vericert.hls.Gible.
 Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.Predicate.
+Require Import vericert.common.Errormonad.
+Import ErrorMonad.
+Import ErrorMonadExtra.
+
+#[local] Open Scope monad_scope.
 
 #[local] Hint Resolve AssocMap.gempty : htlh.
 #[local] Hint Resolve AssocMap.gso : htlh.
@@ -40,62 +45,14 @@ Require Import vericert.hls.Predicate.
 #[local] Hint Resolve Ple_refl : htlh.
 #[local] Hint Resolve Ple_succ : htlh.
 
-Record state: Type := mkstate {
-  st_st : reg;
-  st_freshreg: reg;
-  st_freshstate: node;
-  st_scldecls: AssocMap.t (option io * scl_decl);
-  st_arrdecls: AssocMap.t (option io * arr_decl);
-  st_datapath: datapath;
+Record control_regs: Type := mk_control_regs {
+  ctrl_st : reg;
+  ctrl_stack : reg;
+  ctrl_preg : reg;
+  ctrl_fin : reg;
+  ctrl_return : reg;
 }.
 
-Definition init_state (st : reg) : state :=
-  mkstate st
-          1%positive
-          1%positive
-          (AssocMap.empty (option io * scl_decl))
-          (AssocMap.empty (option io * arr_decl))
-          (AssocMap.empty stmnt).
-
-Module HTLState <: State.
-
-  Definition st := state.
-
-  Inductive st_incr: state -> state -> Prop :=
-    state_incr_intro:
-      forall (s1 s2: state),
-        st_st s1 = st_st s2 ->
-        Ple s1.(st_freshreg) s2.(st_freshreg) ->
-        Ple s1.(st_freshstate) s2.(st_freshstate) ->
-        (forall n,
-            s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
-        st_incr s1 s2.
-  #[export] Hint Constructors st_incr : htlh.
-
-  Definition st_prop := st_incr.
-  #[export] Hint Unfold st_prop : htlh.
-
-  Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed.
-
-  Lemma st_trans :
-    forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
-  Proof.
-    intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
-    - destruct H4 with n; destruct H7 with n; intuition congruence.
-  Qed.
-
-End HTLState.
-Export HTLState.
-
-Module HTLMonad := Statemonad(HTLState).
-Export HTLMonad.
-
-Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
-Import HTLMonadExtra.
-Export MonadNotation.
-
-#[local] Open Scope monad_scope.
-
 Definition pred_lit (preg: reg) (pred: predicate) :=
   Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)).
 
@@ -133,62 +90,6 @@ Definition state_goto (preg: reg) (p: option pred_op) (st : reg) (n : node) : st
 Definition state_cond (preg: reg) (p: option pred_op) (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
   translate_predicate Vblock preg p (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
 
-Definition check_empty_node_datapath:
-  forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.
-Proof.
-  intros. case (s.(st_datapath)!n); tauto.
-Defined.
-
-Definition append_instr (n : node) (st : stmnt) (d : datapath) : datapath :=
-  match AssocMap.get n d with 
-  | Some st' => AssocMap.set n (Vseq st' st) d
-  | None => AssocMap.set n st d
-  end.
-
-Lemma declare_reg_state_incr :
-  forall i s r sz,
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       s.(st_freshstate)
-       (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
-       s.(st_arrdecls)
-       s.(st_datapath)).
-Proof. Admitted.
-
-Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
-  fun s => OK tt (mkstate
-                s.(st_st)
-                s.(st_freshreg)
-                s.(st_freshstate)
-                (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
-                s.(st_arrdecls)
-                s.(st_datapath))
-              (declare_reg_state_incr i s r sz).
-
-Lemma declare_arr_state_incr :
-  forall i s r sz ln,
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       s.(st_freshstate)
-       s.(st_scldecls)
-       (AssocMap.set r (i, VArray sz ln) s.(st_arrdecls))
-       s.(st_datapath)).
-Proof. Admitted.
-
-Definition declare_arr (i : option io) (r : reg) (sz : nat) (ln : nat) : mon unit :=
-  fun s => OK tt (mkstate
-                s.(st_st)
-                s.(st_freshreg)
-                s.(st_freshstate)
-                s.(st_scldecls)
-                (AssocMap.set r (i, VArray sz ln) s.(st_arrdecls))
-                s.(st_datapath))
-              (declare_arr_state_incr i s r sz ln).
-
 Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
 Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
 
@@ -201,15 +102,17 @@ Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
 Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
   Vbinop op (Vvar r) (Vlit (ZToValue l)).
 
+Definition error {A} m := @Errors.Error A (Errors.msg m).
+
 Definition translate_comparison (c : Integers.comparison) (args : list reg) : Errors.res expr :=
   match c, args with
-  | Integers.Ceq, r1::r2::nil => Errors.OK (bop Veq r1 r2)
-  | Integers.Cne, r1::r2::nil => Errors.OK (bop Vne r1 r2)
-  | Integers.Clt, r1::r2::nil => Errors.OK (bop Vlt r1 r2)
-  | Integers.Cgt, r1::r2::nil => Errors.OK (bop Vgt r1 r2)
-  | Integers.Cle, r1::r2::nil => Errors.OK (bop Vle r1 r2)
-  | Integers.Cge, r1::r2::nil => Errors.OK (bop Vge r1 r2)
-  | _, _ => Errors.Error (Errors.msg "Htlgen: comparison instruction not implemented: other")
+  | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
+  | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
+  | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2)
+  | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)
+  | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)
+  | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)
+  | _, _ => error "Htlpargen: comparison instruction not implemented: other"
   end.
 
 Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
@@ -221,7 +124,7 @@ Definition translate_comparison_imm (c : Integers.comparison) (args : list reg)
   | Integers.Cgt, r1::nil => Errors.OK (boplit Vgt r1 i)
   | Integers.Cle, r1::nil => Errors.OK (boplit Vle r1 i)
   | Integers.Cge, r1::nil => Errors.OK (boplit Vge r1 i)
-  | _, _ => Errors.Error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
+  | _, _ => error "Htlpargen: comparison_imm instruction not implemented: other"
   end.
 
 Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : Errors.res expr :=
@@ -230,7 +133,7 @@ Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : E
   | Integers.Cgt, r1::r2::nil => Errors.OK (bop Vgtu r1 r2)
   | Integers.Cle, r1::r2::nil => Errors.OK (bop Vleu r1 r2)
   | Integers.Cge, r1::r2::nil => Errors.OK (bop Vgeu r1 r2)
-  | _, _ => Errors.Error (Errors.msg "Htlgen: comparison instruction not implemented: other")
+  | _, _ => Errors.Error (Errors.msg "Htlpargen: comparison instruction not implemented: other")
   end.
 
 Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)
@@ -240,7 +143,7 @@ Definition translate_comparison_immu (c : Integers.comparison) (args : list reg)
   | Integers.Cgt, r1::nil => Errors.OK (boplit Vgtu r1 i)
   | Integers.Cle, r1::nil => Errors.OK (boplit Vleu r1 i)
   | Integers.Cge, r1::nil => Errors.OK (boplit Vgeu r1 i)
-  | _, _ => Errors.Error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
+  | _, _ => Errors.Error (Errors.msg "Htlpargen: comparison_imm instruction not implemented: other")
   end.
 
 Definition translate_condition (c : Op.condition) (args : list reg) : Errors.res expr :=
@@ -249,9 +152,9 @@ Definition translate_condition (c : Op.condition) (args : list reg) : Errors.res
   | Op.Ccompu c, _ => translate_comparisonu c args
   | Op.Ccompimm c i, _ => translate_comparison_imm c args i
   | Op.Ccompuimm c i, _ => translate_comparison_immu c args i
-  | Op.Cmaskzero n, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
-  | Op.Cmasknotzero n, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero")
-  | _, _ => Errors.Error (Errors.msg "Htlgen: condition instruction not implemented: other")
+  | Op.Cmaskzero n, _ => Errors.Error (Errors.msg "Htlpargen: condition instruction not implemented: Cmaskzero")
+  | Op.Cmasknotzero n, _ => Errors.Error (Errors.msg "Htlpargen: condition instruction not implemented: Cmasknotzero")
+  | _, _ => Errors.Error (Errors.msg "Htlpargen: condition instruction not implemented: other")
   end.
 
 Definition check_address_parameter_signed (p : Z) : bool :=
@@ -299,8 +202,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex
   | Op.Osub, r1::r2::nil => Errors.OK (bop Vsub r1 r2)
   | Op.Omul, r1::r2::nil => Errors.OK (bop Vmul r1 r2)
   | Op.Omulimm n, r::nil => Errors.OK (boplit Vmul r n)
-  | Op.Omulhs, r1::r2::nil => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: mulhs")
-  | Op.Omulhu, r1::r2::nil => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: mulhu")
+  | Op.Omulhs, r1::r2::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: mulhs")
+  | Op.Omulhu, r1::r2::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: mulhu")
   | Op.Odiv, r1::r2::nil => Errors.OK (bop Vdiv r1 r2)
   | Op.Odivu, r1::r2::nil => Errors.OK (bop Vdivu r1 r2)
   | Op.Omod, r1::r2::nil => Errors.OK (bop Vmod r1 r2)
@@ -322,7 +225,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex
                   (Vbinop Vshru (Vvar r) (Vlit n)))
   | Op.Oshru, r1::r2::nil => Errors.OK (bop Vshru r1 r2)
   | Op.Oshruimm n, r::nil => Errors.OK (boplit Vshru r n)
-  | Op.Ororimm n, r::nil => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
+  | Op.Ororimm n, r::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: Ororimm")
   (*Errors.OK (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))
                                         (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)
   | Op.Oshldimm n, r::nil => Errors.OK (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
@@ -331,7 +234,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex
     do tc <- translate_condition c rl;
     Errors.OK (Vternary tc (Vvar r1) (Vvar r2))
   | Op.Olea a, _ => translate_eff_addressing a args
-  | _, _ => Errors.Error (Errors.msg "Htlgen: Instruction not implemented: other")
+  | _, _ => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: other")
   end.
 
 Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
@@ -393,8 +296,6 @@ Definition translate_cfi (fin rtrn state preg: reg) p (cfi: cf_instr)
     Errors.Error (Errors.msg "HTLPargen: RBbuildin not supported.")
   end.
 
-Definition dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default Ptrue p.
-
 Definition transf_instr (fin rtrn stack state preg: reg) 
            (dc: pred_op * stmnt) (i: instr)
            : Errors.res (pred_op * stmnt) :=
@@ -423,20 +324,17 @@ Definition transf_instr (fin rtrn stack state preg: reg)
     Errors.OK (Pand curr_p (negate (dfltp p)), Vseq d d_stmnt)
   end.
 
-Definition fold_leftE {A B} (f: A -> B -> Errors.res A) (l: list B) (el: A): Errors.res A :=
-  fold_left (fun a b => do a' <- a; f a' b) l (Errors.OK el).
-
 Definition transf_chained_block (fin rtrn stack state preg: reg)
            (dc: @pred_op positive * stmnt)
            (block: list instr)
            : Errors.res (pred_op * stmnt) :=
-  fold_leftE (transf_instr fin rtrn stack state preg) block dc.
+  mfold_left (transf_instr fin rtrn stack state preg) block (ret dc).
 
 Definition transf_parallel_block (fin rtrn stack state preg: reg)
            (dc: @pred_op positive * stmnt)
            (block: list (list instr))
            : Errors.res (pred_op * stmnt) :=
-  fold_leftE (transf_chained_block fin rtrn stack state preg) block dc.
+  mfold_left (transf_chained_block fin rtrn stack state preg) block (ret dc).
 
 Definition transf_parallel_full_block (fin rtrn stack state preg: reg)
            (dc: node * @pred_op positive * datapath)
@@ -457,85 +355,14 @@ Definition transf_seq_block (fin rtrn stack state preg: reg)
            (d: datapath) (n: node)
            (block: list (list (list instr)))
            : Errors.res datapath :=
-  do res <- fold_leftE
-    (transf_parallel_full_block fin rtrn stack state preg) block (n, Ptrue, d);
+  do res <- mfold_left
+    (transf_parallel_full_block fin rtrn stack state preg) block (ret (n, Ptrue, d));
   let '(_, _, d') := res in
   Errors.OK d'.
 
-#[local] Close Scope error_monad_scope.
-#[local] Open Scope monad_scope.
-
-Program Definition transf_seq_blockM (fin rtrn stack preg: reg) (ni: node * ParBB.t): mon unit :=
-  fun st =>
+Definition transf_seq_blockM (ctrl: control_regs) (d: datapath) (ni: node * ParBB.t): res datapath :=
     let (n, i) := ni in
-    match transf_seq_block fin rtrn stack st.(st_st) preg st.(st_datapath) n i with
-    | Errors.OK d => 
-      OK tt (mkstate st.(st_st)
-             st.(st_freshreg)
-             st.(st_freshstate)
-             st.(st_scldecls)
-             st.(st_arrdecls)
-             d) _
-    | Errors.Error m => Error m
-    end.
-Next Obligation.
-admit.
-Admitted.
-
-Definition declare_regs (i: instr): mon unit :=
-  match i with
-  | RBop _ _ _ d => declare_reg None d 32
-  | RBload _ _ _ _ d => declare_reg None d 32
-  | _ => ret tt
-  end.
-
-Definition declare_all_regs (ni: node * ParBB.t): mon unit :=
-  let (n, i) := ni in
-  ParBB.foldl _ (fun (st_f: mon unit) i => do _tt <- st_f; declare_regs i) i (ret tt).
-
-Lemma create_reg_state_incr:
-  forall s sz i,
-    st_incr s (mkstate
-         s.(st_st)
-         (Pos.succ (st_freshreg s))
-         (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
-         s.(st_arrdecls)
-         (st_datapath s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_reg (i : option io) (sz : nat) : mon reg :=
-  fun s => let r := s.(st_freshreg) in
-           OK r (mkstate
-                   s.(st_st)
-                   (Pos.succ r)
-                   (st_freshstate s)
-                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
-                   (st_arrdecls s)
-                   (st_datapath s))
-              (create_reg_state_incr s sz i).
-
-Lemma create_arr_state_incr:
-  forall s sz ln i,
-    st_incr s (mkstate
-         s.(st_st)
-         (Pos.succ (st_freshreg s))
-         (st_freshstate s)
-         s.(st_scldecls)
-         (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
-         (st_datapath s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
-  fun s => let r := s.(st_freshreg) in
-           OK (r, ln) (mkstate
-                   s.(st_st)
-                   (Pos.succ r)
-                   (st_freshstate s)
-                   s.(st_scldecls)
-                   (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
-                   (st_datapath s))
-              (create_arr_state_incr s sz ln i).
+    transf_seq_block ctrl.(ctrl_fin) ctrl.(ctrl_return) ctrl.(ctrl_stack) ctrl.(ctrl_st) ctrl.(ctrl_preg) d n i.
 
 Definition stack_correct (sz : Z) : bool :=
   (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
@@ -580,61 +407,46 @@ Definition decide_order a b c d e f g h : {module_ordering a b c d e f g h} + {T
                    end; unfold module_ordering; auto.
 Defined.
 
-Definition transf_module (f: function) : mon DHTL.module.
-  refine (
+Program Definition transl_module (f: function) : res DHTL.module :=
   if stack_correct f.(fn_stacksize) then
-    do fin <- create_reg (Some Voutput) 1;
-    do rtrn <- create_reg (Some Voutput) 32;
-    do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
-    do start <- create_reg (Some Vinput) 1;
-    do rst <- create_reg (Some Vinput) 1;
-    do clk <- create_reg (Some Vinput) 1;
-    do preg <- create_reg None 128;
-    do _stmnt <- collectlist (transf_seq_blockM fin rtrn stack preg) (Maps.PTree.elements f.(GiblePar.fn_code));
-    do _stmnt' <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(GiblePar.fn_params);
-    do _stmnt'' <- collectlist declare_all_regs (Maps.PTree.elements f.(GiblePar.fn_code));
-    do current_state <- get;
-    match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
-          decide_order (st_st current_state) fin rtrn stack start rst clk preg,
-          max_list_dec (GiblePar.fn_params f) (st_st current_state)
+    let st := Pos.succ (max_reg_function f) in
+    let fin := Pos.succ st in
+    let rtrn := Pos.succ fin in
+    let stack := Pos.succ rtrn in
+    let start := Pos.succ stack in
+    let rst := Pos.succ start in
+    let clk := Pos.succ rst in
+    let preg := Pos.succ clk in 
+    do _stmnt <- mfold_left (transf_seq_blockM (mk_control_regs st stack preg fin rtrn)) 
+                            (Maps.PTree.elements f.(GiblePar.fn_code)) (ret (PTree.empty _));
+    match zle (Z.pos (max_pc_map _stmnt)) Integers.Int.max_unsigned,
+            decide_order st fin rtrn stack start rst clk preg,
+            max_list_dec (GiblePar.fn_params f) st
     with
     | left LEDATA, left MORD, left WFPARAMS =>
         ret (DHTL.mkmodule
            f.(GiblePar.fn_params)
-           current_state.(st_datapath)
+           _stmnt
            f.(fn_entrypoint)
-           current_state.(st_st)
+           st
            stack
-           stack_len
+           (Z.to_nat (f.(fn_stacksize) / 4))
            fin
            rtrn
            start
            rst
            clk
            preg
-           current_state.(st_scldecls)
-           current_state.(st_arrdecls)
+           (AssocMap.empty _)
+           (AssocMap.empty _)
            None
            (max_pc_wf _ LEDATA)
            MORD
            _
            WFPARAMS)
-    | _, _, _ => error (Errors.msg "More than 2^32 states.")
+    | _, _, _ => error "More than 2^32 states."
     end
-  else error (Errors.msg "Stack size misalignment.")); discriminate.
-Defined.
-
-Definition max_state (f: function) : state :=
-  let st := Pos.succ (max_reg_function f) in
-  mkstate st
-          (Pos.succ st)
-          (Pos.succ (max_pc_function f))
-          (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))
-          (st_arrdecls (init_state st))
-          (st_datapath (init_state st)).
-
-Definition transl_module (f : function) : Errors.res DHTL.module :=
-  run_mon (max_state f) (transf_module f).
+  else error "Stack size misalignment.".
 
 Definition transl_fundef := transf_partial_fundef transl_module.
 
diff --git a/src/hls/HTLPargenproof.v b/src/hls/HTLPargenproof.v
new file mode 100644
index 0000000..5c0272f
--- /dev/null
+++ b/src/hls/HTLPargenproof.v
@@ -0,0 +1,983 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2023 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Require Import Coq.micromega.Lia.
+
+Require Import compcert.lib.Maps.
+Require Import compcert.common.Errors.
+Require Import compcert.common.Globalenvs.
+Require compcert.backend.Registers.
+Require Import compcert.common.Linking.
+Require Import compcert.common.Memory.
+Require compcert.common.Globalenvs.
+Require Import compcert.lib.Integers.
+Require Import compcert.common.AST.
+
+Require Import vericert.common.IntegerExtra.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.common.ZExtra.
+Require Import vericert.hls.Array.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.DHTL.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.HTLPargen.
+Require Import vericert.hls.HTLPargen.
+Require Import vericert.hls.Predicate.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
+Require vericert.hls.Verilog.
+Require Import vericert.common.Errormonad.
+Import ErrorMonad.
+Import ErrorMonadExtra.
+
+Require Import Lia.
+
+Local Open Scope assocmap.
+
+#[local] Hint Resolve AssocMap.gss : htlproof.
+#[local] Hint Resolve AssocMap.gso : htlproof.
+
+#[local] Hint Unfold find_assocmap AssocMapExt.get_default : htlproof.
+
+Inductive match_assocmaps : GiblePar.function -> Gible.regset -> assocmap -> Prop :=
+  match_assocmap : forall f rs am,
+    (forall r, Ple r (max_reg_function f) ->
+               val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
+    match_assocmaps f rs am.
+#[local] Hint Constructors match_assocmaps : htlproof.
+
+Inductive match_arrs (m : DHTL.module) (f : GiblePar.function) (sp : Values.val) (mem : mem) :
+  Verilog.assocmap_arr -> Prop :=
+| match_arr : forall asa stack,
+    asa ! (m.(DHTL.mod_stk)) = Some stack /\
+    stack.(arr_length) = Z.to_nat (f.(GiblePar.fn_stacksize) / 4) /\
+    (forall ptr,
+        0 <= ptr < Z.of_nat m.(DHTL.mod_stk_len) ->
+        opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
+                                         (Values.Val.offset_ptr sp (Ptrofs.repr (4 * ptr))))
+                              (Option.default (NToValue 0)
+                                 (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
+    match_arrs m f sp mem asa.
+
+Definition stack_based (v : Values.val) (sp : Values.block) : Prop :=
+   match v with
+   | Values.Vptr sp' off => sp' = sp
+   | _ => True
+   end.
+
+Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop :=
+  forall r, stack_based (Registers.Regmap.get r rs) sp.
+
+Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z)
+  (sp : Values.val) : Prop :=
+  forall ptr,
+    0 <= ptr < (stack_length / 4) ->
+    stack_based (Option.default
+                   Values.Vundef
+                   (Mem.loadv AST.Mint32 m
+                              (Values.Val.offset_ptr sp (Ptrofs.repr (4 * ptr)))))
+                spb.
+
+Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop :=
+  forall ptr v,
+    hi <= ptr <= Ptrofs.max_unsigned ->
+    Z.modulo ptr 4 = 0 ->
+    Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Ptrofs.repr ptr )) = None /\
+    Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Ptrofs.repr ptr )) v = None.
+
+Inductive match_frames : list GiblePar.stackframe -> list DHTL.stackframe -> Prop :=
+| match_frames_nil :
+    match_frames nil nil.
+
+Inductive match_constants : DHTL.module -> assocmap -> Prop :=
+  match_constant :
+    forall m asr,
+      asr!(DHTL.mod_reset m) = Some (ZToValue 0) ->
+      asr!(DHTL.mod_finish m) = Some (ZToValue 0) ->
+      match_constants m asr.
+
+Definition state_st_wf (m : DHTL.module) (s : DHTL.state) :=
+  forall st asa asr res,
+  s = DHTL.State res m st asa asr ->
+  asa!(m.(DHTL.mod_st)) = Some (posToValue st).
+#[local] Hint Unfold state_st_wf : htlproof.
+
+Inductive match_states : GiblePar.state -> DHTL.state -> Prop :=
+| match_state : forall asa asr sf f sp sp' rs mem m st res ps
+    (MASSOC : match_assocmaps f rs asr)
+    (TF : transl_module f = Errors.OK m)
+    (WF : state_st_wf m (DHTL.State res m st asr asa))
+    (MF : match_frames sf res)
+    (MARR : match_arrs m f sp mem asa)
+    (SP : sp = Values.Vptr sp' (Ptrofs.repr 0))
+    (RSBP : reg_stack_based_pointers sp' rs)
+    (ASBP : arr_stack_based_pointers sp' mem (f.(GiblePar.fn_stacksize)) sp)
+    (BOUNDS : stack_bounds sp (f.(GiblePar.fn_stacksize)) mem)
+    (CONST : match_constants m asr),
+    (* Add a relation about ps compared with the state register. *)
+    match_states (GiblePar.State sf f sp st rs ps mem)
+                 (DHTL.State res m st asr asa)
+| match_returnstate :
+    forall
+      v v' stack mem res
+      (MF : match_frames stack res),
+      val_value_lessdef v v' ->
+      match_states (GiblePar.Returnstate stack v mem) (DHTL.Returnstate res v')
+| match_initial_call :
+    forall f m m0
+    (TF : transl_module f = Errors.OK m),
+      match_states (GiblePar.Callstate nil (AST.Internal f) nil m0) (DHTL.Callstate nil m nil).
+#[local] Hint Constructors match_states : htlproof.
+
+Definition match_prog (p: GiblePar.program) (tp: DHTL.program) :=
+  Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\
+  main_is_internal p = true.
+
+Ltac unfold_match H :=
+  match type of H with
+  | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate
+  end.
+
+#[global] Instance TransfHTLLink (tr_fun: GiblePar.program -> Errors.res DHTL.program):
+  TransfLink (fun (p1: GiblePar.program) (p2: DHTL.program) => match_prog p1 p2).
+Proof.
+  red. intros. exfalso. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
+  apply link_prog_inv in H.
+
+  unfold match_prog in *.
+  unfold main_is_internal in *. simplify. repeat (unfold_match H4).
+  repeat (unfold_match H3). simplify.
+  subst. rewrite H0 in *. specialize (H (AST.prog_main p2)).
+  exploit H.
+  apply Genv.find_def_symbol. exists b. split.
+  assumption. apply Genv.find_funct_ptr_iff. eassumption.
+  apply Genv.find_def_symbol. exists b0. split.
+  assumption. apply Genv.find_funct_ptr_iff. eassumption.
+  intros. inv H3. inv H5. destruct H6. inv H5.
+Qed.
+
+Definition match_prog' (p: GiblePar.program) (tp: DHTL.program) :=
+  Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
+
+Lemma match_prog_matches :
+  forall p tp, match_prog p tp -> match_prog' p tp.
+Proof. unfold match_prog. tauto. Qed.
+
+Lemma transf_program_match:
+  forall p tp, HTLPargen.transl_program p = Errors.OK tp -> match_prog p tp.
+Proof.
+  intros. unfold transl_program in H.
+  destruct (main_is_internal p) eqn:?; try discriminate.
+  unfold match_prog. split.
+  apply Linking.match_transform_partial_program; auto.
+  assumption.
+Qed.
+
+Lemma regs_lessdef_add_greater :
+  forall f rs1 rs2 n v,
+    Plt (max_reg_function f) n ->
+    match_assocmaps f rs1 rs2 ->
+    match_assocmaps f rs1 (AssocMap.set n v rs2).
+Proof.
+  inversion 2; subst.
+  intros. constructor.
+  intros. unfold find_assocmap. unfold AssocMapExt.get_default.
+  rewrite AssocMap.gso. eauto.
+  apply Pos.le_lt_trans with _ _ n in H2.
+  unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption.
+Qed.
+#[local] Hint Resolve regs_lessdef_add_greater : htlproof.
+
+Lemma regs_lessdef_add_match :
+  forall f rs am r v v',
+    val_value_lessdef v v' ->
+    match_assocmaps f rs am ->
+    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am).
+Proof.
+  inversion 2; subst.
+  constructor. intros.
+  destruct (peq r0 r); subst.
+  rewrite Registers.Regmap.gss.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
+  rewrite AssocMap.gss. assumption.
+
+  rewrite Registers.Regmap.gso; try assumption.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
+  rewrite AssocMap.gso; eauto.
+Qed.
+#[local] Hint Resolve regs_lessdef_add_match : htlproof.
+
+Lemma list_combine_none :
+  forall n l,
+    length l = n ->
+    list_combine Verilog.merge_cell (list_repeat None n) l = l.
+Proof.
+  induction n; intros; crush.
+  - symmetry. apply length_zero_iff_nil. auto.
+  - destruct l; crush.
+    rewrite list_repeat_cons.
+    crush. f_equal.
+    eauto.
+Qed.
+
+Lemma combine_none :
+  forall n a,
+    a.(arr_length) = n ->
+    arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a.
+Proof.
+  intros.
+  unfold combine.
+  crush.
+
+  rewrite <- (arr_wf a) in H.
+  apply list_combine_none.
+  assumption.
+Qed.
+
+Lemma list_combine_lookup_first :
+  forall l1 l2 n,
+    length l1 = length l2 ->
+    nth_error l1 n = Some None ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n.
+Proof.
+  induction l1; intros; crush.
+
+  rewrite nth_error_nil in H0.
+  discriminate.
+
+  destruct l2 eqn:EQl2. crush.
+  simpl in H. inv H.
+  destruct n; simpl in *.
+  inv H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_first :
+  forall a1 a2 n,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some None ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2.
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_first; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
+Lemma list_combine_lookup_second :
+  forall l1 l2 n x,
+    length l1 = length l2 ->
+    nth_error l1 n = Some (Some x) ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x).
+Proof.
+  induction l1; intros; crush; auto.
+
+  destruct l2 eqn:EQl2. crush.
+  simpl in H. inv H.
+  destruct n; simpl in *.
+  inv H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_second :
+  forall a1 a2 n x,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some (Some x) ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x).
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_second; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
+Ltac unfold_func H :=
+  match type of H with
+  | ?f = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ _ = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H)
+  end.
+
+Lemma init_reg_assoc_empty :
+  forall f l,
+    match_assocmaps f (Gible.init_regs nil l) (DHTL.init_regs nil l).
+Proof.
+  induction l; simpl; constructor; intros.
+  - rewrite Registers.Regmap.gi. unfold find_assocmap.
+    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
+    constructor.
+
+  - rewrite Registers.Regmap.gi. unfold find_assocmap.
+    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
+    constructor.
+Qed.
+
+Lemma arr_lookup_some:
+  forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr)
+    (stack : Array (option value)) (H5 : asa ! r = Some stack) n,
+    exists x, Verilog.arr_assocmap_lookup asa r n = Some x.
+Proof.
+  intros z r0 r asr asa stack H5 n.
+  eexists.
+  unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity.
+Qed.
+#[local] Hint Resolve arr_lookup_some : htlproof.
+
+Section CORRECTNESS.
+
+  Variable prog : GiblePar.program.
+  Variable tprog : DHTL.program.
+
+  Hypothesis TRANSL : match_prog prog tprog.
+
+  Lemma TRANSL' :
+    Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
+  Proof. intros; apply match_prog_matches; assumption. Qed.
+
+  Let ge : GiblePar.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : DHTL.genv := Globalenvs.Genv.globalenv tprog.
+
+  Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed.
+
+  Lemma function_ptr_translated:
+    forall (b: Values.block) (f: GiblePar.fundef),
+      Genv.find_funct_ptr ge b = Some f ->
+      exists tf,
+        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf.
+  Proof.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+
+  Lemma functions_translated:
+    forall (v: Values.val) (f: GiblePar.fundef),
+      Genv.find_funct ge v = Some f ->
+      exists tf,
+        Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf.
+  Proof.
+    intros. exploit (Genv.find_funct_match TRANSL'); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof
+    (Genv.senv_transf_partial TRANSL').
+  #[local] Hint Resolve senv_preserved : htlproof.
+
+  Lemma ptrofs_inj :
+    forall a b,
+      Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b.
+  Proof.
+    intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned.
+    rewrite H. auto.
+  Qed.
+
+  Lemma op_stack_based :
+    forall F V sp v m args rs op ge ver,
+      translate_instr op args = Errors.OK ver ->
+      reg_stack_based_pointers sp rs ->
+      @Op.eval_operation F V ge (Values.Vptr sp Ptrofs.zero) op
+                        (List.map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v ->
+      stack_based v sp.
+  Proof.
+    Ltac solve_no_ptr :=
+      match goal with
+      | H: reg_stack_based_pointers ?sp ?rs |- stack_based (Registers.Regmap.get ?r ?rs) _ =>
+        solve [apply H]
+      | H1: reg_stack_based_pointers ?sp ?rs, H2: Registers.Regmap.get _ _ = Values.Vptr ?b ?i
+        |- context[Values.Vptr ?b _] =>
+        let H := fresh "H" in
+        assert (H: stack_based (Values.Vptr b i) sp) by (rewrite <- H2; apply H1); simplify; solve [auto]
+      | |- context[Registers.Regmap.get ?lr ?lrs] =>
+        destruct (Registers.Regmap.get lr lrs) eqn:?; simplify; auto
+      | |- stack_based (?f _) _ => unfold f
+      | |- stack_based (?f _ _) _ => unfold f
+      | |- stack_based (?f _ _ _) _ => unfold f
+      | |- stack_based (?f _ _ _ _) _ => unfold f
+      | H: ?f _ _ = Some _ |- _ =>
+        unfold f in H; repeat (unfold_match H); inv H
+      | H: ?f _ _ _ _ _ _ = Some _ |- _ =>
+        unfold f in H; repeat (unfold_match H); inv H
+      | H: map (fun r : positive => Registers.Regmap.get r _) ?args = _ |- _ =>
+        destruct args; inv H
+      | |- context[if ?c then _ else _] => destruct c; try discriminate
+      | H: match _ with _ => _ end = Some _ |- _ => repeat (unfold_match H; try discriminate)
+      | H: match _ with _ => _ end = OK _ _ _ |- _ => repeat (unfold_match H; try discriminate)
+      | |- context[match ?g with _ => _ end] => destruct g; try discriminate
+      | |- _ => simplify; solve [auto]
+      end.
+    intros **.
+    unfold translate_instr in *.
+    unfold_match H; repeat (unfold_match H); simplify; try solve [repeat solve_no_ptr].
+    subst.
+    unfold translate_eff_addressing in H.
+    repeat (unfold_match H; try discriminate); simplify; try solve [repeat solve_no_ptr].
+  Qed.
+
+  Lemma int_inj :
+    forall x y,
+      Int.unsigned x = Int.unsigned y ->
+      x = y.
+  Proof.
+    intros. rewrite <- Int.repr_unsigned at 1. rewrite <- Int.repr_unsigned.
+    rewrite <- H. trivial.
+  Qed.
+
+  Lemma Ptrofs_compare_correct :
+    forall a b,
+      Ptrofs.ltu (valueToPtr a) (valueToPtr b) = Int.ltu a b.
+  Proof.
+    intros. unfold valueToPtr. unfold Ptrofs.ltu. unfold Ptrofs.of_int. unfold Int.ltu.
+    rewrite !Ptrofs.unsigned_repr in *; auto using Int.unsigned_range_2.
+  Qed.
+
+  Lemma eval_cond_correct :
+    forall stk f sp pc rs m res ml st asr asa e b f' args cond pr,
+      match_states (GiblePar.State stk f sp pc rs pr m) (DHTL.State res ml st asr asa) ->
+      (forall v, In v args -> Ple v (max_reg_function f)) ->
+      Op.eval_condition cond (List.map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b ->
+      translate_condition cond args = OK e ->
+      Verilog.expr_runp f' asr asa e (boolToValue b).
+  Proof.
+    intros * MSTATE MAX_FUN EVAL TR_INSTR.
+    unfold translate_condition, translate_comparison, translate_comparisonu, translate_comparison_imm, translate_comparison_immu in TR_INSTR.
+    repeat (destruct_match; try discriminate); subst; unfold ret in *; match goal with H: OK _ = OK _ |- _ => inv H end; unfold bop in *; cbn in *;
+     try (solve [econstructor; try econstructor; eauto; unfold binop_run;
+      unfold Values.Val.cmp_bool, Values.Val.cmpu_bool in EVAL; repeat (destruct_match; try discriminate); inv EVAL;
+      inv MSTATE; inv MASSOC;
+      assert (X: Ple p (max_reg_function f)) by eauto;
+      assert (X1: Ple p0 (max_reg_function f)) by eauto;
+      apply H in X; apply H in X1;
+      rewrite Heqv in X;
+      rewrite Heqv0 in X1;
+      inv X; inv X1; auto; try (rewrite Ptrofs_compare_correct; auto)|
+      econstructor; try econstructor; eauto; unfold binop_run;
+      unfold Values.Val.cmp_bool, Values.Val.cmpu_bool in EVAL; repeat (destruct_match; try discriminate); inv EVAL;
+      inv MSTATE; inv MASSOC;
+      assert (X: Ple p (max_reg_function f)) by eauto;
+        apply H in X;
+        rewrite Heqv in X;
+        inv X; auto]).
+  Qed.
+
+  Lemma eval_cond_correct' :
+    forall e stk f sp pc rs m res ml st asr asa v f' args cond pr,
+      match_states (GiblePar.State stk f sp pc rs pr m) (DHTL.State res ml st asr asa) ->
+      (forall v, In v args -> Ple v (max_reg_function f)) ->
+      Values.Val.of_optbool None = v ->
+      translate_condition cond args = OK e ->
+      exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
+  Proof.
+    intros * MSTATE MAX_FUN EVAL TR_INSTR.
+    unfold translate_condition, translate_comparison, translate_comparisonu,
+    translate_comparison_imm, translate_comparison_immu, bop, boplit in *.
+    repeat unfold_match TR_INSTR; inv TR_INSTR; repeat econstructor.
+  Qed.
+
+  Ltac eval_correct_tac :=
+      match goal with
+      | |- context[valueToPtr] => unfold valueToPtr
+      | |- context[valueToInt] => unfold valueToInt
+      | |- context[bop] => unfold bop
+      | H : context[bop] |- _ => unfold bop in H
+      | |- context[boplit] => unfold boplit
+      | H : context[boplit] |- _ => unfold boplit in H
+      | |- context[boplitz] => unfold boplitz
+      | H : context[boplitz] |- _ => unfold boplitz in H
+      | |- val_value_lessdef Values.Vundef _ => solve [constructor]
+      | H : val_value_lessdef _ _ |- val_value_lessdef (Values.Vint _) _ => constructor; inv H
+      | |- val_value_lessdef (Values.Vint _) _ => constructor; auto
+      | H : ret _ _ = OK _ _ _ |- _ => inv H
+      | H : _ :: _ = _ :: _ |- _ => inv H
+      | |- context[match ?d with _ => _ end] => destruct d eqn:?; try discriminate
+      | H : match ?d with _ => _ end = _ |- _ => repeat unfold_match H
+      | H : match ?d with _ => _ end _ = _ |- _ => repeat unfold_match H
+      | |- Verilog.expr_runp _ _ _ ?f _ =>
+        match f with
+        | Verilog.Vternary _ _ _ => idtac
+        | _ => econstructor
+        end
+      | |- val_value_lessdef (?f _ _) _ => unfold f
+      | |- val_value_lessdef (?f _) _ => unfold f
+      | H : ?f (Registers.Regmap.get _ _) _ = Some _ |- _ =>
+        unfold f in H; repeat (unfold_match H)
+      | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _, H2 : val_value_lessdef (Registers.Regmap.get ?r ?rs) _
+        |- _ => rewrite H1 in H2; inv H2
+      | |- _ => eexists; split; try constructor; solve [eauto]
+      | |- context[if ?c then _ else _] => destruct c eqn:?; try discriminate
+      | H : ?b = _ |- _ = boolToValue ?b => rewrite H
+      end.
+
+  Lemma eval_correct_Oshrximm :
+    forall sp rs m v e asr asa f f' stk pc args res ml st n pr,
+      match_states (GiblePar.State stk f sp pc rs pr m) (DHTL.State res ml st asr asa) ->
+      Forall (fun x => (Ple x (max_reg_function f))) args ->
+      Op.eval_operation ge sp (Op.Oshrximm n)
+                        (List.map (fun r : BinNums.positive =>
+                                     Registers.Regmap.get r rs) args) m = Some v ->
+      translate_instr (Op.Oshrximm n) args = OK e ->
+      exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
+  Proof.
+    intros * MSTATE INSTR EVAL TR_INSTR.
+    pose proof MSTATE as MSTATE_2. inv MSTATE.
+    inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR;
+    unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL.
+    (*repeat (simplify; eval_correct_tac; unfold valueToInt in * ).
+            destruct (Z_lt_ge_dec (Int.signed i0) 0).
+            econstructor.*)
+    unfold Values.Val.shrx in *.
+    destruct v0; try discriminate.
+    destruct (Int.ltu n (Int.repr 31)) eqn:?; try discriminate.
+    inversion H1. clear H1.
+    assert (Int.unsigned n <= 30).
+    { unfold Int.ltu in *. destruct (zlt (Int.unsigned n) (Int.unsigned (Int.repr 31))); try discriminate.
+      rewrite Int.unsigned_repr in l by (simplify; lia).
+      replace 31 with (Z.succ 30) in l by auto.
+      apply Zlt_succ_le in l.
+      auto.
+    }
+    rewrite IntExtra.shrx_shrx_alt_equiv in H2 by auto.
+    unfold IntExtra.shrx_alt in *.
+    destruct (zlt (Int.signed i) 0).
+    - repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue;
+      repeat (simplify; eval_correct_tac).
+      unfold valueToInt in *. inv INSTR. apply H in H4. rewrite H3 in H4.
+      inv H4. clear H5.
+      unfold Int.lt in *. rewrite zlt_true in Heqb0. simplify.
+      rewrite Int.unsigned_repr in Heqb0. discriminate.
+      simplify; lia.
+      unfold ZToValue. rewrite Int.signed_repr by (simplify; lia).
+      auto.
+      rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_true; try lia.
+      simplify. inv INSTR. clear H5.  apply H in H4. rewrite H3 in H4. inv H4. auto.
+    - econstructor; econstructor; [eapply Verilog.erun_Vternary_false|idtac]; repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue;
+      repeat (simplify; eval_correct_tac).
+      inv INSTR. clear H5. apply H in H4. rewrite H3 in H4.
+      inv H4.
+      unfold Int.lt in *. rewrite zlt_false in Heqb0. simplify.
+      rewrite Int.unsigned_repr in Heqb0. lia.
+      simplify; lia.
+      unfold ZToValue. rewrite Int.signed_repr by (simplify; lia).
+      auto.
+      rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_false; try lia.
+      simplify. inv INSTR. apply H in H4. unfold valueToInt in *. rewrite H3 in H4. inv H4. auto.
+  Qed.
+
+  Lemma max_reg_function_use:
+    forall l y m,
+      Forall (fun x => Ple x m) l ->
+      In y l ->
+      Ple y m.
+  Proof. 
+    intros. eapply Forall_forall in H; eauto.
+  Qed.
+
+  Ltac eval_correct_tac' :=
+      match goal with
+      | |- context[valueToPtr] => unfold valueToPtr
+      | |- context[valueToInt] => unfold valueToInt
+      | |- context[bop] => unfold bop
+      | H : context[bop] |- _ => unfold bop in H
+      | |- context[boplit] => unfold boplit
+      | H : context[boplit] |- _ => unfold boplit in H
+      | |- context[boplitz] => unfold boplitz
+      | H : context[boplitz] |- _ => unfold boplitz in H
+      | |- val_value_lessdef Values.Vundef _ => solve [constructor]
+      | H : val_value_lessdef _ _ |- val_value_lessdef (Values.Vint _) _ => constructor; inv H
+      | |- val_value_lessdef (Values.Vint _) _ => constructor; auto
+      | H : ret _ _ = OK _ _ _ |- _ => inv H
+      | H : context[max_reg_function ?f]
+        |- context[_ (Registers.Regmap.get ?r ?rs) (Registers.Regmap.get ?r0 ?rs)] =>
+        let HPle1 := fresh "HPle" in
+        let HPle2 := fresh "HPle" in
+        assert (HPle1 : Ple r (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto]));
+        assert (HPle2 : Ple r0 (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto]));
+        apply H in HPle1; apply H in HPle2; eexists; split;
+        [econstructor; eauto; constructor; trivial | inv HPle1; inv HPle2; try (constructor; auto)]
+      | H : context[max_reg_function ?f]
+        |- context[_ (Registers.Regmap.get ?r ?rs) _] =>
+        let HPle1 := fresh "HPle" in
+        assert (HPle1 : Ple r (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto]));
+        apply H in HPle1; eexists; split;
+        [econstructor; eauto; constructor; trivial | inv HPle1; try (constructor; auto)]
+      | H : _ :: _ = _ :: _ |- _ => inv H
+      | |- context[match ?d with _ => _ end] => destruct d eqn:?; try discriminate
+      | H : match ?d with _ => _ end = _ |- _ => repeat unfold_match H
+      | H : match ?d with _ => _ end _ = _ |- _ => repeat unfold_match H
+      | |- Verilog.expr_runp _ _ _ ?f _ =>
+        match f with
+        | Verilog.Vternary _ _ _ => idtac
+        | _ => econstructor
+        end
+      | |- val_value_lessdef (?f _ _) _ => unfold f
+      | |- val_value_lessdef (?f _) _ => unfold f
+      | H : ?f (Registers.Regmap.get _ _) _ = Some _ |- _ =>
+        unfold f in H; repeat (unfold_match H)
+      | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _, H2 : val_value_lessdef (Registers.Regmap.get ?r ?rs) _
+        |- _ => rewrite H1 in H2; inv H2
+      | |- _ => eexists; split; try constructor; solve [eauto]
+      | H : context[max_reg_function ?f] |- context[_ (Verilog.Vvar ?r) (Verilog.Vvar ?r0)] =>
+        let HPle1 := fresh "H" in
+        let HPle2 := fresh "H" in
+        assert (HPle1 : Ple r (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto]));
+        assert (HPle2 : Ple r0 (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto]));
+        apply H in HPle1; apply H in HPle2; eexists; split; try constructor; eauto
+      | H : context[max_reg_function ?f] |- context[Verilog.Vvar ?r] =>
+        let HPle := fresh "H" in
+        assert (HPle : Ple r (max_reg_function f)) by (eapply max_reg_function_use; eauto; simpl; auto; repeat (apply in_cons; try solve [constructor; auto]));
+        apply H in HPle; eexists; split; try constructor; eauto
+      | |- context[if ?c then _ else _] => destruct c eqn:?; try discriminate
+      | H : ?b = _ |- _ = boolToValue ?b => rewrite H
+      end.
+
+  Lemma int_unsigned_lt_ptrofs_max :
+    forall a,
+      0 <= Int.unsigned a <= Ptrofs.max_unsigned.
+  Proof.
+    intros. pose proof (Int.unsigned_range_2 a).
+    assert (Int.max_unsigned = Ptrofs.max_unsigned) by auto.
+    lia.
+  Qed.
+
+  Lemma ptrofs_unsigned_lt_int_max :
+    forall a,
+      0 <= Ptrofs.unsigned a <= Int.max_unsigned.
+  Proof.
+    intros. pose proof (Ptrofs.unsigned_range_2 a).
+    assert (Int.max_unsigned = Ptrofs.max_unsigned) by auto.
+    lia.
+  Qed.
+
+  Hint Resolve int_unsigned_lt_ptrofs_max : int_ptrofs.
+  Hint Resolve ptrofs_unsigned_lt_int_max : int_ptrofs.
+  Hint Resolve Ptrofs.unsigned_range_2 : int_ptrofs.
+  Hint Resolve Int.unsigned_range_2 : int_ptrofs.
+
+(* Ptrofs.agree32_of_int_eq: forall (a : ptrofs) (b : int), Ptrofs.agree32 a b -> Ptrofs.of_int b = a *)
+(* Ptrofs.agree32_of_int: Archi.ptr64 = false -> forall b : int, Ptrofs.agree32 (Ptrofs.of_int b) b *)
+(* Ptrofs.agree32_sub: *)
+(*   Archi.ptr64 = false -> *)
+(*   forall (a1 : ptrofs) (b1 : int) (a2 : ptrofs) (b2 : int), *)
+(*   Ptrofs.agree32 a1 b1 -> Ptrofs.agree32 a2 b2 -> Ptrofs.agree32 (Ptrofs.sub a1 a2) (Int.sub b1 b2) *)
+  Lemma eval_correct_sub :
+    forall a b a' b',
+      val_value_lessdef a a' ->
+      val_value_lessdef b b' ->
+      val_value_lessdef (Values.Val.sub a b) (Int.sub a' b').
+  Proof.
+    intros * HPLE HPLE0.
+    assert (ARCHI: Archi.ptr64 = false) by auto.
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto].
+    - rewrite ARCHI. constructor. unfold valueToPtr.
+      apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr; auto with int_ptrofs.
+      apply Ptrofs.agree32_sub; auto; rewrite <- Int.repr_unsigned; now apply Ptrofs.agree32_repr.
+    - rewrite ARCHI. destruct_match; constructor.
+      unfold Ptrofs.to_int. unfold valueToInt.
+      apply int_inj. rewrite Int.unsigned_repr; auto with int_ptrofs.
+      apply Ptrofs.agree32_sub; auto; unfold valueToPtr; now apply Ptrofs.agree32_of_int.
+  Qed.
+
+  Lemma eval_correct_mul :
+    forall a b a' b',
+      val_value_lessdef a a' ->
+      val_value_lessdef b b' ->
+      val_value_lessdef (Values.Val.mul a b) (Int.mul a' b').
+  Proof.
+    intros * HPLE HPLE0.
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto].
+  Qed.
+
+  Lemma eval_correct_mul' :
+    forall a a' n,
+      val_value_lessdef a a' ->
+      val_value_lessdef (Values.Val.mul a (Values.Vint n)) (Int.mul a' (intToValue n)).
+  Proof.
+    intros * HPLE.
+    inv HPLE; cbn in *; unfold valueToInt; try solve [constructor; auto].
+  Qed.
+
+  Lemma eval_correct_and :
+    forall a b a' b',
+      val_value_lessdef a a' ->
+      val_value_lessdef b b' ->
+      val_value_lessdef (Values.Val.and a b) (Int.and a' b').
+  Proof.
+    intros * HPLE HPLE0.
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto].
+  Qed.
+
+  Lemma eval_correct_and' :
+    forall a a' n,
+      val_value_lessdef a a' ->
+      val_value_lessdef (Values.Val.and a (Values.Vint n)) (Int.and a' (intToValue n)).
+  Proof.
+    intros * HPLE.
+    inv HPLE; cbn in *; unfold valueToInt; try solve [constructor; auto].
+  Qed.
+
+  Lemma eval_correct_or :
+    forall a b a' b',
+      val_value_lessdef a a' ->
+      val_value_lessdef b b' ->
+      val_value_lessdef (Values.Val.or a b) (Int.or a' b').
+  Proof.
+    intros * HPLE HPLE0.
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto].
+  Qed.
+
+  Lemma eval_correct_or' :
+    forall a a' n,
+      val_value_lessdef a a' ->
+      val_value_lessdef (Values.Val.or a (Values.Vint n)) (Int.or a' (intToValue n)).
+  Proof.
+    intros * HPLE.
+    inv HPLE; cbn in *; unfold valueToInt; try solve [constructor; auto].
+  Qed.
+
+  Lemma eval_correct_xor :
+    forall a b a' b',
+      val_value_lessdef a a' ->
+      val_value_lessdef b b' ->
+      val_value_lessdef (Values.Val.xor a b) (Int.xor a' b').
+  Proof.
+    intros * HPLE HPLE0.
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try solve [constructor; auto].
+  Qed.
+
+  Lemma eval_correct_xor' :
+    forall a a' n,
+      val_value_lessdef a a' ->
+      val_value_lessdef (Values.Val.xor a (Values.Vint n)) (Int.xor a' (intToValue n)).
+  Proof.
+    intros * HPLE.
+    inv HPLE; cbn in *; unfold valueToInt; try solve [constructor; auto].
+  Qed.
+
+  Lemma eval_correct_shl :
+    forall a b a' b',
+      val_value_lessdef a a' ->
+      val_value_lessdef b b' ->
+      val_value_lessdef (Values.Val.shl a b) (Int.shl a' b').
+  Proof.
+    intros * HPLE HPLE0.
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try destruct_match; now constructor.
+  Qed.
+
+  Lemma eval_correct_shl' :
+    forall a a' n,
+      val_value_lessdef a a' ->
+      val_value_lessdef (Values.Val.shl a (Values.Vint n)) (Int.shl a' (intToValue n)).
+  Proof.
+    intros * HPLE.
+    inv HPLE; cbn in *; unfold valueToInt; try destruct_match; now constructor.
+  Qed.
+
+  Lemma eval_correct_shr :
+    forall a b a' b',
+      val_value_lessdef a a' ->
+      val_value_lessdef b b' ->
+      val_value_lessdef (Values.Val.shr a b) (Int.shr a' b').
+  Proof.
+    intros * HPLE HPLE0.
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try destruct_match; now constructor.
+  Qed.
+
+  Lemma eval_correct_shr' :
+    forall a a' n,
+      val_value_lessdef a a' ->
+      val_value_lessdef (Values.Val.shr a (Values.Vint n)) (Int.shr a' (intToValue n)).
+  Proof.
+    intros * HPLE.
+    inv HPLE; cbn in *; unfold valueToInt; try destruct_match; now constructor.
+  Qed.
+
+  Lemma eval_correct_shru :
+    forall a b a' b',
+      val_value_lessdef a a' ->
+      val_value_lessdef b b' ->
+      val_value_lessdef (Values.Val.shru a b) (Int.shru a' b').
+  Proof.
+    intros * HPLE HPLE0.
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; try destruct_match; now constructor.
+  Qed.
+
+  Lemma eval_correct_shru' :
+    forall a a' n,
+      val_value_lessdef a a' ->
+      val_value_lessdef (Values.Val.shru a (Values.Vint n)) (Int.shru a' (intToValue n)).
+  Proof.
+    intros * HPLE.
+    inv HPLE; cbn in *; unfold valueToInt; try destruct_match; now constructor.
+  Qed.
+
+  Lemma eval_correct_add :
+    forall a b a' b',
+      val_value_lessdef a a' ->
+      val_value_lessdef b b' ->
+      val_value_lessdef (Values.Val.add a b) (Int.add a' b').
+  Proof.
+    intros * HPLE HPLE0.
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; 
+    try destruct_match; constructor; auto; unfold valueToPtr;
+    unfold Ptrofs.of_int; apply ptrofs_inj; 
+    rewrite Ptrofs.unsigned_repr by auto with int_ptrofs;
+    [rewrite Int.add_commut|]; apply Ptrofs.agree32_add; auto; 
+    rewrite <- Int.repr_unsigned; now apply Ptrofs.agree32_repr.
+  Qed.
+
+  Lemma eval_correct_add' :
+    forall a a' n,
+      val_value_lessdef a a' ->
+      val_value_lessdef (Values.Val.add a (Values.Vint n)) (Int.add a' (intToValue n)).
+  Proof.
+    intros * HPLE.
+    inv HPLE; cbn in *; unfold valueToInt; try destruct_match; try constructor; auto.
+    unfold valueToPtr. apply ptrofs_inj. unfold Ptrofs.of_int. 
+    rewrite Ptrofs.unsigned_repr by auto with int_ptrofs.
+    apply Ptrofs.agree32_add; auto. rewrite <- Int.repr_unsigned.
+    apply Ptrofs.agree32_repr; auto.
+    unfold intToValue. rewrite <- Int.repr_unsigned.
+    apply Ptrofs.agree32_repr; auto.
+  Qed.
+
+  Lemma eval_correct :
+    forall sp op rs m v e asr asa f f' stk pc args res ml st pr,
+      match_states (GiblePar.State stk f sp pc rs pr m) (DHTL.State res ml st asr asa) ->
+      Forall (fun x => (Ple x (max_reg_function f))) args ->
+      Op.eval_operation ge sp op
+                        (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
+      translate_instr op args = OK e ->
+      exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
+  Proof.
+    intros * MSTATE INSTR EVAL TR_INSTR.
+    pose proof MSTATE as MSTATE_2. inv MSTATE.
+    inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR;
+    unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL;
+    repeat (simplify; eval_correct_tac; unfold valueToInt in *);  
+    repeat (apply Forall_cons_iff in INSTR; destruct INSTR as (?HPLE & INSTR));
+      try (apply H in HPLE); try (apply H in HPLE0).
+    - do 2 econstructor; eauto. repeat econstructor.
+    - do 2 econstructor; eauto. repeat econstructor. cbn.
+      inv HPLE; cbn; try solve [constructor]; unfold valueToInt in *.
+      constructor; unfold valueToInt; auto.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_sub.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_mul.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_mul'.
+    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
+      do 2 econstructor; eauto. repeat econstructor. unfold binop_run.
+      rewrite Heqb. auto. constructor; auto.
+    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
+      do 2 econstructor; eauto. repeat econstructor. unfold binop_run.
+      rewrite Heqb. auto. constructor; auto.
+    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
+      do 2 econstructor; eauto. repeat econstructor. unfold binop_run.
+      rewrite Heqb. auto. constructor; auto.
+    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
+      do 2 econstructor; eauto. repeat econstructor. unfold binop_run.
+      rewrite Heqb. auto. constructor; auto.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_and.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_and'.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_or.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_or'.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_xor.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_xor'.
+    - do 2 econstructor; eauto. repeat econstructor. cbn. inv HPLE; now constructor.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shl.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shl'.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr'.
+    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. 
+      assert (0 <= 31 <= Int.max_unsigned). 
+      { pose proof Int.two_wordsize_max_unsigned as Y. 
+        unfold Int.zwordsize, Int.wordsize, Wordsize_32.wordsize in Y. lia. }
+      assert (Int.unsigned n <= 30).
+      { unfold Int.ltu in Heqb. destruct_match; try discriminate.
+        clear Heqs. rewrite Int.unsigned_repr in l by auto. lia. }
+      rewrite IntExtra.shrx_shrx_alt_equiv by auto.
+      case_eq (Int.lt (asr # p) (ZToValue 0)); intros HLT.
+      + assert ((if zlt (Int.signed (valueToInt asr # p)) 0 then true else false) = true).
+        { destruct_match; auto; unfold valueToInt in *. exfalso.
+          assert (Int.signed asr # p < 0 -> False) by auto. apply H2. unfold Int.lt in HLT.
+          destruct_match; try discriminate. auto. }
+        destruct_match; try discriminate.
+        do 2 econstructor; eauto. repeat econstructor. now rewrite HLT.
+        constructor; cbn. unfold IntExtra.shrx_alt. rewrite Heqs. auto.
+      + assert ((if zlt (Int.signed (valueToInt asr # p)) 0 then true else false) = false).
+        { destruct_match; auto; unfold valueToInt in *. exfalso.
+          assert (Int.signed asr # p >= 0 -> False) by auto. apply H2. unfold Int.lt in HLT.
+          destruct_match; try discriminate. auto. }
+        destruct_match; try discriminate.
+        do 2 econstructor; eauto. eapply erun_Vternary_false; repeat econstructor. 
+        now rewrite HLT.
+        constructor; cbn. unfold IntExtra.shrx_alt. rewrite Heqs. auto.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shru.
+    - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shru'.
+    - unfold translate_eff_addressing in H1. 
+      repeat (destruct_match; try discriminate); unfold boplitz in *; simplify;
+          repeat (apply Forall_cons_iff in INSTR; destruct INSTR as (?HPLE & INSTR));
+      try (apply H in HPLE); try (apply H in HPLE0).
+      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+        now apply eval_correct_add'.
+      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+        apply eval_correct_add; auto. apply eval_correct_add; auto.
+        constructor; auto.
+      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+        apply eval_correct_add; try constructor; auto. 
+        apply eval_correct_mul; try constructor; auto. 
+      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+        apply eval_correct_add; try constructor; auto.
+        apply eval_correct_add; try constructor; auto. 
+        apply eval_correct_mul; try constructor; auto. 
+      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+        assert (X: Archi.ptr64 = false) by auto.
+        rewrite X in H2. inv H2.
+        constructor. unfold valueToPtr. unfold Ptrofs.of_int.
+        rewrite Int.unsigned_repr by auto with int_ptrofs.
+        rewrite Ptrofs.repr_unsigned. apply Ptrofs.add_zero_l.
+    - remember (Op.eval_condition cond (List.map (fun r : positive => rs !! r) args) m).
+      destruct o. cbn. symmetry in Heqo.
+      exploit eval_cond_correct; eauto. intros. apply Forall_forall with (x := v) in INSTR; auto.
+      intros. econstructor. split. eauto. destruct b; constructor; auto.
+      exploit eval_cond_correct'; eauto.
+      intros. apply Forall_forall with (x := v) in INSTR; auto.
+    - assert (HARCHI: Archi.ptr64 = false) by auto.
+      unfold Errors.bind in *. destruct_match; try discriminate; []. inv H1.
+      remember (Op.eval_condition c (List.map (fun r : positive => rs !! r) l0) m).
+      destruct o; cbn; symmetry in Heqo.
+      + exploit eval_cond_correct; eauto. intros. apply Forall_forall with (x := v) in INSTR; auto.
+        intros. destruct b.
+        * intros. econstructor. split. econstructor. eauto. econstructor; auto. auto.
+          unfold Values.Val.normalize. rewrite HARCHI. destruct_match; auto; constructor.
+        * intros. econstructor. split. eapply erun_Vternary_false; repeat econstructor. eauto. auto.
+          unfold Values.Val.normalize. rewrite HARCHI. destruct_match; auto; constructor.
+      + exploit eval_cond_correct'; eauto.
+        intros. apply Forall_forall with (x := v) in INSTR; auto. simplify.
+        case_eq (valueToBool x); intros HVALU.
+        * econstructor. econstructor. econstructor. eauto. constructor. eauto. auto. constructor.
+        * econstructor. econstructor. eapply erun_Vternary_false. eauto. constructor. eauto. auto. constructor.
+  Qed.
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index d4bc80a..7786c5d 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -161,6 +161,8 @@ Section PRED_DEFINITION.
 
 End PRED_DEFINITION.
 
+Definition dfltp {A} (p: option (@Predicate.pred_op A)) := Option.default Ptrue p.
+
 Notation "A ∧ B" := (Pand A B) (at level 20) : pred_op.
 Notation "A ∨ B" := (Por A B) (at level 25) : pred_op.
 Notation "⟂" := (Pfalse) : pred_op.