diff options
Diffstat (limited to 'src/hls/DMemorygen.v')
-rw-r--r-- | src/hls/DMemorygen.v | 3308 |
1 files changed, 3308 insertions, 0 deletions
diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v new file mode 100644 index 0000000..6251162 --- /dev/null +++ b/src/hls/DMemorygen.v @@ -0,0 +1,3308 @@ +(* + * 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.DHTL. +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 opt_eqb {A} (eqb: A -> A -> bool) (a b: option A): bool := + match a, b with + | Some a', Some b' => eqb a' b' + | None, None => true + | _, _ => false + end. + +Definition unop_eqb (e1 e2: unop): bool := + match e1, e2 with + | Vneg, Vneg => true + | Vnot, Vnot => true + | _, _ => false + end. + +Definition binop_eqb (e1 e2: binop): bool := + match e1, e2 with + | Vadd, Vadd => true + | Vsub, Vsub => true + | Vmul, Vmul => true + | Vdiv, Vdiv => true + | Vdivu, Vdivu => true + | Vmod, Vmod => true + | Vmodu, Vmodu => true + | Vlt, Vlt => true + | Vltu, Vltu => true + | Vgt, Vgt => true + | Vgtu, Vgtu => true + | Vle, Vle => true + | Vleu, Vleu => true + | Vge, Vge => true + | Vgeu, Vgeu => true + | Veq, Veq => true + | Vne, Vne => true + | Vand, Vand => true + | Vor, Vor => true + | Vxor, Vxor => true + | Vshl, Vshl => true + | Vshr, Vshr => true + | Vshru, Vshru => true + | _, _ => false + end. + +Fixpoint expr_eqb (e1 e2: expr): bool := + match e1, e2 with + | Vlit v, Vlit v' => Int.eq v v' + | Vvar r, Vvar r' => Pos.eqb r r' + | Vvari r e, Vvari r' e' => Pos.eqb r r' && expr_eqb e e' + | Vrange r e1 e2, Vrange r' e1' e2' => + Pos.eqb r r' && expr_eqb e1 e1' && expr_eqb e2 e2' + | Vinputvar r, Vinputvar r' => Pos.eqb r r' + | Vbinop b e1 e2, Vbinop b' e1' e2' => + binop_eqb b b' && expr_eqb e1 e1' && expr_eqb e2 e2' + | Vunop b e1, Vunop b' e1' => + unop_eqb b b' && expr_eqb e1 e1' + | Vternary e1 e2 e3, Vternary e1' e2' e3' => + expr_eqb e1 e1' && expr_eqb e2 e2' && expr_eqb e3 e3' + | _, _ => false + end. + +Fixpoint stmnt_eqb (s1 s2: stmnt): bool := + match s1, s2 with + | Vskip, Vskip => true + | Vseq s1 s2, Vseq s1' s2' => stmnt_eqb s1 s1' && stmnt_eqb s2 s2' + | Vcond e st sf, Vcond e' st' sf' => + expr_eqb e e' + && stmnt_eqb st st' + && stmnt_eqb sf sf' + | Vcase e sl os, Vcase e' sl' os' => + expr_eqb e e' + && stmnt_expr_list_eqb sl sl' + && opt_eqb stmnt_eqb os os' + | Vblock e1 e2, Vblock e1' e2' => + expr_eqb e1 e1' && expr_eqb e2 e2' + | Vnonblock e1 e2, Vnonblock e1' e2' => + expr_eqb e1 e1' && expr_eqb e2 e2' + | _, _ => false + end +with stmnt_expr_list_eqb (s1 s2: stmnt_expr_list): bool := + match s1, s2 with + | Stmntnil, Stmntnil => true + | Stmntcons e s sl, Stmntcons e' s' sl' => + expr_eqb e e' + && stmnt_eqb s s' + && stmnt_expr_list_eqb sl sl' + | _, _ => false + end. + +Fixpoint replace_stmnt (base r b: stmnt): stmnt := + match base with + | Vskip as st | Vblock _ _ as st | Vnonblock _ _ as st => + if stmnt_eqb st r then b else st + | Vseq s1 s2 => + Vseq (replace_stmnt s1 r b) (replace_stmnt s2 r b) + | Vcond c s1 s2 => + Vcond c (replace_stmnt s1 r b) (replace_stmnt s2 r b) + | Vcase e sl (Some os) => + Vcase e (replace_stmnt_expr_list sl r b) (Some (replace_stmnt os r b)) + | Vcase e sl None => + Vcase e (replace_stmnt_expr_list sl r b) None + end +with replace_stmnt_expr_list (base: stmnt_expr_list) (r b: stmnt) := + match base with + | Stmntnil => Stmntnil + | Stmntcons e s sl => + Stmntcons e (replace_stmnt s r b) (replace_stmnt_expr_list sl r b) + end. + +Definition transf_maps state ram in_ (d: PTree.t stmnt) := + match in_ with + | (i, n) => + match PTree.get i d with + | Some (Vseq ((Vblock (Vvar _) _) as rest) (Vblock (Vvari r e1) e2)) => + if r =? (ram_mem ram) then + let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) + (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) + (Vseq (Vblock (Vvar (ram_d_in ram)) e2) + (Vblock (Vvar (ram_addr ram)) e1))) + in + PTree.set i (Vseq rest nd) d + else d + | Some (Vseq (Vblock (Vvar st') e3) (Vblock (Vvar e1) (Vvari r e2))) => + 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 (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) + (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) + (Vblock (Vvar (ram_addr ram)) e2)) + in + let aout := Vblock (Vvar e1) (Vvar (ram_d_out ram)) in + let redirect := Vblock (Vvar state) (Vlit (posToValue n)) in + (PTree.set i (Vseq redirect nd) (PTree.set n (Vseq (Vblock (Vvar st') e3) aout) d)) + else d + | _ => d + end + end. + +Lemma transf_maps_wf : + forall state ram d d' i, + map_well_formed d -> + transf_maps state ram i d = d' -> + map_well_formed d'. +Proof. + unfold transf_maps; intros; repeat destruct_match; try destruct i; + try 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 := + fold_right (transf_maps state ram) d + (zip_range (max_pc d + 1) + (map fst (PTree.elements d))). + +Lemma transf_code_wf' : + forall l d state ram d', + map_well_formed d -> + fold_right (transf_maps state ram) d l = d' -> + map_well_formed d'. +Proof. + induction l; intros; simpl in *. inv H0; auto. + remember (fold_right (transf_maps state ram) d l). (* destruct p. *) +(* apply transf_maps_wf in H0. auto. eapply IHl; eauto. *) +(* Qed. *) Admitted. + +Lemma transf_code_wf : + forall d state ram d', + map_well_formed d -> + transf_code state ram d = d' -> + 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) in + match mod_ram m with + | None => + mkmodule m.(mod_params) + 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 <- Heqt. intuition. 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. *) +Admitted. +#[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 i d_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 -> + transf_maps state ram (i, n) d = d. +Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Admitted. + +(* 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. *) + +(* 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. (* apply merge_arr_empty; mgen_crush. *) *) +(* (* 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). *) *) +(* (* 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: { 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. auto. *) *) +(* (* apply max_reg_stmnt_le_stmnt_tree in H2. *) *) +(* (* apply expr_lt_max_module_controllogic in H2. lia. *) *) +(* (* } *) *) +(* (* 3: { *) *) +(* (* simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) *) +(* (* 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. repeat rewrite AssocMapExt.merge_add_assoc. *) *) +(* (* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) *) +(* (* } *) *) +(* (* solve [auto]. *) *) +(* (* simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) *) +(* (* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) *) +(* (* simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) *) +(* (* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) *) +(* (* simplify. auto. *) *) +(* (* simplify. auto. *) *) +(* (* unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) *) +(* (* unfold_merge. *) *) +(* (* 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 transf_module; repeat destruct_match; try discriminate; simplify. *) *) +(* (* replace (AssocMapExt.merge value ran' rab') with (merge_regs ran' rab'); *) *) +(* (* [|unfold merge_regs; auto]. *) *) +(* (* pose proof H19 as X. *) *) +(* (* eapply match_assocmaps_merge in X. *) *) +(* (* 2: { apply H21. } *) *) +(* (* inv X. rewrite <- H14. eassumption. unfold transf_module in H6; repeat destruct_match; *) *) +(* (* try discriminate; simplify. *) *) +(* (* lia. auto. *) *) + +(* (* econstructor. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) *) +(* (* rewrite AssocMapExt.merge_base_1. *) *) +(* (* remember (max_reg_module m). *) *) +(* (* repeat (apply match_assocmaps_gt; [lia|]). *) *) +(* (* solve [eauto with mgen]. *) *) + +(* (* apply merge_arr_empty. apply match_empty_size_merge. *) *) +(* (* apply match_empty_assocmap_set. *) *) +(* (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) *) +(* (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) *) +(* (* apply match_arrs_merge_set2; auto. *) *) +(* (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) *) +(* (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) *) +(* (* eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. *) *) +(* (* rewrite empty_stack_transf. mgen_crush. *) *) +(* (* eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. *) *) +(* (* rewrite empty_stack_transf. mgen_crush. *) *) +(* (* auto. *) *) +(* (* apply merge_arr_empty_match. *) *) +(* (* apply match_empty_size_merge. apply match_empty_assocmap_set. *) *) +(* (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) *) +(* (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) *) +(* (* apply match_empty_size_merge. apply match_empty_assocmap_set. *) *) +(* (* mgen_crush. eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. *) *) +(* (* rewrite empty_stack_transf; mgen_crush. *) *) +(* (* unfold disable_ram. unfold transf_module; repeat destruct_match; try discriminate; simplify. *) *) +(* (* unfold merge_regs. unfold_merge. *) *) +(* (* remember (max_reg_module m). *) *) +(* (* rewrite find_assocmap_gss. *) *) +(* (* repeat rewrite find_assocmap_gso by lia. *) *) +(* (* rewrite find_assocmap_gss. apply Int.eq_true. *) *) +(* (* - 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. mgen_crush. mgen_crush. eassumption. *) *) +(* (* eassumption. econstructor. simplify. econstructor. econstructor. *) *) +(* (* solve [eauto with mgen]. econstructor. econstructor. econstructor. *) *) +(* (* econstructor. econstructor. auto. auto. auto. *) *) +(* (* econstructor. econstructor. econstructor. *) *) +(* (* econstructor. econstructor. econstructor. 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. unfold_merge. repeat rewrite find_assocmap_gso; try (remember (max_reg_module m); lia). *) *) +(* (* auto. unfold max_reg_module. lia. *) *) +(* (* } *) *) +(* (* 2: { *) *) +(* (* unfold merge_regs. unfold_merge. rewrite AssocMap.gso by lia. rewrite AssocMap.gso by lia. *) *) +(* (* rewrite AssocMap.gss. auto. *) *) +(* (* } *) *) +(* (* { unfold disable_ram, transf_module in DISABLE_RAM; *) *) +(* (* repeat destruct_match; try discriminate. simplify. apply int_eq_not. auto. } *) *) +(* (* { 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. } *) *) +(* (* { 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. *) *) +(* (* } *) *) +(* (* { 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. *) *) +(* (* apply merge_arr_empty2. mgen_crush. *) *) +(* (* apply merge_arr_empty2. mgen_crush. *) *) +(* (* apply merge_arr_empty2. mgen_crush. *) *) +(* (* mgen_crush. *) *) +(* (* } *) *) +(* (* { auto. } *) *) +(* (* { mgen_crush. } *) *) +(* (* { mgen_crush. } *) *) +(* (* { 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. *) +(* (* - 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. } *) + (* simplify. *) + (* assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). *) + (* { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. *) + (* assert (MATCH_SIZE2: match_empty_size m nasa3 /\ match_empty_size m basa3). *) + (* { eapply match_arrs_size_ram_preserved2; mgen_crush. } simplify. *) + (* assert (MATCH_ARR3: match_arrs_size nasa3 basa3) by mgen_crush. *) + (* 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. mgen_crush. mgen_crush. rewrite RAM0; eassumption. rewrite RAM0; eassumption. *) + (* rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H21. rewrite RAM0. *) + (* rewrite RAM. eassumption. eauto. eauto. eauto with mgen. eauto. *) + (* econstructor. mgen_crush. apply match_arrs_merge; mgen_crush. eauto. *) + (* apply match_empty_size_merge; mgen_crush; mgen_crush. *) + (* 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. } *) + (* simplify. *) + (* 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_SIZE2': match_empty_size m ran'4 /\ match_empty_size m rab'4). *) + (* { eapply match_arrs_size_ram_preserved2; mgen_crush. *) + (* unfold match_empty_size, transf_module, empty_stack. *) + (* repeat destruct_match; crush. mgen_crush. } *) + (* apply match_empty_size_merge; mgen_crush; mgen_crush. *) + (* 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. constructor; eauto. *) + (* - do 2 econstructor. apply Smallstep.plus_one. *) + (* apply step_finish; mgen_crush. 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. *) + (* 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]. *) + (* repeat econstructor; mgen_crush. *) + (* 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. *) + (* apply senv_preserved. *) + (* Qed. *) Admitted. + +End CORRECTNESS. |