hyperpolymath · hyperpolymath · Jun 1, 2026 · Jun 1, 2026
@@ -6,11 +6,13 @@ project = "proven"
 author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
 license = "MPL-2.0"
 standard = "RSR 2026"
-last-updated = "2026-05-20"
+last-updated = "2026-06-01"
 
 [architecture-decisions]
 decisions = [
   { id = "ADR-001", title = "OWED-with-justification convention for bodyless declarations in Proofs.idr files", status = "accepted", date = "2026-05-20", body = "Bodyless type signatures (implicit postulates) are made discoverable via triple-pipe doc-comment naming the claim + Idris2 0.8.0 blocker + discharge condition, plus a leading `0 ` erased-multiplicity marker, plus the original bare signature. The `postulate` keyword is NOT used (zero Proofs.idr files use it). Canonical example: src/Proven/SafeChecksum/Proofs.idr. Reference: hyperpolymath/standards#158 Fork A campaign, PROOF-NEEDS.md." },
+  { id = "ADR-002", title = "Fast proof-check CI gate over the proven.ipkg proof modules", status = "accepted", date = "2026-06-01", body = "A required proof-check job runs idris2 --check on each *.Proofs module listed in proven.ipkg (the 29 build-contract proof modules), from the src/ sourcedir with module-relative paths, on a clean idris2-0.8.0 + contrib toolchain (build/ removed so a stale TTC cannot mask a break). This is the fast cone-check recommended in #145 after #127/#145 showed DISCHARGED-but-unbuilt proofs reaching main while the slow full build sat queued. Scope is the ipkg list, not every on-disk Proofs.idr (64 of 93 are intentionally env-blocked or WIP). A corollary of ADR-001: a theorem that can only be closed by consuming an erased 0-multiplicity OWED premise, or an irreducible top-level-constant projection, is itself reverted to OWED rather than given a body that does not type-check. Origin: #147 (gate) and #148 (gate correctness + 5 proof repairs)." },
+  { id = "ADR-003", title = "CI builds the standalone Zig FFI surface; full Idris->RefC->Zig integration deferred", status = "accepted", date = "2026-06-01", body = "The e2e.yml E2E and Bench jobs build ffi/zig/build_standalone.zig (src/main.zig only, the pure-Zig C-ABI surface) instead of the default build.zig, because build.zig's idris2_zig_ffi is a Zig .path dependency on the private, sibling-checkout-only repo nextgen-languages/language-bridges, which CI cannot resolve. The Zig toolchain is provisioned via mlugg/setup-zig@v1 at the build.zig.zon minimum (0.15.2). Full Idris->RefC->Zig integration (idris2 --codegen refc + scripts/build-refc.sh + zig build -Didris-*) is documented in docs/ffi-ci-build.md and deferred until language-bridges is provisioned as a submodule plus a CI read credential. Origin: #149; tracked in #151." },
 ]
 
 [proof-conventions]

@@ -73,7 +73,8 @@ scorecard-fuzzing-source-fixed = "PR #121 (real ClusterFuzzLite + cargo-fuzz)"
 
 [session-history]
 # Most recent first.
-"2026-05-31b" = "CI proof-gate (#147 → #148): added a fast `proof-check` job type-checking every *.Proofs module listed in proven.ipkg (29) from src/ with module-relative paths; fixed two self-inflicted gate bugs (repo-root path → spurious 'module name does not match file name'; over-broad glob over all 93 on-disk vs the 29 ipkg-built). The gate found 5 ipkg proof modules that never compiled (DISCHARGED-but-unbuilt, same disease as #127): SafeUrl appendAssociative (referenced nonexistent Data.List.Equalities.appendAssociative; fixed to sym (Data.List.appendAssociative)) + addParamIncreasesCount (lengthSnoc arg order) now genuinely hold; SafeSQL ×4 and SafeEmail ×1 reverted DISCHARGED→OWED (depended on erased OWED premises / top-level-constant opacity). All 29 now green on a clean idris2-0.8.0+contrib build. ADR-004."
+"2026-06-01" = "Greened main: #148 + #149 admin-merged. #148 — proof-check gate correctness (run from src/ with module-relative paths; ipkg-scoped to the 29 *.Proofs modules) + 5 never-compiled proof repairs: SafeUrl appendAssociative (→ sym (Data.List.appendAssociative)) and addParamIncreasesCount (lengthSnoc arg order) now genuinely discharged; SafeSQL ×4 + SafeEmail ×1 reverted DISCHARGED→OWED (erased premises / top-level-constant opacity); discharged-decls 36→31; ADR-002. #149 — fixed e2e.yml Zig toolchain (goto-bus-stop@v2.2.1/0.15.0 → mlugg@v1/0.15.2 per build.zig.zon) and pointed E2E/Bench at build_standalone.zig (pure-Zig surface; full Idris→Zig pipeline deferred — ADR-003, docs/ffi-ci-build.md, #151); set bindings/rust/fuzz/README.adoc SPDX CC-BY-4.0→MPL-2.0 (fixed Enforce Trustfile Policies). Both merged over the one remaining red, governance / Language / package anti-pattern policy — pre-existing, lives in hyperpolymath/standards (rsr-antipattern.yml), likely flags banned-language bindings (typescript/hy/javascript); tracked in #150."
+"2026-05-31b" = "CI proof-gate (#147 → #148): added a fast `proof-check` job type-checking every *.Proofs module listed in proven.ipkg (29) from src/ with module-relative paths; fixed two self-inflicted gate bugs (repo-root path → spurious 'module name does not match file name'; over-broad glob over all 93 on-disk vs the 29 ipkg-built). The gate found 5 ipkg proof modules that never compiled (DISCHARGED-but-unbuilt, same disease as #127): SafeUrl appendAssociative (referenced nonexistent Data.List.Equalities.appendAssociative; fixed to sym (Data.List.appendAssociative)) + addParamIncreasesCount (lengthSnoc arg order) now genuinely hold; SafeSQL ×4 and SafeEmail ×1 reverted DISCHARGED→OWED (depended on erased OWED premises / top-level-constant opacity). All 29 now green on a clean idris2-0.8.0+contrib build. ADR-002."
 "2026-05-31" = "SafeJson Phase 3: #144 DISCHARGES anyMatchesTAny (6-arm split) + singleKeyPath (with-pattern), completing #138. Root-caused a pre-existing breakage: appendLengthInc (from #127) used `lengthSnoc arr v` but contrib Data.List.Equalities.lengthSnoc is element-first — it failed to type-check and blocked the ENTIRE SafeJson.Proofs module (so main did not compile). Fixed to `lengthSnoc v arr`. Verified on a clean idris2-0.8.0+contrib install (full SafeJson cone, 0 errors). Filed #145: the Idris build is not a required status check, so #127's broken merge went green (created→merged in ~2.5min with build jobs still queued); recommends branch-protection gating + faster cone-check job."
 "2026-05-30" = "Phase 3 discharge: PRs #97-124 land (~28 OWED→DISCHARGED conversions). Security tab cleanup: source-fixes for #2 / #296 / #299 + branch-protection safe-subset + 100 Hypatia FP alerts dismissed at API. Estate-wide CSA self-echo bulk-dismiss sweep (~9050 alerts) running in background."
 "2026-05-20" = "Fork A campaign complete: 250 bodyless decls across 28 of 41 modules annotated via OWED-with-justification convention (PRs #37-64, Refs standards#158); cross-prover audit confirms 0 Lean sorry / 0 Coq Admitted in first-party code (only echidnabot dogfood fixtures)"

