infback.c.macros.lean

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

1import ZlibF.Proof.«infback.c.back»
2import ZlibF.Proof.«inflate.c.main.macros»
3
4/-!
5# infback.c: the input macros with the call-back `in`
6
7`PULL`, `PULLBYTE` and `NEEDBITS` of `inflateBack()`. The bit algebra (`BitInv`, `PULLBYTE_succ`, `BITS_run`, `DROPBITS_run`,
8`BYTEBITS_run`) is the one of `inflate()` (module `inflate.c.main.macros`): `PULLBYTE` of `infback.c` differs only in that
9`PULL` may call `in` when no input is left.
10
11The registers describe the rest `bs` of the chunk that `in` returned last (`BIn`); the chunk is in a block of `in` (`ownI`),
12so `out`, the writes into the window and the record tables cannot change it.
13-/
14
15namespace Zlib.Infback.Spec
16open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs
17
18/-- The registers describe the bytes `bs` left of the current chunk (`BitInv`), and a non-empty chunk is in an `ownI` block. -/
19structure BIn (ownI : Nat → Prop) (h : Heap) (l : IL) (bs : List UInt8) : Prop where
20  bit : BitInv h l bs
21  own : bs = [] ∨ ∃ b off, l.next = .ref (.blk b) off ∧ ownI b
22
23/-- The input is finite: a measure `μ` of what `in` can still deliver (it depends only on the blocks of `in`), and a call that
24returns `n` bytes lowers it by at least `n`. Without it `inflateBack` may run for ever: zlib.h does not promise that `in`
25eventually reports the end of input, and the model then runs out of fuel. -/
26structure InFinite (c : BCtx) (ownI : Nat → Prop) (R : Heap → Prop) (μ : Heap → Nat) : Prop where
27  step : ∀ h nx n nx' h', R h → c.inCb c.inDesc nx h = .ok ((n, nx'), h') → μ h' + n.toNat ≤ μ h
28  local_ : ∀ h h', (∀ b, ownI b → h'.bytes b = h.bytes b) → μ h' = μ h
29
30/-- The input still to be read: the bits held, the bytes of the chunk, and what `in` can still deliver (in bits). -/
31def phi (μ : Heap → Nat) (h : Heap) (l : IL) : Nat := l.bits.toNat + 8 * l.have_.toNat + 8 * μ h
32
33end Zlib.Infback.Spec
34
35namespace Zlib.Infback.Proofs
36open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec
37
38theorem BIn.congr {ownI : Nat → Prop} {h h' : Heap} {l : IL} {bs : List UInt8}
39    (hS : ∀ b, ownI b → h'.bytes b = h.bytes b) (B : BIn ownI h l bs) : BIn ownI h' l bs := by
40  obtain ⟨⟨he, hn, hl⟩, ho⟩ := B
41  refine ⟨⟨he, ?_, hl⟩, ho⟩
42  rcases hn with e | ⟨r, a, off, hnx, hg, hsz, hbs⟩
43  · exact Or.inl e
44  · rcases ho with e | ⟨b, off', hb, hown⟩
45    · exact Or.inl e
46    · rw [hb] at hnx
47      obtain ⟨h1, h2⟩ := Ptr.ref.inj hnx
48      subst h1
49      have hg' : h.bytes b = some a := hg
50      refine Or.inr ⟨_, a, off, by rw [hb, h2], ?_, hsz, hbs⟩
51      show h'.bytes b = some a
52      rw [hS b hown, hg']
53
54theorem CbFrame.trans {o : Nat → Prop} {h1 h2 h3 : Heap} (a : CbFrame o h1 h2) (b : CbFrame o h2 h3) : CbFrame o h1 h3 :=
55  ⟨fun x hx => (b.bytes x hx).trans (a.bytes x hx), fun x => (b.live x).trans (a.live x),
56   fun x => (b.words x).trans (a.words x), fun x => (b.ro x).trans (a.ro x), fun x => (b.streams x).trans (a.streams x),
57   fun x => (b.gzheaders x).trans (a.gzheaders x), fun x => (b.dstates x).trans (a.dstates x),
58   fun x => (b.istates x).trans (a.istates x), fun x => (b.gzstates x).trans (a.gzstates x),
59   b.static.trans a.static, b.nextBlk.trans a.nextBlk, b.nalloc.trans a.nalloc, b.allocOk.trans a.allocOk,
60   b.garbage.trans a.garbage⟩
61
62/-- `PULL()` when input is left: nothing happens. -/
63theorem PULL_have {c : BCtx} {l : IL} {h : Heap} (hne : l.have_ ≠ 0) :
64    runX (PULL c) l h = .ok ((.ok (), l), h) := by
65  have hb : (l.have_ == 0) = false := by simpa using hne
66  unfold PULL
67  simp [runX_bind, runX_get, hb, hne, runX_pure]
68
69/-- `PULL()` with no input left and `in` returning a chunk of `n ≠ 0` bytes at `nx`. -/
70theorem PULL_chunk {c : BCtx} {l : IL} {h h' : Heap} {n : UInt32} {nx : BPtr} (h0 : l.have_ = 0) (hn : n ≠ 0)
71    (hin : c.inCb c.inDesc l.next h = .ok ((n, nx), h')) :
72    runX (PULL c) l h = .ok ((.ok (), { l with have_ := n, next := nx }), h') := by
73  have hb : (n == 0) = false := by simpa using hn
74  unfold PULL
75  simp [runX_bind, runX_get, h0, hin, runX_lift_ok, hb, hn, runX_set, runX_pure, runX_lift]
76
77theorem PULL_noinput {c : BCtx} {l : IL} {h h' : Heap} {nx : BPtr} (h0 : l.have_ = 0)
78    (hin : c.inCb c.inDesc l.next h = .ok ((0, nx), h')) :
79    runX (PULL c) l h = .ok ((.error Ex.leave, { l with have_ := 0, next := .null, ret := Z_BUF_ERROR }), h') :=
80  PULL_eof h0 hin
81
82theorem PULLBYTE_c_eq (c : BCtx) {l : IL} {h : Heap} (hne : l.have_ ≠ 0) :
83    runX (Zlib.Infback.PULLBYTE c) l h = runX Zlib.Inflate.PULLBYTE l h := by
84  have hb : (l.have_ == 0) = false := by simpa using hne
85  unfold Zlib.Infback.PULLBYTE Zlib.Inflate.PULLBYTE
86  simp only [runX_bind, PULL_have hne, runX_get, hb, Bool.false_eq_true, ↓reduceIte, runX_pure, runX_set, runX_lift]
87  generalize load8 l.next h = r1
88  rcases r1 with e | ⟨a1, h1⟩
89  · rfl
90  simp only []
91  generalize Ptr.add l.next 1 h1 = r2
92  rcases r2 with e | ⟨a2, h2⟩
93  · rfl
94  simp only []
95  generalize shl64 a1.toUInt64 l.bits h2 = r3
96  rcases r3 with e | ⟨a3, h3⟩ <;> rfl
97
98/-- `PULLBYTE` of `inflate()` with its pointer made explicit. -/
99theorem PULLBYTE_nx {h : Heap} {l : IL} {b : UInt8} {r : BRef} {off : Nat} {a : Array UInt8} (hne : l.have_ ≠ 0)
100    (hnext : l.next = .ref r off) (hg : (Space.get h r : Option (Array UInt8)) = some a) (hlt : off < a.size)
101    (hb : a[off] = b) (hbits : l.bits.toNat < 64) :
102    runX Zlib.Inflate.PULLBYTE l h = .ok ((.ok (), pulled l b (.ref r (off + 1))), h) := by
103  have hne' : (l.have_ == 0) = false := by simpa using hne
104  have hadd : OkOn h (l.next.add 1) (.ref r (off + 1)) := by
105    rw [hnext]; exact Ptr.add_nat_ok (n := 1) hg (by omega)
106  have hld : OkOn h (load8 l.next) b := by
107    rw [hnext]
108    have := Ptr.load_ok (h := h) (r := r) (off := off) hg hlt
109    rw [hb] at this; exact this
110  have hshl : shl64 b.toUInt64 l.bits h = .ok (b.toUInt64 <<< l.bits.toUInt64, h) := by
111    rw [shl64_run _ _ hbits]; rfl
112  unfold Zlib.Inflate.PULLBYTE
113  rw [runX_bind, runX_get]
114  simp only [hne', Bool.false_eq_true, ↓reduceIte]
115  simp only [runX_bind, runX_set, runX_lift_ok hld, runX_lift_ok hadd, runX_lift_ok hshl]
116  rfl
117
118/-- `PULLBYTE` with input left in an `in` chunk: one byte moves into the bit buffer; the chunk stays in its block. -/
119theorem PULLBYTE_have (c : BCtx) {ownI : Nat → Prop} {h : Heap} {l : IL} {b : UInt8} {rest : List UInt8}
120    (B : BIn ownI h l (b :: rest)) (hb : l.bits.toNat ≤ 56) :
121    ∃ nx, runX (Zlib.Infback.PULLBYTE c) l h = .ok ((.ok (), pulled l b nx), h) ∧ BIn ownI h (pulled l b nx) rest ∧
122      (pulled l b nx).bits.toNat = l.bits.toNat + 8 := by
123  have hne0 : l.have_ ≠ 0 := fun e => by have := B.bit.have_eq; rw [e] at this; simp at this
124  obtain ⟨nx, hrun, hB2, -, hbits⟩ := PULLBYTE_succ B.bit hb
125  refine ⟨nx, by rw [PULLBYTE_c_eq c hne0]; exact hrun, ?_, hbits⟩
126  refine ⟨hB2, ?_⟩
127  obtain ⟨bb, off0, hnx0, hown⟩ := B.own.resolve_left (by simp)
128  obtain ⟨r, a, off, hnext, hg, hsz, hbs⟩ := B.bit.next.resolve_left (by simp)
129  rw [hnx0] at hnext
130  obtain ⟨h1, h2⟩ := Ptr.ref.inj hnext
131  subst h1; subst h2
132  have hsz' : off0 + rest.length + 1 ≤ a.size := by simp at hsz; omega
133  have hbs' : b :: rest = a[off0] :: (a.toList.drop (off0 + 1)).take rest.length := by
134    have := take_succ_drop a off0 rest.length hsz'
135    simp only [List.length_cons] at hbs
136    rw [← this]; exact hbs
137  have hbb : a[off0] = b := by injection hbs' with h1; exact h1.symm
138  have hrun2 := PULLBYTE_nx (b := b) hne0 hnx0 hg (by omega) hbb (by omega)
139  rw [hrun] at hrun2
140  have hnx : pulled l b nx = pulled l b (.ref (.blk bb) (off0 + 1)) := by
141    simpa using hrun2
142  right
143  refine ⟨bb, off0 + 1, ?_, hown⟩
144  rw [hnx]; rfl
145
146/-- The registers after a successful `PULLBYTE`/`NEEDBITS`: only `next`, `have`, `hold`, `bits` differ. -/
147def InShape (l l' : IL) : Prop := l' = { l with next := l'.next, have_ := l'.have_, hold := l'.hold, bits := l'.bits }
148
149/-- The registers after the end of input: `next = NULL`, `have = 0`, `ret = Z_BUF_ERROR`. -/
150def EofRegs (l : IL) : IL := { l with have_ := 0, next := .null, ret := Z_BUF_ERROR }
151
152/-- **`PULLBYTE` with the call-back.** Under `CbContract`, with at most 56 bits held: no fault, and either one byte is pulled
153(`ok`: `bits` grows by 8, only the input registers change, `in` was called only if the chunk was used up) or `goto inf_leave`
154with `Z_BUF_ERROR` (`in` returned 0: `next = NULL`, `have = 0`). The call-back changed only its own blocks; `R` holds
155again; the registers describe the new chunk. -/
156theorem PULLBYTE_run (c : BCtx) {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
157    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {μ : Heap → Nat} (hF : InFinite c ownI R μ)
158    {h : Heap} {l : IL} {bs : List UInt8}
159    (B : BIn ownI h l bs) (hR : R h) (hb : l.bits.toNat ≤ 56) :
160    ∃ r l' h' bs', runX (Zlib.Infback.PULLBYTE c) l h = .ok ((r, l'), h') ∧ CbFrame ownI h h' ∧ R h' ∧
161      BIn ownI h' l' bs' ∧
162      (r = .ok () → l'.bits.toNat = l.bits.toNat + 8 ∧ InShape l l') ∧
163      (r = .error Ex.leave → l' = EofRegs l) ∧ (∀ e, r = .error e → e = Ex.leave) ∧
164      phi μ h' l' ≤ phi μ h l := by
165  by_cases hz : l.have_ = 0
166  · have hbs : bs = [] := by
167      have := B.bit.have_eq; rw [hz] at this
168      exact List.eq_nil_of_length_eq_zero (by simpa using this.symm)
169    obtain ⟨n, nx, h', he, fr, hR', hbuf⟩ := hK.inOk h l.next hR
170    by_cases hn : n = 0
171    · subst hn
172      refine ⟨.error Ex.leave, EofRegs l, h', [], ?_, fr, hR', ⟨⟨by simp [EofRegs], Or.inl rfl, B.bit.hold_lt⟩, Or.inl rfl⟩,
173        (fun e => by cases e), fun _ => rfl, (fun e he => by cases he; rfl), ?_⟩
174      · unfold Zlib.Infback.PULLBYTE
175        rw [runX_bind, PULL_noinput hz he]
176        rfl
177      · have hs := hF.step h l.next 0 nx h' hR he
178        have hz0 : l.have_.toNat = 0 := by rw [hz]; rfl
179        simp only [phi, EofRegs]
180        simp only [UInt32.toNat_zero] at hs ⊢
181        omega
182    · obtain ⟨bb, off, a, hnx, hown, ha, hle⟩ := hbuf hn
183      have hn1 : ({ l with have_ := n, next := nx } : IL).have_ ≠ 0 := hn
184      let bsc := (a.toList.drop off).take n.toNat
185      have hlen : bsc.length = n.toNat := by simp [bsc]; omega
186      have hB1 : BIn ownI h' { l with have_ := n, next := nx } bsc :=
187        ⟨⟨hlen.symm, Or.inr ⟨.blk bb, a, off, by simp [hnx], ha, by omega, by rw [hlen]⟩, B.bit.hold_lt⟩,
188          Or.inr ⟨bb, off, by simp [hnx], hown⟩⟩
189      have e1 : runX (Zlib.Infback.PULLBYTE c) l h = runX (Zlib.Infback.PULLBYTE c) { l with have_ := n, next := nx } h' := by
190        unfold Zlib.Infback.PULLBYTE
191        simp only [runX_bind, PULL_chunk hz hn he, PULL_have hn1]
192      have hne : bsc ≠ [] := fun e => hn (by
193        have : n.toNat = 0 := by rw [← hlen, e]; rfl
194        exact UInt32.toNat_inj.mp (by simpa using this))
195      obtain ⟨b0, rest, hbc⟩ : ∃ b0 rest, bsc = b0 :: rest := by
196        cases hh : bsc with
197        | nil => exact absurd hh hne
198        | cons x y => exact ⟨x, y, rfl⟩
199      rw [hbc] at hB1
200      obtain ⟨nx', hrun, hB2, hbits⟩ := PULLBYTE_have c hB1 (by simpa using hb)
201      refine ⟨.ok (), _, h', rest, by rw [e1]; exact hrun, fr, hR', hB2, fun _ => ⟨by simpa using hbits, rfl⟩,
202        (fun e => by cases e), (fun e he => by cases he), ?_⟩
203      have hs := hF.step h l.next n nx h' hR he
204      have h1 := hB2.bit.have_eq
205      have hz0 : l.have_.toNat = 0 := by rw [hz]; rfl
206      rw [hbc] at hlen
207      simp only [phi]
208      simp only [pulled, List.length_cons] at hlen h1 hbits ⊢
209      omega
210  · have hbs : ∃ b rest, bs = b :: rest := by
211      cases hh : bs with
212      | nil => exact absurd (by have := B.bit.have_eq; rw [hh] at this; exact UInt32.toNat_inj.mp (by simpa using this)) hz
213      | cons x y => exact ⟨x, y, rfl⟩
214    obtain ⟨b0, rest, rfl⟩ := hbs
215    obtain ⟨nx, hrun, hB2, hbits⟩ := PULLBYTE_have c B hb
216    refine ⟨.ok (), _, h, rest, hrun, CbFrame.refl _ _, hR, hB2, fun _ => ⟨hbits, rfl⟩, (fun e => by cases e),
217      (fun e he => by cases he), ?_⟩
218    have h1 := hB2.bit.have_eq
219    have h0 := B.bit.have_eq
220    simp only [phi]
221    simp only [pulled, List.length_cons] at h0 h1 hbits ⊢
222    omega
223
224theorem InShape.refl (l : IL) : InShape l l := by cases l; rfl
225
226theorem InShape.trans {l l1 l2 : IL} (a : InShape l l1) (b : InShape l1 l2) : InShape l l2 := by
227  cases l; cases l1; cases l2; simp_all [InShape]
228
229/-- The registers after the end of input in the middle of `NEEDBITS`: the input registers and `ret` differ. -/
230def EofShape (l l' : IL) : Prop :=
231  l' = { l with next := .null, have_ := 0, hold := l'.hold, bits := l'.bits, ret := Z_BUF_ERROR }
232
233theorem EofShape.of_eof {l l1 : IL} (a : InShape l l1) : EofShape l (EofRegs l1) := by
234  cases l; cases l1; simp_all [InShape, EofShape, EofRegs]
235
236/-- **`NEEDBITS(n)` with the call-back**, `n ≤ 49`. No fault. Either at least `n` bits are held afterwards (`ok`; only the
237input registers changed; nothing happens when `n` bits are already held), or `in` returned 0 and the call ends with
238`goto inf_leave`, `Z_BUF_ERROR`, `next = NULL`, `have = 0`. At most `max bits (n+7)` bits are held. The call-back changed only
239its own blocks, `R` holds again, and the registers describe the chunk in use. -/
240theorem NEEDBITS_run (c : BCtx) {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
241    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {μ : Heap → Nat} (hF : InFinite c ownI R μ)
242    {h : Heap} {l : IL} {bs : List UInt8}
243    (B : BIn ownI h l bs) (hR : R h) (n : UInt32) (hn : n.toNat ≤ 49) :
244    ∃ r l' h' bs', runX (NEEDBITS c n) l h = .ok ((r, l'), h') ∧ CbFrame ownI h h' ∧ R h' ∧ BIn ownI h' l' bs' ∧
245      l'.bits.toNat ≤ max l.bits.toNat (n.toNat + 7) ∧ (n.toNat ≤ l.bits.toNat → l' = l) ∧
246      (r = .ok () → n.toNat ≤ l'.bits.toNat ∧ InShape l l') ∧
247      (r = .error Ex.leave → EofShape l l') ∧ (∀ e, r = .error e → e = Ex.leave) ∧ phi μ h' l' ≤ phi μ h l := by
248  let Kf : IL → Nat := fun l1 => if l1.bits.toNat < n.toNat then (n.toNat - l1.bits.toNat + 7) / 8 else 0
249  have key := xwhileBrk_run (cond := (do return (← get).bits < n : X Bool))
250    (body := (do Zlib.Infback.PULLBYTE c; pure false : X Bool))
251    (fun k l1 h1 => ∃ bs1, BIn ownI h1 l1 bs1 ∧ R h1 ∧ CbFrame ownI h h1 ∧ InShape l l1 ∧
252      l1.bits.toNat ≤ max l.bits.toNat (n.toNat + 7) ∧ l.bits.toNat ≤ l1.bits.toNat ∧
253      (n.toNat ≤ l.bits.toNat → l1 = l) ∧ phi μ h1 l1 ≤ phi μ h l ∧ k = Kf l1)
254    (fun r l1 h1 => ∃ bs1, BIn ownI h1 l1 bs1 ∧ R h1 ∧ CbFrame ownI h h1 ∧
255      l1.bits.toNat ≤ max l.bits.toNat (n.toNat + 7) ∧ (n.toNat ≤ l.bits.toNat → l1 = l) ∧
256      (r = .ok () → n.toNat ≤ l1.bits.toNat ∧ InShape l l1) ∧ (r = .error Ex.leave → EofShape l l1) ∧
257      (∀ e, r = .error e → e = Ex.leave) ∧ phi μ h1 l1 ≤ phi μ h l)
258    (fun k l1 h1 hP => by
259      obtain ⟨bs1, B1, R1, F1, S1, M1, Lb, Z1, Ph1, hk⟩ := hP
260      have hnl : l1.bits.toNat < n.toNat := by
261        by_cases hc : l1.bits.toNat < n.toNat
262        · exact hc
263        · simp only [Kf, ite_eq_right hc] at hk; omega
264      have hnl' : l1.bits < n := UInt32.lt_iff_toNat_lt.mpr hnl
265      have hcond : runX (do return (← get).bits < n : X Bool) l1 h1 = .ok ((.ok true, l1), h1) := by
266        rw [runX_cond_lt]; simp [hnl']
267      refine ⟨l1, h1, hcond, ?_⟩
268      obtain ⟨r, l2, h2, bs2, hrun, F2, R2, B2, Hok, Hleave, Herr, Ph2⟩ := PULLBYTE_run c hK hF B1 R1 (by omega)
269      have hFt := CbFrame.trans F1 F2
270      cases r with
271      | error e =>
272        have he := Herr e rfl
273        subst he
274        refine ⟨.error Ex.leave, l2, h2, ?_, ?_⟩
275        · rw [runX_bind, hrun]
276        · have hl2 := Hleave rfl
277          have hsh := EofShape.of_eof S1
278          refine ⟨bs2, B2, R2, hFt, ?_, (fun h0 => by omega), (fun e => by cases e), (fun _ => by rw [hl2]; exact hsh), (fun e he => ?_), (by omega)⟩
279          · rw [hl2]; simp [EofRegs]; omega
280          · cases he; rfl
281      | ok u =>
282        cases u
283        obtain ⟨hb8, hS2⟩ := Hok rfl
284        refine ⟨.ok false, l2, h2, ?_, ?_⟩
285        · rw [runX_bind, hrun]; rfl
286        · refine ⟨bs2, B2, R2, hFt, S1.trans hS2, (by omega), (by omega), (fun h0 => by omega), (by omega), ?_⟩
287          simp only [Kf] at hk ⊢
288          rw [ite_eq_left hnl] at hk
289          split <;> omega)
290    (fun l1 h1 hP => by
291      obtain ⟨bs1, B1, R1, F1, S1, M1, Lb, Z1, Ph1, hk⟩ := hP
292      have hnl : ¬ l1.bits.toNat < n.toNat := by
293        intro hl; simp only [Kf, ite_eq_left hl] at hk; omega
294      refine ⟨l1, h1, (by rw [runX_cond_lt]; simp [UInt32.lt_iff_toNat_lt, hnl]), bs1, B1, R1, F1, M1, Z1,
295        (fun _ => ⟨by omega, S1⟩), (fun e => by cases e), (fun e he => by cases he), Ph1⟩)
296    (k := Kf l) (l := l) (h := h)
297    ⟨bs, B, hR, CbFrame.refl _ _, InShape.refl l, (by omega), Nat.le_refl _, (fun _ => rfl), Nat.le_refl _, rfl⟩
298    (by unfold fuel Kf; split <;> omega)
299  obtain ⟨r, l', h', hr, bs', B', R', F', M', Z', Q1, Q2, Q3, Q4⟩ := key
300  exact ⟨r, l', h', bs', by unfold NEEDBITS xwhile; exact hr, F', R', B', M', Z', Q1, Q2, Q3, Q4⟩
301
302/-- **Witness for `InFinite`.** The call-back `eofIn` (no input) has the measure 0. Together with `cbContract_eof` this shows the
303hypotheses of the macro theorems are met by a concrete call-back on the heap of the real initialisation. -/
304theorem inFinite_eof (c : BCtx) (hc : c.inCb = eofIn) (ownI : Nat → Prop) (R : Heap → Prop) :
305    InFinite c ownI R (fun _ => 0) := by
306  refine ⟨fun h nx n nx' h' _ e => ?_, fun _ _ _ => rfl⟩
307  have e' : (Except.ok ((0, nx), h) : Except Fault ((UInt32 × BPtr) × Heap)) = .ok ((n, nx'), h') := by
308    rw [← e, hc]; rfl
309  have h1 := (Prod.mk.inj (Except.ok.inj e')).1
310  have h2 := (Prod.mk.inj h1).1
311  subst h2
312  simp
313
314end Zlib.Infback.Proofs