From 277a065957f55cca1deef6c6ab1020a1ac87b20e Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 19 May 2026 14:37:10 +0100 Subject: [PATCH] fix(proofs): repair build harness; correct false 'all six compile' claim MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verified with idris2 0.8.0 (which IS installed; the "not installed" note was wrong). The proof build never worked: ipkg sourcedir resolved modules to a non-existent path, and idris2's baked-in prefix points at a missing ~/.asdf path. Both fixed (ipkg ../..; Justfile derives IDRIS2_PREFIX from PATH). True status: 6/7 ABI modules compile (Types, Foreign, WebRTCSignaling, Permissions, Avow, Vext). MediaPipeline.idr FAILS — Idris1 `postulate`, removed in Idris2. So BURBLE-PROOF-STATUS's "all six compile and type-check" was false; corrected here with verified per-module results (ADR-0007). The MediaPipeline fix is policy-sensitive (0-believe_me invariant) and tracked as issue #60 under epic #53 — deliberately not hand-patched. Co-Authored-By: Claude Opus 4.7 (1M context) --- .machine_readable/6a2/STATE.a2ml | 7 +++++++ BURBLE-PROOF-STATUS.md | 6 ++---- Justfile | 4 +++- PROOF-NEEDS.md | 2 +- src/Burble/ABI/burble-abi.ipkg | 2 +- 5 files changed, 14 insertions(+), 7 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index fd8d2a2..68210bd 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -138,6 +138,13 @@ open-failures = 0 # Gate still NOT re-armed (continue-on-error kept per #39); # remaining 156 = genuine test debt + OTP25-vs-CI-OTP27 # skew, needs authoritative CI run to triage. +# 2026-05-19: Idris2 proofs VERIFIED (idris2 0.8.0, prefix fixed) — +# 6/7 ABI modules compile (Types/Foreign/WebRTCSignaling/ +# Permissions/Avow/Vext); MediaPipeline.idr FAILS (Idris1 +# `postulate`, invalid in Idris2). BURBLE-PROOF-STATUS +# 'all six compile' was false (now corrected, ADR-0007). +# ipkg sourcedir + Justfile IDRIS2_PREFIX fixed so the +# harness runs. MediaPipeline fix tracked under epic #53. [crg] grade = "C" diff --git a/BURBLE-PROOF-STATUS.md b/BURBLE-PROOF-STATUS.md index 391547d..bef8e24 100644 --- a/BURBLE-PROOF-STATUS.md +++ b/BURBLE-PROOF-STATUS.md @@ -1,7 +1,7 @@ # Burble Proof Status -**Short version.** All six Idris2 ABI proof modules compile and type-check. See `PROOF-NEEDS.md` for the current proof inventory, and `STATE.a2ml` for any in-progress work. +**Short version (verified 2026-05-19, Idris2 0.8.0).** 6 of 7 ABI modules compile and type-check: `Types`, `Foreign`, `WebRTCSignaling`, `Permissions`, `Avow`, `Vext`. **`MediaPipeline.idr` does NOT compile** — it uses the Idris1 `postulate` keyword, removed in Idris2 (parse error at the `resampleFrame` declaration). The aggregate `just build-proofs` now works (ipkg `sourcedir` + `IDRIS2_PREFIX` were both broken — fixed) but the build still aborts at `MediaPipeline`. Tracked: see the proofs issue under epic #53. Per ADR-0007 the "formally verified" claim is type-check-level for 6/7 modules, NOT all-six. ## Current ABI proofs (all compile) @@ -60,9 +60,7 @@ The `src/interface/abi/` tree is marked **deferred to Phase 1 module-path cleanu **Unsafe FFI debt:** - `prim__registerCallback` in `Burble.ABI.Foreign` is intentionally unexposed. C→Idris callbacks require `believe_me` casts (tracked upstream in idris2#3182). Phase 0 replaces callback usage with `pollEvents` (lock-free ring buffer polling). No `believe_me` or `assert_total` in any module. -**Local smoke-test result:** `tool-blocked: idris2 not installed` on development machine. -The recipe and package file are correct; install `idris2` (v0.7+) to run locally. -CI validation is gated on Workstream 0.1 stabilising (see §4.5 of the Phase 0 plan). +**Local smoke-test result (2026-05-19):** idris2 0.8.0 IS installed (`dev/tools/provers/idris2/0.8.0`); the prior "not installed" note was wrong. The recipe and package file were NOT correct: ipkg `sourcedir` resolved modules to a non-existent path and idris2's baked-in prefix pointed at a missing `~/.asdf` path. Both fixed. Verified per-module result above. ## Phase 0 deploy-smoke status (Workstream 0.4) diff --git a/Justfile b/Justfile index 58735c3..d7e81ab 100644 --- a/Justfile +++ b/Justfile @@ -85,7 +85,9 @@ build-server: # Module collision note: src/interface/abi/ also declares Burble.ABI.Types # and is excluded from this recipe (deferred to Phase 1 module-path cleanup). build-proofs: - cd src/Burble/ABI && idris2 --build burble-abi.ipkg + # idris2 binaries built elsewhere bake in a wrong prefix; derive it + # from the idris2 on PATH (override with IDRIS2_PREFIX if needed). + cd src/Burble/ABI && IDRIS2_PREFIX="${IDRIS2_PREFIX:-$(dirname "$(dirname "$(command -v idris2)")")}" idris2 --build burble-abi.ipkg # Build web client build-client: diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 904c245..4cef59d 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -1,7 +1,7 @@ # Proof Requirements ## Current state -- `src/Burble/ABI/MediaPipeline.idr` — **Linear buffer consumption proof (DONE)** +- `src/Burble/ABI/MediaPipeline.idr` — Linear buffer consumption proof (**does NOT compile under Idris2 0.8.0** — Idris1 `postulate` keyword; tracked under epic #53) - `src/Burble/ABI/WebRTCSignaling.idr` — **JSEP state machine proof (DONE)** - `src/Burble/ABI/Permissions.idr` — **Role transition and lattice well-foundedness (DONE)** - `src/Burble/ABI/Avow.idr` — **Attestation chain non-circularity (DONE)** diff --git a/src/Burble/ABI/burble-abi.ipkg b/src/Burble/ABI/burble-abi.ipkg index d4354d3..206e10a 100644 --- a/src/Burble/ABI/burble-abi.ipkg +++ b/src/Burble/ABI/burble-abi.ipkg @@ -13,7 +13,7 @@ package burble-abi version = 0.1.0 authors = "Jonathan D.A. Jewell" -sourcedir = "." +sourcedir = "../.." -- repo src/ root: Burble.ABI.Types -> src/Burble/ABI/Types.idr modules = Burble.ABI.Types , Burble.ABI.Avow