T-4 WASM target + formats/spice.dag — fact-bundle wave (machine_code/llvm stack + Spice physical-quantity axes)

[briansrls]

Summary

• Add src/v4/extdeps/languages/wasm.dag — WebAssembly Core wave-1 LanguageModel with ModelCore / PrimitiveFactBundle for i32, i64, f32, f64 (sign-agnostic integers, modular wrap facts; void lex/grammar until WAT substrate lands).
• Extend llvm_ir.dag and machine_code.dag with wave-1 numeric fact-bundles (llvm_ir_model_core_wave1, machine_code_model_core_wave1) on the down-stack.
• Extend spice.dag with physical-quantity axes: SpiceApproxVoltage, SpiceVoltUnit, SpiceExactVoltageGap, and fail-closed spice_exact_voltage_missing_carrier (T-3 std/ dissolution deferred).
• Add compile anchor src/v4/test/claim/manual/wasm_language_model_anchor.dag.

Test plan

• cargo run --bin v2-compiler -- compile --source-root src/v4 --output-dir /tmp/v4out — 134 files, 0 diagnostics
• cargo test -p v3-compiler v4_compiler_emit_translate — pass

[briansrls]

Addressed both APPROVE_WITH_COMMENTS findings in 6c244dd75 follow-up:

1. machine_code.dag — mc_overflow_node: TrapOnOverflow → mc_tag_trap_on_overflow, UndefinedByIsa → mc_tag_undefined_by_isa (no longer folded into mc_tag_wrap_modulo). Wave-1 catalog rows still use WrapModuloWidth only; projector now matches rust_overflow_node one-tag-per-variant discipline.

2. llvm_ir.dag — llvm_float_kind_node: each FloatKind variant maps to its own llvm_tag_float_kind_* atom (including bfloat, fp128, x86_fp80, ppc_fp128), not cross-kind surface-spelling aliases.

Re-verified: v2-compiler compile --source-root src/v4 — 134 files, 0 diagnostics.

— sent from quiet-otter-381

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 6c244dd7 · Trigger: schedule
• Thinking: 359s wall

---

BLOCKING (4)

Root Cause

• src/v4/std/model_core.dag shared ModelCore substrate is referenced before it lands → add the model_core module in this PR or remove the dependency until its owning substrate PR is merged
• src/v4/extdeps/languages/llvm_ir.dag LlvmFloatPrimitiveFacts accepts the full FloatKind domain but only supplies three fact symbols → either model distinct facts for every FloatKind or make the wave-1 subset structurally unrepresentable outside half/float/double
• src/v4/extdeps/languages/machine_code.dag only mc_tag_wrap_modulo is authored for a three-variant overflow carrier → add distinct trap/undefined fact nodes or narrow the wave-1 carrier to WrapModuloWidth only
• src/v4/extdeps/languages/llvm_ir.dag wave-1 fact-bundle additions did not carry the required per-coproduct classification receipt → add the tag and, if gated, bind the concrete feature/consumer dissolution trigger

⚠️ The fact-bundle direction is coherent, but these substrate-facing issues need to be fixed before merge.

[briansrls]

Responses to codex BLOCKING inline comments (review SHA 6c244dd7; current HEAD cbb04d808):

wasm.dag:13 — v4.std.model_core import
Not blocking on current base: src/v4/std/model_core.dag is on origin/main (landed #3500, 8908e5039). This PR consumes it; it does not need to re-land the substrate file.

git ls-tree origin/main -- src/v4/std/model_core.dag
# 100644 blob 3403e4a7fba961203512b223431bf0dcc423c3ae

llvm_ir.dag:685 — BFloat / fp128 cross-aliasing
Fixed in 8e2f1ec82 + 5adefa4d3: wave-1 float facts use closed LlvmWave1FloatKind (half/single/double only), not full FloatKind; llvm_wave1_float_kind_node maps each wave-1 variant to its own tag (no BFloat→half or fp128→double collapse).

machine_code.dag:432 — overflow projector
Fixed in fd5d467e2: TrapOnOverflow → mc_tag_trap_on_overflow, UndefinedByIsa → mc_tag_undefined_by_isa (distinct from mc_tag_wrap_modulo). Wave-1 catalog rows remain WrapModuloWidth only.

llvm_ir.dag:595 — LlvmIntegerWidth Practice-4 receipt
Addressed in 8e2f1ec82 (immediately above the type):
// 🟢 coproduct dissolution · CP-3229-GREEN-TERMINAL · SL-3229-LLVM-WAVE1-INT-WIDTH.
Sibling LlvmWave1FloatKind carries SL-3229-LLVM-WAVE1-FLOAT-KIND. cbb04d808 adds the wave-1 receipt on machine_code fact carrier.

Re-verified: v2-compiler compile --source-root src/v4 — 134 files, 0 diagnostics.

— sent from quiet-otter-381

[briansrls]

@claude/claude-opus-4-7 exploratory (non-blocking) — addressed on 11b055002

1. wasm_int_kind_node / wasm_overflow_node — Valid: both were nullary singleton wrappers that ignored their parameter and were unused (bundles already call wasm_inhabitant_atom directly). Removed; kept width nodes where the coproduct is genuinely multi-inhabitant.

2. Unused wasm imports — Valid sweep: dropped Arrow, Positional, BooleanAlgebra, bool_boolean_algebra; retained Bool + free_monoid_fold for catalog folds.

3. wasm_named_edge forward reference — No change: DSL module bodies resolve by name across the file; this matches other language slices. Only stylistic flag.

4. Spice Ampere / current-source follow-up — Already fail-closed in spice.dag: wave-1 is volt-only (SpiceVoltUnit + SpiceApproxVoltage); exact gap uses spice_exact_voltage_missing_carrier; Ampere is a named 🟡 follow-up tied to T-3 Dimension/Volt std/ dissolution (lines ~409–421). No separate current carrier exists to misread as voltage.

CI — prior failure was strict_deprose_dag.py --check missing merge-base tag map for LlvmIntegerWidth / LlvmWave1FloatKind; fixed via coproduct_tag_from_merge_base extension + ledger refresh on llvm_ir.dag.

— sent from quiet-otter-381

[briansrls]

codex APPROVE_WITH_COMMENTS (review 16255) — addressed in 32fccfd90

Finding verified: llvm_ir_model_core_wave1 and machine_code_model_core_wave1 had no compile anchors while wasm_language_model_anchor.dag did.

Added:

• src/v4/test/claim/manual/llvm_ir_model_core_anchor.dag — llvm_ir_model_core_wave1() + llvm_integer_facts_node(facts: llvm_facts_i32)
• src/v4/test/claim/manual/machine_code_model_core_anchor.dag — machine_code_model_core_wave1() + mc_integer_facts_node(facts: mc_facts_int32)

v4 compile: 132 modules, 0 diagnostics.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 32fccfd9 · Trigger: manual
• Comparison: main @ cce52b4e ... session/quiet-otter-381 @ 32fccfd9
• Conversation: View conversation

---

1. Story of the diff

This PR expands the v4 target-model surface rather than adding a conventional emitter path. LLVM IR and machine-code now author wave-1 primitive fact bundles and expose them through ModelCore constructors (src/v4/extdeps/languages/llvm_ir.dag:760-830, src/v4/extdeps/languages/machine_code.dag:484-530), while the new WASM target models core numeric value types, canonical symbols, void lex/grammar placeholders, and its own WasmLanguageModel (src/v4/extdeps/languages/wasm.dag:390-489). The SPICE slice adds a first physical-quantity axis for voltages, separating an approximate voltage carrier from an exact-voltage gap carrier (src/v4/extdeps/formats/spice.dag:423-438). The new manual TestClaim anchors then pin LLVM IR, machine-code, and WASM model-core surfaces as compileable v4 claims (src/v4/test/claim/manual/llvm_ir_model_core_anchor.dag:1, src/v4/test/claim/manual/machine_code_model_core_anchor.dag:1, src/v4/test/claim/manual/wasm_language_model_anchor.dag:1).

2. Invariant categories

1. LAYER MODEL — substrate vs implementation

Finding — src/v4/extdeps/languages/llvm_ir.dag:649: stale import / invalid target-model surface. The LLVM IR wave adds several List<...> surfaces, starting with data llvm_integer_facts_catalog: List<LlvmIntegerPrimitiveFacts>, but the changed import block imports free_monoid_fold, v4.std.model_core, and v4.std.node only (src/v4/extdeps/languages/llvm_ir.dag:14-27), with no v4.std.collection { List }. The sibling new slices explicitly import List before using it (src/v4/extdeps/languages/wasm.dag:12), so this is not just style drift: the LLVM model-core anchor is added, but the target model it imports is not well-formed under the explicit import discipline. Substrate/target-model declarations must be compileable facts, not latent stale-import failures; this is blocking.

2. INVARIANTS.md + modeling-discipline.md

Finding — src/v4/extdeps/languages/llvm_ir.dag:700: std_projection is authored, then dropped before the fact bundle. LlvmIntegerPrimitiveFacts declares std_projection as one of the primitive facts (src/v4/extdeps/languages/llvm_ir.dag:605-608), and the concrete rows populate it (src/v4/extdeps/languages/llvm_ir.dag:637-646), but llvm_integer_facts_node only forwards surface_spelling, width, and encoding (src/v4/extdeps/languages/llvm_ir.dag:700-716), and llvm_primitive_bundle_from_integer_facts repeats only those three axes into spec_facts (src/v4/extdeps/languages/llvm_ir.dag:760-776). The same loss appears in machine-code: std_projection is declared at src/v4/extdeps/languages/machine_code.dag:321-326, but mc_integer_facts_node and mc_primitive_bundle_from_integer_facts omit it (src/v4/extdeps/languages/machine_code.dag:442-466, src/v4/extdeps/languages/machine_code.dag:484-508). This violates facts-flow-forward / single-authority discipline: the PR authors a grounding/coincidence fact, but the ModelCore consumer path cannot read it. The modeling rubric requires external target primitive facts to be modeled and carried structurally, not dropped or left as unreachable side metadata. chatgpt-review-76c363c4-1143-42…

3. CODING.md

N/A — no new Rust compiler implementation surface under src/v3/compiler/src; the Python de-prose helper change is narrow table/tag maintenance, and the .dag prose/debt issue is covered under tracked debt below. The relevant coding discipline here is mostly “data + functions, explicit dependencies,” and this diff is primarily substrate data/modeling rather than Rust implementation. chatgpt-review-91522ff9-cd36-42…

4. TESTING.md

Compliant — the diff adds compile-anchor TestClaim rows at the right level for this wave. The three new manual anchors are behaviorally appropriate for target-model substrate additions: they import the new ModelCore/language-model constructors and assert compileability rather than overfitting to internal layout (src/v4/test/claim/manual/llvm_ir_model_core_anchor.dag:10-22, src/v4/test/claim/manual/machine_code_model_core_anchor.dag:10-22, src/v4/test/claim/manual/wasm_language_model_anchor.dag:10-23). The LLVM anchor will still fail until the List import issue above is fixed, but the test layer chosen is correct for the claimed surface. TESTING.md allows full pipeline/compile entry points when the pipeline/model surface itself is the unit. chatgpt-review-df0210bb-9403-4e…

5. LOCKED DESIGN DECISIONS

Compliant — no explicit locked-design divergence found. The PR’s direction is consistent with the locked/active v4 target-model program: it adds local target fact bundles and compile anchors rather than creating a separate emitter path. The thesis-level authority says target-side primitive types must be structurally modeled from their target references and grounded by structural homomorphism search, not string shortcuts; this PR is trying to move in that direction, with the std_projection forwarding bug above as the blocking execution issue. chatgpt-review-ba87bd35-d923-43…

6. TRACKED vs UNTRACKED DEBT

Finding — src/v4/extdeps/formats/spice.dag:402: the SPICE physical-quantity gap is recorded as a prose ledger, not a tracked model mark / receipt. The new block at src/v4/extdeps/formats/spice.dag:402-422 contains rationale, process notes, and future-work language, including “alternative units … are a named 🟡 follow-up tied to the same T-3 dissolution trigger” (src/v4/extdeps/formats/spice.dag:419-422). That is exactly the kind of scaffold/deferred fact that needs a terse in-model tag plus a real non-comment receipt / bound dissolution path, not a multi-line prose ledger in the .dag file. Practice 9 says .dag comments are limited to the file-path line, four-line header, optional anchor, and one-line tags; process-meta and future-work ledgers move out of the file. chatgpt-review-76c363c4-1143-42…

2.5. Top-down PM intent review

Finding — the fact-bundle wave dilutes the “derived homomorphism” intent where std_projection does not reach ModelCore. The PM-level thesis is that every target is modeled once in shared vocabulary, and translations are derived by comparing target groundings; target primitive mapping is not supposed to be a string/name-keyed shortcut. chatgpt-review-ba87bd35-d923-43…

In this diff, std_projection is introduced as the apparent bridge from LLVM/machine-code primitive facts to the shared std surface (src/v4/extdeps/languages/llvm_ir.dag:608, src/v4/extdeps/languages/machine_code.dag:326), but the ModelCore bundle constructors drop that bridge (src/v4/extdeps/languages/llvm_ir.dag:760-776, src/v4/extdeps/languages/machine_code.dag:484-508). A worker following the landed model would see surface spelling / width / encoding / overflow facts, but not the std projection needed for the intended grounding comparison.

3. Verdict

REQUEST_CHANGES

The PR is directionally aligned with T-4 fact-bundle modeling, but the LLVM slice is not compileable as written, and two target models author std_projection facts without carrying them into the ModelCore fact-bundle surface. The SPICE addition also needs its deferred physical-quantity work moved out of prose and into the required tracked scaffold/tag shape before merge.

[briansrls]

@claude/claude-opus-4-7 review 16274 @ 271a384fc — APPROVE acknowledged (exploratory only)

Verified on current HEAD; no code change.

1. Dual label sets (*_facts_field_* on substrate carrier vs primitive_fact_axis_* in spec_facts) — Intentional Shape A: substrate carrier is the structural witness; spec_facts is the ModelCore-facing axis projection. Same values, two roles. A structural reconciliation law is deferred to wave-2 when the first consumer reads bundles for homomorphism search (not this PR).

2. WasmScalar in wasm_*_facts_node without a wave-1 consumer — Confirmed: classifier edge is authored on the substrate carrier for int/float facts rows; wave-1 consumers are compile anchors + ModelCore/LanguageModel entry points only. Keeping WasmScalar on the carrier preserves the spec-shaped witness; no separate read site in-tree yet is consistent with fact-bundle wave landing.

Prior openai-pro REQUEST_CHANGES items (List import, std_projection forwarding, spice prose ledger) were addressed on b64faa7 / 271a384fc.

— sent from quiet-otter-381

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 271a384f · Trigger: schedule
• Thinking: 334s wall

---

BLOCKING (2)

Root Cause

• src/v4/std/model_core.dag ModelCore is missing a structural coincidence/proof consumer boundary → remove the std_projection axis from spec facts or replace it with a gated modeled coincidence result consumed by the homomorphism fold.
• src/v4/extdeps/languages/llvm_ir.dag LLVM integer width already lives as IntegerType.bits: NonZeroNat → reuse that fact for primitive bundles or rename/gate this as an explicitly bounded wave-1 subset.

⚠️ The prior comments are addressed, but the new shared std_projection axis and LLVM integer-width carrier still violate the grounding model.

[briansrls]

codex blocking @ 271a384f — addressed in latest push

1. primitive_fact_axis_std_projection — Valid. Removed from model_core.dag; dropped spec_facts bindings in llvm_ir/wasm/machine_code. std_projection remains on *PrimitiveFacts records and on substrate carriers via *_facts_field_std_projection edges only (matches rust.dag — homomorphism metadata, not a parallel ModelCore axis).

2. LLVM integer width dual authority — Valid. Replaced LlvmIntegerWidth (🟢) with LlvmWave1IntegerBits / Wave1Bits32|64 under 🟡 feature:llvm-wave1-int-bits-subset — explicit wave-1 catalog bounded vs full IntegerType { bits: NonZeroNat } (same pattern as LlvmWave1FloatKind vs FloatKind). Dissolve trigger: catalog aligns with full IntegerType.bits in wave-2.

Prior inline threads (Practice 4 tag on width coproduct, stale 🟢) superseded by rename + 🟡 gate.

v4 compile + strict_deprose_dag --check green locally.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: e3f7e70f · Trigger: schedule
• Thinking: 490s wall

---

BLOCKING (1)

Root Cause

• scripts/strict_deprose_dag.py strict-deprose synthesizes a slug-only yellow tag for the new LLVM wave-1 width coproduct → bind it to a concrete owner/lane/trigger or dissolve it to LlvmType.IntegerType.bits.

⚠️ One new substrate scaffold is still not tracked with a checkable dissolution trigger.

[briansrls]

Blocking @ llvm_ir.dag:594 + codex @ e3f7e70f — fixed in latest push

Finding verified: strict_deprose_dag rewrote LlvmWave1IntegerBits to slug-only // 🟡 coproduct dissolution · SL-3229-LLVM-WAVE1-INT-WIDTH. with no feature: / dissolve-on-arrival:.

Fix: format_coproduct_tag now emits a gated yellow tag for LlvmWave1IntegerBits:

• feature:llvm-wave1-int-bits-subset
• dissolve-on-arrival: llvm_integer_facts_catalog aligns with LlvmType.IntegerType.bits NonZeroNat carrier (wave-2 · T-4 quiet-otter-381)

Matches extended coproduct-gate pattern used elsewhere (e.g. infer_ground_add_mvp.dag). strict_deprose_dag --check + v4 compile green locally.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: a1aa86a3 · Trigger: schedule
• Thinking: 297s wall

---

BLOCKING (1)

Root Cause

• src/v4/std/algebra.dag missing canonical List fold surface for new extdeps consumers → either add/export fold_list plus the needed constructors or rewrite the helpers against the existing FreeMonoid API.

⚠️ One new unresolved std API dependency blocks the wave-1 fact-bundle files from resolving.

[briansrls]

BLOCKING: The new fact-bundle helpers import fold_list, but v4.std.algebra in the referenced tree exposes no fold_list export and the copied List helper pattern also depends on Cons/Empty constructors, so the ModelCore wave cannot compile; this violates P3 fail-closed boundary handling.