trees.c.heap.gbdef.lean

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

1import ZlibF.Proof.«trees.c.heap.pq»
2import ZlibF.Proof.«trees.c.heap.gbtree»
3
4/-!
5# trees.c: `gen_bitlen` cut into its loops
6
7`gbTop` is `gen_bitlen` with each loop body named, so that every loop has a statement of its own
8(`gen_bitlen_eq : gen_bitlen = gbTop` by `rfl`: the text is the same).
9-/
10
11namespace Zlib.Trees.Proofs
12open C Zlib.Trees
13
14/-- `for (bits = 0; bits <= MAX_BITS; bits++) s->bl_count[bits] = 0;` -/
15def gbZero (s : DeflateStatePtr) : M Int32 :=
16  cfor (σ := Int32) (fun b => pure (decide (b.toInt ≤ MAX_BITS.toInt))) (fun b => iadd b 1)
17    (fun b => do setAt (← pBlCount s) b.toInt 0; pure b) 0
18
19/-- The cost added for a leaf `n` whose `Len` is `bits` and whose extra bits are `xbits`. -/
20def gbTail2 (s : DeflateStatePtr) (tree stree : CtDataPtr) (h n bits ov xbits : Int32) : M (Int32 × Int32) := do
21  let f ← getFc tree n.toInt
22  let t ← iadd bits xbits
23  md s fun d => { d with opt_len := d.opt_len + f.toUInt64 * (i2u t).toUInt64 }
24  if stree != .null then
25    let t2 ← iadd (u16i (← getDl stree n.toInt)) xbits
26    md s fun d => { d with static_len := d.static_len + f.toUInt64 * (i2u t2).toUInt64 }
27  return (h, ov)
28
29/-- The part of the first-pass body after `Len` is stored: count the leaf and add its cost. -/
30def gbTail1 (s : DeflateStatePtr) (tree stree : CtDataPtr) (extra : IPtr) (max_code base : Int32)
31    (h n bits ov : Int32) : M (Int32 × Int32) := do
32  if n.toInt > max_code.toInt then return (h, ov)
33  let bc ← pBlCount s
34  setAt bc bits.toInt ((← Ptr.index bc bits.toInt) + 1)
35  if n.toInt ≥ base.toInt then
36    let x ← Ptr.index extra (← isub n base).toInt
37    gbTail2 s tree stree h n bits ov x
38  else gbTail2 s tree stree h n bits ov 0
39
40/-- The body of the first pass, `h` and `overflow` carried. -/
41def gbBody1 (s : DeflateStatePtr) (tree stree : CtDataPtr) (extra : IPtr) (max_code base max_length : Int32) :
42    Int32 × Int32 → M (Int32 × Int32) :=
43  fun (h, overflow) => do
44    let n ← heapAt s h
45    let bits ← iadd (u16i (← getDl tree (u16i (← getDl tree n.toInt)).toInt)) 1
46    if bits.toInt > max_length.toInt then
47      let ov ← iadd overflow 1
48      setDl tree n.toInt (i2us max_length)
49      gbTail1 s tree stree extra max_code base h n max_length ov
50    else
51      setDl tree n.toInt (i2us bits)
52      gbTail1 s tree stree extra max_code base h n bits overflow
53
54def gbCond1 : Int32 × Int32 → M Bool := fun (h, _) => pure (decide (h.toInt < HEAP_SIZE.toInt))
55
56/-- The first pass. -/
57def gbPass1 (s : DeflateStatePtr) (tree stree : CtDataPtr) (extra : IPtr) (max_code base max_length : Int32)
58    (h0 : Int32) : M (Int32 × Int32) :=
59  cfor (σ := Int32 × Int32) gbCond1 (fun (h, o) => do pure (← iadd h 1, o))
60    (gbBody1 s tree stree extra max_code base max_length) (h0, 0)
61
62/-- One round of the repair: `do { ... } while (overflow > 0)` body. -/
63def gbFix (s : DeflateStatePtr) (max_length : Int32) : Int32 → M Int32 :=
64  fun overflow => do
65    let bits ← isub max_length 1
66    let bc ← pBlCount s
67    let bits ← cwhile (σ := Int32)
68      (fun b => do pure (decide ((← Ptr.index bc b.toInt) == 0), b))
69      (fun b => isub b 1) bits
70    setAt bc bits.toInt ((← Ptr.index bc bits.toInt) - 1)
71    let b1 ← iadd bits 1
72    setAt bc b1.toInt ((← Ptr.index bc b1.toInt) + 2)
73    setAt bc max_length.toInt ((← Ptr.index bc max_length.toInt) - 1)
74    isub overflow 2
75
76/-- The inner loop of the reassignment: `n` leaves of length `bits` are taken from the heap, going down. -/
77def gbInner (s : DeflateStatePtr) (tree : CtDataPtr) (max_code bits : Int32) : Int32 × Int32 → M (Int32 × Int32) :=
78  fun (n, h) => do
79    let h ← isub h 1
80    let m ← heapAt s h
81    if m.toInt > max_code.toInt then return (n, h)
82    let lm ← getDl tree m.toInt
83    if lm.toUInt32 != i2u bits then
84      let fm ← getFc tree m.toInt
85      md s fun d => { d with opt_len := d.opt_len + (i2ul bits - lm.toUInt64) * fm.toUInt64 }
86      setDl tree m.toInt (i2us bits)
87    pure (← isub n 1, h)
88
89/-- The outer loop body of the reassignment. -/
90def gbOuter (s : DeflateStatePtr) (tree : CtDataPtr) (max_code : Int32) : Int32 × Int32 → M (Int32 × Int32) :=
91  fun (bits, h) => do
92    let n0 := u16i (← Ptr.index (← pBlCount s) bits.toInt)
93    let (_, h) ← cwhile (σ := Int32 × Int32)
94      (fun (n, h) => pure (n != 0, (n, h)))
95      (gbInner s tree max_code bits) (n0, h)
96    pure (bits, h)
97
98def gbTop (s : DeflateStatePtr) (desc : TreeDescPtr) : M Unit := do
99  let dd ← ldTreeDesc desc
100  let tree := dd.dyn_tree
101  let max_code := dd.max_code
102  let sd ← ldStaticTreeDesc dd.stat_desc
103  let stree := sd.static_tree
104  let extra := sd.extra_bits
105  let base := sd.extra_base
106  let max_length := sd.max_length
107  let _ ← gbZero s
108  setDl tree (← heapAt s (← rd s).heap_max).toInt 0
109  let h0 ← iadd (← rd s).heap_max 1
110  let (h, overflow) ← gbPass1 s tree stree extra max_code base max_length h0
111  if overflow == 0 then return
112  let _ ← cdoWhile (σ := Int32) (gbFix s max_length)
113    (fun overflow => pure (decide (overflow.toInt > 0), overflow)) overflow
114  let _ ← cfor (σ := Int32 × Int32)
115    (fun (bits, _) => pure (bits != 0))
116    (fun (bits, h) => do pure (← isub bits 1, h))
117    (gbOuter s tree max_code)
118    (max_length, h)
119
120theorem gen_bitlen_eq (s : DeflateStatePtr) (desc : TreeDescPtr) : gen_bitlen s desc = gbTop s desc := rfl
121
122
123/-! ### The loop `cfor` as a `cwhile` rule -/
124
125theorem WS.cfor2 {h0 : Heap} {id : Nat} {σ : Type} {cond : σ → M Bool} {step : σ → M σ} {body : σ → M σ}
126    (Inv : σ → DeflateState → Prop) (μ : σ → DeflateState → Nat) (Q : σ → DeflateState → Prop)
127    (hstep : ∀ s d, Inv s d → WS h0 id (cond s) d (fun c d1 =>
128      (c = false ∧ Q s d1) ∨
129      (c = true ∧ WS h0 id (do step (← body s)) d1 (fun s2 d2 => Inv s2 d2 ∧ μ s2 d2 < μ s d))))
130    {s : σ} {d : DeflateState} (hI : Inv s d) (hfuel : μ s d < fuel) :
131    WS h0 id (cfor cond step body s) d (fun s' d' => Q s' d') := by
132  unfold cfor
133  refine WS.cwhile2 Inv μ Q ?_ hI hfuel
134  intro s d hI
135  have := hstep s d hI
136  refine WS.bind' this fun c d1 hq => ?_
137  rcases hq with ⟨hc, hq⟩ | ⟨hc, hq⟩
138  · subst hc; exact WS.pure' (Or.inl ⟨rfl, hq⟩)
139  · subst hc; exact WS.pure' (Or.inr ⟨rfl, hq⟩)
140
141theorem ws_gbZero {h0 : Heap} {id : Nat} (d : DeflateState) (hsz : d.bl_count.size = 16) :
142    WS h0 id (gbZero (Sp id)) d (fun _ d' => ∃ B : Array UInt16, d' = { d with bl_count := B } ∧ B.size = 16 ∧
143      ∀ i, i < 16 → B[i]! = 0) := by
144  unfold gbZero
145  let Inv : Int32 → DeflateState → Prop := fun b e => ∃ (k : Nat) (B : Array UInt16), b.toInt = k ∧ k ≤ 16 ∧
146    e = { d with bl_count := B } ∧ B.size = 16 ∧ ∀ i, i < 16 → B[i]! = if i < k then 0 else d.bl_count[i]!
147  refine WS.cfor2 (id := id) Inv (fun b _ => 16 - b.toInt.toNat) (fun b e => ∃ B : Array UInt16, e = { d with bl_count := B } ∧
148    B.size = 16 ∧ ∀ i, i < 16 → B[i]! = 0) ?_ ⟨0, d.bl_count, rfl, by omega, rfl, hsz, by intro i hi; simp⟩
149    (by simp only [fuel]; omega)
150  rintro b e ⟨k, B, hb, hk, rfl, hB, hv⟩
151  refine WS.pure' ?_
152  by_cases hlt : k ≤ 15
153  · refine Or.inr ⟨?_, ?_⟩
154    · have : MAX_BITS.toInt = 15 := rfl
155      simp only [decide_eq_true_eq]; omega
156    · have h1i : (1 : Int32).toInt = 1 := rfl
157      have hb0 : 0 ≤ b.toInt := by omega
158      have inner : WS h0 id (do setAt (← pBlCount (Sp id)) b.toInt 0; pure b) { d with bl_count := B }
159          (fun b' e => b' = b ∧ e = { d with bl_count := B.set! k 0 }) := by
160        refine WS.bind' ws_pBlCount fun p e1 ⟨hp, he1⟩ => ?_
161        subst e1; subst hp
162        refine WS.bind' (ws_setAt_blc b.toInt 0 hb0 (by show b.toInt < (B.size : Int); omega)) fun _ e3 he3 => ?_
163        subst he3
164        refine WS.pure' ⟨rfl, ?_⟩
165        have : b.toInt.toNat = k := by omega
166        simp only [this]
167      show WS h0 id (do let b' ← (do setAt (← pBlCount (Sp id)) b.toInt 0; pure b); iadd b' 1) _ _
168      refine WS.bind' inner fun b' e1 ⟨hb', he1⟩ => ?_
169      subst b'; subst he1
170      refine WS.mono (ws_iadd b (1 : Int32) (by have : (1 : Int32).toInt = 1 := rfl; omega)
171        (by have : (1 : Int32).toInt = 1 := rfl; omega)) ?_
172      intro b2 e2 ⟨hb2, he2⟩
173      subst he2
174      have h1i : (1 : Int32).toInt = 1 := rfl
175      refine ⟨⟨k + 1, B.set! k 0, by omega, by omega, rfl, by rw [size_set!]; exact hB, ?_⟩, ?_⟩
176      · intro i hi
177        rw [getD_set B k i 0 (by omega), hv i hi]
178        by_cases e : i = k
179        · subst e; simp
180        · simp only [e, ite_false]; by_cases e2 : i < k <;> simp [e2] <;> omega
181      · show 16 - b2.toInt.toNat < 16 - b.toInt.toNat
182        omega
183  · refine Or.inl ⟨?_, ?_⟩
184    · have : MAX_BITS.toInt = 15 := rfl
185      simp only [decide_eq_false_iff_not]; omega
186    · refine ⟨B, rfl, hB, fun i hi => ?_⟩
187      rw [hv i hi]; simp; omega
188end Zlib.Trees.Proofs