inflate.c.main.table5.lean

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

1import ZlibF.Proof.«inflate.c.main.table4»
2import ZlibF.Proof.«inftrees.c»
3
4/-!
5# inflate.c: `case LENLENS:` -- the `inflate_table(CODES, ...)` call and what follows
6-/
7
8namespace Zlib.Inflate.Proofs
9open C Zlib.Inflate Zlib.Inflate.Spec
10open Zlib.Inftrees (inflate_table)
11
12/-- Storing the arrays `work` and `codes` of the state record. -/
13theorem put_work_codes {h : Heap} {zs : Nat} {s : InflateState} (e : h.istates zs = some s) (wa : Array UInt16)
14    (ca : Array Code) :
15    Space.put (Space.put h (WRef.istate_work zs) wa) (CodeRef.istate_codes zs) ca =
16      setI h zs { s with work := wa, codes := ca } := by
17  rw [WRef.put_istate_work e wa]
18  have e2 : ({ h with istates := upd h.istates zs (some { s with work := wa }) } : Heap).istates zs =
19      some { s with work := wa } := by simp
20  rw [CodeRef.put_istate_codes e2 ca]
21  simp [setI, upd_upd]
22
23/-- The state record after `state->next = state->codes; state->lencode = state->distcode = state->next; state->lenbits = 7`. -/
24def llPre (zs : Nat) (s : InflateState) : InflateState :=
25  { s with next := .ref (.istate_codes zs) 0, distcode := .ref (.istate_codes zs) 0, lencode := .ref (.istate_codes zs) 0, lenbits := 7 }
26
27/-- The state record after a successful table call: `next` moved, `lenbits` as the call left it, `work` and `codes` changed;
28`have = 0`, `mode = CODELENS`. -/
29def llOkSt (zs : Nat) (s : InflateState) (u : Nat) (lb : UInt32) (wa : Array UInt16) (ca : Array Code) : InflateState :=
30  { llPre zs s with next := .ref (.istate_codes zs) u, lenbits := lb, work := wa, codes := ca, «have» := 0, mode := CODELENS }
31
32theorem eta_next_lenbits (x : InflateState) (n : CodePtr) (b : UInt32) (hn : x.next = n) (hb : x.lenbits = b) :
33    { x with next := n, lenbits := b } = x := by
34  cases x; simp_all
35
36/-- The state record when the table call rejected the lengths (before `BAD` is set). -/
37def llBadSt (zs : Nat) (s : InflateState) (wa : Array UInt16) (ca : Array Code) : InflateState :=
38  { llPre zs s with work := wa, codes := ca }
39
40/-- **The rest of `LENLENS`**: with the 19 code-length code lengths in `lens` (each at most 7), the call
41`inflate_table(CODES, lens, 19, &next, &lenbits, work)` returns `0` or `-1` (`-1` exactly when the 19 lengths are not an
42acceptable code in the format specification), changes `work` only below 19 and `codes` only below 128; for `-1` the error
43"invalid code lengths set" (`BAD`, `break`); for `0` `have = 0`, `mode = CODELENS` and the fall-through into `CODELENS`.
44`lenbits` and the position of `next` after the call are those that `inflate_table` leaves (`u ≤ 128`, `lb`); their
45relation to the table is the content theorem of `inflate_table`. -/
46theorem llTail_run {c : Ctx} {l : IL} {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState}
47    (hr : c.strm = some r) (hc : c.st = some (.tab zs)) (hz : r.get h = some z) (hs : h.istates zs = some s)
48    (hwf : s.WellFormed) (hG : Good3 s.lens 19) :
49    ∃ (ret : Int32) (wa' : Array UInt16) (ca' : Array Code), wa'.size = 288 ∧ ca'.size = 1444 ∧
50      (∀ x, 19 ≤ x → wa'[x]? = s.work[x]?) ∧ (∀ x, 128 ≤ x → ca'[x]? = s.codes[x]?) ∧
51      (ret = 0 ∨ ret = -1) ∧
52      (ret = -1 ↔ ¬ ZlibF.Spec.Acceptable .codeLength (Zlib.Inftrees.Spec.lensList s.lens 0 19)) ∧
53      (ret = 0 → ∃ u lb, u ≤ 128 ∧ runX (llTail c) l h = runX (inflate_CODELENS c) { l with ret := 0 }
54        (setI h zs (llOkSt zs s u lb wa' ca'))) ∧
55      (ret = -1 → ∃ i, strTable[i]? = some "invalid code lengths set" ∧
56        runX (llTail c) l h = .ok ((.ok (), { l with ret := -1 }),
57          tcBadHeap (setI h zs (llBadSt zs s wa' ca')) r zs z (llBadSt zs s wa' ca') i)) := by
58  obtain ⟨hl, hw, hcs⟩ := hwf
59  have hs2 : (setI h zs (llPre zs s)).istates zs = some (llPre zs s) := by simp
60  have hgl : Space.get (setI h zs (llPre zs s)) (WRef.istate_lens zs) = some s.lens := by simpa [llPre] using WRef.get_istate_lens hs2
61  have hgw : Space.get (setI h zs (llPre zs s)) (WRef.istate_work zs) = some s.work := by simpa [llPre] using WRef.get_istate_work hs2
62  have hgc : Space.get (setI h zs (llPre zs s)) (CodeRef.istate_codes zs) = some s.codes := by simpa [llPre] using CodeRef.get_istate_codes hs2
63  have hf7 := hG.all
64  have hf15 : ∀ k, k < (19 : UInt32).toNat → (s.lens.getD (0 + k) 0).toNat ≤ 15 := by
65    intro k hk
66    have := hf7 k (by simpa using hk)
67    simpa using (by omega : (s.lens.getD k 0).toNat ≤ 15)
68  have hcodes : CODES = CODES → (19 : UInt32).toNat ≤ 19 ∧ (∀ k, k < (19 : UInt32).toNat → (s.lens.getD (0 + k) 0).toNat ≤ 7) ∧
69      7 ≤ (7 : UInt32).toNat := by
70    intro _
71    refine ⟨by decide, fun k hk => ?_, by decide⟩
72    simpa using hf7 k (by simpa using hk)
73  have hcap : 0 + Zlib.Inftrees.Spec.capOf CODES ≤ s.codes.size := by
74    simp [Zlib.Inftrees.Spec.capOf, CODES]; omega
75  have hne : WRef.istate_work zs ≠ WRef.istate_lens zs := by simp
76  have hl19 : 0 + (19 : UInt32).toNat ≤ s.lens.size := by simp; omega
77  have hw19 : 0 + (19 : UInt32).toNat ≤ s.work.size := by simp; omega
78  have hty : CODES = CODES ∨ CODES = LENS ∨ CODES = DISTS := Or.inl rfl
79  have hlens : CODES = LENS → (19 : UInt32).toNat ≤ 288 := fun e => absurd e (by decide)
80  have hdists : CODES = DISTS → (19 : UInt32).toNat ≤ 32 := fun e => absurd e (by decide)
81  obtain ⟨rr, h3, hrun, hres⟩ := Zlib.Inftrees.Proofs.inflate_table_safe (setI h zs (llPre zs s)) CODES (WRef.istate_lens zs) 0 19
82    (CodeRef.istate_codes zs) 0 7 (WRef.istate_work zs) 0 s.lens s.work s.codes hty hgl hgw hgc (by simp) hne hl19 hw19 hcap
83    hf15 hcodes hlens hdists
84  obtain ⟨rr', h3', hrun', hacc1, hacc0, hacc2⟩ := Zlib.Inftrees.Proofs.inflate_table_correct_ret (setI h zs (llPre zs s)) CODES
85    (WRef.istate_lens zs) 0 19 (CodeRef.istate_codes zs) 0 7 (WRef.istate_work zs) 0 s.lens s.work s.codes hty hgl hgw hgc
86    (by simp) hne hl19 hw19 hcap hf15 hcodes hlens hdists
87  rw [hrun] at hrun'
88  cases hrun'
89  obtain ⟨ret, nx, lb⟩ := rr
90  obtain ⟨wa', ca', hh3, hwa, hca, hfw, hfc, hout⟩ := hres
91  have hh3' : h3 = setI h zs (llBadSt zs s wa' ca') := by
92    rw [hh3, put_work_codes hs2]
93    simp [setI_setI, llBadSt, llPre]
94  have hk : Zlib.Inftrees.Spec.kindOf CODES = ZlibF.Spec.CodeKind.codeLength := by simp [Zlib.Inftrees.Spec.kindOf]
95  rw [hk] at hacc1 hacc0 hacc2
96  have hrun2 : inflate_table CODES (.ref (WRef.istate_lens zs) 0) 19 (.ref (CodeRef.istate_codes zs) 0) 7
97      (.ref (WRef.istate_work zs) 0) (setI h zs (llPre zs s)) = .ok ((ret, nx, lb), h3) := hrun
98  have hret : ret = 0 ∨ ret = -1 := by
99    rcases hout with ⟨h0, _⟩ | ⟨h1 | h1, _⟩
100    · exact Or.inl h0
101    · exact absurd rfl (hacc2 h1).2
102    · exact Or.inr h1
103  refine ⟨ret, wa', ca', by rw [hwa]; exact hw, by rw [hca]; exact hcs, fun x hx => hfw x (Or.inr (by simpa using hx)),
104    fun x hx => hfc x (Or.inr (by simpa [Zlib.Inftrees.Spec.capOf, CODES] using hx)), hret, hacc1, ?_, ?_⟩
105  · intro h0
106    rcases hout with ⟨_, u, hu, hnx⟩ | ⟨h1 | h1, _⟩
107    · refine ⟨u, lb, by simpa [Zlib.Inftrees.Spec.capOf, CODES] using hu, ?_⟩
108      unfold llTail
109      rw [hc]
110      have hrun3 := hrun2
111      simp [llPre] at hrun3
112      simp [runX_bind, runX_lift, wrI_eq, ldI_eq, hs, lensP, workP, codesP, hrun3, hh3', h0, runX_modify, setMode]
113      subst hnx
114      simp [llBadSt, llOkSt, llPre]
115    · rw [h0] at h1; cases h1
116    · rw [h0] at h1; cases h1
117  · intro hm
118    rcases hout with ⟨h0, _⟩ | ⟨_, hnx, hlb⟩
119    · rw [hm] at h0; cases h0
120    · have hs3 : (setI h zs (llBadSt zs s wa' ca')).istates zs = some (llBadSt zs s wa' ca') := by simp
121      have hz3 : r.get (setI h zs (llBadSt zs s wa' ca')) = some z := by simpa using hz
122      obtain ⟨i, hi, hbm⟩ := tcBadMode_run (c := c) "invalid code lengths set" lit_code_lengths hr hc hz3 hs3
123      refine ⟨i, hi, ?_⟩
124      have hbm2 := hbm
125      simp [llBadSt, llPre, tcBadHeap] at hbm2
126      have hrun3 := hrun2
127      simp [llPre] at hrun3
128      unfold llTail
129      rw [hc]
130      subst hnx hlb
131      have hnx' : (llBadSt zs s wa' ca').next = .ref (.istate_codes zs) 0 := by simp [llBadSt, llPre]
132      have hlb' : (llBadSt zs s wa' ca').lenbits = 7 := by simp [llBadSt, llPre]
133      have hetaB : ({ llBadSt zs s wa' ca' with next := .ref (.istate_codes zs) 0, lenbits := 7 } : InflateState) =
134          llBadSt zs s wa' ca' := eta_next_lenbits _ _ _ hnx' hlb'
135      simp [runX_bind, runX_lift, wrI_eq, ldI_eq, hs, lensP, workP, codesP, hrun3, hh3', hm, runX_modify, runX_pure, hetaB]
136      rw [hbm]
137
138end Zlib.Inflate.Proofs