Crc32ByteViews.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«crc32.c»
2
3/-!
4# CRC correctness on every represented byte-array view
5
6The heap's non-block base residues are universally quantified. The caller
7supplies readable bytes, not an alignment restriction or a callee contract.
8The independent checksum definition remains unchanged.
9-/
10
11namespace Zlib.Crc32.Spec.ByteViews
12open C Zlib.Crc32.Proofs
13
14/-- `uLong crc32_z(uLong crc, const unsigned char *buf, z_size_t len)`.
15All represented byte arrays and every origin residue are included. This
16retains the existing raw theorem's full length and arithmetic domain. -/
17def Goal.crc32_z_all_byte_views : Prop :=
18  ∀ (h : Heap), StaticsOK h →
19    ∀ (crc : UInt64) (ref : BRef) (offset : Nat) (bytes : Array UInt8),
20      Space.get h ref = some bytes →
21      ∀ len : UInt64, offset + len.toNat ≤ bytes.size →
22        C.run (crc32_z crc (.ref ref offset) len) h =
23          .ok ((ZlibF.Spec.crc32Update crc.toUInt32
24            ((bytes.toList.drop offset).take len.toNat)).toUInt64, h)
25
26/-- `uLong crc32(uLong crc, const unsigned char *buf, uInt len)`.
27The compatibility wrapper has the same view and origin coverage. -/
28def Goal.crc32_all_byte_views : Prop :=
29  ∀ (h : Heap), StaticsOK h →
30    ∀ (crc : UInt64) (ref : BRef) (offset : Nat) (bytes : Array UInt8),
31      Space.get h ref = some bytes →
32      ∀ len : UInt32, offset + len.toNat ≤ bytes.size →
33        C.run (crc32 crc (.ref ref offset) len) h =
34          .ok ((ZlibF.Spec.crc32Update crc.toUInt32
35            ((bytes.toList.drop offset).take len.toNat)).toUInt64, h)
36
37end Zlib.Crc32.Spec.ByteViews