diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-07-14 08:46:14 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-07-14 08:46:14 +0100 |
commit | aa753acd776638971abb5d9901cc99ef259cb314 (patch) | |
tree | 647722ffa3dae5b10e04cdf46b4e96f27699a26d /src/hls/Abstr.v | |
parent | 839ae9a65535e25e52207d46e274385e0709a90f (diff) | |
download | vericert-aa753acd776638971abb5d9901cc99ef259cb314.tar.gz vericert-aa753acd776638971abb5d9901cc99ef259cb314.zip |
Add work on abstract predicates
Diffstat (limited to 'src/hls/Abstr.v')
-rw-r--r-- | src/hls/Abstr.v | 185 |
1 files changed, 141 insertions, 44 deletions
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') -> |