inffast.c.distance-semantics.lean

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

1import ZlibF.Spec.InflateFastDistanceSemantics
2import ZlibF.Proof.«inftrees.c.decode.stability-rejection»
3
4/-!
5# Fast distance lookup and independent decoding
6
7The existing fast lookup relation is tied to the same finite two-level
8query as the slow decoder. Constructor-derived flags reconcile acceptance
9before the invariant supplies independent symbol meaning or rejection.
10-/
11
12set_option autoImplicit false
13
14namespace Zlib.Inffast.Proofs
15open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
16open Zlib.Inftrees.Spec Zlib.Inftrees.Spec.DecodeSemantics
17open Zlib.Inftrees.Spec.DecodeSoundness
18open Zlib.Inffast.Spec.DistanceSemantics
19
20/-- Every selected fast distance leaf has the independent meaning of its
21actual table query, including all future-stable rejected prefixes. -/
22theorem distance_lookup_matches_format : Goal.distance_lookup_matches_format := by
23  intro e hold bits input tableUsed lens entry consumed inv stable flags hhold hbits look
24  let root := e.s0.distbits.toNat
25  let idx := hold % 2 ^ root
26  let stream := Sg e hold bits input
27  have rootLe : root ≤ 15 := inv.rootTable.2.1
28  have idxLt : idx < 2 ^ root := Nat.mod_lt _ (Nat.two_pow_pos root)
29  have rootRead : readBits root stream =
30      some (idx, Sg e (hold / 2 ^ root) (bits-root) input) := by
31    exact readBits_bitsOfNat root bits hold (inBits e input) (by omega)
32  obtain ⟨first, firstCell, firstPos, firstBits⟩ := inv.rootTable.2.2.2 idx idxLt
33  have firstGet : e.DCA.getD (e.od + idx) default = first := by
34    simp only [Array.getD_eq_getD_getElem?, firstCell, Option.getD_some]
35  have maskBits (op : UInt8) (hm : op &&& 0xf0 = 0) : op &&& 16 = 0 ∧ op &&& 64 = 0 := by
36    have h16 := congrArg (fun x : UInt8 => x &&& 16) hm
37    have h64 := congrArg (fun x : UInt8 => x &&& 64) hm
38    rw [UInt8.and_assoc] at h16 h64
39    exact ⟨h16, h64⟩
40  have smallMask : ∀ op : UInt8, op.toNat ≤ 15 → op &&& 0xf0 = 0 := by
41    apply u8_forall
42    decide +kernel
43  have selected : tableRead DISTS e.DCA e.od root stream = some (entry, consumed) ∧
44      1 ≤ consumed ∧ consumed ≤ 15 ∧ DistLeaf 0 entry := by
45    rcases look with ⟨hget, hconsumed, noLink⟩ |
46      ⟨E0, j, hget, link, jLt, jEq, hleafGet, hconsumed, codeLe, noLink⟩
47    · change e.DCA.getD (e.od + idx) default = entry at hget
48      have he : first = entry := firstGet.symm.trans hget
49      rw [he] at firstCell firstPos firstBits
50      have invalidMask : entry.op &&& 0xf0 ≠ 0 := by
51        intro hm
52        exact noLink (maskBits entry.op hm)
53      have leaf := e.hdt.2.2 idx idxLt
54      rw [hget, ite_eq_right noLink] at leaf
55      refine ⟨?_, ?_, ?_, leaf⟩
56      · simp only [tableRead, rootRead, bind, Option.bind, firstCell]
57        simp only [show DISTS ≠ LENS by decide, ite_false]
58        simp [invalidMask, hconsumed]
59      · omega
60      · omega
61    · change e.DCA.getD (e.od + idx) default = E0 at hget
62      have he : first = E0 := firstGet.symm.trans hget
63      rw [he] at firstCell firstPos firstBits
64      have linkOK := e.hdt.2.2 idx idxLt
65      rw [hget, ite_eq_left link] at linkOK
66      have opMask : E0.op &&& 0xf0 = 0 := smallMask E0.op linkOK.2.2.1
67      have slowLink : Subtable.IsLink DISTS E0 = true := by
68        simp [Subtable.IsLink, show DISTS ≠ LENS by decide, opMask]
69      obtain ⟨bitsRoot, subSafe⟩ := inv.subtables idx E0 idxLt firstCell slowLink
70      have rootFits : E0.bits.toNat ≤ bits := by omega
71      have opFits : E0.op.toNat ≤ bits - E0.bits.toNat := by have := subSafe.2.2.1; omega
72      have secondRead : readBits E0.op.toNat (stream.drop E0.bits.toNat) =
73          some (j, Sg e ((hold / 2 ^ E0.bits.toNat) / 2 ^ E0.op.toNat)
74            ((bits-E0.bits.toNat)-E0.op.toNat) input) := by
75        rw [show stream.drop E0.bits.toNat = Sg e (hold / 2 ^ E0.bits.toNat) (bits-E0.bits.toNat) input
76          from (Sg_drop hold bits input E0.bits.toNat rootFits).symm]
77        rw [jEq]
78        exact readBits_bitsOfNat E0.op.toNat (bits-E0.bits.toNat) (hold / 2 ^ E0.bits.toNat)
79          (inBits e input) opFits
80      obtain ⟨second, secondCell, secondPos, secondBits⟩ := subSafe.2.2.2.2 j jLt
81      have secondGet : e.DCA.getD (e.od+E0.val.toNat+j) default = second := by
82        simp only [Array.getD_eq_getD_getElem?, secondCell, Option.getD_some]
83      have he : second = entry := secondGet.symm.trans hleafGet
84      rw [he] at secondCell secondPos secondBits
85      have leafD := linkOK.2.2.2.2 j jLt
86      rw [hleafGet] at leafD
87      have leaf : DistLeaf 0 entry := ⟨by have := leafD.1; omega, leafD.2⟩
88      refine ⟨?_, ?_, by omega, leaf⟩
89      · simp only [tableRead, rootRead, bind, Option.bind, firstCell]
90        simp only [show DISTS ≠ LENS by decide, ite_false, opMask, BEq.rfl, ite_true]
91        simp only [secondRead, Option.bind_some, secondCell]
92        simp [hconsumed]
93      · omega
94  obtain ⟨query, positive, codeLe, leaf⟩ := selected
95  have streamLong : 15 ≤ stream.length := by
96    simp only [stream, Sg, List.length_append, bitsOfNat_length]
97    omega
98  have paddedStream : DecodeShort.padded stream = stream := by
99    simp [DecodeShort.padded, Nat.sub_eq_zero_of_le streamLong]
100  have queryPadded : tableRead DISTS e.DCA e.od root (DecodeShort.padded stream) = some (entry,consumed) := by
101    rw [paddedStream]
102    exact query
103  have fit : consumed ≤ stream.length := by omega
104  have compatible := flags stream entry consumed streamLong query
105  refine ⟨query, positive, codeLe, leaf, ?_⟩
106  by_cases hasBase : entry.op &&& 16 ≠ 0
107  · right
108    have accepted : LeafAccepted DISTS entry := by
109      simp only [LeafAccepted, show DISTS ≠ LENS by decide, ite_false]
110      exact compatible hasBase
111    obtain ⟨symbol, valid, meaning, hused, decoded, extended⟩ :=
112      inv.short stream entry consumed queryPadded fit accepted
113    exact ⟨hasBase, symbol, valid, meaning, hused, decoded, extended⟩
114  · left
115    have noBase : entry.op &&& 16 = 0 := by simpa using hasBase
116    have invalid : entry.op &&& 64 ≠ 0 := by
117      rcases leaf.2 with h | h
118      · exact False.elim (hasBase h.1)
119      · exact h.2
120    have rejected : ¬ LeafAccepted DISTS entry := by
121      simpa only [LeafAccepted, show DISTS ≠ LENS by decide, ite_false] using invalid
122    have noValid := Zlib.Inftrees.Proofs.short_rejected_leaf_stays_invalid DISTS e.DCA e.od root tableUsed lens
123      inv stable stream entry consumed queryPadded fit rejected
124    exact ⟨noBase, noValid⟩
125
126end Zlib.Inffast.Proofs