inflate.c.reset.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.base»
2
3/-!
4# inflate.c: `inflateReset`, `inflateReset2`, `inflatePrime`, `inflateValidate`, `inflateUndermine`, `inflateMark`,
5`inflateCodesUsed`, `inflateSyncPoint`, `inflateGetHeader`
6
7Safety and specification of the stream functions that change the state record (and, for the two reset functions,
8free the window).
9-/
10
11namespace Zlib.Inflate.Spec
12open C
13
14/-- The state record after `inflateReset` has made its changes and before `inflateResetKeep` runs: a window of another
15size than the requested one is dropped, the requested window size and wrapper become current, the window is empty. -/
16def resetPre (st : InflateState) : InflateState :=
17  { (if st.wbits != st.reqbits then { st with window := .null, wbits := st.reqbits } else st) with
18    wrap := st.reqwrap, wsize := 0, whave := 0, wnext := 0 }
19
20/-- The heap after the window of `st` was freed, if `inflateReset` frees it. -/
21def resetHeap (h : Heap) (st : InflateState) : Heap := if st.wbits != st.reqbits then freeWin h st.window else h
22
23end Zlib.Inflate.Spec
24
25namespace Zlib.Inflate.Proofs
26open C Zlib.Inflate Zlib.Inflate.Spec
27
28theorem windowBlock {h : Heap} {st : InflateState} (hW : WinInv h st) :
29    st.window = .null ∨ ∃ b a, st.window = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false := by
30  rcases hW.block with hn | ⟨w, a, hw, ha, hro, -⟩
31  · exact Or.inl hn
32  · exact Or.inr ⟨w, a, hw, ha, hro⟩
33
34theorem Good.defz {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
35    (hG : Good h r zs z st) : z.zalloc ≠ .null := hG.live.zalloc
36
37theorem live_mid {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
38    (hL : Live h r zs z st) (h0 : Heap) (hz : r.get h0 = some z) (hs : h0.istates zs = some st) : Live h0 r zs z st :=
39  ⟨hz, hs, hL.zst, hL.back, hL.mode, hL.zalloc, hL.zfree⟩
40
41/-- The window pointer is `NULL` or a writable byte block that exists. -/
42def WindowOk (h : Heap) (p : BPtr) : Prop := p = .null ∨ ∃ b a, p = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false
43
44theorem inflateReset_run {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
45    (hL : Live h r zs z st) (hf : z.zfree = .fn "zcfree") (hwo : st.wbits = st.reqbits ∨ WindowOk h st.window) :
46    inflateReset (some r) h = .ok (Z_OK, setI (r.put (resetHeap h st) (resetKeepStream z (resetPre st))) zs
47      (resetKeepState zs (resetPre st))) := by
48  have hz := hL.hz
49  have hs := hL.hs
50  have hsn : (h.istates zs).isSome := by simp [hs]
51  unfold inflateReset
52  by_cases hne : st.wbits = st.reqbits
53  · isimp [stateCheck_live hL, hL.zst, hz, hs, hne]
54    rw [resetKeep_run]
55    rotate_left
56    · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
57    · simp [resetHeap, resetPre, hne, resetKeepState, resetKeepStream]
58  · by_cases hw : st.window = .null
59    · isimp [stateCheck_live hL, hL.zst, hz, hs, hne, hw]
60      rw [resetKeep_run]
61      rotate_left
62      · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
63      · simp [resetHeap, resetPre, hne, hw, resetKeepState, resetKeepStream, freeWin_null]
64    · obtain ⟨b, a, hb, hba, hro⟩ : ∃ b a, st.window = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false := by
65        rcases hwo with hh | hn | hb
66        · exact absurd hh hne
67        · exact absurd hn hw
68        · exact hb
69      isimp [stateCheck_live hL, hL.zst, hz, hs, hne, hw, zfreeB_run hz hf (Or.inr ⟨b, a, hb, hba, hro⟩)]
70      rw [resetKeep_run]
71      rotate_left
72      · exact ⟨by simp [hz], by first | exact setI_istates_same _ _ _ | (rw [freeWin_istates]; exact setI_istates_same _ _ _), hL.zst, by simp [hL.back], by simpa using hL.mode, hL.zalloc, hL.zfree⟩
73      · simp [resetHeap, resetPre, hne, hw, resetKeepState, resetKeepStream, freeWin_null]
74
75
76/-- The invariants of a stream after both records are replaced, over any heap that has the two records. -/
77theorem good_set {h0 : Heap} {r : ZStreamRef} {zs : Nat} {z0 z' : ZStream} {s0 st' : InflateState}
78    (hz0 : r.get h0 = some z0) (hs0 : h0.istates zs = some s0) (hU : Uniq h0) (hF : Fresh h0)
79    (zst : z'.state = some (.inflate zs)) (za : z'.zalloc ≠ .null) (zf : z'.zfree ≠ .null)
80    (back : st'.strm = some r) (hm : HEAD ≤ st'.mode ∧ st'.mode ≤ SYNC) (hI : StInv h0 zs st') :
81    Good (setI (r.put h0 z') zs st') r zs z' st' := by
82  have hS : Shape h0 (setI (r.put h0 z') zs st') :=
83    (shape_put hz0 z').trans (shape_setI (by simpa using hs0) st')
84  refine ⟨⟨?_, by simp, zst, back, hm, za, zf⟩, StInv.congr (h := h0) (h' := setI (r.put h0 z') zs st') (by simp) (by simp) hI,
85    hS.uniq hU, hS.fresh (by simp) hF⟩
86  simp [hz0]
87
88theorem wf_resetPre {st : InflateState} (hw : st.WellFormed) : (resetPre st).WellFormed := by
89  unfold InflateState.WellFormed at *
90  unfold resetPre
91  split <;> simpa using hw
92
93theorem wf_resetKeepState {zs : Nat} {st : InflateState} (hw : st.WellFormed) : (resetKeepState zs st).WellFormed := by
94  unfold InflateState.WellFormed at *
95  simpa [resetKeepState] using hw
96
97theorem reqbits_resetPre (st : InflateState) : (resetPre st).reqbits = st.reqbits := by
98  unfold resetPre; split <;> rfl
99
100theorem ptr_resetPre {zs : Nat} {st : InflateState} (hp : PtrInv zs st) : PtrInv zs (resetPre st) := by
101  unfold PtrInv at *; unfold resetPre; split <;> simpa using hp
102
103theorem bits_resetPre {st : InflateState} (hb : st.bits.toNat ≤ 39) : (resetPre st).bits.toNat ≤ 39 := by
104  unfold resetPre; split <;> simpa using hb
105
106theorem winInv_reset {h : Heap} {st : InflateState} (hW : WinInv h st) (hq : st.reqbits.toNat ≤ 15) :
107    WinInv (resetHeap h st) (resetPre st) := by
108  by_cases hne : st.wbits = st.reqbits
109  · have e : resetHeap h st = h := by simp [resetHeap, hne]
110    rw [e]
111    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
112    · simpa [resetPre, hne] using hW.wbits
113    · simpa [resetPre, hne] using hW.block
114    · intro _; simp [resetPre, hne]
115    · simp [resetPre, hne]
116    · simp [resetPre, hne]
117    · simp [resetPre, hne]
118    · intro hh; simp [resetPre, hne] at hh
119  · refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
120    · simpa [resetPre, hne] using hq
121    · left; simp [resetPre, hne]
122    · intro _; simp [resetPre, hne]
123    · simp [resetPre, hne]
124    · simp [resetPre, hne]
125    · simp [resetPre, hne]
126    · intro hh; simp [resetPre, hne] at hh
127
128theorem resetHeap_owns {h : Heap} {st : InflateState} (hU : Uniq h) (hW : WinInv h st) {S : Nat → Prop}
129    (hO : h.Owns S) : (resetHeap h st).Owns (fun b => S b ∧ ¬ (st.wbits ≠ st.reqbits ∧ WinBlk st b)) := by
130  by_cases hne : st.wbits = st.reqbits
131  · have e : resetHeap h st = h := by simp [resetHeap, hne]
132    rw [e]
133    intro b; rw [hO b]; simp [hne]
134  · have e : resetHeap h st = freeWin h st.window := by simp [resetHeap, hne]
135    rw [e]
136    rcases windowBlock hW with hn | ⟨w, a, hw, hb, hro⟩
137    · rw [hn, freeWin_null]
138      intro b; rw [hO b]; simp [WinBlk, hn]
139    · rw [hw]
140      have := owns_freeWin hU hb hO
141      intro b
142      rw [this b]
143      constructor
144      · rintro ⟨hS, hbw⟩
145        refine ⟨hS, ?_⟩
146        rintro ⟨-, hwb⟩
147        apply hbw
148        unfold WinBlk at hwb
149        rw [hw] at hwb
150        exact (BRef.blk.inj (Ptr.ref.inj hwb).1).symm
151      · rintro ⟨hS, hh⟩
152        refine ⟨hS, fun hbw => hh ⟨hne, ?_⟩⟩
153        unfold WinBlk
154        rw [hw, hbw]
155
156/-- **inflateReset, safety.** On an initialised stream with the default `zfree` the call returns `Z_OK` without a
157fault. If the current window size is not the requested one, the window block is freed (the only free; nothing is
158allocated). The records become `resetKeepStream`/`resetKeepState` of `resetPre st`; the stream is initialised again
159and the invariants hold. -/
160theorem inflateReset_safe {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
161    (hG : Good h r zs z st) (hf : z.zfree = .fn "zcfree") :
162    ∃ h', C.run (inflateReset (some r)) h = .ok (Z_OK, h') ∧
163      h' = setI (r.put (resetHeap h st) (resetKeepStream z (resetPre st))) zs (resetKeepState zs (resetPre st)) ∧
164      Good h' r zs (resetKeepStream z (resetPre st)) (resetKeepState zs (resetPre st)) ∧
165      (∀ S, h.Owns S → h'.Owns (fun b => S b ∧ ¬ (st.wbits ≠ st.reqbits ∧ WinBlk st b))) := by
166  have hL := hG.live
167  have hU : Uniq (resetHeap h st) := by
168    unfold resetHeap; split
169    · exact uniq_freeWin hG.uniq _
170    · exact hG.uniq
171  have hF : Fresh (resetHeap h st) := by
172    unfold resetHeap; split
173    · exact fresh_freeWin hG.fresh _
174    · exact hG.fresh
175  have hz0 : r.get (resetHeap h st) = some z := by unfold resetHeap; split <;> simp [hL.hz]
176  have hs0 : (resetHeap h st).istates zs = some st := by unfold resetHeap; split <;> simp [hL.hs]
177  have hI : StInv (resetHeap h st) zs (resetKeepState zs (resetPre st)) := by
178    have hw := winInv_reset hG.inv.win hG.inv.reqbits
179    refine ⟨wf_resetKeepState (wf_resetPre hG.inv.wf), ?_, by simpa [resetKeepState, reqbits_resetPre] using hG.inv.reqbits, by simp [resetKeepState], ?_⟩
180    · exact ⟨hw.wbits, hw.block, hw.nullws, hw.ws, hw.hv, hw.wn, hw.eq⟩
181    · exact (StInv.resetKeep (st := resetPre st) ⟨wf_resetPre hG.inv.wf, hw, by simpa [reqbits_resetPre] using hG.inv.reqbits, bits_resetPre hG.inv.bits, ptr_resetPre hG.inv.ptr⟩).ptr
182  refine ⟨_, inflateReset_run hG.live hf (Or.inr (windowBlock hG.inv.win)), rfl, ?_, ?_⟩
183  · refine good_set hz0 hs0 hU hF (by simp [resetKeepStream, hL.zst]) (by simpa [resetKeepStream] using hL.zalloc)
184      (by simpa [resetKeepStream] using hL.zfree) (by simp [resetKeepState, resetPre]; split <;> exact hL.back)
185      (by simpa [resetKeepState] using mode_head) hI
186  · intro S hO
187    have hO' := resetHeap_owns hG.uniq hG.inv.win hO
188    exact ((shape_put hz0 _).trans (shape_setI (by simpa using hs0) _)).owns hO'
189
190end Zlib.Inflate.Proofs