inffast.c.length-semantics.lean

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

1import ZlibF.Spec.InflateFastLengthSemantics
2import ZlibF.Proof.«inftrees.c.decode.stability-rejection»
3
4/-!
5# Fast length 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.LengthSemantics
19
20/-- Every selected fast length leaf has the independent meaning of its
21actual table query, including all future-stable rejected prefixes. -/
22theorem length_lookup_matches_format : Goal.length_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.lenbits.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.LCA.getD (e.ol + 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 LENS e.LCA e.ol root stream = some (entry, consumed) ∧
44      1 ≤ consumed ∧ consumed ≤ 15 ∧ LenLeaf 0 entry := by
45    rcases look with ⟨hget, hconsumed, noLink⟩ |
46      ⟨E0, j, hget, link, jLt, jEq, hleafGet, hconsumed, codeLe, noLink⟩
47    · change e.LCA.getD (e.ol + idx) default = entry at hget
48      have he : first = entry := firstGet.symm.trans hget
49      rw [he] at firstCell firstPos firstBits
50      have slowNoLink : (entry.op != 0 && (entry.op &&& 0xf0) == 0) = false := by
51        by_cases opNonzero : entry.op ≠ 0
52        · have invalidMask : entry.op &&& 0xf0 ≠ 0 := by
53            intro hm
54            exact noLink ⟨opNonzero, maskBits entry.op hm⟩
55          simp [invalidMask]
56        · simp_all
57      have leaf := e.hlt.2.2 idx idxLt
58      rw [hget, ite_eq_right noLink] at leaf
59      refine ⟨?_, ?_, ?_, leaf⟩
60      · simp only [tableRead, rootRead, bind, Option.bind, firstCell]
61        simp only [ite_true]
62        simp [slowNoLink, hconsumed]
63      · omega
64      · omega
65    · change e.LCA.getD (e.ol + idx) default = E0 at hget
66      have he : first = E0 := firstGet.symm.trans hget
67      rw [he] at firstCell firstPos firstBits
68      have linkOK := e.hlt.2.2 idx idxLt
69      rw [hget, ite_eq_left link] at linkOK
70      have opMask : E0.op &&& 0xf0 = 0 := smallMask E0.op linkOK.2.2.1
71      have slowLink : Subtable.IsLink LENS E0 = true := by
72        simp [Subtable.IsLink, link.1, opMask]
73      obtain ⟨bitsRoot, subSafe⟩ := inv.subtables idx E0 idxLt firstCell slowLink
74      have rootFits : E0.bits.toNat ≤ bits := by omega
75      have opFits : E0.op.toNat ≤ bits - E0.bits.toNat := by have := subSafe.2.2.1; omega
76      have secondRead : readBits E0.op.toNat (stream.drop E0.bits.toNat) =
77          some (j, Sg e ((hold / 2 ^ E0.bits.toNat) / 2 ^ E0.op.toNat)
78            ((bits-E0.bits.toNat)-E0.op.toNat) input) := by
79        rw [show stream.drop E0.bits.toNat = Sg e (hold / 2 ^ E0.bits.toNat) (bits-E0.bits.toNat) input
80          from (Sg_drop hold bits input E0.bits.toNat rootFits).symm]
81        rw [jEq]
82        exact readBits_bitsOfNat E0.op.toNat (bits-E0.bits.toNat) (hold / 2 ^ E0.bits.toNat)
83          (inBits e input) opFits
84      obtain ⟨second, secondCell, secondPos, secondBits⟩ := subSafe.2.2.2.2 j jLt
85      have secondGet : e.LCA.getD (e.ol+E0.val.toNat+j) default = second := by
86        simp only [Array.getD_eq_getD_getElem?, secondCell, Option.getD_some]
87      have he : second = entry := secondGet.symm.trans hleafGet
88      rw [he] at secondCell secondPos secondBits
89      have leafD := linkOK.2.2.2.2 j jLt
90      rw [hleafGet] at leafD
91      have leaf : LenLeaf 0 entry := ⟨by have := leafD.1; omega, leafD.2⟩
92      refine ⟨?_, ?_, by omega, leaf⟩
93      · simp only [tableRead, rootRead, bind, Option.bind, firstCell]
94        simp only [ite_true, opMask, BEq.rfl]
95        simp only [secondRead, Option.bind_some, secondCell]
96        simp [hconsumed, link.1]
97      · omega
98  obtain ⟨query, positive, codeLe, leaf⟩ := selected
99  have streamLong : 15 ≤ stream.length := by
100    simp only [stream, Sg, List.length_append, bitsOfNat_length]
101    omega
102  have paddedStream : DecodeShort.padded stream = stream := by
103    simp [DecodeShort.padded, Nat.sub_eq_zero_of_le streamLong]
104  have queryPadded : tableRead LENS e.LCA e.ol root (DecodeShort.padded stream) = some (entry,consumed) := by
105    rw [paddedStream]
106    exact query
107  have fit : consumed ≤ stream.length := by omega
108  have compatible := flags stream entry consumed streamLong query
109  refine ⟨query, positive, codeLe, leaf, ?_⟩
110  have agrees : FastTableFlags.FastLeafAccepted LENS entry ↔ LeafAccepted LENS entry := by
111    rcases leaf.2 with literal | base | invalid
112    · simp [FastTableFlags.FastLeafAccepted, LeafAccepted, literal]
113    · have validFlag := compatible base.1
114      simp [FastTableFlags.FastLeafAccepted, LeafAccepted, base.1, validFlag]
115    · have nonzero : entry.op ≠ 0 := by
116        intro zero
117        simp [zero] at invalid
118      simp [FastTableFlags.FastLeafAccepted, LeafAccepted, nonzero, invalid.1, invalid.2]
119  by_cases accepted : FastTableFlags.FastLeafAccepted LENS entry
120  · right
121    obtain ⟨symbol, valid, meaning, hused, decoded, extended⟩ :=
122      inv.short stream entry consumed queryPadded fit (agrees.mp accepted)
123    exact ⟨accepted, symbol, valid, meaning, hused, decoded, extended⟩
124  · left
125    have rejected : ¬ LeafAccepted LENS entry := fun h => accepted (agrees.mpr h)
126    have noValid := Zlib.Inftrees.Proofs.short_rejected_leaf_stays_invalid LENS e.LCA e.ol root tableUsed lens
127      inv stable stream entry consumed queryPadded fit rejected
128    exact ⟨accepted, noValid⟩
129
130end Zlib.Inffast.Proofs