From 777ccb40be50fbb871e24fe8277e99b3f498dd08 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 16:28:38 +0100 Subject: [PATCH] proof(SafeGit): DISCHARGE forbiddenRefCharsAnchor via Refl MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `forbiddenRefChars` is `public export` in SafeGit.idr L24-26 with this exact list literal as its body. The elaborator unfolds the LHS to the RHS for `Refl`. No "Char-list reduction" is needed — both sides are the same literal after `public export` unfolding. One-line proof: - forbiddenRefCharsAnchor = Refl Conversion: - `0 forbiddenRefCharsAnchor : ...` (type-only OWED) → `public export forbiddenRefCharsAnchor : ... = Refl` Same "OWED comment was overly cautious" pattern as the prior 7 discharges this session (#97, #98, #99, #100, #101). The other 2 SafeGit OWEDs (emptyRefNameInvalid, refNameExtracts) DO have real String-FFI / auto-implicit blockers per their OWED comments and are out of scope. Refs hyperpolymath/proven#90 Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Proven/SafeGit/Proofs.idr | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/Proven/SafeGit/Proofs.idr b/src/Proven/SafeGit/Proofs.idr index c86a4b46..d20eb11a 100644 --- a/src/Proven/SafeGit/Proofs.idr +++ b/src/Proven/SafeGit/Proofs.idr @@ -12,11 +12,15 @@ import Proven.SafeGit %default total -||| OWED: spec anchor — 9 ref characters are forbidden by -||| git-check-ref-format. Blocked on Char-list reduction. +||| DISCHARGED: spec anchor — the 9 ref characters forbidden by +||| git-check-ref-format. `forbiddenRefChars` is `public export` with +||| this exact list literal as its body (SafeGit.idr L24-26), so the +||| elaborator unfolds the LHS to the RHS for `Refl`. No "Char-list +||| reduction" is needed — both sides are the same list literal. public export -0 forbiddenRefCharsAnchor : +forbiddenRefCharsAnchor : forbiddenRefChars = [' ', '~', '^', ':', '?', '*', '[', '\\', '\x7F'] +forbiddenRefCharsAnchor = Refl -------------------------------------------------------------------------------- -- OWED postulates