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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
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.
|
