Lane 2 Stage 2a: port effects.dag with decompressed effect substrate

[briansrls]

Summary

Supersedes #513 by carrying the src/v3/std/effects.dag Stage 2a port onto a fresh branch and folding the blocker fixes into the staged substrate shape instead of leaving them as review debt.

What Changed

• ports dsl/std/effects.dag into src/v3/std/effects.dag and keeps the Stage 2a parse/bootstrap smoke coverage from Lane 2 Stage 2a: port effects.dag → src/v3/std/ #513
• preserves create-effect provenance with CreateCause, so POST-default create stays distinct from keyless fail-closed fallback on PUT/PATCH/DELETE
• removes the duplicated shape fact from IdempotencyEvidence, leaving OperationEffect.shape as the single authority
• splits modifier results per axis with ModifierAxisCheck, so declared idempotent and readonly facts each carry their own judgment and neither can erase the other
• extends the Stage 2a smoke test to assert the reshaped substrate declarations bootstrapped successfully

Why

PR #513 proved the staged port could parse and bootstrap, but review converged on the same substrate issue: it compressed modifier facts and create-effect provenance at exactly the point where later lanes start consuming this authority. This branch keeps the useful Stage 2a port and rewrites the load-bearing shape now, before Stage 2b learns a lossy model.

Validation

• cargo fmt --all --check
• cargo test --workspace --exclude v2-compiler-tests effects_dag_
• cargo clippy -p v3-compiler --all-targets -- -D warnings

[briansrls]

codex · gpt-5.4 · c7afa5d2

⚠️ Review (blocking: 2, non-blocking: 2+/0-)

BLOCKING (2)

Root Cause

• src/v3/std/effects.dag The port removed the duplicated shape payload from IdempotencyEvidence but kept the duplicated idempotency verdict itself -> make EffectShape the only authority and derive proof/verdict data from it, or encode evidence so it cannot contradict shape.
• src/v3/std/effects.dag The v2 carry-over copied sum types into v3 without also carrying the classification receipts the current substrate review discipline requires -> add per-type 🟢/🟡/🔴 comments, with ledger entries or named dissolution triggers where applicable, before downstream lanes learn these shapes.

Non-blocking — Strengths

• src/v3/std/effects.dag CreateCause and ModifierAxisCheck are real modeling improvements: POST-default versus keyless fallback provenance now survives, and declared idempotent and readonly facts no longer erase each other.
• src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs The new smoke coverage is scoped well for Stage 2a because it separates parse coverage from Dag::new bootstrap coverage and checks the representative declarations later lanes will query.

ROADMAP — Verified

• Lane 2 Stage 2a acceptance: The PR now has the parse plus representative-signature/bootstrap smoke coverage that docs/lane2-compile-time-proofs.md requires for this stage.

⚠️ The port is close, but I would not land a new substrate file with the remaining parallel idempotency authority and the missing coproduct receipts.

[briansrls]

ChatGPT Review

Principle audit.

Fail-closed. Within the staged .dag scope, this looks good. The important failure edges stay explicit rather than fabricated: missing subject keys on PUT/PATCH/DELETE become CreateEffect { cause: KeylessFallback { ... } } instead of a fake InputField, and declared-idempotent POST cases degrade to DerivationUnknown rather than a false proof (src/v3/std/effects.dag:329-338, 358-393, 451-522). The only panics I saw are in the Rust smoke tests, which is fine for test-only code (src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs:15-34).

Illegal states unrepresentable. The previous blocker is fixed: OperationEffect now carries only shape, and idempotency evidence is projected from that on demand, which matches the thesis claim that idempotency is derived from effect shape rather than authored separately (src/v3/std/effects.dag:230-313; THESIS.md:1192, 1770-1782). My one remaining watch-item is DerivedOpEffect { method, path_template, shape } (src/v3/std/effects.dag:351-356): because shape is derived from the other two, contradictory records are still representable, and nothing downstream in this PR actually consumes method or path_template (src/v3/std/effects.dag:495-548). I would treat that as NON-BLOCKING for Stage 2a, but I would not let later consumers learn it casually.

Facts flow forward. This round is much better. The decompressed facts that matter now survive: CreateCause preserves why a create-shaped effect arose, KeySource preserves key provenance, and modifier checking now keeps idempotent vs readonly judgments distinct per axis instead of flattening them (src/v3/std/effects.dag:179-216, 424-522). The new smoke coverage also makes the port load-bearing for this lane instead of just existing on paper (src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs:37-102). The same minor caveat as above applies: DerivedOpEffect.method/path_template are carried forward but not yet consumed.

