deflate.c.prime.lean

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

1import ZlibF.Proof.«public-deflate-small-queries»
2
3/-!
4# deflate.c: priming refusal before compaction
5
6The entry refuses an invalid stream and any bit count outside 0 through 16.
7The accepted-count path, pending-byte compaction and bit-output relation remain open.
8The statements below cover refusal paths only, not the complete public prime target.
9-/
10
11namespace Zlib.Deflate.Proofs
12open C Zlib.Deflate.Spec ZlibF.Spec.Public ZlibF.Spec.Public.DeflateQueryProof
13
14/-- `int deflatePrime(z_streamp strm, int bits, int value)` checks the stream first. -/
15theorem deflatePrime_refused {h : Heap} {p : ZStreamPtr} (hr : RefusedDeflate h p)
16    (bits value : Int32) :
17    C.run (deflatePrime p bits value) h = .ok (Z_STREAM_ERROR, h) := by
18  unfold deflatePrime
19  exact check_refuse (refused_deflate_dom hr) (refused_deflate_not_init hr) _ _
20
21/-- `int deflatePrime(z_streamp strm, int bits, int value)` refuses invalid counts
22before moving pending bytes. This internal branch needs only `DLive`; it does not
23assume pending-buffer bounds, a bit-output contract or a callee specification. -/
24theorem deflatePrime_invalid_count {h : Heap} {r : ZStreamRef} {i : Nat}
25    {z : ZStream} {s : DeflateState} (hl : DLive h r i z s) (bits value : Int32)
26    (hb : bits.toInt < 0 ∨ 16 < bits.toInt) :
27    C.run (deflatePrime (some r) bits value) h = .ok (Z_BUF_ERROR, h) := by
28  have hc : bits < 0 ∨ bits > 16 := by
29    rcases hb with hb | hb
30    · exact Or.inl (Int32.lt_iff_toInt_lt.mpr (by simpa using hb))
31    · exact Or.inr (Int32.lt_iff_toInt_lt.mpr (by simpa using hb))
32  show deflatePrime (some r) bits value h = _
33  unfold deflatePrime
34  dsimp' [stateCheck_live hl, hl.zst, hl.hz, hl.hs, hc]
35
36#print axioms deflatePrime_refused
37#print axioms deflatePrime_invalid_count
38end Zlib.Deflate.Proofs