Let a function-pointer spec talk about a pointee - #280
Closed
hei411 wants to merge 11 commits into
Closed
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
The `__fp` wrapper owns each pointer argument's existential in the witness `c = (ELIMS & GHOSTS)`, whose elim half holds the *pre-state* pointee values. It has no way to name those values where it needs them, and the damage lands on both sides of the arrow -- #279 records only one of them. `ensures`, as filed in #279: the wrapper states its pure postcondition as `PRE ==> POST`, reusing the very doc it emitted for the `requires`. In the `ensures` that copy is captured by a fresh `exists* (val_p_0: ..)` holding the *post* value, so for a callee that mutates a pointee it mentions, the implication is a tautology and carries nothing. `_old`, and not as #279 describes it: the issue reports the wrapper silently accepting even a false `_old` contract. That has stopped being true. `old (!var_p)` sends Pulse looking for the pre-state `pts_to`, which lives under the witness's pattern `let`, and Pulse will not elaborate `!` into a match branch -- so it is a hard Error 228, not a silent one. `requires`, which #279 does not mention at all: only the innermost `*p` is rewritten to a witness binding, so `**p` comes out as `!val_p_0`, a `!` under that same pattern `let`, staying a Pulse `fn` instead of a value (Error 12). The precondition of any double-pointer function pointer is unusable. `**p` in a normal function's spec has always worked; this is specific to the fnptr path. Four cases, all failing, each with the error it produces: call_indirect_norel Error 19 the guard alone loses the post; nothing relational and no `_old` is needed call_indirect_old Error 228 `_old` across an indirect call call_mixed Error 228 two mutated pointees at elim offsets 2 and 3, behind a `struct dep *`, with `_plain` and `_ghost_arg` in the mix, reached through an `is_valid`-refined field on a const global call_indirect_deep Error 12 `int32_t **p`, both sides + Error 228 `call_mixed` is the one that pins the offset arithmetic: its body updates `*b` before `*a` and its contract is `*b == _old(*b) + _old(*a)`, so a shared or mis-indexed binding gives a wrong answer rather than a vacuous one. The direct callees all verify -- `Func_inc`, `Func_bump` and friends are true of their bodies and propagate fine through a direct call. Only the indirect path is broken. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
One root cause behind all three symptoms of #279 and its neighbours: the `__fp` wrapper's `ensures` has no name for the pre-state pointee value. It does have the witness -- `y_fp: erased c` is a wrapper *parameter*, in scope in the post, and its elim half is exactly that value. Pointee bindings are now keyed by deref *depth* rather than assuming a single level, so `*p` and `**p` are distinct and `**p` resolves to the witness leaf the wrapper already carried instead of being emitted as `!val_p_0`. That alone fixes the `requires` side (Error 12). Registration is bounded by the argument's pointer depth, so a `struct S *`'s second binding -- its `__spec`, not `**s` -- is never mistaken for a pointee. `_old(*p)` no longer emits `old (...)` at all. It resolves to a projection out of `fst (reveal y_fp)` at that argument's elim offset, which *is* the pre-state value, so there is nothing left to read through the pointer. Offsets are accumulated per argument, so a `struct S *` contributing two leaves or a `_plain` parameter contributing none does not misalign the ones after it. The antecedent of `PRE ==> POST` is rebuilt over those `old_` names rather than reusing the `requires` doc, which is what removes the capture by the post's own `exists*`. It is built lazily, only where there is a pure `ensures` to guard, so a wrapper with nothing to say emits nothing new. A bare deref in the `ensures` is left alone -- it must read the post state, and already elaborates inside the `exists*`. The `old_` bindings are emitted by projection, not by pattern: a pattern would break `!` auto-deref inside the post's `exists*` groups. The body's existing `witness_rewrites` eta-expansion reconciles that with the pattern form the `requires` uses, which is the same mechanism the ghost half already relies on. One trap worth recording: `ExprT::SpecVal`'s second field must be the *pointer*, not the value. `Env::infer_expr` types it by dereferencing that field, so passing the value makes inference fail with `CannotDeref` and silently drop the enclosing cast's coercion -- `old_val_p_0 + 1` instead of `v old_val_p_0 + 1`, with no error reported. `test/fnptr_pointee_spec` goes from four failing modules to none, and its comments are rewritten from a bug report into a record of what each case exercises and what it used to produce. Generated `.fst`/`.fsti` were diffed tree-wide against a build of the parent commit: only those four modules differ, so no existing wrapper's spec changed shape. Fixes #279. 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_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))
+ (Struct_inner.struct_inner__pred val_p_0 1.0R val_p_1))
ensures
(exists* (bv: Struct_bar.struct_bar).
pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_bar.struct_bar
diff --git base/core_ref_use/Func_via_back.fsti head/core_ref_use/Func_via_back.fsti
index fdfb719..5995994 100644
--- base/core_ref_use/Func_via_back.fsti
+++ head/core_ref_use/Func_via_back.fsti
@@ -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).
Diff truncated; see the links above for the full version. |
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
1 participant
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.
pointers*) and its base is that branch, not
main. #275 is what makes thewitness
y_fp: erased can explicit wrapper parameter, and that parameter isthe thing this PR reads pre-state values out of — so reviewing or merging this
against
mainwill not make sense. Once #275 lands this retargets tomaincleanly.
Closes #279.
What was wrong
A
__fpwrapper owns each pointer argument's existential in the witnessc = (ELIMS & GHOSTS), whose elim half holds the pre-state pointee values.It had no way to name those values where it needed them, and the damage landed
on both sides of the arrow. #279 records one of the three symptoms.
ensures— as filed. The wrapper states its pure postcondition asPRE ==> POST, reusing the very doc it emitted for therequires. In theensuresthat copy is captured by a freshexists* (val_p_0: ..)holding thepost value, so for any callee that mutates a pointee it mentions the implication
is a tautology:
_old— but not as #279 describes it. The issue reports the wrappersilently accepting even a false
_oldcontract. That had already stopped beingtrue:
old (!var_p)sends Pulse looking for the pre-statepts_to, which livesunder the witness's pattern
let, and Pulse will not elaborate!into a matchbranch. So it was a hard
Error 228—_oldon an address-taken function didnot typecheck at all, rather than typechecking vacuously.
requires— which #279 does not mention. Only the innermost*pwasrewritten to a witness binding, so
**pcame out as!val_p_0: a!underthat same pattern
let, staying a Pulsefninstead of a value (Error 12).The precondition of any double-pointer function pointer was unusable. Worth
noting that
**pin a normal function's spec has always worked — this wasspecific to the fnptr path.
The fix
One root cause, so one change: give the
ensuresa name for the pre-statevalue.
y_fpis a wrapper parameter, so it is already in scope there.so
*pand**pare distinct and**presolves to the witness leaf thewrapper already carried. This alone fixes the
requires. Registration isbounded by the argument's pointer depth, so a
struct S *'s second binding —its
__spec, not**s— is never mistaken for a pointee._old(*p)no longer emitsold (...). It resolves to a projection out offst (reveal y_fp)at that argument's elim offset, which is the pre-statevalue, so there is nothing left to read through the pointer.
PRE ==> POSTis rebuilt over thoseold_names ratherthan reusing the
requiresdoc, which removes the capture. It is builtlazily, only where there is a pure
ensuresto guard, so a wrapper withnothing to say emits nothing new.
struct S *contributing two leaves ora
_plainparameter contributing none does not misalign what follows.The
old_bindings are emitted by projection, not by pattern — a patternwould break
!auto-deref inside the post'sexists*groups. The body'sexisting
witness_rewriteseta-expansion reconciles that with the pattern formthe
requiresuses, which is the same mechanism the ghost half already relieson.
Test
test/fnptr_pointee_spec/, committed red in the first commit so thebefore/after is visible in the history. Four cases:
call_indirect_norelError 19— the guard alone loses the post; nothing relational and no_oldneededcall_indirect_oldError 228—_oldacross an indirect callcall_mixedError 228— two mutated pointees at elim offsets 2 and 3, behind astruct dep *, with_plainand_ghost_argin the mix, reached through anis_valid-refined field on aconstglobalcall_indirect_deepError 12+Error 228—int32_t **p, both sidescall_mixedis the one that pins the offset arithmetic: its body updates*bbefore
*aand its contract is*b == _old(*b) + _old(*a), so a shared ormis-indexed binding gives a wrong answer rather than a vacuous one.
Blast radius
Generated
.fst/.fstiwere diffed tree-wide against a build of the parentcommit: only the four new modules differ.
func_pointer,ghost_fnptrandfnptr_specare byte-identical, so no existing wrapper's spec changed shape.Full suite green.