Design: proof-carrying `wsc.facts` section — loom forwards Z3-discharged invariants to synth

[avrabe]

Proposal (Tier 1 of the post-#228 inliner/codegen feature loop)

The structural opportunity. loom runs after meld fuses the whole world into one closed module, and it already runs a Z3 translation validator on every transform. That combination — closed world + a theorem prover in the loop — is exactly what an open-world MCU LLVM build can't have. Today the loom→synth boundary is lossy wasm: synth must re-derive (or conservatively assume away) every fact loom already proved. This proposes a proof-carrying side channel so synth lowers with facts it could never derive itself.

What

A new custom section wsc.facts (sibling to the existing wsc.transformation.attestation) carrying machine-checkable invariants loom's validator can already discharge, keyed by (function index, instruction offset / SSA value). Candidate fact kinds:

• value range — v ∈ [lo, hi] (e.g. status ∈ [0,1], idx < len)
• shift bound — shift amount < 32/< 64 ⇒ synth emits a bare lsl/lsr, no mask-and-mod materialization
• select totality — a select's condition is total / side-effect-free ⇒ branchless it/csel
• divisor-nonzero — div_u/rem_u divisor ≠ 0 ⇒ drop the trap check
• in-bounds access — a load/store offset is provably within a known allocation ⇒ drop the bounds check
• memory disjointness — two regions provably don't alias ⇒ reorder/keep-in-register across them

synth consumes these as assumptions, not as things to prove. loom stays the prover; synth stays a cheap code generator that trusts proven facts.

Why it can't be forged downstream

An MCU LLVM build compiles each symbol for an open world (unknown callers) with no SMT in the loop, so it must be conservative at every boundary. loom's facts come from the closed fused module + Z3 — unforgeable downstream. This is the highest-leverage "beat-LLVM" lever (the wasm itself is already good per the gust bench; the wins are synth-side).

Open questions for co-design (gale — this is a loom↔synth CONTRACT, so I want your input before I build loom's emitter)

1. Encoding — which keying does synth want: function-index + wasm instruction byte-offset? a stable per-value id? Compact binary vs JSON (attestation is JSON today)?
2. Fact priority — which of the kinds above moves the gust/cortex-m3 cycle needle most? (My guess from Seam-inlining not firing on the gust hot path (mix/transition survive as calls) #226/inline_functions never inlines small multi-call-site leaves (size<10 OR-term shadows MULTI_CALL_SITE_LIMIT); + optimize CLI lacks whole-function DCE #228: shift-bound + select-totality + value-range, since those drove the synth spill/materialization you measured.) Let's order by silicon payoff.
3. Trust model — does synth re-check facts (belt-and-suspenders) or trust loom's signature? Ties into the Release standard: add witness + scry wasm gates, crates.io/npm, rivet verification extraction #227 release-standard (witness/scry gates).
4. Versioning/skew — loom and synth version independently; how do we make a fact-schema mismatch fail safe (synth ignores unknown fact kinds)?

I'll scaffold the loom side (which facts the validator can emit cheaply from its per-function results) once we agree the format. Refs the gust bench (#226, #228) and the closed-world specialization follow-up (Tier 2).

cc @avrabe