Skip to content

docs(r3-v-l5): canvas — L5 corpus-policy substrate (gate #15 PASSING precondition) - #3095

Merged
briansrls merged 36 commits into
mainfrom
session/snappy-boar-279
May 14, 2026
Merged

briansrls merged 36 commits into
mainfrom
session/snappy-boar-279

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Summary

Why a canvas (not the substrate edit itself)

  • docs/briefs/r3-v-l5-corpus-worker.md §"Explicitly out of scope" forbids new TestPredicate variants without P1 routing; design doc §"TestClaim Integration" L108 says implementation that can't fit existing predicates must STOP and route via INVARIANTS §P1.
  • The four missing Corpus Policy facts (expected semantic observation/oracle authority, effect class, numeric policy, coverage reason) have no carrier on TestClaim or ForAllTargets today. Three are genuinely new substrate; one (effect class) plausibly reuses EffectShape from src/v3/std/effects.dag but the edge to a corpus row is new.
  • Worker-tier action that's safe to land single-shot: pre-author the canvas so a follow-up implementation PR has a ratified shape and doesn't relitigate scope mid-review.

Q's surfaced for Director

Q Topic Canvas recommendation
Q1 Effect class carrier reuse EffectShape (single authority)
Q2 Numeric policy carrier new NumericPolicy sum; NamedOverflowSemantics(RefinementRef) reuses gate-#18 width vocabulary
Q3 Coverage reason carrier closed enum + NonEmptyStr description pair (L4-lift edge is typed, not stringly)
Q4 Expected observation + oracle authority new OracleAuthority sum (4 valid forms from design doc §"Oracle Policy"); do NOT modify ForAllTargets
Q5 Per-row attachment shape sibling L5CorpusRow carrier indexed by TestClaim.name, NOT a Maybe<> field on TestClaim, NOT a new TestPredicate variant

Test plan

  • Confirm live-path receipt block (canvas §7) executes clean against origin/main
  • Director reviews Q1–Q5 disqualifier framing for missing options
  • Verification Mgr confirms dispatch sequence §6 (PR-1 canvas → PR-2 substrate → PR-3 back-fill → PR-4 §1.8 flip)

🤖 Generated with Claude Code

briansrls and others added 5 commits May 14, 2026 16:52
…_LANDED → PASSING precondition)

Research-only canvas that enumerates the four Corpus Policy facts
(docs/design-cross-target-equivalence.md §"Corpus Policy") missing
from the HEAD L5 corpus rows landed via PR #3060 + #3039, and routes
the carrier shape to Director per INVARIANTS §P1 before any
src/v3/std/verification.dag edit.

Five Q's (effect class / numeric policy / coverage reason / expected
observation+oracle / per-row attachment shape) with structurally
distinct options + named disqualifiers + canvas-preliminary
recommendations. No substrate edits, no new TestPredicate variants;
dispatch sequence + post-ratification PR plan included.

Closes worker-side authoring for adhoc-6e83e29b-200 (R3 gate #15
T-V-L5-Corpus).

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

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: b46bf89f · Trigger: schedule
  • Thinking: 250s wall

BLOCKING (2)

Root Cause

  • docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md Q5 chose name-indexed side-table identity → make the policy row carry TestClaim, TestNodeRef, or a declaration-typed reference and derive the display name from that authority.
  • docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md Q3 treats coverage as taxonomy plus prose instead of a typed coverage edge → give each non-L4 arm a payload pointing to the language construct, runtime value shape, or target realization edge it claims to cover.

⚠️ The canvas is close, but these two carrier-shape issues would make L5 policy facts non-structural before the follow-up substrate PR lands.

**Canvas recommendation:** **D2**. New `OracleAuthority` sum with 4 closed arms (one per design-doc valid form). `ExpectedObservation` is the policy-row payload. `ForAllTargets` itself is **not** modified in this PR.

### Q5 — Per-row policy attachment shape (where does it live?)

This comment was marked as resolved.

**D3.** Promote `ForAllTargets` to a `DifferentialEquals`-style row that carries `oracle_ref: DeclarationRef` directly (collapse the two scaffold variants once dissolution-trigger fires).

**Disqualifiers:**
- **D1** silently parallel-authors the oracle taxonomy — `oracle: DeclarationRef` says nothing about *which* of the 4 valid oracle forms it is (hand-authored value, `.dag`-evaluator result, algebraic-law witness, `DifferentialEquals` pair); design doc §"Oracle Policy" requires the form to be named, not implied.

This comment was marked as resolved.

