You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
docs(P-022): remove duplicated cp4 measurements from status surfaces
This branch's whole claim is that a checkpoint's measured numbers live in one
generated place and the status surfaces link to it. The cp4 differential was
still typed on three of those surfaces — the branch violating its own contract
in the same commits that state it.
Removed, current cp4 only:
* P-022 checkpoint table, row 4 — the status cell no longer reads "0/0/0 over
the measured set", and the evidence text no longer reads "0/0/0 over the
replayed set". The claim kept is the one that is not a measurement: parity at
the checkpoint-4 surface, the replay asserting equality with every divergence
collected and any one of them a red build, and the exclusion ledger named.
* proposals index, the current cp4 clause — "the replayed set 0/0/0" becomes
"the replayed set asserted equal on the cp4 members"; the generated census is
still linked.
* docs/notes/p022-bridge-verdict-checkpoint4.md — "a green replay reads
0 / 0 / 0 / 0 / 0 by construction" was a hand copy of a sentence the renderer
already emits into the census fragment. The comparison surface is still
described; the result is not.
Historical numbers are untouched: cp1's three censuses (including its own
0/0/0 and the taxonomy defect underneath it), cp2, cp3 and the mutation-round
narratives are records of past measurements, not restatements of the current
one, and this rule is about the second.
Nothing generated, no campaign definition or result, no golden and no
production code is touched — docs only. The recorded campaign's source_commit
a529193 stays an ancestor of this head, so the provenance gate accepts it
without a re-run. ruff, mypy and tests/run_tests.py are green, with the
fragments still in sync.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0167aQj9xTAF5r7K1nTCtDQ5
Copy file name to clipboardExpand all lines: docs/proposals/P-022-rust-core-migration.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -59,7 +59,7 @@ was #258 alone, which is satisfied. Per the checkpoints #259 itself defines:
59
59
| 1 — typed OwnIR validation | **complete — no known strict-door divergence** | Three censuses. The first froze 77 controls and read 0/0/0 — then review found seven divergences the ledger could not express, because the same author wrote the ledger and the port and one gap in reading BR-D1 produced a matching gap in each (`_svc()` always supplied `lifetime`, so no control could omit it). The second is derived from `load()` and `obligations.py` line by line: **193 controls**, opening a further **58** permissive documents and **9** category mismatches. Closing them was architectural — the strict door is a sequential validator over the raw document (`own-ir/src/strict.rs`) reproducing BR-D1's interleaving of shape and semantics *per section, in declaration order*; `serde` is the typed constructor, and a document it rejects after validation is reported as a hole in the validator and asserted against. The obligation **acceptance grammar** is ported (`own-ir/src/protocol.rs`); protocol *analysis* is not, and is not part of what the door accepts. The third census admitted the two families the second had measured and deliberately excluded — source coordinates beyond signed 64 bits, and nesting depth — once #326 closed them Python-first. That opened 7 permissive documents and 8 more category mismatches, and the classification defect underneath them was the ledger reading its category off the reference's *diagnostic* rather than off the mechanism: `_check_column` raises one message for a bool, a string, a float, an out-of-range integer and a zero alike, so a bool column was filed as a 1-based-contract violation. Taxonomy is **seven** categories on **two axes** — `Shape` is now "no representable primitive or container form", `Location` is "a representable coordinate violating its domain rule", and `WellFormedness` covers records that are typed and vocabulary-legal and still cannot mean anything. **216 controls, matrix 35/181, 0/0/0**, no control escaping into serde; 48 mutations across the three rounds, all caught. #294 OD-2 remains a separate tolerant-door concern |
| 3 — interprocedural MOS |**complete for the stage-1 domain**|`dump_summaries()` byte-identical to `python -m ownlang summaries` across **35**`*.summaries.json` goldens. Container-valued metadata is **outside** the declared scalar-metadata parity domain — a separate #294-class door decision, not a silent gap |
62
-
| 4 — analysis wiring | **complete at the checkpoint-4 surface — 0/0/0 over the measured set, with the unmeasured set named** | `own_bridge::check_facts` is BR-V1 verbatim: the Layer 2 document rebuilt as the core AST (`ast.rs` — composing the cp2 evidence rather than lowering twice), `own_analysis::check_module` (ownership, lifetime, buffer policy), the `services[]`/`effects[]` blocks through the `own-analysis` DI and effect finders (BR-P1/P2), the OWN050/051/052 side paths, ERROR-only mapping through the verdict's **`subject`** to a fact handle with the reference's map-or-raise refusal (BR-V2/V3), the analysis-selected anchors preserved (DI004 call site, DI005 store site, OWN025 view site — BR-V5), tiering and suppression (BR-V6), dedup and the stable `(file, line, column, code)` sort (BR-V7/V8). Landing it needed one core change: `own-analysis` now stamps `subject` exactly where `analysis.py`/`lifetimes.py` pass `subject=sym.origin` (pinned through `check_module`). **Layer 3 fixture family built** (`ownlang/verdicts.py`, `tests/fixtures/verdicts/`, `tests/test_verdict_fixtures.py`; Rust replay `own-bridge/tests/verdicts.rs`): the goldens are Python's complete truth — the swept `ownir`/`lowered`/`summaries` corpora plus the synthetic controls — carrying every `Finding` member; the cp4 replay compares identity, anchor, kind and tiering (all members but `message`/`related`/`flow`) and reads **0/0/0 over the replayed set**. The rest is a **named exclusion ledger the replay executes**, not a silent gap — the documents declaring obligation protocols (the OBL analysis is not ported; the bridge *refuses* them rather than return a list with a family missing), the controls for the one representability boundary (a coordinate outside the core's `u32` line domain, which the strict door admits per `spec/OwnIR.md` §4.2 — refused, never clamped; the contract decision is one #259 still owes, and the stated direction is the Python-first tightening recorded on the cp5 row), and the #294 OD-1 controls where the reference's tolerant-door skip/ignore is unreachable through the typed Rust constructor. One declared comparison boundary on refusals: the map-or-raise text is compared up to its `message=` member, because the core's messages are still titles. **The measured census** (goldens by origin, exclusions by expectation, the replayed set with its refusals and findings) **and the recorded mutation campaign live only in the generated fragments** [`docs/generated/p022-cp4-census.md`](../generated/p022-cp4-census.md) and [`docs/generated/p022-cp4-mutations.md`](../generated/p022-cp4-mutations.md), rendered from the ledger and the campaign evidence by `scripts/render_checkpoint_status.py` and held in sync by the test gate — no count is typed in this table |
62
+
| 4 — analysis wiring | **complete at the checkpoint-4 surface — parity over the measured set, with the unmeasured set named** | `own_bridge::check_facts` is BR-V1 verbatim: the Layer 2 document rebuilt as the core AST (`ast.rs` — composing the cp2 evidence rather than lowering twice), `own_analysis::check_module` (ownership, lifetime, buffer policy), the `services[]`/`effects[]` blocks through the `own-analysis` DI and effect finders (BR-P1/P2), the OWN050/051/052 side paths, ERROR-only mapping through the verdict's **`subject`** to a fact handle with the reference's map-or-raise refusal (BR-V2/V3), the analysis-selected anchors preserved (DI004 call site, DI005 store site, OWN025 view site — BR-V5), tiering and suppression (BR-V6), dedup and the stable `(file, line, column, code)` sort (BR-V7/V8). Landing it needed one core change: `own-analysis` now stamps `subject` exactly where `analysis.py`/`lifetimes.py` pass `subject=sym.origin` (pinned through `check_module`). **Layer 3 fixture family built** (`ownlang/verdicts.py`, `tests/fixtures/verdicts/`, `tests/test_verdict_fixtures.py`; Rust replay `own-bridge/tests/verdicts.rs`): the goldens are Python's complete truth — the swept `ownir`/`lowered`/`summaries` corpora plus the synthetic controls — carrying every `Finding` member; the cp4 replay compares identity, anchor, kind and tiering (all members but `message`/`related`/`flow`) and **asserts** equality over the replayed set — every divergence collected without fail-fast, any one of them a red build, so the differential is a property of a green replay rather than a number to copy here. The rest is a **named exclusion ledger the replay executes**, not a silent gap — the documents declaring obligation protocols (the OBL analysis is not ported; the bridge *refuses* them rather than return a list with a family missing), the controls for the one representability boundary (a coordinate outside the core's `u32` line domain, which the strict door admits per `spec/OwnIR.md` §4.2 — refused, never clamped; the contract decision is one #259 still owes, and the stated direction is the Python-first tightening recorded on the cp5 row), and the #294 OD-1 controls where the reference's tolerant-door skip/ignore is unreachable through the typed Rust constructor. One declared comparison boundary on refusals: the map-or-raise text is compared up to its `message=` member, because the core's messages are still titles. **The measured census** (goldens by origin, exclusions by expectation, the replayed set with its refusals and findings) **and the recorded mutation campaign live only in the generated fragments** [`docs/generated/p022-cp4-census.md`](../generated/p022-cp4-census.md) and [`docs/generated/p022-cp4-mutations.md`](../generated/p022-cp4-mutations.md), rendered from the ledger and the campaign evidence by `scripts/render_checkpoint_status.py` and held in sync by the test gate — no count is typed in this table |
63
63
| 4b — protocol analysis (OBL001–005) |**not started — recorded as its own checkpoint, not folded into cp5**| A gap in #259's checkpoint list: none of cp1–cp5 names the obligation-protocol analysis, while #259's final acceptance ("the full #258 family inventory") requires the protocol rows (BR-P3). `ownlang/obligations.py` is a path-sensitive analysis of its own — lattice, walker, matching — so it is a checkpoint of its own rather than a fourth job for cp5 (whose scope is messages, evidence and rendering). Its *normative* place: before #259's final acceptance; it does **not** block cp5. Until it lands the bridge **refuses** a protocol-bearing document (two reference documents in the verdict ledger) rather than return a verdict list with a family missing |
64
64
| 5 — full fact-to-verdict parity |**unblocked, not done**| the goldens already carry `message`, `related` and `flow`; cp5 is the message matrix (BR-V4), the evidence slices, the rendered surfaces (`render*`, `build_sarif` on the bridge path — BR-V9) and tightening the cp4 replay to full equality on the **same frozen goldens** — no regeneration beside the implementation. The `u32` coordinate boundary stays excluded until its contract decision lands; the owner's stated direction is a **Python-first tightening** of the coordinate domain (a negative source line is meaningless), as its own contract change with parity evidence — never "Rust is `u32`, so the reference is wrong" |
| [P-022](P-022-rust-core-migration.md) | Rust core migration: crate DAG, patterns, prior art, differential oracle (Python = golden) | in execution — steps 0–4 built (#214/#249); step 5a done (full diagnostic contract, #255 via #319/#320/#321); step 5b SARIF done (#256; `.ownreport.json` struck — a buffer report needing the AST, not a diagnostics surface); step 6a done (`spec/Bridge.md`, #258); step 6b underway (`own-lowered`/`own-bridge`, #259: lowering and MOS parity landed; strict-door validation complete at 216 controls with no known divergence — the first 0/0/0 proved to be the ledger agreeing with its own author, and the second omitted two families that a Python-first defensive-limit change (#326) had to close before the third could measure them; analysis wiring complete at the checkpoint-4 surface — `check_facts` through the real analyses, Layer 3 goldens built, the replayed set 0/0/0 with an executable exclusion ledger naming the protocol boundary, the `u32` coordinate boundary and the OD-1 door controls (the census is generated: `docs/generated/p022-cp4-census.md`); full fact-to-verdict parity (cp5: messages, evidence, rendered surfaces) open); Python authoritative until cutover |
44
+
| [P-022](P-022-rust-core-migration.md) | Rust core migration: crate DAG, patterns, prior art, differential oracle (Python = golden) | in execution — steps 0–4 built (#214/#249); step 5a done (full diagnostic contract, #255 via #319/#320/#321); step 5b SARIF done (#256; `.ownreport.json` struck — a buffer report needing the AST, not a diagnostics surface); step 6a done (`spec/Bridge.md`, #258); step 6b underway (`own-lowered`/`own-bridge`, #259: lowering and MOS parity landed; strict-door validation complete at 216 controls with no known divergence — the first 0/0/0 proved to be the ledger agreeing with its own author, and the second omitted two families that a Python-first defensive-limit change (#326) had to close before the third could measure them; analysis wiring complete at the checkpoint-4 surface — `check_facts` through the real analyses, Layer 3 goldens built, the replayed set asserted equal on the cp4 members with an executable exclusion ledger naming the protocol boundary, the `u32` coordinate boundary and the OD-1 door controls (the census is generated: `docs/generated/p022-cp4-census.md`); full fact-to-verdict parity (cp5: messages, evidence, rendered surfaces) open); Python authoritative until cutover |
0 commit comments