diff --git a/DECISIONS.md b/DECISIONS.md index 29eab9e960..d3f49132e7 100644 --- a/DECISIONS.md +++ b/DECISIONS.md @@ -44,7 +44,7 @@ Entries give **Question; Blocks; Options; Inclination; Evidence; Depends; Status **Question:** Which concepts are native, protected-service objects, or kernel objects; what is the TCB and derived ABI? **Blocks:** implementation boundary. **Options:** minimal kernel, capability microkernel, broader runtime. **Inclination:** derive ABI from protected transitions, not operation count; archive the provisional sketch. **Evidence:** invariant-to-enforcer map; [ADR-011](decisions/ADR-011-boundary-and-abi.md) — **RESOLVED 2026-09-13: TRUSTED_RUNTIME selected** by the frozen v15 strict-subset selector over a G6-authorized production bundle (`_inner_validate` True; exposure sets 48/28/24; unique strict subset; evidence run `v15-evidence-003`, 518/518 jobs, zero halts; independent decision review seven-of-seven CONFIRMED). Known limitations recorded in ADR-011 as D-012 inputs (pin granularity; pre-freeze assembly gate). **Status:** `RESOLVED`. ### D-012 -**Question:** How are Promotion evidence, policy evolution, compiler/verifier trust, freshness, and replay protection governed? **Blocks:** recursive proof. **Options:** pinned policy, signed generations, diverse/reproducible builds. **Inclination:** evidence binds image/source/toolchain/tests/verifier/policy/parent/freshness. **Evidence:** [ADR-012](decisions/ADR-012-promotion-evidence-governance.md) — **RESOLVED 2026-09-14: governance contracts G-1..G-4 adopted** (pre-freeze assembly gate; whole-file identity retained with deferred protected-worker pilot under owner-ratified triggers T-1/T-2/T-3a, plus T-3b: compiler-verifier assurance and the malicious-candidate matrix reopen — and block promotion — at the recursive-proof milestone or any candidate self-build promotion; immutable policy generations with typed compatibility outcomes; final-point fresh one-use admission with global replay registry and atomic final-point transitions), evidenced by bounded executable models rev12 (65/65 tests incl. the metaclass-behavior probes over M-A intake and M-B time rejection, behavioral identifier/digest/outcome probes, exception-string probes, the no-copy-protocol intake probe, cyclic/over-deep value probes, immutable-expiry-ceiling probes, non-finite-float rejection probes, single-snapshot pair-intake probes, injective-encoding probes, snapshot-derived fork probe, reentrant temporal probes, parameterized cross-registry linearizability probes, no-mutation postconditions, reentrant recovery/expiry probes, closed-grammar and time-domain probes; machine-readable run result) and adversarial reviews (`reviewer:d012-packet-reviewer`, `reviewer:d012-resolution-reviewer`, `reviewer:d012-final-reviewer`, `reviewer:d012-rev5-verify2`, `reviewer:d012-final-reviewer2`, `reviewer:d012-rev7-verifier`, `reviewer:d012-rev8-verifier`, `reviewer:d012-rev9-verifier`, `reviewer:d012-rev10-verifier`, `reviewer:d012-rev11-verifier` — findings corrected through rev12). Owner P0: constrained orchestrator model, TCB pricing deferred, lean caps. Known deferred item: protected-worker pilot (triggers recorded). **Status:** `RESOLVED`. +**Question:** How are Promotion evidence, policy evolution, compiler/verifier trust, freshness, and replay protection governed? **Blocks:** recursive proof. **Options:** pinned policy, signed generations, diverse/reproducible builds. **Inclination:** evidence binds image/source/toolchain/tests/verifier/policy/parent/freshness. **Evidence:** [ADR-012](decisions/ADR-012-promotion-evidence-governance.md) — **RESOLVED 2026-09-14: governance contracts G-1..G-4 adopted** (pre-freeze assembly gate; whole-file identity retained with deferred protected-worker pilot under owner-ratified triggers T-1/T-2/T-3a, plus T-3b: compiler-verifier assurance and the malicious-candidate matrix reopen — and block promotion — at the recursive-proof milestone or any candidate self-build promotion; immutable policy generations with typed compatibility outcomes; final-point fresh one-use admission with global replay registry and atomic final-point transitions), evidenced by bounded executable models rev13 (66/66 tests incl. the standalone replay-registration safety probe, the metaclass-behavior probes over M-A intake and M-B time rejection, behavioral identifier/digest/outcome probes, exception-string probes, the no-copy-protocol intake probe, cyclic/over-deep value probes, immutable-expiry-ceiling probes, non-finite-float rejection probes, single-snapshot pair-intake probes, injective-encoding probes, snapshot-derived fork probe, reentrant temporal probes, parameterized cross-registry linearizability probes, no-mutation postconditions, reentrant recovery/expiry probes, closed-grammar and time-domain probes; machine-readable run result) and adversarial reviews (`reviewer:d012-packet-reviewer`, `reviewer:d012-resolution-reviewer`, `reviewer:d012-final-reviewer`, `reviewer:d012-rev5-verify2`, `reviewer:d012-final-reviewer2`, `reviewer:d012-rev7-verifier`, `reviewer:d012-rev8-verifier`, `reviewer:d012-rev9-verifier`, `reviewer:d012-rev10-verifier`, `reviewer:d012-rev11-verifier`, `reviewer:d012-rev12-verifier` — findings corrected through rev13). Owner P0: constrained orchestrator model, TCB pricing deferred, lean caps. Known deferred item: protected-worker pilot (triggers recorded). **Status:** `RESOLVED`. ### D-013 **Question:** Which native target substrate follows the hosted proof? **Blocks:** H1 only. **Options:** seL4/Microkit, other capability kernel, exokernel, custom. **Inclination:** none before semantic evidence. **Evidence:** TCB/port experiments. **Depends:** D-011. **Status:** `DEFERRED`. diff --git a/README.md b/README.md index 30be8ce2b0..7fcfb90494 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ This is a pre-prototype, not a working OS. The repository is intentionally rigor ## Current status -- **D-001 through D-012 are resolved.** D-001–D-010 adopted the representation-neutral algebras (identity, World-relative scope, authority, recovery, Effects/disclosure, Actor updates, World proposals, typed Budgets, Commitment lifecycles, typed Channels). **D-011 is RESOLVED (2026-09-13): TRUSTED_RUNTIME**, selected by the frozen v15 strict-subset selector over a G6-authorized production bundle — evidence run `v15-evidence-003` (518/518 jobs, zero halts), independent decision review 7/7 CONFIRMED; see [ADR-011](decisions/ADR-011-boundary-and-abi.md). **D-012 is RESOLVED (2026-09-14): promotion-evidence governance contracts G-1..G-4 adopted**, evidenced by bounded executable models rev12 (65/65 tests, machine-readable run result) and the adversarial review chain through `reviewer:d012-rev11-verifier`; see [ADR-012](decisions/ADR-012-promotion-evidence-governance.md). D-013–D-015 remain DEFERRED. +- **D-001 through D-012 are resolved.** D-001–D-010 adopted the representation-neutral algebras (identity, World-relative scope, authority, recovery, Effects/disclosure, Actor updates, World proposals, typed Budgets, Commitment lifecycles, typed Channels). **D-011 is RESOLVED (2026-09-13): TRUSTED_RUNTIME**, selected by the frozen v15 strict-subset selector over a G6-authorized production bundle — evidence run `v15-evidence-003` (518/518 jobs, zero halts), independent decision review 7/7 CONFIRMED; see [ADR-011](decisions/ADR-011-boundary-and-abi.md). **D-012 is RESOLVED (2026-09-14): promotion-evidence governance contracts G-1..G-4 adopted**, evidenced by bounded executable models rev13 (66/66 tests, machine-readable run result) and the adversarial review chain through `reviewer:d012-rev12-verifier`; see [ADR-012](decisions/ADR-012-promotion-evidence-governance.md). D-013–D-015 remain DEFERRED. - **Historical v14 implementation state (superseded by the D-011 resolution; retained):** the v14 experimental contract produced the focused TEST_ONLY slice (518/518 jobs, exact 2,086/496/22 engine/checker calls, retained under `decisions/d011_v14/development/production-readiness/`), complete fail-closed routing predictions for all 377,595 obligations, bounded catalogue membership, and the six v14 modules ([d011_protocol.py](decisions/d011_v14/d011_protocol.py), [d011_stage_c.py](decisions/d011_v14/d011_stage_c.py), [d011_runtime.py](decisions/d011_v14/d011_runtime.py), [d011_authority.py](decisions/d011_v14/d011_authority.py), [d011_producers.py](decisions/d011_v14/d011_producers.py), [d011_stage_b.py](decisions/d011_v14/d011_stage_b.py)) — all TEST_ONLY. The v13 lineage (including its fourteen-artifact freeze at F=`c17a6a2f4040729f4ea9d58b31aa04fd2651c9f7`) and v12 checkpoints are historically retained, not fallback qualification routes. - **Known D-012 deferred items:** the protected-worker pilot (owner-ratified triggers T-1/T-2/T-3a) and compiler-verifier assurance (T-3b) are deferred with pre-registered blocking triggers; the sixth H1 verification attack of the design-convergence record is UNRESOLVED-ENUMERATION and must be reconstructed before the pilot's go/no-go gate can run. diff --git a/decisions/ADR-012-promotion-evidence-governance.md b/decisions/ADR-012-promotion-evidence-governance.md index 85057d324a..671d9608a3 100644 --- a/decisions/ADR-012-promotion-evidence-governance.md +++ b/decisions/ADR-012-promotion-evidence-governance.md @@ -2,7 +2,7 @@ **Date:** 2026-09-14 **Status:** RESOLVED — governance contracts G-1..G-4 adopted; protected-worker pilot deferred with pre-registered triggers -**Evidence:** `AOS/decisions/D-012-PACKET.md` (preregistered rev3; live identity rev12), models `AOS/decisions/d012/m_policy_generations.py` (sha256 `ec1a2769…`, registry lock + type-exact injective tagged encoding via one controlled no-copy-protocol traversal with class-identity-only decisions and cycle/depth guards + non-finite-float rejection + snapshot-derived fork detection), `m_admission_replay.py` (sha256 `91a42b65…`, required M-B→M-A cross-registry lock-composition protocol, full post-callback revalidation, closed time domain with monotonic guard, immutable registered expiry ceiling, single-snapshot generation-pair intake, closed identifier/digest/outcome grammar with fixed rejection details and no exception-string formatting), tests `test_d012_models.py` (65/65 pass, machine-readable run result `d012-model-run-result.json`, head `247100ee8…`), design phase `D-012-DESIGN-CONVERGENCE.md` (sha256 `ae8bdc64…`, byte-identical retained body + corrected provenance footer; sixth H1 attack recorded UNRESOLVED-ENUMERATION), adversarial reviews `reviewer:d012-packet-reviewer` (6 HIGH, addressed in rev2), `reviewer:d012-resolution-reviewer` (7 HIGH, addressed in rev3), `reviewer:d012-final-reviewer` (N1/N2/N3/N4 + coverage, addressed in rev4/rev5), `reviewer:d012-rev5-verify2` (2 HIGH race windows + 2 MEDIUM, addressed in rev6), `reviewer:d012-final-reviewer2` (3 HIGH contract paths + 1 MEDIUM + 1 LOW, addressed in rev7), `reviewer:d012-rev7-verifier` (1 HIGH temporal + 1 MEDIUM provenance + 1 LOW metadata; 2 confirmed closed, addressed in rev8), `reviewer:d012-rev8-verifier` (2 HIGH fail-open paths + 1 MEDIUM snapshot intake + 1 LOW README status, addressed in rev9), `reviewer:d012-rev9-verifier` (1 HIGH copy-protocol intake defect + 1 LOW README onboarding link; expiry ceiling, non-finite grammar, pair snapshot, and status paragraph confirmed closed — addressed in rev10), `reviewer:d012-rev10-verifier` (1 HIGH metaclass whitelist bypass + confirmed closures of the copy-protocol removal and README onboarding link — addressed in rev11), `reviewer:d012-rev11-verifier` (M-A metaclass fix confirmed CLOSED; 2 HIGH + 1 MEDIUM uncovered M-B public-input defects — behavioral durable keys/digests, metaclass time-rejection dispatch, exception-string formatting — addressed in rev12). +**Evidence:** `AOS/decisions/D-012-PACKET.md` (preregistered rev3; live identity rev13), models `AOS/decisions/d012/m_policy_generations.py` (sha256 `ec1a2769…`, registry lock + type-exact injective tagged encoding via one controlled no-copy-protocol traversal with class-identity-only decisions and cycle/depth guards + non-finite-float rejection + snapshot-derived fork detection), `m_admission_replay.py` (sha256 `706f070f…`, required M-B→M-A cross-registry lock-composition protocol, full post-callback revalidation, closed time domain with monotonic guard, immutable registered expiry ceiling, single-snapshot generation-pair intake, closed identifier/digest/outcome grammar with fixed rejection details and no exception-string formatting, independently safe replay registration bound to a live ALLOCATED attempt), tests `test_d012_models.py` (66/66 pass, machine-readable run result `d012-model-run-result.json`, head `19ddfc878…`), design phase `D-012-DESIGN-CONVERGENCE.md` (sha256 `ae8bdc64…`, byte-identical retained body + corrected provenance footer; sixth H1 attack recorded UNRESOLVED-ENUMERATION), adversarial reviews `reviewer:d012-packet-reviewer` (6 HIGH, addressed in rev2), `reviewer:d012-resolution-reviewer` (7 HIGH, addressed in rev3), `reviewer:d012-final-reviewer` (N1/N2/N3/N4 + coverage, addressed in rev4/rev5), `reviewer:d012-rev5-verify2` (2 HIGH race windows + 2 MEDIUM, addressed in rev6), `reviewer:d012-final-reviewer2` (3 HIGH contract paths + 1 MEDIUM + 1 LOW, addressed in rev7), `reviewer:d012-rev7-verifier` (1 HIGH temporal + 1 MEDIUM provenance + 1 LOW metadata; 2 confirmed closed, addressed in rev8), `reviewer:d012-rev8-verifier` (2 HIGH fail-open paths + 1 MEDIUM snapshot intake + 1 LOW README status, addressed in rev9), `reviewer:d012-rev9-verifier` (1 HIGH copy-protocol intake defect + 1 LOW README onboarding link; expiry ceiling, non-finite grammar, pair snapshot, and status paragraph confirmed closed — addressed in rev10), `reviewer:d012-rev10-verifier` (1 HIGH metaclass whitelist bypass + confirmed closures of the copy-protocol removal and README onboarding link — addressed in rev11), `reviewer:d012-rev11-verifier` (M-A metaclass fix confirmed CLOSED; 2 HIGH + 1 MEDIUM uncovered M-B public-input defects — behavioral durable keys/digests, metaclass time-rejection dispatch, exception-string formatting — addressed in rev12), `reviewer:d012-rev12-verifier` (F2/F3 confirmed CLOSED; F1 completed at rev13 — the public register_binding could forge a global replay reservation with unvalidated fields; now validated and bound to a live ALLOCATED attempt). **Depends:** ADR-011 (TRUSTED_RUNTIME), D-004, D-005. **Does not start D-013+.** ## Decision diff --git a/decisions/D-012-PACKET.md b/decisions/D-012-PACKET.md index 07654c2d14..b22dafbd2f 100644 --- a/decisions/D-012-PACKET.md +++ b/decisions/D-012-PACKET.md @@ -1,11 +1,11 @@ # D-012 PACKET — Promotion evidence, policy evolution, and admission governance -**Status:** RESOLVED (2026-09-14, owner P0 sitting; ADR-012). Preregistration remains rev3 (immutable, pre-resolution); the live evidence identity below is correction generation **rev12** (post-resolution adversarial review chain through `reviewer:d012-rev11-verifier`). +**Status:** RESOLVED (2026-09-14, owner P0 sitting; ADR-012). Preregistration remains rev3 (immutable, pre-resolution); the live evidence identity below is correction generation **rev13** (post-resolution adversarial review chain through `reviewer:d012-rev12-verifier`). **Date:** 2026-09-14 (rev3 after resolution review `reviewer:d012-resolution-reviewer`; corrections: evaluator identity bound into generations with `INVALIDATE` on change; precedence order preregistered — FAIL_CLOSED > REJECT (revocation/rollback/fork) > INVALIDATE (divergence/evaluator) > RE_EVALUATE (body); M-B currentness REQUIRED and composed with the G-3 registry at the final point; post-dispatch facts retained regardless of later revocation/expiry (D-004 retention) with a durable post-dispatch crash cut; one live attempt per authority with ABANDONED tombstoning; T-3 split into T-3a (identity pilot, owner request) / T-3b (compiler-verifier assurance + malicious-candidate matrix: recursive-proof milestone or candidate self-build promotion)) **Risk tier:** Full (register lines 11–14: Promotion and TCB concerns are Full by default) **Scope:** Lean governance resolution (owner-selected Option A, 2026-09-14): D-012 is a governance-contract decision resolved by preregistered contract + bounded executable models + adversarial review + one owner decision sitting. No production corpus run is required or permitted for resolution; the D-011 evidence-run template does not apply. **Option set (per procedure):** (A, recommended) lean governance contracts per this packet; (status quo) retain whole-file pinning + D-011 sequencing without a D-012 contract — valid, keeps the cascade cost; (C) full three-slice candidate with protected worker — rejected for this cycle per adversarial review (mini-D-011 risk). Owner selects at P0. -**Frozen candidate identity:** *preregistered rev3 (historical, pre-resolution):* tests `test_d012_models.py` sha256 `24943f082538f827410d77ee97ad987e1caf0d9d9ae05c5289a78a29049a33f3`; *live correction generation rev12 (governing):* `m_policy_generations.py` sha256 `ec1a2769b1a71caf3e7f9ec5b42dc73d82efa0ce506437e1d382d1a13df9feba` (grammar rev4 + registry lock + type-exact injective tagged encoding via one controlled no-copy-protocol traversal with class-identity-only decisions, cycle/depth guards, and fixed rejection details + non-finite-float rejection + snapshot-derived fork detection), `m_admission_replay.py` sha256 `91a42b65d04c683d2cd7a82c45baf0802a6ec867048dc5b2835222da4989935f` (grammar rev4 + required M-B→M-A lock-composition protocol + full post-callback revalidation + closed time domain with monotonic guard + immutable registered expiry ceiling + single-snapshot generation-pair intake + closed identifier/digest/outcome grammar with fixed rejection details and no exception-string formatting), tests `test_d012_models.py` sha256 `595332755312fcc9c95425eb51e6aef273350ac33fa709d35299ccbcadd320aa`; design-phase record `D-012-DESIGN-CONVERGENCE.md` sha256 `ae8bdc6465ec883fece6a7498a7c39a29acc9b0ba719966401eefde6e900da61` (byte-identical retained body + corrected provenance footer; its sixth H1 attack is recorded UNRESOLVED-ENUMERATION); machine-readable run result `d012-model-run-result.json` (65 tests, 0 failures, 0 errors, head `247100ee8…` — rev12, including the metaclass-behavior probes (M-A intake and M-B time rejection), behavioral identifier/digest/outcome probes, exception-string probes, the no-copy-protocol intake probe, cyclic/over-deep value probes, immutable-expiry-ceiling probes, non-finite-float rejection probes, single-snapshot pair-intake probes, injective-encoding probes, snapshot-derived fork probe, reentrant temporal probes, parameterized cross-registry linearizability probes, no-mutation postconditions, reentrant recovery/expiry cases, and closed-grammar/time-domain probes). **P0 ordering (deviation resolved):** the models are evaluated under the **CONSTRAINED posture per P0-1** (owner-selected), with hostile same-process mutation attacks explicitly recorded as out-of-scope assumptions (TA-1 residual) — and the deferred pilot is the mechanism by which that assumption would be revisited (T-3a). The resolution (ADR-012 amendment) requires the owner-ratified T-3a/T-3b split (ratified 2026-09-14, commit `2619b3759`). +**Frozen candidate identity:** *preregistered rev3 (historical, pre-resolution):* tests `test_d012_models.py` sha256 `24943f082538f827410d77ee97ad987e1caf0d9d9ae05c5289a78a29049a33f3`; *live correction generation rev13 (governing):* `m_policy_generations.py` sha256 `ec1a2769b1a71caf3e7f9ec5b42dc73d82efa0ce506437e1d382d1a13df9feba` (grammar rev4 + registry lock + type-exact injective tagged encoding via one controlled no-copy-protocol traversal with class-identity-only decisions, cycle/depth guards, and fixed rejection details + non-finite-float rejection + snapshot-derived fork detection), `m_admission_replay.py` sha256 `706f070fd2d4b2a1c8f5d58990fbe419dc83b0184747aa63a72800d1fb705704` (grammar rev4 + required M-B→M-A lock-composition protocol + full post-callback revalidation + closed time domain with monotonic guard + immutable registered expiry ceiling + single-snapshot generation-pair intake + closed identifier/digest/outcome grammar with fixed rejection details and no exception-string formatting + independently safe replay registration bound to a live ALLOCATED attempt), tests `test_d012_models.py` sha256 `f90e0d890a6e40c909c6e09c5d41279b772ab319594194470ee76ea79a1cf795`; design-phase record `D-012-DESIGN-CONVERGENCE.md` sha256 `ae8bdc6465ec883fece6a7498a7c39a29acc9b0ba719966401eefde6e900da61` (byte-identical retained body + corrected provenance footer; its sixth H1 attack is recorded UNRESOLVED-ENUMERATION); machine-readable run result `d012-model-run-result.json` (66 tests, 0 failures, 0 errors, head `19ddfc878…` — rev13, including the standalone replay-registration safety probe, the metaclass-behavior probes (M-A intake and M-B time rejection), behavioral identifier/digest/outcome probes, exception-string probes, the no-copy-protocol intake probe, cyclic/over-deep value probes, immutable-expiry-ceiling probes, non-finite-float rejection probes, single-snapshot pair-intake probes, injective-encoding probes, snapshot-derived fork probe, reentrant temporal probes, parameterized cross-registry linearizability probes, no-mutation postconditions, reentrant recovery/expiry cases, and closed-grammar/time-domain probes). **P0 ordering (deviation resolved):** the models are evaluated under the **CONSTRAINED posture per P0-1** (owner-selected), with hostile same-process mutation attacks explicitly recorded as out-of-scope assumptions (TA-1 residual) — and the deferred pilot is the mechanism by which that assumption would be revisited (T-3a). The resolution (ADR-012 amendment) requires the owner-ratified T-3a/T-3b split (ratified 2026-09-14, commit `2619b3759`). ## Trusted-assumption register (per adversarial review requirement)