inflate.c.main.bits.lean

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

1import ZlibF.Proof.«inflate.c.base»
2import ZlibF.Spec.Format
3
4/-!
5# inflate.c: bit-list algebra and the shift lemmas of the bit buffer
6
7Heap-free. `natBits k n` is the low `k` bits of `n`, least significant first; `bytesBits` is the DEFLATE bit sequence of a byte
8list (RFC 1951, 3.1.1). `bytesBits_eq_bytesToBits` ties it to the format specification `ZlibF.Spec.bytesToBits`.
9The shift lemmas say when `<<<` and `>>>` of the translation are the arithmetic they look like.
10-/
11
12namespace Zlib.Inflate.Proofs
13
14/-- The low `k` bits of `n`, least significant first. -/
15def natBits : Nat → Nat → List Bool
16  | 0, _ => []
17  | k + 1, n => (n % 2 == 1) :: natBits k (n / 2)
18
19/-- Bytes as a DEFLATE bit stream (each byte least significant bit first). -/
20def bytesBits (bs : List UInt8) : List Bool := bs.flatMap fun b => natBits 8 b.toNat
21
22theorem natBits_length : ∀ k n, (natBits k n).length = k
23  | 0, _ => rfl
24  | k + 1, n => by simp [natBits, natBits_length k]
25
26theorem natBits_add : ∀ k m n, natBits (k + m) n = natBits k n ++ natBits m (n / 2 ^ k)
27  | 0, m, n => by simp [natBits]
28  | k + 1, m, n => by
29    rw [show k + 1 + m = (k + m) + 1 by omega]
30    simp only [natBits, natBits_add k m (n / 2), List.cons_append, Nat.div_div_eq_div_mul,
31      Nat.pow_succ]
32    rw [Nat.mul_comm 2 (2 ^ k)]
33
34theorem natBits_mod : ∀ k n, natBits k (n % 2 ^ k) = natBits k n
35  | 0, _ => rfl
36  | k + 1, n => by
37    simp only [natBits]
38    have h1 : n % 2 ^ (k + 1) % 2 = n % 2 := by
39      rw [Nat.pow_succ, Nat.mod_mul_left_mod]
40    have h2 : n % 2 ^ (k + 1) / 2 = (n / 2) % 2 ^ k := by
41      rw [Nat.pow_succ, Nat.mul_comm, Nat.mod_mul_right_div_self]
42    rw [h1, h2, natBits_mod k]
43
44theorem natBits_take (k n j : Nat) (hj : j ≤ k) : (natBits k n).take j = natBits j n := by
45  obtain ⟨m, rfl⟩ : ∃ m, k = j + m := ⟨k - j, by omega⟩
46  rw [natBits_add, List.take_append_of_le_length (by simp [natBits_length])]
47  exact List.take_of_length_le (by simp [natBits_length])
48
49theorem natBits_drop (k n j : Nat) (hj : j ≤ k) :
50    (natBits k n).drop j = natBits (k - j) (n / 2 ^ j) := by
51  obtain ⟨m, rfl⟩ : ∃ m, k = j + m := ⟨k - j, by omega⟩
52  rw [natBits_add, List.drop_append_of_le_length (by simp [natBits_length])]
53  simp [natBits_length]
54
55/-- `hold += b << bits; bits += 8` appends the byte's bits. -/
56theorem natBits_pull (bits hold b : Nat) (hh : hold < 2 ^ bits) (hb : b < 256) :
57    natBits (bits + 8) (hold + b * 2 ^ bits) = natBits bits hold ++ natBits 8 b := by
58  rw [natBits_add]
59  have h1 : natBits bits (hold + b * 2 ^ bits) = natBits bits hold := by
60    rw [← natBits_mod bits (hold + b * 2 ^ bits), ← natBits_mod bits hold]
61    congr 1
62    rw [Nat.add_mul_mod_self_right]
63  have h2 : (hold + b * 2 ^ bits) / 2 ^ bits = b := by
64    rw [Nat.add_mul_div_right _ _ (Nat.two_pow_pos bits), Nat.div_eq_of_lt hh, Nat.zero_add]
65  rw [h1, h2]
66
67theorem bytesBits_nil : bytesBits [] = [] := rfl
68
69theorem bytesBits_cons (b : UInt8) (bs : List UInt8) :
70    bytesBits (b :: bs) = natBits 8 b.toNat ++ bytesBits bs := by
71  simp [bytesBits]
72
73theorem bytesBits_append (xs ys : List UInt8) :
74    bytesBits (xs ++ ys) = bytesBits xs ++ bytesBits ys := by
75  simp [bytesBits]
76
77theorem bytesBits_length (bs : List UInt8) : (bytesBits bs).length = 8 * bs.length := by
78  induction bs with
79  | nil => rfl
80  | cons b bs ih => rw [bytesBits_cons]; simp [natBits_length, ih]; omega
81
82theorem bytesBits_drop (bs : List UInt8) (j : Nat) :
83    (bytesBits bs).drop (8 * j) = bytesBits (bs.drop j) := by
84  induction bs generalizing j with
85  | nil => simp [bytesBits]
86  | cons b bs ih =>
87    cases j with
88    | zero => simp
89    | succ j =>
90      rw [bytesBits_cons, show 8 * (j + 1) = 8 + 8 * j by omega, ← List.drop_drop,
91        List.drop_append_of_le_length (by simp [natBits_length]),
92        List.drop_eq_nil_of_le (as := natBits 8 b.toNat) (by simp [natBits_length]),
93        List.nil_append, ih]
94      simp
95
96theorem natBits_testBit : ∀ k n, natBits k n = (List.range k).map fun i => n.testBit i
97  | 0, _ => rfl
98  | k + 1, n => by
99    rw [List.range_succ_eq_map, List.map_cons, List.map_map, natBits, natBits_testBit k (n / 2)]
100    congr 1
101    · by_cases h : n % 2 = 1 <;> simp [Nat.testBit_zero, h]
102    · apply List.map_congr_left
103      intro i _
104      simp [Function.comp, Nat.testBit_succ]
105
106/-- `bytesBits` is the bit sequence of the format specification. -/
107theorem bytesBits_eq_bytesToBits (bs : List UInt8) : ZlibF.Spec.bytesToBits bs = bytesBits bs := by
108  unfold ZlibF.Spec.bytesToBits bytesBits
109  congr 1; funext b
110  rw [natBits_testBit]
111  rfl
112
113/-! ## The shifts of the bit buffer -/
114
115open C Zlib.Inflate
116
117theorem shl32_run (x n : UInt32) (hn : n.toNat < 32) : shl32 x n = pure (x <<< n) := by
118  have : n < 32 := UInt32.lt_iff_toNat_lt.mpr (by simpa using hn)
119  simp [shl32, this]
120
121theorem shr32_run (x n : UInt32) (hn : n.toNat < 32) : shr32 x n = pure (x >>> n) := by
122  have : n < 32 := UInt32.lt_iff_toNat_lt.mpr (by simpa using hn)
123  simp [shr32, this]
124
125theorem shl64_run (x : UInt64) (n : UInt32) (hn : n.toNat < 64) : shl64 x n = pure (x <<< n.toUInt64) := by
126  have : n < 64 := UInt32.lt_iff_toNat_lt.mpr (by simpa using hn)
127  simp [shl64, this]
128
129theorem shr64_run (x : UInt64) (n : UInt32) (hn : n.toNat < 64) : shr64 x n = pure (x >>> n.toUInt64) := by
130  have : n < 64 := UInt32.lt_iff_toNat_lt.mpr (by simpa using hn)
131  simp [shr64, this]
132
133theorem shr64_toNat (x : UInt64) (n : UInt32) (hn : n.toNat < 64) :
134    (x >>> n.toUInt64).toNat = x.toNat / 2 ^ n.toNat := by
135  rw [UInt64.toNat_shiftRight]
136  simp only [UInt32.toNat_toUInt64]
137  rw [Nat.mod_eq_of_lt hn, Nat.shiftRight_eq_div_pow]
138
139theorem shl64_toNat (x : UInt64) (n : UInt32) (hn : n.toNat < 64)
140    (hx : x.toNat * 2 ^ n.toNat < 2 ^ 64) :
141    (x <<< n.toUInt64).toNat = x.toNat * 2 ^ n.toNat := by
142  rw [UInt64.toNat_shiftLeft]
143  simp only [UInt32.toNat_toUInt64]
144  rw [Nat.mod_eq_of_lt hn, Nat.shiftLeft_eq]
145  exact Nat.mod_eq_of_lt hx
146
147theorem shl32_one_toNat (n : UInt32) (hn : n.toNat < 32) : ((1 : UInt32) <<< n).toNat = 2 ^ n.toNat := by
148  rw [UInt32.toNat_shiftLeft]
149  simp only [UInt32.toNat_one]
150  rw [Nat.mod_eq_of_lt (by omega : n.toNat < 32), Nat.shiftLeft_eq, Nat.one_mul]
151  exact Nat.mod_eq_of_lt (by
152    calc 2 ^ n.toNat < 2 ^ 32 := Nat.pow_lt_pow_right (by decide) hn
153      _ = UInt32.size := rfl)
154
155/-- `(1U << n) - 1` is the mask of `n` low bits. -/
156theorem mask_toNat (n : UInt32) (hn : n.toNat < 32) : ((1 : UInt32) <<< n - 1).toNat = 2 ^ n.toNat - 1 := by
157  have h := shl32_one_toNat n hn
158  have hpos : 1 ≤ 2 ^ n.toNat := Nat.one_le_two_pow
159  rw [UInt32.toNat_sub_of_le]
160  · rw [h]; rfl
161  · rw [UInt32.le_iff_toNat_le, h]; exact hpos
162
163theorem land_mask32 (x : UInt32) (k : Nat) (m : UInt32) (hm : m.toNat = 2 ^ k - 1) :
164    (x &&& m).toNat = x.toNat % 2 ^ k := by
165  rw [UInt32.toNat_and, hm, Nat.and_two_pow_sub_one_eq_mod]
166
167end Zlib.Inflate.Proofs