inffast.c.message.lean

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

1import ZlibF.Proof.«inffast.c.body»
2
3/-!
4# inffast.c: the message at end of block
5
6The original StepPost is unchanged. These derived execution lemmas retain
7that TYPE does not overwrite the message; only the BAD paths do so.
8-/
9
10namespace Zlib.Inffast.Proofs
11open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
12variable {e : Env} {c : Ctx}
13
14/-- The actual length branch preserves the message when it finishes in TYPE. -/
15theorem dolenLen_message_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
16    (l : L) (i o s : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
17    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
18    (hbroke : l.broke = false) (hagain : l.againL = false) (hx : l.op.toNat ≤ 5)
19    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
20    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
21    (hb2 : i = s + 2 → 1 ≤ l.bits.toNat) :
22    Wp (dolenLen c l) (e.heap A msg m) (fun l' h' => ∃ B p q, h' = e.heap B p q ∧ l'.againL = false ∧ (q = TYPE → p = msg)) := by
23  have hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size := by rw [hAsz]; exact e.hAsz
24  have hAb : A.size < 2 ^ 63 := by rw [hAsz]; exact e.hAbig
25  obtain ⟨l', h', hr, hq⟩ := dolenLen_wp hc A msg m l i o s e.hdt hls hA ho hAb hbroke hx hlen hs6 hT hb2
26  refine ⟨l', h', hr, ?_⟩
27  have hag : l'.againL = false := (dolenLen_againL hr).trans hagain
28  obtain ⟨i2, lx, S1, _, _, hrb, i3, H3, b3, E, cb, _, _, _, _, _, _, _, _, hend⟩ := hq
29  rcases hend.2.2 with hgood | hbad
30  · obtain ⟨i', xv, rest, _, _, _, hb, hls', _, hh⟩ := hgood
31    exact ⟨_, msg, m, hh, hag, fun _ => rfl⟩
32  · obtain ⟨i', p, _, _, hb, hls', hh⟩ := hbad
33    exact ⟨A, p, BAD, hh, hag, fun h => False.elim ((by decide : BAD ≠ TYPE) h)⟩
34
35set_option maxHeartbeats 1000000 in
36/-- One actual length-table pass either follows its one permitted link or
37returns a concrete heap whose TYPE mode preserves the message. -/
38theorem dolen_pass_message_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
39    (l : L) (i o s d k : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
40    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
41    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
42    (hb15 : 15 ≤ l.bits.toNat + d) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat + d)
43    (hhere : l.here = .ref e.rl k) (hk : k < e.LCA.size)
44    (hEb : (e.LCA.getD k default).bits.toNat ≤ l.bits.toNat)
45    (hEd : (e.LCA.getD k default).bits.toNat + d ≤ 15)
46    (hcl : (LenLink (e.LCA.getD k default) ∧ LinkOK LenLeaf e.LCA e.ol (e.LCA.getD k default)) ∨
47      LenLeaf d (e.LCA.getD k default)) :
48    Wp (dolen c l) (e.heap A msg m) (fun l' h' =>
49      (l'.againL = true ∧ l'.broke = false ∧ h' = e.heap A msg m ∧
50        LenLink (e.LCA.getD k default) ∧
51        ∃ j, j < 2 ^ (e.LCA.getD k default).op.toNat ∧
52          l'.here = .ref e.rl (e.ol + (e.LCA.getD k default).val.toNat + j) ∧
53          LS e l' i o ∧ l'.bits.toNat = l.bits.toNat - (e.LCA.getD k default).bits.toNat) ∨
54      (∃ B p q, h' = e.heap B p q ∧ l'.againL = false ∧ (q = TYPE → p = msg))) := by
55  have hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size := by rw [hAsz]; exact e.hAsz
56  have hkE : e.LCA[k]'hk = e.LCA.getD k default := by simp [Array.getD_eq_getD_getElem?, hk]
57  have hld : OkOn (e.heap A msg m) (Ptr.load l.here) (e.LCA.getD k default) := by
58    rw [hhere, ← hkE]; exact Ptr.load_ok (e.heap_cget_LCA A msg m) hk
59  have hEbn : (e.LCA.getD k default).bits.toUInt32.toNat = (e.LCA.getD k default).bits.toNat := toNat32 _
60  have hEb64 : (e.LCA.getD k default).bits.toUInt32.toUInt64.toNat = (e.LCA.getD k default).bits.toNat := by simp [toNat32]
61  have hls1 := hls.dropL (e.LCA.getD k default).bits.toUInt32 (by omega) (by omega)
62  rw [dolen_eq_len]
63  dsimp only
64  refine Wp.bindO hld ?_
65  refine Wp.bindO (shr64_ok (x := l.hold) (by omega)) ?_
66  refine Wp.bindO hld ?_
67  generalize e.LCA.getD k default = E at *
68  by_cases hz : (E.op.toUInt32 == 0) = true
69  · simp only [hz, ite_true]
70    refine Wp.bindO hld ?_
71    have hst : store8 l.out E.val.toUInt8 (e.heap A msg m) =
72        .ok ((), e.heap (A.set! o E.val.toUInt8) msg m) := by
73      rw [hls.hout, ← e.heap_put A (A.set! o E.val.toUInt8) msg m]
74      exact Ptr.store_ok (e.heap_bytes_ob A msg m) (e.heap_ro_ob A msg m) (by omega)
75    refine Wp.bindE hst ?_
76    refine Wp.bindO (x := Ptr.ref (BRef.blk e.ob) (o + 1)) ?_ ?_
77    · rw [hls.hout]
78      exact Ptr.add_nat_ok (e.heap_bytes_ob _ msg m) (by simp; omega)
79    · exact Wp.pure' (Or.inr ⟨_, msg, m, rfl, rfl, fun _ => rfl⟩)
80  · have hz' : E.op ≠ 0 := by rw [mask0] at hz; simpa using hz
81    by_cases hb16 : (E.op.toUInt32 &&& 16 != 0) = true
82    · simp only [hz, hb16, ite_true, ite_false, Bool.false_eq_true]
83      have hb16' : E.op &&& 16 ≠ 0 := by rw [mask16] at hb16; simpa using hb16
84      have hbase : (E.op &&& 15).toNat ≤ 5 ∧ 3 ≤ E.val.toNat ∧
85          E.val.toNat + 2 ^ (E.op &&& 15).toNat ≤ 259 := by
86        rcases hcl with h | h
87        · exact False.elim (hb16' h.1.2.1)
88        · rcases h.2 with h0 | h | h
89          · exact False.elim (hz' h0)
90          · exact h.2
91          · exact False.elim (hb16' h.1)
92      refine Wp.bindO hld ?_
93      refine Wp.mono (dolenLen_message_wp hc A msg m
94        { in_ := l.in_, out := l.out, hold := l.hold >>> E.bits.toUInt32.toUInt64, bits := l.bits - E.bits.toUInt32,
95          here := l.here, op := E.op.toUInt32 &&& 15, len := E.val.toUInt32, dist := l.dist, from_ := l.from_,
96          broke := l.broke, againL := false, againD := l.againD }
97        i o s (LS.congr hls1 rfl rfl rfl rfl) hAsz ho hbroke rfl
98        (by rw [mask15]; exact hbase.1) (by simpa [mask15] using hbase.2)
99        hs6 hsi hT (by intro hi; have := hbi2 hi; show 1 ≤ (l.bits - E.bits.toUInt32).toNat
100                       rw [u32_toNat_sub (by omega), hEbn]; omega)) ?_
101      exact fun _ _ h => Or.inr h
102    · have hb16' : E.op &&& 16 = 0 := by rw [mask16] at hb16; simpa using hb16
103      by_cases hb64 : (E.op.toUInt32 &&& 64 == 0) = true
104      · simp only [hz, hb16, hb64, ite_true, ite_false, Bool.false_eq_true]
105        have hb64' : E.op &&& 64 = 0 := by rw [mask64] at hb64; simpa using hb64
106        have hl : LenLink E := ⟨hz', hb16', hb64'⟩
107        have hlk : LinkOK LenLeaf e.LCA e.ol E := by
108          rcases hcl with h | h
109          · exact h.2
110          · rcases h.2 with h0 | h | h
111            · exact False.elim (hz' h0)
112            · exact False.elim (h.1 hb16')
113            · exact False.elim (h.2 hb64')
114        refine Wp.bindO hld ?_
115        have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
116        have hop32 : E.op.toUInt32.toNat < 32 := by rw [toNat32]; have := hlk.2.2.1; omega
117        refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat)) ?_ ?_
118        · rw [hlc]
119          exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol)
120            (n := E.val.toNat) (e.heap_cget_LCA A msg m)
121            (Nat.le_trans (Nat.le_add_right _ _) hlk.2.2.2.1)
122        refine Wp.bindO (shl32_ok hop32) ?_
123        have hlow := hold_low64 (x := l.hold >>> E.bits.toUInt32.toUInt64) (k := E.op.toUInt32) hop32
124        have hjlt : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat < 2 ^ E.op.toNat := by
125          rw [toNat32]; exact Nat.mod_lt _ (Nat.pow_pos (by omega))
126        generalize hjd : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat = j at hlow hjlt
127        refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat + j)) ?_ ?_
128        · rw [hlow]
129          exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol + E.val.toNat)
130            (n := j) (e.heap_cget_LCA A msg m) (by have := hlk.2.2.2.1; omega)
131        refine Wp.pure' (Or.inl ⟨rfl, hbroke, rfl, hl, j, hjlt, rfl,
132          LS.congr hls1 rfl rfl rfl rfl, ?_⟩)
133        rw [u32_toNat_sub (by omega), hEbn]
134      · simp only [hz, hb16, hb64, ite_false, Bool.false_eq_true]
135        by_cases hb32 : (E.op.toUInt32 &&& 32 != 0) = true
136        · simp only [hb32, ite_true]
137          refine Wp.bindE (e.heap_ldstate hc A msg m) ?_
138          refine Wp.bindE (e.heap_stmode hc A msg m TYPE _ rfl) ?_
139          exact Wp.pure' (Or.inr ⟨A, msg, TYPE, rfl, rfl, fun _ => rfl⟩)
140        · simp only [hb32, ite_false, Bool.false_eq_true]
141          obtain ⟨ip, hip⟩ := badData_run hc A msg m "invalid literal/length code" (by decide +kernel)
142          refine Wp.bindE hip ?_
143          exact Wp.pure' (Or.inr ⟨A, .ref (BRef.str ip) 0, BAD, rfl, rfl,
144            fun h => False.elim ((by decide : BAD ≠ TYPE) h)⟩)
145
146/-- The actual `dolen` root/link loop ends after at most two passes. -/
147theorem dolenLoop_message_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
148    (l : L) (i o s kidx : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
149    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
150    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
151    (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat)
152    (hk : kidx < 2 ^ e.s0.lenbits.toNat) (hhere : l.here = .ref e.rl (e.ol + kidx)) :
153    Wp (cdoWhile (dolen c) (fun l => pure (l.againL, l)) l) (e.heap A msg m)
154      (fun l' h' => ∃ B p q, h' = e.heap B p q ∧ l'.againL = false ∧ (q = TYPE → p = msg)) := by
155  have hts := e.hlt
156  obtain ⟨hR, hsz, hall⟩ := hts
157  have hksz : e.ol + kidx < e.LCA.size := by omega
158  have hclass : (LenLink (e.LCA.getD (e.ol + kidx) default) ∧
159      LinkOK LenLeaf e.LCA e.ol (e.LCA.getD (e.ol + kidx) default)) ∨
160      LenLeaf 0 (e.LCA.getD (e.ol + kidx) default) := by
161    have hh := hall kidx hk
162    by_cases hl : LenLink (e.LCA.getD (e.ol + kidx) default)
163    · rw [ite_eq_left hl] at hh; exact Or.inl ⟨hl, hh⟩
164    · rw [ite_eq_right hl] at hh; exact Or.inr hh
165  have hEd0 : (e.LCA.getD (e.ol + kidx) default).bits.toNat + 0 ≤ 15 := by
166    rcases hclass with h | h
167    · exact h.2.1
168    · exact h.1
169  obtain ⟨l1, h1, e1, hq1⟩ := dolen_pass_message_wp hc A msg m l i o s 0 (e.ol + kidx) hls hAsz ho hbroke
170    hs6 hsi hT (by omega) (by intro hi; have := hbi2 hi; omega) hhere hksz (by omega) hEd0 hclass
171  generalize hE0 : e.LCA.getD (e.ol + kidx) default = E0 at hq1 hclass hEd0
172  rcases hq1 with ⟨hag, hbr, hh, hlink, j, hjlt, hhere1, hls1, hb1⟩ | hend
173  · subst hh
174    have hlk : LinkOK LenLeaf e.LCA e.ol E0 := by
175      rcases hclass with h | h
176      · exact h.2
177      · rcases h.2 with h0 | h | h
178        · exact False.elim (hlink.1 h0)
179        · exact False.elim (h.1 hlink.2.1)
180        · exact False.elim (h.2 hlink.2.2)
181    have hleaf := hlk.2.2.2.2 j hjlt
182    have hk2 : e.ol + E0.val.toNat + j < e.LCA.size := by have := hlk.2.2.2.1; omega
183    obtain ⟨l2, h2, e2, hq2⟩ := dolen_pass_message_wp hc A msg m l1 i o s E0.bits.toNat (e.ol + E0.val.toNat + j)
184      hls1 hAsz ho hbr hs6 hsi hT (by omega) (by intro hi; have := hbi2 hi; omega)
185      hhere1 hk2 (by have := hleaf.1; omega) hleaf.1 (Or.inr hleaf)
186    rcases hq2 with ⟨_, _, _, hl2, _⟩ | hend2
187    · rcases hleaf.2 with h0 | h | h
188      · exact False.elim (hl2.1 h0)
189      · exact False.elim (h.1 hl2.2.1)
190      · exact False.elim (h.2 hl2.2.2)
191    · have c1 : (fun l : L => (pure (l.againL, l) : M (Bool × L))) l1 (e.heap A msg m) =
192          .ok ((true, l1), e.heap A msg m) := by simp [hag]
193      have c2 : (fun l : L => (pure (l.againL, l) : M (Bool × L))) l2 h2 =
194          .ok ((false, l2), h2) := by obtain ⟨_, _, _, _, hf, _⟩ := hend2; simp [hf]
195      exact Wp.of_eq (cdoWhile_two e1 c1 e2 c2) hend2
196  · have c1 : (fun l : L => (pure (l.againL, l) : M (Bool × L))) l1 h1 =
197        .ok ((false, l1), h1) := by obtain ⟨_, _, _, _, hf, _⟩ := hend; simp [hf]
198    exact Wp.of_eq (cdoWhile_one e1 c1) hend
199
200/-- Root-table lookup followed by the actual length root/link loop. -/
201theorem dolenRoot_message_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
202    (l : L) (i o s : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
203    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
204    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
205    (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat) :
206    Wp (do
207      let here ← c.lcode.add (l.hold &&& c.lmask.toUInt64).toNat
208      cdoWhile (dolen c) (fun l => pure (l.againL, l)) {l with here})
209      (e.heap A msg m) (fun l' h' => ∃ B p q, h' = e.heap B p q ∧ l'.againL = false ∧ (q = TYPE → p = msg)) := by
210  have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
211  have hR : e.s0.lenbits.toNat < 32 := by have := e.hlt.1; omega
212  have hmask : c.lmask.toUInt64.toNat = 2 ^ e.s0.lenbits.toNat - 1 := by
213    rw [hc.lmask, UInt32.toNat_toUInt64]; exact u32_shl1_sub1 hR
214  have hidx := u64_and_mask (x := l.hold) hmask
215  have hmod : l.hold.toNat % 2 ^ e.s0.lenbits.toNat < 2 ^ e.s0.lenbits.toNat :=
216    Nat.mod_lt _ (Nat.pow_pos (by omega))
217  refine Wp.bindO (x := Ptr.ref e.rl (e.ol + l.hold.toNat % 2 ^ e.s0.lenbits.toNat)) ?_ ?_
218  · rw [hlc, hidx]
219    exact Ptr.add_nat_ok (e.heap_cget_LCA A msg m) (by have := e.hlt.2.1; omega)
220  · exact dolenLoop_message_wp hc A msg m _ i o s _ (LS.congr hls rfl rfl rfl rfl) hAsz ho hbroke
221      hs6 hsi hT hb15 hbi2 hmod rfl
222
223/-- A real fast-body execution that finishes in TYPE keeps the stream's
224original message. This supplements, without changing, the checked StepPost. -/
225theorem inflate_fast_body_type_message (e : Env) (c : Ctx) (A : Array UInt8)
226    (msg : BPtr) (m : UInt32) (l : L) (i o : Nat) (hp : StepPre e c A l i o) :
227    Wp (inflate_fast_body c l) (e.heap A msg m)
228      (fun l' h' => ∃ B p q, h' = e.heap B p q ∧ l'.againL = false ∧ (q = TYPE → p = msg)) := by
229  rcases hp with ⟨hc, hls, hAsz, hi6, ho258, hbroke⟩
230  unfold inflate_fast_body
231  by_cases h1 : l.bits < 15
232  · simp only [h1, ite_true]
233    have hb : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp h1
234    have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
235    refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
236    have hl1 := hls.pullL (by omega) hiin
237    have hb1 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
238    have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
239    have hb1' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
240      simp only [pullL] at hb1 ⊢; omega
241    refine Wp.bindO (pull_run e _ _ (i + 1) o hl1 hb1' hi2 (e.heap_bytes_in A msg m)) ?_
242    have hl2 := hl1.pullL hb1' hi2
243    have hb2 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)))
244      (e.IN.getD (i + 1) 0) (.ref (BRef.blk e.ib) (i + 1 + 1)) hl1.hb
245    exact dolenRoot_message_wp hc A msg m _ (i + 1 + 1) o i hl2 hAsz ho258 hbroke hi6 (by omega) (by omega)
246      (by simp only [pullL] at hb1 hb2 ⊢; omega)
247      (by intro _; simp only [pullL] at hb1 hb2 ⊢; omega)
248  · simp only [h1, ite_false]
249    have hb : 15 ≤ l.bits.toNat := by
250      have : ¬ l.bits.toNat < 15 := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
251      omega
252    exact dolenRoot_message_wp hc A msg m l i o i hls hAsz ho258 hbroke hi6 (by omega) (by omega) hb (by omega)
253
254end Zlib.Inffast.Proofs