InflateFastMatchHistory.lean

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

1import ZlibF.Proof.«inffast.c.match»
2import ZlibF.Proof.«inflate.c.ring»
3import ZlibF.Math.LZ77CopySpec
4
5/-!
6# Fast match copying and chronological history
7
8The fast copier may read two window segments and then overlapping output.
9The result must equal the independent byte-at-a-time copyBack on those
10actual saved bytes. Provenance from earlier calls is a separate invariant.
11-/
12
13namespace Zlib.Inffast.Spec.MatchHistory
14open C Zlib.Inffast Zlib.Inffast.Proofs ZlibF.Math.LZ77Copy
15
16/-- The saved bytes in chronological order at the window's actual base
17offset. No default array access may be selected when the window is used. -/
18def saved (window : Array UInt8) (ws wn wh woff : Nat) : List UInt8 :=
19  (List.range wh).map fun j =>
20    window.getD (woff + Zlib.Inflate.Spec.ringSlot ws wn wh j) 0
21
22/-- All physical branches of the fast array result implement the same
23independent match, including wraparound and overlap into current output.
24An unused window need not have backing storage. -/
25def Goal.match_array_refines_lz77 : Prop :=
26  ∀ (window bytes : Array UInt8) (ws wn wh woff bg o dist len : Nat),
27    wh ≤ ws → wn ≤ ws →
28    (wh ≠ 0 → woff + ws ≤ window.size) →
29    bg ≤ o → o + len ≤ bytes.size → 0 < dist →
30    dist ≤ wh + (o - bg) →
31    writtenBytes (matchArr ws wn woff window bg o dist len bytes)
32      (o + len) (o - bg + len) =
33      ZlibF.Spec.copyBack (saved window ws wn wh woff) dist len
34        (writtenBytes bytes o (o - bg))
35
36/-- Actual source copying is a clean too-far rejection or the independent
37match on saved bytes and current output. The complete old input/bit/link
38frame is retained. This starts at the internal copyMatch cut point. -/
39def Goal.actual_copy_match_refines_lz77 : Prop :=
40  ∀ (e : Env) (c : Ctx) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
41    (l : L) (o : Nat),
42    CtxOK e c →
43    l.out = .ref (.blk e.ob) o → e.bg ≤ o →
44    l.op.toNat = o - e.bg →
45    1 ≤ l.dist.toNat → 3 ≤ l.len.toNat →
46    o + l.len.toNat ≤ bytes.size → l.broke = false →
47    let history := saved e.W e.s0.wsize.toNat e.s0.wnext.toNat e.s0.whave.toNat e.woff
48    let current := writtenBytes bytes o (o - e.bg)
49    if history.length + current.length < l.dist.toNat then
50      ∃ (l' : L) (after : Heap) (p : BPtr),
51        C.run (copyMatch c l) (e.heap bytes msg mode) = .ok (l', after) ∧
52        l'.in_ = l.in_ ∧ l'.hold = l.hold ∧ l'.bits = l.bits ∧
53        l'.againL = l.againL ∧ l'.againD = l.againD ∧
54        l'.broke = true ∧ l'.out = l.out ∧ after = e.heap bytes p BAD
55    else
56      ∃ (l' : L) (after : Heap),
57        C.run (copyMatch c l) (e.heap bytes msg mode) = .ok (l', after) ∧
58        l'.in_ = l.in_ ∧ l'.hold = l.hold ∧ l'.bits = l.bits ∧
59        l'.againL = l.againL ∧ l'.againD = l.againD ∧
60        l'.broke = false ∧ l'.out = .ref (.blk e.ob) (o + l.len.toNat) ∧
61        let result := matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg o
62          l.dist.toNat l.len.toNat bytes
63        after = e.heap result msg mode ∧
64        writtenBytes result (o + l.len.toNat) (o - e.bg + l.len.toNat) =
65          ZlibF.Spec.copyBack history l.dist.toNat l.len.toNat current
66
67end Zlib.Inffast.Spec.MatchHistory