trees.c.inv.lean

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

1import ZlibF.Zlib.«trees.c»
2
3/-!
4# trees.c: the invariant `TreesInv` and the calculus the proofs of `trees.c` use
5
6* `Wp`, a weakest-precondition calculus for `M` (loops with a measure, `if`, `bind`).
7* `setD`, the heap after replacing a deflate record; run lemmas for the helpers of `trees.c.lean`
8  (`rd`, `md`, `getFc`, `setFc`, ...) in terms of it.
9* `TreesInv h id`: the deflate state of block `id` is well formed for the code of `trees.c` (array sizes,
10  descriptors, bit buffer, the byte block that holds `pending_buf` and `sym_buf`, the static tables).
11  `TreesBase` is the part `deflateInit2_` establishes before `_tr_init` runs; `_tr_init_safe` extends it to
12  `TreesInv`.
13* The bit stream of the output (`outBits`): the bits of the pending bytes followed by the bits of `bi_buf`.
14-/
15
16namespace Zlib.Trees.Proofs.Out
17open C Zlib.Trees
18
19/-! ## A weakest-precondition calculus for `M` -/
20
21/-- `m` runs on `h` without a fault and its result satisfies `Q`. -/
22def Wp {α : Type} (m : M α) (h : Heap) (Q : α → Heap → Prop) : Prop :=
23  ∃ a h', m h = .ok (a, h') ∧ Q a h'
24
25theorem Wp.pure' {α : Type} {a : α} {h : Heap} {Q : α → Heap → Prop} (hq : Q a h) :
26    Wp (Pure.pure a : M α) h Q := ⟨a, h, rfl, hq⟩
27
28theorem Wp.bind' {α β : Type} {m : M α} {f : α → M β} {h : Heap} {Q : α → Heap → Prop} {R : β → Heap → Prop}
29    (hm : Wp m h Q) (hf : ∀ a h', Q a h' → Wp (f a) h' R) : Wp (m >>= f) h R := by
30  obtain ⟨a, h1, e, hq⟩ := hm
31  obtain ⟨b, h2, e2, hr⟩ := hf a h1 hq
32  exact ⟨b, h2, by rw [bind_app, e]; exact e2, hr⟩
33
34theorem Wp.mono {α : Type} {m : M α} {h : Heap} {Q R : α → Heap → Prop} (hm : Wp m h Q)
35    (hr : ∀ a h', Q a h' → R a h') : Wp m h R := by
36  obtain ⟨a, h1, e, hq⟩ := hm
37  exact ⟨a, h1, e, hr a h1 hq⟩
38
39theorem Wp.ite {α : Type} {c : Prop} [Decidable c] {m1 m2 : M α} {h : Heap} {Q : α → Heap → Prop}
40    (h1 : c → Wp m1 h Q) (h2 : ¬ c → Wp m2 h Q) : Wp (if c then m1 else m2) h Q := by
41  by_cases hc : c
42  · simp only [hc, ite_true]; exact h1 hc
43  · simp only [hc, ite_false]; exact h2 hc
44
45theorem Wp.of_eq {α : Type} {m : M α} {h h' : Heap} {a : α} (e : m h = .ok (a, h')) {Q : α → Heap → Prop}
46    (hq : Q a h') : Wp m h Q := ⟨a, h', e, hq⟩
47
48theorem Wp.bind_eq {α β : Type} {m : M α} {f : α → M β} {h h1 : Heap} {a : α} {R : β → Heap → Prop}
49    (e : m h = .ok (a, h1)) (hf : Wp (f a) h1 R) : Wp (m >>= f) h R := by
50  obtain ⟨b, h2, e2, hr⟩ := hf
51  exact ⟨b, h2, by rw [bind_app, e]; exact e2, hr⟩
52
53/-- Loop with a measure: `Inv` is kept, the measure decreases at each iteration, and `Q` holds when the
54condition fails. -/
55theorem Wp.cwhile {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ} (Inv : σ → Heap → Prop) (μ : σ → Nat)
56    (Q : σ → Heap → Prop)
57    (hstep : ∀ s h, Inv s h →
58      (∃ s1 h1, cond s h = .ok ((false, s1), h1) ∧ Q s1 h1) ∨
59      (∃ s1 h1 s2 h2, cond s h = .ok ((true, s1), h1) ∧ body s1 h1 = .ok (s2, h2) ∧ Inv s2 h2 ∧ μ s2 < μ s))
60    {s : σ} {h : Heap} (hI : Inv s h) (hfuel : μ s < fuel) :
61    Wp (cwhile cond body s) h Q := by
62  have key : ∀ k n s h, Inv s h → μ s ≤ k → k < n → ∃ s' h', cwhile.go cond body n s h = .ok (s', h') ∧ Q s' h' := by
63    intro k
64    induction k using Nat.strongRecOn with
65    | _ k ih =>
66      intro n s h hI hμ hn
67      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
68      rcases hstep s h hI with ⟨s1, h1, hc, hq⟩ | ⟨s1, h1, s2, h2, hc, hb, hI2, hlt⟩
69      · exact ⟨s1, h1, by simp [cwhile.go, hc], hq⟩
70      · obtain ⟨s', h', hgo, hq⟩ := ih (μ s2) (by omega) n s2 h2 hI2 (Nat.le_refl _) (by omega)
71        exact ⟨s', h', by simp [cwhile.go, hc, hb, hgo], hq⟩
72  obtain ⟨s', h', e, hq⟩ := key (μ s) fuel s h hI (Nat.le_refl _) hfuel
73  exact ⟨s', h', e, hq⟩
74
75/-- `do ... while` with a measure: `Inv` holds before each body; the measure decreases. -/
76theorem Wp.cdoWhile {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ} (Inv : σ → Heap → Prop) (μ : σ → Nat)
77    (Q : σ → Heap → Prop)
78    (hstep : ∀ s h, Inv s h → ∃ s1 h1, body s h = .ok (s1, h1) ∧
79      ((∃ s2 h2, cond s1 h1 = .ok ((false, s2), h2) ∧ Q s2 h2) ∨
80       (∃ s2 h2, cond s1 h1 = .ok ((true, s2), h2) ∧ Inv s2 h2 ∧ μ s2 < μ s)))
81    {s : σ} {h : Heap} (hI : Inv s h) (hfuel : μ s < fuel) :
82    Wp (cdoWhile body cond s) h Q := by
83  have key : ∀ k n s h, Inv s h → μ s ≤ k → k < n → ∃ s' h', cdoWhile.go body cond n s h = .ok (s', h') ∧ Q s' h' := by
84    intro k
85    induction k using Nat.strongRecOn with
86    | _ k ih =>
87      intro n s h hI hμ hn
88      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
89      obtain ⟨s1, h1, hb, hc⟩ := hstep s h hI
90      rcases hc with ⟨s2, h2, hc, hq⟩ | ⟨s2, h2, hc, hI2, hlt⟩
91      · exact ⟨s2, h2, by simp [cdoWhile.go, hb, hc], hq⟩
92      · obtain ⟨s', h', hgo, hq⟩ := ih (μ s2) (by omega) n s2 h2 hI2 (Nat.le_refl _) (by omega)
93        exact ⟨s', h', by simp [cdoWhile.go, hb, hc, hgo], hq⟩
94  obtain ⟨s', h', e, hq⟩ := key (μ s) fuel s h hI (Nat.le_refl _) hfuel
95  exact ⟨s', h', e, hq⟩
96
97/-! ## Machine integers -/
98
99theorem i32_ofInt_toInt {v : Int} (h1 : -2147483648 ≤ v) (h2 : v ≤ 2147483647) : (Int32.ofInt v).toInt = v := by
100  rw [Int32.toInt_ofInt]
101  simp only [Int32.size, Int.bmod]
102  omega
103
104theorem ck_eq {x : Int} (h1 : -2147483648 ≤ x) (h2 : x ≤ 2147483647) : ck x = pure (Int32.ofInt x) := by
105  funext h; simp [ck, h1, h2]
106
107theorem iadd_eq {a b : Int32} (h1 : -2147483648 ≤ a.toInt + b.toInt) (h2 : a.toInt + b.toInt ≤ 2147483647) :
108    iadd a b = pure (Int32.ofInt (a.toInt + b.toInt)) := ck_eq h1 h2
109
110theorem isub_eq {a b : Int32} (h1 : -2147483648 ≤ a.toInt - b.toInt) (h2 : a.toInt - b.toInt ≤ 2147483647) :
111    isub a b = pure (Int32.ofInt (a.toInt - b.toInt)) := ck_eq h1 h2
112
113/-! ## The deflate record and its helpers -/
114
115/-- The heap after replacing the deflate record `id`. -/
116def setD (h : Heap) (id : Nat) (d : DeflateState) : Heap := { h with dstates := upd h.dstates id (some d) }
117
118@[simp] theorem setD_dstates_same (h : Heap) (id : Nat) (d : DeflateState) : (setD h id d).dstates id = some d := by
119  simp [setD]
120theorem setD_dstates_ne (h : Heap) (id k : Nat) (d : DeflateState) (hne : k ≠ id) :
121    (setD h id d).dstates k = h.dstates k := by simp [setD, hne]
122@[simp] theorem setD_bytes (h : Heap) (id : Nat) (d : DeflateState) : (setD h id d).bytes = h.bytes := rfl
123@[simp] theorem setD_words (h : Heap) (id : Nat) (d : DeflateState) : (setD h id d).words = h.words := rfl
124@[simp] theorem setD_ro (h : Heap) (id : Nat) (d : DeflateState) : (setD h id d).ro = h.ro := rfl
125@[simp] theorem setD_static (h : Heap) (id : Nat) (d : DeflateState) : (setD h id d).static = h.static := rfl
126@[simp] theorem setD_streams (h : Heap) (id : Nat) (d : DeflateState) : (setD h id d).streams = h.streams := rfl
127@[simp] theorem setD_setD (h : Heap) (id : Nat) (d d' : DeflateState) : setD (setD h id d) id d' = setD h id d' := by
128  simp [setD, upd_upd]
129
130/-- The heap after replacing the byte block `b`. -/
131def setB (h : Heap) (b : Nat) (a : Array UInt8) : Heap := { h with bytes := upd h.bytes b (some a) }
132
133@[simp] theorem setB_bytes_same (h : Heap) (b : Nat) (a : Array UInt8) : (setB h b a).bytes b = some a := by
134  simp [setB]
135theorem setB_bytes_ne (h : Heap) (b k : Nat) (a : Array UInt8) (hne : k ≠ b) : (setB h b a).bytes k = h.bytes k := by
136  simp [setB, hne]
137@[simp] theorem setB_dstates (h : Heap) (b : Nat) (a : Array UInt8) : (setB h b a).dstates = h.dstates := rfl
138@[simp] theorem setB_ro (h : Heap) (b : Nat) (a : Array UInt8) : (setB h b a).ro = h.ro := rfl
139@[simp] theorem setB_static (h : Heap) (b : Nat) (a : Array UInt8) : (setB h b a).static = h.static := rfl
140@[simp] theorem setB_words (h : Heap) (b : Nat) (a : Array UInt8) : (setB h b a).words = h.words := rfl
141@[simp] theorem setD_setB (h : Heap) (id b : Nat) (a : Array UInt8) (d : DeflateState) :
142    setD (setB h b a) id d = setB (setD h id d) b a := rfl
143
144theorem rd_run {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) :
145    rd (some (.tab id)) h = .ok (d, h) := ldDeflateState_tab e
146
147theorem md_run {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) (f : DeflateState → DeflateState) :
148    md (some (.tab id)) f h = .ok ((), setD h id (f d)) := by
149  simp [md, ldDeflateState_tab e, stDeflateState_tab e, setD]
150  try rfl
151
152theorem sid_run {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) :
153    sid (some (.tab id)) h = .ok (id, h) := by
154  simp [sid, ldDeflateState_tab e]; try rfl
155
156/-- The deflate record `id` of `h` (the default record if it is not live). -/
157def rdD (h : Heap) (id : Nat) : DeflateState := (h.dstates id).getD default
158
159theorem rd_run' {h : Heap} {id : Nat} (e : h.dstates id ≠ none) :
160    rd (some (.tab id)) h = .ok (rdD h id, h) := by
161  cases hd : h.dstates id with
162  | none => exact absurd hd e
163  | some d => simp [rdD, hd, rd_run hd]
164
165theorem md_run' {h : Heap} {id : Nat} (e : h.dstates id ≠ none) (f : DeflateState → DeflateState) :
166    md (some (.tab id)) f h = .ok ((), setD h id (f (rdD h id))) := by
167  cases hd : h.dstates id with
168  | none => exact absurd hd e
169  | some d => simp [rdD, hd, md_run hd]
170
171@[simp] theorem rdD_setD_same (h : Heap) (id : Nat) (d : DeflateState) : rdD (setD h id d) id = d := by
172  simp [rdD]
173@[simp] theorem rdD_setB (h : Heap) (id b : Nat) (a : Array UInt8) : rdD (setB h b a) id = rdD h id := rfl
174theorem setD_ne_none (h : Heap) (id : Nat) (d : DeflateState) : (setD h id d).dstates id ≠ none := by simp
175
176theorem pLtree_run {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) :
177    pLtree (some (.tab id)) h = .ok (.ref (.dstate_dyn_ltree id) 0, h) := by
178  simp [pLtree, sid_run e]; try rfl
179theorem pDtree_run {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) :
180    pDtree (some (.tab id)) h = .ok (.ref (.dstate_dyn_dtree id) 0, h) := by
181  simp [pDtree, sid_run e]; try rfl
182theorem pBltree_run {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) :
183    pBltree (some (.tab id)) h = .ok (.ref (.dstate_bl_tree id) 0, h) := by
184  simp [pBltree, sid_run e]; try rfl
185theorem pHeap_run {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) :
186    pHeap (some (.tab id)) h = .ok (.ref (.dstate_heap id) 0, h) := by
187  simp [pHeap, sid_run e]; try rfl
188theorem pDepth_run {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) :
189    pDepth (some (.tab id)) h = .ok (.ref (.dstate_depth id) 0, h) := by
190  simp [pDepth, sid_run e]; try rfl
191theorem pBlCount_run {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) :
192    pBlCount (some (.tab id)) h = .ok (.ref (.dstate_bl_count id) 0, h) := by
193  simp [pBlCount, sid_run e]; try rfl
194
195
196/-! ## The static data of `trees.c` -/
197
198/-- The static tables and descriptors of `trees.c` are installed: `install_trees` (`trees.c.lean`) provides this on
199any heap, and no function of `trees.c` changes `h.static`. -/
200def TreesStatic (st : Statics) : Prop := trees_statics st = st
201
202theorem install_trees_static (h : Heap) : TreesStatic (install_trees h).static := by
203  simp [TreesStatic, install_trees, trees_statics]
204
205theorem TreesStatic.dist_code {st : Statics} (hs : TreesStatic st) : st.dist_code = dist_code_tab := by
206  have := congrArg Statics.dist_code hs; simpa [trees_statics] using this.symm
207theorem TreesStatic.length_code {st : Statics} (hs : TreesStatic st) : st.length_code = length_code_tab := by
208  have := congrArg Statics.length_code hs; simpa [trees_statics] using this.symm
209theorem TreesStatic.base_dist {st : Statics} (hs : TreesStatic st) : st.base_dist = base_dist_tab := by
210  have := congrArg Statics.base_dist hs; simpa [trees_statics] using this.symm
211theorem TreesStatic.base_length {st : Statics} (hs : TreesStatic st) : st.base_length = base_length_tab := by
212  have := congrArg Statics.base_length hs; simpa [trees_statics] using this.symm
213theorem TreesStatic.static_ltree {st : Statics} (hs : TreesStatic st) : st.static_ltree = static_ltree_tab := by
214  have := congrArg Statics.static_ltree hs; simpa [trees_statics] using this.symm
215theorem TreesStatic.static_dtree {st : Statics} (hs : TreesStatic st) : st.static_dtree = static_dtree_tab := by
216  have := congrArg Statics.static_dtree hs; simpa [trees_statics] using this.symm
217theorem TreesStatic.extra_lbits {st : Statics} (hs : TreesStatic st) : st.extra_lbits = extra_lbits_tab := by
218  have := congrArg Statics.extra_lbits hs; simpa [trees_statics] using this.symm
219theorem TreesStatic.extra_dbits {st : Statics} (hs : TreesStatic st) : st.extra_dbits = extra_dbits_tab := by
220  have := congrArg Statics.extra_dbits hs; simpa [trees_statics] using this.symm
221theorem TreesStatic.extra_blbits {st : Statics} (hs : TreesStatic st) : st.extra_blbits = extra_blbits_tab := by
222  have := congrArg Statics.extra_blbits hs; simpa [trees_statics] using this.symm
223
224theorem dist_code_tab_size : dist_code_tab.size = 512 := by decide +kernel
225theorem length_code_tab_size : length_code_tab.size = 256 := by decide +kernel
226theorem static_ltree_tab_size : static_ltree_tab.size = 288 := by decide +kernel
227theorem static_dtree_tab_size : static_dtree_tab.size = 30 := by decide +kernel
228
229/-! ## The invariant -/
230
231/-- **What `deflateInit2_` establishes before `_tr_init` runs.** The deflate record `d` of block `id` is live and
232well formed (`dyn_ltree`, `heap`, `depth` have `HEAP_SIZE` = 573 entries, `dyn_dtree` 61, `bl_tree` 39, `bl_count`
23316); the static tables of `trees.c` are installed; `pending_buf` is the start of the writable byte block `b`, whose
234content is `buf` and whose size is `4 * lit_bufsize` (`ZALLOC(strm, lit_bufsize, LIT_BUFS)`, with
235`pending_buf_size = 4 * lit_bufsize`); `sym_buf = pending_buf + lit_bufsize` is in the same block
236(`deflate.c` L519: the overlay of the symbols on the output); `sym_end = (lit_bufsize - 1) * 3`;
237`lit_bufsize = 1 << (memLevel + 6)` lies in `128 .. 32768`; and `pending <= pending_buf_size` (zero after
238`deflateResetKeep`). -/
239structure TreesBase (h : Heap) (id : Nat) (d : DeflateState) (b : Nat) (buf : Array UInt8) : Prop where
240  dstate : h.dstates id = some d
241  wf : d.WellFormed
242  static : TreesStatic h.static
243  pbuf : d.pending_buf = .ref (.blk b) 0
244  bytes : h.bytes b = some buf
245  rw : h.ro b = false
246  size : buf.size = 4 * d.lit_bufsize.toNat
247  psize : d.pending_buf_size.toNat = buf.size
248  sym : d.sym_buf = .ref (.blk b) d.lit_bufsize.toNat
249  lit_lo : 128 ≤ d.lit_bufsize.toNat
250  lit_hi : d.lit_bufsize.toNat ≤ 32768
251  sym_end : d.sym_end.toNat = 3 * (d.lit_bufsize.toNat - 1)
252  pending_le : d.pending.toNat ≤ d.pending_buf_size.toNat
253
254/-- **What `_tr_init` adds.** The three tree descriptors point at the arrays of the record and at the static
255descriptors; the bit buffer holds `bi_valid <= 16 = Buf_size` bits (fact F9 of `docs/proof/trees.md`: `send_bits`
256shifts by at most 16) and no bit above them; the symbol count is a multiple of 3 and at most `sym_end`
257(`_tr_tally` is always followed by a flush when `sym_next == sym_end`). -/
258structure TreesRun (id : Nat) (d : DeflateState) : Prop where
259  ldyn : d.l_desc.dyn_tree = .ref (.dstate_dyn_ltree id) 0
260  lstat : d.l_desc.stat_desc = some .st_static_l_desc
261  ddyn : d.d_desc.dyn_tree = .ref (.dstate_dyn_dtree id) 0
262  dstat : d.d_desc.stat_desc = some .st_static_d_desc
263  bldyn : d.bl_desc.dyn_tree = .ref (.dstate_bl_tree id) 0
264  blstat : d.bl_desc.stat_desc = some .st_static_bl_desc
265  bi_lo : 0 ≤ d.bi_valid.toInt
266  bi_hi : d.bi_valid.toInt ≤ 16
267  bi_buf : d.bi_buf.toNat < 2 ^ d.bi_valid.toInt.toNat
268  sym_next_le : d.sym_next.toNat ≤ d.sym_end.toNat
269  sym_next_mod : d.sym_next.toNat % 3 = 0
270
271/-- The part of `TreesRun` that does not mention the symbol buffer: descriptors and bit buffer. -/
272structure TreesRun0 (id : Nat) (d : DeflateState) : Prop where
273  ldyn : d.l_desc.dyn_tree = .ref (.dstate_dyn_ltree id) 0
274  lstat : d.l_desc.stat_desc = some .st_static_l_desc
275  ddyn : d.d_desc.dyn_tree = .ref (.dstate_dyn_dtree id) 0
276  dstat : d.d_desc.stat_desc = some .st_static_d_desc
277  bldyn : d.bl_desc.dyn_tree = .ref (.dstate_bl_tree id) 0
278  blstat : d.bl_desc.stat_desc = some .st_static_bl_desc
279  bi_lo : 0 ≤ d.bi_valid.toInt
280  bi_hi : d.bi_valid.toInt ≤ 16
281  bi_buf : d.bi_buf.toNat < 2 ^ d.bi_valid.toInt.toNat
282
283theorem TreesRun.to0 {id : Nat} {d : DeflateState} (hr : TreesRun id d) : TreesRun0 id d :=
284  ⟨hr.ldyn, hr.lstat, hr.ddyn, hr.dstat, hr.bldyn, hr.blstat, hr.bi_lo, hr.bi_hi, hr.bi_buf⟩
285
286theorem TreesRun0.withSym {id : Nat} {d : DeflateState} (hr : TreesRun0 id d) (h1 : d.sym_next.toNat ≤ d.sym_end.toNat)
287    (h2 : d.sym_next.toNat % 3 = 0) : TreesRun id d :=
288  ⟨hr.ldyn, hr.lstat, hr.ddyn, hr.dstat, hr.bldyn, hr.blstat, hr.bi_lo, hr.bi_hi, hr.bi_buf, h1, h2⟩
289
290/-- **The deflate state is well formed for the code of `trees.c`**, with the byte block `b` (content `buf`) that
291holds `pending_buf` and `sym_buf`. -/
292structure TreesInvAt (h : Heap) (id : Nat) (d : DeflateState) (b : Nat) (buf : Array UInt8) : Prop where
293  base : TreesBase h id d b buf
294  run : TreesRun id d
295
296/-- `TreesInv h id`: the deflate state of block `id` is well formed for the code of `trees.c` (see `TreesInvAt`). -/
297def TreesInv (h : Heap) (id : Nat) : Prop := ∃ d b buf, TreesInvAt h id d b buf
298
299/-- Everything of the heap except the byte block `b` and the deflate record `id` is the same. -/
300structure HFrame (h h' : Heap) (b id : Nat) : Prop where
301  bytes : ∀ k, k ≠ b → h'.bytes k = h.bytes k
302  dstates : ∀ k, k ≠ id → h'.dstates k = h.dstates k
303  words : ∀ k, h'.words k = h.words k
304  ro : ∀ k, h'.ro k = h.ro k
305  streams : ∀ k, h'.streams k = h.streams k
306  gzheaders : ∀ k, h'.gzheaders k = h.gzheaders k
307  istates : ∀ k, h'.istates k = h.istates k
308  gzstates : ∀ k, h'.gzstates k = h.gzstates k
309  static : h'.static = h.static
310  nextBlk : h'.nextBlk = h.nextBlk
311  nalloc : h'.nalloc = h.nalloc
312  allocOk : h'.allocOk = h.allocOk
313  garbage : h'.garbage = h.garbage
314
315theorem HFrame.refl (h : Heap) (b id : Nat) : HFrame h h b id :=
316  ⟨fun _ _ => rfl, fun _ _ => rfl, fun _ => rfl, fun _ => rfl, fun _ => rfl, fun _ => rfl, fun _ => rfl,
317   fun _ => rfl, rfl, rfl, rfl, rfl, rfl⟩
318
319theorem HFrame.trans {h1 h2 h3 : Heap} {b id : Nat} (a : HFrame h1 h2 b id) (c : HFrame h2 h3 b id) :
320    HFrame h1 h3 b id :=
321  ⟨fun k hk => (c.bytes k hk).trans (a.bytes k hk), fun k hk => (c.dstates k hk).trans (a.dstates k hk),
322   fun k => (c.words k).trans (a.words k), fun k => (c.ro k).trans (a.ro k),
323   fun k => (c.streams k).trans (a.streams k), fun k => (c.gzheaders k).trans (a.gzheaders k),
324   fun k => (c.istates k).trans (a.istates k), fun k => (c.gzstates k).trans (a.gzstates k),
325   c.static.trans a.static, c.nextBlk.trans a.nextBlk, c.nalloc.trans a.nalloc, c.allocOk.trans a.allocOk,
326   c.garbage.trans a.garbage⟩
327
328theorem HFrame.setD (h : Heap) (b id : Nat) (d : DeflateState) : HFrame h (setD h id d) b id :=
329  ⟨fun _ _ => rfl, fun k hk => setD_dstates_ne h id k d hk, fun _ => rfl, fun _ => rfl, fun _ => rfl,
330   fun _ => rfl, fun _ => rfl, fun _ => rfl, rfl, rfl, rfl, rfl, rfl⟩
331
332theorem HFrame.setB (h : Heap) (b id : Nat) (a : Array UInt8) : HFrame h (setB h b a) b id :=
333  ⟨fun k hk => setB_bytes_ne h b k a hk, fun _ _ => rfl, fun _ => rfl, fun _ => rfl, fun _ => rfl,
334   fun _ => rfl, fun _ => rfl, fun _ => rfl, rfl, rfl, rfl, rfl, rfl⟩
335
336
337/-! ## The bit stream of the output -/
338
339/-- The low `n` bits of `v`, least significant first. -/
340def natBits (v n : Nat) : List Bool := (List.range n).map (fun i => v.testBit i)
341
342/-- The bits of the first `n` bytes of `a`, each byte least significant bit first. -/
343def bytesBits (a : Array UInt8) (n : Nat) : List Bool := (List.range n).flatMap (fun i => natBits (a.getD i 0).toNat 8)
344
345/-- **The output so far**, as a bit stream: the bits of the pending bytes `pending_buf[0 .. pending)` (each byte least
346significant bit first, as DEFLATE packs them), followed by the `bi_valid` low bits of `bi_buf` (least significant
347first). `buf` is the content of the byte block of `pending_buf`. Every bit writer of `trees.c` appends to this
348stream, and `flush_pending` moves complete bytes out of it. -/
349def outBits (buf : Array UInt8) (d : DeflateState) : List Bool :=
350  bytesBits buf d.pending.toNat ++ natBits d.bi_buf.toNat d.bi_valid.toInt.toNat
351
352@[simp] theorem natBits_length (v n : Nat) : (natBits v n).length = n := by simp [natBits]
353
354theorem natBits_add (v m n : Nat) : natBits v (m + n) = natBits v m ++ natBits (v >>> m) n := by
355  unfold natBits
356  rw [List.range_add, List.map_append, List.map_map]
357  congr 1
358  apply List.map_congr_left
359  intro i _
360  simp [Nat.testBit_shiftRight]
361
362theorem natBits_congr {v w : Nat} (n : Nat) (h : v % 2 ^ n = w % 2 ^ n) : natBits v n = natBits w n := by
363  unfold natBits
364  apply List.map_congr_left
365  intro i hi
366  have hi : i < n := List.mem_range.mp hi
367  have h1 := Nat.testBit_mod_two_pow v n i
368  rw [h] at h1
369  simp [hi] at h1
370  exact h1.symm
371
372theorem natBits_zero (n : Nat) : natBits 0 n = List.replicate n false := by
373  unfold natBits
374  apply List.ext_getElem <;> simp
375
376@[simp] theorem bytesBits_zero (a : Array UInt8) : bytesBits a 0 = [] := by simp [bytesBits]
377
378theorem bytesBits_succ (a : Array UInt8) (n : Nat) :
379    bytesBits a (n + 1) = bytesBits a n ++ natBits (a.getD n 0).toNat 8 := by
380  simp [bytesBits, List.range_succ]
381
382@[simp] theorem bytesBits_length (a : Array UInt8) (n : Nat) : (bytesBits a n).length = 8 * n := by
383  induction n with
384  | zero => simp
385  | succ n ih => rw [bytesBits_succ]; simp [ih]; omega
386
387theorem bytesBits_congr {a a' : Array UInt8} (n : Nat) (h : ∀ i, i < n → a.getD i 0 = a'.getD i 0) :
388    bytesBits a n = bytesBits a' n := by
389  induction n with
390  | zero => simp
391  | succ n ih =>
392    rw [bytesBits_succ, bytesBits_succ, ih (fun i hi => h i (by omega)), h n (by omega)]
393
394theorem bytesBits_set {a : Array UInt8} {j n : Nat} (v : UInt8) (hj : n ≤ j) :
395    bytesBits (a.set! j v) n = bytesBits a n := by
396  apply bytesBits_congr
397  intro i hi
398  rw [Array.set!_eq_setIfInBounds, Array.getD_eq_getD_getElem?, Array.getD_eq_getD_getElem?,
399    Array.getElem?_setIfInBounds]
400  have : j ≠ i := by omega
401  simp [this]
402
403end Zlib.Trees.Proofs.Out