Finish store proof modulo:

* EXPR_OK proofs (Yann).
* Trivial register size proof (i.e. register values < 2^32).
* Read bounds (to be extracted from RTL semantics).
* Stack frame proof issues.

1 files changed, 206 insertions, 1 deletions

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 37cebb6..08b1216 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -1647,7 +1647,212 @@ Section CORRECTNESS.
         }
         apply ASBP; assumption.
 
-      + admit.
+      + invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+        rewrite ARCHI in H0. simplify.
+
+        unfold check_address_parameter_unsigned in *;
+        unfold check_address_parameter_signed in *; simplify.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in H1. clear ZERO.
+        rewrite Integers.Ptrofs.add_zero_l in H1.
+
+        remember i0 as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        rename H0 into MOD_PRESERVE.
+
+        (** Start of proof proper *)
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor.
+        eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+        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 (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.
+
+        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 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 H10.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H10; 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 H10.
+        rewrite Z_div_mult in H10; try lia.
+        replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H10 by reflexivity.
+        rewrite <- PtrofsExtra.divu_unsigned in H10; unfold_constants; try lia.
+        rewrite H10. 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 H8.
+             rewrite Z2Nat.id in H12; try lia.
+             apply Zmult_lt_compat_r with (p := 4) in H12; try lia.
+             rewrite ZLib.div_mul_undo in H12; 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 H10; 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 H10; try lia.
+             rewrite ZLib.div_mul_undo in H10; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+        apply ASBP; assumption.
 
     - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.