diff options
Diffstat (limited to 'src/translation/HTLgenproof.v')
-rw-r--r-- | src/translation/HTLgenproof.v | 624 |
1 files changed, 457 insertions, 167 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 9b59269..24191ae 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. +From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra. From coqup Require HTL Verilog. Require Import Lia. @@ -348,6 +348,7 @@ Section CORRECTNESS. exists asr' asa', HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). + Theorem transl_step_correct: forall (S1 : RTL.state) t S2, RTL.step ge S1 t S2 -> @@ -393,7 +394,7 @@ Section CORRECTNESS. 2: { reflexivity. } rewrite AssocMap.gss. unfold Verilog.merge_arr. - setoid_rewrite H1. + setoid_rewrite H5. reflexivity. rewrite combine_length. @@ -501,33 +502,89 @@ Section CORRECTNESS. | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x end. - Opaque Z.mul. - - - (* FIXME: Should be able to use the spec to avoid destructing here. *) + - (* FIXME: Should be able to use the spec to avoid destructing here? *) destruct c, chunk, addr, args; simplify; rt; simplify. - + admit. (* FIXME: Alignment *) - - + (* FIXME: Why is this degenerate? Should we support this mode? *) - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; simplify. - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; discriminate. - - + invert MARR. simplify. + + (** 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. - pose proof (RSBP r1) as RSBPr1. - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; - destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. + 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 READ_BOUND_LOW by admit. + assert (Integers.Ptrofs.signed 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. + { 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. @@ -535,99 +592,302 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. simplify. eapply Verilog.erun_Vbinop with (EQ := ?[EQ1]). (* FIXME: These will be shelved and cause sadness. *) eapply Verilog.erun_Vbinop with (EQ := ?[EQ2]). - eapply Verilog.erun_Vbinop with (EQ := ?[EQ3]). - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - eapply Verilog.erun_Vbinop with (EQ := ?[EQ4]). - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. - econstructor. (* FIXME: Oh dear. *) + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. - unfold Verilog.arr_assocmap_lookup. simplify. setoid_rewrite H3. + all: simplify. + + (** Verilog array lookup *) + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5. f_equal. - simplify. unfold Verilog.merge_regs. + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. - simplify. rewrite assumption_32bit. - econstructor; simplify; eauto. + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. - unfold Verilog.merge_regs. unfold_merge. + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. apply regs_lessdef_add_match. - pose proof H1. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) by reflexivity. - rewrite H4 in H5. - setoid_rewrite Integers.Ptrofs.add_zero_l in H5. + (** Equality proof *) + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H7. clear ZERO. + setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4)))). + + exploit H7. + rewrite Z2Nat.id; eauto. + apply Z.div_pos; lia. + + intros I. + + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (vdivs (vplus asr # r0 (ZToValue 32 z) ?EQ2) (ZToValue 32 4) ?EQ1)) + as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite NORMALISE in I. + rewrite H1 in I. + invert I. assumption. + + (** PC match *) + 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. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match arrays *) + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H5. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. + + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. + assumption. + + (** RSBP preservation *) + unfold reg_stack_based_pointers. intros. + destruct (Pos.eq_dec r1 dst); try rewrite e. (* FIXME: Prepare this for automation *) + + rewrite Registers.Regmap.gss. + unfold arr_stack_based_pointers in ASBP. + specialize (ASBP (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + exploit ASBP; auto; intros I. + + rewrite NORMALISE in I. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in I. clear ZERO. + simplify. + rewrite Integers.Ptrofs.add_zero_l in I. + rewrite H1 in I. + assumption. + simplify. + + rewrite Registers.Regmap.gso; auto. + + + (* FIXME: Why is this degenerate? Should we support this mode? *) + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; discriminate. + + + (** 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. + pose proof (RSBP r1) as RSBPr1. - specialize (H5 (uvalueToZ - (vplus (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) (ZToValue 32 (z0 / 4)) ?EQ2) - (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) ?EQ1))). + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; + destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. - assert (0 <= uvalueToZ - (vplus (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) (ZToValue 32 (z0 / 4)) ?EQ2) - (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) ?EQ1) < - Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit. - apply H5 in H6. + rewrite ARCHI in H1. simplify. + subst. + clear RSBPr1. - invert MASSOC. - pose proof (H7 r0). - pose proof (H7 r1). + 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 H8 in HPler0. - apply H10 in HPler1. + apply H6 in HPler0. + apply H8 in HPler1. invert HPler0; invert HPler1; try congruence. - rewrite EQr0 in H12. - rewrite EQr1 in H13. - - assert ((Integers.Ptrofs.unsigned - (Integers.Ptrofs.add i0 - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) - (Integers.Int.repr z0))))) = - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.repr - (4 * - uvalueToZ - (vplus - (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) - (ZToValue 32 (z0 / 4)) ?EQ2) - (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) - ?EQ1))))) by admit. - - rewrite <- H19 in H6. - rewrite H0 in H6. - invert H6. - assert (forall x, Z.to_nat (uvalueToZ x) = valueToNat x) as VALUE_IDENTITY by admit. - rewrite VALUE_IDENTITY in H21. - assumption. + rewrite EQr0 in H10. + rewrite EQr1 in H12. + invert H10. invert H12. + clear H0. clear H6. clear H8. + + unfold check_address_parameter in *. simplify. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) + (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 (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. + + (** 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. + 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. + } + + (** 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. + + (** Start of proof proper *) + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. simplify. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ3]). (* FIXME: These will be shelved and cause sadness. *) + eapply Verilog.erun_Vbinop with (EQ := ?[EQ4]). + eapply Verilog.erun_Vbinop with (EQ := ?[EQ5]). + econstructor. econstructor. econstructor. econstructor. + econstructor. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]). + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. + all: simplify. + + (** Verilog array lookup *) + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5. + f_equal. + + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. + + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. + apply regs_lessdef_add_match. + + (** Equality proof *) + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H7. clear ZERO. + setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4)))). + + exploit H7. + rewrite Z2Nat.id; eauto. + apply Z.div_pos; lia. + + intros I. + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + 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)) + as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite NORMALISE in I. + rewrite H1 in I. + invert I. assumption. + + (** PC match *) 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. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. + (** Match arrays *) econstructor. repeat split; simplify. unfold HTL.empty_stack. @@ -638,7 +898,7 @@ Section CORRECTNESS. 2: { reflexivity. } rewrite AssocMap.gss. unfold Verilog.merge_arr. - setoid_rewrite H3. + setoid_rewrite H5. reflexivity. rewrite combine_length. @@ -655,46 +915,24 @@ Section CORRECTNESS. eauto. apply combine_none. assumption. + (** RSBP preservation *) unfold reg_stack_based_pointers. intros. - destruct (Pos.eq_dec r2 dst); subst. + destruct (Pos.eq_dec r2 dst); try rewrite e. (* FIXME: Prepare this for automation *) rewrite Registers.Regmap.gss. - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP ((Integers.Ptrofs.unsigned - (Integers.Ptrofs.add i0 - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) - (Integers.Int.repr z0))))) / 4)). - exploit ASBP; auto; intros. - 1: { - split. - - admit. (*apply Z.div_pos; lia.*) - - admit. (* apply Zmult_lt_reg_r with (p := 4); try lia. *) - (* repeat rewrite ZLib.div_mul_undo; lia. *) - } - replace (4 * ((Integers.Ptrofs.unsigned - (Integers.Ptrofs.add i0 - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) - (Integers.Int.repr z0))))) / 4)) with (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add i0 - (Integers.Ptrofs.of_int - (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) - (Integers.Int.repr z0))))) in H0. - 2: { - rewrite Z.mul_comm. - admit. - (* rewrite ZLib.div_mul_undo; lia. *) - } - rewrite Integers.Ptrofs.repr_unsigned in H0. - simplify. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) by reflexivity. - rewrite H4 in H0. - setoid_rewrite Integers.Ptrofs.add_zero_l in H0. - rewrite H1 in H0. + specialize (ASBP (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + exploit ASBP; auto; intros I. + + rewrite NORMALISE in I. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in I. clear ZERO. simplify. + rewrite Integers.Ptrofs.add_zero_l in I. + rewrite H1 in I. assumption. + simplify. rewrite Registers.Regmap.gso; auto. @@ -704,68 +942,126 @@ Section CORRECTNESS. destruct (Archi.ptr64) eqn:ARCHI; simplify. rewrite ARCHI in H0. simplify. - (** Here we are assuming that any stack read will be within the bounds - of the activation record. *) - assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + unfold check_address_parameter in EQ; 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 (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. + + (** Modular preservation proof *) + rename H8 into MOD_PRESERVE. + + (** 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. + + (** Start of proof proper *) eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. econstructor. econstructor. econstructor. simplify. econstructor. econstructor. econstructor. econstructor. simplify. - unfold Verilog.arr_assocmap_lookup. setoid_rewrite H3. + all: simplify. + + (** Verilog array lookup *) + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5. f_equal. - simplify. unfold Verilog.merge_regs. + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. - simplify. rewrite assumption_32bit. - econstructor; simplify; eauto. + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. - unfold Verilog.merge_regs. unfold_merge. + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. apply regs_lessdef_add_match. (** Equality proof *) - (* FIXME: 32-bit issue. *) - assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) as VALUE_IDENTITY by admit. - rewrite VALUE_IDENTITY. - specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)). - rewrite Z2Nat.id in H5; try lia. - exploit H5; auto; intros. - 1: { - split. - - apply Z.div_pos; lia. - - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; lia. - } - 2: { - assert (0 < RTL.fn_stacksize f) by lia. - apply Z.div_pos; lia. - } - replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0. - 2: { - rewrite Z.mul_comm. - rewrite ZLib.div_mul_undo; lia. - } - rewrite Integers.Ptrofs.repr_unsigned in H0. - rewrite H1 in H0. - invert H0. assumption. - + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H7. clear ZERO. + setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4)))). + + exploit H7. + rewrite Z2Nat.id; eauto. + apply Z.div_pos; lia. + + intros I. + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (ZToValue 32 (Integers.Ptrofs.signed OFFSET / 4))) + as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite NORMALISE in I. + rewrite H1 in I. + invert I. assumption. + + (** PC match *) 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. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. + (** Match arrays *) econstructor. repeat split; simplify. unfold HTL.empty_stack. @@ -776,7 +1072,7 @@ Section CORRECTNESS. 2: { reflexivity. } rewrite AssocMap.gss. unfold Verilog.merge_arr. - setoid_rewrite H3. + setoid_rewrite H5. reflexivity. rewrite combine_length. @@ -793,30 +1089,24 @@ Section CORRECTNESS. eauto. apply combine_none. assumption. + (** RSBP preservation *) unfold reg_stack_based_pointers. intros. - destruct (Pos.eq_dec r0 dst); subst. + destruct (Pos.eq_dec r0 dst); try rewrite e. (* FIXME: Prepare this for automation *) rewrite Registers.Regmap.gss. - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned i0 / 4)). - exploit ASBP; auto; intros. - 1: { - split. - - apply Z.div_pos; lia. - - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; lia. - } - replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0. - 2: { - rewrite Z.mul_comm. - rewrite ZLib.div_mul_undo; lia. - } - rewrite Integers.Ptrofs.repr_unsigned in H0. - simplify. - rewrite H1 in H0. + specialize (ASBP (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + exploit ASBP; auto; intros I. + + rewrite NORMALISE in I. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in I. clear ZERO. simplify. + rewrite Integers.Ptrofs.add_zero_l in I. + rewrite H1 in I. assumption. + simplify. rewrite Registers.Regmap.gso; auto. |