Repository navigation
R3 Verification Mgr — lane through R3 close - #3060
Conversation
|
Review metadata
1. Story of the diffThis PR tightens the 2. Invariant categories
N/A — this is implementation-only runner logic plus a Rust regression test; it does not add or alter a Dag substrate type,
Compliant — fail-closed / facts-flow-forward:
Compliant — the change stays within the existing data-and-pattern-match style: it decomposes
Compliant — the added test is behavior-driven and focused on one contract: an empty
N/A — the diff does not modify a locked design document or introduce a semantic divergence from the Pure Bootstrap / verification direction. It narrows an existing runner acceptance path by making
Compliant — no new scaffold, TODO, temporary file, or extra authority is introduced. The only forward reference is to the later byte-regeneration check, and this PR reduces the interim gap by ensuring 2.5. Top-down PM intent reviewCompliant — the change preserves the high-level verification intent: a generated-from-DAG manifest entry marked 3. VerdictAPPROVE. The PR is a narrow fail-closed tightening of an existing verification predicate, with an appropriate regression test and no substrate, locked-design, or debt-tracking issues visible in the diff. |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
f014ae98· Trigger:schedule - Thinking:
237s wall
BLOCKING (1)
Root Cause
src/v3/compiler/tests/integration/test_runner_test.rsThe new ResolvedFact negative test reused the older non-generated-path fixture shape → switch the fixture to a generated manifest path so source_hash validation is the first failing obligation.
| file_name: "pb_test_file_generated_from_dag.v3", | ||
| predicate: GeneratedFromDag(census_authority, [ | ||
| ResolvedFact { | ||
| output_path: "src/v3/compiler/tests/integration.rs", |
There was a problem hiding this comment.
BLOCKING: This fixture uses a path already outside the generated-file authority, so the runner fails on path membership before reaching the new empty-source_hash diagnostic; use a known GENERATED_FILES path to make the P3 fail-closed check actually exercise the added branch.
…precondition) (#3095) * docs(r3-v-l5): canvas — L5 corpus-policy substrate (gate #15 CONSUMER_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> * docs(r3-v-l5): fix Corpus Policy cardinality six → seven (cursor BLOCKING) * docs(r3-v-l5): fix INVARIANTS anchor P5 → P2/P3 on Q2-B3 disqualifier (cursor APPROVE_WITH_COMMENTS) * docs(r3-v-l5): correct ForAllTargets field summary — input_ref exists; ProgramOutputBind is a doc-comment, not a field (cursor BLOCKING) * docs(r3-v-l5): L5CorpusRowPolicy uses typed TestClaim edge, not String name key (briansrls BLOCKING P2) * docs(r3-v-l5): CoverageReason — add C4 with typed per-arm payload edges; drop coverage_description prose slot (briansrls BLOCKING P2) * docs(r3-v-l5): reconcile carrier (single L5CorpusRow in std.r3_l5_corpus) + 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> * docs(r3-v-l5): Q1 disqualify A1/A3 — EffectShape axis mismatch with locked 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> * docs(r3-v-l5): align §1 + §6 PR-2 landing surface with §5 (new r3_l5_corpus.dag module; no verification.dag substrate edit) (cursor BLOCKING) * docs(r3-v-l5): tighten §5 — import line lives in L5 fixture, not verification.dag (cursor BLOCKING) * docs(r3-v-l5): Q2 — split NumericPolicy into two independent axes (int + 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> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Auto-opened by session-dashboard for session
neat-raven-162.Pushing to
session/neat-raven-162advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan