inflate.c.witness.lean

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

1import ZlibF.Proof.«inflate.c.window»
2
3/-!
4# inflate.c: non-vacuity witnesses for the stream-management theorems
5
6A heap with one writable `z_stream` (all zero: the caller gave no allocator functions) and nothing else. The real
7`inflateInit2_` runs on it (through `inflateInit2_ok`, whose hypotheses are checked here), and the heap it makes
8satisfies the hypotheses (`Good`) of `inflateResetKeep_safe`, `inflateReset_safe`, `inflateReset2_safe`,
9`inflateEnd_safe` and `inflateStateCheck_total`, which are then applied to it.
10-/
11
12namespace Zlib.Inflate.Witness
13open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs
14
15/-- One stream (block 0, all zero: no allocator functions) and a read-only byte block 1 holding "1" (the version
16string's first character); the next free block is 2. -/
17def h0 : Heap :=
18  { Heap.empty with
19    streams := upd Heap.empty.streams 0 (some ZStream.zeroed),
20    bytes := upd Heap.empty.bytes 1 (some #[49, 0]),
21    ro := upd Heap.empty.ro 1 true,
22    nextBlk := 2 }
23
24theorem h0_uniq : Uniq h0 := by
25  intro b
26  by_cases h1 : b = 1
27  · subst h1; simp [h0, Heap.empty, upd_ne _ _ _ _ (by decide : (1 : Nat) ≠ 0)]
28  by_cases h0' : b = 0
29  · subst h0'; simp [h0, Heap.empty, upd_ne _ _ _ _ (by decide : (0 : Nat) ≠ 1)]
30  · simp [h0, Heap.empty, upd_ne _ _ _ _ h1, upd_ne _ _ _ _ h0']
31
32theorem h0_fresh : Fresh h0 := by
33  intro b hb hl
34  have hb' : 2 ≤ b := hb
35  have h1 : b ≠ 1 := by omega
36  have h0' : b ≠ 0 := by omega
37  simp [Heap.live, h0, Heap.empty, upd_ne _ _ _ _ h1, upd_ne _ _ _ _ h0'] at hl
38
39theorem h0_get : (ZStreamRef.tab 0).get h0 = some ZStream.zeroed := by
40  simp [ZStreamRef.get, h0, upd_ne _ _ _ _ (by decide : (0 : Nat) ≠ 1)]
41
42theorem h0_version : OkOn h0 (index8 (.ref (.blk 1) 0) 0) 49 := by
43  have := index8_ok (h := h0) (blk := 1) (off := 0) (i := 0) (bytes := #[49, 0]) (by simp [h0]) (by simp)
44  simpa using this
45
46theorem params15 : reset2Params 15 = some (5, 15) := by decide
47
48/-- The real `inflateInit2_` runs on `h0` (all hypotheses of `inflateInit2_ok` hold there) and makes a heap that
49satisfies the hypotheses `Good` of the other theorems. -/
50theorem init_witness : ∃ (h1 : Heap) (z1 : ZStream) (st1 : InflateState),
51    C.run (inflateInit2_ (some (.tab 0)) 15 (.ref (.blk 1) 0) 112) h0 = .ok (Z_OK, h1) ∧
52    Good h1 (.tab 0) 2 z1 st1 ∧ z1.zfree = .fn "zcfree" := by
53  obtain ⟨h1, hr, -, hG, -⟩ := inflateInit2_ok (r := .tab 0) (z := ZStream.zeroed) (w := 15) (version := .ref (.blk 1) 0)
54    h0_uniq h0_fresh h0_get (by simp [h0, Heap.empty]) (Or.inl rfl) (Or.inl rfl) (by simp) h0_version params15 |>.imp
55    fun h' hh => hh
56  refine ⟨h1, _, _, hr, hG, ?_⟩
57  have e : ZStream.zeroed.zfree = FnPtr.null := rfl
58  simp [resetKeepStream, initStream2, initStream, e]
59
60end Zlib.Inflate.Witness