inffast.c.pass.lean

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

1import ZlibF.Proof.«inffast.c.dist»
2
3namespace Zlib.Inffast.Proofs
4open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
5
6variable {e : Env} {c : Ctx}
7
8set_option maxHeartbeats 1000000 in
9/-- One pass of the block at `dodist:`. Either it follows a link (`againD`), or it ends the distance block. -/
10theorem dodist_pass (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o d k : Nat)
11    (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)
12    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
13    (hhere : l.here = .ref e.rd k) (hk : k < e.DCA.size)
14    (hEb : (e.DCA.getD k default).bits.toNat ≤ l.bits.toNat)
15    (hEd : (e.DCA.getD k default).bits.toNat + d ≤ 15)
16    (hcl : DistClass e (e.DCA.getD k default))
17    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat + d)) :
18    Wp (dodist c l) (e.heap A msg m) (fun l' h' =>
19      (l'.againD = true ∧ l'.broke = false ∧ h' = e.heap A msg m ∧
20        ((e.DCA.getD k default).op &&& 16 = 0 ∧ (e.DCA.getD k default).op &&& 64 = 0) ∧
21        ∃ j, j < 2 ^ (e.DCA.getD k default).op.toNat ∧
22          j = (l.hold.toNat / 2 ^ (e.DCA.getD k default).bits.toNat) % 2 ^ (e.DCA.getD k default).op.toNat ∧
23          l'.here = .ref e.rd (e.od + (e.DCA.getD k default).val.toNat + j) ∧ LS e l' i o ∧
24          Sg e l'.hold.toNat l'.bits.toNat i = (Sg e l.hold.toNat l.bits.toNat i).drop (e.DCA.getD k default).bits.toNat ∧
25          l'.bits.toNat = l.bits.toNat - (e.DCA.getD k default).bits.toNat ∧
26          l'.len = l.len ∧ l'.out = l.out ∧ l'.dist = l.dist ∧ l'.againL = l.againL) ∨
27      DistEnd e A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop (e.DCA.getD k default).bits.toNat) i o l.len.toNat
28        (e.DCA.getD k default) l' h') := by
29  have hkE : e.DCA[k]'hk = e.DCA.getD k default := by simp [Array.getD_eq_getD_getElem?, hk]
30  have hld : OkOn (e.heap A msg m) (Ptr.load l.here) (e.DCA.getD k default) := by
31    rw [hhere, ← hkE]; exact Ptr.load_ok (e.heap_cget_DCA A msg m) hk
32  have hEb64 : (((e.DCA.getD k default).bits.toUInt32).toUInt64).toNat = (e.DCA.getD k default).bits.toNat := by
33    simp [toNat32]
34  have hEbn : ((e.DCA.getD k default).bits.toUInt32).toNat = (e.DCA.getD k default).bits.toNat := toNat32 _
35  have hls1 : LS e (dropL l (e.DCA.getD k default).bits.toUInt32) i o :=
36    hls.dropL _ (by omega) (by omega)
37  have hEb64 : (((e.DCA.getD k default).bits.toUInt32).toUInt64).toNat = (e.DCA.getD k default).bits.toNat := by
38    simp [toNat32]
39  have hEbn : ((e.DCA.getD k default).bits.toUInt32).toNat = (e.DCA.getD k default).bits.toNat := toNat32 _
40  have hls1 : LS e (dropL l (e.DCA.getD k default).bits.toUInt32) i o :=
41    hls.dropL _ (by omega) (by omega)
42  have hsg1 := Sg_dropL (e := e) l (e.DCA.getD k default).bits.toUInt32 i (by omega) (by omega)
43  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
44    intro x _; rw [u64_shr (by omega), hEbn]
45  unfold dodist
46  dsimp only
47  refine Wp.bindO hld ?_
48  refine Wp.bindO (shr64_ok (x := l.hold) (by omega)) ?_
49  refine Wp.bindO hld ?_
50  generalize e.DCA.getD k default = E at *
51  have hsg1' : Sg e (l.hold >>> E.bits.toUInt32.toUInt64).toNat (l.bits - E.bits.toUInt32).toNat i =
52      (Sg e l.hold.toNat l.bits.toNat i).drop E.bits.toNat := by
53    have := hsg1; rw [hEbn] at this; exact this
54  by_cases hb16 : (E.op.toUInt32 &&& 16 != 0) = true
55  · simp only [hb16, ite_true]
56    have hb16' : E.op &&& 16 ≠ 0 := by
57      rw [mask16] at hb16; simpa using hb16
58    have hbase : E.op &&& 16 ≠ 0 ∧ ((E.op &&& 15).toNat ≤ 13) ∧ 1 ≤ E.val.toNat := by
59      rcases hcl with h | h | h
60      · exact h
61      · exact absurd h.1 hb16'
62      · exact absurd h.1 hb16'
63    refine Wp.bindO hld ?_
64    have hv : E.val.toUInt32.toNat = E.val.toNat := by simp
65    have hv2 := UInt16.toNat_lt E.val
66    have hbn := dropL_bits l E.bits.toUInt32 (by omega)
67    have key := (dodistBase_wp hc A msg m
68      { in_ := l.in_, out := l.out, hold := l.hold >>> E.bits.toUInt32.toUInt64, bits := l.bits - E.bits.toUInt32,
69        here := l.here, op := E.op.toUInt32 &&& 15, len := l.len, dist := E.val.toUInt32, from_ := l.from_,
70        broke := l.broke, againL := l.againL, againD := false } i o (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb
71      (by rw [mask15]; exact hbase.2.1) (by rw [hv]; exact hbase.2.2) (by rw [hv]; omega) hlen hbroke
72      (by rcases hpull with h | h
73          · exact Or.inl h
74          · refine Or.inr ⟨h.1, ?_⟩
75            show 5 ≤ (l.bits - E.bits.toUInt32).toNat
76            have hbn' : (l.bits - E.bits.toUInt32).toNat = l.bits.toNat - E.bits.toNat := by
77              rw [u32_toNat_sub (by omega), hEbn]
78            omega))
79    unfold dodistBase distCont at key
80    dsimp only at key
81    refine Wp.mono key ?_
82    intro l' h' hq
83    obtain ⟨i', xv, rest, hi1, hi2, hr, hagD, hres⟩ := hq
84    refine Or.inr ⟨fun hl => hb16' hl.1, hagD, ?_⟩
85    rcases hres with ⟨hb, hls', hsg, hh⟩ | ⟨hb, hls', p, hh⟩
86    · refine Or.inl ⟨i', xv, rest, hi1, hi2, ?_, hb, hls', hsg, ?_⟩
87      · have : (E.op.toUInt32 &&& 15).toNat = (E.op &&& 15).toNat := mask15 _
88        rw [this] at hr
89        rw [hsg1'] at hr
90        exact hr
91      · rw [hh]; simp only [hv]
92    · exact Or.inr ⟨i', p, hi1, hi2, hb, hls', hh⟩
93  · -- not a base: a link or an invalid code
94    have hb16' : E.op &&& 16 = 0 := by
95      rw [mask16] at hb16; simpa using hb16
96    by_cases hb64 : (E.op.toUInt32 &&& 64 == 0) = true
97    · simp only [hb16, hb64, ite_true, ite_false, Bool.false_eq_true]
98      have hb64' : E.op &&& 64 = 0 := by
99        rw [mask64] at hb64; simpa using hb64
100      have hlink : 1 ≤ E.op.toNat ∧ E.op.toNat ≤ 15 ∧ e.od + E.val.toNat + 2 ^ E.op.toNat ≤ e.DCA.size := by
101        rcases hcl with h | h | h
102        · exact absurd hb16' h.1
103        · exact ⟨h.2.2.1, h.2.2.2.1, h.2.2.2.2⟩
104        · exact absurd hb64' h.2
105      refine Wp.bindO hld ?_
106      have hdc : c.dcode = .ref e.rd e.od := by rw [hc.dcode]; exact e.hdc
107      have hop32 : E.op.toUInt32.toNat < 32 := by rw [toNat32]; omega
108      refine Wp.bindO (x := Ptr.ref e.rd (e.od + E.val.toNat)) ?_ ?_
109      · rw [hdc]
110        exact Ptr.add_nat_ok (e.heap_cget_DCA A msg m) (Nat.le_trans (Nat.le_add_right _ _) hlink.2.2)
111      refine Wp.bindO (shl32_ok hop32) ?_
112      have hlow := hold_low64 (x := l.hold >>> E.bits.toUInt32.toUInt64) (k := E.op.toUInt32) hop32
113      have hjlt : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat < 2 ^ E.op.toNat := by
114        rw [toNat32]; exact Nat.mod_lt _ (Nat.pow_pos (by omega))
115      generalize hjd : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat = j at hlow hjlt
116      refine Wp.bindO (x := Ptr.ref e.rd (e.od + E.val.toNat + j)) ?_ ?_
117      · rw [hlow]
118        exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rd) (a := e.DCA) (off := e.od + E.val.toNat)
119          (n := j) (e.heap_cget_DCA A msg m) (by have := hlink.2.2; omega)
120      refine Wp.pure' (Or.inl ⟨rfl, hbroke, rfl, ⟨hb16', hb64'⟩, j, hjlt, by rw [← hjd, u64_shr (by omega), hEbn, toNat32],  rfl, LS.congr hls1 rfl rfl rfl rfl, hsg1',
121        (by show (l.bits - E.bits.toUInt32).toNat = _; rw [u32_toNat_sub (by omega), hEbn]), rfl, rfl, rfl, rfl⟩)
122    · simp only [hb16, hb64, ite_false, Bool.false_eq_true]
123      obtain ⟨ip, hip⟩ := badData_run hc A msg m "invalid distance code" (by decide +kernel)
124      refine Wp.bindE hip (Wp.pure' (Or.inr ⟨fun hl => (by rw [mask64] at hb64; simpa using hb64 : E.op &&& 64 ≠ 0) hl.2, rfl, Or.inr ⟨i, Ptr.ref (BRef.str ip) 0, Nat.le_refl _, by omega, rfl,
125        LS.congr hls1 rfl rfl rfl rfl, rfl⟩⟩))
126
127end Zlib.Inffast.Proofs