chore: merge root Idris fix from main

Author: hyperpolymath

.github/workflows/governance.yml

@@ -31,4 +31,4 @@ permissions:
 
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@main
+    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@861b5e911d9e5dcfb3c0ab3dd2a9a3c8fd0a1613

.machine_readable/6a2/STATE.a2ml

@@ -52,15 +52,15 @@ postulate-keyword-uses = 0
 
 [active-campaigns]
 fork-a-annotation = "complete"
-phase-3-discharge = "in flight — umbrella issue #90, sequencing SafeUrl → SafeRegex → SafeBase64 → SafeEmail. 34 DISCHARGED of ~209 Tier A sites (~16% as of 2026-05-30). PRs #97-124 landed this cycle."
-fork-b-discharge = "triage open — quick-wins flagged in PROOF-NEEDS.md (SafeCrypto isSecure refactor; SafePath already-Refl pairs)"
+phase-3-discharge = "in flight — umbrella issue #90, sequencing SafeUrl → SafeRegex → SafeBase64 → SafeEmail. 36 DISCHARGED of ~209 Tier A sites (~17.3% as of 2026-06-03, +2 from SafeEmail errorMakesInvalid + warningKeepsValid). PRs #97-124 + #144 landed this cycle."
+fork-b-discharge = "in flight — quick-wins: SafeCrypto isSecure refactor COMPLETED (modernIsSecure, standardIsSecure); SafePath already-Refl pairs still under triage"
 
 [ci-infrastructure]
 # 2026-05-30 session — workflow hardening
 fuzzing = "ClusterFuzzLite + cargo-fuzz; 4 fuzz targets on FFI parse surface (safe_url_parse, safe_email_is_valid, safe_json_is_valid, safe_path_has_traversal). Per-PR + weekly batch; PR #121. Replaces prior broken setup (pointed at nonexistent dir + AGPL header)."
 concurrency-cancel = "added to architecture-enforcement.yml, idris2-ci.yml, zig-ffi.yml, trustfile.yml, boj-build.yml. PR #115."
 per-job-timeouts = "added to the same 4 workflows; budget proportional to expected runtime (5-45 min)."
-branch-protection-main = "6 safe settings active: dismiss_stale_reviews, required_linear_history, required_conversation_resolution, required_signatures, allow_force_pushes=false, allow_deletions=false. enforce_admins + required_approving_review_count=0 deliberately to preserve solo admin-merge workflow."
+branch-protection-main = "7 safe settings active: dismiss_stale_reviews, required_linear_history, required_conversation_resolution, required_signatures, allow_force_pushes=false, allow_deletions=false, proof-check. enforce_admins + required_approving_review_count=0 deliberately to preserve solo admin-merge workflow."
 
 [security-tab-state]
 # 2026-05-30 — Hypatia + CodeQL + Scorecard alert disposition
@@ -73,6 +73,7 @@ scorecard-fuzzing-source-fixed = "PR #121 (real ClusterFuzzLite + cargo-fuzz)"
 
 [session-history]
 # Most recent first.
+"2026-06-03" = "Kanban: #145 CLOSED — admin configured branch protection to require proof-check status check. Full #145 tracking: filed 2026-05-31 → proof-check job added via #147/#148 → main greened 2026-06-01 → branch protection configured 2026-06-03. The gate type-checks all 29 ipkg *.Proofs modules in parallel with build. 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."

docs/proof-debt-triage-tier-a.md

@@ -14,8 +14,8 @@ This file is the per-site disposition data for every `||| OWED:` annotation in t
 
 | Disposition | Count | Share | Estimated Phase 3 cost |
 |---|---:|---:|---|
-| **DISCHARGE** (provable in Idris2 0.8.0 today) | **~59** | 28% | ~30h (~4 focused days) |
-| **DISCHARGE-after-totality** (blocked on totality refactor first) | **~7** | 3% | TBD per totality ticket |
+| **DISCHARGE** (provable in Idris2 0.8.0 today) | **~61** | 28% | ~31h (~4 focused days) |
+| **DISCHARGE-after-totality** (blocked on totality refactor first) | **~5** | 3% | TBD per totality ticket |
 | **PROPERTY-TEST** (concrete-input spot-check in `tests/properties/`) | **~66** | 31% | ~22h (~3 focused days) |
 | **OWED-AXIOM** (permanent or until-Idris2-upgrade) | **~79** | 38% | 0h discharge; ongoing ledger maintenance |
 
@@ -309,16 +309,16 @@ Discrepancies of ±2 against the 210 figure are real — sub-agents occasionally
 | setHasKey | 139 | `isObject obj ⇒ hasKey k (set k v obj) = True` | 1 | OWED-AXIOM | 0 | same `prim__eq_String` blocker |
 | removeNotHasKey | 157 | `hasKey k (remove k obj) = False` | 1 | OWED-AXIOM | 0 | String `!=` on pairs + filter |
 | appendLengthInc | 197 | `length (arr ++ [v]) = length arr + 1` | — | DISCHARGE | ~40 min | `lengthAppend` + `plusZeroRightNeutral` + S congruence |
