Skip to content

Commit f43fb41

Browse files
tahina-protahina-pro
committed
implement ArrayPtr with FStarLang/FStar#2349 
1 parent f2dcb46 commit f43fb41

File tree

4 files changed

+396
-5
lines changed

4 files changed

+396
-5
lines changed

Diff for: ‎src/lowparse/LowParse.SteelST.ArrayPtr.fsti

+4-4
Original file line numberDiff line numberDiff line change
@@ -131,16 +131,16 @@ val gsplit (#opened: _) (#a:Type) (#value: v a) (x: t a) (i:SZ.t)
131131
(fun _ -> True)
132132

133133
inline_for_extraction
134-
val split' (#opened: _) (#a:Type) (#vl #vr: v a) (x: t a) (i: SZ.t) (x': Ghost.erased (t a))
135-
: STAtomicBase (t a) false opened Unobservable
134+
val split' (#a:Type) (#vl #vr: v a) (x: t a) (i: SZ.t) (x': Ghost.erased (t a))
135+
: ST (t a)
136136
(arrayptr x vl `star` arrayptr x' vr)
137137
(fun res -> arrayptr x vl `star` arrayptr res vr)
138138
(adjacent (array_of vl) (array_of vr) /\ SZ.v i == length (array_of vl))
139139
(fun res -> res == Ghost.reveal x')
140140

141141
inline_for_extraction
142-
let split (#opened: _) (#a:Type) (#value: v a) (x: t a) (i:SZ.t)
143-
: STAtomicBase (t a) false opened Unobservable
142+
let split (#a:Type) (#value: v a) (x: t a) (i:SZ.t)
143+
: ST (t a)
144144
(arrayptr x value)
145145
(fun res -> exists_ (fun vl -> exists_ (fun vr ->
146146
arrayptr x vl `star` arrayptr res vr `star` pure (

Diff for: ‎src/lowparse/steel_array/LowParse.SteelST.ArrayPtr.fst

+1-1
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ let gsplit #_ #_ #v x i =
103103
rewrite (arrayptr0 res vr) (arrayptr res vr);
104104
res
105105

106-
let split' #_ #_ #vl #vr x i x' =
106+
let split' #_ #vl #vr x i x' =
107107
rewrite (arrayptr x vl) (arrayptr0 x vl);
108108
rewrite (arrayptr x' vr) (arrayptr0 x' vr);
109109
let _ = gen_elim () in

Diff for: ‎src/lowparse/steel_c_array/LowParse.SteelST.ArrayPtr.fst

+337
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,337 @@
1+
module LowParse.SteelST.ArrayPtr
2+
module STC = Steel.ST.C.Types
3+
4+
let t elt = STC.array_ptr (STC.scalar elt)
5+
6+
[@@erasable]
7+
noeq
8+
type array elt = {
9+
array_ptr: STC.array (STC.scalar elt);
10+
array_perm: Steel.FractionalPermission.perm;
11+
// array_base_len: (len: SZ.t { SZ.v len == SA.base_len (STC.base (STC.array_ptr_of array_ptr)) });
12+
}
13+
14+
let len x = SZ.uint_to_t (STC.array_length x.array_ptr)
15+
16+
let array_perm x = x.array_perm
17+
18+
[@@erasable]
19+
noeq
20+
type v t = {
21+
v_array: array t;
22+
v_contents: Seq.lseq t (length v_array);
23+
}
24+
25+
let array_of x = x.v_array
26+
let contents_of x = x.v_contents
27+
28+
let array_contents_inj _ _ = ()
29+
30+
let mk_full_scalar_seq_index (#t: Type) (s: Seq.seq t) (i: nat { i < Seq.length s }) : GTot (STC.scalar_t t) =
31+
STC.mk_scalar (Seq.index s i)
32+
33+
let mk_full_scalar_seq (#t: Type) (s: Seq.seq t) : GTot (Seq.seq (STC.scalar_t t)) =
34+
Seq.init_ghost (Seq.length s) (mk_full_scalar_seq_index s)
35+
36+
let mk_scalar_seq (#t: Type) (p: perm) (s: Seq.seq t) : GTot (Seq.seq (STC.scalar_t t)) =
37+
STC.mk_fraction_seq (STC.scalar t) (mk_full_scalar_seq s) p
38+
39+
[@__reduce__]
40+
let arrayptr1 (#elt: _) (v: v elt) (s: Ghost.erased (Seq.seq (STC.scalar_t elt))) : Tot vprop =
41+
STC.array_pts_to v.v_array.array_ptr s
42+
43+
[@__reduce__]
44+
let arrayptr0 (#elt: _) (r: t elt) (v: v elt) : Tot vprop =
45+
exists_ (fun s ->
46+
arrayptr1 v s `star` pure (
47+
Ghost.reveal s `Seq.equal` mk_scalar_seq v.v_array.array_perm v.v_contents /\
48+
STC.array_ptr_of v.v_array.array_ptr == r /\
49+
(Seq.length v.v_contents > 0 ==> v.v_array.array_perm `lesser_equal_perm` full_perm)
50+
))
51+
52+
let arrayptr r v = arrayptr0 r v
53+
54+
let adjacent x1 x2 =
55+
x1.array_perm == x2.array_perm /\
56+
STC.array_ptr_of x2.array_ptr == STC.array_ref_shift (STC.array_ptr_of x1.array_ptr) (len x1)
57+
58+
let merge x1 x2 = {
59+
array_ptr = (| STC.array_ptr_of x1.array_ptr, Ghost.hide (len x1 `SZ.add` len x2) |);
60+
array_perm = x1.array_perm;
61+
// array_base_len = x1.array_base_len;
62+
}
63+
64+
let merge_assoc x1 x2 x3 =
65+
STC.array_ref_shift_assoc (STC.array_ptr_of x1.array_ptr) (len x1) (len x2)
66+
67+
let join #_ #a #vl #vr al ar =
68+
rewrite (arrayptr al vl) (arrayptr0 al vl);
69+
rewrite (arrayptr ar vr) (arrayptr0 ar vr);
70+
let _ = gen_elim () in
71+
let res = {
72+
v_array = merge (array_of vl) (array_of vr);
73+
v_contents = Seq.append vl.v_contents vr.v_contents;
74+
}
75+
in
76+
STC.array_join res.v_array.array_ptr vl.v_array.array_ptr vr.v_array.array_ptr (len (array_of vl));
77+
rewrite (arrayptr0 al res) (arrayptr al res);
78+
res
79+
80+
unfold
81+
let gsplit_post
82+
(#a:Type) (value: v a) (x: t a) (i:SZ.t)
83+
(res: t a)
84+
(vl vr: v a)
85+
: GTot prop
86+
=
87+
SZ.v i <= length (array_of value) /\
88+
merge_into (array_of vl) (array_of vr) (array_of value) /\
89+
contents_of' vl `Seq.equal` seq_slice (contents_of' value) 0 (SZ.v i) /\
90+
length (array_of vl) == SZ.v i /\
91+
length (array_of vr) == length (array_of value) - SZ.v i /\
92+
contents_of' vr `Seq.equal` seq_slice (contents_of' value) (SZ.v i) (length (array_of value)) /\
93+
contents_of' value `Seq.equal` (contents_of' vl `Seq.append` contents_of' vr) /\
94+
(SZ.v i == 0 ==> Ghost.reveal res == x)
95+
96+
let gsplit #_ #_ #v x i =
97+
rewrite (arrayptr x v) (arrayptr0 x v);
98+
let _ = gen_elim () in
99+
let _ = STC.ghost_array_split _ i in
100+
let vl_array = {
101+
array_ptr = STC.array_split_l v.v_array.array_ptr i;
102+
array_perm = v.v_array.array_perm;
103+
// array_base_len = v.v_array.array_base_len;
104+
}
105+
in
106+
let vl = {
107+
v_array = vl_array;
108+
v_contents = Seq.slice v.v_contents 0 (SZ.v i);
109+
}
110+
in
111+
let vr_array = {
112+
array_ptr = STC.array_split_r v.v_array.array_ptr i;
113+
array_perm = v.v_array.array_perm;
114+
// array_base_len = v.v_array.array_base_len;
115+
}
116+
in
117+
let vr = {
118+
v_array = vr_array;
119+
v_contents = Seq.slice v.v_contents (SZ.v i) (Seq.length v.v_contents);
120+
}
121+
in
122+
let res = Ghost.hide (STC.array_ptr_of vr_array.array_ptr) in
123+
STC.array_ref_shift_zero x;
124+
let s = vpattern_replace (STC.array_pts_to (STC.array_split_l _ _)) in
125+
rewrite (STC.array_pts_to (STC.array_split_l _ _) _) (arrayptr1 vl s);
126+
rewrite (arrayptr0 x vl) (arrayptr x vl);
127+
let s = vpattern_replace (STC.array_pts_to _) in
128+
rewrite (STC.array_pts_to _ _) (arrayptr1 vr s);
129+
rewrite (arrayptr0 res vr) (arrayptr res vr);
130+
assert (gsplit_post v x i res vl vr);
131+
noop ();
132+
res
133+
134+
inline_for_extraction [@@noextract_to "krml"]
135+
let stc_array_ref_split
136+
(#t: Type)
137+
(#td: STC.typedef t)
138+
(#s: Ghost.erased (Seq.seq t))
139+
(al: STC.array_ref td)
140+
(len: STC.array_len_t al)
141+
(aa aal aar: Ghost.erased (STC.array td))
142+
(i: SZ.t)
143+
: ST (_: STC.array_ref td { SZ.v i <= SZ.v len /\ Seq.length s == SZ.v len})
144+
(STC.array_pts_to aa s)
145+
(fun _ -> STC.array_pts_to aal (Seq.slice s 0 (SZ.v i)) `star`
146+
STC.array_pts_to aar (Seq.slice s (SZ.v i) (Seq.length s)))
147+
(SZ.v i <= SZ.v len /\
148+
Ghost.reveal aa == (| al, len |) /\
149+
Ghost.reveal aal == STC.array_split_l aa i /\
150+
Ghost.reveal aar == STC.array_split_r aa i
151+
)
152+
(fun ar ->
153+
Ghost.reveal aa == (| al, len |) /\
154+
ar == STC.array_ptr_of (STC.array_split_r aa i)
155+
)
156+
= rewrite (STC.array_pts_to aa s) (STC.array_pts_to (| al, len |) s);
157+
let res = STC.array_ref_split al len i in
158+
vpattern_rewrite (fun a -> STC.array_pts_to a _ `star` STC.array_pts_to (STC.array_split_r _ _) _) aal;
159+
vpattern_rewrite (fun a -> STC.array_pts_to aal _ `star` STC.array_pts_to a _) aar;
160+
return res
161+
162+
let split' #elt #vl #vr x i x' =
163+
rewrite (arrayptr x' vr) (arrayptr0 x' vr);
164+
let _ = gen_elim () in
165+
rewrite (arrayptr0 x' vr) (arrayptr x' vr);
166+
let vm = join x x' in
167+
rewrite (arrayptr x vm) (arrayptr0 x vm);
168+
let _ = gen_elim () in
169+
let res : t elt = stc_array_ref_split x (len vm.v_array) _ vl.v_array.array_ptr vr.v_array.array_ptr i in
170+
noop ();
171+
rewrite (arrayptr0 x vl) (arrayptr x vl);
172+
noop ();
173+
rewrite (arrayptr0 res vr) (arrayptr res vr);
174+
return res
175+
176+
let index #t #v r i =
177+
rewrite (arrayptr r v) (arrayptr0 r v);
178+
let _ = gen_elim () in
179+
[@@inline_let]
180+
let a : STC.array (STC.scalar t) = (| r, Ghost.hide (len v.v_array) |) in
181+
let s = vpattern_replace (STC.array_pts_to _) in
182+
vpattern_rewrite (fun a -> STC.array_pts_to a _) a;
183+
let p = STC.array_cell a i in
184+
let res = STC.read p in
185+
let _ = STC.unarray_cell a i p in
186+
drop (STC.has_array_cell _ _ _);
187+
rewrite (STC.array_pts_to _ _) (arrayptr1 v s);
188+
rewrite (arrayptr0 r v) (arrayptr r v);
189+
return res
190+
191+
let upd #elt #v r i x =
192+
rewrite (arrayptr r v) (arrayptr0 r v);
193+
let _ = gen_elim () in
194+
[@@inline_let]
195+
let a : STC.array (STC.scalar elt) = (| r, Ghost.hide (len v.v_array) |) in
196+
vpattern_rewrite (fun a -> STC.array_pts_to a _) a;
197+
let p = STC.array_cell a i in
198+
STC.write p x;
199+
let _ = STC.unarray_cell a i p in
200+
drop (STC.has_array_cell _ _ _);
201+
let s' = vpattern_replace (STC.array_pts_to _) in
202+
let res = {
203+
v_array = v.v_array;
204+
v_contents = Seq.upd v.v_contents (SZ.v i) x;
205+
}
206+
in
207+
rewrite (STC.array_pts_to _ _) (arrayptr1 res s');
208+
rewrite (arrayptr0 r res) (arrayptr r res);
209+
return res
210+
211+
let set_array_perm
212+
(#t: Type)
213+
(a: array t)
214+
(p: perm)
215+
: Ghost (array t)
216+
(requires True)
217+
(ensures (fun y -> len y == len a /\ array_perm y == p))
218+
= {
219+
a with array_perm = p
220+
}
221+
222+
let set_array_perm_idem
223+
(#t: Type)
224+
(a: array t)
225+
(p1 p2: perm)
226+
: Lemma
227+
(set_array_perm (set_array_perm a p1) p2 == set_array_perm a p2)
228+
= ()
229+
230+
let set_array_perm_eq
231+
(#t: Type)
232+
(a: array t)
233+
: Lemma
234+
(set_array_perm a (array_perm a) == a)
235+
= ()
236+
237+
let set_array_perm_adjacent
238+
(#t: Type)
239+
(a1 a2: array t)
240+
(p: perm)
241+
: Lemma
242+
(requires (adjacent a1 a2))
243+
(ensures (
244+
merge_into (set_array_perm a1 p) (set_array_perm a2 p) (set_array_perm (merge a1 a2) p)
245+
))
246+
= ()
247+
248+
#set-options "--ide_id_info_off"
249+
250+
let share
251+
(#opened: _)
252+
(#elt: Type)
253+
(#x: v elt)
254+
(a: t elt)
255+
(p1 p2: perm)
256+
: STGhost (Ghost.erased (v elt & v elt)) opened
257+
(arrayptr a x)
258+
(fun res -> arrayptr a (fst res) `star` arrayptr a (snd res))
259+
(array_perm (array_of x) == p1 `Steel.FractionalPermission.sum_perm` p2)
260+
(fun res ->
261+
contents_of' (fst res) == contents_of x /\
262+
contents_of' (snd res) == contents_of x /\
263+
array_of (fst res) == set_array_perm (array_of x) p1 /\
264+
array_of (snd res) == set_array_perm (array_of x) p2
265+
)
266+
=
267+
rewrite (arrayptr a x) (arrayptr0 a x);
268+
let _ = gen_elim () in
269+
vpattern_rewrite (STC.array_pts_to _) _;
270+
STC.mk_fraction_seq_split_gen _ (mk_full_scalar_seq x.v_contents) x.v_array.array_perm p1 p2;
271+
let res1 = {
272+
v_array = set_array_perm x.v_array p1;
273+
v_contents = x.v_contents;
274+
}
275+
in
276+
let res2 = {
277+
v_array = set_array_perm x.v_array p2;
278+
v_contents = x.v_contents;
279+
}
280+
in
281+
let res = Ghost.hide (res1, res2) in
282+
let s = vpattern_replace (fun s -> STC.array_pts_to _ s `star` STC.array_pts_to _ (STC.mk_fraction_seq _ _ p2)) in
283+
rewrite (STC.array_pts_to _ s) (arrayptr1 (fst res) s);
284+
rewrite (arrayptr0 a (fst res)) (arrayptr a (fst res));
285+
let s = vpattern_replace (STC.array_pts_to _) in
286+
rewrite (STC.array_pts_to _ _) (arrayptr1 (snd res) s);
287+
rewrite (arrayptr0 a (snd res)) (arrayptr a (snd res));
288+
res
289+
290+
let gather
291+
(#opened: _)
292+
(#elt: Type)
293+
(#x1 #x2: v elt)
294+
(a: t elt)
295+
: STGhost (v elt) opened
296+
(arrayptr a x1 `star` arrayptr a x2)
297+
(fun res -> arrayptr a res)
298+
(array_of x1 == set_array_perm (array_of x2) (array_perm (array_of x1)))
299+
(fun res ->
300+
contents_of' res == contents_of x1 /\
301+
contents_of' res == contents_of x2 /\
302+
array_of res == set_array_perm (array_of x1) (array_perm (array_of x1) `Steel.FractionalPermission.sum_perm` array_perm (array_of x2))
303+
)
304+
= rewrite (arrayptr a x1) (arrayptr0 a x1);
305+
let _ = gen_elim () in
306+
rewrite (STC.array_pts_to _ _) (STC.array_pts_to x1.v_array.array_ptr (STC.mk_fraction_seq (STC.scalar elt) (mk_full_scalar_seq x1.v_contents) x1.v_array.array_perm));
307+
rewrite (arrayptr a x2) (arrayptr0 a x2);
308+
let _ = gen_elim () in
309+
rewrite
310+
(STC.array_pts_to x2.v_array.array_ptr _)
311+
(STC.array_pts_to x1.v_array.array_ptr (STC.mk_fraction_seq (STC.scalar elt) (mk_full_scalar_seq x2.v_contents) x2.v_array.array_perm));
312+
STC.array_fractional_permissions_theorem (mk_full_scalar_seq x1.v_contents) (mk_full_scalar_seq x2.v_contents) x1.v_array.array_perm x2.v_array.array_perm x1.v_array.array_ptr;
313+
rewrite
314+
(STC.array_pts_to x1.v_array.array_ptr (STC.mk_fraction_seq (STC.scalar elt) (mk_full_scalar_seq x2.v_contents) x2.v_array.array_perm))
315+
(STC.array_pts_to x1.v_array.array_ptr (STC.mk_fraction_seq (STC.scalar elt) (mk_full_scalar_seq x1.v_contents) x2.v_array.array_perm));
316+
STC.mk_fraction_seq_join x1.v_array.array_ptr (mk_full_scalar_seq x1.v_contents) x1.v_array.array_perm x2.v_array.array_perm;
317+
let s = vpattern_replace (STC.array_pts_to _) in
318+
let res = {
319+
v_array = set_array_perm x1.v_array (x1.v_array.array_perm `Steel.FractionalPermission.sum_perm` x2.v_array.array_perm);
320+
v_contents = x1.v_contents;
321+
}
322+
in
323+
let prf
324+
(i: nat)
325+
: Lemma
326+
(requires (i < length x1.v_array))
327+
(ensures (
328+
i < length x1.v_array /\
329+
Seq.index x1.v_contents i == Seq.index x2.v_contents i
330+
))
331+
= STC.mk_scalar_inj (Seq.index x1.v_contents i) (Seq.index x2.v_contents i) full_perm full_perm
332+
in
333+
Classical.forall_intro (Classical.move_requires prf);
334+
assert (x2.v_contents `Seq.equal` x1.v_contents);
335+
rewrite (STC.array_pts_to _ _) (arrayptr1 res s);
336+
rewrite (arrayptr0 a res) (arrayptr a res);
337+
res

0 commit comments

Comments
 (0)