inftrees.c.lean

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

1import ZlibF.Proof.«inftrees.c.main»
2
3/-!
4# inftrees.c: safety of `inflate_table`
5
6The statement is `Zlib.Inftrees.Proofs.inflate_table_safe`. The proof is in the modules `inftrees.c.proofs.math`
7(arithmetic of canonical codes), `.base` (the reasoning rules for the monad, the heap lemmas, the translation cut at
8its join points), `.step` (one pass of the main loop) and `.main` (the other loops and the assembly).
9-/
10
11namespace Zlib.Inftrees.Proofs
12open C Zlib.Inftrees Zlib.Inftrees.Spec
13
14/-- **inflate_table, safety.** Take the call `inflate_table(type, lens, codes, table, bits, work)` with `lens` the
15array `la` from offset `ol`, `work` the array `wa` from offset `ow`, and `*table` the array `ca` from offset `oc`
16(`code` entries), `*bits` the value `bits`, in any heap `h` in which
17
18* `type` is `CODES`, `LENS` or `DISTS`;
19* `lens` has at least `codes` entries, each at most 15 (`MAXBITS`; the C only assumes it), and `work` has at least
20  `codes` entries; `lens` and `work` are different arrays;
21* `ca` is writable and has at least `Spec.capOf type` entries from `oc` on: 128 for `CODES`, `ENOUGH_LENS` (852) for
22  `LENS`, `ENOUGH_DISTS` (592) for `DISTS`, which is what `inflate.c` provides;
23* `codes` is at most 19 (`CODES`), 288 (`LENS`; `inflate.c` has at most 286) or 32 (`DISTS`; `inflate.c` has at most
24  30), so that `work[sym] - match` stays inside the 31 or 32 entries of `lbase`, `lext`, `dbase`, `dext`;
25* for `CODES` every length is at most 7 and `*bits` is at least 7 (the caller passes `7`): without them a `CODES`
26  table could open sub-tables, which the C does not guard against with `ENOUGH`.
27
28`*bits` is arbitrary for `LENS` and `DISTS`; incomplete and over-subscribed codes are allowed (they return `-1`).
29
30Then the call ends without undefined behaviour (no fault, no write outside the table or `work`, no read outside
31`lens`, `work` and the tables of base values), and `Spec.Result` holds: only `work` (inside `[ow, ow + codes)`) and
32the table (inside `[oc, oc + cap)`) changed, the result is `0`, `1` or `-1`, and for `0` the table pointer moved
33forward inside the space given. -/
34theorem inflate_table_safe (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32) (rc : CodeRef)
35    (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat) (la wa : Array UInt16) (ca : Array Code)
36    (hty : type = CODES ∨ type = LENS ∨ type = DISTS)
37    (hgl : Space.get h rl = some la) (hgw : Space.get h rw = some wa) (hgc : Space.get h rc = some ca)
38    (hro : Space.ro h rc = false) (hne : rw ≠ rl)
39    (hla : ol + codes.toNat ≤ la.size) (hwa : ow + codes.toNat ≤ wa.size) (hca : oc + capOf type ≤ ca.size)
40    (hf15 : ∀ k, k < codes.toNat → (la.getD (ol + k) 0).toNat ≤ 15)
41    (hcodes : type = CODES → codes.toNat ≤ 19 ∧ (∀ k, k < codes.toNat → (la.getD (ol + k) 0).toNat ≤ 7) ∧
42      7 ≤ bits.toNat)
43    (hlens : type = LENS → codes.toNat ≤ 288) (hdists : type = DISTS → codes.toNat ≤ 32) :
44    ∃ r h', C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h = .ok (r, h') ∧
45      Result h rw rc ow oc (capOf type) codes.toNat wa ca (.ref rc oc) bits r h' := by
46  let P : CallPre h type rl ol codes rc oc bits rw ow :=
47    ⟨la, wa, ca, hty, hgl, hgw, hgc, hro, hne, hla, hwa, hca, hf15, hcodes, hlens, hdists⟩
48  obtain ⟨r, h', hrun, hq, _⟩ := itTop_wp P
49  exact ⟨r, h', by rw [C.run, inflate_table_eq]; exact hrun, hq⟩
50
51
52/-- **inflate_table, return code.** Under the hypotheses of `inflate_table_safe`, the call returns `-1` exactly
53when the lengths `lens[0 .. codes-1]` are not acceptable to `inflate_table` in the specification
54(`ZlibF.Spec.Acceptable`: no length above 15, the Kraft inequality holds, and the code is complete, or has no
55symbol, or (not for the code-length code) has one symbol, of length 1). It returns `0` or `1` only for acceptable
56lengths, and `1` (table too large for `ENOUGH_LENS` / `ENOUGH_DISTS`) only for `LENS` or `DISTS`.
57
58Callers covered. `inflate.c` (and `infback.c`) call `inflate_table(CODES, lens, 19, &next, &lenbits(=7), work)` on
593-bit lengths (so at most 7), `inflate_table(LENS, lens, nlen, ...)` with `nlen <= 286` and
60`inflate_table(DISTS, lens + nlen, ndist, ...)` with `ndist <= 30`, with `next` inside `codes[1444]` such that at
61least 852 (`LENS`) or 592 (`DISTS`) entries remain, and `work[288]`. These satisfy the hypotheses: `CODES` needs
62`codes <= 19`, every length `<= 7` and `bits >= 7` (they pass exactly 7); `LENS` needs `codes <= 288`; `DISTS` needs
63`codes <= 32`. The theorem is wider than the callers in `codes` (288 and 32 instead of 286 and 30) and in `bits`
64(arbitrary for `LENS` and `DISTS`). The fixed-code tables are not built by `inflate_table` in the default build. -/
65theorem inflate_table_correct_ret (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32) (rc : CodeRef)
66    (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat) (la wa : Array UInt16) (ca : Array Code)
67    (hty : type = CODES ∨ type = LENS ∨ type = DISTS)
68    (hgl : Space.get h rl = some la) (hgw : Space.get h rw = some wa) (hgc : Space.get h rc = some ca)
69    (hro : Space.ro h rc = false) (hne : rw ≠ rl)
70    (hla : ol + codes.toNat ≤ la.size) (hwa : ow + codes.toNat ≤ wa.size) (hca : oc + capOf type ≤ ca.size)
71    (hf15 : ∀ k, k < codes.toNat → (la.getD (ol + k) 0).toNat ≤ 15)
72    (hcodes : type = CODES → codes.toNat ≤ 19 ∧ (∀ k, k < codes.toNat → (la.getD (ol + k) 0).toNat ≤ 7) ∧
73      7 ≤ bits.toNat)
74    (hlens : type = LENS → codes.toNat ≤ 288) (hdists : type = DISTS → codes.toNat ≤ 32) :
75    ∃ r h', C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h = .ok (r, h') ∧
76      (r.1 = -1 ↔ ¬ ZlibF.Spec.Acceptable (kindOf type) (lensList la ol codes.toNat)) ∧
77      (r.1 = 0 → ZlibF.Spec.Acceptable (kindOf type) (lensList la ol codes.toNat)) ∧
78      (r.1 = 1 → ZlibF.Spec.Acceptable (kindOf type) (lensList la ol codes.toNat) ∧ type ≠ CODES) := by
79  let P : CallPre h type rl ol codes rc oc bits rw ow :=
80    ⟨la, wa, ca, hty, hgl, hgw, hgc, hro, hne, hla, hwa, hca, hf15, hcodes, hlens, hdists⟩
81  obtain ⟨r, h', hrun, hres, hr0, hr1, hrm⟩ := itTop_wp P
82  have hacc := acc_iff type P.f codes.toNat hf15
83  have e : lensOf P.f codes.toNat = lensList la ol codes.toNat := rfl
84  rw [e] at hacc
85  have hr3 : r.1 = 0 ∨ r.1 = 1 ∨ r.1 = -1 := by
86    obtain ⟨_, _, _, _, _, _, _, hr⟩ := hres
87    rcases hr with ⟨h0, _⟩ | ⟨h1 | h1, _⟩
88    · exact Or.inl h0
89    · exact Or.inr (Or.inl h1)
90    · exact Or.inr (Or.inr h1)
91  refine ⟨r, h', by rw [C.run, inflate_table_eq]; exact hrun, ⟨fun hm hA => hrm hm (hacc.mpr hA), fun hn => ?_⟩,
92    fun h0 => hacc.mp (hr0 h0), fun h1 => ⟨hacc.mp (hr1 h1).1, (hr1 h1).2⟩⟩
93  rcases hr3 with h0 | h1 | hm
94  · exact absurd (hacc.mp (hr0 h0)) hn
95  · exact absurd (hacc.mp (hr1 h1).1) hn
96  · exact hm
97
98/-! ### Non-vacuity
99
100A heap made by the runtime: `allocInflateState` gives the inflate state, and the first three entries of its `lens`
101array are set with `Ptr.store` to the lengths `1, 2, 2` (a complete code). -/
102
103/-- The heap of the examples. -/
104def witHeap : Heap :=
105  match C.run (do
106      let st ← allocInflateState
107      Ptr.store (Ptr.ref (WRef.istate_lens 0) 0) (1 : UInt16)
108      Ptr.store (Ptr.ref (WRef.istate_lens 0) 1) (2 : UInt16)
109      Ptr.store (Ptr.ref (WRef.istate_lens 0) 2) (2 : UInt16)
110      pure st) Heap.empty with
111  | .ok (_, h) => h
112  | .error _ => Heap.empty
113
114set_option maxRecDepth 100000 in
115set_option maxHeartbeats 4000000 in
116/-- All hypotheses of `inflate_table_safe` hold on `witHeap`, for the call `inflate_table(DISTS, state->lens, 3,
117&state->next, 5, state->work)`, and the conclusion is an actual run. -/
118example : ∃ r h', C.run (inflate_table DISTS (.ref (WRef.istate_lens 0) 0) 3 (.ref (CodeRef.istate_codes 0) 0) 5
119      (.ref (WRef.istate_work 0) 0)) witHeap = .ok (r, h') ∧
120    Result witHeap (WRef.istate_work 0) (CodeRef.istate_codes 0) 0 0 (capOf DISTS) 3
121      (witHeap.istates 0).get!.work (witHeap.istates 0).get!.codes (.ref (CodeRef.istate_codes 0) 0) 5 r h' :=
122  inflate_table_safe witHeap DISTS (WRef.istate_lens 0) 0 3 (CodeRef.istate_codes 0) 0 5 (WRef.istate_work 0) 0
123    (witHeap.istates 0).get!.lens (witHeap.istates 0).get!.work (witHeap.istates 0).get!.codes
124    (Or.inr (Or.inr rfl)) rfl rfl rfl rfl (by decide) (by decide +kernel) (by decide +kernel) (by decide +kernel) (by decide +kernel)
125    (fun h => absurd h (by decide)) (fun h => absurd h (by decide)) (fun _ => by decide +kernel)
126
127set_option maxRecDepth 100000 in
128set_option maxHeartbeats 4000000 in
129/-- The run is a real one: the call returns `0`, the table pointer advances by 4 entries (the root has 2 bits, the longest
130length) and `*bits` becomes 2. -/
131example : ((C.run (inflate_table DISTS (.ref (WRef.istate_lens 0) 0) 3 (.ref (CodeRef.istate_codes 0) 0) 5
132      (.ref (WRef.istate_work 0) 0)) witHeap).toOption.map (fun p => (p.1.1, p.1.2.1, p.1.2.2))) =
133    some (0, .ref (CodeRef.istate_codes 0) 4, 2) := by decide +kernel
134
135end Zlib.Inftrees.Proofs