…ings)

Co-Authored-By: Claude <[email protected]>

…ecursive-NEQ demotion (PR #879 review)

Every FP ADT in the #871 battery had exactly one FP-carrying
constructor, so the multi-arm z3.Or decomposition in
_datatype_value_eq -- and its per-arm recognizer conjuncts -- was
unexercised, and the NEQ arm's recursive-demotion path (eq is None
-> None) was unpinned.

Two new pins: a mixed-constructor sum type (MA(Float64) | MB(Int))
whose cross-constructor inequality must stay a Tier-1 proof (dropping
the recognizer conjuncts flips exactly this test RED -- the unguarded
wrong-constructor arm's unconstrained accessors lose the proof) plus
NaN-guarded same-constructor reflexivity staying Tier-1; and !=
on a recursive FP-containing ADT demoting to an honest Tier-3
(RED against the structural-= fallback, which falsely proves it).

Mutation-validated: recognizer-guard drop -> only the sum-type pin
RED (8 others green); structural-= fallback -> 6 RED including the
new recursive-NEQ pin.

Skip-changelog: tests-only follow-up; the existing #871 [Unreleased] bullet was extended in this commit to note the fifth mutation axis

Co-Authored-By: Claude <[email protected]>

…d arguments (#882)

A call to a helper whose requires() constrains ADT-typed parameters produced
no call_pre obligation at all — no E501, no Tier-3 warning — so `vera verify`
reported ok:true for a call it never statically examined, while the identical
Int-parameter program correctly fired E501 and `vera run` trapped at runtime.

Root cause in SmtContext._translate_call_with_info: a constructor-call argument
(MkP(1)) only translates once the callee's concrete ADT sort exists in the Z3
sort cache, but in a caller context that never declared that ADT the sort was
never materialised, so _find_sort_for_ctor returned None, the whole call bailed,
and the obligation vanished.

The call translator now materialises each ADT-typed parameter's sort from the
callee's declared types before checking the precondition, so — post-#879 —
MkP(1) vs MkP(2) is statically refutable (E501 + counterexample), a satisfiable
call discharges, and nested-ADT / Float64-field-NaN arguments refute correctly.
Where the argument or the precondition genuinely can't be modelled (a host-handle
field such as Map, an undecidable predicate like string_length(...) > 0) the
obligation demotes to a loud Tier-3 E522 warning rather than silently not
existing (DESIGN.md: degrade loudly; the runtime guard still enforces it).

Return-value modelling is deliberately unchanged: an ADT-argument call whose
result feeds a postcondition stays opaque exactly as before, so no corpus
program's postcondition tier moves. A before/after verify --json census over all
145 conformance + example programs shows tier1 unchanged (1231); the only
movement is three example call sites (http, inference, async_http_fanout) gaining
one honest Tier-3 call_pre demotion each for their undecidable string_length
preconditions (+3 Tier-3).

Adds a run-level conformance program (ch06_requires_adt_arg) and eight unit tests
(TestAdtCallSitePrecondition). Mutation-validated three ways.

Co-Authored-By: Claude <[email protected]>

…e group (#881)

Close a completeness gap in the #881 mutually-recursive sort fix found by the
PR #879 adversarial soundness review: a `data` cycle whose cross-reference
passes THROUGH a `Tuple` field still crashed `vera verify` with the identical
uncaught RecursionError #881 exists to eliminate — `data C { MkC(Tuple<C,
Int>) }`, or a pair `data A { MkA(Tuple<B, Int>) }` / `data B { MkB(A) }`.

`_collect_adt_group` discovered the back-referenced member through the Tuple's
type args, but the Tuple sort was built by a FRESH `_get_or_create_adt_sort`
call that did not share the group's builder map, so its ADT component
re-entered sort creation for the still-uncached member and recursed unboundedly
(C -> build Tuple<C,Int> -> build C -> build Tuple<C,Int> -> ...). A Tuple
reachable through a member's field is now itself a group member — a single
`Tuple` constructor whose fields are its concrete components — so its
back-reference stitches to the shared in-progress builder and the whole
strongly-connected group is declared together via `z3.CreateDatatypes`. The
group representation is unified to `key -> [(ctor_name, concrete_field_types)]`
so registered ADTs and Tuples build through one loop. The `_z3_sort_name`
naming choke point is untouched (kept disjoint from the concurrent #884
sort-naming change).

Audit (skeptic-flagged): Tuple is the only structural field-type carrier — an
alias resolving to such a Tuple was affected too (aliases resolve to the Tuple
before the verifier) and is now fixed; a refinement-wrapped ADT field was
already unwrapped by `_enqueue_adt_types` and was never affected.

Equality obligations mirror #871: a Tuple-mediated NON-FP cycle proves
reflexivity Tier-1 (structural `=` agrees with the runtime); a recursive
Float64-through-Tuple cycle has no finite equality expansion and demotes to a
loud Tier-3 runtime check rather than a false proof; a FINITE Float64-in-Tuple
field uses per-field fpEQ statically (correctly disproving reflexivity via a
NaN counterexample).

New conformance program `ch02_adt_tuple_recursive` (run level) and four
regression tests + two mutation-kill parametrize cases in
`tests/test_mutual_recursive_sorts_881.py`. Written test-first: each new case
raises RecursionError on the pre-fix walk; mutation-validated — disabling the
Tuple-member branch flips exactly the six Tuple-mediated tests back to
RecursionError while the direct-reference tests stay green. A before/after
`verify --json` census over all conformance + example programs shows zero tier
movement beyond the new program (+3 Tier-1, +4 Tier-3, the same E525/E522
classes as the sibling mutual-recursion program).

Co-Authored-By: Claude <[email protected]>

…crash Z3 construction (#881) (#894)

* fix(smt): build mutually-recursive ADT sorts together via z3.CreateDatatypes (#881)

A mutually-recursive `data` pair — `data A { MkA, WrapB(B) }` / `data B { MkB,
WrapA(A) }` with a function over `@A` — passed `vera check` and ran under `vera
run`, but `vera verify` aborted with an uncaught Python `RecursionError` deep
in `_get_or_create_adt_sort`: a check-green program yielding a raw interpreter
traceback (the same class as #861 and the #871 sort-equality lineage). The
self-recursive case was handled by a single `self_ref_key`/`self_ref_dt` pair,
but that pair could name only ONE in-progress sort, so building `A` recursed
into building `B`, which recursed into building `A` again, until the recursion
limit tripped (FP-independent — an Int-only pair crashed identically).

Sort construction now declares every datatype reachable through constructor
fields together as one strongly-connected group via `z3.CreateDatatypes`
(`_collect_adt_group` + a builder map in `_vera_type_to_z3_sort`), the sound,
complete option that keeps Tier-1 static reasoning (DESIGN.md: maximise static
guarantees). Self-recursion is the singleton-group case; the `key ->
z3.Datatype` name transformation is hoisted to one `_z3_sort_name` choke point.
Because the sort now BUILDS, the #871 Float64-cycle guard is reachable for
mutually-recursive types: a non-Float64 mutual pair proves reflexivity Tier-1,
while a recursive Float64-containing mutual pair demotes to an honest loud
Tier-3 runtime check rather than a false proof.

New conformance program `ch02_adt_mutual_recursive` (run level) and regression
suite `tests/test_mutual_recursive_sorts_881.py` (issue repro, 3-cycle,
one-base-case pair, Float64-field pair, non-FP-Tier-1 vs recursive-FP-Tier-3
equality; mutation-kill re-raises RecursionError when group construction is
reverted). `verify --json` census over all 37 examples shows zero tier
movement (no corpus program declared mutually-recursive `data` before this).

Co-Authored-By: Claude <[email protected]>

* fix(smt): declare Tuple-mediated recursive datatype cycles in the same group (#881)

Close a completeness gap in the #881 mutually-recursive sort fix found by the
PR #879 adversarial soundness review: a `data` cycle whose cross-reference
passes THROUGH a `Tuple` field still crashed `vera verify` with the identical
uncaught RecursionError #881 exists to eliminate — `data C { MkC(Tuple<C,
Int>) }`, or a pair `data A { MkA(Tuple<B, Int>) }` / `data B { MkB(A) }`.

`_collect_adt_group` discovered the back-referenced member through the Tuple's
type args, but the Tuple sort was built by a FRESH `_get_or_create_adt_sort`
call that did not share the group's builder map, so its ADT component
re-entered sort creation for the still-uncached member and recursed unboundedly
(C -> build Tuple<C,Int> -> build C -> build Tuple<C,Int> -> ...). A Tuple
reachable through a member's field is now itself a group member — a single
`Tuple` constructor whose fields are its concrete components — so its
back-reference stitches to the shared in-progress builder and the whole
strongly-connected group is declared together via `z3.CreateDatatypes`. The
group representation is unified to `key -> [(ctor_name, concrete_field_types)]`
so registered ADTs and Tuples build through one loop. The `_z3_sort_name`
naming choke point is untouched (kept disjoint from the concurrent #884
sort-naming change).

Audit (skeptic-flagged): Tuple is the only structural field-type carrier — an
alias resolving to such a Tuple was affected too (aliases resolve to the Tuple
before the verifier) and is now fixed; a refinement-wrapped ADT field was
already unwrapped by `_enqueue_adt_types` and was never affected.

Equality obligations mirror #871: a Tuple-mediated NON-FP cycle proves
reflexivity Tier-1 (structural `=` agrees with the runtime); a recursive
Float64-through-Tuple cycle has no finite equality expansion and demotes to a
loud Tier-3 runtime check rather than a false proof; a FINITE Float64-in-Tuple
field uses per-field fpEQ statically (correctly disproving reflexivity via a
NaN counterexample).

New conformance program `ch02_adt_tuple_recursive` (run level) and four
regression tests + two mutation-kill parametrize cases in
`tests/test_mutual_recursive_sorts_881.py`. Written test-first: each new case
raises RecursionError on the pre-fix walk; mutation-validated — disabling the
Tuple-member branch flips exactly the six Tuple-mediated tests back to
RecursionError while the direct-reference tests stay green. A before/after
`verify --json` census over all conformance + example programs shows zero tier
movement beyond the new program (+3 Tier-1, +4 Tier-3, the same E525/E522
classes as the sibling mutual-recursion program).

Co-Authored-By: Claude <[email protected]>

* docs(testing): sync check_conformance.py table rows to 111 conformance entries (#894 review)

Co-Authored-By: Claude <[email protected]>

---------

Co-authored-by: T <[email protected]>
Co-authored-by: Claude <[email protected]>