From ffb5566e0a1c9c412cbbe19f966e45926fff8760 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 17:34:05 +0100 Subject: [PATCH] proof(SafeChecksum): DISCHARGE crc32PolynomialIsIEEE via Refl MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `crc32Polynomial` is `public export` with body `0xEDB88320` in SafeChecksum.idr L21-23. Bits32 literal equality is primitive — both sides of `crc32Polynomial = 0xEDB88320` reduce to the same literal and `Refl` closes. The OWED's "numeric-literal opaque under Bits32" only applies to REDUCING `crc32Polynomial` to a *different* literal; here LHS and RHS are the same literal so the blocker doesn't apply. One-line proof: - crc32PolynomialIsIEEE = Refl Eleventh PR in today's overly-cautious-OWED hunt. Refs hyperpolymath/proven#90 Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Proven/SafeChecksum/Proofs.idr | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/Proven/SafeChecksum/Proofs.idr b/src/Proven/SafeChecksum/Proofs.idr index 2ec3ef07..603466c4 100644 --- a/src/Proven/SafeChecksum/Proofs.idr +++ b/src/Proven/SafeChecksum/Proofs.idr @@ -52,12 +52,15 @@ import Data.Bits -------------------------------------------------------------------------------- ||| OWED: CRC32 polynomial is the IEEE 802.3 bit-reversed value -||| `0xEDB88320`. Held back by Idris2 0.8.0 not reducing the named -||| `crc32Polynomial : Bits32` constant to its literal value by Refl -||| alone (numeric-literal opaque under `Bits32`). Discharge once a -||| `Data.Bits` reflective tactic is available. +||| `0xEDB88320`. DISCHARGED: `crc32Polynomial` is `public export` +||| with body `0xEDB88320` (SafeChecksum.idr L21-23). `Bits32` literal +||| equality is primitive — both sides reduce to the same literal and +||| `Refl` closes. The "numeric-literal opaque under Bits32" cited in +||| the OWED only applies to REDUCING `crc32Polynomial` to a *different* +||| literal; here LHS and RHS are the same literal. public export -0 crc32PolynomialIsIEEE : crc32Polynomial = 0xEDB88320 +crc32PolynomialIsIEEE : crc32Polynomial = 0xEDB88320 +crc32PolynomialIsIEEE = Refl ||| OWED: Adler-32 modulus is `65521`, the largest prime less than ||| `2^16` (the choice is load-bearing — primality is what gives