Repository navigation
[codex] docs(r3): audit gate 16 fixed-point preconditions #3028
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
8 commits
Select commit
Hold shift + click to select a range
fbd9583
docs(r3): audit gate 16 fixed-point preconditions
briansrls c85d5bd
Merge remote-tracking branch 'origin/main' into session/smart-ram-625
briansrls 2770128
Merge remote-tracking branch 'origin/main' into session/smart-ram-625
briansrls 58bbd6e
Merge remote-tracking branch 'origin/main' into session/smart-ram-625
briansrls 1af5a9b
Merge remote-tracking branch 'origin/main' into session/smart-ram-625
briansrls eeec7bf
Merge remote-tracking branch 'origin/main' into session/smart-ram-625
briansrls dcf0caa
Merge remote-tracking branch 'origin/main' into session/smart-ram-625
briansrls 33c7ce0
Merge remote-tracking branch 'origin/main' into session/smart-ram-625
briansrls File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
45 changes: 45 additions & 0 deletions
45
docs/audit/r3-gap3-fixed-point-precondition-coordination-2026-05-13.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,45 @@ | ||
| # R3 Gap 3 fixed-point precondition coordination (2026-05-13) | ||
|
|
||
| **Status:** coordination audit; no gate status changes. | ||
|
|
||
| **Scope:** `docs/r3-actual-close-plan.md` Gap 3 / §1.8 gate #16 (`pb_self_compile_fixed_point`) R3 strong-form sequencing. This note cross-checks the four joint preconditions named by `docs/briefs/r3-pb-t-fixedpoint-worker.md` against local source-of-truth docs at HEAD and records the next manager-facing actions. | ||
|
|
||
| ## Verdict | ||
|
|
||
| Gate #16 remains **not dispatch-eligible** for the R3 strong suite. The P0 pins landed, but none of the four joint preconditions can be read as green from the local authorities: | ||
|
|
||
| | Precondition | Current read at HEAD | Source-of-truth pointer | Coordination action | | ||
| |---|---|---|---| | ||
| | R2-Evaluator landed and stable | **Blocked.** The R2 closure ledger still lists all five Evaluator sub-lanes as `in-flight` or `not-started`; later R3 evaluator PR sweeps show partial progress but do not replace the ledger. | `docs/r2-closure-ledger.md` lines 250-263; `docs/r3-actual-close-plan.md` Gap 3 | Director/PM needs an Evaluator lane disposition before any ledger update: respawn a dedicated R3 Evaluator Mgr, fold explicit sub-lanes into existing managers, or run Director-direct ad hoc dispatch. After that, refresh the five ledger cells from HEAD evidence. | | ||
| | R2-Grounding Rust + Python closed | **Blocked / unproven.** LanguageSpec remains in-flight in the R2 closure ledger, and Shape-A / Python+Go readiness is still cited as a blocker by L5/Evaluator readiness docs. | `docs/r2-closure-ledger.md` row `T-Ground-LanguageSpec`; `docs/briefs/r2-evaluator-closure-residuals.md`; `docs/r3-program-plan.md` rows #15/#16 | Grounding owner should produce a Rust+Python closure receipt that is ledger-consumable by T-FixedPoint. Do not let T-FixedPoint infer target coverage from scattered target-specific PRs. | | ||
| | T-LP / SG-0 closed | **Blocked.** T-LensProducer-Retirement remains not-started in the R2 ledger. Live SG-0 expected-list snapshot is nonzero: non-test 53, test 121, fragments 2. | `docs/r2-closure-ledger.md` PB continuation row; `src/v3/compiler/tests/integration/sg0_census_test.rs`; `docs/r3-program-plan.md` rows #5-#8 | PB/Debt-Paydown sequencing remains upstream of fixed point. Gate #16 must not author `pb_self_compile_fixed_point_strong` while #5-#8 are open. | | ||
| | Row-B materialization landed | **Blocked.** The rule is designed, but no dispatch-time frozen Row-B target set exists because the ledger read cannot yet happen. The current `FixedPointConverges` runner path still only supports `default_fixed_point_source` / `pipeline_stage_snapshots`, so non-Rust Row-B verification also needs the named extension from the fixed-point brief. | `docs/briefs/r3-pb-t-fixedpoint-worker.md` §§Acceptance / Single grounding gate; `src/v3/compiler/src/test_runner.rs` `FixedPointConverges` payload checks | Once the first three preconditions are green, PB should freeze Row-B rows from the single ledger read and extend `self_host_fixed_point` or a sibling step for per-target emission byte-stability before claiming the suite is executable. | | ||
|
|
||
| ## Evaluator sub-lane ledger refresh target | ||
|
|
||
| Gap 3's dominant hidden blocker is the Evaluator precondition. The close predicate for this precondition is not a new §1.8 row set; it is the existing R2 closure ledger cells turning green at HEAD: | ||
|
|
||
| | R2 closure-ledger sub-lane | Current ledger status | Required close state for Gap 3 | | ||
| |---|---|---| | ||
| | `runtime_value_model_structural` | `in-flight` | `green` with HEAD evidence | | ||
| | `body_evaluator_structural` | `not-started` | `green` with executable body-evaluator evidence | | ||
| | `lens_application_complete_reflection` | `in-flight` | `green` with complete reflection + lens fold evidence | | ||
| | `witness_construction_structural` | `not-started` | `green` with runtime witness materialization evidence | | ||
| | `cross_target_equivalence_harness_structural` | `not-started` | `green` with harness primitive evidence; L5 corpus remains its own R3 consumer | | ||
|
|
||
| Partial R3-era work should be mapped into these exact cells, not into parallel status labels. The current branch has audit trails (`docs/audit/r3-evaluator-pr-1275-1500-debt-sweep.md`, `docs/audit/r3-evaluator-pr-1500-1803-debt-sweep.md`, `docs/audit/r3-evaluator-pr-1804-onward-debt-sweep.md`) that help populate evidence, but they are not themselves the closure ledger. | ||
|
|
||
| ## Sequencing rule for gate #16 | ||
|
|
||
| 1. Keep `src/v3/std/verification.dag` in P0-only state; no `pb_self_compile_fixed_point_strong` suite until the single dispatch ledger read is green. | ||
| 2. Resolve Evaluator ownership first, because it gates T-LP, Row-B execution, and most downstream verification consumers. | ||
| 3. Refresh the R2 closure ledger's Evaluator cells from HEAD before T-FixedPoint consumes them. | ||
| 4. Obtain a Grounding Rust+Python closure receipt from the Grounding owner; do not substitute L5 or Shape-A planning prose. | ||
| 5. Let PB/Debt-Paydown close T-LP/SG-0 (#5-#8) before PB starts the P3 fixed-point worker. | ||
| 6. At P3 dispatch, freeze Row-B targets from the same ledger read that gates dispatch, then materialize Row A + Row B + Row C in the strong suite and extend the fixed-point verifier for non-Rust Row-B byte-stability. | ||
|
|
||
| ## Message to parent / Director | ||
|
|
||
| Use this as the coordination payload if the dashboard is reachable: | ||
|
|
||
| > Gap 3 gate #16 remains sequencing-held. Local audit confirms all four joint preconditions are still non-green: Evaluator ledger has five open cells, Grounding Rust+Python has no ledger-consumable close receipt, T-LP/SG-0 is open with SG-0 snapshot 53 non-test / 121 test / 2 fragments, and Row-B cannot materialize until the dispatch ledger read. Recommended next action is Director/PM decision on Evaluator lane ownership, then ledger refresh against the five existing R2 closure cells; do not dispatch PB P3 or author `pb_self_compile_fixed_point_strong` yet. | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
BLOCKING: The Director payload asks for an Evaluator lane ownership decision even though
docs/r3-actual-close-plan.md§6 already ratifies option (a), so the new audit contradicts the single authoritative closure plan’s current manager-facing action.