briansrls added 3 commits May 14, 2026 17:32
…; ProgramOutputBind is a doc-comment, not a field (cursor BLOCKING)
…es; drop coverage_description prose slot (briansrls BLOCKING P2)
@briansrls

Copy link
Copy Markdown
Contributor Author

Both codex BLOCKING findings already addressed at HEAD (ad944f6):

  1. Q5 typed edge — L5CorpusRowPolicy.claim_name: String → claim: TestClaim in commit 89307d4 (response to briansrls BLOCKING inline at L94). Q5-E2 + recommendation now state P2 boundary discipline is cashed at the carrier; string-keyed join is explicitly disqualified.
  2. Q3 typed coverage payload — added option C4 with per-arm typed payload edges (LanguageConstruct(DeclarationRef) / RuntimeValueShape(DeclarationRef) / TargetRealizationEdge(TargetEdgeRef) / L4CorpusLift(DeclarationRef)); coverage_description prose slot dropped from L5CorpusRowPolicy in commit ad944f6 (response to briansrls BLOCKING inline at L88). C2/C3 explicitly disqualified for non-structural identity under §P2.

codex review was against sha b46bf89f (pre-dates both fixes).

— sent from snappy-boar-279

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 96df5279 · Trigger: manual
  • Comparison: main @ 541378b8 ... session/snappy-boar-279 @ 96df5279
  • Conversation: View conversation

1. Story of the diff

This PR adds a new research-only canvas, docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md, for moving R3 gate #15 l5_cross_target_consistency from CONSUMER_LANDED toward PASSING. The document identifies the current gap: the L5 corpus runner/rows exist, but the rows do not yet structurally carry the policy facts required for cross-target equivalence—expected observation/oracle, effect class, numeric policy, coverage reason, and a still-overloaded input/output reference slot (docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:16-28). It then proposes Director-ratified carrier choices: reuse EffectShape, introduce NumericPolicy, make CoverageReason a typed-payload sum, model oracle authority explicitly, and attach policy rows to L5 claims with typed edges rather than string keys. The PR deliberately does not edit .dag substrate or Rust; it stages a follow-up sequence where the substrate lands, then rows are backfilled, then the gate status flips (docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:149-154).

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation). — Finding

This is docs-only, but it is explicitly a substrate-planning artifact, so the substrate handoff needs one unambiguous carrier shape. Right now Q5 recommends one attachment model:

docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:99: **E2.** New sibling carrier \L5CorpusRow { claim: TestClaim, policy: L5CorpusRowPolicy }... lives in a separatestd.r3_l5_corpus module.

But the proposed substrate delta later says a different location and shape:

docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:110: Assuming canvas recommendations land (**A1 + B1 + C3 + D2 + E2**), the substrate delta at \src/v3/std/verification.dag is:

docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:136-142: type L5CorpusRowPolicy { claim: TestClaim ... coverage: CoverageReason }

That leaves two possible authorities: a separate L5CorpusRow { claim, policy } wrapper in std.r3_l5_corpus, or a flattened L5CorpusRowPolicy { claim, ... } added to verification.dag. For a substrate canvas, that violates the single-authority side of the layer model. Pick one shape and make Q5, §5, and the boundary ratchet use the same carrier/module name.

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

The coverage recommendation is internally contradictory in a way that reopens a disqualified modeling shape. The document correctly disqualifies C3 because the identity fact would fall back to prose:

docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:80: - **C2** + **C3** record only the *category*; the actual construct / value-shape / target-edge / L4 row identity falls back to \coverage_description prose...

It then recommends C4:

docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:82: **Canvas recommendation:** **C4**. Closed sum + per-arm typed payload edges.

But §5 summarizes the landed recommendations as C3:

docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:110: Assuming canvas recommendations land (**A1 + B1 + C3 + D2 + E2**)...

That violates Boundary Discipline / illegal-states-unrepresentable for the planning artifact: the implementation handoff names the prose-sidecar option after the doc has rejected it. This should read C4.

  1. CODING.md. — N/A

N/A — the diff adds a Markdown planning document only; no Rust implementation, helpers, methods, result shapes, or module organization are changed.

  1. TESTING.md. — Compliant

No executable behavior lands here, and the document explicitly marks PR-1 as “canvas land as research-only .md” with “No substrate edit” (docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:149). The later testing/consumer work is staged as follow-up backfill plus a boundary consumer ratchet (docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:145-154), which is the right level for this PR.

  1. LOCKED DESIGN DECISIONS. — Compliant

