infback.c.pull.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.inv»
2
3/-!
4# infback.c: `PULL()` with the call-back, on the invariant of the loop
5
6`PULL_run` is the part of `PULLBYTE_run` before the byte is taken. `STORED` and the copy loops use `PULL` alone.
7-/
8
9namespace Zlib.Infback.Proofs
10open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec
11
12/-- **`PULL()` with the call-back.** No fault. Either input is left afterwards (`ok`, `have /= 0`; `in` is called only when the
13chunk was used up; only the input registers change), or `in` returned 0 and the call ends with `goto inf_leave`,
14`Z_BUF_ERROR`. The call-back changed only its own blocks, `R` holds again, the registers describe the chunk in use, and the
15input still to be read never grows. -/
16theorem PULL_run (c : BCtx) {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
17    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {μ : Heap → Nat} (hF : InFinite c ownI R μ)
18    {h : Heap} {l : IL} {bs : List UInt8} (B : BIn ownI h l bs) (hR : R h) :
19    ∃ r l' h' bs', runX (PULL c) l h = .ok ((r, l'), h') ∧ CbFrame ownI h h' ∧ R h' ∧ BIn ownI h' l' bs' ∧
20      (r = .ok () → l'.have_ ≠ 0 ∧ InShape l l') ∧ (r = .error Ex.leave → l' = EofRegs l) ∧
21      (∀ e, r = .error e → e = Ex.leave) ∧ (l'.bits = l.bits ∧ l'.hold = l.hold) ∧ phi μ h' l' ≤ phi μ h l := by
22  by_cases hz : l.have_ = 0
23  · have hz0 : l.have_.toNat = 0 := by rw [hz]; rfl
24    obtain ⟨n, nx, h', he, fr, hR', hbuf⟩ := hK.inOk h l.next hR
25    have hs := hF.step h l.next n nx h' hR he
26    by_cases hn : n = 0
27    · subst hn
28      refine ⟨.error Ex.leave, EofRegs l, h', [], PULL_noinput hz he, fr, hR',
29        ⟨⟨by simp [EofRegs], Or.inl rfl, B.bit.hold_lt⟩, Or.inl rfl⟩, (fun e => by cases e), fun _ => rfl,
30        (fun e he => by cases he; rfl), ⟨rfl, rfl⟩, ?_⟩
31      simp only [phi, EofRegs]
32      simp only [UInt32.toNat_zero] at hs ⊢
33      omega
34    · obtain ⟨bb, off, a, hnx, hown, ha, hle⟩ := hbuf hn
35      have hn1 : ({ l with have_ := n, next := nx } : IL).have_ ≠ 0 := hn
36      have hlen : ((a.toList.drop off).take n.toNat).length = n.toNat := by simp; omega
37      refine ⟨.ok (), { l with have_ := n, next := nx }, h', (a.toList.drop off).take n.toNat, PULL_chunk hz hn he, fr, hR',
38        ⟨⟨hlen.symm, Or.inr ⟨.blk bb, a, off, by simp [hnx], ha, by omega, by rw [hlen]⟩, B.bit.hold_lt⟩,
39          Or.inr ⟨bb, off, by simp [hnx], hown⟩⟩, fun _ => ⟨hn1, rfl⟩, (fun e => by cases e), (fun e he => by cases he), ⟨rfl, rfl⟩, ?_⟩
40      simp only [phi]
41      omega
42  · refine ⟨.ok (), l, h, bs, PULL_have hz, CbFrame.refl _ _, hR, B, fun _ => ⟨hz, InShape.refl l⟩, (fun e => by cases e),
43      (fun e he => by cases he), ⟨rfl, rfl⟩, Nat.le_refl _⟩
44
45end Zlib.Infback.Proofs