diff options
Diffstat (limited to 'src/hls/Memorygen.v')
| -rw-r--r-- | src/hls/Memorygen.v | 3201 |
1 files changed, 0 insertions, 3201 deletions
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v deleted file mode 100644 index 34e264d..0000000 --- a/src/hls/Memorygen.v +++ /dev/null @@ -1,3201 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see <https://www.gnu.org/licenses/>. - *) - -Require Import Coq.micromega.Lia. - -Require Import compcert.backend.Registers. -Require Import compcert.common.AST. -Require Import compcert.common.Globalenvs. -Require compcert.common.Memory. -Require Import compcert.common.Values. -Require Import compcert.lib.Floats. -Require Import compcert.lib.Integers. -Require Import compcert.lib.Maps. -Require compcert.common.Smallstep. -Require compcert.verilog.Op. - -Require Import vericert.common.Vericertlib. -Require Import vericert.hls.ValueInt. -Require Import vericert.hls.Verilog. -Require Import vericert.hls.HTL. -Require Import vericert.hls.AssocMap. -Require Import vericert.hls.Array. - -Local Open Scope positive. -Local Open Scope assocmap. - -#[local] Hint Resolve max_reg_stmnt_le_stmnt_tree : mgen. -#[local] Hint Resolve max_reg_stmnt_lt_stmnt_tree : mgen. -#[local] Hint Resolve max_stmnt_lt_module : mgen. - -Lemma int_eq_not_false : forall x, Int.eq x (Int.not x) = false. -Proof. - intros. unfold Int.eq. - rewrite Int.unsigned_not. - replace Int.max_unsigned with 4294967295%Z by crush. - assert (X: forall x, (x <> 4294967295 - x)%Z) by lia. - specialize (X (Int.unsigned x)). apply zeq_false; auto. -Qed. - -Definition transf_maps state ram in_ (dc: PTree.t stmnt * PTree.t stmnt) := - match dc, in_ with - | (d, c), (i, n) => - match PTree.get i d, PTree.get i c with - | Some (Vnonblock (Vvari r e1) e2), Some c_s => - if r =? (ram_mem ram) then - let nd := Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) - (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) - (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2) - (Vnonblock (Vvar (ram_addr ram)) e1))) - in - (PTree.set i nd d, c) - else dc - | Some (Vnonblock (Vvar e1) (Vvari r e2)), Some (Vnonblock (Vvar st') e3) => - if (r =? (ram_mem ram)) && (st' =? state) && (Z.pos n <=? Int.max_unsigned)%Z - && (e1 <? state) && (max_reg_expr e2 <? state) && (max_reg_expr e3 <? state) - then - let nd := - Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) - (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) - (Vnonblock (Vvar (ram_addr ram)) e2)) - in - let aout := Vnonblock (Vvar e1) (Vvar (ram_d_out ram)) in - let redirect := Vnonblock (Vvar state) (Vlit (posToValue n)) in - (PTree.set i nd (PTree.set n aout d), - PTree.set i redirect (PTree.set n (Vnonblock (Vvar st') e3) c)) - else dc - | _, _ => dc - end - end. - -Lemma transf_maps_wf : - forall state ram d c d' c' i, - map_well_formed c /\ map_well_formed d -> - transf_maps state ram i (d, c) = (d', c') -> - map_well_formed c' /\ map_well_formed d'. -Proof. - unfold transf_maps; intros; repeat destruct_match; - match goal with - | H: (_, _) = (_, _) |- _ => inv H - end; auto. - unfold map_well_formed. - simplify; intros. - destruct (Pos.eq_dec p0 p1); subst; auto. - destruct (Pos.eq_dec p p1); subst. unfold map_well_formed in *. - apply AssocMap.elements_correct in Heqo. - eapply in_map with (f := fst) in Heqo. simplify. - apply H1 in Heqo. auto. - apply AssocMapExt.elements_iff in H3. inv H3. - repeat rewrite AssocMap.gso in H8 by lia. - apply AssocMap.elements_correct in H8. - eapply in_map with (f := fst) in H8. simplify. - unfold map_well_formed in *. apply H0 in H8. auto. - apply AssocMapExt.elements_iff in H3. inv H3. - destruct (Pos.eq_dec p0 p1); subst; auto. - destruct (Pos.eq_dec p p1); subst. unfold map_well_formed in *. - apply AssocMap.elements_correct in Heqo. - eapply in_map with (f := fst) in Heqo. simplify. - apply H1 in Heqo. auto. - repeat rewrite AssocMap.gso in H8 by lia. - apply AssocMap.elements_correct in H8. - eapply in_map with (f := fst) in H8. simplify. - unfold map_well_formed in *. apply H1 in H8. auto. - unfold map_well_formed in *; simplify; intros. - destruct (Pos.eq_dec p0 p1); subst; auto. - destruct (Pos.eq_dec p p1); subst. unfold map_well_formed in *. - apply AssocMap.elements_correct in Heqo. - eapply in_map with (f := fst) in Heqo. simplify. - apply H1 in Heqo. auto. - apply AssocMapExt.elements_iff in H. inv H. - repeat rewrite AssocMap.gso in H2 by lia. - apply AssocMap.elements_correct in H2. - eapply in_map with (f := fst) in H2. simplify. - unfold map_well_formed in *. apply H1 in H2. auto. -Qed. - -Definition max_pc {A: Type} (m: PTree.t A) := - fold_right Pos.max 1%positive (map fst (PTree.elements m)). - -Fixpoint zip_range {A: Type} n (l: list A) {struct l} := - match l with - | nil => nil - | a :: b => (a, n) :: zip_range (n+1) b - end. - -Lemma zip_range_fst_idem : forall A (l: list A) a, map fst (zip_range a l) = l. -Proof. induction l; crush. Qed. - -Lemma zip_range_not_in_snd : - forall A (l: list A) a n, a < n -> ~ In a (map snd (zip_range n l)). -Proof. - unfold not; induction l; crush. - inv H0; try lia. eapply IHl. - assert (X: a0 < n + 1) by lia. apply X; auto. auto. -Qed. - -Lemma zip_range_snd_no_repet : - forall A (l: list A) a, list_norepet (map snd (zip_range a l)). -Proof. - induction l; crush; constructor; auto; []. - apply zip_range_not_in_snd; lia. -Qed. - -Lemma zip_range_in : - forall A (l: list A) a n i, In (a, i) (zip_range n l) -> In a l. -Proof. - induction l; crush. inv H. inv H0. auto. right. eapply IHl; eauto. -Qed. - -Lemma zip_range_not_in : - forall A (l: list A) a i n, ~ In a l -> ~ In (a, i) (zip_range n l). -Proof. - unfold not; induction l; crush. inv H0. inv H1. apply H. left. auto. - apply H. right. eapply zip_range_in; eauto. -Qed. - -Lemma zip_range_no_repet : - forall A (l: list A) a, list_norepet l -> list_norepet (zip_range a l). -Proof. - induction l; simplify; constructor; - match goal with H: list_norepet _ |- _ => inv H end; - [apply zip_range_not_in|]; auto. -Qed. - -Definition transf_code state ram d c := - fold_right (transf_maps state ram) (d, c) - (zip_range (Pos.max (max_pc c) (max_pc d) + 1) - (map fst (PTree.elements d))). - -Lemma transf_code_wf' : - forall l c d state ram c' d', - map_well_formed c /\ map_well_formed d -> - fold_right (transf_maps state ram) (d, c) l = (d', c') -> - map_well_formed c' /\ map_well_formed d'. -Proof. - induction l; intros; simpl in *. inv H0; auto. - remember (fold_right (transf_maps state ram) (d, c) l). destruct p. - apply transf_maps_wf in H0. auto. eapply IHl; eauto. -Qed. - -Lemma transf_code_wf : - forall c d state ram c' d', - map_well_formed c /\ map_well_formed d -> - transf_code state ram d c = (d', c') -> - map_well_formed c' /\ map_well_formed d'. -Proof. eauto using transf_code_wf'. Qed. - -Lemma ram_wf : - forall x, - x + 1 < x + 2 /\ x + 2 < x + 3 /\ x + 3 < x + 4 /\ x + 4 < x + 5 /\ x + 5 < x + 6. -Proof. lia. Qed. - -Lemma module_ram_wf' : - forall m addr, - addr = max_reg_module m + 1 -> - mod_clk m < addr. -Proof. unfold max_reg_module; lia. Qed. - -Definition transf_module (m: module): module. - refine ( - let max_reg := max_reg_module m in - let addr := max_reg+1 in - let en := max_reg+2 in - let d_in := max_reg+3 in - let d_out := max_reg+4 in - let wr_en := max_reg+5 in - let u_en := max_reg+6 in - let new_size := (mod_stk_len m) in - let ram := mk_ram new_size (mod_stk m) en u_en addr wr_en d_in d_out ltac:(eauto using ram_wf) in - let tc := transf_code (mod_st m) ram (mod_datapath m) (mod_controllogic m) in - match mod_ram m with - | None => - mkmodule m.(mod_params) - (fst tc) - (snd tc) - (mod_entrypoint m) - (mod_st m) - (mod_stk m) - (mod_stk_len m) - (mod_finish m) - (mod_return m) - (mod_start m) - (mod_reset m) - (mod_clk m) - (AssocMap.set u_en (None, VScalar 1) - (AssocMap.set en (None, VScalar 1) - (AssocMap.set wr_en (None, VScalar 1) - (AssocMap.set d_out (None, VScalar 32) - (AssocMap.set d_in (None, VScalar 32) - (AssocMap.set addr (None, VScalar 32) m.(mod_scldecls))))))) - (AssocMap.set m.(mod_stk) - (None, VArray 32 (2 ^ Nat.log2_up new_size))%nat m.(mod_arrdecls)) - (Some ram) - _ (mod_ordering_wf m) _ (mod_params_wf m) - | _ => m - end). - eapply transf_code_wf. apply (mod_wf m). destruct tc eqn:?; simpl. - rewrite <- Heqp. intuition. - inversion 1; subst. auto using module_ram_wf'. -Defined. - -Definition transf_fundef := transf_fundef transf_module. - -Definition transf_program (p : program) := - transform_program transf_fundef p. - -Inductive match_assocmaps : positive -> assocmap -> assocmap -> Prop := - match_assocmap: forall p rs rs', - (forall r, r < p -> rs!r = rs'!r) -> - match_assocmaps p rs rs'. - -Inductive match_arrs : assocmap_arr -> assocmap_arr -> Prop := -| match_assocmap_arr_intro: forall ar ar', - (forall s arr, - ar ! s = Some arr -> - exists arr', - ar' ! s = Some arr' - /\ (forall addr, - array_get_error addr arr = array_get_error addr arr') - /\ arr_length arr = arr_length arr')%nat -> - (forall s, ar ! s = None -> ar' ! s = None) -> - match_arrs ar ar'. - -Inductive match_arrs_size : assocmap_arr -> assocmap_arr -> Prop := - match_arrs_size_intro : - forall nasa basa, - (forall s arr, - nasa ! s = Some arr -> - exists arr', - basa ! s = Some arr' /\ arr_length arr = arr_length arr') -> - (forall s arr, - basa ! s = Some arr -> - exists arr', - nasa ! s = Some arr' /\ arr_length arr = arr_length arr') -> - (forall s, basa ! s = None <-> nasa ! s = None) -> - match_arrs_size nasa basa. - -Definition match_empty_size (m : module) (ar : assocmap_arr) : Prop := - match_arrs_size (empty_stack m) ar. -#[local] Hint Unfold match_empty_size : mgen. - -Definition disable_ram (ram: option ram) (asr : assocmap_reg) : Prop := - match ram with - | Some r => Int.eq (asr # ((ram_en r), 32)) (asr # ((ram_u_en r), 32)) = true - | None => True - end. - -Inductive match_stackframes : stackframe -> stackframe -> Prop := - match_stackframe_intro : - forall r m pc asr asa asr' asa' - (DISABLE_RAM: disable_ram (mod_ram (transf_module m)) asr') - (MATCH_ASSOC: match_assocmaps (max_reg_module m + 1) asr asr') - (MATCH_ARRS: match_arrs asa asa') - (MATCH_EMPT1: match_empty_size m asa) - (MATCH_EMPT2: match_empty_size m asa') - (MATCH_RES: r < mod_st m), - match_stackframes (Stackframe r m pc asr asa) - (Stackframe r (transf_module m) pc asr' asa'). - -Inductive match_states : state -> state -> Prop := -| match_state : - forall res res' m st asr asr' asa asa' - (ASSOC: match_assocmaps (max_reg_module m + 1) asr asr') - (ARRS: match_arrs asa asa') - (STACKS: list_forall2 match_stackframes res res') - (ARRS_SIZE: match_empty_size m asa) - (ARRS_SIZE2: match_empty_size m asa') - (DISABLE_RAM: disable_ram (mod_ram (transf_module m)) asr'), - match_states (State res m st asr asa) - (State res' (transf_module m) st asr' asa') -| match_returnstate : - forall res res' i - (STACKS: list_forall2 match_stackframes res res'), - match_states (Returnstate res i) (Returnstate res' i) -| match_initial_call : - forall m, - match_states (Callstate nil m nil) - (Callstate nil (transf_module m) nil). -#[local] Hint Constructors match_states : htlproof. - -Definition empty_stack_ram r := - AssocMap.set (ram_mem r) (Array.arr_repeat None (ram_size r)) (AssocMap.empty arr). - -Definition empty_stack' len st := - AssocMap.set st (Array.arr_repeat None len) (AssocMap.empty arr). - -Definition match_empty_size' l s (ar : assocmap_arr) : Prop := - match_arrs_size (empty_stack' l s) ar. -#[local] Hint Unfold match_empty_size : mgen. - -Definition merge_reg_assocs r := - Verilog.mkassociations (Verilog.merge_regs (assoc_nonblocking r) (assoc_blocking r)) empty_assocmap. - -Definition merge_arr_assocs st len r := - Verilog.mkassociations (Verilog.merge_arrs (assoc_nonblocking r) (assoc_blocking r)) (empty_stack' len st). - -Inductive match_reg_assocs : positive -> reg_associations -> reg_associations -> Prop := - match_reg_association: - forall p rab rab' ran ran', - match_assocmaps p rab rab' -> - match_assocmaps p ran ran' -> - match_reg_assocs p (mkassociations rab ran) (mkassociations rab' ran'). - -Inductive match_arr_assocs : arr_associations -> arr_associations -> Prop := - match_arr_association: - forall rab rab' ran ran', - match_arrs rab rab' -> - match_arrs ran ran' -> - match_arr_assocs (mkassociations rab ran) (mkassociations rab' ran'). - -Ltac mgen_crush := crush; eauto with mgen. - -Lemma match_assocmaps_equiv : forall p a, match_assocmaps p a a. -Proof. constructor; auto. Qed. -#[local] Hint Resolve match_assocmaps_equiv : mgen. - -Lemma match_arrs_equiv : forall a, match_arrs a a. -Proof. econstructor; mgen_crush. Qed. -#[local] Hint Resolve match_arrs_equiv : mgen. - -Lemma match_reg_assocs_equiv : forall p a, match_reg_assocs p a a. -Proof. destruct a; constructor; mgen_crush. Qed. -#[local] Hint Resolve match_reg_assocs_equiv : mgen. - -Lemma match_arr_assocs_equiv : forall a, match_arr_assocs a a. -Proof. destruct a; constructor; mgen_crush. Qed. -#[local] Hint Resolve match_arr_assocs_equiv : mgen. - -Lemma match_arrs_size_equiv : forall a, match_arrs_size a a. -Proof. intros; repeat econstructor; eauto. Qed. -#[local] Hint Resolve match_arrs_size_equiv : mgen. - -Lemma match_stacks_equiv : - forall m s l, - mod_stk m = s -> - mod_stk_len m = l -> - empty_stack' l s = empty_stack m. -Proof. unfold empty_stack', empty_stack; mgen_crush. Qed. -#[local] Hint Rewrite match_stacks_equiv : mgen. - -Lemma match_assocmaps_max1 : - forall p p' a b, - match_assocmaps (Pos.max p' p) a b -> - match_assocmaps p a b. -Proof. - intros. inv H. constructor. intros. - apply H0. lia. -Qed. -#[local] Hint Resolve match_assocmaps_max1 : mgen. - -Lemma match_assocmaps_max2 : - forall p p' a b, - match_assocmaps (Pos.max p p') a b -> - match_assocmaps p a b. -Proof. - intros. inv H. constructor. intros. - apply H0. lia. -Qed. -#[local] Hint Resolve match_assocmaps_max2 : mgen. - -Lemma match_assocmaps_ge : - forall p p' a b, - match_assocmaps p' a b -> - p <= p' -> - match_assocmaps p a b. -Proof. - intros. inv H. constructor. intros. - apply H1. lia. -Qed. -#[local] Hint Resolve match_assocmaps_ge : mgen. - -Lemma match_reg_assocs_max1 : - forall p p' a b, - match_reg_assocs (Pos.max p' p) a b -> - match_reg_assocs p a b. -Proof. intros; inv H; econstructor; mgen_crush. Qed. -#[local] Hint Resolve match_reg_assocs_max1 : mgen. - -Lemma match_reg_assocs_max2 : - forall p p' a b, - match_reg_assocs (Pos.max p p') a b -> - match_reg_assocs p a b. -Proof. intros; inv H; econstructor; mgen_crush. Qed. -#[local] Hint Resolve match_reg_assocs_max2 : mgen. - -Lemma match_reg_assocs_ge : - forall p p' a b, - match_reg_assocs p' a b -> - p <= p' -> - match_reg_assocs p a b. -Proof. intros; inv H; econstructor; mgen_crush. Qed. -#[local] Hint Resolve match_reg_assocs_ge : mgen. - -Definition forall_ram (P: reg -> Prop) ram := - P (ram_en ram) - /\ P (ram_u_en ram) - /\ P (ram_addr ram) - /\ P (ram_wr_en ram) - /\ P (ram_d_in ram) - /\ P (ram_d_out ram). - -Lemma forall_ram_lt : - forall m r, - (mod_ram m) = Some r -> - forall_ram (fun x => x < max_reg_module m + 1) r. -Proof. - assert (X: forall a b c, a < b + 1 -> a < Pos.max c b + 1) by lia. - unfold forall_ram; simplify; unfold HTL.max_reg_module; repeat apply X; - unfold HTL.max_reg_ram; rewrite H; try lia. -Qed. -#[local] Hint Resolve forall_ram_lt : mgen. - -Definition exec_all d_s c_s rs1 ar1 rs3 ar3 := - exists f rs2 ar2, - stmnt_runp f rs1 ar1 c_s rs2 ar2 - /\ stmnt_runp f rs2 ar2 d_s rs3 ar3. - -Definition exec_all_ram r d_s c_s rs1 ar1 rs4 ar4 := - exists f rs2 ar2 rs3 ar3, - stmnt_runp f rs1 ar1 c_s rs2 ar2 - /\ stmnt_runp f rs2 ar2 d_s rs3 ar3 - /\ exec_ram (merge_reg_assocs rs3) (merge_arr_assocs (ram_mem r) (ram_size r) ar3) (Some r) rs4 ar4. - -(* Lemma merge_reg_idempotent : *) -(* forall rs p, *) -(* match_reg_assocs p (merge_reg_assocs (merge_reg_assocs rs)) (merge_reg_assocs rs). *) -(* Proof. intros. unfold merge_reg_assocs. cbn. unfold merge_regs. *) -(* #[global] Hint Rewrite merge_reg_idempotent : mgen. *) - -Lemma merge_arr_idempotent : - forall ar st len v v', - (assoc_nonblocking ar)!st = Some v -> - (assoc_blocking ar)!st = Some v' -> - arr_length v' = len -> - arr_length v = len -> - (assoc_blocking (merge_arr_assocs st len (merge_arr_assocs st len ar)))!st - = (assoc_blocking (merge_arr_assocs st len ar))!st - /\ (assoc_nonblocking (merge_arr_assocs st len (merge_arr_assocs st len ar)))!st - = (assoc_nonblocking (merge_arr_assocs st len ar))!st. -Proof. - split; simplify; eauto. - unfold merge_arrs. - rewrite AssocMap.gcombine by reflexivity. - unfold empty_stack'. - (* rewrite AssocMap.gss. *) - (* setoid_rewrite merge_arr_empty2; auto. *) - (* rewrite AssocMap.gcombine by reflexivity. *) - (* unfold merge_arr, arr. *) - (* rewrite H. rewrite H0. auto. *) - (* unfold combine. *) - (* simplify. *) - (* rewrite list_combine_length. *) - (* rewrite (arr_wf v). rewrite (arr_wf v'). *) - (* lia. *) -(* Qed. *) Admitted. - -Lemma empty_arr : - forall m s, - (exists l, (empty_stack m) ! s = Some (arr_repeat None l)) - \/ (empty_stack m) ! s = None. -Proof. - unfold empty_stack. simplify. - destruct (Pos.eq_dec s (mod_stk m)); subst. - left. eexists. apply AssocMap.gss. - right. rewrite AssocMap.gso; auto. -Qed. - -Lemma merge_arr_empty': - forall m ar s v, - match_empty_size m ar -> - (merge_arrs (empty_stack m) ar) ! s = v -> - ar ! s = v. -Proof. - inversion 1; subst. - pose proof (empty_arr m s). - simplify. - destruct (merge_arrs (empty_stack m) ar) ! s eqn:?; subst. - - inv H3. inv H4. - learn H3 as H5. apply H0 in H5. inv H5. simplify. - unfold merge_arrs in *. (* rewrite AssocMap.gcombine in Heqo; auto. *) - (* rewrite H3 in Heqo. erewrite merge_arr_empty2 in Heqo. auto. eauto. *) - (* rewrite list_repeat_len in H6. auto. *) - (* learn H4 as H6. apply H2 in H6. *) - (* unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto. *) - (* rewrite H4 in Heqo. unfold Verilog.arr in *. rewrite H6 in Heqo. *) - (* discriminate. *) - (* - inv H3. inv H4. learn H3 as H4. apply H0 in H4. inv H4. simplify. *) - (* rewrite list_repeat_len in H6. *) - (* unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto. rewrite H3 in Heqo. *) - (* unfold Verilog.arr in *. rewrite H4 in Heqo. *) - (* discriminate. *) - (* apply H2 in H4; auto. *) -(* Qed. *) Admitted. - -Lemma merge_arr_empty : - forall m ar ar', - match_empty_size m ar -> - match_arrs ar ar' -> - match_arrs (merge_arrs (empty_stack m) ar) ar'. -Proof. - inversion 1; subst; inversion 1; subst; - econstructor; intros; apply merge_arr_empty' in H6; auto. -Qed. -#[local] Hint Resolve merge_arr_empty : mgen. - -Lemma merge_arr_empty'': - forall m ar s v, - match_empty_size m ar -> - ar ! s = v -> - (merge_arrs (empty_stack m) ar) ! s = v. -Proof. - inversion 1; subst. - pose proof (empty_arr m s). - simplify. - destruct (merge_arrs (empty_stack m) ar) ! s eqn:?; subst. - - inv H3. inv H4. - learn H3 as H5. apply H0 in H5. inv H5. simplify. - unfold merge_arrs in *. (* rewrite AssocMap.gcombine in Heqo; auto. *) -(* rewrite H3 in Heqo. erewrite merge_arr_empty2 in Heqo. auto. eauto. *) -(* rewrite list_repeat_len in H6. auto. *) -(* learn H4 as H6. apply H2 in H6. *) -(* unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto. *) -(* rewrite H4 in Heqo. unfold Verilog.arr in *. rewrite H6 in Heqo. *) -(* discriminate. *) -(* - inv H3. inv H4. learn H3 as H4. apply H0 in H4. inv H4. simplify. *) -(* rewrite list_repeat_len in H6. *) -(* unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto. rewrite H3 in Heqo. *) -(* unfold Verilog.arr in *. rewrite H4 in Heqo. *) -(* discriminate. *) -(* apply H2 in H4; auto. *) -(* Qed. *) Admitted. - -Lemma merge_arr_empty_match : - forall m ar, - match_empty_size m ar -> - match_empty_size m (merge_arrs (empty_stack m) ar). -Proof. - inversion 1; subst. - constructor; simplify. - learn H3 as H4. apply H0 in H4. inv H4. simplify. - eexists; split; eauto. apply merge_arr_empty''; eauto. - apply merge_arr_empty' in H3; auto. - split; simplify. - unfold merge_arrs in H3. (* rewrite AssocMap.gcombine in H3; auto. *) -(* unfold merge_arr in *. *) -(* destruct (empty_stack m) ! s eqn:?; *) -(* destruct ar ! s; try discriminate; eauto. *) -(* apply merge_arr_empty''; auto. apply H2 in H3; auto. *) -(* Qed. *) Admitted. -#[local] Hint Resolve merge_arr_empty_match : mgen. - -Definition ram_present {A: Type} ar r v v' := - (assoc_nonblocking ar)!(ram_mem r) = Some v - /\ @arr_length A v = ram_size r - /\ (assoc_blocking ar)!(ram_mem r) = Some v' - /\ arr_length v' = ram_size r. - -Lemma find_assoc_get : - forall rs r trs, - rs ! r = trs ! r -> - rs # r = trs # r. -Proof. - intros; unfold find_assocmap, AssocMapExt.get_default; rewrite H; auto. -Qed. -#[local] Hint Resolve find_assoc_get : mgen. - -Lemma find_assoc_get2 : - forall rs p r v trs, - (forall r, r < p -> rs ! r = trs ! r) -> - r < p -> - rs # r = v -> - trs # r = v. -Proof. - intros; unfold find_assocmap, AssocMapExt.get_default; rewrite <- H; auto. -Qed. -#[local] Hint Resolve find_assoc_get2 : mgen. - -Lemma get_assoc_gt : - forall A (rs : AssocMap.t A) p r v trs, - (forall r, r < p -> rs ! r = trs ! r) -> - r < p -> - rs ! r = v -> - trs ! r = v. -Proof. intros. rewrite <- H; auto. Qed. -#[local] Hint Resolve get_assoc_gt : mgen. - -Lemma expr_runp_matches : - forall f rs ar e v, - expr_runp f rs ar e v -> - forall trs tar, - match_assocmaps (max_reg_expr e + 1) rs trs -> - match_arrs ar tar -> - expr_runp f trs tar e v. -Proof. - induction 1. - - intros. econstructor. - - intros. econstructor. inv H0. symmetry. - apply find_assoc_get. - apply H2. crush. - - intros. econstructor. apply IHexpr_runp; eauto. - inv H1. constructor. simplify. - assert (forall a b c, a < b + 1 -> a < Pos.max c b + 1) by lia. - eapply H4 in H1. eapply H3 in H1. auto. - inv H2. - unfold arr_assocmap_lookup in *. - destruct (stack ! r) eqn:?; [|discriminate]. - inv H1. - inv H0. - eapply H3 in Heqo. inv Heqo. inv H0. - unfold arr in *. rewrite H1. inv H5. - rewrite H0. auto. - - intros. econstructor; eauto. eapply IHexpr_runp1; eauto. - econstructor. inv H2. intros. - assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia. - simplify. - eapply H5 in H2. apply H4 in H2. auto. - apply IHexpr_runp2; eauto. - econstructor. inv H2. intros. - assert (forall a b c, a < b + 1 -> a < Pos.max c b + 1) by lia. - simplify. eapply H5 in H2. apply H4 in H2. auto. - - intros. econstructor; eauto. - - intros. econstructor; eauto. apply IHexpr_runp1; eauto. - constructor. inv H2. intros. simplify. - assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia. - eapply H5 in H2. apply H4 in H2. auto. - apply IHexpr_runp2; eauto. simplify. - assert (forall a b c d, a < b + 1 -> a < Pos.max c (Pos.max b d) + 1) by lia. - constructor. intros. eapply H4 in H5. inv H2. apply H6 in H5. auto. - - intros. eapply erun_Vternary_false. apply IHexpr_runp1; eauto. constructor. inv H2. - intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia. - eapply H5 in H2. apply H4 in H2. auto. - apply IHexpr_runp2; eauto. econstructor. inv H2. simplify. - assert (forall a b c d, a < b + 1 -> a < Pos.max c (Pos.max d b) + 1) by lia. - eapply H5 in H2. apply H4 in H2. auto. auto. -Qed. -#[local] Hint Resolve expr_runp_matches : mgen. - -Lemma expr_runp_matches2 : - forall f rs ar e v p, - expr_runp f rs ar e v -> - max_reg_expr e < p -> - forall trs tar, - match_assocmaps p rs trs -> - match_arrs ar tar -> - expr_runp f trs tar e v. -Proof. - intros. eapply expr_runp_matches; eauto. - assert (max_reg_expr e + 1 <= p) by lia. - mgen_crush. -Qed. -#[local] Hint Resolve expr_runp_matches2 : mgen. - -Lemma match_assocmaps_gss : - forall p rab rab' r rhsval, - match_assocmaps p rab rab' -> - match_assocmaps p rab # r <- rhsval rab' # r <- rhsval. -Proof. - intros. inv H. econstructor. - intros. - unfold find_assocmap. unfold AssocMapExt.get_default. - destruct (Pos.eq_dec r r0); subst. - repeat rewrite PTree.gss; auto. - repeat rewrite PTree.gso; auto. -Qed. -#[local] Hint Resolve match_assocmaps_gss : mgen. - -Lemma match_assocmaps_gt : - forall p s ra ra' v, - p <= s -> - match_assocmaps p ra ra' -> - match_assocmaps p ra (ra' # s <- v). -Proof. - intros. inv H0. constructor. - intros. rewrite AssocMap.gso; try lia. apply H1; auto. -Qed. -#[local] Hint Resolve match_assocmaps_gt : mgen. - -Lemma match_reg_assocs_block : - forall p rab rab' r rhsval, - match_reg_assocs p rab rab' -> - match_reg_assocs p (block_reg r rab rhsval) (block_reg r rab' rhsval). -Proof. inversion 1; econstructor; eauto with mgen. Qed. -#[local] Hint Resolve match_reg_assocs_block : mgen. - -Lemma match_reg_assocs_nonblock : - forall p rab rab' r rhsval, - match_reg_assocs p rab rab' -> - match_reg_assocs p (nonblock_reg r rab rhsval) (nonblock_reg r rab' rhsval). -Proof. inversion 1; econstructor; eauto with mgen. Qed. -#[local] Hint Resolve match_reg_assocs_nonblock : mgen. - -Lemma some_inj : - forall A (x: A) y, - Some x = Some y -> - x = y. -Proof. inversion 1; auto. Qed. - -Lemma arrs_present : - forall r i v ar arr, - (arr_assocmap_set r i v ar) ! r = Some arr -> - exists b, ar ! r = Some b. -Proof. - intros. unfold arr_assocmap_set in *. - destruct ar!r eqn:?. - rewrite AssocMap.gss in H. - inv H. eexists. auto. rewrite Heqo in H. discriminate. -Qed. - -Ltac inv_exists := - match goal with - | H: exists _, _ |- _ => inv H - end. - -Lemma array_get_error_bound_gt : - forall A i (a : Array A), - (i >= arr_length a)%nat -> - array_get_error i a = None. -Proof. - intros. unfold array_get_error. - apply nth_error_None. destruct a. simplify. - lia. -Qed. -#[local] Hint Resolve array_get_error_bound_gt : mgen. - -Lemma array_get_error_each : - forall A addr i (v : A) a x, - arr_length a = arr_length x -> - array_get_error addr a = array_get_error addr x -> - array_get_error addr (array_set i v a) = array_get_error addr (array_set i v x). -Proof. - intros. - destruct (Nat.eq_dec addr i); subst. - destruct (lt_dec i (arr_length a)). - repeat rewrite array_get_error_set_bound; auto. - rewrite <- H. auto. - apply Nat.nlt_ge in n. - repeat rewrite array_get_error_bound_gt; auto. - rewrite <- array_set_len. rewrite <- H. lia. - repeat rewrite array_gso; auto. -Qed. -#[local] Hint Resolve array_get_error_each : mgen. - -Lemma match_arrs_gss : - forall ar ar' r v i, - match_arrs ar ar' -> - match_arrs (arr_assocmap_set r i v ar) (arr_assocmap_set r i v ar'). -Proof. - Ltac mag_tac := - match goal with - | H: ?ar ! _ = Some _, H2: forall s arr, ?ar ! s = Some arr -> _ |- _ => - let H3 := fresh "H" in - learn H as H3; apply H2 in H3; inv_exists; simplify - | H: ?ar ! _ = None, H2: forall s, ?ar ! s = None -> _ |- _ => - let H3 := fresh "H" in - learn H as H3; apply H2 in H3; inv_exists; simplify - | H: ?ar ! _ = _ |- context[match ?ar ! _ with _ => _ end] => - unfold Verilog.arr in *; rewrite H - | H: ?ar ! _ = _, H2: context[match ?ar ! _ with _ => _ end] |- _ => - unfold Verilog.arr in *; rewrite H in H2 - | H: context[(_ # ?s <- _) ! ?s] |- _ => rewrite AssocMap.gss in H - | H: context[(_ # ?r <- _) ! ?s], H2: ?r <> ?s |- _ => rewrite AssocMap.gso in H; auto - | |- context[(_ # ?s <- _) ! ?s] => rewrite AssocMap.gss - | H: ?r <> ?s |- context[(_ # ?r <- _) ! ?s] => rewrite AssocMap.gso; auto - end. - intros. - inv H. econstructor; simplify. - destruct (Pos.eq_dec r s); subst. - - unfold arr_assocmap_set, Verilog.arr in *. - destruct ar!s eqn:?. - mag_tac. - econstructor; simplify. - repeat mag_tac; auto. - intros. repeat mag_tac. simplify. - apply array_get_error_each; auto. - repeat mag_tac; crush. - repeat mag_tac; crush. - - unfold arr_assocmap_set in *. - destruct ar ! r eqn:?. rewrite AssocMap.gso in H; auto. - apply H0 in Heqo. apply H0 in H. repeat inv_exists. simplify. - econstructor. unfold Verilog.arr in *. rewrite H3. simplify. - rewrite AssocMap.gso; auto. eauto. intros. auto. auto. - apply H1 in Heqo. apply H0 in H. repeat inv_exists; simplify. - econstructor. unfold Verilog.arr in *. rewrite Heqo. simplify; eauto. - - destruct (Pos.eq_dec r s); unfold arr_assocmap_set, Verilog.arr in *; simplify; subst. - destruct ar!s eqn:?; repeat mag_tac; crush. - apply H1 in H. mag_tac; crush. - destruct ar!r eqn:?; repeat mag_tac; crush. - apply H1 in Heqo. repeat mag_tac; auto. -Qed. -#[local] Hint Resolve match_arrs_gss : mgen. - -Lemma match_arr_assocs_block : - forall rab rab' r i rhsval, - match_arr_assocs rab rab' -> - match_arr_assocs (block_arr r i rab rhsval) (block_arr r i rab' rhsval). -Proof. inversion 1; econstructor; eauto with mgen. Qed. -#[local] Hint Resolve match_arr_assocs_block : mgen. - -Lemma match_arr_assocs_nonblock : - forall rab rab' r i rhsval, - match_arr_assocs rab rab' -> - match_arr_assocs (nonblock_arr r i rab rhsval) (nonblock_arr r i rab' rhsval). -Proof. inversion 1; econstructor; eauto with mgen. Qed. -#[local] Hint Resolve match_arr_assocs_nonblock : mgen. - -Lemma match_states_same : - forall f rs1 ar1 c rs2 ar2 p, - stmnt_runp f rs1 ar1 c rs2 ar2 -> - max_reg_stmnt c < p -> - forall trs1 tar1, - match_reg_assocs p rs1 trs1 -> - match_arr_assocs ar1 tar1 -> - exists trs2 tar2, - stmnt_runp f trs1 tar1 c trs2 tar2 - /\ match_reg_assocs p rs2 trs2 - /\ match_arr_assocs ar2 tar2. -Proof. - Ltac match_states_same_facts := - match goal with - | H: match_reg_assocs _ _ _ |- _ => - let H2 := fresh "H" in - learn H as H2; inv H2 - | H: match_arr_assocs _ _ |- _ => - let H2 := fresh "H" in - learn H as H2; inv H2 - | H1: context[exists _, _], H2: context[exists _, _] |- _ => - learn H1; learn H2; - exploit H1; mgen_crush; exploit H2; mgen_crush - | H1: context[exists _, _] |- _ => - learn H1; exploit H1; mgen_crush - end. - Ltac match_states_same_tac := - match goal with - | |- exists _, _ => econstructor - | |- _ < _ => lia - | H: context[_ <> _] |- stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ => - eapply stmnt_runp_Vcase_nomatch - | |- stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ => - eapply stmnt_runp_Vcase_match - | H: valueToBool _ = false |- stmnt_runp _ _ _ _ _ _ => - eapply stmnt_runp_Vcond_false - | |- stmnt_runp _ _ _ _ _ _ => econstructor - | |- expr_runp _ _ _ _ _ => eapply expr_runp_matches2 - end; mgen_crush; try lia. - induction 1; simplify; repeat match_states_same_facts; - try destruct_match; try solve [repeat match_states_same_tac]. - - inv H. exists (block_reg r {| assoc_blocking := rab'; assoc_nonblocking := ran' |} rhsval); - repeat match_states_same_tac; econstructor. - - exists (nonblock_reg r {| assoc_blocking := rab'; assoc_nonblocking := ran' |} rhsval); - repeat match_states_same_tac; inv H; econstructor. - - econstructor. exists (block_arr r i {| assoc_blocking := rab'0; assoc_nonblocking := ran'0 |} rhsval). - simplify; repeat match_states_same_tac. inv H. econstructor. - repeat match_states_same_tac. eauto. mgen_crush. - - econstructor. exists (nonblock_arr r i {| assoc_blocking := rab'0; assoc_nonblocking := ran'0 |} rhsval). - simplify; repeat match_states_same_tac. inv H. econstructor. - repeat match_states_same_tac. eauto. mgen_crush. -Qed. - -Lemma match_reg_assocs_merge : - forall p rs rs', - match_reg_assocs p rs rs' -> - match_reg_assocs p (merge_reg_assocs rs) (merge_reg_assocs rs'). -Proof. - inversion 1. - econstructor; econstructor; crush. inv H3. inv H. - inv H7. inv H9. - unfold merge_regs. - destruct (ran!r) eqn:?; destruct (rab!r) eqn:?. - erewrite AssocMapExt.merge_correct_1; eauto. - erewrite AssocMapExt.merge_correct_1; eauto. - rewrite <- H2; eauto. - erewrite AssocMapExt.merge_correct_1; eauto. - erewrite AssocMapExt.merge_correct_1; eauto. - rewrite <- H2; eauto. - erewrite AssocMapExt.merge_correct_2; eauto. - erewrite AssocMapExt.merge_correct_2; eauto. - rewrite <- H2; eauto. - rewrite <- H; eauto. - erewrite AssocMapExt.merge_correct_3; eauto. - erewrite AssocMapExt.merge_correct_3; eauto. - rewrite <- H2; eauto. - rewrite <- H; eauto. -Qed. -#[local] Hint Resolve match_reg_assocs_merge : mgen. - -Lemma transf_not_changed : - forall state ram n d c i d_s c_s, - (forall e1 e2 r, d_s <> Vnonblock (Vvari r e1) e2) -> - (forall e1 e2 r, d_s <> Vnonblock e1 (Vvari r e2)) -> - d!i = Some d_s -> - c!i = Some c_s -> - transf_maps state ram (i, n) (d, c) = (d, c). -Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Qed. - -Lemma transf_not_changed_neq : - forall state ram n d c d' c' i a d_s c_s, - transf_maps state ram (a, n) (d, c) = (d', c') -> - d!i = Some d_s -> - c!i = Some c_s -> - a <> i -> n <> i -> - d'!i = Some d_s /\ c'!i = Some c_s. -Proof. - unfold transf_maps; intros; repeat destruct_match; mgen_crush; - match goal with [ H: (_, _) = (_, _) |- _ ] => inv H end; - repeat (rewrite AssocMap.gso; auto). -Qed. - -Lemma forall_gt : - forall l, Forall (Pos.ge (fold_right Pos.max 1 l)) l. -Proof. - induction l; auto. - constructor. inv IHl; simplify; lia. - simplify. destruct (Pos.max_dec a (fold_right Pos.max 1 l)). - rewrite e. apply Pos.max_l_iff in e. apply Pos.le_ge in e. - apply Forall_forall. rewrite Forall_forall in IHl. - intros. - assert (X: forall a b c, a >= c -> c >= b -> a >= b) by lia. - apply X with (b := x) in e; auto. - rewrite e; auto. -Qed. - -Lemma max_index_list : - forall A (l : list (positive * A)) i d_s, - In (i, d_s) l -> - list_norepet (map fst l) -> - i <= fold_right Pos.max 1 (map fst l). -Proof. - induction l; crush. - inv H. inv H0. simplify. lia. - inv H0. - let H := fresh "H" in - assert (H: forall a b c, c <= b -> c <= Pos.max a b) by lia; - apply H; eapply IHl; eauto. -Qed. - -Lemma max_index : - forall A d i (d_s: A), d ! i = Some d_s -> i <= max_pc d. -Proof. - unfold max_pc; - eauto using max_index_list, - PTree.elements_correct, PTree.elements_keys_norepet. -Qed. - -Lemma max_index_2' : - forall l i, i > fold_right Pos.max 1 l -> Forall (Pos.gt i) l. -Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed. - -Lemma max_index_2'' : - forall l i, Forall (Pos.gt i) l -> ~ In i l. -Proof. - induction l; crush. unfold not in *. - intros. inv H0. inv H. lia. eapply IHl. - inv H. apply H4. auto. -Qed. - -Lemma elements_correct_none : - forall A am k, - ~ List.In k (List.map (@fst _ A) (AssocMap.elements am)) -> - AssocMap.get k am = None. -Proof. - intros. apply AssocMapExt.elements_correct' in H. unfold not in *. - destruct am ! k eqn:?; auto. exfalso. apply H. eexists. auto. -Qed. -#[local] Hint Resolve elements_correct_none : assocmap. - -Lemma max_index_2 : - forall A (d: AssocMap.t A) i, i > max_pc d -> d ! i = None. -Proof. - intros. unfold max_pc in *. apply max_index_2' in H. - apply max_index_2'' in H. apply elements_correct_none. auto. -Qed. - -Definition match_prog (p: program) (tp: program) := - Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp. - -Lemma transf_program_match: - forall p, match_prog p (transf_program p). -Proof. - intros. unfold transf_program, match_prog. - apply Linking.match_transform_program. -Qed. - -Lemma exec_all_Vskip : - forall rs ar, - exec_all Vskip Vskip rs ar rs ar. -Proof. - unfold exec_all. - intros. repeat econstructor. - Unshelve. unfold fext. exact tt. -Qed. - -Lemma match_assocmaps_trans: - forall p rs1 rs2 rs3, - match_assocmaps p rs1 rs2 -> - match_assocmaps p rs2 rs3 -> - match_assocmaps p rs1 rs3. -Proof. - intros. inv H. inv H0. econstructor; eauto. - intros. rewrite H1 by auto. auto. -Qed. - -Lemma match_reg_assocs_trans: - forall p rs1 rs2 rs3, - match_reg_assocs p rs1 rs2 -> - match_reg_assocs p rs2 rs3 -> - match_reg_assocs p rs1 rs3. -Proof. - intros. inv H. inv H0. - econstructor; eapply match_assocmaps_trans; eauto. -Qed. - -Lemma empty_arrs_match : - forall m, - match_arrs (empty_stack m) (empty_stack (transf_module m)). -Proof. - intros; - unfold empty_stack, transf_module; repeat destruct_match; mgen_crush. -Qed. -#[local] Hint Resolve empty_arrs_match : mgen. - -Lemma max_module_stmnts : - forall m, - Pos.max (max_stmnt_tree (mod_controllogic m)) - (max_stmnt_tree (mod_datapath m)) < max_reg_module m + 1. -Proof. intros. unfold max_reg_module. lia. Qed. -#[local] Hint Resolve max_module_stmnts : mgen. - -Lemma transf_module_code : - forall m, - mod_ram m = None -> - transf_code (mod_st m) - {| ram_size := mod_stk_len m; - ram_mem := mod_stk m; - ram_en := max_reg_module m + 2; - ram_addr := max_reg_module m + 1; - ram_wr_en := max_reg_module m + 5; - ram_d_in := max_reg_module m + 3; - ram_d_out := max_reg_module m + 4; - ram_u_en := max_reg_module m + 6; - ram_ordering := ram_wf (max_reg_module m) |} - (mod_datapath m) (mod_controllogic m) - = ((mod_datapath (transf_module m)), mod_controllogic (transf_module m)). -Proof. unfold transf_module; intros; repeat destruct_match; crush. - apply surjective_pairing. Qed. -#[local] Hint Resolve transf_module_code : mgen. - -Lemma transf_module_code_ram : - forall m r, mod_ram m = Some r -> transf_module m = m. -Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed. -#[local] Hint Resolve transf_module_code_ram : mgen. - -Lemma mod_reset_lt : forall m, mod_reset m < max_reg_module m + 1. -Proof. intros; unfold max_reg_module; lia. Qed. -#[local] Hint Resolve mod_reset_lt : mgen. - -Lemma mod_finish_lt : forall m, mod_finish m < max_reg_module m + 1. -Proof. intros; unfold max_reg_module; lia. Qed. -#[local] Hint Resolve mod_finish_lt : mgen. - -Lemma mod_return_lt : forall m, mod_return m < max_reg_module m + 1. -Proof. intros; unfold max_reg_module; lia. Qed. -#[local] Hint Resolve mod_return_lt : mgen. - -Lemma mod_start_lt : forall m, mod_start m < max_reg_module m + 1. -Proof. intros; unfold max_reg_module; lia. Qed. -#[local] Hint Resolve mod_start_lt : mgen. - -Lemma mod_stk_lt : forall m, mod_stk m < max_reg_module m + 1. -Proof. intros; unfold max_reg_module; lia. Qed. -#[local] Hint Resolve mod_stk_lt : mgen. - -Lemma mod_st_lt : forall m, mod_st m < max_reg_module m + 1. -Proof. intros; unfold max_reg_module; lia. Qed. -#[local] Hint Resolve mod_st_lt : mgen. - -Lemma mod_reset_modify : - forall m ar ar' v, - match_assocmaps (max_reg_module m + 1) ar ar' -> - ar ! (mod_reset m) = Some v -> - ar' ! (mod_reset (transf_module m)) = Some v. -Proof. - inversion 1. intros. - unfold transf_module; repeat destruct_match; simplify; - rewrite <- H0; eauto with mgen. -Qed. -#[local] Hint Resolve mod_reset_modify : mgen. - -Lemma mod_finish_modify : - forall m ar ar' v, - match_assocmaps (max_reg_module m + 1) ar ar' -> - ar ! (mod_finish m) = Some v -> - ar' ! (mod_finish (transf_module m)) = Some v. -Proof. - inversion 1. intros. - unfold transf_module; repeat destruct_match; simplify; - rewrite <- H0; eauto with mgen. -Qed. -#[local] Hint Resolve mod_finish_modify : mgen. - -Lemma mod_return_modify : - forall m ar ar' v, - match_assocmaps (max_reg_module m + 1) ar ar' -> - ar ! (mod_return m) = Some v -> - ar' ! (mod_return (transf_module m)) = Some v. -Proof. - inversion 1. intros. - unfold transf_module; repeat destruct_match; simplify; - rewrite <- H0; eauto with mgen. -Qed. -#[local] Hint Resolve mod_return_modify : mgen. - -Lemma mod_start_modify : - forall m ar ar' v, - match_assocmaps (max_reg_module m + 1) ar ar' -> - ar ! (mod_start m) = Some v -> - ar' ! (mod_start (transf_module m)) = Some v. -Proof. - inversion 1. intros. - unfold transf_module; repeat destruct_match; simplify; - rewrite <- H0; eauto with mgen. -Qed. -#[local] Hint Resolve mod_start_modify : mgen. - -Lemma mod_st_modify : - forall m ar ar' v, - match_assocmaps (max_reg_module m + 1) ar ar' -> - ar ! (mod_st m) = Some v -> - ar' ! (mod_st (transf_module m)) = Some v. -Proof. - inversion 1. intros. - unfold transf_module; repeat destruct_match; simplify; - rewrite <- H0; eauto with mgen. -Qed. -#[local] Hint Resolve mod_st_modify : mgen. - -Lemma match_arrs_read : - forall ra ra' addr v mem, - arr_assocmap_lookup ra mem addr = Some v -> - match_arrs ra ra' -> - arr_assocmap_lookup ra' mem addr = Some v. -Proof. - unfold arr_assocmap_lookup. intros. destruct_match; destruct_match; try discriminate. - inv H0. eapply H1 in Heqo0. inv Heqo0. simplify. unfold arr in *. - rewrite H in Heqo. inv Heqo. - rewrite H0. auto. - inv H0. eapply H1 in Heqo0. inv Heqo0. inv H0. unfold arr in *. - rewrite H3 in Heqo. discriminate. -Qed. -#[local] Hint Resolve match_arrs_read : mgen. - -Lemma match_reg_implies_equal : - forall ra ra' p a b c, - Int.eq (ra # a) (ra # b) = c -> - a < p -> b < p -> - match_assocmaps p ra ra' -> - Int.eq (ra' # a) (ra' # b) = c. -Proof. - unfold find_assocmap, AssocMapExt.get_default; intros. - inv H2. destruct (ra ! a) eqn:?; destruct (ra ! b) eqn:?; - repeat rewrite <- H3 by lia; rewrite Heqo; rewrite Heqo0; auto. -Qed. -#[local] Hint Resolve match_reg_implies_equal : mgen. - -Lemma exec_ram_same : - forall rs1 ar1 ram rs2 ar2 p, - exec_ram rs1 ar1 (Some ram) rs2 ar2 -> - forall_ram (fun x => x < p) ram -> - forall trs1 tar1, - match_reg_assocs p rs1 trs1 -> - match_arr_assocs ar1 tar1 -> - exists trs2 tar2, - exec_ram trs1 tar1 (Some ram) trs2 tar2 - /\ match_reg_assocs p rs2 trs2 - /\ match_arr_assocs ar2 tar2. -Proof. - Ltac exec_ram_same_facts := - match goal with - | H: match_reg_assocs _ _ _ |- _ => let H2 := fresh "H" in learn H as H2; inv H2 - | H: match_assocmaps _ _ _ |- _ => let H2 := fresh "H" in learn H as H2; inv H2 - | H: match_arr_assocs _ _ |- _ => let H2 := fresh "H" in learn H as H2; inv H2 - | H: match_arrs _ _ |- _ => let H2 := fresh "H" in learn H as H2; inv H2 - end. - inversion 1; subst; destruct ram; unfold forall_ram; simplify; repeat exec_ram_same_facts. - - repeat (econstructor; mgen_crush). - - do 2 econstructor; simplify; - [eapply exec_ram_Some_write; [ apply H1 | apply H2 | | | | | ] | | ]; - mgen_crush. - - do 2 econstructor; simplify; [eapply exec_ram_Some_read | | ]; - repeat (try econstructor; mgen_crush). -Qed. - -Lemma match_assocmaps_merge : - forall p nasr basr nasr' basr', - match_assocmaps p nasr nasr' -> - match_assocmaps p basr basr' -> - match_assocmaps p (merge_regs nasr basr) (merge_regs nasr' basr'). -Proof. - unfold merge_regs. - intros. inv H. inv H0. econstructor. - intros. - destruct nasr ! r eqn:?; destruct basr ! r eqn:?. - erewrite AssocMapExt.merge_correct_1; mgen_crush. - erewrite AssocMapExt.merge_correct_1; mgen_crush. - erewrite AssocMapExt.merge_correct_1; mgen_crush. - erewrite AssocMapExt.merge_correct_1; mgen_crush. - erewrite AssocMapExt.merge_correct_2; mgen_crush. - erewrite AssocMapExt.merge_correct_2; mgen_crush. - erewrite AssocMapExt.merge_correct_3; mgen_crush. - erewrite AssocMapExt.merge_correct_3; mgen_crush. -Qed. -#[local] Hint Resolve match_assocmaps_merge : mgen. - -Lemma list_combine_nth_error1 : - forall l l' addr v, - length l = length l' -> - nth_error l addr = Some (Some v) -> - nth_error (list_combine merge_cell l l') addr = Some (Some v). -Proof. induction l; destruct l'; destruct addr; crush. Qed. - -Lemma list_combine_nth_error2 : - forall l' l addr v, - length l = length l' -> - nth_error l addr = Some None -> - nth_error l' addr = Some (Some v) -> - nth_error (list_combine merge_cell l l') addr = Some (Some v). -Proof. induction l'; try rewrite nth_error_nil in *; destruct l; destruct addr; crush. Qed. - -Lemma list_combine_nth_error3 : - forall l l' addr, - length l = length l' -> - nth_error l addr = Some None -> - nth_error l' addr = Some None -> - nth_error (list_combine merge_cell l l') addr = Some None. -Proof. induction l; destruct l'; destruct addr; crush. Qed. - -Lemma list_combine_nth_error4 : - forall l l' addr, - length l = length l' -> - nth_error l addr = None -> - nth_error (list_combine merge_cell l l') addr = None. -Proof. induction l; destruct l'; destruct addr; crush. Qed. - -Lemma list_combine_nth_error5 : - forall l l' addr, - length l = length l' -> - nth_error l' addr = None -> - nth_error (list_combine merge_cell l l') addr = None. -Proof. induction l; destruct l'; destruct addr; crush. Qed. - -Lemma array_get_error_merge1 : - forall a a0 addr v, - arr_length a = arr_length a0 -> - array_get_error addr a = Some (Some v) -> - array_get_error addr (combine merge_cell a a0) = Some (Some v). -Proof. - unfold array_get_error, combine in *; intros; - apply list_combine_nth_error1; destruct a; destruct a0; crush. -Qed. - -Lemma array_get_error_merge2 : - forall a a0 addr v, - arr_length a = arr_length a0 -> - array_get_error addr a0 = Some (Some v) -> - array_get_error addr a = Some None -> - array_get_error addr (combine merge_cell a a0) = Some (Some v). -Proof. - unfold array_get_error, combine in *; intros; - apply list_combine_nth_error2; destruct a; destruct a0; crush. -Qed. - -Lemma array_get_error_merge3 : - forall a a0 addr, - arr_length a = arr_length a0 -> - array_get_error addr a0 = Some None -> - array_get_error addr a = Some None -> - array_get_error addr (combine merge_cell a a0) = Some None. -Proof. - unfold array_get_error, combine in *; intros; - apply list_combine_nth_error3; destruct a; destruct a0; crush. -Qed. - -Lemma array_get_error_merge4 : - forall a a0 addr, - arr_length a = arr_length a0 -> - array_get_error addr a = None -> - array_get_error addr (combine merge_cell a a0) = None. -Proof. - unfold array_get_error, combine in *; intros; - apply list_combine_nth_error4; destruct a; destruct a0; crush. -Qed. - -Lemma array_get_error_merge5 : - forall a a0 addr, - arr_length a = arr_length a0 -> - array_get_error addr a0 = None -> - array_get_error addr (combine merge_cell a a0) = None. -Proof. - unfold array_get_error, combine in *; intros; - apply list_combine_nth_error5; destruct a; destruct a0; crush. -Qed. - -Lemma match_arrs_merge' : - forall addr nasa basa arr s x x0 a a0 nasa' basa', - (AssocMap.combine merge_arr nasa basa) ! s = Some arr -> - nasa ! s = Some a -> - basa ! s = Some a0 -> - nasa' ! s = Some x0 -> - basa' ! s = Some x -> - arr_length x = arr_length x0 -> - array_get_error addr a0 = array_get_error addr x -> - arr_length a0 = arr_length x -> - array_get_error addr a = array_get_error addr x0 -> - arr_length a = arr_length x0 -> - array_get_error addr arr = array_get_error addr (combine merge_cell x0 x). -Proof. - intros. rewrite AssocMap.gcombine in H by auto. - unfold merge_arr in H. - rewrite H0 in H. rewrite H1 in H. inv H. - destruct (array_get_error addr a0) eqn:?; destruct (array_get_error addr a) eqn:?. - destruct o; destruct o0. - erewrite array_get_error_merge1; eauto. erewrite array_get_error_merge1; eauto. - rewrite <- H6 in H4. rewrite <- H8 in H4. auto. - erewrite array_get_error_merge2; eauto. erewrite array_get_error_merge2; eauto. - rewrite <- H6 in H4. rewrite <- H8 in H4. auto. - erewrite array_get_error_merge1; eauto. erewrite array_get_error_merge1; eauto. - rewrite <- H6 in H4. rewrite <- H8 in H4. auto. - erewrite array_get_error_merge3; eauto. erewrite array_get_error_merge3; eauto. - rewrite <- H6 in H4. rewrite <- H8 in H4. auto. - erewrite array_get_error_merge4; eauto. erewrite array_get_error_merge4; eauto. - rewrite <- H6 in H4. rewrite <- H8 in H4. auto. - erewrite array_get_error_merge5; eauto. erewrite array_get_error_merge5; eauto. - rewrite <- H6 in H4. rewrite <- H8 in H4. auto. - erewrite array_get_error_merge5; eauto. erewrite array_get_error_merge5; eauto. - rewrite <- H6 in H4. rewrite <- H8 in H4. auto. -Qed. - -Lemma match_arrs_merge : - forall nasa nasa' basa basa', - match_arrs_size nasa basa -> - match_arrs nasa nasa' -> - match_arrs basa basa' -> - match_arrs (merge_arrs nasa basa) (merge_arrs nasa' basa'). -Proof. - unfold merge_arrs. - intros. inv H. inv H0. inv H1. econstructor. - - intros. destruct nasa ! s eqn:?; destruct basa ! s eqn:?; unfold Verilog.arr in *. - + pose proof Heqo. apply H in Heqo. pose proof Heqo0. apply H0 in Heqo0. - repeat inv_exists. simplify. - eexists. simplify. rewrite AssocMap.gcombine; eauto. - unfold merge_arr. unfold Verilog.arr in *. rewrite H11. rewrite H12. auto. - intros. eapply match_arrs_merge'; eauto. eapply H2 in H7; eauto. - inv_exists. simplify. congruence. - rewrite AssocMap.gcombine in H1; auto. unfold merge_arr in H1. - rewrite H7 in H1. rewrite H8 in H1. inv H1. - repeat rewrite combine_length; auto. - eapply H2 in H7; eauto. inv_exists; simplify; congruence. - eapply H2 in H7; eauto. inv_exists; simplify; congruence. - + apply H2 in Heqo; inv_exists; crush. - + apply H3 in Heqo0; inv_exists; crush. - + rewrite AssocMap.gcombine in H1 by auto. unfold merge_arr in *. - rewrite Heqo in H1. rewrite Heqo0 in H1. discriminate. - - intros. rewrite AssocMap.gcombine in H1 by auto. unfold merge_arr in H1. - repeat destruct_match; crush. - rewrite AssocMap.gcombine by auto; unfold merge_arr. - apply H5 in Heqo. apply H6 in Heqo0. - unfold Verilog.arr in *. - rewrite Heqo. rewrite Heqo0. auto. -Qed. -#[local] Hint Resolve match_arrs_merge : mgen. - -Lemma match_empty_size_merge : - forall nasa2 basa2 m, - match_empty_size m nasa2 -> - match_empty_size m basa2 -> - match_empty_size m (merge_arrs nasa2 basa2). -Proof. - intros. inv H. inv H0. constructor. - simplify. unfold merge_arrs. rewrite AssocMap.gcombine by auto. - pose proof H0 as H6. apply H1 in H6. inv_exists; simplify. - pose proof H0 as H9. apply H in H9. inv_exists; simplify. - eexists. simplify. unfold merge_arr. unfold Verilog.arr in *. rewrite H6. - rewrite H9. auto. rewrite H8. symmetry. apply combine_length. congruence. - intros. - destruct (nasa2 ! s) eqn:?; destruct (basa2 ! s) eqn:?. - unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. - unfold merge_arr in *. setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0. inv H0. - apply H2 in Heqo. apply H4 in Heqo0. repeat inv_exists; simplify. - eexists. simplify. eauto. rewrite list_combine_length. - rewrite (arr_wf a). rewrite (arr_wf a0). lia. - unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. - unfold merge_arr in *. setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0. - apply H2 in Heqo. inv_exists; simplify. - econstructor; eauto. - unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. - unfold merge_arr in *. setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0. - inv H0. apply H4 in Heqo0. inv_exists; simplify. econstructor; eauto. - unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. - unfold merge_arr in *. setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0. - discriminate. - split; intros. - unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. - unfold merge_arr in *. repeat destruct_match; crush. apply H5 in Heqo0; auto. - pose proof H0. - apply H5 in H0. - apply H3 in H6. unfold merge_arrs. rewrite AssocMap.gcombine by auto. - setoid_rewrite H0. setoid_rewrite H6. auto. -Qed. -#[local] Hint Resolve match_empty_size_merge : mgen. - -Lemma match_empty_size_match : - forall m nasa2 basa2, - match_empty_size m nasa2 -> - match_empty_size m basa2 -> - match_arrs_size nasa2 basa2. -Proof. - Ltac match_empty_size_match_solve := - match goal with - | H: context[forall s arr, ?ar ! s = Some arr -> _], H2: ?ar ! _ = Some _ |- _ => - let H3 := fresh "H" in - learn H; pose proof H2 as H3; apply H in H3; repeat inv_exists - | H: context[forall s, ?ar ! s = None <-> _], H2: ?ar ! _ = None |- _ => - let H3 := fresh "H" in - learn H; pose proof H2 as H3; apply H in H3 - | H: context[forall s, _ <-> ?ar ! s = None], H2: ?ar ! _ = None |- _ => - let H3 := fresh "H" in - learn H; pose proof H2 as H3; apply H in H3 - | |- exists _, _ => econstructor - | |- _ ! _ = Some _ => eassumption - | |- _ = _ => congruence - | |- _ <-> _ => split - end; simplify. - inversion 1; inversion 1; constructor; simplify; repeat match_empty_size_match_solve. -Qed. -#[local] Hint Resolve match_empty_size_match : mgen. - -Lemma match_get_merge : - forall p ran ran' rab rab' s v, - s < p -> - match_assocmaps p ran ran' -> - match_assocmaps p rab rab' -> - (merge_regs ran rab) ! s = Some v -> - (merge_regs ran' rab') ! s = Some v. -Proof. - intros. - assert (X: match_assocmaps p (merge_regs ran rab) (merge_regs ran' rab')) by auto with mgen. - inv X. rewrite <- H3; auto. -Qed. -#[local] Hint Resolve match_get_merge : mgen. - -Ltac masrp_tac := - match goal with - | H: context[forall s arr, ?ar ! s = Some arr -> _], H2: ?ar ! _ = Some _ |- _ => - let H3 := fresh "H" in - learn H; pose proof H2 as H3; apply H in H3; repeat inv_exists - | H: context[forall s, ?ar ! s = None <-> _], H2: ?ar ! _ = None |- _ => - let H3 := fresh "H" in - learn H; pose proof H2 as H3; apply H in H3 - | H: context[forall s, _ <-> ?ar ! s = None], H2: ?ar ! _ = None |- _ => - let H3 := fresh "H" in - learn H; pose proof H2 as H3; apply H in H3 - | ra: arr_associations |- _ => - let ra1 := fresh "ran" in let ra2 := fresh "rab" in destruct ra as [ra1 ra2] - | |- _ ! _ = _ => solve [mgen_crush] - | |- _ = _ => congruence - | |- _ <> _ => lia - | H: ?ar ! ?s = _ |- context[match ?ar ! ?r with _ => _ end] => learn H; destruct (Pos.eq_dec s r); subst - | H: ?ar ! ?s = _ |- context[match ?ar ! ?s with _ => _ end] => setoid_rewrite H - | |- context[match ?ar ! ?s with _ => _ end] => destruct (ar ! s) eqn:? - | H: ?s <> ?r |- context[(_ # ?r <- _) ! ?s] => rewrite AssocMap.gso - | H: ?r <> ?s |- context[(_ # ?r <- _) ! ?s] => rewrite AssocMap.gso - | |- context[(_ # ?s <- _) ! ?s] => rewrite AssocMap.gss - | H: context[match ?ar ! ?r with _ => _ end ! ?s] |- _ => - destruct (ar ! r) eqn:?; destruct (Pos.eq_dec r s); subst - | H: ?ar ! ?s = _, H2: context[match ?ar ! ?s with _ => _ end] |- _ => - setoid_rewrite H in H2 - | H: context[match ?ar ! ?s with _ => _ end] |- _ => destruct (ar ! s) eqn:? - | H: ?s <> ?r, H2: context[(_ # ?r <- _) ! ?s] |- _ => rewrite AssocMap.gso in H2 - | H: ?r <> ?s, H2: context[(_ # ?r <- _) ! ?s] |- _ => rewrite AssocMap.gso in H2 - | H: context[(_ # ?s <- _) ! ?s] |- _ => rewrite AssocMap.gss in H - | |- context[match_empty_size] => constructor - | |- context[arr_assocmap_set] => unfold arr_assocmap_set - | H: context[arr_assocmap_set] |- _ => unfold arr_assocmap_set in H - | |- exists _, _ => econstructor - | |- _ <-> _ => split - end; simplify. - -Lemma match_empty_assocmap_set : - forall m r i rhsval asa, - match_empty_size m asa -> - match_empty_size m (arr_assocmap_set r i rhsval asa). -Proof. - inversion 1; subst; simplify. - constructor. intros. - repeat masrp_tac. - intros. do 5 masrp_tac; try solve [repeat masrp_tac]. - apply H1 in H3. inv_exists. simplify. - econstructor. simplify. apply H3. congruence. - repeat masrp_tac. destruct (Pos.eq_dec r s); subst. - rewrite AssocMap.gss in H8. discriminate. - rewrite AssocMap.gso in H8; auto. apply H2 in H8. auto. - destruct (Pos.eq_dec r s); subst. apply H1 in H5. inv_exists. simplify. - rewrite H5 in H8. discriminate. - rewrite AssocMap.gso; auto. - apply H2 in H5. auto. apply H2 in H5. auto. - Unshelve. auto. -Qed. -#[local] Hint Resolve match_empty_assocmap_set : mgen. - -Lemma match_arrs_size_stmnt_preserved : - forall m f rs1 ar1 ar2 c rs2, - stmnt_runp f rs1 ar1 c rs2 ar2 -> - match_empty_size m (assoc_nonblocking ar1) -> - match_empty_size m (assoc_blocking ar1) -> - match_empty_size m (assoc_nonblocking ar2) /\ match_empty_size m (assoc_blocking ar2). -Proof. - induction 1; inversion 1; inversion 1; eauto; simplify; try solve [repeat masrp_tac]. - subst. apply IHstmnt_runp2; apply IHstmnt_runp1; auto. - apply IHstmnt_runp2; apply IHstmnt_runp1; auto. - apply match_empty_assocmap_set. auto. - apply match_empty_assocmap_set. auto. -Qed. - -Lemma match_arrs_size_stmnt_preserved2 : - forall m f rs1 na ba na' ba' c rs2, - stmnt_runp f rs1 {| assoc_nonblocking := na; assoc_blocking := ba |} c rs2 - {| assoc_nonblocking := na'; assoc_blocking := ba' |} -> - match_empty_size m na -> - match_empty_size m ba -> - match_empty_size m na' /\ match_empty_size m ba'. -Proof. - intros. - remember ({| assoc_blocking := ba; assoc_nonblocking := na |}) as ar1. - remember ({| assoc_blocking := ba'; assoc_nonblocking := na' |}) as ar2. - assert (X1: na' = (assoc_nonblocking ar2)) by (rewrite Heqar2; auto). rewrite X1. - assert (X2: ba' = (assoc_blocking ar2)) by (rewrite Heqar2; auto). rewrite X2. - assert (X3: na = (assoc_nonblocking ar1)) by (rewrite Heqar1; auto). rewrite X3 in *. - assert (X4: ba = (assoc_blocking ar1)) by (rewrite Heqar1; auto). rewrite X4 in *. - eapply match_arrs_size_stmnt_preserved; mgen_crush. -Qed. -#[local] Hint Resolve match_arrs_size_stmnt_preserved2 : mgen. - -Lemma match_arrs_size_ram_preserved : - forall m rs1 ar1 ar2 ram rs2, - exec_ram rs1 ar1 ram rs2 ar2 -> - match_empty_size m (assoc_nonblocking ar1) -> - match_empty_size m (assoc_blocking ar1) -> - match_empty_size m (assoc_nonblocking ar2) - /\ match_empty_size m (assoc_blocking ar2). -Proof. - induction 1; inversion 1; inversion 1; subst; simplify; try solve [repeat masrp_tac]. - masrp_tac. masrp_tac. solve [repeat masrp_tac]. - masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. - masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. - masrp_tac. apply H8 in H1; inv_exists; simplify. repeat masrp_tac. auto. - repeat masrp_tac. - repeat masrp_tac. - repeat masrp_tac. - destruct (Pos.eq_dec (ram_mem r) s); subst; repeat masrp_tac. - destruct (Pos.eq_dec (ram_mem r) s); subst; repeat masrp_tac. - apply H9 in H17; auto. apply H9 in H17; auto. - Unshelve. eauto. -Qed. -#[local] Hint Resolve match_arrs_size_ram_preserved : mgen. - -Lemma match_arrs_size_ram_preserved2 : - forall m rs1 na na' ba ba' ram rs2, - exec_ram rs1 {| assoc_nonblocking := na; assoc_blocking := ba |} ram rs2 - {| assoc_nonblocking := na'; assoc_blocking := ba' |} -> - match_empty_size m na -> match_empty_size m ba -> - match_empty_size m na' /\ match_empty_size m ba'. -Proof. - intros. - remember ({| assoc_blocking := ba; assoc_nonblocking := na |}) as ar1. - remember ({| assoc_blocking := ba'; assoc_nonblocking := na' |}) as ar2. - assert (X1: na' = (assoc_nonblocking ar2)) by (rewrite Heqar2; auto). rewrite X1. - assert (X2: ba' = (assoc_blocking ar2)) by (rewrite Heqar2; auto). rewrite X2. - assert (X3: na = (assoc_nonblocking ar1)) by (rewrite Heqar1; auto). rewrite X3 in *. - assert (X4: ba = (assoc_blocking ar1)) by (rewrite Heqar1; auto). rewrite X4 in *. - eapply match_arrs_size_ram_preserved; mgen_crush. -Qed. -#[local] Hint Resolve match_arrs_size_ram_preserved2 : mgen. - -Lemma empty_stack_m : - forall m, empty_stack m = empty_stack' (mod_stk_len m) (mod_stk m). -Proof. unfold empty_stack, empty_stack'; mgen_crush. Qed. -#[local] Hint Rewrite empty_stack_m : mgen. - -Ltac clear_forall := - repeat match goal with - | H: context[forall _, _] |- _ => clear H - end. - -Lemma list_combine_none : - forall n l, - length l = n -> - list_combine Verilog.merge_cell (list_repeat None n) l = l. -Proof. - induction n; intros; crush. - - symmetry. apply length_zero_iff_nil. auto. - - destruct l; crush. - rewrite list_repeat_cons. - crush. f_equal. - eauto. -Qed. - -Lemma combine_none : - forall n a, - a.(arr_length) = n -> - arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. -Proof. - intros. - unfold combine. - crush. - - rewrite <- (arr_wf a) in H. - apply list_combine_none. - assumption. -Qed. - -Lemma combine_none2 : - forall n a addr, - arr_length a = n -> - array_get_error addr (combine Verilog.merge_cell (arr_repeat None n) a) - = array_get_error addr a. -Proof. intros; auto using array_get_error_equal, combine_none. Qed. - -Lemma list_combine_lookup_first : - forall l1 l2 n, - length l1 = length l2 -> - nth_error l1 n = Some None -> - nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. -Proof. - induction l1; intros; crush. - - rewrite nth_error_nil in H0. - discriminate. - - destruct l2 eqn:EQl2. crush. - simpl in H. inv H. - destruct n; simpl in *. - inv H0. simpl. reflexivity. - eauto. -Qed. - -Lemma combine_lookup_first : - forall a1 a2 n, - a1.(arr_length) = a2.(arr_length) -> - array_get_error n a1 = Some None -> - array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2. -Proof. - intros. - - unfold array_get_error in *. - apply list_combine_lookup_first; eauto. - rewrite a1.(arr_wf). rewrite a2.(arr_wf). - assumption. -Qed. - -Lemma list_combine_lookup_second : - forall l1 l2 n x, - length l1 = length l2 -> - nth_error l1 n = Some (Some x) -> - nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). -Proof. - induction l1; intros; crush; auto. - - destruct l2 eqn:EQl2. crush. - simpl in H. inv H. - destruct n; simpl in *. - inv H0. simpl. reflexivity. - eauto. -Qed. - -Lemma combine_lookup_second : - forall a1 a2 n x, - a1.(arr_length) = a2.(arr_length) -> - array_get_error n a1 = Some (Some x) -> - array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x). -Proof. - intros. - - unfold array_get_error in *. - apply list_combine_lookup_second; eauto. - rewrite a1.(arr_wf). rewrite a2.(arr_wf). - assumption. -Qed. - -Lemma match_get_arrs2 : - forall a i v l, - length a = l -> - list_combine merge_cell (list_set i (Some v) (list_repeat None l)) a = - list_combine merge_cell (list_repeat None l) (list_set i (Some v) a). -Proof. - induction a; crush; subst. - - destruct i. unfold list_repeat. unfold list_repeat'. auto. - unfold list_repeat. unfold list_repeat'. auto. - - destruct i. - rewrite list_repeat_cons. simplify. auto. - rewrite list_repeat_cons. simplify. f_equal. apply IHa. auto. -Qed. - -Lemma match_get_arrs : - forall addr i v x4 x x3, - x4 = arr_length x -> - x4 = arr_length x3 -> - array_get_error addr (combine merge_cell (array_set i (Some v) (arr_repeat None x4)) - (combine merge_cell x x3)) - = array_get_error addr (combine merge_cell (arr_repeat None x4) - (array_set i (Some v) (combine merge_cell x x3))). -Proof. - intros. apply array_get_error_equal. unfold combine. simplify. - destruct x; destruct x3; simplify. - apply match_get_arrs2. rewrite list_combine_length. subst. - rewrite H0. lia. -Qed. - -Lemma combine_array_set' : - forall a b i v, - length a = length b -> - list_combine merge_cell (list_set i (Some v) a) b = - list_set i (Some v) (list_combine merge_cell a b). -Proof. - induction a; simplify; crush. - - destruct i; crush. - - destruct i; destruct b; crush. - f_equal. apply IHa. auto. -Qed. - -Lemma combine_array_set : - forall a b i v addr, - arr_length a = arr_length b -> - array_get_error addr (combine merge_cell (array_set i (Some v) a) b) - = array_get_error addr (array_set i (Some v) (combine merge_cell a b)). -Proof. - intros. destruct a; destruct b. unfold array_set. simplify. - unfold array_get_error. simplify. f_equal. - apply combine_array_set'. crush. -Qed. - -Lemma array_get_combine' : - forall a b a' b' addr, - length a = length b -> - length a = length b' -> - length a = length a' -> - nth_error a addr = nth_error a' addr -> - nth_error b addr = nth_error b' addr -> - nth_error (list_combine merge_cell a b) addr = - nth_error (list_combine merge_cell a' b') addr. -Proof. - induction a; crush. - - destruct b; crush; destruct b'; crush; destruct a'; crush. - - destruct b; crush; destruct b'; crush; destruct a'; crush; - destruct addr; crush; apply IHa. -Qed. - -Lemma array_get_combine : - forall a b a' b' addr, - arr_length a = arr_length b -> - arr_length a = arr_length b' -> - arr_length a = arr_length a' -> - array_get_error addr a = array_get_error addr a' -> - array_get_error addr b = array_get_error addr b' -> - array_get_error addr (combine merge_cell a b) - = array_get_error addr (combine merge_cell a' b'). -Proof. - intros; unfold array_get_error, combine in *; destruct a; destruct b; - destruct a'; destruct b'; simplify; apply array_get_combine'; crush. -Qed. - -Lemma match_empty_size_exists_Some : - forall m rab s v, - match_empty_size m rab -> - rab ! s = Some v -> - exists v', (empty_stack m) ! s = Some v' /\ arr_length v = arr_length v'. -Proof. inversion 1; intros; repeat masrp_tac. Qed. - -Lemma match_empty_size_exists_None : - forall m rab s, - match_empty_size m rab -> - rab ! s = None -> - (empty_stack m) ! s = None. -Proof. inversion 1; intros; repeat masrp_tac. Qed. - -Lemma match_empty_size_exists_None' : - forall m rab s, - match_empty_size m rab -> - (empty_stack m) ! s = None -> - rab ! s = None. -Proof. inversion 1; intros; repeat masrp_tac. Qed. - -Lemma match_empty_size_exists_Some' : - forall m rab s v, - match_empty_size m rab -> - (empty_stack m) ! s = Some v -> - exists v', rab ! s = Some v' /\ arr_length v = arr_length v'. -Proof. inversion 1; intros; repeat masrp_tac. Qed. - -Lemma match_arrs_Some : - forall ra ra' s v, - match_arrs ra ra' -> - ra ! s = Some v -> - exists v', ra' ! s = Some v' - /\ (forall addr, array_get_error addr v = array_get_error addr v') - /\ arr_length v = arr_length v'. -Proof. inversion 1; intros; repeat masrp_tac. intros. rewrite H5. auto. Qed. - -Lemma match_arrs_None : - forall ra ra' s, - match_arrs ra ra' -> - ra ! s = None -> - ra' ! s = None. -Proof. inversion 1; intros; repeat masrp_tac. Qed. - -Ltac learn_next := - match goal with - | H: match_empty_size _ ?rab, H2: ?rab ! _ = Some _ |- _ => - let H3 := fresh "H" in - learn H2 as H3; eapply match_empty_size_exists_Some in H3; - eauto; inv_exists; simplify - | H: match_empty_size _ ?rab, H2: ?rab ! _ = None |- _ => - let H3 := fresh "H" in - learn H2 as H3; eapply match_empty_size_exists_None in H3; eauto - end. - -Ltac learn_empty := - match goal with - | H: match_empty_size _ _, H2: (empty_stack _) ! _ = Some _ |- _ => - let H3 := fresh "H" in - learn H as H3; eapply match_empty_size_exists_Some' in H3; - [| eassumption]; inv_exists; simplify - | H: match_arrs ?ar _, H2: ?ar ! _ = Some _ |- _ => - let H3 := fresh "H" in - learn H as H3; eapply match_arrs_Some in H3; - [| eassumption]; inv_exists; simplify - | H: match_empty_size _ _, H2: (empty_stack _) ! _ = None |- _ => - let H3 := fresh "H" in - learn H as H3; eapply match_empty_size_exists_None' in H3; - [| eassumption]; simplify - end. - -Lemma empty_set_none : - forall m ran rab s i v s0, - match_empty_size m ran -> - match_empty_size m rab -> - (arr_assocmap_set s i v ran) ! s0 = None -> - (arr_assocmap_set s i v rab) ! s0 = None. -Proof. - unfold arr_assocmap_set; inversion 1; subst; simplify. - destruct (Pos.eq_dec s s0); subst. - destruct ran ! s0 eqn:?. - rewrite AssocMap.gss in H4. inv H4. - learn_next. learn_empty. rewrite H6; auto. - destruct ran ! s eqn:?. rewrite AssocMap.gso in H4. - learn_next. learn_empty. rewrite H6. rewrite AssocMap.gso. - repeat match goal with - | H: Learnt _ |- _ => clear H - end. clear Heqo. clear H5. clear H6. - learn_next. repeat learn_empty. auto. auto. auto. - pose proof Heqo. learn_next; repeat learn_empty. - repeat match goal with - | H: Learnt _ |- _ => clear H - end. - pose proof H4. learn_next; repeat learn_empty. - rewrite H7. auto. -Qed. - -Ltac clear_learnt := - repeat match goal with - | H: Learnt _ |- _ => clear H - end. - -Lemma match_arrs_size_assoc : - forall a b, - match_arrs_size a b -> - match_arrs_size b a. -Proof. inversion 1; constructor; crush; split; apply H2. Qed. -#[local] Hint Resolve match_arrs_size_assoc : mgen. - -Lemma match_arrs_merge_set2 : - forall rab rab' ran ran' s m i v, - match_empty_size m rab -> - match_empty_size m ran -> - match_empty_size m rab' -> - match_empty_size m ran' -> - match_arrs rab rab' -> - match_arrs ran ran' -> - match_arrs (merge_arrs (arr_assocmap_set s i v ran) rab) - (merge_arrs (arr_assocmap_set s i v (empty_stack m)) - (merge_arrs ran' rab')). -Proof. - simplify. - constructor; intros. - unfold arr_assocmap_set in *. destruct (Pos.eq_dec s s0); subst. - destruct ran ! s0 eqn:?. unfold merge_arrs in *. rewrite AssocMap.gcombine in *; auto. - learn_next. repeat learn_empty. - econstructor. simplify. rewrite H6. rewrite AssocMap.gcombine by auto. - rewrite AssocMap.gss. simplify. setoid_rewrite H9. setoid_rewrite H7. simplify. - intros. rewrite AssocMap.gss in H5. setoid_rewrite H13 in H5. - simplify. pose proof (empty_arr m s0). inv H5. inv_exists. setoid_rewrite H5 in H6. inv H6. - unfold arr_repeat in H8. simplify. rewrite list_repeat_len in H8. rewrite list_repeat_len in H10. - rewrite match_get_arrs. crush. rewrite combine_none2. rewrite combine_array_set; try congruence. - apply array_get_error_each. rewrite combine_length; try congruence. - rewrite combine_length; try congruence. - apply array_get_combine; crush. - rewrite <- array_set_len. rewrite combine_length; crush. crush. crush. - setoid_rewrite H21 in H6; discriminate. rewrite combine_length. - rewrite <- array_set_len; crush. - unfold merge_arr in *. rewrite AssocMap.gss in H5. setoid_rewrite H13 in H5. - inv H5. rewrite combine_length. rewrite <- array_set_len; crush. - rewrite <- array_set_len; crush. - rewrite combine_length; crush. - destruct rab ! s0 eqn:?. learn_next. repeat learn_empty. - rewrite H11 in Heqo. discriminate. - unfold merge_arrs in H5. rewrite AssocMap.gcombine in H5; auto. rewrite Heqo in H5. - rewrite Heqo0 in H5. crush. - - destruct ran ! s eqn:?. - learn_next. repeat learn_empty. rewrite H6. - unfold merge_arrs in *. rewrite AssocMap.gcombine in H5; auto. - rewrite AssocMap.gcombine; auto. rewrite AssocMap.gso in H5; auto. - rewrite AssocMap.gso; auto. - destruct ran ! s0 eqn:?. - learn_next. - repeat match goal with - | H: Learnt _ |- _ => clear H - end. - repeat learn_empty. - repeat match goal with - | H: Learnt _ |- _ => clear H - end. - rewrite AssocMap.gcombine; auto. setoid_rewrite Heqo0 in H5. setoid_rewrite H29 in H5. - simplify. - pose proof (empty_arr m s0). inv H5. inv_exists. rewrite H5 in H21. inv H21. - econstructor. simplify. setoid_rewrite H23. rewrite H25. setoid_rewrite H5. - simplify. intros. rewrite combine_none2. apply array_get_combine; solve [crush]. - crush. rewrite list_combine_length. rewrite (arr_wf x5). rewrite (arr_wf x6). - rewrite <- H26. rewrite <- H28. rewrite list_repeat_len. lia. rewrite list_combine_length. - rewrite (arr_wf a). rewrite (arr_wf x7). rewrite combine_length. rewrite arr_repeat_length. - rewrite H24. rewrite <- H32. rewrite list_repeat_len. lia. - rewrite arr_repeat_length. rewrite combine_length. rewrite <- H26. symmetry. apply list_repeat_len. - congruence. - rewrite H37 in H21; discriminate. - repeat match goal with - | H: Learnt _ |- _ => clear H - end. eapply match_empty_size_exists_None in H0; eauto. - clear H6. repeat learn_empty. setoid_rewrite Heqo0 in H5. - setoid_rewrite H29 in H5. discriminate. - pose proof (match_arrs_merge ran ran' rab rab'). - eapply match_empty_size_match in H; [|apply H0]. - apply H6 in H; auto. inv H. apply H7 in H5. inv_exists. simplify. - learn_next. rewrite H9. econstructor. simplify. - apply merge_arr_empty''; mgen_crush. - auto. auto. - unfold merge_arrs in *. rewrite AssocMap.gcombine in H5; auto. rewrite AssocMap.gcombine; auto. - destruct (arr_assocmap_set s i v ran) ! s0 eqn:?; destruct rab ! s0 eqn:?; crush. - learn_next. repeat learn_empty. - repeat match goal with - | H: Learnt _ |- _ => clear H - end. - erewrite empty_set_none. rewrite AssocMap.gcombine; auto. - simplify. rewrite H7. rewrite H8. auto. apply H0. mgen_crush. auto. -Qed. - -Definition all_match_empty_size m ar := - match_empty_size m (assoc_nonblocking ar) /\ match_empty_size m (assoc_blocking ar). -#[local] Hint Unfold all_match_empty_size : mgen. - -Definition match_module_to_ram m ram := - ram_size ram = mod_stk_len m /\ ram_mem ram = mod_stk m. -#[local] Hint Unfold match_module_to_ram : mgen. - -Lemma zip_range_forall_le : - forall A (l: list A) n, Forall (Pos.le n) (map snd (zip_range n l)). -Proof. - induction l; crush; constructor; [lia|]. - assert (forall n x, n+1 <= x -> n <= x) by lia. - apply Forall_forall. intros. apply H. generalize dependent x. - apply Forall_forall. apply IHl. -Qed. - -Lemma transf_code_fold_correct: - forall l m state ram d' c' n, - fold_right (transf_maps state ram) (mod_datapath m, mod_controllogic m) l = (d', c') -> - Forall (fun x => x < n) (map fst l) -> - Forall (Pos.le n) (map snd l) -> - list_norepet (map fst l) -> - list_norepet (map snd l) -> - (forall p i c_s rs1 ar1 rs2 ar2 trs1 tar1 d_s, - i < n -> - all_match_empty_size m ar1 -> - all_match_empty_size m tar1 -> - match_module_to_ram m ram -> - (mod_datapath m)!i = Some d_s -> - (mod_controllogic m)!i = Some c_s -> - match_reg_assocs p rs1 trs1 -> - match_arr_assocs ar1 tar1 -> - max_reg_module m < p -> - exec_all d_s c_s rs1 ar1 rs2 ar2 -> - exists d_s' c_s' trs2 tar2, - d'!i = Some d_s' /\ c'!i = Some c_s' - /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2 - /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) - /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2) - (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2)). -Proof. - induction l as [| a l IHl]; simplify. - - match goal with - | H: (_, _) = (_, _) |- _ => inv H - end; - unfold exec_all in *; repeat inv_exists; simplify. - exploit match_states_same; - try match goal with - | H: stmnt_runp _ _ _ ?c _ _, H2: (mod_controllogic _) ! _ = Some ?c |- _ => apply H - end; eauto; mgen_crush; - try match goal with - | H: (mod_controllogic _) ! _ = Some ?c |- _ => - apply max_reg_stmnt_le_stmnt_tree in H; unfold max_reg_module in *; lia - end; intros; - exploit match_states_same; - try match goal with - | H: stmnt_runp _ _ _ ?c _ _, H2: (mod_datapath _) ! _ = Some ?c |- _ => apply H - end; eauto; mgen_crush; - try match goal with - | H: (mod_datapath _) ! _ = Some ?c |- _ => - apply max_reg_stmnt_le_stmnt_tree in H; unfold max_reg_module in *; lia - end; intros; - repeat match goal with - | |- exists _, _ => eexists - end; simplify; eauto; - unfold exec_all_ram; - repeat match goal with - | |- exists _, _ => eexists - end; simplify; eauto. - constructor. admit. - Abort. - -Lemma empty_stack_transf : forall m, empty_stack (transf_module m) = empty_stack m. -Proof. unfold empty_stack, transf_module; intros; repeat destruct_match; crush. Qed. - -Definition alt_unchanged (d : AssocMap.t stmnt) (c: AssocMap.t stmnt) d' c' i := - d ! i = d' ! i /\ c ! i = c' ! i. - -Definition alt_store ram d (c : AssocMap.t stmnt) d' c' i := - exists e1 e2, - d' ! i = Some (Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) - (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) - (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2) - (Vnonblock (Vvar (ram_addr ram)) e1)))) - /\ c' ! i = c ! i - /\ d ! i = Some (Vnonblock (Vvari (ram_mem ram) e1) e2). - -Definition alt_load state ram d (c : AssocMap.t stmnt) d' c' i n := - exists ns e1 e2, - d' ! i = Some (Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) - (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) - (Vnonblock (Vvar (ram_addr ram)) e2))) - /\ d' ! n = Some (Vnonblock (Vvar e1) (Vvar (ram_d_out ram))) - /\ c' ! i = Some (Vnonblock (Vvar state) (Vlit (posToValue n))) - /\ c' ! n = Some (Vnonblock (Vvar state) ns) - /\ c ! i = Some (Vnonblock (Vvar state) ns) - /\ d ! i = Some (Vnonblock (Vvar e1) (Vvari (ram_mem ram) e2)) - /\ e1 < state - /\ max_reg_expr e2 < state - /\ max_reg_expr ns < state - /\ (Z.pos n <= Int.max_unsigned)%Z. - -Definition alternatives state ram d c d' c' i n := - alt_unchanged d c d' c' i - \/ alt_store ram d c d' c' i - \/ alt_load state ram d c d' c' i n. - -Lemma transf_alternatives : - forall ram n d c state i d' c', - transf_maps state ram (i, n) (d, c) = (d', c') -> - i <> n -> - alternatives state ram d c d' c' i n. -Proof. - intros. unfold transf_maps in *. - repeat destruct_match; match goal with - | H: (_, _) = (_, _) |- _ => inv H - end; try solve [left; econstructor; crush]; simplify; - repeat match goal with - | H: (_ =? _) = true |- _ => apply Peqb_true_eq in H; subst - end; unfold alternatives; right; - match goal with - | H: context[Vnonblock (Vvari _ _) _] |- _ => left - | _ => right - end; repeat econstructor; simplify; - repeat match goal with - | |- ( _ # ?s <- _ ) ! ?s = Some _ => apply AssocMap.gss - | |- ( _ # ?s <- _ ) ! ?r = Some _ => rewrite AssocMap.gso by lia - | |- _ = None => apply max_index_2; lia - | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H - end; auto. -Qed. - -Lemma transf_alternatives_neq : - forall state ram a n' n d'' c'' d' c' i d c, - transf_maps state ram (a, n) (d, c) = (d', c') -> - a <> i -> n' <> n -> i <> n' -> a <> n' -> - i <> n -> a <> n -> - alternatives state ram d'' c'' d c i n' -> - alternatives state ram d'' c'' d' c' i n'. -Proof. - unfold alternatives, alt_unchanged, alt_store, alt_load, transf_maps; intros; - repeat match goal with H: _ \/ _ |- _ => inv H | H: _ /\ _ |- _ => destruct H end; - [left | right; left | right; right]; - repeat inv_exists; simplify; - repeat destruct_match; - repeat match goal with - | H: (_, _) = (_, _) |- _ => inv H - | |- exists _, _ => econstructor - end; repeat split; repeat rewrite AssocMap.gso by lia; eauto; lia. -Qed. - -Lemma transf_alternatives_neq2 : - forall state ram a n' n d'' c'' d' c' i d c, - transf_maps state ram (a, n) (d', c') = (d, c) -> - a <> i -> n' <> n -> i <> n' -> a <> n' -> i <> n -> - alternatives state ram d c d'' c'' i n' -> - alternatives state ram d' c' d'' c'' i n'. -Proof. - unfold alternatives, alt_unchanged, alt_store, alt_load, transf_maps; intros; - repeat match goal with H: _ \/ _ |- _ => inv H | H: _ /\ _ |- _ => destruct H end; - [left | right; left | right; right]; - repeat inv_exists; simplify; - repeat destruct_match; - repeat match goal with - | H: (_, _) = (_, _) |- _ => inv H - | |- exists _, _ => econstructor - end; repeat split; repeat rewrite AssocMap.gso in * by lia; eauto; lia. -Qed. - -Lemma transf_alt_unchanged_neq : - forall i c'' d'' d c d' c', - alt_unchanged d' c' d'' c'' i -> - d' ! i = d ! i -> - c' ! i = c ! i -> - alt_unchanged d c d'' c'' i. -Proof. unfold alt_unchanged; simplify; congruence. Qed. - -Lemma transf_maps_neq : - forall state ram d c i n d' c' i' n' va vb vc vd, - transf_maps state ram (i, n) (d, c) = (d', c') -> - d ! i' = va -> d ! n' = vb -> - c ! i' = vc -> c ! n' = vd -> - i <> i' -> i <> n' -> n <> i' -> n <> n' -> - d' ! i' = va /\ d' ! n' = vb /\ c' ! i' = vc /\ c' ! n' = vd. -Proof. - unfold transf_maps; intros; repeat destruct_match; simplify; - repeat match goal with - | H: (_, _) = (_, _) |- _ => inv H - | H: (_ =? _) = true |- _ => apply Peqb_true_eq in H; subst - | |- context[( _ # ?s <- _ ) ! ?r] => rewrite AssocMap.gso by lia - end; crush. -Qed. - -Lemma alternatives_different_map : - forall l state ram d c d'' c'' d' c' n i p, - i <= p -> n > p -> - Forall (Pos.lt p) (map snd l) -> - Forall (Pos.ge p) (map fst l) -> - ~ In n (map snd l) -> - ~ In i (map fst l) -> - fold_right (transf_maps state ram) (d, c) l = (d', c') -> - alternatives state ram d' c' d'' c'' i n -> - alternatives state ram d c d'' c'' i n. -Proof. - Opaque transf_maps. - induction l; intros. - - crush. - - simplify; repeat match goal with - | H: context[_ :: _] |- _ => inv H - | H: transf_maps _ _ _ (fold_right (transf_maps ?s ?r) (?d, ?c) ?l) = (_, _) |- _ => - let X := fresh "X" in - remember (fold_right (transf_maps s r) (d, c) l) as X - | X: _ * _ |- _ => destruct X - | H: (_, _) = _ |- _ => symmetry in H - end; simplify. - remember p0 as i'. symmetry in Heqi'. subst. - remember p1 as n'. symmetry in Heqn'. subst. - assert (i <> n') by lia. - assert (n <> i') by lia. - assert (n <> n') by lia. - assert (i <> i') by lia. - eapply IHl; eauto. - eapply transf_alternatives_neq2; eauto; try lia. -Qed. - -Lemma transf_fold_alternatives : - forall l state ram d c d' c' i n d_s c_s, - fold_right (transf_maps state ram) (d, c) l = (d', c') -> - Pos.max (max_pc c) (max_pc d) < n -> - Forall (Pos.lt (Pos.max (max_pc c) (max_pc d))) (map snd l) -> - Forall (Pos.ge (Pos.max (max_pc c) (max_pc d))) (map fst l) -> - list_norepet (map fst l) -> - list_norepet (map snd l) -> - In (i, n) l -> - d ! i = Some d_s -> - c ! i = Some c_s -> - alternatives state ram d c d' c' i n. -Proof. - Opaque transf_maps. - induction l; crush; []. - repeat match goal with - | H: context[_ :: _] |- _ => inv H - | H: transf_maps _ _ _ (fold_right (transf_maps ?s ?r) (?d, ?c) ?l) = (_, _) |- _ => - let X := fresh "X" in - remember (fold_right (transf_maps s r) (d, c) l) as X - | X: _ * _ |- _ => destruct X - | H: (_, _) = _ |- _ => symmetry in H - end. - inv H5. inv H1. simplify. - eapply alternatives_different_map; eauto. - simplify; lia. simplify; lia. apply transf_alternatives; auto. lia. - simplify. - assert (X: In i (map fst l)). { replace i with (fst (i, n)) by auto. apply in_map; auto. } - assert (X2: In n (map snd l)). { replace n with (snd (i, n)) by auto. apply in_map; auto. } - assert (X3: n <> p0). { destruct (Pos.eq_dec n p0); subst; crush. } - assert (X4: i <> p). { destruct (Pos.eq_dec i p); subst; crush. } - eapply transf_alternatives_neq; eauto; apply max_index in H7; lia. - Transparent transf_maps. -Qed. - -Lemma zip_range_inv : - forall A (l: list A) i n, - In i l -> - exists n', In (i, n') (zip_range n l) /\ n' >= n. -Proof. - induction l; crush. - inv H. econstructor. - split. left. eauto. lia. - eapply IHl in H0. inv H0. inv H. - econstructor. split. right. apply H0. lia. -Qed. - -Lemma zip_range_not_in_fst : - forall A (l: list A) a n, ~ In a l -> ~ In a (map fst (zip_range n l)). -Proof. unfold not; induction l; crush; inv H0; firstorder. Qed. - -Lemma zip_range_no_repet_fst : - forall A (l: list A) a, list_norepet l -> list_norepet (map fst (zip_range a l)). -Proof. - induction l; simplify; constructor; inv H; firstorder; - eapply zip_range_not_in_fst; auto. -Qed. - -Lemma transf_code_alternatives : - forall state ram d c d' c' i d_s c_s, - transf_code state ram d c = (d', c') -> - d ! i = Some d_s -> - c ! i = Some c_s -> - exists n, alternatives state ram d c d' c' i n. -Proof. - unfold transf_code; - intros. - pose proof H0 as X. - apply PTree.elements_correct in X. assert (In i (map fst (PTree.elements d))). - { replace i with (fst (i, d_s)) by auto. apply in_map. auto. } - exploit zip_range_inv. apply H2. intros. inv H3. simplify. - instantiate (1 := (Pos.max (max_pc c) (max_pc d) + 1)) in H3. - exists x. - eapply transf_fold_alternatives; - eauto using forall_gt, PTree.elements_keys_norepet, max_index. lia. - assert (Forall (Pos.le (Pos.max (max_pc c) (max_pc d) + 1)) - (map snd (zip_range (Pos.max (max_pc c) (max_pc d) + 1) - (map fst (PTree.elements d))))) by apply zip_range_forall_le. - apply Forall_forall; intros. eapply Forall_forall in H4; eauto. lia. - rewrite zip_range_fst_idem. apply Forall_forall; intros. - apply AssocMapExt.elements_iff in H4. inv H4. apply max_index in H6. lia. - eapply zip_range_no_repet_fst. apply PTree.elements_keys_norepet. - eapply zip_range_snd_no_repet. -Qed. - -Lemma max_reg_stmnt_not_modified : - forall s f rs ar rs' ar', - stmnt_runp f rs ar s rs' ar' -> - forall r, - max_reg_stmnt s < r -> - (assoc_blocking rs) ! r = (assoc_blocking rs') ! r. -Proof. - induction 1; crush; - try solve [repeat destruct_match; apply IHstmnt_runp; try lia; auto]. - assert (X: (assoc_blocking asr1) ! r = (assoc_blocking asr2) ! r) by (apply IHstmnt_runp2; lia). - assert (X2: (assoc_blocking asr0) ! r = (assoc_blocking asr1) ! r) by (apply IHstmnt_runp1; lia). - congruence. - inv H. simplify. rewrite AssocMap.gso by lia; auto. -Qed. - -Lemma max_reg_stmnt_not_modified_nb : - forall s f rs ar rs' ar', - stmnt_runp f rs ar s rs' ar' -> - forall r, - max_reg_stmnt s < r -> - (assoc_nonblocking rs) ! r = (assoc_nonblocking rs') ! r. -Proof. - induction 1; crush; - try solve [repeat destruct_match; apply IHstmnt_runp; try lia; auto]. - assert (X: (assoc_nonblocking asr1) ! r = (assoc_nonblocking asr2) ! r) by (apply IHstmnt_runp2; lia). - assert (X2: (assoc_nonblocking asr0) ! r = (assoc_nonblocking asr1) ! r) by (apply IHstmnt_runp1; lia). - congruence. - inv H. simplify. rewrite AssocMap.gso by lia; auto. -Qed. - -Lemma int_eq_not_changed : - forall ar ar' r r2 b, - Int.eq (ar # r) (ar # r2) = b -> - ar ! r = ar' ! r -> - ar ! r2 = ar' ! r2 -> - Int.eq (ar' # r) (ar' # r2) = b. -Proof. - unfold find_assocmap, AssocMapExt.get_default. intros. - rewrite <- H0. rewrite <- H1. auto. -Qed. - -Lemma merge_find_assocmap : - forall ran rab x, - ran ! x = None -> - (merge_regs ran rab) # x = rab # x. -Proof. - unfold merge_regs, find_assocmap, AssocMapExt.get_default. - intros. destruct (rab ! x) eqn:?. - erewrite AssocMapExt.merge_correct_2; eauto. - erewrite AssocMapExt.merge_correct_3; eauto. -Qed. - -Lemma max_reg_module_controllogic_gt : - forall m i v p, - (mod_controllogic m) ! i = Some v -> - max_reg_module m < p -> - max_reg_stmnt v < p. -Proof. - intros. unfold max_reg_module in *. - apply max_reg_stmnt_le_stmnt_tree in H. lia. -Qed. - -Lemma max_reg_module_datapath_gt : - forall m i v p, - (mod_datapath m) ! i = Some v -> - max_reg_module m < p -> - max_reg_stmnt v < p. -Proof. - intros. unfold max_reg_module in *. - apply max_reg_stmnt_le_stmnt_tree in H. lia. -Qed. - -Lemma merge_arr_empty2 : - forall m ar ar', - match_empty_size m ar' -> - match_arrs ar ar' -> - match_arrs ar (merge_arrs (empty_stack m) ar'). -Proof. - inversion 1; subst; inversion 1; subst. - econstructor; intros. apply H4 in H6; inv_exists. simplify. - eapply merge_arr_empty'' in H6; eauto. - (* apply H5 in H6. pose proof H6. apply H2 in H7. *) -(* unfold merge_arrs. rewrite AssocMap.gcombine; auto. setoid_rewrite H6. *) -(* setoid_rewrite H7. auto. *) -(* Qed. *) Admitted. -#[local] Hint Resolve merge_arr_empty2 : mgen. - -Lemma find_assocmap_gso : - forall ar x y v, x <> y -> (ar # y <- v) # x = ar # x. -Proof. - unfold find_assocmap, AssocMapExt.get_default; intros; rewrite AssocMap.gso; auto. -Qed. - -Lemma find_assocmap_gss : - forall ar x v, (ar # x <- v) # x = v. -Proof. - unfold find_assocmap, AssocMapExt.get_default; intros; rewrite AssocMap.gss; auto. -Qed. - -Lemma expr_lt_max_module_datapath : - forall m x, - max_reg_stmnt x <= max_stmnt_tree (mod_datapath m) -> - max_reg_stmnt x < max_reg_module m + 1. -Proof. unfold max_reg_module. lia. Qed. - -Lemma expr_lt_max_module_controllogic : - forall m x, - max_reg_stmnt x <= max_stmnt_tree (mod_controllogic m) -> - max_reg_stmnt x < max_reg_module m + 1. -Proof. unfold max_reg_module. lia. Qed. - -Lemma int_eq_not : - forall x y, Int.eq x y = true -> Int.eq x (Int.not y) = false. -Proof. - intros. pose proof (Int.eq_spec x y). rewrite H in H0. subst. - apply int_eq_not_false. -Qed. - -Lemma match_assocmaps_gt2 : - forall (p s : positive) (ra ra' : assocmap) (v : value), - p <= s -> match_assocmaps p ra ra' -> match_assocmaps p (ra # s <- v) ra'. -Proof. - intros; inv H0; constructor; intros. - destruct (Pos.eq_dec r s); subst. lia. - rewrite AssocMap.gso by lia. auto. -Qed. - -Lemma match_assocmaps_switch_neq : - forall p ra ra' r v' s v, - match_assocmaps p ra ((ra' # r <- v') # s <- v) -> - s <> r -> - match_assocmaps p ra ((ra' # s <- v) # r <- v'). -Proof. - inversion 1; constructor; simplify. - destruct (Pos.eq_dec r0 s); destruct (Pos.eq_dec r0 r); subst; try lia. - rewrite AssocMap.gso by lia. specialize (H0 s). apply H0 in H5. - rewrite AssocMap.gss in H5. rewrite AssocMap.gss. auto. - rewrite AssocMap.gss. apply H0 in H5. rewrite AssocMap.gso in H5 by lia. - rewrite AssocMap.gss in H5. auto. - repeat rewrite AssocMap.gso by lia. - apply H0 in H5. repeat rewrite AssocMap.gso in H5 by lia. - auto. -Qed. - -Lemma match_assocmaps_duplicate : - forall p ra ra' v' s v, - match_assocmaps p ra (ra' # s <- v) -> - match_assocmaps p ra ((ra' # s <- v') # s <- v). -Proof. - inversion 1; constructor; simplify. - destruct (Pos.eq_dec r s); subst. - rewrite AssocMap.gss. apply H0 in H4. rewrite AssocMap.gss in H4. auto. - repeat rewrite AssocMap.gso by lia. apply H0 in H4. rewrite AssocMap.gso in H4 by lia. - auto. -Qed. - -Ltac simplify := intros; unfold_constants; cbn in *; - repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp); - cbn in *. - -Ltac simplify_val := repeat (simplify; 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 crush := simplify; try discriminate; try congruence; try lia; liapp; - try assumption; auto. - -Ltac mgen_crush_local := crush; eauto with mgen. - -Lemma translation_correct : - forall m asr nasa1 basa1 nasr1 basr1 basr2 nasr2 nasa2 basa2 nasr3 basr3 - nasa3 basa3 asr'0 asa'0 res' st tge pstval sf asa ctrl data f, - asr ! (mod_reset m) = Some (ZToValue 0) -> - asr ! (mod_finish m) = Some (ZToValue 0) -> - asr ! (mod_st m) = Some (posToValue st) -> - (mod_controllogic m) ! st = Some ctrl -> - (mod_datapath m) ! st = Some data -> - stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} - {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} ctrl - {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} - {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} -> - basr1 ! (mod_st m) = Some (posToValue st) -> - stmnt_runp f {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} - {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} data - {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |} - {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |} -> - exec_ram {| assoc_blocking := merge_regs nasr2 basr2; assoc_nonblocking := empty_assocmap |} - {| assoc_blocking := merge_arrs nasa2 basa2; assoc_nonblocking := empty_stack m |} None - {| assoc_blocking := basr3; assoc_nonblocking := nasr3 |} - {| assoc_blocking := basa3; assoc_nonblocking := nasa3 |} -> - (merge_regs nasr3 basr3) ! (mod_st m) = Some (posToValue pstval) -> - (Z.pos pstval <= 4294967295)%Z -> - match_states (State sf m st asr asa) (State res' (transf_module m) st asr'0 asa'0) -> - mod_ram m = None -> - exists R2 : state, - Smallstep.plus step tge (State res' (transf_module m) st asr'0 asa'0) Events.E0 R2 /\ - match_states (State sf m pstval (merge_regs nasr3 basr3) (merge_arrs nasa3 basa3)) R2. -Proof. - Ltac tac0 := - repeat match goal with - | H: match_reg_assocs _ _ _ |- _ => inv H - | H: match_arr_assocs _ _ |- _ => inv H - end. - intros. - repeat match goal with - | H: match_states _ _ |- _ => inv H - | H: context[exec_ram] |- _ => inv H - | H: mod_ram _ = None |- _ => - let H2 := fresh "TRANSF" in learn H as H2; apply transf_module_code in H2 - end. - eapply transf_code_alternatives in TRANSF; eauto; simplify; unfold alternatives in *. - repeat match goal with H: _ \/ _ |- _ => inv H end. - - unfold alt_unchanged in *; simplify. - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). - { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; eauto with mgen. } - assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). - { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. - assert (MATCH_ARR3: match_arrs_size nasa2 basa2) by eauto with mgen. - exploit match_states_same; try solve [apply H4 | eapply max_stmnt_lt_module; eauto - | econstructor; eauto with mgen]; - intros; repeat inv_exists; simplify; tac0. - exploit match_states_same; try solve [eapply H6 | eapply max_stmnt_lt_module; eauto - | econstructor; eauto with mgen]; - intros; repeat inv_exists; simplify; tac0. - assert (MATCH_SIZE1': match_empty_size m ran'0 /\ match_empty_size m rab'0). - { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; eauto with mgen. - rewrite empty_stack_transf; eauto with mgen. } - assert (MATCH_SIZE2': match_empty_size m ran'2 /\ match_empty_size m rab'2). - { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. - assert (MATCH_ARR3': match_arrs_size ran'2 rab'2) by eauto with mgen. - do 2 econstructor. apply Smallstep.plus_one. econstructor. - eauto with mgen. eauto with mgen. eauto with mgen. - rewrite <- H12. eassumption. rewrite <- H7. eassumption. - eauto. eauto with mgen. eauto. - rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; try discriminate. - econstructor. simplify. - unfold disable_ram in *. unfold transf_module in DISABLE_RAM. - repeat destruct_match; try discriminate; []. simplify. - pose proof H17 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. - pose proof H17 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. - pose proof H18 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. - pose proof H18 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. - pose proof H17 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. - pose proof H17 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. - pose proof H18 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. - pose proof H18 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. - simplify. - pose proof DISABLE_RAM as DISABLE_RAM1. - eapply int_eq_not_changed with (ar' := rab') in DISABLE_RAM; try congruence. - eapply int_eq_not_changed with (ar' := rab'1) in DISABLE_RAM; try congruence. - rewrite AssocMap.gempty in R2. rewrite <- R2 in R4. - rewrite AssocMap.gempty in R2'. rewrite <- R2' in R4'. - eapply int_eq_not_changed in DISABLE_RAM; auto. repeat (rewrite merge_find_assocmap; try congruence). - eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - auto. auto. eauto with mgen. auto. - econstructor; mgen_crush_local. apply merge_arr_empty; mgen_crush_local. - unfold disable_ram in *. unfold transf_module in DISABLE_RAM. - repeat destruct_match; crush. unfold transf_module in Heqo; repeat destruct_match; crush. - pose proof H17 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1. - pose proof H17 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2. - pose proof H18 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3. - pose proof H18 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4. - pose proof H17 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'. - pose proof H17 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'. - pose proof H18 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'. - pose proof H18 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'. - simplify. - pose proof DISABLE_RAM as DISABLE_RAM1. - eapply int_eq_not_changed with (ar' := rab') in DISABLE_RAM; try congruence. - eapply int_eq_not_changed with (ar' := rab'1) in DISABLE_RAM; try congruence. - rewrite AssocMap.gempty in R2. rewrite <- R2 in R4. - rewrite AssocMap.gempty in R2'. rewrite <- R2' in R4'. - eapply int_eq_not_changed in DISABLE_RAM; auto. repeat (rewrite merge_find_assocmap; try congruence). - unfold empty_assocmap; apply AssocMap.gempty. - unfold empty_assocmap; apply AssocMap.gempty. - eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - - unfold alt_store in *; simplify. inv H6. inv H19. inv H19. simplify. - exploit match_states_same; try solve [eapply H4 | eapply max_stmnt_lt_module; eauto - | econstructor; eauto with mgen]; - intros; repeat inv_exists; simplify; tac0. - do 2 econstructor. apply Smallstep.plus_one. econstructor. solve [eauto with mgen]. solve [eauto with mgen]. - solve [eauto with mgen]. - rewrite H7. eassumption. eassumption. eassumption. solve [eauto with mgen]. - econstructor. econstructor. econstructor. econstructor. econstructor. - auto. auto. auto. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - eapply expr_runp_matches2. eassumption. 2: { cbn. eassumption. } - pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. - apply expr_lt_max_module_datapath in X; simplify; remember (max_reg_module m); lia. - auto. - econstructor. econstructor. eapply expr_runp_matches2; eauto. - pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. - apply expr_lt_max_module_datapath in X. - remember (max_reg_module m); simplify; lia. - - rewrite empty_stack_transf. - unfold transf_module; repeat destruct_match; try discriminate; simplify; []. - eapply exec_ram_Some_write. - 3: { - simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. - repeat rewrite find_assocmap_gso by lia. - pose proof H12 as X. - eapply max_reg_stmnt_not_modified_nb with (r := (max_reg_module m + 2)) in X. - rewrite AssocMap.gempty in X. - apply merge_find_assocmap. repeat rewrite AssocMap.gso by lia. auto. - apply max_reg_stmnt_le_stmnt_tree in H2. - apply expr_lt_max_module_controllogic in H2. lia. - } - 3: { - simplify. unfold merge_regs. erewrite merge_get_default4. eauto. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - } - { unfold disable_ram in *. unfold transf_module in DISABLE_RAM; - repeat destruct_match; try discriminate. - simplify. - pose proof H12 as X2. - pose proof H12 as X4. - apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in X2. - apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in X4. - assert (forall ar ar' x, ar ! x = ar' ! x -> ar # x = ar' # x). - { intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H6. auto. } - apply H6 in X2. apply H6 in X4. simplify. rewrite <- X2. rewrite <- X4. - apply int_eq_not. auto. - apply max_reg_stmnt_le_stmnt_tree in H2. - apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia. - apply max_reg_stmnt_le_stmnt_tree in H2. - apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia. - } - 2: { - simplify. unfold merge_regs. erewrite merge_get_default4. eauto. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - } - solve [auto]. - simplify. unfold merge_regs. erewrite merge_get_default4. eauto. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - simplify. unfold merge_regs. erewrite merge_get_default4. eauto. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - simplify. auto. - simplify. auto. - unfold merge_regs. repeat rewrite ! AssocMapExt.merge_add_assoc. - unfold empty_assocmap. - assert (mod_st (transf_module m) < max_reg_module m + 1). - { unfold max_reg_module, transf_module; repeat destruct_match; try discriminate; simplify; lia. } - remember (max_reg_module m). - repeat rewrite AssocMap.gso by lia. - unfold_merge. - apply merge_get_default4. - repeat rewrite AssocMap.gso by lia. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - eapply match_assocmaps_merge in H21. - 2: { apply H21. } - admit. admit. - - econstructor. unfold merge_regs. admit. - - apply merge_arr_empty. apply match_empty_size_merge. - apply match_empty_assocmap_set. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush_local. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush_local. - apply match_arrs_merge_set2; auto. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush_local. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush_local. - eapply match_arrs_size_stmnt_preserved in H12; mgen_crush_local. - rewrite empty_stack_transf. mgen_crush_local. - eapply match_arrs_size_stmnt_preserved in H12; mgen_crush_local. - rewrite empty_stack_transf. mgen_crush_local. - auto. - admit. - admit. admit. - - unfold alt_load in *; simplify. inv H6. - 2: { match goal with H: context[location_is] |- _ => inv H end. } - match goal with H: context[location_is] |- _ => inv H end. - inv H30. simplify. inv H4. - 2: { match goal with H: context[location_is] |- _ => inv H end. } - inv H27. simplify. - do 2 econstructor. eapply Smallstep.plus_two. - econstructor. mgen_crush_local. mgen_crush_local. mgen_crush_local. eassumption. - eassumption. econstructor. simplify. econstructor. econstructor. - solve [eauto with mgen]. econstructor. econstructor. econstructor. - econstructor. econstructor. auto. auto. auto. - econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. cbn. eapply expr_runp_matches2; auto. eassumption. - 2: { eassumption. } - pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. - apply expr_lt_max_module_datapath in X. simplify. remember (max_reg_module m); lia. - auto. - - simplify. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. - eapply exec_ram_Some_read; simplify. - 2: { - unfold merge_regs. admit. - } - 2: { - unfold merge_regs. admit. - } - { unfold disable_ram, transf_module in DISABLE_RAM; - repeat destruct_match; try discriminate. simplify. apply int_eq_not. auto. admit. } (* } *) -(* { unfold merge_regs; unfold_merge. repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. } *) -(* { unfold merge_regs; unfold_merge. apply AssocMap.gss. } *) -(* { eapply match_arrs_read. eassumption. mgen_crush_local. } *) -(* { crush. } *) -(* { crush. } *) -(* { unfold merge_regs. unfold_merge. *) -(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) -(* assert (mod_st m < max_reg_module m + 1). *) -(* { unfold max_reg_module; lia. } *) -(* remember (max_reg_module m). repeat rewrite AssocMap.gso by lia. *) -(* apply AssocMap.gss. *) -(* } *) -(* { auto. } *) - -(* { econstructor. *) -(* { unfold merge_regs. unfold_merge. *) -(* assert (mod_reset m < max_reg_module m + 1). *) -(* { unfold max_reg_module; lia. } *) -(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) -(* assert (mod_st m < mod_reset m). *) -(* { pose proof (mod_ordering_wf m); unfold module_ordering in *. simplify. *) -(* repeat match goal with *) -(* | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H *) -(* end; lia. *) -(* } *) -(* repeat rewrite AssocMap.gso by lia. *) -(* inv ASSOC. rewrite <- H19. auto. lia. *) -(* } *) -(* { unfold merge_regs. unfold_merge. *) -(* assert (mod_finish m < max_reg_module m + 1). *) -(* { unfold max_reg_module; lia. } *) -(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) -(* assert (mod_st m < mod_finish m). *) -(* { pose proof (mod_ordering_wf m). unfold module_ordering in *. simplify. *) -(* repeat match goal with *) -(* | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H *) -(* end; lia. *) -(* } *) -(* repeat rewrite AssocMap.gso by lia. *) -(* inv ASSOC. rewrite <- H19. auto. lia. *) -(* } *) -(* { unfold merge_regs. unfold_merge. *) -(* assert (mod_st m < max_reg_module m + 1). *) -(* { unfold max_reg_module; lia. } *) -(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) -(* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) -(* } *) -(* { eassumption. } *) -(* { eassumption. } *) -(* { econstructor. econstructor. simplify. unfold merge_regs. unfold_merge. *) -(* eapply expr_runp_matches. eassumption. *) -(* assert (max_reg_expr x0 + 1 <= max_reg_module m + 1). *) -(* { pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) -(* apply expr_lt_max_module_controllogic in X. simplify. remember (max_reg_module m). lia. } *) -(* assert (max_reg_expr x0 + 1 <= mod_st m). *) -(* { unfold module_ordering in *. simplify. *) -(* repeat match goal with *) -(* | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H *) -(* end. *) -(* pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) -(* simplify. lia. *) -(* } *) -(* remember (max_reg_module m). *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* simplify. *) -(* eapply match_assocmaps_ge. eauto. lia. *) -(* mgen_crush_local. *) -(* } *) -(* { simplify. unfold merge_regs. unfold_merge. *) -(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) -(* assert (mod_st m < max_reg_module m + 1). *) -(* { unfold max_reg_module; lia. } *) -(* remember (max_reg_module m). *) -(* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) -(* } *) -(* { *) -(* simplify. econstructor. econstructor. econstructor. simplify. *) -(* unfold merge_regs; unfold_merge. *) -(* repeat rewrite find_assocmap_gso by lia. apply find_assocmap_gss. *) -(* } *) -(* { simplify. rewrite empty_stack_transf. *) -(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) -(* econstructor. simplify. *) -(* unfold merge_regs; unfold_merge. simplify. *) -(* assert (r < max_reg_module m + 1). *) -(* { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. *) -(* unfold max_reg_stmnt in X. simplify. *) -(* lia. lia. } *) -(* assert (mod_st m < max_reg_module m + 1). *) -(* { unfold max_reg_module; lia. } *) -(* repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. *) -(* repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. *) -(* apply Int.eq_true. *) -(* } *) -(* { crush. } *) -(* { crush. } *) -(* { unfold merge_regs. unfold_merge. simplify. *) -(* assert (r < mod_st m). *) -(* { unfold module_ordering in *. simplify. *) -(* repeat match goal with *) -(* | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H *) -(* end. *) -(* pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) -(* simplify. lia. *) -(* } *) -(* unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. *) -(* simplify. rewrite AssocMap.gso in H8 by lia. rewrite AssocMap.gss in H8. *) -(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) -(* repeat rewrite AssocMap.gso by lia. *) -(* apply AssocMap.gss. } *) -(* { eassumption. } *) -(* } *) -(* { eauto. } *) -(* { econstructor. *) -(* { unfold merge_regs. unfold_merge. simplify. *) -(* apply match_assocmaps_gss. *) -(* unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. *) -(* rewrite AssocMap.gso in H8. rewrite AssocMap.gss in H8. inv H8. *) -(* remember (max_reg_module m). *) -(* assert (mod_st m < max_reg_module m + 1). *) -(* { unfold max_reg_module; lia. } *) -(* apply match_assocmaps_switch_neq; [|lia]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_switch_neq; [|lia]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_switch_neq; [|lia]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_switch_neq; [|lia]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_switch_neq; [|lia]. *) -(* apply match_assocmaps_gt; [lia|]. *) -(* apply match_assocmaps_duplicate. *) -(* apply match_assocmaps_gss. auto. *) -(* assert (r < mod_st m). *) -(* { unfold module_ordering in *. simplify. *) -(* repeat match goal with *) -(* | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H *) -(* end. *) -(* pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) -(* simplify. lia. *) -(* } lia. *) -(* } *) -(* { *) -(* apply merge_arr_empty. mgen_crush_local. *) -(* apply merge_arr_empty2. mgen_crush_local. *) -(* apply merge_arr_empty2. mgen_crush_local. *) -(* apply merge_arr_empty2. mgen_crush_local. *) -(* mgen_crush_local. *) -(* } *) -(* { auto. } *) -(* { mgen_crush_local. } *) -(* { mgen_crush_local. } *) -(* { unfold disable_ram. *) -(* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) -(* unfold merge_regs. unfold_merge. simplify. *) -(* assert (mod_st m < max_reg_module m + 1). *) -(* { unfold max_reg_module; lia. } *) -(* assert (r < max_reg_module m + 1). *) -(* { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. *) -(* unfold max_reg_stmnt in X. simplify. *) -(* lia. lia. } *) -(* repeat rewrite find_assocmap_gso by lia. *) -(* rewrite find_assocmap_gss. *) -(* repeat rewrite find_assocmap_gso by lia. *) -(* rewrite find_assocmap_gss. apply Int.eq_true. *) -(* } *) -(* } *) -(* Qed. *) Admitted. - -Lemma exec_ram_resets_en : - forall rs ar rs' ar' r, - exec_ram rs ar (Some r) rs' ar' -> - assoc_nonblocking rs = empty_assocmap -> - Int.eq ((assoc_blocking (merge_reg_assocs rs')) # (ram_en r, 32)) - ((assoc_blocking (merge_reg_assocs rs')) # (ram_u_en r, 32)) = true. -Proof. - inversion 1; intros; subst; unfold merge_reg_assocs; simplify. - - rewrite H6. mgen_crush_local. - (* - unfold merge_regs. rewrite H12. unfold_merge. *) -(* unfold find_assocmap, AssocMapExt.get_default in *. *) -(* rewrite AssocMap.gss; auto. rewrite AssocMap.gso; auto. setoid_rewrite H4. apply Int.eq_true. *) -(* pose proof (ram_ordering r); lia. *) -(* - unfold merge_regs. rewrite H11. unfold_merge. *) -(* unfold find_assocmap, AssocMapExt.get_default in *. *) -(* rewrite AssocMap.gss; auto. *) -(* repeat rewrite AssocMap.gso by (pose proof (ram_ordering r); lia). *) -(* setoid_rewrite H3. apply Int.eq_true. *) -(* Qed. *) Admitted. - -Lemma disable_ram_set_gso : - forall rs r i v, - disable_ram (Some r) rs -> - i <> (ram_en r) -> i <> (ram_u_en r) -> - disable_ram (Some r) (rs # i <- v). -Proof. - unfold disable_ram, find_assocmap, AssocMapExt.get_default; intros; - repeat rewrite AssocMap.gso by lia; auto. -Qed. -#[local] Hint Resolve disable_ram_set_gso : mgen. - -Lemma disable_ram_None rs : disable_ram None rs. -Proof. unfold disable_ram; auto. Qed. -#[local] Hint Resolve disable_ram_None : mgen. - -Lemma init_regs_equal_empty l st : - Forall (Pos.gt st) l -> (init_regs nil l) ! st = None. -Proof. induction l; simplify; apply AssocMap.gempty. Qed. - -Lemma forall_lt_num : - forall l p p', Forall (Pos.gt p) l -> p < p' -> Forall (Pos.gt p') l. -Proof. induction l; crush; inv H; constructor; [lia | eauto]. Qed. - -Section CORRECTNESS. - - Context (prog tprog: program). - Context (TRANSL: match_prog prog tprog). - - Let ge : genv := Genv.globalenv prog. - Let tge : genv := Genv.globalenv tprog. - - Lemma symbols_preserved: - forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. - Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed. - #[local] Hint Resolve symbols_preserved : mgen. - - Lemma function_ptr_translated: - forall (b: Values.block) (f: fundef), - Genv.find_funct_ptr ge b = Some f -> - exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = tf. - Proof using TRANSL. - intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. - intros (cu & tf & P & Q & R); exists tf; auto. - Qed. - #[local] Hint Resolve function_ptr_translated : mgen. - - Lemma functions_translated: - forall (v: Values.val) (f: fundef), - Genv.find_funct ge v = Some f -> - exists tf, - Genv.find_funct tge v = Some tf /\ transf_fundef f = tf. - Proof using TRANSL. - intros. exploit (Genv.find_funct_match TRANSL); eauto. - intros (cu & tf & P & Q & R); exists tf; auto. - Qed. - #[local] Hint Resolve functions_translated : mgen. - - Lemma senv_preserved: - Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). - Proof (Genv.senv_transf TRANSL). - #[local] Hint Resolve senv_preserved : mgen. - - Theorem transf_step_correct: - forall (S1 : state) t S2, - step ge S1 t S2 -> - forall R1, - match_states S1 R1 -> - exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. - Proof. - Ltac transf_step_correct_assum := - match goal with - | H: match_states _ _ |- _ => let H2 := fresh "MATCH" in learn H as H2; inv H2 - | H: mod_ram ?m = Some ?r |- _ => - let H2 := fresh "RAM" in learn H; - pose proof (transf_module_code_ram m r H) as H2 - | H: mod_ram ?m = None |- _ => - let H2 := fresh "RAM" in learn H; - pose proof (transf_module_code m H) as H2 - end. - Ltac transf_step_correct_tac := - match goal with - | |- Smallstep.plus _ _ _ _ _ => apply Smallstep.plus_one - end. - induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum; - repeat transf_step_correct_tac. - - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). - { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush_local. } - simplify. - assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). - { eapply match_arrs_size_stmnt_preserved2; mgen_crush_local. } simplify. - assert (MATCH_SIZE2: match_empty_size m nasa3 /\ match_empty_size m basa3). - { eapply match_arrs_size_ram_preserved2; mgen_crush_local. } simplify. - assert (MATCH_ARR3: match_arrs_size nasa3 basa3) by mgen_crush_local. - exploit match_states_same. apply H4. eauto with mgen. - econstructor; eauto. econstructor; eauto. econstructor; eauto. econstructor; eauto. - intros. repeat inv_exists. simplify. inv H18. inv H21. - exploit match_states_same. apply H6. eauto with mgen. - econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H18. inv H23. - exploit exec_ram_same; eauto. eauto with mgen. - econstructor. eapply match_assocmaps_merge; eauto. eauto with mgen. - econstructor. - apply match_arrs_merge; eauto with mgen. eauto with mgen. - intros. repeat inv_exists. simplify. inv H18. inv H28. - econstructor; simplify. apply Smallstep.plus_one. econstructor. - mgen_crush_local. mgen_crush_local. mgen_crush_local. rewrite RAM0; eassumption. rewrite RAM0; eassumption. - rewrite RAM0. eassumption. mgen_crush_local. eassumption. rewrite RAM0 in H21. rewrite RAM0. - rewrite RAM. eassumption. eauto. eauto. eauto with mgen. eauto. - econstructor. mgen_crush_local. apply match_arrs_merge; mgen_crush_local. eauto. - apply match_empty_size_merge; mgen_crush_local; mgen_crush_local. - assert (MATCH_SIZE1': match_empty_size m ran'0 /\ match_empty_size m rab'0). - { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush_local. } - simplify. - assert (MATCH_SIZE2': match_empty_size m ran'2 /\ match_empty_size m rab'2). - { eapply match_arrs_size_stmnt_preserved2; mgen_crush_local. } simplify. - assert (MATCH_SIZE2': match_empty_size m ran'4 /\ match_empty_size m rab'4). - { eapply match_arrs_size_ram_preserved2; mgen_crush_local. - unfold match_empty_size, transf_module, empty_stack. - repeat destruct_match; crush. mgen_crush_local. } - apply match_empty_size_merge; mgen_crush_local; mgen_crush_local. - unfold disable_ram. - unfold transf_module; repeat destruct_match; crush. - apply exec_ram_resets_en in H21. unfold merge_reg_assocs in H21. - simplify. auto. auto. - - eapply translation_correct; eauto. - - do 2 econstructor. apply Smallstep.plus_one. - apply step_finish; mgen_crush_local. constructor; eauto. - - do 2 econstructor. apply Smallstep.plus_one. - apply step_finish; mgen_crush_local. econstructor; eauto. - - econstructor. econstructor. apply Smallstep.plus_one. econstructor. - replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m) by (rewrite RAM0; auto). - replace (mod_reset (transf_module m)) with (mod_reset m) by (rewrite RAM0; auto). - replace (mod_finish (transf_module m)) with (mod_finish m) by (rewrite RAM0; auto). - replace (empty_stack (transf_module m)) with (empty_stack m) by (rewrite RAM0; auto). - replace (mod_params (transf_module m)) with (mod_params m) by (rewrite RAM0; auto). - replace (mod_st (transf_module m)) with (mod_st m) by (rewrite RAM0; auto). - repeat econstructor; mgen_crush_local. - unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (mod_params_wf m). - pose proof (mod_ram_wf m r Heqo0). - pose proof (ram_ordering r). - simplify. - repeat rewrite find_assocmap_gso by lia. - assert ((init_regs nil (mod_params m)) ! (ram_en r) = None). - { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } - assert ((init_regs nil (mod_params m)) ! (ram_u_en r) = None). - { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } - unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H14. auto. - - econstructor. econstructor. apply Smallstep.plus_one. econstructor. - replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m). - replace (mod_reset (transf_module m)) with (mod_reset m). - replace (mod_finish (transf_module m)) with (mod_finish m). - replace (empty_stack (transf_module m)) with (empty_stack m). - replace (mod_params (transf_module m)) with (mod_params m). - replace (mod_st (transf_module m)) with (mod_st m). - all: try solve [unfold transf_module; repeat destruct_match; mgen_crush_local]. - repeat econstructor; mgen_crush_local. - unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - unfold max_reg_module. - repeat rewrite find_assocmap_gso by lia. - assert (max_reg_module m + 1 > max_list (mod_params m)). - { unfold max_reg_module. lia. } - apply max_list_correct in H0. - unfold find_assocmap, AssocMapExt.get_default. - rewrite init_regs_equal_empty. rewrite init_regs_equal_empty. auto. - eapply forall_lt_num. eassumption. unfold max_reg_module. lia. - eapply forall_lt_num. eassumption. unfold max_reg_module. lia. - - inv STACKS. destruct b1; subst. - econstructor. econstructor. apply Smallstep.plus_one. - econstructor. eauto. - clear Learn. inv H0. inv H3. inv STACKS. inv H3. constructor. - constructor. intros. - rewrite RAM0. - destruct (Pos.eq_dec r res); subst. - rewrite AssocMap.gss. - rewrite AssocMap.gss. auto. - rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. - destruct (Pos.eq_dec (mod_st m) r); subst. - rewrite AssocMap.gss. - rewrite AssocMap.gss. auto. - rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H1. auto. - auto. auto. auto. auto. - rewrite RAM0. rewrite RAM. rewrite RAM0 in DISABLE_RAM. rewrite RAM in DISABLE_RAM. - apply disable_ram_set_gso. - apply disable_ram_set_gso. auto. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (ram_ordering r0). simplify. - pose proof (mod_ram_wf m r0 H). lia. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (ram_ordering r0). simplify. - pose proof (mod_ram_wf m r0 H). lia. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (ram_ordering r0). simplify. - pose proof (mod_ram_wf m r0 H). lia. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (ram_ordering r0). simplify. - pose proof (mod_ram_wf m r0 H). lia. - - inv STACKS. destruct b1; subst. - econstructor. econstructor. apply Smallstep.plus_one. - econstructor. eauto. - clear Learn. inv H0. inv H3. inv STACKS. constructor. - constructor. intros. - unfold transf_module. repeat destruct_match; crush. - destruct (Pos.eq_dec r res); subst. - rewrite AssocMap.gss. - rewrite AssocMap.gss. auto. - rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. - destruct (Pos.eq_dec (mod_st m) r); subst. - rewrite AssocMap.gss. - rewrite AssocMap.gss. auto. - rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC. apply H. auto. - auto. auto. auto. auto. - Opaque disable_ram. - unfold transf_module in *; repeat destruct_match; crush. - apply disable_ram_set_gso. - apply disable_ram_set_gso. - auto. - simplify. unfold max_reg_module. lia. - simplify. unfold max_reg_module. lia. - simplify. unfold max_reg_module. lia. - simplify. unfold max_reg_module. lia. - Qed. - #[local] Hint Resolve transf_step_correct : mgen. - - Lemma transf_initial_states : - forall s1 : state, - initial_state prog s1 -> - exists s2 : state, - initial_state tprog s2 /\ match_states s1 s2. - Proof using TRANSL. - simplify. inv H. - exploit function_ptr_translated. eauto. intros. - inv H. inv H3. - econstructor. econstructor. econstructor. - eapply (Genv.init_mem_match TRANSL); eauto. - setoid_rewrite (Linking.match_program_main TRANSL). - rewrite symbols_preserved. eauto. - eauto. - econstructor. - Qed. - #[local] Hint Resolve transf_initial_states : mgen. - - Lemma transf_final_states : - forall (s1 : state) - (s2 : state) - (r : Int.int), - match_states s1 s2 -> - final_state s1 r -> - final_state s2 r. - Proof using TRANSL. - intros. inv H0. inv H. inv STACKS. unfold valueToInt. constructor. auto. - Qed. - #[local] Hint Resolve transf_final_states : mgen. - - Theorem transf_program_correct: - Smallstep.forward_simulation (semantics prog) (semantics tprog). - Proof using TRANSL. - eapply Smallstep.forward_simulation_plus; mgen_crush_local. - apply senv_preserved. - Qed. - -End CORRECTNESS. |