public-crc-updates.lean

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

1import ZlibF.Spec.Public.Checksums
2import ZlibF.Proof.«crc32.c.views»
3
4/-!
5# Complete public CRC update results
6
7The public buffer relation includes every represented byte-array view,
8zero-length one-past reads, and null initial-value queries of any length.
9The actual views theorems retain arbitrary address residues and seeds.
10-/
11
12namespace ZlibF.Spec.Public.Proofs
13open C
14
15/-- `uLong crc32_z(uLong crc, const Bytef *buf, z_size_t len)`.
16Every public readable buffer and null query has its exact CRC result,
17without changing any heap field. -/
18theorem crc32_z : Goal.crc32_z := by
19  intro h seed pointer length bytes globals readable
20  rcases readable with ⟨rfl,rfl⟩ | ⟨ref,offset,data,rfl,get,bounds,rfl⟩
21  · simpa only [ite_true] using Zlib.Crc32.Proofs.crc32_z_null h seed length
22  · simpa only [reduceCtorEq,ite_false] using
23      Zlib.Crc32.Proofs.crc32_z_all_byte_views h globals seed ref offset data get length bounds
24
25/-- `uLong crc32(uLong crc, const Bytef *buf, uInt len)`.
26The compatibility entry retains the full public buffer domain, every
2732-bit length and seed, and the complete immutable-heap result. -/
28theorem crc32 : Goal.crc32 := by
29  intro h seed pointer length bytes globals readable
30  rcases readable with ⟨rfl,rfl⟩ | ⟨ref,offset,data,rfl,get,bounds,rfl⟩
31  · simpa only [ite_true] using Zlib.Crc32.Proofs.crc32_null h seed length
32  · simpa only [reduceCtorEq,ite_false] using
33      Zlib.Crc32.Proofs.crc32_all_byte_views h globals seed ref offset data get length bounds
34
35end ZlibF.Spec.Public.Proofs