From 7c65ec1299876f83e4b3a86d50a6a6a24663c5c3 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Tue, 2 Jul 2024 17:37:50 -0700 Subject: [PATCH 01/32] WIP slice --- lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 116 ++++++++++++++++ lib/pulse/lib/Pulse.Lib.Slice.fst | 192 ++++++++++++++++++++++++++ lib/pulse/lib/Pulse.Lib.Slice.fsti | 101 ++++++++++++++ 3 files changed, 409 insertions(+) create mode 100644 lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti create mode 100644 lib/pulse/lib/Pulse.Lib.Slice.fst create mode 100644 lib/pulse/lib/Pulse.Lib.Slice.fsti diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti new file mode 100644 index 000000000..52aab9663 --- /dev/null +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -0,0 +1,116 @@ +module Pulse.Lib.ArrayPtr +open FStar.Tactics.V2 +open Pulse.Lib.Pervasives +module SZ = FStar.SizeT +module A = Pulse.Lib.Array + +(* This module can be used only for Pulse programs extracted to C, not Rust. *) + +val ptr : Type0 -> Type0 + +[@@erasable] +val footprint : Type0 + +val pts_to (#t: Type) (s: ptr t) (#[exact (`1.0R)] p: perm) (fp: footprint) (v: Seq.seq t) : vprop + +val pts_to_is_small (#a:Type) (x:ptr a) (p:perm) (fp: footprint) (s:Seq.seq a) + : Lemma (is_small (pts_to x #p fp s)) + [SMTPat (is_small (pts_to x #p fp s))] + +val is_from_array (#t: Type) (p: perm) (fp: footprint) (a: A.array t) : vprop + +val from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) : stt (ptr t) + (A.pts_to a #p v) + (fun s -> exists* fp . pts_to s #p fp v ** is_from_array p fp a) + +val to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#fp: footprint) (#v: Seq.seq t) : stt_ghost unit emp_inames + (pts_to s #p fp v ** is_from_array p fp a ** pure ( + Seq.length v == A.length a + )) + (fun _ -> A.pts_to a #p v) + +(* Written x.(i) *) +val op_Array_Access + (#t: Type) + (a: ptr t) + (i: SZ.t) + (#p: perm) + (#fp: footprint) + (#s: Ghost.erased (Seq.seq t){SZ.v i < Seq.length s}) + : stt t + (requires + pts_to a #p fp s) + (ensures fun res -> + pts_to a #p fp s ** + pure (res == Seq.index s (SZ.v i))) + +(* Written a.(i) <- v *) +val op_Array_Assignment + (#t: Type) + (a: ptr t) + (i: SZ.t) + (v: t) + (#fp: footprint) + (#s: Ghost.erased (Seq.seq t) {SZ.v i < Seq.length s}) + : stt unit + (requires + pts_to a fp s) + (ensures fun res -> + pts_to a fp (Seq.upd s (SZ.v i) v)) + +val share + (#a:Type) + (arr:ptr a) + (#s:Ghost.erased (Seq.seq a)) + (#fp: footprint) + (#p:perm) +: stt_ghost unit emp_inames + (requires pts_to arr #p fp s) + (ensures fun _ -> pts_to arr #(p /. 2.0R) fp s ** pts_to arr #(p /. 2.0R) fp s) + +[@@allow_ambiguous] +val gather + (#a:Type) + (arr:ptr a) + (#s0 #s1:Ghost.erased (Seq.seq a)) + (#p0 #p1:perm) + (#fp: footprint) +: stt_ghost unit emp_inames + (requires pts_to arr #p0 fp s0 ** pts_to arr #p1 fp s1) + (ensures fun _ -> pts_to arr #(p0 +. p1) fp s0 ** pure (s0 == s1)) + +val adjacent: footprint -> footprint -> prop + +val merge: (fp1: footprint) -> (fp2: footprint {adjacent fp1 fp2}) -> footprint + +val merge_assoc: (fp1: footprint) -> (fp2: footprint) -> (fp3: footprint) -> Lemma + (ensures ( + ((adjacent fp1 fp2 /\ adjacent (merge fp1 fp2) fp3) <==> (adjacent fp1 fp2 /\ adjacent fp2 fp3)) /\ + ((adjacent fp2 fp3 /\ adjacent fp1 (merge fp2 fp3)) <==> (adjacent fp1 fp2 /\ adjacent fp2 fp3)) /\ + ((adjacent fp1 fp2 /\ adjacent fp2 fp3) ==> + merge (merge fp1 fp2) fp3 == merge fp1 (merge fp2 fp3) + ) + )) + [SMTPatOr [ + [SMTPat (adjacent fp1 fp2); SMTPat (adjacent (merge fp1 fp2) fp3)]; + [SMTPat (adjacent fp2 fp3); SMTPat (adjacent fp1 (merge fp2 fp3))]; + [SMTPat (adjacent fp1 fp2); SMTPat (adjacent fp2 fp3)]; + ]] + +val split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (ptr t) + (requires pts_to s #p fp v ** pure (SZ.v i <= Seq.length v)) + (ensures fun s' -> + exists* v1 v2 fp1 fp2 . + pts_to s #p fp1 v1 ** + pts_to s' #p fp2 v2 ** + pure ( + adjacent fp1 fp2 /\ + merge fp1 fp2 == fp /\ + SZ.v i <= Seq.length v /\ + (v1, v2) == Seq.split v (SZ.v i) + ) + ) + +val join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint) (#v1: Seq.seq t) (s2: ptr t) (#fp2: footprint {adjacent fp1 fp2}) (#v2: Seq.seq t) : stt_ghost unit emp_inames + (pts_to s1 #p fp1 v1 ** pts_to s2 #p fp2 v2) + (fun _ -> pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2)) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst new file mode 100644 index 000000000..49a6a47a4 --- /dev/null +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -0,0 +1,192 @@ +module Pulse.Lib.Slice + +module AP = Pulse.Lib.ArrayPtr + +noeq +type slice t = { + elt: AP.ptr t; + len: SZ.t; + fp: AP.footprint; +} + +let len s = s.len + +let pts_to #t s #p v = + AP.pts_to s.elt #p s.fp v ** + pure (Seq.length v == SZ.v s.len) + +let pts_to_is_small x p v = () + +```pulse +ghost +fn pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) +requires (pts_to s #p v) +ensures (pts_to s #p v ** pure (Seq.length v == SZ.v (len s))) + +{ + unfold (pts_to s #p v); + fold (pts_to s #p v) +} +``` + +let is_from_array #t a p s = + AP.is_from_array p s.fp a ** + pure (SZ.v s.len == A.length a) + +```pulse +fn from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { + SZ.v alen == A.length a /\ + (mutb == true ==> p == 1.0R) +}) +requires (A.pts_to a #p v) +returns s: (slice t) +ensures ( + pts_to s #p v ** + is_from_array a p s + ) +{ + A.pts_to_len a; + let ptr = AP.from_array a; + with fp . assert (AP.pts_to ptr #p fp v ** AP.is_from_array p fp a); + let res : slice t = { + elt = ptr; + len = alen; + fp = fp; + }; + rewrite (AP.pts_to ptr #p fp v) as (AP.pts_to res.elt #p res.fp v); + fold (pts_to res #p v); + rewrite (AP.is_from_array p fp a) as (AP.is_from_array p res.fp a); + fold (is_from_array a p res); + res +} +``` + +```pulse +ghost +fn to_array + (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: array t) +requires (pts_to s #p v ** is_from_array a p s) +ensures (A.pts_to a #p v) +{ + unfold (pts_to s #p v); + unfold (is_from_array a p s); + AP.to_array s.elt a +} +``` + +```pulse +fn op_Array_Access + (#t: Type) + (a: slice t) + (i: SZ.t) + (#p: perm) + (#s: Ghost.erased (Seq.seq t){SZ.v i < Seq.length s}) + requires + pts_to a #p s +returns res : t +ensures + pts_to a #p s ** + pure (res == Seq.index s (SZ.v i)) +{ + unfold (pts_to a #p s); + let res = AP.op_Array_Access a.elt i; + fold (pts_to a #p s); + res +} +``` + +```pulse +fn op_Array_Assignment + (#t: Type) + (a: slice t) + (i: SZ.t) + (v: t) + (#s: Ghost.erased (Seq.seq t) {SZ.v i < Seq.length s}) + requires + pts_to a s + ensures + pts_to a (Seq.upd s (SZ.v i) v) +{ + unfold (pts_to a s); + AP.op_Array_Assignment a.elt i v; + fold (pts_to a (Seq.upd s (SZ.v i) v)) +} +``` + +```pulse +ghost +fn share + (#a:Type) + (arr:slice a) + (#s:Ghost.erased (Seq.seq a)) + (#p:perm) +requires + pts_to arr #p s +ensures pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s +{ + unfold (pts_to arr #p s); + AP.share arr.elt; + fold (pts_to arr #(p /. 2.0R) s); + fold (pts_to arr #(p /. 2.0R) s) +} +``` + +```pulse +ghost +fn gather + (#a:Type) + (arr:slice a) + (#s0 #s1:Ghost.erased (Seq.seq a)) + (#p0 #p1:perm) +requires pts_to arr #p0 s0 ** pts_to arr #p1 s1 +ensures pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1) +{ + unfold (pts_to arr #p0 s0); + unfold (pts_to arr #p1 s1); + AP.gather arr.elt; + fold (pts_to arr #(p0 +. p1) s0) +} +``` + +let is_split #t s p i s1 s2 = + pure ( + s1.elt == s.elt /\ + AP.adjacent s1.fp s2.fp /\ + AP.merge s1.fp s2.fp == s.fp + ) + +val split0 (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice t & slice t) + (requires pts_to s #p v ** pure (SZ.v i <= Seq.length v)) + (ensures fun res -> let (s1, s2) = res in + exists* v1 v2 . + pts_to s1 #p v1 ** + pts_to s2 #p v2 ** + is_split s p i s1 s2 ** + pure ( + SZ.v i <= Seq.length v /\ + (v1, v2) == Seq.split v (SZ.v i) + ) + ) + + +```pulse +ghost +fn split0 (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) + requires pts_to s #p v ** pure (SZ.v i <= Seq.length v) + returns res : (slice t & slice t) + ensures (let (s1, s2) = res in + exists* v1 v2 . + pts_to s1 #p v1 ** + pts_to s2 #p v2 ** + is_split s p i s1 s2 ** + pure ( + SZ.v i <= Seq.length v /\ + (v1, v2) == Seq.split v (SZ.v i) + ) + ) +{ + admit () +} +``` + +let split s #p #v i = split0 s #p #v i diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti new file mode 100644 index 000000000..2b7b2c4f9 --- /dev/null +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -0,0 +1,101 @@ +module Pulse.Lib.Slice +open FStar.Tactics.V2 +open Pulse.Lib.Pervasives +module SZ = FStar.SizeT +module A = Pulse.Lib.Array + +val slice : Type0 -> Type0 + +val len (#t: Type) : slice t -> SZ.t + +val pts_to (#t: Type) (s: slice t) (#[exact (`1.0R)] p: perm) (v: Seq.seq t) : vprop + +val pts_to_is_small (#a:Type) (x:slice a) (p:perm) (s:Seq.seq a) + : Lemma (is_small (pts_to x #p s)) + [SMTPat (is_small (pts_to x #p s))] + +val pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) : stt_ghost unit emp_inames + (pts_to s #p v) + (fun _ -> pts_to s #p v ** pure (Seq.length v == SZ.v (len s))) + +val is_from_array (#t: Type) (a: array t) (p: perm) (s: slice t) : vprop + +val from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { + SZ.v alen == A.length a /\ + (mutb == true ==> p == 1.0R) +}) : stt (slice t) + (A.pts_to a #p v) + (fun s -> + pts_to s #p v ** + is_from_array a p s + ) + +val to_array (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: array t) : stt_ghost unit emp_inames + (pts_to s #p v ** is_from_array a p s) + (fun _ -> A.pts_to a #p v) + +(* Written x.(i) *) +val op_Array_Access + (#t: Type) + (a: slice t) + (i: SZ.t) + (#p: perm) + (#s: Ghost.erased (Seq.seq t){SZ.v i < Seq.length s}) + : stt t + (requires + pts_to a #p s) + (ensures fun res -> + pts_to a #p s ** + pure (res == Seq.index s (SZ.v i))) + + +(* Written a.(i) <- v *) +val op_Array_Assignment + (#t: Type) + (a: slice t) + (i: SZ.t) + (v: t) + (#s: Ghost.erased (Seq.seq t) {SZ.v i < Seq.length s}) + : stt unit + (requires + pts_to a s) + (ensures fun res -> + pts_to a (Seq.upd s (SZ.v i) v)) + +val share + (#a:Type) + (arr:slice a) + (#s:Ghost.erased (Seq.seq a)) + (#p:perm) +: stt_ghost unit emp_inames + (requires pts_to arr #p s) + (ensures fun _ -> pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s) + +[@@allow_ambiguous] +val gather + (#a:Type) + (arr:slice a) + (#s0 #s1:Ghost.erased (Seq.seq a)) + (#p0 #p1:perm) +: stt_ghost unit emp_inames + (requires pts_to arr #p0 s0 ** pts_to arr #p1 s1) + (ensures fun _ -> pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1)) + +val is_split (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t) (right: slice t) : vprop + +val split (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice t & slice t) + (requires pts_to s #p v ** pure (SZ.v i <= Seq.length v)) + (ensures fun (s1, s2) -> + exists* v1 v2 . + pts_to s1 #p v1 ** + pts_to s2 #p v2 ** + is_split s p i s1 s2 ** + pure ( + SZ.v i <= Seq.length v /\ + (v1, v2) == Seq.split v (SZ.v i) + ) + ) + +val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (#i: SZ.t) (s: slice t) : stt_ghost unit emp_inames + (pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s p i s1 s2) + (fun _ -> pts_to s #p (Seq.append v1 v2)) From 6f7b4883585abd347915716e5ca785082ecb58ed Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Tue, 2 Jul 2024 23:10:37 -0700 Subject: [PATCH 02/32] implement Pulse.Lib.Slice --- lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 17 ++++--- lib/pulse/lib/Pulse.Lib.Slice.fst | 66 +++++++++++++++------------ lib/pulse/lib/Pulse.Lib.Slice.fsti | 26 +++++++++-- 3 files changed, 70 insertions(+), 39 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index 52aab9663..7db05d342 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -97,18 +97,23 @@ val merge_assoc: (fp1: footprint) -> (fp2: footprint) -> (fp3: footprint) -> Lem [SMTPat (adjacent fp1 fp2); SMTPat (adjacent fp2 fp3)]; ]] +let split_postcond + (#t: Type) (fp: footprint) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) + (v1: Seq.seq t) (v2: Seq.seq t) (fp1: footprint) (fp2: footprint) +: Tot prop += + adjacent fp1 fp2 /\ + merge fp1 fp2 == fp /\ + SZ.v i <= Seq.length v /\ + (v1, v2) == Seq.split v (SZ.v i) + val split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (ptr t) (requires pts_to s #p fp v ** pure (SZ.v i <= Seq.length v)) (ensures fun s' -> exists* v1 v2 fp1 fp2 . pts_to s #p fp1 v1 ** pts_to s' #p fp2 v2 ** - pure ( - adjacent fp1 fp2 /\ - merge fp1 fp2 == fp /\ - SZ.v i <= Seq.length v /\ - (v1, v2) == Seq.split v (SZ.v i) - ) + pure (split_postcond fp v i v1 v2 fp1 fp2) ) val join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint) (#v1: Seq.seq t) (s2: ptr t) (#fp2: footprint {adjacent fp1 fp2}) (#v2: Seq.seq t) : stt_ghost unit emp_inames diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index 49a6a47a4..b1934e711 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -152,41 +152,51 @@ let is_split #t s p i s1 s2 = pure ( s1.elt == s.elt /\ AP.adjacent s1.fp s2.fp /\ - AP.merge s1.fp s2.fp == s.fp - ) - -val split0 (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice t & slice t) - (requires pts_to s #p v ** pure (SZ.v i <= Seq.length v)) - (ensures fun res -> let (s1, s2) = res in - exists* v1 v2 . - pts_to s1 #p v1 ** - pts_to s2 #p v2 ** - is_split s p i s1 s2 ** - pure ( - SZ.v i <= Seq.length v /\ - (v1, v2) == Seq.split v (SZ.v i) - ) + AP.merge s1.fp s2.fp == s.fp /\ + SZ.v s.len == SZ.v s1.len + SZ.v s2.len ) +let is_split_is_small s p i s1 s2 = () ```pulse -ghost -fn split0 (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) +fn split (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) requires pts_to s #p v ** pure (SZ.v i <= Seq.length v) returns res : (slice t & slice t) - ensures (let (s1, s2) = res in - exists* v1 v2 . - pts_to s1 #p v1 ** - pts_to s2 #p v2 ** - is_split s p i s1 s2 ** - pure ( - SZ.v i <= Seq.length v /\ - (v1, v2) == Seq.split v (SZ.v i) - ) - ) + ensures (split_post s p v i res) { - admit () + unfold (pts_to s #p v); + Seq.lemma_split v (SZ.v i); + let elt' = AP.split s.elt i; + with fp1 _v1 fp2 _v2 . assert (AP.pts_to s.elt #p fp1 _v1 ** AP.pts_to elt' #p fp2 _v2 ** pure (AP.split_postcond s.fp v i _v1 _v2 fp1 fp2)); + let s1 = { + elt = s.elt; + len = i; + fp = fp1; + }; + fold (pts_to s1 #p _v1); + let s2 = { + elt = elt'; + len = s.len `SZ.sub` i; + fp = fp2; + }; + fold (pts_to s2 #p _v2); + fold (is_split s p i s1 s2); + fold (split_post' s p v i s1 s2); + fold (split_post s p v i (s1, s2)); + (s1, s2) } ``` -let split s #p #v i = split0 s #p #v i +```pulse +ghost +fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (#i: SZ.t) (s: slice t) + requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s p i s1 s2 + ensures pts_to s #p (Seq.append v1 v2) +{ + unfold (is_split s p i s1 s2); + unfold (pts_to s1 #p v1); + unfold (pts_to s2 #p v2); + AP.join s1.elt s2.elt; + fold (pts_to s #p (Seq.append v1 v2)) +} +``` diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index 2b7b2c4f9..6a9c052fb 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -83,10 +83,16 @@ val gather val is_split (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t) (right: slice t) : vprop -val split (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice t & slice t) - (requires pts_to s #p v ** pure (SZ.v i <= Seq.length v)) - (ensures fun (s1, s2) -> - exists* v1 v2 . +val is_split_is_small (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t) (right: slice t) + : Lemma (is_small (is_split s p i left right)) + [SMTPat (is_small (is_split s p i left right))] + +let split_post' + (#t: Type) (s: slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) + (s1: slice t) + (s2: slice t) +: Tot vprop += exists* v1 v2 . pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s p i s1 s2 ** @@ -94,7 +100,17 @@ val split (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.v i <= Seq.length v /\ (v1, v2) == Seq.split v (SZ.v i) ) - ) + +let split_post + (#t: Type) (s: slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) + (res: (slice t & slice t)) +: Tot vprop += let (s1, s2) = res in + split_post' s p v i s1 s2 + +val split (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice t & slice t) + (requires pts_to s #p v ** pure (SZ.v i <= Seq.length v)) + (ensures fun res -> split_post s p v i res) val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (#i: SZ.t) (s: slice t) : stt_ghost unit emp_inames (pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s p i s1 s2) From 8e1f5f0188c8e2b3eb21aa6db0c108678317c003 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 3 Jul 2024 00:32:07 -0700 Subject: [PATCH 03/32] implement Pulse.Lib.ArrayPtr --- lib/pulse/lib/Pulse.Lib.Array.Core.fst | 35 ++++ lib/pulse/lib/Pulse.Lib.Array.Core.fsti | 21 +++ lib/pulse/lib/Pulse.Lib.ArrayPtr.fst | 207 +++++++++++++++++++++++ lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 32 ++-- lib/pulse/lib/Pulse.Lib.HigherArray.fst | 40 +++++ lib/pulse/lib/Pulse.Lib.HigherArray.fsti | 23 ++- lib/pulse/lib/Pulse.Lib.Slice.fst | 2 +- 7 files changed, 342 insertions(+), 18 deletions(-) create mode 100644 lib/pulse/lib/Pulse.Lib.ArrayPtr.fst diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fst b/lib/pulse/lib/Pulse.Lib.Array.Core.fst index 512c5e902..7e809981e 100644 --- a/lib/pulse/lib/Pulse.Lib.Array.Core.fst +++ b/lib/pulse/lib/Pulse.Lib.Array.Core.fst @@ -362,6 +362,41 @@ ensures post } ``` +```pulse +ghost +fn pts_to_range_share + (#a:Type) + (arr:array a) + (#l #r: nat) + (#s:Seq.seq a) + (#p:perm) + requires pts_to_range arr l r #p s + ensures pts_to_range arr l r #(p /. 2.0R) s ** pts_to_range arr l r #(p /. 2.0R) s +{ + unfold (pts_to_range arr l r #p s); + H.pts_to_range_share arr; + fold (pts_to_range arr l r #(p /. 2.0R) s); + fold (pts_to_range arr l r #(p /. 2.0R) s); +} +``` + +```pulse +ghost +fn pts_to_range_gather + (#a:Type) + (arr:array a) + (#l #r: nat) + (#s0 #s1: Seq.seq a) + (#p0 #p1:perm) + requires pts_to_range arr l r #p0 s0 ** pts_to_range arr l r #p1 s1 + ensures pts_to_range arr l r #(p0 +. p1) s0 ** pure (s0 == s1) +{ + unfold (pts_to_range arr l r #p0 s0); + unfold (pts_to_range arr l r #p1 s1); + H.pts_to_range_gather arr; + fold (pts_to_range arr l r #(p0 +. p1) s0) +} +``` (* this is universe-polymorphic in ret_t; so can't define it in Pulse yet *) let with_local' diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fsti b/lib/pulse/lib/Pulse.Lib.Array.Core.fsti index 94b9a84a5..241498c68 100644 --- a/lib/pulse/lib/Pulse.Lib.Array.Core.fsti +++ b/lib/pulse/lib/Pulse.Lib.Array.Core.fsti @@ -213,6 +213,27 @@ val pts_to_range_upd Seq.length s0 == r - l /\ s == Seq.upd s0 (SZ.v i - l) v )) +val pts_to_range_share + (#a:Type) + (arr:array a) + (#l #r: nat) + (#s:Seq.seq a) + (#p:perm) +: stt_ghost unit emp_inames + (requires pts_to_range arr l r #p s) + (ensures fun _ -> pts_to_range arr l r #(p /. 2.0R) s ** pts_to_range arr l r #(p /. 2.0R) s) + +[@@allow_ambiguous] +val pts_to_range_gather + (#a:Type) + (arr:array a) + (#l #r: nat) + (#s0 #s1: Seq.seq a) + (#p0 #p1:perm) +: stt_ghost unit emp_inames + (requires pts_to_range arr l r #p0 s0 ** pts_to_range arr l r #p1 s1) + (ensures fun _ -> pts_to_range arr l r #(p0 +. p1) s0 ** pure (s0 == s1)) + val with_local (#a:Type0) (init:a) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst new file mode 100644 index 000000000..567a231f1 --- /dev/null +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst @@ -0,0 +1,207 @@ +module Pulse.Lib.ArrayPtr + +noeq +type ptr t = { + base: A.array t; + offset: (offset: SZ.t { SZ.v offset <= A.length base}) +} + +[@@erasable] +noeq +type footprint (t: Type0) = { + elt: ptr t; + len: (len: SZ.t { SZ.v elt.offset + SZ.v len <= A.length elt.base}); +} + +let pts_to s #p fp v = + A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v fp.len) #p v ** + pure (fp.elt == s) + +let pts_to_is_small x p fp s = () + +let is_from_array p fp a = + pure (fp.elt.base == a /\ SZ.v fp.len == A.length a) + +```pulse +fn from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) + requires A.pts_to a #p v + returns s: ptr t + ensures exists* fp . pts_to s #p fp v ** is_from_array p fp a +{ + A.pts_to_len a; + let res = { + base = a; + offset = 0sz; + }; + let fp = { + elt = res; + len = SZ.uint_to_t (A.length a); + }; + fold (is_from_array p fp a); + A.pts_to_range_intro a p v; + rewrite (A.pts_to_range a 0 (A.length a) #p v) + as (A.pts_to_range res.base (SZ.v res.offset) (SZ.v res.offset + SZ.v fp.len) #p v); + fold (pts_to res #p fp v); + res +} +``` + +```pulse +ghost +fn to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#fp: footprint t) (#v: Seq.seq t) + requires pts_to s #p fp v ** is_from_array p fp a ** pure ( + Seq.length v == A.length a + ) + ensures A.pts_to a #p v +{ + unfold (is_from_array p fp a); + unfold (pts_to s #p fp v); + rewrite (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v fp.len) #p v) + as (A.pts_to_range a 0 (A.length a) #p v); + A.pts_to_range_elim a _ _; +} +``` + +```pulse +fn op_Array_Access + (#t: Type) + (a: ptr t) + (i: SZ.t) + (#p: perm) + (#fp: footprint t) + (#s: Ghost.erased (Seq.seq t){SZ.v i < Seq.length s}) + requires + pts_to a #p fp s + returns res: t + ensures + pts_to a #p fp s ** + pure (res == Seq.index s (SZ.v i)) +{ + unfold (pts_to a #p fp s); + A.pts_to_range_prop a.base; + let res = A.pts_to_range_index a.base (SZ.add a.offset i); + fold (pts_to a #p fp s); + res +} +``` + +```pulse +fn op_Array_Assignment + (#t: Type) + (a: ptr t) + (i: SZ.t) + (v: t) + (#fp: footprint t) + (#s: Ghost.erased (Seq.seq t) {SZ.v i < Seq.length s}) + requires + pts_to a fp s + ensures + pts_to a fp (Seq.upd s (SZ.v i) v) +{ + unfold (pts_to a fp s); + A.pts_to_range_prop a.base; + let res = A.pts_to_range_upd a.base (SZ.add a.offset i) v; + fold (pts_to a fp (Seq.upd s (SZ.v i) v)); +} +``` + +```pulse +ghost +fn share + (#a:Type) + (arr:ptr a) + (#s:Ghost.erased (Seq.seq a)) + (#fp: footprint a) + (#p:perm) + requires pts_to arr #p fp s + ensures pts_to arr #(p /. 2.0R) fp s ** pts_to arr #(p /. 2.0R) fp s +{ + unfold (pts_to arr #p fp s); + A.pts_to_range_share arr.base; + fold (pts_to arr #(p /. 2.0R) fp s); + fold (pts_to arr #(p /. 2.0R) fp s); +} +``` + +```pulse +ghost +fn gather + (#a:Type) + (arr:ptr a) + (#s0 #s1:Ghost.erased (Seq.seq a)) + (#p0 #p1:perm) + (#fp: footprint a) + requires pts_to arr #p0 fp s0 ** pts_to arr #p1 fp s1 + ensures pts_to arr #(p0 +. p1) fp s0 ** pure (s0 == s1) +{ + unfold (pts_to arr #p0 fp s0); + unfold (pts_to arr #p1 fp s1); + A.pts_to_range_gather arr.base; + fold (pts_to arr #(p0 +. p1) fp s0) +} +``` + +let adjacent fp1 fp2 = + fp1.elt.base == fp2.elt.base /\ + SZ.v fp1.elt.offset + SZ.v fp1.len == SZ.v fp2.elt.offset + +let merge fp1 fp2 = { + elt = fp1.elt; + len = SZ.add fp1.len fp2.len; +} + +let merge_assoc fp1 fp2 fp3 = () + +```pulse +fn split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint t) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) + requires pts_to s #p fp v ** pure (SZ.v i <= Seq.length v) + returns s' : ptr t + ensures + exists* v1 v2 fp1 fp2 . + pts_to s #p fp1 v1 ** + pts_to s' #p fp2 v2 ** + pure (split_postcond fp v i v1 v2 fp1 fp2) +{ + unfold (pts_to s #p fp v); + A.pts_to_range_prop s.base; + let s' = { + base = s.base; + offset = SZ.add s.offset i; + }; + let fp1 = { + elt = fp.elt; + len = i; + }; + let fp2 = { + elt = s'; + len = SZ.sub fp.len i; + }; + A.pts_to_range_split s.base _ (SZ.v s'.offset) _; + with s1 . assert (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1); + rewrite + (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1) + as (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v fp1.len) #p s1); + fold (pts_to s #p fp1 s1); + with s2 . assert (A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + SZ.v fp.len) #p s2); + rewrite + (A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + SZ.v fp.len) #p s2) + as (A.pts_to_range s'.base (SZ.v s'.offset) (SZ.v s'.offset + SZ.v fp2.len) #p s2); + fold (pts_to s' #p fp2 s2); + s' +} +``` + +```pulse +ghost +fn join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint t) (#v1: Seq.seq t) (s2: ptr t) (#fp2: footprint t {adjacent fp1 fp2}) (#v2: Seq.seq t) + requires pts_to s1 #p fp1 v1 ** pts_to s2 #p fp2 v2 + ensures pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2) +{ + unfold (pts_to s1 #p fp1 v1); + unfold (pts_to s2 #p fp2 v2); + rewrite (A.pts_to_range s2.base (SZ.v s2.offset) (SZ.v s2.offset + SZ.v fp2.len) #p v2) + as (A.pts_to_range s1.base (SZ.v s1.offset + SZ.v fp1.len) (SZ.v s1.offset + SZ.v (merge fp1 fp2).len) #p v2); + A.pts_to_range_join s1.base (SZ.v s1.offset) (SZ.v s1.offset + SZ.v fp1.len) (SZ.v s1.offset + SZ.v (merge fp1 fp2).len); + fold (pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2)) +} +``` diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index 7db05d342..53439d5e9 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -9,21 +9,21 @@ module A = Pulse.Lib.Array val ptr : Type0 -> Type0 [@@erasable] -val footprint : Type0 +val footprint : Type0 -> Type0 -val pts_to (#t: Type) (s: ptr t) (#[exact (`1.0R)] p: perm) (fp: footprint) (v: Seq.seq t) : vprop +val pts_to (#t: Type) (s: ptr t) (#[exact (`1.0R)] p: perm) (fp: footprint t) (v: Seq.seq t) : vprop -val pts_to_is_small (#a:Type) (x:ptr a) (p:perm) (fp: footprint) (s:Seq.seq a) +val pts_to_is_small (#a:Type) (x:ptr a) (p:perm) (fp: footprint a) (s:Seq.seq a) : Lemma (is_small (pts_to x #p fp s)) [SMTPat (is_small (pts_to x #p fp s))] -val is_from_array (#t: Type) (p: perm) (fp: footprint) (a: A.array t) : vprop +val is_from_array (#t: Type) (p: perm) (fp: footprint t) (a: A.array t) : vprop val from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) : stt (ptr t) (A.pts_to a #p v) (fun s -> exists* fp . pts_to s #p fp v ** is_from_array p fp a) -val to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#fp: footprint) (#v: Seq.seq t) : stt_ghost unit emp_inames +val to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#fp: footprint t) (#v: Seq.seq t) : stt_ghost unit emp_inames (pts_to s #p fp v ** is_from_array p fp a ** pure ( Seq.length v == A.length a )) @@ -35,7 +35,7 @@ val op_Array_Access (a: ptr t) (i: SZ.t) (#p: perm) - (#fp: footprint) + (#fp: footprint t) (#s: Ghost.erased (Seq.seq t){SZ.v i < Seq.length s}) : stt t (requires @@ -50,7 +50,7 @@ val op_Array_Assignment (a: ptr t) (i: SZ.t) (v: t) - (#fp: footprint) + (#fp: footprint t) (#s: Ghost.erased (Seq.seq t) {SZ.v i < Seq.length s}) : stt unit (requires @@ -62,7 +62,7 @@ val share (#a:Type) (arr:ptr a) (#s:Ghost.erased (Seq.seq a)) - (#fp: footprint) + (#fp: footprint a) (#p:perm) : stt_ghost unit emp_inames (requires pts_to arr #p fp s) @@ -74,16 +74,16 @@ val gather (arr:ptr a) (#s0 #s1:Ghost.erased (Seq.seq a)) (#p0 #p1:perm) - (#fp: footprint) + (#fp: footprint a) : stt_ghost unit emp_inames (requires pts_to arr #p0 fp s0 ** pts_to arr #p1 fp s1) (ensures fun _ -> pts_to arr #(p0 +. p1) fp s0 ** pure (s0 == s1)) -val adjacent: footprint -> footprint -> prop +val adjacent (#t: Type): footprint t -> footprint t -> prop -val merge: (fp1: footprint) -> (fp2: footprint {adjacent fp1 fp2}) -> footprint +val merge (#t: Type): (fp1: footprint t) -> (fp2: footprint t {adjacent fp1 fp2}) -> footprint t -val merge_assoc: (fp1: footprint) -> (fp2: footprint) -> (fp3: footprint) -> Lemma +val merge_assoc (#t: Type): (fp1: footprint t) -> (fp2: footprint t) -> (fp3: footprint t) -> Lemma (ensures ( ((adjacent fp1 fp2 /\ adjacent (merge fp1 fp2) fp3) <==> (adjacent fp1 fp2 /\ adjacent fp2 fp3)) /\ ((adjacent fp2 fp3 /\ adjacent fp1 (merge fp2 fp3)) <==> (adjacent fp1 fp2 /\ adjacent fp2 fp3)) /\ @@ -98,8 +98,8 @@ val merge_assoc: (fp1: footprint) -> (fp2: footprint) -> (fp3: footprint) -> Lem ]] let split_postcond - (#t: Type) (fp: footprint) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) - (v1: Seq.seq t) (v2: Seq.seq t) (fp1: footprint) (fp2: footprint) + (#t: Type) (fp: footprint t) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) + (v1: Seq.seq t) (v2: Seq.seq t) (fp1: footprint t) (fp2: footprint t) : Tot prop = adjacent fp1 fp2 /\ @@ -107,7 +107,7 @@ let split_postcond SZ.v i <= Seq.length v /\ (v1, v2) == Seq.split v (SZ.v i) -val split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (ptr t) +val split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint t) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (ptr t) (requires pts_to s #p fp v ** pure (SZ.v i <= Seq.length v)) (ensures fun s' -> exists* v1 v2 fp1 fp2 . @@ -116,6 +116,6 @@ val split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint) (#v: Ghost.erased (S pure (split_postcond fp v i v1 v2 fp1 fp2) ) -val join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint) (#v1: Seq.seq t) (s2: ptr t) (#fp2: footprint {adjacent fp1 fp2}) (#v2: Seq.seq t) : stt_ghost unit emp_inames +val join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint t) (#v1: Seq.seq t) (s2: ptr t) (#fp2: footprint t {adjacent fp1 fp2}) (#v2: Seq.seq t) : stt_ghost unit emp_inames (pts_to s1 #p fp1 v1 ** pts_to s2 #p fp2 v2) (fun _ -> pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2)) diff --git a/lib/pulse/lib/Pulse.Lib.HigherArray.fst b/lib/pulse/lib/Pulse.Lib.HigherArray.fst index 8509c412b..4f891a9a9 100644 --- a/lib/pulse/lib/Pulse.Lib.HigherArray.fst +++ b/lib/pulse/lib/Pulse.Lib.HigherArray.fst @@ -902,3 +902,43 @@ ensures } ``` let pts_to_range_upd = pts_to_range_upd' + +```pulse +ghost +fn pts_to_range_share + (#a:Type) + (arr:array a) + (#l #r: nat) + (#s:Seq.seq a) + (#p:perm) + requires pts_to_range arr l r #p s + ensures pts_to_range arr l r #(p /. 2.0R) s ** pts_to_range arr l r #(p /. 2.0R) s +{ + pts_to_range_prop arr; + unfold (pts_to_range arr l r #p s); + unfold (token #(in_bounds l r arr) _); + share (array_slice arr l r); + pts_to_range_intro_ij arr (p /. 2.0R) s l r (); + pts_to_range_intro_ij arr (p /. 2.0R) s l r (); +} +``` + +```pulse +ghost +fn pts_to_range_gather + (#a:Type) + (arr:array a) + (#l #r: nat) + (#s0 #s1: Seq.seq a) + (#p0 #p1:perm) + requires pts_to_range arr l r #p0 s0 ** pts_to_range arr l r #p1 s1 + ensures pts_to_range arr l r #(p0 +. p1) s0 ** pure (s0 == s1) +{ + pts_to_range_prop arr #l #r #p0; + unfold (pts_to_range arr l r #p0 s0); + unfold (token #(in_bounds l r arr) _); + unfold (pts_to_range arr l r #p1 s1); + gather (array_slice arr l r); + fold (pts_to_range arr l r #(p0 +. p1) s0) +} +``` diff --git a/lib/pulse/lib/Pulse.Lib.HigherArray.fsti b/lib/pulse/lib/Pulse.Lib.HigherArray.fsti index bfd85f2d0..017e64a77 100644 --- a/lib/pulse/lib/Pulse.Lib.HigherArray.fsti +++ b/lib/pulse/lib/Pulse.Lib.HigherArray.fsti @@ -212,4 +212,25 @@ val pts_to_range_upd pts_to_range a l r s ** pure( Seq.length s0 == r - l /\ s == Seq.upd s0 (SZ.v i - l) v - )) \ No newline at end of file + )) + +val pts_to_range_share + (#a:Type) + (arr:array a) + (#l #r: nat) + (#s:Seq.seq a) + (#p:perm) +: stt_ghost unit emp_inames + (requires pts_to_range arr l r #p s) + (ensures fun _ -> pts_to_range arr l r #(p /. 2.0R) s ** pts_to_range arr l r #(p /. 2.0R) s) + +[@@allow_ambiguous] +val pts_to_range_gather + (#a:Type) + (arr:array a) + (#l #r: nat) + (#s0 #s1: Seq.seq a) + (#p0 #p1:perm) +: stt_ghost unit emp_inames + (requires pts_to_range arr l r #p0 s0 ** pts_to_range arr l r #p1 s1) + (ensures fun _ -> pts_to_range arr l r #(p0 +. p1) s0 ** pure (s0 == s1)) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index b1934e711..f775bc01f 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -6,7 +6,7 @@ noeq type slice t = { elt: AP.ptr t; len: SZ.t; - fp: AP.footprint; + fp: AP.footprint t; } let len s = s.len From f0ace6e63f626fa5c43b8e3fa96a123b4bddb127 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 3 Jul 2024 09:04:51 -0700 Subject: [PATCH 04/32] add a mutb tag on Slice.split --- lib/pulse/lib/Pulse.Lib.Slice.fst | 4 ++-- lib/pulse/lib/Pulse.Lib.Slice.fsti | 9 +++++++-- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index f775bc01f..7ed3b3f0e 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -159,8 +159,8 @@ let is_split #t s p i s1 s2 = let is_split_is_small s p i s1 s2 = () ```pulse -fn split (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) - requires pts_to s #p v ** pure (SZ.v i <= Seq.length v) +fn split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) + requires pts_to s #p v ** pure (split_precond mutb p v i) returns res : (slice t & slice t) ensures (split_post s p v i res) { diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index 6a9c052fb..13338dde0 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -87,6 +87,11 @@ val is_split_is_small (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t : Lemma (is_small (is_split s p i left right)) [SMTPat (is_small (is_split s p i left right))] +let split_precond + (#t: Type) (mutb: bool) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) +: Tot prop += SZ.v i <= Seq.length v /\ (mutb == true ==> p == 1.0R) + let split_post' (#t: Type) (s: slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) (s1: slice t) @@ -108,8 +113,8 @@ let split_post = let (s1, s2) = res in split_post' s p v i s1 s2 -val split (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice t & slice t) - (requires pts_to s #p v ** pure (SZ.v i <= Seq.length v)) +val split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice t & slice t) + (requires pts_to s #p v ** pure (split_precond mutb p v i)) (ensures fun res -> split_post s p v i res) val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (#i: SZ.t) (s: slice t) : stt_ghost unit emp_inames From ccdc7059d0593ee366c79252a85dcae4d02bee5d Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 3 Jul 2024 16:08:26 -0700 Subject: [PATCH 05/32] C extraction rules for Pulse.Lib.ArrayPtr --- src/extraction/ExtractPulse.fst | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst index 092df9a75..d9265917b 100644 --- a/src/extraction/ExtractPulse.fst +++ b/src/extraction/ExtractPulse.fst @@ -25,6 +25,7 @@ let pulse_translate_type_without_decay : translate_type_without_decay_t = fun en (let p = Syntax.string_of_mlpath p in p = "Pulse.Lib.Reference.ref" || p = "Pulse.Lib.Array.Core.array" || + p = "Pulse.Lib.ArrayPtr.ptr" || p = "Pulse.Lib.Vec.vec") -> TBuf (translate_type_without_decay env arg) @@ -93,22 +94,32 @@ let pulse_translate_expr : translate_expr_t = fun env e -> when string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Access" -> EBufRead (translate_expr env e, translate_expr env i) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e; i; v; _w ]) - when string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Assignment" -> - EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e; i; _p; _fp; _w ]) + when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Access" -> + EBufRead (translate_expr env e, translate_expr env i) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, (e :: i :: _)) - when string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_index" -> + when string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_index" || + string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Access" -> EBufRead (translate_expr env e, translate_expr env i) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, (e :: i :: v :: _)) - when string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_upd" -> + when string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_upd" || + string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ x; _w ]) when string_of_mlpath p = "Pulse.Lib.Array.Core.free" -> EBufFree (translate_expr env x) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ x; _p; _w ]) + when string_of_mlpath p = "Pulse.Lib.ArrayPtr.from_array" -> + translate_expr env x + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ a; _p; _fp; _w; i ]) + when string_of_mlpath p = "Pulse.Lib.ArrayPtr.split" -> + EBufSub (translate_expr env a, translate_expr env i) + (* Pulse control, while etc *) | MLE_App ({expr=MLE_Name p}, [{expr=MLE_Fun (_, test)}; {expr=MLE_Fun(_, body)}]) when (string_of_mlpath p = "Pulse.Lib.Core.while_") -> From dd08c8a2cc793713e762c835d267ac7c0252b41e Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 3 Jul 2024 16:08:38 -0700 Subject: [PATCH 06/32] snap --- src/ocaml/plugin/generated/ExtractPulse.ml | 68 ++++++++++++++++++---- 1 file changed, 56 insertions(+), 12 deletions(-) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index d2705ac42..065f30904 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -6,8 +6,9 @@ let (pulse_translate_type_without_decay : match t with | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when let p1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - ((p1 = "Pulse.Lib.Reference.ref") || - (p1 = "Pulse.Lib.Array.Core.array")) + (((p1 = "Pulse.Lib.Reference.ref") || + (p1 = "Pulse.Lib.Array.Core.array")) + || (p1 = "Pulse.Lib.ArrayPtr.ptr")) || (p1 = "Pulse.Lib.Vec.vec") -> let uu___ = @@ -328,16 +329,15 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = uu___3); FStar_Extraction_ML_Syntax.mlty = uu___4; FStar_Extraction_ML_Syntax.loc = uu___5;_}, - e2::i::v::_w::[]) + e2::i::_p::_fp::_w::[]) when let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Array.Core.op_Array_Assignment" -> + uu___6 = "Pulse.Lib.ArrayPtr.op_Array_Access" -> let uu___6 = let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in let uu___8 = FStar_Extraction_Krml.translate_expr env i in - let uu___9 = FStar_Extraction_Krml.translate_expr env v in - (uu___7, uu___8, uu___9) in - FStar_Extraction_Krml.EBufWrite uu___6 + (uu___7, uu___8) in + FStar_Extraction_Krml.EBufRead uu___6 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -352,8 +352,11 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = FStar_Extraction_ML_Syntax.loc = uu___5;_}, e2::i::uu___6) when - let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.Array.Core.pts_to_range_index" -> + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Array.Core.pts_to_range_index") || + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Array.Core.op_Array_Access") + -> let uu___7 = let uu___8 = FStar_Extraction_Krml.translate_expr env e2 in let uu___9 = FStar_Extraction_Krml.translate_expr env i in @@ -373,8 +376,11 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = FStar_Extraction_ML_Syntax.loc = uu___5;_}, e2::i::v::uu___6) when - let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.Array.Core.pts_to_range_upd" -> + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Array.Core.pts_to_range_upd") || + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.ArrayPtr.op_Array_Assignment") + -> let uu___7 = let uu___8 = FStar_Extraction_Krml.translate_expr env e2 in let uu___9 = FStar_Extraction_Krml.translate_expr env i in @@ -399,6 +405,44 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = uu___6 = "Pulse.Lib.Array.Core.free" -> let uu___6 = FStar_Extraction_Krml.translate_expr env x in FStar_Extraction_Krml.EBufFree uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + x::_p::_w::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.from_array" -> + FStar_Extraction_Krml.translate_expr env x + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + a::_p::_fp::_w::i::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.split" -> + let uu___6 = + let uu___7 = FStar_Extraction_Krml.translate_expr env a in + let uu___8 = FStar_Extraction_Krml.translate_expr env i in + (uu___7, uu___8) in + FStar_Extraction_Krml.EBufSub uu___6 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -469,7 +513,7 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = | uu___1 -> FStar_Compiler_Effect.raise FStar_Extraction_Krml.NotSupportedByKrmlExtension) -let (uu___263 : unit) = +let (uu___292 : unit) = FStar_Extraction_Krml.register_pre_translate_type_without_decay pulse_translate_type_without_decay; FStar_Extraction_Krml.register_pre_translate_expr pulse_translate_expr \ No newline at end of file From a7c6df5170f127f85d91555e9ad95ceed73b5162 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 11 Jul 2024 20:17:49 -0700 Subject: [PATCH 07/32] Karamel chokes on tuples, use custom slice pair type instead --- lib/pulse/lib/Pulse.Lib.Slice.fst | 6 +++--- lib/pulse/lib/Pulse.Lib.Slice.fsti | 8 +++++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index 7ed3b3f0e..d24cc971f 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -161,7 +161,7 @@ let is_split_is_small s p i s1 s2 = () ```pulse fn split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) requires pts_to s #p v ** pure (split_precond mutb p v i) - returns res : (slice t & slice t) + returns res : slice_pair t ensures (split_post s p v i res) { unfold (pts_to s #p v); @@ -182,8 +182,8 @@ fn split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq. fold (pts_to s2 #p _v2); fold (is_split s p i s1 s2); fold (split_post' s p v i s1 s2); - fold (split_post s p v i (s1, s2)); - (s1, s2) + fold (split_post s p v i (s1 `SlicePair` s2)); + (s1 `SlicePair` s2) } ``` diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index 13338dde0..7e57c97d0 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -87,6 +87,8 @@ val is_split_is_small (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t : Lemma (is_small (is_split s p i left right)) [SMTPat (is_small (is_split s p i left right))] +noeq type slice_pair (t: Type) = | SlicePair: (fst: slice t) -> (snd: slice t) -> slice_pair t + let split_precond (#t: Type) (mutb: bool) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) : Tot prop @@ -108,12 +110,12 @@ let split_post' let split_post (#t: Type) (s: slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) - (res: (slice t & slice t)) + (res: slice_pair t) : Tot vprop -= let (s1, s2) = res in += let SlicePair s1 s2 = res in split_post' s p v i s1 s2 -val split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice t & slice t) +val split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice_pair t) (requires pts_to s #p v ** pure (split_precond mutb p v i)) (ensures fun res -> split_post s p v i res) From 3db83f3f7c041fc3ab71c193a1980261f1b41467 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 19 Jul 2024 08:42:53 -0700 Subject: [PATCH 08/32] Revert "snap" This reverts commit dd08c8a2cc793713e762c835d267ac7c0252b41e. --- src/ocaml/plugin/generated/ExtractPulse.ml | 68 ++++------------------ 1 file changed, 12 insertions(+), 56 deletions(-) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index 065f30904..d2705ac42 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -6,9 +6,8 @@ let (pulse_translate_type_without_decay : match t with | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when let p1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - (((p1 = "Pulse.Lib.Reference.ref") || - (p1 = "Pulse.Lib.Array.Core.array")) - || (p1 = "Pulse.Lib.ArrayPtr.ptr")) + ((p1 = "Pulse.Lib.Reference.ref") || + (p1 = "Pulse.Lib.Array.Core.array")) || (p1 = "Pulse.Lib.Vec.vec") -> let uu___ = @@ -329,15 +328,16 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = uu___3); FStar_Extraction_ML_Syntax.mlty = uu___4; FStar_Extraction_ML_Syntax.loc = uu___5;_}, - e2::i::_p::_fp::_w::[]) + e2::i::v::_w::[]) when let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.ArrayPtr.op_Array_Access" -> + uu___6 = "Pulse.Lib.Array.Core.op_Array_Assignment" -> let uu___6 = let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in let uu___8 = FStar_Extraction_Krml.translate_expr env i in - (uu___7, uu___8) in - FStar_Extraction_Krml.EBufRead uu___6 + let uu___9 = FStar_Extraction_Krml.translate_expr env v in + (uu___7, uu___8, uu___9) in + FStar_Extraction_Krml.EBufWrite uu___6 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -352,11 +352,8 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = FStar_Extraction_ML_Syntax.loc = uu___5;_}, e2::i::uu___6) when - (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.Array.Core.pts_to_range_index") || - (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.Array.Core.op_Array_Access") - -> + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Array.Core.pts_to_range_index" -> let uu___7 = let uu___8 = FStar_Extraction_Krml.translate_expr env e2 in let uu___9 = FStar_Extraction_Krml.translate_expr env i in @@ -376,11 +373,8 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = FStar_Extraction_ML_Syntax.loc = uu___5;_}, e2::i::v::uu___6) when - (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.Array.Core.pts_to_range_upd") || - (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.ArrayPtr.op_Array_Assignment") - -> + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Array.Core.pts_to_range_upd" -> let uu___7 = let uu___8 = FStar_Extraction_Krml.translate_expr env e2 in let uu___9 = FStar_Extraction_Krml.translate_expr env i in @@ -405,44 +399,6 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = uu___6 = "Pulse.Lib.Array.Core.free" -> let uu___6 = FStar_Extraction_Krml.translate_expr env x in FStar_Extraction_Krml.EBufFree uu___6 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___1; - FStar_Extraction_ML_Syntax.loc = uu___2;_}, - uu___3); - FStar_Extraction_ML_Syntax.mlty = uu___4; - FStar_Extraction_ML_Syntax.loc = uu___5;_}, - x::_p::_w::[]) - when - let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.ArrayPtr.from_array" -> - FStar_Extraction_Krml.translate_expr env x - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___1; - FStar_Extraction_ML_Syntax.loc = uu___2;_}, - uu___3); - FStar_Extraction_ML_Syntax.mlty = uu___4; - FStar_Extraction_ML_Syntax.loc = uu___5;_}, - a::_p::_fp::_w::i::[]) - when - let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.ArrayPtr.split" -> - let uu___6 = - let uu___7 = FStar_Extraction_Krml.translate_expr env a in - let uu___8 = FStar_Extraction_Krml.translate_expr env i in - (uu___7, uu___8) in - FStar_Extraction_Krml.EBufSub uu___6 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -513,7 +469,7 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = | uu___1 -> FStar_Compiler_Effect.raise FStar_Extraction_Krml.NotSupportedByKrmlExtension) -let (uu___292 : unit) = +let (uu___263 : unit) = FStar_Extraction_Krml.register_pre_translate_type_without_decay pulse_translate_type_without_decay; FStar_Extraction_Krml.register_pre_translate_expr pulse_translate_expr \ No newline at end of file From 508b1e1224bc0458a898fdb6748b3a102220c3a5 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 19 Jul 2024 08:45:48 -0700 Subject: [PATCH 09/32] pre-merge: do not extract `inv` type --- src/extraction/ExtractPulse.fst | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst index d9265917b..6aef035ce 100644 --- a/src/extraction/ExtractPulse.fst +++ b/src/extraction/ExtractPulse.fst @@ -30,13 +30,6 @@ let pulse_translate_type_without_decay : translate_type_without_decay_t = fun en -> TBuf (translate_type_without_decay env arg) - | MLTY_Named ([_inv], p) when - (let p = Syntax.string_of_mlpath p in - p = "Pulse.Lib.Core.inv" - ) - -> - TUnit - | _ -> raise NotSupportedByKrmlExtension let flatten_app e = From c8df835dca1a851d47a8ec846cbaa55637ac86dc Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 19 Jul 2024 08:57:43 -0700 Subject: [PATCH 10/32] disentangle ArrayPtr extraction rules from Array.Core --- src/extraction/ExtractPulse.fst | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst index 6aef035ce..afed209fc 100644 --- a/src/extraction/ExtractPulse.fst +++ b/src/extraction/ExtractPulse.fst @@ -87,24 +87,27 @@ let pulse_translate_expr : translate_expr_t = fun env e -> when string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Access" -> EBufRead (translate_expr env e, translate_expr env i) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e; i; _p; _fp; _w ]) - when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Access" -> - EBufRead (translate_expr env e, translate_expr env i) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e; i; v; _w ]) + when string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Assignment" -> + EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, (e :: i :: _)) - when string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_index" || - string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Access" -> + when string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_index" -> EBufRead (translate_expr env e, translate_expr env i) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, (e :: i :: v :: _)) - when string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_upd" || - string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> + when string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_upd" -> EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ x; _w ]) when string_of_mlpath p = "Pulse.Lib.Array.Core.free" -> EBufFree (translate_expr env x) + (* Pulse array pointers (ArrayPtr, as an underlying C extraction for slices *) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e; i; _p; _fp; _w ]) + when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Access" -> + EBufRead (translate_expr env e, translate_expr env i) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ x; _p; _w ]) when string_of_mlpath p = "Pulse.Lib.ArrayPtr.from_array" -> translate_expr env x @@ -113,6 +116,11 @@ let pulse_translate_expr : translate_expr_t = fun env e -> when string_of_mlpath p = "Pulse.Lib.ArrayPtr.split" -> EBufSub (translate_expr env a, translate_expr env i) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, (e :: i :: v :: _)) + when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> + EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v) + + (* Pulse control, while etc *) | MLE_App ({expr=MLE_Name p}, [{expr=MLE_Fun (_, test)}; {expr=MLE_Fun(_, body)}]) when (string_of_mlpath p = "Pulse.Lib.Core.while_") -> From 53a7cf7125e6fd8346cc2cb7a8acbc6f886ba6ff Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 19 Jul 2024 09:27:59 -0700 Subject: [PATCH 11/32] snap --- src/ocaml/plugin/generated/ExtractPulse.ml | 88 +++++++++++++++++++++- 1 file changed, 85 insertions(+), 3 deletions(-) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index 9d8857c5b..dfdb82aae 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -28,8 +28,9 @@ let (pulse_translate_type_without_decay : match t with | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when let p1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - (((p1 = "Pulse.Lib.Reference.ref") || - (p1 = "Pulse.Lib.Array.Core.array")) + ((((p1 = "Pulse.Lib.Reference.ref") || + (p1 = "Pulse.Lib.Array.Core.array")) + || (p1 = "Pulse.Lib.ArrayPtr.ptr")) || (p1 = "Pulse.Lib.Vec.vec")) || (p1 = "Pulse.Lib.Box.box") -> @@ -404,6 +405,87 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___6 = "Pulse.Lib.Array.Core.free" -> let uu___6 = cb x in FStar_Extraction_Krml.EBufFree uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + e2::i::_p::_fp::_w::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.op_Array_Access" -> + let uu___6 = + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___8 = FStar_Extraction_Krml.translate_expr env i in + (uu___7, uu___8) in + FStar_Extraction_Krml.EBufRead uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + x::_p::_w::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.from_array" -> + FStar_Extraction_Krml.translate_expr env x + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + a::_p::_fp::_w::i::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.split" -> + let uu___6 = + let uu___7 = FStar_Extraction_Krml.translate_expr env a in + let uu___8 = FStar_Extraction_Krml.translate_expr env i in + (uu___7, uu___8) in + FStar_Extraction_Krml.EBufSub uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + e2::i::v::uu___6) + when + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> + let uu___7 = + let uu___8 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___9 = FStar_Extraction_Krml.translate_expr env i in + let uu___10 = FStar_Extraction_Krml.translate_expr env v in + (uu___8, uu___9, uu___10) in + FStar_Extraction_Krml.EBufWrite uu___7 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -477,7 +559,7 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = | uu___1 -> FStar_Compiler_Effect.raise FStar_Extraction_Krml.NotSupportedByKrmlExtension) -let (uu___272 : unit) = +let (uu___331 : unit) = FStar_Extraction_Krml.register_pre_translate_type_without_decay pulse_translate_type_without_decay; FStar_Extraction_Krml.register_pre_translate_expr pulse_translate_expr \ No newline at end of file From 798d53346b22390daad7752e346a6a703b2499b2 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 19 Jul 2024 09:37:01 -0700 Subject: [PATCH 12/32] vprop -> slprop; is_small -> is_slprop2 --- lib/pulse/lib/Pulse.Lib.ArrayPtr.fst | 2 +- lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 10 +++++----- lib/pulse/lib/Pulse.Lib.Slice.fst | 4 ++-- lib/pulse/lib/Pulse.Lib.Slice.fsti | 22 +++++++++++----------- 4 files changed, 19 insertions(+), 19 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst index 567a231f1..d6f70382b 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst @@ -17,7 +17,7 @@ let pts_to s #p fp v = A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v fp.len) #p v ** pure (fp.elt == s) -let pts_to_is_small x p fp s = () +let pts_to_is_slprop2 x p fp s = () let is_from_array p fp a = pure (fp.elt.base == a /\ SZ.v fp.len == A.length a) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index 53439d5e9..a706eace7 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -11,13 +11,13 @@ val ptr : Type0 -> Type0 [@@erasable] val footprint : Type0 -> Type0 -val pts_to (#t: Type) (s: ptr t) (#[exact (`1.0R)] p: perm) (fp: footprint t) (v: Seq.seq t) : vprop +val pts_to (#t: Type) (s: ptr t) (#[exact (`1.0R)] p: perm) (fp: footprint t) (v: Seq.seq t) : slprop -val pts_to_is_small (#a:Type) (x:ptr a) (p:perm) (fp: footprint a) (s:Seq.seq a) - : Lemma (is_small (pts_to x #p fp s)) - [SMTPat (is_small (pts_to x #p fp s))] +val pts_to_is_slprop2 (#a:Type) (x:ptr a) (p:perm) (fp: footprint a) (s:Seq.seq a) + : Lemma (is_slprop2 (pts_to x #p fp s)) + [SMTPat (is_slprop2 (pts_to x #p fp s))] -val is_from_array (#t: Type) (p: perm) (fp: footprint t) (a: A.array t) : vprop +val is_from_array (#t: Type) (p: perm) (fp: footprint t) (a: A.array t) : slprop val from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) : stt (ptr t) (A.pts_to a #p v) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index d24cc971f..3973cac99 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -15,7 +15,7 @@ let pts_to #t s #p v = AP.pts_to s.elt #p s.fp v ** pure (Seq.length v == SZ.v s.len) -let pts_to_is_small x p v = () +let pts_to_is_slprop2 x p v = () ```pulse ghost @@ -156,7 +156,7 @@ let is_split #t s p i s1 s2 = SZ.v s.len == SZ.v s1.len + SZ.v s2.len ) -let is_split_is_small s p i s1 s2 = () +let is_split_is_slprop2 s p i s1 s2 = () ```pulse fn split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index 7e57c97d0..52395f019 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -8,17 +8,17 @@ val slice : Type0 -> Type0 val len (#t: Type) : slice t -> SZ.t -val pts_to (#t: Type) (s: slice t) (#[exact (`1.0R)] p: perm) (v: Seq.seq t) : vprop +val pts_to (#t: Type) (s: slice t) (#[exact (`1.0R)] p: perm) (v: Seq.seq t) : slprop -val pts_to_is_small (#a:Type) (x:slice a) (p:perm) (s:Seq.seq a) - : Lemma (is_small (pts_to x #p s)) - [SMTPat (is_small (pts_to x #p s))] +val pts_to_is_slprop2 (#a:Type) (x:slice a) (p:perm) (s:Seq.seq a) + : Lemma (is_slprop2 (pts_to x #p s)) + [SMTPat (is_slprop2 (pts_to x #p s))] val pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) : stt_ghost unit emp_inames (pts_to s #p v) (fun _ -> pts_to s #p v ** pure (Seq.length v == SZ.v (len s))) -val is_from_array (#t: Type) (a: array t) (p: perm) (s: slice t) : vprop +val is_from_array (#t: Type) (a: array t) (p: perm) (s: slice t) : slprop val from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { SZ.v alen == A.length a /\ @@ -81,11 +81,11 @@ val gather (requires pts_to arr #p0 s0 ** pts_to arr #p1 s1) (ensures fun _ -> pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1)) -val is_split (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t) (right: slice t) : vprop +val is_split (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t) (right: slice t) : slprop -val is_split_is_small (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t) (right: slice t) - : Lemma (is_small (is_split s p i left right)) - [SMTPat (is_small (is_split s p i left right))] +val is_split_is_slprop2 (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t) (right: slice t) + : Lemma (is_slprop2 (is_split s p i left right)) + [SMTPat (is_slprop2 (is_split s p i left right))] noeq type slice_pair (t: Type) = | SlicePair: (fst: slice t) -> (snd: slice t) -> slice_pair t @@ -98,7 +98,7 @@ let split_post' (#t: Type) (s: slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) (s1: slice t) (s2: slice t) -: Tot vprop +: Tot slprop = exists* v1 v2 . pts_to s1 #p v1 ** pts_to s2 #p v2 ** @@ -111,7 +111,7 @@ let split_post' let split_post (#t: Type) (s: slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) (res: slice_pair t) -: Tot vprop +: Tot slprop = let SlicePair s1 s2 = res in split_post' s p v i s1 s2 From 5c66c3085dfcdbf3d7df243b7ac47987682d17bb Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 3 Oct 2024 16:46:19 -0700 Subject: [PATCH 13/32] Revert "snap" This reverts commit 53a7cf7125e6fd8346cc2cb7a8acbc6f886ba6ff. --- src/ocaml/plugin/generated/ExtractPulse.ml | 88 +--------------------- 1 file changed, 3 insertions(+), 85 deletions(-) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index dfdb82aae..9d8857c5b 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -28,9 +28,8 @@ let (pulse_translate_type_without_decay : match t with | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when let p1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - ((((p1 = "Pulse.Lib.Reference.ref") || - (p1 = "Pulse.Lib.Array.Core.array")) - || (p1 = "Pulse.Lib.ArrayPtr.ptr")) + (((p1 = "Pulse.Lib.Reference.ref") || + (p1 = "Pulse.Lib.Array.Core.array")) || (p1 = "Pulse.Lib.Vec.vec")) || (p1 = "Pulse.Lib.Box.box") -> @@ -405,87 +404,6 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___6 = "Pulse.Lib.Array.Core.free" -> let uu___6 = cb x in FStar_Extraction_Krml.EBufFree uu___6 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___1; - FStar_Extraction_ML_Syntax.loc = uu___2;_}, - uu___3); - FStar_Extraction_ML_Syntax.mlty = uu___4; - FStar_Extraction_ML_Syntax.loc = uu___5;_}, - e2::i::_p::_fp::_w::[]) - when - let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.ArrayPtr.op_Array_Access" -> - let uu___6 = - let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in - let uu___8 = FStar_Extraction_Krml.translate_expr env i in - (uu___7, uu___8) in - FStar_Extraction_Krml.EBufRead uu___6 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___1; - FStar_Extraction_ML_Syntax.loc = uu___2;_}, - uu___3); - FStar_Extraction_ML_Syntax.mlty = uu___4; - FStar_Extraction_ML_Syntax.loc = uu___5;_}, - x::_p::_w::[]) - when - let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.ArrayPtr.from_array" -> - FStar_Extraction_Krml.translate_expr env x - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___1; - FStar_Extraction_ML_Syntax.loc = uu___2;_}, - uu___3); - FStar_Extraction_ML_Syntax.mlty = uu___4; - FStar_Extraction_ML_Syntax.loc = uu___5;_}, - a::_p::_fp::_w::i::[]) - when - let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.ArrayPtr.split" -> - let uu___6 = - let uu___7 = FStar_Extraction_Krml.translate_expr env a in - let uu___8 = FStar_Extraction_Krml.translate_expr env i in - (uu___7, uu___8) in - FStar_Extraction_Krml.EBufSub uu___6 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___1; - FStar_Extraction_ML_Syntax.loc = uu___2;_}, - uu___3); - FStar_Extraction_ML_Syntax.mlty = uu___4; - FStar_Extraction_ML_Syntax.loc = uu___5;_}, - e2::i::v::uu___6) - when - let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> - let uu___7 = - let uu___8 = FStar_Extraction_Krml.translate_expr env e2 in - let uu___9 = FStar_Extraction_Krml.translate_expr env i in - let uu___10 = FStar_Extraction_Krml.translate_expr env v in - (uu___8, uu___9, uu___10) in - FStar_Extraction_Krml.EBufWrite uu___7 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -559,7 +477,7 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = | uu___1 -> FStar_Compiler_Effect.raise FStar_Extraction_Krml.NotSupportedByKrmlExtension) -let (uu___331 : unit) = +let (uu___272 : unit) = FStar_Extraction_Krml.register_pre_translate_type_without_decay pulse_translate_type_without_decay; FStar_Extraction_Krml.register_pre_translate_expr pulse_translate_expr \ No newline at end of file From db5b6162e77791f8845fe24f55261c0670523e9e Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 3 Oct 2024 17:36:15 -0700 Subject: [PATCH 14/32] sync up to tahina-pro/evercbor@8b15db670299d7ce6916241c1391433de4a39cdc --- lib/pulse/lib/Pulse.Lib.Array.Core.fst | 35 ------ lib/pulse/lib/Pulse.Lib.ArrayPtr.fst | 84 +++++++++++-- lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 52 ++++++-- lib/pulse/lib/Pulse.Lib.Slice.Util.fst | 160 +++++++++++++++++++++++++ lib/pulse/lib/Pulse.Lib.Slice.fst | 17 +++ lib/pulse/lib/Pulse.Lib.Slice.fsti | 4 + src/extraction/ExtractPulse.fst | 5 + 7 files changed, 304 insertions(+), 53 deletions(-) create mode 100644 lib/pulse/lib/Pulse.Lib.Slice.Util.fst diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fst b/lib/pulse/lib/Pulse.Lib.Array.Core.fst index 49be262f7..822d0d067 100644 --- a/lib/pulse/lib/Pulse.Lib.Array.Core.fst +++ b/lib/pulse/lib/Pulse.Lib.Array.Core.fst @@ -398,41 +398,6 @@ fn pts_to_range_gather } ``` -```pulse -ghost -fn pts_to_range_share - (#a:Type) - (arr:array a) - (#l #r: nat) - (#s:Seq.seq a) - (#p:perm) - requires pts_to_range arr l r #p s - ensures pts_to_range arr l r #(p /. 2.0R) s ** pts_to_range arr l r #(p /. 2.0R) s -{ - unfold (pts_to_range arr l r #p s); - H.pts_to_range_share arr; - fold (pts_to_range arr l r #(p /. 2.0R) s); - fold (pts_to_range arr l r #(p /. 2.0R) s); -} -``` - -```pulse -ghost -fn pts_to_range_gather - (#a:Type) - (arr:array a) - (#l #r: nat) - (#s0 #s1: Seq.seq a) - (#p0 #p1:perm) - requires pts_to_range arr l r #p0 s0 ** pts_to_range arr l r #p1 s1 - ensures pts_to_range arr l r #(p0 +. p1) s0 ** pure (s0 == s1) -{ - unfold (pts_to_range arr l r #p0 s0); - unfold (pts_to_range arr l r #p1 s1); - H.pts_to_range_gather arr; - fold (pts_to_range arr l r #(p0 +. p1) s0) -} -``` (* this is universe-polymorphic in ret_t; so can't define it in Pulse yet *) let with_local' diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst index d6f70382b..72ec23bae 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst @@ -69,13 +69,15 @@ fn op_Array_Access (i: SZ.t) (#p: perm) (#fp: footprint t) - (#s: Ghost.erased (Seq.seq t){SZ.v i < Seq.length s}) - requires - pts_to a #p fp s - returns res: t - ensures + (#s: Ghost.erased (Seq.seq t)) + requires + pts_to a #p fp s ** pure (SZ.v i < Seq.length s) + returns res: t + ensures pts_to a #p fp s ** - pure (res == Seq.index s (SZ.v i)) + pure ( + SZ.v i < Seq.length s /\ + res == Seq.index s (SZ.v i)) { unfold (pts_to a #p fp s); A.pts_to_range_prop a.base; @@ -92,11 +94,14 @@ fn op_Array_Assignment (i: SZ.t) (v: t) (#fp: footprint t) - (#s: Ghost.erased (Seq.seq t) {SZ.v i < Seq.length s}) - requires - pts_to a fp s - ensures - pts_to a fp (Seq.upd s (SZ.v i) v) + (#s: Ghost.erased (Seq.seq t)) + requires + pts_to a fp s ** pure (SZ.v i < Seq.length s) + ensures exists* s' . + pts_to a fp s' ** + pure (SZ.v i < Seq.length s /\ + s' == Seq.upd s (SZ.v i) v + ) { unfold (pts_to a fp s); A.pts_to_range_prop a.base; @@ -205,3 +210,60 @@ fn join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint t) (#v1: Seq.seq t) ( fold (pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2)) } ``` + +module R = Pulse.Lib.Reference + +```pulse +fn blit (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t)) (#fp0 #fp1: footprint t) + (src:ptr t) + (idx_src: SZ.t) + (dst:ptr t) + (idx_dst: SZ.t) + (len: SZ.t) +requires + (pts_to src #p0 fp0 s0 ** pts_to dst fp1 s1 ** pure ( + SZ.v idx_src + SZ.v len <= Seq.length s0 /\ + SZ.v idx_dst + SZ.v len <= Seq.length s1 + )) +ensures + (exists* s1' . pts_to src #p0 fp0 s0 ** pts_to dst fp1 s1' ** + pure (blit_post s0 s1 idx_src idx_dst len s1') + ) +{ + unfold (pts_to src #p0 fp0 s0); + A.pts_to_range_prop src.base; + fold (pts_to src #p0 fp0 s0); + let mut pi = 0sz; + while ( + let i = !pi; + SZ.lt i len + ) + invariant b . exists* i s1' . + R.pts_to pi i ** + pts_to src #p0 fp0 s0 ** + pts_to dst fp1 s1' ** + pure ( + SZ.v i <= SZ.v len /\ + b == (SZ.v i < SZ.v len) /\ + blit_post s0 s1 idx_src idx_dst i s1' + ) + { + with s1' . assert (pts_to dst fp1 s1'); + unfold (pts_to dst fp1 s1'); + A.pts_to_range_prop dst.base; + fold (pts_to dst fp1 s1'); + let i = !pi; + let x = op_Array_Access src (SZ.add idx_src i); + op_Array_Assignment dst (SZ.add idx_dst i) x; + pi := SZ.add i 1sz; + Seq.lemma_split (Seq.slice s1' (SZ.v idx_dst) (SZ.v idx_dst + SZ.v (SZ.add i 1sz))) (SZ.v i); + Seq.lemma_split (Seq.slice s0 (SZ.v idx_src) (SZ.v idx_src + SZ.v (SZ.add i 1sz))) (SZ.v i); + Seq.slice_slice s1' (SZ.v idx_dst + SZ.v i) (Seq.length s1') 1 (Seq.length s1' - (SZ.v idx_dst + SZ.v i)); + with s1'' . assert (pts_to dst fp1 s1''); + assert (pure ( + Seq.slice s1'' (SZ.v idx_dst + SZ.v (SZ.add i 1sz)) (Seq.length s1) `Seq.equal` + Seq.slice s1' (SZ.v idx_dst + SZ.v (SZ.add i 1sz)) (Seq.length s1') + )); + }; +} +``` diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index a706eace7..60e1f0173 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -36,13 +36,15 @@ val op_Array_Access (i: SZ.t) (#p: perm) (#fp: footprint t) - (#s: Ghost.erased (Seq.seq t){SZ.v i < Seq.length s}) + (#s: Ghost.erased (Seq.seq t)) : stt t (requires - pts_to a #p fp s) + pts_to a #p fp s ** pure (SZ.v i < Seq.length s)) (ensures fun res -> pts_to a #p fp s ** - pure (res == Seq.index s (SZ.v i))) + pure ( + SZ.v i < Seq.length s /\ + res == Seq.index s (SZ.v i))) (* Written a.(i) <- v *) val op_Array_Assignment @@ -51,12 +53,15 @@ val op_Array_Assignment (i: SZ.t) (v: t) (#fp: footprint t) - (#s: Ghost.erased (Seq.seq t) {SZ.v i < Seq.length s}) + (#s: Ghost.erased (Seq.seq t)) : stt unit (requires - pts_to a fp s) - (ensures fun res -> - pts_to a fp (Seq.upd s (SZ.v i) v)) + pts_to a fp s ** pure (SZ.v i < Seq.length s)) + (ensures fun res -> exists* s' . + pts_to a fp s' ** + pure (SZ.v i < Seq.length s /\ + s' == Seq.upd s (SZ.v i) v + )) val share (#a:Type) @@ -119,3 +124,36 @@ val split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint t) (#v: Ghost.erased val join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint t) (#v1: Seq.seq t) (s2: ptr t) (#fp2: footprint t {adjacent fp1 fp2}) (#v2: Seq.seq t) : stt_ghost unit emp_inames (pts_to s1 #p fp1 v1 ** pts_to s2 #p fp2 v2) (fun _ -> pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2)) + +let blit_post +(#t:_) (s0 s1:Ghost.erased (Seq.seq t)) + (idx_src: SZ.t) + (idx_dst: SZ.t) + (len: SZ.t) + (s1' : Seq.seq t) +: Tot prop += + SZ.v idx_src + SZ.v len <= Seq.length s0 /\ + SZ.v idx_dst + SZ.v len <= Seq.length s1 /\ + Seq.length s1' == Seq.length s1 /\ + Seq.slice s1' (SZ.v idx_dst) (SZ.v idx_dst + SZ.v len) `Seq.equal` + Seq.slice s0 (SZ.v idx_src) (SZ.v idx_src + SZ.v len) /\ + Seq.slice s1' 0 (SZ.v idx_dst) `Seq.equal` + Seq.slice s1 0 (SZ.v idx_dst) /\ + Seq.slice s1' (SZ.v idx_dst + SZ.v len) (Seq.length s1) `Seq.equal` + Seq.slice s1 (SZ.v idx_dst + SZ.v len) (Seq.length s1) + +val blit (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t)) (#fp0 #fp1: footprint t) + (src:ptr t) + (idx_src: SZ.t) + (dst:ptr t) + (idx_dst: SZ.t) + (len: SZ.t) + : stt unit + (pts_to src #p0 fp0 s0 ** pts_to dst fp1 s1 ** pure ( + SZ.v idx_src + SZ.v len <= Seq.length s0 /\ + SZ.v idx_dst + SZ.v len <= Seq.length s1 + )) + (fun _ -> exists* s1' . pts_to src #p0 fp0 s0 ** pts_to dst fp1 s1' ** + pure (blit_post s0 s1 idx_src idx_dst len s1') + ) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst new file mode 100644 index 000000000..a34c39ea1 --- /dev/null +++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst @@ -0,0 +1,160 @@ +module Pulse.Lib.Slice.Util +include Pulse.Lib.Pervasives +include Pulse.Lib.Slice +include Pulse.Lib.Trade + +module S = Pulse.Lib.Slice +module SZ = FStar.SizeT +module T = FStar.Tactics + +noextract +let append_split_precond + (#t: Type) (mutb: bool) (p: perm) (v1: Ghost.erased (Seq.seq t)) (i: SZ.t) +: Tot prop += SZ.v i == Seq.length v1 /\ (mutb == true ==> p == 1.0R) + +let append_split_post' + (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) + (s1: S.slice t) + (s2: S.slice t) +: Tot slprop += + S.pts_to s1 #p v1 ** + S.pts_to s2 #p v2 ** + S.is_split s p i s1 s2 + +let append_split_post + (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) + (res: S.slice_pair t) +: Tot slprop += let S.SlicePair s1 s2 = res in + append_split_post' s p v1 v2 i s1 s2 + +inline_for_extraction +noextract +```pulse +fn append_split (#t: Type) (mutb: bool) (s: S.slice t) (#p: perm) (#v1 #v2: Ghost.erased (Seq.seq t)) (i: SZ.t) + requires S.pts_to s #p (v1 `Seq.append` v2) ** pure (append_split_precond mutb p v1 i) + returns res: S.slice_pair t + ensures append_split_post s p v1 v2 i res +{ + let vs = Ghost.hide (Seq.split (Seq.append v1 v2) (SZ.v i)); + assert (pure (fst vs `Seq.equal` v1)); + assert (pure (snd vs `Seq.equal` v2)); + let res = S.split mutb s i; + match res { + S.SlicePair s1 s2 -> { + unfold (S.split_post s p (Seq.append v1 v2) i res); + unfold (S.split_post' s p (Seq.append v1 v2) i s1 s2); + fold (append_split_post' s p v1 v2 i s1 s2); + fold (append_split_post s p v1 v2 i (S.SlicePair s1 s2)); + (S.SlicePair s1 s2) + } + } +} +``` + +let append_split_trade_post' + (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) + (s1: S.slice t) + (s2: S.slice t) +: Tot slprop += + S.pts_to s1 #p v1 ** + S.pts_to s2 #p v2 ** + (trade (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2) (S.pts_to s #p (v1 `Seq.append` v2))) + +let append_split_trade_post + (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) + (res: S.slice_pair t) +: Tot slprop += let S.SlicePair s1 s2 = res in + append_split_trade_post' s p v1 v2 i s1 s2 + +```pulse +ghost +fn append_split_trade_aux + (#t: Type) (input: S.slice t) (p: perm) (v1 v2: (Seq.seq t)) (i: SZ.t) (input1 input2: S.slice t) (_: unit) + requires S.is_split input p i input1 input2 ** (S.pts_to input1 #p v1 ** S.pts_to input2 #p v2) + ensures S.pts_to input #p (v1 `Seq.append` v2) +{ + S.join input1 input2 input +} +``` + +inline_for_extraction +noextract +```pulse +fn append_split_trade (#t: Type) (mutb: bool) (input: S.slice t) (#p: perm) (#v1 #v2: Ghost.erased (Seq.seq t)) (i: SZ.t) + requires S.pts_to input #p (v1 `Seq.append` v2) ** pure (append_split_precond mutb p v1 i) + returns res: S.slice_pair t + ensures append_split_trade_post input p v1 v2 i res +{ + let res = append_split mutb input i; + match res { + S.SlicePair input1 input2 -> { + unfold (append_split_post input p v1 v2 i res); + unfold (append_split_post' input p v1 v2 i input1 input2); + intro_trade _ _ _ (append_split_trade_aux input p v1 v2 i input1 input2); + fold (append_split_trade_post' input p v1 v2 i input1 input2); + fold (append_split_trade_post input p v1 v2 i (S.SlicePair input1 input2)); + (S.SlicePair input1 input2) + } + } +} +``` + +let split_trade_post' + (#t: Type) (s: S.slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) + (s1: S.slice t) + (s2: S.slice t) +: Tot slprop += exists* v1 v2 . + S.pts_to s1 #p v1 ** + S.pts_to s2 #p v2 ** + (trade (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2) (S.pts_to s #p v)) ** + pure ( + SZ.v i <= Seq.length v /\ + (v1, v2) == Seq.split v (SZ.v i) + ) + +let split_trade_post + (#t: Type) (s: S.slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) + (res: S.slice_pair t) +: Tot slprop += let (S.SlicePair s1 s2) = res in + split_trade_post' s p v i s1 s2 + +```pulse +ghost +fn split_trade_aux + (#t: Type) (s: S.slice t) (p: perm) (v: Seq.seq t) (i: SZ.t) + (s1 s2: S.slice t) (v1 v2: Seq.seq t) (hyp: squash (v == Seq.append v1 v2)) (_: unit) + requires (S.is_split s p i s1 s2 ** (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2)) + ensures (S.pts_to s #p v) + { + S.join s1 s2 s + } +``` + +inline_for_extraction +noextract +```pulse +fn split_trade (#t: Type) (mutb: bool) (s: S.slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) + requires S.pts_to s #p v ** pure (S.split_precond mutb p v i) + returns res: S.slice_pair t + ensures split_trade_post s p v i res +{ + Seq.lemma_split v (SZ.v i); + let res = S.split mutb s i; + match res { S.SlicePair s1 s2 -> { + unfold (S.split_post s p v i res); + unfold (S.split_post' s p v i s1 s2); + with v1 v2 . assert (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2); + intro_trade _ _ _ (split_trade_aux s p v i s1 s2 v1 v2 ()); + fold (split_trade_post' s p v i s1 s2); + fold (split_trade_post s p v i (S.SlicePair s1 s2)); + (S.SlicePair s1 s2) + }} +} +``` diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index 3973cac99..f6f849669 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -200,3 +200,20 @@ fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: fold (pts_to s #p (Seq.append v1 v2)) } ``` + +```pulse +fn copy + (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t)) +requires + (exists* v_dst . pts_to dst v_dst ** pts_to src #p v ** pure (len src == len dst)) +ensures + (pts_to dst v ** pts_to src #p v) +{ + with v_dst . assert (pts_to dst v_dst); + unfold (pts_to dst v_dst); + unfold (pts_to src #p v); + AP.blit src.elt 0sz dst.elt 0sz src.len; + fold (pts_to src #p v); + fold (pts_to dst v) +} +``` diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index 52395f019..5ca4b6efc 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -122,3 +122,7 @@ val split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (#i: SZ.t) (s: slice t) : stt_ghost unit emp_inames (pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s p i s1 s2) (fun _ -> pts_to s #p (Seq.append v1 v2)) + +val copy (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t)) : stt unit + (exists* v_dst . pts_to dst v_dst ** pts_to src #p v ** pure (len src == len dst)) + (fun _ -> pts_to dst v ** pts_to src #p v) diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst index a5a45d09d..4c45b3656 100644 --- a/src/extraction/ExtractPulse.fst +++ b/src/extraction/ExtractPulse.fst @@ -136,6 +136,11 @@ let pulse_translate_expr : translate_expr_t = fun env e -> when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _; _; _; _; e1; e2; e3; e4; e5 ]) when ( + string_of_mlpath p = "Pulse.Lib.ArrayPtr.blit" + ) -> + EBufBlit (translate_expr env e1, translate_expr env e2, translate_expr env e3, translate_expr env e4, translate_expr env e5) + (* Pulse control, while etc *) | MLE_App ({expr=MLE_Name p}, [{expr=MLE_Fun (_, test)}; {expr=MLE_Fun(_, body)}]) From 3be62c5e80dfa9887ceffa1ede873d70e15af1b4 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 3 Oct 2024 17:37:04 -0700 Subject: [PATCH 15/32] snap --- src/ocaml/plugin/generated/ExtractPulse.ml | 112 ++++++++++++++++++++- 1 file changed, 109 insertions(+), 3 deletions(-) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index 46c9ff2eb..838530474 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -28,8 +28,9 @@ let (pulse_translate_type_without_decay : match t with | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when let p1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - (((p1 = "Pulse.Lib.Reference.ref") || - (p1 = "Pulse.Lib.Array.Core.array")) + ((((p1 = "Pulse.Lib.Reference.ref") || + (p1 = "Pulse.Lib.Array.Core.array")) + || (p1 = "Pulse.Lib.ArrayPtr.ptr")) || (p1 = "Pulse.Lib.Vec.vec")) || (p1 = "Pulse.Lib.Box.box") -> @@ -404,6 +405,111 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___6 = "Pulse.Lib.Array.Core.free" -> let uu___6 = cb x in FStar_Extraction_Krml.EBufFree uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + e2::i::_p::_fp::_w::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.op_Array_Access" -> + let uu___6 = + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___8 = FStar_Extraction_Krml.translate_expr env i in + (uu___7, uu___8) in + FStar_Extraction_Krml.EBufRead uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + x::_p::_w::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.from_array" -> + FStar_Extraction_Krml.translate_expr env x + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + a::_p::_fp::_w::i::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.split" -> + let uu___6 = + let uu___7 = FStar_Extraction_Krml.translate_expr env a in + let uu___8 = FStar_Extraction_Krml.translate_expr env i in + (uu___7, uu___8) in + FStar_Extraction_Krml.EBufSub uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + e2::i::v::uu___6) + when + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> + let uu___7 = + let uu___8 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___9 = FStar_Extraction_Krml.translate_expr env i in + let uu___10 = FStar_Extraction_Krml.translate_expr env v in + (uu___8, uu___9, uu___10) in + FStar_Extraction_Krml.EBufWrite uu___7 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + uu___6::uu___7::uu___8::uu___9::uu___10::e11::e2::e3::e4::e5::[]) + when + let uu___11 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___11 = "Pulse.Lib.ArrayPtr.blit" -> + let uu___11 = + let uu___12 = FStar_Extraction_Krml.translate_expr env e11 in + let uu___13 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___14 = FStar_Extraction_Krml.translate_expr env e3 in + let uu___15 = FStar_Extraction_Krml.translate_expr env e4 in + let uu___16 = FStar_Extraction_Krml.translate_expr env e5 in + (uu___12, uu___13, uu___14, uu___15, uu___16) in + FStar_Extraction_Krml.EBufBlit uu___11 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -483,7 +589,7 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = | uu___1 -> FStar_Compiler_Effect.raise FStar_Extraction_Krml.NotSupportedByKrmlExtension) -let (uu___277 : unit) = +let (uu___356 : unit) = FStar_Extraction_Krml.register_pre_translate_type_without_decay pulse_translate_type_without_decay; FStar_Extraction_Krml.register_pre_translate_expr pulse_translate_expr \ No newline at end of file From c72f82b1150920a432276dc6fce19fd6fe2abba6 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Oct 2024 14:54:32 -0700 Subject: [PATCH 16/32] Avoid deprecated triple-backtick syntax. --- lib/pulse/lib/Pulse.Lib.Array.Core.fst | 4 ---- lib/pulse/lib/Pulse.Lib.ArrayPtr.fst | 19 +------------------ lib/pulse/lib/Pulse.Lib.HigherArray.fst | 4 ---- lib/pulse/lib/Pulse.Lib.Slice.Util.fst | 11 +---------- lib/pulse/lib/Pulse.Lib.Slice.fst | 21 +-------------------- share/pulse/examples/bug-reports/Bug166.fst | 3 +-- 6 files changed, 4 insertions(+), 58 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fst b/lib/pulse/lib/Pulse.Lib.Array.Core.fst index 822d0d067..6dd3ff41c 100644 --- a/lib/pulse/lib/Pulse.Lib.Array.Core.fst +++ b/lib/pulse/lib/Pulse.Lib.Array.Core.fst @@ -362,7 +362,6 @@ ensures post free arr } -```pulse ghost fn pts_to_range_share (#a:Type) @@ -378,9 +377,7 @@ fn pts_to_range_share fold (pts_to_range arr l r #(p /. 2.0R) s); fold (pts_to_range arr l r #(p /. 2.0R) s); } -``` -```pulse ghost fn pts_to_range_gather (#a:Type) @@ -396,7 +393,6 @@ fn pts_to_range_gather H.pts_to_range_gather arr; fold (pts_to_range arr l r #(p0 +. p1) s0) } -``` (* this is universe-polymorphic in ret_t; so can't define it in Pulse yet *) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst index 72ec23bae..8bb51c36b 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst @@ -1,4 +1,5 @@ module Pulse.Lib.ArrayPtr +#lang-pulse noeq type ptr t = { @@ -22,7 +23,6 @@ let pts_to_is_slprop2 x p fp s = () let is_from_array p fp a = pure (fp.elt.base == a /\ SZ.v fp.len == A.length a) -```pulse fn from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) requires A.pts_to a #p v returns s: ptr t @@ -44,9 +44,7 @@ fn from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t) fold (pts_to res #p fp v); res } -``` -```pulse ghost fn to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#fp: footprint t) (#v: Seq.seq t) requires pts_to s #p fp v ** is_from_array p fp a ** pure ( @@ -60,9 +58,7 @@ fn to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#fp: footprint t) (#v as (A.pts_to_range a 0 (A.length a) #p v); A.pts_to_range_elim a _ _; } -``` -```pulse fn op_Array_Access (#t: Type) (a: ptr t) @@ -85,9 +81,7 @@ fn op_Array_Access fold (pts_to a #p fp s); res } -``` -```pulse fn op_Array_Assignment (#t: Type) (a: ptr t) @@ -108,9 +102,7 @@ fn op_Array_Assignment let res = A.pts_to_range_upd a.base (SZ.add a.offset i) v; fold (pts_to a fp (Seq.upd s (SZ.v i) v)); } -``` -```pulse ghost fn share (#a:Type) @@ -126,9 +118,7 @@ fn share fold (pts_to arr #(p /. 2.0R) fp s); fold (pts_to arr #(p /. 2.0R) fp s); } -``` -```pulse ghost fn gather (#a:Type) @@ -144,7 +134,6 @@ fn gather A.pts_to_range_gather arr.base; fold (pts_to arr #(p0 +. p1) fp s0) } -``` let adjacent fp1 fp2 = fp1.elt.base == fp2.elt.base /\ @@ -157,7 +146,6 @@ let merge fp1 fp2 = { let merge_assoc fp1 fp2 fp3 = () -```pulse fn split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint t) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) requires pts_to s #p fp v ** pure (SZ.v i <= Seq.length v) returns s' : ptr t @@ -194,9 +182,7 @@ fn split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint t) (#v: Ghost.erased ( fold (pts_to s' #p fp2 s2); s' } -``` -```pulse ghost fn join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint t) (#v1: Seq.seq t) (s2: ptr t) (#fp2: footprint t {adjacent fp1 fp2}) (#v2: Seq.seq t) requires pts_to s1 #p fp1 v1 ** pts_to s2 #p fp2 v2 @@ -209,11 +195,9 @@ fn join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint t) (#v1: Seq.seq t) ( A.pts_to_range_join s1.base (SZ.v s1.offset) (SZ.v s1.offset + SZ.v fp1.len) (SZ.v s1.offset + SZ.v (merge fp1 fp2).len); fold (pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2)) } -``` module R = Pulse.Lib.Reference -```pulse fn blit (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t)) (#fp0 #fp1: footprint t) (src:ptr t) (idx_src: SZ.t) @@ -266,4 +250,3 @@ ensures )); }; } -``` diff --git a/lib/pulse/lib/Pulse.Lib.HigherArray.fst b/lib/pulse/lib/Pulse.Lib.HigherArray.fst index 1247c6e07..d468a2af1 100644 --- a/lib/pulse/lib/Pulse.Lib.HigherArray.fst +++ b/lib/pulse/lib/Pulse.Lib.HigherArray.fst @@ -904,7 +904,6 @@ ensures let pts_to_range_upd = pts_to_range_upd' -```pulse ghost fn pts_to_range_share (#a:Type) @@ -922,9 +921,7 @@ fn pts_to_range_share pts_to_range_intro_ij arr (p /. 2.0R) s l r (); pts_to_range_intro_ij arr (p /. 2.0R) s l r (); } -``` -```pulse ghost fn pts_to_range_gather (#a:Type) @@ -942,4 +939,3 @@ fn pts_to_range_gather gather (array_slice arr l r); fold (pts_to_range arr l r #(p0 +. p1) s0) } -``` diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst index a34c39ea1..f02a31b6f 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst @@ -1,4 +1,5 @@ module Pulse.Lib.Slice.Util +#lang-pulse include Pulse.Lib.Pervasives include Pulse.Lib.Slice include Pulse.Lib.Trade @@ -32,7 +33,6 @@ let append_split_post inline_for_extraction noextract -```pulse fn append_split (#t: Type) (mutb: bool) (s: S.slice t) (#p: perm) (#v1 #v2: Ghost.erased (Seq.seq t)) (i: SZ.t) requires S.pts_to s #p (v1 `Seq.append` v2) ** pure (append_split_precond mutb p v1 i) returns res: S.slice_pair t @@ -52,7 +52,6 @@ fn append_split (#t: Type) (mutb: bool) (s: S.slice t) (#p: perm) (#v1 #v2: Ghos } } } -``` let append_split_trade_post' (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) @@ -71,7 +70,6 @@ let append_split_trade_post = let S.SlicePair s1 s2 = res in append_split_trade_post' s p v1 v2 i s1 s2 -```pulse ghost fn append_split_trade_aux (#t: Type) (input: S.slice t) (p: perm) (v1 v2: (Seq.seq t)) (i: SZ.t) (input1 input2: S.slice t) (_: unit) @@ -80,11 +78,9 @@ fn append_split_trade_aux { S.join input1 input2 input } -``` inline_for_extraction noextract -```pulse fn append_split_trade (#t: Type) (mutb: bool) (input: S.slice t) (#p: perm) (#v1 #v2: Ghost.erased (Seq.seq t)) (i: SZ.t) requires S.pts_to input #p (v1 `Seq.append` v2) ** pure (append_split_precond mutb p v1 i) returns res: S.slice_pair t @@ -102,7 +98,6 @@ fn append_split_trade (#t: Type) (mutb: bool) (input: S.slice t) (#p: perm) (#v1 } } } -``` let split_trade_post' (#t: Type) (s: S.slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) @@ -125,7 +120,6 @@ let split_trade_post = let (S.SlicePair s1 s2) = res in split_trade_post' s p v i s1 s2 -```pulse ghost fn split_trade_aux (#t: Type) (s: S.slice t) (p: perm) (v: Seq.seq t) (i: SZ.t) @@ -135,11 +129,9 @@ fn split_trade_aux { S.join s1 s2 s } -``` inline_for_extraction noextract -```pulse fn split_trade (#t: Type) (mutb: bool) (s: S.slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) requires S.pts_to s #p v ** pure (S.split_precond mutb p v i) returns res: S.slice_pair t @@ -157,4 +149,3 @@ fn split_trade (#t: Type) (mutb: bool) (s: S.slice t) (#p: perm) (#v: Ghost.eras (S.SlicePair s1 s2) }} } -``` diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index f6f849669..fc3a099d8 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -1,4 +1,5 @@ module Pulse.Lib.Slice +#lang-pulse module AP = Pulse.Lib.ArrayPtr @@ -17,7 +18,6 @@ let pts_to #t s #p v = let pts_to_is_slprop2 x p v = () -```pulse ghost fn pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) requires (pts_to s #p v) @@ -27,13 +27,11 @@ ensures (pts_to s #p v ** pure (Seq.length v == SZ.v (len s))) unfold (pts_to s #p v); fold (pts_to s #p v) } -``` let is_from_array #t a p s = AP.is_from_array p s.fp a ** pure (SZ.v s.len == A.length a) -```pulse fn from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { SZ.v alen == A.length a /\ (mutb == true ==> p == 1.0R) @@ -59,9 +57,7 @@ ensures ( fold (is_from_array a p res); res } -``` -```pulse ghost fn to_array (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: array t) @@ -72,9 +68,7 @@ ensures (A.pts_to a #p v) unfold (is_from_array a p s); AP.to_array s.elt a } -``` -```pulse fn op_Array_Access (#t: Type) (a: slice t) @@ -93,9 +87,7 @@ ensures fold (pts_to a #p s); res } -``` -```pulse fn op_Array_Assignment (#t: Type) (a: slice t) @@ -111,9 +103,7 @@ fn op_Array_Assignment AP.op_Array_Assignment a.elt i v; fold (pts_to a (Seq.upd s (SZ.v i) v)) } -``` -```pulse ghost fn share (#a:Type) @@ -129,9 +119,7 @@ ensures pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s fold (pts_to arr #(p /. 2.0R) s); fold (pts_to arr #(p /. 2.0R) s) } -``` -```pulse ghost fn gather (#a:Type) @@ -146,7 +134,6 @@ ensures pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1) AP.gather arr.elt; fold (pts_to arr #(p0 +. p1) s0) } -``` let is_split #t s p i s1 s2 = pure ( @@ -158,7 +145,6 @@ let is_split #t s p i s1 s2 = let is_split_is_slprop2 s p i s1 s2 = () -```pulse fn split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) requires pts_to s #p v ** pure (split_precond mutb p v i) returns res : slice_pair t @@ -185,9 +171,7 @@ fn split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq. fold (split_post s p v i (s1 `SlicePair` s2)); (s1 `SlicePair` s2) } -``` -```pulse ghost fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (#i: SZ.t) (s: slice t) requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s p i s1 s2 @@ -199,9 +183,7 @@ fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: AP.join s1.elt s2.elt; fold (pts_to s #p (Seq.append v1 v2)) } -``` -```pulse fn copy (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t)) requires @@ -216,4 +198,3 @@ ensures fold (pts_to src #p v); fold (pts_to dst v) } -``` diff --git a/share/pulse/examples/bug-reports/Bug166.fst b/share/pulse/examples/bug-reports/Bug166.fst index 38f3e08c8..fa08771e3 100644 --- a/share/pulse/examples/bug-reports/Bug166.fst +++ b/share/pulse/examples/bug-reports/Bug166.fst @@ -1,8 +1,8 @@ module Bug166 open Pulse +#lang-pulse inline_for_extraction noextract -```pulse fn h () requires emp returns x : int @@ -10,5 +10,4 @@ fn h () { 42 } -``` let h2 = h \ No newline at end of file From 55f6d0eae272bba783e368b189687fb858b11022 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Oct 2024 14:56:36 -0700 Subject: [PATCH 17/32] Add copyright headers. --- lib/pulse/lib/Pulse.Lib.ArrayPtr.fst | 16 ++++++++++++++++ lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 16 ++++++++++++++++ lib/pulse/lib/Pulse.Lib.Slice.Util.fst | 16 ++++++++++++++++ lib/pulse/lib/Pulse.Lib.Slice.fst | 16 ++++++++++++++++ lib/pulse/lib/Pulse.Lib.Slice.fsti | 16 ++++++++++++++++ 5 files changed, 80 insertions(+) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst index 8bb51c36b..b300bb7a4 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst @@ -1,3 +1,19 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) + module Pulse.Lib.ArrayPtr #lang-pulse diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index 60e1f0173..9945f42db 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -1,3 +1,19 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) + module Pulse.Lib.ArrayPtr open FStar.Tactics.V2 open Pulse.Lib.Pervasives diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst index f02a31b6f..6e383cf1a 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst @@ -1,3 +1,19 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) + module Pulse.Lib.Slice.Util #lang-pulse include Pulse.Lib.Pervasives diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index fc3a099d8..dda6d0f10 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -1,3 +1,19 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) + module Pulse.Lib.Slice #lang-pulse diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index 5ca4b6efc..efd14f630 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -1,3 +1,19 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) + module Pulse.Lib.Slice open FStar.Tactics.V2 open Pulse.Lib.Pervasives From f47ec37f023131eec470aead51404e3b2802246b Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Oct 2024 15:45:20 -0700 Subject: [PATCH 18/32] Remove footprint. --- lib/pulse/lib/Pulse.Lib.ArrayPtr.fst | 174 ++++++++++--------------- lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 93 +++++-------- lib/pulse/lib/Pulse.Lib.Slice.Util.fst | 6 +- lib/pulse/lib/Pulse.Lib.Slice.fst | 65 ++++----- lib/pulse/lib/Pulse.Lib.Slice.fsti | 20 +-- 5 files changed, 140 insertions(+), 218 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst index b300bb7a4..980ff06cb 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst @@ -23,54 +23,44 @@ type ptr t = { offset: (offset: SZ.t { SZ.v offset <= A.length base}) } -[@@erasable] -noeq -type footprint (t: Type0) = { - elt: ptr t; - len: (len: SZ.t { SZ.v elt.offset + SZ.v len <= A.length elt.base}); -} +let base a = a.base +let offset a = SZ.v a.offset -let pts_to s #p fp v = - A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v fp.len) #p v ** - pure (fp.elt == s) +let pts_to s #p v = + A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v -let pts_to_is_slprop2 x p fp s = () +let pts_to_is_slprop2 x p s = () -let is_from_array p fp a = - pure (fp.elt.base == a /\ SZ.v fp.len == A.length a) +let is_from_array s sz a = + pure (sz == A.length a /\ s.base == a) fn from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) requires A.pts_to a #p v returns s: ptr t - ensures exists* fp . pts_to s #p fp v ** is_from_array p fp a + ensures pts_to s #p v ** is_from_array s (Seq.length v) a { A.pts_to_len a; let res = { base = a; offset = 0sz; }; - let fp = { - elt = res; - len = SZ.uint_to_t (A.length a); - }; - fold (is_from_array p fp a); + fold (is_from_array res (Seq.length v) a); A.pts_to_range_intro a p v; rewrite (A.pts_to_range a 0 (A.length a) #p v) - as (A.pts_to_range res.base (SZ.v res.offset) (SZ.v res.offset + SZ.v fp.len) #p v); - fold (pts_to res #p fp v); + as (A.pts_to_range res.base (SZ.v res.offset) (SZ.v res.offset + Seq.length v) #p v); + fold (pts_to res #p v); res } ghost -fn to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#fp: footprint t) (#v: Seq.seq t) - requires pts_to s #p fp v ** is_from_array p fp a ** pure ( - Seq.length v == A.length a - ) +fn to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#v: Seq.seq t) + requires pts_to s #p v ** is_from_array s (Seq.length v) a ensures A.pts_to a #p v { - unfold (is_from_array p fp a); - unfold (pts_to s #p fp v); - rewrite (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v fp.len) #p v) + unfold is_from_array s (Seq.length v) a; + unfold pts_to s #p v; + A.pts_to_range_prop s.base; + rewrite (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v) as (A.pts_to_range a 0 (A.length a) #p v); A.pts_to_range_elim a _ _; } @@ -80,21 +70,20 @@ fn op_Array_Access (a: ptr t) (i: SZ.t) (#p: perm) - (#fp: footprint t) (#s: Ghost.erased (Seq.seq t)) requires - pts_to a #p fp s ** pure (SZ.v i < Seq.length s) + pts_to a #p s ** pure (SZ.v i < Seq.length s) returns res: t ensures - pts_to a #p fp s ** + pts_to a #p s ** pure ( SZ.v i < Seq.length s /\ res == Seq.index s (SZ.v i)) { - unfold (pts_to a #p fp s); + unfold pts_to a #p s; A.pts_to_range_prop a.base; let res = A.pts_to_range_index a.base (SZ.add a.offset i); - fold (pts_to a #p fp s); + fold pts_to a #p s; res } @@ -103,20 +92,19 @@ fn op_Array_Assignment (a: ptr t) (i: SZ.t) (v: t) - (#fp: footprint t) (#s: Ghost.erased (Seq.seq t)) requires - pts_to a fp s ** pure (SZ.v i < Seq.length s) + pts_to a s ** pure (SZ.v i < Seq.length s) ensures exists* s' . - pts_to a fp s' ** + pts_to a s' ** pure (SZ.v i < Seq.length s /\ s' == Seq.upd s (SZ.v i) v ) { - unfold (pts_to a fp s); + unfold pts_to a s; A.pts_to_range_prop a.base; let res = A.pts_to_range_upd a.base (SZ.add a.offset i) v; - fold (pts_to a fp (Seq.upd s (SZ.v i) v)); + fold pts_to a (Seq.upd s (SZ.v i) v); } ghost @@ -124,15 +112,14 @@ fn share (#a:Type) (arr:ptr a) (#s:Ghost.erased (Seq.seq a)) - (#fp: footprint a) (#p:perm) - requires pts_to arr #p fp s - ensures pts_to arr #(p /. 2.0R) fp s ** pts_to arr #(p /. 2.0R) fp s + requires pts_to arr #p s + ensures pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s { - unfold (pts_to arr #p fp s); + unfold pts_to arr #p s; A.pts_to_range_share arr.base; - fold (pts_to arr #(p /. 2.0R) fp s); - fold (pts_to arr #(p /. 2.0R) fp s); + fold pts_to arr #(p /. 2.0R) s; + fold pts_to arr #(p /. 2.0R) s; } ghost @@ -141,98 +128,77 @@ fn gather (arr:ptr a) (#s0 #s1:Ghost.erased (Seq.seq a)) (#p0 #p1:perm) - (#fp: footprint a) - requires pts_to arr #p0 fp s0 ** pts_to arr #p1 fp s1 - ensures pts_to arr #(p0 +. p1) fp s0 ** pure (s0 == s1) + requires pts_to arr #p0 s0 ** pts_to arr #p1 s1 ** pure (Seq.length s0 == Seq.length s1) + ensures pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1) { - unfold (pts_to arr #p0 fp s0); - unfold (pts_to arr #p1 fp s1); + unfold pts_to arr #p0 s0; + unfold pts_to arr #p1 s1; A.pts_to_range_gather arr.base; - fold (pts_to arr #(p0 +. p1) fp s0) + fold pts_to arr #(p0 +. p1) s0 } -let adjacent fp1 fp2 = - fp1.elt.base == fp2.elt.base /\ - SZ.v fp1.elt.offset + SZ.v fp1.len == SZ.v fp2.elt.offset - -let merge fp1 fp2 = { - elt = fp1.elt; - len = SZ.add fp1.len fp2.len; -} - -let merge_assoc fp1 fp2 fp3 = () - -fn split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint t) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) - requires pts_to s #p fp v ** pure (SZ.v i <= Seq.length v) - returns s' : ptr t - ensures - exists* v1 v2 fp1 fp2 . - pts_to s #p fp1 v1 ** - pts_to s' #p fp2 v2 ** - pure (split_postcond fp v i v1 v2 fp1 fp2) +fn split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t { SZ.v i <= Seq.length v }) + requires pts_to s #p v + returns s' : ptr t + ensures + pts_to s #p (Seq.slice v 0 (SZ.v i)) ** + pts_to s' #p (Seq.slice v (SZ.v i) (Seq.length v)) ** + pure (adjacent s (SZ.v i) s') { - unfold (pts_to s #p fp v); + unfold pts_to s #p v; A.pts_to_range_prop s.base; let s' = { base = s.base; offset = SZ.add s.offset i; }; - let fp1 = { - elt = fp.elt; - len = i; - }; - let fp2 = { - elt = s'; - len = SZ.sub fp.len i; - }; A.pts_to_range_split s.base _ (SZ.v s'.offset) _; - with s1 . assert (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1); + with s1. assert A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1; rewrite (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1) - as (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v fp1.len) #p s1); - fold (pts_to s #p fp1 s1); - with s2 . assert (A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + SZ.v fp.len) #p s2); + as (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v i) #p s1); + fold pts_to s #p s1; + with s2. assert A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2; rewrite - (A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + SZ.v fp.len) #p s2) - as (A.pts_to_range s'.base (SZ.v s'.offset) (SZ.v s'.offset + SZ.v fp2.len) #p s2); - fold (pts_to s' #p fp2 s2); + (A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2) + as (A.pts_to_range s'.base (SZ.v s'.offset) (SZ.v s'.offset + Seq.length s2) #p s2); + fold pts_to s' #p s2; s' } ghost -fn join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint t) (#v1: Seq.seq t) (s2: ptr t) (#fp2: footprint t {adjacent fp1 fp2}) (#v2: Seq.seq t) - requires pts_to s1 #p fp1 v1 ** pts_to s2 #p fp2 v2 - ensures pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2) +fn join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq.seq t) + requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2) + ensures pts_to s1 #p (Seq.append v1 v2) { - unfold (pts_to s1 #p fp1 v1); - unfold (pts_to s2 #p fp2 v2); - rewrite (A.pts_to_range s2.base (SZ.v s2.offset) (SZ.v s2.offset + SZ.v fp2.len) #p v2) - as (A.pts_to_range s1.base (SZ.v s1.offset + SZ.v fp1.len) (SZ.v s1.offset + SZ.v (merge fp1 fp2).len) #p v2); - A.pts_to_range_join s1.base (SZ.v s1.offset) (SZ.v s1.offset + SZ.v fp1.len) (SZ.v s1.offset + SZ.v (merge fp1 fp2).len); - fold (pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2)) + unfold pts_to s1 #p v1; + unfold pts_to s2 #p v2; + rewrite (A.pts_to_range s2.base (SZ.v s2.offset) (SZ.v s2.offset + Seq.length v2) #p v2) + 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); + 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); + fold (pts_to s1 #p (Seq.append v1 v2)) } module R = Pulse.Lib.Reference -fn blit (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t)) (#fp0 #fp1: footprint t) +fn blit (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t)) (src:ptr t) (idx_src: SZ.t) (dst:ptr t) (idx_dst: SZ.t) (len: SZ.t) requires - (pts_to src #p0 fp0 s0 ** pts_to dst fp1 s1 ** pure ( + (pts_to src #p0 s0 ** pts_to dst s1 ** pure ( SZ.v idx_src + SZ.v len <= Seq.length s0 /\ SZ.v idx_dst + SZ.v len <= Seq.length s1 )) ensures - (exists* s1' . pts_to src #p0 fp0 s0 ** pts_to dst fp1 s1' ** + (exists* s1' . pts_to src #p0 s0 ** pts_to dst s1' ** pure (blit_post s0 s1 idx_src idx_dst len s1') ) { - unfold (pts_to src #p0 fp0 s0); + unfold (pts_to src #p0 s0); A.pts_to_range_prop src.base; - fold (pts_to src #p0 fp0 s0); + fold (pts_to src #p0 s0); let mut pi = 0sz; while ( let i = !pi; @@ -240,18 +206,18 @@ ensures ) invariant b . exists* i s1' . R.pts_to pi i ** - pts_to src #p0 fp0 s0 ** - pts_to dst fp1 s1' ** + pts_to src #p0 s0 ** + pts_to dst s1' ** pure ( SZ.v i <= SZ.v len /\ b == (SZ.v i < SZ.v len) /\ blit_post s0 s1 idx_src idx_dst i s1' ) { - with s1' . assert (pts_to dst fp1 s1'); - unfold (pts_to dst fp1 s1'); + with s1'. assert pts_to dst s1'; + unfold pts_to dst s1'; A.pts_to_range_prop dst.base; - fold (pts_to dst fp1 s1'); + fold pts_to dst s1'; let i = !pi; let x = op_Array_Access src (SZ.add idx_src i); op_Array_Assignment dst (SZ.add idx_dst i) x; @@ -259,7 +225,7 @@ ensures Seq.lemma_split (Seq.slice s1' (SZ.v idx_dst) (SZ.v idx_dst + SZ.v (SZ.add i 1sz))) (SZ.v i); Seq.lemma_split (Seq.slice s0 (SZ.v idx_src) (SZ.v idx_src + SZ.v (SZ.add i 1sz))) (SZ.v i); Seq.slice_slice s1' (SZ.v idx_dst + SZ.v i) (Seq.length s1') 1 (Seq.length s1' - (SZ.v idx_dst + SZ.v i)); - with s1'' . assert (pts_to dst fp1 s1''); + with s1''. assert pts_to dst s1''; assert (pure ( Seq.slice s1'' (SZ.v idx_dst + SZ.v (SZ.add i 1sz)) (Seq.length s1) `Seq.equal` Seq.slice s1' (SZ.v idx_dst + SZ.v (SZ.add i 1sz)) (Seq.length s1') diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index 9945f42db..52afd79b9 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -24,25 +24,23 @@ module A = Pulse.Lib.Array val ptr : Type0 -> Type0 -[@@erasable] -val footprint : Type0 -> Type0 +val base #t (p: ptr t) : GTot (A.array t) +val offset #t (p: ptr t) : GTot nat -val pts_to (#t: Type) (s: ptr t) (#[exact (`1.0R)] p: perm) (fp: footprint t) (v: Seq.seq t) : slprop +val pts_to (#t: Type) (s: ptr t) (#[exact (`1.0R)] p: perm) (v: Seq.seq t) : slprop -val pts_to_is_slprop2 (#a:Type) (x:ptr a) (p:perm) (fp: footprint a) (s:Seq.seq a) - : Lemma (is_slprop2 (pts_to x #p fp s)) - [SMTPat (is_slprop2 (pts_to x #p fp s))] +val pts_to_is_slprop2 (#a:Type) (x:ptr a) (p:perm) (s:Seq.seq a) + : Lemma (is_slprop2 (pts_to x #p s)) + [SMTPat (is_slprop2 (pts_to x #p s))] -val is_from_array (#t: Type) (p: perm) (fp: footprint t) (a: A.array t) : slprop +val is_from_array (#t: Type) (s: ptr t) (sz: nat) (a: A.array t) : slprop val from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) : stt (ptr t) (A.pts_to a #p v) - (fun s -> exists* fp . pts_to s #p fp v ** is_from_array p fp a) + (fun s -> pts_to s #p v ** is_from_array s (Seq.length v) a) -val to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#fp: footprint t) (#v: Seq.seq t) : stt_ghost unit emp_inames - (pts_to s #p fp v ** is_from_array p fp a ** pure ( - Seq.length v == A.length a - )) +val to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#v: Seq.seq t) : stt_ghost unit emp_inames + (pts_to s #p v ** is_from_array s (Seq.length v) a) (fun _ -> A.pts_to a #p v) (* Written x.(i) *) @@ -51,13 +49,12 @@ val op_Array_Access (a: ptr t) (i: SZ.t) (#p: perm) - (#fp: footprint t) (#s: Ghost.erased (Seq.seq t)) : stt t (requires - pts_to a #p fp s ** pure (SZ.v i < Seq.length s)) + pts_to a #p s ** pure (SZ.v i < Seq.length s)) (ensures fun res -> - pts_to a #p fp s ** + pts_to a #p s ** pure ( SZ.v i < Seq.length s /\ res == Seq.index s (SZ.v i))) @@ -68,13 +65,12 @@ val op_Array_Assignment (a: ptr t) (i: SZ.t) (v: t) - (#fp: footprint t) (#s: Ghost.erased (Seq.seq t)) : stt unit (requires - pts_to a fp s ** pure (SZ.v i < Seq.length s)) + pts_to a s ** pure (SZ.v i < Seq.length s)) (ensures fun res -> exists* s' . - pts_to a fp s' ** + pts_to a s' ** pure (SZ.v i < Seq.length s /\ s' == Seq.upd s (SZ.v i) v )) @@ -83,11 +79,10 @@ val share (#a:Type) (arr:ptr a) (#s:Ghost.erased (Seq.seq a)) - (#fp: footprint a) (#p:perm) : stt_ghost unit emp_inames - (requires pts_to arr #p fp s) - (ensures fun _ -> pts_to arr #(p /. 2.0R) fp s ** pts_to arr #(p /. 2.0R) fp s) + (requires pts_to arr #p s) + (ensures fun _ -> pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s) [@@allow_ambiguous] val gather @@ -95,51 +90,25 @@ val gather (arr:ptr a) (#s0 #s1:Ghost.erased (Seq.seq a)) (#p0 #p1:perm) - (#fp: footprint a) : stt_ghost unit emp_inames - (requires pts_to arr #p0 fp s0 ** pts_to arr #p1 fp s1) - (ensures fun _ -> pts_to arr #(p0 +. p1) fp s0 ** pure (s0 == s1)) - -val adjacent (#t: Type): footprint t -> footprint t -> prop + (requires pts_to arr #p0 s0 ** pts_to arr #p1 s1 ** pure (Seq.length s0 == Seq.length s1)) + (ensures fun _ -> pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1)) -val merge (#t: Type): (fp1: footprint t) -> (fp2: footprint t {adjacent fp1 fp2}) -> footprint t -val merge_assoc (#t: Type): (fp1: footprint t) -> (fp2: footprint t) -> (fp3: footprint t) -> Lemma - (ensures ( - ((adjacent fp1 fp2 /\ adjacent (merge fp1 fp2) fp3) <==> (adjacent fp1 fp2 /\ adjacent fp2 fp3)) /\ - ((adjacent fp2 fp3 /\ adjacent fp1 (merge fp2 fp3)) <==> (adjacent fp1 fp2 /\ adjacent fp2 fp3)) /\ - ((adjacent fp1 fp2 /\ adjacent fp2 fp3) ==> - merge (merge fp1 fp2) fp3 == merge fp1 (merge fp2 fp3) - ) - )) - [SMTPatOr [ - [SMTPat (adjacent fp1 fp2); SMTPat (adjacent (merge fp1 fp2) fp3)]; - [SMTPat (adjacent fp2 fp3); SMTPat (adjacent fp1 (merge fp2 fp3))]; - [SMTPat (adjacent fp1 fp2); SMTPat (adjacent fp2 fp3)]; - ]] - -let split_postcond - (#t: Type) (fp: footprint t) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) - (v1: Seq.seq t) (v2: Seq.seq t) (fp1: footprint t) (fp2: footprint t) -: Tot prop -= - adjacent fp1 fp2 /\ - merge fp1 fp2 == fp /\ - SZ.v i <= Seq.length v /\ - (v1, v2) == Seq.split v (SZ.v i) +let adjacent #t (a: ptr t) (sz: nat) (b: ptr t) : prop = + base a == base b /\ offset a + sz == offset b -val split (#t: Type) (s: ptr t) (#p: perm) (#fp: footprint t) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (ptr t) - (requires pts_to s #p fp v ** pure (SZ.v i <= Seq.length v)) +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) + (requires pts_to s #p v) (ensures fun s' -> - exists* v1 v2 fp1 fp2 . - pts_to s #p fp1 v1 ** - pts_to s' #p fp2 v2 ** - pure (split_postcond fp v i v1 v2 fp1 fp2) + pts_to s #p (Seq.slice v 0 (SZ.v i)) ** + pts_to s' #p (Seq.slice v (SZ.v i) (Seq.length v)) ** + pure (adjacent s (SZ.v i) s') ) -val join (#t: Type) (s1: ptr t) (#p: perm) (#fp1: footprint t) (#v1: Seq.seq t) (s2: ptr t) (#fp2: footprint t {adjacent fp1 fp2}) (#v2: Seq.seq t) : stt_ghost unit emp_inames - (pts_to s1 #p fp1 v1 ** pts_to s2 #p fp2 v2) - (fun _ -> pts_to s1 #p (merge fp1 fp2) (Seq.append v1 v2)) +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 + (pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2)) + (fun _ -> pts_to s1 #p (Seq.append v1 v2)) let blit_post (#t:_) (s0 s1:Ghost.erased (Seq.seq t)) @@ -159,17 +128,17 @@ let blit_post Seq.slice s1' (SZ.v idx_dst + SZ.v len) (Seq.length s1) `Seq.equal` Seq.slice s1 (SZ.v idx_dst + SZ.v len) (Seq.length s1) -val blit (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t)) (#fp0 #fp1: footprint t) +val blit (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t)) (src:ptr t) (idx_src: SZ.t) (dst:ptr t) (idx_dst: SZ.t) (len: SZ.t) : stt unit - (pts_to src #p0 fp0 s0 ** pts_to dst fp1 s1 ** pure ( + (pts_to src #p0 s0 ** pts_to dst s1 ** pure ( SZ.v idx_src + SZ.v len <= Seq.length s0 /\ SZ.v idx_dst + SZ.v len <= Seq.length s1 )) - (fun _ -> exists* s1' . pts_to src #p0 fp0 s0 ** pts_to dst fp1 s1' ** + (fun _ -> exists* s1' . pts_to src #p0 s0 ** pts_to dst s1' ** pure (blit_post s0 s1 idx_src idx_dst len s1') ) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst index 6e383cf1a..cfdb4d45e 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst @@ -38,7 +38,7 @@ let append_split_post' = S.pts_to s1 #p v1 ** S.pts_to s2 #p v2 ** - S.is_split s p i s1 s2 + S.is_split s s1 s2 let append_split_post (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) @@ -89,7 +89,7 @@ let append_split_trade_post ghost fn append_split_trade_aux (#t: Type) (input: S.slice t) (p: perm) (v1 v2: (Seq.seq t)) (i: SZ.t) (input1 input2: S.slice t) (_: unit) - requires S.is_split input p i input1 input2 ** (S.pts_to input1 #p v1 ** S.pts_to input2 #p v2) + requires S.is_split input input1 input2 ** (S.pts_to input1 #p v1 ** S.pts_to input2 #p v2) ensures S.pts_to input #p (v1 `Seq.append` v2) { S.join input1 input2 input @@ -140,7 +140,7 @@ ghost fn split_trade_aux (#t: Type) (s: S.slice t) (p: perm) (v: Seq.seq t) (i: SZ.t) (s1 s2: S.slice t) (v1 v2: Seq.seq t) (hyp: squash (v == Seq.append v1 v2)) (_: unit) - requires (S.is_split s p i s1 s2 ** (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2)) + requires (S.is_split s s1 s2 ** (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2)) ensures (S.pts_to s #p v) { S.join s1 s2 s diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index dda6d0f10..c658a5ffd 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -23,65 +23,55 @@ noeq type slice t = { elt: AP.ptr t; len: SZ.t; - fp: AP.footprint t; } let len s = s.len let pts_to #t s #p v = - AP.pts_to s.elt #p s.fp v ** + AP.pts_to s.elt #p v ** pure (Seq.length v == SZ.v s.len) let pts_to_is_slprop2 x p v = () ghost fn pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) -requires (pts_to s #p v) -ensures (pts_to s #p v ** pure (Seq.length v == SZ.v (len s))) - + requires pts_to s #p v + ensures pts_to s #p v ** pure (Seq.length v == SZ.v (len s)) { unfold (pts_to s #p v); fold (pts_to s #p v) } -let is_from_array #t a p s = - AP.is_from_array p s.fp a ** - pure (SZ.v s.len == A.length a) - -fn from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { - SZ.v alen == A.length a /\ - (mutb == true ==> p == 1.0R) -}) -requires (A.pts_to a #p v) -returns s: (slice t) -ensures ( - pts_to s #p v ** - is_from_array a p s - ) +let is_from_array a s = + AP.is_from_array s.elt (SZ.v s.len) a + +fn from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) + (alen: SZ.t { SZ.v alen == A.length a /\ (mutb == true ==> p == 1.0R) }) + requires A.pts_to a #p v + returns s: (slice t) + ensures + pts_to s #p v ** + is_from_array a s { A.pts_to_len a; let ptr = AP.from_array a; - with fp . assert (AP.pts_to ptr #p fp v ** AP.is_from_array p fp a); let res : slice t = { elt = ptr; len = alen; - fp = fp; }; - rewrite (AP.pts_to ptr #p fp v) as (AP.pts_to res.elt #p res.fp v); - fold (pts_to res #p v); - rewrite (AP.is_from_array p fp a) as (AP.is_from_array p res.fp a); - fold (is_from_array a p res); + fold pts_to res #p v; + fold is_from_array a res; res } ghost fn to_array (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: array t) -requires (pts_to s #p v ** is_from_array a p s) +requires (pts_to s #p v ** is_from_array a s) ensures (A.pts_to a #p v) { unfold (pts_to s #p v); - unfold (is_from_array a p s); + unfold is_from_array a s; AP.to_array s.elt a } @@ -151,15 +141,14 @@ ensures pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1) fold (pts_to arr #(p0 +. p1) s0) } -let is_split #t s p i s1 s2 = +let is_split #t s s1 s2 = pure ( s1.elt == s.elt /\ - AP.adjacent s1.fp s2.fp /\ - AP.merge s1.fp s2.fp == s.fp /\ + AP.adjacent s1.elt (SZ.v s1.len) s2.elt /\ SZ.v s.len == SZ.v s1.len + SZ.v s2.len ) -let is_split_is_slprop2 s p i s1 s2 = () +let is_split_is_slprop2 s s1 s2 = () fn split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) requires pts_to s #p v ** pure (split_precond mutb p v i) @@ -168,32 +157,30 @@ fn split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq. { unfold (pts_to s #p v); Seq.lemma_split v (SZ.v i); - let elt' = AP.split s.elt i; - with fp1 _v1 fp2 _v2 . assert (AP.pts_to s.elt #p fp1 _v1 ** AP.pts_to elt' #p fp2 _v2 ** pure (AP.split_postcond s.fp v i _v1 _v2 fp1 fp2)); + let elt' = AP.split s.elt #p #v i; + with _v1 _v2. assert AP.pts_to s.elt #p _v1 ** AP.pts_to elt' #p _v2; let s1 = { elt = s.elt; len = i; - fp = fp1; }; fold (pts_to s1 #p _v1); let s2 = { elt = elt'; len = s.len `SZ.sub` i; - fp = fp2; }; fold (pts_to s2 #p _v2); - fold (is_split s p i s1 s2); + fold (is_split s s1 s2); fold (split_post' s p v i s1 s2); fold (split_post s p v i (s1 `SlicePair` s2)); (s1 `SlicePair` s2) } ghost -fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (#i: SZ.t) (s: slice t) - requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s p i s1 s2 +fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (s: slice t) + requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s s1 s2 ensures pts_to s #p (Seq.append v1 v2) { - unfold (is_split s p i s1 s2); + unfold (is_split s s1 s2); unfold (pts_to s1 #p v1); unfold (pts_to s2 #p v2); AP.join s1.elt s2.elt; diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index efd14f630..c9cc6ecf2 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -34,7 +34,7 @@ val pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) : stt_ghost un (pts_to s #p v) (fun _ -> pts_to s #p v ** pure (Seq.length v == SZ.v (len s))) -val is_from_array (#t: Type) (a: array t) (p: perm) (s: slice t) : slprop +val is_from_array (#t: Type) (a: array t) (s: slice t) : slprop val from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { SZ.v alen == A.length a /\ @@ -43,11 +43,11 @@ val from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (A.pts_to a #p v) (fun s -> pts_to s #p v ** - is_from_array a p s + is_from_array a s ) val to_array (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: array t) : stt_ghost unit emp_inames - (pts_to s #p v ** is_from_array a p s) + (pts_to s #p v ** is_from_array a s) (fun _ -> A.pts_to a #p v) (* Written x.(i) *) @@ -97,11 +97,11 @@ val gather (requires pts_to arr #p0 s0 ** pts_to arr #p1 s1) (ensures fun _ -> pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1)) -val is_split (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t) (right: slice t) : slprop +val is_split (#t: Type) (s: slice t) (left: slice t) (right: slice t) : slprop -val is_split_is_slprop2 (#t: Type) (s: slice t) (p: perm) (i: SZ.t) (left: slice t) (right: slice t) - : Lemma (is_slprop2 (is_split s p i left right)) - [SMTPat (is_slprop2 (is_split s p i left right))] +val is_split_is_slprop2 (#t: Type) (s: slice t) (left: slice t) (right: slice t) + : Lemma (is_slprop2 (is_split s left right)) + [SMTPat (is_slprop2 (is_split s left right))] noeq type slice_pair (t: Type) = | SlicePair: (fst: slice t) -> (snd: slice t) -> slice_pair t @@ -118,7 +118,7 @@ let split_post' = exists* v1 v2 . pts_to s1 #p v1 ** pts_to s2 #p v2 ** - is_split s p i s1 s2 ** + is_split s s1 s2 ** pure ( SZ.v i <= Seq.length v /\ (v1, v2) == Seq.split v (SZ.v i) @@ -135,8 +135,8 @@ val split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq (requires pts_to s #p v ** pure (split_precond mutb p v i)) (ensures fun res -> split_post s p v i res) -val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (#i: SZ.t) (s: slice t) : stt_ghost unit emp_inames - (pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s p i s1 s2) +val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (s: slice t) : stt_ghost unit emp_inames + (pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s s1 s2) (fun _ -> pts_to s #p (Seq.append v1 v2)) val copy (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t)) : stt unit From a088160504e6952ed6ebfc43ffb54dbfce7c47ce Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Oct 2024 15:52:09 -0700 Subject: [PATCH 19/32] snap --- src/ocaml/plugin/generated/ExtractPulse.ml | 110 ++++++++++++++++++++- 1 file changed, 108 insertions(+), 2 deletions(-) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index 2382123d6..20062bbcd 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -28,8 +28,9 @@ let (pulse_translate_type_without_decay : match t with | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when let p1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - (((p1 = "Pulse.Lib.Reference.ref") || - (p1 = "Pulse.Lib.Array.Core.array")) + ((((p1 = "Pulse.Lib.Reference.ref") || + (p1 = "Pulse.Lib.Array.Core.array")) + || (p1 = "Pulse.Lib.ArrayPtr.ptr")) || (p1 = "Pulse.Lib.Vec.vec")) || (p1 = "Pulse.Lib.Box.box") -> @@ -404,6 +405,111 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___6 = "Pulse.Lib.Array.Core.free" -> let uu___6 = cb x in FStar_Extraction_Krml.EBufFree uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + e2::i::_p::_fp::_w::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.op_Array_Access" -> + let uu___6 = + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___8 = FStar_Extraction_Krml.translate_expr env i in + (uu___7, uu___8) in + FStar_Extraction_Krml.EBufRead uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + x::_p::_w::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.from_array" -> + FStar_Extraction_Krml.translate_expr env x + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + a::_p::_fp::_w::i::[]) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.ArrayPtr.split" -> + let uu___6 = + let uu___7 = FStar_Extraction_Krml.translate_expr env a in + let uu___8 = FStar_Extraction_Krml.translate_expr env i in + (uu___7, uu___8) in + FStar_Extraction_Krml.EBufSub uu___6 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + e2::i::v::uu___6) + when + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> + let uu___7 = + let uu___8 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___9 = FStar_Extraction_Krml.translate_expr env i in + let uu___10 = FStar_Extraction_Krml.translate_expr env v in + (uu___8, uu___9, uu___10) in + FStar_Extraction_Krml.EBufWrite uu___7 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + uu___6::uu___7::uu___8::uu___9::uu___10::e11::e2::e3::e4::e5::[]) + when + let uu___11 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___11 = "Pulse.Lib.ArrayPtr.blit" -> + let uu___11 = + let uu___12 = FStar_Extraction_Krml.translate_expr env e11 in + let uu___13 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___14 = FStar_Extraction_Krml.translate_expr env e3 in + let uu___15 = FStar_Extraction_Krml.translate_expr env e4 in + let uu___16 = FStar_Extraction_Krml.translate_expr env e5 in + (uu___12, uu___13, uu___14, uu___15, uu___16) in + FStar_Extraction_Krml.EBufBlit uu___11 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = From 5dd49ca21f67242d84aa1dc900b236ffb4223f9e Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Oct 2024 17:12:47 -0700 Subject: [PATCH 20/32] Remove mutb flag. --- lib/pulse/lib/Pulse.Lib.Slice.Util.fst | 133 ++++++++----------------- lib/pulse/lib/Pulse.Lib.Slice.fst | 24 +++-- lib/pulse/lib/Pulse.Lib.Slice.fsti | 45 ++------- 3 files changed, 64 insertions(+), 138 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst index cfdb4d45e..1b1050957 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst @@ -22,70 +22,25 @@ include Pulse.Lib.Trade module S = Pulse.Lib.Slice module SZ = FStar.SizeT -module T = FStar.Tactics - -noextract -let append_split_precond - (#t: Type) (mutb: bool) (p: perm) (v1: Ghost.erased (Seq.seq t)) (i: SZ.t) -: Tot prop -= SZ.v i == Seq.length v1 /\ (mutb == true ==> p == 1.0R) - -let append_split_post' - (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) - (s1: S.slice t) - (s2: S.slice t) -: Tot slprop -= - S.pts_to s1 #p v1 ** - S.pts_to s2 #p v2 ** - S.is_split s s1 s2 - -let append_split_post - (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) - (res: S.slice_pair t) -: Tot slprop -= let S.SlicePair s1 s2 = res in - append_split_post' s p v1 v2 i s1 s2 inline_for_extraction noextract -fn append_split (#t: Type) (mutb: bool) (s: S.slice t) (#p: perm) (#v1 #v2: Ghost.erased (Seq.seq t)) (i: SZ.t) - requires S.pts_to s #p (v1 `Seq.append` v2) ** pure (append_split_precond mutb p v1 i) - returns res: S.slice_pair t - ensures append_split_post s p v1 v2 i res +fn append_split (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) + (#v1: Ghost.erased (Seq.seq t) { SZ.v i == Seq.length v1 }) + (#v2: Ghost.erased (Seq.seq t)) + requires S.pts_to s #p (v1 `Seq.append` v2) + returns res: S.slice_pair t + ensures + (let S.SlicePair s1 s2 = res in + S.pts_to s1 #p v1 ** + S.pts_to s2 #p v2 ** + S.is_split s s1 s2) { - let vs = Ghost.hide (Seq.split (Seq.append v1 v2) (SZ.v i)); - assert (pure (fst vs `Seq.equal` v1)); - assert (pure (snd vs `Seq.equal` v2)); - let res = S.split mutb s i; - match res { - S.SlicePair s1 s2 -> { - unfold (S.split_post s p (Seq.append v1 v2) i res); - unfold (S.split_post' s p (Seq.append v1 v2) i s1 s2); - fold (append_split_post' s p v1 v2 i s1 s2); - fold (append_split_post s p v1 v2 i (S.SlicePair s1 s2)); - (S.SlicePair s1 s2) - } - } + assert pure (v1 `Seq.equal` Seq.slice (Seq.append v1 v2) 0 (SZ.v i)); + assert pure (v2 `Seq.equal` Seq.slice (Seq.append v1 v2) (SZ.v i) (Seq.length v1 + Seq.length v2)); + S.split s i } -let append_split_trade_post' - (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) - (s1: S.slice t) - (s2: S.slice t) -: Tot slprop -= - S.pts_to s1 #p v1 ** - S.pts_to s2 #p v2 ** - (trade (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2) (S.pts_to s #p (v1 `Seq.append` v2))) - -let append_split_trade_post - (#t: Type) (s: S.slice t) (p: perm) (v1 v2: Ghost.erased (Seq.seq t)) (i: SZ.t) - (res: S.slice_pair t) -: Tot slprop -= let S.SlicePair s1 s2 = res in - append_split_trade_post' s p v1 v2 i s1 s2 - ghost fn append_split_trade_aux (#t: Type) (input: S.slice t) (p: perm) (v1 v2: (Seq.seq t)) (i: SZ.t) (input1 input2: S.slice t) (_: unit) @@ -97,22 +52,20 @@ fn append_split_trade_aux inline_for_extraction noextract -fn append_split_trade (#t: Type) (mutb: bool) (input: S.slice t) (#p: perm) (#v1 #v2: Ghost.erased (Seq.seq t)) (i: SZ.t) - requires S.pts_to input #p (v1 `Seq.append` v2) ** pure (append_split_precond mutb p v1 i) - returns res: S.slice_pair t - ensures append_split_trade_post input p v1 v2 i res +fn append_split_trade (#t: Type) (input: S.slice t) (#p: perm) (i: SZ.t) + (#v1: Ghost.erased (Seq.seq t) { SZ.v i == Seq.length v1 }) + (#v2: Ghost.erased (Seq.seq t)) + requires S.pts_to input #p (v1 `Seq.append` v2) + returns res: S.slice_pair t + ensures + (let SlicePair s1 s2 = res in + S.pts_to s1 #p v1 ** S.pts_to s2 #p v2 ** + trade (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2) + (S.pts_to input #p (v1 `Seq.append` v2))) { - let res = append_split mutb input i; - match res { - S.SlicePair input1 input2 -> { - unfold (append_split_post input p v1 v2 i res); - unfold (append_split_post' input p v1 v2 i input1 input2); - intro_trade _ _ _ (append_split_trade_aux input p v1 v2 i input1 input2); - fold (append_split_trade_post' input p v1 v2 i input1 input2); - fold (append_split_trade_post input p v1 v2 i (S.SlicePair input1 input2)); - (S.SlicePair input1 input2) - } - } + let SlicePair s1 s2 = append_split input i; + intro_trade _ _ _ (append_split_trade_aux input p v1 v2 i s1 s2); + SlicePair s1 s2 } let split_trade_post' @@ -142,26 +95,26 @@ fn split_trade_aux (s1 s2: S.slice t) (v1 v2: Seq.seq t) (hyp: squash (v == Seq.append v1 v2)) (_: unit) requires (S.is_split s s1 s2 ** (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2)) ensures (S.pts_to s #p v) - { - S.join s1 s2 s - } +{ + S.join s1 s2 s +} inline_for_extraction noextract -fn split_trade (#t: Type) (mutb: bool) (s: S.slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) - requires S.pts_to s #p v ** pure (S.split_precond mutb p v i) - returns res: S.slice_pair t - ensures split_trade_post s p v i res +fn split_trade (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) + requires S.pts_to s #p v + returns res: S.slice_pair t + ensures + (let SlicePair s1 s2 = res in + let v1 = Seq.slice v 0 (SZ.v i) in + let v2 = Seq.slice v (SZ.v i) (Seq.length v) in + S.pts_to s1 #p v1 ** S.pts_to s2 #p v2 ** + trade (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2) + (S.pts_to s #p (v1 `Seq.append` v2))) { Seq.lemma_split v (SZ.v i); - let res = S.split mutb s i; - match res { S.SlicePair s1 s2 -> { - unfold (S.split_post s p v i res); - unfold (S.split_post' s p v i s1 s2); - with v1 v2 . assert (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2); - intro_trade _ _ _ (split_trade_aux s p v i s1 s2 v1 v2 ()); - fold (split_trade_post' s p v i s1 s2); - fold (split_trade_post s p v i (S.SlicePair s1 s2)); - (S.SlicePair s1 s2) - }} + let SlicePair s1 s2 = S.split s i; + with v1 v2. assert S.pts_to s1 #p v1 ** S.pts_to s2 #p v2; + intro_trade _ _ _ (split_trade_aux s p v i s1 s2 v1 v2 ()); + S.SlicePair s1 s2 } diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index c658a5ffd..298c16fcd 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -45,8 +45,8 @@ fn pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) let is_from_array a s = AP.is_from_array s.elt (SZ.v s.len) a -fn from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) - (alen: SZ.t { SZ.v alen == A.length a /\ (mutb == true ==> p == 1.0R) }) +fn from_array (#t: Type) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) + (alen: SZ.t { SZ.v alen == A.length a }) requires A.pts_to a #p v returns s: (slice t) ensures @@ -150,28 +150,30 @@ let is_split #t s s1 s2 = let is_split_is_slprop2 s s1 s2 = () -fn split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) - requires pts_to s #p v ** pure (split_precond mutb p v i) - returns res : slice_pair t - ensures (split_post s p v i res) +fn split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t) + (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) + requires pts_to s #p v + returns res : slice_pair t + ensures + (let SlicePair s1 s2 = res in + pts_to s1 #p (Seq.slice v 0 (SZ.v i)) ** + pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)) ** + is_split s s1 s2) { unfold (pts_to s #p v); Seq.lemma_split v (SZ.v i); let elt' = AP.split s.elt #p #v i; - with _v1 _v2. assert AP.pts_to s.elt #p _v1 ** AP.pts_to elt' #p _v2; let s1 = { elt = s.elt; len = i; }; - fold (pts_to s1 #p _v1); + fold pts_to s1 #p (Seq.slice v 0 (SZ.v i)); let s2 = { elt = elt'; len = s.len `SZ.sub` i; }; - fold (pts_to s2 #p _v2); + fold pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)); fold (is_split s s1 s2); - fold (split_post' s p v i s1 s2); - fold (split_post s p v i (s1 `SlicePair` s2)); (s1 `SlicePair` s2) } diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index c9cc6ecf2..14b92159c 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -36,15 +36,9 @@ val pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) : stt_ghost un val is_from_array (#t: Type) (a: array t) (s: slice t) : slprop -val from_array (#t: Type) (mutb: bool) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { - SZ.v alen == A.length a /\ - (mutb == true ==> p == 1.0R) -}) : stt (slice t) +val from_array (#t: Type) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { SZ.v alen == A.length a }) : stt (slice t) (A.pts_to a #p v) - (fun s -> - pts_to s #p v ** - is_from_array a s - ) + (fun s -> pts_to s #p v ** is_from_array a s) val to_array (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: array t) : stt_ghost unit emp_inames (pts_to s #p v ** is_from_array a s) @@ -105,35 +99,12 @@ val is_split_is_slprop2 (#t: Type) (s: slice t) (left: slice t) (right: slice t) noeq type slice_pair (t: Type) = | SlicePair: (fst: slice t) -> (snd: slice t) -> slice_pair t -let split_precond - (#t: Type) (mutb: bool) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) -: Tot prop -= SZ.v i <= Seq.length v /\ (mutb == true ==> p == 1.0R) - -let split_post' - (#t: Type) (s: slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) - (s1: slice t) - (s2: slice t) -: Tot slprop -= exists* v1 v2 . - pts_to s1 #p v1 ** - pts_to s2 #p v2 ** - is_split s s1 s2 ** - pure ( - SZ.v i <= Seq.length v /\ - (v1, v2) == Seq.split v (SZ.v i) - ) - -let split_post - (#t: Type) (s: slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) - (res: slice_pair t) -: Tot slprop -= let SlicePair s1 s2 = res in - split_post' s p v i s1 s2 - -val split (#t: Type) (mutb: bool) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t) : stt (slice_pair t) - (requires pts_to s #p v ** pure (split_precond mutb p v i)) - (ensures fun res -> split_post s p v i res) +val split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) : stt (slice_pair t) + (requires pts_to s #p v) + (ensures fun (SlicePair s1 s2) -> + pts_to s1 #p (Seq.slice v 0 (SZ.v i)) ** + pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)) ** + is_split s s1 s2) val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (s: slice t) : stt_ghost unit emp_inames (pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s s1 s2) From 81c5508f94d45540e6ee8d61b25d886280242b95 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Oct 2024 17:31:06 -0700 Subject: [PATCH 21/32] Fix extraction. --- src/extraction/ExtractPulse.fst | 4 ++-- src/ocaml/plugin/generated/ExtractPulse.ml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst index 4c45b3656..97bdfa483 100644 --- a/src/extraction/ExtractPulse.fst +++ b/src/extraction/ExtractPulse.fst @@ -120,7 +120,7 @@ let pulse_translate_expr : translate_expr_t = fun env e -> EBufFree (cb x) (* Pulse array pointers (ArrayPtr, as an underlying C extraction for slices *) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e; i; _p; _fp; _w ]) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e; i; _p; _w ]) when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Access" -> EBufRead (translate_expr env e, translate_expr env i) @@ -128,7 +128,7 @@ let pulse_translate_expr : translate_expr_t = fun env e -> when string_of_mlpath p = "Pulse.Lib.ArrayPtr.from_array" -> translate_expr env x - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ a; _p; _fp; _w; i ]) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ a; _p; _w; i ]) when string_of_mlpath p = "Pulse.Lib.ArrayPtr.split" -> EBufSub (translate_expr env a, translate_expr env i) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index 20062bbcd..da39b2429 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -417,7 +417,7 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = uu___3); FStar_Extraction_ML_Syntax.mlty = uu___4; FStar_Extraction_ML_Syntax.loc = uu___5;_}, - e2::i::_p::_fp::_w::[]) + e2::i::_p::_w::[]) when let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___6 = "Pulse.Lib.ArrayPtr.op_Array_Access" -> @@ -455,7 +455,7 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = uu___3); FStar_Extraction_ML_Syntax.mlty = uu___4; FStar_Extraction_ML_Syntax.loc = uu___5;_}, - a::_p::_fp::_w::i::[]) + a::_p::_w::i::[]) when let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___6 = "Pulse.Lib.ArrayPtr.split" -> From e83cdf5a97550b2874959bd469038b6cb42013e3 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Oct 2024 17:31:18 -0700 Subject: [PATCH 22/32] Add C extraction test. --- share/pulse/examples/Example.Slice.fst | 32 ++++++++++++++++++++++++++ share/pulse/examples/Makefile | 27 ++++++++-------------- 2 files changed, 41 insertions(+), 18 deletions(-) create mode 100644 share/pulse/examples/Example.Slice.fst diff --git a/share/pulse/examples/Example.Slice.fst b/share/pulse/examples/Example.Slice.fst new file mode 100644 index 000000000..22d82e2c3 --- /dev/null +++ b/share/pulse/examples/Example.Slice.fst @@ -0,0 +1,32 @@ +(* + Copyright 2023 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module Example.Slice +#lang-pulse +open Pulse +open Pulse.Lib.Slice + +fn test () requires emp ensures emp { + let arr = Pulse.Lib.Array.alloc 42uy 10sz; + let slice = from_array arr 10sz; + let SlicePair s1 s2 = split slice 2sz; + share s2; + let x = s2.(2sz); + s1.(1sz) <- x; + gather s2; + join s1 s2 slice; + to_array slice; + Pulse.Lib.Array.free arr; +} \ No newline at end of file diff --git a/share/pulse/examples/Makefile b/share/pulse/examples/Makefile index 0f0e17787..b6b5dfa33 100755 --- a/share/pulse/examples/Makefile +++ b/share/pulse/examples/Makefile @@ -20,6 +20,9 @@ $(OUTPUT_DIRECTORY)/Example_Hashtable.c: $(addprefix $(OUTPUT_DIRECTORY)/,\ Pulse_Lib_Vec.krml \ Pulse_Lib_HashTable_Type.krml Pulse_Lib_HashTable_Spec.krml Pulse_Lib_HashTable.krml) +$(OUTPUT_DIRECTORY)/Example_Slice.c: $(addprefix $(OUTPUT_DIRECTORY)/,\ + Pulse_Lib_Slice.krml) + $(OUTPUT_DIRECTORY)/Example_Unreachable.c: $(addprefix $(OUTPUT_DIRECTORY)/,FStar_Pervasives.krml FStar_Pervasives_Native.krml) $(OUTPUT_DIRECTORY)/%.c: $(EXTRA_KRML_DEPS) $(OUTPUT_DIRECTORY)/%.krml @@ -31,6 +34,8 @@ extract: $(OUTPUT_DIRECTORY)/ExtractionTest.ml .PHONY: extract_unreachable extract_unreachable: $(OUTPUT_DIRECTORY)/Example_Unreachable.ml +EXTRACT_C_FILES = $(addprefix $(OUTPUT_DIRECTORY)/,ExtractionTest.c PulsePointStruct.c Bug166.c Example_Unreachable.c Example_Hashtable.c Example_Slice.c) + ifneq (,$(KRML_HOME)) test-dpe-c: dice +$(MAKE) -C dice test-c @@ -38,31 +43,17 @@ test-dpe-c: dice test-cbor: dice +$(MAKE) -C dice/cbor -extract_c: $(OUTPUT_DIRECTORY)/ExtractionTest.c - -extract_pulse_c: $(OUTPUT_DIRECTORY)/PulsePointStruct.c - -extract_c_bug166: $(OUTPUT_DIRECTORY)/Bug166.c - -extract_c_unreachable: $(OUTPUT_DIRECTORY)/Example_Unreachable.c - -extract_c_hashtable: $(OUTPUT_DIRECTORY)/Example_Hashtable.c - else test-dpe-c: test-cbor: -extract_c: - -extract_pulse_c: - -extract_c_bug166: - -extract_c_unreachable: +EXTRACT_C_FILES = endif +extract_c: $(EXTRACT_C_FILES) + test: test-cbor extract extract_pulse_c extract_c extract_c_bug166 test-dpe-c test-error-messages extract_c_unreachable extract_c_hashtable test-error-messages: @@ -70,6 +61,6 @@ test-error-messages: .PHONY: test-dpe-c test-error-messages -.PHONY: extract_pulse_c extract_c extract_c_bug166 extract_c_unreachable extract_c_hashtable +.PHONY: extract_pulse_c extract_c .PHONY: test test-cbor test-cbor-raw From a4e169cbc1ab4481f27f57844884abaa28d52d7f Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Oct 2024 18:05:11 -0700 Subject: [PATCH 23/32] Add pulse2rust support for slices --- pulse2rust/src/Pulse2Rust.Extract.fst | 16 ++++ .../src/ocaml/generated/Pulse2Rust_Extract.ml | 65 +++++++++++-- pulse2rust/tests/Makefile | 27 ++++-- pulse2rust/tests/src/.gitignore | 1 + pulse2rust/tests/src/example_slice.rs | 17 ++++ pulse2rust/tests/src/pulsetutorial_array.rs | 94 +++++++++++++++++++ share/pulse/examples/Example.Slice.fst | 10 +- 7 files changed, 210 insertions(+), 20 deletions(-) create mode 100644 pulse2rust/tests/src/.gitignore create mode 100644 pulse2rust/tests/src/example_slice.rs create mode 100644 pulse2rust/tests/src/pulsetutorial_array.rs diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst index 35abfe4f9..572d48f3d 100644 --- a/pulse2rust/src/Pulse2Rust.Extract.fst +++ b/pulse2rust/src/Pulse2Rust.Extract.fst @@ -183,6 +183,10 @@ let rec extract_mlty (g:env) (t:S.mlty) : typ = when S.string_of_mlpath p = "Pulse.Lib.Array.Core.array" -> let is_mut = true in mk_slice is_mut arg + | S.MLTY_Named ([arg], p) + when S.string_of_mlpath p = "Pulse.Lib.Slice.slice" -> + let is_mut = true in + mk_slice is_mut arg | S.MLTY_Named ([arg; _], p) when S.string_of_mlpath p = "Pulse.Lib.Array.Core.larray" -> let is_mut = true in @@ -402,6 +406,10 @@ let rec extract_mlpattern_to_pat (g:env) (p:S.mlpattern) : env & pat = let g, ps = fold_left_map extract_mlpattern_to_pat g ps in g, mk_pat_tuple ps + | S.MLP_CTor (p, ps) when snd p = "SlicePair" -> + let g, ps = fold_left_map extract_mlpattern_to_pat g ps in + g, + mk_pat_tuple ps | S.MLP_CTor (p, ps) -> let g, ps = fold_left_map extract_mlpattern_to_pat g ps in let path = @@ -610,6 +618,7 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::i::_) when S.string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Access" || S.string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_index" || + S.string_of_mlpath p = "Pulse.Lib.Slice.op_Array_Access" || S.string_of_mlpath p = "Pulse.Lib.Vec.op_Array_Access" || S.string_of_mlpath p = "Pulse.Lib.Vec.read_ref" -> @@ -618,6 +627,7 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e1::e2::e3::_) when S.string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Assignment" || S.string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_upd" || + S.string_of_mlpath p = "Pulse.Lib.Slice.op_Array_Assignment" || S.string_of_mlpath p = "Pulse.Lib.Vec.op_Array_Assignment" || S.string_of_mlpath p = "Pulse.Lib.Vec.write_ref" -> @@ -644,6 +654,12 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = (extract_mlexpr g e_r) (extract_mlexpr g e_x) + | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::_) + when S.string_of_mlpath p = "Pulse.Lib.Slice.from_array" -> + extract_mlexpr g e + | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::_::i::_) + when S.string_of_mlpath p = "Pulse.Lib.Slice.split" -> + mk_method_call (extract_mlexpr g e) "split_at_mut" [extract_mlexpr g i] // // vec_as_array e extracted to &mut e diff --git a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml index ebff33497..2a04c74cd 100644 --- a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml +++ b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml @@ -238,6 +238,10 @@ let rec (extract_mlty : let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___ = "Pulse.Lib.Array.Core.array" -> let is_mut = true in mk_slice is_mut arg + | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when + let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___ = "Pulse.Lib.Slice.slice" -> + let is_mut = true in mk_slice is_mut arg | FStar_Extraction_ML_Syntax.MLTY_Named (arg::uu___::[], p) when let uu___1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___1 = "Pulse.Lib.Array.Core.larray" -> @@ -577,6 +581,14 @@ let rec (extract_mlpattern_to_pat : | (g1, ps1) -> let uu___1 = Pulse2Rust_Rust_Syntax.mk_pat_tuple ps1 in (g1, uu___1)) + | FStar_Extraction_ML_Syntax.MLP_CTor (p1, ps) when + (FStar_Pervasives_Native.snd p1) = "SlicePair" -> + let uu___ = + FStar_Compiler_List.fold_left_map extract_mlpattern_to_pat g ps in + (match uu___ with + | (g1, ps1) -> + let uu___1 = Pulse2Rust_Rust_Syntax.mk_pat_tuple ps1 in + (g1, uu___1)) | FStar_Extraction_ML_Syntax.MLP_CTor (p1, ps) -> let uu___ = FStar_Compiler_List.fold_left_map extract_mlpattern_to_pat g ps in @@ -1091,10 +1103,13 @@ and (extract_mlexpr : FStar_Extraction_ML_Syntax.loc = uu___4;_}, e1::i::uu___5) when - (((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Array.Core.op_Array_Access") || + ((((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.Array.Core.op_Array_Access") || + (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.Array.Core.pts_to_range_index")) + || (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Array.Core.pts_to_range_index")) + uu___6 = "Pulse.Lib.Slice.op_Array_Access")) || (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___6 = "Pulse.Lib.Vec.op_Array_Access")) @@ -1119,10 +1134,13 @@ and (extract_mlexpr : FStar_Extraction_ML_Syntax.loc = uu___4;_}, e1::e2::e3::uu___5) when - (((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Array.Core.op_Array_Assignment") || + ((((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.Array.Core.op_Array_Assignment") || + (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.Array.Core.pts_to_range_upd")) + || (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Array.Core.pts_to_range_upd")) + uu___6 = "Pulse.Lib.Slice.op_Array_Assignment")) || (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___6 = "Pulse.Lib.Vec.op_Array_Assignment")) @@ -1183,6 +1201,41 @@ and (extract_mlexpr : let uu___6 = extract_mlexpr g e_r in let uu___7 = extract_mlexpr g e_x in Pulse2Rust_Rust_Syntax.mk_mem_replace uu___5 uu___6 uu___7 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2::[]); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e1::uu___5) + when + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.Slice.from_array" -> extract_mlexpr g e1 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2::[]); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e1::uu___5::i::uu___6) + when + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Slice.split" -> + let uu___7 = extract_mlexpr g e1 in + let uu___8 = let uu___9 = extract_mlexpr g i in [uu___9] in + Pulse2Rust_Rust_Syntax.mk_method_call uu___7 "split_at_mut" uu___8 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = diff --git a/pulse2rust/tests/Makefile b/pulse2rust/tests/Makefile index fd2b02dc1..8b6ad54db 100644 --- a/pulse2rust/tests/Makefile +++ b/pulse2rust/tests/Makefile @@ -1,7 +1,7 @@ PULSE_HOME ?= ../.. PULSE_EXAMPLES_ROOT ?= $(PULSE_HOME)/share/pulse/examples -SRC_DIRS := $(addprefix $(PULSE_EXAMPLES_ROOT)/,by-example dice/external dice/external/hacl dice/external/l0 dice/dpe dice/engine dice/l0) +SRC_DIRS := $(addprefix $(PULSE_EXAMPLES_ROOT)/,. by-example dice/external dice/external/hacl dice/external/l0 dice/dpe dice/engine dice/l0) ifneq (,$(wildcard $(PULSE_EXAMPLES_ROOT)/dice/_output/cache)) SRC_DIRS += $(PULSE_EXAMPLES_ROOT)/dice/_output/cache endif @@ -16,7 +16,8 @@ CACHE_DIRECTORY := $(OUTPUT_DIRECTORY)/cache FSTAR_OPTIONS += --warn_error -342 --cmi MAIN=../main.exe -RUST_SRC_DIR=./src/ +RUST_SRC_DIR=src +RUST_OUT_DIR=out DPE_OUTPUT_DIR=../dpe/src/generated all: test dpe @@ -60,17 +61,23 @@ FSTAR_DEP_OPTIONS=--extract '* -FStar.Tactics -FStar.Reflection -Pulse +Pulse.Cl # files. If so, then this %.ast rule will be generic and can move to # share/pulse/Makefile.include-base. -%.ast: +$(OUTPUT_DIRECTORY)/%.ast: $(FSTAR) --admit_smt_queries true --codegen Extension $(subst .ast,.fst, $(subst _,., $(notdir $@))) --extract_module $(basename $(subst .ast,.fst, $(subst _,., $(notdir $@)))) -pulsetutorial-array.rs: PulseTutorial_Array.ast - $(MAIN) -odir $(RUST_SRC_DIR) $(addprefix $(OUTPUT_DIRECTORY)/, $^) +$(RUST_SRC_DIR)/pulsetutorial_array.rs: $(OUTPUT_DIRECTORY)/PulseTutorial_Array.ast + $(MAIN) -odir $(RUST_SRC_DIR) $+ -pulsetutorial-loops.rs: PulseTutorial_Loops.ast - $(MAIN) -odir $(RUST_SRC_DIR) $(addprefix $(OUTPUT_DIRECTORY)/, $^) +$(RUST_SRC_DIR)/pulsetutorial_loops.rs: $(OUTPUT_DIRECTORY)/PulseTutorial_Loops.ast + $(MAIN) -odir $(RUST_SRC_DIR) $+ -pulsetutorial-algorithms.rs: PulseTutorial_Algorithms.ast - $(MAIN) -odir $(RUST_SRC_DIR) $(addprefix $(OUTPUT_DIRECTORY)/, $^) +$(RUST_SRC_DIR)/pulsetutorial_algorithms.rs: $(OUTPUT_DIRECTORY)/PulseTutorial_Algorithms.ast + $(main) -odir $(rust_src_dir) $+ + +$(RUST_SRC_DIR)/example_slice.rs: $(OUTPUT_DIRECTORY)/Example_Slice.ast + $(MAIN) -odir $(RUST_SRC_DIR) $+ + +%.rlib: %.rs + rustc --crate-type rlib -o $@ $+ DPE_FILES = EngineTypes.ast \ EngineCore.ast \ @@ -87,7 +94,7 @@ DPE_LIB = L0Core,Pulse.Lib.Array,FStar.SizeT,EverCrypt.HMAC,EverCrypt.Hash.Incre dpe.rs: $(DPE_FILES) $(MAIN) -odir $(DPE_OUTPUT_DIR)/ -lib $(DPE_LIB) $(addprefix $(OUTPUT_DIRECTORY)/, $^) -all-rs: pulsetutorial-loops.rs pulsetutorial-algorithms.rs +all-rs: $(addprefix $(RUST_SRC_DIR)/, pulsetutorial_loops.rlib pulsetutorial_algorithms.rs pulsetutorial_array.rs example_slice.rlib) test: all-rs cargo test diff --git a/pulse2rust/tests/src/.gitignore b/pulse2rust/tests/src/.gitignore new file mode 100644 index 000000000..e9e98e15f --- /dev/null +++ b/pulse2rust/tests/src/.gitignore @@ -0,0 +1 @@ +*.rlib diff --git a/pulse2rust/tests/src/example_slice.rs b/pulse2rust/tests/src/example_slice.rs new file mode 100644 index 000000000..55a35c8db --- /dev/null +++ b/pulse2rust/tests/src/example_slice.rs @@ -0,0 +1,17 @@ +//// +//// +//// This file is generated by the Pulse2Rust tool +//// +//// + +pub fn test(arr: &mut [u8]) -> () { + let slice = arr; + let _letpattern = slice.split_at_mut(2); + match _letpattern { + (mut s1, mut s2) => { + let x = s2[2]; + s1[1] = x; + } + } +} + diff --git a/pulse2rust/tests/src/pulsetutorial_array.rs b/pulse2rust/tests/src/pulsetutorial_array.rs new file mode 100644 index 000000000..abbc90465 --- /dev/null +++ b/pulse2rust/tests/src/pulsetutorial_array.rs @@ -0,0 +1,94 @@ +//// +//// +//// This file is generated by the Pulse2Rust tool +//// +//// + +pub fn read_i(arr: &mut [T], p: (), s: (), i: usize) -> T { + arr[i] +} +pub fn write_i(arr: &mut [T], s: (), x: T, i: usize) -> () { + arr[i] = x; +} +pub fn compare( + p1: (), + p2: (), + a1: &mut [T], + a2: &mut [T], + l: usize, + __s1: (), + __s2: (), +) -> bool { + let mut i = 0; + while { + let vi = i; + if vi < l { + let v1 = a1[vi]; + let v2 = a2[vi]; + v1 == v2 + } else { + false + } + } { + let vi = i; + i = vi + 1; + } + let vi = i; + let res = vi == l; + let i1 = res; + i1 +} +pub fn copy( + a1: &mut [T], + a2: &mut [T], + l: usize, + p2: (), + __s1: (), + __s2: (), +) -> () { + let mut i = 0; + while { + let vi = i; + vi < l + } { + let vi = i; + let v = a2[vi]; + a1[vi] = v; + i = vi + 1; + } +} +pub fn copy2( + a1: &mut [T], + a2: &mut [T], + l: usize, + p2: (), + __s1: (), + __s2: (), +) -> () { + let mut i = 0; + while { + let vi = i; + vi < l + } { + let vi = i; + let v = a2[vi]; + a1[vi] = v; + i = vi + 1; + } +} +pub fn compare_stack_arrays(uu___: ()) -> () { + let a1 = &mut [0; 2]; + let a2 = &mut [0; 2]; + let b = super::pulsetutorial_array::compare((), (), a1, a2, 2, (), ()); +} +pub fn heap_arrays(uu___: ()) -> std::vec::Vec { + let mut a1 = vec![0; 2]; + let mut a2 = vec![0; 2]; + drop(a1); + a2 +} +pub fn copy_app(mut v: std::vec::Vec) -> () { + let a = &mut [0; 2]; + super::pulsetutorial_array::copy2(&mut v, a, 2, (), (), ()) +} + diff --git a/share/pulse/examples/Example.Slice.fst b/share/pulse/examples/Example.Slice.fst index 22d82e2c3..536a99b63 100644 --- a/share/pulse/examples/Example.Slice.fst +++ b/share/pulse/examples/Example.Slice.fst @@ -17,10 +17,13 @@ module Example.Slice #lang-pulse open Pulse open Pulse.Lib.Slice +module A = Pulse.Lib.Array -fn test () requires emp ensures emp { - let arr = Pulse.Lib.Array.alloc 42uy 10sz; - let slice = from_array arr 10sz; +fn test (arr: A.array UInt8.t) + requires A.pts_to arr seq![0uy; 1uy; 2uy; 3uy; 4uy] + ensures exists* s. A.pts_to arr s ** pure (s `Seq.equal` seq![0uy; 4uy; 2uy; 3uy; 4uy]) { + A.pts_to_len arr; + let slice = from_array arr 5sz; let SlicePair s1 s2 = split slice 2sz; share s2; let x = s2.(2sz); @@ -28,5 +31,4 @@ fn test () requires emp ensures emp { gather s2; join s1 s2 slice; to_array slice; - Pulse.Lib.Array.free arr; } \ No newline at end of file From afa7c562718fa4b0154dda2a35bee91c9357b61b Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Oct 2024 20:22:05 -0700 Subject: [PATCH 24/32] Fix makefile. --- share/pulse/examples/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/share/pulse/examples/Makefile b/share/pulse/examples/Makefile index b6b5dfa33..0bfc8aabf 100755 --- a/share/pulse/examples/Makefile +++ b/share/pulse/examples/Makefile @@ -54,7 +54,7 @@ endif extract_c: $(EXTRACT_C_FILES) -test: test-cbor extract extract_pulse_c extract_c extract_c_bug166 test-dpe-c test-error-messages extract_c_unreachable extract_c_hashtable +test: test-cbor extract extract_pulse_c extract_c test-dpe-c test-error-messages test-error-messages: +$(MAKE) -C bug-reports/error-messages From 9d683b4e1f3c6225606e4cdb0609c568d7f5b698 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 8 Oct 2024 09:59:12 -0700 Subject: [PATCH 25/32] Fix makefile. --- pulse2rust/tests/Makefile | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/pulse2rust/tests/Makefile b/pulse2rust/tests/Makefile index 8b6ad54db..13ebfd797 100644 --- a/pulse2rust/tests/Makefile +++ b/pulse2rust/tests/Makefile @@ -20,6 +20,7 @@ RUST_SRC_DIR=src RUST_OUT_DIR=out DPE_OUTPUT_DIR=../dpe/src/generated +.PHONY: all all: test dpe include $(PULSE_HOME)/share/pulse/Makefile.include @@ -79,23 +80,28 @@ $(RUST_SRC_DIR)/example_slice.rs: $(OUTPUT_DIRECTORY)/Example_Slice.ast %.rlib: %.rs rustc --crate-type rlib -o $@ $+ -DPE_FILES = EngineTypes.ast \ - EngineCore.ast \ +DPE_FILES = $(addprefix $(OUTPUT_DIRECTORY)/, \ + EngineTypes.ast \ + EngineCore.ast \ HACL.ast \ L0Types.ast \ Pulse_Lib_HashTable_Type.ast \ Pulse_Lib_HashTable_Spec.ast \ Pulse_Lib_HashTable.ast \ DPETypes.ast \ - DPE.ast + DPE.ast \ +) DPE_LIB = L0Core,Pulse.Lib.Array,FStar.SizeT,EverCrypt.HMAC,EverCrypt.Hash.Incremental,EverCrypt.Ed25519,EverCrypt.AutoConfig2,Spec.Hash.Definitions +.PHONY: dpe.rs dpe.rs: $(DPE_FILES) - $(MAIN) -odir $(DPE_OUTPUT_DIR)/ -lib $(DPE_LIB) $(addprefix $(OUTPUT_DIRECTORY)/, $^) + $(MAIN) -odir $(DPE_OUTPUT_DIR)/ -lib $(DPE_LIB) $^ +.PHONY: all-rs all-rs: $(addprefix $(RUST_SRC_DIR)/, pulsetutorial_loops.rlib pulsetutorial_algorithms.rs pulsetutorial_array.rs example_slice.rlib) +.PHONY: test test: all-rs cargo test @@ -103,6 +109,7 @@ test: all-rs external: ../dpe/gen-rust-bindings.sh +.PHONY: dpe dpe: dpe.rs external cd ../dpe && cargo build && cd - $(MAKE) -C ../dpe -f c.Makefile From 8d84d33295412eef3673ffdc47ea7e396310d786 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 8 Oct 2024 11:41:43 -0700 Subject: [PATCH 26/32] Test and fix copy extraction. --- pulse2rust/src/Pulse2Rust.Extract.fst | 3 +++ .../src/ocaml/generated/Pulse2Rust_Extract.ml | 20 +++++++++++++++++ pulse2rust/tests/Makefile | 2 +- pulse2rust/tests/src/example_slice.rs | 4 ++++ share/pulse/examples/Example.Slice.fst | 11 +++++++--- src/extraction/ExtractPulse.fst | 7 +++--- src/ocaml/plugin/generated/ExtractPulse.ml | 22 +++++++++---------- 7 files changed, 50 insertions(+), 19 deletions(-) diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst index 572d48f3d..f8cf62541 100644 --- a/pulse2rust/src/Pulse2Rust.Extract.fst +++ b/pulse2rust/src/Pulse2Rust.Extract.fst @@ -660,6 +660,9 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::_::i::_) when S.string_of_mlpath p = "Pulse.Lib.Slice.split" -> mk_method_call (extract_mlexpr g e) "split_at_mut" [extract_mlexpr g i] + | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, a::_::b::_) + when S.string_of_mlpath p = "Pulse.Lib.Slice.copy" -> + mk_method_call (extract_mlexpr g a) "copy_from_slice" [extract_mlexpr g b] // // vec_as_array e extracted to &mut e diff --git a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml index 2a04c74cd..e0af51ab7 100644 --- a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml +++ b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml @@ -1236,6 +1236,26 @@ and (extract_mlexpr : let uu___7 = extract_mlexpr g e1 in let uu___8 = let uu___9 = extract_mlexpr g i in [uu___9] in Pulse2Rust_Rust_Syntax.mk_method_call uu___7 "split_at_mut" uu___8 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2::[]); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + a::uu___5::b::uu___6) + when + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Slice.copy" -> + let uu___7 = extract_mlexpr g a in + let uu___8 = let uu___9 = extract_mlexpr g b in [uu___9] in + Pulse2Rust_Rust_Syntax.mk_method_call uu___7 "copy_from_slice" + uu___8 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = diff --git a/pulse2rust/tests/Makefile b/pulse2rust/tests/Makefile index 13ebfd797..74fd26498 100644 --- a/pulse2rust/tests/Makefile +++ b/pulse2rust/tests/Makefile @@ -72,7 +72,7 @@ $(RUST_SRC_DIR)/pulsetutorial_loops.rs: $(OUTPUT_DIRECTORY)/PulseTutorial_Loops. $(MAIN) -odir $(RUST_SRC_DIR) $+ $(RUST_SRC_DIR)/pulsetutorial_algorithms.rs: $(OUTPUT_DIRECTORY)/PulseTutorial_Algorithms.ast - $(main) -odir $(rust_src_dir) $+ + $(MAIN) -odir $(RUST_SRC_DIR) $+ $(RUST_SRC_DIR)/example_slice.rs: $(OUTPUT_DIRECTORY)/Example_Slice.ast $(MAIN) -odir $(RUST_SRC_DIR) $+ diff --git a/pulse2rust/tests/src/example_slice.rs b/pulse2rust/tests/src/example_slice.rs index 55a35c8db..0dc7a16bf 100644 --- a/pulse2rust/tests/src/example_slice.rs +++ b/pulse2rust/tests/src/example_slice.rs @@ -11,6 +11,10 @@ pub fn test(arr: &mut [u8]) -> () { (mut s1, mut s2) => { let x = s2[2]; s1[1] = x; + let _letpattern1 = s2.split_at_mut(2); + match _letpattern1 { + (mut s3, mut s4) => s3.copy_from_slice(s4), + } } } } diff --git a/share/pulse/examples/Example.Slice.fst b/share/pulse/examples/Example.Slice.fst index 536a99b63..b348a6494 100644 --- a/share/pulse/examples/Example.Slice.fst +++ b/share/pulse/examples/Example.Slice.fst @@ -20,15 +20,20 @@ open Pulse.Lib.Slice module A = Pulse.Lib.Array fn test (arr: A.array UInt8.t) - requires A.pts_to arr seq![0uy; 1uy; 2uy; 3uy; 4uy] - ensures exists* s. A.pts_to arr s ** pure (s `Seq.equal` seq![0uy; 4uy; 2uy; 3uy; 4uy]) { + requires A.pts_to arr seq![0uy; 1uy; 2uy; 3uy; 4uy; 5uy] + ensures exists* s. A.pts_to arr s ** pure (s `Seq.equal` seq![0uy; 4uy; 4uy; 5uy; 4uy; 5uy]) { A.pts_to_len arr; - let slice = from_array arr 5sz; + let slice = from_array arr 6sz; let SlicePair s1 s2 = split slice 2sz; share s2; let x = s2.(2sz); s1.(1sz) <- x; gather s2; + let SlicePair s3 s4 = split s2 2sz; + pts_to_len s3; + pts_to_len s4; + copy s3 s4; + join s3 s4 s2; join s1 s2 slice; to_array slice; } \ No newline at end of file diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst index 97bdfa483..8123075a0 100644 --- a/src/extraction/ExtractPulse.fst +++ b/src/extraction/ExtractPulse.fst @@ -136,10 +136,9 @@ let pulse_translate_expr : translate_expr_t = fun env e -> when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _; _; _; _; e1; e2; e3; e4; e5 ]) when ( - string_of_mlpath p = "Pulse.Lib.ArrayPtr.blit" - ) -> - EBufBlit (translate_expr env e1, translate_expr env e2, translate_expr env e3, translate_expr env e4, translate_expr env e5) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _; _; e1; e2; e3; e4; e5 ]) + when string_of_mlpath p = "Pulse.Lib.ArrayPtr.blit" -> + EBufBlit (translate_expr env e1, translate_expr env e2, translate_expr env e3, translate_expr env e4, translate_expr env e5) (* Pulse control, while etc *) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index da39b2429..87ad7a470 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -498,18 +498,18 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = uu___3); FStar_Extraction_ML_Syntax.mlty = uu___4; FStar_Extraction_ML_Syntax.loc = uu___5;_}, - uu___6::uu___7::uu___8::uu___9::uu___10::e11::e2::e3::e4::e5::[]) + uu___6::uu___7::uu___8::e11::e2::e3::e4::e5::[]) when - let uu___11 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___11 = "Pulse.Lib.ArrayPtr.blit" -> - let uu___11 = - let uu___12 = FStar_Extraction_Krml.translate_expr env e11 in - let uu___13 = FStar_Extraction_Krml.translate_expr env e2 in - let uu___14 = FStar_Extraction_Krml.translate_expr env e3 in - let uu___15 = FStar_Extraction_Krml.translate_expr env e4 in - let uu___16 = FStar_Extraction_Krml.translate_expr env e5 in - (uu___12, uu___13, uu___14, uu___15, uu___16) in - FStar_Extraction_Krml.EBufBlit uu___11 + let uu___9 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___9 = "Pulse.Lib.ArrayPtr.blit" -> + let uu___9 = + let uu___10 = FStar_Extraction_Krml.translate_expr env e11 in + let uu___11 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___12 = FStar_Extraction_Krml.translate_expr env e3 in + let uu___13 = FStar_Extraction_Krml.translate_expr env e4 in + let uu___14 = FStar_Extraction_Krml.translate_expr env e5 in + (uu___10, uu___11, uu___12, uu___13, uu___14) in + FStar_Extraction_Krml.EBufBlit uu___9 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = From c5fb18e0f8a87886a861a6fabe4e965acf57ec9e Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 8 Oct 2024 11:50:42 -0700 Subject: [PATCH 27/32] Clarify comment. --- lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index 52afd79b9..f52d4466b 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -20,7 +20,15 @@ open Pulse.Lib.Pervasives module SZ = FStar.SizeT module A = Pulse.Lib.Array -(* This module can be used only for Pulse programs extracted to C, not Rust. *) +(* +The `ArrayPtr.ptr t` type in this module cannot be extracted to Rust +because of the `split` operation, which assumes that the same pointer +can point to either the large subarray or its sub-subarray, depending on the permission. +Rust slices have the length baked in, so they cannot support this operation +without modifying the pointer. + +Use `Pulse.Lib.Slice.slice` instead when possible. +*) val ptr : Type0 -> Type0 From 8afd55d7e8e4b33bf65762c4f0d59e5bea752947 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 8 Oct 2024 12:18:59 -0700 Subject: [PATCH 28/32] Rename AP.blit to AP.memcpy for consistency. --- lib/pulse/lib/Pulse.Lib.ArrayPtr.fst | 75 ++++++++-------------- lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 40 +++--------- lib/pulse/lib/Pulse.Lib.Slice.fst | 5 +- src/extraction/ExtractPulse.fst | 4 +- src/ocaml/plugin/generated/ExtractPulse.ml | 4 +- 5 files changed, 44 insertions(+), 84 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst index 980ff06cb..000e738eb 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst @@ -180,55 +180,34 @@ fn join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq module R = Pulse.Lib.Reference -fn blit (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t)) - (src:ptr t) - (idx_src: SZ.t) - (dst:ptr t) - (idx_dst: SZ.t) - (len: SZ.t) -requires - (pts_to src #p0 s0 ** pts_to dst s1 ** pure ( - SZ.v idx_src + SZ.v len <= Seq.length s0 /\ - SZ.v idx_dst + SZ.v len <= Seq.length s1 - )) -ensures - (exists* s1' . pts_to src #p0 s0 ** pts_to dst s1' ** - pure (blit_post s0 s1 idx_src idx_dst len s1') - ) +fn memcpy + (#t:Type0) (#p0:perm) + (src:ptr t) (idx_src: SZ.t) + (dst:ptr t) (idx_dst: SZ.t) + (len: SZ.t) + (#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 }) + (#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 }) + requires pts_to src #p0 s0 ** pts_to dst s1 + ensures 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)) { - unfold (pts_to src #p0 s0); - A.pts_to_range_prop src.base; - fold (pts_to src #p0 s0); - let mut pi = 0sz; - while ( - let i = !pi; - SZ.lt i len - ) - invariant b . exists* i s1' . - R.pts_to pi i ** - pts_to src #p0 s0 ** - pts_to dst s1' ** - pure ( - SZ.v i <= SZ.v len /\ - b == (SZ.v i < SZ.v len) /\ - blit_post s0 s1 idx_src idx_dst i s1' - ) + let mut i = 0sz; + while (let vi = !i; SZ.lt vi len) + invariant b. exists* s1' vi. + R.pts_to i vi ** + pts_to src #p0 s0 ** + pts_to dst s1' ** + pure (b == SZ.lt vi len /\ SZ.lte vi len /\ + Seq.length s1' == Seq.length s1 /\ + forall (j:nat). j < Seq.length s1' ==> + Seq.index s1' j == (if j < SZ.v vi then Seq.index s0 j else Seq.index s1 j)) { - with s1'. assert pts_to dst s1'; - unfold pts_to dst s1'; - A.pts_to_range_prop dst.base; - fold pts_to dst s1'; - let i = !pi; - let x = op_Array_Access src (SZ.add idx_src i); - op_Array_Assignment dst (SZ.add idx_dst i) x; - pi := SZ.add i 1sz; - Seq.lemma_split (Seq.slice s1' (SZ.v idx_dst) (SZ.v idx_dst + SZ.v (SZ.add i 1sz))) (SZ.v i); - Seq.lemma_split (Seq.slice s0 (SZ.v idx_src) (SZ.v idx_src + SZ.v (SZ.add i 1sz))) (SZ.v i); - Seq.slice_slice s1' (SZ.v idx_dst + SZ.v i) (Seq.length s1') 1 (Seq.length s1' - (SZ.v idx_dst + SZ.v i)); - with s1''. assert pts_to dst s1''; - assert (pure ( - Seq.slice s1'' (SZ.v idx_dst + SZ.v (SZ.add i 1sz)) (Seq.length s1) `Seq.equal` - Seq.slice s1' (SZ.v idx_dst + SZ.v (SZ.add i 1sz)) (Seq.length s1') - )); + let vi = !i; + let x = src.(vi); + dst.(vi) <- x; + i := SZ.add vi 1sz; }; + with s1'. assert pts_to dst s1'; + assert pure (s1' `Seq.equal` + (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1))) } diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index f52d4466b..62c36ee8b 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -118,35 +118,13 @@ val join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Se (pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2)) (fun _ -> pts_to s1 #p (Seq.append v1 v2)) -let blit_post -(#t:_) (s0 s1:Ghost.erased (Seq.seq t)) - (idx_src: SZ.t) - (idx_dst: SZ.t) - (len: SZ.t) - (s1' : Seq.seq t) -: Tot prop -= - SZ.v idx_src + SZ.v len <= Seq.length s0 /\ - SZ.v idx_dst + SZ.v len <= Seq.length s1 /\ - Seq.length s1' == Seq.length s1 /\ - Seq.slice s1' (SZ.v idx_dst) (SZ.v idx_dst + SZ.v len) `Seq.equal` - Seq.slice s0 (SZ.v idx_src) (SZ.v idx_src + SZ.v len) /\ - Seq.slice s1' 0 (SZ.v idx_dst) `Seq.equal` - Seq.slice s1 0 (SZ.v idx_dst) /\ - Seq.slice s1' (SZ.v idx_dst + SZ.v len) (Seq.length s1) `Seq.equal` - Seq.slice s1 (SZ.v idx_dst + SZ.v len) (Seq.length s1) - -val blit (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t)) - (src:ptr t) - (idx_src: SZ.t) - (dst:ptr t) - (idx_dst: SZ.t) - (len: SZ.t) +val memcpy + (#t:Type0) (#p0:perm) + (src:ptr t) (idx_src: SZ.t) + (dst:ptr t) (idx_dst: SZ.t) + (len: SZ.t) + (#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 }) + (#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 }) : stt unit - (pts_to src #p0 s0 ** pts_to dst s1 ** pure ( - SZ.v idx_src + SZ.v len <= Seq.length s0 /\ - SZ.v idx_dst + SZ.v len <= Seq.length s1 - )) - (fun _ -> exists* s1' . pts_to src #p0 s0 ** pts_to dst s1' ** - pure (blit_post s0 s1 idx_src idx_dst len s1') - ) + (pts_to src #p0 s0 ** pts_to dst s1) + (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))) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index 298c16fcd..06842d179 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -199,7 +199,10 @@ ensures with v_dst . assert (pts_to dst v_dst); unfold (pts_to dst v_dst); unfold (pts_to src #p v); - AP.blit src.elt 0sz dst.elt 0sz src.len; + AP.memcpy src.elt 0sz dst.elt 0sz src.len; fold (pts_to src #p v); + assert pure (v `Seq.equal` + Seq.append (Seq.slice v 0 (SZ.v src.len)) + (Seq.slice v_dst (SZ.v src.len) (Seq.length v_dst))); fold (pts_to dst v) } diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst index 8123075a0..484ce3004 100644 --- a/src/extraction/ExtractPulse.fst +++ b/src/extraction/ExtractPulse.fst @@ -136,8 +136,8 @@ let pulse_translate_expr : translate_expr_t = fun env e -> when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Assignment" -> EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _; _; e1; e2; e3; e4; e5 ]) - when string_of_mlpath p = "Pulse.Lib.ArrayPtr.blit" -> + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; e1; e2; e3; e4; e5; _; _ ]) + when string_of_mlpath p = "Pulse.Lib.ArrayPtr.memcpy" -> EBufBlit (translate_expr env e1, translate_expr env e2, translate_expr env e3, translate_expr env e4, translate_expr env e5) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index 87ad7a470..678fe03e1 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -498,10 +498,10 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) = uu___3); FStar_Extraction_ML_Syntax.mlty = uu___4; FStar_Extraction_ML_Syntax.loc = uu___5;_}, - uu___6::uu___7::uu___8::e11::e2::e3::e4::e5::[]) + uu___6::e11::e2::e3::e4::e5::uu___7::uu___8::[]) when let uu___9 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___9 = "Pulse.Lib.ArrayPtr.blit" -> + uu___9 = "Pulse.Lib.ArrayPtr.memcpy" -> let uu___9 = let uu___10 = FStar_Extraction_Krml.translate_expr env e11 in let uu___11 = FStar_Extraction_Krml.translate_expr env e2 in From 84456796344da6ef9d21e10fbf800548d70d563c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 8 Oct 2024 13:09:47 -0700 Subject: [PATCH 29/32] Use pts_to typeclass. --- lib/pulse/lib/Pulse.Lib.ArrayPtr.fst | 57 +++++++++++++------- lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 2 +- lib/pulse/lib/Pulse.Lib.Slice.Util.fst | 38 ++++++------- lib/pulse/lib/Pulse.Lib.Slice.fst | 74 +++++++++++++++++--------- lib/pulse/lib/Pulse.Lib.Slice.fsti | 2 +- share/pulse/examples/Example.Slice.fst | 4 +- 6 files changed, 109 insertions(+), 68 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst index 000e738eb..11afa6347 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst @@ -26,8 +26,27 @@ type ptr t = { let base a = a.base let offset a = SZ.v a.offset -let pts_to s #p v = +instance has_pts_to_array_ptr t = { + pts_to = (fun s #p v -> + A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v) +} + +ghost fn unfold_pts_to #t (s: ptr t) #p v + requires pts_to s #p v + ensures A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v +{ + rewrite pts_to s #p v as A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v +} + +ghost fn fold_pts_to #t (s: ptr t) #p v + requires A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v + ensures pts_to s #p v +{ + rewrite + A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v + as pts_to s #p v +} let pts_to_is_slprop2 x p s = () @@ -48,7 +67,7 @@ fn from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t) A.pts_to_range_intro a p v; rewrite (A.pts_to_range a 0 (A.length a) #p v) as (A.pts_to_range res.base (SZ.v res.offset) (SZ.v res.offset + Seq.length v) #p v); - fold (pts_to res #p v); + fold_pts_to res #p v; res } @@ -58,7 +77,7 @@ fn to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#v: Seq.seq t) ensures A.pts_to a #p v { unfold is_from_array s (Seq.length v) a; - unfold pts_to s #p v; + unfold_pts_to s #p v; A.pts_to_range_prop s.base; rewrite (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v) as (A.pts_to_range a 0 (A.length a) #p v); @@ -80,10 +99,10 @@ fn op_Array_Access SZ.v i < Seq.length s /\ res == Seq.index s (SZ.v i)) { - unfold pts_to a #p s; + unfold_pts_to a #p s; A.pts_to_range_prop a.base; let res = A.pts_to_range_index a.base (SZ.add a.offset i); - fold pts_to a #p s; + fold_pts_to a #p s; res } @@ -101,10 +120,10 @@ fn op_Array_Assignment s' == Seq.upd s (SZ.v i) v ) { - unfold pts_to a s; + unfold_pts_to a s; A.pts_to_range_prop a.base; let res = A.pts_to_range_upd a.base (SZ.add a.offset i) v; - fold pts_to a (Seq.upd s (SZ.v i) v); + fold_pts_to a (Seq.upd s (SZ.v i) v); } ghost @@ -116,10 +135,10 @@ fn share requires pts_to arr #p s ensures pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s { - unfold pts_to arr #p s; + unfold_pts_to arr #p s; A.pts_to_range_share arr.base; - fold pts_to arr #(p /. 2.0R) s; - fold pts_to arr #(p /. 2.0R) s; + fold_pts_to arr #(p /. 2.0R) s; + fold_pts_to arr #(p /. 2.0R) s; } ghost @@ -131,10 +150,10 @@ fn gather requires pts_to arr #p0 s0 ** pts_to arr #p1 s1 ** pure (Seq.length s0 == Seq.length s1) ensures pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1) { - unfold pts_to arr #p0 s0; - unfold pts_to arr #p1 s1; + unfold_pts_to arr #p0 s0; + unfold_pts_to arr #p1 s1; A.pts_to_range_gather arr.base; - fold pts_to arr #(p0 +. p1) s0 + fold_pts_to arr #(p0 +. p1) s0 } fn split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t { SZ.v i <= Seq.length v }) @@ -145,7 +164,7 @@ fn split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ. pts_to s' #p (Seq.slice v (SZ.v i) (Seq.length v)) ** pure (adjacent s (SZ.v i) s') { - unfold pts_to s #p v; + unfold_pts_to s #p v; A.pts_to_range_prop s.base; let s' = { base = s.base; @@ -156,12 +175,12 @@ fn split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ. rewrite (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1) as (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v i) #p s1); - fold pts_to s #p s1; + fold_pts_to s #p s1; with s2. assert A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2; rewrite (A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2) as (A.pts_to_range s'.base (SZ.v s'.offset) (SZ.v s'.offset + Seq.length s2) #p s2); - fold pts_to s' #p s2; + fold_pts_to s' #p s2; s' } @@ -170,12 +189,12 @@ fn join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2) ensures pts_to s1 #p (Seq.append v1 v2) { - unfold pts_to s1 #p v1; - unfold pts_to s2 #p v2; + unfold_pts_to s1 #p v1; + unfold_pts_to s2 #p v2; rewrite (A.pts_to_range s2.base (SZ.v s2.offset) (SZ.v s2.offset + Seq.length v2) #p v2) 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); 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); - fold (pts_to s1 #p (Seq.append v1 v2)) + fold_pts_to s1 #p (Seq.append v1 v2) } module R = Pulse.Lib.Reference diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index 62c36ee8b..3e308be45 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -35,7 +35,7 @@ val ptr : Type0 -> Type0 val base #t (p: ptr t) : GTot (A.array t) val offset #t (p: ptr t) : GTot nat -val pts_to (#t: Type) (s: ptr t) (#[exact (`1.0R)] p: perm) (v: Seq.seq t) : slprop +instance val has_pts_to_array_ptr (t: Type) : has_pts_to (ptr t) (Seq.seq t) val pts_to_is_slprop2 (#a:Type) (x:ptr a) (p:perm) (s:Seq.seq a) : Lemma (is_slprop2 (pts_to x #p s)) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst index 1b1050957..40759ad46 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst @@ -28,12 +28,12 @@ noextract fn append_split (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) (#v1: Ghost.erased (Seq.seq t) { SZ.v i == Seq.length v1 }) (#v2: Ghost.erased (Seq.seq t)) - requires S.pts_to s #p (v1 `Seq.append` v2) + requires pts_to s #p (v1 `Seq.append` v2) returns res: S.slice_pair t ensures (let S.SlicePair s1 s2 = res in - S.pts_to s1 #p v1 ** - S.pts_to s2 #p v2 ** + pts_to s1 #p v1 ** + pts_to s2 #p v2 ** S.is_split s s1 s2) { assert pure (v1 `Seq.equal` Seq.slice (Seq.append v1 v2) 0 (SZ.v i)); @@ -44,8 +44,8 @@ fn append_split (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) ghost fn append_split_trade_aux (#t: Type) (input: S.slice t) (p: perm) (v1 v2: (Seq.seq t)) (i: SZ.t) (input1 input2: S.slice t) (_: unit) - requires S.is_split input input1 input2 ** (S.pts_to input1 #p v1 ** S.pts_to input2 #p v2) - ensures S.pts_to input #p (v1 `Seq.append` v2) + requires S.is_split input input1 input2 ** (pts_to input1 #p v1 ** pts_to input2 #p v2) + ensures pts_to input #p (v1 `Seq.append` v2) { S.join input1 input2 input } @@ -55,13 +55,13 @@ noextract fn append_split_trade (#t: Type) (input: S.slice t) (#p: perm) (i: SZ.t) (#v1: Ghost.erased (Seq.seq t) { SZ.v i == Seq.length v1 }) (#v2: Ghost.erased (Seq.seq t)) - requires S.pts_to input #p (v1 `Seq.append` v2) + requires pts_to input #p (v1 `Seq.append` v2) returns res: S.slice_pair t ensures (let SlicePair s1 s2 = res in - S.pts_to s1 #p v1 ** S.pts_to s2 #p v2 ** - trade (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2) - (S.pts_to input #p (v1 `Seq.append` v2))) + pts_to s1 #p v1 ** pts_to s2 #p v2 ** + trade (pts_to s1 #p v1 ** pts_to s2 #p v2) + (pts_to input #p (v1 `Seq.append` v2))) { let SlicePair s1 s2 = append_split input i; intro_trade _ _ _ (append_split_trade_aux input p v1 v2 i s1 s2); @@ -74,9 +74,9 @@ let split_trade_post' (s2: S.slice t) : Tot slprop = exists* v1 v2 . - S.pts_to s1 #p v1 ** - S.pts_to s2 #p v2 ** - (trade (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2) (S.pts_to s #p v)) ** + pts_to s1 #p v1 ** + pts_to s2 #p v2 ** + (trade (pts_to s1 #p v1 ** pts_to s2 #p v2) (pts_to s #p v)) ** pure ( SZ.v i <= Seq.length v /\ (v1, v2) == Seq.split v (SZ.v i) @@ -93,8 +93,8 @@ ghost fn split_trade_aux (#t: Type) (s: S.slice t) (p: perm) (v: Seq.seq t) (i: SZ.t) (s1 s2: S.slice t) (v1 v2: Seq.seq t) (hyp: squash (v == Seq.append v1 v2)) (_: unit) - requires (S.is_split s s1 s2 ** (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2)) - ensures (S.pts_to s #p v) + requires (S.is_split s s1 s2 ** (pts_to s1 #p v1 ** pts_to s2 #p v2)) + ensures (pts_to s #p v) { S.join s1 s2 s } @@ -102,19 +102,19 @@ fn split_trade_aux inline_for_extraction noextract fn split_trade (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) - requires S.pts_to s #p v + requires pts_to s #p v returns res: S.slice_pair t ensures (let SlicePair s1 s2 = res in let v1 = Seq.slice v 0 (SZ.v i) in let v2 = Seq.slice v (SZ.v i) (Seq.length v) in - S.pts_to s1 #p v1 ** S.pts_to s2 #p v2 ** - trade (S.pts_to s1 #p v1 ** S.pts_to s2 #p v2) - (S.pts_to s #p (v1 `Seq.append` v2))) + pts_to s1 #p v1 ** pts_to s2 #p v2 ** + trade (pts_to s1 #p v1 ** pts_to s2 #p v2) + (pts_to s #p (v1 `Seq.append` v2))) { Seq.lemma_split v (SZ.v i); let SlicePair s1 s2 = S.split s i; - with v1 v2. assert S.pts_to s1 #p v1 ** S.pts_to s2 #p v2; + with v1 v2. assert pts_to s1 #p v1 ** pts_to s2 #p v2; intro_trade _ _ _ (split_trade_aux s p v i s1 s2 v1 v2 ()); S.SlicePair s1 s2 } diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index 06842d179..576cf0f58 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -27,9 +27,31 @@ type slice t = { let len s = s.len -let pts_to #t s #p v = - AP.pts_to s.elt #p v ** +let has_pts_to_slice t = { + pts_to = (fun s #p v -> + pts_to s.elt #p v ** + pure (Seq.length v == SZ.v s.len)) +} + +ghost fn unfold_pts_to #t (s: slice t) #p v + requires pts_to s #p v + ensures pts_to s.elt #p v ** + pure (Seq.length v == SZ.v s.len) +{ + rewrite pts_to s #p v as + pts_to s.elt #p v ** pure (Seq.length v == SZ.v s.len) +} + +ghost fn fold_pts_to #t (s: slice t) #p v + requires pts_to s.elt #p v ** + pure (Seq.length v == SZ.v s.len) + ensures pts_to s #p v +{ + rewrite pts_to s.elt #p v ** + pure (Seq.length v == SZ.v s.len) + as pts_to s #p v; +} let pts_to_is_slprop2 x p v = () @@ -38,8 +60,8 @@ fn pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) requires pts_to s #p v ensures pts_to s #p v ** pure (Seq.length v == SZ.v (len s)) { - unfold (pts_to s #p v); - fold (pts_to s #p v) + unfold_pts_to s #p v; + fold_pts_to s #p v } let is_from_array a s = @@ -59,7 +81,7 @@ fn from_array (#t: Type) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) elt = ptr; len = alen; }; - fold pts_to res #p v; + fold_pts_to res #p v; fold is_from_array a res; res } @@ -70,7 +92,7 @@ fn to_array requires (pts_to s #p v ** is_from_array a s) ensures (A.pts_to a #p v) { - unfold (pts_to s #p v); + unfold_pts_to s #p v; unfold is_from_array a s; AP.to_array s.elt a } @@ -88,9 +110,9 @@ ensures pts_to a #p s ** pure (res == Seq.index s (SZ.v i)) { - unfold (pts_to a #p s); + unfold_pts_to a #p s; let res = AP.op_Array_Access a.elt i; - fold (pts_to a #p s); + fold_pts_to a #p s; res } @@ -105,9 +127,9 @@ fn op_Array_Assignment ensures pts_to a (Seq.upd s (SZ.v i) v) { - unfold (pts_to a s); + unfold_pts_to a s; AP.op_Array_Assignment a.elt i v; - fold (pts_to a (Seq.upd s (SZ.v i) v)) + fold_pts_to a (Seq.upd s (SZ.v i) v) } ghost @@ -120,10 +142,10 @@ requires pts_to arr #p s ensures pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s { - unfold (pts_to arr #p s); + unfold_pts_to arr #p s; AP.share arr.elt; - fold (pts_to arr #(p /. 2.0R) s); - fold (pts_to arr #(p /. 2.0R) s) + fold_pts_to arr #(p /. 2.0R) s; + fold_pts_to arr #(p /. 2.0R) s } ghost @@ -135,10 +157,10 @@ fn gather requires pts_to arr #p0 s0 ** pts_to arr #p1 s1 ensures pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1) { - unfold (pts_to arr #p0 s0); - unfold (pts_to arr #p1 s1); + unfold_pts_to arr #p0 s0; + unfold_pts_to arr #p1 s1; AP.gather arr.elt; - fold (pts_to arr #(p0 +. p1) s0) + fold_pts_to arr #(p0 +. p1) s0 } let is_split #t s s1 s2 = @@ -160,19 +182,19 @@ fn split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t) pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)) ** is_split s s1 s2) { - unfold (pts_to s #p v); + unfold_pts_to s #p v; Seq.lemma_split v (SZ.v i); let elt' = AP.split s.elt #p #v i; let s1 = { elt = s.elt; len = i; }; - fold pts_to s1 #p (Seq.slice v 0 (SZ.v i)); + fold_pts_to s1 #p (Seq.slice v 0 (SZ.v i)); let s2 = { elt = elt'; len = s.len `SZ.sub` i; }; - fold pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)); + fold_pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)); fold (is_split s s1 s2); (s1 `SlicePair` s2) } @@ -183,10 +205,10 @@ fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: ensures pts_to s #p (Seq.append v1 v2) { unfold (is_split s s1 s2); - unfold (pts_to s1 #p v1); - unfold (pts_to s2 #p v2); + unfold_pts_to s1 #p v1; + unfold_pts_to s2 #p v2; AP.join s1.elt s2.elt; - fold (pts_to s #p (Seq.append v1 v2)) + fold_pts_to s #p (Seq.append v1 v2) } fn copy @@ -197,12 +219,12 @@ ensures (pts_to dst v ** pts_to src #p v) { with v_dst . assert (pts_to dst v_dst); - unfold (pts_to dst v_dst); - unfold (pts_to src #p v); + unfold_pts_to dst v_dst; + unfold_pts_to src #p v; AP.memcpy src.elt 0sz dst.elt 0sz src.len; - fold (pts_to src #p v); + fold_pts_to src #p v; assert pure (v `Seq.equal` Seq.append (Seq.slice v 0 (SZ.v src.len)) (Seq.slice v_dst (SZ.v src.len) (Seq.length v_dst))); - fold (pts_to dst v) + fold_pts_to dst v } diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index 14b92159c..f219301e7 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -24,7 +24,7 @@ val slice : Type0 -> Type0 val len (#t: Type) : slice t -> SZ.t -val pts_to (#t: Type) (s: slice t) (#[exact (`1.0R)] p: perm) (v: Seq.seq t) : slprop +instance val has_pts_to_slice (t: Type u#0) : has_pts_to (slice t) (Seq.seq t) val pts_to_is_slprop2 (#a:Type) (x:slice a) (p:perm) (s:Seq.seq a) : Lemma (is_slprop2 (pts_to x #p s)) diff --git a/share/pulse/examples/Example.Slice.fst b/share/pulse/examples/Example.Slice.fst index b348a6494..122b3c566 100644 --- a/share/pulse/examples/Example.Slice.fst +++ b/share/pulse/examples/Example.Slice.fst @@ -20,8 +20,8 @@ open Pulse.Lib.Slice module A = Pulse.Lib.Array fn test (arr: A.array UInt8.t) - requires A.pts_to arr seq![0uy; 1uy; 2uy; 3uy; 4uy; 5uy] - ensures exists* s. A.pts_to arr s ** pure (s `Seq.equal` seq![0uy; 4uy; 4uy; 5uy; 4uy; 5uy]) { + requires pts_to arr seq![0uy; 1uy; 2uy; 3uy; 4uy; 5uy] + ensures exists* s. pts_to arr s ** pure (s `Seq.equal` seq![0uy; 4uy; 4uy; 5uy; 4uy; 5uy]) { A.pts_to_len arr; let slice = from_array arr 6sz; let SlicePair s1 s2 = split slice 2sz; From 56cfbb999e9cd6827deb20ff92cfa63a7b4d2980 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 8 Oct 2024 13:18:12 -0700 Subject: [PATCH 30/32] Remove unused code. --- lib/pulse/lib/Pulse.Lib.Slice.Util.fst | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst index 40759ad46..9155f4a0b 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst @@ -68,27 +68,6 @@ fn append_split_trade (#t: Type) (input: S.slice t) (#p: perm) (i: SZ.t) SlicePair s1 s2 } -let split_trade_post' - (#t: Type) (s: S.slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) - (s1: S.slice t) - (s2: S.slice t) -: Tot slprop -= exists* v1 v2 . - pts_to s1 #p v1 ** - pts_to s2 #p v2 ** - (trade (pts_to s1 #p v1 ** pts_to s2 #p v2) (pts_to s #p v)) ** - pure ( - SZ.v i <= Seq.length v /\ - (v1, v2) == Seq.split v (SZ.v i) - ) - -let split_trade_post - (#t: Type) (s: S.slice t) (p: perm) (v: Ghost.erased (Seq.seq t)) (i: SZ.t) - (res: S.slice_pair t) -: Tot slprop -= let (S.SlicePair s1 s2) = res in - split_trade_post' s p v i s1 s2 - ghost fn split_trade_aux (#t: Type) (s: S.slice t) (p: perm) (v: Seq.seq t) (i: SZ.t) From 24f4886c5f19a5d8e1e7406c55df21b88d422891 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 8 Oct 2024 13:23:00 -0700 Subject: [PATCH 31/32] pulse2rust: Slice.len --- pulse2rust/src/Pulse2Rust.Extract.fst | 3 +++ .../src/ocaml/generated/Pulse2Rust_Extract.ml | 18 ++++++++++++++++++ pulse2rust/tests/src/example_slice.rs | 2 +- share/pulse/examples/Example.Slice.fst | 3 ++- 4 files changed, 24 insertions(+), 2 deletions(-) diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst index f8cf62541..2ca88e832 100644 --- a/pulse2rust/src/Pulse2Rust.Extract.fst +++ b/pulse2rust/src/Pulse2Rust.Extract.fst @@ -663,6 +663,9 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, a::_::b::_) when S.string_of_mlpath p = "Pulse.Lib.Slice.copy" -> mk_method_call (extract_mlexpr g a) "copy_from_slice" [extract_mlexpr g b] + | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [a]) + when S.string_of_mlpath p = "Pulse.Lib.Slice.len" -> + mk_method_call (extract_mlexpr g a) "len" [] // // vec_as_array e extracted to &mut e diff --git a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml index e0af51ab7..3a8a53f53 100644 --- a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml +++ b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml @@ -1256,6 +1256,24 @@ and (extract_mlexpr : let uu___8 = let uu___9 = extract_mlexpr g b in [uu___9] in Pulse2Rust_Rust_Syntax.mk_method_call uu___7 "copy_from_slice" uu___8 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2::[]); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + a::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Pulse.Lib.Slice.len" -> + let uu___5 = extract_mlexpr g a in + Pulse2Rust_Rust_Syntax.mk_method_call uu___5 "len" [] | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = diff --git a/pulse2rust/tests/src/example_slice.rs b/pulse2rust/tests/src/example_slice.rs index 0dc7a16bf..17fde9346 100644 --- a/pulse2rust/tests/src/example_slice.rs +++ b/pulse2rust/tests/src/example_slice.rs @@ -9,7 +9,7 @@ pub fn test(arr: &mut [u8]) -> () { let _letpattern = slice.split_at_mut(2); match _letpattern { (mut s1, mut s2) => { - let x = s2[2]; + let x = s2[s1.len()]; s1[1] = x; let _letpattern1 = s2.split_at_mut(2); match _letpattern1 { diff --git a/share/pulse/examples/Example.Slice.fst b/share/pulse/examples/Example.Slice.fst index 122b3c566..ded284bfe 100644 --- a/share/pulse/examples/Example.Slice.fst +++ b/share/pulse/examples/Example.Slice.fst @@ -25,8 +25,9 @@ fn test (arr: A.array UInt8.t) A.pts_to_len arr; let slice = from_array arr 6sz; let SlicePair s1 s2 = split slice 2sz; + pts_to_len s1; share s2; - let x = s2.(2sz); + let x = s2.(len s1); s1.(1sz) <- x; gather s2; let SlicePair s3 s4 = split s2 2sz; From 40664bcb8dfb39089eafe3776239f224fcfce329 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 8 Oct 2024 13:25:53 -0700 Subject: [PATCH 32/32] Make argument order more robust. --- lib/pulse/lib/Pulse.Lib.Slice.fst | 4 ++-- lib/pulse/lib/Pulse.Lib.Slice.fsti | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index 576cf0f58..85486df77 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -67,8 +67,8 @@ fn pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) let is_from_array a s = AP.is_from_array s.elt (SZ.v s.len) a -fn from_array (#t: Type) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) - (alen: SZ.t { SZ.v alen == A.length a }) +fn from_array (#t: Type) (a: array t) (#p: perm) (alen: SZ.t) + (#v: Ghost.erased (Seq.seq t) { SZ.v alen == A.length a }) requires A.pts_to a #p v returns s: (slice t) ensures diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index f219301e7..b7fc4794b 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -36,7 +36,7 @@ val pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) : stt_ghost un val is_from_array (#t: Type) (a: array t) (s: slice t) : slprop -val from_array (#t: Type) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { SZ.v alen == A.length a }) : stt (slice t) +val from_array (#t: Type) (a: array t) (#p: perm) (alen: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v alen == A.length a }) : stt (slice t) (A.pts_to a #p v) (fun s -> pts_to s #p v ** is_from_array a s)