LZ77CopySpec.lean

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

1import ZlibF.Spec.Format.Deflate
2import ZlibF.Proof.«inffast.c.copy»
3
4/-!
5# Array copying and the independent LZ77 history operation
6
7The array functions describe bytewise writes. The format's copyBack reads
8from the growing dictionary-plus-output history. These obligations relate
9the two without a heap or an assumption about a translated callee.
10-/
11
12namespace ZlibF.Math.LZ77Copy
13open C ZlibF.Spec
14
15/-- The count output bytes immediately before the current write offset. -/
16def writtenBytes (bytes : Array UInt8) (offset count : Nat) : List UInt8 :=
17  (bytes.toList.drop (offset - count)).take count
18
19/-- A potentially overlapping output copy implements copyBack. The source
20can read bytes written earlier in this same copy. No length-258 bound is
21needed for this heap-free equality. -/
22def Goal.output_copy_refines_lz77 : Prop :=
23  ∀ (dict : List UInt8) (bytes : Array UInt8) (offset count dist n : Nat),
24    count ≤ offset → 0 < dist → dist ≤ count → offset + n ≤ bytes.size →
25    writtenBytes (Zlib.Inffast.Proofs.cpyN n (offset - dist) offset bytes)
26      (offset + n) (count + n) =
27      copyBack dict dist n (writtenBytes bytes offset count)
28
29/-- A saved-window chunk implements copyBack until the source reaches the
30current call's output. The pointwise premise is a relation between array
31data and history; the actual circular-window proof must establish it. -/
32def Goal.window_copy_refines_lz77 : Prop :=
33  ∀ (dict : List UInt8) (bytes window : Array UInt8)
34    (offset count sourceOffset dist n : Nat),
35    count ≤ offset → count < dist → dist ≤ dict.length + count →
36    n ≤ dist - count → offset + n ≤ bytes.size → sourceOffset + n ≤ window.size →
37    (∀ i, i < n → window.getD (sourceOffset + i) 0 =
38      dict.getD (dict.length + count - dist + i) 0) →
39    writtenBytes (Zlib.Inffast.Proofs.blitN window n sourceOffset offset bytes)
40      (offset + n) (count + n) =
41      copyBack dict dist n (writtenBytes bytes offset count)
42
43end ZlibF.Math.LZ77Copy