adler32.c.public-block.lean

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

1import ZlibF.Proof.«public-adler-combine»
2import ZlibF.Proof.«adler32.c.public-one»
3
4namespace Zlib.Adler32.Proofs
5open C Zlib.Adler32 Zlib.Adler32.Spec
6
7def canonicalStart (a : UInt64) : UInt32 :=
8  UInt32.ofNat (a.toNat % 65536 % 65521 + 65536 * (a.toNat / 65536 % 65536 % 65521))
9
10theorem adler_format_seed (a : UInt64) (bs : List UInt8) :
11    ZlibF.Spec.adler32Update (canonicalStart a) bs =
12      UInt32.ofNat (Zlib.Adler32.Spec.adler32 a.toNat bs) := by
13  have h := adler_fold_components bs (a.toNat % 65536 % 65521)
14    (a.toNat / 65536 % 65536 % 65521) (Nat.mod_lt _ (by decide)) (Nat.mod_lt _ (by decide))
15  simpa [canonicalStart, Zlib.Adler32.Spec.adler32, Zlib.Adler32.Spec.BASE] using h
16
17theorem adler32_z_block_format {h : Heap} {blk : Nat} {bytes : Array UInt8}
18    (hb : h.bytes blk = some bytes) (a : UInt64) (off L : Nat)
19    (hfit : off + L ≤ bytes.size) (hL : L < 2 ^ 64) (h1 : L ≠ 1) :
20    C.run (adler32_z a (.ref (.blk blk) off) L.toUInt64) h =
21      .ok ((ZlibF.Spec.adler32Update (canonicalStart a) (seg bytes off L)).toUInt64, h) := by
22  obtain ⟨r, hr, hv⟩ := adler32_z_correct_ne_one h blk bytes hb a off L hfit hL h1
23  rw [hr]
24  congr 2
25  apply UInt64.toNat_inj.mp
26  rw [UInt32.toNat_toUInt64, adler_format_seed, UInt32.toNat_ofNat', hv]
27  have h := sums_lt (a.toNat % 65536 % 65521) (a.toNat / 65536 % 65536 % 65521)
28    (seg bytes off L) (Nat.mod_lt _ (by decide)) (Nat.mod_lt _ (by decide))
29  change (sums _ _ _).1 < 65521 ∧ (sums _ _ _).2 < 65521 at h
30  have he : Zlib.Adler32.Spec.adler32 a.toNat (seg bytes off L) < 2 ^ 32 := by
31    unfold Zlib.Adler32.Spec.adler32
32    simp only [Zlib.Adler32.Spec.BASE]
33    omega
34  exact (Nat.mod_eq_of_lt he).symm
35
36
37theorem seg_eq_slice (bytes : Array UInt8) (off L : Nat) (hfit : off + L ≤ bytes.size) :
38    seg bytes off L = (bytes.toList.drop off).take L := by
39  apply List.ext_getElem
40  · have hlen : L ≤ bytes.size - off := by omega
41    simp [seg, List.length_take, List.length_drop, Nat.min_eq_left hlen]
42  · intro i hi hj
43    have hlen : i < L := by simpa [seg] using hi
44    have hidx : off + i < bytes.size := by omega
45    simp only [seg, List.getElem_map, List.getElem_range, List.getElem_take,
46      List.getElem_drop, Array.getElem_toList]
47    exact (getElem_eq_bang bytes (off+i) hidx).symm
48
49#print axioms adler32_z_block_format
50#print axioms seg_eq_slice
51end Zlib.Adler32.Proofs