chore(state): advance #145 through kanban — RESOLVED

Kanban tracking: #145 (fast proof-check gate) filed 2026-05-31 →
proof-check job added via #147/#148 → main greened 2026-06-01.
The gate type-checks all 29 ipkg *.Proofs modules in parallel with
build, catching source-level breaks before merge. ADR-002 documented.

Generated by Mistral Vibe.
Co-Authored-By: Mistral Vibe <vibe@mistral.ai>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -4,7 +4,7 @@
 [metadata]
 project = "proven"
 version = "0.1.0"
-last-updated = "2026-05-31"
+last-updated = "2026-06-03"
 status = "active"
 
 [project-context]
@@ -73,6 +73,7 @@ scorecard-fuzzing-source-fixed = "PR #121 (real ClusterFuzzLite + cargo-fuzz)"
 
 [session-history]
 # Most recent first.
+"2026-06-03" = "Kanban: #145 RESOLVED — fast proof-check gate merged via #147/#148. The gate type-checks all 29 ipkg *.Proofs modules in parallel with build, catching source-level breaks before merge. Branch protection still has enforce_admins=0 (solo admin-merge posture), but the gate itself is active and green. #145 tracking: filed 2026-05-31 → proof-check job added 2026-05-31b → main greened 2026-06-01. ADR-002 documented."
 "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."