T-4.17 Wave 2b: wasm type deepening + AlgebraInhabitanceDecl fill (deps T-4/T-33/T-2; SM5 gate dissolved #3697) by briansrls · Pull Request #3831 · gunb-ai/gunbc

briansrls · 2026-05-28T20:35:31Z

Summary

Adds wasm Wave 2b type deepening to wasm.dag:

Inhabitance: i32/i64 → commutative_semiring_type_node; f32/f64 → approximate_field_type_node, each with grounded witness Nodes (P2 single-authority: algebra field carries type node, not inhabitance wrapper).
Laws: WasmModelCoreLawKey coproduct with full 🟡 dissolution scaffold (feature/owner/dissolve-on-arrival).
Effects: pure signatures for wasm integer/float numeric operations.
Partiality: fail-closed div_s/div_u/rem_s/rem_u on zero divisor; div_s on signed quotient overflow (idiv_s only; irem_s returns 0 for INT_MIN /-1) (INT_MIN / -1 trap).
Entry points: wasm_model_core_wave2b() / wasm_language_model_wave2b() (wave1 aliases delegate here).
Ratchets: smoke test v4_wasm_language_model_declares_wave2b_algebra_inhabitance (+0 SG-0 paths), anchor updated to wave2b, strict_deprose_dag.py ledger tag for WasmModelCoreLawKey.
P5 receipt: INVARIANTS.md row for v4_compiler_emit_translate_smoke_test.rs documents the wasm same-path expansion under ROADMAP § T-PB-B deferral (matching Python wave-2b pattern).

Test plan

python3 scripts/strict_deprose_dag.py --check — pass
cargo test -p v3-compiler v4_wasm_language_model_declares_wave2b_algebra_inhabitance — pending current-head CI
Dashboard reviews on current HEAD — pending

Notes

No merge-ready assertion until current-head dashboard reviews (≥2 approvals, no REQUEST_CHANGES) and CI green. Operator merges manually.

…l (deps

briansrls · 2026-05-28T21:11:40Z

Review metadata

Provider / model: openai-pro / gpt-5-5-thinking
Commit: 66e8c66f · Trigger: manual
Comparison: main @ 252b7b18 ... session/snappy-wolf-136-wasm-wave2b @ 66e8c66f
Conversation: View conversation

1. Story of the diff

This PR deepens the Wasm v4 language model from a wave-1 primitive-fact bundle into a wave-2b ModelCore population. src/v4/extdeps/languages/wasm.dag now derives algebra inhabitance rows from the integer/float fact catalogs, builds law obligations, records pure operation effect signatures, and marks integer division/remainder as fail-closed partial operations. It also preserves the old *_wave1 entrypoints as aliases to the new wave-2b entrypoints, updates the manual compile anchor to consume wasm_model_core_wave2b, and extends the existing Rust smoke harness to assert that the Wasm model imports the new algebra/model-core surfaces. chatgpt-review-9ffedc2b-d87f-4e…

2. Invariant categories

LAYER MODEL (substrate vs implementation). Finding — src/v4/extdeps/languages/wasm.dag:1762 introduces a substrate-facing 🟡 coproduct, WasmModelCoreLawKey, and src/v4/extdeps/languages/wasm.dag:1887 consumes it through wasm_law_kind_symbol; the tag is only SL-T4-WAVE2B-WASM-LAW-KEY, with no feature:/consumer: gate or bound dissolution trigger. Because this is an extdeps language model feeding ModelCore, the yellow scaffold needs the same full modeling discipline as other substrate-facing carriers.
INVARIANTS.md + modeling-discipline.md. Finding — same issue: Practice 4 requires every 🟡 coproduct to bind a concrete named arrival and dissolve-on-arrival plan; here the diff adds the coproduct at src/v4/extdeps/languages/wasm.dag:1762, and the companion allowlist marks it only as scaffold:T-4-wave-2b at scripts/strict_deprose_dag.py:307, which is a milestone label, not a named missing primitive/consumer. Modeling discipline explicitly says a bare sunset milestone is not a valid gate, and an untracked 🟡 blocks merge. chatgpt-review-a94a0858-74a3-42…
CODING.md. Compliant — the new Rust test is small and interface-oriented: v4_wasm_language_model_declares_wave2b_algebra_inhabitance checks import/function surfaces without adding hidden state, panics outside test context, or new production Rust behavior.
TESTING.md. Compliant — the PR adds a focused smoke assertion for the new Wasm wave-2b algebra inhabitance surface in the existing v4 language-model integration harness, and updates the manual .dag compile anchor from wave-1 to wave-2b. This is the right level for the current parse/compile-anchor phase, though it remains structural smoke coverage rather than semantic law execution.
LOCKED DESIGN DECISIONS. Compliant — the change moves in the locked direction: Wasm target facts are authored in the extdeps language spec and consumed through std.model_core/std.algebra Node constructors, not through a compiler-side lookup table or emitter special case.
TRACKED vs UNTRACKED DEBT. Finding — src/v4/extdeps/languages/wasm.dag:1762 plus scripts/strict_deprose_dag.py:307 create a yellow law-key scaffold, but the diff does not state the three required properties: a concrete gate kind, the missing primitive/consumer, and the dissolution trigger. SL-T4-WAVE2B-WASM-LAW-KEY is a receipt slug; by itself it does not tell the next worker when the coproduct must dissolve.

2.5. Top-down PM intent review

Compliant with one blocking tracking defect. The PM-level intent behind T-4.17 Wave 2b is preserved: Wasm’s target model is moving toward structurally declared primitive facts, algebra inhabitance, law obligations, effects, and partiality, which supports the thesis goal that target grounding is modeled once in the shared substrate and then read mechanically. The only intent risk is the unbound yellow law-key coproduct: as written, it can become permanent scaffold rather than a dissolved bridge, which conflicts with the project’s progress-as-dissolution discipline.

3. Verdict

REQUEST_CHANGES

The Wasm wave-2b modeling direction is solid, and the main ModelCore population looks coherent. But the new WasmModelCoreLawKey 🟡 scaffold is not sufficiently tracked: add a concrete feature: or consumer: gate plus its bound dissolution trigger, or dissolve the law-key enum now.

Align wasm.dag law-key scaffold comment with typescript/rust Wave 2b precedent (feature:model-core-law-expression-carrier, owner, and dissolve-on-arrival trigger). Teach strict_deprose_dag to emit the same long-form tag for WasmModelCoreLawKey as TsModelCoreLawKey. Addresses cursor + openai-pro REQUEST_CHANGES on #3831.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 887934ac · Trigger: schedule
Thinking: 232s wall

BLOCKING (2)

Root Cause

src/v3/compiler/tests/integration/v4_compiler_emit_translate_smoke_test.rs the new smoke ratchets commutative_semiring_node/approximate_field_node imports rather than the type-node constructors → require the *_type_node constructors and build the inhabitance rows from actual wasm inhabitant nodes.
src/v4/extdeps/languages/wasm.dag Wave-2b partiality vocabulary only has divisor-nonzero/divide-by-zero symbols → add signed-overflow precondition/discharge facts and attach them to wasm_op_integer_div_s.

⚠️ The new ModelCore rows need the algebra carrier shape fixed and the missing WebAssembly signed-division trap modeled before this lands.

Sign in to view

+
+fn wasm_integer_algebra_inhabitance(facts: WasmIntegerPrimitiveFacts) -> AlgebraInhabitanceDecl {
+  let inhabitant = wasm_integer_facts_node(facts: facts)
+  AlgebraInhabitanceDecl {


Sign in to view

+
+fn wasm_partiality_semantics_wave2b() -> PartialitySemanticsDecl {
+  PartialitySemanticsDecl {
+    operations: [


- AlgebraInhabitanceDecl.algebra: commutative_semiring_type_node / approximate_field_type_node (not inhabitance wrapper *_node carriers) - Partiality: add signed-quotient-overflow precondition/discharge for wasm_op_integer_div_s and wasm_op_integer_rem_s (WASM idiv_s/irem_s trap) - Smoke test ratchets *_type_node imports Addresses blocking review on #3831 (P2 single-authority + P1 spec fidelity). Co-authored-by: Cursor <cursoragent@cursor.com>

Co-authored-by: Cursor <cursoragent@cursor.com>

…l (deps

WebAssembly irem_s returns 0 for INT_MIN rem_s -1; only idiv_s traps on that edge. Remove the incorrect rem_s quotient-overflow partiality row. Addresses cursor REQUEST_CHANGES review 19833 on #3831. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls

Review metadata

Provider / model: codex / unknown
Commit: ae92452a · Trigger: schedule
Thinking: 260s wall

BLOCKING (1)

Root Cause

src/v4/extdeps/languages/wasm.dag Wave-2b folds only the primitive facts catalogs, which do not carry the canonical wasm_inhabitant_i32/i64/f32/f64 identity → fold algebra inhabitance and law rows over records that carry both inhabitant id and facts, then build with wasm_integer_inhabitant_node/wasm_float_inhabitant_node.

⚠️ One substrate authority split remains in the new Wasm ModelCore algebra rows.

Sign in to view

+}
+
+fn wasm_integer_algebra_inhabitance(facts: WasmIntegerPrimitiveFacts) -> AlgebraInhabitanceDecl {
+  let inhabitant = wasm_integer_facts_node(facts: facts)


…l (deps

…pt row Reconcile HEAD wasm Wave 2b same-path expansion with origin/main PR #3840 MVP-1 ratchet paragraph; remove committed conflict markers. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 93f75542 · Trigger: schedule
Thinking: 312s wall

ROADMAP — Verified

T-PB-B pb_rust_tests_outside_residual_zero: The same-path Rust smoke expansion is receipted in INVARIANTS with +0 SG-0 paths under the concrete T-PB-B row.

✅ No blocking concerns found in the current diff.

Unblocks CI strict_deprose_dag import test (SyntaxError on main from #3831). Co-authored-by: Cursor <cursoragent@cursor.com>

Per r4-program-dispatch-plan.md row 6 ("De-prose Python removal — Delete now"): remove the de-prose Python ratchet wholesale rather than patching it. - scripts/strict_deprose_dag.py — deleted - scripts/test_strict_deprose_dag.py — deleted - .github/workflows/ci.yml — drop the "v4 strict-deprose script self-test (Python)" and "v4 strict-deprose allowlist (--check; merge-base + Part 6 inventory)" steps The immediate trigger: the WasmModelCoreLawKey branch added in #3831 dropped the trailing tuple lines, leaving an unclosed `(` at line 446 and breaking py_compile on every PR. Patching that block would cement a script we have already chosen to dissolve; the dispatch-plan accepts a brief enforcement gap until lens enforcement lands. Note: scripts/refresh_v4_dissolution_tag_authority.py imports from strict_deprose_dag and will break on next ad-hoc invocation. It is not on CI and is left for a follow-on disposal PR rather than expanded scope here. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Per r4-program-dispatch-plan.md row 6 ("De-prose Python removal — Delete now"): remove the de-prose Python ratchet wholesale rather than patching it. - scripts/strict_deprose_dag.py — deleted - scripts/test_strict_deprose_dag.py — deleted - .github/workflows/ci.yml — drop the "v4 strict-deprose script self-test (Python)" and "v4 strict-deprose allowlist (--check; merge-base + Part 6 inventory)" steps The immediate trigger: the WasmModelCoreLawKey branch added in #3831 dropped the trailing tuple lines, leaving an unclosed `(` at line 446 and breaking py_compile on every PR. Patching that block would cement a script we have already chosen to dissolve; the dispatch-plan accepts a brief enforcement gap until lens enforcement lands. Note: scripts/refresh_v4_dissolution_tag_authority.py imports from strict_deprose_dag and will break on next ad-hoc invocation. It is not on CI and is left for a follow-on disposal PR rather than expanded scope here. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls and others added 3 commits May 28, 2026 20:35

WIP: T-4.17 Wave 2b: wasm type deepening + AlgebraInhabitanceDecl fil…

b09e095

…l (deps

WIP: T-4.17 Wave 2b: wasm type deepening + AlgebraInhabitanceDecl fil…

acabf8a

…l (deps

merge origin/main into session/snappy-wolf-136-wasm-wave2b

887934a

briansrls marked this pull request as ready for review May 28, 2026 21:08

fix(wasm.dag): align strict_deprose header and law-key coproduct tag

66e8c66

briansrls commented May 28, 2026

View reviewed changes

briansrls and others added 4 commits May 28, 2026 22:27

chore: apply cargo fmt after wasm wave2b smoke test update

91aacaf

Co-authored-by: Cursor <cursoragent@cursor.com>

WIP: T-4.17 Wave 2b: wasm type deepening + AlgebraInhabitanceDecl fil…

7221386

…l (deps

briansrls commented May 28, 2026

View reviewed changes

Comment thread src/v4/extdeps/languages/wasm.dag Outdated

}

fn wasm_integer_algebra_inhabitance(facts: WasmIntegerPrimitiveFacts) -> AlgebraInhabitanceDecl {

let inhabitant = wasm_integer_facts_node(facts: facts)

This comment was marked as resolved.

Sign in to view

briansrls added 2 commits May 28, 2026 23:37

WIP: T-4.17 Wave 2b: wasm type deepening + AlgebraInhabitanceDecl fil…

5864ecf

…l (deps

WIP: T-4.17 Wave 2b: wasm type deepening + AlgebraInhabitanceDecl fil…

041fbb8

…l (deps

briansrls force-pushed the session/snappy-wolf-136-wasm-wave2b branch from 35349d4 to 041fbb8 Compare May 28, 2026 23:39

fix(invariants): resolve merge conflict in emit-translate smoke recei…

93f7554

…pt row Reconcile HEAD wasm Wave 2b same-path expansion with origin/main PR #3840 MVP-1 ratchet paragraph; remove committed conflict markers. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls mentioned this pull request May 28, 2026

T-4.17 Wave 2b: wasm type deepening + AlgebraInhabitanceDecl fill (deps T-4/T-33/T-2; SM5 gate dissolved #3697) #3851

Closed

6 tasks

briansrls commented May 29, 2026

View reviewed changes

Merge branch 'main' into session/snappy-wolf-136-wasm-wave2b

81283b0

briansrls merged commit f6c2f8a into main May 29, 2026
2 checks passed

briansrls added a commit that referenced this pull request May 29, 2026

fix(scripts): close WasmModelCoreLawKey return in strict_deprose_dag

a8a2187

Unblocks CI strict_deprose_dag import test (SyntaxError on main from #3831). Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls mentioned this pull request May 29, 2026

chore: delete strict_deprose_dag.py + test + 2 CI steps #3864

Merged

2 tasks

briansrls deleted the session/snappy-wolf-136-wasm-wave2b branch June 1, 2026 18:43

Navigation Menu

Repository navigation

T-4.17 Wave 2b: wasm type deepening + AlgebraInhabitanceDecl fill (deps T-4/T-33/T-2; SM5 gate dissolved #3697) - #3831

T-4.17 Wave 2b: wasm type deepening + AlgebraInhabitanceDecl fill (deps T-4/T-33/T-2; SM5 gate dissolved #3697)#3831
briansrls merged 13 commits into
mainfrom
session/snappy-wolf-136-wasm-wave2b

briansrls commented May 28, 2026 •

edited

Loading

Uh oh!

briansrls commented May 28, 2026

Uh oh!

briansrls left a comment

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls left a comment

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented May 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Test plan

Notes

Uh oh!

briansrls commented May 28, 2026

1. Story of the diff

2. Invariant categories

2.5. Top-down PM intent review

3. Verdict

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 28, 2026 •

edited

Loading