CompressBoundary.lean

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

1import ZlibF.Spec.Api.Concrete
2
3namespace ZlibF.Spec.Api.Proofs
4
5/-- Argument rejection precedes clearing the scalar or initialising a compressor:
6the `_z` model writes no bytes and preserves the initial capacity when it has a scalar. -/
7theorem compress2Z_rejected {c : CompressCall} {r : CompressResult}
8    (hrejected : c.rejected) (hr : Compress2Z c r) :
9    r.rc = Z.streamError ∧ r.produced = [] ∧
10      r.storedLength = (if c.lengthNull then none else some c.capacity) := by
11  simpa only [Compress2Z, ite_eq_left hrejected] using hr
12
13/-- A null destination with zero capacity reaches initialisation. For valid parameters
14its only model outcomes are allocation failure or the inner stream error, with zero output
15and the scalar cleared. -/
16theorem compress2Z_null_zero_iff {c : CompressCall} {r : CompressResult} {p : DeflParams}
17    (hdest : c.destNull = true) (hcap : c.capacity = 0)
18    (hsource : c.sourceNull = false) (hlength : c.lengthNull = false)
19    (hparams : compressParams c.level = some p) :
20    Compress2Z c r ↔
21      (r.rc = Z.memError ∨ r.rc = Z.streamError) ∧ r.produced = [] ∧
22        r.storedLength = some 0 := by
23  simp [Compress2Z, CompressCall.rejected, hdest, hcap, hsource, hlength, hparams]
24
25/-- The compatibility-wrapper model has no defined outcome for a null length pointer. -/
26theorem compress2Wrapper_null_length {c : CompressCall} {r : CompressResult}
27    (hlength : c.lengthNull = true) : ¬ Compress2Wrapper c r := by
28  simp [Compress2Wrapper, hlength]
29
30/-- A missing scalar is a clean error in the actual translated `_z` entry, on every heap. -/
31theorem compress2_z_null_length_returns (dest source : C.BPtr) (sourceLen : UInt64)
32    (level : Int32) (h : C.Heap) :
33    Concrete.compress2_z dest none source sourceLen level h =
34      .ret h (C.Z_STREAM_ERROR, none) := by
35  rfl
36
37/-- A missing scalar faults in the actual translated compatibility wrapper before `_z`
38can perform its argument checks, on every heap. -/
39theorem compress2_null_length_faults (dest source : C.BPtr) (sourceLen : UInt64)
40    (level : Int32) (h : C.Heap) :
41    Concrete.compress2 dest none source sourceLen level h = .fault := by
42  rfl
43
44/-- Positive model witness: a null source with nonempty input is rejected even for a bad level;
45the original length survives. -/
46theorem compress2Z_source_null_witness :
47    Compress2Z ⟨[0], 7, 10, true, false, false⟩ ⟨Z.streamError, [], some 7⟩ := by
48  simp [Compress2Z, CompressCall.rejected]
49
50/-- Positive model witness: a null scalar is rejected without a stored length, before level
51validation or the positive-capacity null-destination check. -/
52theorem compress2Z_length_null_witness :
53    Compress2Z ⟨[], 7, 10, true, true, true⟩ ⟨Z.streamError, [], none⟩ := by
54  simp [Compress2Z, CompressCall.rejected]
55
56/-- Positive model witness: a null destination with positive capacity is an early argument
57error, so the original length survives. -/
58theorem compress2Z_dest_null_positive_witness :
59    Compress2Z ⟨[0], 7, 10, false, true, false⟩ ⟨Z.streamError, [], some 7⟩ := by
60  simp [Compress2Z, CompressCall.rejected]
61
62/-- Positive model witness: a bad level with acceptable pointer shapes is rejected after
63clearing the scalar. -/
64theorem compress2Z_invalid_level_witness :
65    Compress2Z ⟨[0], 7, 10, false, false, false⟩ ⟨Z.streamError, [], some 0⟩ := by
66  simp [Compress2Z, CompressCall.rejected, compressParams, deflInit?]
67
68/-- Positive model witness: the zero-capacity null destination may fail allocation. -/
69theorem compress2Z_null_zero_mem_witness :
70    Compress2Z ⟨[0], 0, 6, false, true, false⟩ ⟨Z.memError, [], some 0⟩ := by
71  simp [Compress2Z, CompressCall.rejected, compressParams, deflInit?]
72
73/-- Positive model witness: after successful initialisation, the zero-capacity null
74destination is refused by the inner compressor. -/
75theorem compress2Z_null_zero_stream_witness :
76    Compress2Z ⟨[0], 0, 6, false, true, false⟩ ⟨Z.streamError, [], some 0⟩ := by
77  simp [Compress2Z, CompressCall.rejected, compressParams, deflInit?]
78
79end ZlibF.Spec.Api.Proofs