From 8fda19cb580bda72f374bc2176d7e2efa5cd613b Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 28 Jun 2020 15:06:17 +0100 Subject: Work on proof. --- src/common/Coquplib.v | 3 + src/common/IntegerExtra.v | 50 +++++++ src/translation/HTLgenproof.v | 301 +++++++++++++++++++++++++++++++++++++++++- src/verilog/Array.v | 53 ++++++++ 4 files changed, 405 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index b4ca906..b8a02d2 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -117,6 +117,9 @@ Ltac simplify := unfold_constants; simpl in *; Global Opaque Nat.div. Global Opaque Z.mul. +Infix "==nat" := eq_nat_dec (no associativity, at level 50). +Infix "==Z" := Z.eq_dec (no associativity, at level 50). + (* Definition const (A B : Type) (a : A) (b : B) : A := a. Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *) diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 2f9aae6..5f06e26 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -51,6 +51,23 @@ Module PtrofsExtra. Ltac ptrofs_mod_tac m := repeat (ptrofs_mod_match m); lia. + Lemma signed_mod_unsigned_mod : + forall x m, + 0 < m -> + Ptrofs.modulus mod m = 0 -> + Ptrofs.signed x mod m = 0 -> + Ptrofs.unsigned x mod m = 0. + Proof. + intros. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed + end; try (simplify; lia); ptrofs_mod_tac m. + Qed. + Lemma of_int_mod : forall x m, Int.signed x mod m = 0 -> @@ -121,6 +138,25 @@ Module PtrofsExtra. congruence. Qed. + Lemma divs_unsigned : + forall x y, + 0 <= Ptrofs.signed x -> + 0 < Ptrofs.signed y -> + Ptrofs.unsigned (Ptrofs.divs x y) = Ptrofs.signed x / Ptrofs.signed y. + Proof. + intros. + unfold Ptrofs.divs. + rewrite Ptrofs.unsigned_repr. + apply Z.quot_div_nonneg; lia. + split. + apply Z.quot_pos; lia. + apply Zquot.Zquot_le_upper_bound; try lia. + eapply Z.le_trans. + 2: { apply ZBinary.Z.le_mul_diag_r; simplify; try lia. } + pose proof (Ptrofs.signed_range x). + simplify; lia. + Qed. + Lemma mul_unsigned : forall x y, Ptrofs.mul x y = @@ -130,6 +166,20 @@ Module PtrofsExtra. apply Ptrofs.eqm_samerepr. apply Ptrofs.eqm_mult; exists 0; lia. Qed. + + Lemma pos_signed_unsigned : + forall x, + 0 <= Ptrofs.signed x -> + Ptrofs.signed x = Ptrofs.unsigned x. + Proof. + intros. + rewrite Ptrofs.unsigned_signed. + destruct (Ptrofs.lt x Ptrofs.zero) eqn:EQ. + unfold Ptrofs.lt in EQ. + destruct (zlt (Ptrofs.signed x) (Ptrofs.signed Ptrofs.zero)); try discriminate. + replace (Ptrofs.signed (Ptrofs.zero)) with 0 in l by reflexivity. lia. + reflexivity. + Qed. End PtrofsExtra. Module IntExtra. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index cee04e9..1e16398 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -18,7 +18,7 @@ From compcert Require RTL Registers AST Integers. From compcert Require Import Globalenvs Memory. -From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra. +From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra. From coqup Require HTL Verilog. Require Import Lia. @@ -196,6 +196,67 @@ Proof. 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; simplify. + + rewrite nth_error_nil in H0. + discriminate. + + destruct l2 eqn:EQl2. simplify. + simpl in H. invert H. + destruct n; simpl in *. + invert 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; simplify; auto. + + destruct l2 eqn:EQl2. simplify. + simpl in H. invert H. + destruct n; simpl in *. + invert 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. + (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) Lemma assumption_32bit : forall v, @@ -1109,7 +1170,243 @@ Section CORRECTNESS. rewrite Registers.Regmap.gso; auto. - destruct c, chunk, addr, args; simplify; rt; simplify. - + admit. + + (** 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 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. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.signed 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. + } + + (* (** 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. + 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.divs + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (vdivs (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 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 admit. + 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 (Z.to_nat ptr + = + valueToNat (vdivs (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7)) + as EXPR_OK' by admit. + + 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'. + 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. + apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + } + + rewrite <- EXPR_OK. + rewrite PtrofsExtra.divs_unsigned; try assumption. + 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. + + 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. + replace (Integers.Ptrofs.signed (Integers.Ptrofs.repr 4)) with 4 by reflexivity. + rewrite <- PtrofsExtra.pos_signed_unsigned in n0; try lia. + 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. + + admit. + + admit. + admit. diff --git a/src/verilog/Array.v b/src/verilog/Array.v index fc52f04..f3e1cd7 100644 --- a/src/verilog/Array.v +++ b/src/verilog/Array.v @@ -41,6 +41,15 @@ Proof. Qed. Hint Resolve list_set_spec2 : array. +Lemma list_set_spec3 {A : Type} : + forall l i1 i2 (x : A), + i1 <> i2 -> + nth_error (list_set i1 x l) i2 = nth_error l i2. +Proof. + induction l; intros; destruct i1; destruct i2; simplify; try lia; try reflexivity; firstorder. +Qed. +Hint Resolve list_set_spec3 : array. + Lemma array_set_wf {A : Type} : forall l ln i (x : A), length l = ln -> length (list_set i x l) = ln. @@ -80,6 +89,13 @@ Proof. Qed. Hint Resolve array_set_spec2 : array. +Lemma array_set_len {A : Type} : + forall a i (x : A), + a.(arr_length) = (array_set i x a).(arr_length). +Proof. + unfold array_set. simplify. reflexivity. +Qed. + Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A := nth_error a.(arr_contents) i. @@ -117,6 +133,19 @@ Proof. eauto with array. Qed. +Lemma array_gso {A : Type} : + forall (a : Array A) i1 i2 x, + i1 <> i2 -> + array_get_error i2 (array_set i1 x a) = array_get_error i2 a. +Proof. + intros. + + unfold array_get_error. + unfold array_set. + simplify. + eauto with array. +Qed. + Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A := nth i a.(arr_contents) x. @@ -130,6 +159,17 @@ Proof. info_eauto with array. Qed. +Lemma array_get_get_error {A : Type} : + forall (a : Array A) i x d, + array_get_error i a = Some x -> + array_get i d a = x. +Proof. + intros. + unfold array_get. + unfold array_get_error in H. + auto using nth_error_nth. +Qed. + (** Tail recursive version of standard library function. *) Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A := match n with @@ -231,6 +271,19 @@ Proof. apply list_repeat'_cons. Qed. +Lemma list_repeat_lookup {A : Type} : + forall n i (a : A), + i < n -> + nth_error (list_repeat a n) i = Some a. +Proof. + induction n; intros. + + destruct i; simplify; lia. + + rewrite list_repeat_cons. + destruct i; simplify; firstorder. +Qed. + Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n). Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C := -- cgit