infback.c.end.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«infback.c.init»
2
3/-!
4# infback.c: `inflateBackEnd`
5
6`inflateBackEnd` frees the state record and clears the stream's state pointer. It does not run `inflateStateCheck`, and
7it never touches the window, which belongs to the caller.
8-/
9
10namespace Zlib.Infback.Spec
11open C Zlib.Inflate Zlib.Inflate.Spec
12
13/-- The heap after a successful `inflateBackEnd`: the state record is freed and the stream's state pointer is `NULL`. -/
14def backEndHeap (h : Heap) (r : ZStreamRef) (z : ZStream) (zs : Nat) : Heap :=
15  r.put (freeIst h zs) { z with state := none }
16
17end Zlib.Infback.Spec
18
19namespace Zlib.Infback.Proofs
20open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec
21
22/-- A null stream: `Z_STREAM_ERROR`, nothing changes. -/
23theorem inflateBackEnd_nullstream (h : Heap) : inflateBackEnd none h = .ok (Z_STREAM_ERROR, h) := by
24  simp [inflateBackEnd]
25
26/-- No state, or no `zfree`: `Z_STREAM_ERROR`, nothing changes. -/
27theorem inflateBackEnd_refused {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z)
28    (hno : z.state = none ∨ z.zfree = .null) :
29    inflateBackEnd (some r) h = .ok (Z_STREAM_ERROR, h) := by
30  rcases hno with e | e <;> isimp [inflateBackEnd, hz, e]
31
32/-- **inflateBackEnd, success.** On a stream set up by `inflateBackInit_` it returns `Z_OK` without a fault, frees the
33state record, sets the stream's state pointer to `NULL`, and frees nothing else (the window is the caller's). The
34blocks the stream owned are the old ones except the state. -/
35theorem inflateBackEnd_ok {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
36    (hG : BackGood h r zs z st) :
37    ∃ h', C.run (inflateBackEnd (some r)) h = .ok (Z_OK, h') ∧ h' = backEndHeap h r z zs ∧
38      Uniq h' ∧ Fresh h' ∧ r.get h' = some { z with state := none } ∧
39      (∀ S, h.Owns S → h'.Owns (fun b => S b ∧ b ≠ zs)) := by
40  have hz := hG.hz
41  have hs := hG.hs
42  have hrun : inflateBackEnd (some r) h = .ok (Z_OK, backEndHeap h r z zs) := by
43    unfold inflateBackEnd
44    have hz0 : z.zfree ≠ .null := by rw [hG.zfree]; intro c; cases c
45    have hs0 : z.state ≠ none := by rw [hG.zst]; intro c; cases c
46    isimp [hz, hs0, hz0, hG.zst, hG.zfree, zfrees_run hz hG.zfree hs, backEndHeap]
47  have hU1 : Uniq (freeIst h zs) := uniq_freeIst hG.uniq zs
48  have hz1 : r.get (freeIst h zs) = some z := by simpa using hz
49  refine ⟨_, by rw [C.run]; exact hrun, rfl, ?_, ?_, ?_, ?_⟩
50  · exact (shape_put hz1 _).uniq hU1
51  · exact (shape_put hz1 _).fresh (by simp [backEndHeap]) (fresh_freeIst hG.fresh zs)
52  · simp [backEndHeap, hz]
53  · intro S hO
54    have hO1 := owns_freeIst hG.uniq hs hO
55    exact (shape_put hz1 _).owns hO1
56
57end Zlib.Infback.Proofs