Finish first IStore proof (modulo some admissions).

2 files changed, 305 insertions, 69 deletions

diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index ec1fb07..8df70d9 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -140,23 +140,23 @@ Module PtrofsExtra.
     congruence.
   Qed.
 
-  Lemma divs_unsigned :
+  Lemma divu_unsigned :
     forall x y,
-      0 <= Ptrofs.signed x ->
-      0 < Ptrofs.signed y ->
-      Ptrofs.unsigned (Ptrofs.divs x y) = Ptrofs.signed x / Ptrofs.signed y.
+      0 < Ptrofs.unsigned y ->
+      Ptrofs.unsigned x < Ptrofs.max_unsigned ->
+      Ptrofs.unsigned (Ptrofs.divu x y) = Ptrofs.unsigned x / Ptrofs.unsigned y.
   Proof.
     intros.
-    unfold Ptrofs.divs.
-    rewrite Ptrofs.unsigned_repr.
-    apply Z.quot_div_nonneg; lia.
+    unfold Ptrofs.divu.
+    rewrite Ptrofs.unsigned_repr; auto.
     split.
-    apply Z.quot_pos; lia.
-    apply Zquot.Zquot_le_upper_bound; try lia.
+    apply Z.div_pos; auto.
+    apply Ptrofs.unsigned_range.
+    apply Z.div_le_upper_bound; auto.
     eapply Z.le_trans.
-    2: { apply ZBinary.Z.le_mul_diag_r; simplify; try lia. }
-    pose proof (Ptrofs.signed_range x).
-    simplify; lia.
+    apply Z.lt_le_incl. exact H0.
+    rewrite Z.mul_comm.
+    apply Z.le_mul_diag_r; simplify; lia.
   Qed.
 
   Lemma mul_unsigned :
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index eb9ff7a..ce92264 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -1177,17 +1177,17 @@ Section CORRECTNESS.
         invert H8.
         clear H0. clear H6.
 
-        unfold check_address_parameter in *. simplify.
+        unfold check_address_parameter_unsigned in *;
+        unfold check_address_parameter_signed in *; simplify.
 
         remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
                                       (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
 
         (** Read bounds assumption *)
-        assert (0 <= Integers.Ptrofs.signed OFFSET) as WRITE_BOUND_LOW by admit.
-        assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH by admit.
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH by admit.
 
         (** Modular preservation proof *)
-        assert (Integers.Ptrofs.signed OFFSET mod 4 = 0) as MOD_PRESERVE.
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
         { rewrite HeqOFFSET.
           apply PtrofsExtra.add_mod; simplify; try lia.
           exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
@@ -1197,41 +1197,6 @@ Section CORRECTNESS.
           rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
         }
 
-        (* (** Normalisation proof *) *)
-        (* assert (Integers.Ptrofs.repr *)
-        (*           (4 * Integers.Ptrofs.unsigned *)
-        (*                  (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *)
-        (*   as NORMALISE. *)
-        (* { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *)
-        (*   rewrite <- PtrofsExtra.mul_unsigned. *)
-        (*   apply PtrofsExtra.mul_divs; auto. *)
-        (*   rewrite Integers.Ptrofs.signed_repr; simplify; lia. } *)
-
-        (* (** Normalised bounds proof *) *)
-        (* assert (0 <= *)
-        (*         Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) *)
-        (*         < (RTL.fn_stacksize f / 4)) *)
-        (* as NORMALISE_BOUND. *)
-        (* { split. *)
-        (*   apply Integers.Ptrofs.unsigned_range_2. *)
-        (*   assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity. *)
-        (*   unfold Integers.Ptrofs.divs at 2 in H0. *)
-        (*   rewrite H0. clear H0. *)
-        (*   rewrite Integers.Ptrofs.unsigned_repr; simplify. *)
-        (*   rewrite Integers.Ptrofs.signed_repr; simplify; try lia. *)
-        (*   rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. *)
-        (*   apply Zmult_lt_reg_r with (p := 4); try lia. *)
-        (*   repeat rewrite ZLib.div_mul_undo; try lia. *)
-        (*   rewrite Integers.Ptrofs.signed_repr. *)
-        (*   rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. *)
-        (*   split. *)
-        (*   apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia. *)
-        (*   apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia. *)
-        (*   simplify; lia. } *)
-
-        (* inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *)
-        (* clear NORMALISE_BOUND. *)
-
         eexists. split.
         eapply Smallstep.plus_one.
         eapply HTL.step_module; eauto.
@@ -1274,11 +1239,11 @@ Section CORRECTNESS.
         (** Equality proof *)
         assert (Z.to_nat
                   (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divs
+                     (Integers.Ptrofs.divu
                         OFFSET
                         (Integers.Ptrofs.repr 4)))
                 =
-                valueToNat (vdivs (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7))
+                valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7))
           as EXPR_OK by admit.
 
         assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
@@ -1322,7 +1287,8 @@ Section CORRECTNESS.
         constructor.
         erewrite combine_lookup_second.
         simpl.
-        assert (Ple src (RTL.max_reg_function f)) by admit.
+        assert (Ple src (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
         apply H0 in H14.
         destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H14; eauto.
 
@@ -1330,12 +1296,248 @@ Section CORRECTNESS.
         unfold arr_repeat. simplify.
         rewrite list_repeat_len. auto.
 
-        assert (Z.to_nat ptr
+        assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+        rewrite Z.mul_comm in H14.
+        rewrite Z_div_mult in H14; try lia.
+        replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H14 by reflexivity.
+        rewrite <- PtrofsExtra.divu_unsigned in H14; unfold_constants; try lia.
+        rewrite H14. rewrite EXPR_OK.
+        rewrite array_get_error_set_bound.
+        reflexivity.
+        unfold arr_length, arr_repeat. simpl.
+        rewrite list_repeat_len. lia.
+
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             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.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H13.
+             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); simplify; lia.
+        }
+
+        rewrite <- 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.
+        rewrite ZLib.div_mul_undo in e; try lia.
+        rewrite combine_lookup_first.
+        eapply H7; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+        rewrite array_gso.
+        unfold array_get_error.
+        unfold arr_repeat.
+        simplify.
+        apply list_repeat_lookup.
+        lia.
+        unfold_constants.
+        intro.
+        apply Z2Nat.inj_iff in H14; try lia.
+        apply Z.div_pos; try lia.
+        apply Integers.Ptrofs.unsigned_range.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        unfold arr_stack_based_pointers.
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        simplify.
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        simplify.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+        destruct (Archi.ptr64); try discriminate.
+        pose proof (RSBP src). rewrite EQ_SRC in H0.
+        assumption.
+
+        simpl.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             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.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H0.
+             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); simplify; lia.
+        }
+        apply ASBP; assumption.
+
+      + (** Preamble *)
+        invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+
+        unfold reg_stack_based_pointers in RSBP.
+        pose proof (RSBP r0) as RSBPr0.
+
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify.
+
+        rewrite ARCHI in H1. simplify.
+        subst.
+
+        pose proof MASSOC as MASSOC'.
+        invert MASSOC'.
+        pose proof (H0 r0).
+        assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        apply H6 in HPler0.
+        invert HPler0; try congruence.
+        rewrite EQr0 in H8.
+        invert H8.
+        clear H0. clear H6.
+
+        unfold check_address_parameter_unsigned in *;
+        unfold check_address_parameter_signed in *; simplify.
+
+        remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                      (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+        { rewrite HeqOFFSET.
+          apply PtrofsExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          rewrite Integers.Ptrofs.signed_repr; try assumption.
+          admit. (* FIXME: Register bounds. *)
+          apply PtrofsExtra.of_int_mod.
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+        }
+
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor.
+        eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+        econstructor.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]).
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]).
+        econstructor.
+        econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+
+        all: simplify.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_greater. apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match stacks *)
+        admit.
+
+        (** Equality proof *)
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
                 =
-                valueToNat (vdivs (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7))
-          as EXPR_OK' by admit.
+                valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7))
+          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.
+
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        unfold Verilog.arr_assocmap_set.
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        rewrite AssocMap.gss.
+        setoid_rewrite H5.
+        reflexivity.
 
-        rewrite <- EXPR_OK'.
+        rewrite combine_length.
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        apply list_repeat_len.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        rewrite H4. reflexivity.
+
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        constructor.
+        erewrite combine_lookup_second.
+        simpl.
+        assert (Ple src (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+        apply H0 in H14.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H14; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+
+        assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+        rewrite Z.mul_comm in H14.
+        rewrite Z_div_mult in H14; try lia.
+        replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H14 by reflexivity.
+        rewrite <- PtrofsExtra.divu_unsigned in H14; unfold_constants; try lia.
+        rewrite H14. rewrite EXPR_OK.
         rewrite array_get_error_set_bound.
         reflexivity.
         unfold arr_length, arr_repeat. simpl.
@@ -1352,22 +1554,19 @@ Section CORRECTNESS.
              right.
              apply ZExtra.mod_0_bounds; try lia.
              apply ZLib.Z_mod_mult'.
-             apply PtrofsExtra.signed_mod_unsigned_mod; eauto; lia.
-             split; try lia.
              invert H13.
              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); simplify; lia.
         }
 
         rewrite <- EXPR_OK.
-        rewrite PtrofsExtra.divs_unsigned; try assumption.
+        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 <- PtrofsExtra.pos_signed_unsigned in e; try lia.
         rewrite ZLib.div_mul_undo in e; try lia.
-        rewrite <- PtrofsExtra.pos_signed_unsigned in n; lia.
         rewrite combine_lookup_first.
         eapply H7; eauto.
 
@@ -1380,16 +1579,53 @@ Section CORRECTNESS.
         simplify.
         apply list_repeat_lookup.
         lia.
-        replace (Integers.Ptrofs.signed (Integers.Ptrofs.repr 4)) with 4 by reflexivity.
-        rewrite <- PtrofsExtra.pos_signed_unsigned in n0; try lia.
+        unfold_constants.
         intro.
         apply Z2Nat.inj_iff in H14; try lia.
-        apply Z.div_pos; lia.
-        replace (Integers.Ptrofs.signed (Integers.Ptrofs.repr 4)) with 4 by reflexivity; lia.
+        apply Z.div_pos; try lia.
+        apply Integers.Ptrofs.unsigned_range.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        unfold arr_stack_based_pointers.
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        simplify.
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        simplify.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+        destruct (Archi.ptr64); try discriminate.
+        pose proof (RSBP src). rewrite EQ_SRC in H0.
+        assumption.
+
+        simpl.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             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.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H0.
+             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); simplify; lia.
+        }
+        apply ASBP; assumption.
+
 
-        admit.
 
-      + admit.
       + admit.
 
     - eexists. split. apply Smallstep.plus_one.