Finish istore and iload without any admits

2 files changed, 115 insertions, 119 deletions

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 4e2598f..5aa6628 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -1305,18 +1305,7 @@ Section CORRECTNESS.
       apply regs_lessdef_add_match; big_tac.
 
       (** Equality proof *)
-      match goal with (* Prevents issues with evars *)
-      | [ |- context [valueToNat ?x] ] =>
-        assert (Z.to_nat
-                  (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divu
-                        OFFSET
-                        (Integers.Ptrofs.repr 4)))
-                =
-                valueToNat x)
-          as EXPR_OK by admit
-      end.
-      rewrite <- EXPR_OK.
+      rewrite <- offset_expr_ok_3.
 
       specialize (H9 (Integers.Ptrofs.unsigned
                         (Integers.Ptrofs.divu
@@ -1330,7 +1319,26 @@ Section CORRECTNESS.
                           (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
       exploit ASBP; big_tac.
       rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
-  Admitted.
+
+      constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso.
+      assumption. lia.
+      assert (HPle: Ple dst (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
+      unfold Ple in HPle. lia.
+      rewrite AssocMap.gso. rewrite AssocMap.gso.
+      assumption. lia.
+      assert (HPle: Ple dst (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
+      unfold Ple in HPle. lia.
+
+      Unshelve.
+      exact (Values.Vint (Int.repr 0)).
+      exact tt.
+      exact (Values.Vint (Int.repr 0)).
+      exact tt.
+      exact (Values.Vint (Int.repr 0)).
+      exact tt.
+  Qed.
   Hint Resolve transl_iload_correct : htlproof.
 
   Lemma transl_istore_correct:
@@ -1428,17 +1436,6 @@ Section CORRECTNESS.
       apply AssocMap.gss.
 
       (** Equality proof *)
-      match goal with
-      | [ |- context [valueToNat ?x] ] =>
-        assert (Z.to_nat
-                  (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divu
-                        OFFSET
-                        (Integers.Ptrofs.repr 4)))
-                =
-                valueToNat x)
-          as EXPR_OK by admit
-      end.
 
       assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
       inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
@@ -1498,11 +1495,12 @@ Section CORRECTNESS.
       rewrite Z_div_mult in HMul; try lia.
       replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in HMul by reflexivity.
       rewrite <- PtrofsExtra.divu_unsigned in HMul; unfold_constants; try lia.
-      rewrite HMul. rewrite EXPR_OK.
+      rewrite HMul. rewrite <- offset_expr_ok.
+      rewrite HeqOFFSET.
       rewrite array_get_error_set_bound.
       reflexivity.
       unfold arr_length, arr_repeat. simpl.
-      rewrite list_repeat_len. lia.
+      rewrite list_repeat_len. rewrite HeqOFFSET in HMul. lia.
 
       erewrite Mem.load_store_other with (m1 := m).
       2: { exact H1. }
@@ -1526,7 +1524,7 @@ Section CORRECTNESS.
            apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
 
-      rewrite <- EXPR_OK.
+      rewrite <- offset_expr_ok.
       rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
       destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
       apply Z.mul_cancel_r with (p := 4) in e; try lia.
@@ -1545,18 +1543,20 @@ Section CORRECTNESS.
       lia.
       unfold_constants.
       intro.
-      apply Z2Nat.inj_iff in H14; try lia.
+      Search (Z.to_nat _ = Z.to_nat _).
+      apply Z2Nat.inj_iff in H14; rewrite HeqOFFSET in n0; try lia.
       apply Z.div_pos; try lia.
       apply Integers.Ptrofs.unsigned_range.
+      apply Integers.Ptrofs.unsigned_range_2.
 
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity.
       unfold arr_stack_based_pointers.
       intros.
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
 
       crush.
       erewrite Mem.load_store_same.
-      2: { rewrite ZERO.
+      2: { rewrite ZERO1.
            rewrite Integers.Ptrofs.add_zero_l.
            rewrite e.
            rewrite Integers.Ptrofs.unsigned_repr.
@@ -1571,12 +1571,15 @@ Section CORRECTNESS.
       simpl.
       erewrite Mem.load_store_other with (m1 := m).
       2: { exact H1. }
-      2: { (*right.
-           rewrite ZERO.
+      2: { right.
+           rewrite ZERO1.
            rewrite Integers.Ptrofs.add_zero_l.
            rewrite Integers.Ptrofs.unsigned_repr.
            simpl.
            destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+           rewrite HeqOFFSET in *. simplify_val.
+           left; auto.
+           rewrite HeqOFFSET in *. simplify_val.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
@@ -1584,8 +1587,7 @@ Section CORRECTNESS.
            apply Zmult_lt_compat_r with (p := 4) in H15; try lia.
            rewrite ZLib.div_mul_undo in H15; try lia.
            split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.*)
-        admit.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
       apply ASBP; assumption.
 
@@ -1598,7 +1600,7 @@ Section CORRECTNESS.
            rewrite ZERO.
            rewrite Integers.Ptrofs.add_zero_l.
            rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
-           apply ZExtra.mod_0_bounds; crush; try lia. admit. admit. }
+           apply ZExtra.mod_0_bounds; crush; try lia. }
       crush.
       exploit (BOUNDS ptr); try lia. intros. crush.
       exploit (BOUNDS ptr v); try lia. intros.
@@ -1624,7 +1626,7 @@ Section CORRECTNESS.
       assumption. lia.
 
     + (** Preamble *)
-      invert MARR. crush.
+      invert MARR. inv CONST. crush.
 
       unfold Op.eval_addressing in H0.
       destruct (Archi.ptr64) eqn:ARCHI; crush.
@@ -1648,13 +1650,13 @@ Section CORRECTNESS.
         by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
       assert (HPler1 : Ple r1 (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-      apply H6 in HPler0.
-      apply H8 in HPler1.
+      apply H8 in HPler0.
+      apply H11 in HPler1.
       invert HPler0; invert HPler1; try congruence.
-      rewrite EQr0 in H9.
-      rewrite EQr1 in H11.
-      invert H9. invert H11.
-      clear H0. clear H6. clear H8.
+      rewrite EQr0 in H13.
+      rewrite EQr1 in H14.
+      invert H13. invert H14.
+      clear H0. clear H8. clear H11.
 
       unfold check_address_parameter_signed in *;
       unfold check_address_parameter_unsigned in *; crush.
@@ -1666,17 +1668,8 @@ Section CORRECTNESS.
 
       (** Modular preservation proof *)
       assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; crush; try lia.
-        rewrite Integers.Ptrofs.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush.
-        apply PtrofsExtra.of_int_mod.
-        apply IntExtra.add_mod; crush.
-        apply IntExtra.mul_mod2; crush.
-        rewrite Integers.Int.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush.
-        rewrite Integers.Int.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush. }
+      { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify.
+        apply Zdivide_mod. assumption. }
 
       (** Write bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
@@ -1690,16 +1683,11 @@ Section CORRECTNESS.
       eexists. split.
       eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
-      apply assumption_32bit.
       econstructor. econstructor. econstructor.
       eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor.
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]).
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]).
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]).
       econstructor. econstructor. econstructor. econstructor.
       econstructor.
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]).
       econstructor. econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
@@ -1713,7 +1701,6 @@ Section CORRECTNESS.
       apply AssocMap.gss.
 
       (** Match states *)
-      rewrite assumption_32bit.
       econstructor; eauto.
 
       (** Match assocmaps *)
@@ -1729,17 +1716,6 @@ Section CORRECTNESS.
       apply AssocMap.gss.
 
       (** Equality proof *)
-      assert (Z.to_nat
-                (Integers.Ptrofs.unsigned
-                   (Integers.Ptrofs.divu
-                      OFFSET
-                      (Integers.Ptrofs.repr 4)))
-              =
-              valueToNat (vdiv
-                            (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12)
-                                   ?EQ10) (ZToValue 32 4) ?EQ9))
-        as EXPR_OK by admit.
-
       assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
       inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
 
@@ -1755,7 +1731,7 @@ Section CORRECTNESS.
       rewrite AssocMap.gss.
       unfold Verilog.merge_arr.
       rewrite AssocMap.gss.
-      setoid_rewrite H5.
+      setoid_rewrite H7.
       reflexivity.
 
       rewrite combine_length.
@@ -1779,6 +1755,7 @@ Section CORRECTNESS.
            rewrite Integers.Ptrofs.add_zero_l.
            rewrite e.
            rewrite Integers.Ptrofs.unsigned_repr.
+           rewrite HeqOFFSET.
            exact H1.
            apply Integers.Ptrofs.unsigned_range_2. }
       constructor.
@@ -1786,19 +1763,20 @@ Section CORRECTNESS.
       simpl.
       assert (Ple src (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H0 in H16.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H16; eauto.
+      apply H0 in H17.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H17; eauto.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
       rewrite list_repeat_len. auto.
 
       assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in H16.
-      rewrite Z_div_mult in H16; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H16 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H16; unfold_constants; try lia.
-      rewrite H16. rewrite EXPR_OK.
+      rewrite Z.mul_comm in H17.
+      rewrite Z_div_mult in H17; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H17 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H17; unfold_constants; try lia.
+      rewrite H17. rewrite <- offset_expr_ok_2.
+      rewrite HeqOFFSET in *.
       rewrite array_get_error_set_bound.
       reflexivity.
       unfold arr_length, arr_repeat. simpl.
@@ -1812,23 +1790,26 @@ Section CORRECTNESS.
            rewrite Integers.Ptrofs.unsigned_repr.
            simpl.
            destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+           rewrite HeqOFFSET in *. simplify_val.
+           left; auto.
+           rewrite HeqOFFSET in *. simplify_val.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
-           rewrite Z2Nat.id in H18; try lia.
-           apply Zmult_lt_compat_r with (p := 4) in H18; try lia.
-           rewrite ZLib.div_mul_undo in H18; try lia.
+           rewrite Z2Nat.id in H19; try lia.
+           apply Zmult_lt_compat_r with (p := 4) in H19; try lia.
+           rewrite ZLib.div_mul_undo in H19; try lia.
            split; try lia.
            apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
 
-      rewrite <- EXPR_OK.
+      rewrite <- offset_expr_ok_2.
       rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
       destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
       apply Z.mul_cancel_r with (p := 4) in e; try lia.
       rewrite ZLib.div_mul_undo in e; try lia.
       rewrite combine_lookup_first.
-      eapply H7; eauto.
+      eapply H9; eauto.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
@@ -1841,18 +1822,20 @@ Section CORRECTNESS.
       lia.
       unfold_constants.
       intro.
-      apply Z2Nat.inj_iff in H16; try lia.
+      rewrite HeqOFFSET in *.
+      apply Z2Nat.inj_iff in H17; try lia.
       apply Z.div_pos; try lia.
       apply Integers.Ptrofs.unsigned_range.
+      apply Integers.Ptrofs.unsigned_range_2.
 
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity.
       unfold arr_stack_based_pointers.
       intros.
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
 
       crush.
       erewrite Mem.load_store_same.
-      2: { rewrite ZERO.
+      2: { rewrite ZERO1.
            rewrite Integers.Ptrofs.add_zero_l.
            rewrite e.
            rewrite Integers.Ptrofs.unsigned_repr.
@@ -1868,17 +1851,20 @@ Section CORRECTNESS.
       erewrite Mem.load_store_other with (m1 := m).
       2: { exact H1. }
       2: { right.
-           rewrite ZERO.
+           rewrite ZERO1.
            rewrite Integers.Ptrofs.add_zero_l.
            rewrite Integers.Ptrofs.unsigned_repr.
            simpl.
            destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+           rewrite HeqOFFSET in *. simplify_val.
+           left; auto.
+           rewrite HeqOFFSET in *. simplify_val.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
            invert H0.
-           apply Zmult_lt_compat_r with (p := 4) in H17; try lia.
-           rewrite ZLib.div_mul_undo in H17; try lia.
+           apply Zmult_lt_compat_r with (p := 4) in H18; try lia.
+           rewrite ZLib.div_mul_undo in H18; try lia.
            split; try lia.
            apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
@@ -1889,7 +1875,8 @@ Section CORRECTNESS.
       assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
       erewrite Mem.load_store_other with (m1 := m).
       2: { exact H1. }
-      2: { right. right. simpl.
+      2: { rewrite HeqOFFSET in *. simplify_val.
+           right. right. simpl.
            rewrite ZERO.
            rewrite Integers.Ptrofs.add_zero_l.
            rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
@@ -1911,7 +1898,12 @@ Section CORRECTNESS.
                                                                  (Integers.Ptrofs.repr ptr))) v).
       apply X in H0. invert H0. congruence.
 
-    + invert MARR. crush.
+      constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
+      assumption. lia.
+      unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
+      assumption. lia.
+
+    + invert MARR. inv CONST. crush.
 
       unfold Op.eval_addressing in H0.
       destruct (Archi.ptr64) eqn:ARCHI; crush.
@@ -1942,7 +1934,6 @@ Section CORRECTNESS.
       eexists. split.
       eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
-      apply assumption_32bit.
       econstructor. econstructor. econstructor.
       eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor. econstructor. econstructor. econstructor.
@@ -1956,7 +1947,6 @@ Section CORRECTNESS.
       apply AssocMap.gss.
 
       (** Match states *)
-      rewrite assumption_32bit.
       econstructor; eauto.
 
       (** Match assocmaps *)
@@ -1972,14 +1962,6 @@ Section CORRECTNESS.
       apply AssocMap.gss.
 
       (** Equality proof *)
-      assert (Z.to_nat
-                (Integers.Ptrofs.unsigned
-                   (Integers.Ptrofs.divu
-                      OFFSET
-                      (Integers.Ptrofs.repr 4)))
-              =
-              valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4)))
-        as EXPR_OK by admit.
 
       assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
       inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
@@ -1996,7 +1978,7 @@ Section CORRECTNESS.
       rewrite AssocMap.gss.
       unfold Verilog.merge_arr.
       rewrite AssocMap.gss.
-      setoid_rewrite H5.
+      setoid_rewrite H7.
       reflexivity.
 
       rewrite combine_length.
@@ -2024,19 +2006,19 @@ Section CORRECTNESS.
       simpl.
       assert (Ple src (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H0 in H8.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto.
+      apply H0 in H11.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H11; eauto.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
       rewrite list_repeat_len. auto.
 
       assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in H8.
-      rewrite Z_div_mult in H8; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia.
-      rewrite H8. rewrite EXPR_OK.
+      rewrite Z.mul_comm in H11.
+      rewrite Z_div_mult in H11; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H11 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H11; unfold_constants; try lia.
+      rewrite H11. rewrite <- offset_expr_ok_3.
       rewrite array_get_error_set_bound.
       reflexivity.
       unfold arr_length, arr_repeat. simpl.
@@ -2053,20 +2035,20 @@ Section CORRECTNESS.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
-           rewrite Z2Nat.id in H11; try lia.
-           apply Zmult_lt_compat_r with (p := 4) in H11; try lia.
-           rewrite ZLib.div_mul_undo in H11; try lia.
+           rewrite Z2Nat.id in H14; try lia.
+           apply Zmult_lt_compat_r with (p := 4) in H14; try lia.
+           rewrite ZLib.div_mul_undo in H14; try lia.
            split; try lia.
            apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
 
-      rewrite <- EXPR_OK.
+      rewrite <- offset_expr_ok_3.
       rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
       destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
       apply Z.mul_cancel_r with (p := 4) in e; try lia.
       rewrite ZLib.div_mul_undo in e; try lia.
       rewrite combine_lookup_first.
-      eapply H7; eauto.
+      eapply H9; eauto.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
@@ -2079,7 +2061,7 @@ Section CORRECTNESS.
       lia.
       unfold_constants.
       intro.
-      apply Z2Nat.inj_iff in H8; try lia.
+      apply Z2Nat.inj_iff in H11; try lia.
       apply Z.div_pos; try lia.
       apply Integers.Ptrofs.unsigned_range.
 
@@ -2115,8 +2097,8 @@ Section CORRECTNESS.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
            invert H0.
-           apply Zmult_lt_compat_r with (p := 4) in H9; try lia.
-           rewrite ZLib.div_mul_undo in H9; try lia.
+           apply Zmult_lt_compat_r with (p := 4) in H13; try lia.
+           rewrite ZLib.div_mul_undo in H13; try lia.
            split; try lia.
            apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
@@ -2147,7 +2129,20 @@ Section CORRECTNESS.
                                          (Integers.Ptrofs.unsigned
                                             (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
                                                                  (Integers.Ptrofs.repr ptr))) v).
-      apply X in H0. invert H0. congruence.*)
+      apply X in H0. invert H0. congruence.
+
+      constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
+      assumption. lia.
+      unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
+      assumption. lia.
+
+      Unshelve.
+      exact tt.
+      exact (Values.Vint (Int.repr 0)).
+      exact tt.
+      exact (Values.Vint (Int.repr 0)).
+      exact tt.
+      exact (Values.Vint (Int.repr 0)).
   Admitted.
   Hint Resolve transl_istore_correct : htlproof.
 
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
index 4e34c06..2220998 100644
--- a/src/verilog/ValueInt.v
+++ b/src/verilog/ValueInt.v
@@ -162,6 +162,7 @@ Proof.
   inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial.
 Qed.
 
-Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int in *).
+Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue,
+                                       ptrToValue in *).
 
 Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption.