Skip to content

Dissolution upstream P6 — std/algebra.dag+std/nat.dag fold/cata FreeMonoid+Nat Wave-A2 [#3243 §1.1] - #3249

Merged
briansrls merged 2 commits into
mainfrom
session/royal-raven-52
May 18, 2026
Merged

Dissolution upstream P6 — std/algebra.dag+std/nat.dag fold/cata FreeMonoid+Nat Wave-A2 [#3243 §1.1]#3249
briansrls merged 2 commits into
mainfrom
session/royal-raven-52

Conversation

@briansrls

@briansrls briansrls commented May 18, 2026

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session royal-raven-52.
Pushing to session/royal-raven-52 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

@briansrls
briansrls marked this pull request as ready for review May 18, 2026 02:31
briansrls
briansrls commented May 18, 2026
View reviewed changes

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 4a1d4723 · Trigger: schedule
  • Thinking: 160s wall

Non-blocking — Strengths

  • src/v4/std/algebra.dag The new FreeMonoid fold is the canonical structural eliminator and the derived predicates now consume it instead of repeating Empty/Cons recursion.
  • src/v4/std/nat.dag The new Nat catamorphism centralizes Zero/Succ recursion and keeps nat_add and nat_mul as derived consumers of that authority.

✅ No blocking concerns for this .dag std-model change.

@briansrls briansrls mentioned this pull request May 18, 2026
Merged
1 task
briansrls
briansrls commented May 18, 2026
View reviewed changes

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: c7d0523b · Trigger: schedule
  • Thinking: 170s wall

Non-blocking — Strengths

  • src/v4/std/algebra.dag free_monoid_fold gives FreeMonoid a canonical eliminator, and the derived helpers now consume it instead of matching the coproduct directly.
  • src/v4/std/nat.dag nat_cata centralizes Nat structural recursion, and nat_add/nat_mul now derive through that authority without adding a second representation.

✅ No blocking concerns for this .dag std-model change.

briansrls added a commit that referenced this pull request May 18, 2026
@briansrls @claude
docs: design-dissolution-lens.md (B1) — dissolution-lens enforcement …
f561f28 
…spec (#3275)

* docs: design-dissolution-lens.md (B1) — the dissolution-lens enforcement spec

Specifies the enforcement mechanism for Practice 10's dissolution
findings (rework-tracker PR #3240 task B1): a lens family of
deterministic structural checks over the .dag model, run as hard CI
gates.

Two layers: Layer 0 = standard compiler hygiene (unused var/param/import/
declaration, exhaustiveness, ignored result, …) — the floor every
mainstream compiler enforces, on by default in every profile; Layer 1 =
the dissolution lenses (discriminant-predicate / degenerate-type /
hollow-type / carrier-clone / catamorphism), composing Layer-0
primitives. Includes the selective-profile model (scope→profile,
compiler substrate runs the strictest), the issue→invariant→lens
methodology, the discriminant-vs-catamorphism distinction, and a living
slipped-by ledger root-causing #3250/#3255/#3256/#3249.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* design-dissolution-lens: address still-hawk B1 review (R1, R2, minor)

R1 — add L1.6 emit/template lens. The keystone lists emit/template
dissolution as structurally decidable ("a literal template-string
field"); a structurally-decidable finding gets a lens, not silent
omission.

R2 — reconcile §7's scaffold contradiction. §7 forbids a file dialing
its own profile, but the scaffold profile used a "// scaffold:" file
marker. Reworded: the marker is the in-file record of a reviewer-
approved, ratchet-only, scope-level decision, not self-service; Layer 0
stays on under scaffold; and the keystone's 🟡-binds-a-plan mandate is
profile-independent — turning Layer 1 off suppresses the CI hard-error,
never the modeling obligation (else "// scaffold:" = invisible debt).

Minor — L1.3 cites Practice 8 (hollow-alias) so "hollow declarations"
does not read as a new finding name.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 18, 2026
@briansrls @claude
design-dissolution-lens: §9 — model-derived lens only, no interim scr…
36ccc86 
…ipt (#3283)

* docs: design-dissolution-lens.md (B1) — the dissolution-lens enforcement spec

Specifies the enforcement mechanism for Practice 10's dissolution
findings (rework-tracker PR #3240 task B1): a lens family of
deterministic structural checks over the .dag model, run as hard CI
gates.

Two layers: Layer 0 = standard compiler hygiene (unused var/param/import/
declaration, exhaustiveness, ignored result, …) — the floor every
mainstream compiler enforces, on by default in every profile; Layer 1 =
the dissolution lenses (discriminant-predicate / degenerate-type /
hollow-type / carrier-clone / catamorphism), composing Layer-0
primitives. Includes the selective-profile model (scope→profile,
compiler substrate runs the strictest), the issue→invariant→lens
methodology, the discriminant-vs-catamorphism distinction, and a living
slipped-by ledger root-causing #3250/#3255/#3256/#3249.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* design-dissolution-lens: address still-hawk B1 review (R1, R2, minor)

R1 — add L1.6 emit/template lens. The keystone lists emit/template
dissolution as structurally decidable ("a literal template-string
field"); a structurally-decidable finding gets a lens, not silent
omission.

R2 — reconcile §7's scaffold contradiction. §7 forbids a file dialing
its own profile, but the scaffold profile used a "// scaffold:" file
marker. Reworded: the marker is the in-file record of a reviewer-
approved, ratchet-only, scope-level decision, not self-service; Layer 0
stays on under scaffold; and the keystone's 🟡-binds-a-plan mandate is
profile-independent — turning Layer 1 off suppresses the CI hard-error,
never the modeling obligation (else "// scaffold:" = invisible debt).

Minor — L1.3 cites Practice 8 (hollow-alias) so "hollow declarations"
does not read as a new finding name.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* design-dissolution-lens: §9 — model-derived lens only, no interim script

Operator decision: the dissolution lens must be compiler-integral /
model-derived ("actually mechanical"), not a bolt-on Python checker. A
scripts/check-* script that text-scans .dag is itself a hand-rolled
.dag-walker — the anti-pattern the lens exists to remove (§9 already
said "the lens cannot be hand-rolled either"; the interim-checker step
contradicted it). §9 rewritten: no interim script form; the lens is
gated on the v4 front-end (CP-1) + the v4 lens stage; until then the
interim net is the reviewer prompts + burn-down pre-gate, not a script.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls
briansrls force-pushed the session/royal-raven-52 branch from 824d9ad to 16e2ef6 Compare May 18, 2026 07:02
@briansrls
briansrls merged commit f78fb9e into main May 18, 2026
7 checks passed
This was referenced May 18, 2026
Closed
Closed
briansrls
briansrls commented May 18, 2026
View reviewed changes

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 824d9ad2 · Trigger: schedule
  • Thinking: 191s wall

✅ Mixed design/std .dag substrate PR; I found no blocking concerns against the thesis or modeling invariants.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@briansrls