LZ77HistorySpec.lean

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

1import ZlibF.Spec.Format.Deflate
2
3/-!
4# Retained windows and complete independent output history
5
6The decoder retains only a suffix of earlier bytes. A match reaching no
7farther than that suffix must agree with copying against the full history.
8These are list statements, independent of the heap representation.
9-/
10
11namespace ZlibF.Math.LZ77History
12open ZlibF.Spec
13
14/-- Copying only appends bytes, exactly one for each requested byte. -/
15def Goal.copy_back_extends_history : Prop :=
16  ∀ (dict history : List UInt8) (dist n : Nat),
17    history <+: copyBack dict dist n history ∧
18    (copyBack dict dist n history).length = history.length + n
19
20/-- Physical chunks compose to the same independent bytewise match. -/
21def Goal.copy_back_compose : Prop :=
22  ∀ (dict history : List UInt8) (dist n m : Nat),
23    copyBack dict dist (n + m) history =
24      copyBack dict dist m (copyBack dict dist n history)
25
26/-- When a distance reaches only retained bytes, forgetting older history
27does not change the new output. The suffix relation must be established
28from actual window updates by the enclosing decoder proof. -/
29def Goal.retained_history_agrees : Prop :=
30  ∀ (dict past current saved : List UInt8) (dist n : Nat),
31    saved <:+ (dict ++ past) →
32    0 < dist → dist ≤ saved.length + current.length →
33    copyBack dict dist n (past ++ current) =
34      past ++ copyBack saved dist n current
35
36/-- For a distance within the configured capacity, retaining the complete
37window loses no usable history. A too-far check on the retained bytes is
38then exactly the independent check on the entire preceding history. -/
39def Goal.window_distance_check_agrees : Prop :=
40  ∀ (dict past current : List UInt8) (capacity dist : Nat),
41    dist ≤ capacity →
42    ((((dict ++ past).drop ((dict ++ past).length - capacity)) ++ current).length < dist ↔
43      (dict ++ past ++ current).length < dist)
44
45end ZlibF.Math.LZ77History