Function pointers: ghost arguments, correct witness arity, and array-length refinements - #281
Closed
hei411 wants to merge 11 commits into
Closed
Function pointers: ghost arguments, correct witness arity, and array-length refinements#281hei411 wants to merge 11 commits into
hei411 wants to merge 11 commits into
Conversation
This test does not pass, deliberately, in the same spirit as dda5a8b ("add failing cases for initialized array locals"). It records a gap rather than fixing it, so the branch should not be merged as is. Taking the address of a function whose contract uses `_ghost_arg` emits a `__fp` wrapper interface that does not typecheck: * Error 72 at out/Funcptr_impl_one.fsti(11,51-11,56): - Identifier not found: var_v `emit_fn_sig_inner` and `emit_pure_fn` both walk `decl.ghost_args` and do two things per ghost argument: push a `(#var_v: erased ty)` binder, and register the name with `env.push_var_decl(..., RValue)`. `emit_fnptr_spec_core` walks only `decl.args` and does neither, so the two omissions land on the same line: Func_impl_one.fsti (verifies) Funcptr_impl_one.fsti (Error 72) (#var_v: erased ty_int32_t) -- binder absent -- pts_to var_q #1.0R var_v pts_to var_q #1.0R (!var_v) The name is free *and*, being unregistered, the `$(v)` antiquotation is lowered as a C variable read rather than a plain rvalue. There is a second, independent gap behind it: a function pointer has nowhere to pass a ghost argument. The witness tuple `c` is built purely from `req_witness_groups`, i.e. from ownership groups of pointer arguments, so a `_plain` pointer under a user-written `_preserves` slprop contributes nothing and `c` collapses to `unit` -- call sites emit `call_div ... (hide ())`. The test covers one and two ghost arguments, since those exercise the arity-1 and arity-N witness shapes, and includes direct-call counterparts that already verify today to isolate the fnptr path. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
An indirect call site has no callee declaration, so the ghost arity has to travel with the *type* written at the call site -- a struct field or a local. `TypeT::FnPtr` therefore gains `ghost_args`, read off a `pal-ghost-arg` annotation on a `FieldDecl` or `VarDecl`. The erased witness `c` of `Pulse.Lib.C.FuncPtr` widens from the elim tuple alone to `(elims & ghosts)`, and a call site emits `hide (elims, (_, .., _))`. The tuple spine has to be written out: Pulse solves a hole standing for a tuple *leaf*, but not one standing for a whole tuple. Neither `_ghost_arg` nor `_plain` affects assignability -- `vtype_eq` ignores the former and `vtype_whnf` strips the latter -- so they are purely a call-site obligation. test/ghost_fnptr covers one and two ghost arguments, a mixed case with two owned pointers and two ghosts (a witness nested on both sides), a no-ghost control, direct calls, calls through a global ops table, and a call through a local function pointer. It also covers a field-level `_refine` carrying `is_valid`: `struct ops` advertises a *weaker* contract for `m` than `impl_mixed`'s own, so `get_ops` must reach it with `FuncPtr.weaken` and two ghost coercions, and `call_via_returned_ops` then dispatches through the returned pointer with no `of_fn_div_valid` of its own. Unlike `struct itemx` in test/func_pointer this closes no module cycle, because `impl_mixed`'s signature never mentions `struct ops`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
Follow-up review of the previous commit.
`check.rs` never visited `TypeT::FnPtr`'s `ghost_args`: the five other type
walkers were extended but this one still matched `{ args, ret, .. }`, so a
malformed ghost-arg type on a field or local was silently unvalidated.
In the test, `m_post_w` was a contentless alias for `post_of`, which obscured
where the weakening actually happens. `post_of` now goes straight into
`weaken` and the field `_refine`, leaving `m_pre_w` as the only thing that
weakens and `m_wpost` as a visible identity coercion. Also folded three
restatements of the hole/spine rule into one, dropped an aside about a module
cycle that does not arise here, and replaced `call_direct_one`/`_two` with
`call_direct_mixed`, which subsumes both.
Two things I checked and deliberately did *not* change:
- `env.rs`'s `FnRef` decay carrying `ghost_args` is unobserved by any emitted
output (verified: the suite is green with `vec![]` there), because an
indirect call reads a field or a local, never a bare `FnRef`. Kept, since
`vec![]` would be a lie the moment that stops holding; noted in a comment.
- `fnptr_with_ghost_args`'s wrapper arms look over-general, but `trTypeAttrs`
applies wrappers by attribute name without consulting the underlying type,
so `_plain` and the other refinement forms really can sit on a
function-pointer declaration. Narrowing the match rejected valid input.
Recorded the reason in a comment.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
Reverts src/ and cpp/ to main, dropping the TypeT::FnPtr ghost_args
plumbing. That approach made the call site work by widening the declared
type, which is the wrong lever: it forces every fnptr variable's
annotations to agree with the callee's.
Instead, add `eta_expanded` and its four eager-intro rules to
Pulse.Lib.C.FuncPtr, and carry it in `call`/`call_div`'s precondition.
Discharging `eta_expanded ?w` at a tuple type expands `?w` into a real
spine of fresh leaf uvars, which Pulse can then solve. `tuple3` and
above are flat in F*, so a binary rule never fires on them; producers
must fold witness types to the right for one rule to suffice.
Measured: eta alone is not enough. The leaves are inferred only when the
spec destructures the witness by pattern (`let (a, b) = reveal w in`);
`fst`/`snd` projections, which is what PAL emits today, lose them. A
`pure` conjunct mentioning the leaves, `prevent_lifting`, an explicit
rather than implicit witness, and an extra non-witness argument were all
ruled out individually.
test/ghost_fnptr gains `impl_plain_two`, `assign_across_shapes` and
`call_across_shapes`: one function-pointer variable, written with two
implementations whose `_plain` annotations disagree, and called after
each write.
NOTE: this commit does not pass `make test`. ghost_fnptr is the target
to work toward, and fails in exactly two ways:
- 3 x Error 72, `_ghost_arg` dropped on fnptr declarations, so the
witness comes out `erased unit` and the ghost name is unbound;
- 1 x Error 76 in call_across_shapes, where both calls receive the
same witness read off the declared type although the second callee
needs `unit`.
`pre` and `post` are already emitted as `_` and inferred per call from
the `is_valid` in scope. The witness is the only argument still derived
syntactically, so closing the gap is localized to how
`emit_fnptr_spec_core` binds it, plus a `rewrite each` prelude in the
wrapper body to unstick the resulting match.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
A function-pointer call site used to compute its `erased c` witness syntactically, by reading the pointee values off the *declared* type of the function-pointer variable. That made the witness part of the variable's interface: a variable could only hold callees that agreed on which arguments were `_plain` and on how many `_ghost_arg`s they had, and the declaration had to repeat the callee's ghost arity. Call sites now emit `_` and let Pulse infer it, which needs three things: * The witness is always the pair `(ELIMS & GHOSTS)` -- the existentials eliminated from the pointer arguments, and the `_ghost_arg`s -- with each side right-nested binary. `Pulse.Lib.C.FuncPtr`'s `eta_expanded_pair` rule is binary, and F*'s `a & b & c` is a flat `tuple3` rather than nested `tuple2`s, so only a right-nested spine can be solved. The pair is unconditional (an argument-less function gets `(unit & unit)`) so that every function pointer of a given C type has the same `c`. * The wrapper's `requires` destructures the witness by *pattern* rather than by `fst`/`snd`. This is the crux: a pattern applied to an unsolved witness is a stuck match, so the prover defers, eta solves the spine, and the leaves fall out of ordinary slprop matching. Projections look matchable immediately, so the prover commits and is left with a non-invertible `fst (reveal ?w) =?= v`. * Two consequences of introducing that match, both of which cost real time to find, so they are commented where they bite: Pulse's spec-level `!` auto-deref does not cross a match branch (it silently degrades to the stateful read), so pointee reads in the `requires` now emit the witness binding name; and `with_pure` is left partially applied under a match, so the wrapper `requires` emits `pure`. Neither applies to the `ensures`, which binds its own `exists*` and must stay definitionally equal to the callee's own post -- hence each ownership group is emitted twice, deliberately. The wrapper body eta-expands the witness in a single `rewrite each`; doing it one level at a time works only to depth 1 and then fails to prove the tuple-eta equality for the inner Ghost projection. `emit_fnptr_spec_core` also now handles `decl.ghost_args` at all, which is what lets `_ghost_arg` be dropped from function-pointer variable declarations. `test/ghost_fnptr` covers the payoff: `assign_across_shapes` and `call_across_shapes` put callees with different `_plain` annotations in one variable and call through it. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
`call_across_shapes` only varied the *elim* half of the witness: both callees had zero ghost arguments. Extend it (and `assign_across_shapes`) to four callees that disagree on both halves -- impl_elim_two 2 elims, 0 ghosts c = ((i32 & i32) & unit) impl_plain_two 0 elims, 0 ghosts c = (unit & unit) impl_one_of_two 0 elims, 1 ghost c = (unit & i32) impl_two 0 elims, 2 ghosts c = (unit & (i32 & i32)) -- so the ghost side is exercised empty, singular and nested, all through one function-pointer variable. `impl_one_of_two` is new; its unused `r` is there only so the last three share a C type. `impl_two`'s result is discarded, since it states no `_ensures` and folding it into the sum would be an unprovable `int32` overflow check rather than anything about witnesses. Also drop the `_ghost_arg`s from the `struct ops` fields and correct the header comment, which claimed an indirect call site learns its ghost arity from the type written in the struct and emits `hide (elims, (_, .., _))`. Neither is true now that call sites emit `_`; and in fact `pal-ghost-arg` is only ever read for a `FunctionDecl` (cpp/impl.cpp), never a `FieldDecl`, so those annotations were silently ignored no-ops. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
Drops the witness-inference emitter changes from e6861a0 and returns src/pass/emit.rs to its state on main. The `deref_subst` / `deref_record` / `deref_apply` machinery, the `pure_not_with_pure` switch, the nested witness helpers and the emit-twice hack all go with it, as does emitting `_` for the witness at function-pointer call sites. `pulse/Pulse.Lib.C.FuncPtr.fsti` (the `eta_expanded` rules) and `test/ghost_fnptr/` are deliberately left in place, so the suite now fails: the test states the behaviour we want from the emitter and there is no emitter support for it any more. Context for the revert: the `deref_subst` approach was judged too convoluted, and the simpler alternative does not exist in the shape it was proposed in. Keeping the witness pattern-let but hoisting `__pred (!p)` and `with_pure` out of it still fails, because Pulse's `!` lifting is poisoned by a match anywhere in the term (Error 12); hiding the match behind an `unfold` helper clears that but then `!p` cannot find its `pts_to`, which now sits inside the hidden match (Error 228). So the pointee value has to be spelled as the witness-bound name one way or another, and a cleaner way to arrange that still needs designing. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
18ef155 put emit.rs back on main. This restores the witness encoding, but built on an IR node instead of a HashMap keyed on rendered expressions. The wrapper's `requires` has to bind the witness leaves by *pattern*, not by projection: at a call site the witness is an unsolved `?w`, and matching `pts_to var_a #1.0R (fst (fst (reveal ?w)))` fails because that head is not invertible, while the pattern form is a stuck match that the `eta_expanded` rules can solve. That pattern desugars to a `match`, and two of Pulse's frontend rewrites do not traverse into a match branch: `!r` in a spec (which needs to find the ambient `pts_to`) and `with_pure p ** rest` (which needs to see the surrounding conjunction). `deref_subst` existed only to work around the first. But `!var_a` was redundant to begin with: the same arm of `emit_type_slprop_inner` binds the pointee two lines earlier. Recursing with that binding instead of `Deref(this)` means `!` is never emitted under the match, so the problem cannot arise. That needs one emitter-introduced node, `ExprT::SpecVal`, holding the binding's mangled name and the pointer it came from (the latter only so nested bindings keep deriving names from the same base identifier). Refinements fall out too: `subst_this_rvalue` already substitutes `$(this)`, so `$(this)->x` renders `(val_a_0).struct_b__x`. It also lets the `Regular`/`Consumed` groups be emitted once rather than twice, since `requires` and `ensures` now want the same docs. `subst_this_rvalue` becomes `subst_spec_rvalue`, taking a small `SpecSubst` rather than a bare `this`, so its existing in-place traversal can also rewrite `*p` to the pointee binding in a wrapper's user-written `_requires`. The `pure`-for-`with_pure` switch stays: that breakage is the missing continuation, not `!`, and the value-passing change does not touch it. Every function now spells pointee ownership `val_a_0` rather than `(!var_a)`. This is a wider output change than the encoding needs, but it is semantically identical and uniform. The one place it bit was `extract_base_ident`, which has to see through `SpecVal` or nested bindings lose their base name. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
A struct with a pointer field gets an `[@@Erasable]` `struct_X__spec`, so an owned `struct X *` parameter contributes two elim components to a function pointer's witness rather than one. #277 reports that as a call-site arity bug, but the code it quotes -- which wrote the elim spine out by hand, one component per pointer argument -- no longer exists: the call site emits `_` for the whole witness and `eta_expanded` solves the spine, so there is nothing left to miscount. `call_dep` is the issue's reproducer and verifies, alongside its `call_ok` control. `call_mixed` then puts every kind of component in one witness -- a `__spec` leaf, a second owned pointer, and a ghost argument -- c = ((struct_dep & (struct_dep__spec & ty_int32_t)) & ty_int32_t) the first case in the tree where both halves are non-trivial and one argument contributes more than one leaf. Its `ops_mixed` field carries `is_valid` as a `_refine`, which is *not* what makes the call go through: a global's `acquire` yields a bare `pts_to` at the global's value rather than the struct's `__pred`, so the refinement is not in scope. Reintroducing it is free -- `o_m.m` is definitionally `of_fn_div .. impl_mixed`, so `of_fn_div_valid` supplies the `is_valid` from `emp` -- and `call_via_o_mixed` in test/ghost_fnptr already relies on that without saying so. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
A struct-level `_refine` mentioning an `_array` field's `_length` breaks the
`__fp` wrapper of any function that is address-taken:
* Error 54 at out/Funcptr_use.fsti(17,27-17,75) by pointer
* Error 54 at out/Funcptr_use_byval.fsti(15,27-15,73) by value
`Func_use` and `Func_use_byval` (the direct calls) both verify.
PAL emits `arr._length` as `reveal (length_of arr)`. `length_of` is a
`ghost fn` that needs its `array_pts_to` in the ambient context and answers
through `rewrites_to`, so resolving it depends on a Pulse normalisation step.
In a wrapper that conjunct sits inside the witness pattern `let`, which
desugars to a `match`, and the normalisation does not run there.
The by-value case is the sharper one: its two failing conjuncts mention only
`x_fp`, a plain parameter, and never a witness binding -- they fail purely
because of where they sit, not what they refer to.
Committed red on purpose; the fix follows.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
`length_of` is a `ghost fn`: it needs the array's `array_pts_to` in the ambient
context and answers through `rewrites_to`, so resolving it depends on a Pulse
normalisation step. A function pointer wrapper puts the whole `requires` inside
the witness pattern `let`, which desugars to a `match`, and that step does not
run there. A struct-level `_refine` reading an `_array` field's `_length` was
therefore fatal to the wrapper of any address-taken function:
* Error 54 at out/Funcptr_use.fsti(17,27-17,75)
* Error 54 at out/Funcptr_use_byval.fsti(15,27-15,73)
`pure` versus `with_pure` is not the issue -- `with_pure` only trades those for
Error 230, or for nine errors ending in Error 339. Nor is it about what the
conjunct refers to: in the by-value case the failing conjuncts name only the
plain parameter `x_fp` and no witness binding, and still fail.
The struct's predicate already binds a spec record holding each array field's
`array_spec`, and `array_spec_len` is a pure `GTot` projection of it. So emit
reveal (length_of (var_b).struct_box__arr)
-> array_spec_len val_b_0.struct_box__spec__arr_0
which needs no ownership in context and no rewrite, and so elaborates under a
match as readily as outside one. This is the same move `PointerKind::Ref`
already makes by handing its pointee down as a `SpecVal` rather than a `Deref`,
and the spelling is the one already used for flexible array members.
A `spec_scope` stack records, for the duration of a struct's slprop, the spec
record its predicate just bound; the `VAttr(Length)` arm consults it. Spec field
names are re-derived through the existing `Name::TypeRefSpecField` mangling
rather than threaded through a new map. The rewrite applies only to a
directly-owned array field of a struct in scope; everything else keeps the
`length_of` spelling unchanged.
Beyond the new cases this changes one typedef pred and four `refine_struct`
modules, all of which still verify.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
Generated F* output diffEffect of this pull request on the F* code SummaryFull diff: full diff artifact Diffdiff --git base/addr_global/Func_call_via_addr_of_global_struct.fst head/addr_global/Func_call_via_addr_of_global_struct.fst
index 3f21c5d..2f6b788 100644
--- base/addr_global/Func_call_via_addr_of_global_struct.fst
+++ head/addr_global/Func_call_via_addr_of_global_struct.fst
@@ -17,7 +17,7 @@ divergent fn func_call_via_addr_of_global_struct ()
_
(!(Struct_ops_anon_1.struct_ops_anon_1__get_op (!var_p)))
(2l, 3l)
- (hide ())));
+ _));
Pulse.Lib.C.FuncPtr.drop_is_valid _ _ _;
drop_ (exists* q. pts_to Global_g_ops.addr_var_g_ops #q _);
return return_1;
diff --git base/addr_global/Funcptr_add.fst head/addr_global/Funcptr_add.fst
index 4ebd91a..c588c5b 100644
--- base/addr_global/Funcptr_add.fst
+++ head/addr_global/Funcptr_add.fst
@@ -5,7 +5,7 @@ open Pulse.Lib.C
-divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)) (y_fp: erased unit)
+divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)) (y_fp: erased (unit & unit))
requires ((Pulse.Lib.C.FuncPtr.prevent_lifting
(let var_a = (fst x_fp) in
let var_b = (snd x_fp) in
@@ -29,5 +29,5 @@ divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.t
((id #int (Int32.v var_b)) < 100)))) ==> (((return_1 =
(var_a `Int32.add` var_b))))))))
{
- Func_add.func_add (fst x_fp) (snd x_fp)
+ Func_add.func_add (fst x_fp) (snd x_fp)
}
\ No newline at end of file
diff --git base/addr_global/Funcptr_add.fsti head/addr_global/Funcptr_add.fsti
index 6d913a3..e5ed181 100644
--- base/addr_global/Funcptr_add.fsti
+++ head/addr_global/Funcptr_add.fsti
@@ -5,7 +5,7 @@ open Pulse.Lib.C
-divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)) (y_fp: erased unit)
+divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)) (y_fp: erased (unit & unit))
requires ((Pulse.Lib.C.FuncPtr.prevent_lifting
(let var_a = (fst x_fp) in
let var_b = (snd x_fp) in
diff --git base/anon_struct/Func_frob.fst head/anon_struct/Func_frob.fst
index 604ab24..937c132 100644
--- base/anon_struct/Func_frob.fst
+++ head/anon_struct/Func_frob.fst
@@ -6,13 +6,11 @@ open Pulse.Lib.C
divergent fn func_frob (var_b: (ref Struct_baz.struct_baz))
requires
exists* (val_b_0: Struct_baz.struct_baz).
- ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
- (Struct_baz.struct_baz__pred (!var_b) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred val_b_0 1.0R))
returns return_1 : Int32.t
ensures
exists* (val_b_0: Struct_baz.struct_baz).
- ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
- (Struct_baz.struct_baz__pred (!var_b) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred val_b_0 1.0R))
ensures
(with_pure
((!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b))) =
diff --git base/anon_struct/Func_frob.fsti head/anon_struct/Func_frob.fsti
index ce430af..59d7f0b 100644
--- base/anon_struct/Func_frob.fsti
+++ head/anon_struct/Func_frob.fsti
@@ -6,11 +6,11 @@ open Pulse.Lib.C
divergent fn func_frob (var_b: (ref Struct_baz.struct_baz))
requires
exists* (val_b_0: Struct_baz.struct_baz).
- ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred (!var_b) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred val_b_0 1.0R))
returns return_1 : Int32.t
ensures
exists* (val_b_0: Struct_baz.struct_baz).
- ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred (!var_b) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred val_b_0 1.0R))
ensures
(with_pure
((!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b))) =
diff --git base/anon_struct/Func_use_profiles.fst head/anon_struct/Func_use_profiles.fst
index ed56271..f97d2df 100644
--- base/anon_struct/Func_use_profiles.fst
+++ head/anon_struct/Func_use_profiles.fst
@@ -9,14 +9,14 @@ divergent fn func_use_profiles (var_p: (ref Typedef_profiles.ty_profiles))
(val_p_0: Typedef_profiles.ty_profiles)
(val_p_1: Struct_profiles.struct_profiles__spec).
((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
- (Typedef_profiles.ty_profiles__pred (!var_p) 1.0R val_p_1))
+ (Typedef_profiles.ty_profiles__pred val_p_0 1.0R val_p_1))
returns return_1 : unit
ensures
exists*
(val_p_0: Typedef_profiles.ty_profiles)
(val_p_1: Struct_profiles.struct_profiles__spec).
((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
- (Typedef_profiles.ty_profiles__pred (!var_p) 1.0R val_p_1))
+ (Typedef_profiles.ty_profiles__pred val_p_0 1.0R val_p_1))
{
let mut var_p = var_p;
}
\ No newline at end of file
diff --git base/anon_struct/Func_use_profiles.fsti head/anon_struct/Func_use_profiles.fsti
index 06a4fbb..e0e2e67 100644
--- base/anon_struct/Func_use_profiles.fsti
+++ head/anon_struct/Func_use_profiles.fsti
@@ -7,9 +7,9 @@ divergent fn func_use_profiles (var_p: (ref Typedef_profiles.ty_profiles))
requires
exists* (val_p_0: Typedef_profiles.ty_profiles) (val_p_1: Struct_profiles.struct_profiles__spec).
((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
- (Typedef_profiles.ty_profiles__pred (!var_p) 1.0R val_p_1))
+ (Typedef_profiles.ty_profiles__pred val_p_0 1.0R val_p_1))
returns return_1 : unit
ensures
exists* (val_p_0: Typedef_profiles.ty_profiles) (val_p_1: Struct_profiles.struct_profiles__spec).
((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
- (Typedef_profiles.ty_profiles__pred (!var_p) 1.0R val_p_1))
\ No newline at end of file
+ (Typedef_profiles.ty_profiles__pred val_p_0 1.0R val_p_1))
\ No newline at end of file
diff --git base/anon_struct/Struct_profiles_anon_1.fst head/anon_struct/Struct_profiles_anon_1.fst
index d8322eb..3800d0f 100644
--- base/anon_struct/Struct_profiles_anon_1.fst
+++ head/anon_struct/Struct_profiles_anon_1.fst
@@ -32,11 +32,11 @@ let predicate struct_profiles_anon_1__pred
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_0) **
(Pulse.Lib.Reference.pts_to
- (!(this).struct_profiles_anon_1__begin)
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_0
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_1) **
(Typedef_profile.ty_profile__pred
- (!(!(this).struct_profiles_anon_1__begin))
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_1
p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_2) **
(Pulse.Lib.Reference.pts_to
@@ -44,11 +44,11 @@ let predicate struct_profiles_anon_1__pred
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_0) **
(Pulse.Lib.Reference.pts_to
- (!(this).struct_profiles_anon_1__end)
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_0
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_1) **
(Typedef_profile.ty_profile__pred
- (!(!(this).struct_profiles_anon_1__end))
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_1
p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_2) **
(Pulse.Lib.Reference.pts_to
@@ -56,11 +56,11 @@ let predicate struct_profiles_anon_1__pred
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_0) **
(Pulse.Lib.Reference.pts_to
- (!(this).struct_profiles_anon_1__allocated)
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_0
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_1) **
(Typedef_profile.ty_profile__pred
- (!(!(this).struct_profiles_anon_1__allocated))
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_1
p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_2))
[@@pulse_eager_unfold] let predicate struct_profiles_anon_1__uninit_pred
@@ -80,11 +80,11 @@ struct_profiles_anon_1__pred_unfold
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_0)
ensures (Pulse.Lib.Reference.pts_to
- (!(this).struct_profiles_anon_1__begin)
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_0
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_1)
ensures (Typedef_profile.ty_profile__pred
- (!(!(this).struct_profiles_anon_1__begin))
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_1
p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_2)
ensures (Pulse.Lib.Reference.pts_to
@@ -92,11 +92,11 @@ struct_profiles_anon_1__pred_unfold
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_0)
ensures (Pulse.Lib.Reference.pts_to
- (!(this).struct_profiles_anon_1__end)
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_0
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_1)
ensures (Typedef_profile.ty_profile__pred
- (!(!(this).struct_profiles_anon_1__end))
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_1
p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_2)
ensures (Pulse.Lib.Reference.pts_to
@@ -104,11 +104,11 @@ struct_profiles_anon_1__pred_unfold
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_0)
ensures (Pulse.Lib.Reference.pts_to
- (!(this).struct_profiles_anon_1__allocated)
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_0
#p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_1)
ensures (Typedef_profile.ty_profile__pred
- (!(!(this).struct_profiles_anon_1__allocated))
+ val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_1
p
val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_2)
{
@@ -129,23 +129,14 @@ struct_profiles_anon_1__pred_fold
(val_allocated_1: Typedef_profile.ty_profile)
(val_allocated_2: Struct_profile.struct_profile__spec)
requires (Pulse.Lib.Reference.pts_to (this).struct_profiles_anon_1__begin #p val_begin_0)
- requires (Pulse.Lib.Reference.pts_to (!(this).struct_profiles_anon_1__begin) #p val_begin_1)
- requires (Typedef_profile.ty_profile__pred
- (!(!(this).struct_profiles_anon_1__begin))
- p
- val_begin_2)
+ requires (Pulse.Lib.Reference.pts_to val_begin_0 #p val_begin_1)
+ requires (Typedef_profile.ty_profile__pred val_begin_1 p val_begin_2)
requires (Pulse.Lib.Reference.pts_to (this).struct_profiles_anon_1__end #p val_end_0)
- requires (Pulse.Lib.Reference.pts_to (!(this).struct_profiles_anon_1__end) #p val_end_1)
- requires (Typedef_profile.ty_profile__pred (!(!(this).struct_profiles_anon_1__end)) p val_end_2)
+ requires (Pulse.Lib.Reference.pts_to val_end_0 #p val_end_1)
+ requires (Typedef_profile.ty_profile__pred val_end_1 p val_end_2)
requires (Pulse.Lib.Reference.pts_to (this).struct_profiles_anon_1__allocated #p val_allocated_0)
- requires (Pulse.Lib.Reference.pts_to
- (!(this).struct_profiles_anon_1__allocated)
- #p
- val_allocated_1)
- requires (Typedef_profile.ty_profile__pred
- (!(!(this).struct_profiles_anon_1__allocated))
- p
- val_allocated_2)
+ requires (Pulse.Lib.Reference.pts_to val_allocated_0 #p val_allocated_1)
+ requires (Typedef_profile.ty_profile__pred val_allocated_1 p val_allocated_2)
ensures struct_profiles_anon_1__pred this p ({
struct_profiles_anon_1__spec__begin_0 = val_begin_0;
struct_profiles_anon_1__spec__begin_1 = val_begin_1;
diff --git base/antiquot/Func_test_declare.fst head/antiquot/Func_test_declare.fst
index c20cae0..1aed9e5 100644
--- base/antiquot/Func_test_declare.fst
+++ head/antiquot/Func_test_declare.fst
@@ -7,7 +7,7 @@ divergent fn func_test_declare (var_x: (ref Typedef_my_pair.ty_my_pair))
requires
exists* (val_x_0: Typedef_my_pair.ty_my_pair).
((Pulse.Lib.Reference.pts_to var_x #1.0R val_x_0) **
- (Typedef_my_pair.ty_my_pair__pred (!var_x) 1.0R))
+ (Typedef_my_pair.ty_my_pair__pred val_x_0 1.0R))
requires
(with_pure
((id #int (Int32.v (!(Struct_my_pair_anon_1.struct_my_pair_anon_1__get_a var_x)))) = 0))
@@ -15,7 +15,7 @@ divergent fn func_test_declare (var_x: (ref Typedef_my_pair.ty_my_pair))
ensures
exists* (val_x_0: Typedef_my_pair.ty_my_pair).
((Pulse.Lib.Reference.pts_to var_x #1.0R val_x_0) **
- (Typedef_my_pair.ty_my_pair__pred (!var_x) 1.0R))
+ (Typedef_my_pair.ty_my_pair__pred val_x_0 1.0R))
ensures
(with_pure
((id #int (Int32.v (!(Struct_my_pair_anon_1.struct_my_pair_anon_1__get_a var_x)))) = 0))
diff --git base/antiquot/Func_test_declare.fsti head/antiquot/Func_test_declare.fsti
index a5d3f39..d7cc547 100644
--- base/antiquot/Func_test_declare.fsti
+++ head/antiquot/Func_test_declare.fsti
@@ -7,7 +7,7 @@ divergent fn func_test_declare (var_x: (ref Typedef_my_pair.ty_my_pair))
requires
exists* (val_x_0: Typedef_my_pair.ty_my_pair).
((Pulse.Lib.Reference.pts_to var_x #1.0R val_x_0) **
- (Typedef_my_pair.ty_my_pair__pred (!var_x) 1.0R))
+ (Typedef_my_pair.ty_my_pair__pred val_x_0 1.0R))
requires
(with_pure
((id #int (Int32.v (!(Struct_my_pair_anon_1.struct_my_pair_anon_1__get_a var_x)))) = 0))
@@ -15,7 +15,7 @@ returns return_1 : unit
ensures
exists* (val_x_0: Typedef_my_pair.ty_my_pair).
((Pulse.Lib.Reference.pts_to var_x #1.0R val_x_0) **
- (Typedef_my_pair.ty_my_pair__pred (!var_x) 1.0R))
+ (Typedef_my_pair.ty_my_pair__pred val_x_0 1.0R))
ensures
(with_pure
((id #int (Int32.v (!(Struct_my_pair_anon_1.struct_my_pair_anon_1__get_a var_x)))) = 0))
\ No newline at end of file
diff --git base/array_addressof_loses_index/Func_get_via_addressof_const.fst head/array_addressof_loses_index/Func_get_via_addressof_const.fst
index 61c04c5..1e54a3c 100644
--- base/array_addressof_loses_index/Func_get_via_addressof_const.fst
+++ head/array_addressof_loses_index/Func_get_via_addressof_const.fst
@@ -9,14 +9,14 @@ divergent fn func_get_via_addressof_const (var_c: (ref Typedef_containercopy.ty_
(val_c_0: Typedef_containercopy.ty_containercopy)
(val_c_1: Struct_containercopy.struct_containercopy__spec).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Typedef_containercopy.ty_containercopy__pred (!var_c) 1.0R val_c_1))
+ (Typedef_containercopy.ty_containercopy__pred val_c_0 1.0R val_c_1))
returns return_1 : (array Int32.t)
ensures
exists*
(val_c_0: Typedef_containercopy.ty_containercopy)
(val_c_1: Struct_containercopy.struct_containercopy__spec).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Typedef_containercopy.ty_containercopy__pred (!var_c) 1.0R val_c_1))
+ (Typedef_containercopy.ty_containercopy__pred val_c_0 1.0R val_c_1))
{
let mut var_c = var_c;
return
diff --git base/array_addressof_loses_index/Func_get_via_addressof_const.fsti head/array_addressof_loses_index/Func_get_via_addressof_const.fsti
index b856456..b84cc8a 100644
--- base/array_addressof_loses_index/Func_get_via_addressof_const.fsti
+++ head/array_addressof_loses_index/Func_get_via_addressof_const.fsti
@@ -9,11 +9,11 @@ requires
(val_c_0: Typedef_containercopy.ty_containercopy)
(val_c_1: Struct_containercopy.struct_containercopy__spec).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Typedef_containercopy.ty_containercopy__pred (!var_c) 1.0R val_c_1))
+ (Typedef_containercopy.ty_containercopy__pred val_c_0 1.0R val_c_1))
returns return_1 : (array Int32.t)
ensures
exists*
(val_c_0: Typedef_containercopy.ty_containercopy)
(val_c_1: Struct_containercopy.struct_containercopy__spec).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Typedef_containercopy.ty_containercopy__pred (!var_c) 1.0R val_c_1))
\ No newline at end of file
+ (Typedef_containercopy.ty_containercopy__pred val_c_0 1.0R val_c_1))
\ No newline at end of file
diff --git base/array_test/Typedef_b32_struct.fst head/array_test/Typedef_b32_struct.fst
index a90d140..fc5e8a1 100644
--- base/array_test/Typedef_b32_struct.fst
+++ head/array_test/Typedef_b32_struct.fst
@@ -11,7 +11,8 @@ let ty_b32_struct : Type = Struct_b32_struct_anon_1.struct_b32_struct_anon_1
(val_this_0: Struct_b32_struct_anon_1.struct_b32_struct_anon_1__spec) =
((Struct_b32_struct_anon_1.struct_b32_struct_anon_1__pred this p val_this_0) **
(with_pure
- ((reveal (length_of (this).Struct_b32_struct_anon_1.struct_b32_struct_anon_1__x)) = 32)))
+ ((array_spec_len val_this_0.Struct_b32_struct_anon_1.struct_b32_struct_anon_1__spec__x_0) =
+ 32)))
[@@pulse_eager_unfold] let predicate ty_b32_struct__uninit_pred
([@@@mkey] this: ty_b32_struct)
(val_this_0: (array_spec UInt8.t)) =
diff --git base/array_typedef_pointer/Typedef_PCE.fst head/array_typedef_pointer/Typedef_PCE.fst
index 3e2dd9b..a524e0f 100644
--- base/array_typedef_pointer/Typedef_PCE.fst
+++ head/array_typedef_pointer/Typedef_PCE.fst
@@ -9,7 +9,7 @@ let ty_pce : Type = (ref Typedef_E.ty_e)
([@@@mkey] this: ty_pce)
(p: perm)
(val_this_0: Typedef_E.ty_e) =
- ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_E.ty_e__pred (!this) p))
+ ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_E.ty_e__pred val_this_0 p))
[@@pulse_eager_unfold] let predicate ty_pce__uninit_pred ([@@@mkey] this: ty_pce) =
((Pulse.Lib.Reference.pts_to_uninit this))
instance has_zero_default_ty_pce : (has_zero_default ty_pce) = { zero_default = null }
\ No newline at end of file
diff --git base/array_typedef_pointer/Typedef_PE.fst head/array_typedef_pointer/Typedef_PE.fst
index 35e5aa9..16a21a2 100644
--- base/array_typedef_pointer/Typedef_PE.fst
+++ head/array_typedef_pointer/Typedef_PE.fst
@@ -9,7 +9,7 @@ let ty_pe : Type = (ref Typedef_E.ty_e)
([@@@mkey] this: ty_pe)
(p: perm)
(val_this_0: Typedef_E.ty_e) =
- ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_E.ty_e__pred (!this) p))
+ ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_E.ty_e__pred val_this_0 p))
[@@pulse_eager_unfold] let predicate ty_pe__uninit_pred ([@@@mkey] this: ty_pe) =
((Pulse.Lib.Reference.pts_to_uninit this))
instance has_zero_default_ty_pe : (has_zero_default ty_pe) = { zero_default = null }
\ No newline at end of file
diff --git base/bitfields/Func_read_a.fst head/bitfields/Func_read_a.fst
index 0f37290..7199801 100644
--- base/bitfields/Func_read_a.fst
+++ head/bitfields/Func_read_a.fst
@@ -7,12 +7,12 @@ divergent fn func_read_a (var_s: (ref Struct_flags.struct_flags))
requires
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
returns return_1 : UInt32.t
ensures
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_a var_s))))
{
let mut var_s = var_s;
diff --git base/bitfields/Func_read_a.fsti head/bitfields/Func_read_a.fsti
index f067204..68e069d 100644
--- base/bitfields/Func_read_a.fsti
+++ head/bitfields/Func_read_a.fsti
@@ -7,10 +7,10 @@ divergent fn func_read_a (var_s: (ref Struct_flags.struct_flags))
requires
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
returns return_1 : UInt32.t
ensures
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_a var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_read_flag.fst head/bitfields/Func_read_flag.fst
index 0719ee6..4495c26 100644
--- base/bitfields/Func_read_flag.fst
+++ head/bitfields/Func_read_flag.fst
@@ -7,12 +7,12 @@ divergent fn func_read_flag (var_s: (ref Struct_bits.struct_bits))
requires
exists* (val_s_0: Struct_bits.struct_bits).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ (Struct_bits.struct_bits__pred val_s_0 1.0R))
returns return_1 : bool
ensures
exists* (val_s_0: Struct_bits.struct_bits).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ (Struct_bits.struct_bits__pred val_s_0 1.0R))
ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_flag var_s))))
{
let mut var_s = var_s;
diff --git base/bitfields/Func_read_flag.fsti head/bitfields/Func_read_flag.fsti
index fecfbe3..37a3653 100644
--- base/bitfields/Func_read_flag.fsti
+++ head/bitfields/Func_read_flag.fsti
@@ -6,11 +6,9 @@ open Pulse.Lib.C
divergent fn func_read_flag (var_s: (ref Struct_bits.struct_bits))
requires
exists* (val_s_0: Struct_bits.struct_bits).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
returns return_1 : bool
ensures
exists* (val_s_0: Struct_bits.struct_bits).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_flag var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_read_full.fst head/bitfields/Func_read_full.fst
index da3cbdc..f9d5d7d 100644
--- base/bitfields/Func_read_full.fst
+++ head/bitfields/Func_read_full.fst
@@ -7,12 +7,12 @@ divergent fn func_read_full (var_s: (ref Struct_flags.struct_flags))
requires
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
returns return_1 : UInt32.t
ensures
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_full var_s))))
{
let mut var_s = var_s;
diff --git base/bitfields/Func_read_full.fsti head/bitfields/Func_read_full.fsti
index 986c490..ef0f74c 100644
--- base/bitfields/Func_read_full.fsti
+++ head/bitfields/Func_read_full.fsti
@@ -7,10 +7,10 @@ divergent fn func_read_full (var_s: (ref Struct_flags.struct_flags))
requires
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
returns return_1 : UInt32.t
ensures
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_full var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_read_nibble.fst head/bitfields/Func_read_nibble.fst
index 6389432..a156e3d 100644
--- base/bitfields/Func_read_nibble.fst
+++ head/bitfields/Func_read_nibble.fst
@@ -7,12 +7,12 @@ divergent fn func_read_nibble (var_s: (ref Struct_bits.struct_bits))
requires
exists* (val_s_0: Struct_bits.struct_bits).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ (Struct_bits.struct_bits__pred val_s_0 1.0R))
returns return_1 : UInt8.t
ensures
exists* (val_s_0: Struct_bits.struct_bits).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ (Struct_bits.struct_bits__pred val_s_0 1.0R))
ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_nibble var_s))))
{
let mut var_s = var_s;
diff --git base/bitfields/Func_read_nibble.fsti head/bitfields/Func_read_nibble.fsti
index ed8fabb..96ac5e2 100644
--- base/bitfields/Func_read_nibble.fsti
+++ head/bitfields/Func_read_nibble.fsti
@@ -6,11 +6,9 @@ open Pulse.Lib.C
divergent fn func_read_nibble (var_s: (ref Struct_bits.struct_bits))
requires
exists* (val_s_0: Struct_bits.struct_bits).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
returns return_1 : UInt8.t
ensures
exists* (val_s_0: Struct_bits.struct_bits).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_nibble var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_read_tdef.fst head/bitfields/Func_read_tdef.fst
index fd1e6a8..c463c5d 100644
--- base/bitfields/Func_read_tdef.fst
+++ head/bitfields/Func_read_tdef.fst
@@ -7,12 +7,12 @@ divergent fn func_read_tdef (var_s: (ref Struct_tdef.struct_tdef))
requires
exists* (val_s_0: Struct_tdef.struct_tdef).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
returns return_1 : Typedef_uint16_t.ty_uint16_t
ensures
exists* (val_s_0: Struct_tdef.struct_tdef).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
ensures ((Typedef_uint16_t.ty_uint16_t__pred return_1 1.0R))
ensures (with_pure (return_1 = (!(Struct_tdef.struct_tdef__get_a var_s))))
{
diff --git base/bitfields/Func_read_tdef.fsti head/bitfields/Func_read_tdef.fsti
index af5c5e5..c886040 100644
--- base/bitfields/Func_read_tdef.fsti
+++ head/bitfields/Func_read_tdef.fsti
@@ -6,12 +6,10 @@ open Pulse.Lib.C
divergent fn func_read_tdef (var_s: (ref Struct_tdef.struct_tdef))
requires
exists* (val_s_0: Struct_tdef.struct_tdef).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
returns return_1 : Typedef_uint16_t.ty_uint16_t
ensures
exists* (val_s_0: Struct_tdef.struct_tdef).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
ensures ((Typedef_uint16_t.ty_uint16_t__pred return_1 1.0R))
ensures (with_pure (return_1 = (!(Struct_tdef.struct_tdef__get_a var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_set_a.fst head/bitfields/Func_set_a.fst
index d913f13..0dfa9e0 100644
--- base/bitfields/Func_set_a.fst
+++ head/bitfields/Func_set_a.fst
@@ -7,12 +7,12 @@ divergent fn func_set_a (var_s: (ref Struct_flags.struct_flags))
requires
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
ensures (with_pure ((id #int (UInt32.v (!(Struct_flags.struct_flags__get_a var_s)))) = 5))
{
let mut var_s = var_s;
diff --git base/bitfields/Func_set_a.fsti head/bitfields/Func_set_a.fsti
index bc3a634..b6c1740 100644
--- base/bitfields/Func_set_a.fsti
+++ head/bitfields/Func_set_a.fsti
@@ -7,10 +7,10 @@ divergent fn func_set_a (var_s: (ref Struct_flags.struct_flags))
requires
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
ensures (with_pure ((id #int (UInt32.v (!(Struct_flags.struct_flags__get_a var_s)))) = 5))
\ No newline at end of file
diff --git base/bitfields/Func_tdef_in_range.fst head/bitfields/Func_tdef_in_range.fst
index 19ec482..8ecfb68 100644
--- base/bitfields/Func_tdef_in_range.fst
+++ head/bitfields/Func_tdef_in_range.fst
@@ -7,12 +7,12 @@ divergent fn func_tdef_in_range (var_s: (ref Struct_tdef.struct_tdef))
requires
exists* (val_s_0: Struct_tdef.struct_tdef).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_tdef.struct_tdef).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
{
let mut var_s = var_s;
assert (with_pure ((id #int (UInt16.v (!(Struct_tdef.struct_tdef__get_a (!var_s))))) <= 3));
diff --git base/bitfields/Func_tdef_in_range.fsti head/bitfields/Func_tdef_in_range.fsti
index 3d27218..97d12ea 100644
--- base/bitfields/Func_tdef_in_range.fsti
+++ head/bitfields/Func_tdef_in_range.fsti
@@ -6,10 +6,8 @@ open Pulse.Lib.C
divergent fn func_tdef_in_range (var_s: (ref Struct_tdef.struct_tdef))
requires
exists* (val_s_0: Struct_tdef.struct_tdef).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_tdef.struct_tdef).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
\ No newline at end of file
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
\ No newline at end of file
diff --git base/bitfields/Func_write_a.fst head/bitfields/Func_write_a.fst
index a57ca6f..269a5c8 100644
--- base/bitfields/Func_write_a.fst
+++ head/bitfields/Func_write_a.fst
@@ -7,12 +7,12 @@ divergent fn func_write_a (var_s: (ref Struct_flags.struct_flags)) (var_v: UInt3
requires
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
ensures
(with_pure
((id #int (UInt32.v (!(Struct_flags.struct_flags__get_a var_s)))) =
diff --git base/bitfields/Func_write_a.fsti head/bitfields/Func_write_a.fsti
index b73bba6..da2a65c 100644
--- base/bitfields/Func_write_a.fsti
+++ head/bitfields/Func_write_a.fsti
@@ -7,12 +7,12 @@ divergent fn func_write_a (var_s: (ref Struct_flags.struct_flags)) (var_v: UInt3
requires
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_flags.struct_flags).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_flags.struct_flags__pred (!var_s) 1.0R))
+ (Struct_flags.struct_flags__pred val_s_0 1.0R))
ensures
(with_pure
((id #int (UInt32.v (!(Struct_flags.struct_flags__get_a var_s)))) =
diff --git base/bitfields/Func_write_flag.fst head/bitfields/Func_write_flag.fst
index bd19896..1bba047 100644
--- base/bitfields/Func_write_flag.fst
+++ head/bitfields/Func_write_flag.fst
@@ -7,12 +7,12 @@ divergent fn func_write_flag (var_s: (ref Struct_bits.struct_bits)) (var_v: bool
requires
exists* (val_s_0: Struct_bits.struct_bits).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ (Struct_bits.struct_bits__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_bits.struct_bits).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ (Struct_bits.struct_bits__pred val_s_0 1.0R))
ensures (with_pure ((!(Struct_bits.struct_bits__get_flag var_s)) = var_v))
{
let mut var_s = var_s;
diff --git base/bitfields/Func_write_flag.fsti head/bitfields/Func_write_flag.fsti
index b621d8f..ffa6053 100644
--- base/bitfields/Func_write_flag.fsti
+++ head/bitfields/Func_write_flag.fsti
@@ -6,11 +6,9 @@ open Pulse.Lib.C
divergent fn func_write_flag (var_s: (ref Struct_bits.struct_bits)) (var_v: bool)
requires
exists* (val_s_0: Struct_bits.struct_bits).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_bits.struct_bits).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
ensures (with_pure ((!(Struct_bits.struct_bits__get_flag var_s)) = var_v))
\ No newline at end of file
diff --git base/bitfields/Func_write_nibble.fst head/bitfields/Func_write_nibble.fst
index 61bcea2..f158d2a 100644
--- base/bitfields/Func_write_nibble.fst
+++ head/bitfields/Func_write_nibble.fst
@@ -7,12 +7,12 @@ divergent fn func_write_nibble (var_s: (ref Struct_bits.struct_bits)) (var_v: UI
requires
exists* (val_s_0: Struct_bits.struct_bits).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ (Struct_bits.struct_bits__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_bits.struct_bits).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ (Struct_bits.struct_bits__pred val_s_0 1.0R))
ensures
(with_pure
((id #int (UInt8.v (!(Struct_bits.struct_bits__get_nibble var_s)))) =
diff --git base/bitfields/Func_write_nibble.fsti head/bitfields/Func_write_nibble.fsti
index c54541d..6d8f5ec 100644
--- base/bitfields/Func_write_nibble.fsti
+++ head/bitfields/Func_write_nibble.fsti
@@ -6,13 +6,11 @@ open Pulse.Lib.C
divergent fn func_write_nibble (var_s: (ref Struct_bits.struct_bits)) (var_v: UInt8.t)
requires
exists* (val_s_0: Struct_bits.struct_bits).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_bits.struct_bits).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_bits.struct_bits__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
ensures
(with_pure
((id #int (UInt8.v (!(Struct_bits.struct_bits__get_nibble var_s)))) =
diff --git base/bitfields/Func_write_tdef.fst head/bitfields/Func_write_tdef.fst
index 6bab42f..f9409f6 100644
--- base/bitfields/Func_write_tdef.fst
+++ head/bitfields/Func_write_tdef.fst
@@ -9,13 +9,13 @@ divergent fn func_write_tdef
requires
exists* (val_s_0: Struct_tdef.struct_tdef).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
requires ((Typedef_uint16_t.ty_uint16_t__pred var_v 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_tdef.struct_tdef).
((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
ensures ((Typedef_uint16_t.ty_uint16_t__pred var_v 1.0R))
ensures
(with_pure
diff --git base/bitfields/Func_write_tdef.fsti head/bitfields/Func_write_tdef.fsti
index 54cae02..c97a741 100644
--- base/bitfields/Func_write_tdef.fsti
+++ head/bitfields/Func_write_tdef.fsti
@@ -8,14 +8,12 @@ divergent fn func_write_tdef
(var_v: Typedef_uint16_t.ty_uint16_t)
requires
exists* (val_s_0: Struct_tdef.struct_tdef).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
requires ((Typedef_uint16_t.ty_uint16_t__pred var_v 1.0R))
returns return_1 : unit
ensures
exists* (val_s_0: Struct_tdef.struct_tdef).
- ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
- (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
+ ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
ensures ((Typedef_uint16_t.ty_uint16_t__pred var_v 1.0R))
ensures
(with_pure
diff --git base/container_of/Struct_packet_space.fst head/container_of/Struct_packet_space.fst
index 709a26b..a862c52 100644
--- base/container_of/Struct_packet_space.fst
+++ head/container_of/Struct_packet_space.fst
@@ -26,7 +26,7 @@ let predicate struct_packet_space__pred
(this).struct_packet_space__back
#p
val_packet_space_0.struct_packet_space__spec__back_0) **
- (Typedef_int32_t.ty_int32_t__pred (!(this).struct_packet_space__back) p))
+ (Typedef_int32_t.ty_int32_t__pred val_packet_space_0.struct_packet_space__spec__back_0 p))
[@@pulse_eager_unfold] let predicate struct_packet_space__uninit_pred
([@@@mkey] this: struct_packet_space) =
((Typedef_ack_tracker_t.ty_ack_tracker_t__uninit_pred (this).struct_packet_space__tracker) **
@@ -45,7 +45,7 @@ struct_packet_space__pred_unfold
(this).struct_packet_space__back
#p
val_packet_space_0.struct_packet_space__spec__back_0)
- ensures (Typedef_int32_t.ty_int32_t__pred (!(this).struct_packet_space__back) p)
+ ensures (Typedef_int32_t.ty_int32_t__pred val_packet_space_0.struct_packet_space__spec__back_0 p)
{
unfold struct_packet_space__pred this p val_packet_space_0
}
@@ -58,7 +58,7 @@ struct_packet_space__pred_fold
requires (Typedef_ack_tracker_t.ty_ack_tracker_t__pred (this).struct_packet_space__tracker p)
requires (Typedef_int32_t.ty_int32_t__pred (this).struct_packet_space__id p)
requires (Pulse.Lib.Reference.pts_to (this).struct_packet_space__back #p val_back_0)
- requires (Typedef_int32_t.ty_int32_t__pred (!(this).struct_packet_space__back) p)
+ requires (Typedef_int32_t.ty_int32_t__pred val_back_0 p)
ensures struct_packet_space__pred this p ({
struct_packet_space__spec__back_0 = val_back_0;
})
diff --git base/core_ref_chain/Struct_b.fst head/core_ref_chain/Struct_b.fst
index dd11a81..6f84e07 100644
--- base/core_ref_chain/Struct_b.fst
+++ head/core_ref_chain/Struct_b.fst
@@ -16,7 +16,7 @@ assume val struct_b__sizeof_pos (a: Type0 { a == struct_b }) :
}
let predicate struct_b__pred ([@@@mkey] this: struct_b) (p: perm) (val_b_0: struct_b__spec) =
((Pulse.Lib.Reference.pts_to (this).struct_b__pa #p val_b_0.struct_b__spec__pa_0) **
- (Struct_a.struct_a__pred (!(this).struct_b__pa) p))
+ (Struct_a.struct_a__pred val_b_0.struct_b__spec__pa_0 p))
[@@pulse_eager_unfold] let predicate struct_b__uninit_pred ([@@@mkey] this: struct_b) =
((Pulse.Lib.Reference.pts_to_uninit (this).struct_b__pa))
[@@pulse_intro]
@@ -27,7 +27,7 @@ struct_b__pred_unfold
(val_b_0: struct_b__spec)
requires struct_b__pred this p val_b_0
ensures (Pulse.Lib.Reference.pts_to (this).struct_b__pa #p val_b_0.struct_b__spec__pa_0)
- ensures (Struct_a.struct_a__pred (!(this).struct_b__pa) p)
+ ensures (Struct_a.struct_a__pred val_b_0.struct_b__spec__pa_0 p)
{
unfold struct_b__pred this p val_b_0
}
@@ -38,7 +38,7 @@ struct_b__pred_fold
(p: perm)
(val_pa_0: Struct_a.struct_a)
requires (Pulse.Lib.Reference.pts_to (this).struct_b__pa #p val_pa_0)
- requires (Struct_a.struct_a__pred (!(this).struct_b__pa) p)
+ requires (Struct_a.struct_a__pred val_pa_0 p)
ensures struct_b__pred this p ({
struct_b__spec__pa_0 = val_pa_0;
})
diff --git base/core_ref_chain/Typedef_a_owned.fst head/core_ref_chain/Typedef_a_owned.fst
index 4cd8dcc..62c0aa2 100644
--- base/core_ref_chain/Typedef_a_owned.fst
+++ head/core_ref_chain/Typedef_a_owned.fst
@@ -10,7 +10,7 @@ let ty_a_owned : Type = (ref Struct_a.struct_a)
(p: perm)
(val_this_0: Struct_a.struct_a) =
((Pulse.Lib.Reference.pts_to this #p val_this_0) **
- (Struct_a.struct_a__pred (!this) p) **
+ (Struct_a.struct_a__pred val_this_0 p) **
(exists* (bv: Struct_b.struct_b).
pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_b.struct_b
(((!this)).Struct_a.struct_a__pb)) bv))
diff --git base/core_ref_struct/Func_get_data.fst head/core_ref_struct/Func_get_data.fst
index 0e276eb..71393e8 100644
--- base/core_ref_struct/Func_get_data.fst
+++ head/core_ref_struct/Func_get_data.fst
@@ -7,12 +7,12 @@ divergent fn func_get_data (var_c: (ref Struct_child.struct_child))
requires
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
+ (Struct_child.struct_child__pred val_c_0 1.0R))
returns return_1 : Int32.t
ensures
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
+ (Struct_child.struct_child__pred val_c_0 1.0R))
{
let mut var_c = var_c;
return (!(Struct_child.struct_child__get_data (!var_c)));
diff --git base/core_ref_struct/Func_get_data.fsti head/core_ref_struct/Func_get_data.fsti
index e2e9e6f..b16f35a 100644
--- base/core_ref_struct/Func_get_data.fsti
+++ head/core_ref_struct/Func_get_data.fsti
@@ -7,9 +7,9 @@ divergent fn func_get_data (var_c: (ref Struct_child.struct_child))
requires
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
+ (Struct_child.struct_child__pred val_c_0 1.0R))
returns return_1 : Int32.t
ensures
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
\ No newline at end of file
+ (Struct_child.struct_child__pred val_c_0 1.0R))
\ No newline at end of file
diff --git base/core_ref_struct/Func_has_parent.fst head/core_ref_struct/Func_has_parent.fst
index 45f3aa9..3fb9356 100644
--- base/core_ref_struct/Func_has_parent.fst
+++ head/core_ref_struct/Func_has_parent.fst
@@ -7,12 +7,12 @@ divergent fn func_has_parent (var_c: (ref Struct_child.struct_child))
requires
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
+ (Struct_child.struct_child__pred val_c_0 1.0R))
returns return_1 : bool
ensures
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
+ (Struct_child.struct_child__pred val_c_0 1.0R))
{
let mut var_c = var_c;
return (not (Pulse.Lib.C.CoreRef.core_is_null (!(Struct_child.struct_child__get_up (!var_c)))));
diff --git base/core_ref_struct/Func_has_parent.fsti head/core_ref_struct/Func_has_parent.fsti
index 8aec117..34ff227 100644
--- base/core_ref_struct/Func_has_parent.fsti
+++ head/core_ref_struct/Func_has_parent.fsti
@@ -7,9 +7,9 @@ divergent fn func_has_parent (var_c: (ref Struct_child.struct_child))
requires
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
+ (Struct_child.struct_child__pred val_c_0 1.0R))
returns return_1 : bool
ensures
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
\ No newline at end of file
+ (Struct_child.struct_child__pred val_c_0 1.0R))
\ No newline at end of file
diff --git base/core_ref_struct/Func_set_data.fst head/core_ref_struct/Func_set_data.fst
index 1c0d2e5..6f3cd33 100644
--- base/core_ref_struct/Func_set_data.fst
+++ head/core_ref_struct/Func_set_data.fst
@@ -7,12 +7,12 @@ divergent fn func_set_data (var_c: (ref Struct_child.struct_child)) (var_v: Int3
requires
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
+ (Struct_child.struct_child__pred val_c_0 1.0R))
returns return_1 : unit
ensures
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
+ (Struct_child.struct_child__pred val_c_0 1.0R))
{
let mut var_c = var_c;
let mut var_v = var_v;
diff --git base/core_ref_struct/Func_set_data.fsti head/core_ref_struct/Func_set_data.fsti
index 5646f81..8ac597e 100644
--- base/core_ref_struct/Func_set_data.fsti
+++ head/core_ref_struct/Func_set_data.fsti
@@ -7,9 +7,9 @@ divergent fn func_set_data (var_c: (ref Struct_child.struct_child)) (var_v: Int3
requires
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
+ (Struct_child.struct_child__pred val_c_0 1.0R))
returns return_1 : unit
ensures
exists* (val_c_0: Struct_child.struct_child).
((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
- (Struct_child.struct_child__pred (!var_c) 1.0R))
\ No newline at end of file
+ (Struct_child.struct_child__pred val_c_0 1.0R))
\ No newline at end of file
diff --git base/core_ref_struct/Struct_parent.fst head/core_ref_struct/Struct_parent.fst
index a825e3f..4c5b50e 100644
--- base/core_ref_struct/Struct_parent.fst
+++ head/core_ref_struct/Struct_parent.fst
@@ -22,7 +22,7 @@ let predicate struct_parent__pred
(this).struct_parent__down
#p
val_parent_0.struct_parent__spec__down_0) **
- (Struct_child.struct_child__pred (!(this).struct_parent__down) p))
+ (Struct_child.struct_child__pred val_parent_0.struct_parent__spec__down_0 p))
[@@pulse_eager_unfold] let predicate struct_parent__uninit_pred ([@@@mkey] this: struct_parent) =
((Pulse.Lib.Reference.pts_to_uninit (this).struct_parent__down))
[@@pulse_intro]
@@ -36,7 +36,7 @@ struct_parent__pred_unfold
(this).struct_parent__down
#p
val_parent_0.struct_parent__spec__down_0)
- ensures (Struct_child.struct_child__pred (!(this).struct_parent__down) p)
+ ensures (Struct_child.struct_child__pred val_parent_0.struct_parent__spec__down_0 p)
{
unfold struct_parent__pred this p val_parent_0
}
@@ -47,7 +47,7 @@ struct_parent__pred_fold
(p: perm)
(val_down_0: Struct_child.struct_child)
requires (Pulse.Lib.Reference.pts_to (this).struct_parent__down #p val_down_0)
- requires (Struct_child.struct_child__pred (!(this).struct_parent__down) p)
+ requires (Struct_child.struct_child__pred val_down_0 p)
ensures struct_parent__pred this p ({
struct_parent__spec__down_0 = val_down_0;
})
diff --git base/core_ref_use/Func_store.fst head/core_ref_use/Func_store.fst
index 41eeb79..55bf01b 100644
--- base/core_ref_use/Func_store.fst
+++ head/core_ref_use/Func_store.fst
@@ -7,12 +7,12 @@ divergent fn func_store (var_b: (ref Struct_bar.struct_bar))
requires
exists* (val_b_0: Struct_bar.struct_bar) (val_b_1: Struct_bar.struct_bar__spec).
((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
- (Struct_bar.struct_bar__pred (!var_b) 1.0R val_b_1))
+ (Struct_bar.struct_bar__pred val_b_0 1.0R val_b_1))
returns return_1 : unit
ensures
exists* (val_b_0: Struct_bar.struct_bar) (val_b_1: Struct_bar.struct_bar__spec).
((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
- (Struct_bar.struct_bar__pred (!var_b) 1.0R val_b_1))
+ (Struct_bar.struct_bar__pred val_b_0 1.0R val_b_1))
{
let mut var_b = var_b;
let mut var_c : core_ref;
diff --git base/core_ref_use/Func_store.fsti head/core_ref_use/Func_store.fsti
index 4879ddf..3fe949b 100644
--- base/core_ref_use/Func_store.fsti
+++ head/core_ref_use/Func_store.fsti
@@ -7,9 +7,9 @@ divergent fn func_store (var_b: (ref Struct_bar.struct_bar))
requires
exists* (val_b_0: Struct_bar.struct_bar) (val_b_1: Struct_bar.struct_bar__spec).
((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
- (Struct_bar.struct_bar__pred (!var_b) 1.0R val_b_1))
+ (Struct_bar.struct_bar__pred val_b_0 1.0R val_b_1))
returns return_1 : unit
ensures
exists* (val_b_0: Struct_bar.struct_bar) (val_b_1: Struct_bar.struct_bar__spec).
((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
- (Struct_bar.struct_bar__pred (!var_b) 1.0R val_b_1))
\ No newline at end of file
+ (Struct_bar.struct_bar__pred val_b_0 1.0R val_b_1))
\ No newline at end of file
diff --git base/core_ref_use/Func_via_back.fst head/core_ref_use/Func_via_back.fst
index 7942298..ad92041 100644
--- base/core_ref_use/Func_via_back.fst
+++ head/core_ref_use/Func_via_back.fst
@@ -7,7 +7,7 @@ divergent fn func_via_back (var_p: (ref Struct_inner.struct_inner))
requires
exists* (val_p_0: Struct_inner.struct_inner) (val_p_1: Struct_inner.struct_inner__spec).
((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
- (Struct_inner.struct_inner__pred (!var_p) 1.0R val_p_1))
+ (Struct_inner.struct_inner__pred val_p_0 1.0R val_p_1))
requires
(exists* (bv: Struct_bar.struct_bar).
pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_bar.struct_bar
@@ -16,7 +16,7 @@ pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_bar.struct_bar
ensures
exists* (val_p_0: Struct_inner.struct_inner) (val_p_1: Struct_inner.struct_inner__spec).
((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
- (Struct_inner.struct_inner__pred (!var_p) 1.0R val_p_1))
Diff truncated; see the links above for the full version. |
gebner
reviewed
Aug 28, 2026
| /// binding: in a function-pointer wrapper the whole `requires` sits under | ||
| /// the witness's pattern `match`, where Pulse will not elaborate `!p`. | ||
| pointees: &'a [(Rc<IdentT>, Rc<str>)], | ||
| } |
Contributor
There was a problem hiding this comment.
Is this related to the !var_a -> val_a_0 changes I've seen in the diff? This is not good, it might work for pointers but not in general. Are impure specs broken somehow?
Contributor
Author
|
Closing this PR for now. Modifying Fstar first |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Three related gaps in what a function pointer's
__fpwrapper could express.They are separate features but share one root cause, described at the bottom.
What's new
_ghost_argon function pointers. A function whose contract used a ghostargument could not have its address taken: the wrapper gave the ghost no
binder, so its name was free and, being unregistered, was lowered as a
C-variable read (
!var_v). The witness widens from the elim tuple alone to(elims & ghosts); the wrapper projects ghost bindings out of the secondcomponent and a call site emits
hide (elims, (_, .., _)).The
structfield must repeat the_ghost_args, soghost_argsis nowcarried on
TypeT::FnPtras well as onFnDecl: an indirect call has nocallee declaration, and its only information is the static type it calls
through. It is not part of the pointer's F* type and
vtype_eqignores it,so annotations are needed where you call, never where you assign. The
(elims & ghosts)pair is introduced only when ghosts exist — pairingunconditionally would give every ordinary function pointer an unconstrained
unitslot that a call site could fill only by writing()literally.Correct witness arity for structs with a
__speccompanion. The calleecounted witness components per binding and the call site per argument.
Those agree until the pointee struct has a pointer field, at which point the
struct contributes both its value and its
__spec, and the call site droppedone. The failure surfaced as an ownership goal rather than an arity error, so
it read as a missing permission.
Array
_lengthrefinements through a function pointer. A struct-level_refinereading an_arrayfield's_lengthwas fatal to the wrapper of anyaddress-taken function (
Error 54, orError 230with a single refinement)._lengthon such a field is now emitted asarray_spec_lenof thepredicate's spec record instead of a
length_ofcall.Issues
Closes #277.
Not fixed here: #279 (wrappers dropping pointee postconditions) is a separate
branch and should land after this one.
Why the
match, and why all the bookkeepingThe wrapper destructures its witness with a pattern
let, which desugars to amatch. That is not a stylistic choice.A pattern binds each leaf as a plain variable, so a caller's goal
pts_to x val_aunifies directly and solves it. Read the same leaf withfst/sndand the goal becomespts_to x (fst ?w)— not invertible, so thewitness metavariable never solves and every indirect call fails with
Error 228 ... Unexpected unresolved uvars in the term: 'call ()'. Measuredboth on minimal oracles and on real PAL output. For the same reason the witness
spine is written out rather than left as one hole: Pulse solves a hole standing
for a tuple leaf, never one standing for a whole tuple, since
snd (reveal ?u)is inert until
?uis a realMktuple2.The price is that the entire
requiresthen sits inside a match branch, andPulse's frontend rewrites do not traverse one. So anything in a spec that
depends on such a rewrite has to be resolved by PAL before emission. That
single fact is what produced the three pieces of bookkeeping in this PR, which
otherwise look unrelated:
SpecSubst::pointees!p, which needs to see the ambientpts_to; the binding is named directly insteadpure_not_with_purewith_pure's continuation, which is never supplied inside a match, leaving a partially-appliedwith_pure pthat is not anslpropspec_scopelength_of, aghost fnanswering throughrewrites_to; replaced by the pure projectionarray_spec_lenEach is the same move: pre-compute in PAL what Pulse would otherwise derive in
context. It is worth noting how far the symptoms diverge from that common
cause — a dropped witness component reports as missing ownership, and the
length_ofcase reports asFatal_ErrorInSolveDeferredConstraints, with theerror number changing (54 versus 230) purely with the number of refinements.
Nested projection out of the widened witness relies on FStarLang/FStar#4492,
which is in the pinned nightly.
Follow-up
The principled fix for the third item is to fold struct-level
_refines intothe struct's own
__pred, rather than leaving them as siblingpureconjuncts at each use site — which is exactly why a typedef-level array
refine never had this bug. That relocates every struct refinement in the tree,
so it is left for its own change.
Tests
test/ghost_fnptr/covers one ghost, two ghosts, a mixed case with two ownedpointers and two ghosts (witness nested on both sides), a no-ghost control,
calls through a global
struct ops, and a call through a local functionpointer. It also exercises a field-level
_refinecarrying a deliberatelyweaker
is_valid, reached viaFuncPtr.weaken, so a returnedstruct ops *hands out a callable
mwith noof_fn_div_validat the call site.test/fnptr_spec/adds the__spec-companion call sites and the array-lengthrefinement, by pointer and by value. The by-value form is the sharper of the
two: with no
pts_toto eliminate, its refinement conjuncts mention only theplain parameter and no witness binding at all, and were still rejected — the
constraint is where a term sits, not what it names.
The array-length commit is split red-then-green so the before/after is visible
in history.