Utilities.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
2import ZlibF.Spec.Api.Compress
3
4namespace ZlibF.Spec.Public
5open C ZlibF.Spec
6
7def compressRejected (dest : BPtr) (capacity : Option UInt64) (source : BPtr) (n : UInt64) : Prop :=
8  capacity = none ∨ (source = .null ∧ n ≠ 0) ∨
9    ∃ c, capacity = some c ∧ dest = .null ∧ c ≠ 0
10
11def CompressArguments (h : Heap) (dest : BPtr) (capacity : Option UInt64)
12    (source : BPtr) (n : UInt64) (xs : List UInt8) : Prop :=
13  compressRejected dest capacity source n ∨
14  ∃ c, capacity = some c ∧ Bytes h source n.toNat xs ∧ Writable h dest c.toNat ∧
15    Separate source n.toNat dest c.toNat
16
17/-- The four compressor entries share the data relation. Their scalar-pointer domains and
18returned scalar types remain separate. No compressor or allocator theorem is assumed. -/
19def CompressorContract
20    (program : BPtr → Option UInt64 → BPtr → UInt64 → M (Int32 × Option UInt64))
21    (level : Int32) (nullableLength : Bool) : Prop :=
22  ∀ h dest capacity source n xs,
23    Fresh h → LibraryGlobals h → (nullableLength = false → capacity ≠ none) →
24    CompressArguments h dest capacity source n xs →
25    ∃ rc stored after out expected,
26      C.run (program dest capacity source n) h = .ok ((rc, stored), after) ∧
27      Store h dest out expected ∧ SameObjects expected after ∧
28      (rc = Z_MEM_ERROR → AllocationFailed h after) ∧
29      (compressRejected dest capacity source n →
30        rc = Z_STREAM_ERROR ∧ stored = capacity ∧ out = [] ∧ after = h) ∧
31      (¬ compressRejected dest capacity source n →
32        Api.Compress2Z
33          { source := xs, capacity := (capacity.getD 0).toNat, level := level.toInt
34            sourceNull := source == .null, destNull := dest == .null, lengthNull := false }
35          { rc := rc.toInt, produced := out, storedLength := stored.map UInt64.toNat })
36
37/-- `int compress2_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t sourceLen, int level)`.
38Includes null-cell rejection, unchanged capacity on argument rejection, exact stored length,
39valid compressed data, buffer exhaustion, allocation failure, frame and complete cleanup. -/
40def Goal.compress2_z : Prop :=
41  ∀ level, CompressorContract (fun d c s n => Zlib.Compress.compress2_z d c s n level) level true
42
43/-- `int compress2(Bytef *dest, uLongf *destLen, const Bytef *source, uLong sourceLen, int level)`.
44The wrapper reads the length cell before `_z` checks; its length cell must be nonnull. -/
45def Goal.compress2 : Prop :=
46  ∀ level, CompressorContract (fun d c s n => do
47    let (rc, size) ← Zlib.Compress.compress2 d c s n level
48    pure (rc, some size)) level false
49
50/-- `int compress_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t sourceLen)`.
51The nullable-length `_z` contract at the default compression level. -/
52def Goal.compress_z : Prop :=
53  CompressorContract Zlib.Compress.compress_z Z_DEFAULT_COMPRESSION true
54
55/-- `int compress(Bytef *dest, uLongf *destLen, const Bytef *source, uLong sourceLen)`.
56The nonnull-length wrapper contract at the default compression level. -/
57def Goal.compress : Prop :=
58  CompressorContract (fun d c s n => do
59    let (rc, size) ← Zlib.Compress.compress d c s n
60    pure (rc, some size)) Z_DEFAULT_COMPRESSION false
61
62/-- Observable decompression on buffers. Memory failure can follow output. Buffer exhaustion
63does not assert that unused trailing source bytes can extend a valid compressed stream. -/
64def Uncompressed (src : List UInt8) (capacity : Nat) (rc : Int32)
65    (out : List UInt8) (used : Nat) : Prop :=
66  Api.Uncompress2 true src capacity rc.toInt out used
67
68/-- Scalar cells are separate from data buffers and from each other. This is the explicit
69scalar-alias representation limit recorded in `docs/deviations.md`. -/
70def UtilitySeparation (dest : BPtr) (capacity : Nat) (source : BPtr) (n : Nat)
71    (destLen sourceLen : BPtr) : Prop :=
72  Separate dest capacity source n ∧ Separate destLen 8 dest capacity ∧
73  Separate destLen 8 source n ∧ Separate sourceLen 8 dest capacity ∧
74  Separate sourceLen 8 source n ∧ Separate destLen 8 sourceLen 8
75
76/-- Counted decompression retains both length cells on early argument and init failures.
77Later memory failure stores the actual output and consumption lengths. -/
78def UncompressCounted
79    (program : BPtr → BPtr → BPtr → BPtr → M Int32) (nullableLengths : Bool) : Prop :=
80  ∀ h dest destLen source sourceLen capacity n src,
81    Fresh h → LibraryGlobals h →
82    (destLen ≠ .null → LengthCell h destLen capacity) →
83    (sourceLen ≠ .null → LengthCell h sourceLen n) →
84    (nullableLengths = false → destLen ≠ .null ∧ sourceLen ≠ .null) →
85    (source ≠ .null → Bytes h source n.toNat src) →
86    (dest ≠ .null → Writable h dest capacity.toNat) →
87    UtilitySeparation dest capacity.toNat source n.toNat destLen sourceLen →
88    ∃ rc after, C.run (program dest destLen source sourceLen) h = .ok (rc, after) ∧
89      (sourceLen = .null ∨ destLen = .null ∨ (source = .null ∧ n ≠ 0) ∨
90        (dest = .null ∧ capacity ≠ 0) → rc = Z_STREAM_ERROR ∧ SameObjects h after) ∧
91      (sourceLen ≠ .null → destLen ≠ .null →
92        (source = .null → n = 0) → (dest = .null → capacity = 0) →
93        ∃ out used got consumed h₁ h₂ expected,
94          Store h dest out h₁ ∧ Store h₁ sourceLen (lengthBytes consumed) h₂ ∧
95          Store h₂ destLen (lengthBytes got) expected ∧ SameObjects expected after ∧
96          Uncompressed (if source = .null then [] else src) capacity.toNat rc out used ∧
97          ((got.toNat = out.length ∧ consumed.toNat = used) ∨
98            (rc = Z_MEM_ERROR ∧ out = [] ∧ got = capacity ∧ consumed = n)) ∧
99          (rc = Z_MEM_ERROR → AllocationFailed h after))
100
101/-- `int uncompress2_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t *sourceLen)`.
102Includes both nullable scalar checks, trailing input, partial output on memory failure and cleanup. -/
103def Goal.uncompress2_z : Prop := UncompressCounted Zlib.Uncompr.uncompress2_z true
104
105/-- `int uncompress2(Bytef *dest, uLongf *destLen, const Bytef *source, uLong *sourceLen)`.
106Both scalar cells are read by the wrapper before the checked `_z` entry. -/
107def Goal.uncompress2 : Prop := UncompressCounted Zlib.Uncompr.uncompress2 false
108
109def UncompressSingle (program : BPtr → BPtr → BPtr → UInt64 → M Int32)
110    (nullableLength : Bool) : Prop :=
111  ∀ h dest destLen source capacity n src,
112    Fresh h → LibraryGlobals h →
113    (destLen ≠ .null → LengthCell h destLen capacity) →
114    (nullableLength = false → destLen ≠ .null) →
115    (source ≠ .null → Bytes h source n.toNat src) →
116    (dest ≠ .null → Writable h dest capacity.toNat) →
117    Separate source n.toNat dest capacity.toNat →
118    Separate destLen 8 dest capacity.toNat → Separate destLen 8 source n.toNat →
119    ∃ rc after, C.run (program dest destLen source n) h = .ok (rc, after) ∧
120      (destLen = .null ∨ (source = .null ∧ n ≠ 0) ∨ (dest = .null ∧ capacity ≠ 0) →
121        rc = Z_STREAM_ERROR ∧ SameObjects h after) ∧
122      (destLen ≠ .null → (source = .null → n = 0) → (dest = .null → capacity = 0) →
123        ∃ out used got h₁ expected,
124          Store h dest out h₁ ∧ Store h₁ destLen (lengthBytes got) expected ∧
125          SameObjects expected after ∧
126          Uncompressed (if source = .null then [] else src) capacity.toNat rc out used ∧
127          (got.toNat = out.length ∨ (rc = Z_MEM_ERROR ∧ out = [] ∧ got = capacity)) ∧
128          (rc = Z_MEM_ERROR → AllocationFailed h after))
129
130/-- `int uncompress_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t sourceLen)`.
131Only the output length is visible. A null output-length cell is a checked argument error. -/
132def Goal.uncompress_z : Prop := UncompressSingle Zlib.Uncompr.uncompress_z true
133
134/-- `int uncompress(Bytef *dest, uLongf *destLen, const Bytef *source, uLong sourceLen)`.
135The output-length cell must be readable before the wrapper calls `_z`. -/
136def Goal.uncompress : Prop := UncompressSingle Zlib.Uncompr.uncompress false
137
138end ZlibF.Spec.Public