inffast.c.body-origin.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.InflateFastBodyOrigin
2import ZlibF.Proof.«inffast.c.origin»
3import ZlibF.Proof.«inffast.c.body»
4import ZlibF.Proof.«inffast.c.distance-origin»
5
6/-!
7# The actual fast body preserves its source-bit origin
8
9Every source refill and drop updates the exact suffix invariant. Copying
10and control fields preserve the buffered bits. No decoding-table semantic
11contract is assumed; the existing table safety domain is retained.
12-/
13
14namespace Zlib.Inffast.Proofs.BodyOriginProof
15open C Zlib.Inffast Zlib.Inffast.Spec Zlib.Inffast.Proofs ZlibF.Spec
16
17variable {e : Env} {c : Ctx}
18
19private theorem pull_origin {l : L} {i o used : Nat}
20    (hl : LS e l i o) (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used)
21    (buffer : l.bits.toNat ≤ 22) (available : i < e.i0 + e.sm0.avail_in.toNat) :
22    Origin.Inv e (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1))).hold.toNat
23      (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1))).bits.toNat (i + 1) used := by
24  have next := pull_preserves_origin e l.hold.toNat l.bits.toNat i used origin available
25  simpa only [pullL_hold l _ _ hl.hb hl.hH, pullL_bits l _ _ hl.hb] using next
26
27private theorem drop_origin {l : L} {i o used : Nat} (count : UInt32)
28    (hl : LS e l i o) (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used)
29    (available : count.toNat ≤ l.bits.toNat) :
30    Origin.Inv e (dropL l count).hold.toNat (dropL l count).bits.toNat i (used + count.toNat) := by
31  exact (actual_drop_preserves_origin e e.h0 l i o used count hl origin available).2.2
32
33private theorem refill_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s used : Nat)
34    (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)
35    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
36    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 3) (hT3 : i = s + 3 → 4 ≤ l.bits.toNat)
37    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
38    Wp (dolenRefill c l) (e.heap A msg m) (fun l' _ =>
39      ∃ i' o' used', LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
40  unfold dolenRefill
41  by_cases h1 : l.bits < 15
42  · simp only [h1, ite_true]
43    have h1' : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp h1
44    have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
45    refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
46    have hl3 := hls.pullL (by omega) hiin
47    have origin3 := pull_origin hls origin (by omega) hiin
48    have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
49    have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
50    have hb3' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
51      simp only [pullL] at hb3 ⊢; omega
52    refine Wp.bindO (pull_run e _ _ (i + 1) o hl3 hb3' hi2 (e.heap_bytes_in A msg m)) ?_
53    have hl4 := hl3.pullL hb3' hi2
54    have origin4 := pull_origin hl3 origin3 hb3' hi2
55    have hb4 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (e.IN.getD (i + 1) 0)
56      (.ref (BRef.blk e.ib) (i + 1 + 1)) hl3.hb
57    simp only [pullL] at hb3 hb4
58    obtain ⟨lr, hr, run, _, endOrigin⟩ := actual_distance_block_preserves_origin e c A msg m _ (i + 1 + 1) o used
59      hc hl4 hA ho hAb hbroke hlen (by simp only [pullL]; omega) (by
60        by_cases hc3 : i = s + 3
61        · right; have := hT3 hc3; simp only [pullL]; omega
62        · left; omega) origin4
63    exact Wp.of_eq run endOrigin
64  · simp only [h1, ite_false]
65    have h1' : 15 ≤ l.bits.toNat := by
66      have : ¬ (l.bits.toNat < 15) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
67      omega
68    obtain ⟨lr, hr, run, _, endOrigin⟩ := actual_distance_block_preserves_origin e c A msg m l i o used
69      hc hls hA ho hAb hbroke hlen h1' (Or.inl (by omega)) origin
70    exact Wp.of_eq run endOrigin
71
72private theorem ext_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s used : Nat)
73    (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)
74    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hx : l.op.toNat ≤ 5) (hxb : l.op.toNat ≤ l.bits.toNat)
75    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
76    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 3) (hT3 : i = s + 3 → 4 + l.op.toNat ≤ l.bits.toNat)
77    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
78    Wp (dolenExt c l) (e.heap A msg m) (fun l' _ =>
79      ∃ i' o' used', LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
80  unfold dolenExt
81  have hxs : l.op.toNat < 32 := by omega
82  refine Wp.bindO (shl32_ok hxs) ?_
83  dsimp only
84  have hlow := hold_low32 (x := l.hold) (k := l.op) hxs
85  have hlowlt : l.hold.toNat % 2 ^ l.op.toNat < 2 ^ l.op.toNat := Nat.mod_lt _ (Nat.pow_pos (by omega))
86  have hpow : 0 < 2 ^ l.op.toNat := Nat.pow_pos (by omega)
87  have hlen' : (l.len + (l.hold.toUInt32 &&& (1 <<< l.op) - 1)).toNat = l.len.toNat + l.hold.toNat % 2 ^ l.op.toNat := by
88    rw [u32_toNat_add (by rw [hlow]; omega), hlow]
89  refine Wp.bindO (shr64_ok (x := l.hold) (n := l.op.toUInt64) (by rw [UInt32.toNat_toUInt64]; omega)) ?_
90  have hls1 : LS e (dropL l l.op) i o := hls.dropL l.op hxb (by omega)
91  have origin1 := drop_origin l.op hls origin hxb
92  have hbn := dropL_bits l l.op hxb
93  refine Wp.mono (refill_origin_wp hc A msg m
94    { in_ := l.in_, out := l.out, hold := l.hold >>> l.op.toUInt64, bits := l.bits - l.op, here := l.here, op := l.op,
95      len := l.len + (l.hold.toUInt32 &&& (1 <<< l.op) - 1), dist := l.dist, from_ := l.from_, broke := l.broke,
96      againL := l.againL, againD := l.againD } i o s (used + l.op.toNat) (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb hbroke
97    (by rw [hlen']; omega) hs6 hT (by intro h3; have := hT3 h3; show 4 ≤ (l.bits - l.op).toNat; simp only [dropL] at hbn; omega)
98    origin1) ?_
99  intro l' h' result
100  obtain ⟨i', o', used', locals, finalOrigin, mono⟩ := result
101  exact ⟨i', o', used', locals, finalOrigin, by omega⟩
102
103private theorem len_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s used : Nat)
104    (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)
105    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hx : l.op.toNat ≤ 5)
106    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
107    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 2) (hb2 : i = s + 2 → 1 ≤ l.bits.toNat)
108    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
109    Wp (dolenLen c l) (e.heap A msg m) (fun l' _ =>
110      ∃ i' o' used', LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
111  unfold dolenLen
112  by_cases h0 : l.op != 0
113  · simp only [h0, ite_true]
114    have h0' : l.op.toNat ≠ 0 := by
115      intro h; apply (by simpa using h0 : l.op ≠ 0); exact UInt32.toNat_inj.mp (by simpa using h)
116    by_cases h1 : l.bits < l.op
117    · simp only [h1, ite_true]
118      have h1' : l.bits.toNat < l.op.toNat := UInt32.lt_iff_toNat_lt.mp h1
119      have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
120      refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
121      have hl3 := hls.pullL (by omega) hiin
122      have origin3 := pull_origin hls origin (by omega) hiin
123      have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
124      exact ext_origin_wp hc A msg m _ (i + 1) o s used hl3 hA ho hAb hbroke (by simp only [pullL]; omega)
125        (by simp only [pullL] at hb3 ⊢; omega) (by simp only [pullL]; omega) hs6 (by omega)
126        (by intro h3; simp only [pullL] at hb3 ⊢; have := hb2 (by omega); omega) origin3
127    · simp only [h1, ite_false]
128      have h1' : l.op.toNat ≤ l.bits.toNat := by
129        have : ¬ (l.bits.toNat < l.op.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
130        omega
131      exact ext_origin_wp hc A msg m l i o s used hls hA ho hAb hbroke hx h1' hlen hs6 (by omega)
132        (by intro h3; omega) origin
133  · simp only [h0, ite_false]
134    exact refill_origin_wp hc A msg m l i o s used hls hA ho hAb hbroke ⟨hlen.1, by
135      have : 0 < 2 ^ l.op.toNat := Nat.pow_pos (by omega)
136      omega⟩ hs6 (by omega) (by intro h3; omega) origin
137
138set_option maxHeartbeats 1000000 in
139/-- One actual length-table pass either follows its one permitted link or
140establishes the reviewed body postcondition. -/
141private theorem pass_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
142    (l : L) (i o s d k used : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
143    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
144    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
145    (hb15 : 15 ≤ l.bits.toNat + d) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat + d)
146    (hhere : l.here = .ref e.rl k) (hk : k < e.LCA.size)
147    (hEb : (e.LCA.getD k default).bits.toNat ≤ l.bits.toNat)
148    (hEd : (e.LCA.getD k default).bits.toNat + d ≤ 15)
149    (hcl : (LenLink (e.LCA.getD k default) ∧ LinkOK LenLeaf e.LCA e.ol (e.LCA.getD k default)) ∨
150      LenLeaf d (e.LCA.getD k default))
151    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
152    Wp (dolen c l) (e.heap A msg m) (fun l' h' =>
153      ((l'.againL = true ∧ l'.broke = false ∧ h' = e.heap A msg m ∧
154        LenLink (e.LCA.getD k default) ∧
155        ∃ j, j < 2 ^ (e.LCA.getD k default).op.toNat ∧
156          l'.here = .ref e.rl (e.ol + (e.LCA.getD k default).val.toNat + j) ∧
157          LS e l' i o ∧ l'.bits.toNat = l.bits.toNat - (e.LCA.getD k default).bits.toNat) ∨
158      StepPost e A msg m s o l' h') ∧
159      ∃ i' o' used', LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
160  have hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size := by rw [hAsz]; exact e.hAsz
161  have hAb : A.size < 2 ^ 63 := by rw [hAsz]; exact e.hAbig
162  have hkE : e.LCA[k]'hk = e.LCA.getD k default := by simp [Array.getD_eq_getD_getElem?, hk]
163  have hld : OkOn (e.heap A msg m) (Ptr.load l.here) (e.LCA.getD k default) := by
164    rw [hhere, ← hkE]; exact Ptr.load_ok (e.heap_cget_LCA A msg m) hk
165  have hEbn : (e.LCA.getD k default).bits.toUInt32.toNat = (e.LCA.getD k default).bits.toNat := toNat32 _
166  have hEb64 : (e.LCA.getD k default).bits.toUInt32.toUInt64.toNat = (e.LCA.getD k default).bits.toNat := by simp [toNat32]
167  have hls1 := hls.dropL (e.LCA.getD k default).bits.toUInt32 (by omega) (by omega)
168  have origin1 := drop_origin (e.LCA.getD k default).bits.toUInt32 hls origin (by omega)
169  rw [dolen_eq_len]
170  dsimp only
171  refine Wp.bindO hld ?_
172  refine Wp.bindO (shr64_ok (x := l.hold) (by omega)) ?_
173  refine Wp.bindO hld ?_
174  generalize e.LCA.getD k default = E at *
175  by_cases hz : (E.op.toUInt32 == 0) = true
176  · simp only [hz, ite_true]
177    refine Wp.bindO hld ?_
178    have hst : store8 l.out E.val.toUInt8 (e.heap A msg m) =
179        .ok ((), e.heap (A.set! o E.val.toUInt8) msg m) := by
180      rw [hls.hout, ← e.heap_put A (A.set! o E.val.toUInt8) msg m]
181      exact Ptr.store_ok (e.heap_bytes_ob A msg m) (e.heap_ro_ob A msg m) (by omega)
182    refine Wp.bindE hst ?_
183    refine Wp.bindO (x := Ptr.ref (BRef.blk e.ob) (o + 1)) ?_ ?_
184    · rw [hls.hout]
185      exact Ptr.add_nat_ok (e.heap_bytes_ob _ msg m) (by simp; omega)
186    · refine Wp.pure' ⟨Or.inr ?_, ?_⟩
187      · refine ⟨i, o + 1, A.set! o E.val.toUInt8, msg, m, ?_, hsi, by omega, by omega, by omega,
188          by simp, rfl, rfl, ?_, ?_, ?_⟩
189        · exact ⟨hls.hin, rfl, hls.hi0, hls.hi1, by have := hls.ho0; omega, hls1.hb, hls1.hH, hls1.hacc⟩
190        · intro j hj
191          have hne : o ≠ j := by omega
192          simp [Array.set!, hne]
193        · intro _; exact ⟨by omega, rfl, rfl⟩
194        · intro h; simp [hbroke] at h
195      · refine ⟨i, o + 1, used + E.bits.toUInt32.toNat, ?_, origin1, by omega⟩
196        exact ⟨hls.hin, rfl, hls.hi0, hls.hi1, by have := hls.ho0; omega, hls1.hb, hls1.hH, hls1.hacc⟩
197  · have hz' : E.op ≠ 0 := by rw [mask0] at hz; simpa using hz
198    by_cases hb16 : (E.op.toUInt32 &&& 16 != 0) = true
199    · simp only [hz, hb16, ite_true, ite_false, Bool.false_eq_true]
200      have hb16' : E.op &&& 16 ≠ 0 := by rw [mask16] at hb16; simpa using hb16
201      have hbase : (E.op &&& 15).toNat ≤ 5 ∧ 3 ≤ E.val.toNat ∧
202          E.val.toNat + 2 ^ (E.op &&& 15).toNat ≤ 259 := by
203        rcases hcl with h | h
204        · exact False.elim (hb16' h.1.2.1)
205        · rcases h.2 with h0 | h | h
206          · exact False.elim (hz' h0)
207          · exact h.2
208          · exact False.elim (hb16' h.1)
209      refine Wp.bindO hld ?_
210      let stage : L :=
211        { in_ := l.in_, out := l.out, hold := l.hold >>> E.bits.toUInt32.toUInt64, bits := l.bits - E.bits.toUInt32,
212          here := l.here, op := E.op.toUInt32 &&& 15, len := E.val.toUInt32, dist := l.dist, from_ := l.from_,
213          broke := l.broke, againL := false, againD := l.againD }
214      have stageLocals : LS e stage i o := LS.congr hls1 rfl rfl rfl rfl
215      have stageOrigin : Origin.Inv e stage.hold.toNat stage.bits.toNat i (used + E.bits.toUInt32.toNat) := origin1
216      have stageExtra : stage.op.toNat ≤ 5 := by dsimp [stage]; rw [mask15]; exact hbase.1
217      have stageLength : 3 ≤ stage.len.toNat ∧ stage.len.toNat + 2 ^ stage.op.toNat ≤ 259 := by
218        simpa [stage, mask15] using hbase.2
219      have stageBits : i = s + 2 → 1 ≤ stage.bits.toNat := by
220        intro hi
221        have := hbi2 hi
222        dsimp [stage]
223        rw [u32_toNat_sub (by omega), hEbn]
224        omega
225      obtain ⟨l', h', run, outOrigin⟩ := len_origin_wp hc A msg m stage i o s (used + E.bits.toUInt32.toNat)
226        stageLocals hA ho hAb hbroke stageExtra stageLength hs6 hT stageBits stageOrigin
227      have step := Wp.at_run (dolenLen_step_wp hc A msg m stage i o s stageLocals hAsz ho
228        hbroke rfl stageExtra stageLength hs6 hsi hT stageBits) run
229      refine Wp.of_eq run ⟨Or.inr step, ?_⟩
230      obtain ⟨i', o', used', locals', origin', mono⟩ := outOrigin
231      exact ⟨i', o', used', locals', origin', by omega⟩
232    · have hb16' : E.op &&& 16 = 0 := by rw [mask16] at hb16; simpa using hb16
233      by_cases hb64 : (E.op.toUInt32 &&& 64 == 0) = true
234      · simp only [hz, hb16, hb64, ite_true, ite_false, Bool.false_eq_true]
235        have hb64' : E.op &&& 64 = 0 := by rw [mask64] at hb64; simpa using hb64
236        have hl : LenLink E := ⟨hz', hb16', hb64'⟩
237        have hlk : LinkOK LenLeaf e.LCA e.ol E := by
238          rcases hcl with h | h
239          · exact h.2
240          · rcases h.2 with h0 | h | h
241            · exact False.elim (hz' h0)
242            · exact False.elim (h.1 hb16')
243            · exact False.elim (h.2 hb64')
244        refine Wp.bindO hld ?_
245        have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
246        have hop32 : E.op.toUInt32.toNat < 32 := by rw [toNat32]; have := hlk.2.2.1; omega
247        refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat)) ?_ ?_
248        · rw [hlc]
249          exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol)
250            (n := E.val.toNat) (e.heap_cget_LCA A msg m)
251            (Nat.le_trans (Nat.le_add_right _ _) hlk.2.2.2.1)
252        refine Wp.bindO (shl32_ok hop32) ?_
253        have hlow := hold_low64 (x := l.hold >>> E.bits.toUInt32.toUInt64) (k := E.op.toUInt32) hop32
254        have hjlt : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat < 2 ^ E.op.toNat := by
255          rw [toNat32]; exact Nat.mod_lt _ (Nat.pow_pos (by omega))
256        generalize hjd : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat = j at hlow hjlt
257        refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat + j)) ?_ ?_
258        · rw [hlow]
259          exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol + E.val.toNat)
260            (n := j) (e.heap_cget_LCA A msg m) (by have := hlk.2.2.2.1; omega)
261        refine Wp.pure' ⟨Or.inl ⟨rfl, hbroke, rfl, hl, j, hjlt, rfl,
262          LS.congr hls1 rfl rfl rfl rfl, ?_⟩,
263          i, o, used + E.bits.toUInt32.toNat, LS.congr hls1 rfl rfl rfl rfl, origin1, by omega⟩
264        rw [u32_toNat_sub (by omega), hEbn]
265      · simp only [hz, hb16, hb64, ite_false, Bool.false_eq_true]
266        by_cases hb32 : (E.op.toUInt32 &&& 32 != 0) = true
267        · simp only [hb32, ite_true]
268          refine Wp.bindE (e.heap_ldstate hc A msg m) ?_
269          refine Wp.bindE (e.heap_stmode hc A msg m TYPE _ rfl) ?_
270          refine Wp.pure' ⟨Or.inr ?_, i, o, used + E.bits.toUInt32.toNat,
271            LS.congr hls1 rfl rfl rfl rfl, origin1, by omega⟩
272          refine ⟨i, o, A, msg, TYPE, LS.congr hls1 rfl rfl rfl rfl, hsi, by omega, by omega, by omega,
273            rfl, rfl, rfl, (fun _ _ => rfl), ?_, (fun _ => Or.inl rfl)⟩
274          intro h; cases h
275        · simp only [hb32, ite_false, Bool.false_eq_true]
276          obtain ⟨ip, hip⟩ := badData_run hc A msg m "invalid literal/length code" (by decide +kernel)
277          refine Wp.bindE hip ?_
278          refine Wp.pure' ⟨Or.inr ?_, i, o, used + E.bits.toUInt32.toNat, LS.congr hls1 rfl rfl rfl rfl, origin1, by omega⟩
279          refine ⟨i, o, A, .ref (BRef.str ip) 0, BAD, LS.congr hls1 rfl rfl rfl rfl, hsi, by omega, by omega, by omega,
280            rfl, rfl, rfl, (fun _ _ => rfl), ?_, (fun _ => Or.inr rfl)⟩
281          intro h; cases h
282
283/-- The actual `dolen` root/link loop ends after at most two passes. -/
284private theorem loop_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
285    (l : L) (i o s kidx used : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
286    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
287    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
288    (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat)
289    (hk : kidx < 2 ^ e.s0.lenbits.toNat) (hhere : l.here = .ref e.rl (e.ol + kidx))
290    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
291    Wp (cdoWhile (dolen c) (fun l => pure (l.againL, l)) l) (e.heap A msg m)
292      (fun l' h' => StepPost e A msg m s o l' h' ∧
293        ∃ i' o' used', LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
294  have hts := e.hlt
295  obtain ⟨hR, hsz, hall⟩ := hts
296  have hksz : e.ol + kidx < e.LCA.size := by omega
297  have hclass : (LenLink (e.LCA.getD (e.ol + kidx) default) ∧
298      LinkOK LenLeaf e.LCA e.ol (e.LCA.getD (e.ol + kidx) default)) ∨
299      LenLeaf 0 (e.LCA.getD (e.ol + kidx) default) := by
300    have hh := hall kidx hk
301    by_cases hl : LenLink (e.LCA.getD (e.ol + kidx) default)
302    · rw [ite_eq_left hl] at hh; exact Or.inl ⟨hl, hh⟩
303    · rw [ite_eq_right hl] at hh; exact Or.inr hh
304  have hEd0 : (e.LCA.getD (e.ol + kidx) default).bits.toNat + 0 ≤ 15 := by
305    rcases hclass with h | h
306    · exact h.2.1
307    · exact h.1
308  obtain ⟨l1, h1, e1, hq1, origin1⟩ := pass_origin_wp hc A msg m l i o s 0 (e.ol + kidx) used hls hAsz ho hbroke
309    hs6 hsi hT (by omega) (by intro hi; have := hbi2 hi; omega) hhere hksz (by omega) hEd0 hclass origin
310  generalize hE0 : e.LCA.getD (e.ol + kidx) default = E0 at hq1 hclass hEd0
311  rcases hq1 with ⟨hag, hbr, hh, hlink, j, hjlt, hhere1, hls1, hb1⟩ | hend
312  · subst hh
313    obtain ⟨i1, o1, used1, locals1, O1, mono1⟩ := origin1
314    have i1eq : i1 = i := (Ptr.ref.inj (locals1.hin.symm.trans hls1.hin)).2
315    have o1eq : o1 = o := (Ptr.ref.inj (locals1.hout.symm.trans hls1.hout)).2
316    subst i1 o1
317    have hlk : LinkOK LenLeaf e.LCA e.ol E0 := by
318      rcases hclass with h | h
319      · exact h.2
320      · rcases h.2 with h0 | h | h
321        · exact False.elim (hlink.1 h0)
322        · exact False.elim (h.1 hlink.2.1)
323        · exact False.elim (h.2 hlink.2.2)
324    have hleaf := hlk.2.2.2.2 j hjlt
325    have hk2 : e.ol + E0.val.toNat + j < e.LCA.size := by have := hlk.2.2.2.1; omega
326    obtain ⟨l2, h2, e2, hq2, origin2⟩ := pass_origin_wp hc A msg m l1 i o s E0.bits.toNat (e.ol + E0.val.toNat + j) used1
327      hls1 hAsz ho hbr hs6 hsi hT (by omega) (by intro hi; have := hbi2 hi; omega)
328      hhere1 hk2 (by have := hleaf.1; omega) hleaf.1 (Or.inr hleaf) O1
329    rcases hq2 with ⟨_, _, _, hl2, _⟩ | hend2
330    · rcases hleaf.2 with h0 | h | h
331      · exact False.elim (hl2.1 h0)
332      · exact False.elim (h.1 hl2.2.1)
333      · exact False.elim (h.2 hl2.2.2)
334    · have c1 : (fun l : L => (pure (l.againL, l) : M (Bool × L))) l1 (e.heap A msg m) =
335          .ok ((true, l1), e.heap A msg m) := by simp [hag]
336      have c2 : (fun l : L => (pure (l.againL, l) : M (Bool × L))) l2 h2 =
337          .ok ((false, l2), h2) := by simp [StepPost.againL hend2]
338      refine Wp.of_eq (cdoWhile_two e1 c1 e2 c2) ⟨hend2, ?_⟩
339      obtain ⟨i2, o2, used2, locals2, O2, mono2⟩ := origin2
340      exact ⟨i2, o2, used2, locals2, O2, by omega⟩
341  · have c1 : (fun l : L => (pure (l.againL, l) : M (Bool × L))) l1 h1 =
342        .ok ((false, l1), h1) := by simp [StepPost.againL hend]
343    exact Wp.of_eq (cdoWhile_one e1 c1) ⟨hend, origin1⟩
344
345
346/-- Root-table lookup followed by the actual length root/link loop. -/
347private theorem root_origin_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
348    (l : L) (i o s used : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
349    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
350    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
351    (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat)
352    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
353    Wp (do
354      let here ← c.lcode.add (l.hold &&& c.lmask.toUInt64).toNat
355      cdoWhile (dolen c) (fun l => pure (l.againL, l)) {l with here})
356      (e.heap A msg m) (fun l' h' => StepPost e A msg m s o l' h' ∧
357        ∃ i' o' used', LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
358  have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
359  have hR : e.s0.lenbits.toNat < 32 := by have := e.hlt.1; omega
360  have hmask : c.lmask.toUInt64.toNat = 2 ^ e.s0.lenbits.toNat - 1 := by
361    rw [hc.lmask, UInt32.toNat_toUInt64]; exact u32_shl1_sub1 hR
362  have hidx := u64_and_mask (x := l.hold) hmask
363  have hmod : l.hold.toNat % 2 ^ e.s0.lenbits.toNat < 2 ^ e.s0.lenbits.toNat :=
364    Nat.mod_lt _ (Nat.pow_pos (by omega))
365  refine Wp.bindO (x := Ptr.ref e.rl (e.ol + l.hold.toNat % 2 ^ e.s0.lenbits.toNat)) ?_ ?_
366  · rw [hlc, hidx]
367    exact Ptr.add_nat_ok (e.heap_cget_LCA A msg m) (by have := e.hlt.2.1; omega)
368  · exact loop_origin_wp hc A msg m _ i o s _ used (LS.congr hls rfl rfl rfl rfl) hAsz ho hbroke
369      hs6 hsi hT hb15 hbi2 hmod rfl origin
370
371
372/-- Every source path retains the original body postcondition and an exact
373source suffix; accepted table-symbol semantics are a separate obligation. -/
374theorem actual_body_preserves_origin : BodyOrigin.Goal.actual_body_preserves_origin := by
375  intro e c A msg m l i o used hp origin
376  rcases hp with ⟨hc, hls, hAsz, hi6, ho258, hbroke⟩
377  change Wp (inflate_fast_body c l) (e.heap A msg m) (fun l' h' => StepPost e A msg m i o l' h' ∧
378    ∃ i' o' used', LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used')
379  unfold inflate_fast_body
380  by_cases h1 : l.bits < 15
381  · simp only [h1, ite_true]
382    have hb : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp h1
383    have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
384    refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
385    have hl1 := hls.pullL (by omega) hiin
386    have origin1 := pull_origin hls origin (by omega) hiin
387    have hb1 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
388    have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
389    have hb1' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
390      simp only [pullL] at hb1 ⊢; omega
391    refine Wp.bindO (pull_run e _ _ (i + 1) o hl1 hb1' hi2 (e.heap_bytes_in A msg m)) ?_
392    have hl2 := hl1.pullL hb1' hi2
393    have origin2 := pull_origin hl1 origin1 hb1' hi2
394    have hb2 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)))
395      (e.IN.getD (i + 1) 0) (.ref (BRef.blk e.ib) (i + 1 + 1)) hl1.hb
396    exact root_origin_wp hc A msg m _ (i + 1 + 1) o i used hl2 hAsz ho258 hbroke hi6 (by omega) (by omega)
397      (by simp only [pullL] at hb1 hb2 ⊢; omega)
398      (by intro _; simp only [pullL] at hb1 hb2 ⊢; omega) origin2
399  · simp only [h1, ite_false]
400    have hb : 15 ≤ l.bits.toNat := by
401      have : ¬ l.bits.toNat < 15 := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
402      omega
403    exact root_origin_wp hc A msg m l i o i used hls hAsz ho258 hbroke hi6 (by omega) (by omega) hb (by omega) origin
404
405end Zlib.Inffast.Proofs.BodyOriginProof
406
407namespace Zlib.Inffast.Proofs
408open Zlib.Inffast.Spec
409/-- The entire actual body retains the exact entry-stream origin on every exit. -/
410theorem actual_body_preserves_origin : BodyOrigin.Goal.actual_body_preserves_origin :=
411  BodyOriginProof.actual_body_preserves_origin
412end Zlib.Inffast.Proofs