@@ -0,0 +1,68 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# FFI CI build: standalone surface (now) vs full Idris→Zig pipeline (deferred)
+
+`proven`'s FFI layer compiles Idris 2 to C via the RefC backend and wraps it in
+a stable C ABI with Zig (`Idris2 --codegen refc → .c → zig build → libproven`).
+There are **two** Zig build entry points:
+
+| File | Builds | External deps | Used by |
+|------|--------|---------------|---------|
+| `ffi/zig/build.zig` | full Idris→RefC→Zig `libproven` | `idris2_zig_ffi` (path dep on `nextgen-languages/language-bridges`) + generated RefC C | local dev, full integration |
+| `ffi/zig/build_standalone.zig` | `libproven_ffi.a` from `src/main.zig` only (pure-Zig C-ABI surface) | none | **CI** (`e2e.yml`) |
+
+## Why CI uses the standalone build (ADR-003)
+
+`build.zig` declares its `idris2_zig_ffi` dependency as a Zig **`.path`**
+dependency:
+
+    .idris2_zig_ffi = .{ .path = "../../../nextgen-languages/language-bridges/bridges/idris2" }
+
+That points at a **private, cross-owner sibling repo** which CI does not (and
+cannot, without a credential) check out, so `zig build` fails at dependency
+resolution. `build_standalone.zig` compiles `src/main.zig` alone — and that
+file imports only `std`/`builtin` — so it needs neither the bridge nor the
+generated RefC, giving CI a real (if narrower) Zig FFI build + unit-test signal.
+
+`e2e.yml` therefore runs, with Zig provisioned by `mlugg/setup-zig@v1` at
+`0.15.2` (the `build.zig.zon` minimum):
+
+    zig build       --build-file build_standalone.zig      # E2E build
+    zig build test  --build-file build_standalone.zig      # E2E tests
+    zig build bench --build-file build_standalone.zig || … # Bench (soft)
+
+## The full pipeline (recipe — Idris half verified locally)
+
+The canonical recipe is the root `Justfile` (`build-refc` + `build-ffi`).
+Verified locally on idris2-0.8.0 + contrib:
+
+    # Step 1 — Idris → RefC C  (scripts/build-refc.sh, IPKG=proven-ffi.ipkg)
+    idris2 --codegen refc --build proven-ffi.ipkg     # → build/exec/proven-ffi.c
+    # staged to build/refc/ ; the script prints the four paths used below
+
+    # Step 2 — Zig links the RefC C + Idris runtime/support into libproven
+    PFX=$(idris2 --prefix)
+    zig build \
+      -Didris-refc="$PWD/build/refc" \
+      -Didris-refc-runtime="$(find "$PFX" -path '*/support/refc' -type d | head -1)" \
+      -Didris-c-support="$(find "$PFX" -path '*/support/c' -type d | head -1)" \
+      -Didris-support-lib="$(find "$PFX" -path '*/lib/libidris2_support.*' | head -1 | xargs dirname)"
+
+Requires `libgmp` (the RefC runtime links `gmp`/`pthread`/`m`).
+
+## Enabling full integration in CI (deferred — #151)
+
+The default `build.zig` needs `nextgen-languages/language-bridges` present.
+Because it is **private** and **not** a submodule, CI cannot fetch it today.
+To enable:
+
+1. Add `language-bridges` as a **git submodule** inside `proven`, and point
+   `ffi/zig/build.zig.zon`'s `.path` at the in-repo submodule location (the
+   current `../../../…` escapes the repo, so it must change).
+2. Add a **CI read credential** (deploy key / PAT) and use `actions/checkout`
+   with `submodules: true`.
+3. Add/extend a workflow that installs Idris2 + `libgmp`, runs
+   `scripts/build-refc.sh`, then the `zig build -Didris-*` invocation above.
+
+Tracked in #151. The interim standalone build is ADR-003.