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/common/IntegerExtra.v | 24 +-- src/translation/HTLgenproof.v | 350 +++++++++++++++++++++++++++++++++++------- 2 files changed, 305 insertions(+), 69 deletions(-) (limited to 'src') 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. -- cgit