inffast.c.sig.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«inffast.c.match»
2import ZlibF.Spec.Format
3
4/-!
5# inffast.c: the bit stream that the bit buffer and the input pointer stand for
6
7`bitsOfNat H b` is the list of the low `b` bits of `H`, least significant first (the order in which the bits of the
8buffer are consumed). `Sg e H b i` is the bit sequence of a state of `inflate_fast`: the `b` bits of the buffer `H`,
9then the bits of the input bytes from offset `i` to the end of the input range. Reading a byte into the buffer, and
10dropping bits, do not change the sequence (up to the dropped bits).
11-/
12
13namespace Zlib.Inffast.Proofs
14open C Zlib.Inffast Zlib.Inffast.Spec
15
16open ZlibF.Spec
17
18/-- The low `b` bits of `H`, least significant first. -/
19def bitsOfNat (H b : Nat) : List Bool := (List.range b).map fun j => H.testBit j
20
21theorem bitsOfNat_length (H b : Nat) : (bitsOfNat H b).length = b := by simp [bitsOfNat]
22
23theorem bitsOfNat_succ (H b : Nat) : bitsOfNat H (b + 1) = H.testBit 0 :: bitsOfNat (H / 2) b := by
24  unfold bitsOfNat
25  rw [List.range_succ_eq_map]
26  simp [Function.comp_def, Nat.testBit_div_two]
27
28theorem bitsOfNat_zero (H : Nat) : bitsOfNat H 0 = [] := rfl
29
30theorem bitsOfNat_drop (H b k : Nat) (hk : k ≤ b) : bitsOfNat (H / 2 ^ k) (b - k) = (bitsOfNat H b).drop k := by
31  apply List.ext_getElem
32  · simp [bitsOfNat_length]
33  · intro n h1 h2
34    simp only [bitsOfNat, List.getElem_map, List.getElem_range, List.getElem_drop, Nat.testBit_div_two_pow]
35    rw [Nat.add_comm]
36
37theorem readBits_bitsOfNat : ∀ (x b H : Nat) (r : List Bool), x ≤ b →
38    readBits x (bitsOfNat H b ++ r) = some (H % 2 ^ x, bitsOfNat (H / 2 ^ x) (b - x) ++ r)
39  | 0, b, H, r, _ => by simp [readBits, Nat.mod_one]
40  | x + 1, b, H, r, hx => by
41    obtain ⟨b, rfl⟩ : ∃ b', b = b' + 1 := ⟨b - 1, by omega⟩
42    rw [bitsOfNat_succ]
43    simp only [List.cons_append, readBits]
44    rw [readBits_bitsOfNat x b (H / 2) r (by omega)]
45    simp only
46    have h1 : H / 2 / 2 ^ x = H / 2 ^ (x + 1) := by rw [Nat.div_div_eq_div_mul, Nat.pow_succ, Nat.mul_comm]
47    have h2 : (if H.testBit 0 then 1 else 0) + 2 * (H / 2 % 2 ^ x) = H % 2 ^ (x + 1) := by
48      rw [Nat.pow_succ', Nat.mod_mul]
49      have : (if H.testBit 0 then 1 else 0) = H % 2 := by
50        rw [Nat.testBit_zero]
51        by_cases h : H % 2 = 1
52        · simp [h]
53        · have : H % 2 = 0 := by omega
54          simp [this]
55      rw [this]
56    rw [h1, h2, show b + 1 - (x + 1) = b - x by omega]
57
58variable (e : Env)
59
60/-- The bits of the input bytes from offset `i` to the end of the input range. -/
61def inBits (i : Nat) : List Bool :=
62  bytesToBits ((e.IN.toList.drop i).take (e.i0 + e.sm0.avail_in.toNat - i))
63
64/-- The bit sequence of a state: the bits of the buffer, then the bits of the unread input. -/
65def Sg (H b i : Nat) : List Bool := bitsOfNat H b ++ inBits e i
66
67theorem inBits_pull (i : Nat) (hi : i < e.i0 + e.sm0.avail_in.toNat) :
68    inBits e i = byteBits (e.IN.getD i 0) ++ inBits e (i + 1) := by
69  have hsz := e.hINsz
70  unfold inBits
71  have h1 : e.i0 + e.sm0.avail_in.toNat - i = (e.i0 + e.sm0.avail_in.toNat - (i + 1)) + 1 := by omega
72  rw [h1]
73  have hlt : i < e.IN.toList.length := by simp; omega
74  rw [List.drop_eq_getElem_cons hlt, List.take_succ_cons]
75  simp only [bytesToBits, List.flatMap_cons]
76  congr 1
77  simp [Array.getD_eq_getD_getElem?, show i < e.IN.size by omega]
78
79theorem Sg_pull (H b i : Nat) (hH : H < 2 ^ b) (hi : i < e.i0 + e.sm0.avail_in.toNat) :
80    Sg e (H + (e.IN.getD i 0).toNat * 2 ^ b) (b + 8) (i + 1) = Sg e H b i := by
81  unfold Sg
82  rw [inBits_pull e i hi]
83  have key : bitsOfNat (H + (e.IN.getD i 0).toNat * 2 ^ b) (b + 8) = bitsOfNat H b ++ byteBits (e.IN.getD i 0) := by
84    unfold bitsOfNat byteBits
85    rw [List.range_add, List.map_append]
86    congr 1
87    · apply List.map_congr_left
88      intro j hj
89      have hj' : j < b := List.mem_range.mp hj
90      rw [Nat.add_comm H, Nat.mul_comm, Nat.testBit_two_pow_mul_add _ hH]
91      simp [hj']
92    · rw [List.map_map]
93      apply List.map_congr_left
94      intro j hj
95      simp only [Function.comp_apply]
96      rw [Nat.add_comm H, Nat.mul_comm, Nat.testBit_two_pow_mul_add _ hH]
97      have hnl : ¬ (b + j < b) := by omega
98      simp [hnl]
99  rw [key, List.append_assoc]
100
101end Zlib.Inffast.Proofs