Coproduct dissolution. This is materially improved. The effect-specific coproducts now have classification receipts inline, and the decompressions look like real modeling wins rather than mechanical churn: CreateCause keeps “real POST create” distinct from “fail-closed keyless fallback,” and ModifierAxisCheck makes “not declared” structurally distinct from “declared and judged” (src/v3/std/effects.dag:186-233, 424-449). I do not see the earlier missing-receipt problem on the effect-facing sum types anymore. The staged http_path copy is also clearly tracked staging debt rather than a silent second system (src/v3/std/effects.dag:14-20, 66-76).

Single authority. The important fix landed: the old shape/evidence dual authority is gone, and EffectShape is back to being the canonical idempotency fact, with IdempotencyEvidence as a derived report carrier (src/v3/std/effects.dag:220-262, 282-313). I also do not count the staged v3 copy itself as untracked debt, because the file header names the bootstrap window and dissolution trigger explicitly, and the thesis does allow milestone-conditional staged grounding during the M1(2.5)→M3 transition (src/v3/std/effects.dag:3-20; THESIS.md:961-985). The only remaining authority question is whether DerivedOpEffect is meant to be durable substrate or just temporary carry-over glue.

API-level enforcement. Better than before. ModifierAxisCheck prevents “declared but no verdict” from being representable, and removing evidence from OperationEffect means callers cannot hand-author contradictory idempotency verdicts at that boundary (src/v3/std/effects.dag:282-313, 432-522). The DerivedOpEffect width issue is still convention-level rather than type-enforced, which is why I’d settle it before 17a gives it a real consumer.

Design question. Is DerivedOpEffect supposed to be a durable substrate type, or is the real downstream boundary just OperationEffect/EffectShape with the transport facts staying at the extdep source?

That matters because the roadmap’s 17a target is “extdeps REST operations tagged with EffectShape,” with evidence and test obligations derived from that (ROADMAP.md:1127-1138). Right now DerivedOpEffect still packages derivation inputs (method, path_template) alongside the derived output (shape) (src/v3/std/effects.dag:351-356, 395-413). If that record is durable, the project is still committing to a wider substrate shape than the roadmap’s consumer model actually needs; if it is just staging glue, this is the cheap moment to collapse it before the first real consumer ossifies around it.

Verdict. APPROVE_WITH_COMMENTS.

The earlier blocking dual-authority problem is fixed, the new decompressions are real improvements, and the smoke coverage makes the port meaningfully load-bearing for Stage 2a. I would land this, but I would answer the DerivedOpEffect question before 17a wiring starts teaching later consumers that the wider record is canonical.

LOOP HEALTH: converging — this round removes the previous blocker, adds real parse/bootstrap acceptance coverage, and leaves only a narrower pre-consumer shape question rather than expanding the debt surface.

---

View conversation

[briansrls]

Meta-Review (Loop Health)

Loop summary.

In the supplied artifacts, I can see 3 review rounds across 2 visible revision states: 1 codex review and 2 browser reviews, all on 2026-04-17 over about 69 minutes. I cannot recover the exact Git commit count from the attachments alone, but the history clearly spans at least two code states because the first browser review still sees OperationEffect { shape, evidence }, while the last browser review says that blocker is fixed.

Forward progress evidence.

This loop did real work. The biggest blocker was not hand-waved; it was removed. The first browser review and codex both flagged the same substrate error: dual idempotency authority. The later browser review confirms that OperationEffect now carries only shape, with idempotency evidence derived on demand. That matches the thesis claim that idempotency must be derived from EffectShape, not stored as a parallel authority.

It also created a real consumer path, even if it is only the smallest one that counts. The roadmap says std/effects.dag is decorative when it has no structural consumer, and Track 17a’s intended end state is extdep REST operations tagged with EffectShape plus derived idempotency obligations. The review history shows this PR now has parse/bootstrap smoke coverage that makes std.effects load-bearing for Stage 2a. That is genuine forward progress under “consumers define correctness,” even though it is not yet the full Track 17a consumer.

The loop also paid off one recurring review class instead of only moving comments around. Codex flagged missing coproduct receipts; the final browser review says those receipts are now inline, and it treats CreateCause, KeySource, and ModifierAxisCheck as real decompressions rather than flat carry-over enums.

