diff --git a/docs/design-composed-effect-reshape.md b/docs/design-composed-effect-reshape.md new file mode 100644 index 00000000000..1f39cf2954c --- /dev/null +++ b/docs/design-composed-effect-reshape.md @@ -0,0 +1,254 @@ +> Part of: [lane2-compile-time-proofs.md](./lane2-compile-time-proofs.md) (Lane 2 Stage 2a follow-up) | Unblocks: Lane 2 Stage 2b (workflow idempotency lens), Track 17a REST wiring + +# Design Brief — `ComposedEffect` reshape + +**Brief:** Brief A (Lane 2 Stage 2a / Track 17a boundary follow-up) +**Consumers:** Stage 2b workflow-idempotency lens; Stage 2c test-obligation materialization; Track 17a REST consumers (once wired). +**Status:** Implemented — with two revisions in response to PR review on commit `b42edc15`. +- **R1 (landed at `b42edc15`):** lifted the `Bool + String?` summary into `CompositionVerdict = IdempotentComposition | BrokenBy { first_breaker: OperationEffect }` wrapped in `ComposedEffect { operations, verdict }`. +- **R2 (responding to codex review):** partitioned `EffectShape` into `IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)` and narrowed `BrokenBy` to `BreakingOperation { shape: BreakingShape }`. Fixed the inner-variant hole (idempotent ops could no longer be named as the breaker). +- **R3 (responding to ChatGPT review):** dropped `ComposedEffect` entirely. `compose_effects` now returns `CompositionVerdict` directly. The R2 record still correlated two fields — the `operations` walk and the `verdict` — that the constructor could keep coherent by convention but the type could not. `.dag` records are directly constructible, so any caller could build an incoherent `ComposedEffect`. R3 fixes the outer-record hole by deleting the record. + +After R3 the verdict carrier is structurally sound all the way down: `CompositionVerdict` is a sum whose each variant is internally coherent, and there is no correlated sibling field for it to disagree with. The evidence chain (`List`) stays at its natural site — the caller's input — not duplicated onto the output. + +--- + +## Problem + +`src/v3/std/effects.dag` ships `ComposedEffect` as: + +```dag +type ComposedEffect { + operations: List + idempotent: Bool + breaking_operation: String? +} +``` + +The record admits illegal state combinations: + +| `idempotent` | `breaking_operation` | Meaning | +|--------------|----------------------|----------------------------------------------| +| `true` | `None` | ✅ Workflow is idempotent. | +| `false` | `Some(name)` | ✅ Workflow broken by `name`. | +| `true` | `Some(name)` | ❌ Contradiction — idempotent but has breaker. | +| `false` | `None` | ❌ Non-idempotent but no breaker to blame. | + +`compose_effects` happens to produce only valid combinations today, but that is a *behavioral* invariant (an `iff` the constructor maintains) rather than a *state-space* invariant (an `iff` the type enforces). This is the same bug class `feedback_state_space_vs_behavioral_invariants` names: a `Bool` + correlated `Option` pair should be a single sum whose variants are exactly the valid combinations. + +The roadmap deferral at `src/v3/ROADMAP.md` §"Lane 2 Stage 2a / Track 17a boundary" already prescribes the direction: + +> ... before any Track 17a consumer lands. ... at minimum drop redundant `idempotent`, or **better encode "no breaker" versus "broken by operation X" in the type shape itself**. + +Stage 2b's idempotency lens (which consumes `compose_effects`) and Stage 2c's test-emission layer (which consumes `generate_idempotency_obligations`) are not yet written. Stage 2b's `WorkflowIdempotencyReport` (designed in `lane2-compile-time-proofs.md` §Stage 2b) wraps `ComposedEffect` and re-exposes the same boolean + optional breaker pair; locking the structural shape *before* the lens ships keeps the illegal states out of the lens report too. + +No current consumer reads `.idempotent` or `.breaking_operation` — grep shows the type is only parsed (smoke test) or re-exported (v2 bootstrap). This is the window. + +--- + +## Design + +### R3 — drop the outer record; partition `EffectShape`; narrow the breaker carrier + +The final shape has three structural pieces — the partitioned `EffectShape`, the narrowed `BreakingOperation`, and the sum-shaped `CompositionVerdict` — and no outer record around them: + +```dag +// Partition: idempotent-subset. +type IdempotentShape + = ReadEffect + | UpsertEffect { key_source: KeySource } + | DeleteEffect { key_source: KeySource } + +// Partition: breaking-subset (non-idempotent by construction). +type BreakingShape + = CreateEffect { cause: CreateCause } + | AppendEffect + +// EffectShape is the disjoint union of the two subsets. +type EffectShape + = IsIdempotent(IdempotentShape) + | IsBreaking(BreakingShape) + +type OperationEffect { + operation_name: String + shape: EffectShape +} + +// Breaking-subset projection of OperationEffect. Cannot carry an +// idempotent shape — that combination is unrepresentable, not merely +// disallowed by a constructor convention. +type BreakingOperation { + operation_name: String + shape: BreakingShape +} + +// The effects-algebra verdict for a composed workflow. Returned +// directly by `compose_effects` — no enclosing record. +type CompositionVerdict + = IdempotentComposition + | BrokenBy { first_breaker: BreakingOperation } +``` + +`compose_effects` projects each op via `operation_to_breaker` and returns the verdict directly: + +```dag +fn operation_to_breaker(op: OperationEffect) -> BreakingOperation? { + match op.shape { + IsIdempotent => None + IsBreaking(breaking) => + Some(BreakingOperation { + operation_name: op.operation_name, + shape: breaking + }) + } +} + +fn compose_effects(effects: List) -> CompositionVerdict { + let breaker_candidates = effects |> flat_map(op => + match operation_to_breaker(op: op) { + Some(b) => [b] + None => [] + } + ) + match breaker_candidates |> first { + Some(b) => BrokenBy { first_breaker: b } + None => IdempotentComposition + } +} +``` + +Properties (R3): + +- **State-space sound at the verdict.** `CompositionVerdict` is a sum whose each variant is internally coherent. `IdempotentComposition` carries no payload; `BrokenBy` carries exactly one `BreakingOperation`, and `BreakingOperation.shape: BreakingShape` cannot admit idempotent variants. Nothing beside the verdict can be made to disagree with it because nothing *is* beside it. +- **State-space sound at the shape boundary.** `EffectShape = IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)` makes the idempotent/breaking partition structural. Consumers that need the classification (`is_idempotent_effect`, `operation_is_breaking`) read the outer variant directly rather than enumerating variants and deciding each case. Adding a new `EffectShape` member requires choosing which side of the partition it inhabits — the compiler enforces this via exhaustive match on the two-arm outer sum. +- **Evidence at its natural site.** `List` is the caller's own input to `compose_effects`. Callers that want both the walk and the verdict keep the input in scope and read the return value — two facts, two sites, zero correlation to enforce. Stage 2c's obligation generator already consumes `List` directly (not `ComposedEffect`), so nothing regresses. +- **Single-authority by type shape, not by convention.** There is no carrier for a caller to incoherently construct. `BrokenBy { first_breaker: some_BreakingOperation }` is locally coherent: the variant carries what the variant carries. `.dag` lets anyone construct it, but the constructed value's state-space is the variant itself — there is no sibling field to correlate with. +- **Cleaner consumers.** `classify_idempotent_disagreement` takes `shape: BreakingShape` directly — the previous "dead arms" for idempotent shapes (unreachable but required by exhaustive match on the old flat `EffectShape`) dissolve. `check_modifier_vs_derivation` matches the op's outer partition variant instead of calling `is_idempotent_effect` and then re-destructuring. + +### Known trade-off — `BreakingOperation` is a copy, not a carrier-relative witness + +`BrokenBy.first_breaker: BreakingOperation` is a structural copy of an element of `compose_effects`'s input `List`, not a carrier-relative witness pointing at that element. If a caller holds both the input list and the verdict, the type system does not enforce `first_breaker ∈ effects`: anyone can construct a standalone `BreakingOperation { operation_name: "fabricated", shape: AppendEffect }` and wrap it in `BrokenBy`. The discipline "go through `compose_effects`" is convention, not shape, at the `BreakingOperation` level. + +**Why not a witness here.** The project's `feedback_state_space_vs_behavioral_invariants` discipline would ordinarily push for a handle — the right shape for "this field must refer to an element of that carrier" is an `ElementRef` handle whose constructor takes the list and a slot, analogous to `ParamRef` / `TransformRef` in Track 9 (`ROADMAP.md:763-772`). `ElementRef` is **deliberately not yet declared** per the same Track 9 entry: "the handle lands when a concrete consumer needs it, not speculatively." No consumer of `CompositionVerdict` exists yet (Stage 2b's lens is not written, Track 17a REST wiring is not written), so there is no concrete shape to anchor an `ElementRef` graduation against. Landing one now would be speculative. + +**What this means for the boundary.** The Stage 2a / Track 17a boundary is cleared at the wrapper / record level — the R1 `Bool + String?` correlation, the R1 breaker-carrier inner-variant hole, and the R2 outer-record-pairs-two-fields hole are all dissolved. The deeper single-authority concern — whether `first_breaker` should be a handle rather than a copy — is a separate design axis that belongs with the first real consumer (most likely the Stage 2b lens). When Stage 2b lands, if the report needs to render "position of the breaker in the workflow" or tie the verdict back to its evidence chain structurally, that is the moment to promote `BreakingOperation` to `ElementRef` (and ship the `ElementRef` graduation alongside). This brief explicitly does not pre-declare the handle. + +**Tracked follow-up.** `ROADMAP.md` §"Lane 2 Stage 2a / Track 17a boundary" names this trade-off and points at Track 9's deferred `ElementRef` graduation as the place where a witness-based breaker would land if and when a Stage 2b / Track 17a consumer justifies it. The boundary is cleared for the specific shape contract Stage 2a owns; the "is the breaker a handle or a copy" design axis is an independent, consumer-driven decision deferred to the Stage 2b / Track 17a implementation PRs. + +### Revision trail + +- **R1 (landed at `b42edc15`).** `type CompositionVerdict = IdempotentComposition | BrokenBy { first_breaker: OperationEffect }` wrapped in `type ComposedEffect { operations, verdict }`. codex review flagged: `BrokenBy.first_breaker: OperationEffect` admits idempotent shapes. +- **R2.** Partitioned `EffectShape` into `IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)`; narrowed `BrokenBy.first_breaker: BreakingOperation { shape: BreakingShape }`. ChatGPT review flagged: the `{ operations, verdict }` record still admits incoherent pairs — `operations: [breaker]` + `verdict: IdempotentComposition`, or `BrokenBy { first_breaker }` where the breaker isn't the first breaker in `operations` or isn't in `operations` at all. Records are directly constructible in `.dag`; the constructor's coherence is behavioral, not structural. +- **R3 (this land).** Dropped `ComposedEffect`. `compose_effects` returns `CompositionVerdict` directly. The record-level correlation problem dissolves because there is no record. + +Each revision goes one layer deeper into the same critique: *make illegal states unrepresentable at every structural level*, not just the outer one or the inner one. R3 hits all levels at once. + +### Alternatives considered (revisited at R3) + +**Option A — drop `idempotent`, keep `breaking_operation`.** Let the presence of `Some(name)` encode non-idempotency; `None` encodes idempotency. Cheapest reshape. Rejected because it keeps the `String?` back-reference (name-keyed lookup into `operations`) and because the meaning of "idempotent" hides inside `Option`'s shape — readers have to know the convention. The sum makes the convention structural. + +**Option C — drop `ComposedEffect` entirely.** Return `CompositionVerdict` alone. **This is R3.** The R1/R2 briefs rejected this on the grounds that "Stage 2c needs the walk," but that reasoning was wrong: Stage 2c's `generate_idempotency_obligations` consumes `List` directly, not `ComposedEffect`. No consumer actually needed the pairing to be materialized at the verdict boundary. The record was a convenience that admitted incoherence; removing it removes the correlation risk. + +**Option D — store the verdict only; derive the walk on demand.** Consumers that want the chain re-walk the input. Essentially R3 for the single-consumer case: the input is the caller's own list, so "derive on demand" is just "keep using the variable you already have." + +**Option E — pure sum with `operations` inside each variant.** + +```dag +type ComposedEffect + = IdempotentComposition { operations: List } + | BrokenBy { operations: List, first_breaker: OperationEffect } +``` + +Rejected: duplicates the evidence across variants; still admits a version of the R2 critique — `BrokenBy.operations` could disagree with `first_breaker`. R3 (no wrapper) dominates this option. + +**Option F — structural tie between `first_breaker` and `operations`.** Encode `first_breaker` as an index into `operations` plus a refinement that the index is in-bounds and points at a `BreakingShape`, or split the record into `preceding: List`, `breaker: BreakingOperation`, `following: List`. Rejected: substantially more machinery; no consumer today needs the structural tie; R3 gets the same soundness with less surface by not pairing the two in a carrier at all. + +### What stays + +- `type OperationEffect { operation_name: String; shape: EffectShape }` — signature unchanged (`shape` still reads `EffectShape`; just the internal structure of `EffectShape` partitioned). +- `fn generate_idempotency_obligations(ops: List) -> List` — unchanged signature (still consumes `List`). +- `derive_op_effect`, `derive_effect_shape` — signatures unchanged; constructor call sites adjusted to the partitioned `EffectShape`. +- `type IdempotencyEvidence`, `type ModifierAgreement`, `type ModifierAxisCheck`, `type ModifierCheck` — unchanged. + +### What changes (R3-final) + +- `type EffectShape` (v3) — flat five-variant sum → `IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)`. +- New `type IdempotentShape`, `type BreakingShape`, `type BreakingOperation` (v3). +- New `type CompositionVerdict = IdempotentComposition | BrokenBy { first_breaker: BreakingOperation }` (v3). +- **`type ComposedEffect` is removed.** The old `{ operations, idempotent, breaking_operation }` is gone; the intermediate `{ operations, verdict }` is also gone. +- `fn compose_effects(effects: List) -> CompositionVerdict` — returns the verdict directly; no enclosing record. +- `fn is_idempotent_effect` — collapses to a two-arm match on the outer partition variant. +- `fn derive_idempotency_evidence` — becomes a nested match (outer partition, then inner variant). +- `fn operation_is_breaking` — reads the partition directly off `op.shape` (no evidence round-trip). +- New `fn operation_to_breaker(op: OperationEffect) -> BreakingOperation?` (v3). +- `fn classify_idempotent_disagreement` — argument type narrows from `EffectShape` to `BreakingShape` (dead-arm cleanup). +- `fn classify_readonly_agreement` — nested match; the `IsBreaking` arm collapses to one case. +- `fn check_modifier_vs_derivation` — matches `op.shape`'s outer partition variant directly for the idempotent check; readonly still delegates to `classify_readonly_agreement`. + +### v2 scope — do not mirror + +The Stage 2a `DerivedOpEffect` collapse (PR #521) only touched v3. v2's `dsl/std/effects.dag` still ships `DerivedOpEffect` and the old `ComposedEffect` shape, and `src/v2/stage0/src/std_effects.rs` generates from the v2 authority, so the two sides are already in structural drift inside Stage 2a. That precedent is the right one: v2 is bootstrap-only, not end-user-facing, and mirroring every v3 reshape back into v2 doubles the reshape work for zero downstream benefit. This brief recommends the same discipline — **v3-only reshape**. v2 `ComposedEffect` stays on the `Bool + String?` shape until v2 retires. If something on the v2 critical path ever reads `.idempotent` or `.breaking_operation` (nothing does today), the implementer can revisit; otherwise the v2 divergence is paid-off debt, not live risk. + +One related asymmetry, flagged for later: v2's `OperationEffect` carries an `evidence: IdempotencyEvidence` field that v3 projects on demand via `derive_idempotency_evidence`. That is a separate cleanup (evidence-vs-shape duplication) and is **not** in scope for this brief. + +--- + +## Consumer impact + +| Site | Reads `ComposedEffect` fields? | Impact | +|---------------------------------------------------------------|--------------------------------|--------| +| `src/v3/std/effects.dag` (authoring) | n/a — it IS the authoring site | reshape | +| `src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs` | No — parse-only smoke | name-check list updated to R3 types; `ComposedEffect` removed | +| `src/v2/stage0/src/std_effects.rs` | No — generated from v2 `dsl/std/effects.dag` | **unchanged** (v2 authority not touched by this reshape) | +| `src/v2/stage0/src/v2_compiler_effect_derivation.rs` | No — re-export only from v2 bootstrap | **unchanged** | +| `src/v2/effect_derivation.dag` | No — imports v2 `ComposedEffect` name only | **unchanged** | +| Stage 2b lens (`src/v3/lenses/idempotency.dag`, not yet written) | Will read verdict | consume `CompositionVerdict` directly from `compose_effects`; pair with caller-held `List` if the lens report needs the walk | + +No v3 consumer currently depends on any `ComposedEffect` field — the type was new in R1/R2 and is being removed before its first consumer lands. The reshape is a pre-consumer window. + +--- + +## Acceptance + +Implementation PR must satisfy (R3-final): + +1. `src/v3/std/effects.dag` defines: + - `type IdempotentShape = ReadEffect | UpsertEffect { key_source: KeySource } | DeleteEffect { key_source: KeySource }` + - `type BreakingShape = CreateEffect { cause: CreateCause } | AppendEffect` + - `type EffectShape = IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)` + - `type BreakingOperation { operation_name: String; shape: BreakingShape }` + - `type CompositionVerdict = IdempotentComposition | BrokenBy { first_breaker: BreakingOperation }` + - No `type ComposedEffect`. The outer record is gone; `compose_effects` returns `CompositionVerdict` directly. +2. `compose_effects(effects: List) -> CompositionVerdict` returns `IdempotentComposition` iff `effects |> flat_map(operation_to_breaker) |> is_empty`, and `BrokenBy { first_breaker }` otherwise with `first_breaker` structurally equal to the first projected `BreakingOperation`. +3. v2 is explicitly **not** touched (see §v2 scope). `dsl/std/effects.dag` and `src/v2/stage0/src/std_effects.rs` stay on the old shape. +4. `lane2_stage_2a_effects_smoke.rs` asserts the following top-level types are present in the parsed DAG: `EffectShape`, `IdempotentShape`, `BreakingShape`, `CreateCause`, `KeySource`, `IdempotencyEvidence`, `CompositionVerdict`, `OperationEffect`, `BreakingOperation`, `ModifierAgreement`, `ModifierAxisCheck`, `ModifierCheck`. (Variants of sum types are not asserted separately — the v3 bootstrap does not expose variants as standalone declarations.) +5. `src/v3/ROADMAP.md` §"Lane 2 Stage 2a / Track 17a boundary" reads **Cleared (this PR)** with a description that names the partition *and* the removal of the outer record; `lane2-compile-time-proofs.md` §Stage 2a boundary note updates to the R3 shape; the Stage 2b pre-start gate language names `CompositionVerdict` (not `ComposedEffect`) as the algebra's output and tells the lens implementer to pair it with the caller-held `List` rather than recreate the pairing at the lens boundary. +6. Stage 2b's `WorkflowIdempotencyReport` design (in `lane2-compile-time-proofs.md` §Stage 2b) is not touched by this PR — but the lens implementer, when Stage 2b lands, must match on `CompositionVerdict` and project through `BrokenBy.first_breaker.shape: BreakingShape` rather than reintroduce a parallel `Bool + String?` pair; the draft `breaking_op: String?` field in the §Stage 2b report is a placeholder from before this reshape landed and should be replaced with a structural carrier derived from `CompositionVerdict`. + +Non-goals: + +- `OperationEffect.evidence` v2/v3 divergence (separate cleanup). +- Any Stage 2b lens logic. +- Diagnostic rendering of the breaker (Stage 2b scope). + +--- + +## Open question (resolved at land) + +Did this warrant a numbered DB? No, even after R3. The final reshape introduces four new carriers (`IdempotentShape`, `BreakingShape`, `BreakingOperation`, `CompositionVerdict`) but they are all tight refinements of shapes already in the same file; no cross-lane footprint, no new substrate concept. The brief is the design doc. + +**Lessons from the R1 → R2 → R3 arc.** Each revision went one layer deeper into the same critique: +- **R1 → R2 (codex review):** the outer summary was a sum, but the sum's *payload* still admitted incoherent inner shapes. State-space soundness has to reach the nested carriers, not stop at the outer variant. +- **R2 → R3 (ChatGPT review):** the payload was sound, but the *record wrapper* paired it with a sibling field (the walk) that the type system couldn't correlate. State-space soundness across sibling fields of a record is convention unless the record's own construction is restricted — and `.dag` records don't restrict construction. + +The brief-review discipline that falls out: when adding a new carrier, audit *every field* and *every sibling-field pair* against `feedback_state_space_vs_behavioral_invariants`. "This sum is clean" is not enough; the sum's payload, and anything paired with the sum in a record, needs the same scrutiny. If the pairing requires a constructor discipline to stay coherent, the pairing is API-level and should be removed or replaced with a structural tie (index-plus-refinement, split variants, or just "return one, let the caller keep the other in scope"). + +--- + +## Pointers + +- Authoring site: `src/v3/std/effects.dag` — `type EffectShape`, `type IdempotentShape`, `type BreakingShape`, `type OperationEffect`, `type BreakingOperation`, `type CompositionVerdict`, `fn compose_effects`, `fn operation_to_breaker`, `fn operation_is_breaking`. +- v2 parallel authority (explicitly not mirrored by this reshape): `dsl/std/effects.dag` (`ComposedEffect` still on the `Bool + String?` shape; `EffectShape` still flat). +- Roadmap: `src/v3/ROADMAP.md` §"Lane 2 Stage 2a / Track 17a boundary". +- Stage 2a boundary note: `docs/lane2-compile-time-proofs.md` §Stage 2a. +- Pattern authority: `feedback_state_space_vs_behavioral_invariants` — "dissolve the bools into a single enum whose variants are only the valid combinations." Extended by the R1→R3 arc: soundness must reach *every* structural level — the outer variant, every field of every carrier, and every sibling-field pair within any record. diff --git a/docs/lane2-compile-time-proofs.md b/docs/lane2-compile-time-proofs.md index 6252133a19f..dc3c6122919 100644 --- a/docs/lane2-compile-time-proofs.md +++ b/docs/lane2-compile-time-proofs.md @@ -38,17 +38,32 @@ This lane closes the "❌ not wired" gaps across six stages. After Lane 2 comple **Scope:** port `dsl/std/effects.dag` → `src/v3/std/effects.dag`. Structural carry-over only. -**Boundary note (cleared for `DerivedOpEffect`):** `DerivedOpEffect { method, path_template, shape }` was collapsed into `OperationEffect { operation_name, shape }` as the Stage 2a follow-up. The `method` / `path_template` fields were carried as bootstrap-local staging glue but never consumed downstream — both modifier falsification and obligation generation project through `shape` alone, and `ReadEffect` already encodes "method was GET/HEAD/OPTIONS" structurally. `derive_op_effect` now returns `OperationEffect?`, so derivation outputs the same shape `compose_effects` composes. +**Boundary note (cleared):** Stage 2a plus all three follow-up refinements have landed. The final shape responds to two review rounds that each pushed state-space soundness one layer deeper. -`ComposedEffect { operations, idempotent, breaking_operation }` is still provisional. The workflow verdict must not harden around duplicated summary fields; before real Track 17a / Stage 2b consumers depend on it, the follow-up should either drop `idempotent` as redundant or replace the record with a sum-shaped result where "no breaker" versus "broken by operation X" is structural. +`DerivedOpEffect { method, path_template, shape }` was collapsed into `OperationEffect { operation_name, shape }` in PR #521. The `method` / `path_template` fields were carried as bootstrap-local staging glue but never consumed downstream — both modifier falsification and obligation generation project through `shape` alone, and `ReadEffect` already encodes "method was GET/HEAD/OPTIONS" structurally. `derive_op_effect` now returns `OperationEffect?`, so derivation outputs the same shape `compose_effects` composes. -Lane 2 does not get to silently normalize around this remaining convenience shape. +`ComposedEffect { operations, idempotent, breaking_operation }` was removed entirely; `EffectShape` partitioned; `compose_effects` now returns `CompositionVerdict` directly. The final R3 shape: -Copy: -- `EffectShape = ReadEffect | UpsertEffect | DeleteEffect | CreateEffect | AppendEffect` +- `type IdempotentShape = ReadEffect | UpsertEffect { key_source } | DeleteEffect { key_source }` +- `type BreakingShape = CreateEffect { cause } | AppendEffect` +- `type EffectShape = IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)` +- `type BreakingOperation { operation_name, shape: BreakingShape }` +- `type CompositionVerdict = IdempotentComposition | BrokenBy { first_breaker: BreakingOperation }` +- `fn compose_effects(effects: List) -> CompositionVerdict` +- No `ComposedEffect`. The evidence chain stays on the caller's side as the input `List`; the verdict is the output. + +Design: [design-composed-effect-reshape.md](./design-composed-effect-reshape.md) (R3-final). v3-only per the same scope discipline PR #521 used. The partition means `is_idempotent_effect` reads the outer variant directly; `operation_is_breaking` does too; `classify_idempotent_disagreement` narrows its argument to `BreakingShape` (dead-arm cleanup). Dropping the record means there is no correlated-fields invariant for the type to fail to enforce. + +Copy (post-reshape, R3): +- `IdempotentShape = ReadEffect | UpsertEffect | DeleteEffect` +- `BreakingShape = CreateEffect | AppendEffect` +- `EffectShape = IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)` - `KeySource` (for upsert/delete key derivation) - `IdempotencyEvidence = LatticeEffect | IdentityEffect | NonIdempotent` -- `is_idempotent_effect`, `compose_effects`, `ComposedEffect`, `OperationEffect` +- `OperationEffect { operation_name, shape: EffectShape }` +- `BreakingOperation { operation_name, shape: BreakingShape }` +- `CompositionVerdict = IdempotentComposition | BrokenBy { first_breaker: BreakingOperation }` +- `is_idempotent_effect`, `operation_is_breaking`, `operation_to_breaker`, `compose_effects` - `derive_effect_shape(method, path)` — HTTP method + path → EffectShape - `generate_idempotency_obligations` - `check_modifier_vs_derivation` @@ -87,7 +102,9 @@ Lens reads each operation's declared `idempotent` modifier AND derives from path **Escalation:** if workflow structure isn't representable cleanly — e.g., control flow in a pipeline doesn't map to a linear `List` — surface. Don't stretch `compose_effects` to handle branches silently; the algebra needs to reflect branch-wise composition, which is a legitimate design extension. -**Pre-start gate:** Stage 2b does not start consuming `ComposedEffect` as if it were stable substrate. The Stage 2a `DerivedOpEffect` collapse has landed (derivation now emits `OperationEffect`, which is the same shape `compose_effects` walks). The remaining Stage 2a follow-up is `ComposedEffect`: it must stop encoding workflow verdicts as duplicated summary fields before Stage 2b consumers depend on it. +**Pre-start gate:** cleared. All Stage 2a follow-ups have landed — `DerivedOpEffect` collapsed into `OperationEffect` (PR #521); `EffectShape` partitioned into `IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)`; `BrokenBy`'s payload narrowed to `BreakingOperation { shape: BreakingShape }`; `ComposedEffect` removed. `compose_effects(effects: List) -> CompositionVerdict` is the algebra's output. Stage 2b consumes `CompositionVerdict` directly; callers pair it with their own input `List` for diagnostic rendering. The Stage 2b `WorkflowIdempotencyReport` shape above is one layer higher (a lens report with diagnostic), not a duplication of the algebra verdict — when Stage 2b implements it, the report must match on `CompositionVerdict` and project through `BrokenBy.first_breaker.shape: BreakingShape`. The `breaking_op: String?` field in the draft `WorkflowIdempotencyReport` shape above is a design placeholder from before the Stage 2a partition landed; Stage 2b's implementer should replace it with a structural carrier derived from `CompositionVerdict` rather than copy the flat shape. The implementer must not reintroduce a `ComposedEffect`-style record that pairs `CompositionVerdict` with a sibling list field, since that reintroduces the correlated-fields incoherence R3 just removed. + +**Stage 2b / Track 17a design axis — witness vs copy.** `BreakingOperation` today is a *copy* of the originating `OperationEffect`, not a carrier-relative witness into `compose_effects`'s input list. This is a deliberate Track 9 deferral: `ElementRef`-style handles "land when a concrete consumer needs it, not speculatively" (`ROADMAP.md:763-772`). When the Stage 2b lens or a Track 17a consumer first needs to render the breaker's position in the workflow or structurally tie the verdict back to its evidence chain, the handle graduation belongs in that PR — not retrofitted into Stage 2a. Until that graduation, consumers that need position-in-workflow can search the caller's input list by name; the verdict itself is sound (sum variants coherent, `BreakingShape` narrowing intact). ### Stage 2c — Test obligation materialization (M) diff --git a/src/v3/ROADMAP.md b/src/v3/ROADMAP.md index 96956120b93..4800859ecb3 100644 --- a/src/v3/ROADMAP.md +++ b/src/v3/ROADMAP.md @@ -511,11 +511,22 @@ Implementation scope (M, once design locks): extend `TestClaim` with `requires: ### Lane 2 Stage 2a / Track 17a boundary -**Deferral: `ComposedEffect` boundary cleanup (S).** PR #517 carried `ComposedEffect { operations, idempotent, breaking_operation }` forward as a temporary workflow summary shape. Acceptable only as a short-lived bridge. Before Track 17a REST wiring or Stage 2b workflow-idempotency consumers start depending on it, a follow-up PR must reshape `ComposedEffect` so workflow verdicts are structural rather than duplicated summary fields — at minimum drop redundant `idempotent`, or better encode "no breaker" versus "broken by operation X" in the type shape itself. +Cleared (this PR, R3-final): the `ComposedEffect` record is gone; `EffectShape` is partitioned by idempotency class; `compose_effects` returns `CompositionVerdict` directly. The final shapes are: +- `type IdempotentShape = ReadEffect | UpsertEffect { key_source } | DeleteEffect { key_source }` +- `type BreakingShape = CreateEffect { cause } | AppendEffect` +- `type EffectShape = IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)` +- `type BreakingOperation { operation_name, shape: BreakingShape }` +- `type CompositionVerdict = IdempotentComposition | BrokenBy { first_breaker: BreakingOperation }` +- (No `ComposedEffect`.) +- `fn compose_effects(effects: List) -> CompositionVerdict` -The thing we must not do is let Track 17a treat this convenience record as canonical by inertia. **Yellow-flag threshold:** this deferral must clear before any Track 17a consumer lands. Design anchor: [lane2-compile-time-proofs.md](../../docs/lane2-compile-time-proofs.md) Stage 2a / Stage 2b boundary note. No standalone DB yet; if cleanup needs a new durable carrier shape, write the DB in the follow-up PR instead of growing the scaffold ad hoc. +Three illegal-state boundaries dissolved, in order: the old `Bool + String?` admitted `(true, Some(_))` and `(false, None)`; R1's `BrokenBy { first_breaker: OperationEffect }` admitted `OperationEffect { shape: ReadEffect }` in the breaker slot (codex flag); R2's `ComposedEffect { operations, verdict }` admitted `verdict: IdempotentComposition` alongside `operations: [breaker]`, and `BrokenBy { first_breaker }` whose breaker is not in `operations` (ChatGPT flag — records are directly constructible in `.dag`, so the constructor's coherence is behavioral). R3 drops the outer record; `CompositionVerdict` is sound all the way down and `List` stays at the caller site. Downstream: `is_idempotent_effect` reduces to a two-arm outer match; `classify_idempotent_disagreement` takes `BreakingShape` directly (dead-arm cleanup); Stage 2c's obligation generator already consumed `List` directly, so no consumer regresses. Design: [design-composed-effect-reshape.md](../../docs/design-composed-effect-reshape.md). v3-only — v2's `dsl/std/effects.dag` stays on the flat `EffectShape` + `Bool + String?` shape per the same scope discipline PR #521 used. The Stage 2b pre-start gate no longer names `ComposedEffect` as an open shape. -Cleared (this PR): `DerivedOpEffect { method, path_template, shape }` collapsed into `OperationEffect { operation_name, shape }`. The `method` / `path_template` fields were never consumed downstream — both the modifier check and obligation generator project through `shape` alone, and the `ReadEffect` variant already encodes "method was GET/HEAD/OPTIONS." `derive_op_effect` now returns `OperationEffect?` directly, so Stage 2b's `compose_effects` consumes the same shape derivation produces. Future diagnostic rendering that wants the originating method/path should attach a separate evidence carrier to the diagnostic, not smuggle transport facts onto the effect record. +**Review arc.** R1 at `b42edc15` landed the `Bool + String?` → `CompositionVerdict` lift with `BrokenBy { first_breaker: OperationEffect }` wrapped in `ComposedEffect { operations, verdict }`. Codex review flagged the inner-variant hole (breaker payload admitted idempotent shapes); R2 partitioned `EffectShape` and narrowed `BrokenBy` to `BreakingOperation`. ChatGPT review then flagged the outer-record hole (operations/verdict correlation was behavioral, not structural) and recommended returning `CompositionVerdict` directly; R3 is that fix. Each round pushed state-space soundness one layer deeper: outer sum → inner payload → record wrapper. + +**Known trade-off, not a blocker for Stage 2a.** `BreakingOperation` is a structural copy of its originating `OperationEffect`, not a carrier-relative witness into the input list. A caller can construct a standalone `BreakingOperation` and wrap it in `BrokenBy` without any type-level tie to any `List`; the discipline "go through `compose_effects`" is convention, not shape. The right shape for this is an `ElementRef`-style handle, analogous to `ParamRef` / `TransformRef` in Track 9 (see `ROADMAP.md:763-772`). Per Track 9's stated policy — "the handle lands when a concrete consumer needs it, not speculatively" — `ElementRef` is deliberately not yet declared, and no current consumer of `CompositionVerdict` exists to pin the graduation against. **Tracked as a consumer-driven follow-up for Stage 2b / Track 17a:** when the Stage 2b lens or the first Track 17a consumer needs to render "position of breaker in workflow" or structurally tie the verdict to its evidence chain, that is the moment to graduate `BreakingOperation` into `ElementRef` and ship the `ElementRef` declaration alongside. Until then, the verdict's state-space is sound within itself (sum variants are internally coherent, `BreakingShape` can't admit idempotent shapes); only the verdict-to-evidence-chain tie remains copy-based. + +Cleared (prior PR #521): `DerivedOpEffect { method, path_template, shape }` collapsed into `OperationEffect { operation_name, shape }`. The `method` / `path_template` fields were never consumed downstream — both the modifier check and obligation generator project through `shape` alone, and the `ReadEffect` variant already encodes "method was GET/HEAD/OPTIONS." `derive_op_effect` now returns `OperationEffect?` directly, so Stage 2b's `compose_effects` consumes the same shape derivation produces. Future diagnostic rendering that wants the originating method/path should attach a separate evidence carrier to the diagnostic, not smuggle transport facts onto the effect record. ### Lane 1 Stage 1b diff --git a/src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs b/src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs index 8cb95b253c4..bc851996f29 100644 --- a/src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs +++ b/src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs @@ -88,11 +88,14 @@ fn effects_dag_exposes_core_effect_algebra_types() { // parse-only carry-over where the types fail to lower. for name in [ "EffectShape", + "IdempotentShape", + "BreakingShape", "CreateCause", "KeySource", "IdempotencyEvidence", - "ComposedEffect", + "CompositionVerdict", "OperationEffect", + "BreakingOperation", "ModifierAgreement", "ModifierAxisCheck", "ModifierCheck", diff --git a/src/v3/std/effects.dag b/src/v3/std/effects.dag index 1bb7a30af0e..f729840e7c7 100644 --- a/src/v3/std/effects.dag +++ b/src/v3/std/effects.dag @@ -19,26 +19,63 @@ // `dsl/std/effects.dag`; keep the two in sync during the bootstrap // window. See `THESIS.md` §"Two groundings" bootstrap note. // -// **Scope (Lane 2 Stage 2a).** Structural carry-over only: -// - `EffectShape`, `CreateCause`, `KeySource`, `IdempotencyEvidence` -// - `ComposedEffect`, `OperationEffect` -// - `is_idempotent_effect`, `compose_effects` +// **Scope (Lane 2 Stage 2a + follow-ups).** Structural carry-over of +// the v2 authority, with v3-only refinements already landed: +// - `EffectShape = IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)` (partition) +// - `IdempotentShape`, `BreakingShape` +// - `CreateCause`, `KeySource`, `IdempotencyEvidence` +// - `OperationEffect`, `BreakingOperation` +// - `CompositionVerdict = IdempotentComposition | BrokenBy { first_breaker: BreakingOperation }` +// - `is_idempotent_effect`, `operation_is_breaking`, `operation_to_breaker` +// - `compose_effects(effects: List) -> CompositionVerdict` // - `derive_effect_shape(method, path)` — HTTP method + path → EffectShape // - `generate_idempotency_obligations`, `check_modifier_vs_derivation` // v2-specific imports, parser quirks, and Rust bridge code do NOT // come over. Pure `.dag` declarations. // -// Stage 2a follow-up (cleared): `DerivedOpEffect` was collapsed into -// `OperationEffect`. The previous shape carried `method` and -// `path_template` fields alongside `operation_name` + `shape`, but -// nothing downstream ever read the transport fields — the modifier -// check and obligation generator both project through `shape` alone, -// and the `ReadEffect` variant already encodes "method was GET/HEAD/ -// OPTIONS." `OperationEffect` is the durable carrier Stage 2b's -// `compose_effects` walks; `derive_op_effect` now returns it -// directly. Future diagnostic rendering that wants the originating -// method/path should attach a separate evidence carrier to the -// diagnostic, not smuggle transport facts onto the effect record. +// Stage 2a follow-ups (cleared): +// +// 1. `DerivedOpEffect` was collapsed into `OperationEffect` (PR #521). +// The previous shape carried `method` and `path_template` fields +// alongside `operation_name` + `shape`, but nothing downstream ever +// read the transport fields — the modifier check and obligation +// generator both project through `shape` alone, and the +// `ReadEffect` variant already encodes "method was GET/HEAD/OPTIONS." +// `OperationEffect` is the durable carrier Stage 2b's `compose_effects` +// walks; `derive_op_effect` now returns it directly. Future diagnostic +// rendering that wants the originating method/path should attach a +// separate evidence carrier to the diagnostic, not smuggle transport +// facts onto the effect record. +// +// 2. `ComposedEffect { operations, idempotent: Bool, breaking_operation: String? }` +// was removed entirely. `compose_effects` now returns +// `CompositionVerdict = IdempotentComposition | BrokenBy { first_breaker: BreakingOperation }` +// directly. The earlier intermediate form wrapped the verdict in a +// `{ operations, verdict }` record so callers could get the walk and +// the judgment from one value, but reviewer feedback on the +// intermediate R2 shape pointed out that pairing them admits +// incoherence: `verdict: IdempotentComposition` with a breaking op +// in `operations`, or `BrokenBy { first_breaker }` where the breaker +// is not actually in `operations`. `.dag` records are directly +// constructible, so "the constructor keeps them coherent" is a +// behavioral invariant, not a type-level one. Dropping the record +// leaves `operations` as the caller's own input and the verdict as +// the pure projected output — two facts kept separate at their +// natural sites, with no correlation for the type system to enforce. +// +// 3. `EffectShape` was partitioned into +// `IsIdempotent(IdempotentShape) | IsBreaking(BreakingShape)`, +// and `BrokenBy`'s payload narrowed to `BreakingOperation { shape: BreakingShape }`. +// The earlier flat `BrokenBy { first_breaker: OperationEffect }` shape +// still admitted `OperationEffect { shape: ReadEffect }` — an +// idempotent op in the breaker slot — enforced only by the +// `compose_effects` filter. Partitioning EffectShape at the type +// level, and narrowing the carrier to `BreakingShape`, makes naming +// an idempotent op as the workflow breaker unrepresentable rather +// than disallowed-by-convention. Consumers still match on the five +// concrete variants (ReadEffect / UpsertEffect / DeleteEffect / +// CreateEffect / AppendEffect) through the outer-variant destructure; +// the per-variant algebra is unchanged. // // DESIGN PRINCIPLE: // Idempotency is not a flag. It is a DERIVED PROPERTY of the @@ -194,13 +231,33 @@ fn last_path_param(template: PathTemplate) -> String? { // Set with insert/remove → BoundedLattice (idempotent) // List with append → FreeMonoid (NOT idempotent) -type EffectShape +// 🟢 TERMINAL. The idempotent subset of effect shapes. All variants +// here form either an identity (ReadEffect) or a lattice meet on +// their target state (UpsertEffect / DeleteEffect); repeat application +// converges. +type IdempotentShape = ReadEffect | UpsertEffect { key_source: KeySource } | DeleteEffect { key_source: KeySource } - | CreateEffect { cause: CreateCause } + +// 🟢 TERMINAL. The non-idempotent subset of effect shapes. Create +// (POST-style) and Append (free monoid) both duplicate on repeat +// application, so any workflow that includes them cannot be +// retried convergently. +type BreakingShape + = CreateEffect { cause: CreateCause } | AppendEffect +// The fundamental classification of an operation's effect, expressed +// as the disjoint union of its idempotent and breaking subsets. +// Idempotency is not a property we then derive by scanning variants — +// it is encoded in the outer variant `IsIdempotent` / `IsBreaking` +// by construction, so `first_breaker: BreakingShape` and similar +// restricted carriers are well-typed without filtering. +type EffectShape + = IsIdempotent(IdempotentShape) + | IsBreaking(BreakingShape) + // 🟢 TERMINAL at current derivation scope. `CreateEffect` has two // semantically distinct provenances that later diagnostics need to // keep separate: conservative POST-create and keyless fail-closed @@ -250,14 +307,13 @@ type IdempotencyEvidence | IdentityEffect | NonIdempotent { reason: String } -// Whether an effect is idempotent — derived from its shape. +// Whether an effect is idempotent — the partition's outer variant +// already encodes the answer, so this is a single-step match rather +// than a per-variant enumeration. fn is_idempotent_effect(shape: EffectShape) -> Bool { match shape { - ReadEffect => true - UpsertEffect => true - DeleteEffect => true - CreateEffect => false - AppendEffect => false + IsIdempotent => true + IsBreaking => false } } @@ -265,16 +321,22 @@ fn is_idempotent_effect(shape: EffectShape) -> Bool { // the single `EffectShape` authority, not a second authored fact. fn derive_idempotency_evidence(shape: EffectShape) -> IdempotencyEvidence { match shape { - ReadEffect => IdentityEffect - UpsertEffect => LatticeEffect - DeleteEffect => LatticeEffect - CreateEffect => - NonIdempotent { - reason: "create-shaped effect duplicates on repeat application" + IsIdempotent(inner) => + match inner { + ReadEffect => IdentityEffect + UpsertEffect => LatticeEffect + DeleteEffect => LatticeEffect } - AppendEffect => - NonIdempotent { - reason: "append-shaped effect duplicates on repeat application" + IsBreaking(inner) => + match inner { + CreateEffect => + NonIdempotent { + reason: "create-shaped effect duplicates on repeat application" + } + AppendEffect => + NonIdempotent { + reason: "append-shaped effect duplicates on repeat application" + } } } } @@ -291,42 +353,81 @@ fn derive_idempotency_evidence(shape: EffectShape) -> IdempotencyEvidence { // meet_a ∘ append_b applied twice ≠ applied once // (the append duplicates on the second application) -type ComposedEffect { - operations: List - idempotent: Bool - breaking_operation: String? -} - // Per-operation effect entry in a workflow. type OperationEffect { operation_name: String shape: EffectShape } -// True if this operation's derived evidence records non-idempotency. -// The evidence is projected from `shape` on demand so `shape` -// remains the only authored authority. +// 🟢 TERMINAL. The breaking-subset projection of OperationEffect. +// `shape: BreakingShape` structurally restricts the variant space — +// no idempotent shape can inhabit this carrier — so naming an +// idempotent op as the workflow breaker is unrepresentable, not +// merely disallowed by a constructor convention. +type BreakingOperation { + operation_name: String + shape: BreakingShape +} + +// 🟢 TERMINAL. The composition of idempotent lattice meets is +// idempotent; a single non-idempotent operation poisons the chain. +// The judgment space is therefore exactly two states: the workflow +// converges, or some operation broke convergence. No third state. +// +// `first_breaker: BreakingOperation` is a state-space-sound witness: +// its `shape` field ranges only over `BreakingShape`, so the verdict +// cannot name an idempotent op as the breaker. Downstream diagnostics +// project shape / cause directly. +type CompositionVerdict + = IdempotentComposition + | BrokenBy { first_breaker: BreakingOperation } + +// True if this operation is non-idempotent. Reads the partition +// directly off `EffectShape` — no evidence-projection round-trip. fn operation_is_breaking(op: OperationEffect) -> Bool { - match derive_idempotency_evidence(shape: op.shape) { - LatticeEffect => false - IdentityEffect => false - NonIdempotent => true + match op.shape { + IsIdempotent => false + IsBreaking => true } } -// Compose a list of operation effects into a workflow-level verdict. -fn compose_effects(effects: List) -> ComposedEffect { - let breakers = effects |> filter(op => operation_is_breaking(op: op)) - let breaker_first = breakers |> first - let breaker_name = match breaker_first { - Some(op) => Some(op.operation_name) - None => None +// Project an OperationEffect to the breaking-subset witness when its +// shape falls in `BreakingShape`; `None` when the op is idempotent. +// The outer-variant match is exhaustive, so adding a new EffectShape +// partition member forces this projection to update. +fn operation_to_breaker(op: OperationEffect) -> BreakingOperation? { + match op.shape { + IsIdempotent => None + IsBreaking(breaking) => + Some(BreakingOperation { + operation_name: op.operation_name, + shape: breaking + }) } - let count_breakers = breakers |> count - ComposedEffect { - operations: effects, - idempotent: count_breakers == 0, - breaking_operation: breaker_name +} + +// Compose a list of operation effects into a workflow-level verdict. +// Returns `CompositionVerdict` directly — no enclosing record around +// the verdict plus the input list. Callers that want the evidence +// chain keep the input `List` in scope; pairing the +// verdict with the walk inside a record would create a second +// authority (the list) alongside the projected one (the verdict), +// and `.dag` records are directly constructible, so the two could +// be made to disagree without any type-level obstruction. +// +// Flat-maps each op through `operation_to_breaker`, then takes the +// first breaker (if any). `BrokenBy` is only constructible from a +// `BreakingOperation`, so the verdict is state-space sound. +fn compose_effects(effects: List) -> CompositionVerdict { + let breaker_candidates = effects |> flat_map(op => + match operation_to_breaker(op: op) { + Some(b) => [b] + None => [] + } + ) + match breaker_candidates |> first { + Some(b) => BrokenBy { first_breaker: b } + None => IdempotentComposition } } @@ -367,7 +468,7 @@ fn parse_http_method(raw: String) -> HttpMethod? { } fn keyless_create(method: HttpMethod) -> EffectShape { - CreateEffect { cause: KeylessFallback { method: method } } + IsBreaking(CreateEffect { cause: KeylessFallback { method: method } }) } // Given a last-param lookup result, build the Upsert variant when @@ -376,14 +477,14 @@ fn keyless_create(method: HttpMethod) -> EffectShape { // share one key-resolution strategy across PUT and PATCH. fn upsert_or_create(last_param: String?, method: HttpMethod) -> EffectShape { match last_param { - Some(p) => UpsertEffect { key_source: PathParam { param: p } } + Some(p) => IsIdempotent(UpsertEffect { key_source: PathParam { param: p } }) None => keyless_create(method: method) } } fn delete_or_create(last_param: String?, method: HttpMethod) -> EffectShape { match last_param { - Some(p) => DeleteEffect { key_source: PathParam { param: p } } + Some(p) => IsIdempotent(DeleteEffect { key_source: PathParam { param: p } }) None => keyless_create(method: method) } } @@ -393,10 +494,10 @@ fn derive_effect_shape( path: PathTemplate ) -> EffectShape { match method { - GET => ReadEffect - HEAD => ReadEffect - OPTIONS => ReadEffect - POST => CreateEffect { cause: PostAlways } + GET => IsIdempotent(ReadEffect) + HEAD => IsIdempotent(ReadEffect) + OPTIONS => IsIdempotent(ReadEffect) + POST => IsBreaking(CreateEffect { cause: PostAlways }) DELETE => delete_or_create(last_param: last_path_param(template: path), method: method) PUT => upsert_or_create(last_param: last_path_param(template: path), method: method) PATCH => upsert_or_create(last_param: last_path_param(template: path), method: method) @@ -458,11 +559,15 @@ type ModifierCheck { } // Disagreement classifier when the user declared idempotent but -// the derivation says otherwise. POST-create stays the -// fail-closed-but-maybe-idempotent case (DerivationUnknown); a -// keyless fallback on PUT/PATCH/DELETE is a hard disagreement -// because the required subject-key witness is missing. -fn classify_idempotent_disagreement(shape: EffectShape) -> ModifierAgreement { +// the derivation says otherwise. Takes `BreakingShape` directly — +// the partition already guarantees the derivation says +// non-idempotent, so no idempotent-shape arms are reachable. +// POST-create stays the fail-closed-but-maybe-idempotent case +// (DerivationUnknown); a keyless fallback on PUT/PATCH/DELETE is a +// hard disagreement because the required subject-key witness is +// missing; AppendEffect is a hard disagreement because free-monoid +// append cannot be retried convergently. +fn classify_idempotent_disagreement(shape: BreakingShape) -> ModifierAgreement { match shape { CreateEffect { cause } => match cause { @@ -475,28 +580,27 @@ fn classify_idempotent_disagreement(shape: EffectShape) -> ModifierAgreement { reason: "declared idempotent but method-derived effect fell back to keyless CreateEffect" } } - ReadEffect => - Disagrees { reason: "derivation says non-idempotent but modifier declares idempotent" } - UpsertEffect => - Disagrees { reason: "derivation says non-idempotent but modifier declares idempotent" } - DeleteEffect => - Disagrees { reason: "derivation says non-idempotent but modifier declares idempotent" } AppendEffect => - Disagrees { reason: "derivation says non-idempotent but modifier declares idempotent" } + Disagrees { reason: "declared idempotent but derivation says non-idempotent via append-shaped effect" } } } -// Readonly-declaration classifier: only read-shaped effects agree. +// Readonly-declaration classifier: only `ReadEffect` agrees; every +// other idempotent shape (upsert/delete) writes the target, and every +// breaking shape does too. Nested match keeps the specific reasons per +// write-shape available, but the `IsBreaking` arm collapses because the +// verdict is identical across create/append. fn classify_readonly_agreement(shape: EffectShape) -> ModifierAgreement { match shape { - ReadEffect => Agrees - UpsertEffect => - Disagrees { reason: "readonly declared but derived effect writes target state" } - DeleteEffect => - Disagrees { reason: "readonly declared but derived effect writes target state" } - CreateEffect => - Disagrees { reason: "readonly declared but derived effect writes target state" } - AppendEffect => + IsIdempotent(inner) => + match inner { + ReadEffect => Agrees + UpsertEffect => + Disagrees { reason: "readonly declared but derived effect writes target state" } + DeleteEffect => + Disagrees { reason: "readonly declared but derived effect writes target state" } + } + IsBreaking => Disagrees { reason: "readonly declared but derived effect writes target state" } } } @@ -506,14 +610,14 @@ fn check_modifier_vs_derivation( declared_idempotent: Bool, declared_readonly: Bool ) -> ModifierCheck { - let derived_idempotent = is_idempotent_effect(shape: op.shape) let idempotent_check = if declared_idempotent then - if derived_idempotent then - ModifierDeclared { agreement: Agrees } - else - ModifierDeclared { - agreement: classify_idempotent_disagreement(shape: op.shape) - } + match op.shape { + IsIdempotent => ModifierDeclared { agreement: Agrees } + IsBreaking(breaking) => + ModifierDeclared { + agreement: classify_idempotent_disagreement(shape: breaking) + } + } else ModifierNotDeclared let readonly_check = if declared_readonly then