trees.c.emit-state.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»
2import ZlibF.Proof.«trees.c.emit»
3import ZlibF.Proof.«trees.c.runs»
4import ZlibF.Proof.«trees.c.monad»
5
6/-! # trees.c: exact heap/output states between actual bit-writing calls -/
7
8namespace Zlib.Trees.Proofs.Out
9open C Zlib.Trees
10
11/-- Direct state facts for a prefix of actual bit-writing calls. There are
12no called-function contracts in this representation. -/
13structure EmitState (id b : Nat) (h0 : Heap) (d0 : DeflateState) (buf0 : Array UInt8)
14    (w : List Bool) (h : Heap) (d : DeflateState) (buf : Array UInt8) : Prop where
15  heap : h = setD (setB h0 b buf) id d
16  inv : TreesInvAt h id d b buf
17  bits : outBits buf d = outBits buf0 d0 ++ w
18  size : buf.size = buf0.size
19  frame : ∀ i, (i < d0.pending.toNat ∨ d.pending.toNat ≤ i) → buf.getD i 0 = buf0.getD i 0
20  lower : d0.pending.toNat ≤ d.pending.toNat
21  fields : BitsDiff d0 d
22
23/-- Start a trace at the actual caller heap. -/
24theorem EmitState.start {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
25    (hI : TreesInvAt h id d b buf) : EmitState id b h d buf [] h d buf := by
26  refine ⟨?_, hI, by simp, rfl, fun _ _ => rfl, Nat.le_refl _, BitsDiff.refl d⟩
27  rw [setB_self hI.base.bytes, setD_self hI.base.dstate]
28
29/-- Compose a proved actual emission with the already recorded prefix. -/
30theorem EmitState.step {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
31    {w v : List Bool} {m : M Unit} {k : Nat} (ht : EmitState id b h0 d0 buf0 w h d buf)
32    (he : Emit id b m h d buf v k) :
33    ∃ h' d' buf', m h = .ok ((), h') ∧ EmitState id b h0 d0 buf0 (w ++ v) h' d' buf' := by
34  obtain ⟨buf', d', hr, hi, ho, hs, hf, hlo, hhi, hd⟩ := he
35  refine ⟨_, d', buf', hr, ?_, hi, ?_, hs.trans ht.size, ?_, by have := ht.lower; omega, ht.fields.trans hd⟩
36  · rw [ht.heap, setB_setD, setB_setB, setD_setD]
37  · rw [ho, ht.bits, List.append_assoc]
38  · intro i hidx
39    rw [hf i (by have := ht.lower; omega), ht.frame i (by omega)]
40
41/-- The source record arrays remain exactly those of the initial heap. -/
42theorem EmitState.tree_arrays {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
43    {w : List Bool} (ht : EmitState id b h0 d0 buf0 w h d buf) :
44    d.dyn_ltree = d0.dyn_ltree ∧ d.dyn_dtree = d0.dyn_dtree ∧ d.bl_tree = d0.bl_tree := by
45  obtain ⟨p, a, v, u, he⟩ := ht.fields
46  rw [he]
47  exact ⟨rfl, rfl, rfl⟩
48
49/-- Transport a total bit-room bound to an actual intermediate state. -/
50theorem EmitState.room {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
51    {w : List Bool} (ht : EmitState id b h0 d0 buf0 w h d buf) (n total : Nat)
52    (hp : w.length + n ≤ total)
53    (hr : 8 * d0.pending.toNat + d0.bi_valid.toInt.toNat + total ≤ 8 * buf0.size) :
54    8 * d.pending.toNat + d.bi_valid.toInt.toNat + n ≤ 8 * buf.size := by
55  have hc := congrArg List.length ht.bits
56  simp only [outBits_length, List.length_append] at hc
57  rw [ht.size]
58  omega
59
60/-- Turn a complete actual run and its trace into the existing emission
61relation. The byte bound follows from exact output length. -/
62theorem EmitState.emit {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
63    {w : List Bool} {m : M Unit} (ht : EmitState id b h0 d0 buf0 w h d buf)
64    (hr : m h0 = .ok ((), h)) :
65    Emit id b m h0 d0 buf0 w (d0.bi_valid.toInt.toNat + w.length) := by
66  have hc := congrArg List.length ht.bits
67  simp only [outBits_length, List.length_append] at hc
68  refine ⟨buf, d, ?_, ?_, ht.bits, ht.size, ht.frame, ht.lower, by omega, ht.fields⟩
69  · rw [← ht.heap]
70    exact hr
71  · rw [← ht.heap]
72    exact ht.inv
73
74/-- A terminating actual computation and its returned value/heap facts. -/
75def EWP {α : Type} (m : M α) (h : Heap) (Q : α → Heap → Prop) : Prop :=
76  ∃ a h', m h = .ok (a, h') ∧ Q a h'
77
78theorem EWP.pure {α : Type} {h : Heap} {a : α} {Q : α → Heap → Prop}
79    (hq : Q a h) : EWP (pure a) h Q := ⟨a, h, rfl, hq⟩
80
81theorem EWP.bind {α β : Type} {h : Heap} {m : M α} {f : α → M β}
82    {P : α → Heap → Prop} {Q : β → Heap → Prop}
83    (hm : EWP m h P) (hf : ∀ a h', P a h' → EWP (f a) h' Q) :
84    EWP (m >>= f) h Q := by
85  obtain ⟨a, h', hr, hp⟩ := hm
86  obtain ⟨v, h'', hs, hq⟩ := hf a h' hp
87  exact ⟨v, h'', by rw [bind_app, hr]; exact hs, hq⟩
88
89theorem EWP.read {α β : Type} {h : Heap} {m : M α} {f : α → M β} {a : α}
90    {Q : β → Heap → Prop} (hr : m h = .ok (a, h)) (hf : EWP (f a) h Q) :
91    EWP (m >>= f) h Q := by
92  refine EWP.bind (P := fun a' h' => a' = a ∧ h' = h) ⟨a, h, hr, rfl, rfl⟩ ?_
93  rintro _ _ ⟨rfl, rfl⟩
94  exact hf
95
96theorem EWP.mono {α : Type} {h : Heap} {m : M α} {P Q : α → Heap → Prop}
97    (hm : EWP m h P) (hf : ∀ a h', P a h' → Q a h') : EWP m h Q := by
98  obtain ⟨a, h', hr, hp⟩ := hm
99  exact ⟨a, h', hr, hf a h' hp⟩
100
101/-- Stored code words and lengths, observed without changing them. -/
102def blWords (d : DeflateState) (k : Nat) : UInt16 × UInt16 :=
103  (d.bl_tree[k]!.fc, d.bl_tree[k]!.dl)
104
105/-- Only scalar code data, not a called-function contract. -/
106def CodeFits (t : Nat → UInt16 × UInt16) (k : Nat) : Prop :=
107  (t k).2.toNat ≤ 15 ∧ (t k).1.toNat < 2 ^ (t k).2.toNat
108
109/-- The actual bit-length-tree pointer and both entry loads are executed.
110Source arrays are transported by the recorded write frame. -/
111theorem EmitState.bl_code {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
112    {w : List Bool} (ht : EmitState id b h0 d0 buf0 w h d buf) (k : Nat) (hk : k < 19)
113    (hc : CodeFits (blWords d0) k)
114    (hr : 8 * d.pending.toNat + d.bi_valid.toInt.toNat + (blWords d0 k).2.toNat ≤ 8 * buf.size) :
115    EWP (do send_code (some (.tab id)) (k : Int) (← pBltree (some (.tab id)))) h
116      (fun _ h' => ∃ d' buf', EmitState id b h0 d0 buf0 (w ++ codeBits (blWords d0) k) h' d' buf') := by
117  have hB : 19 ≤ d.bl_tree.size := by have := ht.inv.base.wf.2.2.1; omega
118  have heq := ht.tree_arrays.2.2
119  have hdl := getDl_sel ht.inv.base.dstate .bl (i := k) (by exact Nat.lt_of_lt_of_le hk hB)
120  have hfc := getFc_sel ht.inv.base.dstate .bl (i := k) (by exact Nat.lt_of_lt_of_le hk hB)
121  change getDl (.ref (.dstate_bl_tree id) 0) (k : Int) h = .ok (d.bl_tree[k]!.dl, h) at hdl
122  change getFc (.ref (.dstate_bl_tree id) 0) (k : Int) h = .ok (d.bl_tree[k]!.fc, h) at hfc
123  rw [heq] at hdl hfc
124  obtain ⟨h', d', buf', hs, ht'⟩ := ht.step
125    (send_code_emit ht.inv (k : Int) (.ref (.dstate_bl_tree id) 0) _ _ hdl hfc hc.1 hc.2 hr)
126  refine ⟨(), h', ?_, d', buf', ht'⟩
127  rw [bind_app, pBltree_run ht.inv.base.dstate]
128  exact hs
129
130/-- Actual extra-bit emission preserves the same exact heap frame. -/
131theorem EmitState.extra_bits {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
132    {w : List Bool} (ht : EmitState id b h0 d0 buf0 w h d buf) (value len : Int32) (V L : Nat)
133    (hV : v16 value = V) (hL : len.toInt.toNat = L) (hl0 : 0 ≤ len.toInt) (hl15 : len.toInt ≤ 15)
134    (hfit : V < 2 ^ L)
135    (hr : 8 * d.pending.toNat + d.bi_valid.toInt.toNat + L ≤ 8 * buf.size) :
136    EWP (send_bits (some (.tab id)) value len) h
137      (fun _ h' => ∃ d' buf', EmitState id b h0 d0 buf0 (w ++ natBits V L) h' d' buf') := by
138  have he := send_bits_emit ht.inv value len hl0 hl15 (by rwa [hV, hL]) (by rwa [hL])
139  rw [hV, hL] at he
140  obtain ⟨h', d', buf', hs, ht'⟩ := ht.step he
141  exact ⟨(), h', hs, d', buf', ht'⟩
142
143end Zlib.Trees.Proofs.Out