Debt accumulation evidence.

The remaining debt is narrow, but it is real. The final browser review explicitly says DerivedOpEffect { method, path_template, shape } is still wider than the roadmap’s intended boundary, because it stores derivation inputs next to the derived fact, and nothing in this PR actually consumes those extra fields. That means the loop solved the worst instance of “parallel authority,” but not the whole class. If Stage 2b/2c consumers learn DerivedOpEffect as canonical, the same problem will come back one layer later.

That is the main reason I am not calling this loop “clean.” The modeling discipline says substrate issues are blocking once they start propagating, and recurring patterns should be promoted into structural rules, not rediscovered per file. This loop did promote the OperationEffect authority split into a real substrate fix, but it did not yet promote the surviving “derived output bundled with derivation inputs” pattern into a stronger invariant or a narrower type boundary.

There is also still staged bootstrap debt: the staged v3 copy and the inline http_path duplication. But the reviews treat that as bounded, named, and carrying a dissolution direction, not as silent debt creep. So it counts as tracked debt, not loop failure.

Cheating signal.

Low. The implementer is documenting compromises instead of hiding them. The staged copy and helper duplication are explicitly named as bootstrap-local debt, and the reviews accept them only because they are bounded and have a dissolution direction. The most recent fix is structural where it mattered most—delete evidence from OperationEffect—and tactical where the blast radius would have widened—leave DerivedOpEffect in place for now. That is accounted triage, not quiet “good enough for now” cheating.

Meta-verdict — ⚖️ SHIP_WITH_DEBT

This loop is making forward progress, but the next round is unlikely to pay for itself. The review cycle already caught and fixed the one blocker that would become much more expensive after merge: dual idempotency authority. It also added a real Stage 2a consumer gate. What remains is explicit, pre-consumer debt around DerivedOpEffect, not hidden rot. Merge this PR, then make the follow-up PR do exactly one thing: collapse or explicitly classify DerivedOpEffect before Track 17a teaches later consumers that the wider record is canonical. Another generic round on this PR is more likely to churn than to change the direction.

---

View conversation

[briansrls]

codex · gpt-5.4 · 92132627

⚠️ Review (blocking: 1, non-blocking: 2+/0-)

BLOCKING (1)

Root Cause

• src/v3/std/effects.dag The inline http_path carry-over documents the file-level staging bridge but never records the type-level dissolution status of the new token coproduct -> add a UrlPathToken receipt (ledger if 🟢, named trigger if 🟡) before downstream lanes consume it.

Non-blocking — Strengths

• src/v3/std/effects.dag CreateCause and ModifierAxisCheck are real decompressions: POST-default versus keyless fallback provenance now survives, and declared idempotent versus readonly judgments no longer erase each other.
• src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs The parse/bootstrap smoke split matches the Stage 2a acceptance gate and makes the staged port load-bearing instead of parse-only.

ROADMAP — Verified

• Lane 2 Stage 2a acceptance: The PR now includes the parse smoke plus representative-signature/bootstrap checks that docs/lane2-compile-time-proofs.md requires for this stage.

⚠️ The earlier blockers are fixed, but I would not land a new substrate port while the staged inline path-token coproduct still lacks its classification receipt.

[briansrls]

BLOCKING: UrlPathToken is a new substrate coproduct with no 🟢/🟡/🔴 receipt, so Stage 2b would still learn an unclassified carrier in violation of modeling-discipline principle 4.

[briansrls]

codex · gpt-5.4 · 92132627

⚠️ Review (blocking: 1, non-blocking: 2+/0-)

BLOCKING (1)

Root Cause

• src/v3/std/effects.dag The inline http_path carry-over documents the file-level staging bridge but never records the type-level dissolution status of the new token coproduct -> add a UrlPathToken receipt (ledger if 🟢, named trigger if 🟡) before downstream lanes consume it.

Non-blocking — Strengths

• src/v3/std/effects.dag CreateCause and ModifierAxisCheck are real decompressions: POST-default versus keyless fallback provenance now survives, and declared idempotent versus readonly judgments no longer erase each other.
• src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs The parse/bootstrap smoke split matches the Stage 2a acceptance gate and makes the staged port load-bearing instead of parse-only.

ROADMAP — Verified

