diff --git a/CHANGELOG.md b/CHANGELOG.md index de4343f..1af4050 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] ### 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 +- 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) - Safe `pollEvents` returning `Maybe NifEvent` instead of raw `Bits64` diff --git a/docs/decisions/0007-claims-to-evidence-discipline.adoc b/docs/decisions/0007-claims-to-evidence-discipline.adoc new file mode 100644 index 0000000..2f850b9 --- /dev/null +++ b/docs/decisions/0007-claims-to-evidence-discipline.adoc @@ -0,0 +1,67 @@ += Architecture Decision Record: 0007-claims-to-evidence-discipline + + + +# 7. Claims-to-evidence discipline & optional-dependency policy + +Date: 2026-05-19 + +## Status + +Accepted + +Formalises the recurring `STATE.a2ml [blockers-and-issues] doc-reality-drift` +problem. Implements the doc-honesty half of the "Earn the Core" program +(tracking epic + issue #51). + +## Context + +Doc-reality drift is a recurring, self-acknowledged failure mode: the +README/ROADMAP have repeatedly claimed as DONE things that are partial in +the shipped build (Formal Proofs "DONE" but no runtime enforcement; PTP +"sub-microsecond" but the hardware clock NIF is unvalidated and absent; +QUIC and SNIF marketed while `quicer`/`wasmex` are disabled optional deps; +"<10 ms" / "500+ concurrent" unbenchmarked). + +Each overclaim taxes the credibility of the *true* core claims. The +`EXPLAINME.adoc` "show me the receipts, with honest caveats" pattern is +the correct instinct but is not enforced repo-wide, and "optional" NIF +dependencies are described as if always present. + +## Decision + +1. **Claims map to evidence.** Every capability stated as fact in + `README.adoc` / `ROADMAP.adoc` / marketing-facing docs MUST map to (a) + a concrete code path and (b) an automated test. Anything not meeting + both goes in an explicit **Experimental** or **Aspirational** section, + clearly labelled as such. +2. **Optional dependencies are experimental-until-wired.** A capability + that depends on an optional/disabled NIF (`quicer`/msquic, + `wasmex`/SNIF, `elmdb`, …) is **Experimental** in user-facing docs + until the dependency is built, enabled, and covered by a test in CI. + Runtime code already degrades gracefully (the `:quicer` / + `Burble.Bolt.Quic` pattern, ADR-0004; SNIF/`Wasmex`, PR #46) — the + *claims* must match that reality. +3. **Drift is a release gate.** Re-attaining/holding CRG C includes a + check that headline claims have not regressed against this policy. + +## Consequences + +### Positive + +- The README's core claims become trustworthy; the strong core stops + being obscured by the augmented layer's ambition. +- A single, citable policy to close `doc-reality-drift` entries against. + +### Negative + +- The README will, in the short term, *look* less impressive: several + features move under "Experimental". This is the point — honest scope + is the asset. + +### Neutral + +- No code change. Enforcement is editorial + a CI doc-claim check + (scoped under issue #51 / CRG-C #50). +- The formal-proof "DONE vs enforced" claim is the subject of its own + decision — see ADR-0008. diff --git a/docs/decisions/0008-formal-proof-enforcement-vs-scope.adoc b/docs/decisions/0008-formal-proof-enforcement-vs-scope.adoc new file mode 100644 index 0000000..d153a66 --- /dev/null +++ b/docs/decisions/0008-formal-proof-enforcement-vs-scope.adoc @@ -0,0 +1,69 @@ += Architecture Decision Record: 0008-formal-proof-enforcement-vs-scope + + + +# 8. Formal-proof enforcement vs. scoping the "formally verified" claim + +Date: 2026-05-19 + +## Status + +Proposed + +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. + +## Context + +Burble markets a "Majestic / Dual-Track" formally-verified posture. The +reality (`BURBLE-PROOF-STATUS.md`, `PROOF-NEEDS.md`, `READINESS.adoc`): + +- All six Idris2 ABI proof modules **compile and type-check** + (Types, Permissions, Avow, Vext, MediaPipeline, WebRTCSignaling). +- But **runtime enforcement is not wired**: `Burble.Verification.Avow` + is data-type-only; there is no bridge making the Elixir runtime reject + values that violate the proven types. `READINESS.adoc`: *"safe by + construction for current use cases. Dependent-type enforcement is a + correctness hardening measure, not a security boundary."* + +So "formally verified" is true at the *type-check* level and aspirational +at the *runtime-enforcement* level. ADR-0007 requires this gap be either +closed or scoped honestly; which one is a strategic choice with real cost. + +## Decision + +**To be decided by the maintainer.** Options: + +* **Option A — Wire enforcement.** Build the Idris2→runtime enforcement + bridge (proof-derived validators at the Elixir/Zig ABI boundary) as a + scheduled phase. Highest rigor; substantial effort; turns the + differentiator into a real moat (supports Route B "Majestic"). +* **Option B — Scope the claim.** State precisely: "ABI proofs compile + and type-check; runtime enforcement is on the roadmap." Cheap, honest, + immediately removes the overclaim; keeps the proofs as design + assurance rather than a runtime guarantee. +* **Option C — Hybrid.** Scope the claim now (Option B wording) **and** + schedule enforcement for one high-value module (e.g. `Permissions` or + `Avow`) as a proof-of-concept before committing to the full bridge. + +Recommendation (non-binding): **Option C** — it satisfies ADR-0007 +immediately (no overclaim) while preserving the Majestic differentiator +as a funded, scoped experiment rather than perpetual aspiration. + +## Consequences + +### Positive + +- Removes a long-standing overclaim regardless of which option is chosen. +- Forces an explicit, recorded decision instead of silent drift. + +### Negative + +- Option A is expensive; Option B narrows the marketing story. + +### Neutral + +- Until accepted, ADR-0007 governs: the "formally verified" claim must + read as type-check-level only, with runtime enforcement labelled + Experimental/Aspirational. diff --git a/docs/decisions/README.adoc b/docs/decisions/README.adoc index ac78ea4..9855ef9 100644 --- a/docs/decisions/README.adoc +++ b/docs/decisions/README.adoc @@ -35,4 +35,12 @@ New ADRs copy `0000-template.adoc` and take the next number. | link:0006-proven-frame-not-applicable-to-bolt-packet.adoc[0006] | proven-frame is not applicable to Burble.Bolt.Packet | Accepted + +| link:0007-claims-to-evidence-discipline.adoc[0007] +| Claims-to-evidence discipline & optional-dependency policy +| Accepted + +| link:0008-formal-proof-enforcement-vs-scope.adoc[0008] +| Formal-proof enforcement vs. scoping the "formally verified" claim +| Proposed |===