Optimize certificate data builders and restore host-matrix timeout (#177)

[afflom]

Closes #177

Summary

Makes the certificate A and B kernel-data builders linear in match arm count and short-circuits repeated term transformations across large modules, cutting non-Lean conformance time by 3×–10.7× across the six slowest tests (conformance_sp_02, conformance_sp_08, conformance_sp_10, conformance_sp_12, conformance_tc_05, and certificates(wide_match(240))) without deleting or thinning any conformance test or certificate assertion:

1. Precomputed arm suffix lists (crates/lexlean/src/production/certificate/data_a/matching.rs, structural.rs, boundary.rs):
   • Added Writer::prepare_arms (PreArm), which translates each arm's (shape, binders, body) once and builds the right-to-left List.cons suffix chain in $O(n)$ before iterating over arms.
   • arm_hit and arm_miss now index directly into pre: &[PreArm] in $O(1)$ per step instead of rebuilding the remaining suffix of arms on every step ($\Theta(n^3) \to O(n^2)$ total term allocations across all arms).
2. Bottom-up term metadata (clean, loose, min_free) and $O(1)$ short-circuits (crates/lexlean/src/production/kernel.rs, crates/lexlean/src/production/kernel/ext.rs):
   • Propagated clean (meta-free), loose (loose de Bruijn variable bound), and min_free (minimum free-variable ID) bottom-up in $O(1)$ inside Builder::push.
   • Updated Builder::resolve / resolve_memo to look up meta_id(term) directly in solved: &HashMap<usize, Term> and skip a second pass when every value in solved is already meta_clean.
   • Added $O(1)$ short-circuits using min_free and loose_bound to abstract_over, lift, instantiate, instantiate_beta, substitute, and has_placeholder.
3. Linear reverse cursor in Aligner (crates/lexlean/src/production/certificate/data_b/align.rs):
   • Updated Aligner::m and Aligner::m_arm to advance a reverse cursor across arms in $O(n)$ instead of scanning from index 0 on every arm.
4. Direct core assembly (crates/lexlean/src/sdk.rs, crates/lexlean/src/production/certificate.rs) and cached correspondence rules (crates/lexlean/src/production/preserve.rs):
   • Added sdk::assemble_core and updated record_source to print CoreModule directly without serializing it to a multi-MB JSON string and re-parsing it first.
   • Updated correspondence_rules() to reuse the cached native() OnceLock instead of re-parsing RustCorr.lex.tex and RustSound.lex.tex on every call.
5. Host-matrix timeout (.github/workflows/ci.yml):
   • Restored host-matrix timeout-minutes from 300 back to 120.

Local Timings (Before vs. After on x86_64-unknown-linux-gnu)

Test	Before (193cd2148)	After (5ac8a788c)	Speedup
certificates(wide_match(240)) (--lib)	59.98s	11.76s	5.1×
conformance_sp_02	1374s	128.88s	10.7×
conformance_sp_08	~1600s	295.36s	5.4×
conformance_sp_10 (non-Lean)	163s	36.12s	4.5×
conformance_sp_12	124s	41.36s	3.0×
conformance_tc_05	307s	52.86s	5.8×

Verification

• just fmt-check
• just lint
• cargo xtask verify-governance
• cargo xtask audit-production
• cargo test --manifest-path crates/lexlean/Cargo.toml --lib
• cargo test --manifest-path crates/conformance/Cargo.toml --test conformance conformance_sp_02 -- --exact
• cargo test --manifest-path crates/conformance/Cargo.toml --test conformance conformance_sp_08 -- --exact
• cargo test --manifest-path crates/conformance/Cargo.toml --test conformance conformance_sp_10 -- --exact
• cargo test --manifest-path crates/conformance/Cargo.toml --test conformance conformance_sp_12 -- --exact
• cargo test --manifest-path crates/conformance/Cargo.toml --test conformance conformance_tc_05 -- --exact

[afflom]

@afflom @humuhumu33 Full ready-for-review gate run 39122833578 is 25/25 green (honesty and reproducibility also green: 27/27 checks passed, mergeStateStatus: CLEAN) on 838b47c6b, which contains main (193cd2148).

Whole-Gate Timing Comparison (39122833578 vs. Train 39101767733)

Job	Train (39101767733)	PR #189 (39122833578)	Delta
build and non-Lean tests (aarch64-unknown-linux-gnu)	58m 00s	38m 45s	−19.2 min
build and non-Lean tests (aarch64-apple-darwin)	78m 00s	45m 03s	−33.0 min
build and non-Lean tests (x86_64-pc-windows-msvc)	69m 00s	46m 44s	−22.3 min
build and non-Lean tests (x86_64-apple-darwin)	100m 00s	50m 51s	−49.1 min
just vv (bdd-preservation)	93m 00s	46m 35s	−46.4 min
Subtotal (4 host-matrix legs + bdd-preservation)	398.0 min	228.0 min	−170.0 runner-minutes
Whole gate (all 25 jobs)	730.0 min	596.4 min	−133.6 runner-minutes

[afflom]

Rebased cleanly onto main (d51d9f223, wave 2) at eff2cd382 and verified cargo xtask validate locally. Full ready-for-review gate is running now. cc @afflom @humuhumu33

[afflom]

Maintainer: this PR's head 838b47c6b is merged unchanged into wave 3, #191 (with #188 and #175), so that one gate covers the three; #191 merges on its green gate and this PR is then closed by hand with a pointer. Please hold further pushes here; anything new goes in a comment and I carry it. The host-matrix timeout-minutes is 240 on the wave rather than the 120 this PR restores, because BS-02 now runs on every host (#190); this run measures the new slowest host time.

---

Generated by Claude Code

[afflom]

Landed through wave 3, #191, merged to main as efea57d85: this branch's head 838b47c6b is merged there unchanged, so its commits are in main's history and #177 is closed by that merge with the acceptance measurement recorded on the issue (Intel mac 140 → 104 min, Windows 105 → 65, whole gate 872 → 698 runner-minutes). The only difference from this PR is the host-matrix timeout-minutes (240 on main, not 120), explained on #177 and #190. Closing this PR by hand.

---

Generated by Claude Code