From 28bbd20b7d1a5e63ef52c9f8b6e54f8fe88e8dc5 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 17:35:19 +0100 Subject: [PATCH] proof(SafeCBOR): DISCHARGE maxNestingDepthAnchor via Refl MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `MaxNestingDepth` is `public export` with body `64` (SafeCBOR.idr L150-152). Both sides of `MaxNestingDepth = 64` are the same `Nat` literal — `Refl` closes without unary expansion (Idris2 compares literals via Integer representation). One-line proof: - maxNestingDepthAnchor = Refl Same literal-vs-literal pattern as the SafeArchive maxCompressionRatioAnchor + maxTotalSizeAnchor pair in the prior PR. Thirteenth PR in today's overly-cautious-OWED hunt. Refs hyperpolymath/proven#90 Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Proven/SafeCBOR/Proofs.idr | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Proven/SafeCBOR/Proofs.idr b/src/Proven/SafeCBOR/Proofs.idr index faad3cf5..e6567344 100644 --- a/src/Proven/SafeCBOR/Proofs.idr +++ b/src/Proven/SafeCBOR/Proofs.idr @@ -217,6 +217,9 @@ emptyMapNoDupes = Refl -- OWED -------------------------------------------------------------------------------- -||| OWED: `MaxNestingDepth = 64`. Blocked on Nat-literal opacity. +||| DISCHARGED: `MaxNestingDepth = 64`. `MaxNestingDepth` is `public +||| export` with body `64` (SafeCBOR.idr L150-152). Both sides are +||| the same `Nat` literal — `Refl` closes without unary expansion. public export -0 maxNestingDepthAnchor : MaxNestingDepth = 64 +maxNestingDepthAnchor : MaxNestingDepth = 64 +maxNestingDepthAnchor = Refl