Wave-1 Worker B — std/constraints.dag + std/coercion.dag (strict substrate, exact-only)

[briansrls]

Auto-opened by session-dashboard for session calm-pike-379.
Pushing to session/calm-pike-379 advances this PR.

Worker attestation

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

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

Summary

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

Test plan

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

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 90239925 · Trigger: schedule
• Thinking: 337s wall

---

BLOCKING (4)

Root Cause

• src/v4/std/constraints.dag Canonical uniqueness is modeled as policy rather than a solved fact → remove the Bool and make ambiguous grounding only an Outcome::Rejected diagnostic.
• src/v4/std/coercion.dag Target choice is modeled as caller policy rather than canonical structural derivation → delete order-based selection and reject ambiguous candidates.
• src/v4/std/coercion.dag The target grounding lacks a witness tying Node to its canonical hash → reuse CanonicalGrounding or add a structural witness derived from the target Node.
• src/v4/std/coercion.dag Scaffold execution state is mixed into the terminal mismatch domain → keep the not-realized diagnostic as a tracked scaffold or gate it with a dissolution trigger.

⚠️ The substrate shape needs tightening before this lands.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 0104fe51 · Trigger: schedule
• Thinking: 333s wall

---

BLOCKING (3)

Root Cause

• src/v4/std/constraints.dag CanonicalGrounding splits root identity out of ConstraintGraph instead of projecting it from the witness → remove the duplicate root or make the witness the sole root/hash carrier.
• src/v4/std/coercion.dag Coercion result shape stores derived target beside its witness instead of projecting from CoercionWitness.target → consume the witness target as the sole authority.
• src/v4/std/coercion.dag AcceptedLoss is modeled as a singleton payload instead of a compositional loss carrier → make accepted losses accumulate under the coercion-quality composition.

⚠️ The prior inline findings are addressed, but the new substrate still admits duplicate authorities and silently drops loss evidence.

[briansrls]

BLOCKING: CanonicalGrounding.root can disagree with witness.source_graph.root, so the canonical grounding boundary has two authorities for the grounded Node (INVARIANTS P2).

[briansrls]

BLOCKING: CoercionResult.target can disagree with witness.target.root, allowing the result to expose a target Node not tied to the verified target grounding (INVARIANTS P2).

[briansrls]

BLOCKING: Composing Lossy with any later Lossy returns only the left AcceptedLoss, so accepted-loss evidence from the right branch is silently dropped across the T-9 quality boundary (INVARIANTS P2 facts-flow-forward).

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 0104fe51 · Trigger: manual
• Comparison: main @ deda6f21 ... session/calm-pike-379 @ 0104fe51
• Conversation: View conversation

---

1. Story of the diff

This PR stages two new v4 std/ substrate boundaries. src/v4/std/constraints.dag introduces the constraint graph shape, constraint provenance, and canonical-grounding witness/result surface, while keeping the actual solver fail-closed behind solve_constraints returning Rejected with a typed diagnostic (src/v4/std/constraints.dag:25-69, src/v4/std/constraints.dag:117-126). src/v4/std/coercion.dag then consumes CanonicalGrounding to model candidate target groundings, a coercion fold policy, mismatch diagnostics, witnesses, and result quality, again leaving candidate selection / fold / witness verification as fail-closed scaffolds (src/v4/std/coercion.dag:26-80, src/v4/std/coercion.dag:124-158). The intended shape is a strict exact-only substrate seam: declarations exist now so later T-9/T-10 consumers have a typed boundary, but no rewrite/coercion behavior is realized yet.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — src/v4/std/coercion.dag:77-80 violates single authority / illegal-states-unrepresentable. CoercionResult carries both witness: CoercionWitness and a separate target: Node, but CoercionWitness.target is already a CanonicalGrounding (src/v4/std/coercion.dag:71-74), and CanonicalGrounding already carries the target root: Node (src/v4/std/constraints.dag:63-65). That lets a result state target = A while its witness proves target.root = B. Because this is substrate, downstream consumers would have to choose which target authority to trust. Remove the parallel target: Node, or make the result’s target only accessible through the witness’s canonical grounding.

1. INVARIANTS.md + modeling-discipline.md.

Finding — src/v4/std/coercion.dag:64-68 violates fail-closed exact-only modeling. The file declares itself “exact-only coercion fold, no rewrites” (src/v4/std/coercion.dag:5), but the substrate admits Lossy { accepted_loss: AcceptedLoss } as a successful CoercionQuality and CoercionResult stores that quality (src/v4/std/coercion.dag:77-80). coercion_quality_compose then preserves Lossy as a composable successful quality (src/v4/std/coercion.dag:111-120). In an exact-only substrate, lossy conversion should be unrepresentable as an accepted result; loss should surface as a rejected diagnostic, or the lossy path needs an explicit PM-level design reconciliation.

1. CODING.md.

Compliant. The new code uses data plus free functions, small structured surfaces, and typed Outcome/Diagnostic returns rather than hidden state or prose-driven behavior; the staged functions fail through structured Rejected values (src/v4/std/constraints.dag:117-126, src/v4/std/coercion.dag:124-158). Comment density is also constrained to the allowed header/tag style.

1. TESTING.md.

