blob: 307eb163190027335dab49024b82db87caf0e23a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
Require Export ImpIO.
Import Notations.
Local Open Scope impure.
(********************************)
(* (Weak) HConsing *)
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".
Axiom xhCons: forall {A}, ((A -> A -> ?? bool) * (pre_hashV A -> ?? hashV A)) -> ?? hashConsing A.
Extract Constant xhCons => "ImpHConsOracles.xhCons".
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) ;;
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;
|}.
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')).
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')).
|
