deflate.c.life.check.lean

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

1import ZlibF.Proof.«deflate.c.base»
2
3/-!
4# deflate.c: `deflateTune`, `deflateSetHeader`, `deflateUsed`, `deflatePending`
5
6The four small functions that read or set a few fields of an initialised stream. Each starts with the stream check
7(`deflateStateCheck`); on a stream the check refuses it returns `Z_STREAM_ERROR` and changes nothing.
8-/
9
10namespace Zlib.Deflate.Spec
11open C
12
13/-- The state record after `deflateTune`: the four tuning fields are the arguments (`int` to `unsigned` for three of
14them, which wraps; `nice_match` is an `int`). -/
15def tuneD (d : DeflateState) (good_length max_lazy nice_length max_chain : Int32) : DeflateState :=
16  { d with good_match := good_length.toUInt32, max_lazy_match := max_lazy.toUInt32, nice_match := nice_length,
17           max_chain_length := max_chain.toUInt32 }
18
19/-- The state record after `deflateSetHeader` on a gzip stream: the header pointer is stored. -/
20def setHeaderD (d : DeflateState) (head : GzHeaderPtr) : DeflateState := { d with gzhead := head }
21
22end Zlib.Deflate.Spec
23
24namespace Zlib.Deflate.Proofs
25open C Zlib.Deflate Zlib.Deflate.Spec
26
27/-! ### deflateTune -/
28
29theorem deflateTune_run {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
30    (hL : DLive h r ds z d) (g m n c : Int32) :
31    deflateTune (some r) g m n c h = .ok (Z_OK, setD h ds (tuneD d g m n c)) := by
32  unfold deflateTune
33  dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, tuneD]
34
35theorem _root_.Zlib.Deflate.Spec.DStInv.tune {h : Heap} {ds : Nat} {d : DeflateState} (hI : DStInv h ds d) (g m n c : Int32) :
36    DStInv h ds (tuneD d g m n c) :=
37  { hI with blocks := hI.blocks_keys rfl rfl rfl rfl rfl rfl rfl rfl rfl rfl }
38
39/-- **deflateTune, safety and specification.** On an initialised stream (any `int` arguments, including negative ones,
40which `zlib.h` leaves to the caller) the call returns `Z_OK` and never faults. It changes the four tuning fields of the
41state record and nothing else: `good_match`, `max_lazy_match` and `max_chain_length` become the arguments converted to
42`unsigned`, `nice_match` the argument. The stream is initialised again with the invariants intact, and the live
43blocks are the same (no allocation, no free). -/
44theorem deflateTune_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
45    (hG : DGood h r ds z d) (g m n c : Int32) :
46    ∃ h', C.run (deflateTune (some r) g m n c) h = .ok (Z_OK, h') ∧ h' = setD h ds (tuneD d g m n c) ∧
47      DGood h' r ds z (tuneD d g m n c) ∧ (∀ b, h'.live b ↔ h.live b) := by
48  refine ⟨_, deflateTune_run hG.live g m n c, rfl, ?_, ?_⟩
49  · exact hG.setD' (d' := tuneD d g m n c) rfl hG.live.status (hG.inv.tune g m n c) (by trkeep)
50  · intro b; exact (shape_setD hG.live.hs _).live b
51
52/-- **deflateTune, refusal.** On a stream the check refuses (including `NULL`), the call returns `Z_STREAM_ERROR` and
53changes nothing. -/
54theorem deflateTune_reject {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm)
55    (g m n c : Int32) : C.run (deflateTune strm g m n c) h = .ok (Z_STREAM_ERROR, h) := by
56  unfold deflateTune
57  exact check_refuse hD hN _ _
58
59
60/-! ### deflateSetHeader -/
61
62theorem deflateSetHeader_run_gz {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
63    (hL : DLive h r ds z d) (hw : d.wrap = 2) (head : GzHeaderPtr) :
64    deflateSetHeader (some r) head h = .ok (Z_OK, setD h ds (setHeaderD d head)) := by
65  unfold deflateSetHeader
66  dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, setHeaderD, hw]
67
68theorem deflateSetHeader_run_other {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
69    (hL : DLive h r ds z d) (hw : d.wrap ≠ 2) (head : GzHeaderPtr) :
70    deflateSetHeader (some r) head h = .ok (Z_STREAM_ERROR, h) := by
71  unfold deflateSetHeader
72  dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw]
73
74theorem _root_.Zlib.Deflate.Spec.DStInv.setHeader {h : Heap} {ds : Nat} {d : DeflateState} (hI : DStInv h ds d)
75    (head : GzHeaderPtr) (hg : GzOk h head) : DStInv h ds (setHeaderD d head) :=
76  { hI with blocks := hI.blocks_keys rfl rfl rfl rfl rfl rfl rfl rfl rfl rfl, gz := hg }
77
78/-- **deflateSetHeader, safety and specification (gzip stream).** On an initialised stream whose wrapper is gzip
79(`wrap = 2`) and for a header pointer that is `NULL` or a live `gz_header` record, the call returns `Z_OK`, never
80faults, and stores the pointer in the state (`gzhead`); nothing else changes. The stream is initialised again with the
81invariants intact; no block is allocated or freed. (`zlib.h` requires the header to stay valid until the header has
82been written; that concerns the later calls of `deflate`, not this one.) -/
83theorem deflateSetHeader_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
84    (hG : DGood h r ds z d) (hw : d.wrap = 2) (head : GzHeaderPtr) (hg : GzOk h head) :
85    ∃ h', C.run (deflateSetHeader (some r) head) h = .ok (Z_OK, h') ∧ h' = setD h ds (setHeaderD d head) ∧
86      DGood h' r ds z (setHeaderD d head) ∧ (∀ b, h'.live b ↔ h.live b) := by
87  refine ⟨_, deflateSetHeader_run_gz hG.live hw head, rfl, ?_, ?_⟩
88  · exact hG.setD' (d' := setHeaderD d head) rfl hG.live.status (hG.inv.setHeader head hg) (by trkeep)
89  · intro b; exact (shape_setD hG.live.hs _).live b
90
91/-- **deflateSetHeader on a stream that is not gzip.** `Z_STREAM_ERROR`, nothing changes. -/
92theorem deflateSetHeader_not_gzip {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
93    (hL : DLive h r ds z d) (hw : d.wrap ≠ 2) (head : GzHeaderPtr) :
94    C.run (deflateSetHeader (some r) head) h = .ok (Z_STREAM_ERROR, h) :=
95  deflateSetHeader_run_other hL hw head
96
97/-- **deflateSetHeader, refusal.** On a stream the check refuses (including `NULL`): `Z_STREAM_ERROR`, nothing changes. -/
98theorem deflateSetHeader_reject {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm)
99    (head : GzHeaderPtr) : C.run (deflateSetHeader strm head) h = .ok (Z_STREAM_ERROR, h) := by
100  unfold deflateSetHeader
101  exact check_refuse hD hN _ _
102
103/-! ### deflateUsed -/
104
105theorem deflateUsed_run {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
106    (hL : DLive h r ds z d) (hasBits : Bool) :
107    deflateUsed (some r) hasBits h = .ok ((Z_OK, if hasBits then some d.bi_used else none), h) := by
108  unfold deflateUsed
109  dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs]
110
111/-- **deflateUsed, safety and specification.** On an initialised stream the call returns `Z_OK` and, when the pointer
112`bits` is not `NULL` (`hasBits`), the value `bi_used` that would be stored through it; the heap is unchanged. -/
113theorem deflateUsed_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
114    (hL : DLive h r ds z d) (hasBits : Bool) :
115    C.run (deflateUsed (some r) hasBits) h = .ok ((Z_OK, if hasBits then some d.bi_used else none), h) :=
116  deflateUsed_run hL hasBits
117
118/-- **deflateUsed, refusal.** `Z_STREAM_ERROR`, no value stored, nothing changes. -/
119theorem deflateUsed_reject {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm)
120    (hasBits : Bool) : C.run (deflateUsed strm hasBits) h = .ok ((Z_STREAM_ERROR, none), h) := by
121  unfold deflateUsed
122  exact check_refuse hD hN _ _
123
124/-! ### deflatePending -/
125
126/-- What `deflatePending` returns for the state record `d`: the pending count does not fit `unsigned` only if
127`pending >= 2^32`, in which case the C stores `(unsigned)-1` and returns `Z_BUF_ERROR`. -/
128def pendingResult (d : DeflateState) (hasPending hasBits : Bool) : Int32 × Option UInt32 × Option Int32 :=
129  let bits := if hasBits then some d.bi_valid else none
130  if hasPending then
131    if d.pending.toUInt32.toUInt64 != d.pending then (Z_BUF_ERROR, some 0xffffffff, bits)
132    else (Z_OK, some d.pending.toUInt32, bits)
133  else (Z_OK, none, bits)
134
135theorem deflatePending_run {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
136    (hL : DLive h r ds z d) (hasPending hasBits : Bool) :
137    deflatePending (some r) hasPending hasBits h = .ok (pendingResult d hasPending hasBits, h) := by
138  unfold deflatePending
139  cases hasPending <;> cases hasBits <;> dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, pendingResult] <;>
140    split <;> simp_all
141
142/-- **deflatePending, safety and specification.** On an initialised stream with the invariant the call never faults
143and returns `Z_OK`; the count stored through `pending` (when it is not `NULL`) is exactly the number of pending output
144bytes, and the value stored through `bits` is `bi_valid`. The heap is unchanged. (The count is at most
145`4 * lit_bufsize <= 2^17`, so the overflow case of the C, `Z_BUF_ERROR` with `(unsigned)-1`, cannot happen.) -/
146theorem deflatePending_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
147    (hG : DGood h r ds z d) (hasPending hasBits : Bool) :
148    C.run (deflatePending (some r) hasPending hasBits) h =
149      .ok ((Z_OK, (if hasPending then some d.pending.toUInt32 else none), (if hasBits then some d.bi_valid else none)), h) ∧
150    (hasPending = true → d.pending.toUInt32.toNat = d.pending.toNat) := by
151  have hI := hG.inv
152  obtain ⟨w, p, q, b, hB⟩ := hI.blocks
153  obtain ⟨off, -, hpl⟩ := hB.pout
154  have hlit : d.lit_bufsize.toNat ≤ 32768 := by
155    have := hI.lit; have := hI.hsize; have := hI.hbits_hi
156    have : 2 ^ d.hash_bits.toNat ≤ 2 ^ 16 := Nat.pow_le_pow_right (by omega) hI.hbits_hi
157    omega
158  have hpend : d.pending.toNat < 2 ^ 32 := by
159    have := hB.psize; omega
160  have e1 : d.pending.toUInt32.toUInt64 = d.pending := by
161    apply UInt64.toNat_inj.mp
162    rw [UInt32.toNat_toUInt64, UInt64.toNat_toUInt32]
163    exact Nat.mod_eq_of_lt hpend
164  have e2 : d.pending.toUInt32.toNat = d.pending.toNat := by
165    rw [UInt64.toNat_toUInt32]; exact Nat.mod_eq_of_lt hpend
166  refine ⟨?_, fun _ => e2⟩
167  have := deflatePending_run hG.live hasPending hasBits
168  rw [C.run, this]
169  simp [pendingResult, e1]
170  cases hasPending <;> cases hasBits <;> simp
171
172/-- **deflatePending, refusal.** `Z_STREAM_ERROR`, no value stored, nothing changes. -/
173theorem deflatePending_reject {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm)
174    (hasPending hasBits : Bool) :
175    C.run (deflatePending strm hasPending hasBits) h = .ok ((Z_STREAM_ERROR, none, none), h) := by
176  unfold deflatePending
177  exact check_refuse hD hN _ _
178
179end Zlib.Deflate.Proofs