精确证明目标

这些约定描述完整调用序列，以及初始化能够建立的有效状态。每项都可以继续进入相关定义；证明进度见进度页。

调用序列

/-- All legal public histories are safe and retain cleanup. For ordinary data epochs every
input/output split is covered, including allocation failures and dictionary handshakes.
Completion is stated against the independent byte-format relation. -/
def Goal.inflate_sequence : Prop :=
  StreamSequenceSafety .inflate ∧
  (∀ wb wrap bits r h log, Api.inflWbits wb.toInt = some (wrap, bits) →
    InflateDataTrace wb r h log →
    (log.singleDictionary = true → log.result = Z_STREAM_END →
      Api.Layer.Decodes wrap bits log.dictionary log.input log.output) ∧
    (∀ source decoded, Api.Layer.Decodes wrap bits log.dictionary source decoded →
      log.singleDictionary = true → Api.FullWindow wrap bits source → log.input <+: source →
      log.output <+: decoded ∧ log.result ≠ Z_DATA_ERROR ∧
      (log.result = Z_STREAM_END → log.input = source ∧ log.output = decoded))) ∧
  InflateCompletes

/-- All legal public histories are safe and retain cleanup. A finished ordinary data epoch
encodes exactly its accepted input, for every accepted parameter set and flush schedule. -/
def Goal.deflate_sequence : Prop :=
  StreamSequenceSafety .deflate ∧
  (∀ level method wb mem strategy p r h log,
    Api.deflInit? level.toInt method.toInt wb.toInt mem.toInt strategy.toInt = some p →
    DeflateDataTrace level method wb mem strategy r h log →
    log.result = Z_STREAM_END → DecodesFor p log.dictionary log.output log.input) ∧
  DeflateCompletes

/-- Includes actual callback execution and raw-format delivery, re-use of the window, and
complete end cleanup. Callback memory and returning/finite-input obligations remain explicit. -/
def Goal.inflate_back_sequence : Prop :=
  Goal.inflateBack ∧
  (∀ h r i window n, BackReachable h r i window n →
    (∃ z s, BackValid h r i z s ∧ s.window = window ∧ s.wsize.toNat = n) ∧
    ∃ after z, C.run (Zlib.Infback.inflateBackEnd (some r)) h = .ok (Z_OK, after) ∧
      r.get after = some z ∧ z.state = none ∧
      Frame h after (fun b => StreamRoot r b ∨ b = i) ∧
      LiveChange h after (fun _ => False) (fun b => b = i))

