deflate.c.init.success.lean

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

1import ZlibF.Proof.«deflate.c.init.construct»
2import ZlibF.Proof.«deflate.c.init.storage»
3
4/-! # deflate.c: successful default buffer construction -/
5
6namespace Zlib.Deflate.Proofs.DefaultInit
7open C Zlib.Deflate Zlib.Deflate.Spec
8open Zlib.Trees.Proofs.Out (TreesBase TreesStatic)
9set_option autoImplicit false
10
11def readyHeap (h : Heap) (ds : Nat) (r : ZStreamRef) (level : Int32) : Heap :=
12  setD (successfulBuffers h) ds
13    (readyState r level h.nextBlk (h.nextBlk + 1) (h.nextBlk + 2) (h.nextBlk + 3))
14
15theorem buffer_state_success (h : Heap) (r : ZStreamRef)
16    (ha : ∀ j, j < 4 → h.allocOk (h.nalloc + j) = true) :
17    bufferState h (baseState r) =
18      allocatedState r h.nextBlk (h.nextBlk + 1) (h.nextBlk + 2) (h.nextBlk + 3) := by
19  have ps := (buffers_success h ha).2
20  have w := congrArg (fun x : BPtr × WPtr × WPtr × BPtr => x.1) ps
21  have p := congrArg (fun x : BPtr × WPtr × WPtr × BPtr => x.2.1) ps
22  have q := congrArg (fun x : BPtr × WPtr × WPtr × BPtr => x.2.2.1) ps
23  have b := congrArg (fun x : BPtr × WPtr × WPtr × BPtr => x.2.2.2) ps
24  dsimp only [bufferPointers] at w p q b
25  simp only [bufferState, allocatedState, w, p, q, b]
26
27/-- The real pointer addition and final stores reach the constructed
28default state before the actual reset call. -/
29theorem finish_to_reset (h : Heap) (ds : Nat) (r : ZStreamRef) (level : Int32)
30    (ha : ∀ j, j < 4 → h.allocOk (h.nalloc + j) = true) :
31    finish (some r) (some (.tab ds)) level (bufferPointers h)
32        (setD (buffersHeap h) ds (bufferState h (baseState r))) =
33      deflateReset (some r) (readyHeap h ds r level) := by
34  have he := (buffers_success h ha).1
35  have hp := (buffers_success h ha).2
36  rw [he, buffer_state_success h r ha, hp]
37  let d := allocatedState r h.nextBlk (h.nextBlk + 1) (h.nextBlk + 2) (h.nextBlk + 3)
38  let g := setD (successfulBuffers h) ds d
39  have hb : g.bytes (h.nextBlk + 3) = some (byteGarbage h 3) := by
40    simp [g, successfulBuffers]
41  have padd_run : padd (.ref (.blk (h.nextBlk + 3)) 0 : BPtr) 16384 g =
42      .ok (.ref (.blk (h.nextBlk + 3)) 16384, g) := by
43    have hget : Space.get g (BRef.blk (h.nextBlk + 3)) = some (byteGarbage h 3) := hb
44    have add := Ptr.add_nat_ok (off := 0) (n := 16384) hget (by simp [byteGarbage])
45    simpa only [OkOn, padd, Nat.zero_add] using add
46  unfold finish
47  simp only [bind_app, Bool.or_false, Bool.false_or]
48  change (do
49    let sym_buf ← padd (.ref (.blk (h.nextBlk + 3)) 0 : BPtr) 16384
50    wr (some (.tab ds)) (fun d => { d with sym_buf, sym_end := 49149 })
51    wr (some (.tab ds)) (fun d => { d with level, strategy := 0, «method» := 8 })
52    deflateReset (some r)) g = _
53  rw [bind_app, padd_run]
54  simp only [bind_app, wrD_eq, g, setD_dstates_same, setD_setD]
55  rfl
56
57/-- All buffer geometry and tree storage follow from the actual successful
58requests. pending_out and window_size are deliberately left for reset. -/
59theorem ready_storage {h : Heap} {r : ZStreamRef} {z : ZStream} {ds : Nat}
60    (level : Int32) (hf : Fresh h) (hu : Uniq h) (hz : r.get h = some z)
61    (hs : h.dstates ds = some (baseState r)) (hds : ds < h.nextBlk)
62    (halloc : DefAlloc z) (hzs : z.state = some (.deflate ds))
63    (hstatic : TreesStatic h.static)
64    (ha : ∀ j, j < 4 → h.allocOk (h.nalloc + j) = true) :
65    let d := readyState r level h.nextBlk (h.nextBlk + 1) (h.nextBlk + 2) (h.nextBlk + 3)
66    let g := readyHeap h ds r level
67    DLive g r ds z d ∧ TreesBase g ds d (h.nextBlk + 3) ((g.bytes (h.nextBlk + 3)).getD #[]) ∧
68      DBlocks g { d with pending_out := d.pending_buf }
69        h.nextBlk (h.nextBlk + 1) (h.nextBlk + 2) (h.nextBlk + 3) ∧ Uniq g ∧ Fresh g := by
70  let d := readyState r level h.nextBlk (h.nextBlk + 1) (h.nextBlk + 2) (h.nextBlk + 3)
71  let g := readyHeap h ds r level
72  have slots := (buffers_success h ha).1
73  have hsf : (successfulBuffers h).dstates ds = some (baseState r) := by simpa [successfulBuffers] using hs
74  have hsh := shape_setD hsf d
75  have huB : Uniq (successfulBuffers h) := by rw [← slots]; exact buffers_uniq hu hf
76  have hfB : Fresh (successfulBuffers h) := by rw [← slots]; exact buffers_fresh hf
77  have hgZ : r.get g = some z := by
78    change r.get (setD (successfulBuffers h) ds d) = some z
79    rw [ZStreamRef.get_setD, ← slots, get_buffersHeap]
80    exact hz
81  have wf : d.WellFormed := by
82    simp [d, readyState, allocatedState, baseState, DeflateState.WellFormed,
83      DeflateState.zeroed, DeflateState.garbage]
84  have hb : DBlocks g { d with pending_out := d.pending_buf }
85      h.nextBlk (h.nextBlk + 1) (h.nextBlk + 2) (h.nextBlk + 3) := by
86    refine ⟨rfl, rfl, rfl, rfl,
87      ⟨byteGarbage h 0, ?_, ?_⟩, ?_, ⟨wordGarbage h 1, ?_, ?_⟩,
88      ⟨wordGarbage h 2, ?_, ?_⟩, ⟨byteGarbage h 3, ?_, ?_⟩,
89      ?_, ?_, by omega, by omega, 0, rfl, ?_⟩
90    all_goals simp [g, readyHeap, successfulBuffers, d, readyState, allocatedState, baseState,
91      byteGarbage, wordGarbage, DeflateState.zeroed, DeflateState.garbage, Junk.of]
92  refine ⟨⟨hgZ, by simp [g, readyHeap], hzs, rfl, Or.inl rfl,
93    by rw [halloc.1]; decide, by rw [halloc.2]; decide⟩,
94    ?_, hb, hsh.uniq huB, hsh.fresh (by rfl) hfB⟩
95  refine ⟨by simp [g, readyHeap], wf, ?_, rfl, ?_, hb.bro, ?_, ?_, rfl,
96    by change 128 ≤ (16384 : UInt32).toNat; decide +kernel,
97    by change (16384 : UInt32).toNat ≤ 32768; decide +kernel,
98    by change (49149 : UInt32).toNat = 3 * ((16384 : UInt32).toNat - 1); decide +kernel, ?_⟩
99  · simpa [g, readyHeap, successfulBuffers] using hstatic
100  · simp [g, readyHeap, successfulBuffers]
101  · simp [g, readyHeap, successfulBuffers, d, readyState, allocatedState,
102      byteGarbage]
103  · simp [g, readyHeap, successfulBuffers, d, readyState, allocatedState, byteGarbage]
104  · simp [d, readyState, allocatedState, baseState, DeflateState.zeroed, DeflateState.garbage, Junk.of]
105
106end Zlib.Deflate.Proofs.DefaultInit