diff options
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 2843 |
1 files changed, 1477 insertions, 1366 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 272a434..75ee2fb 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -34,7 +34,6 @@ Require vericert.hls.HTL. Require Import vericert.hls.HTLgen. Require Import vericert.hls.HTLgenspec. Require Import vericert.hls.ValueInt. -Require Import vericert.hls.FunctionalUnits. Require vericert.hls.Verilog. Require Import Lia. @@ -63,10 +62,10 @@ Definition state_st_wf (m : HTL.module) (s : HTL.state) := Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : Verilog.assocmap_arr -> Prop := | match_arr : forall asa stack, - asa ! (m.(HTL.mod_ram).(ram_mem)) = Some stack /\ + asa ! (m.(HTL.mod_stk)) = Some stack /\ stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\ (forall ptr, - 0 <= ptr < Z.of_nat m.(HTL.mod_ram).(ram_size) -> + 0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) -> opt_val_value_lessdef (Mem.loadv AST.Mint32 mem (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))) (Option.default (NToValue 0) @@ -406,7 +405,7 @@ Section CORRECTNESS. Lemma op_stack_based : forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk, tr_instr fin rtrn st stk (RTL.Iop op args res0 pc') - (Verilog.Vblock (Verilog.Vvar res0) e) + (Verilog.Vnonblock (Verilog.Vvar res0) e) (state_goto st pc') -> reg_stack_based_pointers sp rs -> (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> @@ -1004,42 +1003,40 @@ Section CORRECTNESS. constructor. Qed. -(*| -The proof of semantic preservation for the translation of instructions is a -simulation argument based on diagrams of the following form: - -:: -> match_states -> code st rs ------------------------- State m st assoc -> || | -> || | -> || | -> \/ v -> code st rs' ------------------------ State m st assoc' -> match_states - -where ``tr_code c data control fin rtrn st`` is assumed to hold. - -The precondition and postcondition is that that should hold is ``match_assocmaps -rs assoc``. -|*) + (** The proof of semantic preservation for the translation of instructions + is a simulation argument based on diagrams of the following form: +<< + match_states + code st rs ---------------- State m st assoc + || | + || | + || | + \/ v + code st rs' --------------- State m st assoc' + match_states +>> + where [tr_code c data control fin rtrn st] is assumed to hold. + + The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. + *) Definition transl_instr_prop (instr : RTL.instruction) : Prop := forall m asr asa fin rtrn st stmt trans res, - tr_instr fin rtrn st (m.(HTL.mod_ram).(ram_mem)) instr stmt trans -> + tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> exists asr' asa', HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). - Opaque combine. +Ltac name_goal name := refine ?[name]. + +Ltac unfold_merge := + unfold merge_assocmap; repeat (rewrite AssocMapExt.merge_add_assoc); + try (rewrite AssocMapExt.merge_base_1). Ltac tac0 := match goal with | [ |- HTL.exec_ram _ _ _ _ _ ] => constructor - | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs - | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr - | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge + | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; cbn; unfold_merge | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros - | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack @@ -1071,11 +1068,97 @@ rs assoc``. | [ H : opt_val_value_lessdef _ _ |- _ ] => inv H | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H + | [ |- context[AssocMapExt.merge]] => progress unfold_merge end. + Ltac simplify_local := intros; unfold_constants; cbn in *; + repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp); + cbn in *. + + Ltac simplify_val := repeat (simplify_local; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue, + ptrToValue in *). + + Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption. + Ltac small_tac := repeat (crush_val; try array; try ptrofs); crush_val; auto. Ltac big_tac := repeat (crush_val; try array; try ptrofs; try tac0); crush_val; auto. + Lemma merge_get_default : + forall ars ars' r x, + ars ! r = Some x -> + (AssocMapExt.merge _ ars ars') # r = x. + Proof. + unfold AssocMapExt.merge; intros. + unfold "#", AssocMapExt.get_default. + rewrite AssocMap.gcombine by auto. + unfold AssocMapExt.merge_atom. + now rewrite !H. + Qed. + + Lemma merge_get_default2 : + forall ars ars' r, + ars ! r = None -> + (AssocMapExt.merge _ ars ars') # r = ars' # r. + Proof. + unfold AssocMapExt.merge; intros. + unfold "#", AssocMapExt.get_default. + rewrite AssocMap.gcombine by auto. + unfold AssocMapExt.merge_atom. + now rewrite !H. + Qed. + + Lemma merge_get_default3 : + forall A ars ars' r, + ars ! r = None -> + (AssocMapExt.merge A ars ars') ! r = ars' ! r. + Proof. + unfold AssocMapExt.merge; intros. + unfold "#", AssocMapExt.get_default. + rewrite AssocMap.gcombine by auto. + unfold AssocMapExt.merge_atom. + now rewrite !H. + Qed. + + Lemma merge_get_default4 : + forall A ars ars' r x, + ars ! r = Some x -> + (AssocMapExt.merge A ars ars') ! r = Some x. + Proof. + unfold AssocMapExt.merge; intros. + unfold "#", AssocMapExt.get_default. + rewrite AssocMap.gcombine by auto. + unfold AssocMapExt.merge_atom. + now rewrite !H. + Qed. + + Lemma match_assocmaps_merge_empty: + forall f rs ars, + match_assocmaps f rs ars -> + match_assocmaps f rs (AssocMapExt.merge value empty_assocmap ars). + Proof. + inversion 1; subst; clear H. + constructor; intros. + rewrite merge_get_default2; auto. + Qed. + + Opaque AssocMap.get. + Opaque AssocMap.set. + Opaque AssocMapExt.merge. + Opaque Verilog.merge_arr. + + Lemma match_assocmaps_ext : + forall f rs ars1 ars2, + (forall x, Ple x (RTL.max_reg_function f) -> ars1 ! x = ars2 ! x) -> + match_assocmaps f rs ars1 -> + match_assocmaps f rs ars2. + Proof. + intros * YFRL YMATCH. + inv YMATCH. constructor; intros x' YPLE. + unfold "#", AssocMapExt.get_default in *. + rewrite <- YFRL by auto. + eauto. + Qed. + Lemma transl_inop_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) (rs : RTL.regset) (m : mem) (pc' : RTL.node), @@ -1094,17 +1177,33 @@ rs assoc``. apply Smallstep.plus_one. eapply HTL.step_module; eauto. inv CONST; assumption. - inv CONST; assumption. + inv CONST; assumption. (* processing of state *) econstructor. - (* crush. *) - (* econstructor. *) - (* econstructor. *) - (* econstructor. *) - - (* all: inv MARR; big_tac. *) Abort. - -(* inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. + crush. + econstructor. + econstructor. + econstructor. + big_tac. + cbn. + + solve [inv MARR; big_tac]. + + (* inv MARR; big_tac. *) + inv MARR; big_tac; auto. + + - eapply match_assocmaps_ext; [|eauto]; intros. + repeat unfold_merge. rewrite AssocMap.gso by (unfold Ple in *; lia). + rewrite AssocMapExt.merge_base_1; auto. + - rewrite <- H1. unfold Verilog.merge_arrs. + rewrite !AssocMap.gcombine by auto. rewrite !AssocMap.gss. + setoid_rewrite H1. + repeat erewrite Verilog.merge_arr_empty2; eauto. + - inv CONST; cbn in *. constructor; cbn in *. + + repeat unfold_merge. rewrite AssocMap.gso by lia. + unfold_merge; auto. + + repeat unfold_merge. rewrite AssocMap.gso by lia. + unfold_merge; auto. Unshelve. exact tt. Qed. @@ -1138,27 +1237,38 @@ rs assoc``. all: big_tac. - assert (HPle: Ple res0 (RTL.max_reg_function f)) + - assert (HPle: Ple res0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - - unfold Ple in HPle. lia. - apply regs_lessdef_add_match. assumption. - apply regs_lessdef_add_greater. unfold Plt; lia. assumption. - assert (HPle: Ple res0 (RTL.max_reg_function f)) + unfold Ple in HPle. lia. + - eapply match_assocmaps_merge_empty. eapply match_assocmaps_ext; intros. + unfold Ple in *. instantiate (1 := asr # res0 <- x). + destruct (peq res0 x1); subst. + + rewrite merge_get_default4 with (x := x); + apply AssocMap.gss. + + rewrite merge_get_default3; [now rewrite AssocMap.gso by auto|]. + rewrite AssocMap.gso by auto. + now rewrite AssocMap.gso by lia. + + now apply regs_lessdef_add_match. + - assert (HPle: Ple res0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle; lia. - eapply op_stack_based; eauto. - inv CONST. constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - Unshelve. exact tt. + unfold Ple in HPle. lia. + - unfold Verilog.merge_arrs. + rewrite ! AssocMap.gcombine by auto. rewrite ! AssocMap.gss. + erewrite ! Verilog.merge_arr_empty2; eauto. + erewrite ! Verilog.merge_arr_empty2; eauto. + - assumption. + - eapply op_stack_based; eauto. + - assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in *. + inv CONST. constructor; cbn. + repeat rewrite merge_get_default3 by solve [auto | lia]. + rewrite merge_get_default3; [eauto | ]. + repeat rewrite AssocMap.gso by solve [auto | lia]. auto. + repeat rewrite merge_get_default3 by solve [auto | lia]. + rewrite merge_get_default3; [eauto | ]. + repeat rewrite AssocMap.gso by solve [auto | lia]. auto. + Unshelve. apply tt. Qed. #[local] Hint Resolve transl_iop_correct : htlproof. @@ -1266,373 +1376,374 @@ rs assoc``. Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. Proof. - intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. - inv_state. inv_arr_access. - - + (** Preamble *) - inv MARR. inv CONST. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. - - rewrite ARCHI in H1. crush. - subst. - - pose proof MASSOC as MASSOC'. - inv MASSOC'. - pose proof (H0 r0). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - apply H0 in HPler0. - inv HPler0; try congruence. - rewrite EQr0 in H11. - inv H11. - - unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. - apply Zdivide_mod. assumption. } - - (** Read bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. - split; try lia; apply Integers.Ptrofs.unsigned_range_2. - small_tac. } - - (** Normalisation proof *) - assert (Integers.Ptrofs.repr - (4 * Integers.Ptrofs.unsigned - (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_divu; crush; auto. } - - (** Normalised bounds proof *) - assert (0 <= - 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 (HDIV: forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. - unfold Integers.Ptrofs.divu at 2 in HDIV. - rewrite HDIV. clear HDIV. - rewrite Integers.Ptrofs.unsigned_repr; crush. - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; try lia. - apply Z.div_pos; small_tac. - apply Z.div_le_upper_bound; small_tac. } - - 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. crush. - econstructor. econstructor. econstructor. crush. - econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. - - all: big_tac. - - 1: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } - - 2: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } - - (** Match assocmaps *) - apply regs_lessdef_add_match; big_tac. - - (** Equality proof *) - rewrite <- offset_expr_ok. - - specialize (H9 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - exploit H9; big_tac. - - (** RSBP preservation *) - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; big_tac. - rewrite NORMALISE in H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption. - constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple dst (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple dst (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - + (** Preamble *) - inv MARR. inv CONST. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - 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; crush. - - rewrite ARCHI in H1. crush. - subst. - clear RSBPr1. - - pose proof MASSOC as MASSOC'. - inv 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; crush; 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 H11 in HPler1. - inv HPler0; inv HPler1; try congruence. - rewrite EQr0 in H13. - rewrite EQr1 in H14. - inv H13. inv H14. - clear H0. clear H8. clear H11. - - unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ 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. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. - apply Zdivide_mod. assumption. } - - (** Read bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. - split; try lia; apply Integers.Ptrofs.unsigned_range_2. - small_tac. } - - (** Normalisation proof *) - assert (Integers.Ptrofs.repr - (4 * Integers.Ptrofs.unsigned - (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_divu; crush. } - - (** Normalised bounds proof *) - assert (0 <= - 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.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. - unfold Integers.Ptrofs.divu at 2 in H14. - rewrite H14. clear H14. - rewrite Integers.Ptrofs.unsigned_repr; crush. - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; try lia. - apply Z.div_pos; small_tac. - apply Z.div_le_upper_bound; 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. crush. - econstructor. econstructor. econstructor. crush. - econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. auto. econstructor. - econstructor. econstructor. econstructor. econstructor. - all: big_tac. - - 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } - - 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } - - (** Match assocmaps *) - apply regs_lessdef_add_match; big_tac. - - (** Equality proof *) - rewrite <- offset_expr_ok_2. - - specialize (H9 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - exploit H9; big_tac. - - (** RSBP preservation *) - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; big_tac. - rewrite NORMALISE in H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption. - - constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple dst (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple dst (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - - + inv MARR. inv CONST. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - rewrite ARCHI in H0. crush. - - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; crush. - - 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. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. - apply Zdivide_mod. assumption. } - - (** Read bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:?EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. } - - (** Normalisation proof *) - assert (Integers.Ptrofs.repr - (4 * Integers.Ptrofs.unsigned - (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_divu; crush. } - - (** Normalised bounds proof *) - assert (0 <= - 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.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; crush. - apply Zmult_lt_reg_r with (p := 4); try lia. - repeat rewrite ZLib.div_mul_undo; try lia. - apply Z.div_pos; small_tac. - apply Z.div_le_upper_bound; 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. crush. - econstructor. econstructor. econstructor. econstructor. crush. - - all: big_tac. - - 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } - - 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } - - (** Match assocmaps *) - apply regs_lessdef_add_match; big_tac. - - (** Equality proof *) - rewrite <- offset_expr_ok_3. - - specialize (H9 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - exploit H9; big_tac. - - (** RSBP preservation *) - unfold arr_stack_based_pointers in ASBP. - specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; big_tac. - rewrite NORMALISE in H0. rewrite H1 in H0. assumption. - - constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple dst (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple dst (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - - Unshelve. - exact (Values.Vint (Int.repr 0)). - exact tt. - exact (Values.Vint (Int.repr 0)). - exact tt. - exact (Values.Vint (Int.repr 0)). - exact tt. - Qed. + (* intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. *) + (* inv_state. inv_arr_access. *) + + (* + (** Preamble *) *) + (* inv MARR. inv CONST. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + + (* unfold reg_stack_based_pointers in RSBP. *) + (* pose proof (RSBP r0) as RSBPr0. *) + + (* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *) + + (* rewrite ARCHI in H1. crush. *) + (* subst. *) + + (* pose proof MASSOC as MASSOC'. *) + (* inv MASSOC'. *) + (* pose proof (H0 r0). *) + (* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) + (* apply H0 in HPler0. *) + (* inv HPler0; try congruence. *) + (* rewrite EQr0 in H11. *) + (* inv H11. *) + + (* unfold check_address_parameter_signed in *; *) + (* unfold check_address_parameter_unsigned in *; crush. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) + (* (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. *) + (* apply Zdivide_mod. assumption. } *) + + (* (** Read bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) + (* unfold stack_bounds in BOUNDS. *) + (* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. *) + (* split; try lia; apply Integers.Ptrofs.unsigned_range_2. *) + (* small_tac. } *) + + (* (** Normalisation proof *) *) + (* assert (Integers.Ptrofs.repr *) + (* (4 * Integers.Ptrofs.unsigned *) + (* (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_divu; crush; auto. } *) + + (* (** Normalised bounds proof *) *) + (* assert (0 <= *) + (* 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 (HDIV: forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *) + (* unfold Integers.Ptrofs.divu at 2 in HDIV. *) + (* rewrite HDIV. clear HDIV. *) + (* rewrite Integers.Ptrofs.unsigned_repr; crush. *) + (* apply Zmult_lt_reg_r with (p := 4); try lia. *) + (* repeat rewrite ZLib.div_mul_undo; try lia. *) + (* apply Z.div_pos; small_tac. *) + (* apply Z.div_le_upper_bound; small_tac. } *) + + (* 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. crush. *) + (* econstructor. econstructor. econstructor. crush. *) + (* econstructor. econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + (* econstructor. econstructor. *) + + (* all: big_tac. *) + + (* 1: { *) + (* assert (HPle : Ple dst (RTL.max_reg_function f)). *) + (* eapply RTL.max_reg_function_def. eassumption. auto. *) + (* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *) + (* } *) + + (* 2: { *) + (* assert (HPle : Ple dst (RTL.max_reg_function f)). *) + (* eapply RTL.max_reg_function_def. eassumption. auto. *) + (* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *) + (* } *) + + (* (** Match assocmaps *) *) + (* apply regs_lessdef_add_match; big_tac. *) + + (* (** Equality proof *) *) + (* rewrite <- offset_expr_ok. *) + + (* specialize (H9 (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4)))). *) + (* exploit H9; big_tac. *) + + (* (** RSBP preservation *) *) + (* unfold arr_stack_based_pointers in ASBP. *) + (* specialize (ASBP (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *) + (* exploit ASBP; big_tac. *) + (* rewrite NORMALISE in H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption. *) + (* constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. *) + (* assumption. lia. *) + (* assert (HPle: Ple dst (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) + (* unfold Ple in HPle. lia. *) + (* rewrite AssocMap.gso. rewrite AssocMap.gso. *) + (* assumption. lia. *) + (* assert (HPle: Ple dst (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) + (* unfold Ple in HPle. lia. *) + (* + (** Preamble *) *) + (* inv MARR. inv CONST. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + + (* 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; crush. *) + + (* rewrite ARCHI in H1. crush. *) + (* subst. *) + (* clear RSBPr1. *) + + (* pose proof MASSOC as MASSOC'. *) + (* inv 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; crush; 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 H11 in HPler1. *) + (* inv HPler0; inv HPler1; try congruence. *) + (* rewrite EQr0 in H13. *) + (* rewrite EQr1 in H14. *) + (* inv H13. inv H14. *) + (* clear H0. clear H8. clear H11. *) + + (* unfold check_address_parameter_signed in *; *) + (* unfold check_address_parameter_unsigned in *; crush. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ 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. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. *) + (* apply Zdivide_mod. assumption. } *) + + (* (** Read bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) + (* unfold stack_bounds in BOUNDS. *) + (* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. *) + (* split; try lia; apply Integers.Ptrofs.unsigned_range_2. *) + (* small_tac. } *) + + (* (** Normalisation proof *) *) + (* assert (Integers.Ptrofs.repr *) + (* (4 * Integers.Ptrofs.unsigned *) + (* (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_divu; crush. } *) + + (* (** Normalised bounds proof *) *) + (* assert (0 <= *) + (* 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.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *) + (* unfold Integers.Ptrofs.divu at 2 in H14. *) + (* rewrite H14. clear H14. *) + (* rewrite Integers.Ptrofs.unsigned_repr; crush. *) + (* apply Zmult_lt_reg_r with (p := 4); try lia. *) + (* repeat rewrite ZLib.div_mul_undo; try lia. *) + (* apply Z.div_pos; small_tac. *) + (* apply Z.div_le_upper_bound; 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. crush. *) + (* econstructor. econstructor. econstructor. crush. *) + (* econstructor. econstructor. econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + (* econstructor. econstructor. auto. econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + (* all: big_tac. *) + + (* 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). *) + (* eapply RTL.max_reg_function_def. eassumption. auto. *) + (* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *) + + (* 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). *) + (* eapply RTL.max_reg_function_def. eassumption. auto. *) + (* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *) + + (* (** Match assocmaps *) *) + (* apply regs_lessdef_add_match; big_tac. *) + + (* (** Equality proof *) *) + (* rewrite <- offset_expr_ok_2. *) + + (* specialize (H9 (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4)))). *) + (* exploit H9; big_tac. *) + + (* (** RSBP preservation *) *) + (* unfold arr_stack_based_pointers in ASBP. *) + (* specialize (ASBP (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *) + (* exploit ASBP; big_tac. *) + (* rewrite NORMALISE in H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption. *) + + (* constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. *) + (* assumption. lia. *) + (* assert (HPle: Ple dst (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) + (* unfold Ple in HPle. lia. *) + (* rewrite AssocMap.gso. rewrite AssocMap.gso. *) + (* assumption. lia. *) + (* assert (HPle: Ple dst (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) + (* unfold Ple in HPle. lia. *) + + (* + inv MARR. inv CONST. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + (* rewrite ARCHI in H0. crush. *) + + (* unfold check_address_parameter_unsigned in *; *) + (* unfold check_address_parameter_signed in *; crush. *) + + (* 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. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. *) + (* apply Zdivide_mod. assumption. } *) + + (* (** Read bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:?EQ; crush; auto. *) + (* unfold stack_bounds in BOUNDS. *) + (* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. } *) + + (* (** Normalisation proof *) *) + (* assert (Integers.Ptrofs.repr *) + (* (4 * Integers.Ptrofs.unsigned *) + (* (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_divu; crush. } *) + + (* (** Normalised bounds proof *) *) + (* assert (0 <= *) + (* 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.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; crush. *) + (* apply Zmult_lt_reg_r with (p := 4); try lia. *) + (* repeat rewrite ZLib.div_mul_undo; try lia. *) + (* apply Z.div_pos; small_tac. *) + (* apply Z.div_le_upper_bound; 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. crush. *) + (* econstructor. econstructor. econstructor. econstructor. crush. *) + + (* all: big_tac. *) + + (* 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). *) + (* eapply RTL.max_reg_function_def. eassumption. auto. *) + (* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *) + + (* 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). *) + (* eapply RTL.max_reg_function_def. eassumption. auto. *) + (* apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *) + + (* (** Match assocmaps *) *) + (* apply regs_lessdef_add_match; big_tac. *) + + (* (** Equality proof *) *) + (* rewrite <- offset_expr_ok_3. *) + + (* specialize (H9 (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu *) + (* OFFSET *) + (* (Integers.Ptrofs.repr 4)))). *) + (* exploit H9; big_tac. *) + + (* (** RSBP preservation *) *) + (* unfold arr_stack_based_pointers in ASBP. *) + (* specialize (ASBP (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *) + (* exploit ASBP; big_tac. *) + (* rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *) + + (* constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. *) + (* assumption. lia. *) + (* assert (HPle: Ple dst (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) + (* unfold Ple in HPle. lia. *) + (* rewrite AssocMap.gso. rewrite AssocMap.gso. *) + (* assumption. lia. *) + (* assert (HPle: Ple dst (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *) + (* unfold Ple in HPle. lia. *) + + (* Unshelve. *) + (* exact (Values.Vint (Int.repr 0)). *) + (* exact tt. *) + (* exact (Values.Vint (Int.repr 0)). *) + (* exact tt. *) + (* exact (Values.Vint (Int.repr 0)). *) + (* exact tt. *) + (* Qed. *) + Admitted. #[local] Hint Resolve transl_iload_correct : htlproof. Lemma transl_istore_correct: @@ -1648,861 +1759,861 @@ rs assoc``. exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. Proof. - intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. - inv_state. inv_arr_access. - - + (** Preamble *) - inv MARR. inv CONST. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - unfold reg_stack_based_pointers in RSBP. - pose proof (RSBP r0) as RSBPr0. - - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. - - rewrite ARCHI in H1. crush. - subst. - - pose proof MASSOC as MASSOC'. - inv MASSOC'. - pose proof (H0 r0). - assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; crush; eauto). - apply H8 in HPler0. - inv HPler0; try congruence. - rewrite EQr0 in H11. - inv H11. - clear H0. clear H8. - - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. - apply Zdivide_mod. assumption. } - - (** Write bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac. - apply Integers.Ptrofs.unsigned_range_2. } - - (** Start of proof proper *) - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. - eapply Verilog.stmnt_runp_Vnonblock_arr. crush. - econstructor. - econstructor. - econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - - all: try constructor; crush. - - (** State Lookup *) - unfold Verilog.merge_regs. - crush. - unfold_merge. - apply AssocMap.gss. - - (** Match states *) - econstructor; eauto. - - (** Match assocmaps *) - unfold Verilog.merge_regs. crush. unfold_merge. - apply regs_lessdef_add_greater. - unfold Plt; lia. - assumption. - - (** States well formed *) - unfold state_st_wf. inversion 1. crush. - unfold Verilog.merge_regs. - unfold_merge. - apply AssocMap.gss. - - (** Equality proof *) - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. - - econstructor. - repeat split; crush. - unfold HTL.empty_stack. - crush. - unfold Verilog.merge_arrs. - - rewrite AssocMap.gcombine by reflexivity. - rewrite AssocMap.gss. - erewrite Verilog.merge_arr_empty2. - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gcombine by reflexivity. - rewrite AssocMap.gss. - rewrite AssocMap.gss. - unfold Verilog.merge_arr. - setoid_rewrite H7. - reflexivity. - - rewrite AssocMap.gcombine by reflexivity. - unfold Verilog.merge_arr. - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gss. - rewrite AssocMap.gss. - setoid_rewrite H7. - reflexivity. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - symmetry. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite H4. - apply list_repeat_len. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite H4. - apply list_repeat_len. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) - (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. - - 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. - rewrite HeqOFFSET. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - constructor. - erewrite combine_lookup_second. - simplify. - assert (HPle : Ple src (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H11 in HPle. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv HPle; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - - assert (HMul : 4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in HMul. - rewrite Z_div_mult in HMul; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in HMul by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in HMul; unfold_constants; try lia. - rewrite HMul. rewrite <- offset_expr_ok. - rewrite HeqOFFSET. - rewrite array_get_error_set_bound. - reflexivity. - unfold arr_length, arr_repeat. simpl. - rewrite list_repeat_len. rewrite HeqOFFSET in HMul. 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. - rewrite HeqOFFSET in *. simplify_val. - destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. - rewrite HeqOFFSET in *. simplify_val. - left; auto. - rewrite HeqOFFSET in *. simplify_val. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - rewrite Z2Nat.id in H15; try lia. - apply Zmult_lt_compat_r with (p := 4) in H15; try lia. - rewrite ZLib.div_mul_undo in H15; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - - rewrite <- offset_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 H9; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - rewrite array_gso. - unfold array_get_error. - unfold arr_repeat. - crush. - apply list_repeat_lookup. - lia. - unfold_constants. - intro. - apply Z2Nat.inj_iff in H13; rewrite HeqOFFSET in n0; try lia. - apply Z.div_pos; try lia. - apply Integers.Ptrofs.unsigned_range. - apply Integers.Ptrofs.unsigned_range_2. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity. - unfold arr_stack_based_pointers. - intros. - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - crush. - erewrite Mem.load_store_same. - 2: { rewrite ZERO1. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - crush. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. - destruct (Archi.ptr64); try discriminate. - pose proof (RSBP src). rewrite EQ_SRC in H11. - assumption. - - simpl. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO1. - 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. - rewrite HeqOFFSET in *. simplify_val. - left; auto. - rewrite HeqOFFSET in *. simplify_val. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - inv H11. - 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); crush; lia. - } - apply ASBP; assumption. - - unfold stack_bounds in *. intros. - simpl. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { rewrite HeqOFFSET in *. simplify_val. - right. right. simpl. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. - apply ZExtra.mod_0_bounds; crush; try lia. } - crush. - exploit (BOUNDS ptr); try lia. intros. crush. - exploit (BOUNDS ptr v); try lia. intros. - inv H11. - match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. - assert (Mem.valid_access m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H11. - exact H11. eapply Mem.store_valid_access_3. eassumption. } - pose proof (Mem.valid_access_store m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) v). - apply X in H11. inv H11. congruence. - - constructor; simplify. unfold Verilog.merge_regs. unfold_merge. - rewrite AssocMap.gso. - assumption. lia. - unfold Verilog.merge_regs. unfold_merge. - rewrite AssocMap.gso. - assumption. lia. - - + (** Preamble *) - inv MARR. inv CONST. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - - 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; crush. - - rewrite ARCHI in H1. crush. - subst. - clear RSBPr1. - - pose proof MASSOC as MASSOC'. - inv 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; crush; 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 H11 in HPler1. - inv HPler0; inv HPler1; try congruence. - rewrite EQr0 in H13. - rewrite EQr1 in H14. - inv H13. inv H14. - clear H0. clear H8. clear H11. - - unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; crush. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ 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. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. - apply Zdivide_mod. assumption. } - - (** Write bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. - split; try lia; apply Integers.Ptrofs.unsigned_range_2. - small_tac. } - - (** Start of proof proper *) - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. - eapply Verilog.stmnt_runp_Vnonblock_arr. crush. - econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - - all: try constructor; crush. - - (** State Lookup *) - unfold Verilog.merge_regs. - crush. - unfold_merge. - apply AssocMap.gss. - - (** Match states *) - econstructor; eauto. - - (** Match assocmaps *) - unfold Verilog.merge_regs. crush. unfold_merge. - apply regs_lessdef_add_greater. - unfold Plt; lia. - assumption. - - (** States well formed *) - unfold state_st_wf. inversion 1. crush. - unfold Verilog.merge_regs. - unfold_merge. - apply AssocMap.gss. - - (** Equality proof *) - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. - - econstructor. - repeat split; crush. - unfold HTL.empty_stack. - crush. - unfold Verilog.merge_arrs. - - rewrite AssocMap.gcombine by reflexivity. - rewrite AssocMap.gss. - erewrite Verilog.merge_arr_empty2. - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gcombine by reflexivity. - rewrite AssocMap.gss. - rewrite AssocMap.gss. - unfold Verilog.merge_arr. - setoid_rewrite H7. - reflexivity. - - rewrite AssocMap.gcombine by reflexivity. - unfold Verilog.merge_arr. - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gss. - rewrite AssocMap.gss. - setoid_rewrite H7. - reflexivity. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - symmetry. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite H4. - apply list_repeat_len. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite H4. - apply list_repeat_len. - - remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ 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. - 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. - rewrite HeqOFFSET. - 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 H14 in H15. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H15; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - - assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H15. - rewrite Z_div_mult in H15; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H15 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H15; unfold_constants; try lia. - rewrite H15. rewrite <- offset_expr_ok_2. - rewrite HeqOFFSET in *. - 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. - rewrite HeqOFFSET in *. simplify_val. - left; auto. - rewrite HeqOFFSET in *. simplify_val. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - rewrite Z2Nat.id in H17; try lia. - apply Zmult_lt_compat_r with (p := 4) in H17; try lia. - rewrite ZLib.div_mul_undo in H17; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - - rewrite <- offset_expr_ok_2. - 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 H9; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - rewrite array_gso. - unfold array_get_error. - unfold arr_repeat. - crush. - apply list_repeat_lookup. - lia. - unfold_constants. - intro. - rewrite HeqOFFSET in *. - apply Z2Nat.inj_iff in H15; try lia. - apply Z.div_pos; try lia. - apply Integers.Ptrofs.unsigned_range. - apply Integers.Ptrofs.unsigned_range_2. - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity. - unfold arr_stack_based_pointers. - intros. - destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - - crush. - erewrite Mem.load_store_same. - 2: { rewrite ZERO1. - rewrite Integers.Ptrofs.add_zero_l. - rewrite e. - rewrite Integers.Ptrofs.unsigned_repr. - exact H1. - apply Integers.Ptrofs.unsigned_range_2. } - crush. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. - destruct (Archi.ptr64); try discriminate. - pose proof (RSBP src). rewrite EQ_SRC in H14. - assumption. - - simpl. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. - rewrite ZERO1. - 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. - rewrite HeqOFFSET in *. simplify_val. - left; auto. - rewrite HeqOFFSET in *. simplify_val. - right. - apply ZExtra.mod_0_bounds; try lia. - apply ZLib.Z_mod_mult'. - inv H14. - apply Zmult_lt_compat_r with (p := 4) in H16; try lia. - rewrite ZLib.div_mul_undo in H16; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - apply ASBP; assumption. - - unfold stack_bounds in *. intros. - simpl. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { rewrite HeqOFFSET in *. simplify_val. - right. right. simpl. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. - apply ZExtra.mod_0_bounds; crush; try lia. } - crush. - exploit (BOUNDS ptr); try lia. intros. crush. - exploit (BOUNDS ptr v); try lia. intros. - simplify. - match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. - assert (Mem.valid_access m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H14. - exact H14. eapply Mem.store_valid_access_3. eassumption. } - pose proof (Mem.valid_access_store m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) v). - apply X in H14. inv H14. congruence. - - constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. - assumption. lia. - unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. - assumption. lia. - - + inv MARR. inv CONST. crush. - - unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; crush. - rewrite ARCHI in H0. crush. - - unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; crush. - - 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. - - (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. - { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. - apply Zdivide_mod. assumption. } - - (** Write bounds proof *) - assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:?EQ; crush; auto. - unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. - crush. - replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. - small_tac. } - - (** Start of proof proper *) - eexists. split. - eapply Smallstep.plus_one. - eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. - eapply Verilog.stmnt_runp_Vnonblock_arr. crush. - econstructor. econstructor. econstructor. econstructor. - - all: try constructor; crush. - - (** State Lookup *) - unfold Verilog.merge_regs. - crush. - unfold_merge. - apply AssocMap.gss. - - (** Match states *) - econstructor; eauto. - - (** Match assocmaps *) - unfold Verilog.merge_regs. crush. unfold_merge. - apply regs_lessdef_add_greater. - unfold Plt; lia. - assumption. - - (** States well formed *) - unfold state_st_wf. inversion 1. crush. - unfold Verilog.merge_regs. - unfold_merge. - apply AssocMap.gss. - - (** Equality proof *) - - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. - - econstructor. - repeat split; crush. - unfold HTL.empty_stack. - crush. - unfold Verilog.merge_arrs. - - rewrite AssocMap.gcombine by reflexivity. - rewrite AssocMap.gss. - erewrite Verilog.merge_arr_empty2. - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gcombine by reflexivity. - rewrite AssocMap.gss. - rewrite AssocMap.gss. - unfold Verilog.merge_arr. - setoid_rewrite H7. - reflexivity. - - rewrite AssocMap.gcombine by reflexivity. - unfold Verilog.merge_arr. - unfold Verilog.arr_assocmap_set. - rewrite AssocMap.gss. - rewrite AssocMap.gss. - setoid_rewrite H7. - reflexivity. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - symmetry. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite H4. - apply list_repeat_len. - - rewrite combine_length. - rewrite <- array_set_len. - unfold arr_repeat. crush. - apply list_repeat_len. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite H4. - apply list_repeat_len. - - remember i0 as OFFSET. - 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 H8. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H8; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - - assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H8. - rewrite Z_div_mult in H8; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia. - rewrite H8. rewrite <- offset_expr_ok_3. - 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'. - rewrite Z2Nat.id in H13; try lia. - apply Zmult_lt_compat_r with (p := 4) in H13; try lia. - rewrite ZLib.div_mul_undo in H13; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - - rewrite <- offset_expr_ok_3. - 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 H9; eauto. - - rewrite <- array_set_len. - unfold arr_repeat. crush. - rewrite list_repeat_len. auto. - rewrite array_gso. - unfold array_get_error. - unfold arr_repeat. - crush. - apply list_repeat_lookup. - lia. - unfold_constants. - intro. - apply Z2Nat.inj_iff in H8; 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). - - crush. - 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. } - crush. - 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'. - inv H0. - apply Zmult_lt_compat_r with (p := 4) in H11; try lia. - rewrite ZLib.div_mul_undo in H11; try lia. - split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. - } - apply ASBP; assumption. - - unfold stack_bounds in *. intros. - simpl. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - erewrite Mem.load_store_other with (m1 := m). - 2: { exact H1. } - 2: { right. right. simpl. - rewrite ZERO. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. - apply ZExtra.mod_0_bounds; crush; try lia. } - crush. - exploit (BOUNDS ptr); try lia. intros. crush. - exploit (BOUNDS ptr v); try lia. intros. - inv H0. - match goal with | |- ?x = _ => destruct x eqn:?EQ end; try reflexivity. - assert (Mem.valid_access m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H0. - exact H0. eapply Mem.store_valid_access_3. eassumption. } - pose proof (Mem.valid_access_store m AST.Mint32 sp' - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) - (Integers.Ptrofs.repr ptr))) v). - apply X in H0. inv H0. congruence. - - constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. - assumption. lia. - unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. - assumption. lia. - - Unshelve. - exact tt. - exact (Values.Vint (Int.repr 0)). - exact tt. - exact (Values.Vint (Int.repr 0)). - exact tt. - exact (Values.Vint (Int.repr 0)). - Qed. + (* intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. *) + (* inv_state. inv_arr_access. *) + + (* + (** Preamble *) *) + (* inv MARR. inv CONST. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + + (* unfold reg_stack_based_pointers in RSBP. *) + (* pose proof (RSBP r0) as RSBPr0. *) + + (* destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *) + + (* rewrite ARCHI in H1. crush. *) + (* subst. *) + + (* pose proof MASSOC as MASSOC'. *) + (* inv MASSOC'. *) + (* pose proof (H0 r0). *) + (* assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *) + (* apply H8 in HPler0. *) + (* inv HPler0; try congruence. *) + (* rewrite EQr0 in H11. *) + (* inv H11. *) + (* clear H0. clear H8. *) + + (* unfold check_address_parameter_unsigned in *; *) + (* unfold check_address_parameter_signed in *; crush. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) + (* (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. *) + (* apply Zdivide_mod. assumption. } *) + + (* (** Write bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) + (* unfold stack_bounds in BOUNDS. *) + (* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac. *) + (* apply Integers.Ptrofs.unsigned_range_2. } *) + + (* (** Start of proof proper *) *) + (* eexists. split. *) + (* eapply Smallstep.plus_one. *) + (* eapply HTL.step_module; eauto. *) + (* econstructor. econstructor. econstructor. *) + (* eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *) + (* econstructor. *) + (* econstructor. *) + (* econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + + (* all: try constructor; crush. *) + + (* (** State Lookup *) *) + (* unfold Verilog.merge_regs. *) + (* crush. *) + (* unfold_merge. *) + (* apply AssocMap.gss. *) + + (* (** Match states *) *) + (* econstructor; eauto. *) + + (* (** Match assocmaps *) *) + (* unfold Verilog.merge_regs. crush. unfold_merge. *) + (* apply regs_lessdef_add_greater. *) + (* unfold Plt; lia. *) + (* assumption. *) + + (* (** States well formed *) *) + (* unfold state_st_wf. inversion 1. crush. *) + (* unfold Verilog.merge_regs. *) + (* unfold_merge. *) + (* apply AssocMap.gss. *) + + (* (** Equality proof *) *) + + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *) + + (* econstructor. *) + (* repeat split; crush. *) + (* unfold HTL.empty_stack. *) + (* crush. *) + (* unfold Verilog.merge_arrs. *) + + (* rewrite AssocMap.gcombine by reflexivity. *) + (* rewrite AssocMap.gss. *) + (* erewrite Verilog.merge_arr_empty2. *) + (* unfold Verilog.arr_assocmap_set. *) + (* rewrite AssocMap.gcombine by reflexivity. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. *) + (* unfold Verilog.merge_arr. *) + (* setoid_rewrite H7. *) + (* reflexivity. *) + + (* rewrite AssocMap.gcombine by reflexivity. *) + (* unfold Verilog.merge_arr. *) + (* unfold Verilog.arr_assocmap_set. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. *) + (* setoid_rewrite H7. *) + (* reflexivity. *) + + (* rewrite combine_length. *) + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* symmetry. *) + (* apply list_repeat_len. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite H4. *) + (* apply list_repeat_len. *) + + (* rewrite combine_length. *) + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* apply list_repeat_len. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite H4. *) + (* apply list_repeat_len. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *) + (* (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *) + + (* 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. *) + (* rewrite HeqOFFSET. *) + (* exact H1. *) + (* apply Integers.Ptrofs.unsigned_range_2. } *) + (* constructor. *) + (* erewrite combine_lookup_second. *) + (* simplify. *) + (* assert (HPle : Ple src (RTL.max_reg_function f)) *) + (* by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) + (* apply H11 in HPle. *) + (* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv HPle; eauto. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite list_repeat_len. auto. *) + + (* assert (HMul : 4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *) + (* rewrite Z.mul_comm in HMul. *) + (* rewrite Z_div_mult in HMul; try lia. *) + (* replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in HMul by reflexivity. *) + (* rewrite <- PtrofsExtra.divu_unsigned in HMul; unfold_constants; try lia. *) + (* rewrite HMul. rewrite <- offset_expr_ok. *) + (* rewrite HeqOFFSET. *) + (* rewrite array_get_error_set_bound. *) + (* reflexivity. *) + (* unfold arr_length, arr_repeat. simpl. *) + (* rewrite list_repeat_len. rewrite HeqOFFSET in HMul. 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. *) + (* rewrite HeqOFFSET in *. simplify_val. *) + (* destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *) + (* rewrite HeqOFFSET in *. simplify_val. *) + (* left; auto. *) + (* rewrite HeqOFFSET in *. simplify_val. *) + (* right. *) + (* apply ZExtra.mod_0_bounds; try lia. *) + (* apply ZLib.Z_mod_mult'. *) + (* rewrite Z2Nat.id in H15; try lia. *) + (* apply Zmult_lt_compat_r with (p := 4) in H15; try lia. *) + (* rewrite ZLib.div_mul_undo in H15; try lia. *) + (* split; try lia. *) + (* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) + (* } *) + + (* rewrite <- offset_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 H9; eauto. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite list_repeat_len. auto. *) + (* rewrite array_gso. *) + (* unfold array_get_error. *) + (* unfold arr_repeat. *) + (* crush. *) + (* apply list_repeat_lookup. *) + (* lia. *) + (* unfold_constants. *) + (* intro. *) + (* apply Z2Nat.inj_iff in H13; rewrite HeqOFFSET in n0; try lia. *) + (* apply Z.div_pos; try lia. *) + (* apply Integers.Ptrofs.unsigned_range. *) + (* apply Integers.Ptrofs.unsigned_range_2. *) + + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity. *) + (* unfold arr_stack_based_pointers. *) + (* intros. *) + (* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + + (* crush. *) + (* erewrite Mem.load_store_same. *) + (* 2: { rewrite ZERO1. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite e. *) + (* rewrite Integers.Ptrofs.unsigned_repr. *) + (* exact H1. *) + (* apply Integers.Ptrofs.unsigned_range_2. } *) + (* crush. *) + (* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *) + (* destruct (Archi.ptr64); try discriminate. *) + (* pose proof (RSBP src). rewrite EQ_SRC in H11. *) + (* assumption. *) + + (* simpl. *) + (* erewrite Mem.load_store_other with (m1 := m). *) + (* 2: { exact H1. } *) + (* 2: { right. *) + (* rewrite ZERO1. *) + (* 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. *) + (* rewrite HeqOFFSET in *. simplify_val. *) + (* left; auto. *) + (* rewrite HeqOFFSET in *. simplify_val. *) + (* right. *) + (* apply ZExtra.mod_0_bounds; try lia. *) + (* apply ZLib.Z_mod_mult'. *) + (* inv H11. *) + (* 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); crush; lia. *) + (* } *) + (* apply ASBP; assumption. *) + + (* unfold stack_bounds in *. intros. *) + (* simpl. *) + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* erewrite Mem.load_store_other with (m1 := m). *) + (* 2: { exact H1. } *) + (* 2: { rewrite HeqOFFSET in *. simplify_val. *) + (* right. right. simpl. *) + (* rewrite ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *) + (* apply ZExtra.mod_0_bounds; crush; try lia. } *) + (* crush. *) + (* exploit (BOUNDS ptr); try lia. intros. crush. *) + (* exploit (BOUNDS ptr v); try lia. intros. *) + (* inv H11. *) + (* match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *) + (* assert (Mem.valid_access m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) Writable). *) + (* { pose proof H1. eapply Mem.store_valid_access_2 in H11. *) + (* exact H11. eapply Mem.store_valid_access_3. eassumption. } *) + (* pose proof (Mem.valid_access_store m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) v). *) + (* apply X in H11. inv H11. congruence. *) + + (* constructor; simplify. unfold Verilog.merge_regs. unfold_merge. *) + (* rewrite AssocMap.gso. *) + (* assumption. lia. *) + (* unfold Verilog.merge_regs. unfold_merge. *) + (* rewrite AssocMap.gso. *) + (* assumption. lia. *) + + (* + (** Preamble *) *) + (* inv MARR. inv CONST. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + + (* 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; crush. *) + + (* rewrite ARCHI in H1. crush. *) + (* subst. *) + (* clear RSBPr1. *) + + (* pose proof MASSOC as MASSOC'. *) + (* inv 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; crush; 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 H11 in HPler1. *) + (* inv HPler0; inv HPler1; try congruence. *) + (* rewrite EQr0 in H13. *) + (* rewrite EQr1 in H14. *) + (* inv H13. inv H14. *) + (* clear H0. clear H8. clear H11. *) + + (* unfold check_address_parameter_signed in *; *) + (* unfold check_address_parameter_unsigned in *; crush. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ 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. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. *) + (* apply Zdivide_mod. assumption. } *) + + (* (** Write bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *) + (* unfold stack_bounds in BOUNDS. *) + (* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *) + (* split; try lia; apply Integers.Ptrofs.unsigned_range_2. *) + (* small_tac. } *) + + (* (** Start of proof proper *) *) + (* eexists. split. *) + (* eapply Smallstep.plus_one. *) + (* eapply HTL.step_module; eauto. *) + (* econstructor. econstructor. econstructor. *) + (* eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *) + (* econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + (* econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + + (* all: try constructor; crush. *) + + (* (** State Lookup *) *) + (* unfold Verilog.merge_regs. *) + (* crush. *) + (* unfold_merge. *) + (* apply AssocMap.gss. *) + + (* (** Match states *) *) + (* econstructor; eauto. *) + + (* (** Match assocmaps *) *) + (* unfold Verilog.merge_regs. crush. unfold_merge. *) + (* apply regs_lessdef_add_greater. *) + (* unfold Plt; lia. *) + (* assumption. *) + + (* (** States well formed *) *) + (* unfold state_st_wf. inversion 1. crush. *) + (* unfold Verilog.merge_regs. *) + (* unfold_merge. *) + (* apply AssocMap.gss. *) + + (* (** Equality proof *) *) + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *) + + (* econstructor. *) + (* repeat split; crush. *) + (* unfold HTL.empty_stack. *) + (* crush. *) + (* unfold Verilog.merge_arrs. *) + + (* rewrite AssocMap.gcombine by reflexivity. *) + (* rewrite AssocMap.gss. *) + (* erewrite Verilog.merge_arr_empty2. *) + (* unfold Verilog.arr_assocmap_set. *) + (* rewrite AssocMap.gcombine by reflexivity. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. *) + (* unfold Verilog.merge_arr. *) + (* setoid_rewrite H7. *) + (* reflexivity. *) + + (* rewrite AssocMap.gcombine by reflexivity. *) + (* unfold Verilog.merge_arr. *) + (* unfold Verilog.arr_assocmap_set. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. *) + (* setoid_rewrite H7. *) + (* reflexivity. *) + + (* rewrite combine_length. *) + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* symmetry. *) + (* apply list_repeat_len. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite H4. *) + (* apply list_repeat_len. *) + + (* rewrite combine_length. *) + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* apply list_repeat_len. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite H4. *) + (* apply list_repeat_len. *) + + (* remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ 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. *) + (* 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. *) + (* rewrite HeqOFFSET. *) + (* 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 H14 in H15. *) + (* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H15; eauto. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite list_repeat_len. auto. *) + + (* assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *) + (* rewrite Z.mul_comm in H15. *) + (* rewrite Z_div_mult in H15; try lia. *) + (* replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H15 by reflexivity. *) + (* rewrite <- PtrofsExtra.divu_unsigned in H15; unfold_constants; try lia. *) + (* rewrite H15. rewrite <- offset_expr_ok_2. *) + (* rewrite HeqOFFSET in *. *) + (* 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. *) + (* rewrite HeqOFFSET in *. simplify_val. *) + (* left; auto. *) + (* rewrite HeqOFFSET in *. simplify_val. *) + (* right. *) + (* apply ZExtra.mod_0_bounds; try lia. *) + (* apply ZLib.Z_mod_mult'. *) + (* rewrite Z2Nat.id in H17; try lia. *) + (* apply Zmult_lt_compat_r with (p := 4) in H17; try lia. *) + (* rewrite ZLib.div_mul_undo in H17; try lia. *) + (* split; try lia. *) + (* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) + (* } *) + + (* rewrite <- offset_expr_ok_2. *) + (* 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 H9; eauto. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite list_repeat_len. auto. *) + (* rewrite array_gso. *) + (* unfold array_get_error. *) + (* unfold arr_repeat. *) + (* crush. *) + (* apply list_repeat_lookup. *) + (* lia. *) + (* unfold_constants. *) + (* intro. *) + (* rewrite HeqOFFSET in *. *) + (* apply Z2Nat.inj_iff in H15; try lia. *) + (* apply Z.div_pos; try lia. *) + (* apply Integers.Ptrofs.unsigned_range. *) + (* apply Integers.Ptrofs.unsigned_range_2. *) + + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity. *) + (* unfold arr_stack_based_pointers. *) + (* intros. *) + (* destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *) + + (* crush. *) + (* erewrite Mem.load_store_same. *) + (* 2: { rewrite ZERO1. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite e. *) + (* rewrite Integers.Ptrofs.unsigned_repr. *) + (* exact H1. *) + (* apply Integers.Ptrofs.unsigned_range_2. } *) + (* crush. *) + (* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *) + (* destruct (Archi.ptr64); try discriminate. *) + (* pose proof (RSBP src). rewrite EQ_SRC in H14. *) + (* assumption. *) + + (* simpl. *) + (* erewrite Mem.load_store_other with (m1 := m). *) + (* 2: { exact H1. } *) + (* 2: { right. *) + (* rewrite ZERO1. *) + (* 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. *) + (* rewrite HeqOFFSET in *. simplify_val. *) + (* left; auto. *) + (* rewrite HeqOFFSET in *. simplify_val. *) + (* right. *) + (* apply ZExtra.mod_0_bounds; try lia. *) + (* apply ZLib.Z_mod_mult'. *) + (* inv H14. *) + (* apply Zmult_lt_compat_r with (p := 4) in H16; try lia. *) + (* rewrite ZLib.div_mul_undo in H16; try lia. *) + (* split; try lia. *) + (* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) + (* } *) + (* apply ASBP; assumption. *) + + (* unfold stack_bounds in *. intros. *) + (* simpl. *) + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* erewrite Mem.load_store_other with (m1 := m). *) + (* 2: { exact H1. } *) + (* 2: { rewrite HeqOFFSET in *. simplify_val. *) + (* right. right. simpl. *) + (* rewrite ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *) + (* apply ZExtra.mod_0_bounds; crush; try lia. } *) + (* crush. *) + (* exploit (BOUNDS ptr); try lia. intros. crush. *) + (* exploit (BOUNDS ptr v); try lia. intros. *) + (* simplify. *) + (* match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *) + (* assert (Mem.valid_access m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) Writable). *) + (* { pose proof H1. eapply Mem.store_valid_access_2 in H14. *) + (* exact H14. eapply Mem.store_valid_access_3. eassumption. } *) + (* pose proof (Mem.valid_access_store m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) v). *) + (* apply X in H14. inv H14. congruence. *) + + (* constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. *) + (* assumption. lia. *) + (* unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. *) + (* assumption. lia. *) + + (* + inv MARR. inv CONST. crush. *) + + (* unfold Op.eval_addressing in H0. *) + (* destruct (Archi.ptr64) eqn:ARCHI; crush. *) + (* rewrite ARCHI in H0. crush. *) + + (* unfold check_address_parameter_unsigned in *; *) + (* unfold check_address_parameter_signed in *; crush. *) + + (* 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. *) + + (* (** Modular preservation proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *) + (* { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. *) + (* apply Zdivide_mod. assumption. } *) + + (* (** Write bounds proof *) *) + (* assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *) + (* { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:?EQ; crush; auto. *) + (* unfold stack_bounds in BOUNDS. *) + (* exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *) + (* crush. *) + (* replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. *) + (* small_tac. } *) + + (* (** Start of proof proper *) *) + (* eexists. split. *) + (* eapply Smallstep.plus_one. *) + (* eapply HTL.step_module; eauto. *) + (* econstructor. econstructor. econstructor. *) + (* eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *) + (* econstructor. econstructor. econstructor. econstructor. *) + + (* all: try constructor; crush. *) + + (* (** State Lookup *) *) + (* unfold Verilog.merge_regs. *) + (* crush. *) + (* unfold_merge. *) + (* apply AssocMap.gss. *) + + (* (** Match states *) *) + (* econstructor; eauto. *) + + (* (** Match assocmaps *) *) + (* unfold Verilog.merge_regs. crush. unfold_merge. *) + (* apply regs_lessdef_add_greater. *) + (* unfold Plt; lia. *) + (* assumption. *) + + (* (** States well formed *) *) + (* unfold state_st_wf. inversion 1. crush. *) + (* unfold Verilog.merge_regs. *) + (* unfold_merge. *) + (* apply AssocMap.gss. *) + + (* (** Equality proof *) *) + + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *) + + (* econstructor. *) + (* repeat split; crush. *) + (* unfold HTL.empty_stack. *) + (* crush. *) + (* unfold Verilog.merge_arrs. *) + + (* rewrite AssocMap.gcombine by reflexivity. *) + (* rewrite AssocMap.gss. *) + (* erewrite Verilog.merge_arr_empty2. *) + (* unfold Verilog.arr_assocmap_set. *) + (* rewrite AssocMap.gcombine by reflexivity. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. *) + (* unfold Verilog.merge_arr. *) + (* setoid_rewrite H7. *) + (* reflexivity. *) + + (* rewrite AssocMap.gcombine by reflexivity. *) + (* unfold Verilog.merge_arr. *) + (* unfold Verilog.arr_assocmap_set. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. *) + (* setoid_rewrite H7. *) + (* reflexivity. *) + + (* rewrite combine_length. *) + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* symmetry. *) + (* apply list_repeat_len. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite H4. *) + (* apply list_repeat_len. *) + + (* rewrite combine_length. *) + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* apply list_repeat_len. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite H4. *) + (* apply list_repeat_len. *) + + (* remember i0 as OFFSET. *) + (* 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 H8. *) + (* destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H8; eauto. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite list_repeat_len. auto. *) + + (* assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *) + (* rewrite Z.mul_comm in H8. *) + (* rewrite Z_div_mult in H8; try lia. *) + (* replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity. *) + (* rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia. *) + (* rewrite H8. rewrite <- offset_expr_ok_3. *) + (* 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'. *) + (* rewrite Z2Nat.id in H13; try lia. *) + (* apply Zmult_lt_compat_r with (p := 4) in H13; try lia. *) + (* rewrite ZLib.div_mul_undo in H13; try lia. *) + (* split; try lia. *) + (* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) + (* } *) + + (* rewrite <- offset_expr_ok_3. *) + (* 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 H9; eauto. *) + + (* rewrite <- array_set_len. *) + (* unfold arr_repeat. crush. *) + (* rewrite list_repeat_len. auto. *) + (* rewrite array_gso. *) + (* unfold array_get_error. *) + (* unfold arr_repeat. *) + (* crush. *) + (* apply list_repeat_lookup. *) + (* lia. *) + (* unfold_constants. *) + (* intro. *) + (* apply Z2Nat.inj_iff in H8; 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). *) + + (* crush. *) + (* 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. } *) + (* crush. *) + (* 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'. *) + (* inv H0. *) + (* apply Zmult_lt_compat_r with (p := 4) in H11; try lia. *) + (* rewrite ZLib.div_mul_undo in H11; try lia. *) + (* split; try lia. *) + (* apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *) + (* } *) + (* apply ASBP; assumption. *) + + (* unfold stack_bounds in *. intros. *) + (* simpl. *) + (* assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *) + (* erewrite Mem.load_store_other with (m1 := m). *) + (* 2: { exact H1. } *) + (* 2: { right. right. simpl. *) + (* rewrite ZERO. *) + (* rewrite Integers.Ptrofs.add_zero_l. *) + (* rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *) + (* apply ZExtra.mod_0_bounds; crush; try lia. } *) + (* crush. *) + (* exploit (BOUNDS ptr); try lia. intros. crush. *) + (* exploit (BOUNDS ptr v); try lia. intros. *) + (* inv H0. *) + (* match goal with | |- ?x = _ => destruct x eqn:?EQ end; try reflexivity. *) + (* assert (Mem.valid_access m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) Writable). *) + (* { pose proof H1. eapply Mem.store_valid_access_2 in H0. *) + (* exact H0. eapply Mem.store_valid_access_3. eassumption. } *) + (* pose proof (Mem.valid_access_store m AST.Mint32 sp' *) + (* (Integers.Ptrofs.unsigned *) + (* (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *) + (* (Integers.Ptrofs.repr ptr))) v). *) + (* apply X in H0. inv H0. congruence. *) + + (* constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. *) + (* assumption. lia. *) + (* unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. *) + (* assumption. lia. *) + + (* Unshelve. *) + (* exact tt. *) + (* exact (Values.Vint (Int.repr 0)). *) + (* exact tt. *) + (* exact (Values.Vint (Int.repr 0)). *) + (* exact tt. *) + (* exact (Values.Vint (Int.repr 0)). *) + (* Qed. *) Admitted. #[local] Hint Resolve transl_istore_correct : htlproof. Lemma transl_icond_correct: @@ -2532,48 +2643,48 @@ rs assoc``. intros. eapply RTL.max_reg_function_use. apply H22. auto. econstructor. auto. simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. - apply AssocMap.gss. + unfold_merge. apply AssocMap.gss. inv MARR. inv CONST. big_tac. - constructor; rewrite AssocMap.gso; simplify; try assumption; lia. - - eexists. split. apply Smallstep.plus_one. - clear H32. - eapply HTL.step_module; eauto. - inv CONST; assumption. - inv CONST; assumption. - econstructor; simpl; trivial. - constructor; trivial. - eapply Verilog.erun_Vternary_false; simpl; eauto. - eapply eval_cond_correct; eauto. intros. - intros. eapply RTL.max_reg_function_use. apply H22. auto. - econstructor. auto. - simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. - apply AssocMap.gss. - - inv MARR. inv CONST. - big_tac. - constructor; rewrite AssocMap.gso; simplify; try assumption; lia. - - Unshelve. all: exact tt. - Qed. + (* constructor; rewrite AssocMap.gso; simplify; try assumption; lia. *) + (* - eexists. split. apply Smallstep.plus_one. *) + (* clear H32. *) + (* eapply HTL.step_module; eauto. *) + (* inv CONST; assumption. *) + (* inv CONST; assumption. *) + (* econstructor; simpl; trivial. *) + (* constructor; trivial. *) + (* eapply Verilog.erun_Vternary_false; simpl; eauto. *) + (* eapply eval_cond_correct; eauto. intros. *) + (* intros. eapply RTL.max_reg_function_use. apply H22. auto. *) + (* econstructor. auto. *) + (* simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. *) + (* apply AssocMap.gss. *) + + (* inv MARR. inv CONST. *) + (* big_tac. *) + (* constructor; rewrite AssocMap.gso; simplify; try assumption; lia. *) + + (* Unshelve. all: exact tt. *) + (* Qed. *) Admitted. #[local] Hint Resolve transl_icond_correct : htlproof. - (*Lemma transl_ijumptable_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) - (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) - (n : Integers.Int.int) (pc' : RTL.node), - (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> - Registers.Regmap.get arg rs = Values.Vint n -> - list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> - forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. - Proof. - intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. - - #[local] Hint Resolve transl_ijumptable_correct : htlproof.*) + (*Lemma transl_ijumptable_correct: *) + (* forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *) + (* (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) *) + (* (n : Integers.Int.int) (pc' : RTL.node), *) + (* (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> *) + (* Registers.Regmap.get arg rs = Values.Vint n -> *) + (* list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> *) + (* forall R1 : HTL.state, *) + (* match_states (RTL.State s f sp pc rs m) R1 -> *) + (* exists R2 : HTL.state, *) + (* Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *) + (* Proof. *) + (* intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. *) + + (* #[local] Hint Resolve transl_ijumptable_correct : htlproof.*) Lemma transl_ireturn_correct: forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) @@ -2613,54 +2724,54 @@ rs assoc``. apply HTL.step_finish. unfold Verilog.merge_regs. unfold_merge; simpl. - rewrite AssocMap.gso. - apply AssocMap.gss. lia. - apply AssocMap.gss. - rewrite Events.E0_left. reflexivity. - - constructor; auto. - constructor. - - (* FIXME: Duplication *) - - econstructor. split. - eapply Smallstep.plus_two. - eapply HTL.step_module; eauto. - inv CONST; assumption. - inv CONST; assumption. - constructor. - econstructor; simpl; trivial. - econstructor; simpl; trivial. - constructor. constructor. constructor. - constructor. constructor. constructor. - constructor. - - unfold state_st_wf in WF; big_tac; eauto. - - destruct wf1 as [HCTRL HDATA]. apply HCTRL. - apply AssocMapExt.elements_iff. eexists. - match goal with H: control ! pc = Some _ |- _ => apply H end. - - apply HTL.step_finish. - unfold Verilog.merge_regs. - unfold_merge. - unfold_merge. - rewrite AssocMap.gso. - apply AssocMap.gss. simpl; lia. - apply AssocMap.gss. - rewrite Events.E0_left. trivial. - - constructor; auto. - - simpl. inversion MASSOC. subst. - unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. - apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. - assert (HPle : Ple r (RTL.max_reg_function f)). - eapply RTL.max_reg_function_use. eassumption. simpl; auto. - apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - - Unshelve. - all: constructor. - Qed. + (* rewrite AssocMap.gso. *) + (* apply AssocMap.gss. lia. *) + (* apply AssocMap.gss. *) + (* rewrite Events.E0_left. reflexivity. *) + + (* constructor; auto. *) + (* constructor. *) + + (* (* FIXME: Duplication *) *) + (* - econstructor. split. *) + (* eapply Smallstep.plus_two. *) + (* eapply HTL.step_module; eauto. *) + (* inv CONST; assumption. *) + (* inv CONST; assumption. *) + (* constructor. *) + (* econstructor; simpl; trivial. *) + (* econstructor; simpl; trivial. *) + (* constructor. constructor. constructor. *) + (* constructor. constructor. constructor. *) + (* constructor. *) + + (* unfold state_st_wf in WF; big_tac; eauto. *) + + (* destruct wf1 as [HCTRL HDATA]. apply HCTRL. *) + (* apply AssocMapExt.elements_iff. eexists. *) + (* match goal with H: control ! pc = Some _ |- _ => apply H end. *) + + (* apply HTL.step_finish. *) + (* unfold Verilog.merge_regs. *) + (* unfold_merge. *) + (* unfold_merge. *) + (* rewrite AssocMap.gso. *) + (* apply AssocMap.gss. simpl; lia. *) + (* apply AssocMap.gss. *) + (* rewrite Events.E0_left. trivial. *) + + (* constructor; auto. *) + + (* simpl. inversion MASSOC. subst. *) + (* unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. *) + (* apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. *) + (* assert (HPle : Ple r (RTL.max_reg_function f)). *) + (* eapply RTL.max_reg_function_use. eassumption. simpl; auto. *) + (* apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *) + + (* Unshelve. *) + (* all: constructor. *) + (* Qed. *) Admitted. #[local] Hint Resolve transl_ireturn_correct : htlproof. Lemma transl_callstate_correct: @@ -2866,13 +2977,13 @@ rs assoc``. Proof. induction 1; eauto with htlproof; (intros; inv_state). Qed. - #[local] Hint Resolve transl_step_correct : htlproof.*) + #[local] Hint Resolve transl_step_correct : htlproof. Theorem transf_program_correct: Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). Proof. eapply Smallstep.forward_simulation_plus; eauto with htlproof. apply senv_preserved. - (*Qed.*)Admitted. + Qed. End CORRECTNESS. |