crc-static-address.lean

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

1import ZlibF.Proof.«public-crc-updates»
2import ZlibF.Spec.Public.Domains
3
4/-!
5# Static-byte-view CRC regression
6
7The witness and 47-byte input are identical to the former address-model
8counterexample. Both actual public entries now return the independent CRC
9update and preserve the same heap.
10-/
11open C Zlib.Crc32 Zlib.Crc32.Proofs ZlibF.Spec.Public
12
13def crcWitness : Heap := witnessHeap
14
15def crcWitnessBytes : List UInt8 := (crcWitness.static.dist_code.toList.drop 0).take 47
16
17theorem crc_witness_globals : CrcGlobals crcWitness := by
18  simp [CrcGlobals, crcWitness, witnessHeap, Zlib.Crc32.initStatics]
19
20theorem crc_witness_buffer :
21    BufferBytes crcWitness (.ref .st_dist_code 0) 47 crcWitnessBytes := by
22  right
23  refine ⟨.st_dist_code, 0, crcWitness.static.dist_code, rfl, ?_, ?_, rfl⟩
24  · rfl
25  · decide +kernel
26
27
28/-- The unchanged static-view witness has the exact independent checksum. -/
29theorem crc_witness_correct :
30    C.run (crc32_z 0 (.ref .st_dist_code 0) 47) crcWitness =
31      .ok ((ZlibF.Spec.crc32Update 0 crcWitnessBytes).toUInt64,crcWitness) := by
32  have result := ZlibF.Spec.Public.Proofs.crc32_z crcWitness 0 (.ref .st_dist_code 0) 47
33    crcWitnessBytes crc_witness_globals crc_witness_buffer
34  simpa only [reduceCtorEq,ite_false,show (0 : UInt64).toUInt32 = (0 : UInt32) by decide] using result
35
36/-- The 32-bit-length compatibility entry returns the same exact value. -/
37theorem crc32_witness_correct :
38    C.run (crc32 0 (.ref .st_dist_code 0) 47) crcWitness =
39      .ok ((ZlibF.Spec.crc32Update 0 crcWitnessBytes).toUInt64,crcWitness) := by
40  have result := ZlibF.Spec.Public.Proofs.crc32 crcWitness 0 (.ref .st_dist_code 0) 47
41    crcWitnessBytes crc_witness_globals crc_witness_buffer
42  simpa only [reduceCtorEq,ite_false,show (0 : UInt64).toUInt32 = (0 : UInt32) by decide] using result
43
44#print axioms crc_witness_correct
45#print axioms crc32_witness_correct