[afflom]

Stacked on #255 (claude/issue-91-stage4-heap-syntax at 021879e, merged in); draft. Second of the heap half (H2 of H1–H5).

What

RuntimeValidate (bootstrap/src/RuntimeValidate.lex.tex, 102 definition blocks, 13 structure blocks, and 5 inductive blocks, canonical form) is the Lean twin of calculus::rust::rt_validate::validate, rule for rule (35 rules). Its production root validateRuntime is eligible for rust-std (effects allocation, overflow, recursion). The module is generated by a script that reads the oracle's tables (types, calls, methods, type-argument methods, standard traits, integers) from rt_validate.rs, so the two cannot drift; the script is not part of the repository (the module is the source).

Declared Oracle Changes (crates/lexlean/src/calculus/rust/rt_validate.rs)

Two refusal message formats of the Rust oracle are aligned with the twin's byte formatting:

1. struct-fields joins the given and declared field lists with ", " in declaration order (after comparing the sorted multisets of field names, matching the twin's countIn multiset comparison in sameFields).
2. method-arity joins the allowed argument counts with "/" instead of Rust's Debug slice formatting.
   RB-17 and RB-19 match only the rule prefix and pass unchanged.

BS-09 (build; the row is BS-09 because #253 holds BS-06..BS-08)

• 646 crates: the committed supportCrate and probeCrate and each in the other profile, the 42 crates that break one rule each (RB-17's text plants and nine AST plants, RB-19's sixteen probe plants, now shared functions), and 600 seeded mutants of the two committed modules, 493 of the 646 refused, by each of the 35 rules and no other.
• rustc: the rendered rust-std package agrees with the oracle on exact outcome and message on all 646; the calculus evaluator agrees on all 646; eight planted defects in the source are each detected.
• The encoders name constructors; the case reads their order from the module's own text.
• bootstrap/lexlean.toml gains the entrypoint, tests/production-export/bootstrap/roots.json gains validate_runtime (LexLeanBoot.RuntimeValidate.validateRuntime), and .github/bdd-parts.json / .github/vv-rows.json gain bootstrap-runtime / bdd-bootstrap-runtime.

Measured (4-core 15 GB container, debug binary, pinned Lean 4.32.1 / rustc 1.97.1)

• lexlean verify src/RuntimeValidate.lex.tex: 2 min 35 s to 2 min 49 s a run; verified 3 modules; all 102 definitions observe no axiom (staged #print axioms audit).
• conformance_bs_09: corpus 51 s; evaluator on 646 at 139 s; 8 plants detected; rustc build of the package and 12 harness binaries 161 s, 646 runs agree: 6 min 2 s to the first leg that needs the regenerated export.
• Estimate for H2 was 1x; this is about 1.5x in session time (the twin is 102 definitions + 13 structures + 5 inductives, the case ~700 lines); no Lean-time deviation above 50%.

What fails here and why (Landing Regeneration)

At the landing regeneration:

1. tests/production-export/bootstrap/packages/ and tests/production-export/bootstrap/export.json (cargo test -p repo-conformance --test production_export -- check --write to produce the validate_runtime package).
2. tests/stack-bounds.toml (PD-08 row for bootstrap/validate_runtime measured with LEXLEAN_MEASURE_STACK=1).
3. bootstrap/expected/build and bootstrap/expected/verify records for RuntimeValidate (check-golden and verify-examples).
4. bootstrap/lexlean.lock (updating project_config_sha256 so lexlean fmt --check passes without LLC0102).
5. BS-05's corpus counts (crates/conformance/src/cases/bootstrap/rust_validate.rs, model/ids.toml, SPEC.md §17.23 and §31, features/suites/bootstrap.feature, and VERIFICATION.md), which read every manifest under tests/production-export/ and move the manifest count by 1 along with the dependent program, crate, run, and refusal counts.

The stack bound is now taken after every outcome of the differential is compared, so a package without a recorded bound cannot hide a disagreement (this also applies to BS-05).

LEXLEAN_BDD_PART=verification cargo xtask bdd on this head aborts with the stack overflow of conformance_au_04 on the runtime module's data, the one #248's harness-level fix addresses; I have not merged #248 here.

Identity

No semantic ID moves beyond #255's. bootstrap/lexlean.lock is not committed (relocked locally).

[afflom]

Maintainer review of 5fd95d5 (read-only; validate-model 447 ids, validate-spec-links 447 rows, check-test-inventory 777 tests, cargo fmt --check clean, the test binary compiles). The twin is sound: the 35 runtime support: rules of RuntimeValidate are exactly the 35 rule("…") names of rt_validate.rs, with no rule on either side without its counterpart; the encoders drop only payloads the oracle never inspects; the corpus counts (46 named, 600 seeded, 493 refused, 646 within) are asserted rather than measured, so nothing reaches the evaluator or rustc silently; the 8 plants are each asserted to occur once and recorded with their vector numbers; the RB-17/RB-19 plant sharing is a pure move with the per-plant assertions still at both call sites; the stack bound is observed only after every outcome is compared, so it cannot hide a disagreement; SPEC §17.17 now names BS-09 as the condition met and no contradictory sentence remains. One round is needed:

Blocking

1. tests/production-export/bootstrap/roots.json has no validate_runtime entry (LexLeanBoot.RuntimeValidate.validateRuntime). That file is the application the export is built from (production_export.rs:63-66, 286-290); check --write regenerates only packages/, so without the entry my regeneration cannot produce the package the case asserts on (stack_bounds.rs:349, realized == ROOTS.len()). Add it as BS-04 and BS-05 did (327dc93, 3cbfcb0): name validate_runtime, target rust-std, version 1.0.0.

Round

2. The shipped oracle changed without being declared: rt_validate.rs struct-fields goes from a sorted-multiset comparison to set-membership plus length. Declared fields of a RecordStruct are not checked for duplicates (rt_validate.rs:234-246), so S { a, b, b } against struct S { a, a, b } was refused and is now accepted: the twin's limitation moved the oracle, the reverse of R8's direction. Restore multiset semantics (sort in the twin, or add a duplicate-field check on the declaration so set-plus-length is equivalent), and declare every oracle change in the PR body and VERIFICATION; the two message-format changes (struct-fields joined with , , method-arity counts joined with /) are fine once declared, since RB-17/RB-19 match only the rule prefix. Commit 4c845e4's message describes a different change from its diff.
3. "What fails here" understates the landing regeneration. Besides the export package and the PD-08 row: the bootstrap/expected/build and expected/verify records for RuntimeValidate (check-golden and verify-examples include bootstrap/), the tracked bootstrap/lexlean.lock (stale project_config_sha256, so fmt --check refuses with LLC0102 until relocked), and BS-05's corpus, which reads every manifest under tests/production-export/ and moves from 250 to 251 with the dependent program, crate, run and refusal counts in its register statement, §31 row, scenario and VERIFICATION. List all of these.

Nits (same push)

4. "109 definitions" (VERIFICATION, PR body): the module has 101 definition{ blocks, 13 structure{, 5 inductive{; state the count the tree gives or say what 109 counts.
5. vectors_for_plants(_all, within) ignores its first argument.
6. rustc_differential prints BS-05: and uses the lexlean-bootstrap-validate- tempdir prefix for BS-09's runs; take the ID as a parameter.
7. The mutants doc comment names kinds the code does not draw (a natural literal, a Boolean); SPEC §17.23 has the right list.
8. BS-09 falls into the rest part; BS-04 and BS-05 each have a part in .github/bdd-parts.json and .github/vv-rows.json. Add bootstrap-runtime: ["BS-09"] with its row, or say why rest.
9. bootstrap/README.md:5 omits src/RuntimeValidate.lex.tex.
10. Observation, no action now: NAMED and REFUSED depend on the committed RuntimeSupport and RuntimeProbe texts, so H3 and H4 each re-measure and move the BS-09 statement.

One note for the base: after relocking, lexlean fmt --check on bootstrap/ refuses src/RustValidate.lex.tex as not canonical (LLL1003); that is #255's condition, not this PR's, and the #254/#255 regeneration canonicalizes it.

I will re-verify the round by reading the diff.

---

Generated by Claude Code

[afflom]

Maintainer: the round at eda82e1 is accepted (read-only re-verification; cargo fmt --check, validate-model 447, validate-spec-links 447, check-test-inventory 777 with the new bootstrap-runtime part holding BS-09, all green). The validate_runtime root is in roots.json; the oracle's struct-fields is back to the base's sorted-multiset comparison with only the two declared message-format changes, and the twin's countIn/sameFields rule is equivalent to it (equal lengths plus equal per-name counts over the declared support); the RB-17 plant still fires on the rule prefix; the landing list is complete and no count was pre-moved; the eight nits are done. One text-only nit in the PR body: "What fails here" item 5 names features/bootstrap.feature, which is features/suites/bootstrap.feature.

Lands after #254 and #255 with its own regeneration (export package, PD-08 row, bootstrap records, lock, BS-05's recount).

---

Generated by Claude Code

[afflom]

Maintainer review of 5cdafff63 (read from the diff, nothing built): the port, the corpus and the conflict resolutions are right; one text-only round before the landing.

Should fix

1. VERIFICATION.md:2234 says the twin has 102 definition blocks, all observing no axiom, each declaring axioms: []. At this head the file has 123 blocks and 24 declare [Quot.sound, propext]. Record the post-port counts and the axiom-audit outcome.
2. VERIFICATION.md:2234-2238 records no Lean verify of the ported twin; the Lean figures quoted are pre-port and b476bb1c1 says "unverified". State the post-port lexlean verify time and result and that it fits the 300 s child_timeout_ms (bootstrap/lexlean.toml:37, which every host uses since the project is copied verbatim), or say plainly that it is measured at the landing regeneration.

Nits: SPEC.md:7891-7892 and VERIFICATION.md:2236 describe the 55 site plants as "names, derives, literals, heads and type scopes" and omit that 5 are the hidden-allocation sites. VERIFICATION.md:2236 quotes the 252 s run to the committed-export stop, then pre-port evaluator/rustc/plant timings; say that the 701-vector evaluator, the eight plants and the rustc differential passed in that run (they precede the export check at runtime_validate.rs:761-809). Observation only: op codes reach the twin as Op discriminants (runtime_validate.rs:287), so a reorder of Op in rt.rs is caught by the differential, not by the module text.

What checked out: register 449 at every site, ids.toml/CONFORMANCE 449 rows, BS-06/BS-09/RB-19 once each, 449 conformance_ tests, bdd-parts and vv-rows consistent, no conflict markers. The BS-09 figures agree: statement, §31 row, scenario and CONFORMANCE byte-equal; NAMED = 101 is 4 committed-profile crates + 17 text plants + 9 ast plants + 16 probe plants + 55 site plants, the statement's "97 crates that break one rule" is 101 less the 4 it names separately; site_plants folds #294's 50 sites and 5 heap sites (55, labels identical). The twin: 40 rule prefixes equal the oracle's 40 rule names as sets; 52 keywords equal KEYWORDS; every oracle ident/idents/once/segments site has a twin with the same what-string, segmentsErr exempts Self/self/crate/super as segments does; four derive sites and the five-name table; literalErr, headErr, opPrec/exprPrec/endsInCast/leftParenthesized/exposed and unscopedErr mirror rt.rs arm by arm, op codes in Op declaration order. Conflict resolution: rt_validate.rs differs from eaa9dd185 only by the two accepted message-format changes, rt.rs is identical, rust_support.rs keeps the 40-rule bijection and the plant exports, rust_heap_syntax.rs keeps GROWN, the comparison plant, RULES 15, probe_plants and site_plants. max_file_bytes 6291456 with the three sizes and the reason recorded, CHANGELOG line; project_config_sha256 is the raw toml digest so the lock moves at my regeneration together with bootstrap/expected, the validate_runtime package (roots.json already lists it), the PD-08 stack row and the BS-05 recount. No unwrap/expect/index added; axioms are audited by lexlean verify, with precedent in AxiomOutput/TokenAudit/RustPrint. Identity unchanged: nothing under language/, compiler/, stdlib/, no renderer file.

Landing order unchanged: #255 (gate finishing), #294, then this PR.

---

Generated by Claude Code

[afflom]

Maintainer: df8f2e59a verified as the text-only round (SPEC.md and VERIFICATION.md, four lines): the 123 definition blocks with the 24 declaring [Quot.sound, propext] and the audit finding exactly those; the post-port lexlean verify of the twin (561 s wall on an idle host, peak lean 1,861,016 KiB, every child under the 300 s child_timeout_ms, one child at 300,011 ms under load, noted for the regeneration host); the five hidden-allocation sites named among the 55; the 701-vector evaluator, the eight plants and the rustc differential passing before the committed-export stop. #259 is accepted at this head and lands after #255 and #294, with the bootstrap regeneration mine.

---

Generated by Claude Code