From 48a1381cd8466888c3034e7359b6775fafe5ed15 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 6 Oct 2022 20:10:44 +0100 Subject: [sched] Remove some unprovable lemmas --- src/common/Optionmonad.v | 3 +- src/hls/Abstr.v | 61 ++- src/hls/GiblePargen.v | 41 +- src/hls/GiblePargenproof.v | 955 ++++++--------------------------------------- src/hls/HashTree.v | 20 + 5 files changed, 179 insertions(+), 901 deletions(-) (limited to 'src') diff --git a/src/common/Optionmonad.v b/src/common/Optionmonad.v index 037dd83..8112eb9 100644 --- a/src/common/Optionmonad.v +++ b/src/common/Optionmonad.v @@ -70,8 +70,7 @@ Module Option <: Monad. End Option. Module OptionExtra. - Module OE := MonadExtra(Option). - Export OE. + Module Export OE := MonadExtra(Option). Lemma mfold_left_Some : forall A B f x n y, diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 6a7e676..07a9649 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -176,12 +176,14 @@ Definition get_forest v (f: forest) := Definition set_forest r v (f: forest) := mk_forest (RTree.set r v f.(forest_regs)) f.(forest_preds) f.(forest_exit). -Definition get_forest_p p (f: forest) := - match PTree.get p f.(forest_preds) with +Definition get_forest_p' p (f: PTree.t pred_pexpr) := + match PTree.get p f with | None => Plit (true, PEbase p) | Some v' => v' end. +Definition get_forest_p p (f: forest) := get_forest_p' p f.(forest_preds). + Definition set_forest_p p v (f: forest) := mk_forest f.(forest_regs) (PTree.set p v f.(forest_preds)) f.(forest_exit). @@ -278,6 +280,12 @@ Variant sem_exit : ctx -> exit_expression -> option cf_instr -> Prop := forall ctx, sem_exit ctx EEbase None. +(*| +``sem_pred`` is the semantics for evaluating a single predicate expression to a +boolean value, which will later be used to evaluate predicate expressions to +booleans. +|*) + Variant sem_pred : ctx -> pred_expression -> bool -> Prop := | Spred: forall ctx args c lv v, @@ -290,7 +298,11 @@ Variant sem_pred : ctx -> pred_expression -> bool -> Prop := (*| I was trying to avoid such rich semantics for pred_pexpr (by not having the type -in the first place), but I think it is needed to model predicates properly. +in the first place), but I think it is needed to model predicates properly. The +main problem is that these semantics are quite strict, and they state that one +must be able to execute the left and right hand sides of an ``Pand``, for +example, to be able to show that the ``Pand`` itself has a value. Otherwise it +is not possible to evaluate the ``Pand``. |*) Inductive sem_pexpr (c: ctx) : pred_pexpr -> bool -> Prop := @@ -308,16 +320,23 @@ Inductive sem_pexpr (c: ctx) : pred_pexpr -> bool -> Prop := sem_pexpr c p2 b2 -> sem_pexpr c (Por p1 p2) (b1 || b2). -Fixpoint from_pred_op (f: forest) (p: pred_op): pred_pexpr := +(*| +``from_pred_op`` translates a ``pred_op`` into a ``pred_pexpr``. The main +difference between the two is that ``pred_op`` contains register that predicate +registers that speak about the current state of predicates, whereas +``pred_pexpr`` have been expanded into expressions. +|*) + +Fixpoint from_pred_op (f: PTree.t pred_pexpr) (p: pred_op): pred_pexpr := match p with | Ptrue => Ptrue | Pfalse => Pfalse - | Plit (b, p') => if b then f #p p' else negate (f #p p') + | Plit (b, p') => if b then get_forest_p' p' f else negate (get_forest_p' p' f) | Pand a b => Pand (from_pred_op f a) (from_pred_op f b) | Por a b => Por (from_pred_op f a) (from_pred_op f b) end. -Inductive sem_pred_expr {A B: Type} (f: forest) (sem: ctx -> A -> B -> Prop): +Inductive sem_pred_expr {A B: Type} (f: PTree.t pred_pexpr) (sem: ctx -> A -> B -> Prop): ctx -> predicated A -> B -> Prop := | sem_pred_expr_cons_true : forall ctx e pr p' v, @@ -336,7 +355,7 @@ Inductive sem_pred_expr {A B: Type} (f: forest) (sem: ctx -> A -> B -> Prop): sem_pred_expr f sem ctx (NE.singleton (pr, e)) v . -Definition collapse_pe (p: pred_expr) : option expression := +Definition collapse_pe (p: pred_expr) : option expression := (* unused *) match p with | NE.singleton (APtrue, p) => Some p | _ => None @@ -351,16 +370,22 @@ Inductive sem_predset : ctx -> forest -> predset -> Prop := Inductive sem_regset : ctx -> forest -> regset -> Prop := | Sregset: forall ctx f rs', - (forall x, sem_pred_expr f sem_value ctx (f #r (Reg x)) (rs' !! x)) -> + (forall x, sem_pred_expr f.(forest_preds) sem_value ctx (f #r (Reg x)) (rs' !! x)) -> sem_regset ctx f rs'. +(*| +Talking about the actual generation of the forest, to make this work one has to +be able to make the assumption that ``forall i, eval (f #p i) = eval (f' #p +i)``, which should then allow for the equivalences of registers and expressions. +|*) + Inductive sem : ctx -> forest -> instr_state * option cf_instr -> Prop := | Sem: forall ctx rs' m' f pr' cf, sem_regset ctx f rs' -> sem_predset ctx f pr' -> - sem_pred_expr f sem_mem ctx (f #r Mem) m' -> - sem_pred_expr f sem_exit ctx f.(forest_exit) cf -> + sem_pred_expr f.(forest_preds) sem_mem ctx (f #r Mem) m' -> + sem_pred_expr f.(forest_preds) sem_exit ctx f.(forest_exit) cf -> sem ctx f (mk_instr_state rs' pr' m', cf). End SEMANTICS. @@ -392,6 +417,9 @@ with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := end . +Scheme expression_ind2 := Induction for expression Sort Prop + with expression_list_ind2 := Induction for expression_list Sort Prop. + Definition beq_pred_expression (e1 e2: pred_expression) : bool := match e1, e2 with | PEbase p1, PEbase p2 => if peq p1 p2 then true else false @@ -408,9 +436,6 @@ Definition beq_exit_expression (e1 e2: exit_expression) : bool := | _, _ => false end. -Scheme expression_ind2 := Induction for expression Sort Prop - with expression_list_ind2 := Induction for expression_list Sort Prop. - Lemma beq_expression_correct: forall e1 e2, beq_expression e1 e2 = true -> e1 = e2. Proof. @@ -569,8 +594,7 @@ Module HashExpr' <: MiniDecidableType. End HashExpr'. Module HashExpr := Make_UDT(HashExpr'). -Module HT := HashTree(HashExpr). -Import HT. +Module Import HT := HashTree(HashExpr). Module PHashExpr' <: MiniDecidableType. Definition t := pred_expression. @@ -688,8 +712,7 @@ Lemma match_states_trans x y z : match_states x y -> match_states y z -> match_states x z. Proof. repeat inversion 1; constructor; crush. Qed. -#[global] -Instance match_states_Equivalence : Equivalence match_states := +#[global] Instance match_states_Equivalence : Equivalence match_states := { Equivalence_Reflexive := match_states_refl ; Equivalence_Symmetric := match_states_commut ; Equivalence_Transitive := match_states_trans ; }. @@ -1455,7 +1478,7 @@ Lemma forest_pred_gso: (f #p dst <- w) #p dst' = f #p dst'. Proof. unfold "#p"; intros. - unfold forest_preds. unfold set_forest_p. + unfold forest_preds, set_forest_p, get_forest_p'. rewrite PTree.gso; auto. Qed. @@ -1464,6 +1487,6 @@ Lemma forest_pred_gss: (f #p dst <- w) #p dst = w. Proof. unfold "#p"; intros. - unfold forest_preds. unfold set_forest_p. + unfold forest_preds, set_forest_p, get_forest_p'. rewrite PTree.gss; auto. Qed. diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index af09ee6..c2ed9e3 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -182,7 +182,7 @@ Definition upd_pred_forest (p: pred_op) (f: forest): forest := f.(forest_preds) f.(forest_exit). -Fixpoint from_predicated (b: bool) (f: forest) (a: predicated pred_expression): pred_pexpr := +Fixpoint from_predicated (b: bool) (f: PTree.t pred_pexpr) (a: predicated pred_expression): pred_pexpr := match a with | NE.singleton (p, e) => Pimplies (from_pred_op f p) (Plit (b, e)) | (p, e) ::| r => @@ -190,41 +190,6 @@ Fixpoint from_predicated (b: bool) (f: forest) (a: predicated pred_expression): (from_predicated b f r) end. -(* Fixpoint get_pred' (f: forest) (ap: pred_op): option apred_op := *) -(* match ap with *) -(* | Ptrue => Some Ptrue *) -(* | Pfalse => Some Pfalse *) -(* | Plit (a, b) => *) -(* match f # (Pred b) with *) -(* | NE.singleton (Ptrue, p) => Some (Plit (a, p)) *) -(* | _ => None *) -(* end *) -(* | Pand a b => match (get_pred' f a), (get_pred' f b) with *) -(* | Some a', Some b' => Some (Pand a' b') *) -(* | _, _ => None *) -(* end *) -(* | Por a b => match (get_pred' f a), (get_pred' f b) with *) -(* | Some a', Some b' => Some (Por a' b') *) -(* | _, _ => None *) -(* end *) -(* end. *) - -(* Definition get_pred (f: forest) (ap: option pred_op): option apred_op := *) -(* get_pred' f (Option.default T ap). *) - -(* Fixpoint get_pred' (f: forest) (ap: pred_op): apred_op := *) -(* match ap with *) -(* | Ptrue => Ptrue *) -(* | Pfalse => Pfalse *) -(* | Plit (a, b) => *) -(* apredicated_to_apred_op a (f # (Pred b)) *) -(* | Pand a b => Pand (get_pred' f a) (get_pred' f b) *) -(* | Por a b => Por (get_pred' f a) (get_pred' f b) *) -(* end. *) - -(* Definition get_pred (f: forest) (ap: option pred_op): apred_op := *) -(* get_pred' f (Option.default Ptrue ap). *) - #[local] Open Scope monad_scope. Definition simpl_combine {A: Type} (a b: option (@Predicate.pred_op A)) := @@ -275,8 +240,8 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest Some (pred, f #r Mem <- pruned) | RBsetpred p' c args p => let new_pred := - (from_pred_op f (dfltp p' ∧ pred) - → from_predicated true f (map_predicated (pred_ret (PEsetpred c)) + (from_pred_op f.(forest_preds) (dfltp p' ∧ pred) + → from_predicated true f.(forest_preds) (map_predicated (pred_ret (PEsetpred c)) (merge (list_translation args f)))) in do _ <- is_initial_pred f p; diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index bcc3fd0..05467ed 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -41,6 +41,9 @@ Import OptionExtra. #[local] Open Scope forest. #[local] Open Scope pred_op. +#[local] Opaque simplify. +#[local] Opaque deep_simplify. + (*| ============== RTLPargenproof @@ -110,457 +113,6 @@ Proof. induction l; crush. Qed. Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}. Proof. destruct (check_dest_l i r); tauto. Qed. -(* Lemma check_dest_update : *) -(* forall f f' i r, *) -(* check_dest i r = false -> *) -(* update (Some f) i = Some f' -> *) -(* (snd f') # (Reg r) = (snd f) # (Reg r). *) -(* Proof. *) -(* destruct i; crush; try apply Pos.eqb_neq in H; unfold update; destruct_match; crush. *) -(* inv Heqp. *) -(* Admitted. *) - -(* Lemma check_dest_l_forall2 : *) -(* forall l r, *) -(* Forall (fun x => check_dest x r = false) l -> *) -(* check_dest_l l r = false. *) -(* Proof. *) -(* induction l; crush. *) -(* inv H. apply orb_false_intro; crush. *) -(* Qed. *) - -(* Lemma check_dest_l_ex2 : *) -(* forall l r, *) -(* (exists a, In a l /\ check_dest a r = true) -> *) -(* check_dest_l l r = true. *) -(* Proof. *) -(* induction l; crush. *) -(* specialize (IHl r). inv H. *) -(* apply orb_true_intro; crush. *) -(* apply orb_true_intro; crush. *) -(* right. apply IHl. exists x. auto. *) -(* Qed. *) - -(* Lemma check_list_l_false : *) -(* forall l x r, *) -(* check_dest_l (l ++ x :: nil) r = false -> *) -(* check_dest_l l r = false /\ check_dest x r = false. *) -(* Proof. *) -(* simplify. *) -(* apply check_dest_l_forall in H. apply Forall_app in H. *) -(* simplify. apply check_dest_l_forall2; auto. *) -(* apply check_dest_l_forall in H. apply Forall_app in H. *) -(* simplify. inv H1. auto. *) -(* Qed. *) - -(* Lemma check_dest_l_ex : *) -(* forall l r, *) -(* check_dest_l l r = true -> *) -(* exists a, In a l /\ check_dest a r = true. *) -(* Proof. *) -(* induction l; crush. *) -(* destruct (check_dest a r) eqn:?; try solve [econstructor; crush]. *) -(* simplify. *) -(* exploit IHl. apply H. simplify. econstructor. simplify. right. eassumption. *) -(* auto. *) -(* Qed. *) - -(* Lemma check_list_l_true : *) -(* forall l x r, *) -(* check_dest_l (l ++ x :: nil) r = true -> *) -(* check_dest_l l r = true \/ check_dest x r = true. *) -(* Proof. *) -(* simplify. *) -(* apply check_dest_l_ex in H; simplify. *) -(* apply in_app_or in H. inv H. left. *) -(* apply check_dest_l_ex2. exists x0. auto. *) -(* inv H0; auto. *) -(* Qed. *) - -(* Lemma check_dest_l_dec2 l r : *) -(* {Forall (fun x => check_dest x r = false) l} *) -(* + {exists a, In a l /\ check_dest a r = true}. *) -(* Proof. *) -(* destruct (check_dest_l_dec l r); [right | left]; *) -(* auto using check_dest_l_ex, check_dest_l_forall. *) -(* Qed. *) - -(* Lemma abstr_comp : *) -(* forall l i f x x0, *) -(* fold_left update (l ++ i :: nil) f = x -> *) -(* fold_left update l f = x0 -> *) -(* x = update x0 i. *) -(* Proof. induction l; intros; crush; eapply IHl; eauto. Qed. *) - -(* - -Lemma gen_list_base: - forall FF ge sp l rs exps st1, - (forall x, @sem_value FF ge sp st1 (exps # (Reg x)) (rs !! x)) -> - sem_val_list ge sp st1 (list_translation l exps) rs ## l. -Proof. - induction l. - intros. simpl. constructor. - intros. simpl. eapply Scons; eauto. -Qed. - -Lemma check_dest_update2 : - forall f r rl op p, - (update f (RBop p op rl r)) # (Reg r) = Eop op (list_translation rl f) (f # Mem). -Proof. crush; rewrite map2; auto. Qed. - -Lemma check_dest_update3 : - forall f r rl p addr chunk, - (update f (RBload p chunk addr rl r)) # (Reg r) = Eload chunk addr (list_translation rl f) (f # Mem). -Proof. crush; rewrite map2; auto. Qed. - -Lemma abstract_seq_correct_aux: - forall FF ge sp i st1 st2 st3 f, - @step_instr FF ge sp st3 i st2 -> - sem ge sp st1 f st3 -> - sem ge sp st1 (update f i) st2. -Proof. - intros; inv H; simplify. - { simplify; eauto. } (*apply match_states_refl. }*) - { inv H0. inv H6. destruct st1. econstructor. simplify. - constructor. intros. - destruct (resource_eq (Reg res) (Reg x)). inv e. - rewrite map2. econstructor. eassumption. apply gen_list_base; eauto. - rewrite Regmap.gss. eauto. - assert (res <> x). { unfold not in *. intros. apply n. rewrite H0. auto. } - rewrite Regmap.gso by auto. - rewrite genmap1 by auto. auto. - - rewrite genmap1; crush. } - { inv H0. inv H7. constructor. constructor. intros. - destruct (Pos.eq_dec dst x); subst. - rewrite map2. econstructor; eauto. - apply gen_list_base. auto. rewrite Regmap.gss. auto. - rewrite genmap1. rewrite Regmap.gso by auto. auto. - unfold not in *; intros. inv H0. auto. - rewrite genmap1; crush. - } - { inv H0. inv H7. constructor. constructor; intros. - rewrite genmap1; crush. - rewrite map2. econstructor; eauto. - apply gen_list_base; auto. - } -Qed. - -Lemma regmap_list_equiv : - forall A (rs1: Regmap.t A) rs2, - (forall x, rs1 !! x = rs2 !! x) -> - forall rl, rs1##rl = rs2##rl. -Proof. induction rl; crush. Qed. - -Lemma sem_update_Op : - forall A ge sp st f st' r l o0 o m rs v, - @sem A ge sp st f st' -> - Op.eval_operation ge sp o0 rs ## l m = Some v -> - match_states st' (mk_instr_state rs m) -> - exists tst, - sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m) tst. -Proof. - intros. inv H1. simplify. - destruct st. - econstructor. simplify. - { constructor. - { constructor. intros. destruct (Pos.eq_dec x r); subst. - { pose proof (H5 r). rewrite map2. pose proof H. inv H. econstructor; eauto. - { inv H9. eapply gen_list_base; eauto. } - { instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. erewrite regmap_list_equiv; eauto. } } - { rewrite Regmap.gso by auto. rewrite genmap1; crush. inv H. inv H7; eauto. } } - { inv H. rewrite genmap1; crush. eauto. } } - { constructor; eauto. intros. - destruct (Pos.eq_dec r x); - subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. } -Qed. - -Lemma sem_update_load : - forall A ge sp st f st' r o m a l m0 rs v a0, - @sem A ge sp st f st' -> - Op.eval_addressing ge sp a rs ## l = Some a0 -> - Mem.loadv m m0 a0 = Some v -> - match_states st' (mk_instr_state rs m0) -> - exists tst : instr_state, - sem ge sp st (update f (RBload o m a l r)) tst - /\ match_states (mk_instr_state (Regmap.set r v rs) m0) tst. -Proof. - intros. inv H2. pose proof H. inv H. inv H9. - destruct st. - econstructor; simplify. - { constructor. - { constructor. intros. - destruct (Pos.eq_dec x r); subst. - { rewrite map2. econstructor; eauto. eapply gen_list_base. intros. - rewrite <- H6. eauto. - instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. auto. } - { rewrite Regmap.gso by auto. rewrite genmap1; crush. } } - { rewrite genmap1; crush. eauto. } } - { constructor; auto; intros. destruct (Pos.eq_dec r x); - subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. } -Qed. - -Lemma sem_update_store : - forall A ge sp a0 m a l r o f st m' rs m0 st', - @sem A ge sp st f st' -> - Op.eval_addressing ge sp a rs ## l = Some a0 -> - Mem.storev m m0 a0 rs !! r = Some m' -> - match_states st' (mk_instr_state rs m0) -> - exists tst, sem ge sp st (update f (RBstore o m a l r)) tst - /\ match_states (mk_instr_state rs m') tst. -Proof. - intros. inv H2. pose proof H. inv H. inv H9. - destruct st. - econstructor; simplify. - { econstructor. - { econstructor; intros. rewrite genmap1; crush. } - { rewrite map2. econstructor; eauto. eapply gen_list_base. intros. rewrite <- H6. - eauto. specialize (H6 r). rewrite H6. eauto. } } - { econstructor; eauto. } -Qed. - -Lemma sem_update : - forall A ge sp st x st' st'' st''' f, - sem ge sp st f st' -> - match_states st' st''' -> - @step_instr A ge sp st''' x st'' -> - exists tst, sem ge sp st (update f x) tst /\ match_states st'' tst. -Proof. - intros. destruct x; inv H1. - { econstructor. split. - apply sem_update_RBnop. eassumption. - apply match_states_commut. auto. } - { eapply sem_update_Op; eauto. } - { eapply sem_update_load; eauto. } - { eapply sem_update_store; eauto. } -Qed. - -Lemma sem_update2_Op : - forall A ge sp st f r l o0 o m rs v, - @sem A ge sp st f (mk_instr_state rs m) -> - Op.eval_operation ge sp o0 rs ## l m = Some v -> - sem ge sp st (update f (RBop o o0 l r)) (mk_instr_state (Regmap.set r v rs) m). -Proof. - intros. destruct st. constructor. - inv H. inv H6. - { constructor; intros. simplify. - destruct (Pos.eq_dec r x); subst. - { rewrite map2. econstructor. eauto. - apply gen_list_base. eauto. - rewrite Regmap.gss. auto. } - { rewrite genmap1; crush. rewrite Regmap.gso; auto. } } - { simplify. rewrite genmap1; crush. inv H. eauto. } -Qed. - -Lemma sem_update2_load : - forall A ge sp st f r o m a l m0 rs v a0, - @sem A ge sp st f (mk_instr_state rs m0) -> - Op.eval_addressing ge sp a rs ## l = Some a0 -> - Mem.loadv m m0 a0 = Some v -> - sem ge sp st (update f (RBload o m a l r)) (mk_instr_state (Regmap.set r v rs) m0). -Proof. - intros. simplify. inv H. inv H7. constructor. - { constructor; intros. destruct (Pos.eq_dec r x); subst. - { rewrite map2. rewrite Regmap.gss. econstructor; eauto. - apply gen_list_base; eauto. } - { rewrite genmap1; crush. rewrite Regmap.gso; eauto. } - } - { simplify. rewrite genmap1; crush. } -Qed. - -Lemma sem_update2_store : - forall A ge sp a0 m a l r o f st m' rs m0, - @sem A ge sp st f (mk_instr_state rs m0) -> - Op.eval_addressing ge sp a rs ## l = Some a0 -> - Mem.storev m m0 a0 rs !! r = Some m' -> - sem ge sp st (update f (RBstore o m a l r)) (mk_instr_state rs m'). -Proof. - intros. simplify. inv H. inv H7. constructor; simplify. - { econstructor; intros. rewrite genmap1; crush. } - { rewrite map2. econstructor; eauto. apply gen_list_base; eauto. } -Qed. - -Lemma sem_update2 : - forall A ge sp st x st' st'' f, - sem ge sp st f st' -> - @step_instr A ge sp st' x st'' -> - sem ge sp st (update f x) st''. -Proof. - intros. - destruct x; inv H0; - eauto using sem_update_RBnop, sem_update2_Op, sem_update2_load, sem_update2_store. -Qed. - -Lemma abstr_sem_val_mem : - forall A B ge tge st tst sp a, - ge_preserved ge tge -> - forall v m, - (@sem_mem A ge sp st a m /\ match_states st tst -> @sem_mem B tge sp tst a m) /\ - (@sem_value A ge sp st a v /\ match_states st tst -> @sem_value B tge sp tst a v). -Proof. - intros * H. - apply expression_ind2 with - - (P := fun (e1: expression) => - forall v m, - (@sem_mem A ge sp st e1 m /\ match_states st tst -> @sem_mem B tge sp tst e1 m) /\ - (@sem_value A ge sp st e1 v /\ match_states st tst -> @sem_value B tge sp tst e1 v)) - - (P0 := fun (e1: expression_list) => - forall lv, @sem_val_list A ge sp st e1 lv /\ match_states st tst -> @sem_val_list B tge sp tst e1 lv); - simplify; intros; simplify. - { inv H1. inv H2. constructor. } - { inv H2. inv H1. rewrite H0. constructor. } - { inv H3. } - { inv H3. inv H4. econstructor. apply H1; auto. simplify. eauto. constructor. auto. auto. - apply H0; simplify; eauto. constructor; eauto. - unfold ge_preserved in *. simplify. rewrite <- H2. auto. - } - { inv H3. } - { inv H3. inv H4. econstructor. apply H1; eauto; simplify; eauto. constructor; eauto. - apply H0; simplify; eauto. constructor; eauto. - inv H. rewrite <- H4. eauto. - auto. - } - { inv H4. inv H5. econstructor. apply H0; eauto. simplify; eauto. constructor; eauto. - apply H2; eauto. simplify; eauto. constructor; eauto. - apply H1; eauto. simplify; eauto. constructor; eauto. - inv H. rewrite <- H5. eauto. auto. - } - { inv H4. } - { inv H1. constructor. } - { inv H3. constructor; auto. apply H0; eauto. apply Mem.empty. } -Qed. - -Lemma abstr_sem_value : - forall a A B ge tge sp st tst v, - @sem_value A ge sp st a v -> - ge_preserved ge tge -> - match_states st tst -> - @sem_value B tge sp tst a v. -Proof. intros; eapply abstr_sem_val_mem; eauto; apply Mem.empty. Qed. - -Lemma abstr_sem_mem : - forall a A B ge tge sp st tst v, - @sem_mem A ge sp st a v -> - ge_preserved ge tge -> - match_states st tst -> - @sem_mem B tge sp tst a v. -Proof. intros; eapply abstr_sem_val_mem; eauto. Qed. - -Lemma abstr_sem_regset : - forall a a' A B ge tge sp st tst rs, - @sem_regset A ge sp st a rs -> - ge_preserved ge tge -> - (forall x, a # x = a' # x) -> - match_states st tst -> - exists rs', @sem_regset B tge sp tst a' rs' /\ (forall x, rs !! x = rs' !! x). -Proof. - inversion 1; intros. - inv H7. - econstructor. simplify. econstructor. intros. - eapply abstr_sem_value; eauto. rewrite <- H6. - eapply H0. constructor; eauto. - auto. -Qed. - -Lemma abstr_sem : - forall a a' A B ge tge sp st tst st', - @sem A ge sp st a st' -> - ge_preserved ge tge -> - (forall x, a # x = a' # x) -> - match_states st tst -> - exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'. -Proof. - inversion 1; subst; intros. - inversion H4; subst. - exploit abstr_sem_regset; eauto; inv_simp. - do 3 econstructor; eauto. - rewrite <- H3. - eapply abstr_sem_mem; eauto. -Qed. - -Lemma abstract_execution_correct': - forall A B ge tge sp st' a a' st tst, - @sem A ge sp st a st' -> - ge_preserved ge tge -> - check a a' = true -> - match_states st tst -> - exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'. -Proof. - intros; - pose proof (check_correct a a' H1); - eapply abstr_sem; eauto. -Qed. - -Lemma states_match : - forall st1 st2 st3 st4, - match_states st1 st2 -> - match_states st2 st3 -> - match_states st3 st4 -> - match_states st1 st4. -Proof. - intros * H1 H2 H3; destruct st1; destruct st2; destruct st3; destruct st4. - inv H1. inv H2. inv H3; constructor. - unfold regs_lessdef in *. intros. - repeat match goal with - | H: forall _, _, r : positive |- _ => specialize (H r) - end. - congruence. - auto. -Qed. - -Lemma step_instr_block_same : - forall ge sp st st', - step_instr_block ge sp st nil st' -> - st = st'. -Proof. inversion 1; auto. Qed. - -Lemma step_instr_seq_same : - forall ge sp st st', - step_instr_seq ge sp st nil st' -> - st = st'. -Proof. inversion 1; auto. Qed. - -Lemma sem_update' : - forall A ge sp st a x st', - sem ge sp st (update (abstract_sequence empty a) x) st' -> - exists st'', - @step_instr A ge sp st'' x st' /\ - sem ge sp st (abstract_sequence empty a) st''. -Proof. - Admitted. - -Lemma rtlpar_trans_correct : - forall bb ge sp sem_st' sem_st st, - sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> - match_states sem_st st -> - exists st', RTLPar.step_instr_block ge sp st bb st' - /\ match_states sem_st' st'. -Proof. - induction bb using rev_ind. - { repeat econstructor. eapply abstract_interp_empty3 in H. - inv H. inv H0. constructor; congruence. } - { simplify. inv H0. repeat rewrite concat_app in H. simplify. - rewrite app_nil_r in H. - exploit sem_separate; eauto; inv_simp. - repeat econstructor. admit. admit. - } -Admitted. - -(*Lemma abstract_execution_correct_ld: - forall bb bb' cfi ge tge sp st st' tst, - RTLBlock.step_instr_list ge sp st bb st' -> - ge_preserved ge tge -> - schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> - match_states_ld st tst -> - exists tst', RTLPar.step_instr_block tge sp tst bb' tst' - /\ match_states st' tst'. -Proof. - intros.*) -*) - Lemma match_states_list : forall A (rs: Regmap.t A) rs', (forall r, rs !! r = rs' !! r) -> @@ -577,245 +129,6 @@ Proof. | repeat rewrite Regmap.gso by auto ]; auto. Qed. -(*Lemma abstract_interp_empty3 : - forall A ctx st', - @sem A ctx empty st' -> match_states (ctx_is ctx) st'. -Proof. - inversion 1; subst; simplify. destruct ctx. - destruct ctx_is. - constructor; intros. - - inv H0. specialize (H3 x). inv H3. inv H8. reflexivity. - - inv H1. specialize (H3 x). inv H3. inv H8. reflexivity. - - inv H2. inv H8. reflexivity. -Qed. - -Lemma step_instr_matches : - forall A a ge sp st st', - @step_instr A ge sp st a st' -> - forall tst, - match_states st tst -> - exists tst', step_instr ge sp tst a tst' - /\ match_states st' tst'. -Proof. - induction 1; simplify; - match goal with H: match_states _ _ |- _ => inv H end; - try solve [repeat econstructor; try erewrite match_states_list; - try apply PTree_matches; eauto; - match goal with - H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto - end]. - - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end. - repeat econstructor; try erewrite match_states_list; eauto. - erewrite <- eval_predf_pr_equiv; eassumption. - apply PTree_matches; assumption. - repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto. - erewrite <- eval_predf_pr_equiv; eassumption. - econstructor; auto. - match goal with H: eval_pred _ _ _ _ |- _ => inv H end. - repeat econstructor; try erewrite match_states_list; eauto. - (*- destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end. - repeat econstructor; try erewrite match_states_list; eauto. - erewrite <- eval_predf_pr_equiv; eassumption. - apply PTree_matches; assumption. - repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto. - erewrite <- eval_predf_pr_equiv; eassumption. - econstructor; auto. - match goal with H: eval_pred _ _ _ _ |- _ => inv H end. - repeat econstructor; try erewrite match_states_list; eauto. - - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end. - repeat econstructor; try erewrite match_states_list; eauto. - match goal with - H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto - end. - erewrite <- eval_predf_pr_equiv; eassumption. - repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto. - match goal with - H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto - end. - erewrite <- eval_predf_pr_equiv; eassumption. - match goal with H: eval_pred _ _ _ _ |- _ => inv H end. - repeat econstructor; try erewrite match_states_list; eauto. - match goal with - H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto - end. - - admit.*) Admitted. - -Lemma step_instr_list_matches : - forall a ge sp st st', - step_instr_list ge sp st a st' -> - forall tst, match_states st tst -> - exists tst', step_instr_list ge sp tst a tst' - /\ match_states st' tst'. -Proof. - induction a; intros; inv H; - try (exploit step_instr_matches; eauto; []; simplify; - exploit IHa; eauto; []; simplify); repeat econstructor; eauto. -Qed. - -Lemma step_instr_seq_matches : - forall a ge sp st st', - step_instr_seq ge sp st a st' -> - forall tst, match_states st tst -> - exists tst', step_instr_seq ge sp tst a tst' - /\ match_states st' tst'. -Proof. - induction a; intros; inv H; - try (exploit step_instr_list_matches; eauto; []; simplify; - exploit IHa; eauto; []; simplify); repeat econstructor; eauto. -Qed. - -Lemma step_instr_block_matches : - forall bb ge sp st st', - step_instr_block ge sp st bb st' -> - forall tst, match_states st tst -> - exists tst', step_instr_block ge sp tst bb tst' - /\ match_states st' tst'. -Proof. - induction bb; intros; inv H; - try (exploit step_instr_seq_matches; eauto; []; simplify; - exploit IHbb; eauto; []; simplify); repeat econstructor; eauto. -Qed. - -Lemma rtlblock_trans_correct' : - forall bb ge sp st x st'', - RTLBlock.step_instr_list ge sp st (bb ++ x :: nil) st'' -> - exists st', RTLBlock.step_instr_list ge sp st bb st' - /\ step_instr ge sp st' x st''. -Proof. - induction bb. - crush. exists st. - split. constructor. inv H. inv H6. auto. - crush. inv H. exploit IHbb. eassumption. simplify. - econstructor. split. - econstructor; eauto. eauto. -Qed. - -Lemma abstract_interp_empty A st : @sem A st empty (ctx_is st). -Proof. destruct st, ctx_is. simpl. repeat econstructor. Qed. - -Lemma abstract_seq : - forall l f i, - abstract_sequence f (l ++ i :: nil) = update (abstract_sequence f l) i. -Proof. induction l; crush. Qed. - -Lemma abstract_sequence_update : - forall l r f, - check_dest_l l r = false -> - (abstract_sequence f l) # (Reg r) = f # (Reg r). -Proof. - induction l using rev_ind; crush. - rewrite abstract_seq. rewrite check_dest_update. apply IHl. - apply check_list_l_false in H. tauto. - apply check_list_l_false in H. tauto. -Qed. - -(*Lemma sem_separate : - forall A ctx b a st', - sem ctx (abstract_sequence empty (a ++ b)) st' -> - exists st'', - @sem A ctx (abstract_sequence empty a) st'' - /\ @sem A (mk_ctx st'' (ctx_sp ctx) (ctx_ge ctx)) (abstract_sequence empty b) st'. -Proof. - induction b using rev_ind; simplify. - { econstructor. simplify. rewrite app_nil_r in H. eauto. apply abstract_interp_empty. } - { simplify. rewrite app_assoc in H. rewrite abstract_seq in H. - exploit sem_update'; eauto; simplify. - exploit IHb; eauto; inv_simp. - econstructor; split; eauto. - rewrite abstract_seq. - eapply sem_update2; eauto. - } -Qed.*) - -Lemma sem_update_RBnop : - forall A ctx f st', - @sem A ctx f st' -> sem ctx (update f RBnop) st'. -Proof. auto. Qed. - -Lemma sem_update_Op : - forall A ge sp ist f st' r l o0 o m rs v ps, - @sem A (mk_ctx ist sp ge) f st' -> - eval_predf ps o = true -> - Op.eval_operation ge sp o0 (rs ## l) m = Some v -> - match_states st' (mk_instr_state rs ps m) -> - exists tst, - sem (mk_ctx ist sp ge) (update f (RBop (Some o) o0 l r)) tst - /\ match_states (mk_instr_state (Regmap.set r v rs) ps m) tst. -Proof. - intros. inv H1. inv H. inv H1. inv H3. simplify. - econstructor. simplify. - { constructor; try constructor; intros; try solve [rewrite genmap1; now eauto]. - destruct (Pos.eq_dec x r); subst. - { rewrite map2. specialize (H1 r). inv H1. -(*} - } - destruct st. - econstructor. simplify. - { constructor. - { constructor. intros. destruct (Pos.eq_dec x r); subst. - { pose proof (H5 r). rewrite map2. pose proof H. inv H. econstructor; eauto. - { inv H9. eapply gen_list_base; eauto. } - { instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. erewrite regmap_list_equiv; eauto. } } - { rewrite Regmap.gso by auto. rewrite genmap1; crush. inv H. inv H7; eauto. } } - { inv H. rewrite genmap1; crush. eauto. } } - { constructor; eauto. intros. - destruct (Pos.eq_dec r x); - subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. } -Qed.*) Admitted. - -Lemma sem_update : - forall A ge sp st x st' st'' st''' f, - sem (mk_ctx st sp ge) f st' -> - match_states st' st''' -> - @step_instr A ge sp st''' x st'' -> - exists tst, sem (mk_ctx st sp ge) (update f x) tst /\ match_states st'' tst. -Proof. - intros. destruct x. - - inv H1. econstructor. simplify. eauto. symmetry; auto. - - inv H1. inv H0. econstructor. - Admitted. - -Lemma rtlblock_trans_correct : - forall bb ge sp st st', - RTLBlock.step_instr_list ge sp st bb st' -> - forall tst, - match_states st tst -> - exists tst', sem (mk_ctx tst sp ge) (abstract_sequence empty bb) tst' - /\ match_states st' tst'. -Proof. - induction bb using rev_ind; simplify. - { econstructor. simplify. apply abstract_interp_empty. - inv H. auto. } - { apply rtlblock_trans_correct' in H. simplify. - rewrite abstract_seq. - exploit IHbb; try eassumption; []; simplify. - exploit sem_update. apply H1. symmetry; eassumption. - eauto. simplify. econstructor. split. apply H3. - auto. } -Qed. - -Lemma abstract_execution_correct: - forall bb bb' cfi cfi' ge tge sp st st' tst, - RTLBlock.step_instr_list ge sp st bb st' -> - ge_preserved ge tge -> - schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi') = true -> - match_states st tst -> - exists tst', RTLPar.step_instr_block tge sp tst bb' tst' - /\ match_states st' tst'. -Proof. - intros. - unfold schedule_oracle in *. simplify. unfold empty_trees in H4. - exploit rtlblock_trans_correct; try eassumption; []; simplify. -(*) exploit abstract_execution_correct'; - try solve [eassumption | apply state_lessdef_match_sem; eassumption]. - apply match_states_commut. eauto. inv_simp. - exploit rtlpar_trans_correct; try eassumption; []; inv_simp. - exploit step_instr_block_matches; eauto. apply match_states_commut; eauto. inv_simp. - repeat match goal with | H: match_states _ _ |- _ => inv H end. - do 2 econstructor; eauto. - econstructor; congruence. -Qed.*)Admitted.*) - Definition match_prog (prog : GibleSeq.program) (tprog : GiblePar.program) := match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. @@ -1168,23 +481,45 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. sem (mk_ctx i sp ge) f' (i'', None). Proof. Admitted. + Lemma truthy_dflt : + forall ps p, + truthy ps p -> eval_predf ps (dfltp p) = true. + Proof. intros. destruct p; cbn; inv H; auto. Qed. + + Lemma Pand_true_left : + forall ps a b, + eval_predf ps a = false -> + eval_predf ps (a ∧ b) = false. + Proof. + intros. + rewrite eval_predf_Pand. now rewrite H. + Qed. + + Lemma eval_predf_simplify : + forall ps x, + eval_predf ps (simplify x) = eval_predf ps x. + Proof. Admitted. Lemma sem_update_instr_term : - forall f i' i'' a sp i cf p p' p'' f', + forall f i' i'' sp i cf p p' p'' f', sem (mk_ctx i sp ge) f (i', None) -> step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) -> - update (p', f) a = Some (p'', f') -> + update (p', f) (RBexit p cf) = Some (p'', f') -> + eval_predf (is_ps i') p' = true -> sem (mk_ctx i sp ge) f' (i'', Some cf) - /\ eval_predf (is_ps i) p'' = false. + /\ eval_predf (is_ps i') p'' = false. Proof. - Admitted. - - (* Lemma step_instr_lessdef : *) - (* forall sp a i i' ti, *) - (* step_instr ge sp (Iexec i) a (Iexec i') -> *) - (* state_lessdef i ti -> *) - (* exists ti', step_instr ge sp (Iexec ti) a (Iexec ti') /\ state_lessdef i' ti'. *) - (* Proof. Admitted. *) + intros. inv H0. simpl in *. + unfold Option.bind in *. destruct_match; try discriminate. + apply truthy_dflt in H6. inv H1. + assert (eval_predf (Gible.is_ps i'') (¬ dfltp p) = false). + { rewrite eval_predf_negate. now rewrite negb_false_iff. } + apply Pand_true_left with (b := p') in H0. + rewrite <- eval_predf_simplify in H0. split; auto. + unfold "<-e". + destruct i''. + inv H. constructor; auto. admit. admit. simplify. + Admitted. Lemma step_instr_lessdef_term : forall sp a i i' ti cf, @@ -1193,36 +528,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. Admitted. -(* Lemma app_predicated_semregset : - forall A ctx o f res r y, - @sem_regset A ctx f res -> - falsy (ctx_ps ctx) o -> - @sem_regset A ctx f # r <- (app_predicated o f#r y) res. - Proof. - inversion 1; subst; crush. - constructor; intros. - destruct (resource_eq r (Reg x)); subst. - + rewrite map2; eauto. unfold app_predicated. inv H1. admit. - + rewrite genmap1; auto. - Admitted. - - Lemma app_predicated_sempredset : - forall A ctx o f rs r y ps, - @sem_predset A ctx f rs -> - falsy ps o -> - @sem_predset A ctx f # r <- (app_predicated o f#r y) rs. - Proof. Admitted. - - Lemma app_predicated_sem : - forall A ctx o f i cf r y, - @sem A ctx f (i, cf) -> - falsy (is_ps i) o -> - @sem A ctx f # r <- (app_predicated o f#r y) (i, cf). - Proof. - inversion 1; subst; crush. - constructor. - Admitted.*) - Lemma combined_falsy : forall i o1 o, falsy i o1 -> @@ -1233,99 +538,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. constructor. auto. Qed. - (* Inductive is_predicate_expr: expression -> Prop := *) - (* | is_predicate_expr_Epredset : *) - (* forall c a, is_predicate_expr (Esetpred c a) *) - (* | is_predicate_expr_Ebase : *) - (* forall p, is_predicate_expr (Ebase (Pred p)). *) - - (* Inductive apred_wf: apred_op -> Prop := *) - (* | apred_wf_Plit: forall b p, *) - (* is_predicate_expr p -> *) - (* apred_wf (Plit (b, p)) *) - (* | apred_wf_Ptrue: apred_wf Ptrue *) - (* | apred_wf_Pfalse: apred_wf Pfalse *) - (* | apred_wf_Pand: forall a b, *) - (* apred_wf a -> apred_wf b -> apred_wf (a ∧ b) *) - (* | apred_wf_Por: forall a b, *) - (* apred_wf a -> apred_wf b -> apred_wf (a ∨ b). *) - - (* Lemma apred_and_false1 : *) - (* forall A ctx a b c, *) - (* @eval_apred A ctx a false -> *) - (* @eval_apred A ctx b c -> *) - (* eval_apred ctx (a ∧ b) false. *) - (* Proof. *) - (* intros. *) - (* replace false with (false && c) by auto. *) - (* constructor; auto. *) - (* Qed. *) - - (* Lemma apred_and_false2 : *) - (* forall A ctx a b c, *) - (* @eval_apred A ctx a c -> *) - (* eval_apred ctx b false -> *) - (* eval_apred ctx (a ∧ b) false. *) - (* Proof. *) - (* intros. *) - (* replace false with (c && false) by eauto with bool. *) - (* constructor; auto. *) - (* Qed. *) - - (* #[local] Opaque simplify. *) - - (* Lemma apred_simplify: *) - (* forall A ctx a b, *) - (* @eval_apred A ctx a b -> *) - (* @eval_apred A ctx (simplify a) b. *) - (* Proof. Admitted. *) - - (* Lemma exists_get_pred_eval : *) - (* forall A ctx f p, *) - (* exists c, @eval_apred A ctx (get_pred' f p) c. *) - (* Proof. *) - (* induction p; crush; try solve [econstructor; constructor; eauto]. *) - (* destruct_match. inv Heqp0. econstructor. *) - (* unfold apredicated_to_apred_op. *) - (* Admitted. (*probably not provable.*) *) - - (* Lemma falsy_update : *) - (* forall A f a ctx p f', *) - (* @eval_apred A ctx (fst f) false -> *) - (* update (Some f) a = Some (p, f') -> *) - (* eval_apred ctx p false. *) - (* Proof. *) - (* destruct f; destruct a; inversion 1; subst; crush; *) - (* destruct_match; simplify; auto; *) - (* unfold Option.bind, Option.bind2 in *; *) - (* repeat (destruct_match; try discriminate; []); simplify; auto. *) - (* apply apred_simplify. eapply apred_and_false2; eauto. admit. *) - (* apply apred_simplify. eapply apred_and_false2; eauto. admit. *) - (* constructor; auto. *) - (* constructor; auto. *) - (* constructor; auto. *) - (* constructor; auto. *) - (* constructor; auto. *) - (* rewrite H2. *) - (* apply apred_simplify. eapply apred_and_false2; eauto. admit. *) - (* apply apred_simplify. eapply apred_and_false2; eauto. admit. *) - (* Unshelve. all: exact true. *) - (* Admitted. *) - - (* Lemma abstr_fold_falsy : *) - (* forall x i0 sp cf i f p p' f', *) - (* sem (mk_ctx i0 sp ge) f (i, cf) -> *) - (* eval_apred (mk_ctx i0 sp ge) p false -> *) - (* fold_left update x (Some (p, f)) = Some (p', f') -> *) - (* sem (mk_ctx i0 sp ge) f' (i, cf). *) - (* Proof. *) - (* induction x; crush. *) - (* eapply IHx. *) - (* destruct a; destruct f; crush; *) - (* try solve [eapply app_predicated_sem; eauto; apply combined_falsy; auto]. *) - (* (* now apply falsy_update. *) *) - (* (* Qed. *) Admitted. *) - Lemma state_lessdef_sem : forall i sp f i' ti cf, sem (mk_ctx i sp ge) f (i', cf) -> @@ -1335,29 +547,88 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. (* #[local] Opaque update. *) + Lemma mfold_left_update_Some : + forall xs x v, + mfold_left update xs x = Some v -> + exists y, x = Some y. + Proof. Admitted. + + Lemma step_instr_term_exists : + forall A B ge sp v x v2 cf, + @step_instr A B ge sp (Iexec v) x (Iterm v2 cf) -> + exists p, x = RBexit p cf. + Proof using. inversion 1; eauto. Qed. + + Lemma abstr_fold_falsy : + forall A i sp ge f i' cf p f' ilist p', + @sem A (mk_ctx i sp ge) f (i', cf) -> + mfold_left update ilist (Some (p, f)) = Some (p', f') -> + eval_predf (is_ps i') p = false -> + sem (mk_ctx i sp ge) f' (i', cf). + Proof. Admitted. + + Ltac destr := destruct_match; try discriminate; []. + + Lemma eval_predf_update_true : + forall i i' curr_p next_p f f_next instr sp, + update (curr_p, f) instr = Some (next_p, f_next) -> + step_instr ge sp (Iexec i) instr (Iexec i') -> + eval_predf (is_ps i) curr_p = true -> + eval_predf (is_ps i') next_p = true. + Proof. + intros * UPD STEP EVAL. destruct instr; cbn [update] in UPD; + try solve [unfold Option.bind in *; try destr; inv UPD; inv STEP; auto]. + - unfold Option.bind in *. destr. inv UPD. inv STEP; auto. cbn [is_ps] in *. + admit. + - unfold Option.bind in *. destr. inv UPD. inv STEP. inv H3. admit. + Admitted. (* This only needs the addition of the property that any setpreds will not contain the + predicate in the name. *) + + Lemma eval_predf_lessdef : + forall p a b, + state_lessdef a b -> + eval_predf (is_ps a) p = eval_predf (is_ps b) p. + Proof using. + induction p; crush. + - inv H. simpl. unfold eval_predf. simpl. + repeat destr. inv Heqp0. rewrite H1. auto. + - rewrite !eval_predf_Pand. + erewrite IHp1 by eassumption. + now erewrite IHp2 by eassumption. + - rewrite !eval_predf_Por. + erewrite IHp1 by eassumption. + now erewrite IHp2 by eassumption. + Qed. + Lemma abstr_fold_correct : - forall sp x i i' i'' cf f p f', + forall sp x i i' i'' cf f p f' curr_p, SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) -> - sem (mk_ctx i sp ge) (snd f) (i', None) -> - mfold_left update x (Some f) = Some (p, f') -> + sem (mk_ctx i sp ge) f (i', None) -> + eval_predf (is_ps i') curr_p = true -> + mfold_left update x (Some (curr_p, f)) = Some (p, f') -> forall ti, state_lessdef i ti -> exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf) /\ state_lessdef i'' ti'. Proof. - induction x; simplify; inv H. - - destruct f. (* exploit update_Some; eauto; intros. simplify. *) - (* rewrite H3 in H1. destruct x0. *) - (* exploit IHx; eauto. eapply sem_update_instr; eauto. *) - (* - destruct f. *) - (* exploit state_lessdef_sem; eauto; intros. simplify. *) - (* exploit step_instr_lessdef_term; eauto; intros. simplify. *) - (* inv H6. exploit update_Some; eauto; simplify. destruct x2. *) - (* exploit sem_update_instr_term; eauto; simplify. *) - (* eexists; split. *) - (* eapply abstr_fold_falsy; eauto. *) - (* rewrite H6 in H1. eauto. auto. *) - (* Qed. *) Admitted. + induction x as [| x xs IHx ]; intros; cbn -[update] in *; inv H; cbn [fst snd] in *. + - (* inductive case *) + exploit mfold_left_update_Some; eauto; intros Hexists; + inversion Hexists as [[curr_p_inter f_inter] EXEQ]; clear Hexists. + exploit eval_predf_update_true; eauto; intros EVALTRUE. + rewrite EXEQ in H2. eapply IHx in H2; eauto; cbn [fst snd] in *. + eapply sem_update_instr; eauto. + - (* terminal case *) + exploit mfold_left_update_Some; eauto; intros Hexists; + inversion Hexists as [[curr_p_inter f_inter] EXEQ]; clear Hexists. rewrite EXEQ in H2. + exploit state_lessdef_sem; eauto; intros H; inversion H as [v [Hi LESSDEF]]; clear H. + exploit step_instr_lessdef_term; eauto; intros H; inversion H as [v2 [Hi2 LESSDEF2]]; clear H. + exploit step_instr_term_exists; eauto; inversion 1 as [? ?]; subst; clear H. + erewrite eval_predf_lessdef in H1 by eassumption. + exploit sem_update_instr_term; eauto; intros [A B]. + exists v2. split. inv Hi2. + eapply abstr_fold_falsy; try eassumption. auto. + Qed. Lemma sem_regset_empty : forall A ctx, @sem_regset A ctx empty (ctx_rs ctx). @@ -1396,7 +667,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. destruct_match; try easy. destruct p; simplify. eapply abstr_fold_correct; eauto. - simplify. eapply sem_empty. + simplify. eapply sem_empty. auto. Qed. Lemma abstr_check_correct : @@ -1413,7 +684,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. abstract_sequence x = Some x' -> sem (mk_ctx i sp ge) x' (i', (Some cf)) -> state_lessdef i ti -> - exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) + exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. Admitted. diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v index 80a7825..86bc598 100644 --- a/src/hls/HashTree.v +++ b/src/hls/HashTree.v @@ -459,3 +459,23 @@ Module HashTree(H: Hashable). Module HashMonad := Statemonad(HashState). End HashTree. + +Definition gt_1 {A} h := + forall x (y: A), h ! x = Some y -> 1 < x. + +Module HashTreeProperties (Import H: Hashable). + + Module Import HT := HashTree(H). + + Lemma hash_value_gt : + forall max v h, + gt_1 h -> + gt_1 (snd (hash_value max v h)). + Proof. + unfold gt_1, hash_value; intros. + destruct_match; eauto. + destruct (peq (Pos.max max (max_key h) + 1) x); [subst;lia|]. + cbn [snd] in *. rewrite PTree.gso in H0; eauto. + Qed. + +End HashTreeProperties. -- cgit