fix(codegen/verifier): monomorphize nested generic where-helpers and thread origin-module tables into imported-generic clones

[aallan]

Summary

Fixes the two mono-pipeline bugs the cluster grounding paired: #990 (a forall<T> where-helper under a non-generic parent is never monomorphized — check-green, verify-green, unknown func at compile) and #998 (mono clones of imported generics compile with the importer's span tables, silently dropping the #820 @Nat → @Int widen guards the library's vera verify promised Tier-3 — u64.MAX → -1, no trap).

#990 — nested generic discovery, codegen and verifier in lockstep by construction

Generic discovery collected mono bases from top-level program.declarations only. A generic helper nested in a non-generic function's where block was invisible: no clone emitted, the parent's concrete-typed call lowered to the bare unmangled name, and WAT assembly failed.

Both sides now build their base set with one shared collector (vera/monomorphize.py collect_nested_generic_decls), used by codegen Pass 1.5 and the verifier's instance discovery — so the two sides collect the identical set and each nested instantiation is emitted and verified per-monomorphization (_verify_fn's forall dispatch already keys on the decl name; the discovery fill is all it needed). The collector stops at the first generic node in either direction: a generic helper's own subtree is carried per-clone and hoisted by the #904 path, so nothing double-emits (pinned at the WAT level). The Pass-2 where-fn sweep likewise stops at a generic template's subtree, and the template-warning suppression set now includes nested templates.

#998 — clone provenance: origin-module tables for imported-generic clones

The module harvest records each unshadowed imported generic's origin path (_imported_generic_origins); every emitted clone of an imported base is tagged (_mono_clone_origins) at all three emission sites — the main worklist, the shadowed mod$… worklist, and the shadowed-body transitive chase — and per-clone hoisted where-helpers inherit their clone's origin. The mono compile loop then threads imported=True + that module's module_artifacts table for tagged clones exactly like Pass 2.5/2.6 bodies (monomorphization preserves node spans, so the template module's table keys the clone body correctly; absent tables fall back to the #986 suppression, never a wrong-file guard). A local generic's clones carry no tag and keep the main-file tables.

Evidence

