Streams.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.History
2import ZlibF.Spec.Api.Inflate
3import ZlibF.Spec.PlatformMemory
4
5namespace ZlibF.Spec.Public
6open C ZlibF.Spec
7
8def advance : BPtr → Nat → BPtr
9  | .null, _ => .null
10  | .ref r i, n => .ref r (i + n)
11
12def StreamAccounting (z z' : ZStream) (used produced : Nat) : Prop :=
13  used ≤ z.avail_in.toNat ∧ produced ≤ z.avail_out.toNat ∧
14  z'.avail_in.toNat + used = z.avail_in.toNat ∧
15  z'.avail_out.toNat + produced = z.avail_out.toNat ∧
16  z'.next_in = advance z.next_in used ∧ z'.next_out = advance z.next_out produced ∧
17  z'.state = z.state ∧ z'.zalloc = z.zalloc ∧ z'.zfree = z.zfree ∧
18  z'.opaque = z.opaque ∧ z'.reserved = z.reserved
19
20/-- `int inflate(z_streamp strm, int flush)`.
21The domain is actual init/call history, not an arbitrary hand-built decoder state.
22The selected LP64 platform scope explicitly requires every live represented
23byte object to have at most PTRDIFF_MAX bytes (size < 2^63), including caller
24storage from non-malloc origins. See docs/deviations.md.
25Includes all signed flush arguments, progress, terminal/error modes, output bounds,
26counter timing on late memory failure, caller frame and ownership of a new window.
27The sequence target states format correctness across all input/output splits. -/
28def Goal.inflate : Prop :=
29  ∀ h r i z s flush,
30    StreamReachable .inflate h r → Zlib.Inflate.Spec.Good h r i z s →
31    ZlibF.PlatformMemory.ByteObjectsFit h →
32    Zlib.Inflate.Spec.DefAlloc z → StreamBuffers h r → ActiveHeader h r →
33    ∃ rc after z' s' used out,
34      C.run (Zlib.Inflate.inflate (some r) flush) h = .ok (rc, after) ∧
35      Zlib.Inflate.Spec.Good after r i z' s' ∧ StreamAccounting z z' used out.length ∧
36      Bytes after z.next_out out.length out ∧
37      (rc = Z_OK ∨ rc = Z_STREAM_END ∨ rc = Z_NEED_DICT ∨ rc = Z_STREAM_ERROR ∨
38       rc = Z_DATA_ERROR ∨ rc = Z_MEM_ERROR ∨ rc = Z_BUF_ERROR) ∧
39      (rc = Z_OK → (used ≠ 0 ∨ out ≠ []) ∧ flush ≠ Z_FINISH) ∧
40      (rc = Z_STREAM_END → s'.mode = DONE) ∧
41      (rc = Z_NEED_DICT → s'.mode = DICT) ∧
42      (rc = Z_DATA_ERROR → s'.mode = BAD) ∧
43      (rc = Z_MEM_ERROR → s'.mode = MEM ∧ z'.total_in = z.total_in ∧ z'.total_out = z.total_out) ∧
44      (rc = Z_OK ∨ rc = Z_STREAM_END ∨ rc = Z_DATA_ERROR ∨ rc = Z_BUF_ERROR →
45        z'.total_in = z.total_in + UInt64.ofNat used ∧
46        z'.total_out = z.total_out + UInt64.ofNat out.length) ∧
47      BufferFrame h after
48        (fun b => StreamRoot r b ∨ InflateOwned i s b ∨ s.head = some (.tab b))
49        (⟨z.next_out, out.length⟩ :: HeaderRegions h s.head) ∧
50      LiveChange h after (fun b => InflateOwned i s' b ∧ ¬ h.live b) (fun _ => False)
51
52/-- `int deflate(z_streamp strm, int flush)`.
53Preserve the live stream and its five allocations. Account for exactly the bytes accepted
54and delivered, including progress on a full output buffer and clean parameter refusals.
55The sequence target states valid encoding, flush semantics and completion. -/
56def Goal.deflate : Prop :=
57  ∀ h r i z s flush,
58    StreamReachable .deflate h r → Zlib.Deflate.Spec.DGood h r i z s →
59    StreamBuffers h r → ActiveHeader h r →
60    ∃ rc after z' s' used out,
61      C.run (Zlib.Deflate.deflate (some r) flush) h = .ok (rc, after) ∧
62      Zlib.Deflate.Spec.DGood after r i z' s' ∧ StreamAccounting z z' used out.length ∧
63      Bytes after z.next_out out.length out ∧
64      z'.total_in = z.total_in + UInt64.ofNat used ∧
65      z'.total_out = z.total_out + UInt64.ofNat out.length ∧
66      (rc = Z_OK ∨ rc = Z_STREAM_END ∨ rc = Z_STREAM_ERROR ∨ rc = Z_BUF_ERROR) ∧
67      (rc = Z_STREAM_ERROR ↔
68        flush.toInt < 0 ∨ 5 < flush.toInt ∨ z.next_out = .null ∨
69        (z.next_in = .null ∧ z.avail_in ≠ 0) ∨
70        (s.status = FINISH_STATE ∧ flush ≠ Z_FINISH)) ∧
71      (flush.toInt < 0 ∨ 5 < flush.toInt → rc = Z_STREAM_ERROR ∧ after = h) ∧
72      (rc = Z_STREAM_END → flush = Z_FINISH ∧ s'.status = FINISH_STATE ∧
73        z'.avail_in = 0 ∧ s'.pending = 0 ∧ s'.bi_valid = 0) ∧
74      BufferFrame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) [⟨z.next_out, out.length⟩] ∧
75      LiveChange h after (fun _ => False) (fun _ => False) ∧ after.nalloc = h.nalloc
76
77def bound64 (n : Nat) : UInt64 := UInt64.ofNat (min n (2 ^ 64 - 1))
78
79def WrapperLength (h : Heap) (s : DeflateState) (n : Nat) : Prop :=
80  (s.wrap = 0 ∧ n = 0) ∨
81  ((s.wrap = 1 ∨ s.wrap = -1) ∧ n = 6 + if s.strstart = 0 then 0 else 4) ∨
82  ((s.wrap = 2 ∨ s.wrap = -2) ∧
83    ((s.gzhead = none ∧ n = 18) ∨ ∃ g gh name comment,
84      s.gzhead = some (.tab g) ∧ h.gzheaders g = some gh ∧
85      (gh.name = .null ∧ name = [] ∨ CString h gh.name name) ∧
86      (gh.comment = .null ∧ comment = [] ∨ CString h gh.comment comment) ∧
87      n = 18 + (if gh.extra = .null then 0 else 2 + gh.extra_len.toNat) +
88        (if gh.name = .null then 0 else name.length + 1) +
89        (if gh.comment = .null then 0 else comment.length + 1) +
90        (if gh.hcrc = 0 then 0 else 2)))
91
92def deflateBoundValue (s : DeflateState) (wrapper n : Nat) : UInt64 :=
93  if s.w_bits = 15 ∧ s.hash_bits = 15 then
94    bound64 (n + n / 4096 + n / 16384 + n / 33554432 + 7 + wrapper)
95  else if s.w_bits ≤ s.hash_bits ∧ s.level ≠ 0 then
96    bound64 (n + n / 8 + n / 256 + n / 512 + 4 + wrapper)
97  else bound64 (n + n / 32 + n / 128 + n / 2048 + 7 + wrapper)
98
99def DeflateBoundContract (program : ZStreamPtr → UInt64 → M UInt64) : Prop :=
100  (∀ h n, C.run (program none n) h = .ok
101    (bound64 (max (n.toNat + n.toNat / 8 + n.toNat / 256 + n.toNat / 512 + 4)
102      (n.toNat + n.toNat / 32 + n.toNat / 128 + n.toNat / 2048 + 7) + 18), h)) ∧
103  (∀ h r i z s wrapper n,
104    Zlib.Deflate.Spec.DGood h r i z s → WrapperLength h s wrapper →
105    C.run (program (some r) n) h = .ok (deflateBoundValue s wrapper n.toNat, h))
106
107/-- `z_size_t deflateBound_z(z_streamp strm, z_size_t sourceLen)`.
108The mathematical bound includes the entire gzip header, with saturation instead of overflow.
109The known extra-length arithmetic issue remains an implementation proof blocker. -/
110def Goal.deflateBound_z : Prop := DeflateBoundContract Zlib.Deflate.deflateBound_z
111
112/-- `uLong deflateBound(z_streamp strm, uLong sourceLen)`.
113The LP64 wrapper has the same numeric range; other ABIs need a conversion contract. -/
114def Goal.deflateBound : Prop := DeflateBoundContract Zlib.Deflate.deflateBound
115
116def PendingBits (h : Heap) (s : DeflateState) (bits : List Bool) : Prop :=
117  ∃ bytes, Bytes h s.pending_out s.pending.toNat bytes ∧
118    bits = bytesToBits bytes ++ ((List.range s.bi_valid.toInt.toNat).map fun j =>
119      decide (s.bi_buf.toNat / 2 ^ j % 2 = 1))
120
121/-- `int deflatePrime(z_streamp strm, int bits, int value)`.
122Append the requested low bits in transmission order. Compaction can occur before a buffer
123error; invalid bit counts are refused before compaction. No allocation occurs. -/
124def Goal.deflatePrime : Prop :=
125  ∀ h r i z s count value old,
126    Zlib.Deflate.Spec.DGood h r i z s → PendingBits h s old →
127    ∃ rc after s', C.run (Zlib.Deflate.deflatePrime (some r) count value) h = .ok (rc, after) ∧
128      Zlib.Deflate.Spec.DGood after r i z s' ∧
129      (count.toInt < 0 ∨ 16 < count.toInt → rc = Z_BUF_ERROR ∧ after = h) ∧
130      (0 ≤ count.toInt → count.toInt ≤ 16 →
131        s'.pending_out = s'.pending_buf ∧
132        if s.pending_buf_size.toNat - s.pending.toNat < (s.bi_valid.toInt.toNat + count.toInt.toNat) / 8 then
133          rc = Z_BUF_ERROR ∧ PendingBits after s' old
134        else rc = Z_OK ∧ PendingBits after s'
135          (old ++ (List.range count.toInt.toNat).map (fun j => decide (value.toUInt32.toNat / 2 ^ j % 2 = 1)))) ∧
136      Frame h after (DeflateOwned i s) ∧ LiveChange h after (fun _ => False) (fun _ => False) ∧
137      after.nalloc = h.nalloc
138
139/-- `int deflateParams(z_streamp strm, int level, int strategy)`.
140May consume input and write output while finishing the old block. A buffer error retains
141the old parameters; successful changes select the canonical tuning row for a changed level. -/
142def Goal.deflateParams : Prop :=
143  ∀ h r i z s level strategy,
144    StreamReachable .deflate h r → Zlib.Deflate.Spec.DGood h r i z s →
145    StreamBuffers h r → ActiveHeader h r →
146    ∃ rc after z' s' used out,
147      C.run (Zlib.Deflate.deflateParams (some r) level strategy) h = .ok (rc, after) ∧
148      Zlib.Deflate.Spec.DGood after r i z' s' ∧ StreamAccounting z z' used out.length ∧
149      Bytes after z.next_out out.length out ∧
150      (rc = Z_OK ∨ rc = Z_BUF_ERROR ∨ rc = Z_STREAM_ERROR) ∧
151      (rc = Z_OK → s'.level = (if level = -1 then 6 else level) ∧ s'.strategy = strategy) ∧
152      (rc ≠ Z_OK → s'.level = s.level ∧ s'.strategy = s.strategy) ∧
153      ((level.toInt < -1 ∨ 9 < level.toInt ∨ strategy.toInt < 0 ∨ 4 < strategy.toInt) →
154        rc = Z_STREAM_ERROR ∧ after = h) ∧
155      BufferFrame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) [⟨z.next_out, out.length⟩] ∧
156      LiveChange h after (fun _ => False) (fun _ => False) ∧ after.nalloc = h.nalloc
157
158def heldSyncBytes (s : InflateState) : List UInt8 :=
159  (List.range ((s.bits.toNat - s.bits.toNat % 8) / 8)).map fun j =>
160    UInt8.ofNat (s.hold.toNat / 2 ^ (s.bits.toNat % 8 + 8 * j) % 256)
161
162/-- `int inflateSync(z_streamp strm)`.
163Search byte-aligned held bits before new input, retaining the partial marker match.
164On success retain totals and restart at TYPE with validation disabled. -/
165def Goal.inflateSync : Prop :=
166  ∀ h r i z s input,
167    StreamReachable .inflate h r → Zlib.Inflate.Spec.Good h r i z s →
168    Zlib.Inflate.Spec.DefAlloc z → Bytes h z.next_in z.avail_in.toNat input →
169    ∃ rc after z' s' used,
170      C.run (Zlib.Inflate.inflateSync (some r)) h = .ok (rc, after) ∧
171      Zlib.Inflate.Spec.Good after r i z' s' ∧ used ≤ input.length ∧
172      z'.next_in = advance z.next_in used ∧ z'.avail_in.toNat + used = z.avail_in.toNat ∧
173      z'.total_in = z.total_in + UInt64.ofNat used ∧ z'.total_out = z.total_out ∧
174      (if z.avail_in = 0 ∧ s.bits.toNat < 8 then rc = Z_BUF_ERROR ∧ z' = z ∧ s' = s
175       else let start := if s.mode = SYNC then s.have.toNat else
176              (Api.syncSearch 0 (heldSyncBytes s)).1
177            let found := Api.syncSearch start input
178            used = found.2 ∧
179            if found.1 = 4 then rc = Z_OK ∧ s'.mode = TYPE ∧ (s'.wrap &&& 4) = 0
180            else rc = Z_DATA_ERROR ∧ s'.mode = SYNC ∧ s'.have.toNat = found.1) ∧
181      Frame h after (fun b => StreamRoot r b ∨ InflateOwned i s b) ∧
182      LiveChange h after (fun _ => False)
183        (fun b => InflateOwned i s b ∧ ¬ InflateOwned i s' b)
184
185end ZlibF.Spec.Public