diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/extraction/Extraction.v | 2 | ||||
-rw-r--r-- | src/hls/Abstr.v | 185 | ||||
-rw-r--r-- | src/hls/Gible.v | 3 | ||||
-rw-r--r-- | src/hls/GiblePargen.v | 14 | ||||
-rw-r--r-- | src/hls/GiblePargenproof.v | 258 | ||||
-rw-r--r-- | src/hls/HashTree.v | 11 |
6 files changed, 377 insertions, 96 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 29c6e4c..aba2fe7 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -187,7 +187,7 @@ Extract Constant GiblePargen.schedule => "Schedule.schedule_fn". (* Loop normalization *) Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle". -Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty])". +Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 3001123..9902dc9 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021-2022 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 @@ -17,6 +17,7 @@ *) Require Import Coq.Logic.Decidable. +Require Import Coq.Structures.Equalities. Require Import compcert.backend.Registers. Require Import compcert.common.AST. @@ -118,6 +119,24 @@ with expression_list : Type := | Econs : expression -> expression_list -> expression_list . +Definition apred : Type := expression. + +Inductive apred_op : Type := +| APlit: (bool * apred) -> apred_op +| APtrue: apred_op +| APfalse: apred_op +| APand: apred_op -> apred_op -> apred_op +| APor: apred_op -> apred_op -> apred_op. + +(* Declare Scope apred_op. *) + +(* Notation "A ∧ B" := (Pand A B) (at level 20) : apred_op. *) +(* Notation "A ∨ B" := (Por A B) (at level 25) : apred_op. *) +(* Notation "⟂" := (Pfalse) : apred_op. *) +(* Notation "'T'" := (Ptrue) : apred_op. *) + +(* #[local] Open Scope apred_op. *) + (*Inductive pred_expr : Type := | PEsingleton : option pred_op -> expression -> pred_expr | PEcons : option pred_op -> expression -> pred_expr -> pred_expr.*) @@ -210,9 +229,10 @@ Import NE.NonEmptyNotation. #[local] Open Scope non_empty_scope. +Definition apredicated A := NE.non_empty (apred_op * A). Definition predicated A := NE.non_empty (pred_op * A). -Definition pred_expr := predicated expression. +Definition apred_expr := apredicated expression. (*| Using ``IMap`` we can create a map from resources to any other type, as @@ -221,11 +241,11 @@ resources can be uniquely identified as positive numbers. Module Rtree := ITree(R_indexed). -Definition forest : Type := Rtree.t pred_expr. +Definition forest : Type := Rtree.t apred_expr. Definition get_forest v (f: forest) := match Rtree.get v f with - | None => NE.singleton (T, (Ebase v)) + | None => NE.singleton (APtrue, (Ebase v)) | Some v' => v' end. @@ -324,28 +344,43 @@ with sem_val_list : ctx -> expression_list -> list val -> Prop := sem_val_list ctx (Econs e l) (v :: lv) . +Inductive eval_apred (c: ctx): apred_op -> bool -> Prop := +| eval_APtrue : eval_apred c APtrue true +| eval_APfalse : eval_apred c APfalse false +| eval_APlit : forall p (b: bool) bres, + sem_pred c p (if b then bres else negb bres) -> + eval_apred c (APlit (b, p)) bres +| eval_APand : forall p1 p2 b1 b2, + eval_apred c p1 b1 -> + eval_apred c p2 b2 -> + eval_apred c (APand p1 p2) (b1 && b2) +| eval_APor1 : forall p1 p2 b1 b2, + eval_apred c p1 b1 -> + eval_apred c p2 b2 -> + eval_apred c (APor p1 p2) (b1 || b2). + Inductive sem_pred_expr {B: Type} (sem: ctx -> expression -> B -> Prop): - ctx -> pred_expr -> B -> Prop := + ctx -> apred_expr -> B -> Prop := | sem_pred_expr_cons_true : forall ctx e pr p' v, - eval_predf (ctx_ps ctx) pr = true -> + eval_apred ctx pr true -> sem ctx e v -> sem_pred_expr sem ctx ((pr, e) ::| p') v | sem_pred_expr_cons_false : forall ctx e pr p' v, - eval_predf (ctx_ps ctx) pr = false -> + eval_apred ctx pr false -> sem_pred_expr sem ctx p' v -> sem_pred_expr sem ctx ((pr, e) ::| p') v | sem_pred_expr_single : forall ctx e pr v, - eval_predf (ctx_ps ctx) pr = true -> + eval_apred ctx pr true -> sem ctx e v -> sem_pred_expr sem ctx (NE.singleton (pr, e)) v . -Definition collapse_pe (p: pred_expr) : option expression := +Definition collapse_pe (p: apred_expr) : option expression := match p with - | NE.singleton (T, p) => Some p + | NE.singleton (APtrue, p) => Some p | _ => None end. @@ -361,13 +396,13 @@ Inductive sem_regset : ctx -> forest -> regset -> Prop := (forall x, sem_pred_expr sem_value ctx (f # (Reg x)) (rs' !! x)) -> sem_regset ctx f rs'. -Inductive sem : ctx -> forest -> instr_state * cf_instr -> Prop := +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 sem_mem ctx (f # Mem) m' -> - sem_pred_expr sem_exit ctx (f # Exit) (Some cf) -> + sem_pred_expr sem_exit ctx (f # Exit) cf -> sem ctx f (mk_instr_state rs' pr' m', cf). End SEMANTICS. @@ -480,35 +515,49 @@ Proof. intros; destruct (pred_expr_item_eq pe1 pe2) eqn:?; unfold not; [tauto | now right]. Qed. -Module HashExpr <: Hashable. +Module HashExpr' <: MiniDecidableType. Definition t := expression. Definition eq_dec := expression_dec. -End HashExpr. +End HashExpr'. +Module HashExpr := Make_UDT(HashExpr'). Module HT := HashTree(HashExpr). Import HT. -Definition combine_option {A} (a b: option A) : option A := - match a, b with - | Some a', _ => Some a' - | _, Some b' => Some b' - | _, _ => None +Fixpoint hash_predicate (max: predicate) (ap: apred_op) (h: hash_tree) + : pred_op * hash_tree := + match ap with + | APtrue => (Ptrue, h) + | APfalse => (Pfalse, h) + | APlit (b, ap') => + let (p', h') := hash_value max ap' h in + (Plit (b, p'), h') + | APand p1 p2 => + let (p1', h') := hash_predicate max p1 h in + let (p2', h'') := hash_predicate max p2 h' in + (Pand p1' p2', h'') + | APor p1 p2 => + let (p1', h') := hash_predicate max p1 h in + let (p2', h'') := hash_predicate max p2 h' in + (Por p1' p2', h'') end. -Fixpoint norm_expression (max: predicate) (pe: pred_expr) (h: hash_tree) +Fixpoint norm_expression (max: predicate) (pe: apred_expr) (h: hash_tree) : (PTree.t pred_op) * hash_tree := match pe with | NE.singleton (p, e) => - let (p', h') := hash_value max e h in - (PTree.set p' p (PTree.empty _), h') + let (hashed_e, h') := hash_value max e h in + let (hashed_p, h'') := hash_predicate max p h' in + (PTree.set hashed_e hashed_p (PTree.empty _), h'') | (p, e) ::| pr => - let (p', h') := hash_value max e h in - let (p'', h'') := norm_expression max pr h' in - match p'' ! p' with + let (hashed_e, h') := hash_value max e h in + let (norm_pr, h'') := norm_expression max pr h' in + let (hashed_p, h''') := hash_predicate max p h'' in + match norm_pr ! hashed_e with | Some pr_op => - (PTree.set p' (pr_op ∨ p) p'', h'') + (PTree.set hashed_e (pr_op ∨ hashed_p) norm_pr, h''') | None => - (PTree.set p' p p'', h'') + (PTree.set hashed_e hashed_p norm_pr, h''') end end. @@ -534,11 +583,11 @@ Definition encode_expression max pe h := (Pand (Por (Pnot p) (Pvar p')) p'', h'') end.*) -Fixpoint max_pred_expr (pe: pred_expr) : positive := - match pe with - | NE.singleton (p, e) => max_predicate p - | (p, e) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe') - end. +(* Fixpoint max_pred_expr (pe: pred_expr) : positive := *) +(* match pe with *) +(* | NE.singleton (p, e) => max_predicate p *) +(* | (p, e) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe') *) +(* end. *) Definition empty : forest := Rtree.empty _. @@ -584,7 +633,7 @@ Inductive similar {A B} : @ctx A -> @ctx B -> Prop := match_states ist ist' -> similar (mk_ctx ist sp ge) (mk_ctx ist' sp tge). -Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool := +Definition beq_pred_expr_once (pe1 pe2: apred_expr) : bool := match pe1, pe2 with (* PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2 | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 => @@ -603,9 +652,9 @@ Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool := end else false*) | pe1, pe2 => - let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in - let (p1, h) := encode_expression max pe1 (PTree.empty _) in - let (p2, h') := encode_expression max pe2 h in + (* let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in *) + let (p1, h) := encode_expression 1%positive pe1 (PTree.empty _) in + let (p2, h') := encode_expression 1%positive pe2 h in equiv_check p1 p2 end. @@ -631,10 +680,8 @@ Variant sem_pred_tree {A B: Type} (sem: ctx -> expression -> B -> Prop): et ! e = Some expr -> sem_pred_tree sem ctx et pt v. -Variant predicated_mutexcl {A: Type} : predicated A -> Prop := -| predicated_mutexcl_intros : forall pe, - (forall x y, NE.In x pe -> NE.In y pe -> x <> y -> fst x ⇒ ¬ fst y) -> - predicated_mutexcl pe. +Definition predicated_mutexcl {A: Type} (pe: predicated A): Prop := + forall x y, NE.In x pe -> NE.In y pe -> x <> y -> fst x ⇒ ¬ fst y. Lemma hash_value_in : forall max e et h h0, @@ -657,15 +704,65 @@ Lemma norm_expr_constant : Proof. Admitted. Lemma predicated_cons : - forall A (a:pred_op * A) x, + forall A (a: pred_op * A) x, predicated_mutexcl (a ::| x) -> predicated_mutexcl x. Proof. - intros. - inv H. constructor; intros. - apply H0; auto; constructor; tauto. + unfold predicated_mutexcl; intros. + apply H; auto; constructor; tauto. Qed. +Module Type AbstrPredSet. + + Parameter apred_list : list apred_op. + + Parameter h : hash_tree. + + Axiom h_valid : + forall a, + In a apred_list -> + exists p, hash_predicate 1 a h = (p, h). + +End AbstrPredSet. + +Section ABSTR_PRED. + + Context (h: hash_tree). + Context (m: predicate). + + Definition sat_aequiv ap1 ap2 := + exists p1 p2, + sat_equiv p1 p2 + /\ hash_predicate m ap1 h = (p1, h) + /\ hash_predicate m ap2 h = (p2, h). + + Lemma aequiv_symm : forall a b, sat_aequiv a b -> sat_aequiv b a. + Proof. + unfold sat_aequiv; simplify; do 2 eexists; simplify; [symmetry | |]; eauto. + Qed. + + Lemma aequiv_trans : + forall a b c, + sat_aequiv a b -> + sat_aequiv b c -> + sat_aequiv a c. + Proof. + unfold sat_aequiv; intros * H H0; simplify; do 2 eexists; simplify; + [| eassumption | eassumption]; rewrite H0 in H3; inv H3. + transitivity x2; auto. + Qed. + + Instance PER_aequiv : PER sat_aequiv := + { PER_Symmetric := aequiv_symm; + PER_Transitive := aequiv_trans; + }. + +End ABSTR_PRED. + + + +Definition hash_predicate + Lemma norm_expr_mutexcl : forall m pe h t h' e e' p p', norm_expression m pe h = (t, h') -> diff --git a/src/hls/Gible.v b/src/hls/Gible.v index cacca85..fdc9a9d 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -251,6 +251,9 @@ Variant truthy (ps: predset): option pred_op -> Prop := | truthy_None: truthy ps None | truthy_Some: forall p, eval_predf ps p = true -> truthy ps (Some p). +Variant falsy (ps: predset): option pred_op -> Prop := + | falsy_Some: forall p, eval_predf ps p = false -> falsy ps (Some p). + Variant instr_falsy (ps: predset): instr -> Prop := | RBop_falsy : forall p op args res, diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index da0567b..01ee2cd 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -211,7 +211,7 @@ Definition update (fop : option pred_op * forest) (i : instr): (option pred_op * (map_predicated (pred_ret (Esetpred c)) (merge (list_translation args f))))) | RBexit p c => - (combine_pred (Option.map negate p) pred, + (combine_pred (Some (negate (Option.default T p))) pred, f # Exit <- (app_predicated (combine_pred p pred) (f # Exit) (pred_ret (Eexit c)))) end. @@ -224,11 +224,8 @@ code than in the RTLBlock code. Get a sequence from the basic block. |*) -Fixpoint abstract_sequence (f : option pred_op * forest) (b : list instr) : option pred_op * forest := - match b with - | nil => f - | i :: l => abstract_sequence (update f i) l - end. +Definition abstract_sequence (b : list instr) : forest := + snd (fold_left update b (None, empty)). (*| Check equivalence of control flow instructions. As none of the basic blocks @@ -255,9 +252,8 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool := end. Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool := - (check (snd (abstract_sequence (None, empty) bb)) - (snd (abstract_sequence (None, empty) (concat (concat bbt))))) && - empty_trees bb bbt. + (check (abstract_sequence bb) (abstract_sequence (concat (concat bbt)))) + && empty_trees bb bbt. Definition check_scheduled_trees := beq2 schedule_oracle. diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index eaf0c32..955902c 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -59,6 +59,28 @@ Inductive state_lessdef : instr_state -> instr_state -> Prop := (forall x, ps1 !! x = ps2 !! x) -> state_lessdef (mk_instr_state rs1 ps1 m1) (mk_instr_state rs2 ps2 m1). +Lemma state_lessdef_refl x : state_lessdef x x. +Proof. destruct x; constructor; auto. Qed. + +Lemma state_lessdef_symm x y : state_lessdef x y -> state_lessdef y x. +Proof. destruct x; destruct y; inversion 1; subst; simplify; constructor; auto. Qed. + +Lemma state_lessdef_trans : + forall a b c, + state_lessdef a b -> + state_lessdef b c -> + state_lessdef a c. +Proof. + inversion 1; inversion 1; subst; simplify. + constructor; eauto; intros. rewrite H0. auto. +Qed. + +#[global] Instance Equivalence_state_lessdef : Equivalence state_lessdef := + { Equivalence_Reflexive := state_lessdef_refl; + Equivalence_Symmetric := state_lessdef_symm; + Equivalence_Transitive := state_lessdef_trans; + }. + Definition check_dest i r' := match i with | RBop p op rl r => (r =? r')%positive @@ -160,8 +182,8 @@ Qed. Lemma abstr_comp : forall l i f x x0, - abstract_sequence f (l ++ i :: nil) = x -> - abstract_sequence f l = 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. @@ -1036,38 +1058,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. constructor; eauto. Qed. - (* TODO: Fix these proofs, now the cf_instr is in the State. *) - Lemma step_cf_instr_correct: - forall t s s' cf, - GibleSeq.step_cf_instr ge s cf t s' -> - forall r, - match_states s r -> - exists r', step_cf_instr tge r cf t r' /\ match_states s' r'. - Proof using TRANSL. - - (*induction 1; repeat semantics_simpl; - try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)]. - { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - eapply eval_builtin_args_eq. eapply REG. - eapply Events.eval_builtin_args_preserved. eapply symbols_preserved. - eauto. - intros. - unfold regmap_setres. destruct res. - destruct (Pos.eq_dec x0 x); subst. - repeat rewrite Regmap.gss; auto. - repeat rewrite Regmap.gso; auto. - eapply REG. eapply REG. - } - { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). - unfold regmap_optget. destruct or. rewrite REG. constructor; eauto. - constructor; eauto. - } - { exploit IHstep_cf_instr; eauto. simplify. - repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). - erewrite eval_predf_pr_equiv; eauto. - } - Qed.*) Admitted. - #[local] Hint Resolve Events.external_call_symbols_preserved : core. #[local] Hint Resolve eval_builtin_args_eq : core. #[local] Hint Resolve symbols_preserved : core. @@ -1146,6 +1136,195 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. eapply IHx; eauto. Qed. + Lemma eval_predf_negate : + forall ps p, + eval_predf ps (negate p) = negb (eval_predf ps p). + Proof. + unfold eval_predf; intros. rewrite negate_correct. auto. + Qed. + + Lemma is_truthy_negate : + forall ps p pred, + truthy ps p -> + falsy ps (combine_pred (Some (negate (Option.default T p))) pred). + Proof. + inversion 1; subst; simplify. + - destruct pred; constructor; auto. + - destruct pred; constructor. + rewrite eval_predf_Pand. rewrite eval_predf_negate. rewrite H0. auto. + rewrite eval_predf_negate. rewrite H0. auto. + Qed. + + Lemma sem_update_instr : + forall f i' i'' a sp p i, + sem (mk_ctx i sp ge) f (i', None) -> + step_instr ge sp (Iexec i') a (Iexec i'') -> + sem (mk_ctx i sp ge) (snd (update (p, f) a)) (i'', None). + Proof. Admitted. + + Lemma sem_update_instr_term : + forall f i' i'' a sp i cf p p', + sem (mk_ctx i sp ge) f (i', None) -> + step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) -> + sem (mk_ctx i sp ge) (snd (update (p', f) a)) (i'', Some cf) + /\ falsy (is_ps i'') (fst (update (p', f) a)). + 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. + + Lemma step_instr_lessdef_term : + forall sp a i i' ti cf, + step_instr ge sp (Iexec i) a (Iterm i' cf) -> + state_lessdef i ti -> + 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 -> + falsy i (combine_pred o o1). + Proof. + inversion 1; subst; crush. destruct o; simplify. + constructor. rewrite eval_predf_Pand. rewrite H0. crush. + constructor. auto. + Qed. + + Lemma falsy_update : + forall f a ps, + falsy ps (fst f) -> + falsy ps (fst (update f a)). + Proof. + destruct f; destruct a; inversion 1; subst; crush. + rewrite <- H1. constructor. unfold Option.default. destruct o0. + rewrite eval_predf_Pand. rewrite H0. crush. crush. + Qed. + + Lemma abstr_fold_falsy : + forall x i0 sp cf i f, + sem (mk_ctx i0 sp ge) (snd f) (i, cf) -> + falsy (is_ps i) (fst f) -> + sem (mk_ctx i0 sp ge) (snd (fold_left update x 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. + + Lemma state_lessdef_sem : + forall i sp f i' ti cf, + sem (mk_ctx i sp ge) f (i', cf) -> + state_lessdef i ti -> + exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ state_lessdef i' ti'. + Proof. Admitted. + + Lemma abstr_fold_correct : + forall sp x i i' i'' cf f, + SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) -> + sem (mk_ctx i sp ge) (snd f) (i', None) -> + forall ti, + state_lessdef i ti -> + exists ti', sem (mk_ctx ti sp ge) (snd (fold_left update x f)) (ti', Some cf) + /\ state_lessdef i'' ti'. + Proof. + induction x; simplify; inv H. + - destruct f; exploit IHx; eauto; eapply sem_update_instr; eauto. + - destruct f. inversion H5; subst. + exploit state_lessdef_sem; eauto; intros. inv H. inv H2. + exploit step_instr_lessdef_term; eauto; intros. inv H2. inv H4. + exploit sem_update_instr_term; eauto; intros. inv H4. + eexists; split. eapply abstr_fold_falsy; eauto. + auto. + Qed. + + Lemma sem_regset_empty : + forall A ctx, @sem_regset A ctx empty (ctx_rs ctx). + Proof. + intros; constructor; intros. + constructor; auto. constructor. + Qed. + + Lemma sem_predset_empty : + forall A ctx, @sem_predset A ctx empty (ctx_ps ctx). + Proof. + intros; constructor; intros. + constructor; auto. constructor. + Qed. + + Lemma sem_empty : + forall A ctx, @sem A ctx empty (ctx_is ctx, None). + Proof. + intros. destruct ctx. destruct ctx_is. + constructor; try solve [constructor; constructor; crush]. + eapply sem_regset_empty. + eapply sem_predset_empty. + Qed. + + Lemma abstr_sequence_correct : + forall sp x i i'' cf, + SeqBB.step ge sp (Iexec i) x (Iterm i'' cf) -> + forall ti, + state_lessdef i ti -> + exists ti', sem (mk_ctx ti sp ge) (abstract_sequence x) (ti', Some cf) + /\ state_lessdef i'' ti'. + Proof. + unfold abstract_sequence. intros; eapply abstr_fold_correct; eauto. + simplify. eapply sem_empty. + Qed. + + Lemma abstr_check_correct : + forall sp i i' a b cf ti, + check a b = true -> + sem (mk_ctx i sp ge) a (i', cf) -> + state_lessdef i ti -> + exists ti', sem (mk_ctx ti sp ge) b (ti', cf) + /\ state_lessdef i' ti'. + Proof. Admitted. + + Lemma abstr_seq_reverse_correct : + forall sp x i i' ti cf, + sem (mk_ctx i sp ge) (abstract_sequence x) (i', (Some cf)) -> + state_lessdef i ti -> + exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) + /\ state_lessdef i' ti'. + Proof. Admitted. + Lemma schedule_oracle_correct : forall x y sp i i' ti cf, schedule_oracle x y = true -> @@ -1153,7 +1332,16 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. state_lessdef i ti -> exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf) /\ state_lessdef i' ti'. - Proof. Admitted. + Proof. + unfold schedule_oracle; intros. simplify. + exploit abstr_sequence_correct; eauto; simplify. + exploit abstr_check_correct; eauto. apply state_lessdef_refl. simplify. + exploit abstr_seq_reverse_correct; eauto. apply state_lessdef_refl. simplify. + exploit seqbb_step_parbb_step; eauto; intros. + econstructor; split; eauto. + etransitivity; eauto. + etransitivity; eauto. + Qed. Lemma step_cf_correct : forall cf ts s s' t, diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v index f3c57a8..9f9ec81 100644 --- a/src/hls/HashTree.v +++ b/src/hls/HashTree.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021-2022 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 @@ -16,6 +16,8 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +Require Import Coq.Structures.Equalities. + Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. @@ -136,12 +138,7 @@ Proof. eapply IHl. eauto. Qed. -Module Type Hashable. - - Parameter t: Type. - Parameter eq_dec: forall (t1 t2: t), {t1 = t2} + {t1 <> t2}. - -End Hashable. +Module Type Hashable := UsualDecidableType. Module HashTree(H: Hashable). |