• RED-first: tests/test_generic_where_helper_990.py failed with the exact unknown func $gid diagnostic (4 tests); the flipped tests/test_xmod_generic_widen_gap.py failed with trap kind None (silent widen) at the unshadowed, shadowed, and hoisted-helper doors. All 15 flipped GREEN with the fix; controls (Generic forall<T> fn with a where-block helper crashes codegen (unknown func: helper not found) #904 hoisting, local-clone guard, shadowed in-range) were green throughout.
• Cross-component lockstep: a nested_generic_where_helper corpus entry in the Per-monomorphization static verification for generic functions #732 differential (tests/test_monomorphize_differential.py) was RED against the codegen-only fix (codegen emitted gid instances the verifier never discovered) and is GREEN with the shared collector — the invariant now pins the lockstep permanently.
• Seven-mutant battery, all killed: codegen discovery drop, verifier discovery drop, main-worklist origin drop, shadowed origin drop, hoist-propagation drop, imported=False mis-flag, and flatten-descends-into-generic — each REDs its specific test (the last one required a T-independent grandchild observable, added for exactly that reason).
• Conformance: new run-level tests/conformance/ch09_generic_where_nongeneric_parent.vera with an enforced sentinel (156 programs); full suite 7,298 tests, mypy clean, 37 examples.

Discovered along the way (filed, queued — no deferrals)

The grounding probes surfaced two pre-existing siblings (confirmed identical at the 75f1ff4 base): #999 (a nested generic inside an imported function — discovery never seeds from module bodies) and #1000 (a private module generic reached transitively from an exported one — never harvested as a clone base). Both are loud unknown-func failures, filed with repros and fix directions; KNOWN_ISSUES + SKILL rows ride this PR.

Scope honesty

• A bare-name collision between a nested generic and a top-level generic resolves top-level-wins (matching how plain where-helpers flatten today); per-scope duplicate-name semantics are Duplicate where-helper names crash WAT assembly (duplicate func identifier) instead of a diagnostic; pre-#978 variant ran silently wrong #991's subject, queued next.
• Imported-generic clone bodies still resolve sibling calls by bare name (no module_renames threading on the mono path) — unchanged by this PR; clone naming/resolution attribution remains the #661 latent gap (comment updated to say exactly which half Monomorphized clones of imported generic fns drop the #820 component widen guards — library verify promises Tier-3, importer runs unguarded #998 added).

Docs lockstep

KNOWN_ISSUES/SKILL rows for #990/#998 deleted and #999/#1000 added; spec/11's widening paragraph now states imported-generic clones are guarded (one remaining component site: the E531 generic field, #757); CHANGELOG bullets for both fixes plus the #987 bullet's residual clause updated; TESTING.md rows and all counts reconciled (7,298 tests / 156 conformance), site assets regenerated.

Closes #990
Closes #998

Summary by CodeRabbit

• Bug Fixes

  • Improved cross-module generic instantiation so widening checks remain effective, including shadowed calls and imported where helpers.
  • Fixed nested generic where-helper cloning/hoisting issues (e.g., #990) and addressed related generic-instantiation gaps across module boundaries.
  • Updated widening-guard coverage for @Nat→@Int to reflect only the remaining unguarded @Int field warning.

• Tests

  • Added regression tests covering nested forall where helpers and imported generic widening/trap behaviour.
  • Conformance suite expanded to 156 programs (total tests 7,309).

• Documentation

  • Refreshed project status metrics, conformance/testing guidance, known-issue listings, and updated @Nat→@Int spec wording.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 3fbaecd8-7ac4-4544-9610-2e88a21b42fc

📥 Commits

Reviewing files that changed from the base of the PR and between ca7e592 and 8a6aab6.

📒 Files selected for processing (1)

• tests/test_generic_where_helper_990.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)

---

📝 Walkthrough

Walkthrough

This change discovers nested generic where-helpers, preserves imported monomorphisation origins for widening guards, adds regression and conformance coverage, and updates compiler documentation and project metrics.

Changes

Generic monomorphisation and widening guards

Layer / File(s)	Summary
Nested helper discovery and clone generation vera/monomorphize.py, vera/verifier.py, vera/codegen/monomorphize.py	Nested forall<T> helpers are collected through where trees and included in verifier and codegen monomorphisation discovery.
Imported origin propagation and guarded compilation vera/codegen/modules.py, vera/codegen/core.py, vera/codegen/monomorphize.py	Imported generic bases, clones, shadowed clones, and hoisted helpers retain origin modules so compilation uses the corresponding module tables and widening guards.
Conformance and regression coverage tests/conformance/manifest.json, tests/test_generic_where_helper_990.py, tests/test_monomorphize_differential.py, tests/test_xmod_generic_widen_gap.py	Tests cover nested helper cloning, duplicate suppression, imported and shadowed widening traps, hoisted helper provenance, transitive imports, and local generic behaviour.
Specification and project documentation AGENTS.md, CHANGELOG.md, CLAUDE.md, FAQ.md, KNOWN_ISSUES.md, README.md, ROADMAP.md, SKILL.md, TESTING.md, spec/11-compilation.md	Documentation records 156 conformance programmes, revised test counts, issue status, and updated widening-guard coverage.

Estimated code review effort: 4 (Complex) | ~45 minutes

Sequence Diagram(s)

sequenceDiagram
  participant Verifier
  participant Monomorphize
  participant CodeGenerator
  participant ModuleTables
  Verifier->>Monomorphize: discover nested generic where-helpers
  Monomorphize->>CodeGenerator: emit concrete clones and record origins
  CodeGenerator->>ModuleTables: select origin module tables
  ModuleTables-->>CodeGenerator: provide span and target-type tables

Loading

Possibly related issues

• A generic where-helper under a generic ancestor is never monomorphized — clone hoisting leaves its own forall unbound (unknown func at compile) #1002 — Covers nested generic discovery and clone-hoisting under generic ancestors.
• A forall where-helper under a non-generic parent is never monomorphized — check/verify green, compile fails unknown-func #990 — Covers monomorphising nested forall<T> helpers under non-generic parents.
• Imported function bodies never get generic-instantiation discovery (nested helper, or an imported generic called from another module's body) — unknown func at compile #999 — Concerns related nested generic discovery and imported instantiation paths.
• Monomorphized clones of imported generic fns drop the #820 component widen guards — library verify promises Tier-3, importer runs unguarded #998 — Covers preserving imported generic clone origins for widening guards.
• @Nat → @Int widening: remaining deferred coercion sites (follow-up to #813) #820 — Tracks the related cross-module widening-guard work.

Possibly related PRs

• aallan/vera#767 — Also changes generic verification and instantiation discovery.
• aallan/vera#989 — Also changes where-helper flattening and emission logic.

Suggested labels: compiler, tests, spec, docs

🚥 Pre-merge checks | ✅ 7 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 36.17% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.

✅ Passed checks (7 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title accurately summarises the two main fixes: nested generic where-helper monomorphisation and origin-module table threading for imported generic clones.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Changelog Covers Public-Surface Changes	✅ Passed	CHANGELOG.md explicitly covers the public-surface behaviour changes (#987/#998/#820 and #990), including the spec/11 widening-guard updates.
Spec And Implementation Move Together	✅ Passed	PASS: the #998 widen-guard behaviour is reflected in spec/11, and the #990 nested where-helper fix fits existing §11.4.3 where-block semantics.
Diagnostics Carry An Error Code	✅ Passed	PASS: the PR’s touched user-facing diagnostics already carry E/W codes; only pre-existing internal/exempt fallbacks omit codes, and they weren’t introduced here.

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch fix/990-998-mono-pipeline

---

_{Comment @coderabbitai help to get the list of available commands.}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 93.47%. Comparing base (75f1ff4) to head (8a6aab6).

Additional details and impacted files

@@                Coverage Diff                 @@
##           release/v0.1.4    #1001      +/-   ##
==================================================
+ Coverage           93.45%   93.47%   +0.01%     
==================================================
  Files                  96       96              
  Lines               31734    31771      +37     
  Branches              456      456              
==================================================
+ Hits                29658    29697      +39     
+ Misses               2063     2061       -2     
  Partials               13       13              

Flag	Coverage Δ
javascript	78.41% <ø> (ø)
python	95.26% <100.00%> (+0.01%)	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[coderabbitai]

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@TESTING.md`:
- Around line 171-175: Update the dual-target conformance differential
description in the test_wasi_target.py row to state 127 run-level conformance
programs instead of 126, and search the entire TESTING.md file for remaining
stale 126 references related to this count so all occurrences stay consistent
with the overview total.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 88c28eca-7229-4176-8fa3-76c6dcb994ae

📥 Commits

Reviewing files that changed from the base of the PR and between 75f1ff4 and 010f30a.

⛔ Files ignored due to path filters (6)

• docs/SKILL.md is excluded by !docs/**
• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• tests/conformance/ch09_generic_where_nongeneric_parent.vera is excluded by !**/*.vera

📒 Files selected for processing (19)

• AGENTS.md
• CHANGELOG.md
• CLAUDE.md
• FAQ.md
• KNOWN_ISSUES.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• spec/11-compilation.md
• tests/conformance/manifest.json
• tests/test_generic_where_helper_990.py
• tests/test_monomorphize_differential.py
• tests/test_xmod_generic_widen_gap.py
• vera/codegen/core.py
• vera/codegen/modules.py
• vera/codegen/monomorphize.py
• vera/monomorphize.py
• vera/verifier.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)

[aallan]

Review round — 3 pr-review agents + 3-lens adversarial panel

The mechanism survived everything thrown at it: the panel confirmed zero findings across its three lenses, and the round's changes are coverage hardening, one mutant-battery hole closed, an honest docs correction, and two pre-existing bugs filed.

The soundness story (panel, independently of the PR's own tests)

Lying-contract matrix (lens 1): a nested generic with a false ensures is caught as an honest E500 (naming the failing instantiation with a concrete counterexample) through every discovery route — body call, contract-predicate-only, transitive via a sibling nested generic, Bool-only instantiation, and the import door. The base-vs-head differential proves the probes reach the new code: at the base the same lie verifies clean (E520 downgrade) and the call dangles at compile. The ensures+run differential holds over the newly-verified population (proved ⇒ never violated at runtime across input sweeps incl. extrema), per-instantiation aggregation names only the failing instantiation (a pigeonhole contract true at T=Bool, false at T=Int, reports exactly pig<Int>), and the meet-aggregation ordering makes a false Tier-1 impossible by construction. A corpus-wide sweep (all conformance + examples) found zero codegen-emitted instances the verifier doesn't cover.

Origin-routing matrix (lens 2): local+imported generics mutually instantiated route to their own tables (both directions trap at u64.MAX; at base the imported side silently returned -1); same-named public generics in two modules are a hard duplicate-definition error in both import orders, so the first-seen-wins pairing hazard is unreachable; transitive and shadowed-chase clones trap at head where base silently widened. The decisive probe: an engineered main-file span collision (a non-widen Array<Nat> literal at the exact span of the library's widen site) — the tagged clone reads the module table and traps correctly, while monkeypatching the origin recording to a no-op reproduces the silent -1. The tag is load-bearing exactly where the pre-#987 collision hazard lived, and the guard cannot over-fire by construction (a correct tag resolves to the clone's own checker-assigned targets).

Structure (lens 3): WAT is byte-stable across hash seeds (the new dicts introduce no iteration-order effects), same-(name,types) instantiations from body + sibling + contract dedup to one clone, uninstantiated nested templates keep their E604 warning while instantiated ones are suppressed per-name (not over-broad), warm re-registration doesn't accumulate stale instances, and nested clones are never exported.

Fixed in this round

1. Chase-site mutant hole (test-analyzer): the original seven-mutant battery covered the main-worklist origin recording but not _chase_normal_transitive's — and the first transitive tests I added were killed by the wrong path (main-worklist transitivity). The shadowed-body chase shape (lib::wrap → unshadowed widening sibling) is the only population that exercises that site; it now REDs the mutant.
2. Transitive widen coverage (test-analyzer): same-module outer→inner and 3-module-chain shapes — both silently -1 at base, both genuinely fixed by this PR, previously untested. Whole-module imports deliberately (the filtered form hits the pre-existing Imported function bodies never get generic-instantiation discovery (nested helper, or an imported generic called from another module's body) — unknown func at compile #999-family wall).
3. Three more fixed shapes pinned: contract-only reachability (+ a differential corpus entry), nested-to-nested transitivity, recursion in a nested generic (compile+run harness — an exact ensures over opaque recursion is a pre-existing E500).
4. SKILL Imported function bodies never get generic-instantiation discovery (nested helper, or an imported generic called from another module's body) — unknown func at compile #999 workaround corrected (comment-analyzer, empirically refuted): hoisting the helper does NOT work — the imported parent body is never scanned. Rewritten to the verified escapes; KNOWN_ISSUES row broadened to the mechanism level (no nesting required — the review probes hit it with a plain imported fn calling a transitively-imported generic).
5. Two docstring corrections (code-reviewer + test-analyzer): _flatten_where_fns no longer claims "at any depth" unqualified, and collect_nested_generic_decls no longer overclaims that hoisting handles a generic descendant's own forall — it doesn't, which is…

Filed from this round: #1002 (+ #999 broadened)

The probes found generic helpers under a generic ancestor are never monomorphized — clone hoisting substitutes only the ancestor's type vars, leaving the descendant's own forall unbound (check-green AND verify-green over an uncompilable program). Pre-existing at base (verified in a pinned worktree; the #990 fix advances the failure one level deeper in one shape but does not cause it). Filed as #1002 with tracker rows and an honest-pin test riding this PR; #999 was retitled/broadened with the no-nesting-required evidence.

Methodology note

All probe work ran in pinned per-commit worktrees (the #997 round's contamination lesson) — zero cross-agent interference this time.

[coderabbitai]

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@tests/test_generic_where_helper_990.py`:
- Around line 276-307: Update
test_generic_under_generic_ancestor_still_dangles_1002 to assert that at least
one error diagnostic contains “unknown func” by checking all entries in errs,
rather than indexing errs[0]. Preserve the existing failure message and `#1002`
pin behavior.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 21bf4313-c663-484c-8ff2-8de888e1e078

📥 Commits

Reviewing files that changed from the base of the PR and between 010f30a and ca7e592.

⛔ Files ignored due to path filters (2)

• docs/SKILL.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**

📒 Files selected for processing (11)

• FAQ.md
• KNOWN_ISSUES.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• tests/test_generic_where_helper_990.py
• tests/test_monomorphize_differential.py
• tests/test_xmod_generic_widen_gap.py
• vera/codegen/core.py
• vera/monomorphize.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)