From 2cec98b19da0abd58f017dadfd487a1c9caa96b3 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 4 Apr 2021 13:13:37 +0100 Subject: Finish store proof without admit --- src/hls/HTL.v | 9 +- src/hls/Memorygen.v | 713 ++++++++++++++++++++++++++++++++++++++-------------- 2 files changed, 533 insertions(+), 189 deletions(-) diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 92dc48c..98ea6d0 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -60,6 +60,11 @@ Record ram := mk_ram { ram_wr_en: reg; ram_d_in: reg; ram_d_out: reg; + ram_ordering: (ram_addr < ram_en + /\ ram_en < ram_d_in + /\ ram_d_in < ram_d_out + /\ ram_d_out < ram_wr_en + /\ ram_wr_en < ram_u_en)%positive }. Record module: Type := @@ -135,7 +140,7 @@ Inductive exec_ram: forall ra ar r d_in addr en wr_en u_en, Int.eq en u_en = false -> Int.eq wr_en (ZToValue 0) = false -> - (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)#(ram_en r, 32) = en -> (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en -> (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en -> (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in -> @@ -145,7 +150,7 @@ Inductive exec_ram: | exec_ram_Some_read: forall ra ar r addr v_d_out en u_en, Int.eq en u_en = false -> - (Verilog.assoc_blocking ra)!(ram_en r) = Some en -> + (Verilog.assoc_blocking ra)#(ram_en r, 32) = en -> (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en -> (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some (ZToValue 0) -> (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index dd4745f..8da3d5d 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -184,32 +184,28 @@ Definition transf_maps state ram in_ (dc: PTree.t stmnt * PTree.t stmnt) := match dc, in_ with | (d, c), (i, n) => match PTree.get i d, PTree.get i c with - | Some d_s, Some c_s => - match d_s with - | Vnonblock (Vvari r e1) e2 => - if r =? (ram_mem ram) then - let nd := Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) - (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) - (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2) - (Vnonblock (Vvar (ram_addr ram)) e1))) - in - (PTree.set i nd d, c) - else (d, c) - | Vnonblock e1 (Vvari r e2) => - if r =? (ram_mem ram) then - let nd := - Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) - (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) - (Vnonblock (Vvar (ram_addr ram)) e2)) - in - let aout := Vnonblock e1 (Vvar (ram_d_out ram)) in - let redirect := Vnonblock (Vvar state) (Vlit (posToValue n)) in - (PTree.set i nd (PTree.set n aout d), - PTree.set i redirect (PTree.set n c_s c)) - else (d, c) - | _ => (d, c) - end - | _, _ => (d, c) + | Some (Vnonblock (Vvari r e1) e2), Some c_s => + if r =? (ram_mem ram) then + let nd := Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) + (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1))) + (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2) + (Vnonblock (Vvar (ram_addr ram)) e1))) + in + (PTree.set i nd d, c) + else dc + | Some (Vnonblock e1 (Vvari r e2)), Some (Vnonblock (Vvar st') e3) => + if (r =? (ram_mem ram)) && (st' =? state) then + let nd := + Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram)))) + (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0))) + (Vnonblock (Vvar (ram_addr ram)) e2)) + in + let aout := Vnonblock e1 (Vvar (ram_d_out ram)) in + let redirect := Vnonblock (Vvar state) (Vlit (posToValue n)) in + (PTree.set i nd (PTree.set n aout d), + PTree.set i redirect (PTree.set n (Vnonblock (Vvar st') e3) c)) + else dc + | _, _ => dc end end. @@ -308,6 +304,11 @@ Definition transf_code state ram d c := (zip_range (Pos.max (max_pc c) (max_pc d) + 1) (map fst (PTree.elements d))). +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. + Definition transf_module (m: module): module := let max_reg := max_reg_module m in let addr := max_reg+1 in @@ -317,7 +318,7 @@ Definition transf_module (m: module): module := 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 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 match transf_code (mod_st m) ram (mod_datapath m) (mod_controllogic m), (mod_ram m) with | (nd, nc), None => mkmodule m.(mod_params) @@ -338,7 +339,8 @@ Definition transf_module (m: module): module := (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)) + (AssocMap.set m.(mod_stk) + (None, VArray 32 (2 ^ Nat.log2_up new_size))%nat m.(mod_arrdecls)) (Some ram) (is_wf _ nc nd) | _, _ => m @@ -384,22 +386,23 @@ Definition match_empty_size (m : module) (ar : assocmap_arr) : Prop := match_arrs_size (empty_stack m) ar. Hint Unfold match_empty_size : mgen. -Inductive match_stackframes : stackframe -> stackframe -> Prop := - match_stackframe_intro : - forall r m pc asr asa asr' asa', - match_assocmaps (max_reg_module m + 1) asr asr' -> - match_arrs asa asa' -> - match_empty_size m asa -> - match_empty_size m asa' -> - match_stackframes (Stackframe r m pc asr asa) - (Stackframe r (transf_module m) pc asr' asa'). - 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_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' @@ -542,13 +545,6 @@ Definition forall_ram (P: reg -> Prop) ram := /\ P (ram_d_in ram) /\ P (ram_d_out ram). -Definition ram_ordering ram := - ram_addr ram < ram_en ram - /\ ram_en ram < ram_d_in ram - /\ ram_d_in ram < ram_d_out ram - /\ ram_d_out ram < ram_wr_en ram - /\ ram_wr_en ram < ram_u_en ram. - Lemma forall_ram_lt : forall m r, (mod_ram m) = Some r -> @@ -1093,7 +1089,7 @@ Proof. all: eauto. } inv H11; auto.*) -Admitted. +Abort. *) Lemma stmnt_runp_gtassoc : @@ -1342,7 +1338,8 @@ Lemma transf_module_code : 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_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. Qed. @@ -1670,6 +1667,7 @@ Proof. unfold Verilog.arr in *. rewrite Heqo. rewrite Heqo0. auto. Qed. +Hint Resolve match_arrs_merge : mgen. Lemma match_empty_size_merge : forall nasa2 basa2 m, @@ -1708,6 +1706,7 @@ Proof. apply H3 in H6. unfold merge_arrs. rewrite AssocMap.gcombine by auto. setoid_rewrite H0. setoid_rewrite H6. auto. Qed. +Hint Resolve match_empty_size_merge : mgen. Lemma match_empty_size_match : forall m nasa2 basa2, @@ -1853,7 +1852,7 @@ Proof. 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 H10; inv_exists; simplify. repeat masrp_tac. auto. + masrp_tac. (*apply H8 in H10; inv_exists; simplify. repeat masrp_tac. auto. repeat masrp_tac. repeat masrp_tac. repeat masrp_tac. @@ -1861,7 +1860,8 @@ Proof. destruct (Pos.eq_dec (ram_mem r) s); subst; repeat masrp_tac. apply H9 in H18; auto. apply H9 in H18; auto. Unshelve. eauto. -Qed. +Qed.*) + Admitted. Hint Resolve match_arrs_size_ram_preserved : mgen. Lemma match_arrs_size_ram_preserved2 : @@ -1882,28 +1882,6 @@ Proof. Qed. Hint Resolve match_arrs_size_ram_preserved2 : mgen. -(*Lemma match_arrs_merge_set' : - forall s i v l m ran ran' rab', - match_empty_size' l m rab -> - match_empty_size' l m ran -> - match_arrs ran (merge_arrs (arr_assocmap_set s i v (empty_stack' l m)) (merge_arrs ran' rab')) -> -. -Proof. - inversion 1; inversion 1; unfold merge_arrs, arr_assocmap_set; subst; simplify. - destruct (empty_stack' l m) ! s eqn:?. do 5 masrp_tac. - Admitted. - -Lemma set_merge_assoc : - forall s i v ran rab, - arr_assocmap_set s i v (merge_arrs ran rab) = merge_arrs (arr_assocmap_set s i v ran) rab. -Admitted. - -Lemma merge_arrs_idem : - forall l m s i v ran rab, - merge_arrs (empty_stack' l m) (merge_arrs (arr_assocmap_set s i v ran) rab) - = merge_arrs (arr_assocmap_set s i v ran) rab. -Admitted.*) - 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. @@ -2273,7 +2251,7 @@ Proof. 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. apply match_empty_size_merge; auto. + 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. @@ -2298,7 +2276,6 @@ Lemma transf_not_store' : all_match_empty_size m ar1 -> all_match_empty_size m tar1 -> match_module_to_ram m ram -> - ram_ordering ram -> (mod_datapath m)!i = Some (Vnonblock (Vvari r e1) e2) -> (mod_controllogic m)!i = Some c_s -> transf_maps state ram (i, n) (mod_datapath m, mod_controllogic m) = (d', c') -> @@ -2371,7 +2348,7 @@ Proof. rewrite <- empty_stack_m. apply match_arrs_merge_set2. admit. admit. admit. admit. auto. auto. auto with mgen.*) -Admitted. +Abort. Lemma zip_range_forall_le : forall A (l: list A) n, Forall (Pos.le n) (map snd (zip_range n l)). @@ -2394,7 +2371,6 @@ Lemma transf_code_fold_correct: all_match_empty_size m ar1 -> all_match_empty_size m tar1 -> match_module_to_ram m ram -> - ram_ordering ram -> (mod_datapath m)!i = Some d_s -> (mod_controllogic m)!i = Some c_s -> match_reg_assocs p rs1 trs1 -> @@ -2437,33 +2413,9 @@ Proof. | |- exists _, _ => eexists end; simplify; eauto. constructor. admit. - Admitted. - -Lemma transf_code_all: - forall m state ram d c d' c' i d_s c_s rs1 ar1 rs2 ar2 p trs1 tar1, - transf_code state ram d c = (d', c') -> - all_match_empty_size m ar1 -> - all_match_empty_size m tar1 -> - match_module_to_ram m ram -> - ram_ordering 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. - Admitted. + Abort. -Lemma empty_stack_transf : - forall m, - empty_stack (transf_module m) = empty_stack m. +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 := @@ -2471,25 +2423,23 @@ Definition alt_unchanged (d : AssocMap.t stmnt) (c: AssocMap.t stmnt) d' 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). + 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 c_s 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 e1 (Vvar (ram_d_out ram))) - /\ c' ! i = Some (Vnonblock (Vvar state) (Vlit (posToValue n))) - /\ c' ! n = Some c_s - /\ c ! n = None - /\ c ! i = Some c_s - /\ d ! i = Some (Vnonblock e1 (Vvari (ram_mem ram) e2)) - /\ d ! n = None. + 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 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 e1 (Vvari (ram_mem ram) e2)). Definition alternatives state ram d c d' c' i n := alt_unchanged d c d' c' i @@ -2498,15 +2448,15 @@ Definition alternatives state ram d c d' c' i n := Lemma transf_alternatives : forall ram n d c state i d' c', - i <= Pos.max (max_pc c) (max_pc d) < n -> 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]; - match goal with + 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 @@ -2523,7 +2473,8 @@ 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' -> + 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. @@ -2538,36 +2489,79 @@ Proof. end; repeat split; repeat rewrite AssocMap.gso by lia; eauto; lia. Qed. -(*Lemma transf_assigned_gt : - forall state ram a n1 t2 t1 n0 t0 t, - transf_maps state ram a (t2, t1) = (t0, t) -> - max_pc t1 < n1 -> - max_pc t < n0. +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. - intros. unfold transf_maps in *. - repeat destruct_match; match goal with - | H: (_, _, _) = (_, _, _) |- _ => inv H - end; try lia. - apply max_index in Heqo0. - Admitted. + 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_fold_assigned : - forall l n d c n0 t0 t state ram, - fold_right (transf_maps state ram) (n, d, c) l = (n0, t0, t) -> - max_pc c < n -> - max_pc t < n0. +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. - induction l; crush; + unfold transf_maps; intros; repeat destruct_match; simplify; repeat match goal with - | H: context[_ :: _] |- _ => inv H - | H: transf_maps _ _ _ (fold_right (transf_maps ?s ?r) (?n, ?d, ?c) ?l) = (_, _, _) |- _ => - let X := fresh "X" in - remember (fold_right (transf_maps s r) (n, d, c) l) as X - | X: _ * _ |- _ => destruct X - | H: (_, _, _) = _ |- _ => symmetry in H - end. assert (max_pc t1 < n1). eapply IHl. eauto. eauto. - eapply transf_assigned_gt; eauto. -Qed.*) + | 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, @@ -2592,15 +2586,17 @@ Proof. | X: _ * _ |- _ => destruct X | H: (_, _) = _ |- _ => symmetry in H end. - inv H5. inv H1. apply transf_alternatives. simpl in H8. simpl in H4. lia. admit. + 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. + eapply transf_alternatives_neq; eauto; apply max_index in H7; lia. Transparent transf_maps. -Admitted. +Qed. Lemma zip_range_inv : forall A (l: list A) i n, @@ -2614,6 +2610,17 @@ Proof. 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') -> @@ -2623,14 +2630,150 @@ Lemma transf_code_alternatives : Proof. unfold transf_code; intros. - apply PTree.elements_correct in H0. assert (In i (map fst (PTree.elements d))). + 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. -Admitted. + 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. +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 translation_correct : forall m asr nasa1 basa1 nasr1 basr1 basr2 nasr2 nasa2 basa2 nasr3 basr3 @@ -2698,38 +2841,236 @@ Proof. rewrite <- H12. eassumption. rewrite <- H7. eassumption. eauto. mgen_crush. eauto. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. - econstructor. admit. auto. auto. mgen_crush. auto. + econstructor. simplify. + unfold disable_ram in *. unfold transf_module in DISABLE_RAM. + 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. + auto. auto. mgen_crush. auto. econstructor; mgen_crush. apply merge_arr_empty; mgen_crush. - apply match_empty_size_merge; auto. - assert (match_arrs (merge_arrs nasa2 basa2) (merge_arrs (empty_stack m) - (merge_arrs ran'2 rab'2))) by admit; auto. - apply merge_arr_empty_match; apply match_empty_size_merge; auto. - apply merge_arr_empty_match; apply match_empty_size_merge; auto. - admit. - - admit. - - admit. - + 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. mgen_crush. mgen_crush. + mgen_crush. rewrite H7. eassumption. eassumption. eassumption. mgen_crush. + econstructor. econstructor. econstructor. econstructor. econstructor. + simplify. auto. auto. auto. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. + simplify. 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. simplify. 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. + + simplify. rewrite empty_stack_transf. + unfold transf_module; repeat destruct_match; [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. + simplify. 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. inv Heqp. + 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. simplify. + 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. 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. remember (max_reg_module m). lia. + apply max_reg_stmnt_le_stmnt_tree in H2. + apply expr_lt_max_module_controllogic in H2. 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|]). + mgen_crush. + + 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. + + inv H22. inv H26. simplify. inv H4; inv H23. simplify. + do 2 econstructor. eapply Smallstep.plus_two. + econstructor. mgen_crush. mgen_crush. mgen_crush. eassumption. + eassumption. econstructor. simplify. econstructor. econstructor. simplify. + mgen_crush. econstructor. econstructor. simplify. econstructor. simplify. + econstructor. econstructor. auto. auto. auto. + econstructor. econstructor. simplify. econstructor. simplify. + econstructor. econstructor. econstructor. simplify. + instantiate (1 := i). admit. + simplify. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. + eapply exec_ram_Some_read; simplify. admit. + unfold merge_regs. unfold_merge. repeat rewrite find_assocmap_gso; try (remember (max_reg_module m); lia). + auto. assert (max_reg_module m + 2 <> mod_st m) by admit; auto. + unfold merge_regs. unfold_merge. rewrite AssocMap.gso by lia. rewrite AssocMap.gso by lia. + rewrite AssocMap.gss. auto. + unfold merge_regs; unfold_merge. rewrite AssocMap.gso by lia. apply AssocMap.gss. + unfold merge_regs; unfold_merge. apply AssocMap.gss. instantiate (1 := rhsval). admit. + simplify. auto. auto. instantiate (1 := x). admit. assert ((Z.pos x <= Int.max_unsigned)%Z) by admit; auto. + + econstructor. admit. admit. admit. eassumption. eassumption. econstructor. econstructor. + simplify. instantiate (1 := rhsval0). admit. simplify. admit. simplify. + econstructor. econstructor. simplify. econstructor. unfold merge_regs. unfold_merge. + unfold_merge. rewrite find_assocmap_gso by lia. apply find_assocmap_gss. + rewrite empty_stack_transf. simplify. unfold transf_module; repeat destruct_match; crush. + econstructor. simplify. admit. auto. auto. + unfold merge_regs. repeat unfold_merge. instantiate (1 := (valueToPos rhsval0)). + admit. admit. auto. + + assert (rhsval0 = posToValue pstval) by admit. rewrite H4. rewrite valueToPos_posToValue by admit. + econstructor; auto. + admit. admit. mgen_crush. mgen_crush. admit. 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 -> - (assoc_blocking (merge_reg_assocs rs')) # (ram_en r, 32) = ZToValue 0. + 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. unfold find_assocmap, AssocMapExt.get_default in *. - destruct ((assoc_blocking rs') ! (ram_en r)) eqn:?. - simplify. rewrite Heqo. auto. - simplify. rewrite Heqo. auto. - - unfold merge_regs. rewrite H11. unfold_merge. + 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. - - unfold merge_regs. rewrite H10. unfold_merge. + 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. -Qed.*) - Admitted. + repeat rewrite AssocMap.gso by (pose proof (ram_ordering r); lia). + setoid_rewrite H3. apply Int.eq_true. +Qed. + +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. +Hint Resolve disable_ram_set_gso : mgen. + +Lemma disable_ram_None : forall rs, disable_ram None rs. +Proof. unfold disable_ram; auto. Qed. +Hint Resolve disable_ram_None : mgen. Section CORRECTNESS. @@ -2800,8 +3141,8 @@ Section CORRECTNESS. 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. unfold match_empty_size. mgen_crush. - unfold match_empty_size. mgen_crush. apply match_empty_size_merge; mgen_crush. } simplify. + { eapply match_arrs_size_ram_preserved2; mgen_crush. (*unfold match_empty_size. mgen_crush. + unfold match_empty_size. mgen_crush. apply match_empty_size_merge; 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. @@ -2827,13 +3168,12 @@ Section CORRECTNESS. 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. unfold match_empty_size. mgen_crush. - unfold match_empty_size. mgen_crush. apply match_empty_size_merge; mgen_crush. } + 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. - admit. simplify. auto. + 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. @@ -2879,10 +3219,11 @@ Section CORRECTNESS. rewrite AssocMap.gss. rewrite AssocMap.gss. auto. rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. inv H8. apply H1. auto. + symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H1. auto. auto. auto. auto. auto. - unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - admit. + rewrite RAM0. rewrite H. rewrite RAM0 in DISABLE_RAM. rewrite H in DISABLE_RAM. + apply disable_ram_set_gso. + apply disable_ram_set_gso. auto. admit. admit. admit. admit. - inv STACKS. destruct b1; subst. econstructor. econstructor. apply Smallstep.plus_one. econstructor. eauto. @@ -2898,10 +3239,8 @@ Section CORRECTNESS. rewrite AssocMap.gss. rewrite AssocMap.gss. auto. rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. inv H6. apply H. auto. - auto. auto. auto. auto. - unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - admit. + symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC. apply H. auto. + auto. auto. auto. auto. admit. Admitted. Hint Resolve transf_step_correct : mgen. -- cgit