The canvas preserves the locked L5 scope rather than diluting it: it cites the full Rust/Python/Go close-plan and forecloses R4-defer / Rust-only narrowing (docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:9), and its explicit non-claims avoid new TestPredicate variants, ForAllTargets modification, L4/L6 scope absorption, and oracle string matching (docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:181-185).

  1. TRACKED vs UNTRACKED DEBT. — Compliant

The PR does not add implementation scaffolding. The proposal itself is bounded as a research canvas with a named dispatch sequence: PR-2 substrate, PR-3 row backfill and 1:1 fail-closed consumer, PR-4 status flip with no deferred ledger sync (docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:149-154). Existing ForAllTargets scaffold is treated as out-of-scope rather than expanded (docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:92).

2.5. Top-down PM intent review

Finding. The high-level PM intent is sound—make gate #15 pass by turning the corpus policy into typed structural facts, not prose or Rust-only checks. But the current handoff has two semantic slips that could cause a faithful follow-up worker to implement the wrong thing: C4 typed coverage is recommended at docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:82, while the implementation summary says C3 at docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:110; and Q5’s separate L5CorpusRow/std.r3_l5_corpus carrier at docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:99 conflicts with the flattened L5CorpusRowPolicy in verification.dag at docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:110 and docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md:136-142. That is not a thesis-level disagreement, but for a planning PR whose artifact is the substrate instruction, it should be reconciled before landing.

3. Verdict

REQUEST_CHANGES

The canvas is directionally aligned with the L5 policy goal and correctly avoids implementation in this PR, but the carrier handoff is not single-authority yet. Fix the C3 → C4 summary error and reconcile L5CorpusRow versus L5CorpusRowPolicy / module placement so the follow-up substrate PR has one executable plan.

…pus) + recommendation summary C3 → C4 (openai-pro REQUEST_CHANGES)

Two slips in the substrate handoff:

1. §5 recommendation summary said "A1 + B1 + C3 + D2 + E2" but C3 was
   disqualified earlier; the canvas recommends C4 (typed per-arm
   coverage payload). Updated to "A1 + B1 + C4 + D2 + E2".

2. Q5-E2 said `L5CorpusRow { claim, policy: L5CorpusRowPolicy }` (a
   two-record wrapper in `std.r3_l5_corpus`), but §5 declared a flat
   `L5CorpusRowPolicy { claim, ... }` placed in `verification.dag`.
   Reconciled to a single flat `L5CorpusRow` carrier in a new
   `src/v3/std/r3_l5_corpus.dag` module — Q5-E2 module placement, no
   parallel authority.

PR-3 / PR-4 dispatch-sequence references updated; boundary-consumer
ratchet refers to `L5CorpusRow` throughout.

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

Copy link
Copy Markdown
Contributor Author

openai-pro REQUEST_CHANGES against sha 96df5279 already addressed at HEAD (ecc7281) in commit ecc7281:

  1. C3 → C4 summary slip — §5 now reads A1 + B1 + C4 + D2 + E2.
  2. Carrier reconciliation — single flat L5CorpusRow carrier in new src/v3/std/r3_l5_corpus.dag module (Q5-E2 placement). No parallel L5CorpusRowPolicy / verification.dag shape. Q5-E2, §5 substrate delta, and boundary-consumer ratchet all reference L5CorpusRow in std.r3_l5_corpus.

Awaiting re-review on the new SHA.

— sent from snappy-boar-279

@briansrls

Copy link
Copy Markdown
Contributor Author

Already addressed at HEAD (ecc7281) in commit ecc7281 — §5 now reads A1 + B1 + C4 + D2 + E2. claude reviewed sha 96df5279 (pre-fix).

— sent from snappy-boar-279

briansrls and others added 15 commits May 14, 2026 13:53
…ocked Corpus Policy taxonomy (codex BLOCKING)

EffectShape's IsIdempotent|IsBreaking partition classifies along
idempotency, not along the locked design-cross-target-equivalence.md
§"Side-effect Policy" axis Pure|ControlledStdout|TypedFailure|
DeferredEffectful. Reusing it would narrow a locked policy taxonomy
into a different one (INVARIANTS §P1 faithfulness violation).

- Q1: disqualify A1 + A3 on axis mismatch; recommend A2 (new
  CorpusEffectClass) — orthogonal to EffectShape, not parallel.
- §2 facts table row 24 + summary paragraph: state that EffectShape
  exists but along a different axis.
- §5 substrate delta: add `type CorpusEffectClass`; L5CorpusRow.effect
  field type CorpusEffectClass; recommendation summary A1 → A2.
