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/translation/HTLgenproof.v | 301 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 299 insertions(+), 2 deletions(-) (limited to 'src/translation/HTLgenproof.v') 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. -- cgit From accf4b273525412801dc21c893d41c890c9fed6d Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 28 Jun 2020 17:15:14 +0100 Subject: Fix unsigned/signed issues. --- src/translation/HTLgenproof.v | 110 ++++++++++++++++++------------------------ 1 file changed, 46 insertions(+), 64 deletions(-) (limited to 'src/translation/HTLgenproof.v') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 1e16398..eb9ff7a 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -594,17 +594,17 @@ Section CORRECTNESS. invert H8. clear H0. clear H6. - unfold check_address_parameter in *. simplify. + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned 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 READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_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. *) @@ -617,34 +617,28 @@ Section CORRECTNESS. (** Normalisation proof *) assert (Integers.Ptrofs.repr (4 * Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + (Integers.Ptrofs.divu 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. } + apply PtrofsExtra.mul_divu; simplify; auto; lia. } (** Normalised bounds proof *) assert (0 <= - Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) + Integers.Ptrofs.unsigned (Integers.Ptrofs.divu 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. + assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. + unfold Integers.Ptrofs.divu 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. } + apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_le_upper_bound; lia. } inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; clear NORMALISE_BOUND. @@ -687,7 +681,7 @@ Section CORRECTNESS. setoid_rewrite Integers.Ptrofs.add_zero_l in H7. specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). @@ -699,11 +693,11 @@ Section CORRECTNESS. 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) ?EQ2) (ZToValue 32 4) ?EQ1)) + valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ2) (ZToValue 32 4) ?EQ1)) as EXPR_OK by admit. rewrite <- EXPR_OK. rewrite NORMALISE in I. @@ -757,7 +751,7 @@ Section CORRECTNESS. rewrite Registers.Regmap.gss. unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; auto; intros I. rewrite NORMALISE in I. @@ -804,7 +798,8 @@ Section CORRECTNESS. invert H10. invert H12. clear H0. clear H6. clear H8. - unfold check_address_parameter in *. simplify. + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned in *; simplify. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) (Integers.Ptrofs.of_int @@ -812,11 +807,10 @@ Section CORRECTNESS. (Integers.Int.repr z0)))) as OFFSET. (** Read bounds assumption *) - assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_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. *) @@ -835,34 +829,28 @@ Section CORRECTNESS. (** Normalisation proof *) assert (Integers.Ptrofs.repr (4 * Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + (Integers.Ptrofs.divu 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. } + apply PtrofsExtra.mul_divu; simplify; auto; lia. } (** Normalised bounds proof *) assert (0 <= - Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) + Integers.Ptrofs.unsigned (Integers.Ptrofs.divu 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. + assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. + unfold Integers.Ptrofs.divu 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. } + apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_le_upper_bound; lia. } inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; clear NORMALISE_BOUND. @@ -911,7 +899,7 @@ Section CORRECTNESS. setoid_rewrite Integers.Ptrofs.add_zero_l in H7. specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). @@ -922,12 +910,12 @@ Section CORRECTNESS. intros I. assert (Z.to_nat (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = valueToNat - (vdivs (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ5) - (vmul asr # r1 (ZToValue 32 z) ?EQ6) ?EQ4) (ZToValue 32 4) ?EQ3)) + (vdiv (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ5) + (vmul asr # r1 (ZToValue 32 z) ?EQ6) ?EQ4) (ZToValue 32 4) ?EQ3)) as EXPR_OK by admit. rewrite <- EXPR_OK. rewrite NORMALISE in I. @@ -981,7 +969,7 @@ Section CORRECTNESS. rewrite Registers.Regmap.gss. unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; auto; intros I. rewrite NORMALISE in I. @@ -1001,7 +989,8 @@ Section CORRECTNESS. destruct (Archi.ptr64) eqn:ARCHI; simplify. rewrite ARCHI in H0. simplify. - unfold check_address_parameter in EQ; 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. @@ -1010,43 +999,36 @@ Section CORRECTNESS. remember i0 as OFFSET. (** Read bounds assumption *) - assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. (** Modular preservation proof *) - rename H8 into MOD_PRESERVE. + rename H0 into MOD_PRESERVE. (** Normalisation proof *) assert (Integers.Ptrofs.repr (4 * Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + (Integers.Ptrofs.divu 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. } + apply PtrofsExtra.mul_divu; simplify; auto; try lia. } (** Normalised bounds proof *) assert (0 <= - Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) + Integers.Ptrofs.unsigned (Integers.Ptrofs.divu 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. + assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. + unfold Integers.Ptrofs.divu 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. } + apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_le_upper_bound; lia. } inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; clear NORMALISE_BOUND. @@ -1086,7 +1068,7 @@ Section CORRECTNESS. setoid_rewrite Integers.Ptrofs.add_zero_l in H7. specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). @@ -1097,11 +1079,11 @@ Section CORRECTNESS. intros I. assert (Z.to_nat (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = - valueToNat (ZToValue 32 (Integers.Ptrofs.signed OFFSET / 4))) + valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4))) as EXPR_OK by admit. rewrite <- EXPR_OK. rewrite NORMALISE in I. @@ -1155,7 +1137,7 @@ Section CORRECTNESS. rewrite Registers.Regmap.gss. unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; auto; intros I. rewrite NORMALISE in I. -- cgit From e9b4b89bd491fa91640ef56ccdacc6ecccc03908 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 28 Jun 2020 22:02:44 +0100 Subject: Finish first IStore proof (modulo some admissions). --- src/translation/HTLgenproof.v | 350 +++++++++++++++++++++++++++++++++++------- 1 file changed, 293 insertions(+), 57 deletions(-) (limited to 'src/translation/HTLgenproof.v') 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. -- cgit From b988e11ff068e6c27a5252ed39113ca2bebf35e8 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 28 Jun 2020 22:14:36 +0100 Subject: Fix second IStore proof. --- src/translation/HTLgenproof.v | 79 +++++++++++++++++++++++++++---------------- 1 file changed, 50 insertions(+), 29 deletions(-) (limited to 'src/translation/HTLgenproof.v') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index ce92264..37cebb6 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -1197,6 +1197,7 @@ Section CORRECTNESS. rewrite Integers.Int.signed_repr; simplify; try split; try assumption. } + (** Start of proof proper *) eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. @@ -1396,31 +1397,41 @@ Section CORRECTNESS. unfold reg_stack_based_pointers in RSBP. pose proof (RSBP r0) as RSBPr0. + pose proof (RSBP r1) as RSBPr1. - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify. + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; + destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. rewrite ARCHI in H1. simplify. subst. + clear RSBPr1. pose proof MASSOC as MASSOC'. invert MASSOC'. pose proof (H0 r0). + pose proof (H0 r1). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + assert (HPler1 : Ple r1 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto). apply H6 in HPler0. - invert HPler0; try congruence. - rewrite EQr0 in H8. - invert H8. - clear H0. clear H6. + apply H8 in HPler1. + invert HPler0; invert HPler1; try congruence. + rewrite EQr0 in H10. + rewrite EQr1 in H12. + invert H10. invert H12. + clear H0. clear H6. clear H8. - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; simplify. + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned in *; simplify. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) + (Integers.Int.repr z0)))) as OFFSET. (** Read bounds assumption *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH by admit. + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. @@ -1430,19 +1441,29 @@ Section CORRECTNESS. rewrite Integers.Ptrofs.signed_repr; try assumption. admit. (* FIXME: Register bounds. *) apply PtrofsExtra.of_int_mod. + apply IntExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + apply IntExtra.mul_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + admit. (* FIXME: Register bounds. *) + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. rewrite Integers.Int.signed_repr; simplify; try split; try assumption. } + (** 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. - eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]). - eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]). - 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. @@ -1479,7 +1500,9 @@ Section CORRECTNESS. OFFSET (Integers.Ptrofs.repr 4))) = - valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7)) + 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. @@ -1525,19 +1548,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 H14. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H14; eauto. + apply H0 in H21. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H21; 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 Z.mul_comm in H21. + rewrite Z_div_mult in H21; try lia. + replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H21 by reflexivity. + rewrite <- PtrofsExtra.divu_unsigned in H21; unfold_constants; try lia. + rewrite H21. rewrite EXPR_OK. rewrite array_get_error_set_bound. reflexivity. unfold arr_length, arr_repeat. simpl. @@ -1554,10 +1577,10 @@ Section CORRECTNESS. 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. + invert H20. + rewrite Z2Nat.id in H22; try lia. + apply Zmult_lt_compat_r with (p := 4) in H22; try lia. + rewrite ZLib.div_mul_undo in H22; try lia. split; try lia. apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. } @@ -1581,7 +1604,7 @@ Section CORRECTNESS. lia. unfold_constants. intro. - apply Z2Nat.inj_iff in H14; try lia. + apply Z2Nat.inj_iff in H21; try lia. apply Z.div_pos; try lia. apply Integers.Ptrofs.unsigned_range. @@ -1617,15 +1640,13 @@ 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 H14; try lia. - rewrite ZLib.div_mul_undo in H14; try lia. + apply Zmult_lt_compat_r with (p := 4) in H21; try lia. + rewrite ZLib.div_mul_undo in H21; try lia. split; try lia. apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. } apply ASBP; assumption. - - + admit. - eexists. split. apply Smallstep.plus_one. -- cgit From 2f71ed762e496545699ba804e29c573aa2e0b947 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 28 Jun 2020 22:22:17 +0100 Subject: 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. --- src/translation/HTLgenproof.v | 207 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 206 insertions(+), 1 deletion(-) (limited to 'src/translation/HTLgenproof.v') 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. -- cgit