inflate.c.main.table6.lean

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

1import ZlibF.Proof.«inflate.c.main.table5»
2
3/-!
4# inflate.c: `case LENLENS:` as a whole
5-/
6
7namespace Zlib.Inflate.Proofs
8open C Zlib.Inflate Zlib.Inflate.Spec
9
10/-- The state record after both loops of `LENLENS` ran to the end (`M = ncode - have`). -/
11def llDone (s : InflateState) (S : List Bool) : InflateState :=
12  lzSt (llSt s S (s.ncode.toNat - s.«have».toNat)) (19 - (llSt s S (s.ncode.toNat - s.«have».toNat)).«have».toNat)
13
14theorem llDone_lens (s : InflateState) (S : List Bool) (hnc : s.ncode.toNat ≤ 19) (hhn : s.«have».toNat ≤ s.ncode.toNat) :
15    (llDone s S).lens = lensZero (lensRead s.lens s.«have».toNat S (s.ncode.toNat - s.«have».toNat)) s.ncode.toNat
16      (19 - s.ncode.toNat) := by
17  have h1 := llSt_have s S (s.ncode.toNat - s.«have».toNat) (by omega)
18  unfold llDone lzSt llSt
19  simp only [llSt] at h1 ⊢
20  rw [h1]
21  have e : s.«have».toNat + (s.ncode.toNat - s.«have».toNat) = s.ncode.toNat := by omega
22  rw [e]
23
24theorem llDone_have (s : InflateState) (S : List Bool) (hnc : s.ncode.toNat ≤ 19) (hhn : s.«have».toNat ≤ s.ncode.toNat) :
25    (llDone s S).«have».toNat = 19 := by
26  have h1 := llSt_have s S (s.ncode.toNat - s.«have».toNat) (by omega)
27  have h2 := lzSt_have (llSt s S (s.ncode.toNat - s.«have».toNat)) (19 - (llSt s S (s.ncode.toNat - s.«have».toNat)).«have».toNat)
28    (by omega)
29  unfold llDone
30  omega
31
32/-- **`case LENLENS:`.** From `have ≤ ncode ≤ 19` (as `TABLE` leaves them, or a resumed call) with the lengths read by earlier calls
33being 3-bit values (`Good3`, which holds because `inflate.c` stores only `BITS(3)` there). `M = min (ncode - have) (⌊|S| / 3⌋)`
34code-length code lengths are read from the unread stream `S` (three bits each, `grp`) into `lens[order[have + u]]`.
35
36* `M < ncode - have`: the input ran out; `goto inf_leave` with the registers `l'` (all input pulled, fewer than 3 bits left); the
37  state record has `have + M` and the `M` lengths.
38* `M = ncode - have`: the other lengths are set to 0 (the state `llDone`), `inflate_table(CODES, lens, 19, ...)` is called
39  (result `0` or `-1`; `-1` exactly when the 19 lengths are not an acceptable code in the format specification), and then either
40  the error "invalid code lengths set" (`BAD`, `break`) or `have = 0`, `mode = CODELENS` and the fall-through into `CODELENS`. -/
41theorem inflate_LENLENS_run {c : Ctx} {l : IL} {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState}
42    {bs : List UInt8} (hr : c.strm = some r) (hc : c.st = some (.tab zs)) (hz : r.get h = some z)
43    (hs : h.istates zs = some s) (hwf : s.WellFormed) (hnc : s.ncode.toNat ≤ 19) (hhn : s.«have».toNat ≤ s.ncode.toNat)
44    (hG : Good3 s.lens s.«have».toNat) (B : BitInv h l bs) :
45    ∃ l' j, j ≤ bs.length ∧ BitInv h l' (bs.drop j) ∧
46      stream l' (bs.drop j) = (stream l bs).drop (3 * min (s.ncode.toNat - s.«have».toNat) ((stream l bs).length / 3)) ∧
47      TcRegShape l l' ∧
48      (min (s.ncode.toNat - s.«have».toNat) ((stream l bs).length / 3) < s.ncode.toNat - s.«have».toNat →
49        l'.have_ = 0 ∧ j = bs.length ∧ l'.bits.toNat < 3 ∧
50        runX (inflate_LENLENS c) l h = .ok ((.error Ex.leave, l'), setI h zs
51          (llSt s (stream l bs) (min (s.ncode.toNat - s.«have».toNat) ((stream l bs).length / 3))))) ∧
52      (min (s.ncode.toNat - s.«have».toNat) ((stream l bs).length / 3) = s.ncode.toNat - s.«have».toNat →
53        ∃ (ret : Int32) (wa' : Array UInt16) (ca' : Array Code), wa'.size = 288 ∧ ca'.size = 1444 ∧
54          (∀ x, 19 ≤ x → wa'[x]? = s.work[x]?) ∧ (∀ x, 128 ≤ x → ca'[x]? = s.codes[x]?) ∧
55          (ret = 0 ∨ ret = -1) ∧
56          (ret = -1 ↔ ¬ ZlibF.Spec.Acceptable .codeLength
57            (Zlib.Inftrees.Spec.lensList (llDone s (stream l bs)).lens 0 19)) ∧
58          (ret = 0 → ∃ u lb, u ≤ 128 ∧ runX (inflate_LENLENS c) l h = runX (inflate_CODELENS c) { l' with ret := 0 }
59            (setI h zs (llOkSt zs (llDone s (stream l bs)) u lb wa' ca'))) ∧
60          (ret = -1 → ∃ i, strTable[i]? = some "invalid code lengths set" ∧
61            runX (inflate_LENLENS c) l h = .ok ((.ok (), { l' with ret := -1 }),
62              tcBadHeap (setI h zs (llBadSt zs (llDone s (stream l bs)) wa' ca')) r zs z
63                (llBadSt zs (llDone s (stream l bs)) wa' ca') i))) := by
64  obtain ⟨hl, hw, hcs⟩ := hwf
65  obtain ⟨r1, l', j, hrun1, hj, B', hS', hsh, hl1, hok1⟩ := ll1_run hc hs hl hnc hhn B
66  refine ⟨l', j, hj, B', hS', hsh, ?_, ?_⟩
67  · intro hlt
68    obtain ⟨hr1, h2, h3, h4⟩ := hl1 hlt
69    refine ⟨h2, h3, h4, ?_⟩
70    rw [inflate_LENLENS_eq, runX_bind, hrun1, hr1]
71  · intro heq
72    have hr1 := hok1 heq
73    obtain ⟨S, hSdef⟩ : ∃ S, S = stream l bs := ⟨_, rfl⟩
74    rw [← hSdef] at hrun1 heq ⊢
75    rw [heq] at hrun1
76    obtain ⟨n, hn⟩ : ∃ n, n = s.ncode.toNat - s.«have».toNat := ⟨_, rfl⟩
77    rw [← hn] at hrun1
78    have ht1 : (setI h zs (llSt s S n)).istates zs = some (llSt s S n) := by simp
79    have hht1 := llSt_have s S n (by omega)
80    have hsz1 : (llSt s S n).lens.size = 320 := by simp [llSt, lensRead_size, hl]
81    have hlz := lz_run (c := c) (l := l') hc ht1 hsz1 (by omega)
82    have hdone : llDone s S = lzSt (llSt s S n) (19 - (llSt s S n).«have».toNat) := by
83      unfold llDone; rw [← hn]
84    have hmain : runX (inflate_LENLENS c) l h = runX (llTail c) l' (setI h zs (llDone s S)) := by
85      rw [inflate_LENLENS_eq, runX_bind, hrun1, hr1]
86      simp only []
87      rw [runX_bind, hlz, hdone]
88      simp only [setI_setI]
89    have hgood : Good3 (llDone s S).lens 19 := by
90      rw [llDone_lens s S hnc hhn]
91      have g1 := lensRead_good (a := s.lens) (i0 := s.«have».toNat) S hG (s.ncode.toNat - s.«have».toNat) (by omega)
92      rw [show s.«have».toNat + (s.ncode.toNat - s.«have».toNat) = s.ncode.toNat by omega] at g1
93      have g2 := lensZero_good g1 (19 - s.ncode.toNat) (by omega)
94      rwa [show s.ncode.toNat + (19 - s.ncode.toNat) = 19 by omega] at g2
95    have hwf' : (llDone s S).WellFormed := by
96      refine ⟨?_, ?_, ?_⟩
97      · rw [llDone_lens s S hnc hhn, lensZero_size, lensRead_size]; exact hl
98      · exact hw
99      · exact hcs
100    have hs' : (setI h zs (llDone s S)).istates zs = some (llDone s S) := by simp
101    have hz' : r.get (setI h zs (llDone s S)) = some z := by simpa using hz
102    obtain ⟨ret, wa', ca', hwa, hca, hfw, hfc, hret, hacc, hz0, hz1⟩ := llTail_run (c := c) (l := l') hr hc hz' hs' hwf' hgood
103    refine ⟨ret, wa', ca', hwa, hca, ?_, ?_, hret, hacc, ?_, ?_⟩
104    · intro x hx; rw [hfw x hx]; simp [llDone, lzSt, llSt]
105    · intro x hx; rw [hfc x hx]; simp [llDone, lzSt, llSt]
106    · intro h0
107      obtain ⟨u, lb, hu, hrunu⟩ := hz0 h0
108      exact ⟨u, lb, hu, by rw [hmain, hrunu]; simp only [setI_setI]⟩
109    · intro h0
110      obtain ⟨i, hi, hrunb⟩ := hz1 h0
111      refine ⟨i, hi, ?_⟩
112      rw [hmain, hrunb]
113      simp only [setI_setI]
114
115end Zlib.Inflate.Proofs