public-get-crc-table.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
2
3namespace ZlibF.Spec.Public.Proofs
4open C
5
6set_option maxRecDepth 100000 in
7set_option maxHeartbeats 0 in
8private theorem crc_table_values : ∀ i : Fin 256,
9    Zlib.Crc32H.crc_table[i.val]? = some (ZlibF.Spec.crcByte 0 (UInt8.ofNat i.val)) := by
10  decide +kernel
11
12/-- `const z_crc_t *get_crc_table(void)` returns the read-only reflected CRC table. -/
13theorem get_crc_table : Goal.get_crc_table := by
14  intro h globals
15  refine ⟨.ref .st_crc_table 0, Zlib.Crc32H.crc_table, rfl, rfl, ?_, rfl, ?_, crc_table_values⟩
16  · simpa using globals.1
17  · decide +kernel
18
19#print axioms get_crc_table
20end ZlibF.Spec.Public.Proofs