infback.c.inv.lean

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

1import ZlibF.Proof.«infback.c.room»
2import ZlibF.Proof.«inftrees.c.fixed»
3
4/-!
5# infback.c: the invariant at the top of the loop, and `case TYPE`
6
7`LInv` is what holds whenever `for (;;) switch (state->mode)` is about to read the mode: the stream and the state record
8exist, the window is the caller's writable block, `put`/`left` describe the unwritten tail of the window, the registers
9describe the current input chunk (`BIn`), the call-backs' invariant holds, and at most 39 bits are held.
10-/
11
12namespace Zlib.Infback.Spec
13open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs
14
15/-- The invariant of the dispatch loop. `c.strm = r`, `c.st = zs`; `z`, `s` are the stream and state records; `bs` the rest of
16the current input chunk. -/
17structure LInv (c : BCtx) (win : Nat) (ownI : Nat → Prop) (R : Heap → Prop) (r : ZStreamRef) (zs : Nat) (h : Heap)
18    (l : IL) (z : ZStream) (s : InflateState) (bs : List UInt8) : Prop where
19  cstrm : c.strm = some r
20  cst : c.st = some (.tab zs)
21  hz : r.get h = some z
22  hs : h.istates zs = some s
23  wf : s.WellFormed
24  wnd : ∃ off a, s.window = .ref (.blk win) off ∧ h.bytes win = some a ∧ h.ro win = false ∧ off + s.wsize.toNat ≤ a.size
25  put : ∃ off, s.window = .ref (.blk win) off ∧ l.put = .ref (.blk win) (off + (s.wsize.toNat - l.left.toNat)) ∧
26    l.left.toNat ≤ s.wsize.toNat
27  bin : BIn ownI h l bs
28  hR : R h
29  bits : l.bits.toNat ≤ 39
30
31end Zlib.Infback.Spec
32
33namespace Zlib.Infback.Proofs
34open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec
35
36theorem rdS_ok {c : BCtx} {zs : Nat} {h : Heap} {s : InflateState} (hc : c.st = some (.tab zs))
37    (hs : h.istates zs = some s) {α : Type} (f : InflateState → α) : rdS c.st f h = .ok (f s, h) := by
38  rw [hc, rdI_eq]; simp [hs]
39
40theorem setMode_ok {c : BCtx} {zs : Nat} {h : Heap} {s : InflateState} (hc : c.st = some (.tab zs))
41    (hs : h.istates zs = some s) (m : UInt32) : setMode c.st m h = .ok ((), setI h zs { s with mode := m }) := by
42  rw [hc]; exact setMode_tab hs m
43
44theorem wrS_ok {c : BCtx} {zs : Nat} {h : Heap} {s : InflateState} (hc : c.st = some (.tab zs))
45    (hs : h.istates zs = some s) (f : InflateState → InflateState) : wrS c.st f h = .ok ((), setI h zs (f s)) := by
46  rw [hc]; exact wrS_tab hs f
47
48theorem wf_with {s : InflateState} (hw : s.WellFormed) (s' : InflateState) (e1 : s'.lens = s.lens) (e2 : s'.work = s.work)
49    (e3 : s'.codes = s.codes) : s'.WellFormed := by
50  unfold InflateState.WellFormed at *; rw [e1, e2, e3]; exact hw
51
52/-- A write to the state record that keeps the window and the array sizes keeps the invariant. -/
53theorem LInv.setS {c : BCtx} {win : Nat} {ownI : Nat → Prop} {R : Heap → Prop} {r : ZStreamRef} {zs : Nat} {h : Heap}
54    {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8} (I : LInv c win ownI R r zs h l z s bs)
55    (s' : InflateState) (hw : s'.window = s.window) (hsz : s'.wsize = s.wsize) (e1 : s'.lens = s.lens)
56    (e2 : s'.work = s.work) (e3 : s'.codes = s.codes) (hR' : R (setI h zs s')) :
57    LInv c win ownI R r zs (setI h zs s') l z s' bs := by
58  obtain ⟨hcs, hct, hz, hs, wf, ⟨o1, a, w1, ba, ro, le⟩, ⟨o2, w2, pp, pl⟩, B, hR, hb⟩ := I
59  refine ⟨hcs, hct, by simpa using hz, by simp, wf_with wf s' e1 e2 e3, ⟨o1, a, by rw [hw]; exact w1, by simpa using ba,
60    by simpa using ro, by rw [hsz]; exact le⟩, ⟨o2, by rw [hw]; exact w2, by rw [hsz]; exact pp, by rw [hsz]; exact pl⟩,
61    @BIn.congr ownI h (setI h zs s') l bs (fun _ _ => rfl) B, hR', hb⟩
62
63/-- New registers (same `put` and `left`, a valid chunk, at most 39 bits) keep the invariant. -/
64theorem LInv.regs {c : BCtx} {win : Nat} {ownI : Nat → Prop} {R : Heap → Prop} {r : ZStreamRef} {zs : Nat} {h : Heap}
65    {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8} (I : LInv c win ownI R r zs h l z s bs) {l' : IL}
66    {bs' : List UInt8} (hp : l'.put = l.put) (hl : l'.left = l.left) (B' : BIn ownI h l' bs')
67    (hb : l'.bits.toNat ≤ 39) : LInv c win ownI R r zs h l' z s bs' := by
68  obtain ⟨hcs, hct, hz, hs, wf, wnd, ⟨o2, w2, pp, pl⟩, B, hR, hb0⟩ := I
69  exact ⟨hcs, hct, hz, hs, wf, wnd, ⟨o2, w2, by rw [hp, hl]; exact pp, by rw [hl]; exact pl⟩, B', hR, hb⟩
70
71/-- After a call of `in` or `out` (a `CbFrame` for the blocks `own`, the window being none of them). -/
72theorem LInv.cb {c : BCtx} {win : Nat} {ownI own : Nat → Prop} {R : Heap → Prop} {r : ZStreamRef} {zs : Nat} {h h' : Heap}
73    {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8} (I : LInv c win ownI R r zs h l z s bs)
74    (F : CbFrame own h h') (hw : ¬ own win) (hR' : R h') {l' : IL} {bs' : List UInt8}
75    (hp : l'.put = l.put) (hl : l'.left = l.left) (B' : BIn ownI h' l' bs') (hb : l'.bits.toNat ≤ 39) :
76    LInv c win ownI R r zs h' l' z s bs' := by
77  obtain ⟨hcs, hct, hz, hs, wf, ⟨o1, a, w1, ba, ro, le⟩, ⟨o2, w2, pp, pl⟩, B, hR, hb0⟩ := I
78  refine ⟨hcs, hct, by rw [CbFrame.zget F]; exact hz, by rw [F.istates]; exact hs, wf,
79    ⟨o1, a, w1, by rw [F.bytes win hw]; exact ba, by rw [F.ro]; exact ro, le⟩,
80    ⟨o2, w2, by rw [hp, hl]; exact pp, by rw [hl]; exact pl⟩, B', hR', hb⟩
81
82theorem LInv.R_setI {c : BCtx} {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
83    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {h : Heap} (hR : R h) (zs : Nat)
84    (s : InflateState) : R (setI h zs s) := (hK.local_ h (setI h zs s) (fun _ _ => rfl)).1 hR
85
86/-- `case TYPE` after the last block: `BYTEBITS(); state->mode = DONE`. -/
87theorem TYPE_last {c : BCtx} {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
88    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {μ : Heap → Nat} (hF : InFinite c ownI R μ) {r : ZStreamRef} {zs : Nat}
89    {h : Heap} {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8}
90    (I : LInv c win ownI R r zs h l z s bs) (hl : s.last ≠ 0) :
91    ∃ bs', runX (back_TYPE c) l h = .ok ((.ok (), bytebits l), setI h zs { s with mode := DONE }) ∧
92      LInv c win ownI R r zs (setI h zs { s with mode := DONE }) (bytebits l) z { s with mode := DONE } bs' ∧
93      phi μ (setI h zs { s with mode := DONE }) (bytebits l) ≤ phi μ h l := by
94  have hne : (s.last != 0) = true := by simpa using hl
95  have hrd : liftM (rdS c.st (·.last)) = (liftM (rdS c.st (·.last)) : X Int32) := rfl
96  obtain ⟨B1, hs1, hb1⟩ := BYTEBITS_inv I.bin.bit
97  have I1 := Zlib.Infback.Proofs.LInv.setS I { s with mode := DONE } rfl rfl rfl rfl rfl (LInv.R_setI hK I.hR zs _)
98  have hbl : (bytebits l).bits.toNat ≤ l.bits.toNat := by
99    show (l.bits - (l.bits &&& 7)).toNat ≤ _
100    rw [UInt32.toNat_sub_of_le _ _ (UInt32.le_iff_toNat_le.mpr (and7_le l))]; omega
101  refine ⟨bs, ?_, ?_, ?_⟩
102  · unfold back_TYPE
103    simp [runX_bind, runX_lift_ok (rdS_ok I.cst I.hs _), hne, hl, BYTEBITS_run, runX_lift_ok (setMode_ok I.cst I.hs DONE), runX_pure]
104  · have := I.bits
105    exact Zlib.Infback.Proofs.LInv.regs I1 rfl rfl
106      (@BIn.congr ownI h (setI h zs { s with mode := DONE }) (bytebits l) bs (fun _ _ => rfl) ⟨B1, I.bin.own⟩) (by omega)
107  · simp only [phi]
108    have := I.bin.bit.have_eq
109    have h2 : (bytebits l).have_ = l.have_ := rfl
110    rw [h2]
111    have hm : μ (setI h zs { s with mode := DONE }) = μ h := hF.local_ _ _ (fun _ _ => rfl)
112    omega
113
114set_option maxRecDepth 100000 in
115theorem msg_block_type : "invalid block type" ∈ strTable := by
116  rw [Array.mem_def]; decide +kernel
117
118theorem LInv.putMsg {c : BCtx} {win : Nat} {ownI : Nat → Prop} {R : Heap → Prop} {r : ZStreamRef} {zs : Nat} {h : Heap}
119    {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8} (I : LInv c win ownI R r zs h l z s bs) (m : BPtr)
120    (hR' : R (r.put h { z with msg := m })) :
121    LInv c win ownI R r zs (r.put h { z with msg := m }) l { z with msg := m } s bs := by
122  obtain ⟨hcs, hct, hz, hs, wf, ⟨o1, a, w1, ba, ro, le⟩, pt, B, hR, hb⟩ := I
123  refine ⟨hcs, hct, by simp [hz], by simpa using hs, wf, ⟨o1, a, w1, by simpa using ba, by simpa using ro, le⟩, pt,
124    @BIn.congr ownI h (r.put h { z with msg := m }) l bs (fun _ _ => by simp) B, hR', hb⟩
125
126/-- `strm->msg = "..."; state->mode = BAD;` for a message that is a string literal. -/
127theorem badMode_run (c : BCtx) {r : ZStreamRef} {zs : Nat} {h : Heap} {z : ZStream} {s : InflateState}
128    (hcs : c.strm = some r) (hct : c.st = some (.tab zs)) (hz : r.get h = some z) (hs : h.istates zs = some s)
129    (msg : String) (hm : msg ∈ strTable) :
130    ∃ i, badMode c msg h = .ok ((), setI (r.put h { z with msg := .ref (.str i) 0 }) zs { s with mode := BAD }) := by
131  obtain ⟨i, hi, -⟩ := strLitRef_of_mem (h := h) hm
132  refine ⟨i, ?_⟩
133  have hs' : (r.put h { z with msg := .ref (.str i) 0 }).istates zs = some s := by simpa using hs
134  have hz' : r.get (r.put h { z with msg := .ref (.str i) 0 }) = some { z with msg := .ref (.str i) 0 } := by simp [hz]
135  unfold badMode setMsg Zlib.Zutil.strLit
136  simp [bind_app, hi, hcs, ldZ_eq, hz, stZ_eq, setMode_ok hct hs']
137
138theorem phi_congr {c : BCtx} {ownI : Nat → Prop} {R : Heap → Prop} {μ : Heap → Nat} (hF : InFinite c ownI R μ)
139    {h h' : Heap} (e : ∀ b, h'.bytes b = h.bytes b) (l : IL) : phi μ h' l = phi μ h l := by
140  simp only [phi]; rw [hF.local_ h h' (fun b _ => e b)]
141
142/-- `case TYPE` for a block that is not the last: `NEEDBITS(3)`, the last-block flag, the block type, `DROPBITS`. Either the
143input ended (`Z_BUF_ERROR`), or three bits are consumed and the mode is `STORED`, `LEN` (fixed tables), `TABLE`, or `BAD`
144("invalid block type"). -/
145theorem TYPE_more {c : BCtx} {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
146    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {μ : Heap → Nat} (hF : InFinite c ownI R μ)
147    {r : ZStreamRef} {zs : Nat} {h : Heap} {l : IL} {z : ZStream} {s : InflateState} {bs : List UInt8}
148    (I : LInv c win ownI R r zs h l z s bs) (hl : s.last = 0) :
149    ∃ res l' h' z' s' bs', runX (back_TYPE c) l h = .ok ((res, l'), h') ∧ LInv c win ownI R r zs h' l' z' s' bs' ∧
150      (∀ e, res = .error e → e = Ex.leave ∧ l'.ret = Z_BUF_ERROR ∧ phi μ h' l' ≤ phi μ h l) ∧
151      (res = .ok () → phi μ h' l' + 3 ≤ phi μ h l ∧
152        (s'.mode = STORED ∨ s'.mode = LEN ∨ s'.mode = TABLE ∨ s'.mode = BAD)) := by
153  obtain ⟨res0, l1, h1, bs1, hrun1, F1, R1, B1, M1, Z1, Hok, Hleave, Herr, Ph1⟩ :=
154    NEEDBITS_run c hK hF I.bin I.hR 3 (by decide)
155  have hL1 : ∀ {l1 : IL}, InShape l l1 → l1.put = l.put ∧ l1.left = l.left := by
156    intro l1 hs; exact ⟨by simpa using congrArg IL.put hs, by simpa using congrArg IL.left hs⟩
157  have h3n : (3 : UInt32).toNat = 3 := rfl
158  have hb39 : l1.bits.toNat ≤ 39 := by have := I.bits; rw [h3n] at M1; omega
159  cases res0 with
160  | error e =>
161    have he := Herr e rfl
162    subst he
163    have hE := Hleave rfl
164    have hp : l1.put = l.put := by rw [hE]
165    have hlf : l1.left = l.left := by rw [hE]
166    have I1 := Zlib.Infback.Proofs.LInv.cb I F1 hK.disj.1 R1 hp hlf B1 hb39
167    refine ⟨.error Ex.leave, l1, h1, z, s, bs1, ?_, I1, ?_, fun he => by cases he⟩
168    · unfold back_TYPE
169      simp [runX_bind, runX_lift_ok (rdS_ok I.cst I.hs _), hl, hrun1]
170    · intro e he
171      cases he
172      exact ⟨rfl, by rw [hE], Ph1⟩
173  | ok u =>
174    cases u
175    obtain ⟨h3, hS⟩ := Hok rfl
176    obtain ⟨hp, hlf⟩ := hL1 hS
177    have I1 := Zlib.Infback.Proofs.LInv.cb I F1 hK.disj.1 R1 hp hlf B1 hb39
178    have h3n' : 3 ≤ l1.bits.toNat := by rw [h3n] at h3; exact h3
179    have hb1 : 1 ≤ l1.bits.toNat := by omega
180    -- the registers after `DROPBITS(1)` and `DROPBITS(2)`
181    obtain ⟨B2, -, hbit2⟩ := DROPBITS_inv I1.bin.bit 1 (by simpa using hb1) (by decide)
182    obtain ⟨B3, -, hbit3⟩ := DROPBITS_inv B2 2 (by simp at hbit2 ⊢; omega) (by decide)
183    simp only [UInt32.toNat_one, show (2 : UInt32).toNat = 2 from rfl] at hbit2 hbit3
184    obtain ⟨v1, hv1⟩ : ∃ v1 : UInt32, v1 = l1.hold.toUInt32 &&& ((1 : UInt32) <<< 1 - 1) := ⟨_, rfl⟩
185    obtain ⟨l2, hl2⟩ : ∃ l2 : IL, l2 = { l1 with hold := l1.hold >>> (1 : UInt32).toUInt64, bits := l1.bits - 1 } := ⟨_, rfl⟩
186    obtain ⟨v2, hv2⟩ : ∃ v2 : UInt32, v2 = l2.hold.toUInt32 &&& ((1 : UInt32) <<< 2 - 1) := ⟨_, rfl⟩
187    obtain ⟨l3, hl3⟩ : ∃ l3 : IL, l3 = { l2 with hold := l2.hold >>> (2 : UInt32).toUInt64, bits := l2.bits - 2 } := ⟨_, rfl⟩
188    obtain ⟨s1, hs1d⟩ : ∃ s1 : InflateState, s1 = { s with last := u2i v1 } := ⟨_, rfl⟩
189    have hr1 : runX (BITS 1) l1 h1 = .ok ((.ok v1, l1), h1) := by rw [BITS_run l1 h1 1 (by decide), hv1]
190    have hd1 : ∀ h, runX (DROPBITS 1) l1 h = .ok ((.ok (), l2), h) := by
191      intro h; rw [DROPBITS_run l1 h 1 (by decide), hl2]
192    have hb2 : ∀ h, runX (BITS 2) l2 h = .ok ((.ok v2, l2), h) := by intro h; rw [BITS_run l2 h 2 (by decide), hv2]
193    have hd2 : ∀ h, runX (DROPBITS 2) l2 h = .ok ((.ok (), l3), h) := by
194      intro h; rw [DROPBITS_run l2 h 2 (by decide), hl3]
195    have hw1 : wrS c.st (fun s => { s with last := u2i v1 }) h1 = .ok ((), setI h1 zs s1) := by
196      rw [wrS_ok I1.cst I1.hs, hs1d]
197    have bits2 : l2.bits.toNat = l1.bits.toNat - 1 := by rw [hl2]; simpa using hbit2
198    have bits3 : l3.bits.toNat = l2.bits.toNat - 2 := by
199      rw [hl3, hl2]; simpa using hbit3
200    have B3' : BIn ownI h1 l3 bs1 := by
201      refine ⟨?_, ?_⟩
202      · rw [hl3, hl2]; exact B3
203      · rw [hl3, hl2]; exact I1.bin.own
204    have B3c : ∀ s' : InflateState, BIn ownI (setI h1 zs s') l3 bs1 := fun s' =>
205      @BIn.congr ownI h1 (setI h1 zs s') l3 bs1 (fun _ _ => rfl) B3'
206    have hv2lt : v2.toNat < 4 := by
207      rw [hv2, BITS_toNat l2 2 (by decide)]
208      exact Nat.mod_lt _ (by decide)
209    have hs2 : (setI h1 zs s1).istates zs = some s1 := by simp
210    have hR2 : R (setI h1 zs s1) := LInv.R_setI hK I1.hR zs s1
211    have hzs2 : r.get (setI h1 zs s1) = some z := by simpa using I1.hz
212    have hcases : v2 = 0 ∨ v2 = 1 ∨ v2 = 2 ∨ v2 = 3 := by
213      have : v2.toNat = 0 ∨ v2.toNat = 1 ∨ v2.toNat = 2 ∨ v2.toNat = 3 := by omega
214      rcases this with e | e | e | e
215      · exact Or.inl (UInt32.toNat_inj.mp (by simpa using e))
216      · exact Or.inr (Or.inl (UInt32.toNat_inj.mp (by simpa using e)))
217      · exact Or.inr (Or.inr (Or.inl (UInt32.toNat_inj.mp (by simpa using e))))
218      · exact Or.inr (Or.inr (Or.inr (UInt32.toNat_inj.mp (by simpa using e))))
219    have hphi : ∀ hf : Heap, (∀ b, hf.bytes b = h1.bytes b) → phi μ hf l3 + 3 ≤ phi μ h l := by
220      intro hf hb
221      rw [phi_congr hF hb]
222      simp only [phi] at Ph1 ⊢
223      have : l3.have_ = l1.have_ := by rw [hl3, hl2]
224      rw [this]; omega
225    rcases hcases with rfl | rfl | rfl | rfl
226    · refine ⟨.ok (), l3, setI h1 zs { s1 with mode := STORED }, z, { s1 with mode := STORED }, bs1, ?_, ?_,
227        (fun e he => by cases he), fun _ => ⟨hphi _ (fun _ => rfl), Or.inl rfl⟩⟩
228      · unfold back_TYPE
229        simp only [runX_bind, runX_lift_ok (rdS_ok I.cst I.hs _), hl, bne_self_eq_false, Bool.false_eq_true, ↓reduceIte, hrun1,
230          hr1, runX_lift_ok hw1, hd1, hb2, runX_lift_ok (setMode_ok I1.cst hs2 STORED), hd2]
231        simp only [setI_setI]
232      · exact Zlib.Infback.Proofs.LInv.regs
233          (Zlib.Infback.Proofs.LInv.setS I1 { s1 with mode := STORED } (by rw [hs1d]) (by rw [hs1d]) (by rw [hs1d])
234            (by rw [hs1d]) (by rw [hs1d]) (LInv.R_setI hK I1.hR zs _)) (by rw [hl3, hl2]) (by rw [hl3, hl2]) (B3c _)
235          (by have := I1.bits; omega)
236    · have hfx : Zlib.Inftrees.inflate_fixed c.st (setI h1 zs s1) =
237          .ok ((), setI (setI h1 zs s1) zs (Zlib.Inftrees.Proofs.fixedState s1)) := by
238        rw [I1.cst]; have := Zlib.Inftrees.Proofs.inflate_fixed_ok hs2; rwa [C.run] at this
239      have hs3 : (setI (setI h1 zs s1) zs (Zlib.Inftrees.Proofs.fixedState s1)).istates zs =
240          some (Zlib.Inftrees.Proofs.fixedState s1) := by simp
241      refine ⟨.ok (), l3, setI h1 zs { Zlib.Inftrees.Proofs.fixedState s1 with mode := LEN }, z,
242        { Zlib.Inftrees.Proofs.fixedState s1 with mode := LEN }, bs1, ?_, ?_,
243        (fun e he => by cases he), fun _ => ⟨hphi _ (fun _ => rfl), Or.inr (Or.inl rfl)⟩⟩
244      · unfold back_TYPE
245        simp only [runX_bind, runX_lift_ok (rdS_ok I.cst I.hs _), hl, bne_self_eq_false, Bool.false_eq_true, ↓reduceIte, hrun1,
246          hr1, runX_lift_ok hw1, hd1, hb2, runX_lift_ok hfx, runX_lift_ok (setMode_ok I1.cst hs3 LEN), hd2]
247        simp only [setI_setI]
248      · exact Zlib.Infback.Proofs.LInv.regs
249          (Zlib.Infback.Proofs.LInv.setS I1 { Zlib.Inftrees.Proofs.fixedState s1 with mode := LEN } (by rw [hs1d]; rfl)
250            (by rw [hs1d]; rfl) (by rw [hs1d]; rfl) (by rw [hs1d]; rfl) (by rw [hs1d]; rfl) (LInv.R_setI hK I1.hR zs _))
251          (by rw [hl3, hl2]) (by rw [hl3, hl2]) (B3c _) (by have := I1.bits; omega)
252    · refine ⟨.ok (), l3, setI h1 zs { s1 with mode := TABLE }, z, { s1 with mode := TABLE }, bs1, ?_, ?_,
253        (fun e he => by cases he), fun _ => ⟨hphi _ (fun _ => rfl), Or.inr (Or.inr (Or.inl rfl))⟩⟩
254      · unfold back_TYPE
255        simp only [runX_bind, runX_lift_ok (rdS_ok I.cst I.hs _), hl, bne_self_eq_false, Bool.false_eq_true, ↓reduceIte, hrun1,
256          hr1, runX_lift_ok hw1, hd1, hb2, runX_lift_ok (setMode_ok I1.cst hs2 TABLE), hd2]
257        simp only [setI_setI]
258      · exact Zlib.Infback.Proofs.LInv.regs
259          (Zlib.Infback.Proofs.LInv.setS I1 { s1 with mode := TABLE } (by rw [hs1d]) (by rw [hs1d]) (by rw [hs1d])
260            (by rw [hs1d]) (by rw [hs1d]) (LInv.R_setI hK I1.hR zs _)) (by rw [hl3, hl2]) (by rw [hl3, hl2]) (B3c _)
261          (by have := I1.bits; omega)
262    · obtain ⟨i, hbad⟩ := badMode_run c I1.cstrm I1.cst hzs2 hs2 "invalid block type" msg_block_type
263      have I2 := Zlib.Infback.Proofs.LInv.setS I1 s1 (by rw [hs1d]) (by rw [hs1d]) (by rw [hs1d]) (by rw [hs1d])
264        (by rw [hs1d]) hR2
265      have hRm : R (r.put (setI h1 zs s1) { z with msg := .ref (.str i) 0 }) :=
266        (hK.local_ (setI h1 zs s1) _ (fun b _ => by simp)).1 hR2
267      have I3 := Zlib.Infback.Proofs.LInv.putMsg I2 (.ref (.str i) 0) hRm
268      refine ⟨.ok (), l3, setI (r.put (setI h1 zs s1) { z with msg := .ref (.str i) 0 }) zs { s1 with mode := BAD },
269        { z with msg := .ref (.str i) 0 }, { s1 with mode := BAD }, bs1, ?_, ?_,
270        (fun e he => by cases he), fun _ => ⟨hphi _ (fun b => by simp), Or.inr (Or.inr (Or.inr rfl))⟩⟩
271      · unfold back_TYPE
272        simp only [runX_bind, runX_lift_ok (rdS_ok I.cst I.hs _), hl, bne_self_eq_false, Bool.false_eq_true, ↓reduceIte, hrun1,
273          hr1, runX_lift_ok hw1, hd1, hb2]
274        show runX (liftM (badMode c "invalid block type") >>= fun _ => DROPBITS 2) l2 (setI h1 zs s1) = _
275        simp only [runX_bind, runX_lift_ok hbad, hd2]
276      · exact Zlib.Infback.Proofs.LInv.regs
277          (Zlib.Infback.Proofs.LInv.setS I3 { s1 with mode := BAD } rfl rfl rfl rfl rfl
278            (LInv.R_setI hK I3.hR zs _)) (by rw [hl3, hl2]) (by rw [hl3, hl2]) (@BIn.congr ownI h1 _ l3 bs1 (fun _ _ => by simp) B3') (by have := I1.bits; omega)
279
280end Zlib.Infback.Proofs