diff --git a/CHANGELOG.md b/CHANGELOG.md index 33ec50729..35c519088 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -75,6 +75,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). - **A burndown driven to zero can say so** — `scripts/check_doc_counts.py` tested KNOWN_ISSUES.md's documented `No known bugs.` form by exact match against the whole `## Bugs` section, so the section's standing description read as content and a correctly-written empty table reported "the `## Bugs` table was not found" — the error message prescribing the very form it had just rejected. ROADMAP.md's burndown table had no empty form at all. Both now recognise the marker beside the description (`No open bugs.` for the burndown), so the fix that closes the last bug in a queue can satisfy the gate that checks it; a table emptied WITHOUT the marker is still unreadable, and the header word is still checked against the rows. +- **A disclosed fact's taint follows the value, not the spelling of the call** ([#1406](https://github.com/aallan/vera/issues/1406), [#1407](https://github.com/aallan/vera/issues/1407)). [#1363](https://github.com/aallan/vera/issues/1363) established that a declared-type fact this run disclosed — reported as neither proved nor guarded — must not discharge a downstream goal at Tier 1, and asked a syntactic question to find it: is this `match` scrutinee spelled as a call to a disclosed function. A syntactic question has as many answers as there are spellings, and two of them defeated the rule outright, both measured pre-existing on `release/v0.2.0` with a runtime differential rather than a status difference. Binding the call first — `let @Option = mk(x); match @Option.0 { … }` — makes the scrutinee a slot reference, so the facts were handed to the solver at full strength and the caller's postcondition was `verified` while `vera run` refuted it; one token, and the rule was gone. A forwarding wrapper — `fn wrap(…) { mk(x) }`, then `match wrap(x)` — makes no claim that needs the disclosed fact, so it contributes no obligation, so `disclosed_fn_names`, which reads the obligation stream, never saw it at any depth. Disclosure is now a property of the value: a disclosed call's fresh result term is recorded where it is minted, and the fact gate asks whether the value in hand carries one — by occurrence, so a projection out of a disclosed value, a branch that discloses on one arm, and a value taken apart and REBUILT from a disclosed component all answer yes, mirroring the `ite` recursion `_is_locally_constructed` already uses for the same reason. Asking by occurrence rather than by shape is what makes the construction case need no rule of its own: the disclosed term is still inside the constructor's argument, so the walk finds it, and truncating the walk to the root term reds the rebuild cells along with the projection and join ones. The wrapper half feeds the existing `_rerun_until_disclosure_settles` fixpoint: a function whose body result is a disclosed value joins the disclosed set, so the taint travels one hop per pass and terminates for the reason the fixpoint already terminates. Nothing in the fix names a spelling, which is why the `let` chain, the pipe, the `where` helper and the branch join move with the two reported shapes rather than needing cases of their own. The warm session carries the wrapper answer in its per-function cache entry (`FnCacheEntry.result_disclosed`): a replayed slice re-runs no body, so an uncached forwarder would drop out of the disclosed set and the warm run would prove at Tier 1 exactly what the cold run demotes — the generous direction, and the one that matters. Ten caller spellings are pinned against their clean controls, which must and do stay `verified`; the corpus differential moves nothing, which the reachability count explains rather than excuses — exactly one corpus program discloses at all — `tests/probes/state_handlers/clause_scoping/p4_refined_arg_clause.vera`, one `refine_bind`, with nothing downstream reading the fact — so a selectivity cell supplies the completeness measurement the corpus cannot. Asking the complementary question — not which spelling reaches the gated reader, but how many readers there are — turned up two more, both `verified` at Tier 1 over a value the program then hands back unguarded ([#1413](https://github.com/aallan/vera/issues/1413)): the premise that lets a projected value re-narrow into a second refinement (`Some(@Big)` over a `PosInt` payload), and the component fact a `let`-destructure seeds for a source it treats as guaranteed — a category whose own comment reads "a call: its callee discharged the return type", which is exactly the premise disclosure withdraws. Both take the same treatment, and the demotion path they then follow already existed: `_undecided_reason` has handled a `disclosed` status since #1363 and had simply never been reached from either site. All three readers now ask ONE function — `_established_facts`, which returns the facts the run established and parks the rest in the tainted set — rather than three call sites that happen to agree. #1363's rule and its gate were both right; what let two false Tier-1s outlive it is that the rule lived at one of three sites by convention, so a structural cell now walks the module's own AST and requires that any function reading a source fact consults that gate, making a fourth reader a call to it or a failing test. Their carrier is chosen the same way and for a sharper reason — a refined tuple component IS guarded at the producer's return, so the destructure is only a false Tier-1 CLAIM until the tuple is reached through an ADT payload, at which point `-7` comes back for a value declared `> -3`. Across an import the two mechanisms compose rather than overlap: [#1399](https://github.com/aallan/vera/issues/1399) gives the importer a disclosed set at all and this makes it survive the spellings, so where the direct call alone demoted before, the `let`-bound and wrapper-forwarded ones now do too. The citation composes with them. #1399 names the culprit module by recording the site as it consults the manifest — at the place the fact is withheld — and both new spellings withhold somewhere that consult has long since happened, a `let`-bound value being a slot reference and a forwarder a local call, so the site is carried ON the value instead and across the forwarder hop with it. Without that the two spellings would have demoted with the generic text, re-opening the finding #1399 closed for the direct one. A FOURTH reader of a declared-type source fact was found bypassing the gate, and is routed through it. [#1420](https://github.com/aallan/vera/pull/1420) obligates a call ARGUMENT for the refinements nested inside its parameter's type, and the premise it discharges from is the argument's own declared type — which that site decided about for itself, asking a syntactic question of the value's producing leaves. So a `let`-bound disclosed producer arrived as a slot reference, answered False, and its declared type was granted: measured, the same value gave that obligation `tier3_unguarded` spelled `consume(mk(x))` and **`verified`** spelled `let @T = mk(x); consume(@T.0)`, a Tier-1 claim resting on a fact the same run reported as neither proved nor guarded. That is #1406's bug in a reader added after #1406 was fixed, which is the case the structural cell exists to prevent — and it missed because its producer roster named the two producers of the day rather than the kind. The roster now names this one too, so the walk reds on the bypass, and the behaviour is pinned by both spellings of one value with their clean controls. The local syntactic test is gone rather than left beside the gate. Also corrects a spec sentence that claimed more than the implementation does: a projected re-narrowing and a `let`-destructure's component invariant are Tier 3 when the goal DEPENDS on a withheld fact, not whenever the value they read was disclosed — withheld facts are offered back only after a proof without them fails, so a goal that never needed one keeps its Tier 1, which is now a cell. Rebasing over #1412 moved three things under this PR's cells, each repaired toward the claim rather than the encoding. The runtime exhibit changed site: an ADT payload used to be guarded nowhere, so the bad value reached the consumer's postcondition and refuted it, and #1412 now checks the narrowing where it obligates it, so the constructor sub-pattern guard refuses the program first — seven cells named only the older site, and now assert the REFUSAL at whichever guard reaches it, through one helper so the four sites cannot drift apart again. The two #1413 readers moved from `tier3_unguarded` to `tier3` for the same reason, their narrowings now being guarded; the cells asserted that exact pair when their claim is that the narrowing is not a Tier-1 proof, so they assert that instead — and the gate is still what produces it, measured, since reverting the gate takes both back to `verified`. And the lost-value-behind-a-forwarder cell loses its `Option` carrier, `@Nat` payload narrowings now being guarded and disclosing nothing: it returns to `Option` laundered through an array, where the stand-in's inheritance is still load-bearing. Two cells were found measuring nothing and re-carriered, which is a test change but the reason is a real one about the base: after [#1420](https://github.com/aallan/vera/pull/1420) and [#1435](https://github.com/aallan/vera/pull/1435) a refined RETURN is obligated at every position that publishes it, so an `Option` FORWARDER now carries its own `tier3_unguarded` — which reaches a caller through the obligation-derived set directly and leaves the mechanism the cell was written for doing nothing. Measured rather than inferred: the cross-module forwarder cells passed on `d88bf490` with the manifest union reverted, and the stand-in mint reddened two of the three lost-value cells instead of three. Both move to `Option`, whose narrowing is obligated at the construction site only, so the library's standalone run carries exactly one unguarded obligation and its forwarders record nothing; the forwarder-plus-lost-value cell additionally launders through an ARRAY rather than a tuple, a tuple of `Option` being translated rather than lost (`_fresh_opaque_slot` reached zero times), which would have swapped a mint test for a nothing-test. Each cell now asserts its own premise — the forwarders' obligations carry nothing disclosing — so the next base move that changes this fails loudly instead of passing quietly. The `@Nat` carrier trades the runtime refutation for a guard trap, codegen emitting the `>= 0` check (#1268), so the postcondition refutation stays on the in-module `Option` cells where an ADT payload is guarded nowhere. The construction case arrived from the review of [#1431](https://github.com/aallan/vera/pull/1431) and needed no extension, which was measured on four trees rather than argued: the reviewer's literal spelling (a `None` arm beside a `Some()` one) dies with an E699 sort mismatch on this base and on this branch alone — that crash being [#1424](https://github.com/aallan/vera/issues/1424), this exact shape, which [#1431](https://github.com/aallan/vera/pull/1431) fixes along with its cross-module twin [#1421](https://github.com/aallan/vera/issues/1421) — is `verified` while the run refutes it with that sort fix alone, and is `tier3`/E534 with both — so the sort fix decides whether the term can be BUILT and this decides which facts may discharge a goal over it. Carriers that translate on both revisions — a rebuild whose arms both construct, and a single-constructor ADT whose rebuild has no arm join at all — carry the same shape as ordinary cells here, with the pre-existing Tier-1 proof and the runtime refutation both measured. Adversarial review turned up three more, all fixed here. A value the SMT layer LOSES — a `let` whose RHS it cannot translate, an array literal whose elements it relates only by axiom — was replaced by a fresh stand-in whose provenance was severed, while every reader still took the payload refinement off the binding's declared type: `Tuple(mk(x), 1)` destructured back out proved at Tier 1 over a value the program refutes, and so did `[mk(x)]` indexed back out. Carrier-dependent, which is what hid it — the same spelling over a payload that translates demotes correctly — so the repair is at the MINT rather than at any reader: a stand-in inherits the disclosure of the expression it replaces, which also covers the next kind of stand-in without anyone widening a list. Second, the warm session cached a bool about the top-level name, so a `where` helper that forwards a disclosed value — added to the set while its PARENT's slice was verified, never a declaration in the session's own loop — was dropped and the warm fixpoint settled one hop early, proving at Tier 1 exactly what cold demoted on one of the ten spellings; the slice now caches its whole contribution rather than a fact about its name. Third, keying that set by bare name let one top-level function's tainted helper demote another's clean caller, a completeness loss this change had introduced by extending the set to forwarders; helper entries are now keyed by the owning scope, from the same `(decl, enclosing)` the visibility set is built from. Rebasing over [#1420](https://github.com/aallan/vera/pull/1420) turned the F3 cell red and exposed the SAME keying defect in the other half of the union. The disclosed set is read as the union of an obligation-derived derivation and a result-derived one; F3 scoped the second, and the first went on keying a `where` helper by its bare `fn_name` — a name that means a different function in every owner — so one owner's disclosing helper demoted another owner's clean caller. The attribution is measured rather than assumed: the isolated shape, two same-named helpers each disclosing through an obligation of its OWN with no forwarding anywhere, reports both callers `tier3`/E534 on `release/v0.2.0` BEFORE #1420 as well as after, so the defect was latent in that half from the start and reachable whenever a helper carried a disclosing obligation; what #1420 changed is the reach, by obligating a helper's return so that a merely FORWARDING helper carries one too. Both halves now spell a helper's key through one function, since a set consulted as a union cannot have two spellings for a member, and the obligation carries the top-level owner that key needs. Two cells rather than one, because the forwarding cell goes green again if only the result-derived half is scoped and the isolated one does not. The owner is stamped for whichever scope records the obligation, a guard comparing it against the recording function's own name having been written and then removed: all 73 call sites pass the declaration under verification, and an instrumented run over 919 cells and 251 example and conformance programs never reached a case where the two differed. A second adversarial round found the rule stopping at the import door. [#1399](https://github.com/aallan/vera/issues/1399)'s manifest — what an importer asks about a module it does not verify — was built from the obligation stream alone, so a FORWARDER inside the library recorded nothing and was invisible, while the same declarations in one file demoted correctly. The manifest now emits the UNION of that set with the result-derived one, which is simply the value-following rule reaching the import boundary: `_result_disclosed_fns` is populated from `term_is_disclosed` over a function's own result term, so it asks by OCCURRENCE and never by carrier. That union was removed mid-review and then restored, and the reason it had to come back is worth recording. The removal argued a dichotomy — after [#1412](https://github.com/aallan/vera/pull/1412) a forwarder either publishes the refinement, and is obligated for it, or drops it and hands on no fact — and surveyed six carriers, none of which contradicted it. The second half holds; the first is false. #1412 obligates NARROWINGS, and a forwarder whose declared return is the same refined type as its callee's narrows nothing, so it carries no obligation and the obligation-derived half cannot see it. A carrier survey could not have shown that, being evidence only about the carriers surveyed; the shape that shows it is a handler-clause `@Nat` payload narrowing — a handler declared `Exn` whose clause pattern `throw(@Nat)` narrows the `@Int` payload — which is #1362's category and outside #1412's guards. Measured with the manifest publishing the obligation-derived set alone: the direct call `tier3`/E534, through the library's forwarder **`verified`**, two import hops **`verified`**, and the same three declarations in ONE file `tier3`/E534. The exhibit is that asymmetry rather than a runtime refutation — `int_to_nat` filters the negative into `None`, so the program keeps its postcondition — and what is wrong is a Tier-1 claim resting on a fact the same run reported as neither proved nor guarded. The cells assert EQUALITY with the one-file oracle rather than a literal status, so a change that moves both sides together is a rule adjustment and not a failure, and a change that moves only one is caught. Two shapes found while measuring are NOT fixed here and are tracked as [#1410](https://github.com/aallan/vera/issues/1410), fixed by [#1420](https://github.com/aallan/vera/pull/1420) (merged into the release branch), and [#1424](https://github.com/aallan/vera/issues/1424), fixed by [#1431](https://github.com/aallan/vera/pull/1431); the first of those is the argument position — a disclosed value passed as an argument satisfies a refined parameter with no obligation anywhere, which is the callee's own proof and so out of reach of any taint in the caller; it measures identically before and after this change, for every spelling, and is pinned in that state. A third, two same-named `where` helpers accepted at check and refused by wasm-tools at compile, is [#1433](https://github.com/aallan/vera/issues/1433). - **A type variable reached only through a parameter's type arguments is inferred, not guessed** ([#1395](https://github.com/aallan/vera/issues/1395)). Unification binds a generic's type variables by two routes, and only one of them had been repaired. A variable a parameter names DIRECTLY (`@T`) is bound from the argument's own type name, which since [#1327](https://github.com/aallan/vera/issues/1327) comes from the checker when neither walker can produce one. A variable reached through a parameter's TYPE ARGUMENTS (`@Array`) is bound by `_get_arg_type_info` instead — and that helper carries exactly the same missing arms the type namers did, with none for an indexed argument and none for a nested module call. So `T` stayed unbound on both sides, both fell to the phantom-variable `Bool` default, and — because they agreed — nothing dangled and no diagnostic fired anywhere. `fn head(@Array -> @T)` called on `@Array>.0[0]` was `vera check`-green and `vera verify --json`-clean (`ok: true`, 6 Tier 1 + 1 Tier 3) and emitted `(func $head$Bool ... (result i32))` for a `T` that is `Int`: **invalid WebAssembly**, refused by wasmtime at load. Most shapes hid it, which is why it outlived its siblings — `takes_arr(@Array>.0[0])` on a generic returning `@Int` runs correctly at `Bool`, because `array_length` never reads `T` and an array is a pointer pair whatever its element type is. It takes a generic that RETURNS at `T` for the guess to become a width mismatch. The helper now falls back to the checker's structural answer, exactly as the namers do — and, exactly as they do, only where the walkers left a genuine hole. The consultation runs as a SECOND pass over the arguments, entered only when some variable is still unbound, so it can never displace a binding the walkers made: the checker's answer is a semantic type and the walkers' is a clone-naming vocabulary, and where the two spell the same instantiation differently the emitted symbol must use the walkers'. That ordering is load-bearing, not defensive — consulting in the first pass on BOTH sides makes five corpus programs emit `$option_unwrap_or$Nat` where the second-pass form emits `$Int`, the checker's `Option` for the first argument displacing the `Int` the second parameter's literal supplies. A one-sided mutation shows nothing, because both consultors then move together and agree on the wrong name. Measured across the corpus, no conformance program or example changes its check, verify or compile outcome, its diagnostic set or any obligation, and exactly one changes its emitted WAT: `ch09_prelude` renames one call from `result_unwrap_or$Int_JBool` to `$Int_JString`, which is the checker naming an error type the walkers could not. A variable nothing determines — `E` in `result_map(Ok(100), f)`, whose error position the checker itself leaves free — still takes the documented default, because the distinction drawn here is not phantom versus real but un-nameable versus nameable, which is the distinction `E622` draws. - **The remedy `E155` prescribes now compiles** ([#1387](https://github.com/aallan/vera/issues/1387)). §8.5.2.2's diagnostic tells the reader, verbatim, to "declare 'pick' in this file — a local declaration takes every bare call — and use the module-qualified form 'liba::pick(...)' for the imported ones". Doing exactly that was `[E608]` at compile, whose own fix text then said to rename the declaration in one of the source modules: two of our diagnostics prescribing contradictory fixes, with the one the checker named unreachable. It is also why [#187](https://github.com/aallan/vera/issues/187)'s "no way to resolve the collision without renaming a source declaration" was still literally true for functions. No bare-name collision exists in that shape — with a local `pick` declared, BOTH modules' functions are shadowed and `_register_shadowed_import` emits each under its own `mod$$pick`, which is measured: the fixed program returns 303 from `pick(1) + liba::pick(1) + libb::pick(1)` and the module carries `$pick`, `$mod$liba$pick` and `$mod$libb$pick` as three distinct symbols. The rail fired before any of that, on provenance alone. What decides the question is OWNERSHIP of the bare name, and the ownership argument never depended on genericity: `_generics_cannot_collide` became `_declarations_cannot_collide`, and where NEITHER declaration owns the name — private, outside the filter, reached only transitively, or shadowed by a local declaration — both are shadowed emissions and the rail is silent. Reading the generic classification alone was what left a non-generic pair with two apparent owners, since `module_qualified_generic_names` classifies generics only while a local declaration shadows every module's version of the name. Exactly one owner is still admitted only between two top-level generics, whose clones are named per owner; two owners is the collision the rail exists for, and the §8.5.2.2 ambiguity backstop is unchanged, so a name no namespace can resolve is still refused at check. The negatives are pinned beside the positive: without the local declaration the shape is still `[E155]`, and a genuinely colliding bare export is still refused. diff --git a/FAQ.md b/FAQ.md index 5ad6b4b63..1c24729a5 100644 --- a/FAQ.md +++ b/FAQ.md @@ -279,7 +279,7 @@ The reference compiler is under active development. The current release includes - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute - A 14-chapter formal specification -- 13,575 tests, including a 253-program conformance suite +- 13,686 tests, including a 253-program conformance suite - 43 working example programs - 164 built-in functions covering strings, arrays, math, parsing, and data types - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation diff --git a/README.md b/README.md index 978f6ae77..0a4426f36 100644 --- a/README.md +++ b/README.md @@ -261,7 +261,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md ## Project status -Vera is in **active development** at v0.1.13: 2,000+ commits, 211 releases, 13,575 tests, 95% Python code coverage, 253 conformance programs, 43 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built. +Vera is in **active development** at v0.1.13: 2,000+ commits, 211 releases, 13,686 tests, 95% Python code coverage, 253 conformance programs, 43 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built. The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [14 chapters](spec/). diff --git a/ROADMAP.md b/ROADMAP.md index 8dd0cd541..c3f4ca36e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -12,7 +12,7 @@ Ordering derives from the design principles ([DESIGN.md](DESIGN.md)): verificati ## Where we are -13,575 tests, 253 conformance programs, 43 examples, 14 spec chapters. [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs (burndown material rather than stage work), plus the *limitations* the stages below retire. +13,686 tests, 253 conformance programs, 43 examples, 14 spec chapters. [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs (burndown material rather than stage work), plus the *limitations* the stages below retire. ## The v0.2.0 burndown diff --git a/TESTING.md b/TESTING.md index 784b00700..9e6ae85a2 100644 --- a/TESTING.md +++ b/TESTING.md @@ -6,7 +6,7 @@ This is the single source of truth for Vera's testing infrastructure, coverage d | Metric | Value | |--------|-------| -| **Tests** | 13,575 across 203 files (~192,000 lines of test code; 13,358 passed + 26 stress-deselected, 191 skipped) | +| **Tests** | 13,686 across 204 files (~192,000 lines of test code; 13,469 passed + 26 stress-deselected, 191 skipped) | | **Compiler code coverage** | 95% Python, 87% JavaScript (CI minimum: 80%) | | **Conformance programs** | 253 programs across 9 spec chapters, validating every language feature | | **Example programs** | 43, all validated through `vera check` + `vera verify` | @@ -143,6 +143,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_nat_bind_construction_soundness_1332.py` | 42 | 746 | #1332 — a `@Nat` tuple component narrowed at CONSTRUCTION is obligated, never assumed (part of the #392 false-Tier-1 audit; the construction-position counterpart to `test_nat_narrowing_return_differential.py`'s return-position half). `let @Tuple = Tuple(@Int.0, N)` destructured by an irrefutable single-arm `match` verified as **proved** while `vera run` trapped on a negative: `_translate_match` asserted the arm's `@Nat` sub-pattern source fact UNCONDITIONALLY at the solver's base level, where the datatype accessor axiom reduced it to the construction obligation's own goal — the obligation discharged itself. The anti-circularity test existed but was SYNTACTIC (is the scrutinee AST a `ConstructorCall`?) where a `let`-bound tuple arrives as a slot reference whose TERM is one. Every cell pins the verdict against a control that must not move, because a verdict alone cannot separate the repair from over-rejection: the precondition-discharged form still proves and still runs, the return-position form is unchanged in both directions, and the two construction spellings — with and without the destructure — must agree with each other, which is the internal inconsistency the bug consisted of. The soundness differential asserts the verdict and the run in ONE test (verify-clean beside a trapping run IS the bug, so siblings would each pass alone), with its `requires(@Int.0 >= 0)` parametrisation verify-clean so the implication is exercised with a true antecedent. The REFINED sibling is here too, repaired by the same change and worse in kind — a refined tuple component carries no runtime guard, so pre-fix it returned `-7` for a `PosInt` from a verify-clean build rather than trapping. Two over-rejection controls straddle the guard: one where it FIRES (a tuple built from an already-`@Nat` parameter, whose postcondition still proves from the parameter's own declaration) and one where it does NOT (an opaque `@Tuple` parameter, whose declared source facts must survive). The suite is then parametrised over how the scrutinee is PRODUCED, because a guard asking "is this term literally `C(args)`" is defeated by anything that wraps the construction — an `if` producing the tuple laundered past the first version, verifying both narrowings while the program trapped, and a `match`-produced spelling did the same. Bare constructor, `if` with both arms constructed, `if` with one constructed and one call-produced, `match`-produced and let-of-let are each required to keep the narrowing obligated, in the `@Nat` and refined families alike, beside call-produced and opaque-parameter controls that must keep their facts — the boundary being PROVENANCE: a call- or parameter-produced value's component facts were established in the callee's context, a locally constructed one's are still outstanding | | `test_nested_ctor_sort_1360.py` | 30 | 680 | #1360 — a `Tuple` nested inside a constructor translates, and `verify --json` always envelopes. `let @Option> = Some(Tuple(@Nat.0, 1234));` was check-green and killed `vera verify` with a raw `z3.z3types.Z3Exception: Sort mismatch`, emitting NO `--json` envelope at all. Two sorts derived by different routes disagreed: a nested `Tuple` argument is built by the variadic-tuple branch keyed on the arguments' Z3 sorts (`Nat` reads back as `Int`, so always the `Int` spelling), while the enclosing ctor's sort comes from `_resolve_pinned_sort`, which prefers a cached instantiation equal to the pin MODULO `Nat`/`Int` — sound at a scalar position where both spell one `IntSort`, unsound at a datatype position where #884 made the two injective sorts. The `Nat` appears even in an all-`Int` program because a positive literal types as `Nat` on the declared side, which is why the trigger is the NESTING and not `Nat`; same-ADT nesting (`Some(Some(...))`) is carried as a control, measured passing before the fix, so the repair is pinned to the disagreeing sorts rather than to nesting in general. The envelope half is asserted INDEPENDENTLY of that crash — a translation function is monkeypatched to raise and the cell asserts stdout is a parseable `E699` envelope rather than empty, so the machine-readable contract holds for the next translator bug too — and the pair mutation-validates apart: reverting the sort fix reddens the four translation cells while the controls stay green, breaking the backstop reddens exactly the two envelope cells. A fourth group covers the guard PREDICATE itself: `_ctor_accepts` exists to intercept Z3's raise-instead-of-error behaviour, so a predicate that can itself raise defeats its own purpose — hostile stand-ins whose `arity()`, `domain()` and `sort()` raise must be ANSWERED `False` (the conservative "does not accept", which routes to the decline path) rather than propagate, beside a discrimination cell over real Z3 terms so the group cannot be satisfied by a predicate that swallowed its body and declined everything | | `test_hetero_widen_tailcall.py` | 21 | 378 | The heterogeneous per-arm widen guard vs tail calls (#986) and targets: an arm whose `@Nat` value is a tail call must lower to a plain `call` so the appended guard stays live (`return_call` would skip it — the widening dual of the #983 per-leaf narrowing), the genuine `@Int` arm's recursive `return_call` keeps TCO (100k-depth run), the gate is target-aware (`_is_hetero_int_widen_join`: a hetero join in a `@Nat`-returning context must NOT widen-guard its legal `@Nat` arm — the target-blind gate false-trapped 2^63), and the user `data Tuple` that fooled the builtin-Tuple gate is refused at check (E158, #1397) rather than discriminated — the FIX-3 path is retracted, so the class now measures the refusal beside the genuine carrier's guard: it still traps at u64.MAX, is untouched in range, and its coerce obligation is still `tier3`, which is the desync in the other direction | +| `test_disclosure_taint_follows_value_1406.py` | 111 | 2108 | #1406 / #1407 — a disclosed fact's taint follows the VALUE, not the spelling of the call. #1363 made a fact the run could neither prove nor guard stop discharging downstream goals at Tier 1, and found it by asking whether the `match` scrutinee was spelled as a call to a disclosed function — a syntactic question with as many answers as there are spellings. Binding the call to a `let` first makes the scrutinee a slot reference; a forwarding wrapper carries no obligation of its own, so `disclosed_fn_names`, which reads the obligation stream, never sees it. Both were `verified` at Tier 1 while `vera run` refuted the postcondition, and the runtime differential is what settles it — a status difference alone would not, which is why the carrier is `Option` and not #1363's own tuple: codegen guards a refined return and a refined tuple component at the function boundary, so the tuple shape traps inside the producer and never reaches the caller's contract, while an ADT payload is guarded nowhere. `float_to_int` supplies the opacity a disclosure needs — a refutable narrowing would be E505, an error rather than a disclosure, and would exhibit nothing. Twelve caller spellings run against one producer pair differing in its body alone (`Some(float_to_int(...))` discloses, `Some(7)` proves): direct, `let`, a `let` chain, a branch join whose arms are both call-produced, a pipe, one- and two-level wrappers, a wrapper reaching its result through a `let`, a wrapper through a pipe, a `where` helper, and — from #1431's review — a forwarder that takes the value APART and puts it back together, at one and two hops, since a value CONSTRUCTED from a disclosed component rests on that component's fact exactly as a projection does. Every one carries its clean control, which must stay `verified` — without them a fix that demoted every `match` over a call result would pass the whole file. The corpus can supply neither half: exactly one corpus program discloses at all (1 of 474 — `p4_refined_arg_clause.vera`, whose disclosed fact nothing downstream reads), so a base-vs-head obligation differential over it is silent by construction, and the selectivity cell is what measures completeness instead — one program holding a disclosed producer AND a clean one, where the caller reading the clean one must still prove, which a taint keyed on the sort, the constructor, or the mere presence of a disclosure in the run would fail while passing everything else here. Two shapes are pinned as measured NON-movers rather than omitted: a closure capture is `tier3`/E522 in both polarities (a lambda's result is opaque, so no false Tier 1 is reachable there), and #1410's argument position is `verified` before and after, because that false proof lives in the callee — made once for every caller — and no taint in the caller reaches it. Warm is checked against cold and against its own replay, since a replayed slice re-runs no body and would drop a forwarder out of the disclosed set; `reset()`'s forgetting of the recorded terms is pinned as a unit invariant, no whole program distinguishing it. A last group closes #1413, found by asking the complementary question the matrix cannot — not which spelling reaches the gated reader, but how many readers of the fact there are. Two more: the premise that lets a projected value re-narrow into a second refinement, and the component invariant a `let`-destructure seeds for a source it treats as guaranteed. Each was `verified` at Tier 1 while the program handed back `-7` for a value declared `> -3`, with no trap, and each carries the clean twin that must keep proving — these premises exist to prevent a false E505, so withholding them unconditionally would restore the bug they were written to fix. The destructure cell reaches its tuple through an ADT payload deliberately: a refined tuple component IS guarded at the producer's return, so the bare spelling is a false Tier-1 claim another guard happens to catch, and only the payload route produces the wrong value. The group closes with the cell that makes the repair structural rather than conventional: all three readers call one gate, and a walk over `vera/verifier.py`'s own AST requires that any function calling a source-fact producer also calls it — unless it IS a producer, handing the facts back rather than assuming them — with the producer roster asserted to name live methods so a rename cannot make the check match nothing. #1363's rule and its gate were both right; what let two false Tier-1s outlive it is that the rule lived at one of three sites by convention. Adversarial review added three groups. A value the SMT layer LOSES keeps its taint: a `let` whose RHS does not translate and an array literal whose elements are related only by axiom both mint a stand-in, and each was `verified` at Tier 1 while the run refuted — carrier-dependent, so the cells pick the carrier whose binding falls to `_fresh_opaque_slot` on purpose, and each carries the clean twin that proves losing a value is not itself a demotion. The warm cell is parametrised over EVERY spelling rather than a sample, because sampling two of them is what let a `where`-helper forwarder — never a declaration in the session's own loop — drop out of the warm disclosed set and prove at Tier 1 what cold demoted; a sample was the defect, so a smaller sample is not the fix. And two helpers of the same bare name in different top-level owners are pinned in both spellings, one forwarding a disclosed producer and one a clean one, since keying the set by bare name had made the first demote the second. The rebuild spellings rebuild their `None` arm as `Some(1)`, which is load-bearing rather than cosmetic: a literal `None` arm beside a `Some()` one hits the sort mismatch #1421 fixes and dies with an E699 before a single obligation is emitted, so that spelling is measured on the composed tree and pinned here as a unit over the walk plus a single-constructor ADT whose rebuild has no arm join at all — the cell that separates construction from the join `ite_join` already covers. Two cells carry `Option` rather than `Option` on purpose: after #1420/#1435 a refined RETURN is obligated wherever it is published, so a `PosInt` FORWARDER carries its own `tier3_unguarded` and reaches the caller through the obligation-derived set — the cross-module forwarder cells passed with the manifest union reverted, and the stand-in mint reddened two of three lost-value cells rather than three. A `Nat` narrowing is obligated at the construction site only, so the library discloses exactly once and its forwarders record nothing; the forwarder-plus-lost-value cell launders through an ARRAY because a tuple of `Option` translates rather than being lost, which would have made it a nothing-test. Each asserts its own premise, so a base move that starts obligating forwarders fails loudly rather than leaving the cells green for an unrelated reason; the trade is the runtime refutation, `@Nat` being sign-checked at the boundary (#1268) so the run traps instead — which is why the refutation proper stays on the `Option` cells. Rebasing over #1420 turned the shared-helper-name cell red and exposed the same keying defect in the OTHER half of the disclosed set — that set is a union of an obligation-derived and a result-derived derivation, and only the second had been scoped — so a second collision cell carries the isolated shape: two same-named helpers each disclosing through an obligation of its own, with no forwarding anywhere, which is the only route into the obligation-derived half. Two cells rather than one because the forwarding cell goes green again if only the result-derived half is scoped and the isolated one does not, and the isolated shape reproduces on `release/v0.2.0` before #1420 as well as after, so the defect is that half's own rather than #1420's — what #1420 changed is the reach. Rebasing over #1412 then retired the cross-module forwarder cells altogether, with the reason recorded where they stood: that PR obligates a refined return at every position that publishes it, so a forwarder either publishes the refinement and is named by the obligation-derived set, or drops it and hands on no fact — which makes the manifest union those cells measured unreachable. Reverting it on a scratch tree over five shapes built to break the dichotomy (a forwarder dropping the refinement, one through a `where` helper, one returning a tuple carrying the payload, one two import hops away, one in an `Exn`-declared function) changed no verdict and no cell in this file, so the union is gone; the in-module half of the same union stays, because reverting THAT reds the two rebuild spellings. #1412 also moved the runtime exhibit — the sub-pattern guard refuses the program before its postcondition is reached — so the run assertions go through one helper asserting the REFUSAL rather than naming the older site, the two #1413 cells assert that their narrowing is not Tier 1 rather than pinning the tier it lands at, and the lost-value-behind-a-forwarder cell returns to `Option` laundered through an array, `@Nat` payloads now being guarded and disclosing nothing | | `test_xmod_span_collision.py` | 4 | 156 | #987 — the span-keyed target-type table is single-module (keyed by bare span, no file identity): an imported body's expression span can coincide with a main-file entry. #987 threads each module's OWN table into codegen (`CheckArtifacts.module_artifacts` → `_compile_fn(module_tables=...)`), so the engineered line-for-line collision pair now proves the legal all-`@Nat` imported function is not falsely widen-guarded by CORRECTNESS (its own table targets `Tuple`), not merely suppression — with a `thread_modules=False` control pinning the #986 suppression fallback still holds when no module tables are threaded, and a same-file control proving top-level guards unaffected | | `test_xmod_widening_differential.py` | 18 | 293 | #987 verifier↔codegen widening differential run THROUGH THE IMPORT DOOR (the same-file `test_int_widening_differential` was green while this door was open): for each cross-module shape (array-element, tuple-construction, tuple-destructure control, transitive 3-level, and shadowed-import) the library's standalone verify must classify the `@Nat -> @Int` coercion Tier-3, AND the importing program compiled the way `vera run`/`vera compile` compile it (per-module tables threaded) must TRAP at `u64.MAX` — never the silent -1 — while passing `2^63-1` and `42` unchanged. Pins that the #820 array/tuple-construction guards, recovered from the span-keyed target table, now fire for imported bodies. Also pins the import-door trap is the guard's bare `unreachable` net (not some other trap), and a two-independent-libraries-both-widen scenario asserting BOTH imported bodies trap at `u64.MAX` (kills a first-module-only partial-collection mutant) | | `test_xmod_artifact_collection.py` | 5 | 205 | The per-module `CheckArtifacts.module_artifacts` pass is OPT-IN (`collect_module_artifacts=`, default off) because only the codegen-bound callers consume it and it is O(N²) sub-checks in the module count. Pins that `typecheck_with_artifacts` WITHOUT the flag leaves `module_artifacts` empty (the `vera verify` / warm-session path pays nothing) and WITH it collects each resolved module's own table; plus the GAP-1 artifact-level pin — in a transitive fixture (`main -> alib -> blib`) the middle module `alib`'s target table has 2 entries only because its `direct` flags are re-derived from its OWN imports (a first-module-only / top-level-flags mutant drops it to 1) | diff --git a/docs/llms-full.txt b/docs/llms-full.txt index 645f5e6f7..55109feec 100644 --- a/docs/llms-full.txt +++ b/docs/llms-full.txt @@ -3280,7 +3280,7 @@ The reference compiler is under active development. The current release includes - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute - A 14-chapter formal specification -- 13,575 tests, including a 253-program conformance suite +- 13,686 tests, including a 253-program conformance suite - 43 working example programs - 164 built-in functions covering strings, arrays, math, parsing, and data types - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation diff --git a/spec/06-contracts.md b/spec/06-contracts.md index f55d8c3e0..80187379a 100644 --- a/spec/06-contracts.md +++ b/spec/06-contracts.md @@ -245,7 +245,7 @@ A practical implication: if a function `bad` has an implementation that doesn't **Opaque effect values.** A `let` whose value is an effect operation's result (`let @Int = random_int(0, 9);`) binds a fresh *opaque* constant of the value's type in the verification model, and translation of the body continues past it ([#764](https://github.com/aallan/vera/issues/764), [#1199](https://github.com/aallan/vera/issues/1199)); the same applies per-component to a tuple destructure whose source cannot be projected. Two rules govern how obligations over an opaque value classify: - **Preconditions stay strict.** A call precondition that cannot be proven — because the argument is opaque — is reported (**E501**), exactly as for an opaque function result: establishing the precondition is the caller's obligation, and the repair is an `assert`/`assume` on the value, whose fact flows into the check ([#804](https://github.com/aallan/vera/issues/804)). -- **A goal that holds only from a disclosed fact is Tier 3, not Tier 1.** A declared-type fact whose own obligation was reported as neither proved nor guarded is not a fact the run established. A postcondition provable only once it is assumed is reported **E534** and checked at run time; a call precondition in the same position takes the E532 demotion rather than an E501 violation, since no violating model exists. This rule is **independent of module layout** ([#1399](https://github.com/aallan/vera/issues/1399)): a disclosure made in an imported module demotes its importer exactly as an in-module one does, and transitively along the import graph, so splitting a program across files never turns a Tier-3 truth into a Tier-1 proof. A module's disclosed set is derived from that module's own verification — the same set `vera verify ` reports — and read by its importers; the importer's obligation stream stays its own. +- **A goal that holds only from a disclosed fact is Tier 3, not Tier 1.** A declared-type fact whose own obligation was reported as neither proved nor guarded is not a fact the run established. A postcondition provable only once it is assumed is reported **E534** and checked at run time; a call precondition in the same position takes the E532 demotion rather than an E501 violation, since no violating model exists. Disclosure is a property of the **value**, not of the expression that names it ([#1406](https://github.com/aallan/vera/issues/1406), [#1407](https://github.com/aallan/vera/issues/1407)): the demotion is the same whether the disclosed result reaches the goal directly, through a `let` binding or a chain of them, through a projection or a destructure, joined from a branch that discloses on one arm, or taken apart and rebuilt — a value CONSTRUCTED from a disclosed component is disclosed, because the component's fact is what the reconstruction rests on. A function whose own result is such a value is itself disclosed for its callers, however many forwarding hops separate them — recorded against the function it belongs to, so a `where` helper's disclosure is scoped to its top-level owner and never reaches a same-named helper under a different one — so a wrapper, a pipe or a `where` helper carries the fact's provenance rather than laundering it. The rule binds every reader of the fact, not only a `match` arm's bindings ([#1413](https://github.com/aallan/vera/issues/1413)): a projected value re-narrowing into a second refinement, and a `let`-destructure's component invariant, are each Tier 3 when the goal *depends* on a fact withheld because the value they read from was disclosed — and Tier 1 still when it does not, the withheld facts being offered back only after a proof without them fails, so a goal that never needed one keeps it. This rule is **independent of module layout** ([#1399](https://github.com/aallan/vera/issues/1399)): a disclosure made in an imported module demotes its importer exactly as an in-module one does, and transitively along the import graph, so splitting a program across files never turns a Tier-3 truth into a Tier-1 proof. A module's disclosed set is derived from that module's own verification — the same set `vera verify ` reports — and read by its importers; the importer's obligation stream stays its own. - **An `assert` that is neither proved nor refuted says so.** A body `assert(P)` the solver cannot settle falls to a runtime check and MUST be reported (**E535**), so the construct that moved the tier count is named — the same disclosure `requires` (E521), `ensures` (E522) and `decreases` (E525) already carry. - **Refutations over opaque values are not violations.** A postcondition, refined return, or primitive-operation obligation that *fails* to prove where the goal mentions an opaque constant demotes to a runtime-checked **Tier 3** obligation (`E522` for a postcondition) rather than reporting a definite violation — a countermodel over an unconstrained stand-in says nothing about the value the effect actually produces (`random_int(1, 9)` never returns `0`, but its stand-in would "witness" a zero divisor). A proof that *succeeds* despite the opacity is kept at Tier 1: it holds for every value the constant could take. The demotion is per-obligation, not per-function — a genuine violation elsewhere in the same body is still reported. diff --git a/tests/test_disclosure_taint_follows_value_1406.py b/tests/test_disclosure_taint_follows_value_1406.py new file mode 100644 index 000000000..e3abb511d --- /dev/null +++ b/tests/test_disclosure_taint_follows_value_1406.py @@ -0,0 +1,2108 @@ +"""#1406 / #1407 — a disclosed fact's taint follows the VALUE, not the syntax. + +#1363 established the rule: a declared-type fact whose own obligation this run +DISCLOSED (`tier3_unguarded`, or `tier3` with E534 — neither proved nor +guarded) must not discharge a downstream goal at Tier 1. Its implementation +asked a syntactic question — is this `match` scrutinee spelled as a call to a +disclosed function — and a syntactic question has as many answers as there are +spellings. Two of them defeated it outright: + +* **#1406** — `let @T = mk(x); match @T.0 { … }`. The scrutinee arrives as a + slot reference, so the test answered False and the facts were handed to the + solver at full strength. One token, and the rule was gone. +* **#1407** — `fn wrap(…) { mk(x) }`, then `match wrap(x) { … }`. A forwarder + makes no claim that needs the disclosed fact, so it contributes no + obligation, so `disclosed_fn_names` — which reads the obligation stream — + never sees it, at any depth. + +Both are the same unsoundness as #1363, reached by a different route, and both +are measured here the only way that settles it: the postcondition is +`verified` at Tier 1 and the compiled program refutes it. + +THE CARRIER IS LOAD-BEARING. `Option` is used rather than the tuple +of #1363's own reproducer because codegen guards a refined RETURN and a +refined TUPLE COMPONENT at the function boundary — the tuple shape traps +inside `mk` and never reaches the caller's postcondition, so it can exhibit a +status difference but not a runtime one. An ADT payload is guarded nowhere, +so the disclosed fact is genuinely unenforced and `f`'s contract really is +refutable. `float_to_int` supplies the opacity: the payload's `> 0` can be +neither proved nor refuted, which is what `tier3_unguarded` means. A +refutable narrowing would be `violated`/E505 — an error, not a disclosure — +and would exhibit nothing. + +EVERY SPELLING CARRIES ITS CLEAN CONTROL. The two differ in `mk`'s body +alone: `Some(float_to_int(@Float64.0))` discloses, `Some(7)` proves. Same +name, same signature, same call at the caller. Without the control a fix that +demoted every `match` would pass the whole file, and the controls are what +measure that it does not — none of them may leave `verified`. +""" + +from __future__ import annotations + +import json +import os +import subprocess +import sys +from pathlib import Path + +import pytest + +import vera + +_PKG_PARENT = str(Path(vera.__file__).resolve().parents[1]) + + +def _cli(*args: str) -> subprocess.CompletedProcess[str]: + env = dict(os.environ) + existing = env.get("PYTHONPATH", "") + env["PYTHONPATH"] = ( + f"{_PKG_PARENT}{os.pathsep}{existing}" if existing else _PKG_PARENT + ) + return subprocess.run( + [sys.executable, "-m", "vera.cli", *args], + capture_output=True, text=True, encoding="utf-8", check=False, + env=env, timeout=300, + ) + + +def _verify(tmp_path: Path, source: str, name: str = "p.vera") -> dict: + p = tmp_path / name + p.write_text(source, encoding="utf-8") + proc = _cli("verify", "--json", str(p)) + try: + result = json.loads(proc.stdout) + except json.JSONDecodeError: + raise AssertionError( + f"verify emitted no envelope (exit {proc.returncode})\n" + f"{proc.stdout[:400]}\n{proc.stderr[-600:]}" + ) from None + # An UNRESOLVED call verifies "clean" with only an E200 warning, and its + # result is opaque — so a fixture that forgot to declare its producer + # exhibits a plausible-looking demotion for a reason that has nothing to + # do with disclosure. That is not hypothetical: two cells in this file + # were written without `mk` and passed. Every fixture here is checked for + # it before its verdict is read. + assert "E200" not in [w.get("error_code") for w in result["warnings"]], ( + f"fixture calls an undeclared function, so its obligations are opaque " + f"for a reason unrelated to disclosure:\n{source}" + ) + return result + + +def _run(tmp_path: Path, source: str, arg: str = "-7.0", + name: str = "r.vera") -> str: + """Compile and call `f` with *arg*; return stdout+stderr. + + The default `-7.0` is chosen so no fallback can coincide with it: it is + neither `0` nor the `None` arm's `41`, so a wrong answer cannot be read as + a right one (the payload the disclosed `mk` builds is `-7`). + """ + p = tmp_path / name + p.write_text(source, encoding="utf-8") + proc = _cli("run", str(p), "--fn", "f", "--", arg) + return proc.stdout + proc.stderr + + +# --------------------------------------------------------------------------- +# The fixture family: one caller spelling x {disclosed, clean} producer +# --------------------------------------------------------------------------- + +_POSINT = "type PosInt = { @Int | @Int.0 > 0 };\n" + +_MK_DISCLOSED = """ +private fn mk(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(float_to_int(@Float64.0)) +} +""" + +_MK_CLEAN = """ +private fn mk(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(7) +} +""" + +# A second CLEAN producer, so the `if`-join has two arms neither of which is +# constructed here. A `None` arm would make the joined term a constructor +# application, which `_is_locally_constructed` already drops the facts for +# (#1332) — the join would then fail for a reason that has nothing to do with +# disclosure, and would exhibit nothing about the `ite` walk. +_MK2 = """ +private fn mk2(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(9) +} +""" + +_ARMS = """ Some(@PosInt) -> @PosInt.0, + None -> 41""" + +_F = """ +public fn f(@Float64 -> @Int) + requires(true) + ensures(@Int.result > 0) + effects(pure) +""" + +_WRAP = """ +private fn wrap(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + mk(@Float64.0) +} +""" + + +def _rebuilder(name: str, inner: str) -> str: + """A forwarder that takes the value APART and puts it back together. + + `Some(@PosInt.0)` in the arm is a CONSTRUCTION whose component is the + disclosed payload — the projected-from case one step on, and the shape + the [#1431](https://github.com/aallan/vera/pull/1431) reviewer raised + against this branch. + + THE `None` ARM REBUILDS AS `Some(1)`, and that is not cosmetic. Mixing a + literal `None` arm with a `Some()` arm hits the sort mismatch + [#1421](https://github.com/aallan/vera/issues/1421) fixes: on this + revision the program dies with an E699 before a single obligation is + emitted, so the literal spelling would measure nothing here. With both + arms constructing, the same shape translates on both revisions and the + differential is real. The literal `None`-arm spelling is measured on the + composed tree instead — see + `test_1418_a_value_rebuilt_from_a_disclosed_component_is_disclosed`. + """ + return f""" +private fn {name}(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{{ + match {inner}(@Float64.0) {{ + Some(@PosInt) -> Some(@PosInt.0), + None -> Some(1) + }} +}} +""" + + +#: caller spelling → the declarations after `mk`. Every one of them reaches +#: the same `match` over the same value; only the route differs. +_SPELLINGS: dict[str, str] = { + # The one #1363 already handled — the control that pins the axis. + "direct": _F + "{\n match mk(@Float64.0) {\n" + _ARMS + "\n }\n}\n", + # #1406, the issue's own shape. + "let_bound": _F + "{\n let @Option = mk(@Float64.0);\n" + " match @Option.0 {\n" + _ARMS + "\n }\n}\n", + # Rebound a second time: the taint has to survive a chain, not one hop. + "let_chain": _F + "{\n let @Option = mk(@Float64.0);\n" + " let @Option = @Option.0;\n" + " match @Option.0 {\n" + _ARMS + "\n }\n}\n", + # A branch join: disclosed on one arm only, so the `ite` walk is what + # answers. Reading only the root term would miss this. + "ite_join": _MK2 + _F + "{\n let @Option = if @Float64.0 > 0.0 then {\n" + " mk(@Float64.0)\n } else {\n" + " mk2(@Float64.0)\n };\n" + " match @Option.0 {\n" + _ARMS + "\n }\n}\n", + # A pipe desugars to a call inside the SMT layer, but the AST node the + # syntactic test sees is a pipe. Nothing in the fix names pipes. + "pipe": _F + "{\n match @Float64.0 |> mk() {\n" + _ARMS + "\n }\n}\n", + # #1407, the issue's own shape. + "wrap1": _WRAP + _F + "{\n match wrap(@Float64.0) {\n" + _ARMS + "\n }\n}\n", + # Two hops: the fixpoint has to carry it further than one pass. + "wrap2": _WRAP + """ +private fn wrap_outer(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + wrap(@Float64.0) +} +""" + _F + "{\n match wrap_outer(@Float64.0) {\n" + _ARMS + "\n }\n}\n", + # Both bugs at once: the wrapper reaches its result through a `let`. + "wrap_let": """ +private fn wrap(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + let @Option = mk(@Float64.0); + @Option.0 +} +""" + _F + "{\n match wrap(@Float64.0) {\n" + _ARMS + "\n }\n}\n", + "wrap_pipe": """ +private fn wrap(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + @Float64.0 |> mk() +} +""" + _F + "{\n match @Float64.0 |> wrap() {\n" + _ARMS + "\n }\n}\n", + # A `where` helper is a forwarder the flat registries cannot even name. + "where_helper": _F + "{\n match h(@Float64.0) {\n" + _ARMS + "\n }\n}\n" + """where { + fn h(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + mk(@Float64.0) + } +} +""", + # CONSTRUCTED-from, not merely projected-from: the value is taken apart + # and put back together before the consumer ever sees it. Nothing in the + # rule names constructions — the walk asks by OCCURRENCE, so the disclosed + # term inside the constructor's argument is still there to be found. + "rebuild_ctor": _rebuilder("rebuild", "mk") + + _F + "{\n match rebuild(@Float64.0) {\n" + + _ARMS + "\n }\n}\n", + # Rebuilt twice: taking a value apart and reassembling it must not launder + # the disclosure at any depth. + "rebuild_ctor2": _rebuilder("rebuild", "mk") + + _rebuilder("rebuild_outer", "rebuild") + + _F + "{\n match rebuild_outer(@Float64.0) {\n" + + _ARMS + "\n }\n}\n", +} + +#: The spellings that were `verified` on `origin/release/v0.2.0` and are +#: `tier3`/E534 now. `direct` is excluded because #1363 already demoted it — +#: it is the control, not a mover. +_MOVERS = tuple(s for s in sorted(_SPELLINGS) if s != "direct") + + +#: THE RUNTIME HALF, after #1412. A REFUSED run is the exhibit; which guard +#: refuses it is #1412's business, not this file's. Before it, an ADT payload +#: was guarded nowhere, so the bad value travelled all the way to `f`'s +#: postcondition and refuted it. #1412 checks every obligated narrowing at +#: the place that obligates it, so the constructor sub-pattern guard (#765) +#: now fires first and the program is refused there instead. Both are the +#: same value being refused at run time — which is the claim — and naming +#: only the older site is what turned seven cells red on a base move that +#: strengthened the compiler. +_REFUSALS = ("Postcondition violation", "Refinement violation") + + +def _assert_refused(out: str, what: str = "") -> None: + """The run must REFUSE the value, at whichever guard reaches it first.""" + assert any(m in out for m in _REFUSALS), ( + f"{what}the run was not refused, so this fixture reports no verdict " + f"about soundness — a trap or a setup failure earlier in the run " + f"looks identical to a passing contract here:\n{out[-700:]}" + ) + + +def _source(spelling: str, *, disclosed: bool) -> str: + mk = _MK_DISCLOSED if disclosed else _MK_CLEAN + return _POSINT + mk + _SPELLINGS[spelling] + + +def _f_ensures(result: dict) -> tuple[str, str | None]: + """`f`'s postcondition obligation, as (status, error_code). + + Keyed on the predicate text rather than on position: the spellings emit + different numbers of obligations, and a positional read would silently + follow the wrong one when a helper is added. + """ + hits = [o for o in result["obligations"] + if o["kind"] == "ensures" and o["description"] == "@Int.result > 0"] + assert len(hits) == 1, [ + (o["kind"], o["description"], o["status"]) for o in result["obligations"] + ] + return hits[0]["status"], hits[0].get("error_code") + + +# --------------------------------------------------------------------------- +# The rule, over every spelling +# --------------------------------------------------------------------------- + +@pytest.mark.parametrize("spelling", sorted(_SPELLINGS)) +def test_1406_a_disclosed_value_demotes_however_it_is_spelled( + tmp_path: Path, spelling: str, +) -> None: + """Same value, same `match`, ten routes — one verdict. + + The premise is checked in the same breath as the conclusion: `mk`'s own + obligation must be `tier3_unguarded`, or this fixture is measuring + something other than a disclosed fact and its verdict means nothing. + """ + result = _verify(tmp_path, _source(spelling, disclosed=True)) + assert result["ok"] is True, result.get("diagnostics") + statuses = [(o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"]] + assert ("refine_bind", "tier3_unguarded", "E506") in statuses, ( + f"{spelling}: the producer did not disclose, so this fixture proves " + f"nothing about a disclosed fact — {statuses}" + ) + assert _f_ensures(result) == ("tier3", "E534"), ( + f"{spelling}: the postcondition holds only from a fact this run could " + f"neither prove nor guard, so it is a Tier-3 truth — got " + f"{_f_ensures(result)}" + ) + + +@pytest.mark.parametrize("spelling", sorted(_SPELLINGS)) +def test_1406_a_clean_producer_stays_verified_through_every_spelling( + tmp_path: Path, spelling: str, +) -> None: + """The over-rejection control, one per spelling. + + A fix that demoted every `match` over a call result would satisfy the + cells above and destroy Tier-1 verification for everyone else. These are + what measure that the demotion is keyed on DISCLOSURE: the only difference + from the cell above is `mk`'s body. + """ + result = _verify(tmp_path, _source(spelling, disclosed=False)) + assert result["ok"] is True, result.get("diagnostics") + assert not [o for o in result["obligations"] + if o["status"] == "tier3_unguarded"], ( + f"{spelling}: the control's producer disclosed something, so it is " + f"not a clean control" + ) + assert _f_ensures(result) == ("verified", None), ( + f"{spelling}: a clean producer's fact is established, so the " + f"postcondition is proved — got {_f_ensures(result)}" + ) + + +# --------------------------------------------------------------------------- +# The runtime differential — why the demotion is not merely tidier +# --------------------------------------------------------------------------- + +@pytest.mark.parametrize("spelling", ["let_bound", "wrap1", "rebuild_ctor"]) +def test_1406_the_demoted_contract_is_one_the_program_refutes( + tmp_path: Path, spelling: str, +) -> None: + """`verified` here would be a FALSE Tier 1, not a conservative one. + + The two issues' own shapes, run. `-7.0` reaches `mk`, whose payload the + run could neither prove nor guard, and `f`'s postcondition fails on the + value that comes back. Before the fix this contract was `verified` while + the program did this, which is the definition of unsound; after it, the + contract is Tier 3 and the runtime check is the thing that catches it. + """ + source = _source(spelling, disclosed=True) + assert _f_ensures(_verify(tmp_path, source)) == ("tier3", "E534") + out = _run(tmp_path, source) + _assert_refused(out, f"{spelling}: ") + + +@pytest.mark.parametrize("spelling", ["let_bound", "wrap1", "rebuild_ctor"]) +def test_1406_the_clean_twin_runs_clean(tmp_path: Path, spelling: str) -> None: + """The other half of the differential. + + Without this, "the program refutes it" could be a property of the + spelling rather than of the disclosure — the same route with an + established fact returns its value and violates nothing. + """ + out = _run(tmp_path, _source(spelling, disclosed=False)) + assert "violation" not in out, out[-700:] + # The LAST TOKEN, exactly. `endswith("7")` is satisfied by `-7`, which is + # precisely the disclosed route's answer — so the control could not have + # caught a clean route that returned the disclosed payload (CodeRabbit, + # PR #1418). + assert out.strip().split()[-1] == "7", out[-300:] + + +# --------------------------------------------------------------------------- +# Shapes that do NOT move, pinned so a later change is visible against them +# --------------------------------------------------------------------------- + +_CLOSURE = """ +type IntThunk = fn(Int -> Int) effects(pure); +""" + _F + "{\n let @Option = mk(@Float64.0);\n" \ + " let @IntThunk = fn(@Int -> @Int) effects(pure) {\n" \ + " match @Option.0 {\n" + _ARMS + "\n }\n };\n" \ + " apply_fn(@IntThunk.0, 1)\n}\n" + + +@pytest.mark.parametrize("disclosed", [True, False]) +def test_1406_a_closure_capture_cannot_produce_a_false_tier1( + tmp_path: Path, disclosed: bool, +) -> None: + """Captured in a lambda, the value reaches no Tier-1 proof either way. + + Recorded as a MEASURED non-result rather than left out. A closure's + result is opaque to the verifier, so the enclosing postcondition is + already `tier3`/E522 — for both producers, which is what makes this a pin + and not a mover. If a later change makes a lambda's result transparent, + the disclosed half of this cell must move with it or a new escape opens + silently. + """ + mk = _MK_DISCLOSED if disclosed else _MK_CLEAN + result = _verify(tmp_path, _POSINT + mk + _CLOSURE) + assert result["ok"] is True, result.get("diagnostics") + unguarded = [o for o in result["obligations"] + if o["status"] == "tier3_unguarded"] + assert bool(unguarded) is disclosed, ( + f"the producer's disclosure does not match the fixture's polarity: " + f"{[(o['kind'], o['status']) for o in result['obligations']]}" + ) + assert _f_ensures(result) == ("tier3", "E522"), _f_ensures(result) + + +_ARGUMENT = _POSINT + _MK_DISCLOSED + """ +private fn consume(@Option -> @Int) + requires(true) + ensures(@Int.result > 0) + effects(pure) +{ + match @Option.0 { +""" + _ARMS + """ + } +} +""" + _F + "{\n consume(mk(@Float64.0))\n}\n" + + +def test_1410_the_argument_position_is_unchanged_by_this_fix( + tmp_path: Path, +) -> None: + """#1410's shape, pinned as measured — NOT fixed here. + + Passing a disclosed value as an ARGUMENT leaves `consume`'s postcondition + `verified` while the program refutes it. That is a different rule: the + false proof lives in the callee, which modular verification makes once for + every caller, so no amount of tainting in `f` reaches it. It measures + identically on `origin/release/v0.2.0` and here — for the direct, the + `let`-bound and the wrapper spellings alike — which is the evidence that + it is a separate root cause and not a gap in this one. + + Pinned so #1410's fix is visible against it: when the argument position + gains the obligation the construction position already has, this cell + changes and says so. + """ + result = _verify(tmp_path, _ARGUMENT) + assert result["ok"] is True, result.get("diagnostics") + assert ("refine_bind", "tier3_unguarded", "E506") in [ + (o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"] + ], "the producer did not disclose, so this pin measures nothing" + consume_ens = [o for o in result["obligations"] + if o["kind"] == "ensures" + and o["description"] == "@Int.result > 0"] + assert len(consume_ens) == 2, [ + (o["kind"], o["description"]) for o in result["obligations"] + ] + assert [o["status"] for o in consume_ens] == ["verified", "verified"], ( + f"#1410's shape moved — if that was intended, this cell records the " + f"measurement it moved from: {[o['status'] for o in consume_ens]}" + ) + out = _run(tmp_path, _ARGUMENT) + _assert_refused(out) + + +# --------------------------------------------------------------------------- +# Warm == cold +# --------------------------------------------------------------------------- + +@pytest.mark.parametrize("spelling", sorted(_SPELLINGS)) +def test_1407_a_warm_session_agrees_with_the_cold_run( + tmp_path: Path, spelling: str, +) -> None: + """And keeps agreeing across a replay. + + `where_helper` is here because it is the one that broke (#1418 review + F2). The session's loop walks `program.declarations` and used to cache a + bool about the top-level name, so a `where` helper that forwards a + disclosed value — added to `_result_disclosed_fns` while its PARENT's + slice was verified, never a `decl.name` itself — was dropped, the warm + fixpoint settled one hop early, and warm proved at Tier 1 exactly what + cold demoted. Parametrising over only the two spellings that worked is + what let it through, so this runs over EVERY spelling rather than a + sample — a sample is the defect, not the coverage (CodeRabbit, PR #1418: + `wrap2` needs the warm fixpoint to carry the taint two hops, and + `wrap_let`/`wrap_pipe` need it to survive a forwarder that reaches its + result through a binding). + + The warm path assembles its stream from cached per-function slices, and a + replayed slice re-runs no body — so the wrapper's "hands on a disclosed + value" answer, which the cold path collects DURING translation, has to be + cached with it. Uncached, a replayed `wrap` drops out of the disclosed + set and the warm session proves at Tier 1 exactly what the cold run + demotes: the generous direction, and the one that matters. + """ + from vera.obligations.session import VerificationSession + + source = _source(spelling, disclosed=True) + cold = [(o["kind"], o["status"], o.get("error_code")) + for o in _verify(tmp_path, source)["obligations"]] + + session = VerificationSession() + first = session.verify_source(source, file=str(tmp_path / "s.vera")) + warm = [(o.kind, o.status, o.error_code or None) for o in first.obligations] + second = session.verify_source(source, file=str(tmp_path / "s.vera")) + replay = [(o.kind, o.status, o.error_code or None) for o in second.obligations] + + assert warm == cold, f"warm/cold divergence:\n warm {warm}\n cold {cold}" + assert replay == cold, f"replay divergence:\n replay {replay}\n cold {cold}" + assert ("ensures", "tier3", "E534") in warm, warm + + +# --------------------------------------------------------------------------- +# The accounting identity, over the whole family +# --------------------------------------------------------------------------- + +@pytest.mark.parametrize("spelling", sorted(_SPELLINGS)) +@pytest.mark.parametrize("disclosed", [True, False]) +def test_1406_the_json_accounting_identity_holds( + tmp_path: Path, spelling: str, disclosed: bool, +) -> None: + """`len(obligations) == total + violated + tier3_unguarded`, everywhere. + + A demotion moves an obligation between buckets, and the summary is derived + from the stream — so a fix that recorded a status the summary does not + know how to count would break the partition `verify --json` documents + rather than any single verdict. + """ + result = _verify(tmp_path, _source(spelling, disclosed=disclosed)) + obs = result["obligations"] + summary = result["verification"] + violated = sum(1 for o in obs if o["status"] == "violated") + unguarded = sum(1 for o in obs if o["status"] == "tier3_unguarded") + assert len(obs) == summary["total"] + violated + unguarded, ( + f"{spelling}/{disclosed}: {len(obs)} obligations against total " + f"{summary['total']} + violated {violated} + unguarded {unguarded}" + ) + assert summary["total"] == ( + summary["tier1_verified"] + summary["tier3_runtime"] + ), summary + + +# --------------------------------------------------------------------------- +# Selectivity — the control the corpus cannot supply +# --------------------------------------------------------------------------- + +# NO corpus program discloses anything (measured: 0 of 472 carry a +# `tier3_unguarded` or E534 obligation), so a corpus differential over this +# change is silent by construction and can report no completeness regression +# because it exercises nothing. This is the cell that does: ONE program in +# which a disclosed producer and a clean one both exist, so `_disclosed_fns` +# is non-empty and the taint machinery is live, and the caller that reads from +# the clean one must still prove at Tier 1. A taint keyed on anything coarser +# than the value — the sort, the constructor, the presence of any disclosure +# in the run — passes every other cell in this file and fails here. +_SELECTIVE = _POSINT + _MK_DISCLOSED + """ +private fn mk_ok(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(7) +} + +public fn f_dirty(@Float64 -> @Int) + requires(true) + ensures(@Int.result > 0) + effects(pure) +{ + let @Option = mk(@Float64.0); + match @Option.0 { +""" + _ARMS + """ + } +} + +public fn f_clean(@Float64 -> @Int) + requires(true) + ensures(@Int.result > 0) + effects(pure) +{ + let @Option = mk_ok(@Float64.0); + match @Option.0 { +""" + _ARMS + """ + } +} +""" + + +def test_1406_disclosure_taints_the_value_not_the_run(tmp_path: Path) -> None: + """Both callers in one program: only the one reading a disclosed value moves.""" + result = _verify(tmp_path, _SELECTIVE) + assert result["ok"] is True, result.get("diagnostics") + ensures = [(o["status"], o.get("error_code")) for o in result["obligations"] + if o["kind"] == "ensures" and o["description"] == "@Int.result > 0"] + assert ensures == [("tier3", "E534"), ("verified", None)], ( + f"f_dirty must demote and f_clean must not — got {ensures}" + ) + + +def test_1406_a_warm_session_does_not_carry_the_taint_between_functions( + tmp_path: Path, +) -> None: + """The same selectivity, on one shared solver. + + A warm session reuses one `SmtContext` across every function, and + `reset()` restarts `_fresh_counter` — so the next function mints the same + hash-consed `mk!0` constant the previous one's disclosed call produced. + A recorded term left standing would match a CLEAN call's result by name + collision alone, and `f_clean` would inherit a demotion from a function it + has nothing to do with. + """ + from vera.obligations.session import VerificationSession + + cold = [(o["kind"], o["status"], o.get("error_code")) + for o in _verify(tmp_path, _SELECTIVE)["obligations"]] + session = VerificationSession() + res = session.verify_source(_SELECTIVE, file=str(tmp_path / "s.vera")) + warm = [(o.kind, o.status, o.error_code or None) for o in res.obligations] + assert warm == cold, f"warm/cold divergence:\n warm {warm}\n cold {cold}" + assert warm.count(("ensures", "tier3", "E534")) == 1, warm + + +def test_1406_reset_forgets_the_previous_functions_disclosed_terms() -> None: + """`SmtContext.reset()` drops the recorded terms — pinned directly. + + A warm session reuses one context across a whole program, so + `_disclosed_terms` is per-function state that must not survive the + boundary. No whole program is known to distinguish keeping it — + `_fresh_name` carries the callee's name, so a stale entry can only + collide with a same-named callee's result, which has the same disclosure + status — which is exactly why the invariant is pinned here rather than + through a program that happens to exhibit it. Left to a downstream + symptom, this line would be unpinned and the next change to how a call's + result is named would silently turn a defensive clear into a real leak. + """ + import z3 + + from vera.smt import SmtContext + + smt = SmtContext() + term = z3.Int("_call_mk_1") + smt._disclosed_terms.append(term) + assert smt.term_is_disclosed(term) is True + smt.reset() + assert smt.term_is_disclosed(term) is False, ( + "a previous function's disclosed term is still recorded, so a later " + "function's identically-named call result inherits its demotion" + ) + + +# --------------------------------------------------------------------------- +# #1413 — the other two readers of the same disclosed fact +# --------------------------------------------------------------------------- + +# A disclosed value's declared-type facts are read at THREE places, and #1363 +# gated one. The cells above cover it. These cover the other two, found by +# asking the question the matrix could not: not "which spelling reaches the +# gated reader" but "which readers are there". Both are the same rule and the +# same mechanism — one fact, withheld rather than dropped — and both produce a +# `verified` obligation the program refutes with no trap. + +_BIG = "type Big = { @Int | @Int.0 > -3 };\n" + +# Reader 2: `_check_refined_binding_obligation_term`'s `src_fact`. The arm +# binds the `PosInt` payload as a DIFFERENT refinement, and the narrowing is +# discharged from `PosInt`'s predicate — which the run disclosed. +_REBIND = _POSINT + _BIG + _MK_DISCLOSED + """ +public fn f(@Float64 -> @Int) + requires(true) + ensures(true) + effects(pure) +{ + match mk(@Float64.0) { + Some(@Big) -> @Big.0, + None -> 41 + } +} +""" + +# Reader 3: the let-destructure component seed. The tuple is reached through +# an ADT payload on purpose — a refined tuple component IS guarded at the +# producer's return exit, so the bare `Tuple` spelling is a false +# Tier-1 CLAIM whose value another guard happens to catch. Through a payload +# there is no guard and the wrong value comes out, which is what makes this a +# soundness cell rather than a bookkeeping one. +_DESTRUCTURE = _POSINT + _BIG + """ +private fn mk(@Float64 -> @Option>) + requires(true) + ensures(true) + effects(pure) +{ + Some(Tuple(float_to_int(@Float64.0), 5)) +} + +public fn f(@Float64 -> @Int) + requires(true) + ensures(true) + effects(pure) +{ + match mk(@Float64.0) { + Some(@Tuple) -> { + let Tuple<@PosInt, @Int> = @Tuple.0; + let @Big = @PosInt.0; + @Big.0 + }, + None -> 41 + } +} +""" + +# The clean twins: identical shape, a producer whose payload the solver +# settles. `Some(7)` / `Some(Tuple(7, 5))` narrow into `Big` provably. +_REBIND_CLEAN = _REBIND.replace( + "Some(float_to_int(@Float64.0))", "Some(7)") +_DESTRUCTURE_CLEAN = _DESTRUCTURE.replace( + "Some(Tuple(float_to_int(@Float64.0), 5))", "Some(Tuple(7, 5))") + + +def _narrowing_binds(result: dict) -> list[tuple[str, str | None]]: + """The `refine_bind` obligations that are NOT the producer's own. + + Keyed by excluding the producer's site (`float_to_int(...)`), so the cell + reads the consumer's narrowing rather than the disclosure that feeds it — + which are different obligations with different correct statuses. + """ + return [(o["status"], o.get("error_code")) for o in result["obligations"] + if o["kind"] == "refine_bind" + and "float_to_int" not in (o.get("description") or "")] + + +@pytest.mark.parametrize( + "label,source", + [("rebind", _REBIND), ("destructure", _DESTRUCTURE)], + ids=["rebind", "destructure"], +) +def test_1413_a_renarrowing_off_a_disclosed_value_is_not_tier_1( + tmp_path: Path, label: str, source: str, +) -> None: + """The second and third readers demote, and the run says why they must. + + Before this change both were `verified` — a Tier-1 claim — while the + program returned `-7` for a value declared `Big` (`> -3`) and trapped + nowhere. + + THE ASSERTION IS THE CLAIM, NOT ITS ENCODING. It read + `[("tier3_unguarded", "E506")]`, and #1412 moved the tier under it: every + obligated narrowing is now checked at the place that obligates it, so a + refined ADT sub-pattern bind and a destructured component re-narrowing DO + carry a guard, the obligation lands at `tier3` rather than + `tier3_unguarded`, and the run is refused instead of handing `-7` back. + That is the compiler getting stronger, and pinning the exact tier made + this cell red for it. + + What the cell is FOR is unchanged and still load-bearing, which was + measured rather than assumed: with the gate reverted both come back + `verified`, so the demotion is still this mechanism's doing and not + #1412's. So the claim asserted here is that the narrowing is not a + Tier-1 proof, and that the run refuses the value at whichever guard now + reaches it first. + """ + result = _verify(tmp_path, source) + assert result["ok"] is True, result.get("diagnostics") + binds = _narrowing_binds(result) + assert binds, f"{label}: no consumer narrowing was obligated at all" + assert all(status != "verified" for status, _code in binds), ( + f"{label}: the narrowing holds only from a fact this run could " + f"neither prove nor guard, so it must not be a Tier-1 proof — " + f"got {binds}" + ) + _assert_refused(_run(tmp_path, source), f"{label}: ") + + +@pytest.mark.parametrize( + "label,source", + [("rebind", _REBIND_CLEAN), ("destructure", _DESTRUCTURE_CLEAN)], + ids=["rebind", "destructure"], +) +def test_1413_a_renarrowing_off_a_clean_value_still_proves( + tmp_path: Path, label: str, source: str, +) -> None: + """The over-rejection control for both new readers. + + These premises exist to stop a false E505 — a projection out of a refined + source must be able to use the invariant that source carries. Withholding + them unconditionally would restore exactly the bug `_term_source_fact` was + written to fix, so each reader's gate is measured against a source whose + fact the run DID establish. + """ + result = _verify(tmp_path, source) + assert result["ok"] is True, result.get("diagnostics") + assert not [o for o in result["obligations"] + if o["status"] == "tier3_unguarded"], ( + f"{label}: the control's producer disclosed something" + ) + # TWO here, not one: the clean producer's own `Some(7)` narrowing into + # `PosInt` is itself a `refine_bind`, and it has no `float_to_int` site for + # `_narrowing_binds` to filter on — so the count is asserted rather than + # the filter widened, which would let the consumer's bind go missing + # unnoticed. + binds = [(o["status"], o.get("error_code")) for o in result["obligations"] + if o["kind"] == "refine_bind"] + assert binds == [("verified", None), ("verified", None)], ( + f"{label}: a clean source's invariant must still discharge the " + f"re-narrowing, and the producer's own narrowing must still prove — " + f"got {binds}" + ) + out = _run(tmp_path, source) + assert "violation" not in out, out[-400:] + assert out.strip().split()[-1] == "7", out[-400:] # exact, not a suffix + + +#: The fourth reader, as a program rather than as an AST walk. `consume` +#: declares a parameter with a refinement nested inside it, so #1420 obligates +#: the ARGUMENT for that refinement; the argument's own declared type is the +#: premise, and it rests on a disclosure. Spelled two ways, same value. +_ARG_NESTED = """type PosInt = { @Int | @Int.0 > 0 }; + +private fn mk(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(%s) +} + +private fn consume(@Option -> @Int) + requires(true) + ensures(true) + effects(pure) +{ + match @Option.0 { + Some(@PosInt) -> @PosInt.0, + None -> 41 + } +} + +public fn f(@Float64 -> @Int) + requires(true) + ensures(true) + effects(pure) +{ +%s +} +""" + +_ARG_DIRECT = " consume(mk(@Float64.0))" +_ARG_LET = (" let @Option = mk(@Float64.0);\n" + " consume(@Option.0)") + + +@pytest.mark.parametrize("body,ids", [(_ARG_DIRECT, "direct"), (_ARG_LET, "let")], + ids=["direct", "let_bound"]) +def test_1418_a_nested_refinement_premise_follows_the_value( + tmp_path: Path, body: str, ids: str, +) -> None: + """Both spellings of the same value give the same verdict. + + The nested-refinement site decided disclosure for itself, with a + syntactic test over the value's producing leaves, so the two spellings + disagreed: `tier3_unguarded` written `consume(mk(x))` and **`verified`** + written `let @T = mk(x); consume(@T.0)` — a Tier-1 claim resting on a fact + the same run reported as neither proved nor guarded. #1406's bug, in a + reader added after #1406 was fixed, which is why the structural cell + below now names this producer too. + """ + src = _ARG_NESTED % ("float_to_int(@Float64.0)", body) + result = _verify(tmp_path, src) + assert result["ok"] is True, result.get("diagnostics") + binds = [(o["status"], o.get("error_code")) for o in result["obligations"] + if o["kind"] == "refine_bind"] + assert ("tier3_unguarded", "E506") in binds, binds + assert ("verified", None) not in binds, ( + f"a nested-refinement premise was granted at Tier 1 over a disclosed " + f"value — {binds}" + ) + + +@pytest.mark.parametrize("body", [_ARG_DIRECT, _ARG_LET], + ids=["direct", "let_bound"]) +def test_1418_a_nested_refinement_premise_over_a_clean_value_still_proves( + tmp_path: Path, body: str, +) -> None: + """The control: routing through the gate did not demote every argument.""" + src = _ARG_NESTED % ("7", body) + result = _verify(tmp_path, src) + assert result["ok"] is True, result.get("diagnostics") + binds = [(o["status"], o.get("error_code")) for o in result["obligations"] + if o["kind"] == "refine_bind"] + assert binds and all(b == ("verified", None) for b in binds), binds + + +def test_1413_every_reader_of_a_source_fact_consults_the_one_gate() -> None: + """No reader may decide for itself whether a fact was established. + + #1363's rule was correct and its single gate was correct; what let two + false Tier-1s outlive it is that the rule lived at ONE of the three places + a declared-type source fact is read, by convention rather than by + construction. Convention does not survive a fourth reader. + + The invariant, checked against the module's own AST: a function that calls + a source-fact producer must also call `_established_facts` — unless it IS + a producer, i.e. it hands the facts back to a caller instead of assuming + them. Adding a reader that assumes a fact without asking reddens this. + + The producer roster is asserted to still name real methods, so a rename + cannot make the check vacuous by matching nothing, and the reader set is + asserted EXACTLY rather than as a floor — a floor left enough slack that + dropping a producer from the roster, which is how the fourth reader got + in, still satisfied it. + """ + import ast as pyast + import inspect + + import vera.smt as smt_mod + import vera.verifier as verifier_mod + + #: The functions that BUILD a declared-type fact about a value. A reader + #: is any function that calls one of these and then assumes the result. + #: `_nested_refinement_facts` was NOT here, and that is how a fourth + #: reader got in (#1418 review). #1420 added + #: `_check_nested_refinement_obligation`, which builds a source fact with + #: it and then decided for itself whether to assume it, with a local + #: syntactic test over the value's producing leaves — since deleted with + #: its only call site — so a `let`-bound disclosed producer answered False + #: and its declared type was granted as a premise. Measured: the same value gave that + #: obligation `tier3_unguarded` spelled `consume(mk(x))` and `verified` + #: spelled `let @T = mk(x); consume(@T.0)`. This cell's whole claim is + #: that convention does not survive a fourth reader; it did not, because + #: the roster named the producers of the day rather than the kind. + producers = {"_term_source_fact", "_subpattern_source_facts_term", + "_nested_refinement_facts"} + + # Both modules (#1418 review F5). Every producer lives in the verifier + # today, so the SMT half of this walk currently finds none and is + # VACUOUS there — it is included so that a premise seeded next to the + # recording hook, which now lives in that layer, is inside the check by + # existing code rather than by someone remembering to widen it. The + # roster assertion below is what stops the whole cell going vacuous. + trees = [] + for mod in (verifier_mod, smt_mod): + src_file = inspect.getsourcefile(mod) # not cwd-dependent + assert src_file is not None + trees.append(pyast.parse(Path(src_file).read_text(encoding="utf-8"))) + + # Keyed by (module, name): merging the two namespaces would let a + # same-named function in one module overwrite the other's entry, so a + # reader could be judged by a namesake's call set (CodeRabbit, PR #1418). + defined: set[str] = set() + calls: dict[tuple[str, str], set[str]] = {} + for mod_name, tree in zip(("verifier", "smt"), trees): + for node in pyast.walk(tree): + if not isinstance(node, (pyast.FunctionDef, pyast.AsyncFunctionDef)): + continue + defined.add(node.name) + named: set[str] = set() + for inner in pyast.walk(node): + if (isinstance(inner, pyast.Call) + and isinstance(inner.func, pyast.Attribute) + and isinstance(inner.func.value, pyast.Name) + and inner.func.value.id == "self"): + named.add(inner.func.attr) + calls[(mod_name, node.name)] = named + + missing = sorted(producers - defined) + assert not missing, ( + f"the producer roster names methods that no longer exist ({missing}), " + f"so this check matches nothing and proves nothing — update it" + ) + assert "_established_facts" in defined + + readers = sorted( + f"{mod}:{name}" for (mod, name), named in calls.items() + if named & producers and name not in producers + ) + # EXACT membership, not a floor (#1418 review J2). `>= 3` left a + # reader of slack, so dropping `_nested_refinement_facts` from the + # producer roster — the very omission that let the fourth reader in — + # still satisfied it. A new reader is a deliberate edit here, and so is + # a deleted one. + assert readers == [ + "verifier:_check_nested_refinement_obligation", + "verifier:_check_refined_binding_obligation_term", + "verifier:_subpattern_source_facts", + "verifier:_walk_for_nat_binding_obligations", + ], ( + f"the set of functions reading a declared-type source fact changed: " + f"{readers}. A new one must call `_established_facts` (the check " + f"below); a removed one must be removed from this list, deliberately" + ) + ungated = [ + r for r in readers + if "_established_facts" not in calls[(r.split(":", 1)[0], + r.split(":", 1)[1])] + ] + assert not ungated, ( + f"{ungated} read a declared-type source fact and assume it without " + f"asking `_established_facts` whether this run established it — that " + f"is the shape of #1406 / #1407 / #1413, one reader further out" + ) + + +# --------------------------------------------------------------------------- +# Composition with #1399/#1402: the taint AND the citation cross the import +# --------------------------------------------------------------------------- + +_IMP_LIB = _POSINT + """ +public fn mk(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(float_to_int(@Float64.0)) +} +""" + +_IMP_CALLERS = { + # #1399/#1402's own shape — the control for this group. + "direct": "import oplib;\n" + _POSINT + _F + + "{\n match oplib::mk(@Float64.0) {\n" + _ARMS + "\n }\n}\n", + # #1406 across the boundary: the scrutinee is a slot reference, so the + # importer's manifest consult never fires on it. + "let_bound": "import oplib;\n" + _POSINT + _F + + "{\n let @Option = oplib::mk(@Float64.0);\n" + " match @Option.0 {\n" + _ARMS + "\n }\n}\n", + # #1407 across the boundary: the wrapper is local and carries no + # obligation, so neither this run's stream nor the manifest names it. + "wrapper": "import oplib;\n" + _POSINT + """ +private fn wrap(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + oplib::mk(@Float64.0) +} +""" + _F + "{\n match wrap(@Float64.0) {\n" + _ARMS + "\n }\n}\n", +} + + +def _verify_with_lib(tmp_path: Path, caller: str) -> dict: + (tmp_path / "oplib.vera").write_text(_IMP_LIB, encoding="utf-8") + return _verify(tmp_path, caller, name="main.vera") + + +@pytest.mark.parametrize("spelling", sorted(_IMP_CALLERS)) +def test_1406_the_taint_crosses_an_import_in_every_spelling( + tmp_path: Path, spelling: str, +) -> None: + """#1402 gives the importer a disclosed set; this makes it survive. + + Measured through the rebase: on `release/v0.2.0` before #1402 all three + escaped, with #1402 alone only `direct` demoted, and the two spellings + this PR is about needed both changes. They compose rather than overlap + because the hook the SMT layer records terms through IS + `_scrutinee_is_disclosed_call` — whatever #1402 teaches that method about + resolving an imported callee, the value taint inherits. + """ + result = _verify_with_lib(tmp_path, _IMP_CALLERS[spelling]) + assert result["ok"] is True, result.get("diagnostics") + assert _f_ensures(result) == ("tier3", "E534"), ( + f"{spelling}: an imported disclosure must demote its importer " + f"whatever spelling reaches it — got {_f_ensures(result)}" + ) + + +@pytest.mark.parametrize("spelling", sorted(_IMP_CALLERS)) +def test_1399_the_demotion_still_names_the_import_it_came_from( + tmp_path: Path, spelling: str, +) -> None: + """A demotion this PR newly causes must not be one nobody can act on. + + #1399's finding 4 was that an importer's E534 named nothing: the E504 + identifying the culprit belongs to the library's run, which this one + discards. #1402 fixed that for the direct spelling by citing the site as + it consults the manifest — at the place the fact is withheld. This PR + withholds in two more places where that consult has long since happened + (a `let`-bound value is a slot reference; a forwarder is a local call), + so the citation is carried ON the value instead, and across the forwarder + hop with it. Without that, the two spellings would demote with the + generic text and re-open the finding. + """ + result = _verify_with_lib(tmp_path, _IMP_CALLERS[spelling]) + e534 = [w for w in result["warnings"] if w.get("error_code") == "E534"] + assert len(e534) == 1, [w.get("error_code") for w in result["warnings"]] + text = e534[0]["description"] + assert "oplib::mk" in text, ( + f"{spelling}: the demotion names no culprit, so the reader is told " + f"only that something somewhere was not established — {text}" + ) + assert "oplib.vera" in text and "E506" in text, text + + +# --------------------------------------------------------------------------- +# #1418 review F1 — the value the SMT layer LOST still carries its taint +# --------------------------------------------------------------------------- + +# Where translation fails, a fresh stand-in constant replaces the value and +# the recorded provenance is severed — while every reader still takes the +# payload refinement off the binding's DECLARED type. That is #1363's +# asymmetry one layer down, and it is carrier-dependent, which is what made +# it easy to miss: over an `Option` payload the identical tuple spelling +# translates and demotes correctly, so only a carrier whose binding falls to +# `_fresh_opaque_slot` exhibits it. +_TUPLE_LAUNDER = """{ + let @Tuple, Int> = Tuple(mk(@Float64.0), 1); + let Tuple<@Option, @Int> = @Tuple, Int>.0; + match @Option.0 { +""" + _ARMS + """ + } +} +""" + +_F1_BODIES = { + # A `let` the SMT layer cannot translate: the stand-in is minted by + # `_fresh_opaque_slot`, and the destructure projects out of it. + "tuple_destructure": _F + _TUPLE_LAUNDER, + # An array literal: its constant is related to its elements only by + # axiom, so the occurrence walk cannot reach the element's term. + "array_index": _F + "{\n let @Array> = [mk(@Float64.0)];\n" + " match @Array>.0[0] {\n" + + _ARMS + "\n }\n}\n", +} + +#: BOTH HALVES AT ONCE: a lost value behind a forwarder, so the inter-function +#: taint has to survive the mint too. It lives outside `_F1_BODIES` because +#: it launders through an ARRAY rather than a tuple: an array relates to its +#: elements by axiom, so the value is genuinely LOST and the stand-in's +#: inheritance is what carries the disclosure across, which is the thing this +#: pair is for. +#: +#: It briefly carried `Option`, to make the forwarder record no +#: obligation of its own. #1412 ended both halves of that: a `@Nat` payload +#: narrowing is now GUARDED, so it discloses nothing at all, and a forwarder +#: publishing any refinement is obligated for it — there is no longer a +#: carrier that discloses while its forwarder stays silent. That the mint is +#: still load-bearing here is therefore asserted the only way left, by +#: measurement: reverting the stand-in's inheritance takes `f` back to +#: `verified`, which is what `M_mint` checks. +_F1_FORWARDER = """type PosInt = { @Int | @Int.0 > 0 }; + +private fn mk(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(%s) +} + +private fn warr(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + let @Array> = [mk(@Float64.0)]; + @Array>.0[0] +} + +public fn f(@Float64 -> @Int) + requires(true) + ensures(@Int.result > 0) + effects(pure) +{ + match warr(@Float64.0) { + Some(@PosInt) -> @PosInt.0, + None -> 41 + } +} +""" + + +def test_1418_f1_a_lost_value_behind_a_clean_forwarder_still_carries_it( + tmp_path: Path, +) -> None: + """The mint and the forwarder hop, composed — and the mint load-bearing. + + `tier3`/E534 here; with the stand-in's inheritance reverted it goes back + to `verified`, which is what makes this a third cell `M_mint` reds rather + than a third cell that happens to pass. + """ + src = _F1_FORWARDER % "float_to_int(@Float64.0)" + result = _verify(tmp_path, src) + assert result["ok"] is True, result.get("diagnostics") + statuses = [(o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"]] + assert ("refine_bind", "tier3_unguarded", "E506") in statuses, statuses + assert _f_ensures(result) == ("tier3", "E534"), statuses + _assert_refused(_run(tmp_path, src)) + + +def test_1418_f1_a_lost_clean_value_behind_a_forwarder_still_proves( + tmp_path: Path, +) -> None: + """The control: losing a value is not itself a disclosure.""" + src = _F1_FORWARDER % "7" + result = _verify(tmp_path, src) + assert result["ok"] is True, result.get("diagnostics") + assert _f_ensures(result) == ("verified", None), [ + (o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"] + ] + out = _run(tmp_path, src) + assert "violation" not in out, out[-400:] + assert out.strip().split()[-1] == "7", out[-400:] + + +@pytest.mark.parametrize("shape", sorted(_F1_BODIES)) +def test_1418_f1_a_lost_value_still_carries_its_disclosure( + tmp_path: Path, shape: str, +) -> None: + """A stand-in inherits the disclosure of the expression it replaces. + + Each of these was `verified` at Tier 1 while `vera run --fn f -- -7.0` + refuted the postcondition — on the pre-#1402 base, on this PR's first + head, and on the rebase — because the gate compared a term the disclosed + call never reached. The repair is at the mint, not at the reader: the + stand-in is recorded as a disclosed value, so every reader's gate answers + True for it without any of them learning about opaque slots. + """ + source = _POSINT + _MK_DISCLOSED + _F1_BODIES[shape] + result = _verify(tmp_path, source) + assert result["ok"] is True, result.get("diagnostics") + assert ("refine_bind", "tier3_unguarded", "E506") in [ + (o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"] + ], "the producer did not disclose, so this cell measures nothing" + assert _f_ensures(result) == ("tier3", "E534"), _f_ensures(result) + out = _run(tmp_path, source) + _assert_refused(out, f"{shape}: ") + + +@pytest.mark.parametrize("shape", sorted(_F1_BODIES)) +def test_1418_f1_a_lost_clean_value_still_proves( + tmp_path: Path, shape: str, +) -> None: + """The over-rejection control: losing the value is not itself a demotion. + + A stand-in is minted for the clean producer's binding too, so a fix that + tainted every opaque slot would pass the cells above and destroy Tier-1 + verification for every untranslatable `let` in the language. + """ + source = _POSINT + _MK_CLEAN + _F1_BODIES[shape] + result = _verify(tmp_path, source) + assert result["ok"] is True, result.get("diagnostics") + assert _f_ensures(result) == ("verified", None), _f_ensures(result) + out = _run(tmp_path, source) + assert "violation" not in out, out[-400:] + assert out.strip().split()[-1] == "7", out[-400:] # exact, not a suffix + + +# --------------------------------------------------------------------------- +# #1418 review F3 — a shared bare name must not demote a clean caller +# --------------------------------------------------------------------------- + +def _collide_source(second_helper: str) -> str: + """Two top-level functions, each with its own `where` helper: one + forwarding the disclosed producer, one forwarding the clean one.""" + return _POSINT + _MK_DISCLOSED + """ +private fn mk_ok(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(7) +} + +public fn tainted(@Float64 -> @Int) + requires(true) + ensures(@Int.result > 0) + effects(pure) +{ + match h(@Float64.0) { +""" + _ARMS + """ + } +} +where { + fn h(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + mk(@Float64.0) + } +} +""" + _F + "{\n match " + second_helper + "(@Float64.0) {\n" + _ARMS + """ + } +} +where { + fn """ + second_helper + """(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + mk_ok(@Float64.0) + } +} +""" + + +#: Two owners, two helpers of the SAME bare name, and NO forwarding: each +#: helper discloses (or does not) through an obligation of its OWN. The +#: `_collide_source` family reaches the disclosed set through +#: `_result_disclosed_fns` — the result-derived half — so it cannot tell +#: whether the obligation-derived half is scoped too. This one contains no +#: `mk` at all, so the ONLY route into the set is `disclosed_fn_names`. +_F3_OWN_OBLIGATION = """type PosInt = { @Int | @Int.0 > 0 }; + +public fn tainted(@Float64 -> @Int) + requires(true) + ensures(@Int.result > 0) + effects(pure) +{ + match h(@Float64.0) { + Some(@PosInt) -> @PosInt.0, + None -> 41 + } +} +where { + fn h(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + Some(float_to_int(@Float64.0)) + } +} + +public fn f(@Float64 -> @Int) + requires(true) + ensures(@Int.result > 0) + effects(pure) +{ + match h(@Float64.0) { + Some(@PosInt) -> @PosInt.0, + None -> 41 + } +} +where { + fn h(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + Some(7) + } +} +""" + + +def test_1418_f3_the_obligation_derived_half_is_scoped_too( + tmp_path: Path, +) -> None: + """The other half of the union, isolated — no forwarding anywhere. + + The disclosed set is the UNION of two derivations: the obligation-derived + `disclosed_fn_names` and the result-derived `_result_disclosed_fns`. F3 + scoped the second. The first went on keying a ``where`` helper by its + bare `fn_name`, which means a different function in every owner, so one + owner's disclosing helper demoted another owner's clean caller. + + Measured, not inferred: this shape reports BOTH callers `tier3`/E534 on + `release/v0.2.0` at `212f1a1d` AND at the tip `35ff4def`, with this branch + absent. So the defect is not #1420's — it was latent in that half from + the start, reachable whenever a helper carried a disclosing obligation of + its own. What #1420 changed is the REACH: obligating a helper's return + made a merely FORWARDING helper carry one too, which is what turned + `test_1418_f3_a_shared_helper_name_does_not_demote_a_clean_caller[h]` red + on the rebase and is why both cells are needed — that one goes green + again if only the result-derived half is scoped, and this one does not. + + Both halves now spell a helper's key with one function, `disclosed_key`, + since a set consulted as a union cannot have two spellings for a member. + """ + result = _verify(tmp_path, _F3_OWN_OBLIGATION) + assert result["ok"] is True, result.get("diagnostics") + statuses = [(o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"]] + assert ("refine_bind", "tier3_unguarded", "E506") in statuses, ( + f"the disclosing helper did not disclose, so this measures nothing " + f"about the obligation-derived half — {statuses}" + ) + ensures = [(o["status"], o.get("error_code")) for o in result["obligations"] + if o["kind"] == "ensures" and o["description"] == "@Int.result > 0"] + assert ensures == [("tier3", "E534"), ("verified", None)], ( + f"the owner whose helper discloses must demote and the other must " + f"not — got {ensures}" + ) + + +@pytest.mark.parametrize("second_helper", ["h", "h2"]) +def test_1418_f3_a_shared_helper_name_does_not_demote_a_clean_caller( + tmp_path: Path, second_helper: str, +) -> None: + """Keyed by scope, so a bare name shared across owners is not shared. + + `_result_disclosed_fns` was keyed by `decl.name`, and a `where` helper's + bare name means a different function in every top-level owner — so one + owner's tainted helper took the other owner's clean caller down with it + (#1418 review F3). A completeness loss rather than a soundness one, but + a loss, and one this PR introduced by extending the set to forwarders. + + Both parametrisations must give the same answer: the collision is now + settled by scope, so renaming the helper changes nothing. + """ + result = _verify(tmp_path, _collide_source(second_helper)) + assert result["ok"] is True, result.get("diagnostics") + ensures = [(o["status"], o.get("error_code")) for o in result["obligations"] + if o["kind"] == "ensures" and o["description"] == "@Int.result > 0"] + assert ensures == [("tier3", "E534"), ("verified", None)], ( + f"helper named {second_helper!r}: the tainted caller must demote and " + f"the clean one must not — got {ensures}" + ) + + +_NESTED_HELPER = _POSINT + _MK_DISCLOSED + _F + """{ + match h1(@Float64.0) { +""" + _ARMS + """ + } +} +where { + fn h1(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + h2(@Float64.0) + } + where { + fn h2(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + mk(@Float64.0) + } + } +} +""" + + +def test_1418_a_nested_helper_is_keyed_under_the_top_level_owner( + tmp_path: Path, +) -> None: + """Two levels of `where`, and the scope key has to agree at both. + + `enclosing` is built by APPENDING each parent, so `f -> h1 -> h2` gives + `h2` the chain `(f, h1)` — the OUTERMOST is index 0. Keying on the last + element recorded `h2` under `h1$where$h2` while `h1`, whose own chain is + `(f,)`, looked it up as `f$where$h2`. The miss was in the unsound + direction: `h1` discharged from `h2`'s disclosed result, `f` from + `h1`'s, and the whole chain kept Tier 1 (CodeRabbit, PR #1418). + + One owner per top-level function is the point of the key, so this fixture + is the minimum that can tell the two readings apart — a single level of + nesting cannot, because there `enclosing[0] is enclosing[-1]`. + """ + result = _verify(tmp_path, _NESTED_HELPER) + assert result["ok"] is True, result.get("diagnostics") + assert ("refine_bind", "tier3_unguarded", "E506") in [ + (o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"] + ], "the producer did not disclose, so this cell measures nothing" + assert _f_ensures(result) == ("tier3", "E534"), ( + f"a disclosed value forwarded through two levels of `where` helper " + f"must still demote its caller — got {_f_ensures(result)}" + ) + + +# --------------------------------------------------------------------------- +# #1418 review G1 — a forwarder INSIDE an imported module is disclosed too +# --------------------------------------------------------------------------- + +# #1402's manifest is what an importer asks about a module it does not verify, +# and it was built from `disclosed_fn_names(obligations)` alone. A forwarder +# makes no claim and so records no obligation, so a forwarder inside the +# LIBRARY was invisible while the same three declarations in one file demoted +# correctly — the rule cannot depend on which side of an import the forwarder +# sits. The manifest now emits the union of the obligation-derived set and +# the result-derived one, which is the same union `_disclosed_fn_names` takes +# on this side. +# --------------------------------------------------------------------------- +# #1418 review G1/J1 — a forwarder INSIDE an imported module publishes too +# --------------------------------------------------------------------------- + +# #1399's manifest is what an importer asks about a module it does not verify, +# and built from `disclosed_fn_names(obligations)` alone it cannot see a +# FORWARDER: a function whose declared return is the SAME refined type as its +# callee's NARROWS nothing, so #1412 — which obligates narrowings — gives it no +# obligation to be found by. +# +# This was removed once, on the argument that #1412 had closed the gap: a +# forwarder either publishes the refinement and is obligated for it, or drops +# it and hands on no fact. The second half holds. The FIRST IS FALSE, and a +# survey of six carriers did not show it, because a survey can only ever be +# evidence about the carriers surveyed (#1418 review J1). +# +# The carrier that shows it is a HANDLER-CLAUSE `@Nat` payload narrowing: the +# handler is declared `Exn`, so `throw`'s payload is an `@Int`, and the +# clause pattern `throw(@Nat)` narrows it into a `@Nat` slot. That site is +# #1362's category, which #1412's guards do not cover, so it stays +# `nat_bind`/`tier3_unguarded`/E504 — and `wrap` forwarding it publishes no +# refinement of its own. +# +# THE ONE-FILE ORACLE IS THE POINT. The same three declarations in one file +# demote; across an import they did not. So the cells below assert EQUALITY +# with that oracle rather than a literal status: if the rule changes what a +# disclosed forwarder does, both sides move together or the cell fails. +_J1_LIB = """public fn mk(@Int -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + int_to_nat(handle[Exn] { + throw(@Nat) -> { nat_to_int(@Nat.0) } + } in { + throw(@Int.0) + }) +} + +public fn wrap(@Int -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + mk(@Int.0) +} +""" + +_J1_MID = """import lib; + +public fn reexport(@Int -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + lib::wrap(@Int.0) +} +""" + +_J1_USE = """ +public fn use_it(@Int -> @Int) + requires(true) + ensures(@Int.result >= 0) + effects(pure) +{ + match %s(@Int.0) { + Some(@Nat) -> nat_to_int(@Nat.0), + None -> 0 + } +} +""" + +_J1_ONEFILE = _J1_LIB + _J1_USE % "wrap" + + +def _j1_ensures(result: dict) -> tuple[str, str | None]: + hits = [o for o in result["obligations"] + if o["kind"] == "ensures" and o["description"] == "@Int.result >= 0"] + assert len(hits) == 1, [ + (o["kind"], o["description"], o["status"]) for o in result["obligations"] + ] + return hits[0]["status"], hits[0].get("error_code") + + +def _j1_importer(tmp_path: Path, callee: str, *, mid: bool = False) -> dict: + (tmp_path / "lib.vera").write_text(_J1_LIB, encoding="utf-8") + if mid: + (tmp_path / "mid.vera").write_text(_J1_MID, encoding="utf-8") + imp = "import mid;\n" if mid else "import lib;\n" + return _verify(tmp_path, imp + _J1_USE % callee, name="main.vera") + + +@pytest.mark.parametrize( + "callee,mid", + [("lib::mk", False), ("lib::wrap", False), ("mid::reexport", True)], + ids=["direct", "forwarder", "two_hops"], +) +def test_1418_j1_an_imported_forwarder_publishes_its_disclosure( + tmp_path: Path, callee: str, mid: bool, +) -> None: + """The importer agrees with the one-file oracle, whichever route it takes. + + Measured with the manifest publishing the obligation-derived set alone: + `lib::mk` `tier3`/E534, `lib::wrap` **`verified`**, `mid::reexport` + **`verified`**, and the same declarations in ONE file `tier3`/E534. The + same value, and the verdict turned on which side of an import the + forwarder sat. + + The exhibit is that ASYMMETRY, not a runtime refutation: `int_to_nat` + filters a negative into `None`, so the program returns 0 and keeps its + postcondition. What is wrong is a Tier-1 claim resting on a fact the same + run reported as neither proved nor guarded — which the in-module half of + this rule already refuses. + """ + # The premise: the library discloses exactly once, at the handler clause. + (tmp_path / "lib.vera").write_text(_J1_LIB, encoding="utf-8") + lib = _verify(tmp_path, _J1_LIB, name="lib.vera") + disclosing = [(o["kind"], o["status"], o.get("error_code")) + for o in lib["obligations"] + if o["status"] == "tier3_unguarded" + or (o["status"] == "tier3" and o.get("error_code") == "E534")] + assert disclosing == [("nat_bind", "tier3_unguarded", "E504")], ( + f"the library must disclose exactly once, at the handler-clause " + f"`@Nat` payload bind — got {disclosing}" + ) + + result = _j1_importer(tmp_path, callee, mid=mid) + assert result["ok"] is True, result.get("diagnostics") + assert _j1_ensures(result) == ("tier3", "E534"), ( + f"{callee}: a disclosed value reached the importer, so its " + f"postcondition is a Tier-3 truth — got {_j1_ensures(result)}" + ) + + +@pytest.mark.parametrize( + "callee,mid", + [("lib::mk", False), ("lib::wrap", False), ("mid::reexport", True)], + ids=["direct", "forwarder", "two_hops"], +) +def test_1418_j1_the_import_boundary_changes_nothing( + tmp_path: Path, callee: str, mid: bool, +) -> None: + """EQUALITY with the one-file oracle, not a literal status. + + A cell asserting `tier3`/E534 outright would go red for a change that + moved BOTH sides — the rule being adjusted, rather than broken. What must + hold is that splitting a program across files changes nothing, so the + oracle is computed here and compared. + """ + oracle = _j1_ensures(_verify(tmp_path, _J1_ONEFILE, name="oracle.vera")) + across = _j1_ensures(_j1_importer(tmp_path, callee, mid=mid)) + assert across == oracle, ( + f"{callee}: the same declarations report {across} across an import " + f"and {oracle} in one file — a verdict that depends on which side of " + f"an import a forwarder sits on" + ) + + +# --------------------------------------------------------------------------- +# #1418 review G2 — the `_set_fn_scope` hoist, pinned +# --------------------------------------------------------------------------- + +# `_verify_fn`'s generic branch returns BEFORE the old assignment site, and it +# translates a body on the way out (`_check_generic_refined_return`) with the +# disclosure hook installed. So a generic read the PREVIOUS function's +# `where` helpers, and `_local_fn_names_in_scope()` is what decides whether a +# bare call reaches an IMPORT or a local name — which makes the stale read +# reachable only across an import, and unsound in one direction: a leftover +# helper name makes an imported disclosing callee look local, the manifest is +# never consulted, and the disclosure is suppressed. +# +# Ordering is the fixture. `holder` is verified FIRST and declares a helper +# named `mk`, so `mk` is left in `_scope_fn_names`; the generic `g` that +# follows has no helper of its own and its bare `mk` is `oplib::mk`, the +# disclosing import. With the binding hoisted to the entry of `_verify_fn`, +# `g` starts from its own (empty) scope and the manifest is consulted. +_G2_LIB = _POSINT + """ +public fn mk(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(float_to_int(@Float64.0)) +} +""" + +_G2_STALE_SCOPE = "import oplib;\n" + _POSINT + """ +public fn holder(@Float64 -> @Int) + requires(true) + ensures(true) + effects(pure) +{ + match mk(@Float64.0) { + Some(@PosInt) -> @PosInt.0, + None -> 41 + } +} +where { + fn mk(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + Some(9) + } +} + +public forall fn g(@T, @Float64 -> @PosInt) + requires(true) + ensures(true) + effects(pure) +{ + match mk(@Float64.0) { + Some(@PosInt) -> @PosInt.0, + None -> 41 + } +} +""" + + +def test_1418_g2_a_generic_refined_return_reads_its_own_scope( + tmp_path: Path, +) -> None: + """The generic path sees ITS OWN helpers, not the previous function's. + + A generic's concrete refined return is checked on a path that returns + before the rest of `_verify_fn` runs, so the per-function scope state has + to be bound at the ENTRY or that path reads whatever the last function + left behind. Reverting the hoist leaves the whole suite green, which is + why this cell exists; it reds on that revert. + + Asserted on the outcome, not the mechanism: `g`'s bare `mk` is the + disclosing IMPORT, so its refined return must not come back `verified`. + A stale scope carrying `holder`'s helper of the same name makes the call + look local, skips the manifest, and suppresses the disclosure. + """ + (tmp_path / "oplib.vera").write_text(_G2_LIB, encoding="utf-8") + result = _verify(tmp_path, _G2_STALE_SCOPE, name="main.vera") + assert result["ok"] is True, result.get("diagnostics") + generic = [(o["status"], o.get("error_code")) for o in result["obligations"] + if o["kind"] == "refine_bind" + and o.get("description") == ""] + assert generic == [("tier3", "E506")], ( + f"the generic's refined return proved from an imported disclosure " + f"the previous function's scope hid — got {generic}" + ) + + +# --------------------------------------------------------------------------- +# #1418 review G3 — the F3 residual, pinned as measured +# --------------------------------------------------------------------------- + +_G3_RESIDUAL = _POSINT + _MK_DISCLOSED + """ +private fn mk_ok(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(7) +} +""" + _F + "{\n match h(@Float64.0) {\n" + _ARMS + "\n }\n}\n" + ( + """where { + fn h(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + mk_ok(@Float64.0) + } + + fn inner(@Float64 -> @Int) + requires(true) + ensures(true) + effects(pure) + { + match h(@Float64.0) { +""" + _ARMS + """ + } + } + where { + fn h(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) + { + mk(@Float64.0) + } + } +} +""") + + +def test_1418_g3_the_scope_key_residual_errs_toward_demotion( + tmp_path: Path, +) -> None: + """Two helpers under ONE owner still share a key — pinned, not claimed fixed. + + `_result_disclosed_key` qualifies a `where` helper by its top-level owner, + which separates helpers in DIFFERENT owners. Two helpers under the same + owner — here `h` (clean) beside a nested `h2` (disclosed) — still share + that owner, so the outer caller reading the CLEAN helper is demoted along + with the tainted one. + + That is the safe direction: a Tier-3 report where a Tier-1 proof was + available, never the reverse. Narrowing it further means carrying the + whole lexical chain as the key rather than its root, which is a bigger + change than the soundness fix needed. Pinned so the cost is a + measurement rather than a claim, and so narrowing it later is visible. + """ + result = _verify(tmp_path, _G3_RESIDUAL) + assert result["ok"] is True, result.get("diagnostics") + assert _f_ensures(result) == ("tier3", "E534"), ( + f"the residual moved — if that was intended, this cell records the " + f"state it moved from: {_f_ensures(result)}" + ) + # The safe direction, demonstrated: the value `f` actually returns is the + # CLEAN helper's, so the demotion costs a proof and never soundness. + out = _run(tmp_path, _G3_RESIDUAL) + assert "violation" not in out, out[-400:] + assert out.strip().split()[-1] == "7", out[-400:] + + +#: Reading a disclosed value is not by itself a demotion. The gate withholds +#: the facts; `check_valid` offers them back only after a proof WITHOUT them +#: fails. So a goal over a disclosed value that never needed the withheld +#: fact keeps its Tier 1 — `x - x == 0` holds for every `x`, disclosed or not. +_INDEPENDENT_GOAL = """type PosInt = { @Int | @Int.0 > 0 }; + +type Zero = { @Int | @Int.0 == 0 }; + +private fn mk(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(float_to_int(@Float64.0)) +} + +public fn f(@Float64 -> @Int) + requires(true) + ensures(true) + effects(pure) +{ + match mk(@Float64.0) { + Some(@PosInt) -> { + let @Zero = @PosInt.0 - @PosInt.0; + @Zero.0 + }, + None -> 0 + } +} +""" + + +def test_1418_a_goal_not_needing_the_withheld_fact_stays_tier_1( + tmp_path: Path, +) -> None: + """Withholding is not demotion: only a goal that NEEDS the fact moves. + + The completeness bound on the whole mechanism, and the one a taint keyed + on "did this value come from a disclosed call" rather than on "did the + proof use a withheld fact" would fail. `@PosInt.0 - @PosInt.0` narrows + into `Zero` over a value the run disclosed, and proves at Tier 1 because + `x - x == 0` needs nothing the gate took away. + + Raised against the spec wording in review of this PR — which said such a + reader is Tier 3 "when the value they read from was disclosed", stating + more than the implementation does — and checked here rather than argued. + """ + result = _verify(tmp_path, _INDEPENDENT_GOAL) + assert result["ok"] is True, result.get("diagnostics") + statuses = [(o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"]] + # The premise: the producer really did disclose. + assert ("refine_bind", "tier3_unguarded", "E506") in statuses, statuses + # The claim: the reader over that disclosed value still proves. + binds = [o for o in result["obligations"] + if o["kind"] == "refine_bind" + and o["description"] == "@PosInt.0 - @PosInt.0"] + assert len(binds) == 1, statuses + assert (binds[0]["status"], binds[0].get("error_code")) == ("verified", None), ( + f"a goal that never needed the withheld fact must keep Tier 1 — " + f"{statuses}" + ) + + +#: THE #1431 REVIEWER'S LITERAL SPELLING, which could not be a cell until now. +#: A `None` arm beside a `Some()` one used to die with an E699 sort +#: mismatch before a single obligation was emitted — that crash being #1424, +#: which #1431 fixed. With #1431 in the base the shape translates, so the +#: construction rule is pinned on the exact program the review raised rather +#: than only on the carriers chosen to dodge the crash. +_REBUILT_LITERAL = _POSINT + """ +private fn mk(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(%s) +} + +private fn rebuild(@Float64 -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + match mk(@Float64.0) { + Some(@PosInt) -> Some(@PosInt.0), + None -> None + } +} +""" + _F + "{\n match rebuild(@Float64.0) {\n" + _ARMS + "\n }\n}\n" + + +def test_1418_j3_the_literal_rebuilt_spelling_is_disclosed( + tmp_path: Path, +) -> None: + """`Some(@PosInt.0)` beside a `None` arm — the shape #1431 unblocked. + + The occurrence walk needs no rule for it: a constructor application + containing a projection of a disclosed value contains that value. What + changed is only that the program now reaches the verifier at all. + """ + src = _REBUILT_LITERAL % "float_to_int(@Float64.0)" + result = _verify(tmp_path, src) + assert result["ok"] is True, result.get("diagnostics") + statuses = [(o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"]] + assert ("refine_bind", "tier3_unguarded", "E506") in statuses, statuses + assert _f_ensures(result) == ("tier3", "E534"), statuses + _assert_refused(_run(tmp_path, src)) + + +def test_1418_j3_the_literal_rebuilt_spelling_of_a_clean_value_proves( + tmp_path: Path, +) -> None: + """The control: rebuilding is not itself a disclosure.""" + src = _REBUILT_LITERAL % "7" + result = _verify(tmp_path, src) + assert result["ok"] is True, result.get("diagnostics") + assert _f_ensures(result) == ("verified", None), [ + (o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"] + ] + out = _run(tmp_path, src) + assert "violation" not in out, out[-400:] + assert out.strip().split()[-1] == "7", out[-400:] + + +def test_1418_a_value_rebuilt_from_a_disclosed_component_is_disclosed() -> None: + """CONSTRUCTED-from is covered by the same walk as PROJECTED-from. + + The rule says a value is disclosed when it is, or is projected from, a + disclosed call's result. Rebuilding — `Some(@PosInt.0)` in a match arm + over a disclosed producer — is that situation one step on: the new + payload's fact rests on the disclosed one. It needs no separate rule + because the walk asks by OCCURRENCE, so a constructor application + containing the projection contains the disclosed term. + + A unit cell BESIDE the end-to-end ones, not instead of them: the + `rebuild_ctor` / `rebuild_ctor2` spellings and + `test_1418_a_single_arm_rebuild_is_disclosed` carry the whole-program + shape. What only a unit can pin is the walk's own answer, independent of + which carrier the program happened to use. + + Only the LITERAL `None`-arm spelling the #1431 reviewer wrote — + `match mk(x) { Some(@PosInt) -> Some(@PosInt.0), None -> None }` — cannot + be an end-to-end cell here, because on this revision it dies with an E699 + sort mismatch before any obligation is emitted. That is + [#1421](https://github.com/aallan/vera/issues/1421)'s bug, not this one, + and it was measured on four trees rather than argued: + + | tree | that spelling | + | ----------------------- | ------------------ | + | `release/v0.2.0` base | E699 | + | #1421's sort fix only | `verified`, run refutes | + | this branch only | E699 | + | both | `tier3`/E534 | + + So the two fixes are orthogonal and compose: #1421 decides whether the + term can be BUILT, this branch decides which facts may DISCHARGE a goal + over it. Note the second row — the sort fix alone makes a spelling that + used to crash into one that falsely proves, so it wants this branch under + it. + """ + import z3 + + from vera.smt import SmtContext + + smt = SmtContext() + disclosed = z3.Int("_call_mk_1") + smt._disclosed_terms.append(disclosed) + + project = z3.Function("Option_Some_0", z3.IntSort(), z3.IntSort()) + rebuild = z3.Function("Some", z3.IntSort(), z3.IntSort()) + + payload = project(disclosed) # @PosInt.0 + rebuilt = rebuild(payload) # Some(@PosInt.0) + reread = project(rebuilt) # the consumer's own projection + + assert smt.term_is_disclosed(disclosed) is True + assert smt.term_is_disclosed(payload) is True, "projected-from" + assert smt.term_is_disclosed(rebuilt) is True, "constructed-from" + assert smt.term_is_disclosed(reread) is True, "and back out again" + # The control that keeps this from being vacuous: a term with no + # disclosed component answers False however deeply it is nested. + clean = rebuild(project(z3.Int("_call_mk_ok_1"))) + assert smt.term_is_disclosed(clean) is False + + +# A carrier with ONE constructor, so `rebuild`'s match has a single arm and +# there is no join of any kind. The `rebuild_ctor` spellings above both join +# two arms, and a join is exactly the thing `ite_join` already exercises — if +# the demotion there came from the join rather than from the construction, +# these two cells are where that shows, because here there is no join to +# blame. `mk` builds the payload with `float_to_int` as everywhere else, and +# an ADT payload is guarded by codegen nowhere, so the contract is genuinely +# refutable. +_BOX = """type PosInt = { @Int | @Int.0 > 0 }; + +private data Box { + Wrap(PosInt) +} + +private fn mk(@Float64 -> @Box) + requires(true) + ensures(true) + effects(pure) +{ + Wrap(%s) +} + +private fn rebuild(@Float64 -> @Box) + requires(true) + ensures(true) + effects(pure) +{ + match mk(@Float64.0) { + Wrap(@PosInt) -> Wrap(@PosInt.0) + } +} + +public fn f(@Float64 -> @Int) + requires(true) + ensures(@Int.result > 0) + effects(pure) +{ + match rebuild(@Float64.0) { + Wrap(@PosInt) -> @PosInt.0 + } +} +""" + + +def test_1418_a_single_arm_rebuild_is_disclosed(tmp_path: Path) -> None: + """Construction alone demotes — with no arm join anywhere in the program. + + On `release/v0.2.0` this is `verified` at Tier 1 and the compiled program + refutes it: the full soundness signature, on a shape with no `let`, no + wrapper, and no join — only a value pulled apart and put back together. + """ + src = _BOX % "float_to_int(@Float64.0)" + result = _verify(tmp_path, src) + assert result["ok"] is True, result.get("diagnostics") + statuses = [(o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"]] + assert ("refine_bind", "tier3_unguarded", "E506") in statuses, statuses + assert _f_ensures(result) == ("tier3", "E534"), statuses + # The claim the status is ABOUT: the program really does break it. + out = _run(tmp_path, src) + _assert_refused(out) + + +def test_1418_a_single_arm_rebuild_of_a_clean_value_still_proves( + tmp_path: Path, +) -> None: + """The control: same construction, nothing disclosed, still Tier 1. + + Without this a fix that demoted every rebuild would pass the cell above. + """ + src = _BOX % "7" + result = _verify(tmp_path, src) + assert result["ok"] is True, result.get("diagnostics") + assert _f_ensures(result) == ("verified", None), [ + (o["kind"], o["status"], o.get("error_code")) + for o in result["obligations"] + ] + out = _run(tmp_path, src) + assert "violation" not in out, out[-400:] + assert out.strip().split()[-1] == "7", out[-400:] diff --git a/vera/README.md b/vera/README.md index bfab7a08c..de7031fe0 100644 --- a/vera/README.md +++ b/vera/README.md @@ -92,10 +92,10 @@ execute(compile_result, ...) # → run WASM via wasmtime | ` calls.py` | 1,631 | | Function/constructor/module/ability calls | | | ` control.py` | 929 | | If/match, patterns, effect handlers | | | `resolver.py` | 332 | Resolve | Module path resolution, parse cache | `ModuleResolver` | -| `disclosure.py` | 446 | Verify | Per-module disclosed-function manifests: each module's own verification emits the set `disclosed_fn_names` derives, keyed by owner path and carrying the `DisclosureSite` the importer's E534 cites, so the #1363 demotion crosses an import (#1399); computed BOTTOM-UP over the import DAG so each module is verified once and nothing nests, and content-addressed on the module's own source + its closure's + the budget, which is what makes an edit to an imported module invalidate it | `ModuleDisclosureIndex`, `DisclosureSite` | +| `disclosure.py` | 513 | Verify | Per-module disclosed-function manifests: each module's own verification emits the set `disclosed_fn_names` derives, keyed by owner path and carrying the `DisclosureSite` the importer's E534 cites, so the #1363 demotion crosses an import (#1399); computed BOTTOM-UP over the import DAG so each module is verified once and nothing nests, and content-addressed on the module's own source + its closure's + the budget, which is what makes an edit to an imported module invalidate it | `ModuleDisclosureIndex`, `DisclosureSite` | | `monomorphize.py` | 3,891 | Resolve | Shared generic instantiation discovery + AST substitution (verifier and codegen); each clone's De Bruijn recount renders its binder names under the **origin module's** `AliasEnv`, the one its consumers rebuild the clone's scope with (#1208) | `substitute_type_vars()`, `resolve_type_alias()`, `canonicalize_type_aliases()` | | `regularity.py` | 413 | Type check / Verify | The ONE regular-recursion derivation (#1429), read PER TYPE ARGUMENT of a recursive occurrence: each must be a bare parameter of the enclosing declaration, passed along unchanged, or closed with respect to those parameters — an argument that wraps one inside another type constructor grows at every level and is refused; an occurrence of the declaration's own name must also keep its parameters in their original positions. Asked by TWO consumers that must not disagree — the checker refuses the declaration (`E129`), and the SMT layer declines to MODEL it, because `verify()` is a public entry point whose check-clean precondition a library caller can violate and the datatype-group closure has no fixed point when it is. A second copy would be free to drift into one consumer refusing what the other models. Groups are the strongly connected components of one field-reference graph, so `RegularityIndex` answers for a whole module from a single pass; `recursive_group()` is the straightforward reachability walk it is differentially tested against | `RegularityIndex`, `is_regular()`, `irregular_occurrence()`, `recursive_group()` | -| `smt.py` | 3,289 | Verify | Z3 translation layer; reads each callee's contract in the module that declared it (`_callee_contract_scope`), swapping the naming env its slots render against and the registry its bare-name calls resolve in as one `CalleeScope` (#1208, #1225) | `SmtContext`, `SlotEnv`, `CalleeScope` | +| `smt.py` | 3,846 | Verify | Z3 translation layer; reads each callee's contract in the module that declared it (`_callee_contract_scope`), swapping the naming env its slots render against and the registry its bare-name calls resolve in as one `CalleeScope` (#1208, #1225) | `SmtContext`, `SlotEnv`, `CalleeScope` | | `verifier.py` | 11,648 | Verify | Contract verification; owns the per-module registries every rendering goes through — an imported callee's contract and an imported generic's clone are named, resolved, and quoted in the module that **declared** them (#1208, #1220, #1225) | `verify()` | | `narrowing.py` | 192 | Verify | The ONE derivation of whether a value narrows into a `@Nat` slot, read by BOTH the verifier's `guarded` claim and codegen's guard emission so the two cannot drift (#1362); the type oracle is a parameter because the verifier reads the checker's semantic types while codegen reads declared names | `is_static_nat_typed()`, `has_underflow_leaf()`, `narrows_into_nat()` | | `wasm/` | 27,524 | Compile | WASM translation layer (package) | `WasmContext`, `WasmSlotEnv`, `StringPool` | @@ -120,9 +120,9 @@ execute(compile_result, ...) # → run WASM via wasmtime | ` └ html_serde.py` | 261 | | WASM memory marshalling for HtmlNode ADT | | | `markdown.py` | 751 | Compile | Python Markdown parser/renderer (§9.7.3 subset) | `parse_markdown()`, `render_markdown()`, `has_heading()`, `has_code_block()`, `extract_code_blocks()` | | `markdown_grammar.py` | 147 | Compile | The §9.7.3 grammar, read by BOTH runtimes: patterns, character classes, continuation widths, and the generated copy `runtime.mjs` carries | `PATTERNS`, `CONTINUATION_INDENT`, `fence_close()`, `trim()`, `js_grammar_block()` | -| `obligations/` | 785 | Verify | Reified proof obligations + warm incremental session (#222 A/B) | `ProofObligation`, `VerificationSession` | +| `obligations/` | 909 | Verify | Reified proof obligations + warm incremental session (#222 A/B) | `ProofObligation`, `VerificationSession` | | ` core.py` | 210 | | ProofObligation record: identity (content_key) + discharge outcome | | -| ` cache.py` | 219 | | Invalidation keys (structural/callee/context hashes), DischargeCache | | +| ` cache.py` | 219 | | Invalidation keys (structural/callee/context hashes), DischargeCache; `FnCacheEntry` also carries `result_disclosed`, the one datum a replay cannot recover from the cached diagnostics and obligations (#1407) | | | ` session.py` | 366 | | Warm-Z3 daemon: per-function replay vs re-verify in declaration order; clears the disclosed set per program and re-enters `_verify_source_fixpoint` for one program's fixpoint (#1363) | | | `lsp/` | 1,718 | Serve | Language Server Protocol over stdio (#222 C/D/E/F) | `create_server()`, `vera lsp` | | ` convert.py` | 218 | | Span/SourceLocation/LSP coordinate conversions, UTF-16 transcoding | | @@ -771,7 +771,7 @@ The `ERROR_CODES` dict in `errors.py` maps every code to a short description (17 ## Test Suite -Testing spans a **pytest suite** of 13,575 tests across 203 files: compiler-internals unit tests plus a **conformance suite** (253 programs in `tests/conformance/` validating every language feature against the spec) and **example programs** (43 end-to-end demos). The conformance suite is the definitive specification artifact; most programs target a single feature, though some (slot references, match, contracts) span several, and each serves as a minimal working example. +Testing spans a **pytest suite** of 13,686 tests across 204 files: compiler-internals unit tests plus a **conformance suite** (253 programs in `tests/conformance/` validating every language feature against the spec) and **example programs** (43 end-to-end demos). The conformance suite is the definitive specification artifact; most programs target a single feature, though some (slot references, match, contracts) span several, and each serves as a minimal working example. See **[TESTING.md](../TESTING.md)** for the comprehensive testing reference -- test file table, conformance suite details, compiler code coverage, language feature coverage, helper conventions, validation scripts, CI pipeline, and guidelines for adding tests. diff --git a/vera/disclosure.py b/vera/disclosure.py index 5700b36a7..8cc71ec97 100644 --- a/vera/disclosure.py +++ b/vera/disclosure.py @@ -434,6 +434,36 @@ def _verify_for_disclosure( # WHICH functions is the shared derivation's answer; the walk below only # decorates it with the obligation that earned each one, selected by the # same predicate so the two cannot disagree about what disclosed what. + # + # This loop decorates the OBLIGATION-derived half; the loop after it adds + # the RESULT-derived half (G1). A function is disclosed when its result + # is a disclosed value. Since #1412 that has ONE kind of evidence: an + # obligation of its own that was neither proved nor guarded. A forwarder + # used to make no claim and so record nothing, which made it invisible + # here while the same declarations in one file demoted correctly — so + # this emitted the union of the obligation-derived set with the + # result-derived one. #1412 then obligated a refined return at every + # position that publishes it, which closes that gap where it opens: a + # forwarder handing on a refined value carries its own unguarded + # obligation, and one that does NOT publish the refinement hands on no + # fact for a consumer to lean on. + # + # THE CLAIM IS BOUNDED BY WHAT WAS MEASURED, not by that argument. With + # the union reverted, no verdict moved across a forwarder dropping the + # refinement, one through a `where` helper, one returning a tuple + # carrying the payload, one two import hops away, and one in an + # `Exn`-declared function; and removing it changed no cell in the suite. + # + # #1412 does NOT guard every narrowing. `_NAT_CONSTRUCTION_GUARDED_SITES` + # is `{"tuple component"}`, so an ARRAY ELEMENT and a `Map` VALUE still + # disclose, by design (#1418 review J1). Neither reaches a consumer as a + # declared-type fact in any shape measured: an array's elements are + # modelled opaquely, so a consumer indexing one, passing it to a nested + # refinement, or re-narrowing it with a `let` is REFUTED (E500) rather + # than falsely proved, and a `Map` insert emits no narrowing obligation + # at all. If a shape is found where such a producer's disclosure DOES + # reach an importer through a forwarder, this is where the union goes + # back — for that case, with the reason on the DisclosureSite. names = disclosed_fn_names(result.obligations) manifest: ModuleManifest = {} for o in result.obligations: @@ -443,4 +473,41 @@ def _verify_for_disclosure( file=o.file or file, line=o.line, column=o.column, error_code=o.error_code or "", ) + # A forwarder that narrows nothing has no obligation to decorate, so the + # loop above skipped it (#1418 review J1). Cite the import behind it when + # there is one, and otherwise the forwarder's own declaration — the + # position a reader of the importing diagnostic should open, from which + # the local disclosure it hands on is one call away and carries its own + # E504/E506 in that module's run. + for name, sites in result.result_disclosed.items(): + if name in manifest: + continue + if sites: + manifest[name] = sites[0] + continue + manifest[name] = DisclosureSite( + module=mod.path, fn_name=name, file=file, + line=_decl_line(mod, name), column=0, error_code="", + ) return manifest + + +def _decl_line(mod: ResolvedModule, name: str) -> int: + """The line *name* is declared on in *mod*, or 0 when it cannot be found. + + Walks the declarations rather than trusting a registry, because a + forwarder may be a ``where`` helper, which the flat last-wins registries + cannot name (#1418 review G1). + """ + from vera import ast + + stack = [ + tld.decl for tld in mod.program.declarations + if isinstance(tld.decl, ast.FnDecl) + ] + while stack: + decl = stack.pop() + if decl.name == name and decl.span is not None: + return int(decl.span.line) + stack.extend(decl.where_fns or ()) + return 0 diff --git a/vera/obligations/cache.py b/vera/obligations/cache.py index d209ede77..b42438171 100644 --- a/vera/obligations/cache.py +++ b/vera/obligations/cache.py @@ -45,8 +45,8 @@ import hashlib -from dataclasses import dataclass, fields, is_dataclass -from typing import Iterator +from dataclasses import dataclass, field, fields, is_dataclass +from typing import Any, Iterator from vera import ast from vera.errors import Diagnostic @@ -183,10 +183,31 @@ class FnCacheEntry: :class:`~vera.verifier.VerifySummary` is *derived* from the assembled obligation stream at report-assembly time (#967), so no per-function summary deltas are cached — the cached ``obligations`` are the count. + + ``result_disclosed`` is the one datum that is NOT recoverable from the + two lists (#1407): a function that merely hands on a disclosed value + contributes no obligation saying so, and the cold path collects it while + translating the body — which a replay does not do. Left uncached, a + replayed wrapper would drop out of the disclosed set and the warm run + would prove at Tier 1 what the cold run demotes. + + It is the slice's WHOLE contribution — every key `_verify_fn` added to + `ContractVerifier._result_disclosed_fns` while verifying this + declaration, mapped to the import sites a caller's demotion should cite + (#1418 review F2). A bool about the top-level name was not enough: + verifying a declaration also verifies its `where` helpers, and a helper + that forwards a disclosed value is never itself a `decl.name` in the + session's loop, so the warm disclosed set omitted it and the fixpoint + settled one hop early — warm proving at Tier 1 exactly what cold demoted, + on one of the ten spellings. Caching the contribution rather than a fact + about the name means a future kind of contributor is carried by existing + code instead of needing a new field. An empty dict is a slice that + contributed nothing. """ diagnostics: list[Diagnostic] obligations: list[ProofObligation] + result_disclosed: dict[str, list[Any]] = field(default_factory=dict) class DischargeCache: diff --git a/vera/obligations/core.py b/vera/obligations/core.py index 757d3d9c8..152a6c4d6 100644 --- a/vera/obligations/core.py +++ b/vera/obligations/core.py @@ -156,6 +156,15 @@ class ProofObligation: #: obligation ``_record_obligation`` reifies carries one whenever the #: verifier was given a file at all. file: str | None = None + #: The TOP-LEVEL function owning this obligation's `where` helper, or ``""`` + #: for an obligation of a top-level function. `fn_name` alone is a helper's + #: bare name, which means a different function in every owner, so the + #: disclosed set keyed on it let one owner's tainted helper demote another + #: owner's clean caller (#1418 review F3). Deliberately NOT part of + #: `content_key`: the span and file already separate two helpers of the + #: same name, so hashing it would split cache entries without + #: distinguishing anything. + owner: str = "" def content_key(self) -> str: """Stable identity digest for this obligation. diff --git a/vera/obligations/session.py b/vera/obligations/session.py index 9913d5b6d..021485a1e 100644 --- a/vera/obligations/session.py +++ b/vera/obligations/session.py @@ -305,15 +305,29 @@ def _verify_source_fixpoint( if cached is not None: out_diags.extend(cached.diagnostics) out_obls.extend(cached.obligations) + # F2: the slice's whole contribution, `where` helpers with + # it. Seeded back onto the verifier as well as into the + # session's set, because a LATER fresh slice consults + # `_result_disclosed_fns` for the citation behind a forwarder + # and would otherwise see a hole where a replayed slice sat. + verifier._result_disclosed_fns.update(cached.result_disclosed) stats.replayed_fns += 1 continue d0 = len(verifier.errors) o0 = len(verifier.obligations) + before = dict(verifier._result_disclosed_fns) verifier._verify_fn(decl) + # F2: the DELTA this slice produced — the declaration itself and + # any `where` helper of it that forwards a disclosed value. + contributed = { + k: v for k, v in verifier._result_disclosed_fns.items() + if k not in before or before[k] != v + } entry = FnCacheEntry( diagnostics=list(verifier.errors[d0:]), obligations=list(verifier.obligations[o0:]), + result_disclosed=contributed, ) self._cache.put(key, entry) out_diags.extend(entry.diagnostics) @@ -338,7 +352,20 @@ def _verify_source_fixpoint( # exactly as the cold `verify_program` path derives it from its own — # so the warm and cold summaries agree by construction (the tier counts # can't drift from the obligations a consumer reads). - disclosed = disclosed_fn_names(out_obls) + # #1407: the same union `ContractVerifier._disclosed_fn_names` takes — + # the obligation stream says which functions failed to establish their + # own declared type, `result_disclosed` says which hand such a value + # on, and the fixpoint below needs both or it settles one hop early. + # ONE term, not two. The verifier's own map is the superset: a fresh + # slice's contribution is already in it, a replayed slice's is seeded + # back onto it above, and the imported-generic-clone pass — which runs + # AFTER this loop and verifies bodies of its own — reaches only it + # (CodeRabbit, PR #1418). Unioning the per-slice tally beside it was + # measured dead: mutating either term away killed nothing, because + # each covered the other. Keeping the superset alone leaves one term + # whose removal the warm cells do catch. + disclosed = (disclosed_fn_names(out_obls) + | frozenset(verifier._result_disclosed_fns)) if not disclosed <= self._disclosed: # Re-run knowing what this pass disclosed, exactly as the cold # `verify_program` fixpoint does. The set only grows, so this diff --git a/vera/smt.py b/vera/smt.py index 2782303f3..33ef95b20 100644 --- a/vera/smt.py +++ b/vera/smt.py @@ -9,6 +9,8 @@ from __future__ import annotations +import dataclasses + import contextlib import os import re @@ -536,6 +538,34 @@ def __init__( # that needs one is provable only from something this run admitted it # could not establish, which is a Tier-3 truth and not a Tier-1 proof. self._tainted_facts: list[z3.ExprRef] = [] + # #1406/#1407: the Z3 terms this function's DISCLOSED calls produced. + # Disclosure is a property of the VALUE, not of the syntax that names + # it: `let @T = mk(x); match @T.0 { … }` reaches the match as a slot + # reference and a forwarding wrapper reaches it as a call to a + # function carrying no obligation of its own, yet both hand the + # caller the very value `mk` failed to establish. Recording the term + # lets the taint follow it through every binding, projection and + # branch the SMT layer can see, without naming a single spelling. + self._disclosed_terms: list[z3.ExprRef] = [] + # #1399 x #1406: the CITATION sites that came with each recorded term, + # keyed by its Z3 ast id. An imported disclosure names the module and + # function the demotion should cite, and that name is known where the + # value is PRODUCED, not where its facts are finally read — a + # `let`-bound imported call is a slot reference by the time anything + # asks. Parking the site on the term is what lets the diagnostic + # still name the culprit, and lets it name only the culprit: a site is + # cited when the value carrying it is the one whose facts were + # withheld, not merely because the function called something. + self._disclosed_term_sites: dict[int, list[Any]] = {} + # Optional hook (injected by the verifier) answering whether a CALL + # node targets a function this run disclosed — the verifier owns that + # resolution (bare vs module-qualified, local shadows, and the + # imported module's manifest), so this layer asks rather than + # re-deriving it. Signature: (call_node) -> (bool, [site, ...]); + # the sites are the imported disclosures behind a True, handed over + # for the term rather than left on the verifier's live list. + # None when no verifier is driving (pure-SMT tests). + self._disclosed_call_hook: Any = None # Optional hook (injected by the verifier) returning the source-type # facts a constructor pattern's refined / @Nat sub-pattern bindings # carry, so a match arm body's call PRECONDITIONS see them (CR @@ -1670,6 +1700,12 @@ def _translate_array_lit( index_fn = self._get_index_fn(array_sort, element_sort) for i, elt in enumerate(element_z3s): self.solver.add(index_fn(lit_const, z3.IntVal(i)) == elt) + # #1418 review F1: the literal's own constant is a STAND-IN — an + # element's term is related to it only by the axioms above, which the + # occurrence walk cannot see — so a disclosed element must be + # inherited explicitly or indexing the value back out severs the + # taint. + self._inherit_disclosure(expr, lit_const) return lit_const def _translate_unary( @@ -2479,6 +2515,21 @@ def _translate_call_with_info( else: ret_var = self.declare_int(fresh) + # #1406/#1407: this call's RESULT is the disclosed value. Recorded + # here — the one place a call's term is minted — so every later + # reader of that term (a `let` binding, a projection, a branch join, + # a `match` scrutinee) sees the taint without any of them having to + # recognise the call. The hook resolves the callee, so a spelling + # the verifier can attribute to a disclosed function taints, and one + # it cannot does not. + if self._disclosed_call_hook is not None: + disclosed, sites = self._disclosed_call_hook(call_node) + if disclosed: + self._disclosed_terms.append(ret_var) + if sites: + self._disclosed_term_sites.setdefault( + ret_var.get_id(), []).extend(sites) + # Assume callee postconditions about the return variable saved_result = self._result_var self._result_var = ret_var @@ -2580,7 +2631,65 @@ def _fresh_opaque_slot( if span is None: # pragma: no cover — parser always spans statements return None self._opaque_tainted = True - return z3.Const(f"_opaque_{tag}_{span.line}_{span.column}", sort) + stand_in = z3.Const(f"_opaque_{tag}_{span.line}_{span.column}", sort) + self._inherit_disclosure(node, stand_in) + return stand_in + + def _inherit_disclosure(self, node: object, stand_in: z3.ExprRef) -> None: + """A stand-in term inherits the disclosure of the value it replaces. + + #1363's asymmetry, one layer down (#1418 review F1). Where the SMT + layer LOSES a value — a ``let`` whose RHS it cannot translate, an + array literal whose elements it can only relate by axiom — it mints a + fresh constant, and the recorded provenance of any disclosed call + inside that expression is severed. Every reader still takes the + payload refinement off the binding's DECLARED type, so the fact + survives while the taint does not, and a `Tuple(mk(x), 1)` + destructured back out proved at Tier 1 over a value the program + refutes. Carrier-dependent, which is what made it easy to miss: the + same spelling whose binding happens to translate demotes correctly. + + Called at every mint rather than at the two known callers, so a + future stand-in is covered by existing code. The walk is over ONE + expression's subtree and runs only when a verifier is driving. + """ + if self._disclosed_call_hook is None: + return + found, sites = self._disclosed_calls_in(node) + if not found: + return + self._disclosed_terms.append(stand_in) + if sites: + self._disclosed_term_sites.setdefault( + stand_in.get_id(), []).extend(sites) + + def _disclosed_calls_in(self, node: object) -> tuple[bool, list[Any]]: + """Whether *node*'s subtree contains a disclosed call, and its sites. + + Answers over the AST rather than the Z3 term precisely because this + is the path where there is no usable term: the question is what the + expression MEANS, not what survived translation of it. + """ + found = False + sites: list[Any] = [] + stack: list[object] = [node] + seen: set[int] = set() + while stack: + cur = stack.pop() + if id(cur) in seen: + continue + seen.add(id(cur)) + if isinstance(cur, (ast.FnCall, ast.ModuleCall)): + hit, hit_sites = self._disclosed_call_hook(cur) + if hit: + found = True + sites.extend(hit_sites) + if isinstance(cur, ast.Node): + stack.extend( + getattr(cur, f.name) for f in dataclasses.fields(cur)) + elif isinstance(cur, (list, tuple)): + stack.extend(cur) + return found, sites def _term_mentions_opaque(self, term: z3.ExprRef) -> bool: """#1199: True when *term* contains an ``_opaque_``-named constant @@ -3525,6 +3634,82 @@ def check_valid( return SmtResult(status="disclosed") return result + def term_is_disclosed(self, term: object) -> bool: + """Whether *term* is, or is built from, a disclosed call's result. + + The VALUE half of the #1363 rule (#1406, #1407). A disclosed call's + fresh result term is recorded in + :py:meth:`_translate_call_with_info`; this asks whether the term in + hand carries one. ``@T.0`` after ``let @T = mk(x)`` resolves — via + :class:`SlotEnv`, which stores the RHS's term rather than a fresh + variable of its own — to that very term, and a destructure or + sub-pattern projection is an accessor applied to it, so both answer + yes without either being spelled as a call. + + OCCURRENCE, not identity, for the same reason + :py:func:`~vera.verifier._is_locally_constructed` recurses through + ``ite``: a value joined from two branches is disclosed on whichever + branch discloses, and a value projected out of a disclosed one is the + disclosed value's own component. Over-approximating is the safe + direction — it demotes out of Tier 1, to a runtime check where one + exists (a postcondition's E534) and otherwise to an honest disclosure + (an unguarded narrowing's E506), where under-approximating claims a + proof the run does not have. + + Costs nothing on a clean run: ``_disclosed_terms`` is empty unless + this function actually called something disclosed, and the walk is + skipped outright when it is. + """ + if term is None or not self._disclosed_terms: + return False + return self._term_contains( + term, {d.get_id() for d in self._disclosed_terms}) + + def _term_contains(self, term: object, wanted: set[int]) -> bool: + """Whether any ast id in *wanted* occurs in *term*. + + ONE walk, shared by the withholding test and the citation lookup + (#1406, #1399): "the value carrying this fact" and "the value this + citation belongs to" have to mean the same thing, and two traversals + written separately are two chances for them to drift. + """ + stack: list[Any] = [term] + seen: set[int] = set() + while stack: + cur = stack.pop() + try: + cur_id = cur.get_id() + except (AttributeError, z3.Z3Exception): + continue + if cur_id in wanted: + return True + if cur_id in seen: + continue + seen.add(cur_id) + try: + stack.extend(cur.children()) + except (AttributeError, z3.Z3Exception): # pragma: no cover + continue + return False + + def disclosed_term_sites(self, term: object) -> list[Any]: + """The citation sites of the disclosed values occurring in *term*. + + The companion to :py:meth:`term_is_disclosed`: that answers whether to + withhold, this answers what to name when the withholding causes a + demotion (#1399's imported-disclosure citation, reached through + #1406's value taint). Empty for a purely local disclosure, which + needs no citation — its own E504/E506 is in the same output. + """ + if term is None or not self._disclosed_term_sites: + return [] + out: list[Any] = [] + for recorded in self._disclosed_terms: + sites = self._disclosed_term_sites.get(recorded.get_id()) + if sites and self._term_contains(term, {recorded.get_id()}): + out.extend(sites) + return out + def _check_refutation( self, goal: z3.ExprRef, @@ -3615,6 +3800,19 @@ def reset(self) -> None: reported ``disclosed`` — a demotion inherited from a function it has nothing to do with. + ``_disclosed_terms`` goes with them, and the reason is stated + honestly (#1406). No whole program is known to distinguish keeping + it: ``_fresh_name`` carries the CALLEE's name (``_call_mk_3``), and + ``_fresh_counter`` resets here, so a surviving entry can only collide + with a call to the same-named callee — which has the same disclosure + status, so the answer would be right by accident. It is cleared + because the list is per-function state on a context reused across a + whole program: left standing it grows without bound over a session, + and it makes the correctness of every future answer depend on a + naming detail two files away rather than on this line. + ``test_1406_reset_forgets_the_previous_functions_disclosed_terms`` + pins the invariant directly, since no program exhibits it. + ``_length_fns`` / ``_index_fns`` MUST be cleared even though their ``FuncDeclRef`` objects stay valid across ``solver.reset()``: their side-effect axioms do not. @@ -3636,6 +3834,8 @@ def reset(self) -> None: self._opaque_tainted = False self._path_conditions.clear() self._tainted_facts.clear() # #1363: per-function, must not survive + self._disclosed_terms.clear() # #1406: ditto — see the docstring + self._disclosed_term_sites.clear() # and the citations riding on them self._length_fns = { "Int": z3.Function("length", z3.IntSort(), z3.IntSort()), } diff --git a/vera/verifier.py b/vera/verifier.py index 1ce468a67..1683eef07 100644 --- a/vera/verifier.py +++ b/vera/verifier.py @@ -335,6 +335,35 @@ class VerifySummary: total: int = 0 +def disclosed_key(name: str, owner: str) -> str: + """The name a disclosure is recorded under: bare, or scoped to its owner. + + ONE spelling, shared by the two halves of the disclosed set — the + obligation-derived :func:`disclosed_fn_names` and the result-derived + ``_result_disclosed_fns`` — because the set is consulted as their UNION + and a key spelled two ways is a member the lookup cannot find. + + A top-level name is its own key: it is visible program-wide. A ``where`` + helper's is qualified by its top-level owner, because its bare name means + a DIFFERENT function in every owner, and a bare key made one owner's + tainted helper demote another owner's clean caller (#1418 review F3). + That defect was latent in the obligation-derived half from the start and + only became reachable when a helper first carried a disclosing obligation + of its own; #1420 widened the reachable set to forwarding helpers, which + is what turned the F3 cell red, but the isolated shape reproduces on + `release/v0.2.0` before #1420 too. + + Scoping cannot LOSE a demotion that was needed, which is the direction + that would matter. A helper is reachable only through its owner's + lexical chain (`_scope_fn_names`), and #1383 refuses a bare call to an + imported module's helper, so every caller of a helper sits inside the + owner and looks it up under this same key. The residual is unchanged and + still errs toward demotion: two helpers of one name under ONE owner share + a key. + """ + return f"{owner}\x1fwhere\x1f{name}" if owner else name + + def disclosed_fn_names( obligations: "list[ProofObligation]", ) -> frozenset[str]: @@ -361,7 +390,8 @@ def disclosed_fn_names( disclosed and the taint stopped one hop short. """ return frozenset( - o.fn_name for o in obligations if is_disclosing(o) + disclosed_key(o.fn_name, o.owner) + for o in obligations if is_disclosing(o) ) @@ -446,6 +476,16 @@ class VerifyResult: # discharge order. Empty-list default keeps existing constructors # (tests, tooling) source-compatible. obligations: list[ProofObligation] = field(default_factory=list) + #: The functions this run found to be handing on a disclosed value, + #: mapped to the import sites behind each. NOT derivable from + #: `obligations`: a forwarder whose declared return is the same refined + #: type as its callee's NARROWS nothing, so #1412 obligates it nothing, + #: so a consumer reading only the obligation stream misses it. + #: `vera/disclosure.py`'s manifest is such a consumer, and without this + #: an importer calling that forwarder proved at Tier 1 what the same + #: program in one file demotes (#1418 review J1). + result_disclosed: dict[str, list[DisclosureSite]] = field( + default_factory=dict) def verify( @@ -494,6 +534,7 @@ def verify( diagnostics=verifier.errors, summary=verifier.summary, obligations=verifier.obligations, + result_disclosed=dict(verifier._result_disclosed_fns), ) @@ -578,6 +619,31 @@ def __init__( # Same lifetime as `SmtContext._tainted_facts`, which is what they # describe: per function, cleared with the scope set below. self._tainted_sites: list[DisclosureSite] = [] + # #1407: functions whose own obligations are all fine but whose RESULT + # is a disclosed value — a forwarding wrapper, a `where` helper, the + # tail of a pipe. They carry no failed obligation, so + # `disclosed_fn_names` cannot see them; they are recorded here as each + # body is translated, and unioned in by `_disclosed_fn_names` so the + # existing fixpoint carries the taint one hop further per pass. + # Mapped to the citation sites BEHIND each one, so a demotion reached + # through a forwarder can still name the import at the far end of it + # (#1399's citation, carried across #1407's hop). Empty list = the + # forwarder hands on a purely local disclosure, which needs no + # citation: its own E504/E506 is in this run's output. + self._result_disclosed_fns: dict[str, list[DisclosureSite]] = {} + # #1418 review F3: the TOP-LEVEL owner whose lexical scope the + # function under verification sits in — itself, or the outermost + # ancestor of a `where` helper. A helper's forwarding is keyed under + # it (`_result_disclosed_key`), so two helpers of the same bare name + # in different top-level functions no longer share an entry: one + # forwarding a disclosed producer used to demote the other's clean + # caller. Set beside `_scope_fn_names`, from the same `(decl, + # enclosing)`, so visibility and keying cannot disagree. + self._scope_owner: str = "" + # Whether that owner is a PARENT (a helper is under verification) or + # the function's own name (a top-level one is) — `_scope_owner` alone + # cannot say, being the function's own name in the top-level case. + self._scope_is_helper: bool = False # #680 review: fresh consts pushed to shadow a stale outer slot when an # untranslatable let/destructure rebinds it. A div/sub operand that IS # one falls to Tier-3 (the shadowed value is unknown). Reset per fn. @@ -994,6 +1060,14 @@ def _record_obligation( error_code=error_code, counterexample=counterexample, file=self._current_file, + # An obligation belongs to the scope that records it: every one + # of this method's call sites passes the `decl.name` of the + # function `_verify_fn` is verifying, so `fn_name` IS the scope's + # own name. A guard comparing the two was written here and + # removed: it never differed, over 919 cells and 251 example and + # conformance programs, which makes it a term no test could + # distinguish rather than a safety net. + owner=self._scope_owner if self._scope_is_helper else "", )) @staticmethod @@ -2996,6 +3070,12 @@ def _rerun_until_disclosure_settles(self, program: ast.Program) -> None: # pass's entries suppress this pass's recordings, and the # obligation would vanish from the stream that is kept. self._construction_obligated = set() + # #1407: rebuilt for the same reason — which functions hand on a + # disclosed value is a property of the pass that translated them, + # and this pass withholds more than the last did. Recomputing + # cannot shrink the set: the input `_disclosed_fns` only grows and + # the analysis is monotone in it, so the fixpoint still terminates. + self._result_disclosed_fns = {} self.register_program(program) self._verify_all_declarations(program) @@ -3007,8 +3087,16 @@ def _verify_all_declarations(self, program: ast.Program) -> None: self._verify_shadowed_module_generics() def _disclosed_fn_names(self) -> frozenset[str]: - """This verifier's obligations, through the shared rule.""" - return disclosed_fn_names(self.obligations) + """This verifier's obligations, through the shared rule — plus the + functions that merely HAND ON a disclosed value (#1407). + + The two halves answer the same question about different evidence. + `disclosed_fn_names` reads the obligation stream, which is where a + function that failed to establish its own declared type shows up. A + forwarder leaves no such trace, so it is collected during body + translation instead; both feed the one set every consumer reads.""" + return (disclosed_fn_names(self.obligations) + | frozenset(self._result_disclosed_fns)) def _verify_shadowed_module_generics(self) -> None: """Verify each IMPORTED generic's clone at the type args the importer @@ -3391,6 +3479,18 @@ def _verify_fn( bare helper call resolves to the nearest same-named helper (#991) rather than through the flat, last-wins registry. """ + # PER-FUNCTION SCOPE STATE, SET WHERE THE FUNCTION IS ENTERED. Every + # exit from this method below is a function whose body may still be + # translated — the generic branch's `_check_generic_refined_return` + # translates one and installs the disclosure hook — and the hook asks + # `_local_fn_names_in_scope()`, which reads these. Assigned partway + # down the non-generic path, they were the PREVIOUS function's on that + # route: a generic could have a local call suppressed, or an import + # applied to a local call of the same name, by another function's + # helpers (CodeRabbit, PR #1418). `_tainted_sites` goes with them for + # the reason its own comment gives — a citation belongs to the + # function whose facts were withheld. + self._set_fn_scope(decl, enclosing) if decl.forall_vars: # #1014: a nested generic helper's instances are keyed by its # parent-qualified name (``a$where$g`` — the discovery copy is @@ -3476,11 +3576,6 @@ def _verify_fn( # consult (`_local_fn_names_in_scope`). Set here so the two answers # are built from one `(decl, enclosing)` and cannot disagree about # which helpers are visible. - self._scope_fn_names = frozenset( - wfn.name - for group in (decl, *enclosing) - for wfn in group.where_fns or () - ) # Cleared with it: a citation belongs to the function whose facts were # withheld, and one left standing would name another function's callee. self._tainted_sites = [] @@ -3506,6 +3601,12 @@ def _verify_fn( # arm body's call PRECONDITIONS — the E501 path the narrowing-walk fact # carry never reaches. Stateless, so safe on the warm (shared) smt too. smt._subpattern_fact_hook = self._subpattern_source_facts + # #1406/#1407: and let it record a DISCLOSED call's result term, so + # the taint follows the value into every binding, projection and + # branch that value reaches. The terms it causes to be recorded are + # per-function state, which `SmtContext.reset()` clears — so the warm + # (shared) smt is safe for the same reason `_tainted_facts` is. + smt._disclosed_call_hook = self._disclosed_call_for_value # #994 F1: let the SMT nullary-ctor translation resolve a bare tag's # exact instantiation from the checker's recorded (instance-substituted) # semantic type, instead of the ambiguous base-name scan that crashed Z3 @@ -3652,6 +3753,24 @@ def _verify_fn( # 5. Translate function body body_expr = smt.translate_expr(decl.body, slot_env) + # 5.05. #1407: does this function HAND ON a disclosed value? A + # forwarding wrapper makes no claim that needs the disclosed + # fact, so it contributes no obligation and + # `disclosed_fn_names` — which reads the obligation stream — + # cannot see it, while its caller reads facts off the very + # declared type the original callee failed to establish. The + # body term already carries the taint (the `let`, the branch + # join, the projection are all in it), so the question is just + # whether the value leaving here is a disclosed one. Recorded, + # not acted on: `_disclosed_fn_names` unions it and the + # `_rerun_until_disclosure_settles` fixpoint does the rest, one + # hop per pass, so a chain of wrappers of any depth terminates + # for the reason the fixpoint already terminates. + if smt.term_is_disclosed(body_expr): + self._result_disclosed_fns[ + self._result_disclosed_key(decl.name, is_helper=bool(enclosing)) + ] = smt.disclosed_term_sites(body_expr) + # 5.5. Check primitive-operation safety obligations (spec §6.4.3): # @Nat - @Nat underflow (#520), and division/modulo by zero # plus array index bounds (#680). Walks the body emitting an @@ -6524,6 +6643,21 @@ def _walk_for_nat_binding_obligations( stmt.value, (ast.SlotRef, ast.FnCall, ast.ModuleCall), ) + # #1413: the THIRD reader. "A call — its callee + # discharged the return type" is precisely the premise + # disclosure withdraws, so a guaranteed source is not + # guaranteed when this run disclosed it. A `SlotRef` + # source is answered by its TERM (translating one is an + # env lookup, recording no obligation) and a call by its + # callee, which covers a forwarding wrapper too; the + # translation is skipped outright unless some disclosure + # is live, so a clean program pays nothing. + src_term = None + if source_guaranteed and self._disclosure_is_live(smt): + src_term = ( + smt.translate_expr(stmt.value, cur_env) + if isinstance(stmt.value, ast.SlotRef) else None + ) pushed: list[tuple[str, object]] = [] seeds: list[object] = [] for i, te in enumerate(stmt.type_bindings): @@ -6554,7 +6688,19 @@ def _walk_for_nat_binding_obligations( comp_fact = self._term_source_fact( smt, src_args[i], slot_val) if comp_fact is not None: - seeds.append(comp_fact) + # Through the shared gate. Withholding + # moves a BLOCK-scoped seed onto a + # FUNCTION-scoped list, which widens only + # the second (tainted) attempt — the one + # whose sole outcome is a `disclosed` + # demotion. A fact leaking past its block + # can therefore cost a Tier-1 proof + # elsewhere in the function, never grant + # one; the arm facts have been carried the + # same way since #1363. + seeds.extend(self._established_facts( + [comp_fact], source=stmt.value, + term=src_term, smt=smt)) for tn, sv in pushed: cur_env = cur_env.push(tn, sv) block_assumptions.extend(seeds) @@ -8069,36 +8215,6 @@ def _all_leaves_construct( return False return _is_locally_constructed(val, sort) - def _value_source_disclosed(self, expr: ast.Expr) -> bool: - """Whether the value *expr* PRODUCES came from a call this run - disclosed (#1410). - - :py:meth:`_scrutinee_is_disclosed_call` answers of one expression, and - that is the wrong grain here: `decl.body` is ALWAYS a ``Block``, so at - the return position the bare test answered False for every function - there is — measured, and it is what let a `wrap` forwarding a disclosed - `mk` publish `Option` at Tier 1. An argument can be a - ``Block`` or a branch just as easily. - - Descend to the value-producing leaves and take ``any``, the same - conservatism :py:func:`_is_locally_constructed` takes over an ``ite`` - and :py:meth:`_all_leaves_construct` over its arms: one leaf standing on a - disclosed producer is one path on which the declared type was never - established, and the fact must not be granted on the strength of the - other. - """ - if isinstance(expr, ast.Block): - return (expr.expr is not None - and self._value_source_disclosed(expr.expr)) - if isinstance(expr, ast.IfExpr): - return (self._value_source_disclosed(expr.then_branch) - or (expr.else_branch is not None - and self._value_source_disclosed(expr.else_branch))) - if isinstance(expr, ast.MatchExpr): - return any(self._value_source_disclosed(arm.body) - for arm in expr.arms) - return self._scrutinee_is_disclosed_call(expr) - def _nested_refinement_formal( self, arg: ast.Expr, formal: Type | None, ) -> Type | None: @@ -8391,12 +8507,6 @@ def _check_nested_refinement_obligation( return val = smt.translate_expr(value_node, slot_env) source_ty = self._resolved_type_of(value_node) - # A call to a function this run DISCLOSED did not establish its own - # declared type, so that type is not a premise here — the same third - # case #1363 named at the match scrutinee, at these boundaries - # instead. Asked of the value's producing LEAVES, because a body is - # always a `Block` and the per-expression test answers False for one. - disclosed = self._value_source_disclosed(value_node) # Guardedness is the SITE half intersected with the TYPE half, the # same shape every other `refine_bind` leg uses (#765): the roster # says whether codegen guards AT this position, and @@ -8435,11 +8545,19 @@ def _check_nested_refinement_obligation( return source_facts, _ = self._nested_refinement_facts(smt, source_ty, val) premises = list(assumptions) - if source_facts: - if disclosed: - smt._tainted_facts.extend(source_facts) - else: - premises.extend(source_facts) + # THE GATE, not a fourth hand-rolled copy of it (#1418 review). This + # site had a local test of its own instead — since deleted with its + # only call site — which descended to the value's producing leaves and + # put a SYNTACTIC question to each, so a `let`-bound disclosed + # producer arrived as a slot reference, answered False, and its + # declared type was granted as a premise. That + # is #1406 exactly, in a reader added after it: measured, the same + # value gave this obligation `tier3_unguarded` spelled + # `consume(mk(x))` and `verified` spelled + # `let @T = mk(x); consume(@T.0)`. The gate asks of the VALUE, so + # both spellings agree. + premises.extend(self._established_facts( + source_facts, source=value_node, term=val, smt=smt)) goal = z3.And(*goal_facts) if len(goal_facts) > 1 else goal_facts[0] result = smt.check_valid(goal, premises) if result.status == "verified" and complete: @@ -8887,6 +9005,12 @@ def _check_generic_refined_return( # `match` arm would otherwise false-E505/E501 (the arm accessor is # translated without the field's source refinement fact). smt._subpattern_fact_hook = self._subpattern_source_facts + # #1406/#1407: and let it record a DISCLOSED call's result term, so + # the taint follows the value into every binding, projection and + # branch that value reaches. The terms it causes to be recorded are + # per-function state, which `SmtContext.reset()` clears — so the warm + # (shared) smt is safe for the same reason `_tainted_facts` is. + smt._disclosed_call_hook = self._disclosed_call_for_value # #994 F1: same recorded-type hint as the main path — a bare nullary # ctor in this generic body's refined return must resolve its sort from # the recorded type, not the ambiguous base-name scan. @@ -9016,7 +9140,15 @@ def _check_refined_binding_obligation_term( if source_ty is not None: src_fact = self._term_source_fact(smt, source_ty, term) if src_fact is not None: - local_assumptions.append(src_fact) + # #1413: the SECOND reader. The premise is sound on the rule + # `_term_source_fact` states — every producer of a refined + # value is obligated to discharge it — and a DISCLOSED + # producer is the case that rule does not cover. Through the + # shared gate, so it cannot drift from the other two; when it + # withholds, the non-verdict branch below already reports the + # Tier-3 E506 with `_undecided_reason("disclosed")`'s wording. + local_assumptions.extend(self._established_facts( + [src_fact], source=node, term=term, smt=smt)) result = smt.check_valid(goal, local_assumptions) if result.status == "verified": self._record_obligation(decl.name, "refine_bind", node, "verified") @@ -9164,16 +9296,198 @@ def _subpattern_source_facts( return [] # literal scrutinee — concrete args, not accessors facts = self._subpattern_source_facts_term( self._resolved_type_of(scrutinee), scrutinee_z3, pattern, smt) - if facts and self._scrutinee_is_disclosed_call(scrutinee): - # #1363: the declared type these facts are read off belongs to a - # callee whose OWN obligation for it was disclosed, not - # discharged. The boundary rule that a call-produced value's - # facts were established elsewhere has a third case — disclosed — - # and this is it. Held apart rather than dropped: a goal that - # needs them is still reported, as Tier 3 rather than Tier 1. - smt._tainted_facts.extend(facts) - return [] - return facts + # #1363: the declared type these facts are read off may belong to a + # callee whose OWN obligation for it was disclosed rather than + # discharged. That question, and what to do about it, belong to + # :py:meth:`_established_facts` — the one gate every reader shares. + return self._established_facts( + facts, source=scrutinee, term=scrutinee_z3, smt=smt) + + def _set_fn_scope( + self, decl: ast.FnDecl, enclosing: tuple[ast.FnDecl, ...], + ) -> None: + """Bind the per-function lexical scope, from one ``(decl, enclosing)``. + + The visible ``where``-helper names (#1399's `_local_fn_names_in_scope`), + the owning top-level name those helpers' disclosures are keyed under + (#1418 review F3), and the citation list that belongs to this function + and no other — all three derived here so they cannot disagree about + which function is under verification, and called at the ONE place that + knows: the entry to :py:meth:`_verify_fn`. + """ + self._scope_fn_names = frozenset( + wfn.name + for group in (decl, *enclosing) + for wfn in group.where_fns or () + ) + # `enclosing` is built by APPENDING each parent — `top -> H1 -> H2` + # gives H2 `(top, H1)` — so the OUTERMOST is index 0. Taking the + # last recorded H2 under `H1$where$H2` while H1 looked it up as + # `top$where$H2`, and the miss was in the unsound direction: H1 + # discharged a Tier-1 obligation from H2's disclosed result + # (CodeRabbit, PR #1418). One owner per top-level function is + # the whole point of the key. + self._scope_owner = enclosing[0].name if enclosing else decl.name + # Which of the two the obligations recorded under this scope belong to. + # `_scope_owner` alone cannot say: for a top-level function it IS the + # function's own name, so a helper and its owner are indistinguishable + # by it. + self._scope_is_helper = bool(enclosing) + self._tainted_sites = [] + + def _result_disclosed_key(self, name: str, *, is_helper: bool) -> str: + """The key a forwarding function's disclosure is recorded under (F3). + + A top-level name is its own key: it is visible program-wide, and every + other disclosure set here is keyed that way. A ``where`` helper's is + qualified by the top-level owner whose scope it lives in, because its + bare name means different functions in different owners — and keying + it bare made one owner's tainted helper demote another owner's clean + caller, which is a completeness loss rather than a soundness one but + is a loss all the same. + + Two helpers of the same name under ONE top-level owner still share a + key. That is the diamond #991 addresses for resolution and this does + not: the residual is a demotion, the safe direction, and narrowing it + further means carrying the whole lexical chain as the key rather than + its root. + """ + return disclosed_key(name, self._scope_owner if is_helper else "") + + def _scoped_forwarder_hit(self, name: str) -> bool: + """Whether *name*, called from the scope under verification, resolves + to a ``where`` helper this run found to be forwarding a disclosed + value (F3). + + Asked only for a name the lexical chain actually supplies + (`_scope_fn_names`), so a top-level call is never answered by another + function's helper — the mirror of the visibility test + `_local_fn_names_in_scope` already applies to the manifest consult. + """ + if name not in self._scope_fn_names: + return False + return self._result_disclosed_key( + name, is_helper=True) in self._disclosed_fns + + def _disclosed_call_for_value( + self, call_node: ast.Expr, + ) -> tuple[bool, list[DisclosureSite]]: + """The SMT layer's hook: is this call disclosed, and on whose word? + + `_scrutinee_is_disclosed_call` records an imported disclosure's + citation site as it consults the manifest, which is right when it is + asked AT the place a fact is withheld — the site then belongs to this + function's demotion. This hook asks at every modelled call instead, + which is earlier and more often, so a site left on the live list here + would be cited by a demotion that had nothing to do with it: a + function that calls an imported disclosed helper and is demoted for an + unrelated local reason would name the import as the culprit. + + So the site is taken back off the list and returned, for the SMT layer + to park on the term the call produced. It is put back by + :py:meth:`_established_facts`, and only if that value's facts are the + ones actually withheld — which is what makes the citation true of the + demotion that carries it, and is also how a `let`-bound imported call + keeps its citation at all, its scrutinee being a slot reference by the + time anything asks. + """ + before = len(self._tainted_sites) + hit = self._scrutinee_is_disclosed_call(call_node) + sites = self._tainted_sites[before:] + del self._tainted_sites[before:] + if hit and not sites: + # A FORWARDER answers True from `_result_disclosed_fns` rather + # than from the manifest, so it recorded nothing above — but the + # import it forwards is exactly what a demotion here should cite, + # and the sites were collected when its own body was translated. + # Without this the wrapper spelling demotes with no culprit named, + # which is the gap #1399 closed for the direct spelling. + name = getattr(call_node, "name", "") + sites = list(self._result_disclosed_fns.get(name, ())) + if not sites and name: + sites = list(self._result_disclosed_fns.get( + self._result_disclosed_key(name, is_helper=True), ())) + return hit, sites + + def _established_facts( + self, + facts: list[object], + *, + source: ast.Expr | None, + term: object, + smt: SmtContext, + ) -> list[object]: + """The subset of *facts* this run ESTABLISHED — all of them, or none. + + THE single gate for every reader of a value's declared-type facts + (#1363, #1406, #1407, #1413). There are three such readers — a + ``match`` arm's sub-pattern bindings, the premise that lets a + projected value re-narrow into a second refinement, and the component + invariant a ``let``-destructure seeds — and #1363 gated one of them, + which is how two false Tier-1s outlived it, each proving at Tier 1 + over a value the compiled program then handed back unguarded. They + ASK here rather than each deciding, so a fourth reader is a call to + this function or it is a bug, and there is one place to read to learn + what the rule is. + + Withheld, never dropped. A fact this run did not establish goes to + ``smt._tainted_facts``, where ``check_valid`` offers it only on the + SECOND attempt — so a goal that needs it is still reported, as Tier 3 + rather than Tier 1, instead of failing as though nothing were known. + + *source* is the expression the value came from and *term* its Z3 term. + Either may be absent; they answer different halves of the same + question (see :py:meth:`_value_is_disclosed`). + """ + if not facts or not self._value_is_disclosed(source, term, smt): + return facts + # Attribute it. A syntactic hit recorded its own site as it consulted + # the manifest; a TERM hit's site was parked on the value when the + # call produced it (`_disclosed_call_for_value`), so bring it across + # now — the demotion that follows is the one it is true of. Duplicates + # are harmless: both citation texts dedupe on `site.cite()`. + self._tainted_sites.extend(smt.disclosed_term_sites(term)) + smt._tainted_facts.extend(facts) + return [] + + def _disclosure_is_live(self, smt: SmtContext) -> bool: + """Whether this run has disclosed anything at all. + + The cheap precondition for the whole mechanism. With nothing + disclosed every gate below answers False, so a caller that would have + to WORK to supply :py:meth:`_established_facts` its arguments — the + destructure reader translates its source expression — asks this first + and skips. That keeps the cost on programs that actually have a + disclosure, which, measured over the corpus, is none of them.""" + return bool(self._disclosed_fns or smt._disclosed_terms) + + def _value_is_disclosed( + self, source: ast.Expr | None, term: object, smt: SmtContext, + ) -> bool: + """Whether a value came from a function this run disclosed. + + The whole of the #1363 rule, in the form that does not depend on how + the value was spelled (#1406, #1407). Two questions, either of which + is enough: + + * is *source* written AS a disclosed call + (:py:meth:`_scrutinee_is_disclosed_call`) — the answer that still + works when the value has no Z3 term at all; and + * is *term* a disclosed call's result + (:py:meth:`SmtContext.term_is_disclosed`) — the answer that follows + the value through a ``let``, a destructure, a projection, a branch + join, and through any wrapper the fixpoint has by now marked + disclosed in its own right. + + Neither subsumes the other. A scrutinee the SMT layer could not + translate has no term but is still a recognisable call; a ``let``-bound + one has a term but is a slot reference. Asking both is what makes the + demotion a property of the value rather than of the syntax.""" + return ( + (source is not None + and self._scrutinee_is_disclosed_call(source)) + or smt.term_is_disclosed(term) + ) def _scrutinee_is_disclosed_call(self, scrutinee: ast.Expr) -> bool: """Whether *scrutinee* is a call to a function that was disclosed. @@ -9208,6 +9522,11 @@ def _scrutinee_is_disclosed_call(self, scrutinee: ast.Expr) -> bool: name = scrutinee.name if name in self._disclosed_fns: return True + # F3: a `where` helper's forwarding is keyed under its owner, so the + # bare-name test above cannot see it; this asks the scoped question, + # and only for a name the lexical chain supplies. + if self._scoped_forwarder_hit(name): + return True if isinstance(scrutinee, ast.ModuleCall): if self._module_qualified_base( scrutinee.path, name,