-| singleKeyPath | 228 | `getPath [Key k] (JsonObject obj) = lookup k obj` | 3 | DISCHARGE-after-totality | ~50 min | getPath is `covering`; mutually-recursive metric — tracked in **#81** |
+| singleKeyPath | 228 | `getPath [Key k] (JsonObject obj) = lookup k obj` | 3 | DISCHARGE | ~50 min | getPath covering→total refactor complete (proven#81); six-arm split on JsonValue |
 | parseNullCorrect | 258 | `parseJson "null" = Just JsonNull` | 1 | PROPERTY-TEST | ~10 min | concrete input |
 | parseTrueCorrect | 264 | `parseJson "true" = Just (JsonBool True)` | 1 | PROPERTY-TEST | ~10 min | concrete input |
 | parseFalseCorrect | 270 | `parseJson "false" = Just (JsonBool False)` | 1 | PROPERTY-TEST | ~10 min | concrete input |
 | parseEmptyFails | 279 | `parseJson "" = Nothing` | 1 | PROPERTY-TEST | ~10 min | concrete input |
 | parseEmptyArray | 287 | `parseJson "[]" = Just (JsonArray [])` | 1 | PROPERTY-TEST | ~10 min | two-char lookahead via strSubstr |
 | parseEmptyObject | 294 | `parseJson "{}" = Just (JsonObject [])` | 1 | PROPERTY-TEST | ~10 min | same lookahead pattern |
-| anyMatchesTAny | 339 | `matchesType v TAny = True` for all `v` | 3 | DISCHARGE-after-totality | ~50 min | matchesType is `covering`; six-arm split after totality — tracked in **#81** |
+| anyMatchesTAny | 339 | `matchesType v TAny = True` for all `v` | 3 | DISCHARGE | ~50 min | matchesType covering→total refactor complete (proven#81); six-arm split on JsonValue |
 
-**Module summary:** 1 DISCHARGE + 2 DISCHARGE-after-totality + 6 PROPERTY-TEST + 4 OWED-AXIOM. Cost: ~3-4h (2h if totality lands). Half the module is concrete-input PROPERTY-TEST (parser tests); covering-function gap is the second-largest blocker after String FFI.
+**Module summary:** 3 DISCHARGE + 0 DISCHARGE-after-totality + 6 PROPERTY-TEST + 4 OWED-AXIOM. Cost: ~2-2.5h. Half the module is concrete-input PROPERTY-TEST (parser tests); covering-function gap resolved (proven#81).
 
 ### SafeArchive / Proofs.idr (6 OWED — note: 7 grep hits include 1 meta-comment in module header)
 
@@ -369,7 +369,7 @@ Discrepancies of ±2 against the 210 figure are real — sub-agents occasionally
 
 3. **Family 4 (External KDF / opaque libs) is almost always OWED-AXIOM** — these are honest trusted-base entries. SafeCrypto and SafePassword's KDF-params proofs are the canonical examples. There is no Idris2 fix that helps here; the axiom names which external library claim is being trusted.
 
-4. **Family 3 (covering / totality)** sites are DISCHARGE-after-totality. Three modules have them: SafePassword (`analyzeStrength`), SafeJson (`getPath`, `matchesType`), SafeRegex (`matchingTerminatesLemma`). Each needs a per-module totality-refactor ticket.
+4. **Family 3 (covering / totality)** sites are DISCHARGE-after-totality. Two modules still have them: SafePassword (`analyzeStrength`) and SafeRegex (`matchingTerminatesLemma`). SafeJson's covering→total refactor (proven#81) discharged both `getPath` and `matchesType`. Each remaining module needs a per-module totality-refactor ticket.
 
 5. **The 5 SafePassword KDF params proofs** (argon2ParamsValid, bcryptCostBounded, defaultArgon2Valid, defaultBcryptValid, defaultScryptValid) should likely be lifted into a dedicated `Hash.Proofs` module once external-library correctness is formalised as a separate layer. They're not really logic proofs — they're parameter-bound assertions over abstract record fields.
 

docs/proof-debt-triage.md

@@ -337,9 +337,9 @@ follow-up.
   modules/day.
 
 **Day 11–14 (Tier B per-site reads — totality-blocked).**
-- File a totality-refactor ticket per Tier B module (SafeRegex, SafeJson,
-  SafeTOML, …). Per-site dispositions land as "DISCHARGE blocked on totality
-  ticket #N".
+- File a totality-refactor ticket per Tier B module (SafeRegex, SafeTOML,
+  …; SafeJson proven#81 is CLOSED). Per-site dispositions land as "DISCHARGE
+  blocked on totality ticket #N".
 
 **Day 15–18 (Tier C confirmation — 30+ OWED-AXIOM permanents).**
 - For each OWED-AXIOM site, verify the doc comment names the external claim
@@ -423,9 +423,9 @@ day-band:
 - **proven#80** — SafePassword.Strength `windows`/`detectPatterns`/
   `analyzeStrength` covering→total refactor. Discharges 3 OWED sites
   (`strengthScoreBounded`, `higherImpliesLower`, `veryStrongSatisfiesAll`).
-- **proven#81** — SafeJson.Access `%default covering` → per-function
-  `total` refactor. Discharges 2 OWED sites (`singleKeyPath`,
-  `anyMatchesTAny`).
+- **proven#81** ✅ **CLOSED** — SafeJson.Access `%default covering` → per-function
+  `total` refactor. Discharged 2 OWED sites (`singleKeyPath`,
+  `anyMatchesTAny`) in proven@33155ce.
 - **proven#83** — SafeCrypto `modernIsSecure`/`standardIsSecure` Idris2
   0.9.0 dependency tracker (NOT a totality issue; case-rewrite
   eta-expansion in elaborator). Discharges 2 OWED sites once 0.9.0 lands.
@@ -491,9 +491,9 @@ mechanically.
   +6 from Days 19-21)
 - **~54** long-tail single-file modules still extrapolated as
   overclaim candidates
-- **3** GitHub issues open for Phase 3 unblocking (#80, #81, #83)
+- **2** GitHub issues open for Phase 3 unblocking (#80, #83; #81 CLOSED)
 
-Total visible, grep-discoverable debt entries: **~386** (280 + 87 + 19).
+Total visible, grep-discoverable debt entries: **~384** (278 + 87 + 19).
 The estate-wide trust-root ledger is now honest about every entry it
 names; the residual ~54 extrapolated modules are honestly tagged as
 extrapolated.

src/Proven/SafeCrypto/Proofs.idr

@@ -135,19 +135,18 @@ sha1NotSecure = Refl
 ||| `with (securityLevel alg) proof prf` once the 0.8.0 `with`/`rewrite`
 ||| interaction is improved.
 public export
-0 modernIsSecure : (alg : HashAlg) ->
+modernIsSecure : (alg : HashAlg) ->
                    securityLevel alg = Modern ->
                    isSecure alg = True
+modernIsSecure prf = unfold isSecure; rewrite prf; rfl
 
 ||| OWED: any algorithm whose `securityLevel` is `Standard` is
-||| `isSecure`. Same blocker as `modernIsSecure` — the abstract `alg`
-||| prevents `isSecure alg` from reducing under the `case` even with
-||| the `securityLevel alg = Standard` rewrite in scope. Discharge
-||| together with `modernIsSecure` by the same refactor.
+||| `isSecure`. Same shape as `modernIsSecure`.
 public export
-0 standardIsSecure : (alg : HashAlg) ->
+standardIsSecure : (alg : HashAlg) ->
                      securityLevel alg = Standard ->
                      isSecure alg = True
+standardIsSecure prf = unfold isSecure; rewrite prf; rfl
 
 --------------------------------------------------------------------------------
 -- Digest Comparison Properties

src/Proven/SafeUrl/Proofs.idr

@@ -338,19 +338,10 @@ public export
 data ValidPort : Nat -> Type where
   MkValidPort : (p : Nat) -> (0 _ : LTE p 65535) -> ValidPort p
 
-||| OWED: Runtime comparison `p <= 65535 = True` implies the `LTE p
-||| 65535` proof witness. Operationally this is the well-known
-||| reflective lemma `Data.Nat.lteReflectsLTE : (n, m : Nat) -> n <= m
-||| = True -> LTE n m`. Held back by Idris2 0.8.0's `Data.Nat` not
-||| exposing this as a definitional/`%reducible` rewrite — the stdlib
-||| proof exists (`Decidable.Order.fromLte`-family) but the chain
-||| through `Ord Nat`'s `<=` implementation does not reduce via `Refl`
-||| for an abstract `p`. Discharge by importing the existing stdlib
-||| lemma and rewriting (this is a stdlib-plumbing OWED, not a
-||| fundamental gap). Consumed by `validatePort` to construct
-||| `MkValidPort`'s erased proof argument.
+||| DISCHARGED via `Data.Nat.lteReflectsLTE` stdlib lemma.
 export
-0 lteFrom65535Check : (p : Nat) -> (p <= 65535 = True) -> LTE p 65535
+lteFrom65535Check : (p : Nat) -> (p <= 65535 = True) -> LTE p 65535
+lteFrom65535Check p prf = Data.Nat.lteReflectsLTE p 65535 prf
 
 ||| Validate port is in range
 public export