Skip to content

Commit 330ab36

Browse files
gebnergebner
authored
Merge pull request #225 from FStarLang/_taramana_slice
A model for Rust slices (and C array pointers)
2 parents 243e8f9 + 40664bc commit 330ab36

18 files changed

+1251
-51
lines changed

‎lib/pulse/lib/Pulse.Lib.Array.Core.fst

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -362,7 +362,6 @@ ensures post
362362
free arr
363363
}
364364

365-
```pulse
366365
ghost
367366
fn pts_to_range_share
368367
(#a:Type)
@@ -378,9 +377,7 @@ fn pts_to_range_share
378377
fold (pts_to_range arr l r #(p /. 2.0R) s);
379378
fold (pts_to_range arr l r #(p /. 2.0R) s);
380379
}
381-
```
382380

383-
```pulse
384381
ghost
385382
fn pts_to_range_gather
386383
(#a:Type)
@@ -396,7 +393,6 @@ fn pts_to_range_gather
396393
H.pts_to_range_gather arr;
397394
fold (pts_to_range arr l r #(p0 +. p1) s0)
398395
}
399-
```
400396

401397

402398
(* this is universe-polymorphic in ret_t; so can't define it in Pulse yet *)

‎lib/pulse/lib/Pulse.Lib.ArrayPtr.fst

Lines changed: 232 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,232 @@
1+
(*
2+
Copyright 2024 Microsoft Research
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
http://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
*)
16+
17+
module Pulse.Lib.ArrayPtr
18+
#lang-pulse
19+
20+
noeq
21+
type ptr t = {
22+
base: A.array t;
23+
offset: (offset: SZ.t { SZ.v offset <= A.length base})
24+
}
25+
26+
let base a = a.base
27+
let offset a = SZ.v a.offset
28+
29+
instance has_pts_to_array_ptr t = {
30+
pts_to = (fun s #p v ->
31+
A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v)
32+
}
33+
34+
ghost fn unfold_pts_to #t (s: ptr t) #p v
35+
requires pts_to s #p v
36+
ensures A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v
37+
{
38+
rewrite pts_to s #p v as
39+
A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v
40+
}
41+
42+
ghost fn fold_pts_to #t (s: ptr t) #p v
43+
requires A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v
44+
ensures pts_to s #p v
45+
{
46+
rewrite
47+
A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v
48+
as pts_to s #p v
49+
}
50+
51+
let pts_to_is_slprop2 x p s = ()
52+
53+
let is_from_array s sz a =
54+
pure (sz == A.length a /\ s.base == a)
55+
56+
fn from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
57+
requires A.pts_to a #p v
58+
returns s: ptr t
59+
ensures pts_to s #p v ** is_from_array s (Seq.length v) a
60+
{
61+
A.pts_to_len a;
62+
let res = {
63+
base = a;
64+
offset = 0sz;
65+
};
66+
fold (is_from_array res (Seq.length v) a);
67+
A.pts_to_range_intro a p v;
68+
rewrite (A.pts_to_range a 0 (A.length a) #p v)
69+
as (A.pts_to_range res.base (SZ.v res.offset) (SZ.v res.offset + Seq.length v) #p v);
70+
fold_pts_to res #p v;
71+
res
72+
}
73+
74+
ghost
75+
fn to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#v: Seq.seq t)
76+
requires pts_to s #p v ** is_from_array s (Seq.length v) a
77+
ensures A.pts_to a #p v
78+
{
79+
unfold is_from_array s (Seq.length v) a;
80+
unfold_pts_to s #p v;
81+
A.pts_to_range_prop s.base;
82+
rewrite (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v)
83+
as (A.pts_to_range a 0 (A.length a) #p v);
84+
A.pts_to_range_elim a _ _;
85+
}
86+
87+
fn op_Array_Access
88+
(#t: Type)
89+
(a: ptr t)
90+
(i: SZ.t)
91+
(#p: perm)
92+
(#s: Ghost.erased (Seq.seq t))
93+
requires
94+
pts_to a #p s ** pure (SZ.v i < Seq.length s)
95+
returns res: t
96+
ensures
97+
pts_to a #p s **
98+
pure (
99+
SZ.v i < Seq.length s /\
100+
res == Seq.index s (SZ.v i))
101+
{
102+
unfold_pts_to a #p s;
103+
A.pts_to_range_prop a.base;
104+
let res = A.pts_to_range_index a.base (SZ.add a.offset i);
105+
fold_pts_to a #p s;
106+
res
107+
}
108+
109+
fn op_Array_Assignment
110+
(#t: Type)
111+
(a: ptr t)
112+
(i: SZ.t)
113+
(v: t)
114+
(#s: Ghost.erased (Seq.seq t))
115+
requires
116+
pts_to a s ** pure (SZ.v i < Seq.length s)
117+
ensures exists* s' .
118+
pts_to a s' **
119+
pure (SZ.v i < Seq.length s /\
120+
s' == Seq.upd s (SZ.v i) v
121+
)
122+
{
123+
unfold_pts_to a s;
124+
A.pts_to_range_prop a.base;
125+
let res = A.pts_to_range_upd a.base (SZ.add a.offset i) v;
126+
fold_pts_to a (Seq.upd s (SZ.v i) v);
127+
}
128+
129+
ghost
130+
fn share
131+
(#a:Type)
132+
(arr:ptr a)
133+
(#s:Ghost.erased (Seq.seq a))
134+
(#p:perm)
135+
requires pts_to arr #p s
136+
ensures pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s
137+
{
138+
unfold_pts_to arr #p s;
139+
A.pts_to_range_share arr.base;
140+
fold_pts_to arr #(p /. 2.0R) s;
141+
fold_pts_to arr #(p /. 2.0R) s;
142+
}
143+
144+
ghost
145+
fn gather
146+
(#a:Type)
147+
(arr:ptr a)
148+
(#s0 #s1:Ghost.erased (Seq.seq a))
149+
(#p0 #p1:perm)
150+
requires pts_to arr #p0 s0 ** pts_to arr #p1 s1 ** pure (Seq.length s0 == Seq.length s1)
151+
ensures pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1)
152+
{
153+
unfold_pts_to arr #p0 s0;
154+
unfold_pts_to arr #p1 s1;
155+
A.pts_to_range_gather arr.base;
156+
fold_pts_to arr #(p0 +. p1) s0
157+
}
158+
159+
fn split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t { SZ.v i <= Seq.length v })
160+
requires pts_to s #p v
161+
returns s' : ptr t
162+
ensures
163+
pts_to s #p (Seq.slice v 0 (SZ.v i)) **
164+
pts_to s' #p (Seq.slice v (SZ.v i) (Seq.length v)) **
165+
pure (adjacent s (SZ.v i) s')
166+
{
167+
unfold_pts_to s #p v;
168+
A.pts_to_range_prop s.base;
169+
let s' = {
170+
base = s.base;
171+
offset = SZ.add s.offset i;
172+
};
173+
A.pts_to_range_split s.base _ (SZ.v s'.offset) _;
174+
with s1. assert A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1;
175+
rewrite
176+
(A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1)
177+
as (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v i) #p s1);
178+
fold_pts_to s #p s1;
179+
with s2. assert A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2;
180+
rewrite
181+
(A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2)
182+
as (A.pts_to_range s'.base (SZ.v s'.offset) (SZ.v s'.offset + Seq.length s2) #p s2);
183+
fold_pts_to s' #p s2;
184+
s'
185+
}
186+
187+
ghost
188+
fn join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq.seq t)
189+
requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2)
190+
ensures pts_to s1 #p (Seq.append v1 v2)
191+
{
192+
unfold_pts_to s1 #p v1;
193+
unfold_pts_to s2 #p v2;
194+
rewrite (A.pts_to_range s2.base (SZ.v s2.offset) (SZ.v s2.offset + Seq.length v2) #p v2)
195+
as (A.pts_to_range s1.base (SZ.v s1.offset + Seq.length v1) (SZ.v s1.offset + Seq.length v1 + Seq.length v2) #p v2);
196+
A.pts_to_range_join s1.base (SZ.v s1.offset) (SZ.v s1.offset + Seq.length v1) (SZ.v s1.offset + Seq.length v1 + Seq.length v2);
197+
fold_pts_to s1 #p (Seq.append v1 v2)
198+
}
199+
200+
module R = Pulse.Lib.Reference
201+
202+
fn memcpy
203+
(#t:Type0) (#p0:perm)
204+
(src:ptr t) (idx_src: SZ.t)
205+
(dst:ptr t) (idx_dst: SZ.t)
206+
(len: SZ.t)
207+
(#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 })
208+
(#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 })
209+
requires pts_to src #p0 s0 ** pts_to dst s1
210+
ensures pts_to src #p0 s0 **
211+
pts_to dst (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1))
212+
{
213+
let mut i = 0sz;
214+
while (let vi = !i; SZ.lt vi len)
215+
invariant b. exists* s1' vi.
216+
R.pts_to i vi **
217+
pts_to src #p0 s0 **
218+
pts_to dst s1' **
219+
pure (b == SZ.lt vi len /\ SZ.lte vi len /\
220+
Seq.length s1' == Seq.length s1 /\
221+
forall (j:nat). j < Seq.length s1' ==>
222+
Seq.index s1' j == (if j < SZ.v vi then Seq.index s0 j else Seq.index s1 j))
223+
{
224+
let vi = !i;
225+
let x = src.(vi);
226+
dst.(vi) <- x;
227+
i := SZ.add vi 1sz;
228+
};
229+
with s1'. assert pts_to dst s1';
230+
assert pure (s1' `Seq.equal`
231+
(Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1)))
232+
}

‎lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
(*
2+
Copyright 2024 Microsoft Research
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
http://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
*)
16+
17+
module Pulse.Lib.ArrayPtr
18+
open FStar.Tactics.V2
19+
open Pulse.Lib.Pervasives
20+
module SZ = FStar.SizeT
21+
module A = Pulse.Lib.Array
22+
23+
(*
24+
The `ArrayPtr.ptr t` type in this module cannot be extracted to Rust
25+
because of the `split` operation, which assumes that the same pointer
26+
can point to either the large subarray or its sub-subarray, depending on the permission.
27+
Rust slices have the length baked in, so they cannot support this operation
28+
without modifying the pointer.
29+
30+
Use `Pulse.Lib.Slice.slice` instead when possible.
31+
*)
32+
33+
val ptr : Type0 -> Type0
34+
35+
val base #t (p: ptr t) : GTot (A.array t)
36+
val offset #t (p: ptr t) : GTot nat
37+
38+
instance val has_pts_to_array_ptr (t: Type) : has_pts_to (ptr t) (Seq.seq t)
39+
40+
val pts_to_is_slprop2 (#a:Type) (x:ptr a) (p:perm) (s:Seq.seq a)
41+
: Lemma (is_slprop2 (pts_to x #p s))
42+
[SMTPat (is_slprop2 (pts_to x #p s))]
43+
44+
val is_from_array (#t: Type) (s: ptr t) (sz: nat) (a: A.array t) : slprop
45+
46+
val from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) : stt (ptr t)
47+
(A.pts_to a #p v)
48+
(fun s -> pts_to s #p v ** is_from_array s (Seq.length v) a)
49+
50+
val to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#v: Seq.seq t) : stt_ghost unit emp_inames
51+
(pts_to s #p v ** is_from_array s (Seq.length v) a)
52+
(fun _ -> A.pts_to a #p v)
53+
54+
(* Written x.(i) *)
55+
val op_Array_Access
56+
(#t: Type)
57+
(a: ptr t)
58+
(i: SZ.t)
59+
(#p: perm)
60+
(#s: Ghost.erased (Seq.seq t))
61+
: stt t
62+
(requires
63+
pts_to a #p s ** pure (SZ.v i < Seq.length s))
64+
(ensures fun res ->
65+
pts_to a #p s **
66+
pure (
67+
SZ.v i < Seq.length s /\
68+
res == Seq.index s (SZ.v i)))
69+
70+
(* Written a.(i) <- v *)
71+
val op_Array_Assignment
72+
(#t: Type)
73+
(a: ptr t)
74+
(i: SZ.t)
75+
(v: t)
76+
(#s: Ghost.erased (Seq.seq t))
77+
: stt unit
78+
(requires
79+
pts_to a s ** pure (SZ.v i < Seq.length s))
80+
(ensures fun res -> exists* s' .
81+
pts_to a s' **
82+
pure (SZ.v i < Seq.length s /\
83+
s' == Seq.upd s (SZ.v i) v
84+
))
85+
86+
val share
87+
(#a:Type)
88+
(arr:ptr a)
89+
(#s:Ghost.erased (Seq.seq a))
90+
(#p:perm)
91+
: stt_ghost unit emp_inames
92+
(requires pts_to arr #p s)
93+
(ensures fun _ -> pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s)
94+
95+
[@@allow_ambiguous]
96+
val gather
97+
(#a:Type)
98+
(arr:ptr a)
99+
(#s0 #s1:Ghost.erased (Seq.seq a))
100+
(#p0 #p1:perm)
101+
: stt_ghost unit emp_inames
102+
(requires pts_to arr #p0 s0 ** pts_to arr #p1 s1 ** pure (Seq.length s0 == Seq.length s1))
103+
(ensures fun _ -> pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1))
104+
105+
106+
let adjacent #t (a: ptr t) (sz: nat) (b: ptr t) : prop =
107+
base a == base b /\ offset a + sz == offset b
108+
109+
val split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t { SZ.v i <= Seq.length v }) : stt (ptr t)
110+
(requires pts_to s #p v)
111+
(ensures fun s' ->
112+
pts_to s #p (Seq.slice v 0 (SZ.v i)) **
113+
pts_to s' #p (Seq.slice v (SZ.v i) (Seq.length v)) **
114+
pure (adjacent s (SZ.v i) s')
115+
)
116+
117+
val join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq.seq t) : stt_ghost unit emp_inames
118+
(pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2))
119+
(fun _ -> pts_to s1 #p (Seq.append v1 v2))
120+
121+
val memcpy
122+
(#t:Type0) (#p0:perm)
123+
(src:ptr t) (idx_src: SZ.t)
124+
(dst:ptr t) (idx_dst: SZ.t)
125+
(len: SZ.t)
126+
(#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 })
127+
(#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 })
128+
: stt unit
129+
(pts_to src #p0 s0 ** pts_to dst s1)
130+
(fun _ -> pts_to src #p0 s0 ** pts_to dst (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1)))

0 commit comments

Comments
 (0)