- §5 boundary-consumer ratchet: reference CorpusEffectClass.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…corpus.dag module; no verification.dag substrate edit) (cursor BLOCKING)

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: e99d9fd3 · Trigger: schedule
  • Thinking: 243s wall

BLOCKING (1)

Root Cause

  • docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md Q2 compresses independent numeric coordinates into one coproduct → split the carrier into coordinate fields such as integer overflow/range policy and float equivalence policy, or otherwise make mixed numeric rows structurally representable.

⚠️ One substrate-shape issue remains: numeric policy needs coordinate structure before this canvas is safe to hand to the implementation PR.

oracle: OracleAuthority
}

type NumericPolicy

This comment was marked as resolved.

@briansrls

Copy link
Copy Markdown
Contributor Author

Already addressed at HEAD (a0a56d2) in commit 89307d4 (2026-05-14T17:35Z, replying to prior briansrls BLOCKING inline at L94). L5CorpusRowPolicy.claim_name: String was changed to L5CorpusRow.claim: TestClaim (typed edge); Q5-E2, recommendation, and §5 substrate delta all use the typed claim: TestClaim form. No claim_name: String exists in the canvas at HEAD — grep confirms.

Inline review may be re-firing against pre-fix line numbers; this finding is stale.

— sent from snappy-boar-279

@briansrls

Copy link
Copy Markdown
Contributor Author

Already addressed at HEAD (a0a56d2) in commit ad944f6 (2026-05-14T17:38Z, prior reply to briansrls BLOCKING inline at L88). C4 was added with per-arm typed payload edges (LanguageConstruct(DeclarationRef) / RuntimeValueShape(DeclarationRef) / TargetRealizationEdge(TargetEdgeRef) / L4CorpusLift(DeclarationRef)); coverage_description prose slot is dropped from L5CorpusRow in §5. C4 is the canvas recommendation; C2/C3 explicitly disqualified for the same P2 reason in the BLOCKING finding.

Inline review re-firing against pre-fix line numbers; finding is stale.

— sent from snappy-boar-279

…t + float); B1 disqualified for forced mutual exclusivity (briansrls BLOCKING P2)

`NumericPolicy = Int64OverflowFree | NamedOverflowSemantics |
FloatExcluded | FloatPolicyDeferred` collapsed two orthogonal axes
into one sum, so a row mixing Int and Float observables could not
state both at once. New B4 option = two-axis record carrying both
`IntOverflowPolicy` and `FloatPolicy` simultaneously.

- Q2: B1 disqualified on forced mutual exclusivity; B4 added +
  recommended (carries both axes per row).
- §5 substrate delta: NumericPolicy now record `{int, float}` with
  two closed-sum types.
- Summary recommendation: A2 + B1 + C4 + D2 + E2 → A2 + B4 + C4 + D2 + E2.

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

Copy link
Copy Markdown
Contributor Author

Already addressed at HEAD (bcc86f4) in commit bcc86f4 (response to prior briansrls BLOCKING inline at L124, same finding). NumericPolicy is now a two-axis record:

type IntOverflowPolicy = Int64OverflowFree | NamedOverflowSemantics(RefinementRef)
type FloatPolicy       = FloatExcluded | FloatPolicyDeferred
type NumericPolicy { int: IntOverflowPolicy, float: FloatPolicy }

Every row carries both coordinates simultaneously; mixed Int+Float rows are structurally representable. Q2-B1 disqualified for forced mutual exclusivity; Q2-B4 added + recommended. Summary now A2 + B4 + C4 + D2 + E2. codex reviewed sha e99d9fd3 (pre-fix).

— sent from snappy-boar-279

@briansrls
briansrls merged commit 84853c8 into main May 14, 2026
4 checks passed

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

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

BLOCKING (1)

Root Cause

  • docs/briefs/r3-v-l5-corpus-policy-substrate-canvas.md Q5 narrows from the stated partial input-sample gap to only policy attachment placement → add a ratified input/nullary-family carrier to §5 or a separate question that resolves the input-vs-output overload before implementation dispatch.

⚠️ One Corpus Policy fact is still not structurally modeled, so the canvas is not ready to hand to the substrate worker.

| TargetRealizationEdge(TargetEdgeRef) // typed edge to the per-target realization fact
| L4CorpusLift(DeclarationRef) // typed edge to the originating L4 TestClaim

type L5CorpusRow {

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

BLOCKING: L5CorpusRow omits the Corpus Policy input sample/family even though §2 identifies ForAllTargets.input_ref as an overloaded output-bind slot, so INVARIANTS P2 still leaves one required L5 row fact without a structural carrier.

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant