Skip to content

proof(SafeChecksum): DISCHARGE crc32PolynomialIsIEEE via Refl (proven#90, #107) #108

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
May 30, 2026
Merged

proof(SafeChecksum): DISCHARGE crc32PolynomialIsIEEE via Refl (proven#90, #107) #108

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 8 additions & 5 deletions src/Proven/SafeChecksum/Proofs.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading