inffast.c.distance-result.lean

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

1import ZlibF.Spec.InflateFastDistanceResult
2import ZlibF.Proof.«inffast.c.match-history»
3import ZlibF.Proof.«inffast.c.distance-semantics»
4import ZlibF.Proof.«inffast.c.advance»
5import ZlibF.Proof.«inffast.c.flags»
6
7/-!
8# Actual distance lookup, extra bits and independent match copying
9
10The source proves the three physical exits before table semantics classify
11its selected symbol. Copy failures retain the exact stream after extras.
12-/
13
14set_option autoImplicit false
15
16namespace Zlib.Inffast.Proofs
17open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
18open Zlib.Inffast.Spec.DistanceResult ZlibF.Math.LZ77Copy
19open Zlib.Inftrees.Spec Zlib.Inftrees.Spec.DecodeSemantics
20variable {e : Env} {c : Ctx}
21
22private theorem copy_result_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
23    (l : L) (i o : Nat) (hls : LS e l i o)
24    (hbg : e.bg ≤ o) (hop : l.op.toNat = o-e.bg)
25    (hd : 1 ≤ l.dist.toNat) (hlen : 3 ≤ l.len.toNat)
26    (hroom : o+l.len.toNat ≤ A.size) (hbroke : l.broke = false) :
27    Wp (copyMatch c l) (e.heap A msg m) (fun l' after =>
28      CopyOutcome e A msg m (Sg e l.hold.toNat l.bits.toNat i) o l.len.toNat l.dist.toNat l' after) := by
29  have copy := actual_copy_match_refines_lz77 e c A msg m l o hc hls.hout hbg hop hd hlen hroom hbroke
30  dsimp only at copy
31  unfold CopyOutcome
32  by_cases far :
33      (MatchHistory.saved e.W e.s0.wsize.toNat e.s0.wnext.toNat e.s0.whave.toNat e.woff).length +
34        (writtenBytes A o (o-e.bg)).length < l.dist.toNat
35  · simp only [far,ite_true] at copy ⊢
36    obtain ⟨l',after,p,run,hin,hold,bits,againL,againD,broke,hout,heap⟩ := copy
37    refine ⟨l',after,run,i,p,broke,?_,?_,heap⟩
38    · exact hls.congr hin hout hold bits
39    · simp only [hold,bits]
40  · simp only [far,ite_false] at copy ⊢
41    obtain ⟨l',after,run,hin,hold,bits,againL,againD,broke,hout,heap,meaning⟩ := copy
42    refine ⟨l',after,run,i,broke,?_,?_,heap,meaning⟩
43    · exact ⟨hin.trans hls.hin,hout,hls.hi0,hls.hi1,by have := hls.ho0; omega,
44        by rw [bits]; exact hls.hb,by rw [hold,bits]; exact hls.hH,by rw [bits]; exact hls.hacc⟩
45    · simp only [hold,bits]
46
47private theorem distCont_result_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o : Nat)
48    (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)
49    (hAb : A.size < 2 ^ 63)
50    (hx : l.op.toNat ≤ 13) (hxb : l.op.toNat ≤ l.bits.toNat) (hd1 : 1 ≤ l.dist.toNat) (hd2 : l.dist.toNat ≤ 65536)
51    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258) (hbroke : l.broke = false) :
52    Wp (distCont c l) (e.heap A msg m) (fun l' after =>
53      ∃ extra rest, readBits l.op.toNat (Sg e l.hold.toNat l.bits.toNat i) = some (extra,rest) ∧
54        CopyOutcome e A msg m rest o l.len.toNat (l.dist.toNat+extra) l' after) := by
55  have hbgo : e.bg ≤ o := by have := e.bg_le; have := hls.ho0; omega
56  have hoA : o ≤ A.size := by omega
57  have hxs : l.op.toNat < 32 := by omega
58  unfold distCont
59  refine Wp.bindO (shl32_ok hxs) ?_
60  dsimp only
61  have hlow := hold_low32 (x := l.hold) (k := l.op) hxs
62  have hlowlt : l.hold.toNat % 2 ^ l.op.toNat < 2 ^ l.op.toNat := Nat.mod_lt _ (Nat.pow_pos (by omega))
63  have hpow : 2 ^ l.op.toNat ≤ 2 ^ 13 := Nat.pow_le_pow_right (by omega) hx
64  have hdist' : (l.dist + (l.hold.toUInt32 &&& (1 <<< l.op) - 1)).toNat = l.dist.toNat + l.hold.toNat % 2 ^ l.op.toNat := by
65    rw [u32_toNat_add (by rw [hlow]; omega), hlow]
66  refine Wp.bindO (shr64_ok (x := l.hold) (n := l.op.toUInt64) (by rw [UInt32.toNat_toUInt64]; omega)) ?_
67  have hbgdef : e.bg = e.o0 - (e.start.toNat - e.sm0.avail_out.toNat) := rfl
68  have hst32 := UInt32.toNat_lt e.start
69  have hstart := e.hstart
70  have hbeg := e.hbeg
71  have hdiff : OkOn (e.heap A msg m) (Ptr.diff l.out c.beg) (Int64.ofInt (((o - e.bg : Nat)) : Int)) := by
72    rw [hls.hout, hc.beg]
73    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)
74      ⟨by omega, by omega⟩
75    have e1 : (o : Int) - (e.bg : Int) = ((o - e.bg : Nat) : Int) := by omega
76    rw [e1] at this
77    exact this
78  refine Wp.bindO hdiff ?_
79  have hopn : (Int64.ofInt (((o - e.bg : Nat)) : Int)).toUInt64.toUInt32.toNat = o - e.bg := i64_toU32 _ (by omega)
80  have hls1 : LS e (dropL l l.op) i o := hls.dropL l.op hxb (by omega)
81  have hrb := readBits_bitsOfNat l.op.toNat l.bits.toNat l.hold.toNat (inBits e i) hxb
82  have hsg := Sg_dropL (e := e) l l.op i hxb (by omega)
83  refine Wp.mono (copy_result_wp (e:=e) (c:=c) hc A msg m
84    { in_ := l.in_, out := l.out, hold := l.hold >>> l.op.toUInt64, bits := l.bits-l.op, here := l.here,
85      op := (Int64.ofInt (((o-e.bg : Nat)) : Int)).toUInt64.toUInt32, len := l.len,
86      dist := l.dist + (l.hold.toUInt32 &&& 1 <<< l.op - 1), from_ := l.from_, broke := l.broke,
87      againL := l.againL, againD := l.againD }
88    i o (LS.congr hls1 rfl rfl rfl rfl) hbgo hopn
89    (by simp only [hdist']; omega) hlen.1 (by simp only []; omega) hbroke) ?_
90  intro l' after copy
91  refine ⟨l.hold.toNat % 2^l.op.toNat,Sg e (dropL l l.op).hold.toNat (dropL l l.op).bits.toNat i,?_,?_⟩
92  · unfold Sg
93    rw [hrb,dropL_hold l l.op (by omega),dropL_bits l l.op hxb]
94  · simpa only [dropL,hdist'] using copy
95
96private theorem dodistBase_result_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o : Nat)
97    (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)
98    (hAb : A.size < 2 ^ 63) (hx : l.op.toNat ≤ 13) (hd1 : 1 ≤ l.dist.toNat) (hd2 : l.dist.toNat ≤ 65536)
99    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258) (hbroke : l.broke = false)
100    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 5 ≤ l.bits.toNat)) :
101    Wp (dodistBase c l) (e.heap A msg m) (fun l' after =>
102      ∃ extra rest, readBits l.op.toNat (Sg e l.hold.toNat l.bits.toNat i) = some (extra,rest) ∧
103        CopyOutcome e A msg m rest o l.len.toNat (l.dist.toNat+extra) l' after) := by
104  unfold dodistBase
105  by_cases h1 : l.bits < l.op
106  · simp only [h1, ite_true]
107    have h1' : l.bits.toNat < l.op.toNat := UInt32.lt_iff_toNat_lt.mp h1
108    have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
109    refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
110    have hl3 := hls.pullL (by omega) hiin
111    have hs3 := Sg_pullL hls (by omega) hiin
112    have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
113    by_cases h2 : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits <
114        (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).op
115    · simp only [h2, ite_true]
116      have h2' : l.bits.toNat + 8 < l.op.toNat := by
117        have := UInt32.lt_iff_toNat_lt.mp h2
118        simp only [pullL] at this hb3 ⊢
119        omega
120      have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
121      have hb3' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by omega
122      refine Wp.bindO (pull_run e _ _ (i + 1) o hl3 hb3' hi2 (e.heap_bytes_in A msg m)) ?_
123      have hl4 := hl3.pullL hb3' hi2
124      have hs4 := Sg_pullL hl3 hb3' hi2
125      have hb4 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (e.IN.getD (i + 1) 0)
126        (.ref (BRef.blk e.ib) (i + 1 + 1)) hl3.hb
127      refine Wp.mono (distCont_result_wp hc A msg m _ (i + 1 + 1) o hl4 hA ho hAb (by simp only [pullL]; omega)
128        (by simp only [pullL] at hb3 hb4 ⊢; omega) (by simp only [pullL]; omega) (by simp only [pullL]; omega)
129        (by simp only [pullL]; omega) (by simp only [pullL]; omega)) ?_
130      intro l' h' hq
131      obtain ⟨extra,rest,read,copy⟩ := hq
132      refine ⟨extra,rest,?_,copy⟩
133      simp only [pullL] at read hs4 hs3 ⊢
134      rw [hs4,hs3] at read
135      exact read
136    · simp only [h2, ite_false]
137      have h2n : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).op.toNat ≤
138          (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat := by
139        have : ¬ ((pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat <
140            (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).op.toNat) :=
141          fun h => h2 (UInt32.lt_iff_toNat_lt.mpr h)
142        omega
143      refine Wp.mono (distCont_result_wp hc A msg m _ (i + 1) o hl3 hA ho hAb (by simp only [pullL]; omega)
144        h2n (by simp only [pullL]; omega) (by simp only [pullL]; omega)
145        (by simp only [pullL]; omega) (by simp only [pullL]; omega)) ?_
146      intro l' h' hq
147      obtain ⟨extra,rest,read,copy⟩ := hq
148      refine ⟨extra,rest,?_,copy⟩
149      simp only [pullL] at read hs3 ⊢
150      rw [hs3] at read
151      exact read
152  · simp only [h1, ite_false]
153    have h1' : l.op.toNat ≤ l.bits.toNat := by
154      have : ¬ (l.bits.toNat < l.op.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
155      omega
156    refine Wp.mono (distCont_result_wp hc A msg m l i o hls hA ho hAb hx h1' hd1 hd2 hlen hbroke) ?_
157    intro l' h' hq
158    exact hq
159
160set_option maxHeartbeats 1000000 in
161private theorem dodist_result_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o d k : Nat)
162    (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)
163    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
164    (hhere : l.here = .ref e.rd k) (hk : k < e.DCA.size)
165    (hEb : (e.DCA.getD k default).bits.toNat ≤ l.bits.toNat)
166    (hEd : (e.DCA.getD k default).bits.toNat + d ≤ 15)
167    (hcl : DistClass e (e.DCA.getD k default))
168    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat + d)) :
169    Wp (dodist c l) (e.heap A msg m) (fun l' after =>
170      l'.againD = true ∨
171        PhysicalOutcome e A msg m (Sg e l.hold.toNat l.bits.toNat i) o l.len.toNat
172          (e.DCA.getD k default) (e.DCA.getD k default).bits.toNat l' after) := by
173  have hkE : e.DCA[k]'hk = e.DCA.getD k default := by simp [Array.getD_eq_getD_getElem?, hk]
174  have hld : OkOn (e.heap A msg m) (Ptr.load l.here) (e.DCA.getD k default) := by
175    rw [hhere, ← hkE]; exact Ptr.load_ok (e.heap_cget_DCA A msg m) hk
176  have hEb64 : (((e.DCA.getD k default).bits.toUInt32).toUInt64).toNat = (e.DCA.getD k default).bits.toNat := by
177    simp [toNat32]
178  have hEbn : ((e.DCA.getD k default).bits.toUInt32).toNat = (e.DCA.getD k default).bits.toNat := toNat32 _
179  have hls1 : LS e (dropL l (e.DCA.getD k default).bits.toUInt32) i o :=
180    hls.dropL _ (by omega) (by omega)
181  have hEb64 : (((e.DCA.getD k default).bits.toUInt32).toUInt64).toNat = (e.DCA.getD k default).bits.toNat := by
182    simp [toNat32]
183  have hEbn : ((e.DCA.getD k default).bits.toUInt32).toNat = (e.DCA.getD k default).bits.toNat := toNat32 _
184  have hls1 : LS e (dropL l (e.DCA.getD k default).bits.toUInt32) i o :=
185    hls.dropL _ (by omega) (by omega)
186  have hsg1 := Sg_dropL (e := e) l (e.DCA.getD k default).bits.toUInt32 i (by omega) (by omega)
187  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
188    intro x _; rw [u64_shr (by omega), hEbn]
189  rw [dodist_eq_base]
190  dsimp only
191  refine Wp.bindO hld ?_
192  refine Wp.bindO (shr64_ok (x:=l.hold)
193    (n:=(e.DCA.getD k default).bits.toUInt32.toUInt64) (by rw [UInt32.toNat_toUInt64,hEbn]; omega)) ?_
194  refine Wp.bindO hld ?_
195  generalize e.DCA.getD k default = E at *
196  have hsg1' : Sg e (l.hold >>> E.bits.toUInt32.toUInt64).toNat (l.bits - E.bits.toUInt32).toNat i =
197      (Sg e l.hold.toNat l.bits.toNat i).drop E.bits.toNat := by
198    have := hsg1; rw [hEbn] at this; exact this
199  by_cases hb16 : (E.op.toUInt32 &&& 16 != 0) = true
200  · simp only [hb16, ite_true]
201    have hb16' : E.op &&& 16 ≠ 0 := by
202      rw [mask16] at hb16; simpa using hb16
203    have hbase : E.op &&& 16 ≠ 0 ∧ ((E.op &&& 15).toNat ≤ 13) ∧ 1 ≤ E.val.toNat := by
204      rcases hcl with h | h | h
205      · exact h
206      · exact absurd h.1 hb16'
207      · exact absurd h.1 hb16'
208    refine Wp.bindO hld ?_
209    have hv : E.val.toUInt32.toNat = E.val.toNat := by simp
210    have hv2 := UInt16.toNat_lt E.val
211    have hbn := dropL_bits l E.bits.toUInt32 (by omega)
212    have key := (dodistBase_result_wp hc A msg m
213      { in_ := l.in_, out := l.out, hold := l.hold >>> E.bits.toUInt32.toUInt64, bits := l.bits - E.bits.toUInt32,
214        here := l.here, op := E.op.toUInt32 &&& 15, len := l.len, dist := E.val.toUInt32, from_ := l.from_,
215        broke := l.broke, againL := l.againL, againD := false } i o (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb
216      (by rw [mask15]; exact hbase.2.1) (by rw [hv]; exact hbase.2.2) (by rw [hv]; omega) hlen hbroke
217      (by rcases hpull with h | h
218          · exact Or.inl h
219          · refine Or.inr ⟨h.1, ?_⟩
220            show 5 ≤ (l.bits - E.bits.toUInt32).toNat
221            have hbn' : (l.bits - E.bits.toUInt32).toNat = l.bits.toNat - E.bits.toNat := by
222              rw [u32_toNat_sub (by omega), hEbn]
223            omega))
224    refine Wp.mono key ?_
225    intro l' after result
226    obtain ⟨extra,rest,read,copy⟩ := result
227    right; right
228    refine ⟨hb16',extra,rest,?_,?_⟩
229    · rw [mask15,hsg1'] at read
230      exact read
231    · simpa only [hv] using copy
232  · -- not a base: a link or an invalid code
233    have hb16' : E.op &&& 16 = 0 := by
234      rw [mask16] at hb16; simpa using hb16
235    by_cases hb64 : (E.op.toUInt32 &&& 64 == 0) = true
236    · simp only [hb16, hb64, ite_true, ite_false, Bool.false_eq_true]
237      have hb64' : E.op &&& 64 = 0 := by
238        rw [mask64] at hb64; simpa using hb64
239      have hlink : 1 ≤ E.op.toNat ∧ E.op.toNat ≤ 15 ∧ e.od + E.val.toNat + 2 ^ E.op.toNat ≤ e.DCA.size := by
240        rcases hcl with h | h | h
241        · exact absurd hb16' h.1
242        · exact ⟨h.2.2.1, h.2.2.2.1, h.2.2.2.2⟩
243        · exact absurd hb64' h.2
244      refine Wp.bindO hld ?_
245      have hdc : c.dcode = .ref e.rd e.od := by rw [hc.dcode]; exact e.hdc
246      have hop32 : E.op.toUInt32.toNat < 32 := by rw [toNat32]; omega
247      refine Wp.bindO (x := Ptr.ref e.rd (e.od + E.val.toNat)) ?_ ?_
248      · rw [hdc]
249        exact Ptr.add_nat_ok (e.heap_cget_DCA A msg m) (Nat.le_trans (Nat.le_add_right _ _) hlink.2.2)
250      refine Wp.bindO (shl32_ok hop32) ?_
251      have hlow := hold_low64 (x := l.hold >>> E.bits.toUInt32.toUInt64) (k := E.op.toUInt32) hop32
252      have hjlt : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat < 2 ^ E.op.toNat := by
253        rw [toNat32]; exact Nat.mod_lt _ (Nat.pow_pos (by omega))
254      generalize hjd : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat = j at hlow hjlt
255      refine Wp.bindO (x := Ptr.ref e.rd (e.od + E.val.toNat + j)) ?_ ?_
256      · rw [hlow]
257        exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rd) (a := e.DCA) (off := e.od + E.val.toNat)
258          (n := j) (e.heap_cget_DCA A msg m) (by have := hlink.2.2; omega)
259      exact Wp.pure' (Or.inl rfl)
260    · simp only [hb16, hb64, ite_false, Bool.false_eq_true]
261      obtain ⟨ip, hip⟩ := badData_run hc A msg m "invalid distance code" (by decide +kernel)
262      refine Wp.bindE hip (Wp.pure' (Or.inr (Or.inl ⟨hb16',i,Ptr.ref (.str ip) 0,rfl,
263        LS.congr hls1 rfl rfl rfl rfl,hsg1',rfl⟩)))
264
265private theorem dodistLoop_result_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o kidx : Nat)
266    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat) (hk : kidx < 2 ^ e.s0.distbits.toNat)
267    (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)
268    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
269    (hhere : l.here = .ref e.rd (e.od + kidx)) (hb15 : 15 ≤ l.bits.toNat)
270    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat)) :
271    Wp (cdoWhile (dodist c) (fun l => pure (l.againD, l)) l) (e.heap A msg m) (fun l' h' =>
272      ∃ E cb, cb ≤ 15 ∧ DistLook e l.hold.toNat kidx E cb ∧
273        DistEnd e A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop cb) i o l.len.toNat E l' h' ∧
274        PhysicalOutcome e A msg m (Sg e l.hold.toNat l.bits.toNat i) o l.len.toNat E cb l' h') := by
275  obtain ⟨hksz, hlk, hnl⟩ := distRoot hts kidx hk
276  have hcl0 := distClass_of (e := e) _ hlk hnl
277  have hEd0 : (e.DCA.getD (e.od + kidx) default).bits.toNat + 0 ≤ 15 := by
278    by_cases hl : DistLink (e.DCA.getD (e.od + kidx) default)
279    · have := (hlk hl).1; omega
280    · have := (hnl hl).1; omega
281  obtain ⟨l1, h1, e1, hq1⟩ := dodist_pass hc A msg m l i o 0 (e.od + kidx) hls hA ho hAb hbroke hlen hhere hksz
282    (by omega) hEd0 hcl0 (by simpa using hpull)
283  obtain ⟨E0, hE0⟩ : ∃ E0, e.DCA.getD (e.od + kidx) default = E0 := ⟨_, rfl⟩
284  rw [hE0] at hq1 hlk hnl hcl0 hEd0
285  rcases hq1 with ⟨hag, hbr, hh, ⟨hl16, hl64⟩, j, hjlt, hjd, hhere1, hls1, hsg1, hb1, hlen1, hout1, hdist1, hagL1⟩ | ⟨hNL, hag, hend⟩
286  · -- a link: the second pass ends the block
287    subst hh
288    have hlink : DistLink E0 := ⟨hl16, hl64⟩
289    have hlk' := hlk hlink
290    have hleaf := hlk'.2.2.2.2 j hjlt
291    have hk2 : e.od + E0.val.toNat + j < e.DCA.size := by
292      have := hlk'.2.2.2.1; omega
293    have hcl1 : DistClass e (e.DCA.getD (e.od + E0.val.toNat + j) default) := by
294      rcases hleaf.2 with h | h
295      · exact Or.inl h
296      · exact Or.inr (Or.inr h)
297    have hb15' : E0.bits.toNat ≤ 15 := hlk'.1
298    obtain ⟨l2, h2, e2, hq2⟩ := dodist_pass hc A msg m l1 i o E0.bits.toNat (e.od + E0.val.toNat + j) hls1 hA ho hAb hbr
299      (by rw [hlen1]; exact hlen) hhere1 hk2 (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⟩)
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 physical := Wp.at_run (dodist_result_wp hc A msg m l1 i o E0.bits.toNat
308          (e.od+E0.val.toNat+j) hls1 hA ho hAb hbr (by rw [hlen1]; exact hlen) hhere1 hk2
309          (by have := hleaf.1; omega) (by omega) hcl1 (by
310            rcases hpull with h | h
311            · exact Or.inl h
312            · exact Or.inr ⟨h.1,by omega⟩)) e2
313      have physical' : PhysicalOutcome e A msg m (Sg e l1.hold.toNat l1.bits.toNat i) o l1.len.toNat
314          (e.DCA.getD (e.od+E0.val.toNat+j) default)
315          (e.DCA.getD (e.od+E0.val.toNat+j) default).bits.toNat l2 h2 := by
316        rcases physical with flag | result
317        · rw [hend2.2.1] at flag; contradiction
318        · exact result
319      have c1 : (fun l : L => (pure (l.againD, l) : M (Bool × L))) l1 (e.heap A msg m) = .ok ((true, l1), e.heap A msg m) := by simp [hag]
320      have c2 : (fun l : L => (pure (l.againD, l) : M (Bool × L))) l2 h2 = .ok ((false, l2), h2) := by simp [hend2.2.1]
321      have e1' : dodist c l (e.heap A msg m) = .ok (l1, e.heap A msg m) := e1
322      refine Wp.of_eq (cdoWhile_two e1' c1 e2 c2) ?_
323      refine ⟨e.DCA.getD (e.od + E0.val.toNat + j) default, E0.bits.toNat + (e.DCA.getD (e.od + E0.val.toNat + j) default).bits.toNat, by have := hleaf.1; omega, ?_, ?_, ?_⟩
324      · refine Or.inr ⟨E0, j, hE0, hlink, hjlt, ?_, rfl, rfl, by have := hleaf.1; omega, ?_⟩
325        · rw [hjd]
326        · intro hl; rcases hleaf.2 with h | h
327          · exact absurd hl.1 h.1
328          · exact absurd hl.2 h.2
329      · have := hend2
330        rw [hlen1] at this
331        have hd : (Sg e l.hold.toNat l.bits.toNat i).drop (E0.bits.toNat + (e.DCA.getD (e.od + E0.val.toNat + j) default).bits.toNat) =
332            ((Sg e l.hold.toNat l.bits.toNat i).drop E0.bits.toNat).drop (e.DCA.getD (e.od + E0.val.toNat + j) default).bits.toNat := by
333          rw [List.drop_drop]
334        rw [hd, ← hsg1]
335        exact this
336      · simpa only [PhysicalOutcome,hlen1,hsg1,List.drop_drop] using physical'
337  · -- the first pass ended the block
338    have c1 : (fun l : L => (pure (l.againD, l) : M (Bool × L))) l1 h1 = .ok ((false, l1), h1) := by simp [hag]
339    have physical := Wp.at_run (dodist_result_wp hc A msg m l i o 0 (e.od+kidx)
340      hls hA ho hAb hbroke hlen hhere hksz (by rw [hE0]; omega) (by rw [hE0]; exact hEd0)
341      (by rw [hE0]; exact hcl0) (by simpa using hpull)) e1
342    rw [hE0] at physical
343    have physical' : PhysicalOutcome e A msg m (Sg e l.hold.toNat l.bits.toNat i) o l.len.toNat E0 E0.bits.toNat l1 h1 := by
344      rcases physical with flag | result
345      · rw [hag] at flag; contradiction
346      · exact result
347    refine Wp.of_eq (cdoWhile_one e1 c1) ?_
348    exact ⟨E0,E0.bits.toNat,by omega,Or.inl ⟨hE0,rfl,hNL⟩,⟨hNL,hag,hend⟩,physical'⟩
349private theorem dolenDist_result_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o : Nat)
350    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
351    (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)
352    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
353    (hb15 : 15 ≤ l.bits.toNat)
354    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat)) :
355    Wp (dolenDist c l) (e.heap A msg m) (fun l' h' =>
356      ∃ E cb, cb ≤ 15 ∧ DistLook e l.hold.toNat (l.hold.toNat % 2 ^ e.s0.distbits.toNat) E cb ∧
357        DistEnd e A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop cb) i o l.len.toNat E l' h' ∧
358        PhysicalOutcome e A msg m (Sg e l.hold.toNat l.bits.toNat i) o l.len.toNat E cb l' h') := by
359  unfold dolenDist
360  have hdc : c.dcode = .ref e.rd e.od := by rw [hc.dcode]; exact e.hdc
361  have hR : e.s0.distbits.toNat < 32 := by have := hts.1; omega
362  have hmask : c.dmask.toUInt64.toNat = 2 ^ e.s0.distbits.toNat - 1 := by
363    rw [hc.dmask, UInt32.toNat_toUInt64]; exact u32_shl1_sub1 hR
364  have hidx := u64_and_mask (x := l.hold) hmask
365  have hmod : l.hold.toNat % 2 ^ e.s0.distbits.toNat < 2 ^ e.s0.distbits.toNat :=
366    Nat.mod_lt _ (Nat.pow_pos (by omega))
367  refine Wp.bindO (x := Ptr.ref e.rd (e.od + l.hold.toNat % 2 ^ e.s0.distbits.toNat)) ?_ ?_
368  · rw [hdc, hidx]
369    exact Ptr.add_nat_ok (e.heap_cget_DCA A msg m) (by have := hts.2.1; omega)
370  · exact Wp.mono (dodistLoop_result_wp hc A msg m { l with here := Ptr.ref e.rd (e.od + l.hold.toNat % 2 ^ e.s0.distbits.toNat) }
371      i o _ hts hmod (LS.congr hls rfl rfl rfl rfl) hA ho hAb hbroke hlen rfl hb15 hpull) (fun _ _ h => h)
372private theorem distance_extra_limit : ∀ k, k < 30 → distExtras.getD k 0 ≤ 13 := by
373  decide +kernel
374
375private theorem distance_extra_mask : ∀ op : UInt8, 16 ≤ op.toNat → op.toNat ≤ 29 →
376    (op &&& 15).toNat = op.toNat-16 := by
377  apply u8_forall
378  decide +kernel
379
380/-- The actual complete distance block selects an independent symbol and
381copies the independent match, or retains its exact input on either error. -/
382theorem actual_distance_refines_lz77 : Goal.actual_distance_refines_lz77 := by
383  intro e c bytes msg mode l input output tableUsed lens ctx locals size room big notBroke len enough pullRoom inv stable flags
384  obtain ⟨l',after,run,entry,consumed,bound,look,old,physical⟩ :=
385    dolenDist_result_wp ctx bytes msg mode l input output e.hdt locals size room big notBroke len enough pullRoom
386  refine ⟨l',after,entry,consumed,run,bound,look,old,?_⟩
387  obtain ⟨query,positive,limit,leaf,meaning⟩ := distance_lookup_matches_format e l.hold.toNat
388    l.bits.toNat input tableUsed lens entry consumed inv stable flags locals.hH enough look
389  unfold Outcome
390  dsimp only
391  rcases meaning with ⟨noBase,future⟩ | ⟨hasBase,symbol,valid,symbolEntry,codeLength,decoded,extended⟩
392  · rcases physical with ⟨_,bad⟩ | ⟨hasBase,_⟩
393    · exact Or.inl ⟨noBase,future,bad⟩
394    · exact False.elim (hasBase noBase)
395  · rcases physical with ⟨noBase,_⟩ | ⟨_,extra,rest,read,copy⟩
396    · exact False.elim (hasBase noBase)
397    · have entryMeaning := symbolEntry
398      unfold SymbolEntry at entryMeaning
399      simp only [show DISTS ≠ LENS by decide,ite_false,valid,ite_true] at entryMeaning
400      obtain ⟨opValue,baseValue⟩ := entryMeaning
401      have extraBound := distance_extra_limit symbol (by omega)
402      have mask := distance_extra_mask entry.op (by omega) (by omega)
403      have extraValue : (entry.op &&& 15).toNat = distExtras.getD symbol 0 := by
404        rw [mask]
405        omega
406      right
407      refine ⟨hasBase,symbol,extra,(Sg e l.hold.toNat l.bits.toNat input).drop consumed,rest,
408        valid,symbolEntry,codeLength,decoded,?_,?_⟩
409      · rw [extraValue] at read
410        exact read
411      · simpa only [CopyOutcome,baseValue] using copy
412
413end Zlib.Inffast.Proofs