inffast.c.step1.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.env»
2
3namespace Zlib.Inffast.Proofs
4open C Zlib.Inffast Zlib.Inffast.Spec
5
6variable (e : Env)
7
8/-- The locals are consistent with the situation: `in` is at offset `i` of the input block, `out` at offset `o` of the
9output block, both within their windows; the bit buffer holds `bits ≤ 30` bits; and the bits read so far account for
10the bytes consumed (`bits ≤ bits_at_entry + 8 * (i - i0)`). -/
11structure LS (l : L) (i o : Nat) : Prop where
12  hin : l.in_ = .ref (BRef.blk e.ib) i
13  hout : l.out = .ref (BRef.blk e.ob) o
14  hi0 : e.i0 ≤ i
15  hi1 : i ≤ e.i0 + e.sm0.avail_in.toNat
16  ho0 : e.o0 ≤ o
17  hb : l.bits.toNat ≤ 30
18  hH : l.hold.toNat < 2 ^ l.bits.toNat
19  hacc : l.bits.toNat + 8 * e.i0 ≤ e.s0.bits.toNat + 8 * i
20
21/-- `l` after `hold += (unsigned long)(*in++) << bits; bits += 8;` with the byte `x` and the new pointer `p`. -/
22def pullL (l : L) (x : UInt8) (p : BPtr) : L :=
23  { l with in_ := p, hold := l.hold + (x.toUInt64 <<< l.bits.toUInt64), bits := l.bits + 8 }
24
25theorem pullL_bits (l : L) (x p) (hb : l.bits.toNat ≤ 30) : (pullL l x p).bits.toNat = l.bits.toNat + 8 := by
26  unfold pullL; exact u32_toNat_add (by simp [UInt32.toNat_ofNat]; omega)
27
28theorem pullL_hold (l : L) (x p) (hb : l.bits.toNat ≤ 30) (hH : l.hold.toNat < 2 ^ l.bits.toNat) :
29    (pullL l x p).hold.toNat = l.hold.toNat + x.toNat * 2 ^ l.bits.toNat := by
30  unfold pullL
31  have h1 := u64_shl x hb
32  have h2 : l.hold.toNat + x.toNat * 2 ^ l.bits.toNat < 2 ^ 64 := by
33    have hx := UInt8.toNat_lt x
34    have : x.toNat * 2 ^ l.bits.toNat ≤ 255 * 2 ^ 30 := by
35      calc x.toNat * 2 ^ l.bits.toNat ≤ 255 * 2 ^ l.bits.toNat := Nat.mul_le_mul_right _ (by omega)
36        _ ≤ 255 * 2 ^ 30 := Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by omega) hb)
37    have : l.hold.toNat < 2 ^ 30 := Nat.lt_of_lt_of_le hH (Nat.pow_le_pow_right (by omega) hb)
38    omega
39  rw [u64_toNat_add (by rw [h1]; exact h2), h1]
40
41theorem pull_run (h : Heap) (l : L) (i o : Nat) (hl : LS e l i o) (hb : l.bits.toNat ≤ 22)
42    (hi : i < e.i0 + e.sm0.avail_in.toNat) (hIN : h.bytes e.ib = some e.IN) :
43    OkOn h (pull l) (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) := by
44  have hlt : i < e.IN.size := by have := e.hINsz; omega
45  have hg : Space.get h (BRef.blk e.ib) = some e.IN := hIN
46  unfold pull
47  rw [hl.hin]
48  refine OkOn.bind (x := e.IN[i]) (Ptr.load_ok hg hlt) ?_
49  have hadd := Ptr.add_nat_ok (h := h) (r := BRef.blk e.ib) (a := e.IN) (off := i) (n := 1) hg (by omega)
50  refine OkOn.bind (x := Ptr.ref (BRef.blk e.ib) (i + 1)) (by simpa using hadd) ?_
51  have hsh : shl64 e.IN[i].toUInt64 l.bits.toUInt64 = pure (e.IN[i].toUInt64 <<< l.bits.toUInt64) :=
52    shl64_eq (by rw [UInt32.toNat_toUInt64]; omega)
53  rw [hsh]
54  have : e.IN.getD i 0 = e.IN[i] := by simp [Array.getD_eq_getD_getElem?, hlt]
55  rw [this]
56  exact rfl
57
58theorem LS.pull {l : L} {i o : Nat} (hl : LS e l i o) (hb : l.bits.toNat ≤ 22) (hi : i < e.i0 + e.sm0.avail_in.toNat)
59    (x : UInt8) : LS e (pullL l x (.ref (BRef.blk e.ib) (i + 1))) (i + 1) o := by
60  have hb' := pullL_bits l x (.ref (BRef.blk e.ib) (i + 1)) hl.hb
61  have hh' := pullL_hold l x (.ref (BRef.blk e.ib) (i + 1)) hl.hb hl.hH
62  have hx := UInt8.toNat_lt x
63  refine ⟨rfl, hl.hout, by have := hl.hi0; omega, by omega, hl.ho0, by omega, ?_, by have := hl.hacc; omega⟩
64  rw [hh', hb']
65  have h8 : 2 ^ (l.bits.toNat + 8) = 2 ^ l.bits.toNat * 256 := by rw [Nat.pow_add]
66  rw [h8]
67  have := hl.hH
68  have h3 : (x.toNat + 1) * 2 ^ l.bits.toNat ≤ 256 * 2 ^ l.bits.toNat := Nat.mul_le_mul_right _ (by omega)
69  have : (x.toNat + 1) * 2 ^ l.bits.toNat = x.toNat * 2 ^ l.bits.toNat + 2 ^ l.bits.toNat := by simp [Nat.add_mul]
70  omega
71
72end Zlib.Inffast.Proofs