inffast.c.distance-origin.lean

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

1import ZlibF.Spec.InflateFastDistanceOrigin
2import ZlibF.Proof.«inffast.c.origin»
3import ZlibF.Proof.«inffast.c.advance»
4
5/-!
6# Source origin through actual distance lookup, extra bits and copying
7
8Every error path retains the exact input suffix. Existing execution
9results are joined only after identifying the same deterministic run.
10-/
11
12set_option autoImplicit false
13
14namespace Zlib.Inffast.Proofs
15open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
16variable {e : Env} {c : Ctx}
17
18private theorem distCont_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o used : Nat)
19    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
20    (hAb : A.size < 2 ^ 63)
21    (hx : l.op.toNat ≤ 13) (hxb : l.op.toNat ≤ l.bits.toNat) (hd1 : 1 ≤ l.dist.toNat) (hd2 : l.dist.toNat ≤ 65536)
22    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258) (hbroke : l.broke = false)
23    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
24    Wp (distCont c l) (e.heap A msg m) (fun l' _ =>
25      l'.in_ = .ref (.blk e.ib) i ∧
26      Origin.Inv e l'.hold.toNat l'.bits.toNat i (used + l.op.toNat)) := by
27  have hbgo : e.bg ≤ o := by have := e.bg_le; have := hls.ho0; omega
28  have hoA : o ≤ A.size := by omega
29  have hxs : l.op.toNat < 32 := by omega
30  unfold distCont
31  refine Wp.bindO (shl32_ok hxs) ?_
32  dsimp only
33  have hlow := hold_low32 (x := l.hold) (k := l.op) hxs
34  have hlowlt : l.hold.toNat % 2 ^ l.op.toNat < 2 ^ l.op.toNat := Nat.mod_lt _ (Nat.pow_pos (by omega))
35  have hpow : 2 ^ l.op.toNat ≤ 2 ^ 13 := Nat.pow_le_pow_right (by omega) hx
36  have hdist' : (l.dist + (l.hold.toUInt32 &&& (1 <<< l.op) - 1)).toNat = l.dist.toNat + l.hold.toNat % 2 ^ l.op.toNat := by
37    rw [u32_toNat_add (by rw [hlow]; omega), hlow]
38  refine Wp.bindO (shr64_ok (x := l.hold) (n := l.op.toUInt64) (by rw [UInt32.toNat_toUInt64]; omega)) ?_
39  have hbgdef : e.bg = e.o0 - (e.start.toNat - e.sm0.avail_out.toNat) := rfl
40  have hst32 := UInt32.toNat_lt e.start
41  have hstart := e.hstart
42  have hbeg := e.hbeg
43  have hdiff : OkOn (e.heap A msg m) (Ptr.diff l.out c.beg) (Int64.ofInt (((o - e.bg : Nat)) : Int)) := by
44    rw [hls.hout, hc.beg]
45    have := Ptr.diff_ok (r := BRef.blk e.ob) (a := A) (o1 := o) (o2 := e.bg) (e.heap_bytes_ob A msg m) hoA (by omega)
46      ⟨by omega, by omega⟩
47    have e1 : (o : Int) - (e.bg : Int) = ((o - e.bg : Nat) : Int) := by omega
48    rw [e1] at this
49    exact this
50  refine Wp.bindO hdiff ?_
51  have hopn : (Int64.ofInt (((o - e.bg : Nat)) : Int)).toUInt64.toUInt32.toNat = o - e.bg := i64_toU32 _ (by omega)
52  have hls1 : LS e (dropL l l.op) i o := hls.dropL l.op hxb (by omega)
53  have hrb := readBits_bitsOfNat l.op.toNat l.bits.toNat l.hold.toNat (inBits e i) hxb
54  have hsg := Sg_dropL (e := e) l l.op i hxb (by omega)
55  refine Wp.mono (copyMatch_run (e := e) (c := c) hc A msg m
56    { in_ := l.in_, out := l.out, hold := l.hold >>> l.op.toUInt64, bits := l.bits - l.op, here := l.here,
57      op := (Int64.ofInt (((o - e.bg : Nat)) : Int)).toUInt64.toUInt32, len := l.len,
58      dist := l.dist + (l.hold.toUInt32 &&& 1 <<< l.op - 1), from_ := l.from_, broke := l.broke, againL := l.againL,
59      againD := l.againD } o hls.hout hbgo hopn (by simp only [hdist']; omega) hlen.1 (by simp; omega) hbroke) ?_
60  intro l' h' hq
61  obtain ⟨hin, hhold, hbits, _, _, _⟩ := hq
62  refine ⟨hin.trans hls.hin, ?_⟩
63  have dropped := drop_preserves_origin e l.hold.toNat l.bits.toNat i used l.op.toNat origin hxb
64  have afterDrop : Origin.Inv e (dropL l l.op).hold.toNat (dropL l l.op).bits.toNat i
65      (used + l.op.toNat) := by
66    simpa only [dropL_hold l l.op (by omega), dropL_bits l l.op hxb] using dropped
67  simpa only [hhold, hbits, dropL] using afterDrop
68
69private theorem pullL_origin (l : L) (i o used : Nat)
70    (hls : LS e l i o) (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used)
71    (available : i < e.i0 + e.sm0.avail_in.toNat) :
72    Origin.Inv e (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1))).hold.toNat
73      (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1))).bits.toNat (i+1) used := by
74  have result := pull_preserves_origin e l.hold.toNat l.bits.toNat i used origin available
75  simpa only [pullL_hold l _ _ hls.hb hls.hH, pullL_bits l _ _ hls.hb] using result
76
77private theorem dodistBase_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
78    (l : L) (i o used : Nat)
79    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size)
80    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hAb : A.size < 2 ^ 63)
81    (hx : l.op.toNat ≤ 13) (hd1 : 1 ≤ l.dist.toNat) (hd2 : l.dist.toNat ≤ 65536)
82    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258) (hbroke : l.broke = false)
83    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨
84      (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 5 ≤ l.bits.toNat))
85    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
86    Wp (dodistBase c l) (e.heap A msg m) (fun l' _ =>
87      ∃ i', l'.in_ = .ref (.blk e.ib) i' ∧
88        Origin.Inv e l'.hold.toNat l'.bits.toNat i' (used + l.op.toNat)) := by
89  unfold dodistBase
90  by_cases h1 : l.bits < l.op
91  · simp only [h1, ite_true]
92    have h1' : l.bits.toNat < l.op.toNat := UInt32.lt_iff_toNat_lt.mp h1
93    have hi : i < e.i0 + e.sm0.avail_in.toNat := by omega
94    refine Wp.bindO (pull_run e _ l i o hls (by omega) hi (e.heap_bytes_in A msg m)) ?_
95    have locals3 := hls.pullL (by omega) hi
96    have origin3 := pullL_origin l i o used hls origin hi
97    have bits3 := pullL_bits l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1)) hls.hb
98    by_cases h2 : (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1))).bits <
99        (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1))).op
100    · simp only [h2, ite_true]
101      have h2' : l.bits.toNat + 8 < l.op.toNat := by
102        have := UInt32.lt_iff_toNat_lt.mp h2
103        simp only [pullL] at this bits3 ⊢
104        omega
105      have hi2 : i+1 < e.i0 + e.sm0.avail_in.toNat := by omega
106      have bound3 : (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1))).bits.toNat ≤ 22 := by omega
107      refine Wp.bindO (pull_run e _ _ (i+1) o locals3 bound3 hi2 (e.heap_bytes_in A msg m)) ?_
108      have locals4 := locals3.pullL bound3 hi2
109      have origin4 := pullL_origin _ (i+1) o used locals3 origin3 hi2
110      have bits4 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1)))
111        (e.IN.getD (i+1) 0) (.ref (.blk e.ib) (i+1+1)) locals3.hb
112      refine Wp.mono (distCont_origin_wp hc A msg m _ (i+1+1) o used locals4 hA ho hAb
113        (by simp only [pullL]; omega) (by simp only [pullL] at bits3 bits4 ⊢; omega)
114        (by simp only [pullL]; omega) (by simp only [pullL]; omega)
115        (by simp only [pullL]; omega) (by simp only [pullL]; omega) origin4) ?_
116      intro l' h' result
117      exact ⟨i+1+1, result⟩
118    · simp only [h2, ite_false]
119      have fits3 : (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1))).op.toNat ≤
120          (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1))).bits.toNat := by
121        have : ¬ ((pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1))).bits.toNat <
122            (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i+1))).op.toNat) :=
123          fun h => h2 (UInt32.lt_iff_toNat_lt.mpr h)
124        omega
125      refine Wp.mono (distCont_origin_wp hc A msg m _ (i+1) o used locals3 hA ho hAb
126        (by simp only [pullL]; omega) fits3 (by simp only [pullL]; omega)
127        (by simp only [pullL]; omega) (by simp only [pullL]; omega)
128        (by simp only [pullL]; omega) origin3) ?_
129      intro l' h' result
130      exact ⟨i+1, result⟩
131  · simp only [h1, ite_false]
132    have fits : l.op.toNat ≤ l.bits.toNat := by
133      have : ¬ (l.bits.toNat < l.op.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
134      omega
135    exact Wp.mono (distCont_origin_wp hc A msg m l i o used hls hA ho hAb hx fits hd1 hd2 hlen hbroke origin)
136      (fun _ _ result => ⟨i, result⟩)
137
138set_option maxHeartbeats 1000000 in
139private theorem dodist_pass_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o d k used : Nat)
140    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
141    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
142    (hhere : l.here = .ref e.rd k) (hk : k < e.DCA.size)
143    (hEb : (e.DCA.getD k default).bits.toNat ≤ l.bits.toNat)
144    (hEd : (e.DCA.getD k default).bits.toNat + d ≤ 15)
145    (hcl : DistClass e (e.DCA.getD k default))
146    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat + d))
147    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
148    Wp (dodist c l) (e.heap A msg m) (fun l' _ =>
149      ∃ i' used', l'.in_ = .ref (.blk e.ib) i' ∧
150        Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
151  have hkE : e.DCA[k]'hk = e.DCA.getD k default := by simp [Array.getD_eq_getD_getElem?, hk]
152  have hld : OkOn (e.heap A msg m) (Ptr.load l.here) (e.DCA.getD k default) := by
153    rw [hhere, ← hkE]; exact Ptr.load_ok (e.heap_cget_DCA A msg m) hk
154  have hEb64 : (((e.DCA.getD k default).bits.toUInt32).toUInt64).toNat = (e.DCA.getD k default).bits.toNat := by
155    simp [toNat32]
156  have hEbn : ((e.DCA.getD k default).bits.toUInt32).toNat = (e.DCA.getD k default).bits.toNat := toNat32 _
157  have hls1 : LS e (dropL l (e.DCA.getD k default).bits.toUInt32) i o :=
158    hls.dropL _ (by omega) (by omega)
159  have hEb64 : (((e.DCA.getD k default).bits.toUInt32).toUInt64).toNat = (e.DCA.getD k default).bits.toNat := by
160    simp [toNat32]
161  have hEbn : ((e.DCA.getD k default).bits.toUInt32).toNat = (e.DCA.getD k default).bits.toNat := toNat32 _
162  have hls1 : LS e (dropL l (e.DCA.getD k default).bits.toUInt32) i o :=
163    hls.dropL _ (by omega) (by omega)
164  have hsg1 := Sg_dropL (e := e) l (e.DCA.getD k default).bits.toUInt32 i (by omega) (by omega)
165  have hlow64 : ∀ x : UInt32, x.toNat < 32 → (l.hold >>> (e.DCA.getD k default).bits.toUInt32.toUInt64).toNat = l.hold.toNat / 2 ^ (e.DCA.getD k default).bits.toNat := by
166    intro x _; rw [u64_shr (by omega), hEbn]
167  have origin1 : Origin.Inv e (dropL l (e.DCA.getD k default).bits.toUInt32).hold.toNat
168      (dropL l (e.DCA.getD k default).bits.toUInt32).bits.toNat i (used + (e.DCA.getD k default).bits.toNat) := by
169    have result := drop_preserves_origin e l.hold.toNat l.bits.toNat i used (e.DCA.getD k default).bits.toNat
170      origin hEb
171    simpa only [dropL_hold l (e.DCA.getD k default).bits.toUInt32 (by rw [hEbn]; omega),
172      dropL_bits l (e.DCA.getD k default).bits.toUInt32 (by rw [hEbn]; exact hEb), hEbn] using result
173  unfold dodist
174  dsimp only
175  refine Wp.bindO hld ?_
176  refine Wp.bindO (shr64_ok (x := l.hold) (by omega)) ?_
177  refine Wp.bindO hld ?_
178  generalize e.DCA.getD k default = E at *
179  have hsg1' : Sg e (l.hold >>> E.bits.toUInt32.toUInt64).toNat (l.bits - E.bits.toUInt32).toNat i =
180      (Sg e l.hold.toNat l.bits.toNat i).drop E.bits.toNat := by
181    have := hsg1; rw [hEbn] at this; exact this
182  by_cases hb16 : (E.op.toUInt32 &&& 16 != 0) = true
183  · simp only [hb16, ite_true]
184    have hb16' : E.op &&& 16 ≠ 0 := by
185      rw [mask16] at hb16; simpa using hb16
186    have hbase : E.op &&& 16 ≠ 0 ∧ ((E.op &&& 15).toNat ≤ 13) ∧ 1 ≤ E.val.toNat := by
187      rcases hcl with h | h | h
188      · exact h
189      · exact absurd h.1 hb16'
190      · exact absurd h.1 hb16'
191    refine Wp.bindO hld ?_
192    have hv : E.val.toUInt32.toNat = E.val.toNat := by simp
193    have hv2 := UInt16.toNat_lt E.val
194    have hbn := dropL_bits l E.bits.toUInt32 (by omega)
195    have key := (dodistBase_origin_wp hc A msg m
196      { in_ := l.in_, out := l.out, hold := l.hold >>> E.bits.toUInt32.toUInt64, bits := l.bits - E.bits.toUInt32,
197        here := l.here, op := E.op.toUInt32 &&& 15, len := l.len, dist := E.val.toUInt32, from_ := l.from_,
198        broke := l.broke, againL := l.againL, againD := false } i o (used + E.bits.toNat) (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb
199      (by rw [mask15]; exact hbase.2.1) (by rw [hv]; exact hbase.2.2) (by rw [hv]; omega) hlen hbroke
200      (by rcases hpull with h | h
201          · exact Or.inl h
202          · refine Or.inr ⟨h.1, ?_⟩
203            show 5 ≤ (l.bits - E.bits.toUInt32).toNat
204            have hbn' : (l.bits - E.bits.toUInt32).toNat = l.bits.toNat - E.bits.toNat := by
205              rw [u32_toNat_sub (by omega), hEbn]
206            omega) origin1)
207    unfold dodistBase distCont at key
208    dsimp only at key
209    refine Wp.mono key ?_
210    intro l' h' result
211    obtain ⟨i', hin, result⟩ := result
212    exact ⟨i', used + E.bits.toNat + (E.op.toUInt32 &&& 15).toNat, hin, result, by omega⟩
213  · -- not a base: a link or an invalid code
214    have hb16' : E.op &&& 16 = 0 := by
215      rw [mask16] at hb16; simpa using hb16
216    by_cases hb64 : (E.op.toUInt32 &&& 64 == 0) = true
217    · simp only [hb16, hb64, ite_true, ite_false, Bool.false_eq_true]
218      have hb64' : E.op &&& 64 = 0 := by
219        rw [mask64] at hb64; simpa using hb64
220      have hlink : 1 ≤ E.op.toNat ∧ E.op.toNat ≤ 15 ∧ e.od + E.val.toNat + 2 ^ E.op.toNat ≤ e.DCA.size := by
221        rcases hcl with h | h | h
222        · exact absurd hb16' h.1
223        · exact ⟨h.2.2.1, h.2.2.2.1, h.2.2.2.2⟩
224        · exact absurd hb64' h.2
225      refine Wp.bindO hld ?_
226      have hdc : c.dcode = .ref e.rd e.od := by rw [hc.dcode]; exact e.hdc
227      have hop32 : E.op.toUInt32.toNat < 32 := by rw [toNat32]; omega
228      refine Wp.bindO (x := Ptr.ref e.rd (e.od + E.val.toNat)) ?_ ?_
229      · rw [hdc]
230        exact Ptr.add_nat_ok (e.heap_cget_DCA A msg m) (Nat.le_trans (Nat.le_add_right _ _) hlink.2.2)
231      refine Wp.bindO (shl32_ok hop32) ?_
232      have hlow := hold_low64 (x := l.hold >>> E.bits.toUInt32.toUInt64) (k := E.op.toUInt32) hop32
233      have hjlt : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat < 2 ^ E.op.toNat := by
234        rw [toNat32]; exact Nat.mod_lt _ (Nat.pow_pos (by omega))
235      generalize hjd : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat = j at hlow hjlt
236      refine Wp.bindO (x := Ptr.ref e.rd (e.od + E.val.toNat + j)) ?_ ?_
237      · rw [hlow]
238        exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rd) (a := e.DCA) (off := e.od + E.val.toNat)
239          (n := j) (e.heap_cget_DCA A msg m) (by have := hlink.2.2; omega)
240      refine Wp.pure' ⟨i, used + E.bits.toNat, hls.hin, origin1, by omega⟩
241    · simp only [hb16, hb64, ite_false, Bool.false_eq_true]
242      obtain ⟨ip, hip⟩ := badData_run hc A msg m "invalid distance code" (by decide +kernel)
243      refine Wp.bindE hip (Wp.pure' ⟨i, used + E.bits.toNat, hls.hin, origin1, by omega⟩)
244
245private theorem origin_at_locals {l : L} {i o input used : Nat}
246    (locals : LS e l i o) (hin : l.in_ = .ref (.blk e.ib) input)
247    (origin : Origin.Inv e l.hold.toNat l.bits.toNat input used) :
248    Origin.Inv e l.hold.toNat l.bits.toNat i used := by
249  have hi : input = i := (Ptr.ref.inj (hin.symm.trans locals.hin)).2
250  simpa only [hi] using origin
251
252private theorem dodistLoop_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
253    (l : L) (i o kidx used : Nat)
254    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat) (hk : kidx < 2 ^ e.s0.distbits.toNat)
255    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size)
256    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hAb : A.size < 2 ^ 63)
257    (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
258    (hhere : l.here = .ref e.rd (e.od + kidx)) (hb15 : 15 ≤ l.bits.toNat)
259    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨
260      (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat))
261    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
262    Wp (cdoWhile (dodist c) (fun l => pure (l.againD, l)) l) (e.heap A msg m) (fun l' _ =>
263      ∃ i' o' used', LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
264  obtain ⟨hksz, hlk, hnl⟩ := distRoot hts kidx hk
265  have hcl0 := distClass_of (e := e) _ hlk hnl
266  have hEd0 : (e.DCA.getD (e.od + kidx) default).bits.toNat + 0 ≤ 15 := by
267    by_cases hl : DistLink (e.DCA.getD (e.od + kidx) default)
268    · have := (hlk hl).1; omega
269    · have := (hnl hl).1; omega
270  obtain ⟨l1, h1, e1, hq1⟩ := dodist_pass hc A msg m l i o 0 (e.od+kidx)
271    hls hA ho hAb hbroke hlen hhere hksz (by omega) hEd0 hcl0 (by simpa using hpull)
272  obtain ⟨input1, used1, hin1, origin1, mono1⟩ := Wp.at_run
273    (dodist_pass_origin_wp hc A msg m l i o 0 (e.od+kidx) used
274      hls hA ho hAb hbroke hlen hhere hksz (by omega) hEd0 hcl0 (by simpa using hpull) origin) e1
275  obtain ⟨E0, hE0⟩ : ∃ E0, e.DCA.getD (e.od+kidx) default = E0 := ⟨_, rfl⟩
276  rw [hE0] at hq1 hlk hnl hcl0 hEd0
277  rcases hq1 with ⟨hag,hbr,hh,⟨hl16,hl64⟩,j,hjlt,hjd,hhere1,hls1,hsg1,hb1,hlen1,hout1,hdist1,hagL1⟩ |
278    ⟨hNL,hag,hend⟩
279  · subst hh
280    have origin1' := origin_at_locals hls1 hin1 origin1
281    have hlink : DistLink E0 := ⟨hl16,hl64⟩
282    have hlk' := hlk hlink
283    have hleaf := hlk'.2.2.2.2 j hjlt
284    have hk2 : e.od + E0.val.toNat + j < e.DCA.size := by have := hlk'.2.2.2.1; omega
285    have hcl1 : DistClass e (e.DCA.getD (e.od + E0.val.toNat + j) default) := by
286      rcases hleaf.2 with h | h
287      · exact Or.inl h
288      · exact Or.inr (Or.inr h)
289    have hb15' : E0.bits.toNat ≤ 15 := hlk'.1
290    obtain ⟨l2,h2,e2,hq2⟩ := dodist_pass hc A msg m l1 i o E0.bits.toNat (e.od+E0.val.toNat+j)
291      hls1 hA ho hAb hbr (by rw [hlen1]; exact hlen) hhere1 hk2
292      (by have := hleaf.1; omega) (by omega) hcl1 (by
293        rcases hpull with h | h
294        · exact Or.inl h
295        · exact Or.inr ⟨h.1,by omega⟩)
296    obtain ⟨input2,used2,hin2,origin2,mono2⟩ := Wp.at_run
297      (dodist_pass_origin_wp hc A msg m l1 i o E0.bits.toNat (e.od+E0.val.toNat+j) used1
298        hls1 hA ho hAb hbr (by rw [hlen1]; exact hlen) hhere1 hk2
299        (by have := hleaf.1; omega) (by omega) hcl1 (by
300          rcases hpull with h | h
301          · exact Or.inl h
302          · exact Or.inr ⟨h.1,by omega⟩) origin1') e2
303    rcases hq2 with ⟨hag2,_,_,⟨hl16',hl64'⟩,_⟩ | hend2
304    · rcases hleaf.2 with h | h
305      · exact absurd hl16' h.1
306      · exact absurd hl64' h.2
307    · have c1 : (fun l : L => (pure (l.againD,l) : M (Bool × L))) l1 (e.heap A msg m) =
308          .ok ((true,l1),e.heap A msg m) := by simp [hag]
309      have c2 : (fun l : L => (pure (l.againD,l) : M (Bool × L))) l2 h2 =
310          .ok ((false,l2),h2) := by simp [hend2.2.1]
311      have e1' : dodist c l (e.heap A msg m) = .ok (l1,e.heap A msg m) := e1
312      refine Wp.of_eq (cdoWhile_two e1' c1 e2 c2) ?_
313      rcases hend2.2.2 with ⟨i',xv,rest,_,_,_,_,locals,_,_⟩ | ⟨i',p,_,_,_,locals,_⟩
314      · exact ⟨i',o+l1.len.toNat,used2,locals,origin_at_locals locals hin2 origin2,by omega⟩
315      · exact ⟨i',o,used2,locals,origin_at_locals locals hin2 origin2,by omega⟩
316  · have c1 : (fun l : L => (pure (l.againD,l) : M (Bool × L))) l1 h1 = .ok ((false,l1),h1) := by simp [hag]
317    refine Wp.of_eq (cdoWhile_one e1 c1) ?_
318    rcases hend with ⟨i',xv,rest,_,_,_,_,locals,_,_⟩ | ⟨i',p,_,_,_,locals,_⟩
319    · exact ⟨i',o+l.len.toNat,used1,locals,origin_at_locals locals hin1 origin1,mono1⟩
320    · exact ⟨i',o,used1,locals,origin_at_locals locals hin1 origin1,mono1⟩
321
322/-- Every actual distance sub-block exit preserves its exact source suffix,
323including invalid-distance and too-far-back errors. -/
324theorem actual_distance_block_preserves_origin : DistanceOrigin.Goal.actual_distance_block_preserves_origin := by
325  intro e c bytes msg mode l i o used hc locals size room big notBroke length enough pullRoom origin
326  have execution : Wp (dolenDist c l) (e.heap bytes msg mode) (fun l' _ =>
327      ∃ i' o' used', LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
328    unfold dolenDist
329    have codePtr : c.dcode = .ref e.rd e.od := by rw [hc.dcode]; exact e.hdc
330    have rootBound : e.s0.distbits.toNat < 32 := by have := e.hdt.1; omega
331    have mask : c.dmask.toUInt64.toNat = 2 ^ e.s0.distbits.toNat - 1 := by
332      rw [hc.dmask,UInt32.toNat_toUInt64]
333      exact u32_shl1_sub1 rootBound
334    have idx := u64_and_mask (x:=l.hold) mask
335    have idxBound : l.hold.toNat % 2 ^ e.s0.distbits.toNat < 2 ^ e.s0.distbits.toNat :=
336      Nat.mod_lt _ (Nat.two_pow_pos _)
337    refine Wp.bindO (x:=Ptr.ref e.rd (e.od+l.hold.toNat%2^e.s0.distbits.toNat)) ?_ ?_
338    · rw [codePtr,idx]
339      exact Ptr.add_nat_ok (e.heap_cget_DCA bytes msg mode) (by have := e.hdt.2.1; omega)
340    · exact dodistLoop_origin_wp hc bytes msg mode
341        {l with here := .ref e.rd (e.od+l.hold.toNat%2^e.s0.distbits.toNat)} i o _ used
342        e.hdt idxBound (LS.congr locals rfl rfl rfl rfl) size room big notBroke length rfl enough pullRoom origin
343  obtain ⟨l',after,run,result⟩ := execution
344  have original := Wp.at_run (dolenDist_wp hc bytes msg mode l i o e.hdt locals size room big notBroke length enough pullRoom) run
345  exact ⟨l',after,run,original,result⟩
346
347end Zlib.Inffast.Proofs