inffast.c.lp.lean

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

1import ZlibF.Proof.«inffast.c.pass»
2
3namespace Zlib.Inffast.Proofs
4open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
5
6theorem fuel_split2 : ∃ n, fuel = n + 1 + 1 := ⟨fuel - 2, by unfold fuel; omega⟩
7
8theorem cdoWhile_one {σ : Type} {body : σ → M σ} {cond : σ → M (Bool × σ)} {s s1 s1' : σ} {h h1 : Heap}
9    (e1 : body s h = .ok (s1, h1)) (c1 : cond s1 h1 = .ok ((false, s1'), h1)) :
10    cdoWhile body cond s h = .ok (s1', h1) := by
11  obtain ⟨n, hn⟩ := fuel_split2
12  unfold cdoWhile
13  rw [hn]
14  simp [cdoWhile.go, e1, c1]
15
16theorem cdoWhile_two {σ : Type} {body : σ → M σ} {cond : σ → M (Bool × σ)} {s s1 s1' s2 s2' : σ} {h h1 h2 : Heap}
17    (e1 : body s h = .ok (s1, h1)) (c1 : cond s1 h1 = .ok ((true, s1'), h1))
18    (e2 : body s1' h1 = .ok (s2, h2)) (c2 : cond s2 h2 = .ok ((false, s2'), h2)) :
19    cdoWhile body cond s h = .ok (s2', h2) := by
20  obtain ⟨n, hn⟩ := fuel_split2
21  unfold cdoWhile
22  rw [hn]
23  simp [cdoWhile.go, e1, c1, e2, c2]
24
25
26variable {e : Env} {c : Ctx}
27
28theorem DistLeaf_class (d : Nat) (E : Code) (h : DistLeaf d E) : (E.op &&& 16 ≠ 0 ∧ (E.op &&& 15).toNat ≤ 13 ∧ 1 ≤ E.val.toNat) ∨
29    (E.op &&& 16 = 0 ∧ E.op &&& 64 ≠ 0) := h.2
30
31/-- A root entry of the distance table is either a leaf or a link whose second level is in range. -/
32theorem distRoot (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat) (kidx : Nat) (hk : kidx < 2 ^ e.s0.distbits.toNat) :
33    e.od + kidx < e.DCA.size ∧
34    ((DistLink (e.DCA.getD (e.od + kidx) default) → LinkOK DistLeaf e.DCA e.od (e.DCA.getD (e.od + kidx) default)) ∧
35     (¬ DistLink (e.DCA.getD (e.od + kidx) default) → DistLeaf 0 (e.DCA.getD (e.od + kidx) default))) := by
36  obtain ⟨_, hsz, hall⟩ := hts
37  refine ⟨by omega, ?_⟩
38  have := hall kidx hk
39  by_cases hl : DistLink (e.DCA.getD (e.od + kidx) default)
40  · rw [ite_eq_left hl] at this
41    exact ⟨fun _ => this, fun h => absurd hl h⟩
42  · rw [ite_eq_right hl] at this
43    exact ⟨fun h => absurd h hl, fun _ => this⟩
44
45theorem distClass_of (E : Code) (hl : DistLink E → LinkOK DistLeaf e.DCA e.od E) (hn : ¬ DistLink E → DistLeaf 0 E) :
46    DistClass e E := by
47  by_cases h : DistLink E
48  · have := hl h
49    exact Or.inr (Or.inl ⟨h.1, h.2, this.2.1, this.2.2.1, this.2.2.2.1⟩)
50  · have := (hn h).2
51    rcases this with h1 | h1
52    · exact Or.inl h1
53    · exact Or.inr (Or.inr h1)
54
55
56/-- The entry on which a distance lookup ends and the number of bits it consumes, for the hold value `H` and the root
57index `kidx`: a root leaf, or a root link and a leaf of its second level. -/
58def DistLook (e : Env) (H kidx : Nat) (E : Code) (cb : Nat) : Prop :=
59  (e.DCA.getD (e.od + kidx) default = E ∧ cb = E.bits.toNat ∧ ¬ DistLink E) ∨
60  (∃ E0 j, e.DCA.getD (e.od + kidx) default = E0 ∧ DistLink E0 ∧ j < 2 ^ E0.op.toNat ∧
61     j = (H / 2 ^ E0.bits.toNat) % 2 ^ E0.op.toNat ∧ e.DCA.getD (e.od + E0.val.toNat + j) default = E ∧
62     cb = E0.bits.toNat + E.bits.toNat ∧ E0.bits.toNat + E.bits.toNat ≤ 15 ∧ ¬ DistLink E)
63
64theorem dodistLoop_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o kidx : Nat)
65    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat) (hk : kidx < 2 ^ e.s0.distbits.toNat)
66    (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)
67    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
68    (hhere : l.here = .ref e.rd (e.od + kidx)) (hb15 : 15 ≤ l.bits.toNat)
69    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat)) :
70    Wp (cdoWhile (dodist c) (fun l => pure (l.againD, l)) l) (e.heap A msg m) (fun l' h' =>
71      ∃ E cb, cb ≤ 15 ∧ DistLook e l.hold.toNat kidx E cb ∧
72        DistEnd e A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop cb) i o l.len.toNat E l' h') := by
73  obtain ⟨hksz, hlk, hnl⟩ := distRoot hts kidx hk
74  have hcl0 := distClass_of (e := e) _ hlk hnl
75  have hEd0 : (e.DCA.getD (e.od + kidx) default).bits.toNat + 0 ≤ 15 := by
76    by_cases hl : DistLink (e.DCA.getD (e.od + kidx) default)
77    · have := (hlk hl).1; omega
78    · have := (hnl hl).1; omega
79  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
80    (by omega) hEd0 hcl0 (by simpa using hpull)
81  obtain ⟨E0, hE0⟩ : ∃ E0, e.DCA.getD (e.od + kidx) default = E0 := ⟨_, rfl⟩
82  rw [hE0] at hq1 hlk hnl hcl0 hEd0
83  rcases hq1 with ⟨hag, hbr, hh, ⟨hl16, hl64⟩, j, hjlt, hjd, hhere1, hls1, hsg1, hb1, hlen1, hout1, hdist1, hagL1⟩ | ⟨hNL, hag, hend⟩
84  · -- a link: the second pass ends the block
85    subst hh
86    have hlink : DistLink E0 := ⟨hl16, hl64⟩
87    have hlk' := hlk hlink
88    have hleaf := hlk'.2.2.2.2 j hjlt
89    have hk2 : e.od + E0.val.toNat + j < e.DCA.size := by
90      have := hlk'.2.2.2.1; omega
91    have hcl1 : DistClass e (e.DCA.getD (e.od + E0.val.toNat + j) default) := by
92      rcases hleaf.2 with h | h
93      · exact Or.inl h
94      · exact Or.inr (Or.inr h)
95    have hb15' : E0.bits.toNat ≤ 15 := hlk'.1
96    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
97      (by rw [hlen1]; exact hlen) hhere1 hk2 (by have := hleaf.1; omega) (by omega) hcl1 (by
98        rcases hpull with h | h
99        · exact Or.inl h
100        · exact Or.inr ⟨h.1, by omega⟩)
101    rcases hq2 with ⟨hag2, -, -, ⟨hl16', hl64'⟩, -⟩ | hend2
102    · rcases hleaf.2 with h | h
103      · exact absurd hl16' h.1
104      · exact absurd hl64' h.2
105    · 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]
106      have c2 : (fun l : L => (pure (l.againD, l) : M (Bool × L))) l2 h2 = .ok ((false, l2), h2) := by simp [hend2.2.1]
107      have e1' : dodist c l (e.heap A msg m) = .ok (l1, e.heap A msg m) := e1
108      refine Wp.of_eq (cdoWhile_two e1' c1 e2 c2) ?_
109      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, ?_, ?_⟩
110      · refine Or.inr ⟨E0, j, hE0, hlink, hjlt, ?_, rfl, rfl, by have := hleaf.1; omega, ?_⟩
111        · rw [hjd]
112        · intro hl; rcases hleaf.2 with h | h
113          · exact absurd hl.1 h.1
114          · exact absurd hl.2 h.2
115      · have := hend2
116        rw [hlen1] at this
117        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) =
118            ((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
119          rw [List.drop_drop]
120        rw [hd, ← hsg1]
121        exact this
122  · -- the first pass ended the block
123    have c1 : (fun l : L => (pure (l.againD, l) : M (Bool × L))) l1 h1 = .ok ((false, l1), h1) := by simp [hag]
124    refine Wp.of_eq (cdoWhile_one e1 c1) ?_
125    refine ⟨E0, E0.bits.toNat, by omega, Or.inl ⟨hE0, rfl, hNL⟩, ⟨hNL, hag, hend⟩⟩
126
127end Zlib.Inffast.Proofs