Sequences.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Spec.Public.Domains
2import ZlibF.Spec.Public.GzTrace
3import ZlibF.Spec.Api.Goals
4
5namespace ZlibF.Spec.Public
6open C Zlib.GzFs ZlibF.Spec
7
8/-- An invariant is a conclusion about every actual history, never an assumed callee contract. -/
9def StreamInvariant : StreamKind → Heap → ZStreamRef → Prop
10  | .inflate, h, r => ∃ i z s, Zlib.Inflate.Spec.Good h r i z s ∧ Zlib.Inflate.Spec.DefAlloc z
11  | .deflate, h, r => ∃ i z s, Zlib.Deflate.Spec.DGood h r i z s ∧ Zlib.Deflate.Spec.DefAlloc z
12
13def StreamWriteRegions (h : Heap) (r : ZStreamRef) : Call → List Region
14  | .inflate _ _ | .deflate _ _ | .deflateParams _ _ _ =>
15      match r.get h with
16      | none => []
17      | some z => ⟨z.next_out, z.avail_out.toNat⟩ ::
18          (match z.state with
19           | some (.inflate i) => match h.istates i with
20             | some s => HeaderRegions h s.head
21             | none => []
22           | _ => [])
23  | .inflateGetDictionary _ p _ | .deflateGetDictionary _ p _ => [⟨p, 32768⟩]
24  | _ => []
25
26def StreamHeaderRecord (h : Heap) (r : ZStreamRef) (call : Call) (b : Nat) : Prop :=
27  call = .inflateGetHeader (some r) (some (.tab b)) ∨
28  (∃ z i s, r.get h = some z ∧ z.state = some (.inflate i) ∧ h.istates i = some s ∧
29    s.head = some (.tab b) ∧ ∃ flush, call = .inflate (some r) flush)
30
31/-- One more call must return from every permitted history, not merely preserve an invariant
32when a caller assumes one. The ledger is exact, including failed calls and released windows. -/
33def StreamSequenceSafety (kind : StreamKind) : Prop :=
34  (∀ h r, StreamReachable kind h r → StreamInvariant kind h r) ∧
35  (∀ h r call, StreamReachable kind h r → StreamOperation kind r call → StreamArguments h r call →
36    ∃ value after, call.execute default h = .ok ((value, default), after) ∧
37      StreamInvariant kind after r ∧
38      BufferFrame h after
39        (fun b => StreamRoot r b ∨ StreamOwned h r b ∨ StreamHeaderRecord h r call b)
40        (StreamWriteRegions h r call) ∧
41      LiveChange h after
42        (fun b => StreamOwned after r b ∧ ¬ h.live b)
43        (fun b => StreamOwned h r b ∧ ¬ StreamOwned after r b)) ∧
44  (∀ h r, StreamReachable kind h r →
45    ∃ rc after z, C.run ((match kind with
46      | .inflate => Zlib.Inflate.inflateEnd
47      | .deflate => Zlib.Deflate.deflateEnd) (some r)) h = .ok (rc, after) ∧
48      (rc = Z_OK ∨ kind = .deflate ∧ rc = Z_DATA_ERROR) ∧
49      r.get after = some z ∧ z.state = none ∧
50      Frame h after (fun b => StreamRoot r b ∨ StreamOwned h r b) ∧
51      LiveChange h after (fun _ => False) (StreamOwned h r))
52
53structure DataLog where
54  input : List UInt8 := []
55  output : List UInt8 := []
56  dictionary : List UInt8 := []
57  result : Int32 := Z_OK
58  /-- False only after a raw dictionary replacement during an already-started data epoch.
59  Such a continuation has multiple dictionary contexts, not one ordinary RFC stream. -/
60  singleDictionary : Bool := true
61  finished : Bool := false
62  boundEligible : Bool := true
63
64/-- Observations of actual calls. These equations neither assume accounting correctness nor
65assume that output is valid compressed data. That is required by the sequence targets. -/
66def DataStep (kind : StreamKind) (h after : Heap) (r : ZStreamRef)
67    (flush rc : Int32) (input output : List UInt8) (used : Nat) : Prop :=
68  ∃ z z', r.get h = some z ∧ r.get after = some z' ∧ StreamBuffers h r ∧ ActiveHeader h r ∧
69    Bytes h z.next_in z.avail_in.toNat input ∧
70    used = z.avail_in.toNat - z'.avail_in.toNat ∧
71    Bytes after z.next_out (z.avail_out.toNat - z'.avail_out.toNat) output ∧
72    C.run ((match kind with | .inflate => Zlib.Inflate.inflate | .deflate => Zlib.Deflate.deflate)
73      (some r) flush) h = .ok (rc, after)
74
75/-- A data epoch begins with the actual init. Rebinding buffers changes no private state.
76Dictionary calls are recorded with their actual result; no earlier specification is assumed.
77Reset starts another epoch; its safety and ownership are covered by StreamSequenceSafety. -/
78inductive InflateDataTrace (wb : Int32) (r : ZStreamRef) : Heap → DataLog → Prop
79  | init {h after version} : InitDomain h r version →
80      C.run (Zlib.Inflate.inflateInit2_ (some r) wb version 112) h = .ok (Z_OK, after) →
81      InflateDataTrace wb r after {}
82  | caller {h after log} : InflateDataTrace wb r h log → Rebuffer h after r →
83      InflateDataTrace wb r after log
84  | step {h after log flush rc input output used} : InflateDataTrace wb r h log →
85      DataStep .inflate h after r flush rc input output used →
86      InflateDataTrace wb r after
87        { log with
88          input := log.input ++ input.take used, output := log.output ++ output
89          result := rc, finished := log.finished || rc == Z_STREAM_END }
90  | dictionary {h after log p n bytes rc} : InflateDataTrace wb r h log →
91      StreamArguments h r (.inflateSetDictionary (some r) p n) → Bytes h p n.toNat bytes →
92      C.run (Zlib.Inflate.inflateSetDictionary (some r) p n) h = .ok (rc, after) →
93      InflateDataTrace wb r after
94        { log with
95          dictionary := if rc = Z_OK then
96            if wb.toInt < 0 then log.dictionary ++ bytes else bytes else log.dictionary
97          singleDictionary := log.singleDictionary &&
98            !(rc = Z_OK && wb.toInt < 0 && (log.input != [] || log.output != [])) }
99
100inductive DeflateDataTrace (level method wb mem strategy : Int32) (r : ZStreamRef) : Heap → DataLog → Prop
101  | init {h after version} : InitDomain h r version →
102      C.run (Zlib.Deflate.deflateInit2_ (some r) level method wb mem strategy version 112) h = .ok (Z_OK, after) →
103      DeflateDataTrace level method wb mem strategy r after {}
104  | caller {h after log} : DeflateDataTrace level method wb mem strategy r h log → Rebuffer h after r →
105      DeflateDataTrace level method wb mem strategy r after log
106  | step {h after log flush rc input output used} : DeflateDataTrace level method wb mem strategy r h log →
107      DataStep .deflate h after r flush rc input output used →
108      DeflateDataTrace level method wb mem strategy r after
109        { log with
110          input := log.input ++ input.take used, output := log.output ++ output
111          result := rc, finished := log.finished || rc == Z_STREAM_END
112          boundEligible := log.boundEligible && flush == Z_FINISH }
113  | dictionary {h after log p n bytes rc} : DeflateDataTrace level method wb mem strategy r h log →
114      log.input = [] → log.output = [] →
115      StreamArguments h r (.deflateSetDictionary (some r) p n) → Bytes h p n.toNat bytes →
116      C.run (Zlib.Deflate.deflateSetDictionary (some r) p n) h = .ok (rc, after) →
117      DeflateDataTrace level method wb mem strategy r after
118        { log with dictionary := if rc = Z_OK then log.dictionary ++ bytes else log.dictionary }
119
120def DecodesFor (p : Api.DeflParams) (dictionary compressed plain : List UInt8) : Prop :=
121  match p.wrap with
122  | .raw => Deflate.Decodes (dictionary.drop (dictionary.length - 2 ^ p.wbits)) compressed plain
123  | .zlib => Zlib.Decodes dictionary compressed plain
124  | .gzip => Gzip.Decodes compressed plain
125
126/-- With the remainder of a valid stream and sufficient output room, a returning, non-failing
127decoder finishes. A pending dictionary must have been supplied. No assumed model step occurs. -/
128def InflateCompletes : Prop :=
129  ∀ wb wrap bits r h log source decoded z i s flush,
130    Api.inflWbits wb.toInt = some (wrap, bits) → InflateDataTrace wb r h log →
131    log.singleDictionary = true → log.finished = false →
132    Api.Layer.Decodes wrap bits log.dictionary source decoded → Api.FullWindow wrap bits source →
133    log.input <+: source → Zlib.Inflate.Spec.Good h r i z s →
134    s.mode ≠ BAD → s.mode ≠ MEM → s.mode ≠ SYNC → (s.mode = DICT → s.havedict ≠ 0) →
135    StreamBuffers h r → ActiveHeader h r → NoAllocationFailure h →
136    Bytes h z.next_in z.avail_in.toNat (source.drop log.input.length) →
137    decoded.length ≤ log.output.length + z.avail_out.toNat →
138    (flush = Z_NO_FLUSH ∨ flush = Z_SYNC_FLUSH ∨ flush = Z_FINISH) →
139    ∃ after, C.run (Zlib.Inflate.inflate (some r) flush) h = .ok (Z_STREAM_END, after) ∧
140      Bytes after z.next_out (decoded.length - log.output.length) (decoded.drop log.output.length)
141
142/-- The documented finish-only bound supplies enough space for completion. Eligibility is
143computed by the actual trace constructors; a proof cannot choose or reset that flag. -/
144def DeflateCompletes : Prop :=
145  ∀ level method wb mem strategy p r h log input z i s,
146    Api.deflInit? level.toInt method.toInt wb.toInt mem.toInt strategy.toInt = some p →
147    DeflateDataTrace level method wb mem strategy r h log →
148    log.boundEligible = true → log.finished = false →
149    Zlib.Deflate.Spec.DGood h r i z s → StreamBuffers h r → ActiveHeader h r →
150    Bytes h z.next_in z.avail_in.toNat input → 0 < z.avail_out.toNat →
151    ({ Api.DeflState.fresh p with dict := some log.dictionary }).bound (log.input.length + input.length) ≤
152      log.output.length + z.avail_out.toNat →
153    ∃ after, C.run (Zlib.Deflate.deflate (some r) Z_FINISH) h = .ok (Z_STREAM_END, after)
154
155/-- All legal public histories are safe and retain cleanup. For ordinary data epochs every
156input/output split is covered, including allocation failures and dictionary handshakes.
157Completion is stated against the independent byte-format relation. -/
158def Goal.inflate_sequence : Prop :=
159  StreamSequenceSafety .inflate ∧
160  (∀ wb wrap bits r h log, Api.inflWbits wb.toInt = some (wrap, bits) →
161    InflateDataTrace wb r h log →
162    (log.singleDictionary = true → log.result = Z_STREAM_END →
163      Api.Layer.Decodes wrap bits log.dictionary log.input log.output) ∧
164    (∀ source decoded, Api.Layer.Decodes wrap bits log.dictionary source decoded →
165      log.singleDictionary = true → Api.FullWindow wrap bits source → log.input <+: source →
166      log.output <+: decoded ∧ log.result ≠ Z_DATA_ERROR ∧
167      (log.result = Z_STREAM_END → log.input = source ∧ log.output = decoded))) ∧
168  InflateCompletes
169
170/-- All legal public histories are safe and retain cleanup. A finished ordinary data epoch
171encodes exactly its accepted input, for every accepted parameter set and flush schedule. -/
172def Goal.deflate_sequence : Prop :=
173  StreamSequenceSafety .deflate ∧
174  (∀ level method wb mem strategy p r h log,
175    Api.deflInit? level.toInt method.toInt wb.toInt mem.toInt strategy.toInt = some p →
176    DeflateDataTrace level method wb mem strategy r h log →
177    log.result = Z_STREAM_END → DecodesFor p log.dictionary log.output log.input) ∧
178  DeflateCompletes
179
180/-- Callback histories use the same caller-owned window across repeated decoding calls. -/
181inductive BackReachable : Heap → ZStreamRef → Nat → BPtr → Nat → Prop
182  | init {h after r version wb window} : InitDomain h r version →
183      8 ≤ wb.toInt → wb.toInt ≤ 15 → Writable h window (2 ^ wb.toInt.toNat) → window ≠ .null →
184      C.run (Zlib.Infback.inflateBackInit_ (some r) wb window version 112) h = .ok (Z_OK, after) →
185      BackReachable after r h.nextBlk window (2 ^ wb.toInt.toNat)
186  | caller {h after r i window n} : BackReachable h r i window n → Rebuffer h after r →
187      SameBytePrefix h after window window n → BackReachable after r i window n
188  | step {h after r i window n z input inDesc output outDesc first rc}
189      (protocol : CallbackProtocol r i window n input inDesc output outDesc) :
190      BackReachable h r i window n → r.get h = some z →
191      (if z.next_in = .null then first = [] else Bytes h z.next_in z.avail_in.toNat first) →
192      Separate z.next_in first.length window n →
193      protocol.invariant h { supplied := first, chunks := [], active := z.next_in, held := first } →
194      C.run (Zlib.Infback.inflateBack (some r) input inDesc output outDesc) h = .ok (rc, after) →
195      BackReachable after r i window n
196
197/-- Includes actual callback execution and raw-format delivery, re-use of the window, and
198complete end cleanup. Callback memory and returning/finite-input obligations remain explicit. -/
199def Goal.inflate_back_sequence : Prop :=
200  Goal.inflateBack ∧
201  (∀ h r i window n, BackReachable h r i window n →
202    (∃ z s, BackValid h r i z s ∧ s.window = window ∧ s.wsize.toNat = n) ∧
203    ∃ after z, C.run (Zlib.Infback.inflateBackEnd (some r)) h = .ok (Z_OK, after) ∧
204      r.get after = some z ∧ z.state = none ∧
205      Frame h after (fun b => StreamRoot r b ∨ b = i) ∧
206      LiveChange h after (fun _ => False) (fun b => b = i))
207
208/-- The gz lifecycle includes every admitted operation, external file growth and final close.
209The per-entry read contracts express transparent/concatenated-member decoding and the
210per-entry write contracts account for accepted bytes and seek zeros. -/
211def Goal.gz_sequence : Prop :=
212  (∀ h fs i, GzReachable h fs i → FileSystem fs ∧ ∃ s, GzValid h i s) ∧
213  (∀ h fs i s call, GzReachable h fs i → h.gzstates i = some s →
214    GzOperation i call → GzArguments h i s call →
215    ∃ value fs' after s', call.execute fs h = .ok ((value, fs'), after) ∧
216      GzValid after i s' ∧ FileSystem fs' ∧
217      LiveChange h after
218        (fun b => GzOwned after i s' b ∧ ¬ h.live b)
219        (fun b => GzOwned h i s b ∧ ¬ GzOwned after i s' b)) ∧
220  (∀ h fs i s, GzReachable h fs i → h.gzstates i = some s →
221    ∃ rc fs' after, Zlib.Gzclose.gzclose (some (.in_gzstate_x i)) fs h = .ok ((rc, fs'), after) ∧
222      CloseEffects h after fs fs' i s) ∧
223  Goal.gzread ∧ Goal.gzfread ∧ Goal.gzgetc ∧ Goal.gzgets ∧
224  Goal.gzwrite ∧ Goal.gzfwrite ∧ Goal.gzflush ∧ Goal.gzclose ∧ GzWriterFormat
225
226end ZlibF.Spec.Public