trees.c.runs.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.arrays»
2
3/-!
4# trees.c: the run-length model of `scan_tree` and `send_tree`
5
6The model (`RunSt`, `runStep`, `runAt`, `runBits`, `runFreq`, ...) and its invariant lemmas are those of the earlier proof
7(`Spec/trees/Emit`, `Proofs/trees/EmitSendTree`), with the bit strings written with `natBits`.
8-/
9
10namespace Zlib.Trees.Proofs.Out
11open C Zlib.Trees
12
13/-- Bits of `send_code(s, c, tree)`: `Len` bits of `Code`, least significant first. -/
14def codeBits (t : Nat → UInt16 × UInt16) (n : Nat) : List Bool :=
15  natBits (t n).1.toNat (t n).2.toNat
16
17/-- Run-length state of `scan_tree` / `send_tree`: `prevlen`, `nextlen`, `count`, `max_count`, `min_count`. -/
18structure RunSt where
19  prev : Int
20  next : Nat
21  cnt : Nat
22  mx : Nat
23  mn : Nat
24
25/-- Initial state for the lengths `L n = tree[n].Len`. -/
26def runInit (L : Nat → Nat) : RunSt :=
27  if L 0 = 0 then ⟨-1, L 0, 0, 138, 3⟩ else ⟨-1, L 0, 0, 7, 4⟩
28
29/-- One iteration at index `n`: the new state, and the finished run `(curlen, prevlen, count, min_count)` if the run
30ends here. -/
31def runStep (L : Nat → Nat) (n : Nat) (s : RunSt) : RunSt × Option (Nat × Int × Nat × Nat) :=
32  let cur := s.next
33  let nx := L (n + 1)
34  let cnt := s.cnt + 1
35  if cnt < s.mx ∧ cur = nx then (⟨s.prev, nx, cnt, s.mx, s.mn⟩, none)
36  else
37    ((if nx = 0 then ⟨cur, nx, 0, 138, 3⟩ else if cur = nx then ⟨cur, nx, 0, 6, 3⟩
38      else ⟨cur, nx, 0, 7, 4⟩), some (cur, s.prev, cnt, s.mn))
39
40/-- State before iteration `n`. -/
41def runAt (L : Nat → Nat) : Nat → RunSt
42  | 0 => runInit L
43  | n + 1 => (runStep L n (runAt L n)).1
44
45/-- The bits `send_tree` emits for one finished run, with the bit-length code `blt`
46(`REP_3_6 = 16`, `REPZ_3_10 = 17`, `REPZ_11_138 = 18`). -/
47def runBits (blt : Nat → UInt16 × UInt16) : Option (Nat × Int × Nat × Nat) → List Bool
48  | none => []
49  | some (cur, prev, cnt, mn) =>
50    if cnt < mn then (List.replicate cnt (codeBits blt cur)).flatten
51    else if cur ≠ 0 then
52      (if (cur : Int) ≠ prev then codeBits blt cur ++ codeBits blt 16 ++ natBits (cnt - 1 - 3) 2
53       else codeBits blt 16 ++ natBits (cnt - 3) 2)
54    else if cnt ≤ 10 then codeBits blt 17 ++ natBits (cnt - 3) 3
55    else codeBits blt 18 ++ natBits (cnt - 11) 7
56
57/-- Bits emitted by the first `n` iterations of `send_tree`. -/
58def treeBitsUpTo (blt : Nat → UInt16 × UInt16) (L : Nat → Nat) : Nat → List Bool
59  | 0 => []
60  | n + 1 => treeBitsUpTo blt L n ++ runBits blt (runStep L n (runAt L n)).2
61
62/-- Everything `send_tree(s, tree, max_code)` emits. -/
63def sendTreeBits (blt : Nat → UInt16 × UInt16) (L : Nat → Nat) (maxc : Nat) : List Bool :=
64  treeBitsUpTo blt L (maxc + 1)
65
66/-- How much one finished run adds to the frequency of bit-length symbol `k` (`scan_tree`). -/
67def runFreq : Option (Nat × Int × Nat × Nat) → Nat → Nat
68  | none, _ => 0
69  | some (cur, prev, cnt, mn), k =>
70    if cnt < mn then (if k = cur then cnt else 0)
71    else if cur ≠ 0 then (if (cur : Int) ≠ prev ∧ k = cur then 1 else 0) + (if k = 16 then 1 else 0)
72    else if cnt ≤ 10 then (if k = 17 then 1 else 0)
73    else (if k = 18 then 1 else 0)
74
75/-- Frequency added to bit-length symbol `k` by the first `n` iterations of `scan_tree`. -/
76def scanFreqUpTo (L : Nat → Nat) : Nat → Nat → Nat
77  | 0, _ => 0
78  | n + 1, k => scanFreqUpTo L n k + runFreq (runStep L n (runAt L n)).2 k
79
80/-- The lengths `scan_tree` sees: `L` with the guard `0xffff` at `max_code + 1`. -/
81def guarded (L : Nat → Nat) (maxc : Nat) (i : Nat) : Nat := if i = maxc + 1 then 0xffff else L i
82
83
84/-- Invariant of the run-length state (what makes every `send_bits` value fit). -/
85def RunInv (s : RunSt) : Prop :=
86  s.cnt < s.mx ∧ (s.next = 0 → s.mx = 138 ∧ s.mn = 3) ∧
87  (s.next ≠ 0 → (s.mx = 6 ∧ s.mn = 3 ∧ (s.next : Int) = s.prev) ∨
88    (s.mx = 7 ∧ s.mn = 4 ∧ (s.next : Int) ≠ s.prev)) ∧
89  -1 ≤ s.prev ∧ s.prev < 2 ^ 16
90
91theorem runAt_next (L : Nat → Nat) (n : Nat) : (runAt L n).next = L n := by
92  cases n with
93  | zero => simp only [runAt, runInit]; split <;> rfl
94  | succ n =>
95    simp only [runAt, runStep]
96    split
97    · rfl
98    · split
99      · rfl
100      · split <;> rfl
101
102theorem runInv_runAt (L : Nat → Nat) (hL : ∀ n, L n < 2 ^ 16) (n : Nat) : RunInv (runAt L n) := by
103  induction n with
104  | zero =>
105    simp only [runAt, runInit]
106    split
107    · rename_i h0; refine ⟨by simp, fun _ => ⟨rfl, rfl⟩, fun h => absurd h0 h, by simp, by simp⟩
108    · rename_i h0
109      refine ⟨by simp, fun h => absurd h h0, fun _ => Or.inr ⟨rfl, rfl, by simp <;> omega⟩, by simp, by simp⟩
110  | succ n ih =>
111    obtain ⟨i1, i2, i3, i4, i5⟩ := ih
112    have hnext := runAt_next L n
113    simp only [runAt, runStep]
114    split
115    · rename_i hc
116      obtain ⟨hc1, hc2⟩ := hc
117      refine ⟨hc1, ?_, ?_, i4, i5⟩
118      · intro h0; apply i2; rw [← hc2] at h0; exact h0
119      · intro h0; have := i3 (by rw [hc2]; exact h0); simp only at this ⊢; rw [← hc2]; exact this
120    · rename_i hc
121      have hcur : (runAt L n).next < 2 ^ 16 := by rw [hnext]; exact hL n
122      split
123      · rename_i hnx
124        exact ⟨by simp, fun _ => ⟨rfl, rfl⟩, fun h => absurd hnx h, by simp, by simp <;> omega⟩
125      · split
126        · rename_i hnx he
127          exact ⟨by simp, fun h => absurd h hnx, fun _ => Or.inl ⟨rfl, rfl, by simp [he]⟩, by simp, by simp <;> omega⟩
128        · rename_i hnx he
129          exact ⟨by simp, fun h => absurd h hnx, fun _ => Or.inr ⟨rfl, rfl, by simp <;> omega⟩, by simp, by simp <;> omega⟩
130
131theorem treeBitsUpTo_mono (blt : Nat → UInt16 × UInt16) (L : Nat → Nat) {i j : Nat} (h : i ≤ j) :
132    (treeBitsUpTo blt L i).length ≤ (treeBitsUpTo blt L j).length := by
133  induction j with
134  | zero => have : i = 0 := by omega
135            subst this; exact Nat.le_refl _
136  | succ j ih =>
137    by_cases e : i = j + 1
138    · subst e; exact Nat.le_refl _
139    · have := ih (by omega); simp only [treeBitsUpTo, List.length_append]; omega
140
141/-- `tree[i].Freq += v` (modulo 2^16). -/
142def addFc (a : Array CtData) (i : Nat) (v : UInt16) : Array CtData := a.set! i { (a[i]!) with fc := (a[i]!).fc + v }
143
144@[simp] theorem addFc_size (a : Array CtData) (i : Nat) (v : UInt16) : (addFc a i v).size = a.size := by
145  simp [addFc]
146
147theorem addFc_dl (a : Array CtData) (i : Nat) (v : UInt16) (k : Nat) : ((addFc a i v)[k]!).dl = (a[k]!).dl := by
148  unfold addFc; rw [getElem!_set!]; split <;> simp_all
149
150theorem addFc_fc (a : Array CtData) (i : Nat) (v : UInt16) (hi : i < a.size) (k : Nat) :
151    ((addFc a i v)[k]!).fc = if k = i then (a[k]!).fc + v else (a[k]!).fc := by
152  unfold addFc; rw [getElem!_set!]
153  by_cases h : i = k
154  · subst h; simp [hi]
155  · simp [h, Ne.symm h]
156
157
158end Zlib.Trees.Proofs.Out