…ering, generic-HOF consultors, refinement peeling (#867)

One shared cycle-guarded resolver (resolve_fn_type_alias, relocated to
vera/monomorphize.py to avoid an import cycle): apply_fn closure-return
consultors, the generic higher-order-function monomorphization sites
(calls.py + monomorphize.py twins), and FnType-terminal after refinement
unwrapping. Flips the pre-existing still-fails-loud #867 pin to
awaited-correctly.

PR #880 review, 4th single-hop site: _slot_name_to_wasm_type
(vera/wasm/inference.py) classified only a BARE FnType alias as an i32
closure pointer, so a let/param slot annotated with a refinement-wrapped
fn alias (type Foo = { @fn(...) | p };) or one chained through a
refinement resolved to None — the binding was rejected with CodegenSkip
("has no WASM representation") and its whole function dropped, on a
check/verify-green program. A plain NamedType chain was already handled
by the _resolve_base_type_name prefix, so only the refinement-involving
shapes remained. Routed through the same shared resolver; mutation-kill:
un-routing it flips exactly its two refinement-slot tests, all others
green.

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]>

…ct position (#874)

Contract-clause eq(a,b)/compare(a,b) now lower to the same canonical
==/Ordering form codegen already uses in bodies (was an uncaught
CodegenSkip), and the verifier desugars them to the FP-correct == /
Ordering encoding (was a silent Tier-3 deferral). Includes the review
round: where-fn contract lowering, compare Tier-1 Ordering-sort
materialization, the _is_user_fn shadowing guard, and a tightened
trap assertion.

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

…uses; dedicated E532 code (#882)

Completes the #882 fix after the blast-radius review found it incomplete
for its own scope plus a diagnostic-code semantics mismatch.

GAP 1 (silent loss inside ensures): a contracted call whose precondition
cannot be checked statically records its call-pre demotion during step-7
postcondition translation, which runs AFTER the step-6b demotion drain, so
the obligation vanished — the exact silent-loss #882 closes, still open for
calls in ensures position. The demotion drain now runs a second time (step
8b) after ensures / refined-return / decreases translation, before the
where-fn recursion reset()s the shared SMT context. RED-first probe: a call
in an ensures clause produced zero call_pre obligations while the
statement-position twin produced one; mutation-killed by deleting the second
drain (both ensures tests flip RED).

GAP 2 (wrong code): the demotion was tagged E522, whose registered meaning
is "Cannot verify postcondition (body undecidable)". Minted E532 "Cannot
verify call-site precondition (undecidable)" so the class is one concept per
code; a program can now carry E522 (postcondition) and E532 (call site)
distinctly (async_http_fanout does).

Tier census over 146 conformance + example programs: 1231/495/1726 (parent)
-> 1235/499/1730, all movement accounted for (new all-Tier-1 fixture +4;
four programs each gain one honest E532 call_pre demotion +4); zero silent
regressions. Spec §6.4.2 documents the demotion; doc counts refreshed.

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

…onger collide (#884)

The verifier named Z3 datatype sorts with the old lossy sanitize
(`key.replace("<", "_").replace(">", "").replace(", ", "_")`), so a
monomorphized `Box<Int>` and a flat ADT literally named `Box_Int` both
became the Z3 name `Box_Int`. Z3's per-context datatype cache conflates
same-named sorts (the last `create()` wins and earlier same-named sorts
silently adopt its structure), so `Box<Int>`'s sort acquired the flat
ADT's `MkBoxInt(Bool)` constructor — a false E500 counterexample
(`@Box<Int>.0 = MkBoxInt(False)`) on trivially-true valid code.

Both Z3 sort-name sites (`_get_or_create_adt_sort` and
`_get_or_create_tuple_sort` in `vera/smt.py`) now route through the
injective `mangle_type_name` mangler #775 introduced for WAT symbols, so
distinct type keys can never share a Z3 sort name. The full-type-string
sort cache and the #871 nested-Float64 fpEQ walk are unaffected (the cache
is keyed by the type string, not the Z3-visible name).

Soundness-safe: the conflation only freed field constraints, producing
conservative false negatives, never a false Tier-1 — a genuinely-false
ensures over the colliding pair is still disproved after the fix, now with
the correct `MkBox` constructor.

Both sort-name sites are independently pinned, one collision per site, so
neither `mangle_type_name` call can be reverted without flipping a test:

- ADT site (`_get_or_create_adt_sort`): the `Box<Int>` / flat `Box_Int`
  collision. Reverting it re-collides the sorts and flips the three
  `Box`-collision tests (verifies-clean, correct-constructor, and the
  false-prove probe) back to the false E500.
- Tuple site (`_get_or_create_tuple_sort`): a `Tuple<Tuple<Int>, Int>` vs
  `Tuple<Tuple<Int, Int>>` collision. Both keys lossy-sanitize to
  `Tuple_Tuple_Int_Int`; under the lossy name the two synthesised tuple
  sorts share one Z3 datatype, and a match arm projecting a field index
  the conflated sort does not carry crashes the verifier with
  `z3.z3types.Z3Exception: Invalid accessor index` at `sort.accessor`
  (in `_bind_pattern`). Reverting it flips the new tuple-collision test.
  Confirmed load-bearing: reverting this site with only the `Box`
  collision test present flipped nothing.

The rename also broke the verifier's Array-element reverse lookup, fixed
here since #884 caused it. `_get_element_sort_for_array`'s tier-3 fallback
reconstructed the `_z3_sorts` key by string surgery
(`elt_key.replace("_", "<", 1) + ">"`) that assumed the old lossy naming,
so after the rename a generic-ADT element (`Array<Box<Int>>` → sort
`Array_Box_LInt_R`) produced the non-matching candidate `Box<LInt_R>` and
the lookup silently returned None. Latent — tier 1's creation-time direct
map (`_array_element_sorts`) fires for every live path, and no corpus
program indexes an `Array<Generic<T>>` in a contract this way — but
dead-on-arrival for that shape. A new injective inverse
`unmangle_type_name` (a left-to-right prefix-code decode, round-trip-tested
against `mangle_type_name`) recovers the key correctly, and the stale
tier-3 comment is corrected.

Pinned by tests/test_verifier_sort_name_collision_884.py (ADT + tuple
collisions, rename-control, false-prove disproved for the right reason),
the ch06_adt_sort_disambiguation conformance program,
TestSmtContextDirect.test_element_sort_reverse_lookup_tier3_generic_adt
(the Array-element unit pin), and the unmangle round-trip / non-range-input
tests in TestMangleInjectivity. Mutation-validated: reverting either
sort-name site to the lossy sanitize flips its collision test RED, and
reverting the Array-element lookup to the old string surgery flips the
reverse-lookup unit test RED.

Pre-existing on main; found by the PR #883 adversarial panel.

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

…redicates (#887 review)

The Pass 1.6 ability-op walker `_rewrite_ops_in_expr` fell through
`ForallExpr`/`ExistsExpr` to the leaf return, so an `eq`/`compare` inside a
`forall`/`exists` contract predicate was never rewritten to its canonical
operator form. A quantifier in a contract is runtime-lowered by
`_translate_quantifier`, which compiles the predicate `AnonFn` body — so the
un-canonicalized ability op reached the WASM backend as a bare unregistered
`FnCall` and tripped the same uncaught `CodegenSkip` as #874's original
top-level case.

The walker now descends into the quantifier's `domain` and `predicate`. Two new
codegen tests (`forall`+`eq` and `exists`+`compare` in an `ensures`) are
mutation-validated: both flip RED to the `CodegenSkip` when the new branch is
disabled, GREEN when restored. Also syncs TESTING.md/ROADMAP.md test totals
(6,076 -> 6,078) for the two new tests.

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

…rose list (#892 review)

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

#893 review)

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

…, #873)

An imported generic instantiated only by the importer was monomorphized
nowhere — check passed but run failed WASM validation at `call $gid`, for
both the bare and module-qualified call forms (#774). The importer now
harvests imported public generics, merges the unshadowed ones into its
`generic_decls`, and the shared discovery walks `ModuleCall` targets. The
module-qualified-called — is now monomorphized under a distinct
`mod$<path>$gen$…` name reached only by the qualified call.

A generic whose only call site is inside a closure body failed run with
`unknown func` (#873): `_compile_lifted_closure` now threads
`generic_fn_info` + `known_fns`.

Completeness gaps closed one level deeper (PR #888 review): a shadowed
generic calling another generic emits the transitive clone (both sides);
the statement-position result-shape predicates share one ModuleCall target
resolver with the desugar; an unshadowed generic calling a shadowed sibling
has its shadowed clone discovered by scanning the emitted normal clones.

Soundness keystone (CR 3519156263): an imported generic's clone RUNS in the
importer but its body lives in another module, so a LYING module contract
ran unverified — a false Tier-1 (verify clean, run traps the clone's
postcondition). Worse, a same-named LOCAL generic absorbed the module call's
instantiation into its bare key, proving the local's contract in the module
clone's place. The importer now records every shadowed module clone under
its `mod$…` base (never the bare name a local generic owns), and verifies
each imported generic's clone (shadowed and unshadowed) at its own
instantiations, turning a lying module contract into an honest E500. The
warm incremental session runs the same verification so warm == cold.

Codegen and verifier discovery move in lockstep — proved by the #732
differential (namespaced keys distinguish module clone from same-named
local generic). Mutation-validated: disable the imported-generic verify
pass → lying-contract tests stop catching E500; desync either side's mod$…
key → differential flips; disable either side's normal-clone scan → the
unshadowed-caller case flips.

Run-level conformance programs `ch08_cross_module_generic` and
`ch09_generic_in_closure`; spec §11.16.

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

#873)

Closes #774
Closes #773
Closes #873

Closes #884

Reconciled the #881 (mutual-recursion group-builder) and #884 (injective
sort naming) changes to smt.py: kept #881's group-builder structure and its
`_z3_sort_name` choke point, and made that choke point delegate to the
injective `mangle_type_name` (#884's fix) so all sort-name generation —
group members and tuples alike — is injective in one place.

…#874)

Closes #874

#882)

Closes #882

…lowering (#867)

Closes #867

…tters (#869)

Closes #869

…mance, 6234 tests)

Post-merge reconciliation for the release/v0.1.0 integration branch: conformance
109→118, tests →6234 across 99 files, per-file table rows, verify/run level
counts, and the passed/skipped subtotal (6,162 passed, 46 skipped) from the full
integrated suite run.  Site assets regenerated.  All gate scripts green.

…orts returns the reachable closure (#890)

A check-green program with ZERO generics crashed at `vera run` with
`unknown func: failed to find name $via_mid` when `main` imported `mid`
and `mid` imported `base`: `mid`'s body calls `base::wrap40`, but `base`
was never registered or compiled into the importer's flat WASM module, so
the emitted body was left with a dangling call.

Root cause: `ModuleResolver.resolve_imports` (vera/resolver.py) returned
only the top-level program's DIRECT imports, even though its recursion had
already parsed and cached the transitively-reached `base`. Codegen, the
checker, and the verifier all consumed a module list missing every
transitive dependency.

Fix: `resolve_imports` now returns the transitive closure of reachable
modules, deduplicated (a `main -> {left, right} -> base` diamond yields
`base` once), each tagged `direct` (imported by the top-level program) vs
transitive-only. Codegen harvests and compiles every module in the closure
so an imported body's call to a deeper module resolves.

Spec §8.6.4 preserved — a transitive module's declarations are NOT visible
to the original importer: the checker and verifier inject only `direct`
modules into the importer's callable namespace and qualified-call
registries, and codegen subtracts a `_transitive_only_names` set from its
cross-module guard rail so a main-program body calling a purely transitive
symbol fails loudly at compile rather than silently binding to the
definition emitted for a sibling module. Cycle-safe via the resolver's
existing `_in_progress` E011 guard.

Test-first + mutation-validated: the RED tests (chain + diamond) fail on
the pre-fix code with the exact `unknown func`; reverting the closure
return flips them RED again, and disabling the `_transitive_only_names`
subtraction flips the §8.6.4 visibility test RED. A run-level conformance
program (ch08_transitive_module_import + _mid/_base companions) pins the
end-to-end behaviour.

Pre-existing on main; found by the PR #888 review.

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

…at module (#890)

fix(resolver): transitive module imports compiled into the importer's flat module (#890)

… mono clone (#891)

A generic instantiated over a parameterized ADT — `gid(MkBox(7))` for
`gid : forall<T> fn(@t -> @t)` and `data Box<T> { MkBox(T) }` — passed
`vera check`/`vera verify` but trapped at `vera run` with
`type mismatch: expected i64, found i32` while compiling the `gid$Box`
clone.

Root cause: `_infer_expr_wasm_type`'s `ResultRef` arm
(`vera/wasm/inference.py`) inferred only the scalar primitives and
returned `None` for everything else. Once `T = Box`, the clone's
postcondition `@T.result == @T.0` compares two i32 heap pointers, but the
`ResultRef` (`@Box.result`) defaulted to the scalar i64, so the equality
fell through to the `i64.eq` default while the operands were i32 — an
ill-typed clone body wasmtime rejects at instantiation. The `SlotRef`
operand (`@Box.0`) and the clone's `param`/`result` signature were
already i32; only the postcondition op disagreed.

Fix: the `ResultRef` and `SlotRef` arms now share one
`_ref_type_name_wasm_type` helper, so an ADT-bound (and pair-/handle-bound)
type variable lowers to i32 consistently across the signature and every
slot/result read.

New conformance program `ch02_generic_over_param_adt` (run level; suite
now 112) plus a regression test in `tests/test_codegen_monomorphize.py`
pin `gid(MkBox(42))` unwrapping to 42. Mutation-validated: reverting the
`ResultRef` arm to the pre-fix scalar-only logic restores the trap,
flipping the test RED.

Pre-existing on main; found by the PR #888 soundness review.

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

…ono clone (#891)

fix(codegen): generic over a parameterized ADT no longer traps in its mono clone (#891)

…d path (#772)

An `Eq`-constrained generic (`forall<T where Eq<T>>`) called with a value whose
type is inferred from a constructor — `eq2(MkBox("a"), …)` — dropped the type
argument: the monomorphizer resolves a `ConstructorCall` to the bare ADT name
`Box` (correct for clone mangling, since `Box<T>` is a uniform pointer), leaving
the `Eq` gate no `<String>` to inspect. Pre-#773 this false-accepted `Box<String>`
and emitted an unsound equality; post-#773 (structural derivation) it flipped to
an over-reject — a `Box<String>` that should derive `Eq` was refused E613, while
the slot-ref call form was accepted and ran correctly.

Fix scopes type-arg recovery to CONSTRAINED type vars: a `ConstructorCall` bound
to a `@T` carrying an ability bound now keeps its type argument (`Box<String>`,
via `_get_arg_type_info`) for the clone name, the substituted slot type in the
clone body, and the E613 gate — so the constructor path derives/rejects exactly
as the slot-ref path does. Unconstrained generics stay bare (no clone splitting).
The parallel WASM call-site rewriter and return-type resolver apply the same
recovery (new `_generic_constrained_vars` side table) so the mangled call matches
the emitted clone, and the direct `==` path (`Some(1) == Some(1)`) recovers the
operand type argument in `vera/wasm/operators.py`.

Soundness held: `Box<Array>` / `Box<Map>` still reject with E613, no E699 leak,
and the checker<->codegen structural-Eq differential (#732/#773) stays symmetric.
Mutation-validated both halves; full existing Eq suites pass unchanged. New
conformance program `ch09_ctor_inferred_eq` (run level) exercises the path.

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

…rred path (#772)

fix(codegen): Eq auto-derivation is type-arg-aware on the constructor-inferred path (#772)

…rence (#878)

A generic whose type argument must be inferred from a user-fn call's return
type in argument position monomorphized to the Bool phantom-var default: on a
check-green program `vera run` emitted a call to a `$Bool` clone Pass 1.5 never
produced, so the caller (often `main`) was skipped and dropped from the exports
("No exported functions to call"), or a private helper left a dangling `call`
that failed WAT validation.

Root cause is the lossy WAT collapse `i32 -> "Bool"` (a Decimal handle, an ADT,
and an Option/Result pointer are all i32 — the same value as the phantom
default) applied to user-fn returns on both the discovery and the body-emission
sides:

- Discovery (vera/codegen/monomorphize.py): `_build_mono_context` seeded the
  shared `fn_ret_types` from WAT signatures, so a generic bound solely by a
  user-fn return was discovered as `$Bool` while the #732 verifier discovered
  the precise type — a differential desync masked only by identity clone
  bodies. Now seeds from each fn's declared return TypeExpr, exactly as the
  verifier does, with the WAT collapse kept only as a fallback.
- Body-emission (vera/wasm/inference.py): `_get_arg_type_info_wasm` had no
  FnCall branch, so a parameterized return in `Option<VeraT>` position bound
  nothing; and a user-fn call in bare `@VeraT` position collapsed i32 to Bool.
  It now mirrors discovery's FnCall branch (shared _BUILTIN_PARAMETERIZED_RETURNS
  plus a non-generic-user-fn parameterized case) and consults the declared
  return TypeExpr for the ambiguous i32 case. GENERIC calls are excluded from
  the user-fn branch (their declared return is over the callee's own type vars,
  not concrete types) so they fall through to generic-return resolution exactly
  as discovery does — keeping the two consultors in lockstep.

Test values are deliberately Decimal returns (`0.3333...`) that cannot coincide
with the Bool default (1/0), the exact Bool-coincidence trap CLAUDE.md warns
about. New run-level conformance program ch09_generic_infer_user_fn_return (suite
123) plus three regression tests (crash-via-IO, WAT-mangle discriminator,
discovery-vs-verifier differential); each change is independently mutation-
validated. Does not weaken #888's cross-module/closure discovery.

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

…ry, verifier, and call-rewrite (#878)

fix(mono): recover user-fn return types in generic instantiation inference (#878)

The #878 merge resolved KNOWN_ISSUES to 'No known bugs.', but #898 (Eq
over-reject on sparse multi-type-param ADTs) is an open bug-labelled issue,
so the one-to-one Bugs invariant requires its row until it's fixed.

Skip-changelog: docs-only bookkeeping, no vera/ or spec/ change.

 (generic-over-Unit)

Maintainer decisions: fix the #898 checker cross-argument over-reject (not just
the E619 diagnostic), and fix #900 (generic-over-Unit codegen crash) for v0.1.0.
Both now bug-labelled and tracked one-to-one.

Skip-changelog: docs-only bookkeeping.

…uracy

`Eq` auto-derivation over a sparse multi-type-parameter ADT
(`data Res<A, B> { MkOk(A), MkErr(B) }`) on the constructor-inferred path used
to over-reject. Two fixes close it fully.

TASK 1 — cross-argument type-argument merge (the real over-reject).
`eq2(MkErr(5), MkOk("x"))` is a fully-determined `Res<String, Int>` (arg 0
fixes B, arg 1 fixes A) but first-argument-wins binding rejected it with E202.
The checker's inference (`_infer_type_args`/`_unify_for_inference`,
vera/checker/resolution.py) now MERGES per-type-parameter information across the
arguments via a shared `merge_inferred_types` primitive (vera/types.py): a
fresh placeholder yields to the more-determined sibling, a nested per-position
disagreement is a genuine conflict reported as the new E205 ("Conflicting type
argument inference"), and a top-level scalar mismatch stays an ordinary E202
(so `set_add(@set<Nat>.0, "oops")` and the #747 `pick(@Nat.0, @Int.0)` Nat
narrowing are unchanged). The monomorphizer discovery
(`_infer_type_args_from_args`, shared by codegen AND the #732 verifier) and the
WASM call-rewrite (`_resolve_generic_call`) apply the same merge, so all three
consultors emit/reference the identical `Res<String, Int>` clone — the
type-checked call compiles, runs by value, and verifies Tier 1. A per-parameter
conflict is never silently merged (is_subtype backstop); a determined-non-Eq
cross-arg type (`Res<Int, Array<Int>>`) type-checks then rejects E613. A
genuinely under-determined case (`eq2(MkOk(3), MkOk(4))`, B free on both) stays
a correct E202 false-reject.

TASK 2 — E619 diagnostic accuracy.
`_eq_type_arg_under_determined` (vera/codegen/monomorphize.py) emits E619 only
when the type WOULD derive once its free params are Eq-bound (every recovered
component is Eq). A known non-Eq component, recovered (`Res<A, Array<Int>>`) or
structural (`W<A,B>{ K(Array<A>, B) }`), is the accurate E613 instead. A free
slot is materialised as a reserved `?` sentinel (`Res<?, Int>`, never emitted)
so the gate can probe derivability with each free slot provisionally Eq.

Round-3 review polish:
- E619 message no longer leaks the `?` sentinel and its fix is compilable Vera:
  free slots render by their declared parameter name (`Res<A, Int>`) and the
  fix suggests a concrete Eq annotation (`let @res<Int, Int> = ...;`).
- The #732 differential's inline and call-rewrite corpora gain the cross-arg
  merge shape, so a future merge regression is caught by the soundness oracle
  (symmetric collapse trips the vacuous-emission guard; asymmetric one-sided
  merge surfaces as a dangling `eq2$Res` clone). Mutation-validated.
- E205 moved into numeric order in errors.py.
- E619/E613 still emit at line 0 (no call-site span reachable at the mono
  discovery point; pre-existing for E613, not newly introduced).

Mutation-validated (each flips only its discriminating tests RED): neuter
merge_inferred_types; suppress its conflict flag (falls to E202 backstop);
collapse the mono merge; skip the gate's component-Eq probe; drop the WASM-side
merge; leak the E619 sentinel. #772 and #878 untouched; full suite green
(6260 passed). New checker tests, codegen round-2/round-3 tests, differential
corpus entries, and conformance `ch09_multiparam_ctor_eq`.

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

…nation diagnostic (#898)

fix(checker,codegen): cross-argument type-arg merge + accurate Eq under-determination diagnostic (#898)

Found during #900; pre-existing, non-generic. Folding into the #900 PR per
maintainer plan (same Unit-as-degenerate-component design family).

Skip-changelog: docs-only bookkeeping.

…rview table (91% combined) — CR #938 review

TESTING.md's CI-threshold paragraph claimed "Current coverage is 96%", conflicting
with the overview table's "95% Python, 61% JavaScript — 91% combined" (the single
source of truth). Aligned the number and clarified that the Python (pytest --cov)
and JavaScript (V8 / vera/browser/runtime.mjs) flags report to Codecov independently.

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