Repository navigation
Conversation
Structural carry-over of `dsl/std/effects.dag` to v3's staged-file tree. Ports the declarations the Lane 2 lens pipeline consumes downstream (2b idempotency lens, 2c test generation, 2d symbolic cost): - `EffectShape = ReadEffect | UpsertEffect | DeleteEffect | CreateEffect | AppendEffect` - `KeySource = PathParam | InputField | CompositeKey` - `IdempotencyEvidence = LatticeEffect | IdentityEffect | NonIdempotent` - `ComposedEffect`, `OperationEffect`, `DerivedOpEffect`, `ModifierAgreement`, `ModifierCheck`, `IdempotencyTestObligation`, `WorkflowEffectConcern` records - `is_idempotent_effect`, `compose_effects`, `parse_http_method`, `derive_effect_shape`, `derive_op_effect`, `check_modifier_vs_derivation`, `generate_idempotency_obligations` functions v2-specific imports, parser quirks, and Rust bridge code do NOT come over per the Stage 2a scope. Function bodies are v3-compatible minimal encodings of the v2 authority — the surface form is reshaped to use only v3 grammar forms (`if...then...else`, single-binding match arms, explicit variant enumeration). Signatures are authoritative; bodies reflatten toward the v2 shape when v3 grows `&&` / `||` / `_` wildcard / `if`-block form. `PathTemplate` + `UrlPathToken` inlined as minimal carriers until `std.http_path` ports to `src/v3/std/` in a future stage. Structural- identical to `dsl/std/http_path.dag` so the future port replaces inline definitions without reshaping this file. Bootstrap-staged per the established pattern (see `src/v3/std/ list.dag` note): build.rs picks up `src/v3/std/*.dag` automatically, no `bootstrap.rs` edit needed. Acceptance (per docs/lane2-compile-time-proofs.md:52): - `effects.dag` parses cleanly (`real_stdlib_parse_smoke:: effects_dag_parses`) - Bootstrap loads without diagnostics (`lane2_stage_2a_effects_ smoke::effects_dag_bootstraps_without_diagnostics`) - Five representative function signatures registered (`lane2_ stage_2a_effects_smoke::effects_dag_exposes_five_representative_ function_signatures`) - Core effect-algebra types present (`lane2_stage_2a_effects_smoke:: effects_dag_exposes_core_effect_algebra_types`) Unblocks Lane 2 Stage 2b (workflow idempotency lens). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
ChatGPT ReviewPrinciple audit. 1. Fail-closed. This looks good in the core algebra. The port keeps the conservative behavior the current effects surface already banks: POST always derives 2. Illegal states unrepresentable. For a Stage 2a structural carry-over, this is in decent shape. 3. Facts flow forward. Mostly satisfied: the port carries the actual downstream facts, not just names— 4. Coproduct dissolution. No new Rust substrate enum debt shows up here. The new 5. Single authority. Mostly good. Moving the effect algebra into 6. API-level enforcement. Within the model, yes: idempotency is derived from Design question. Should Stage 2a bank the Verdict. APPROVE_WITH_COMMENTS. The port looks careful, the fail-closed derivation behavior matches the current effects acceptance surface, and the added smoke tests are scope-appropriate for a “structural carry-over only” step. I would merge this, with the LOOP HEALTH: converging — this round turns previously decorative |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 50e6024c0b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| DELETE => delete_or_create(last_param: last_path_param(template: path)) | ||
| PUT => upsert_or_create(last_param: last_path_param(template: path)) | ||
| PATCH => upsert_or_create(last_param: last_path_param(template: path)) |
There was a problem hiding this comment.
derive_effect_shape calls last_path_param here, and derive_op_effect also calls parse_path_template, but src/v3/std/effects.dag only inlines the carrier types and never declares/imports those helper functions. Bootstrap does not load dsl/std/http_path.dag (see the hardcoded fixture list in src/v3/compiler/src/bootstrap.rs:103-123), so these callable references stay dangling and inference will fail with ResolveError when compiling code that includes these std bodies.
Useful? React with 👍 / 👎.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 50e6024c
BLOCKING (2)
Root Cause
src/v3/std/effects.dagEffect shape is modeled once on OperationEffect and again inside IdempotencyEvidence -> pick one authority and derive the other projection instead of storing both.src/v3/std/effects.dagCreateEffect currently compresses multiple derivation causes and the classifier only receives the compressed shape -> carry HttpMethod or explicit derivation provenance into the agreement decision, or split those causes structurally.
Non-blocking — Strengths
src/v3/std/effects.dagThe inline UrlPathToken/PathTemplate bridge is documented, bounded to two carriers, and names the std.http_path port as its dissolution trigger, so this bootstrap duplication is tracked debt rather than silent drift.src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rsThe new bootstrap smoke matches the Stage 2a acceptance gate by checking Dag::new() registration instead of stopping at parse-only coverage.
ROADMAP — Verified
- Lane 2 Stage 2a acceptance: The PR lands both the parse smoke and the bootstrap signature/type smoke called out in docs/lane2-compile-time-proofs.md.
ROADMAP — Incomplete
- Lane 2 Stage 2b handoff: ModifierAgreement still conflates distinct CreateEffect causes, so the next idempotency lens would inherit the wrong disagreement semantics if it consumes this surface unchanged.
| } | ||
|
|
||
| // Per-operation effect entry in a workflow. | ||
| type OperationEffect { |
There was a problem hiding this comment.
BLOCKING: OperationEffect carries shape separately from IdempotencyEvidence.shape, so contradictory effect models are representable and compose_effects can read a different authority than downstream consumers (illegal states unrepresentable / single authority).
| // the derivation says otherwise. POST-with-no-path-key is the | ||
| // fail-closed-but-maybe-idempotent case (DerivationUnknown); every | ||
| // other shape is a hard Disagrees. | ||
| fn classify_idempotent_disagreement(shape: EffectShape) -> ModifierAgreement { |
There was a problem hiding this comment.
BLOCKING: classify_idempotent_disagreement collapses every CreateEffect into DerivationUnknown, so keyless PUT/PATCH/DELETE lose the HttpMethod fact and are misreported as maybe-idempotent (facts flow forward).
|
BLOCKING (2) Root Cause
Non-blocking — Strengths
ROADMAP — Verified
ROADMAP — Incomplete
|
ChatGPT ReviewPrinciple audit. Grounding this in the thesis’s decompression/lossiness claim and the active six-principle checklist, not just source parity with v2 ( Fail-closed. This mostly looks good for a Stage 2a port. The derivation stays conservative instead of fabricating keys — Illegal states unrepresentable. BLOCKING: Facts flow forward. BLOCKING: the same Coproduct dissolution. Most of the port looks fine here: Single authority. I do not see a new hidden second authority in the staged helper inlining itself; the API-level enforcement. BLOCKING: the API currently relies on contributors knowing that Design question. Is That matters because the current type shape answers “all modifiers” in its field names, but answers “one branch won” in its data model. If Stage 2b consumes this as authoritative, it will learn a lossy substrate shape and every later fix gets more expensive. If the intent is one-axis-at-a-time, the API should enforce that instead of accepting both booleans and silently collapsing them. Verdict. REQUEST_CHANGES. The port itself looks disciplined, and the new parse/bootstrap smokes are real progress. But I would fix LOOP HEALTH: converging — this round clearly advances Stage 2a by landing the port plus real bootstrap/parse coverage, but |
Meta-Review (Loop Health)According to a document from April 17, 2026, the visible loop on PR #513 is surfacing the same substrate debt more clearly, but not yet converting that insight into a structural rule. 🔁 PAUSE_AND_REGROUP. Loop summary. Visible history: 3 review rounds, 1 visible revision state in the supplied artifacts, 1 codex review, 2 browser reviews, over about 27 minutes (17:34:17Z → 18:01:21Z). The attachments show the current diff and the three review events, but not a full commit ledger, so the honest count is one visible snapshot rather than a recoverable PR-wide commit total. Forward progress evidence. The loop did accomplish one concrete thing: The problem is that the project’s own roadmap still treats Debt accumulation evidence. Net scaffold count went up, not down. The reviews repeatedly call out the inline More importantly, the later reviews are not finding unrelated bugs. They are converging on the same class: split effect authority, compressed CreateEffect provenance, and a lossy Cheating signal. The implementer is documenting the edge compromises, but not the core ones. The Meta-verdict. 🔁 PAUSE_AND_REGROUP This is not revert territory: the port plus smoke coverage are useful. It is not ship-with-debt territory either: the debt sits exactly at the first real consumer boundary, and the roadmap says that is the moment where |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · a26ec323
✅ Review (blocking: 0, non-blocking: 1+/0-)
Non-blocking — Strengths
src/v3/compiler/tests/lane2_stage_2a_effects_smoke.rsThe added helper smoke closes the bootstrap self-containment gap by provingeffects.dagregisters the inlined path helpers underDag::new().
|
✅ Review (blocking: 0, non-blocking: 1+/0-) Non-blocking — Strengths
|
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Three lossy compressions in the new v3 effect substrate. All three are cheap to fix during the port; all three become harder once Stage 2b/2c read this surface. Anchored in INVARIANTS.md L:992 ("every fact in exactly one place") and L:2022 ("make illegal states unrepresentable").
Blocker 1 — ModifierCheck.agreement is one verdict over two independent axes
type ModifierCheck {
...
declared_idempotent: Bool
declared_readonly: Bool
derived_shape: EffectShape
agreement: ModifierAgreement // <-- one field, two facts
}
A PUT declared both idempotent and readonly is two independent questions ("is the idempotent claim true?" and "is the readonly claim true?") with two independent answers. One agreement field answers one, and check_modifier_vs_derivation's branch order picks which. The other axis is silently dropped. Concrete bad state: PUT declared idempotent + readonly returns Agrees because the idempotent branch matched first, even though readonly should disagree.
Fix — split per axis, fold "declared" into Option:
type ModifierCheck {
operation_name: String
derived_shape: EffectShape
idempotent_check: Option<ModifierAgreement> // Some iff declared_idempotent
readonly_check: Option<ModifierAgreement> // Some iff declared_readonly
}
Option<T> subsumes the boolean and the verdict in one field; a contributor cannot construct "declared but no verdict" or "verdict but not declared."
Blocker 2 — OperationEffect.shape and IdempotencyEvidence.shape store the same fact twice
type OperationEffect {
shape: EffectShape
evidence: IdempotencyEvidence
}
type IdempotencyEvidence
= LatticeEffect { shape: EffectShape } // <-- duplicate
| IdentityEffect
| NonIdempotent { shape: EffectShape, ... } // <-- duplicate
Single-authority violation directly (INVARIANTS.md L:992). Fix: drop shape from the two IdempotencyEvidence variants. Consumers who need shape read OperationEffect.shape. The variant contributes provenance (lattice / identity / why-not), not shape.
type IdempotencyEvidence
= LatticeEffect
| IdentityEffect
| NonIdempotent { reason: String }
Blocker 3 (acknowledged soft) — CreateEffect compresses three causes
POST-always, PUT-no-key, DELETE-no-key all derive CreateEffect. Stage 2b will likely want to distinguish "legitimate POST create" from "fail-closed fallback because no key was derived" (different fix-it suggestions, different failure modes). v2 compresses these too; v3 Stage 2a is the port-time window to split:
type EffectShape
= ReadEffect
| UpsertEffect { key_source: KeySource }
| DeleteEffect { key_source: KeySource }
| CreateEffect { cause: CreateCause }
| AppendEffect
type CreateCause
= PostAlways
| KeylessFallback { method: HttpMethod } // PUT/DELETE with no path param
Soft because it is the codex blocker from the previous round, and "fix now or punt explicitly to 2b" is a reasonable judgment call. Punt is acceptable IF named as a 2b dissolution target in Lane 2 Stage 2a → 2b handoff notes — otherwise it calcifies as "the v3 effect shape" silently.
Non-blocking notes
- Inline
UrlPathToken/PathTemplate/parse_path_template/last_path_paramcarry-over withstd.http_path.dagnamed as dissolution trigger is the right tracking shape. Keep as-is. - The
Dag::new()bootstrap smoke test is the right acceptance gate per the staged plan; the "5 representative function signatures" specificity is good — beats parse-only coverage.
Verdict
REQUEST_CHANGES. Fix blockers 1+2 inline (substrate is being defined by this PR; later reshape costs much more). Decide blocker 3 explicitly: fix now, or punt with named 2b dissolution target.
Two codex blockers on 86ee7e9: 1. `resolve_operator_arrow`'s primitive fallback mirrored the refined lhs carrier onto every operand position, so the new universal refinement-discharge pass treated the mirrored refinement as a real requirement. Literal `10` in `d > 10` (with `d: Int where d != 0`) was typed as `Int where d != 0` on the callee side and failed discharge. Fix: `strip_refinement_to_base` normalizes primitive- operator inputs/output to the underlying base declaration. Operators are structurally over base types; refinements are surface-level facts about values, not part of an operator's arrow contract. 2. `refinement_targets_equal` compared `TransformTarget::Callable` targets via nominal `DeclarationId` equality, but call lowering materializes a fresh `Instantiation` per call-site when the callee has retained template arguments. Two syntactically identical calls to the same generic predicate from different refinement contexts carried different Callable ids. Fix: compare through `declaration_shapes_equivalent`, which walks `Instantiation` / `ResolvedIdentifier` and compares template + substituted arguments structurally. Converts the PR's narrowed-already-refined test from the call-shaped workaround (`is_big(d, 10)`) to the operator-shaped honest form (`d > 10`), which fix 1 unlocks. Adds a new callable-predicate structural-identity test with a generic predicate called from two refinement sites. Demotes ROADMAP 3a.3 from ✅ Shipped to 🟡 Partial — the admitted- surface vs supported-fragment mismatch remains: `lower_parameter_ refinement` accepts any `SurfaceExpr`, but `predicates_structurally_ equal` walks only `Value`/`Transform`. A `where`-expression that lowers through `Branch` is accepted at lowering and rejected at discharge as "not equal" rather than "unsupported shape." Closure requires either rejecting out-of-fragment shapes at lowering or extending the walker — same lossy-compression pattern catalogued in PR #511 (Cluster/IntraClusterCall) and PR #513 (ModifierCheck/ EffectShape). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Superseded by #517, which carries the Stage 2a port onto |
* Lane 3 Stage 3a.3-full: where refinement consumer wiring (DB-11)
Predicate lowering, call-site structural-equality discharge, and
arm-local narrowing for `where` refinements on fn parameters.
- lower.rs: lower_parameter_refinement builds a predicate Declaration
(Arrow with UserDefined Bind body) + refined type Declaration
aliasing the base via ResolvedIdentifier with refinement: Some(pred).
Threaded into seed_function_signature, lower_fn_item_expr_body, and
lower_fn_item_unparsed. narrow_scope_for_predicate rebuilds the
then-arm scope when the cond is a single-parameter predicate.
- infer.rs: decide_transform runs check_refinement_discharge after
structural equivalence. predicates_structurally_equal walks both
predicate DAGs, pairing each side's Bind.params[0] as the refined
parameter slot. No SMT, no entailment, no interning.
signature_type_shape stops at refinement carriers so Arrow walks
preserve the refined decl id on the callee side.
- m2_feature_parity_test.rs: 8 acceptance tests for refined-parameter
compile, literal-arg rejection, matching-refinement forwarding,
distinct-refinement non-discharge, if-predicate narrowing,
non-narrowing rejection, signatureless regression, substrate
integrity (Behavior still 5 variants).
- ROADMAP + dag.rs doc comment: flip 3a.3 to Shipped; document
consumer wiring; note emission follow-up for narrowed ports.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* DB-11 (3a.3): walk refinement alias chain in discharge
Narrowing an already-refined parameter creates a decl that carries only
the narrow predicate in `refinement` while aliasing the outer refined
decl via `Atom(ResolvedIdentifier(outer))`. The outer decl still carries
its own refinement. Previous discharge read only
`actual.declaration.refinement` (the innermost), so programs like
fn caller(d: Int where d != 0) -> Int =
if is_big(d, 10) then div(n, d) else 0
were false-rejected: the narrowed port's refinement is `is_big(d, 10)`,
not `d != 0`, even though `d != 0` is structurally carried on the alias
chain. `check_refinement_discharge` now walks the chain and discharges
if ANY level's refinement walks structurally equal to the callee's.
Pure structural walk, still no SMT or entailment.
Addresses ChatGPT codex review on PR #515.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* DB-11 (3a.3): strip operator operands + structural callable identity
Two codex blockers on 86ee7e9:
1. `resolve_operator_arrow`'s primitive fallback mirrored the refined
lhs carrier onto every operand position, so the new universal
refinement-discharge pass treated the mirrored refinement as a real
requirement. Literal `10` in `d > 10` (with `d: Int where d != 0`)
was typed as `Int where d != 0` on the callee side and failed
discharge. Fix: `strip_refinement_to_base` normalizes primitive-
operator inputs/output to the underlying base declaration. Operators
are structurally over base types; refinements are surface-level
facts about values, not part of an operator's arrow contract.
2. `refinement_targets_equal` compared `TransformTarget::Callable`
targets via nominal `DeclarationId` equality, but call lowering
materializes a fresh `Instantiation` per call-site when the callee
has retained template arguments. Two syntactically identical calls
to the same generic predicate from different refinement contexts
carried different Callable ids. Fix: compare through
`declaration_shapes_equivalent`, which walks `Instantiation` /
`ResolvedIdentifier` and compares template + substituted arguments
structurally.
Converts the PR's narrowed-already-refined test from the call-shaped
workaround (`is_big(d, 10)`) to the operator-shaped honest form
(`d > 10`), which fix 1 unlocks. Adds a new callable-predicate
structural-identity test with a generic predicate called from two
refinement sites.
Demotes ROADMAP 3a.3 from ✅ Shipped to 🟡 Partial — the admitted-
surface vs supported-fragment mismatch remains: `lower_parameter_
refinement` accepts any `SurfaceExpr`, but `predicates_structurally_
equal` walks only `Value`/`Transform`. A `where`-expression that
lowers through `Branch` is accepted at lowering and rejected at
discharge as "not equal" rather than "unsupported shape." Closure
requires either rejecting out-of-fragment shapes at lowering or
extending the walker — same lossy-compression pattern catalogued in
PR #511 (Cluster/IntraClusterCall) and PR #513 (ModifierCheck/
EffectShape).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* DB-11 (3a.3): add `&&` / `||` as first-class OperatorKind::Logical
Prerequisite for the composite-canonical refinement refactor. Substrate
previously had no logical operators — `OperatorKind` was `Arithmetic |
Comparison` only — so a `where` clause like `d > 0 && d < 10` failed
at parse, and narrowing an already-refined param had to synthesize its
composite via the `Atom(ResolvedIdentifier(outer))` alias chain. That
alias-chain workaround is the "composite vs chain" shape the ChatGPT
review flagged: the same conjunction of refinements was representable
as either one composite predicate (unreachable without `&&`) or a
chain of unary narrowings. With `&&` / `||` landed, the canonical
composite form becomes expressible and the next step can collapse the
two shapes into one.
Additions:
- `operators::LogicalOp { And, Or }` and `OperatorKind::Logical(_)`.
- `tokenize::TokenKind::{AmpAmp, PipePipe}`; punctuation matches `&&`
and `||` (added before the existing `|` fallback so `|>` still
tokenizes).
- `parse::parse_logical_or` + `parse_logical_and` inserted between
`parse_expr` and `parse_comparison` — `||` lower than `&&` lower
than comparison, left-associative both, standard precedence.
- `infer::resolve_operator_arrow` primitive fallback now types
Logical as Bool → Bool → Bool independent of `lhs_type`. An Int
lhs on `&&` surfaces a Bool mismatch instead of propagating
through the operand slots (which is what Arithmetic / Comparison
do by design, but would be wrong for Logical).
- Emitters (`emit_rust`, `emit_python`, `emit_go`) short-circuit
Logical before the algebra-field lookup — Bool has no
`OrderedRing`-style algebra today, and Logical is Bool-
monomorphic, so there is nothing to dispatch through. Rust / Go
render `&&` / `||`; Python renders `and` / `or`.
Tests: 3 new — `where d > 0 && d < 10` compiles (composite
refinement body), `where d < 0 || d > 100` compiles (disjunction),
`fn f(d: Int) = d && d` rejects (non-Bool operand surfaces as
diagnostic). All 23 m2 tests pass; workspace green; clippy + fmt
clean; stage0 ratchet at 0.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* DB-11 (3a.3): composite-canonical refinements + single construction authority
One substrate shape per logical fact, one constructor per shape.
**Canonical conjunction = composite predicate.** A port's refinement
is always a single predicate `Declaration`; no alias chains. User-
written `where d > 0 && d < 10` and narrowing-produced
`where outer_pred && new_pred` share the same substrate shape — one
`Bind { value: Transform(Logical(And), [lhs_body, rhs_body]) }`.
`narrow_scope_for_predicate` over an already-refined port clones the
outer predicate's body with its param slot re-pointed at a fresh
composite slot (`clone_predicate_body`), joins with the freshly
lowered cond via a `Transform(Logical(And))`, and wraps the result in
one new refined `Declaration` whose connective aliases the TRUE BASE
— not the outer refined decl. The ChatGPT-reviewer "chain vs composite"
shape duality is closed: there is only composite.
**Discharge simplifies.** `check_refinement_discharge` drops the alias-
chain walk from 86ee7e9. A new `predicate_discharges` accepts either
full structural equality or a composite conjunct match: if the
actual predicate's body root is `Transform(Logical(And), [a, b])`,
the composite discharges the expected predicate iff either `a` or
`b` does, recursively. Pure structural — the conjunction fact lives
on the substrate, discharge reads it.
**Single construction authority.** `seed_function_signatures_phase`
is now the only caller of `lower_parameter_refinement` for parameter
`where` clauses. `lower_fn_item_expr_body` reads the seeded `Arrow`
inputs + output directly; `lower_fn_item_unparsed` is deleted (seeding
already produced the final `Arrow { body: Unparsed(body_span) }` for
`SurfaceItem::FnExternalBody`). Before: body lowering re-ran
`lower_parameter_refinement` and overwrote the Arrow, leaving the
seeded predicate Bind + refined Declaration orphaned. After: one
constructor, one Declaration, one Bind per `where`.
**ROADMAP.** Landing section rewritten to reflect the structural shape
(not just the list of fixes). Branch-shaped predicate bodies remain
tracked debt — out-of-fragment `Branch` nodes fail-closed at
narrow-time (clone returns None, narrowing falls back cleanly).
Tests: all 23 `m2_feature_parity` pass. The narrowed-already-refined
test now exercises the composite conjunct path (composite =
`d != 0 && d > 10`, callee expects `d != 0`, conjunct match succeeds)
instead of the alias-chain walk.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* DB-11 (3a.3): defer parameter refinement lowering to a post-data phase
Codex P1 on `ef4ec7b`: `seed_function_signatures_phase` ran BEFORE the
data pre-pass populated top-level `data` declarations' connectives
and `value_body`s. A `where` predicate referencing a top-level
constant — e.g., `where d > THRESHOLD` with `data THRESHOLD: Int = 10`
— resolved the reference against a placeholder declaration and
marked the port `Unresolved`, creating an order-dependent false
failure. The previous build masked this because body lowering re-ran
`lower_parameter_refinement` (after data was populated) and overwrote
the Arrow; the single-construction-authority fix removed that re-run,
which exposed the latent ordering bug.
Fix splits refinement lowering off seeding into its own phase
`lower_parameter_refinements_phase`, run AFTER the data pre-pass and
BEFORE the main fn-body pass. Seeding now seeds base decls only; the
new phase lowers refinements and updates the fn's Arrow inputs with
the refined decl ids. Sole caller of `lower_parameter_refinement` for
parameter `where` clauses — single construction authority preserved
across the ordering fix.
Test: `test_3a3_refinement_references_top_level_data_constant` —
regression lock exercising the exact shape codex flagged
(`data THRESHOLD: Int = 10` + `fn big(d: Int where d > THRESHOLD)`).
Also records P1.2 (`signature_type_shape` skipping substitution for
refined generic parameters) as tracked ROADMAP debt — latent before
DB-11 consumer-wiring (no tests exercised refined generics); visible
now. Fix requires substituting through the refinement carrier and
re-attaching at call site, or rejecting refinements on type
parameters at lowering. Out of scope for this PR.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* DB-11 (3a.3): flatten-and-subset conjunction discharge
ChatGPT R5 review on `31a3709d`: "refinement conjunction is not yet
canonical independent of grouping — `a && (b && c)` and `(a && b) && c`
are distinct substrate shapes for the same logical fact." Load-bearing
example: outer refinement `a` narrowed under cond `b && c` produces
composite body `a && (b && c)` (right-associated by
`build_narrowed_refinement`'s `outer && new`). Before this fix,
`body_discharges` could only recurse into one root conjunct of the
actual tree at a time, so forwarding that narrowed value to a callee
expecting `a && b` rejected the program — `a && b` is not a subtree
of `a && (b && c)`, even though the logical fact holds.
Fix: treat a predicate body as the maximal multiset of non-`And`
leaves reachable by recursively unfolding every
`Transform(Logical(And), [lhs, rhs])` root. `body_discharges` now
flattens both actual and expected, then checks that every expected
leaf has a structurally-equal actual leaf. `a && (b && c)`,
`(a && b) && c`, and `a && b && c` all share leaf multiset
`{a, b, c}` and discharge each other symmetrically.
Still pure structural — no SMT, no ordering, no entailment beyond
leaf-membership. The reviewer explicitly offered this as an
acceptable resolution ("discharge needs to compare flattened
conjunct sets rather than syntax trees"); lowering-time
canonicalization would also work but has larger blast radius.
Test: `test_3a3_conjunction_discharge_ignores_grouping` — regression
lock using narrowing to produce the right-associated composite
(parens aren't in the v3 surface yet, but narrowing's
`outer && new_cond` nesting is enough to exercise the asymmetry).
Pre-flatten, the test rejects; post-flatten it compiles.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* DB-11 (3a.3): reject out-of-fragment `where` predicate shapes at lowering
Codex BLOCKING on `df5fc7b3`: `lower_parameter_refinement` accepts any
`SurfaceExpr` into `Declaration.refinement`, but the discharge walker
(`refinement_ports_equal`) and the composite-narrowing clone
(`clone_predicate_body`) only model `Value` and `Transform` predicate
bodies. A `where if cond then ... else ...` was admitted at lowering
and failed downstream as a generic "not structurally equal" mismatch
— the admitted surface was wider than the supported fragment, and the
boundary between them was behavioral instead of honest.
Fix (Option A from codex): fail-closed at the lowering boundary. A
new `refinement_predicate_out_of_fragment` walks a `where` predicate's
`SurfaceExpr` and returns `Some((shape_label, span))` for the first
`If` / `Match` / `Lambda` / `Record` / `List` node reached.
`lower_parameter_refinements_phase` calls this gate before lowering
each refinement; out-of-fragment shapes yield a `ResolveError`
diagnostic naming the unsupported construct and the parameter reverts
to its base (unrefined) declaration. The user sees the honest boundary
message at the `where` span instead of a misleading downstream "not
equal" at a call site.
Option B (extend the walker/clone to model Branch/Loop/Bind) stays on
the ROADMAP as future work; the landed fragment gate makes it a
pure extension path with no silent-compromise debt between here and
there.
Test: `test_3a3_rejects_out_of_fragment_refinement_predicate` — locks
that `where if cond then ... else ...` rejects at lowering with a
shape-named diagnostic.
ROADMAP Remaining now has only refined-generic-substitution as
open work (previously two items); admitted-surface/supported-fragment
moved to "Closed (this PR)."
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 participant
Summary
dsl/std/effects.dag→src/v3/std/effects.dag. Structural carry-over only per Lane 2 Stage 2a scope. Unblocks Lane 2 Stage 2b (workflow idempotency lens).PathTemplate+UrlPathTokeninlined as minimal carriers fromdsl/std/http_path.dag(the full file doesn't yet port to v3; inline definitions are structural-identical so a future port replaces them without reshapingeffects.dag).if ... then ... else, single-binding match arms, explicit variant enumeration). Bodies reflatten toward the v2 shape when v3 grows&&/||/_wildcard /if-block form.list.dagpattern:build.rspicks upsrc/v3/std/*.dagautomatically, nobootstrap.rsedit needed.What's in this PR
src/v3/std/effects.dag— the portsrc/v3/compiler/tests/real_stdlib_parse_smoke.rs—effects_dag_parsesmatches the existing per-std-file patternsrc/v3/compiler/tests/lane2_stage_2a_effects_smoke.rs— Stage 2a acceptance smoke:effects_dag_bootstraps_without_diagnostics— fullDag::new()bootstrap sees no diagnostics fromeffects.dageffects_dag_exposes_five_representative_function_signatures—is_idempotent_effect,compose_effects,derive_effect_shape,check_modifier_vs_derivation,generate_idempotency_obligationsall registered as Arrow declarationseffects_dag_exposes_core_effect_algebra_types—EffectShape,KeySource,IdempotencyEvidence,ComposedEffect,OperationEffectall present as record/enum typesAcceptance (per docs/lane2-compile-time-proofs.md:52)
effects.dagreturns emptycargo clippy --all-targets -- -D warnings)cargo fmt --all --check)cargo test --workspace --exclude v2-compiler-tests)Ports
Types:
EffectShape(Read / Upsert / Delete / Create / Append)KeySource(PathParam / InputField / CompositeKey)IdempotencyEvidence(Lattice / Identity / NonIdempotent)ComposedEffect,OperationEffectDerivedOpEffect,ModifierAgreement,ModifierCheckIdempotencyTestObligation,WorkflowEffectConcernPathTemplate,UrlPathToken(inlined; see note above)Functions:
is_idempotent_effect— derives idempotency from EffectShape variantcompose_effects— workflow-level idempotency verdict via first-breaker scanparse_http_method— String → HttpMethod?derive_effect_shape— HttpMethod × PathTemplate → EffectShape (fail-closed per v2 table)derive_op_effect— combines parse + derive for a single opcheck_modifier_vs_derivation— cross-checks declaredidempotent/readonlyagainst derivationgenerate_idempotency_obligations— filters idempotent ops, emitsf(f(x)) == f(x)test obligationsNot in this PR
std.http_pathport — deferred; inline carriers ineffects.dagsatisfy Stage 2a.🤖 Generated with Claude Code