Skip to content

Use new pre/postcondition syntax #536

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
gebner merged 5 commits into from
Feb 3, 2026
Merged

Use new pre/postcondition syntax #536

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9faa4af
Update requires syntax: use multiple requires clauses instead of **
gebner Jan 30, 2026
161c61c
Update preserves/ensures syntax: use multiple clauses instead of **
gebner Jan 30, 2026
f4cf2ec
Remove redundant 'requires emp', 'ensures emp', and 'preserves emp' c…
gebner Jan 30, 2026
9c3a637
Replace matching requires/ensures pairs with preserves
gebner Jan 30, 2026
958aa13
Refresh syntax: use multiple clauses and preserves
gebner Feb 3, 2026
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
1 change: 0 additions & 1 deletion lib/pulse/c/Pulse.C.Types.Array.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -556,7 +556,6 @@ requires
(freeable_array a ** array_pts_to a s ** pure (
full_seq td s
))
ensures emp
{
let al = array_ptr_of a;
let n: array_len_t al = array_len_of a;
Expand Down
1 change: 0 additions & 1 deletion lib/pulse/c/Pulse.C.Types.Base.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,6 @@ requires
(pts_to_or_null p v ** pure (
p == null _
))
ensures emp
{
rewrite (pts_to_or_null p v) as emp
}
Expand Down
49 changes: 27 additions & 22 deletions lib/pulse/lib/Pulse.Lib.AVLTree.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,8 +139,9 @@ fn cases_of_is_tree #t (x:tree_t t) (ft:T.tree t)

ghost
fn is_tree_case_none (#t:Type) (x:tree_t t) (#l:T.tree t)
requires is_tree x l ** pure (x == None)
ensures is_tree x l ** pure (l == T.Leaf)
preserves is_tree x l
requires pure (x == None)
ensures pure (l == T.Leaf)
{
rewrite each x as None;
cases_of_is_tree None l;
Expand All @@ -154,7 +155,8 @@ fn is_tree_case_none (#t:Type) (x:tree_t t) (#l:T.tree t)

ghost
fn is_tree_case_some (#t:Type) (x:tree_t t) (v:node_ptr t) (#ft:T.tree t)
requires is_tree x ft ** pure (x == Some v)
requires is_tree x ft
requires pure (x == Some v)
ensures
exists* (node:node t) (ltree:T.tree t) (rtree:T.tree t).
(v |-> node) **
Expand All @@ -173,9 +175,9 @@ ensures


fn rec height (#t:Type0) (x:tree_t t)
requires is_tree x 'l
preserves is_tree x 'l
returns n:nat
ensures is_tree x 'l ** pure (n == T.height 'l)
ensures pure (n == T.height 'l)
{
match x {
None -> {
Expand All @@ -201,9 +203,9 @@ fn rec height (#t:Type0) (x:tree_t t)


fn is_empty (#t:Type) (x:tree_t t) (#ft:G.erased(T.tree t))
requires is_tree x ft
preserves is_tree x ft
returns b:bool
ensures is_tree x ft ** pure (b <==> (T.is_empty ft))
ensures pure (b <==> (T.is_empty ft))
{
match x {
None -> {
Expand All @@ -225,7 +227,6 @@ let null_tree_t (t:Type0) : tree_t t = None


fn create (t:Type0)
requires emp
returns x:tree_t t
ensures is_tree x T.Leaf
{
Expand All @@ -239,7 +240,8 @@ fn node_cons (#t:Type0) (v:t) (ltree:tree_t t) (rtree:tree_t t) (#l:(T.tree t))
requires is_tree ltree l **
is_tree rtree r //functional equivalent of x is 'l; x is the tail of the constructed tree.
returns y:tree_t t
ensures is_tree y (T.Node v l r) ** (pure (Some? y))
ensures is_tree y (T.Node v l r)
ensures (pure (Some? y))
{
let y = Box.alloc { data=v; left =ltree; right = rtree };
intro_is_tree_node (Some y) y;
Expand All @@ -251,9 +253,10 @@ fn node_cons (#t:Type0) (v:t) (ltree:tree_t t) (rtree:tree_t t) (#l:(T.tree t))
/// Appends value [v] at the leftmost leaf of the tree that [ptr] points to.

fn rec append_left_none (#t:Type0) (x:tree_t t) (v:t) (#ft:G.erased (T.tree t))
requires is_tree x ft ** pure (None? x)
preserves is_tree x ft
requires pure (None? x)
returns y:tree_t t
ensures is_tree x ft ** is_tree y (T.Node v T.Leaf T.Leaf)
ensures is_tree y (T.Node v T.Leaf T.Leaf)
{
let left = create t;
let right = create t;
Expand Down Expand Up @@ -355,9 +358,9 @@ fn rec append_right (#t:Type0) (x:tree_t t) (v:t) (#ft:G.erased (T.tree t))


fn node_data (#t:Type) (x:tree_t t) (#ft:G.erased (T.tree t))
requires is_tree x ft ** (pure (Some? x))
preserves is_tree x ft
requires (pure (Some? x))
returns v:t
ensures is_tree x ft
{
let np = Some?.v x;

Expand All @@ -374,9 +377,9 @@ fn node_data (#t:Type) (x:tree_t t) (#ft:G.erased (T.tree t))


fn rec mem (#t:eqtype) (x:tree_t t) (v: t) (#ft:G.erased (T.tree t))
requires is_tree x ft
preserves is_tree x ft
returns b:bool
ensures is_tree x ft ** pure (b <==> (T.mem ft v))
ensures pure (b <==> (T.mem ft v))
{
match x {
None -> {
Expand Down Expand Up @@ -412,7 +415,8 @@ fn rec mem (#t:eqtype) (x:tree_t t) (v: t) (#ft:G.erased (T.tree t))


fn get_some_ref (#t:Type) (x:tree_t t)
requires is_tree x 'l ** pure (T.Node? 'l)
requires is_tree x 'l
requires pure (T.Node? 'l)
returns v:node_ptr t
ensures
exists* (node:node t) (ltree:T.tree t) (rtree:T.tree t).
Expand Down Expand Up @@ -538,9 +542,9 @@ module M = FStar.Math.Lib


fn rec is_balanced (#t:Type0) (tree:tree_t t)
requires is_tree tree 'l
preserves is_tree tree 'l
returns b:bool
ensures is_tree tree 'l ** pure (b <==> (T.is_balanced 'l))
ensures pure (b <==> (T.is_balanced 'l))
{
match tree {
None -> {
Expand Down Expand Up @@ -742,8 +746,9 @@ fn rec insert_avl (#t:Type0) (cmp: T.cmp t) (tree:tree_t t) (key: t)

ghost
fn is_tree_case_some1 (#t:Type) (x:tree_t t) (v:node_ptr t) (#ft:T.tree t)
requires is_tree x ft ** pure (x == Some v)
ensures is_tree x ft ** pure (T.Node? ft)
preserves is_tree x ft
requires pure (x == Some v)
ensures pure (T.Node? ft)
{
rewrite each x as Some v;
cases_of_is_tree (Some v) ft;
Expand All @@ -753,9 +758,9 @@ fn is_tree_case_some1 (#t:Type) (x:tree_t t) (v:node_ptr t) (#ft:T.tree t)
}

fn rec tree_max_c (#t:Type0) (tree:tree_t t) (#l:G.erased(T.tree t){T.Node? l})
requires is_tree tree l
preserves is_tree tree l
returns y:t
ensures is_tree tree l ** pure (y == T.tree_max l)
ensures pure (y == T.tree_max l)
{
match tree {
None -> {
Expand Down
12 changes: 6 additions & 6 deletions lib/pulse/lib/Pulse.Lib.AVLTree.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,23 +31,23 @@ val is_tree #t ([@@@mkey] ct:tree_t t) (ft:T.tree t)
: Tot slprop (decreases ft)

fn height (#t:Type0) (x:tree_t t) (#ft:G.erased (T.tree t))
requires is_tree x ft
preserves is_tree x ft
returns n : nat
ensures is_tree x ft ** pure (n == T.height ft)
ensures pure (n == T.height ft)

fn is_empty (#t:Type) (x:tree_t t) (#ft:G.erased(T.tree t))
requires is_tree x ft
preserves is_tree x ft
returns b : bool
ensures is_tree x ft ** pure (b <==> (T.is_empty ft))
ensures pure (b <==> (T.is_empty ft))

fn create (t:Type0)
returns x : tree_t t
ensures is_tree x T.Leaf

fn mem (#t:eqtype) (x:tree_t t) (v: t) (#ft:G.erased (T.tree t))
requires is_tree x ft
preserves is_tree x ft
returns b : bool
ensures is_tree x ft ** pure (b <==> (T.mem ft v))
ensures pure (b <==> (T.mem ft v))

fn insert_avl
(#t:Type0) (cmp: T.cmp t) (tree:tree_t t) (key: t)
Expand Down
63 changes: 39 additions & 24 deletions lib/pulse/lib/Pulse.Lib.AnchoredReference.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,8 @@ fn alloc (#a:Type) (x:a) (#p:_) (#anc:anchor_rel p)
ghost
fn share (#a:Type) (#p:_) (#anc:_) (r:ref a p anc) (#f: perm) (#v:erased a)
requires pts_to r #f v
ensures pts_to r #(f /. 2.0R) v ** pts_to r #(f /. 2.0R) v
ensures pts_to r #(f /. 2.0R) v
ensures pts_to r #(f /. 2.0R) v
{
unfold (pts_to r #f v);
with k. assert (GPR.pts_to r k);
Expand All @@ -125,8 +126,10 @@ fn share (#a:Type) (#p:_) (#anc:_) (r:ref a p anc) (#f: perm) (#v:erased a)

ghost
fn gather (#a:Type) (#p:_) (#anc:_) (r:ref a p anc) (#v1 #v2:erased a) (#f1 #f2: perm)
requires pts_to r #f1 v1 ** pts_to r #f2 v2
ensures pts_to r #(f1 +. f2) v1 ** pure (v1 == v2)
requires pts_to r #f1 v1
requires pts_to r #f2 v2
ensures pts_to r #(f1 +. f2) v1
ensures pure (v1 == v2)
{
unfold (pts_to r #f1 v1);
unfold (pts_to r #f2 v2);
Expand All @@ -136,7 +139,8 @@ fn gather (#a:Type) (#p:_) (#anc:_) (r:ref a p anc) (#v1 #v2:erased a) (#f1 #f2:

ghost
fn write (#a:Type) (#p:_) (#anc:_) (r:ref a p anc) (#v:erased a) (w : erased a)
requires pts_to r v ** pure (p v w /\ (forall anchor. anc anchor v ==> anc anchor w))
requires pts_to r v
requires pure (p v w /\ (forall anchor. anc anchor v ==> anc anchor w))
ensures pts_to r w
{
unfold (pts_to r v);
Expand All @@ -147,7 +151,8 @@ fn write (#a:Type) (#p:_) (#anc:_) (r:ref a p anc) (#v:erased a) (w : erased a)

ghost
fn write_full (#a:Type) (#p:_) (#anc:_) (r:ref a p anc) (#v:erased a) (w : erased a)
requires pts_to_full r v ** pure (p v w /\ anc w w)
requires pts_to_full r v
requires pure (p v w /\ anc w w)
ensures pts_to_full r w
{
unfold (pts_to_full r v);
Expand All @@ -169,7 +174,8 @@ fn leave_anchor_pts_to
ghost
fn drop_anchor (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a)
requires pts_to_full r v
ensures pts_to r v ** anchored r v
ensures pts_to r v
ensures anchored r v
{
unfold (pts_to_full r v);
with k. assert (GPR.pts_to r k);
Expand All @@ -185,7 +191,8 @@ ghost
fn unfold_anchored (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a)
requires anchored r v
returns k:FRAP.knowledge anc
ensures GPR.pts_to r k ** pure (owns_only_anchor v k)
ensures GPR.pts_to r k
ensures pure (owns_only_anchor v k)
{
unfold (anchored r v);
with k. assert (GPR.pts_to r k);
Expand All @@ -194,7 +201,8 @@ fn unfold_anchored (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a)

ghost
fn fold_anchored (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a) (k:FRAP.knowledge anc)
requires GPR.pts_to r k ** pure (owns_only_anchor v k)
requires GPR.pts_to r k
requires pure (owns_only_anchor v k)
ensures anchored r v
{
fold (anchored r v)
Expand All @@ -203,8 +211,11 @@ fn fold_anchored (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a) (

ghost
fn lift_anchor (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a) (va:a)
requires pts_to r v ** anchored r va ** pure (anc v v)
ensures pts_to_full r v ** pure (anc va v /\ True)
requires pts_to r v
requires anchored r va
requires pure (anc v v)
ensures pts_to_full r v
ensures pure (anc va v /\ True)
{
unfold (pts_to r v);
with k0. assert (GPR.pts_to r k0);
Expand All @@ -217,8 +228,9 @@ fn lift_anchor (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a) (va

ghost
fn recall_anchor (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a) (va:a) (#f:perm)
requires pts_to r #f v ** anchored r va
ensures pts_to r #f v ** anchored r va ** pure (anc va v)
preserves pts_to r #f v
preserves anchored r va
ensures pure (anc va v)
{
unfold (pts_to r #f v);
with k0. assert (GPR.pts_to r k0);
Expand All @@ -234,7 +246,8 @@ ghost
fn unfold_snapshot (#a:Type) (#p:_) (#anc:_) (r : ref a p anc) (#v:a)
requires snapshot r v
returns k:FRAP.knowledge anc
ensures GPR.pts_to r k ** pure (snapshot_pred v k)
ensures GPR.pts_to r k
ensures pure (snapshot_pred v k)
{
unfold (snapshot r v);
with k. assert (GPR.pts_to r k);
Expand All @@ -243,16 +256,17 @@ fn unfold_snapshot (#a:Type) (#p:_) (#anc:_) (r : ref a p anc) (#v:a)

ghost
fn fold_snapshot (#a:Type) (#p:_) (#anc:_) (r : ref a p anc) (#v:a) (k:FRAP.knowledge anc)
requires GPR.pts_to r k ** pure (snapshot_pred v k)
requires GPR.pts_to r k
requires pure (snapshot_pred v k)
ensures snapshot r v
{
fold (snapshot r v)
}

ghost
fn dup_snapshot (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a)
requires snapshot r v
ensures snapshot r v ** snapshot r v
preserves snapshot r v
ensures snapshot r v
{
unfold snapshot;
with k. assert (GPR.pts_to r k);
Expand All @@ -265,8 +279,8 @@ fn dup_snapshot (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) (#v:a)

ghost
fn take_snapshot_core (#a:Type) (#p:_) (#f:perm) (#anc:anchor_rel p) (r : ref a p anc) (#b:bool) (#v:a)
requires core_pts_to r #f v b
ensures core_pts_to r #f v b ** snapshot r v
preserves core_pts_to r #f v b
ensures snapshot r v
{
with k. assert (GPR.pts_to r k);
rewrite (GPR.pts_to r k)
Expand All @@ -278,8 +292,8 @@ fn take_snapshot_core (#a:Type) (#p:_) (#f:perm) (#anc:anchor_rel p) (r : ref a

ghost
fn take_snapshot (#a:Type) (#p:_) (#f:perm) (#anc:anchor_rel p) (r : ref a p anc) (#v:a)
requires pts_to r #f v
ensures pts_to r #f v ** snapshot r v
preserves pts_to r #f v
ensures snapshot r v
{
unfold (pts_to r #f v);
take_snapshot_core #a #p #f r #false #v;
Expand All @@ -288,8 +302,8 @@ fn take_snapshot (#a:Type) (#p:_) (#f:perm) (#anc:anchor_rel p) (r : ref a p anc

ghost
fn take_snapshot_full (#a:Type) (#p:_) (#f:perm) (#anc:anchor_rel p) (r : ref a p anc) (#v:a)
requires pts_to_full r #f v
ensures pts_to_full r #f v ** snapshot r v
preserves pts_to_full r #f v
ensures snapshot r v
{
unfold (pts_to_full r #f v);
take_snapshot_core #a #p #f r #true #v;
Expand All @@ -298,8 +312,9 @@ fn take_snapshot_full (#a:Type) (#p:_) (#f:perm) (#anc:anchor_rel p) (r : ref a

ghost
fn recall_snapshot (#a:Type) (#p:_) (#anc:anchor_rel p) (r : ref a p anc) #f (#v0 #v:a)
requires pts_to r #f v ** snapshot r v0
ensures pts_to r #f v ** snapshot r v0 ** pure (p v0 v /\ True)
preserves pts_to r #f v
preserves snapshot r v0
ensures pure (p v0 v /\ True)
{
unfold (pts_to r #f v);
with k. assert (GPR.pts_to r k);
Expand Down
Loading
Loading