InflateFastDistanceResult.lean

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

1import ZlibF.Spec.InflateFastDistanceSemantics
2import ZlibF.Spec.InflateFastMatchHistory
3import ZlibF.Spec.InflateFast
4
5/-!
6# Independent symbol and copy meaning of the actual distance block
7
8All input is retained. A rejected symbol, a too-far match and a successful
9match have distinct results. The saved history is the actual window data;
10its provenance from earlier public calls remains a separate obligation.
11-/
12
13namespace Zlib.Inffast.Spec.DistanceResult
14open C Zlib.Inffast Zlib.Inffast.Proofs ZlibF.Spec
15open Zlib.Inftrees Zlib.Inftrees.Spec
16open ZlibF.Math.LZ77Copy
17
18/-- Physical copying after the distance extras have been consumed. Both
19branches preserve the exact remaining input, including a too-far error. -/
20def CopyOutcome (e : Env) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
21    (source : List Bool) (output len distance : Nat) (l' : L) (after : Heap) : Prop :=
22  let history := MatchHistory.saved e.W e.s0.wsize.toNat e.s0.wnext.toNat
23    e.s0.whave.toNat e.woff
24  let current := writtenBytes bytes output (output - e.bg)
25  if history.length + current.length < distance then
26    ∃ input' errorMsg,
27      l'.broke = true ∧ LS e l' input' output ∧
28      Sg e l'.hold.toNat l'.bits.toNat input' = source ∧
29      after = e.heap bytes errorMsg BAD
30  else
31    ∃ input',
32      let result := matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg output
33        distance len bytes
34      l'.broke = false ∧ LS e l' input' (output + len) ∧
35      Sg e l'.hold.toNat l'.bits.toNat input' = source ∧
36      after = e.heap result msg mode ∧
37      writtenBytes result (output + len) (output - e.bg + len) =
38        copyBack history distance len current
39
40/-- Physical leaf dispatch, before relating the selected entry to an
41independent symbol. This is a result to prove about the actual source,
42not a callee contract assumed by the distance-block goal. -/
43def PhysicalOutcome (e : Env) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
44    (source : List Bool) (output len : Nat) (entry : Code) (consumed : Nat)
45    (l' : L) (after : Heap) : Prop :=
46  (entry.op &&& 16 = 0 ∧
47    ∃ input' errorMsg,
48      l'.broke = true ∧ LS e l' input' output ∧
49      Sg e l'.hold.toNat l'.bits.toNat input' = source.drop consumed ∧
50      after = e.heap bytes errorMsg BAD) ∨
51  (entry.op &&& 16 ≠ 0 ∧
52    ∃ extra rest,
53      readBits (entry.op &&& 15).toNat (source.drop consumed) = some (extra, rest) ∧
54      CopyOutcome e bytes msg mode rest output len (entry.val.toNat + extra) l' after)
55
56/-- The complete distance result, including the exact remaining source
57bits on both errors. A successful copy equals independent bytewise LZ77
58copying on the actual saved window and current output. -/
59def Outcome (e : Env) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
60    (l : L) (input output : Nat) (lens : List Nat) (entry : Code) (consumed : Nat)
61    (l' : L) (after : Heap) : Prop :=
62  let source := Sg e l.hold.toNat l.bits.toNat input
63  let history := MatchHistory.saved e.W e.s0.wsize.toNat e.s0.wnext.toNat
64    e.s0.whave.toNat e.woff
65  let current := writtenBytes bytes output (output - e.bg)
66  (entry.op &&& 16 = 0 ∧
67    (∀ more : List Bool,
68      ¬ ∃ (symbol : Nat) (rest : List Bool),
69        decodeSym lens (source ++ more) = some (symbol, rest) ∧ symbol ≤ 29) ∧
70    ∃ input' errorMsg,
71      l'.broke = true ∧ LS e l' input' output ∧
72      Sg e l'.hold.toNat l'.bits.toNat input' = source.drop consumed ∧
73      after = e.heap bytes errorMsg BAD) ∨
74  (entry.op &&& 16 ≠ 0 ∧
75    ∃ symbol extra codeRest rest,
76      symbol ≤ 29 ∧ DecodeSemantics.SymbolEntry DISTS symbol entry ∧
77      consumed = lens.getD symbol 0 ∧
78      decodeSym lens source = some (symbol, codeRest) ∧
79      readBits (distExtras.getD symbol 0) codeRest = some (extra, rest) ∧
80      let distance := distBases.getD symbol 0 + extra
81      if history.length + current.length < distance then
82        ∃ input' errorMsg,
83          l'.broke = true ∧ LS e l' input' output ∧
84          Sg e l'.hold.toNat l'.bits.toNat input' = rest ∧
85          after = e.heap bytes errorMsg BAD
86      else
87        ∃ input',
88          let result := matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg output
89            distance l.len.toNat bytes
90          l'.broke = false ∧ LS e l' input' (output + l.len.toNat) ∧
91          Sg e l'.hold.toNat l'.bits.toNat input' = rest ∧
92          after = e.heap result msg mode ∧
93          writtenBytes result (output + l.len.toNat) (output - e.bg + l.len.toNat) =
94            copyBack history distance l.len.toNat current)
95
96/-- Every actual distance-block exit retains the old execution result and
97has its independent symbol/copy meaning. Internal table data facts must
98still be established by actual construction. No callee contract or input
99validity is a hypothesis. The physical domain is the existing distance
100block's safety domain, not a restriction added to the public API. -/
101def Goal.actual_distance_refines_lz77 : Prop :=
102  ∀ (e : Env) (c : Ctx) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
103    (l : L) (input output tableUsed : Nat) (lens : List Nat),
104    CtxOK e c → LS e l input output →
105    e.o0 + e.sm0.avail_out.toNat ≤ bytes.size →
106    output + 258 ≤ e.o0 + e.sm0.avail_out.toNat → bytes.size < 2 ^ 63 →
107    l.broke = false → (3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258) →
108    15 ≤ l.bits.toNat →
109    (input + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨
110      (input + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat)) →
111    DecodeTableInvariant.Inv DISTS e.DCA e.od e.s0.distbits.toNat tableUsed lens →
112    DecodeTableStability.StableQuery DISTS e.DCA e.od e.s0.distbits.toNat →
113    FastTableFlags.QueryCompatible DISTS e.DCA e.od e.s0.distbits.toNat →
114    ∃ (l' : L) (after : Heap) (entry : Code) (consumed : Nat),
115      C.run (dolenDist c l) (e.heap bytes msg mode) = .ok (l', after) ∧
116      consumed ≤ 15 ∧
117      DistLook e l.hold.toNat (l.hold.toNat % 2 ^ e.s0.distbits.toNat) entry consumed ∧
118      DistEnd e bytes msg mode
119        ((Sg e l.hold.toNat l.bits.toNat input).drop consumed)
120        input output l.len.toNat entry l' after ∧
121      Outcome e bytes msg mode l input output lens entry consumed l' after
122
123end Zlib.Inffast.Spec.DistanceResult