CompressFailure.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
3/-!
4# First allocator failure in the concrete compressor
5
6The proof follows `compress2_z`, its automatic stream storage, `deflateInit_`, the default
7parameter checks, and the failed state allocation. It invokes no callee correctness contract.
8-/
9
10namespace ZlibF.Spec.Api.Proofs
11open C Zlib.Compress Zlib.Deflate
12
13private theorem version_index : strIndex ZLIB_VERSION = some 57 := by decide +kernel
14
15private theorem version_run (h : Heap) :
16    Zlib.Zutil.zlibVersion h = .ok (.ref (.str 57) 0, h) := by
17  simp [Zlib.Zutil.zlibVersion, Zlib.Zutil.strLit, strLitRef, version_index]
18
19set_option maxRecDepth 100000 in
20private theorem version_load (h : Heap) : load8 (.ref (.str 57) 0) h = .ok (49, h) := by
21  have hg : Space.get h (BRef.str 57) = some (strBytes ZLIB_VERSION) := by
22    rw [BRef.get_str]
23    rfl
24  exact Ptr.load_ok hg (by decide)
25
26/-- Failure of the first default-allocator call is handled by the actual initialisation path:
27the output length is cleared, the local stream is released, byte memory is unchanged, and the
28set of live blocks is preserved. Automatic storage consumes no allocator-failure index. -/
29theorem compress2_z_first_alloc_failure : Goal.compress2_z_first_alloc_failure := by
30  intro before dest source capacity sourceLen hFresh hfail hdest hsource
31  have hmem : Z_MEM_ERROR ≠ Z_OK := by decide
32  have hslot := hFresh.slotUsed_next
33  have hslotOracle : ({ before with allocOk := fun _ => true } : Heap).slotUsed before.nextBlk = false := hslot
34  have hsource' : ¬ (sourceLen > 0 ∧ source = .null) := fun h => hsource h.1 h.2
35  have hdest' : ¬ (capacity > 0 ∧ dest = .null) := fun h => hdest h.1 h.2
36  have harg : ((sourceLen > 0 && source == .null) || (capacity > 0 && dest == .null)) = false := by
37    apply Bool.eq_false_iff.mpr
38    intro h
39    have hh : (sourceLen > 0 ∧ source = .null) ∨ (capacity > 0 ∧ dest = .null) := by
40      simpa only [Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq] using h
41    exact hh.elim hsource' hdest'
42  have hstream : before.streams before.nextBlk = none := by
43    cases he : before.streams before.nextBlk with
44    | none => rfl
45    | some z =>
46      exact (hFresh _ (Nat.le_refl _) (Or.inr (Or.inr (Or.inl (by simp [he]))))).elim
47  let after : Heap := { before with
48    streams := upd before.streams before.nextBlk none
49    nextBlk := before.nextBlk + 1
50    nalloc := before.nalloc + 1 }
51  refine ⟨after, ?_, rfl, rfl, ?_⟩
52  · simp [after, C.run, compress2_z, harg, allocLocalZ, allocZStream, hslotOracle,
53      zwr, zrd, ldZStream, stZStream, ZStreamRef.get, ZStreamRef.put, ZStreamRef.isRo,
54      version_run, deflateInit_, deflateInit2_, version_load,
55      sizeof_z_stream, Z_DEFAULT_COMPRESSION, Z_DEFLATED, MAX_WBITS, DEF_MEM_LEVEL,
56      Z_DEFAULT_STRATEGY, MAX_MEM_LEVEL, Z_FIXED, zalloc_default, allocDeflateState,
57      hfail, hmem, freeZStream, upd_upd]
58  · intro block
59    simp only [after, Heap.live, upd_apply]
60    by_cases he : block = before.nextBlk
61    · subst block
62      simp [hstream]
63    · simp [he]
64
65end ZlibF.Spec.Api.Proofs