diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:25:31 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:25:31 +0100 |
commit | 73a83b969dbb6f4c419ebdcc663f463509b6d6e3 (patch) | |
tree | 259852cd3272f2f31a09d75ac24e31ec1aaa8d9e /lib/Impure/ImpHCons.v | |
parent | 3570ba2827908b280315c922ba7e43289f6d802a (diff) | |
parent | 035a1a9f4b636206acbae4506c5fc4ef322de0c1 (diff) | |
download | compcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.tar.gz compcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.zip |
Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3
Diffstat (limited to 'lib/Impure/ImpHCons.v')
-rw-r--r-- | lib/Impure/ImpHCons.v | 199 |
1 files changed, 199 insertions, 0 deletions
diff --git a/lib/Impure/ImpHCons.v b/lib/Impure/ImpHCons.v new file mode 100644 index 00000000..637116cc --- /dev/null +++ b/lib/Impure/ImpHCons.v @@ -0,0 +1,199 @@ +Require Export ImpIO. + +Import Notations. +Local Open Scope impure. + + +Axiom string_of_hashcode: hashcode -> ?? caml_string. +Extract Constant string_of_hashcode => "string_of_int". + +Axiom hash: forall {A}, A -> ?? hashcode. +Extract Constant hash => "Hashtbl.hash". + +(**************************) +(* (Weak) Sets *) + + +Import Dict. + +Axiom make_dict: forall {A B}, (hash_params A) -> ?? Dict.t A B. +Extract Constant make_dict => "ImpHConsOracles.make_dict". + + +Module Sets. + +Definition t {A} (mod: A -> Prop) := Dict.t A {x | mod x}. + +Definition empty {A} (hp: hash_params A) {mod:A -> Prop}: ?? t mod := + make_dict hp. + +Program Fixpoint add {A} (l: list A) {mod: A -> Prop} (d: t mod): forall {H:forall x, List.In x l -> mod x}, ?? unit := + match l with + | nil => fun H => RET () + | x::l' => fun H => + d.(set)(x,x);; + add l' d + end. + +Program Definition create {A} (hp: hash_params A) (l:list A): ?? t (fun x => List.In x l) := + DO d <~ empty hp (mod:=fun x => List.In x l);; + add l (mod:=fun x => List.In x l) d (H:=_);; + RET d. +Global Opaque create. + +Definition is_present {A} (hp: hash_params A) (x:A) {mod} (d:t mod): ?? bool := + DO oy <~ (d.(get)) x;; + match oy with + | Some y => hp.(test_eq) x (`y) + | None => RET false + end. + +Local Hint Resolve test_eq_correct: wlp. + +Lemma is_present_correct A (hp: hash_params A) x mod (d:t mod): + WHEN is_present hp x d ~> b THEN b=true -> mod x. +Proof. + wlp_simplify; subst; eauto. + - apply proj2_sig. + - discriminate. +Qed. +Hint Resolve is_present_correct: wlp. +Global Opaque is_present. + +Definition msg_assert_incl: pstring := "Sets.assert_incl". + +Fixpoint assert_incl {A} (hp: hash_params A) (l: list A) {mod} (d:t mod): ?? unit := + match l with + | nil => RET () + | x::l' => + DO b <~ is_present hp x d;; + if b then + assert_incl hp l' d + else ( + hp.(log) x;; + FAILWITH msg_assert_incl + ) + end. + +Lemma assert_incl_correct A (hp: hash_params A) l mod (d:t mod): + WHEN assert_incl hp l d ~> _ THEN forall x, List.In x l -> mod x. +Proof. + induction l; wlp_simplify; subst; eauto. +Qed. +Hint Resolve assert_incl_correct: wlp. +Global Opaque assert_incl. + +Definition assert_list_incl {A} (hp: hash_params A) (l1 l2: list A): ?? unit := + (* println "";;print("dict_create ");;*) + DO d <~ create hp l2;; + (*print("assert_incl ");;*) + assert_incl hp l1 d. + +Lemma assert_list_incl_correct A (hp: hash_params A) l1 l2: + WHEN assert_list_incl hp l1 l2 ~> _ THEN List.incl l1 l2. +Proof. + wlp_simplify. +Qed. +Global Opaque assert_list_incl. +Hint Resolve assert_list_incl_correct: wlp. + +End Sets. + + + + +(********************************) +(* (Weak) HConsing *) + +Module HConsing. + +Export HConsingDefs. + +(* NB: this axiom is NOT intended to be called directly, but only through [hCons...] functions below. *) +Axiom xhCons: forall {A}, (hashP A) -> ?? hashConsing A. +Extract Constant xhCons => "ImpHConsOracles.xhCons". + +Definition hCons_eq_msg: pstring := "xhCons: hash eq differs". + +Definition hCons {A} (hp: hashP A): ?? (hashConsing A) := + DO hco <~ xhCons hp ;; + RET {| + hC := (fun x => + DO x' <~ hC hco x ;; + DO b0 <~ hash_eq hp x.(hdata) x' ;; + assert_b b0 hCons_eq_msg;; + RET x'); + next_hid := hco.(next_hid); + next_log := hco.(next_log); + export := hco.(export); + remove := hco.(remove) + |}. + + +Lemma hCons_correct A (hp: hashP A): + WHEN hCons hp ~> hco THEN + (forall x y, WHEN hp.(hash_eq) x y ~> b THEN b=true -> (ignore_hid hp x)=(ignore_hid hp y)) -> + forall x, WHEN hco.(hC) x ~> x' THEN ignore_hid hp x.(hdata)=ignore_hid hp x'. +Proof. + wlp_simplify. +Qed. +Global Opaque hCons. +Hint Resolve hCons_correct: wlp. + + + +(* hashV: extending a given type with hash-consing *) +Record hashV {A:Type}:= { + data: A; + hid: hashcode +}. +Arguments hashV: clear implicits. + +Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashP (hashV A) := {| + hash_eq := fun v1 v2 => test_eq v1.(data) v2.(data); + get_hid := hid; + set_hid := fun v id => {| data := v.(data); hid := id |} +|}. + +Definition liftHV (x:nat) := {| data := x; hid := unknown_hid |}. + +Definition hConsV {A} (hasheq: A -> A -> ?? bool): ?? (hashConsing (hashV A)) := + hCons (hashV_C hasheq). + +Lemma hConsV_correct A (hasheq: A -> A -> ?? bool): + WHEN hConsV hasheq ~> hco THEN + (forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) -> + forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data). +Proof. + Local Hint Resolve f_equal2: core. + wlp_simplify. + exploit H; eauto. + + wlp_simplify. + + intros; congruence. +Qed. +Global Opaque hConsV. +Hint Resolve hConsV_correct: wlp. + +Definition hC_known {A} (hco:hashConsing (hashV A)) (unknownHash_msg: hashinfo (hashV A) -> ?? pstring) (x:hashinfo (hashV A)): ?? hashV A := + DO clock <~ hco.(next_hid)();; + DO x' <~ hco.(hC) x;; + DO ok <~ hash_older x'.(hid) clock;; + if ok + then RET x' + else + hco.(remove) x;; + DO msg <~ unknownHash_msg x;; + FAILWITH msg. + +Lemma hC_known_correct A (hco:hashConsing (hashV A)) msg x: + WHEN hC_known hco msg x ~> x' THEN + (forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data)) -> + x.(hdata).(data)=x'.(data). +Proof. + wlp_simplify. + unfold wlp in * |- ; eauto. +Qed. +Global Opaque hC_known. +Hint Resolve hC_known_correct: wlp. + +End HConsing. |