From 63d2be0b2a63274bcf526193e50672c2f0d2547c Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 31 May 2026 06:50:28 +0000 Subject: [PATCH] =?UTF-8?q?chore(state):=20STATE.a2ml=20=E2=80=94=20record?= =?UTF-8?q?=20#144=20SafeJson=20discharges=20+=20#145=20CI-gating=20findin?= =?UTF-8?q?g?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - discharged-decls 34 -> 36 (anyMatchesTAny, singleKeyPath via #144) - last-updated -> 2026-05-31 - session-history: appendLengthInc root cause (contrib lengthSnoc is element-first; #127's `lengthSnoc arr v` blocked the whole SafeJson.Proofs module) + the #145 CI-gating finding. https://claude.ai/code/session_01MN5vzRR4MK2dkDNaHqqRDy --- .machine_readable/6a2/STATE.a2ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 1592c98c..32fd319a 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -4,7 +4,7 @@ [metadata] project = "proven" version = "0.1.0" -last-updated = "2026-05-30" +last-updated = "2026-05-31" status = "active" [project-context] @@ -30,10 +30,11 @@ bodyless-decls-total = 256 # SafeChecksum convention. See PROOF-NEEDS.md "OWED-with-justification # convention" and META.a2ml ADR-001. -discharged-decls = 34 +discharged-decls = 36 # DISCHARGED entries (OWED → proven Refl or contrib-lemma) landed -# across Phase 3 PRs #97-124 (2026-05-30 session). Each PR converts -# one OWED to a machine-checked theorem. +# across Phase 3 PRs #97-124 (2026-05-30 session) + #144 (2026-05-31: +# SafeJson anyMatchesTAny, singleKeyPath). Each PR converts one OWED to +# a machine-checked theorem. [trust-posture] believe-me-uses = 0 @@ -65,6 +66,7 @@ scorecard-fuzzing-source-fixed = "PR #121 (real ClusterFuzzLite + cargo-fuzz)" [session-history] # Most recent first. +"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)" "2026-05-19" = "Six new modules merged with explicit OWED markers (SafeChecksum, SafeBuffer, SafeBloom, SafeCryptoAccel, SafeHKDF, SafeFPGA) — convention-setting"