From bfad3424b47a3b18c0225142443568bd9e4adbfa Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 12 Oct 2021 18:24:07 +0100 Subject: [sched] Add HashTree.v for hashing arbitrary values --- src/hls/HashTree.v | 413 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 413 insertions(+) create mode 100644 src/hls/HashTree.v (limited to 'src/hls') diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v new file mode 100644 index 0000000..cb712e9 --- /dev/null +++ b/src/hls/HashTree.v @@ -0,0 +1,413 @@ +(* + * Vericert: Verified high-level synthesis. + * 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 + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. +Require Import compcert.lib.Floats. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require compcert.verilog.Op. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.RTLPar. +Require Import vericert.hls.RTLBlockInstr. + +#[local] Open Scope positive. + +#[local] Hint Resolve in_eq : core. +#[local] Hint Resolve in_cons : core. + +Definition max_key {A} (t: PTree.t A) := + fold_right Pos.max 1%positive (map fst (PTree.elements t)). + +Lemma max_key_correct' : + forall l hi, In hi l -> hi <= fold_right Pos.max 1 l. +Proof. + induction l; crush. + inv H. lia. + destruct (Pos.max_dec a (fold_right Pos.max 1 l)); rewrite e. + - apply Pos.max_l_iff in e. + assert (forall a b c, a <= c -> c <= b -> a <= b) by lia. + eapply H; eauto. + - apply IHl; auto. +Qed. + +Lemma max_key_correct : + forall A h_tree hi (c: A), + h_tree ! hi = Some c -> + hi <= max_key h_tree. +Proof. + unfold max_key. intros. apply PTree.elements_correct in H. + apply max_key_correct'. + eapply in_map with (f := fst) in H. auto. +Qed. + +Lemma filter_none : + forall A f l (x: A), filter f l = nil -> In x l -> f x = false. +Proof. induction l; crush; inv H0; subst; destruct_match; crush. Qed. + +Lemma filter_set : + forall A l l' f (x: A), + (In x l -> In x l') -> + In x (filter f l) -> + In x (filter f l'). +Proof. + induction l; crush. + destruct_match; crush. inv H0; crush. + apply filter_In. simplify; crush. +Qed. + +Lemma filter_cons_true : + forall A f l (a: A) l', + filter f l = a :: l' -> f a = true. +Proof. + induction l; crush. destruct (f a) eqn:?. + inv H. auto. eapply IHl; eauto. +Qed. + +Lemma PTree_set_elements : + forall A t x x' (c: A), + In x (PTree.elements t) -> + x' <> (fst x) -> + In x (PTree.elements (PTree.set x' c t)). +Proof. + intros. destruct x. + eapply PTree.elements_correct. simplify. + rewrite PTree.gso; auto. apply PTree.elements_complete in H. auto. +Qed. + +Lemma filter_set2 : + forall A x y z (h: PTree.t A), + In z (PTree.elements (PTree.set x y h)) -> + In z (PTree.elements h) \/ fst z = x. +Proof. + intros. destruct z. + destruct (Pos.eq_dec p x); subst. + tauto. + left. apply PTree.elements_correct. apply PTree.elements_complete in H. + rewrite PTree.gso in H; auto. +Qed. + +Lemma in_filter : forall A f l (x: A), In x (filter f l) -> In x l. +Proof. induction l; crush. destruct_match; crush. inv H; crush. Qed. + +Lemma filter_norepet: + forall A f (l: list A), + list_norepet l -> + list_norepet (filter f l). +Proof. + induction l; crush. + inv H. destruct (f a). + constructor. unfold not in *; intros. apply H2. + eapply in_filter; eauto. + apply IHl; auto. + apply IHl; auto. +Qed. + +Lemma filter_norepet2: + forall A B g (l: list (A * B)), + list_norepet (map fst l) -> + list_norepet (map fst (filter g l)). +Proof. + induction l; crush. + inv H. destruct (g a) eqn:?. + simplify. constructor. unfold not in *. intros. + eapply H2. + apply list_in_map_inv in H. simplify; subst. + rewrite H. + apply filter_In in H1. simplify. + apply in_map. eauto. + eapply IHl. eauto. + eapply IHl. eauto. +Qed. + +Module Type Hashable. + + Parameter t: Type. + Parameter eq_dec: forall (t1 t2: t), {t1 = t2} + {t1 <> t2}. + +End Hashable. + +Module HashTree(H: Hashable). + + Import H. + + Definition hash := positive. + Definition hash_tree := PTree.t t. + + Definition find_tree (el: t) (h: hash_tree) : option hash := + match filter (fun x => if eq_dec el (snd x) then true else false) (PTree.elements h) with + | (p, _) :: nil => Some p + | _ => None + end. + + Definition hash_value (max: hash) (e: t) (h: hash_tree): hash * 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. + + Definition wf_hash_table h_tree := + forall x c, h_tree ! x = Some c -> find_tree c h_tree = Some x. + + Lemma find_tree_correct : + forall c h_tree p, + find_tree c h_tree = Some p -> + h_tree ! p = Some c. + Proof. + intros. + unfold find_tree in H. destruct_match; crush. + destruct_match; simplify. + destruct_match; crush. + assert (In (p, t0) (filter + (fun x : hash * t => + if eq_dec c (snd x) then true else false) (PTree.elements h_tree))). + { setoid_rewrite Heql. constructor; auto. } + apply filter_In in H. simplify. destruct_match; crush. subst. + apply PTree.elements_complete; auto. + Qed. + + Lemma find_tree_unique : + forall c h_tree p p', + find_tree c h_tree = Some p -> + h_tree ! p' = Some c -> + p = p'. + Proof. + intros. + unfold find_tree in H. + repeat (destruct_match; crush; []). + assert (In (p, t0) (filter + (fun x : hash * t => + if eq_dec c (snd x) then true else false) (PTree.elements h_tree))). + { setoid_rewrite Heql. constructor; auto. } + apply filter_In in H. simplify. + destruct (Pos.eq_dec p p'); auto. + exfalso. + destruct_match; subst; crush. + assert (In (p', t0) (PTree.elements h_tree) /\ (fun x : hash * t => + if eq_dec t0 (snd x) then true else false) (p', t0) = true). + { split. apply PTree.elements_correct. auto. setoid_rewrite Heqs. auto. } + apply filter_In in H. setoid_rewrite Heql in H. inv H. simplify. crush. crush. + Qed. + + Lemma hash_no_element' : + forall c h_tree, + find_tree c h_tree = None -> + wf_hash_table h_tree -> + ~ forall x, h_tree ! x = Some c. + Proof. + unfold not, wf_hash_table; intros. + specialize (H1 1). eapply H0 in H1. crush. + Qed. + + Lemma hash_no_element : + forall c h_tree, + find_tree c h_tree = None -> + wf_hash_table h_tree -> + ~ exists x, h_tree ! x = Some c. + Proof. + unfold not, wf_hash_table; intros. + simplify. apply H0 in H2. rewrite H in H2. crush. + Qed. + + Lemma wf_hash_table_set_gso' : + forall h x p0 c', + filter + (fun x : hash * t => + if eq_dec c' (snd x) then true else false) (PTree.elements h) = + (x, p0) :: nil -> + h ! x = Some p0 /\ p0 = c'. + Proof. + intros. + match goal with + | H: filter ?f ?el = ?x::?xs |- _ => + assert (In x (filter f el)) by (rewrite H; crush) + end. + apply filter_In in H0. simplify. destruct_match; subst; crush. + apply PTree.elements_complete; auto. + destruct_match; crush. + Qed. + + Lemma wf_hash_table_set_gso : + forall x x' c' c h, + x <> x' -> + wf_hash_table h -> + find_tree c' h = Some x -> + find_tree c h = None -> + find_tree c' (PTree.set x' c h) = Some x. + Proof. + intros. pose proof H1 as X. unfold find_tree in H1. + destruct_match; crush. + destruct p. destruct l; crush. + apply wf_hash_table_set_gso' in Heql. simplify. + pose proof H2 as Z. apply hash_no_element in H2; auto. + destruct (eq_dec c c'); subst. + { exfalso. eapply H2. econstructor; eauto. } + unfold wf_hash_table in H0. + assert (In (x', c) (PTree.elements (PTree.set x' c h))). + { apply PTree.elements_correct. rewrite PTree.gss; auto. } + assert (In (x, c') (PTree.elements h)). + { apply PTree.elements_correct; auto. } + assert (In (x, c') (PTree.elements (PTree.set x' c h))). + { apply PTree.elements_correct. rewrite PTree.gso; auto. } + pose proof X as Y. + unfold find_tree in X. repeat (destruct_match; crush; []). + match goal with + | H: filter ?f ?el = ?x::?xs |- _ => + assert (In x (filter f el)) by (rewrite H; crush) + end. + apply filter_In in H6. simplify. destruct_match; crush; subst. + unfold find_tree. repeat (destruct_match; crush). + { eapply filter_none in Heql0. + 2: { apply PTree.elements_correct. rewrite PTree.gso; eauto. } + destruct_match; crush. } + + { subst. + repeat match goal with + | H: filter ?f ?el = ?x::?xs |- _ => + learn H; assert (In x (filter f el)) by (rewrite H; crush) + end. + eapply filter_set in H10. rewrite Heql0 in H10. inv H10. simplify. auto. + inv H11. auto. inv H11. intros. eapply PTree_set_elements; auto. } + + { exfalso. subst. + repeat match goal with + | H: filter ?f ?el = ?x::?xs |- _ => + learn H; assert (In x (filter f el)) by (rewrite H; crush) + end. + + pose proof H8 as X2. destruct p1. + pose proof X2 as X4. + apply in_filter in X2. apply PTree.elements_complete in X2. + assert (In (p, t2) (filter + (fun x : positive * t => if eq_dec t0 (snd x) then true else false) + (PTree.elements (PTree.set x' c h)))) by (rewrite H6; eauto). + pose proof H11 as X3. + apply in_filter in H11. apply PTree.elements_complete in H11. + destruct (peq p0 p); subst. + { + assert (list_norepet (map fst (filter + (fun x : positive * t => if eq_dec t0 (snd x) then true else false) + (PTree.elements (PTree.set x' c h))))). + { eapply filter_norepet2. eapply PTree.elements_keys_norepet. } + rewrite Heql0 in H12. simplify. inv H12. eapply H15. apply in_eq. + } + { apply filter_In in X4. simplify. destruct_match; crush; subst. + apply filter_In in X3. simplify. destruct_match; crush; subst. + destruct (peq p x'); subst. + { rewrite PTree.gss in H11; crush. } + { destruct (peq p0 x'); subst. + { rewrite PTree.gss in X2; crush. } + { rewrite PTree.gso in X2 by auto. + rewrite PTree.gso in H11 by auto. + assert (p = p0) by (eapply find_tree_unique; eauto). + crush. } } } } + Qed. + + Lemma wf_hash_table_set : + forall h_tree c v (GT: v > max_key h_tree), + find_tree c h_tree = None -> + wf_hash_table h_tree -> + wf_hash_table (PTree.set v c h_tree). + Proof. + unfold wf_hash_table; simplify. + destruct (peq v x); subst. + pose proof (hash_no_element c h_tree H H0). + rewrite PTree.gss in H1. simplify. + unfold find_tree. + assert (In (x, c0) (PTree.elements (PTree.set x c0 h_tree)) + /\ (fun x : positive * t => if eq_dec c0 (snd x) then true else false) + (x, c0) = true). + { simplify. apply PTree.elements_correct. rewrite PTree.gss. auto. + destruct (eq_dec c0 c0); crush. } + destruct_match. + apply filter_In in H1. rewrite Heql in H1. crush. + apply filter_In in H1. repeat (destruct_match; crush; []). subst. + destruct l. simplify. rewrite Heql in H1. inv H1. inv H3. auto. + crush. + + exfalso. apply H2. destruct p. + pose proof Heql as X. apply filter_cons_true in X. destruct_match; crush; subst. + assert (In (p0, t0) (filter + (fun x : positive * t => if eq_dec t0 (snd x) then true else false) + (PTree.elements (PTree.set x t0 h_tree)))) by (rewrite Heql; eauto). + assert (In (p, t1) (filter + (fun x : positive * t => if eq_dec t0 (snd x) then true else false) + (PTree.elements (PTree.set x t0 h_tree)))) by (rewrite Heql; eauto). + apply filter_In in H4. simplify. destruct_match; crush; subst. + apply in_filter in H3. apply PTree.elements_complete in H5. apply PTree.elements_complete in H3. + assert (list_norepet (map fst (filter + (fun x : positive * t => if eq_dec t1 (snd x) then true else false) + (PTree.elements (PTree.set x t1 h_tree))))). + { eapply filter_norepet2. eapply PTree.elements_keys_norepet. } + rewrite Heql in H4. simplify. + destruct (peq p0 p); subst. + { inv H4. exfalso. eapply H8. eauto. } + destruct (peq x p); subst. + rewrite PTree.gso in H3; auto. econstructor; eauto. + rewrite PTree.gso in H5; auto. econstructor; eauto. + + rewrite PTree.gso in H1; auto. + destruct (eq_dec c c0); subst. + { apply H0 in H1. rewrite H in H1. discriminate. } + apply H0 in H1. + apply wf_hash_table_set_gso; eauto. + Qed. + + Lemma wf_hash_table_distr : + forall m p h_tree h h_tree', + hash_value m p h_tree = (h, h_tree') -> + wf_hash_table h_tree -> + wf_hash_table h_tree'. + Proof. + unfold hash_value; simplify. + destruct_match. + - inv H; auto. + - inv H. apply wf_hash_table_set; try lia; auto. + Qed. + + Lemma wf_hash_table_eq : + forall h_tree a b c, + wf_hash_table h_tree -> + h_tree ! a = Some c -> + h_tree ! b = Some c -> + a = b. + Proof. + unfold wf_hash_table; intros; apply H in H0; eapply find_tree_unique; eauto. + Qed. + + Lemma hash_constant : + forall p h h_tree hi c h_tree' m, + h_tree ! hi = Some c -> + hash_value m p h_tree = (h, h_tree') -> + h_tree' ! hi = Some c. + Proof. + intros. unfold hash_value in H0. destruct_match. + inv H0. eauto. + inv H0. + pose proof H. apply max_key_correct in H0. + rewrite PTree.gso; solve [eauto | lia]. + Qed. + +End HashTree. -- cgit