• Lane 2 Stage 2a acceptance: The PR now includes the parse smoke plus representative-signature/bootstrap checks that docs/lane2-compile-time-proofs.md requires for this stage.

⚠️ The earlier blockers are fixed, but I would not land a new substrate port while the staged inline path-token coproduct still lacks its classification receipt.

[briansrls]

ChatGPT review in progress... (view conversation)

Check back in ~30 minutes for the full review.

[briansrls]

ChatGPT Review

Principle audit.

Fail-closed. Mostly satisfied. Missing path keys now fall back to explicit CreateEffect { cause: KeylessFallback { ... } }, and declared-idempotent POST cases degrade to DerivationUnknown instead of false certainty (src/v3/std/effects.dag:335-344, 457-484). I do still see one quiet edge: parse_http_method / derive_op_effect return None on unknown method strings with no structural reason attached (src/v3/std/effects.dag:346-355, 401-419). I would not block Stage 2a on that alone, but it is behavioral rather than truly fail-closed.

Illegal states unrepresentable. This is my remaining blocker. The earlier OperationEffect shape/evidence split is fixed, which is good (src/v3/std/effects.dag:236-318). But ComposedEffect { operations, idempotent, breaking_operation } can still represent contradictions: idempotent = true with breaking_operation = Some(...), idempotent = false with breaking_operation = None, or summaries that disagree with the actual operations list (src/v3/std/effects.dag:282-286, 306-318). The thesis wants idempotency to emerge from structure rather than an authored flag (THESIS.md:1770-1773), and the discipline is explicit that types should not admit “shouldn’t happen” combinations (modeling-discipline.md:34-49). Because this is substrate, I think that is BLOCKING.

Facts flow forward. Mostly satisfied. This round keeps the right decompressed facts alive — CreateCause, KeySource, and per-axis modifier results survive instead of collapsing back to booleans, and the new parse/bootstrap smoke makes the port load-bearing now (src/v3/std/effects.dag:192-239, 430-527; src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs:37-102). I do not see the earlier shape/evidence loss pattern anymore.

Coproduct dissolution. Satisfied now. The missing UrlPathToken receipt is present with a concrete scaffold trigger, and the effect-facing coproducts all have classification comments inline (src/v3/std/effects.dag:78-82, 157-239, 430-448). I would not re-block this lane on coproduct bookkeeping.

Single authority. The prior blocker here is fixed: EffectShape is again the sole idempotency authority, with IdempotencyEvidence projected from it (src/v3/std/effects.dag:236-318). My remaining single-authority concern is the workflow summary: ComposedEffect.idempotent duplicates a verdict already implied by breaking_operation and, more fundamentally, by operations (src/v3/std/effects.dag:282-318). That is a second source, not just a second reader, so I treat it as the same BLOCKING issue as above.

API-level enforcement. Better than before: OperationEffect no longer lets callers hand-author contradictory shape/evidence pairs, and ModifierAxisCheck makes “declared but no judgment” unrepresentable (src/v3/std/effects.dag:288-318, 438-448). But the workflow-level invariant is still convention-only because nothing stops a caller from constructing an inconsistent ComposedEffect directly. A sum-shaped result or a single derived field would enforce it; the current record does not.

Loop health. This round is clearly forward progress: the old dual-authority blocker is gone, the scaffold receipt landed, and the smoke tests give std.effects a real bootstrap consumer. The only debt signal I still see is one smaller version of the same convenience-summary pattern reappearing in ComposedEffect. LOOP HEALTH: converging — the remaining issue is narrower than last round and worth fixing now before Track 17a gives this result type its first real consumer.

Design question. Should workflow-level idempotency be represented as duplicated summary fields, or should the result shape itself encode the verdict?

Right now compose_effects computes a structurally meaningful distinction — “no breaker” versus “broken by operation X” — but the substrate stores it as Bool + Option<String> next to the full operation list (src/v3/std/effects.dag:282-318). If you keep that record shape, later consumers will learn to trust convenience flags again; if you collapse it now to something like IdempotentWorkflow { operations } | NonIdempotentWorkflow { operations, breaking_operation } (or at minimum drop idempotent and derive it from breaking_operation), the type system carries the thesis claim instead of comments carrying it.

Verdict. REQUEST_CHANGES.

The earlier blockers look fixed, and the new receipt change itself is clean. But I would still reshape ComposedEffect before landing, because this is exactly the stage where a small substrate convenience field becomes tomorrow’s second authority.

---

View conversation