Repository navigation
[P2] Kernel-0: finish accepted-revision validation and decide the rung-2 boundary #328
Description
[P2] Kernel-0: finish accepted-revision validation and decide the rung-2 boundary
Scope and reviewed baseline
Remaining work from #294 (R16). Review date: 29 September 2026.
Branch: wavect/v070, PR #314, source commit 1ae35afe83f62f405b979f57ac90772cfec9daca.
Classification: Integrated validation and explicit promotion decision.
This ticket replaces only the unresolved portion of its predecessor. Migration of the old ticket is not a claim that its whole original scope was completed. A missing hosted CI receipt is not a blocker when the required implementation and substantive local execution are complete.
Already delivered: do not rebuild
The evidence map, ordinary checked owned-Bytes handoff, source/term/target authentication, actual last-owner settlement, hostile fallback/re-entry and renderer caching are implemented. Retained local evidence includes 854 reference comparisons, 2,562 backend comparisons and the 13-row wrapper target checks.
Remaining gap
The pinned document still requires accepted-revision validation and an explicit reviewed rung decision. The existing wrapper transfers Rust-assembled scalar output; it is not an owned Kernel-0 renderer or an ownership theorem.
Work to finish
- Choose the exact revision for this bounded Kernel-0 profile and run the remaining required formal/renderer/authority/bootstrap/differential gates together or reconcile their exact unchanged subjects. Do not repeat completed proof development merely to get a hosted badge.
- Have the responsible reviewer decide whether the stated rung-2 criteria are met, remain unmet, or are intentionally not promoted. Record any concrete technical blocker rather than treating absent hosting as one.
- Keep Rust formatter authority, ordinary wrapper ownership and any Kernel-0 proof claims distinct. Update the rung/evidence status consistently without implying whole-compiler self-hosting.
Acceptance
- The required accepted-profile local gates are complete and evidence is correctly bound to their actual revisions.
- An explicit reviewed promotion/non-promotion outcome resolves the ticket; any remaining technical work is named narrowly. No hosted receipt alone blocks closure.
- No whole-compiler formal verification or new ownership theorem is claimed from wrapper tests.
Boundaries
Use the existing mechanisms and frozen profiles. Do not silently weaken resource, source-authority, ownership, oracle or refusal requirements. This ticket does not authorize paid model/training calls, credentials, external deployment, signing, publication or a support-policy change. Obtain those authorities only where the remaining work actually needs them. Do not reopen excluded deferred work.
Evidence and entry points
- Implemented owned handoff, evidence map and still-open rung decision
- Cached differential corpus completion
Review basis: source/document inspection plus retained repository/issue test reports, not a new execution of the Semaprax test suite. Evidence remains bound to the revision and host on which it was actually produced. Confidence: High.
Activity
wsdt commentedon Sep 30, 2026
Progress on wavect/v070 at 8eefe32: added a Kernel-0 accepted-revision validation ledger with explicit pending receipts for Lean proof, renderer/authority, bootstrap, scalar target/recovery, differential, owned handoff and full baseline; it records the exact revision and reviewer decision needed before a rung outcome. This is planning/evidence structure only. The earlier kernel gate attempt was interrupted, none of the seven receipts has passed on this head, and no rung-2 promotion is claimed. #328 remains open.
wsdt commentedon Sep 30, 2026
Progress on pushed wavect/v080 head 539dbb4: a read-only accepted-revision record validator now checks the seven fixed receipt rows, exact commit identities, canonical JSON, declared source inventory drift, and regular tracked-file modes. Its focused Python self-test passed 4/4, including drift, missing receipt, and symlink refusal. No accepted candidate record, completed receipt inventory, reviewer decision, or rung-2 promotion is claimed; #328 remains open.
wsdt commentedon Sep 30, 2026
Read-only v080 audit: the pinned Kernel-0 accepted-revision record still selects no candidate and leaves all seven required receipts pending; its result is validation-incomplete. Historical 854 reference, 2,562 backend and 13 wrapper rows remain bound to prior subjects unless their exact inventories are reconciled. The concrete rung-2 non-promotion rationale is that five lanes still produce scalar bytes while Rust assembles/owns the token; the wrapper is checked own Bytes -> Bytes, not an owned Kernel-0 renderer or ownership theorem. This rationale can be recorded, but the accepted-revision gate and distinct reviewer outcome still need the seven receipts. No gates ran in this audit, and missing hosting alone is not the blocker.
wsdt commentedon Oct 2, 2026
Completed the bounded accepted-revision decision on wavect/v080 at ce1d73c. Candidate f99c76d has exact-head Lean proof gate PASS, 124/124 required-target Kernel-0 tests, and 10/10 owned-handoff tests (0 failures/ignored); raw logs, commands, tool versions, coverage map and hashes are committed under docs/evidence/kernel-zero-f99c76dc2/. The canonical seven-row record validates with six executed receipts and an explicit user-authorized waiver of the local full profile. Reviewer decision is rung-1-retained: Rust still assembles/owns scalar output and retains formatter authority; the ordinary owned-Bytes wrapper is not an owned Kernel-0 renderer or ownership theorem. No rung-2, whole-compiler proof, or hosted/full-profile pass is claimed. The full profile remains delegated to hosted CI per the user instruction.