inffast.c.length-trace.lean

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

1import ZlibF.Spec.InflateFastLengthTrace
2import ZlibF.Proof.«inffast.c.body»
3
4/-!
5# Selected length-table entries through the actual fast body
6
7The source pass retains its exact entry and both levels' bit count. The
8four leaf outcomes retain actual output or the real length-extra and
9subsequent distance results. Existing safety is joined on the same run.
10-/
11
12namespace Zlib.Inffast.Proofs.LengthTraceProof
13open C Zlib.Inffast Zlib.Inffast.Spec Zlib.Inffast.Proofs ZlibF.Spec
14open Zlib.Inffast.Spec.LengthTrace
15
16variable {e : Env} {c : Ctx}
17
18set_option maxHeartbeats 1000000 in
19private theorem pass_trace_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
20    (l : L) (i o s d k : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
21    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
22    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
23    (hb15 : 15 ≤ l.bits.toNat + d) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat + d)
24    (hhere : l.here = .ref e.rl k) (hk : k < e.LCA.size)
25    (hEb : (e.LCA.getD k default).bits.toNat ≤ l.bits.toNat)
26    (hEd : (e.LCA.getD k default).bits.toNat + d ≤ 15)
27    (hcl : (LenLink (e.LCA.getD k default) ∧ LinkOK LenLeaf e.LCA e.ol (e.LCA.getD k default)) ∨
28      LenLeaf d (e.LCA.getD k default)) :
29    Wp (dolen c l) (e.heap A msg m) (fun l' h' =>
30      (l'.againL = true ∧ l'.broke = false ∧ h' = e.heap A msg m ∧
31        LenLink (e.LCA.getD k default) ∧
32        ∃ j, j < 2 ^ (e.LCA.getD k default).op.toNat ∧
33          l'.here = .ref e.rl (e.ol + (e.LCA.getD k default).val.toNat + j) ∧
34          j = (l.hold.toNat / 2 ^ (e.LCA.getD k default).bits.toNat) % 2 ^ (e.LCA.getD k default).op.toNat ∧
35          LS e l' i o ∧ l'.bits.toNat = l.bits.toNat - (e.LCA.getD k default).bits.toNat ∧
36          Sg e l'.hold.toNat l'.bits.toNat i = (Sg e l.hold.toNat l.bits.toNat i).drop (e.LCA.getD k default).bits.toNat) ∨
37      End e A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop (e.LCA.getD k default).bits.toNat)
38        i o (e.LCA.getD k default) l' h') := by
39  have hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size := by rw [hAsz]; exact e.hAsz
40  have hAb : A.size < 2 ^ 63 := by rw [hAsz]; exact e.hAbig
41  have hkE : e.LCA[k]'hk = e.LCA.getD k default := by simp [Array.getD_eq_getD_getElem?, hk]
42  have hld : OkOn (e.heap A msg m) (Ptr.load l.here) (e.LCA.getD k default) := by
43    rw [hhere, ← hkE]; exact Ptr.load_ok (e.heap_cget_LCA A msg m) hk
44  have hEbn : (e.LCA.getD k default).bits.toUInt32.toNat = (e.LCA.getD k default).bits.toNat := toNat32 _
45  have hEb64 : (e.LCA.getD k default).bits.toUInt32.toUInt64.toNat = (e.LCA.getD k default).bits.toNat := by simp [toNat32]
46  have hls1 := hls.dropL (e.LCA.getD k default).bits.toUInt32 (by omega) (by omega)
47  have hsg1 := Sg_dropL (e := e) l (e.LCA.getD k default).bits.toUInt32 i (by omega) (by omega)
48  rw [dolen_eq_len]
49  dsimp only
50  refine Wp.bindO hld ?_
51  refine Wp.bindO (shr64_ok (x := l.hold) (by omega)) ?_
52  refine Wp.bindO hld ?_
53  generalize e.LCA.getD k default = E at *
54  have hsg1' : Sg e (l.hold >>> E.bits.toUInt32.toUInt64).toNat (l.bits - E.bits.toUInt32).toNat i =
55      (Sg e l.hold.toNat l.bits.toNat i).drop E.bits.toNat := by
56    simpa only [dropL, hEbn] using hsg1
57  by_cases hz : (E.op.toUInt32 == 0) = true
58  · simp only [hz, ite_true]
59    refine Wp.bindO hld ?_
60    have hst : store8 l.out E.val.toUInt8 (e.heap A msg m) =
61        .ok ((), e.heap (A.set! o E.val.toUInt8) msg m) := by
62      rw [hls.hout, ← e.heap_put A (A.set! o E.val.toUInt8) msg m]
63      exact Ptr.store_ok (e.heap_bytes_ob A msg m) (e.heap_ro_ob A msg m) (by omega)
64    refine Wp.bindE hst ?_
65    refine Wp.bindO (x := Ptr.ref (BRef.blk e.ob) (o + 1)) ?_ ?_
66    · rw [hls.hout]
67      exact Ptr.add_nat_ok (e.heap_bytes_ob _ msg m) (by simp; omega)
68    · have hop : E.op = 0 := by rw [mask0] at hz; simpa using hz
69      refine Wp.pure' (Or.inr ?_)
70      refine ⟨?_, rfl, Or.inl ⟨hop, hbroke, ?_, hsg1', rfl⟩⟩
71      · intro link; exact link.1 hop
72      · exact ⟨hls.hin, rfl, hls.hi0, hls.hi1, by have := hls.ho0; omega, hls1.hb, hls1.hH, hls1.hacc⟩
73  · have hz' : E.op ≠ 0 := by rw [mask0] at hz; simpa using hz
74    by_cases hb16 : (E.op.toUInt32 &&& 16 != 0) = true
75    · simp only [hz, hb16, ite_true, ite_false, Bool.false_eq_true]
76      have hb16' : E.op &&& 16 ≠ 0 := by rw [mask16] at hb16; simpa using hb16
77      have hbase : (E.op &&& 15).toNat ≤ 5 ∧ 3 ≤ E.val.toNat ∧
78          E.val.toNat + 2 ^ (E.op &&& 15).toNat ≤ 259 := by
79        rcases hcl with h | h
80        · exact False.elim (hb16' h.1.2.1)
81        · rcases h.2 with h0 | h | h
82          · exact False.elim (hz' h0)
83          · exact h.2
84          · exact False.elim (hb16' h.1)
85      refine Wp.bindO hld ?_
86      let stage : L :=
87        { in_ := l.in_, out := l.out, hold := l.hold >>> E.bits.toUInt32.toUInt64, bits := l.bits - E.bits.toUInt32,
88          here := l.here, op := E.op.toUInt32 &&& 15, len := E.val.toUInt32, dist := l.dist, from_ := l.from_,
89          broke := l.broke, againL := false, againD := l.againD }
90      obtain ⟨l', h', run, result⟩ := dolenLen_wp hc A msg m stage i o s e.hdt
91        (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb hbroke
92        (by dsimp [stage]; rw [mask15]; exact hbase.1)
93        (by simpa [stage, mask15] using hbase.2) hs6 hT
94        (by intro hi; have := hbi2 hi; show 1 ≤ (l.bits - E.bits.toUInt32).toNat
95            rw [u32_toNat_sub (by omega), hEbn]; omega)
96      have hag : l'.againL = false := by simpa [stage] using dolenLen_againL run
97      refine Wp.of_eq run (Or.inr ?_)
98      refine ⟨?_, hag, Or.inr (Or.inl ⟨hz', hb16', ?_⟩)⟩
99      · intro link; exact hb16' link.2.1
100      · obtain ⟨i', extra, rest, hi, hi1, read, refill⟩ := result
101        refine ⟨i', extra, rest, hi, hi1, ?_, ?_⟩
102        · simpa only [stage, mask15, hsg1'] using read
103        · simpa only [stage, UInt16.toNat_toUInt32] using refill
104    · have hb16' : E.op &&& 16 = 0 := by rw [mask16] at hb16; simpa using hb16
105      by_cases hb64 : (E.op.toUInt32 &&& 64 == 0) = true
106      · simp only [hz, hb16, hb64, ite_true, ite_false, Bool.false_eq_true]
107        have hb64' : E.op &&& 64 = 0 := by rw [mask64] at hb64; simpa using hb64
108        have hl : LenLink E := ⟨hz', hb16', hb64'⟩
109        have hlk : LinkOK LenLeaf e.LCA e.ol E := by
110          rcases hcl with h | h
111          · exact h.2
112          · rcases h.2 with h0 | h | h
113            · exact False.elim (hz' h0)
114            · exact False.elim (h.1 hb16')
115            · exact False.elim (h.2 hb64')
116        refine Wp.bindO hld ?_
117        have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
118        have hop32 : E.op.toUInt32.toNat < 32 := by rw [toNat32]; have := hlk.2.2.1; omega
119        refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat)) ?_ ?_
120        · rw [hlc]
121          exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol)
122            (n := E.val.toNat) (e.heap_cget_LCA A msg m)
123            (Nat.le_trans (Nat.le_add_right _ _) hlk.2.2.2.1)
124        refine Wp.bindO (shl32_ok hop32) ?_
125        have hlow := hold_low64 (x := l.hold >>> E.bits.toUInt32.toUInt64) (k := E.op.toUInt32) hop32
126        have hjlt : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat < 2 ^ E.op.toNat := by
127          rw [toNat32]; exact Nat.mod_lt _ (Nat.pow_pos (by omega))
128        generalize hjd : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat = j at hlow hjlt
129        refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat + j)) ?_ ?_
130        · rw [hlow]
131          exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol + E.val.toNat)
132            (n := j) (e.heap_cget_LCA A msg m) (by have := hlk.2.2.2.1; omega)
133        refine Wp.pure' (Or.inl ⟨rfl, hbroke, rfl, hl, j, hjlt, rfl, ?_,
134          LS.congr hls1 rfl rfl rfl rfl, ?_, hsg1'⟩)
135        · have hshift : (l.hold >>> E.bits.toUInt32.toUInt64).toNat = l.hold.toNat / 2 ^ E.bits.toNat := by
136            rw [u64_shr (by omega), hEbn]
137          simpa only [hshift, toNat32] using hjd.symm
138        · rw [u32_toNat_sub (by omega), hEbn]
139      · simp only [hz, hb16, hb64, ite_false, Bool.false_eq_true]
140        by_cases hb32 : (E.op.toUInt32 &&& 32 != 0) = true
141        · simp only [hb32, ite_true]
142          refine Wp.bindE (e.heap_ldstate hc A msg m) ?_
143          refine Wp.bindE (e.heap_stmode hc A msg m TYPE _ rfl) ?_
144          have hb64' : E.op &&& 64 ≠ 0 := by rw [mask64] at hb64; simpa using hb64
145          have hb32' : E.op &&& 32 ≠ 0 := by rw [mask32] at hb32; simpa using hb32
146          refine Wp.pure' (Or.inr ?_)
147          refine ⟨?_, rfl, Or.inr (Or.inr (Or.inl ⟨hz', hb16', hb64', hb32', rfl,
148            LS.congr hls1 rfl rfl rfl rfl, hsg1', rfl⟩))⟩
149          intro link; exact hb64' link.2.2
150        · simp only [hb32, ite_false, Bool.false_eq_true]
151          obtain ⟨ip, hip⟩ := badData_run hc A msg m "invalid literal/length code" (by decide +kernel)
152          refine Wp.bindE hip ?_
153          have hb64' : E.op &&& 64 ≠ 0 := by rw [mask64] at hb64; simpa using hb64
154          have hb32' : E.op &&& 32 = 0 := by rw [mask32] at hb32; simpa using hb32
155          refine Wp.pure' (Or.inr ?_)
156          refine ⟨?_, rfl, Or.inr (Or.inr (Or.inr ⟨hz', hb16', hb64', hb32', rfl,
157            LS.congr hls1 rfl rfl rfl rfl, hsg1', .ref (.str ip) 0, rfl⟩))⟩
158          intro link; exact hb64' link.2.2
159
160private theorem loop_trace_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
161    (l : L) (i o s kidx : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
162    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
163    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
164    (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat)
165    (hk : kidx < 2 ^ e.s0.lenbits.toNat) (hhere : l.here = .ref e.rl (e.ol + kidx)) :
166    Wp (cdoWhile (dolen c) (fun l => pure (l.againL, l)) l) (e.heap A msg m)
167      (fun l' h' => ∃ entry consumed, consumed ≤ 15 ∧
168        LengthSemantics.Look e l.hold.toNat kidx entry consumed ∧
169        End e A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop consumed) i o entry l' h') := by
170  obtain ⟨hR, hsz, hall⟩ := e.hlt
171  have hksz : e.ol + kidx < e.LCA.size := by omega
172  have hclass : (LenLink (e.LCA.getD (e.ol + kidx) default) ∧
173      LinkOK LenLeaf e.LCA e.ol (e.LCA.getD (e.ol + kidx) default)) ∨
174      LenLeaf 0 (e.LCA.getD (e.ol + kidx) default) := by
175    have hh := hall kidx hk
176    by_cases hl : LenLink (e.LCA.getD (e.ol + kidx) default)
177    · rw [ite_eq_left hl] at hh; exact Or.inl ⟨hl, hh⟩
178    · rw [ite_eq_right hl] at hh; exact Or.inr hh
179  have hEd0 : (e.LCA.getD (e.ol + kidx) default).bits.toNat + 0 ≤ 15 := by
180    rcases hclass with h | h
181    · exact h.2.1
182    · exact h.1
183  obtain ⟨l1, h1, run1, result1⟩ := pass_trace_wp hc A msg m l i o s 0 (e.ol + kidx) hls hAsz ho hbroke
184    hs6 hsi hT (by omega) (by intro hi; have := hbi2 hi; omega) hhere hksz (by omega) hEd0 hclass
185  generalize firstCell : e.LCA.getD (e.ol + kidx) default = first at result1 hclass hEd0
186  rcases result1 with ⟨again1, broke1, heap1, link1, j, jLt, here1, jEq, locals1, bits1, stream1⟩ | end1
187  · subst heap1
188    have links : LinkOK LenLeaf e.LCA e.ol first := by
189      rcases hclass with h | h
190      · exact h.2
191      · rcases h.2 with h0 | h | h
192        · exact False.elim (link1.1 h0)
193        · exact False.elim (h.1 link1.2.1)
194        · exact False.elim (h.2 link1.2.2)
195    have leaf := links.2.2.2.2 j jLt
196    have secondIn : e.ol + first.val.toNat + j < e.LCA.size := by have := links.2.2.2.1; omega
197    obtain ⟨l2, h2, run2, result2⟩ := pass_trace_wp hc A msg m l1 i o s first.bits.toNat
198      (e.ol + first.val.toNat + j) locals1 hAsz ho broke1 hs6 hsi hT
199      (by omega) (by intro hi; have := hbi2 hi; omega) here1 secondIn
200      (by have := leaf.1; omega) leaf.1 (Or.inr leaf)
201    rcases result2 with ⟨_, _, _, link2, _⟩ | end2
202    · rcases leaf.2 with h0 | h | h
203      · exact False.elim (link2.1 h0)
204      · exact False.elim (h.1 link2.2.1)
205      · exact False.elim (h.2 link2.2.2)
206    · have cond1 : (fun q : L => (pure (q.againL, q) : M (Bool × L))) l1 (e.heap A msg m) =
207          .ok ((true, l1), e.heap A msg m) := by simp [again1]
208      have cond2 : (fun q : L => (pure (q.againL, q) : M (Bool × L))) l2 h2 =
209          .ok ((false, l2), h2) := by simp [end2.2.1]
210      refine Wp.of_eq (cdoWhile_two run1 cond1 run2 cond2)
211        ⟨e.LCA.getD (e.ol + first.val.toNat + j) default,
212          first.bits.toNat + (e.LCA.getD (e.ol + first.val.toNat + j) default).bits.toNat,
213          by have := leaf.1; omega, ?_, ?_⟩
214      · exact Or.inr ⟨first, j, firstCell, link1, jLt, jEq, rfl, rfl, by have := leaf.1; omega, end2.1⟩
215      · simpa only [stream1, List.drop_drop] using end2
216  · have cond1 : (fun q : L => (pure (q.againL, q) : M (Bool × L))) l1 h1 =
217        .ok ((false, l1), h1) := by simp [end1.2.1]
218    exact Wp.of_eq (cdoWhile_one run1 cond1)
219      ⟨first, first.bits.toNat, by omega, Or.inl ⟨firstCell, rfl, end1.1⟩, end1⟩
220
221private theorem root_trace_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
222    (l : L) (i o s : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
223    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
224    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
225    (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat) :
226    Wp (do
227      let here ← c.lcode.add (l.hold &&& c.lmask.toUInt64).toNat
228      cdoWhile (dolen c) (fun l => pure (l.againL, l)) {l with here}) (e.heap A msg m)
229      (fun l' h' => ∃ entry consumed, consumed ≤ 15 ∧
230        LengthSemantics.Look e l.hold.toNat (l.hold.toNat % 2 ^ e.s0.lenbits.toNat) entry consumed ∧
231        End e A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop consumed) i o entry l' h') := by
232  have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
233  have hR : e.s0.lenbits.toNat < 32 := by have := e.hlt.1; omega
234  have hmask : c.lmask.toUInt64.toNat = 2 ^ e.s0.lenbits.toNat - 1 := by
235    rw [hc.lmask, UInt32.toNat_toUInt64]; exact u32_shl1_sub1 hR
236  have hidx := u64_and_mask (x := l.hold) hmask
237  have hmod : l.hold.toNat % 2 ^ e.s0.lenbits.toNat < 2 ^ e.s0.lenbits.toNat :=
238    Nat.mod_lt _ (Nat.pow_pos (by omega))
239  refine Wp.bindO (x := Ptr.ref e.rl (e.ol + l.hold.toNat % 2 ^ e.s0.lenbits.toNat)) ?_ ?_
240  · rw [hlc, hidx]
241    exact Ptr.add_nat_ok (e.heap_cget_LCA A msg m) (by have := e.hlt.2.1; omega)
242  · exact loop_trace_wp hc A msg m _ i o s _ (LS.congr hls rfl rfl rfl rfl)
243      hAsz ho hbroke hs6 hsi hT hb15 hbi2 hmod rfl
244
245/-- The complete source body retains the chosen literal/length leaf and
246its exact effects, together with the independently proved safety result. -/
247theorem actual_body_retains_selected_length : LengthTrace.Goal.actual_body_retains_selected_length := by
248  intro e c A msg m l i o hp
249  have hc := hp.context
250  have hls := hp.locals
251  have hAsz := hp.outputSize
252  have hi6 := hp.inputRoom
253  have ho258 := hp.outputRoom
254  have hbroke := hp.notStopped
255  have trace : Wp (inflate_fast_body c l) (e.heap A msg m) (fun l' h' =>
256      Sg e (ready e l i).1.hold.toNat (ready e l i).1.bits.toNat (ready e l i).2 =
257        Sg e l.hold.toNat l.bits.toNat i ∧
258      ∃ entry consumed, consumed ≤ 15 ∧
259        LengthSemantics.Look e (ready e l i).1.hold.toNat
260          ((ready e l i).1.hold.toNat % 2 ^ e.s0.lenbits.toNat) entry consumed ∧
261        End e A msg m ((Sg e (ready e l i).1.hold.toNat (ready e l i).1.bits.toNat
262          (ready e l i).2).drop consumed) (ready e l i).2 o entry l' h') := by
263    unfold inflate_fast_body
264    by_cases h1 : l.bits < 15
265    · simp only [ready, h1, ite_true]
266      have hb : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp h1
267      have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
268      refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
269      have hl1 := hls.pullL (by omega) hiin
270      have stream1 := Sg_pullL hls (by omega) hiin
271      have hb1 := pullL_bits l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1)) hls.hb
272      have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
273      have hb1' : (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
274        simp only [pullL] at hb1 ⊢; omega
275      refine Wp.bindO (pull_run e _ _ (i + 1) o hl1 hb1' hi2 (e.heap_bytes_in A msg m)) ?_
276      have hl2 := hl1.pullL hb1' hi2
277      have stream2 := Sg_pullL hl1 hb1' hi2
278      have hb2 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1)))
279        (e.IN.getD (i + 1) 0) (.ref (.blk e.ib) (i + 1 + 1)) hl1.hb
280      refine Wp.mono (root_trace_wp hc A msg m _ (i + 1 + 1) o i hl2 hAsz ho258 hbroke hi6 (by omega) (by omega)
281        (by simp only [pullL] at hb1 hb2 ⊢; omega)
282        (by intro _; simp only [pullL] at hb1 hb2 ⊢; omega)) ?_
283      intro l' h' result
284      exact ⟨stream2.trans stream1, result⟩
285    · simp only [ready, h1, ite_false]
286      have hb : 15 ≤ l.bits.toNat := by
287        have : ¬ l.bits.toNat < 15 := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
288        omega
289      exact Wp.mono (root_trace_wp hc A msg m l i o i hls hAsz ho258 hbroke hi6 (by omega) (by omega) hb (by omega))
290        (fun _ _ result => ⟨by trivial, result⟩)
291  obtain ⟨l', after, run, sameStream, result⟩ := trace
292  have safe := Wp.at_run (inflate_fast_body_step_safe e c A msg m l i o hp) run
293  exact ⟨l', after, run, safe, sameStream, result⟩
294
295end Zlib.Inffast.Proofs.LengthTraceProof
296
297namespace Zlib.Inffast.Proofs
298open Zlib.Inffast.Spec
299/-- The selected literal/length leaf and its actual four-way result are
300retained by the complete fast body on the existing safety domain. -/
301theorem actual_body_retains_selected_length : LengthTrace.Goal.actual_body_retains_selected_length :=
302  LengthTraceProof.actual_body_retains_selected_length
303end Zlib.Inffast.Proofs