参考文档 / ZLIB × LEAN

public-get-crc-table.lean

此页源文件快照 · a87a89435fd10690 · 对应提交的原文 ↗

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

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