/-- The gz lifecycle includes every admitted operation, external file growth and final close.
The per-entry read contracts express transparent/concatenated-member decoding and the
per-entry write contracts account for accepted bytes and seek zeros. -/
def Goal.gz_sequence : Prop :=
  (∀ h fs i, GzReachable h fs i → FileSystem fs ∧ ∃ s, GzValid h i s) ∧
  (∀ h fs i s call, GzReachable h fs i → h.gzstates i = some s →
    GzOperation i call → GzArguments h i s call →
    ∃ value fs' after s', call.execute fs h = .ok ((value, fs'), after) ∧
      GzValid after i s' ∧ FileSystem fs' ∧
      LiveChange h after
        (fun b => GzOwned after i s' b ∧ ¬ h.live b)
        (fun b => GzOwned h i s b ∧ ¬ GzOwned after i s' b)) ∧
  (∀ h fs i s, GzReachable h fs i → h.gzstates i = some s →
    ∃ rc fs' after, Zlib.Gzclose.gzclose (some (.in_gzstate_x i)) fs h = .ok ((rc, fs'), after) ∧
      CloseEffects h after fs fs' i s) ∧
  Goal.gzread ∧ Goal.gzfread ∧ Goal.gzgetc ∧ Goal.gzgets ∧
  Goal.gzwrite ∧ Goal.gzfwrite ∧ Goal.gzflush ∧ Goal.gzclose ∧ GzWriterFormat

初始化定义域

/-- Every accepted signed window parameter has a non-failing init on every permitted heap.
The fixed witness additionally rules out an empty caller domain. -/
def Goal.inflate_initialisation_domain : Prop :=
  (∀ h r version wb wrap bits,
    InitDomain h r version → Api.inflWbits wb.toInt = some (wrap, bits) →
    h.allocOk h.nalloc = true →
    ∃ after, C.run (Zlib.Inflate.inflateInit2_ (some r) wb version 112) h = .ok (Z_OK, after) ∧
      InflateInitial h after r wrap bits ∧ StreamReachable .inflate after r) ∧
  InitDomain witnessHeap (.tab 0) (.ref (.blk 1) 0) ∧
  (∀ wb wrap bits, Api.inflWbits wb.toInt = some (wrap, bits) →
    ∃ after, C.run (Zlib.Inflate.inflateInit2_ (some (.tab 0)) wb (.ref (.blk 1) 0) 112)
      witnessHeap = .ok (Z_OK, after) ∧ InflateInitial witnessHeap after (.tab 0) wrap bits)

/-- Full level, method, window, memory-level and strategy coverage, including normalisation.
No assumption that the post-init invariant already holds is permitted. -/
def Goal.deflate_initialisation_domain : Prop :=
  (∀ h r version level method wb mem strategy p,
    InitDomain h r version →
    Api.deflInit? level.toInt method.toInt wb.toInt mem.toInt strategy.toInt = some p →
    (∀ j, j < 5 → h.allocOk (h.nalloc + j) = true) →
    ∃ after, C.run (Zlib.Deflate.deflateInit2_ (some r) level method wb mem strategy version 112) h =
      .ok (Z_OK, after) ∧ DeflateInitial h after r p ∧ StreamReachable .deflate after r) ∧
  InitDomain witnessHeap (.tab 0) (.ref (.blk 1) 0) ∧
  (∀ level method wb mem strategy p,
    Api.deflInit? level.toInt method.toInt wb.toInt mem.toInt strategy.toInt = some p →
    ∃ after, C.run (Zlib.Deflate.deflateInit2_ (some (.tab 0)) level method wb mem strategy
      (.ref (.blk 1) 0) 112) witnessHeap = .ok (Z_OK, after) ∧
      DeflateInitial witnessHeap after (.tab 0) p)

/-- All eight documented callback-window sizes, with an arbitrary valid caller window.
Init establishes the back-decoder invariant and retains ownership of the window. -/
def Goal.inflate_back_initialisation_domain : Prop :=
  (∀ h r version wb window,
    InitDomain h r version → 8 ≤ wb.toInt → wb.toInt ≤ 15 →
    window ≠ .null → Writable h window (2 ^ wb.toInt.toNat) → h.allocOk h.nalloc = true →
    ∃ after z s, C.run (Zlib.Infback.inflateBackInit_ (some r) wb window version 112) h =
      .ok (Z_OK, after) ∧ BackValid after r h.nextBlk z s ∧ s.window = window ∧
      s.wbits = wb.toUInt32 ∧ Frame h after (StreamRoot r) ∧
      LiveChange h after (fun b => b = h.nextBlk) (fun _ => False)) ∧
  InitDomain witnessHeap (.tab 0) (.ref (.blk 1) 0) ∧
  (∀ wb : Int32, 8 ≤ wb.toInt → wb.toInt ≤ 15 →
    ∃ after z s, C.run (Zlib.Infback.inflateBackInit_ (some (.tab 0)) wb (.ref (.blk 2) 0)
      (.ref (.blk 1) 0) 112) witnessHeap = .ok (Z_OK, after) ∧
      BackValid after (.tab 0) witnessHeap.nextBlk z s ∧ s.window = .ref (.blk 2) 0)

/-- External open success is specified by the fixed file-system semantics. No gz contract
is an assumption. Every accepted mode has a successful concrete open witness. -/
def Goal.gz_initialisation_domain : Prop :=
  (∀ h fs path mode name flags kind level strategy direct fd world start,
    Fresh h → Zlib.Gzlib.Spec.Uniq h → LibraryGlobals h → FileSystem fs →
    NoAllocationFailure h → CString h path name → CString h mode flags →
    parsedMode flags = some (kind, level, strategy, direct) →
    OpenWorld h fs world name flags kind none fd start → fd ≠ -1 →
    ∃ after fs' i s, Zlib.Gzlib.gzopen path mode fs h = .ok ((some (.in_gzstate_x i), fs'), after) ∧
      OpenState after i s kind level strategy direct fd name ∧ GzReachable after fs' i ∧
      Frame h after (fun _ => False) ∧ LiveChange h after (GzOwned after i s) (fun _ => False)) ∧
  (∀ flags kind level strategy direct, 0 ∉ flags →
    parsedMode flags = some (kind, level, strategy, direct) →
    ∃ after fs' i s,
      Zlib.Gzlib.gzopen (.ref (.blk 3) 0) (.ref (.blk 4) 0) (gzWitnessFs kind) (gzWitnessHeap flags) =
        .ok ((some (.in_gzstate_x i), fs'), after) ∧
      OpenState after i s kind level strategy direct s.fd [120] ∧ GzReachable after fs' i)