Skip to content

Some updates to Pulse.Lib.Array #523

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mtzguido merged 2 commits into from
Dec 8, 2025
Merged

Some updates to Pulse.Lib.Array #523

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bb7c14f
Pulse.Lib.Array: introduce mask_share_gen
tahina-pro Nov 14, 2025
a4fc743
Pulse.Lib.Array.memcpy does not require eqtype
tahina-pro Nov 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 15 additions & 6 deletions lib/pulse/lib/Pulse.Lib.Array.Core.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -379,20 +379,29 @@ ghost fn pcm_gather u#a (#t: Type u#a) #l
}

ghost
fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
requires pts_to_mask arr #p s mask
ensures pts_to_mask arr #(p /. 2.0R) s mask
ensures pts_to_mask arr #(p /. 2.0R) s mask
fn mask_share_gen u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p (p1: perm) (p2: perm) #mask
requires pts_to_mask arr #p s mask ** pure ((p <: real) == p1 +. p2)
ensures pts_to_mask arr #p1 s mask
ensures pts_to_mask arr #p2 s mask
{
loc_get ();
pts_to_mask_props arr;
pcm_share
arr p s mask
arr (p /. 2.0R) s mask
arr (p /. 2.0R) s mask;
arr p1 s mask
arr p2 s mask;
drop_ (loc _);
}

ghost
fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
requires pts_to_mask arr #p s mask
ensures pts_to_mask arr #(p /. 2.0R) s mask
ensures pts_to_mask arr #(p /. 2.0R) s mask
{
mask_share_gen arr #s #p (p /. 2.0R) (p /. 2.0R) #mask
}

[@@allow_ambiguous]
ghost fn mask_gather u#a (#t: Type u#a) (arr: array t) #p1 #p2 #s1 #s2 #mask1 #mask2
requires pts_to_mask arr #p1 s1 mask1
Expand Down
6 changes: 6 additions & 0 deletions lib/pulse/lib/Pulse.Lib.Array.Core.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,12 @@ fn mask_free u#a (#elt: Type u#a) (a: array elt) (#s: Ghost.erased (Seq.seq elt)
requires pure (forall i. mask i)
requires pure (is_full_array a)

ghost
fn mask_share_gen u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p (p1: perm) (p2: perm) #mask
requires pts_to_mask arr #p s mask ** pure ((p <: real) == p1 +. p2)
ensures pts_to_mask arr #p1 s mask
ensures pts_to_mask arr #p2 s mask

ghost
fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
requires pts_to_mask arr #p s mask
Expand Down
4 changes: 2 additions & 2 deletions lib/pulse/lib/Pulse.Lib.Array.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ fn compare (#t:eqtype) (l:US.t) (a1 a2:larray t (US.v l)) (#p1 #p2:perm)
(!i = l)
}

fn memcpy_l (#t:eqtype) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
fn memcpy_l (#t:Type0) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
(#p:perm) (#src0 #dst0:Ghost.erased (Seq.seq t))
requires pts_to src #p src0 **
pts_to dst dst0
Expand Down Expand Up @@ -89,7 +89,7 @@ fn memcpy_l (#t:eqtype) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))


fn memcpy
(#t:eqtype)
(#t:Type0)
(l:SZ.t)
(src dst:larray t (SZ.v l))
(#p:perm)
Expand Down
4 changes: 2 additions & 2 deletions lib/pulse/lib/Pulse.Lib.Array.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ fn compare
pure (res <==> Seq.equal s1 s2)

fn memcpy_l
(#t:eqtype)
(#t:Type0)
(l:SZ.t)
(src dst:(a:array t { SZ.v l <= length a }))
(#p:perm)
Expand All @@ -54,7 +54,7 @@ fn memcpy_l
(Seq.slice dst0 (SZ.v l) (length dst)))

fn memcpy
(#t:eqtype)
(#t:Type0)
(l:SZ.t)
(src dst:larray t (SZ.v l))
(#p:perm)
Expand Down
Loading