N/A — no executable behavior is landed. The solver, candidate lookup, fold, and witness verification bodies are all fail-closed scaffolds returning Rejected (src/v4/std/constraints.dag:117-126, src/v4/std/coercion.dag:124-158). Tests would not rescue the substrate-shape violations above; the shape needs correction first.

1. LOCKED DESIGN DECISIONS.

N/A — no attached locked design text is edited or concretely diverged from in the diff. The files reference docs/design-v4-compiler-homomorphism.md anchors (src/v4/std/constraints.dag:6, src/v4/std/coercion.dag:6), but that locked authority is not part of the provided diff surface; the concrete PM-level mismatch is addressed below against the PR/file’s own exact-only contract and the thesis intent.

1. TRACKED vs UNTRACKED DEBT.

Compliant for the scaffolds. Both files mark the scaffold status and bounds in-file: constraints is tied to TASKS T-9 and exact canonical grounding (src/v4/std/constraints.dag:5), coercion is tied to TASKS T-9/T-10 and “exact-only coercion fold, no rewrites” (src/v4/std/coercion.dag:5). The not-yet-realized functions fail closed rather than fabricating outputs (src/v4/std/constraints.dag:121-125, src/v4/std/coercion.dag:140-146, src/v4/std/coercion.dag:151-157).

2.5. Top-down PM intent review

Finding — exact-only intent is semantically diluted. The thesis-level direction is that target translation/coercion is a derived homomorphism over groundings, and unfaithful translations surface as located diagnostics rather than silent bugs (THESIS.md:89-91); the PR’s own coercion file narrows this to “exact-only coercion fold, no rewrites” (src/v4/std/coercion.dag:5). Adding Lossy { accepted_loss: AcceptedLoss } as a successful quality (src/v4/std/coercion.dag:64-68) and making it compose as a successful result (src/v4/std/coercion.dag:111-120) changes that plan’s meaning: a worker following this substrate faithfully could implement accepted lossy coercion instead of rejecting non-exact mappings. That is a PM-level mismatch, not just a naming issue.

3. Verdict

REQUEST_CHANGES

The PR correctly stages fail-closed solver/fold seams, but the new coercion substrate currently permits two states the stated strict exact-only boundary should not allow: a result whose target can disagree with its witness, and a successful Lossy coercion path. Both are substrate-level issues, so they should be fixed before merge.

[briansrls]

Closing as part of Wave-1 disposition.

Same disposition arc as #3439 — closing and re-doing under a corrected brief, not because the work was wrong but because the brief encoded the pre-Pass-B parametric-duplication that PR #3443 (Pass B unification) and PR #3444 (Practice 11) now structurally name.

Why close + redo

Per Practice 11 (PR #3444), the Wave-1 constraints/coercion brief asked for declarations that are now recognized as parametric duplication of find_witness:

• solve_constraints declared as a separate substrate primitive owning std/constraints.dag — actually find_witness(_, _, constraint_satisfaction_predicate, MultiplicityPolicy::UniqueOnly). One call site of the unified primitive, not a sibling.
• coercion_fold declared as a separate substrate primitive owning std/coercion.dag — actually find_witness(_, _, exact_structural_equality_zip_fold, MultiplicityPolicy::TargetSelection(target_lang.target_selection_policy)). Same pattern.
• Lossy quality in the CoercionQuality lattice — would have allowed success-with-warning damage; explicitly removed in Pass A (PR design: Pass A + Pass B amendments — strict simplification + primitive unification #3443). WouldLoseInformation is a Rejected diagnostic, not a third success category.
• Pre-Q11 Outcome<T> shape — the PR was authored against legacy Produced / Rejected{diagnostic}; ratified shape is Accepted{value, diagnostics} | Rejected{diagnostics: NonEmpty}.

Reworking-in-place would require restructuring std/constraints.dag + std/coercion.dag to derive from the (not-yet-existing in this PR) std/find_witness.dag primitive, against a pre-Pass-B baseline. Cleaner to start fresh.

What lands separately

Wave-2 successor worker authors three related files together (per the substrate-home note added to the design doc in PR #3443):

• std/find_witness.dag — the unified primitive (operation + MultiplicityPolicy carrier with UniqueOnly | TargetSelection(TargetSelectionPolicy) for MVP; RewritePolicy(...) deferred to P7 trigger per design)
• std/constraints.dag — ConstraintGraph + ConstraintSolvePolicy + solve_constraints = find_witness(..., UniqueOnly) call site + the constraint-satisfaction predicate algebra
• std/coercion.dag — CoercionCandidateSet (with closed-candidate-set provenance witness) + coercion_fold = find_witness(..., TargetSelection(target_lang.target_selection_policy)) call site + the exact-structural-equality-zip-fold predicate algebra

Brief shape (operation-first per Practice 11): each .dag file is a call site of find_witness with a per-caller predicate + policy; NOT a sibling primitive declaration. LawfulRewriteWitness is P7-trigger, NOT in MVP.

The substance from this PR (predicate algebra shapes, witness payload thinking, TargetSelectionPolicy variant set, CoercionMismatchKind rejection-payload taxonomy) carries forward as reference for the Wave-2 worker.

Thank you to calm-pike-379 + swift-dove-578 for the work; the conceptual content carries forward, the shape gets rebuilt.

— sent from smart-boar-330