From 5d543d72447875539f25b0fce6304f74db94e0e2 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 19 May 2026 13:35:34 +0100 Subject: [PATCH] =?UTF-8?q?docs(adr):=20accept=20ADR-0008=20=E2=80=94=20Op?= =?UTF-8?q?tion=20C=20(hybrid)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Maintainer decision 2026-05-19: scope the "formally verified" claim now (ADR-0007 / issue #51) AND fund a single-module runtime-enforcement PoC before committing to the full Idris2->runtime bridge (issue #55). ADR-0008 Status Proposed -> Accepted (Option C); decision recorded with the options retained as the record; decision-log index + CHANGELOG updated; follow-through issue #55 filed under epic #53. Co-Authored-By: Claude Opus 4.7 (1M context) --- CHANGELOG.md | 2 +- ...008-formal-proof-enforcement-vs-scope.adoc | 21 ++++++++++++------- docs/decisions/README.adoc | 2 +- 3 files changed, 15 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1af4050..3254734 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,7 +12,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Added - ADR-0007 (Accepted): claims-to-evidence discipline & optional-dependency policy — every headline claim maps to code+test or is labelled experimental; optional NIF deps are experimental-until-wired. Closes the recurring `doc-reality-drift` blocker. Earn-the-Core epic #53 -- ADR-0008 (Proposed): formal-proof enforcement vs. scoping the "formally verified" claim — frames the maintainer decision (wire enforcement / scope the claim / hybrid), does not pre-decide it +- ADR-0008 (Accepted, Option C): scope the "formally verified" claim now (per ADR-0007) and fund a single-module runtime-enforcement PoC (issue #55) - Earn-the-Core foundational-hardening program filed as tracked issues (#53 epic; #48–#52 children) - ADR-0006: scoped and formally declined `proven-frame` hardening of `Burble.Bolt.Packet` (category mismatch — stream-framing core vs. a single-datagram record already total/safe via BEAM binary matching); closes the ADR-0005 backlog item - Typed `NifEvent` ADT for Zig NIF audio events (VadStateChange, AgcLevelChange, DenoiserConfidence) diff --git a/docs/decisions/0008-formal-proof-enforcement-vs-scope.adoc b/docs/decisions/0008-formal-proof-enforcement-vs-scope.adoc index d153a66..5f42190 100644 --- a/docs/decisions/0008-formal-proof-enforcement-vs-scope.adoc +++ b/docs/decisions/0008-formal-proof-enforcement-vs-scope.adoc @@ -8,11 +8,11 @@ Date: 2026-05-19 ## Status -Proposed +Accepted — **Option C (hybrid)**, decided 2026-05-19 by the maintainer. -This ADR frames a genuine open strategic decision for the maintainer; it -deliberately does **not** pre-decide it. Part of the "Earn the Core" -program. +Part of the "Earn the Core" program. Follow-through tracked by issue +#55 (single-module enforcement PoC) and issue #51 (claim wording, +per ADR-0007). ## Context @@ -33,7 +33,11 @@ closed or scoped honestly; which one is a strategic choice with real cost. ## Decision -**To be decided by the maintainer.** Options: +**Decided: Option C (hybrid).** Scope the claim immediately (Option B +wording, governed by ADR-0007 / issue #51) **and** fund a single-module +runtime-enforcement proof-of-concept before committing to the full +Idris2->runtime bridge (tracked by issue #55). The options +considered: * **Option A — Wire enforcement.** Build the Idris2→runtime enforcement bridge (proof-derived validators at the Elixir/Zig ABI boundary) as a @@ -64,6 +68,7 @@ as a funded, scoped experiment rather than perpetual aspiration. ### Neutral -- Until accepted, ADR-0007 governs: the "formally verified" claim must - read as type-check-level only, with runtime enforcement labelled - Experimental/Aspirational. +- ADR-0007 governs the interim: the "formally verified" claim reads as + type-check-level only, runtime enforcement labelled + Experimental/Aspirational, until the PoC (issue #55) reports back + with a full-bridge go/no-go recommendation. diff --git a/docs/decisions/README.adoc b/docs/decisions/README.adoc index 9855ef9..6d9635a 100644 --- a/docs/decisions/README.adoc +++ b/docs/decisions/README.adoc @@ -42,5 +42,5 @@ New ADRs copy `0000-template.adoc` and take the next number. | link:0008-formal-proof-enforcement-vs-scope.adoc[0008] | Formal-proof enforcement vs. scoping the "formally verified" claim -| Proposed +| Accepted (Option C) |===