trees.c.heap.base.lean

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

1import ZlibF.Zlib.«trees.c»
2
3/-!
4# trees.c: the calculus for `pqdownheap`, `pqremove`, `gen_bitlen`, `build_tree`
5
6All four functions touch one record of the heap, the `deflate_state` with block number `id`, and nothing else
7(the static tables are read, never written). So the heap is always `setD h0 id d`: a base heap `h0` with the record
8`id` replaced by `d`. `WS h0 id m d Q` says that the computation `m` run on `setD h0 id d` ends without a fault on
9`setD h0 id d'` with a result `a` such that `Q a d'`. Then every proof is about the record `d`, and `h0` only matters
10through the static tables.
11-/
12
13namespace Zlib.Trees.Proofs
14open C Zlib.Trees
15
16/-- The heap `h` with the deflate state `id` replaced by `d`. -/
17def setD (h : Heap) (id : Nat) (d : DeflateState) : Heap := { h with dstates := upd h.dstates id (some d) }
18
19@[simp] theorem setD_dstates_same (h : Heap) (id : Nat) (d : DeflateState) : (setD h id d).dstates id = some d := by
20  simp [setD]
21@[simp] theorem setD_setD (h : Heap) (id : Nat) (d d' : DeflateState) : setD (setD h id d) id d' = setD h id d' := by
22  simp [setD, upd_upd]
23@[simp] theorem setD_static (h : Heap) (id : Nat) (d : DeflateState) : (setD h id d).static = h.static := rfl
24theorem setD_self {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d) : setD h id d = h := by
25  simp [setD, upd_self _ _ _ hd]
26
27/-- `m` run on `setD h0 id d` ends in `setD h0 id d'` with a result `a`, and `Q a d'`. -/
28def WS {α : Type} (h0 : Heap) (id : Nat) (m : M α) (d : DeflateState) (Q : α → DeflateState → Prop) : Prop :=
29  ∃ a d', m (setD h0 id d) = .ok (a, setD h0 id d') ∧ Q a d'
30
31section ws
32variable {α β : Type} {h0 : Heap} {id : Nat}
33
34theorem WS.pure' {a : α} {d : DeflateState} {Q : α → DeflateState → Prop} (hq : Q a d) :
35    WS h0 id (Pure.pure a : M α) d Q := ⟨a, d, rfl, hq⟩
36
37theorem WS.bind' {m : M α} {f : α → M β} {d : DeflateState} {Q : α → DeflateState → Prop}
38    {R : β → DeflateState → Prop} (hm : WS h0 id m d Q) (hf : ∀ a d', Q a d' → WS h0 id (f a) d' R) :
39    WS h0 id (m >>= f) d R := by
40  obtain ⟨a, d1, e, hq⟩ := hm
41  obtain ⟨b, d2, e2, hr⟩ := hf a d1 hq
42  exact ⟨b, d2, by rw [bind_app, e]; exact e2, hr⟩
43
44theorem WS.mono {m : M α} {d : DeflateState} {Q R : α → DeflateState → Prop} (hm : WS h0 id m d Q)
45    (hr : ∀ a d', Q a d' → R a d') : WS h0 id m d R := by
46  obtain ⟨a, d1, e, hq⟩ := hm
47  exact ⟨a, d1, e, hr a d1 hq⟩
48
49theorem WS.ite' {c : Prop} [Decidable c] {m1 m2 : M α} {d : DeflateState} {Q : α → DeflateState → Prop}
50    (h1 : c → WS h0 id m1 d Q) (h2 : ¬ c → WS h0 id m2 d Q) : WS h0 id (if c then m1 else m2) d Q := by
51  by_cases hc : c
52  · simp only [hc, ite_true]; exact h1 hc
53  · simp only [hc, ite_false]; exact h2 hc
54
55theorem WS.of_eq {m : M α} {d d' : DeflateState} {a : α} (e : m (setD h0 id d) = .ok (a, setD h0 id d'))
56    {Q : α → DeflateState → Prop} (hq : Q a d') : WS h0 id m d Q := ⟨a, d', e, hq⟩
57
58/-- `while` with a measure: `Inv` is kept, the measure decreases, and `Q` holds when the condition fails. -/
59theorem WS.cwhile' {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ}
60    (Inv : σ → DeflateState → Prop) (μ : σ → DeflateState → Nat) (Q : σ → DeflateState → Prop)
61    (hstep : ∀ s d, Inv s d →
62      (∃ s1 d1, cond s (setD h0 id d) = .ok ((false, s1), setD h0 id d1) ∧ Q s1 d1) ∨
63      (∃ s1 d1 s2 d2, cond s (setD h0 id d) = .ok ((true, s1), setD h0 id d1) ∧
64        body s1 (setD h0 id d1) = .ok (s2, setD h0 id d2) ∧ Inv s2 d2 ∧ μ s2 d2 < μ s d))
65    {s : σ} {d : DeflateState} (hI : Inv s d) (hfuel : μ s d < fuel) :
66    WS h0 id (cwhile cond body s) d (fun s' d' => Q s' d') := by
67  have key : ∀ k n s d, Inv s d → μ s d ≤ k → k < n →
68      ∃ s' d', cwhile.go cond body n s (setD h0 id d) = .ok (s', setD h0 id d') ∧ Q s' d' := by
69    intro k
70    induction k using Nat.strongRecOn with
71    | _ k ih =>
72      intro n s d hI hμ hn
73      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
74      rcases hstep s d hI with ⟨s1, d1, hc, hq⟩ | ⟨s1, d1, s2, d2, hc, hb, hI2, hlt⟩
75      · exact ⟨s1, d1, by simp [cwhile.go, hc], hq⟩
76      · obtain ⟨s', d', hgo, hq⟩ := ih (μ s2 d2) (by omega) n s2 d2 hI2 (Nat.le_refl _) (by omega)
77        exact ⟨s', d', by simp [cwhile.go, hc, hb, hgo], hq⟩
78  obtain ⟨s', d', e, hq⟩ := key (μ s d) fuel s d hI (Nat.le_refl _) hfuel
79  exact ⟨s', d', e, hq⟩
80
81/-- `do ... while` with a measure. -/
82theorem WS.cdoWhile' {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ}
83    (Inv : σ → DeflateState → Prop) (μ : σ → DeflateState → Nat) (Q : σ → DeflateState → Prop)
84    (hstep : ∀ s d, Inv s d → ∃ s1 d1, body s (setD h0 id d) = .ok (s1, setD h0 id d1) ∧
85      ((∃ s2 d2, cond s1 (setD h0 id d1) = .ok ((false, s2), setD h0 id d2) ∧ Q s2 d2) ∨
86       (∃ s2 d2, cond s1 (setD h0 id d1) = .ok ((true, s2), setD h0 id d2) ∧ Inv s2 d2 ∧ μ s2 d2 < μ s d)))
87    {s : σ} {d : DeflateState} (hI : Inv s d) (hfuel : μ s d < fuel) :
88    WS h0 id (cdoWhile body cond s) d (fun s' d' => Q s' d') := by
89  have key : ∀ k n s d, Inv s d → μ s d ≤ k → k < n →
90      ∃ s' d', cdoWhile.go body cond n s (setD h0 id d) = .ok (s', setD h0 id d') ∧ Q s' d' := by
91    intro k
92    induction k using Nat.strongRecOn with
93    | _ k ih =>
94      intro n s d hI hμ hn
95      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
96      obtain ⟨s1, d1, hb, hc⟩ := hstep s d hI
97      rcases hc with ⟨s2, d2, hc, hq⟩ | ⟨s2, d2, hc, hI2, hlt⟩
98      · exact ⟨s2, d2, by simp [cdoWhile.go, hb, hc], hq⟩
99      · obtain ⟨s', d', hgo, hq⟩ := ih (μ s2 d2) (by omega) n s2 d2 hI2 (Nat.le_refl _) (by omega)
100        exact ⟨s', d', by simp [cdoWhile.go, hb, hc, hgo], hq⟩
101  obtain ⟨s', d', e, hq⟩ := key (μ s d) fuel s d hI (Nat.le_refl _) hfuel
102  exact ⟨s', d', e, hq⟩
103
104/-- `while`, with the steps written as `WS` facts: the condition, and on `true` the body. -/
105theorem WS.cwhile2 {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ}
106    (Inv : σ → DeflateState → Prop) (μ : σ → DeflateState → Nat) (Q : σ → DeflateState → Prop)
107    (hstep : ∀ s d, Inv s d → WS h0 id (cond s) d (fun r d1 =>
108      (r.1 = false ∧ Q r.2 d1) ∨
109      (r.1 = true ∧ WS h0 id (body r.2) d1 (fun s2 d2 => Inv s2 d2 ∧ μ s2 d2 < μ s d))))
110    {s : σ} {d : DeflateState} (hI : Inv s d) (hfuel : μ s d < fuel) :
111    WS h0 id (cwhile cond body s) d (fun s' d' => Q s' d') := by
112  refine WS.cwhile' Inv μ Q ?_ hI hfuel
113  intro s d hI
114  obtain ⟨⟨b, s1⟩, d1, hc, hq⟩ := hstep s d hI
115  rcases hq with ⟨hb, hq⟩ | ⟨hb, s2, d2, hbody, hI2, hlt⟩
116  · simp only at hb hq
117    subst hb
118    exact Or.inl ⟨s1, d1, hc, hq⟩
119  · simp only at hb
120    subst hb
121    exact Or.inr ⟨s1, d1, s2, d2, hc, hbody, hI2, hlt⟩
122
123/-- `do ... while`, with the steps written as `WS` facts. -/
124theorem WS.cdoWhile2 {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ}
125    (Inv : σ → DeflateState → Prop) (μ : σ → DeflateState → Nat) (Q : σ → DeflateState → Prop)
126    (hstep : ∀ s d, Inv s d → WS h0 id (body s) d (fun s1 d1 => WS h0 id (cond s1) d1 (fun r d2 =>
127      (r.1 = false ∧ Q r.2 d2) ∨ (r.1 = true ∧ Inv r.2 d2 ∧ μ r.2 d2 < μ s d))))
128    {s : σ} {d : DeflateState} (hI : Inv s d) (hfuel : μ s d < fuel) :
129    WS h0 id (cdoWhile body cond s) d (fun s' d' => Q s' d') := by
130  refine WS.cdoWhile' Inv μ Q ?_ hI hfuel
131  intro s d hI
132  obtain ⟨s1, d1, hb, ⟨⟨b, s2⟩, d2, hc, hq⟩⟩ := hstep s d hI
133  refine ⟨s1, d1, hb, ?_⟩
134  rcases hq with ⟨hb', hq⟩ | ⟨hb', hI2, hlt⟩
135  · simp only at hb' hq
136    subst hb'
137    exact Or.inl ⟨s2, d2, hc, hq⟩
138  · simp only at hb' hI2 hlt
139    subst hb'
140    exact Or.inr ⟨s2, d2, hc, hI2, hlt⟩
141
142theorem getD_set {α : Type} [Inhabited α] (a : Array α) (k i : Nat) (x : α) (hk : k < a.size) :
143    (a.set! k x)[i]! = if i = k then x else a[i]! := by
144  by_cases h : i = k
145  · subst h; simp [Array.set!_eq_setIfInBounds, getElem!_pos, hk]
146  · simp only [h, ite_false]
147    simp only [Array.set!_eq_setIfInBounds]
148    rcases Nat.lt_or_ge i a.size with hi | hi
149    · rw [getElem!_pos (a.setIfInBounds k x) i (by simpa using hi), getElem!_pos a i hi]
150      rw [Array.getElem_setIfInBounds]; simp [Ne.symm h]; exact hi
151    · have h1 : ¬ i < (a.setIfInBounds k x).size := by simp; omega
152      rw [getElem!_neg (a.setIfInBounds k x) i h1, getElem!_neg a i (by omega)]
153
154theorem size_set! {α : Type} (a : Array α) (k : Nat) (x : α) : (a.set! k x).size = a.size := by simp
155
156end ws
157
158/-! ### Generic array access at offset 0 -/
159
160section arr
161variable {R T : Type} [Space Heap R T] [Inhabited T]
162
163theorem index0_ok {h : Heap} {r : R} {a : Array T} (hg : Space.get h r = some a) {i : Int} (h0 : 0 ≤ i)
164    (h1 : i < a.size) : Ptr.index (Ptr.ref r 0) i h = .ok (a[i.toNat]!, h) := by
165  have := Ptr.index_ok (h := h) (r := r) (a := a) (off := 0) (i := i.toNat) hg (by omega)
166  have e : ((i.toNat : Nat) : Int) = i := by omega
167  rw [e] at this
168  have hlt : i.toNat < a.size := by omega
169  simp only [Nat.zero_add] at this
170  rw [getElem!_pos a i.toNat hlt]
171  exact this
172
173omit [Inhabited T] in
174theorem setAt0_ok {h : Heap} {r : R} {a : Array T} (hg : Space.get h r = some a) (hro : Space.ro h r = false)
175    {i : Int} (h0 : 0 ≤ i) (h1 : i < a.size) (v : T) :
176    setAt (Ptr.ref r 0) i v h = .ok ((), Space.put h r (a.set! i.toNat v)) := by
177  have hadd : OkOn h (Ptr.add (Ptr.ref r 0) i) (Ptr.ref r i.toNat) := by
178    have := Ptr.add_ok (h := h) (r := r) (a := a) (off := 0) (k := i) hg (by omega) (by omega)
179    simpa using this
180  unfold setAt
181  rw [bind_app, hadd]
182  exact Ptr.store_ok hg hro (by omega)
183
184end arr
185
186/-! ### The three dynamic trees -/
187
188/-- Which tree array of the deflate state: `dyn_ltree`, `dyn_dtree` or `bl_tree`. -/
189inductive TK where
190  | lit | dist | bl
191  deriving DecidableEq, Inhabited
192
193def TK.ref : TK → Nat → CtDataRef
194  | .lit, id => .dstate_dyn_ltree id
195  | .dist, id => .dstate_dyn_dtree id
196  | .bl, id => .dstate_bl_tree id
197
198def TK.arr : TK → DeflateState → Array CtData
199  | .lit, d => d.dyn_ltree
200  | .dist, d => d.dyn_dtree
201  | .bl, d => d.bl_tree
202
203def TK.setArr : TK → DeflateState → Array CtData → DeflateState
204  | .lit, d, a => { d with dyn_ltree := a }
205  | .dist, d, a => { d with dyn_dtree := a }
206  | .bl, d, a => { d with bl_tree := a }
207
208/-- The size of the tree array: 573, 61, 39. -/
209def TK.size : TK → Nat
210  | .lit => 573
211  | .dist => 61
212  | .bl => 39
213
214section prim
215variable {h0 : Heap} {id : Nat} {d : DeflateState}
216
217theorem tk_get (k : TK) : Space.get (setD h0 id d) (k.ref id) = some (k.arr d) := by
218  cases k <;> simp [TK.ref, TK.arr, Space.get, setD]
219theorem tk_put (k : TK) (a : Array CtData) : Space.put (setD h0 id d) (k.ref id) a = setD h0 id (k.setArr d a) := by
220  cases k <;> simp [TK.ref, TK.setArr, Space.put, setD, upd_upd]
221theorem tk_ro (k : TK) : Space.ro (setD h0 id d) (k.ref id) = false := by cases k <;> rfl
222
223@[simp] theorem tk_setArr_heap (k : TK) (a) : (k.setArr d a).heap = d.heap := by cases k <;> rfl
224@[simp] theorem tk_setArr_depth (k : TK) (a) : (k.setArr d a).depth = d.depth := by cases k <;> rfl
225@[simp] theorem tk_setArr_bl_count (k : TK) (a) : (k.setArr d a).bl_count = d.bl_count := by cases k <;> rfl
226@[simp] theorem tk_setArr_heap_len (k : TK) (a) : (k.setArr d a).heap_len = d.heap_len := by cases k <;> rfl
227@[simp] theorem tk_setArr_heap_max (k : TK) (a) : (k.setArr d a).heap_max = d.heap_max := by cases k <;> rfl
228@[simp] theorem tk_setArr_opt_len (k : TK) (a) : (k.setArr d a).opt_len = d.opt_len := by cases k <;> rfl
229@[simp] theorem tk_setArr_static_len (k : TK) (a) : (k.setArr d a).static_len = d.static_len := by cases k <;> rfl
230@[simp] theorem tk_setArr_l_desc (k : TK) (a) : (k.setArr d a).l_desc = d.l_desc := by cases k <;> rfl
231@[simp] theorem tk_setArr_d_desc (k : TK) (a) : (k.setArr d a).d_desc = d.d_desc := by cases k <;> rfl
232@[simp] theorem tk_setArr_bl_desc (k : TK) (a) : (k.setArr d a).bl_desc = d.bl_desc := by cases k <;> rfl
233@[simp] theorem tk_arr_setArr (k : TK) (a) : k.arr (k.setArr d a) = a := by cases k <;> rfl
234
235/-- `S id`: the pointer `s`. -/
236abbrev Sp (id : Nat) : DeflateStatePtr := some (DeflateStateRef.tab id)
237
238theorem ws_sid : WS h0 id (sid (Sp id)) d (fun v d' => v = id ∧ d' = d) :=
239  WS.of_eq (by simp [sid, ldDeflateState, DeflateStateRef.get]) ⟨rfl, rfl⟩
240
241theorem ws_rd : WS h0 id (rd (Sp id)) d (fun v d' => v = d ∧ d' = d) :=
242  WS.of_eq (by simp [rd, ldDeflateState, DeflateStateRef.get]) ⟨rfl, rfl⟩
243
244theorem ws_md (f : DeflateState → DeflateState) : WS h0 id (md (Sp id) f) d (fun _ d' => d' = f d) := by
245  refine WS.of_eq (a := ()) (d' := f d) ?_ rfl
246  simp only [md, bind_app, ldDeflateState, DeflateStateRef.get, setD_dstates_same, stDeflateState,
247    DeflateStateRef.isRo, DeflateStateRef.put]
248  simp [setD, upd_upd]
249
250theorem ws_pHeap : WS h0 id (pHeap (Sp id)) d (fun v d' => v = Ptr.ref (IRef.dstate_heap id) 0 ∧ d' = d) :=
251  WS.bind' ws_sid fun a d' ⟨ha, hd'⟩ => by subst ha; subst hd'; exact WS.pure' ⟨rfl, rfl⟩
252theorem ws_pDepth : WS h0 id (pDepth (Sp id)) d (fun v d' => v = Ptr.ref (BRef.dstate_depth id) 0 ∧ d' = d) :=
253  WS.bind' ws_sid fun a d' ⟨ha, hd'⟩ => by subst ha; subst hd'; exact WS.pure' ⟨rfl, rfl⟩
254theorem ws_pBlCount : WS h0 id (pBlCount (Sp id)) d (fun v d' => v = Ptr.ref (WRef.dstate_bl_count id) 0 ∧ d' = d) :=
255  WS.bind' ws_sid fun a d' ⟨ha, hd'⟩ => by subst ha; subst hd'; exact WS.pure' ⟨rfl, rfl⟩
256
257/-! Reads and writes of the arrays of the record. `i` is a C index (an `Int`). -/
258
259theorem ws_index_heap (i : Int) (h0' : 0 ≤ i) (h1 : i < d.heap.size) :
260    WS h0 id (Ptr.index (Ptr.ref (IRef.dstate_heap id) 0) i) d (fun v d' => v = d.heap[i.toNat]! ∧ d' = d) :=
261  WS.of_eq (index0_ok (IRef.get_dstate_heap (setD_dstates_same h0 id d)) h0' h1) ⟨rfl, rfl⟩
262
263theorem ws_setAt_heap (i : Int) (v : Int32) (h0' : 0 ≤ i) (h1 : i < d.heap.size) :
264    WS h0 id (setAt (Ptr.ref (IRef.dstate_heap id) 0) i v) d (fun _ d' => d' = { d with heap := d.heap.set! i.toNat v }) := by
265  refine WS.of_eq (a := ()) (d' := { d with heap := d.heap.set! i.toNat v }) ?_ rfl
266  rw [setAt0_ok (IRef.get_dstate_heap (setD_dstates_same h0 id d)) (IRef.ro_dstate_heap _ _) h0' h1,
267    IRef.put_dstate_heap (setD_dstates_same h0 id d)]
268  simp [setD, upd_upd]
269
270theorem ws_index_depth (i : Int) (h0' : 0 ≤ i) (h1 : i < d.depth.size) :
271    WS h0 id (Ptr.index (Ptr.ref (BRef.dstate_depth id) 0) i) d (fun v d' => v = d.depth[i.toNat]! ∧ d' = d) :=
272  WS.of_eq (index0_ok (BRef.get_dstate_depth (setD_dstates_same h0 id d)) h0' h1) ⟨rfl, rfl⟩
273
274theorem ws_setAt_depth (i : Int) (v : UInt8) (h0' : 0 ≤ i) (h1 : i < d.depth.size) :
275    WS h0 id (setAt (Ptr.ref (BRef.dstate_depth id) 0) i v) d (fun _ d' => d' = { d with depth := d.depth.set! i.toNat v }) := by
276  refine WS.of_eq (a := ()) (d' := { d with depth := d.depth.set! i.toNat v }) ?_ rfl
277  rw [setAt0_ok (BRef.get_dstate_depth (setD_dstates_same h0 id d)) (BRef.ro_dstate_depth _ _) h0' h1,
278    BRef.put_dstate_depth (setD_dstates_same h0 id d)]
279  simp [setD, upd_upd]
280
281theorem ws_index_blc (i : Int) (h0' : 0 ≤ i) (h1 : i < d.bl_count.size) :
282    WS h0 id (Ptr.index (Ptr.ref (WRef.dstate_bl_count id) 0) i) d (fun v d' => v = d.bl_count[i.toNat]! ∧ d' = d) :=
283  WS.of_eq (index0_ok (WRef.get_dstate_bl_count (setD_dstates_same h0 id d)) h0' h1) ⟨rfl, rfl⟩
284
285theorem ws_setAt_blc (i : Int) (v : UInt16) (h0' : 0 ≤ i) (h1 : i < d.bl_count.size) :
286    WS h0 id (setAt (Ptr.ref (WRef.dstate_bl_count id) 0) i v) d (fun _ d' => d' = { d with bl_count := d.bl_count.set! i.toNat v }) := by
287  refine WS.of_eq (a := ()) (d' := { d with bl_count := d.bl_count.set! i.toNat v }) ?_ rfl
288  rw [setAt0_ok (WRef.get_dstate_bl_count (setD_dstates_same h0 id d)) (WRef.ro_dstate_bl_count _ _) h0' h1,
289    WRef.put_dstate_bl_count (setD_dstates_same h0 id d)]
290  simp [setD, upd_upd]
291
292/-! The tree arrays. -/
293
294theorem ws_getFc (k : TK) (i : Int) (h0' : 0 ≤ i) (h1 : i < (k.arr d).size) :
295    WS h0 id (getFc (Ptr.ref (k.ref id) 0) i) d (fun v d' => v = ((k.arr d)[i.toNat]!).fc ∧ d' = d) := by
296  unfold getFc
297  have := index0_ok (tk_get (h0 := h0) (id := id) (d := d) k) h0' h1
298  exact WS.of_eq (by simp only [bind_app, this]; rfl) ⟨rfl, rfl⟩
299
300theorem ws_getDl (k : TK) (i : Int) (h0' : 0 ≤ i) (h1 : i < (k.arr d).size) :
301    WS h0 id (getDl (Ptr.ref (k.ref id) 0) i) d (fun v d' => v = ((k.arr d)[i.toNat]!).dl ∧ d' = d) := by
302  unfold getDl
303  have := index0_ok (tk_get (h0 := h0) (id := id) (d := d) k) h0' h1
304  exact WS.of_eq (by simp only [bind_app, this]; rfl) ⟨rfl, rfl⟩
305
306/-- `tree[i]` with the fields `fc`, `dl` replaced. -/
307def CtData.withFc (e : CtData) (v : UInt16) : CtData := { e with fc := v }
308
309theorem ws_setFc (k : TK) (i : Int) (v : UInt16) (h0' : 0 ≤ i) (h1 : i < (k.arr d).size) :
310    WS h0 id (setFc (Ptr.ref (k.ref id) 0) i v) d
311      (fun _ d' => d' = k.setArr d ((k.arr d).set! i.toNat { (k.arr d)[i.toNat]! with fc := v })) := by
312  refine WS.of_eq (a := ()) (d' := k.setArr d ((k.arr d).set! i.toNat { (k.arr d)[i.toNat]! with fc := v })) ?_ rfl
313  have hg := tk_get (h0 := h0) (id := id) (d := d) k
314  have hpt : OkOn (setD h0 id d) (Ptr.add (Ptr.ref (k.ref id) 0) i) (Ptr.ref (k.ref id) i.toNat) := by
315    have := Ptr.add_ok (h := setD h0 id d) (r := k.ref id) (a := k.arr d) (off := 0) (k := i) hg (by omega) (by omega)
316    simpa using this
317  have hld : OkOn (setD h0 id d) (Ptr.load (Ptr.ref (k.ref id) i.toNat)) ((k.arr d)[i.toNat]!) := by
318    have := Ptr.load_ok (h := setD h0 id d) (r := k.ref id) (a := k.arr d) (off := i.toNat) hg (by omega)
319    rwa [← getElem!_pos (k.arr d) i.toNat (by omega)] at this
320  unfold setFc
321  simp only [bind_app]
322  unfold OkOn at hpt hld
323  rw [hpt]; simp only []
324  rw [hld]; simp only []
325  rw [Ptr.store_ok hg (tk_ro k) (by omega), tk_put]
326
327theorem ws_setDl (k : TK) (i : Int) (v : UInt16) (h0' : 0 ≤ i) (h1 : i < (k.arr d).size) :
328    WS h0 id (setDl (Ptr.ref (k.ref id) 0) i v) d
329      (fun _ d' => d' = k.setArr d ((k.arr d).set! i.toNat { (k.arr d)[i.toNat]! with dl := v })) := by
330  refine WS.of_eq (a := ()) (d' := k.setArr d ((k.arr d).set! i.toNat { (k.arr d)[i.toNat]! with dl := v })) ?_ rfl
331  have hg := tk_get (h0 := h0) (id := id) (d := d) k
332  have hpt : OkOn (setD h0 id d) (Ptr.add (Ptr.ref (k.ref id) 0) i) (Ptr.ref (k.ref id) i.toNat) := by
333    have := Ptr.add_ok (h := setD h0 id d) (r := k.ref id) (a := k.arr d) (off := 0) (k := i) hg (by omega) (by omega)
334    simpa using this
335  have hld : OkOn (setD h0 id d) (Ptr.load (Ptr.ref (k.ref id) i.toNat)) ((k.arr d)[i.toNat]!) := by
336    have := Ptr.load_ok (h := setD h0 id d) (r := k.ref id) (a := k.arr d) (off := i.toNat) hg (by omega)
337    rwa [← getElem!_pos (k.arr d) i.toNat (by omega)] at this
338  unfold setDl
339  simp only [bind_app]
340  unfold OkOn at hpt hld
341  rw [hpt]; simp only []
342  rw [hld]; simp only []
343  rw [Ptr.store_ok hg (tk_ro k) (by omega), tk_put]
344
345end prim
346
347end Zlib.Trees.Proofs