StreamQueries.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.Memory
2
3namespace ZlibF.Spec.Public
4open C
5
6/-- The stream and inflate record accepted by the public state check. This is a
7representation condition, to be established by init and preserved by stream operations. -/
8def InflateView (h : Heap) (r : ZStreamRef) (i : Nat) (z : ZStream) (s : InflateState) : Prop :=
9  r.get h = some z ∧ z.state = StateRef.ofInflateState (some (.tab i)) ∧
10  h.istates i = some s ∧ s.strm = some r ∧ z.zalloc ≠ .null ∧ z.zfree ≠ .null ∧
11  HEAD ≤ s.mode ∧ s.mode ≤ SYNC
12
13/-- The stream and deflate record accepted by the public state check. -/
14def DeflateView (h : Heap) (r : ZStreamRef) (i : Nat) (z : ZStream) (s : DeflateState) : Prop :=
15  r.get h = some z ∧ z.state = StateRef.ofDeflateState (some (.tab i)) ∧
16  h.dstates i = some s ∧ s.strm = some r ∧ z.zalloc ≠ .null ∧ z.zfree ≠ .null ∧
17  (s.status = INIT_STATE ∨ s.status = GZIP_STATE ∨ s.status = EXTRA_STATE ∨
18   s.status = NAME_STATE ∨ s.status = COMMENT_STATE ∨ s.status = HCRC_STATE ∨
19   s.status = BUSY_STATE ∨ s.status = FINISH_STATE)
20
21def putInflate (h : Heap) (i : Nat) (s : InflateState) : Heap :=
22  { h with istates := upd h.istates i (some s) }
23
24def putDeflate (h : Heap) (i : Nat) (s : DeflateState) : Heap :=
25  { h with dstates := upd h.dstates i (some s) }
26
27/-- Cleanly rejected pointers contain enough live storage for the source state check.
28A dangling or wrongly typed state is not a permitted caller argument. -/
29def RefusedInflate (h : Heap) (p : ZStreamPtr) : Prop :=
30  p = none ∨ ∃ r z, p = some r ∧ r.get h = some z ∧
31    (z.zalloc = .null ∨ z.zfree = .null ∨ z.state = none ∨
32      ∃ i s, z.state = some (.inflate i) ∧ h.istates i = some s ∧
33        (s.strm ≠ some r ∨ s.mode < HEAD ∨ SYNC < s.mode))
34
35def RefusedDeflate (h : Heap) (p : ZStreamPtr) : Prop :=
36  p = none ∨ ∃ r z, p = some r ∧ r.get h = some z ∧
37    (z.zalloc = .null ∨ z.zfree = .null ∨ z.state = none ∨
38      ∃ i s, z.state = some (.deflate i) ∧ h.dstates i = some s ∧
39        (s.strm ≠ some r ∨ ¬ (s.status = INIT_STATE ∨ s.status = GZIP_STATE ∨
40          s.status = EXTRA_STATE ∨ s.status = NAME_STATE ∨ s.status = COMMENT_STATE ∨
41          s.status = HCRC_STATE ∨ s.status = BUSY_STATE ∨ s.status = FINISH_STATE)))
42
43def CheckedInflate {α : Type} (program : ZStreamPtr → M α) (error : α)
44    (accepted : Prop) : Prop :=
45  (∀ h p, RefusedInflate h p → C.run (program p) h = .ok (error, h)) ∧ accepted
46
47def CheckedDeflate {α : Type} (program : ZStreamPtr → M α) (error : α)
48    (accepted : Prop) : Prop :=
49  (∀ h p, RefusedDeflate h p → C.run (program p) h = .ok (error, h)) ∧ accepted
50
51/-- `int inflateSyncPoint(z_streamp strm)`.
52The answer is exactly the stored-block boundary test; all memory is preserved. -/
53def Goal.inflateSyncPoint : Prop :=
54  CheckedInflate Zlib.Inflate.inflateSyncPoint Z_STREAM_ERROR <|
55  ∀ h r i z s, InflateView h r i z s →
56    C.run (Zlib.Inflate.inflateSyncPoint (some r)) h =
57      .ok ((if s.mode = STORED ∧ s.bits = 0 then 1 else 0), h)
58
59/-- `long inflateMark(z_streamp strm)`.
60The high half counts code bits; the low half counts remaining stored bytes or match bytes
61already copied. The internal ranges are obligations of the stream invariant. -/
62def Goal.inflateMark : Prop :=
63  CheckedInflate Zlib.Inflate.inflateMark (-65536) <|
64  ∀ h r i z s, InflateView h r i z s →
65    C.run (Zlib.Inflate.inflateMark (some r)) h = .ok
66      (Int64.ofInt (s.back.toInt * 65536 +
67        (if s.mode = COPY then s.length.toNat else
68         if s.mode = MATCH then (s.was - s.length).toNat else 0)), h)
69
70/-- `unsigned long inflateCodesUsed(z_streamp strm)`.
71Return the number of used decode-table slots, with no memory effect. The fixed C
72array has 1444 entries; init and stream preservation establish this representation fact. -/
73def Goal.inflateCodesUsed : Prop :=
74  CheckedInflate Zlib.Inflate.inflateCodesUsed 0xffffffffffffffff <|
75  ∀ h r i z s n, InflateView h r i z s → s.codes.size = 1444 →
76    s.next = .ref (.istate_codes i) n → n ≤ s.codes.size →
77    C.run (Zlib.Inflate.inflateCodesUsed (some r)) h = .ok (UInt64.ofNat n, h)
78
79/-- `int inflateUndermine(z_streamp strm, int subvert)`.
80The default build refuses the extension and restores strict distance checking. -/
81def Goal.inflateUndermine : Prop :=
82  ∀ subvert, CheckedInflate (fun p => Zlib.Inflate.inflateUndermine p subvert) Z_STREAM_ERROR <|
83  ∀ h r i z s, InflateView h r i z s →
84    C.run (Zlib.Inflate.inflateUndermine (some r) subvert) h =
85      .ok (Z_DATA_ERROR, putInflate h i { s with sane := 1 })
86
87/-- `int inflateValidate(z_streamp strm, int check)`.
88Toggle validation in both current and requested wrappers; retain every other field. -/
89def Goal.inflateValidate : Prop :=
90  ∀ check, CheckedInflate (fun p => Zlib.Inflate.inflateValidate p check) Z_STREAM_ERROR <|
91  ∀ h r i z s, InflateView h r i z s →
92    C.run (Zlib.Inflate.inflateValidate (some r) check) h = .ok
93      (Z_OK, putInflate h i { s with
94        wrap := if check ≠ 0 ∧ s.wrap ≠ 0 then s.wrap ||| 4 else s.wrap &&& ~~~4
95        reqwrap := if check ≠ 0 ∧ s.reqwrap ≠ 0 then s.reqwrap ||| 4 else s.reqwrap &&& ~~~4 })
96
97/-- `int inflatePrime(z_streamp strm, int bits, int value)`.
98Negative counts clear pending bits. Counts above 16 or a total above 32 are refused.
99Otherwise append exactly the requested low bits, without allocation. -/
100def Goal.inflatePrime : Prop :=
101  ∀ bits value, CheckedInflate (fun p => Zlib.Inflate.inflatePrime p bits value) Z_STREAM_ERROR <|
102  ∀ h r i z s, InflateView h r i z s → s.bits.toNat ≤ 39 →
103    C.run (Zlib.Inflate.inflatePrime (some r) bits value) h =
104      if bits = 0 then .ok (Z_OK, h)
105      else if bits.toInt < 0 then .ok (Z_OK, putInflate h i { s with hold := 0, bits := 0 })
106      else if 16 < bits.toInt ∨ 32 < s.bits.toNat + bits.toInt.toNat then .ok (Z_STREAM_ERROR, h)
107      else .ok (Z_OK, putInflate h i { s with
108        hold := s.hold + ((value.toUInt32 &&& ((1 <<< bits.toUInt32) - 1)).toUInt64 <<< s.bits.toUInt64)
109        bits := s.bits + bits.toUInt32 })
110
111/-- `int deflatePending(z_streamp strm, unsigned *pending, int *bits)`.
112Optional output cells are independent; omitted cells remain absent. -/
113def Goal.deflatePending : Prop :=
114  ∀ pending bits, CheckedDeflate (fun p => Zlib.Deflate.deflatePending p pending bits)
115    (Z_STREAM_ERROR, none, none) <|
116  ∀ h r i z s, DeflateView h r i z s →
117    C.run (Zlib.Deflate.deflatePending (some r) pending bits) h =
118      .ok (((if pending ∧ 2 ^ 32 ≤ s.pending.toNat then Z_BUF_ERROR else Z_OK),
119        if pending then some (if 2 ^ 32 ≤ s.pending.toNat then 0xffffffff else s.pending.toUInt32) else none,
120        if bits then some s.bi_valid else none), h)
121
122/-- `int deflateUsed(z_streamp strm, int *bits)`.
123Return the modulo-eight bit-use count through the optional scalar result. -/
124def Goal.deflateUsed : Prop :=
125  ∀ bits, CheckedDeflate (fun p => Zlib.Deflate.deflateUsed p bits) (Z_STREAM_ERROR, none) <|
126  ∀ h r i z s, DeflateView h r i z s →
127    C.run (Zlib.Deflate.deflateUsed (some r) bits) h =
128      .ok ((Z_OK, if bits then some s.bi_used else none), h)
129
130/-- `int deflateTune(z_streamp strm, int good_length, int max_lazy, int nice_length, int max_chain)`.
131All signed arguments are covered. The three unsigned fields use C conversion. -/
132def Goal.deflateTune : Prop :=
133  ∀ good lazy nice chain,
134  CheckedDeflate (fun p => Zlib.Deflate.deflateTune p good lazy nice chain) Z_STREAM_ERROR <|
135  ∀ h r i z s, DeflateView h r i z s →
136    C.run (Zlib.Deflate.deflateTune (some r) good lazy nice chain) h =
137      .ok (Z_OK, putDeflate h i { s with
138        good_match := good.toUInt32
139        max_lazy_match := lazy.toUInt32
140        nice_match := nice
141        max_chain_length := chain.toUInt32 })
142
143/-- `int deflateSetHeader(z_streamp strm, gz_headerp head)`.
144Only the gzip wrapper accepts the pointer. The record is retained and read by later calls. -/
145def Goal.deflateSetHeader : Prop :=
146  ∀ head, CheckedDeflate (fun p => Zlib.Deflate.deflateSetHeader p head) Z_STREAM_ERROR <|
147  ∀ h r i z s, DeflateView h r i z s →
148    C.run (Zlib.Deflate.deflateSetHeader (some r) head) h =
149      if s.wrap = 2 then .ok (Z_OK, putDeflate h i { s with gzhead := head })
150      else .ok (Z_STREAM_ERROR, h)
151
152end ZlibF.Spec.Public