inflate.c.hdr.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.misc2»
2import ZlibF.Proof.«inflate.c.start»
3
4/-!
5# inflate.c: `inflateGetHeader` and `inflateInit_`
6
7`inflateGetHeader` stores the caller's `gz_header` pointer in the state and clears the header's `done` field; it
8refuses a stream that does not accept gzip. `inflateInit_` is `inflateInit2_` with `DEF_WBITS` (15), so its theorems are
9those of `inflateInit2_` (`inflateInit2_safe`, `inflateInit2_ok`) with the window bits fixed.
10-/
11
12namespace Zlib.Inflate.Proofs
13open C Zlib.Inflate Zlib.Inflate.Spec
14
15/-! ### The heap after a store into a `gz_header` -/
16
17theorem shape_putG {h : Heap} {g : GzHeaderRef} {gh : GzHeader} (e : g.get h = some gh) (v : GzHeader) :
18    Shape h (g.put h v) := by
19  cases g with
20  | tab i =>
21    simp only [GzHeaderRef.get] at e
22    intro b
23    by_cases hb : b = i
24    · subst hb; simp [GzHeaderRef.put, e]
25    · simp [GzHeaderRef.put, e, upd_ne _ _ _ _ hb]
26
27@[simp] theorem ZStreamRef.get_putG (h : Heap) (r : ZStreamRef) (g : GzHeaderRef) (v : GzHeader) :
28    r.get (g.put h v) = r.get h := by
29  cases g with
30  | tab i => cases r <;> simp only [GzHeaderRef.put, ZStreamRef.get] <;> split <;> rfl
31
32@[simp] theorem GzHeaderRef.put_istates (h : Heap) (g : GzHeaderRef) (v : GzHeader) : (g.put h v).istates = h.istates := by
33  cases g with
34  | tab i => simp only [GzHeaderRef.put]; split <;> rfl
35@[simp] theorem GzHeaderRef.put_bytes (h : Heap) (g : GzHeaderRef) (v : GzHeader) : (g.put h v).bytes = h.bytes := by
36  cases g with
37  | tab i => simp only [GzHeaderRef.put]; split <;> rfl
38@[simp] theorem GzHeaderRef.put_ro (h : Heap) (g : GzHeaderRef) (v : GzHeader) : (g.put h v).ro = h.ro := by
39  cases g with
40  | tab i => simp only [GzHeaderRef.put]; split <;> rfl
41@[simp] theorem GzHeaderRef.put_nextBlk (h : Heap) (g : GzHeaderRef) (v : GzHeader) : (g.put h v).nextBlk = h.nextBlk := by
42  cases g with
43  | tab i => simp only [GzHeaderRef.put]; split <;> rfl
44
45theorem setI_putG (h : Heap) (g : GzHeaderRef) (v : GzHeader) (zs : Nat) (s : InflateState) :
46    setI (g.put h v) zs s = g.put (setI h zs s) v := by
47  cases g with
48  | tab i => simp only [GzHeaderRef.put, setI]; split <;> rfl
49
50/-! ### inflateGetHeader -/
51
52/-- **inflateGetHeader, refusal.** If the state check fails (`StreamDom`: the stream is `NULL` or a live record whose
53state is not a usable inflate state) the call returns `Z_STREAM_ERROR` and changes nothing; `head` is not looked at. -/
54theorem inflateGetHeader_check {h : Heap} {strm : ZStreamPtr} (head : GzHeaderPtr)
55    (hD : StreamDom h strm) (hN : ¬ Initialised h strm) :
56    C.run (inflateGetHeader strm head) h = .ok (Z_STREAM_ERROR, h) := by
57  show inflateGetHeader strm head h = _
58  unfold inflateGetHeader
59  simp [bind_app, pure_app, notInit_check hD hN]
60
61/-- **inflateGetHeader, no gzip.** On an initialised stream whose wrapper request has no gzip bit (`wrap &&& 2 = 0`:
62raw, or zlib only) the call returns `Z_STREAM_ERROR` and changes nothing; `head` is not looked at (a `NULL` `head` is
63fine here). -/
64theorem inflateGetHeader_nogzip {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
65    (hL : Live h r zs z st) (head : GzHeaderPtr) (hw : st.wrap &&& 2 = 0) :
66    C.run (inflateGetHeader (some r) head) h = .ok (Z_STREAM_ERROR, h) := by
67  show inflateGetHeader (some r) head h = _
68  unfold inflateGetHeader
69  isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw]
70
71/-- The state record after a successful `inflateGetHeader`: only `head` changes. -/
72def getHeaderState (head : GzHeaderPtr) (st : InflateState) : InflateState := { st with head := head }
73
74/-- **inflateGetHeader, success.** On an initialised stream that accepts gzip (`wrap &&& 2 ≠ 0`, that is a window-bits
75request of 16 to 31 or 32 to 47) and a live `gz_header` `g` the call returns `Z_OK` without a fault. The result heap
76has the state record with `head = g` (`getHeaderState`) and the header record with `done = 0`; nothing else changes (no
77allocation, no free). The stream stays initialised with the invariants intact. The header's buffers are not touched
78(they stay the caller's; `inflate` fills them later).
79Deviation from `zlib.h`: `head` must be a live record (the documentation requires a valid pointer). -/
80theorem inflateGetHeader_ok {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
81    (hG : Good h r zs z st) {g : GzHeaderRef} {gh : GzHeader} (hg : g.get h = some gh) (hw : st.wrap &&& 2 ≠ 0) :
82    ∃ h', C.run (inflateGetHeader (some r) (some g)) h = .ok (Z_OK, h') ∧
83      h' = g.put (setI h zs (getHeaderState (some g) st)) { gh with done := 0 } ∧
84      Good h' r zs z (getHeaderState (some g) st) ∧ g.get h' = some { gh with done := 0 } ∧
85      (∀ b, h'.live b ↔ h.live b) := by
86  have hL := hG.live
87  have hg1 : g.get (setI h zs (getHeaderState (some g) st)) = some gh := by
88    cases g with | tab i => simp [GzHeaderRef.get, setI] at hg ⊢; exact hg
89  have hrun : inflateGetHeader (some r) (some g) h = .ok (Z_OK, g.put (setI h zs (getHeaderState (some g) st)) { gh with done := 0 }) := by
90    unfold inflateGetHeader
91    have hro : g.isRo = false := by cases g; rfl
92    have hg' : GzHeaderRef.get (setI h zs { st with head := some g }) g = some gh := hg1
93    isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw, getHeaderState, ldGzHeader_ok hg', stGzHeader_ok hg' hro]
94  have hS : Shape h (g.put (setI h zs (getHeaderState (some g) st)) { gh with done := 0 }) :=
95    (shape_setI hL.hs _).trans (shape_putG hg1 _)
96  have hG1 : Good (setI h zs (getHeaderState (some g) st)) r zs z (getHeaderState (some g) st) := by
97    have := good_state hG (st' := getHeaderState (some g) st) rfl hL.mode
98      (hG.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl hG.inv.bits rfl rfl rfl)
99    exact this
100  refine ⟨_, hrun, rfl, ?_, ?_, fun b => hS.live b⟩
101  · obtain ⟨⟨hz, hs, zst, back, hm, za, zf⟩, inv, uniq, fresh⟩ := hG1
102    refine ⟨⟨by simpa using hz, by simpa using hs, zst, back, hm, za, zf⟩, ?_,
103      (shape_putG hg1 _).uniq uniq, (shape_putG hg1 _).fresh (by simp) fresh⟩
104    exact StInv.congr (h := setI h zs (getHeaderState (some g) st)) (by simp) (by simp) inv
105  · cases g with
106    | tab i =>
107      have hi : h.gzheaders i = some gh := hg
108      simp [GzHeaderRef.get, GzHeaderRef.put, setI, hi]
109
110/-- **inflateGetHeader, `NULL` head (a real issue of zlib).** On an initialised stream that accepts gzip, a `NULL`
111`head` is stored in the state and then dereferenced (`head->done = 0`): undefined behaviour in C, a fault here. Only the
112wrapper test comes first, so a `NULL` head on a raw or zlib-only stream is just `Z_STREAM_ERROR`
113(`inflateGetHeader_nogzip`). `zlib.h` does not allow a `NULL` head, so the main theorem excludes it. -/
114theorem inflateGetHeader_null_faults {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
115    (hL : Live h r zs z st) (hw : st.wrap &&& 2 ≠ 0) :
116    C.run (inflateGetHeader (some r) none) h = .error (.ub "null dereference (gz_header)") := by
117  show inflateGetHeader (some r) none h = _
118  unfold inflateGetHeader
119  isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw, ldGzHeader]
120
121/-! ### inflateInit_ -/
122
123theorem params15 : reset2Params 15 = some (5, 15) := by decide
124
125theorem inflateInit__eq (strm : ZStreamPtr) (version : BPtr) (sz : Int32) :
126    inflateInit_ strm version sz = inflateInit2_ strm 15 version sz := rfl
127
128/-- **inflateInit_, safety (every outcome).** `inflateInit_` is `inflateInit2_` with `windowBits = DEF_WBITS = 15`
129(zlib wrapper, 32 KiB window). For a stream record `z` whose allocator functions are `NULL` or the default ones (`zlib.h`
130lets the caller set them before the call; the model has only the defaults), a `version` that is `NULL` or points to a
131readable byte, and any `stream_size`, the call never faults and keeps `Uniq` and `Fresh`. The outcome is exactly one of:
132a version error (nothing changes); `Z_MEM_ERROR` (the allocation oracle says no; nothing leaks); `Z_OK`, with the heap
133`initOkHeap h r z 5 15` (`windowBits = 15` is always accepted, so there is no `Z_STREAM_ERROR`). -/
134theorem inflateInit__safe {h : Heap} {r : ZStreamRef} {z : ZStream} {version : BPtr} {sz : Int32}
135    (hU : Uniq h) (hF : Fresh h) (hz : r.get h = some z)
136    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
137    (hv : version = .null ∨ ∃ c, OkOn h (index8 version 0) c) :
138    ∃ v h', C.run (inflateInit_ (some r) version sz) h = .ok (v, h') ∧ Uniq h' ∧ Fresh h' ∧
139      ((v = Z_VERSION_ERROR ∧ h' = h ∧ (version = .null ∨ (∃ c, OkOn h (index8 version 0) c ∧ c ≠ 49) ∨ sz ≠ 112)) ∨
140       (v = Z_MEM_ERROR ∧ ¬ h.allocOk h.nalloc = true ∧ h' = initMemHeap h r z ∧ (∀ b, h'.live b ↔ h.live b)) ∨
141       (v = Z_OK ∧ sz = 112 ∧ h.allocOk h.nalloc = true ∧ h' = initOkHeap h r z 5 15)) := by
142  obtain ⟨v, h', hr, hU', hF', hc⟩ := inflateInit2_safe (w := 15) (sz := sz) hU hF hz hza hzf hv
143  refine ⟨v, h', hr, hU', hF', ?_⟩
144  rcases hc with c | c | c | c
145  · exact Or.inl c
146  · exact Or.inr (Or.inl c)
147  · obtain ⟨-, -, hp, -⟩ := c
148    rw [params15] at hp; cases hp
149  · obtain ⟨rfl, hsz, hok, wrap, wb, hp, he⟩ := c
150    rw [params15] at hp
151    cases hp
152    exact Or.inr (Or.inr ⟨rfl, hsz, hok, he⟩)
153
154/-- **inflateInit_, success.** If `version[0]` is `'1'`, `stream_size` is 112 and the allocation of the state succeeds,
155the call returns `Z_OK` without a fault. The new state is the block `h.nextBlk` (nothing else is allocated); the stream
156record has the default allocator functions and points to it; the stream is initialised with the invariants intact
157(`Good`); the stream owns exactly one more block (the state; the window is allocated later by `updatewindow`). The
158state is that of `windowBits = 15`: wrapper request 5 (zlib header and check), window of 2^15 bytes, allocated at the first
159decoded byte. -/
160theorem inflateInit__ok {h : Heap} {r : ZStreamRef} {z : ZStream} {version : BPtr}
161    (hU : Uniq h) (hF : Fresh h) (hz : r.get h = some z) (hok : h.allocOk h.nalloc = true)
162    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
163    (hv : version ≠ .null) (hv0 : OkOn h (index8 version 0) 49) :
164    ∃ h', C.run (inflateInit_ (some r) version 112) h = .ok (Z_OK, h') ∧ h' = initOkHeap h r z 5 15 ∧
165      Good h' r h.nextBlk (resetKeepStream (initStream2 z h.nextBlk)
166        (resetPre (reset2Pre 5 15 (initState r)))) (resetKeepState h.nextBlk (resetPre (reset2Pre 5 15 (initState r)))) ∧
167      (∀ S, h.Owns S → h'.Owns (fun b => S b ∨ b = h.nextBlk)) :=
168  inflateInit2_ok (w := 15) hU hF hz hok hza hzf hv hv0 params15
169
170end Zlib.Inflate.Proofs