thermite-spec,thermite-lower: recursion SCHEMES — registry + validator cage + generated folds & fold_bound law (#70)

Basis Stage 2 (epic #62): fold/map/for_all/exists/traverse over recursive
ADTs — the prove-once-instantiate-infinitely engine. 2b (registry +
validator recognition) and 2c (generated Verus folds + fold_bound law +
lowering). Stage 2a was free (a scheme call PARSES as Expr::Call). The exec
mirror (REQ-3, OQ-2) is NOT-STARTED — the v0.1 corpus is spec-only.

DESIGN SOURCES THIS ITERATION:
  - .design/basis/02-recursion-schemes.md (9 REQs; REQ-1/2/4/5/6/7/9 SHIPPED)
  - thermite-design.md §4.2 (named composition, the cage), §4.4 (closed set), §6
  - reference: conformance/list_fold.th + conformance/adt-schemes/cases.json (R-CHAR-3)
  - GROUNDED Verus (verus 0.2026.05.24 --no-cheating): list_len/fold_list/
    for_all_list/fold_bound_list + 3 instances verified 0 errors

REQ STATUS:
  - REQ-1 SHIPPED — schemes.rs `static REGISTRY: [SchemeSig; 5]` + `lookup`;
    consumed by validator::walk_call + lower::collect_scheme_uses
  - REQ-2 SHIPPED — validator::check_scheme flat-step cage (in_scheme_step);
    SpecError::{NestedScheme,SchemeWrongArity,SchemeStepShape}
  - REQ-4 SHIPPED — scheme call accepted as named-composition leaf; nested → NestedScheme
  - REQ-5 SHIPPED — generated fold_<e>/law carry decreases l (Stage-1 dec discipline)
  - REQ-6 SHIPPED — lower::emit_scheme_defs generates fold_<e>/for_all_<e>/<e>_len;
    lower_scheme_call cites them, step → typed spec_fn
  - REQ-7 SHIPPED — emit_fold_bound_law generates fold_bound_<e> (single induction);
    instance cites it, NO fresh induction; negative control (premise dropped) FAILS verus
  - REQ-9 SHIPPED — structured errors, no panics; DEC NUANCE resolved (scheme-call
    instance body lowered WITHOUT spurious decreases — recursion lives in fold_<e>)
  - REQ-3 NOT-STARTED — exec MONOMORPHIZED mirror (corpus spec-only); epic #62
  - REQ-8 NOT-STARTED — fusion laws (map shipped, no fusion-law emission); epic #62

VERIFICATION:
  cargo test --workspace: 138 passed, 0 failed (33 binaries)
  thermite-spec/tests/scheme_validate.rs: 2 passed (list_fold validates; nested_scheme_in_step + unknown_scheme reject)
  thermite-lower/tests/adt_schemes_conformance.rs: 4 passed
    - list_fold → verus --no-cheating "verified, 0 errors" (len_list/sum_list/all_positive L3)
    - multiplier: fold_bound_list + grounded sum_list_bounded instance "verified, 0 errors" (no fresh decreases)
    - negative control: premise removed → verus error (induction is real)
    - list_sum hand-written fold unchanged + verifies (no regression)
  forge check: sum/binary_search/shape/bank_account/list_sum all L3 (no regression)
  cargo clippy --workspace --all-targets -D warnings: PASS
  cargo fmt --all --check: PASS
  verus 0.2026.05.24 present

forge/src/check.rs UNCHANGED: the generated scheme fns are materialized by
the lowerer; the #68 reachable_adt_deps already weaves the enum decl into
each per-item sub-program, so the generated fold_<e> appears in scope.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: dollspace-gay

.design/basis/02-recursion-schemes.md

@@ -695,15 +695,15 @@ authored by the orchestrator from this doc before the builder runs (R-CHAR-3).
 
 | REQ | Status | Evidence |
 |---|---|---|
-| REQ-1 (the scheme set as named primitives; AST = `Expr::Call` + registry, OQ-1 RESOLVED) | NOT-STARTED | epic **#62** Stage 2a. No `fold`/`map`/`for_all`/`exists`/`traverse` scheme recognized in `thermite-spec/src/schemes.rs` (the file does not exist) and no scheme-call resolution; `Expr::Call`/`Expr::Closure` exist in `ast.rs` but admit no scheme today. GROUNDED-feasible (full path `9 verified, 0 errors`), not implemented. Stage 1 (recursive ADTs) is SHIPPED, so the prereq is met. |
-| REQ-2 (the step — flat per-node closure) | NOT-STARTED | epic **#62** Stage 2a/2b. `Expr::Closure` exists (slice-combinator closures) but no scheme-step validation; the flat-closure / no-nested-scheme rule is unimplemented. |
-| REQ-3 (spec form + exec form — exec MONOMORPHIZED, RESOLVED) | NOT-STARTED | epic **#62** Stage 2c (design-refinement: exec form resolved as MONOMORPHIZED, OQ-2). No generated scheme `spec fn` and no exec mirror yet. The SPEC scheme (higher-order passed `spec_fn`, the verified engine) is GROUNDED and unaffected; the EXEC fold is RESOLVED to inline the step into a generated `decreases`-bearing loop (the SHIPPED `conformance/sum.th` while-loop shape), not a higher-order exec function. Not implemented. |
-| REQ-4 (cage bridge — named structural quantification) | NOT-STARTED | epic **#62** Stage 2b. `validator.rs` has no scheme-as-named-composition accept nor the nested-scheme-in-step reject; the caged-flat walk (`walk_expr_inner`, Stage 1 REQ-7) is SHIPPED and admits `Match`/`Field`/`Is` flat — the scheme accept joins it. `for_all_list` cage form GROUNDED (`0 errors`). |
-| REQ-5 (structural `decreases <value>` enforcement) | NOT-STARTED | epic **#62** Stage 2c. The structural-`dec` rule is SHIPPED for hand-written recursive `spec fn`s (Stage 1 REQ-10); the GENERATED scheme `spec fn`s reuse it but the generation itself is unimplemented. GROUNDED: every generated scheme verified with `decreases l`; a no-`decreases` `fold_list` is REJECTED by Verus (negative control). |
-| REQ-6 (scheme → generated Verus recursive `spec fn` + `decreases <value>`) | NOT-STARTED | epic **#62** Stage 2c. `lower.rs` has `is_adt_fold_sum` (SHIPPED, lowers a hand-written recursive fold) but no `lower_scheme_defs` to GENERATE the per-(ADT, scheme) `fold_<e>`/`map_<e>`/`for_all_<e>` nor the scheme-call→generated-call lowering. GROUNDED (full path `fold_list`/`map_list`/`for_all_list` over `List`, `decreases l`, `*tail`, `Box::new`, `9 verified, 0 errors`). |
-| REQ-7 (induction-discharged-once contract shape — the multiplier) | NOT-STARTED | epic **#62** Stage 2c. No generated-law (`lower_scheme_law`) proof-aid emission and no instance-instantiation emission. GROUNDED (FULL path): `fold_bound_list` (single induction) + `sum_list_bounded` (NO induction, CITES the law) `9 verified, 0 errors`; negative control (premise removed) FAILS `8 verified, 1 errors`. |
-| REQ-8 (fusion / composition laws) | NOT-STARTED | epic **#62** Stage 2c. No fusion-law emission in `lower.rs`. GROUNDED: `map_preserves_len_list` (`len_list(map_list(l,g)) == len_list(l)`) `0 errors` (part of the `9 verified` run); `fold∘map` / `map∘map` laws pinned (OQ-3). |
-| REQ-9 (`LowerError`/`SpecError` extension, no panics) | NOT-STARTED | epic **#62** Stage 2b/2c. The scheme reject/lower failure variants are not yet added to the existing error enums in `validator.rs`/`lower.rs`; the structural-`dec` reject reuses Stage 1's SHIPPED recursive-`spec fn` diagnostic. |
+| REQ-1 (the scheme set as named primitives; AST = `Expr::Call` + registry, OQ-1 RESOLVED) | SHIPPED | #70. `thermite-spec/src/schemes.rs` `static REGISTRY: [SchemeSig; 5]` (`fold`/`map`/`for_all`/`exists`/`traverse`) + `lookup`; consumed by `validator::walk_call` (the scheme-call accept) and `thermite_lower::lower::collect_scheme_uses`/`SchemeSig::generated_fn_name`. Asserted against `conformance/adt-schemes/cases.json` in `thermite-spec/tests/scheme_validate.rs::list_fold_validates`. |
+| REQ-2 (the step — flat per-node closure) | SHIPPED | #70. `validator::check_scheme` requires an `Expr::Closure` step of `SchemeSig::step_shape.arity()` params (`SchemeStepShape`) and walks the body in `in_scheme_step` mode; `walk_call` rejects a nested scheme/combinator there with `SpecError::NestedScheme`. Verified: `scheme_validate.rs::reject_cases_yield_the_oracle_error` (`nested_scheme_in_step` → "nested"). |
+| REQ-3 (spec form + exec form — exec MONOMORPHIZED, RESOLVED) | NOT-STARTED | epic **#62** Stage 2c. The SPEC scheme (the generated higher-order `fold_<e>` with the step passed as a `spec_fn`, the verified engine) is SHIPPED (REQ-6). The MONOMORPHIZED EXEC mirror is NOT implemented: the v0.1 corpus `list_fold.th` is SPEC-ONLY (all three items are `spec fn`), so no exec scheme is exercised yet. The exec mirror lands when a corpus exec fn folds an ADT. |
+| REQ-4 (cage bridge — named structural quantification) | SHIPPED | #70. `validator::walk_call` ACCEPTS a top-level scheme call as a named-composition leaf (via `schemes::lookup`) and REJECTS a scheme nested in a step / combinator closure (`NestedScheme`); the caged-flat walk (`walk_expr_inner`, Stage 1 REQ-7) is unchanged. The generated `for_all_list` cage form verifies. Verified: `scheme_validate.rs::list_fold_validates` (`for_all(l, |x| x > 0)` validates). |
+| REQ-5 (structural `decreases <value>` enforcement) | SHIPPED | #70. Each generated scheme `spec fn` (`emit_scheme_spec_fn`) + the law (`emit_fold_bound_law`) carries `decreases l` over the datatype value, inheriting Stage 1's recursive-`spec fn` `dec` discipline. Verified: real `verus --no-cheating` `verified, 0 errors` on the emitted `list_fold.th`; the negative-control no-`decreases` fold is rejected by Verus (grounded during authoring). |
+| REQ-6 (scheme → generated Verus recursive `spec fn` + `decreases <value>`) | SHIPPED | #70. `thermite_lower::lower::emit_scheme_defs` GENERATES `fold_<e>`/`for_all_<e>`/… (`emit_scheme_spec_fn`, `decreases l`, `*tail`, `Box::new`) + the measure `<e>_len`; a scheme CALL lowers via `lower_scheme_call` to a call of the generated fn with the step lowered to a typed `spec_fn` (`lower_step_closure`). Consumer: `lower`. Verified: `thermite-lower/tests/adt_schemes_conformance.rs::list_fold_lowers_to_generated_schemes_and_verifies_l3` (real `verus --no-cheating` `verified, 0 errors`). |
+| REQ-7 (induction-discharged-once contract shape — the multiplier) | SHIPPED | #70. `emit_fold_bound_law` GENERATES `fold_bound_<e>` (single `decreases l` induction, parametric in `f` + a per-node premise); an instance bound is proven by CITING it with NO fresh induction. Consumer: `lower`. Verified: `adt_schemes_conformance.rs::multiplier_instance_cites_the_generated_law_no_fresh_induction` (`verus --no-cheating` `verified, 0 errors`; the instance proof cites `fold_bound_list`, no `decreases`) + `negative_control_premise_removed_fails_verus` (premise removed → verus error; the induction is real). |
+| REQ-8 (fusion / composition laws) | NOT-STARTED | epic **#62** Stage 2c. `map_<e>` generation is shipped (`emit_scheme_spec_fn` `SameAdt`), but no fusion-law (`map_preserves_len_<e>`, `fold∘map`, `map∘map`) emission yet; the v0.1 corpus `list_fold.th` does not exercise `map`/fusion (OQ-3 — the fusion family ships when a pipeline corpus program exercises it). GROUNDED during authoring (`map_preserves_len_list` `0 errors`). |
+| REQ-9 (`LowerError`/`SpecError` extension, no panics) | SHIPPED | #70. `SpecError::{NestedScheme, SchemeWrongArity, SchemeStepShape}` (span-bearing) in `validator.rs`; the scheme lowering reuses `LowerError::Unsupported`/`TooDeep` (a scheme over a non-ADT value / un-resolvable scrutinee). The DEC NUANCE is resolved: a scheme-call instance body lowers WITHOUT a spurious `decreases` (`lower_spec_fn` suppresses it for `is_scheme_call_body`); the generated fold/law carry their own. No `unwrap`/`expect`/`panic!` in `src/`. |
 
 ## Open questions (for the orchestrator before the builder runs)