From 8f9dda38a85613f147b831a1b86f1933fe66a6c7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 12 Oct 2021 18:25:04 +0100 Subject: [sched] Update Abstr.v to use HashTree --- src/hls/Abstr.v | 126 +++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 97 insertions(+), 29 deletions(-) (limited to 'src/hls') diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 271355d..58df532 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz + * Copyright (C) 2021 Yann Herklotz * * 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 @@ -30,6 +30,7 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.HashTree. #[local] Open Scope positive. @@ -508,13 +509,57 @@ Proof. end; subst; f_equal; crush; eauto using Peqb_true_eq]. Qed. -Definition hash_tree := PTree.t expression. +Lemma beq_expression_refl: forall e, beq_expression e e = true. +Proof. + intros. + induction e using expression_ind2 with (P0 := fun el => beq_expression_list el el = true); + crush; repeat (destruct_match; crush); []. + crush. rewrite IHe. rewrite IHe0. auto. +Qed. -Definition find_tree (el: expression) (h: hash_tree) : option positive := - match filter (fun x => beq_expression el (snd x)) (PTree.elements h) with - | (p, _) :: nil => Some p - | _ => None - end. +Lemma beq_expression_list_refl: forall e, beq_expression_list e e = true. +Proof. induction e; auto. simplify. rewrite beq_expression_refl. auto. Qed. + +Lemma beq_expression_correct2: + forall e1 e2, beq_expression e1 e2 = false -> e1 <> e2. +Proof. + induction e1 using expression_ind2 + with (P0 := fun el1 => forall el2, beq_expression_list el1 el2 = false -> el1 <> el2). + - intros. simplify. repeat (destruct_match; crush). + - intros. simplify. repeat (destruct_match; crush). subst. apply IHe1 in H. + unfold not in *. intros. apply H. inv H0. auto. + - intros. simplify. repeat (destruct_match; crush); subst. + unfold not in *; intros. inv H0. rewrite beq_expression_refl in H. + discriminate. + unfold not in *; intros. inv H. rewrite beq_expression_list_refl in Heqb. discriminate. + - simplify. repeat (destruct_match; crush); subst; + unfold not in *; intros. + inv H0. rewrite beq_expression_refl in H; crush. + inv H. rewrite beq_expression_refl in Heqb0; crush. + inv H. rewrite beq_expression_list_refl in Heqb; crush. + - simplify. repeat (destruct_match; crush); subst. + unfold not in *; intros. inv H0. rewrite beq_expression_list_refl in H; crush. + - simplify. repeat (destruct_match; crush); subst. + - simplify. repeat (destruct_match; crush); subst. + apply andb_false_iff in H. inv H. unfold not in *; intros. + inv H. rewrite beq_expression_refl in H0; discriminate. + unfold not in *; intros. inv H. rewrite beq_expression_list_refl in H0; discriminate. +Qed. + +Lemma expression_dec: forall e1 e2: expression, {e1 = e2} + {e1 <> e2}. +Proof. + intros. + destruct (beq_expression e1 e2) eqn:?. apply beq_expression_correct in Heqb. auto. + apply beq_expression_correct2 in Heqb. auto. +Defined. + +Module HashExpr <: Hashable. + Definition t := expression. + Definition eq_dec := expression_dec. +End HashExpr. + +Module HT := HashTree(HashExpr). +Import HT. Definition combine_option {A} (a b: option A) : option A := match a, b with @@ -523,24 +568,13 @@ Definition combine_option {A} (a b: option A) : option A := | _, _ => None end. -Definition max_key {A} (t: PTree.t A) := - fold_right Pos.max 1%positive (map fst (PTree.elements t)). - -Definition hash_expr (max: predicate) (e: expression) (h: hash_tree): predicate * hash_tree := - match find_tree e h with - | Some p => (p, h) - | None => - let nkey := Pos.max max (max_key h) + 1 in - (nkey, PTree.set nkey e h) - end. - Fixpoint encode_expression_ne (max: predicate) (pe: pred_expr_ne) (h: hash_tree): pred_op * hash_tree := match pe with | NE.singleton (p, e) => - let (p', h') := hash_expr max e h in + let (p', h') := hash_value max e h in (Por (Pnot p) (Pvar p'), h') | (p, e) ::| pr => - let (p', h') := hash_expr max e h in + let (p', h') := hash_value max e h in let (p'', h'') := encode_expression_ne max pr h' in (Pand (Por (Pnot p) (Pvar p')) p'', h'') end. @@ -548,7 +582,7 @@ Fixpoint encode_expression_ne (max: predicate) (pe: pred_expr_ne) (h: hash_tree) Definition encode_expression (max: predicate) (pe: pred_expr) (h: hash_tree): pred_op * hash_tree := match pe with | Psingle e => - let (p, h') := hash_expr max e h in (Pvar p, h') + let (p, h') := hash_value max e h in (Pvar p, h') | Plist l => encode_expression_ne max l h end. @@ -686,6 +720,36 @@ Proof. crush. Qed. +Definition inj_asgn_f a b := if (a =? b)%nat then true else false. + +Lemma inj_asgn_eg : + forall a b, + inj_asgn_f a b = inj_asgn_f a a -> a = b. +Proof. + intros. destruct (Nat.eq_dec a b); subst. + auto. unfold inj_asgn_f in H. apply Nat.eqb_neq in n. + rewrite n in H. rewrite Nat.eqb_refl in H. discriminate. +Qed. + +Lemma inj_asgn : + forall a b, + (forall (f: nat -> bool), f a = f b) -> a = b. +Proof. intros. apply inj_asgn_eg. eauto. Qed. + +Lemma sat_predicate_Pvar_inj : + forall p1 p2, + (forall c, sat_predicate (Pvar p1) c = sat_predicate (Pvar p2) c) -> p1 = p2. +Proof. simplify. apply Pos2Nat.inj. eapply inj_asgn. eauto. Qed. + +Lemma hash_present_eq : + forall m e1 e2 p1 h h', + hash_value m e2 h = (p1, h') -> + h ! p1 = Some e1 -> + e1 = e2. +Proof. + intros. unfold hash_value in *. destruct_match. + - inv H. + Section CORRECT. Definition fd := @fundef RTLBlock.bb. @@ -694,25 +758,29 @@ Section CORRECT. Context (ictx: @ctx fd) (octx: @ctx tfd) (HSIM: similar ictx octx). Lemma check_correct_sem_value: - forall x x' v n, + forall x x' v v' n, beq_pred_expr n x x' = true -> sem_pred_expr sem_value ictx x v -> - sem_pred_expr sem_value octx x' v. + sem_pred_expr sem_value octx x' v' -> + v = v'. Proof. + #[local] Opaque PTree.set. unfold beq_pred_expr. intros. repeat (destruct_match; try discriminate; []); subst. unfold sat_pred_simple in *. repeat destruct_match; try discriminate; []; subst. - assert (unsat (Por (Pand p (Pnot p0)) (Pand p0 (Pnot p)))) by eauto. - pose proof (sat_equiv2 _ _ H1). + assert (X: unsat (Por (Pand p (Pnot p0)) (Pand p0 (Pnot p)))) by eauto. + pose proof (sat_equiv2 _ _ X). destruct x, x'; simplify. - repeat destruct_match; try discriminate; []. inv Heqp0. constructor. - inv H0. inv Heqp. + repeat destruct_match; try discriminate; []. inv Heqp0. inv H0. inv H1. + inv Heqp. + + apply sat_predicate_Pvar_inj in H2; subst. assert (e1 = e0) by admit; subst. - assert (forall e v, sem_value ictx e v -> sem_value octx e v) by admit. + assert (forall e v v', sem_value ictx e v -> sem_value octx e v' -> v = v') by admit. - eauto. + eapply H; eauto. - admit. - admit. -- cgit