inflate.c.main.table.lean

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

1import ZlibF.Proof.«inflate.c.main.check0»
2
3/-!
4# inflate.c: `case TABLE:` (the counts of a dynamic block header)
5
6`NEEDBITS(14)`, the three fields `HLIT`, `HDIST`, `HCLEN` (5, 5 and 4 bits), the bounds check and the fall-through into
7`LENLENS`. The theorem states the registers, the state record and the bit stream after the mode, and for the error exit
8the message and the heap.
9-/
10
11namespace Zlib.Inflate.Proofs
12open C Zlib.Inflate Zlib.Inflate.Spec
13
14theorem tcMask5 : ((1 : UInt32) <<< (5 : UInt32) - 1) = 31 := by decide
15theorem tcMask4 : ((1 : UInt32) <<< (4 : UInt32) - 1) = 15 := by decide
16
17theorem tcBITS5_run (l : IL) (h : Heap) : runX (BITS 5) l h = .ok ((.ok (l.hold.toUInt32 &&& 31), l), h) := by
18  rw [BITS_run l h 5 (by decide), tcMask5]
19
20theorem tcBITS4_run (l : IL) (h : Heap) : runX (BITS 4) l h = .ok ((.ok (l.hold.toUInt32 &&& 15), l), h) := by
21  rw [BITS_run l h 4 (by decide), tcMask4]
22
23theorem tcDROP5_run (l : IL) (h : Heap) :
24    runX (DROPBITS 5) l h = .ok ((.ok (), { l with hold := l.hold >>> 5, bits := l.bits - 5 }), h) := by
25  rw [DROPBITS_run l h 5 (by decide)]; rfl
26
27theorem tcDROP4_run (l : IL) (h : Heap) :
28    runX (DROPBITS 4) l h = .ok ((.ok (), { l with hold := l.hold >>> 4, bits := l.bits - 4 }), h) := by
29  rw [DROPBITS_run l h 4 (by decide)]; rfl
30
31/-- The state record after the three fields of the header are read. -/
32def tableCounts (s : InflateState) (hold : UInt64) : InflateState :=
33  { s with nlen := (hold.toUInt32 &&& 31) + 257, ndist := ((hold >>> 5).toUInt32 &&& 31) + 1,
34           ncode := ((hold >>> 5 >>> 5).toUInt32 &&& 15) + 4 }
35
36/-- The registers after the three `DROPBITS` of `TABLE`. -/
37def tableRegs (l : IL) : IL := { l with hold := l.hold >>> 14, bits := l.bits - 14 }
38
39theorem tcShr14 (x : UInt64) : x >>> 5 >>> 5 >>> 4 = x >>> 14 := by
40  apply UInt64.toNat_inj.mp
41  simp [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow, Nat.div_div_eq_div_mul]
42
43theorem tcSub14 (b : UInt32) : b - 5 - 5 - 4 = b - 14 := by
44  apply UInt32.toNat_inj.mp
45  simp [UInt32.toNat_sub]
46  omega
47
48/-- `case TABLE:`. `NEEDBITS(14)`; if the input ran out, `goto inf_leave` with the registers of that moment. Else the three
49fields are read from the low bits of `hold`: `nlen = BITS(5) + 257`, `ndist = BITS(5) + 1`, `ncode = BITS(4) + 4`, `14` bits
50are dropped (`tableRegs`); if `nlen > 286` or `ndist > 30` the error "too many length or distance symbols" (`BAD`, `break`);
51else `have = 0`, `mode = LENLENS` and the fall-through into `LENLENS` (the theorems `inflate_LENLENS_*`). -/
52theorem inflate_TABLE_run {c : Ctx} {l : IL} {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState}
53    {bs : List UInt8} (hr : c.strm = some r) (hc : c.st = some (.tab zs)) (hz : r.get h = some z)
54    (hs : h.istates zs = some s) (B : BitInv h l bs) :
55    ∃ rr l' j, runX (NEEDBITS 14) l h = .ok ((rr, l'), h) ∧ j ≤ bs.length ∧ BitInv h l' (bs.drop j) ∧
56      stream l' (bs.drop j) = stream l bs ∧
57      (rr = .error Ex.leave → l'.have_ = 0 ∧ j = bs.length ∧ l'.bits.toNat < 14 ∧
58        runX (inflate_TABLE c) l h = .ok ((.error Ex.leave, l'), h)) ∧
59      (rr = .ok () → 14 ≤ l'.bits.toNat ∧ BitInv h (tableRegs l') (bs.drop j) ∧
60        stream (tableRegs l') (bs.drop j) = (stream l bs).drop 14 ∧
61        ((tableCounts s l'.hold).nlen > 286 ∨ (tableCounts s l'.hold).ndist > 30 →
62          ∃ i, strTable[i]? = some "too many length or distance symbols" ∧
63            runX (inflate_TABLE c) l h = .ok ((.ok (), tableRegs l'), tcBadHeap h r zs z (tableCounts s l'.hold) i)) ∧
64        (¬ ((tableCounts s l'.hold).nlen > 286 ∨ (tableCounts s l'.hold).ndist > 30) →
65          runX (inflate_TABLE c) l h = runX (inflate_LENLENS c) (tableRegs l')
66            (setI h zs { tableCounts s l'.hold with «have» := 0, mode := LENLENS }))) := by
67  obtain ⟨rr, l', j, hrun, hj, B', hS', hbits, hshape, hmax, hid, hok, hleave⟩ := NEEDBITS_run B 14 (by decide)
68  have hdrop : tableRegs l' = { l' with hold := l'.hold >>> 5 >>> 5 >>> 4, bits := l'.bits - 5 - 5 - 4 } := by
69    simp [tableRegs, tcShr14, tcSub14]
70  refine ⟨rr, l', j, hrun, hj, B', hS', ?_, ?_⟩
71  · intro e
72    obtain ⟨h1, h2, h3⟩ := hleave e
73    refine ⟨h2, h1, h3, ?_⟩
74    unfold inflate_TABLE
75    simp [runX_bind, hrun, e, runX_throw]
76  · intro e
77    have h14 : 14 ≤ l'.bits.toNat := hok e
78    obtain ⟨hB1, hS1, hsub⟩ := DROPBITS_inv B' 14 h14 (by decide)
79    have hreg : tableRegs l' = { l' with hold := l'.hold >>> (14 : UInt32).toUInt64, bits := l'.bits - 14 } := rfl
80    refine ⟨h14, by rw [hreg]; exact hB1, by rw [hreg, hS1, hS']; rfl, ?_, ?_⟩
81    · intro hbad
82      have hz2 : r.get (setI h zs (tableCounts s l'.hold)) = some z := by simpa using hz
83      obtain ⟨i, hi, hbm⟩ := tcBadMode_run (c := c) "too many length or distance symbols" lit_many_symbols hr hc
84        (h := setI h zs (tableCounts s l'.hold)) (z := z) (s := tableCounts s l'.hold) hz2 (by simp)
85      refine ⟨i, hi, ?_⟩
86      have hbm2 : badMode c "too many length or distance symbols" (setI h zs (tableCounts s l'.hold)) =
87          .ok ((), tcBadHeap h r zs z (tableCounts s l'.hold) i) := by
88        rw [hbm]; simp [tcBadHeap, hz]
89      unfold inflate_TABLE
90      rw [hc, hdrop]
91      have hbad' : (286 : UInt32) < (l'.hold.toUInt32 &&& 31) + 257 ∨ (30 : UInt32) < ((l'.hold >>> 5).toUInt32 &&& 31) + 1 := by
92        simpa [tableCounts, gt_iff_lt] using hbad
93      simp [tableCounts] at hbm2
94      simp [runX_bind, runX_lift, ldI_eq, hs, hrun, e, tcBITS5_run, tcBITS4_run, tcDROP5_run, tcDROP4_run, wrI_eq, tableCounts,
95        hbad', runX_pure, setI_setI, hbm2]
96    · intro hn
97      have hn' : ¬ ((286 : UInt32) < (l'.hold.toUInt32 &&& 31) + 257 ∨ (30 : UInt32) < ((l'.hold >>> 5).toUInt32 &&& 31) + 1) := by
98        simpa [tableCounts, gt_iff_lt] using hn
99      unfold inflate_TABLE
100      rw [hc, hdrop]
101      simp [runX_bind, runX_lift, ldI_eq, hs, hrun, e, tcBITS5_run, tcBITS4_run, tcDROP5_run, tcDROP4_run, wrI_eq, tableCounts,
102        hn', runX_pure, setI_setI]
103
104end Zlib.Inflate.Proofs