From 016d64b7c3479d3facab024a763acce0eed1e57a Mon Sep 17 00:00:00 2001 From: "david.yapfest.club" Date: Tue, 15 Sep 2026 01:08:18 -0400 Subject: [PATCH] =?UTF-8?q?D-012=20records=20reconciled=20to=20the=20coher?= =?UTF-8?q?ent=20rev7=20tuple:=20packet,=20ADR-012,=20and=20DECISIONS.md?= =?UTF-8?q?=20bind=20the=20same=20live=20identities=20(M-A=20e26c6f79?= =?UTF-8?q?=E2=80=A6,=20M-B=206f8e3572=E2=80=A6,=20tests=20645a44c0?= =?UTF-8?q?=E2=80=A6,=20design=20record=202d6be6be=E2=80=A6),=2048/48=20te?= =?UTF-8?q?sts,=20run=20result=20at=20head=201b1338ddd,=20the=20full=20adv?= =?UTF-8?q?ersarial=20chain=20through=20reviewer:d012-final-reviewer2,=20a?= =?UTF-8?q?nd=20the=20committed=20in-repo=20D-012-DESIGN-CONVERGENCE.md=20?= =?UTF-8?q?identity;=20preregistration=20rev3=20remains=20explicitly=20lab?= =?UTF-8?q?eled=20historical.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- DECISIONS.md | 2 +- decisions/ADR-012-promotion-evidence-governance.md | 2 +- decisions/D-012-PACKET.md | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/DECISIONS.md b/DECISIONS.md index d9b342593c..fe8bab28cc 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 rev6 (41/41 tests incl. no-mutation postconditions, reentrant recovery/expiry probes, and the cross-registry final-point linearizability probe; machine-readable run result) and adversarial reviews (`reviewer:d012-packet-reviewer`, `reviewer:d012-resolution-reviewer`, `reviewer:d012-final-reviewer`, `reviewer:d012-rev5-verify2` — findings corrected through rev6). 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 rev7 (48/48 tests incl. parameterized cross-registry linearizability probes, no-mutation postconditions, reentrant recovery/expiry probes, closed value-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` — findings corrected through rev7). 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/decisions/ADR-012-promotion-evidence-governance.md b/decisions/ADR-012-promotion-evidence-governance.md index 210e22af69..d25c4f7594 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 rev6), models `AOS/decisions/d012/m_policy_generations.py` (sha256 `9037ea07…`), `m_admission_replay.py` (sha256 `87da4fdd…`, rev6 with M-B→M-A cross-registry lock composition closing the final-point revocation race, and full post-callback revalidation of every commit precondition), tests `test_d012_models.py` (41/41 pass, machine-readable run result `d012-model-run-result.json`, head `805540e1d…`), 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), design phase `D-012-DESIGN-CONVERGENCE.md`. +**Evidence:** `AOS/decisions/D-012-PACKET.md` (preregistered rev3; live identity rev7), models `AOS/decisions/d012/m_policy_generations.py` (sha256 `e26c6f79…`, closed value grammar + registry lock + deep-copy insulation), `m_admission_replay.py` (sha256 `6f8e3572…`, required M-B→M-A cross-registry lock-composition protocol, full post-callback revalidation, closed time domain with monotonic guard), tests `test_d012_models.py` (48/48 pass, machine-readable run result `d012-model-run-result.json`, head `1b1338ddd…`), design phase `D-012-DESIGN-CONVERGENCE.md` (sha256 `2d6be6be…`, committed at rev7), 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). **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 63e460dac5..7ce42e318a 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 **rev6** (post-resolution adversarial review chain through `reviewer:d012-rev5-verify2`). +**Status:** RESOLVED (2026-09-14, owner P0 sitting; ADR-012). Preregistration remains rev3 (immutable, pre-resolution); the live evidence identity below is correction generation **rev7** (post-resolution adversarial review chain through `reviewer:d012-final-reviewer2`). **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 rev6 (governing):* `m_policy_generations.py` sha256 `9037ea0770de26d7fbc383dbe376a8f18c16af946d22b95da05cdbc6fe630534` (grammar rev4 + registry lock), `m_admission_replay.py` sha256 `87da4fddb31e92489ab06bc9a23a4bbf7f30525b7bb29d7ff1d06a794ce9a563` (grammar rev4 + M-B→M-A lock composition and full post-callback revalidation), tests `test_d012_models.py` sha256 `2c1677a5e454e9f3483d2cbac3606b7422866ae3559c41036a222d16df1ccf7f`; machine-readable run result `d012-model-run-result.json` (41 tests, 0 failures, 0 errors, head `805540e1d…` — rev6, including the no-mutation postconditions, reentrant recovery/expiry cases, and the cross-registry final-point linearizability probe). **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 rev7 (governing):* `m_policy_generations.py` sha256 `e26c6f795ee805fa5abcb30b1979b7724d0d27ba81d5ca5e2159a6940b90ba85` (grammar rev4 + registry lock + closed value grammar with deep-copy insulation), `m_admission_replay.py` sha256 `6f8e357296367ae30c44ae024c347ba9c1edb38f689247cdb3e6f7f04f81a074` (grammar rev4 + required M-B→M-A lock-composition protocol, full post-callback revalidation, closed time domain with monotonic guard), tests `test_d012_models.py` sha256 `645a44c034f09195ce5b876ee932bc473369276f20397127160565c54009cb1e`; design-phase record `D-012-DESIGN-CONVERGENCE.md` sha256 `2d6be6be0ef4b31559923d666ae2d60ff33a4788fadb7227c45f920fcc965ecb` (committed at rev7); machine-readable run result `d012-model-run-result.json` (48 tests, 0 failures, 0 errors, head `1b1338ddd…` — rev7, including the parameterized cross-registry linearizability probes, no-mutation postconditions, reentrant recovery/expiry cases, closed-grammar and 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) -- 2.54.0