diff options
Diffstat (limited to 'mppa_k1c/abstractbb/Impure/ImpHCons.v')
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpHCons.v | 104 |
1 files changed, 82 insertions, 22 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpHCons.v b/mppa_k1c/abstractbb/Impure/ImpHCons.v index dd615628..d8002375 100644 --- a/mppa_k1c/abstractbb/Impure/ImpHCons.v +++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v @@ -99,41 +99,101 @@ Hint Resolve assert_list_incl_correct. End Sets. + + + (********************************) (* (Weak) HConsing *) +Module HConsing. -Axiom xhCons: forall {A}, ((A -> A -> ?? bool) * (pre_hashV A -> ?? hashV A)) -> ?? hashConsing A. +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_eq_msg: pstring := "xhCons: hash eq differs". -Definition hCons {A} (hash_eq: A -> A -> ?? bool) (unknownHash_msg: pre_hashV A -> ?? pstring): ?? (hashConsing A) := - DO hco <~ xhCons (hash_eq, fun v => DO s <~ unknownHash_msg v ;; FAILWITH s) ;; +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 (pre_data x) (data x') ;; - assert_b b0 hCons_eq_msg;; - RET x'; - hC_known := fun x => - DO x' <~ hC_known hco x ;; - DO b0 <~ hash_eq (pre_data x) (data x') ;; - assert_b b0 hCons_eq_msg;; - RET x'; - next_log := next_log hco; - export := export hco; + 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: forall A (hash_eq: A -> A -> ?? bool) msg, - WHEN hCons hash_eq msg ~> hco THEN - ((forall x y, WHEN hash_eq x y ~> b THEN b=true -> x=y) -> forall x, WHEN hC hco x ~> x' THEN (pre_data x)=(data x')) - /\ ((forall x y, WHEN hash_eq x y ~> b THEN b=true -> x=y) -> forall x, WHEN hC_known hco x ~> x' THEN (pre_data x)=(data x')). + +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. -Definition hCons_spec {A} (hco: hashConsing A) := - (forall x, WHEN hC hco x ~> x' THEN (pre_data x)=(data x')) /\ (forall x, WHEN hC_known hco x ~> x' THEN (pre_data x)=(data x')). + + +(* 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. + 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. |