infback.c.callbacks.lean

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

1import ZlibF.Proof.«infback.c.end»
2import ZlibF.Zlib.«crc32.c»
3import ZlibF.Zlib.«trees.c»
4
5/-!
6# infback.c: the contract of the two call-backs
7
8`inflateBack(strm, in, in_desc, out, out_desc)` takes the caller's functions as parameters. They are caller code, not
9library code, so a theorem about `inflateBack` is stated for all call-backs that keep the documented contract of `zlib.h`:
10
11* `in`: "`in()` ... returns the number of bytes available ... and sets `*buf` to point to them; it returns zero if no
12  more input is available". The bytes must stay valid and unchanged until the next call of `in` or until `inflateBack`
13  returns.
14* `out`: "should return zero on success, or non-zero on failure". It receives `len` bytes at `buf` (a pointer into the
15  window) and may read them.
16* "Neither `in()` nor `out()` are permitted to change the contents of the window provided to `inflateBackInit()`", and
17  neither may call into the same stream: they do not touch the stream or its state.
18
19The heap form (`CbContract`): each call changes only byte blocks of the call-back's own set (`ownI` for `in`, `ownO` for
20`out`), never the window, never a record table, and allocates and frees nothing. The two own sets are disjoint, so a
21buffer that `in` returned cannot change before the next call of `in`. `R` is the call-back's own invariant (for example
22"my input buffer is intact"); it depends only on the own blocks, and each call keeps it. The tables are compared
23pointwise.
24
25Narrower than `zlib.h` (listed in `docs/proof/callbacks.md`): a call-back does not allocate or free heap blocks, and
26the input buffer is a byte block of the heap.
27-/
28
29namespace Zlib.Infback.Spec
30open C Zlib.Inflate Zlib.Inflate.Spec
31
32/-- The heap `h'` after a call-back that may write only the byte blocks in `own`: every table entry outside `own` is
33as before, the shape of the heap (which blocks are live) and the allocator are untouched. -/
34structure CbFrame (own : Nat → Prop) (h h' : Heap) : Prop where
35  bytes : ∀ b, ¬ own b → h'.bytes b = h.bytes b
36  live : ∀ b, (h'.bytes b).isSome = (h.bytes b).isSome
37  words : ∀ b, h'.words b = h.words b
38  ro : ∀ b, h'.ro b = h.ro b
39  streams : ∀ b, h'.streams b = h.streams b
40  gzheaders : ∀ b, h'.gzheaders b = h.gzheaders b
41  dstates : ∀ b, h'.dstates b = h.dstates b
42  istates : ∀ b, h'.istates b = h.istates b
43  gzstates : ∀ b, h'.gzstates b = h.gzstates b
44  static : h'.static = h.static
45  nextBlk : h'.nextBlk = h.nextBlk
46  nalloc : h'.nalloc = h.nalloc
47  allocOk : h'.allocOk = h.allocOk
48  garbage : h'.garbage = h.garbage
49
50/-- `n` readable bytes start at `p` (a pointer into a byte block of `h`). -/
51def ReadableAt (h : Heap) (p : BPtr) (n : Nat) : Prop :=
52  ∃ b off a, p = .ref (.blk b) off ∧ h.bytes b = some a ∧ off + n ≤ a.size
53
54/-- **The contract of the call-backs of `inflateBack`.** `inCb`/`outCb` are the functions, `inDesc`/`outDesc` the
55descriptors, `win` the block number of the window, `ownI`/`ownO` the byte blocks that `in` and `out` may write, `R` their
56own invariant. See the file comment for the `zlib.h` text. -/
57structure CbContract (inCb : InCb) (inDesc : BPtr) (outCb : OutCb) (outDesc : BPtr) (win : Nat)
58    (ownI ownO : Nat → Prop) (R : Heap → Prop) : Prop where
59  /-- the window belongs to neither call-back, and the two own sets are disjoint -/
60  disj : ¬ ownI win ∧ ¬ ownO win ∧ ∀ b, ownI b → ¬ ownO b
61  /-- `R` depends on the own blocks only -/
62  local_ : ∀ h h', (∀ b, (ownI b ∨ ownO b) → h'.bytes b = h.bytes b) → (R h ↔ R h')
63  /-- `in`: returns the count and the new `*buf`; a non-zero count comes with that many readable bytes in an
64  own block, which `out` cannot change -/
65  inOk : ∀ h nx, R h → ∃ n nx' h', inCb inDesc nx h = .ok ((n, nx'), h') ∧ CbFrame ownI h h' ∧ R h' ∧
66    (n ≠ 0 → ∃ b off a, nx' = .ref (.blk b) off ∧ ownI b ∧ h'.bytes b = some a ∧ off + n.toNat ≤ a.size)
67  /-- `out`: called with `len` readable bytes (the window), returns a result and keeps the frame -/
68  outOk : ∀ h p len, R h → ReadableAt h p len.toNat → ∃ r h', outCb outDesc p len h = .ok (r, h') ∧ CbFrame ownO h h' ∧ R h'
69
70end Zlib.Infback.Spec
71
72namespace Zlib.Infback.Proofs
73open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Infback Zlib.Infback.Spec
74
75theorem CbFrame.refl (own : Nat → Prop) (h : Heap) : CbFrame own h h :=
76  ⟨fun _ _ => rfl, fun _ => rfl, fun _ => rfl, fun _ => rfl, fun _ => rfl, fun _ => rfl, fun _ => rfl, fun _ => rfl,
77    fun _ => rfl, rfl, rfl, rfl, rfl, rfl⟩
78
79/-- A call-back frame keeps the stream records: `get` of a stream reference is unchanged. -/
80theorem CbFrame.zget {own : Nat → Prop} {h h' : Heap} (f : CbFrame own h h') (r : ZStreamRef) : r.get h' = r.get h := by
81  cases r with
82  | tab i => simp [ZStreamRef.get, f.streams]
83  | in_gzstate_strm i => simp [ZStreamRef.get, f.gzstates]
84
85/-- The simplest call-backs: `in` has no input (returns 0) and `out` accepts everything (returns 0). -/
86def eofIn : InCb := fun _ nx => pure (0, nx)
87def okOut : OutCb := fun _ _ _ => pure 0
88
89/-- The trivial call-backs keep the contract, with no own blocks and `R` always true. -/
90theorem cbContract_eof (win : Nat) : CbContract eofIn .null okOut .null win (fun _ => False) (fun _ => False) (fun _ => True) :=
91  ⟨⟨fun h => h.elim, fun h => h.elim, fun _ h => h.elim⟩, fun _ _ _ => Iff.rfl,
92   fun h nx _ => ⟨0, nx, h, rfl, CbFrame.refl _ _, trivial, fun e => absurd rfl e⟩,
93   fun h _ _ _ _ => ⟨0, h, rfl, CbFrame.refl _ _, trivial⟩⟩
94
95/-- An `out` that always fails (returns 1): the same contract. -/
96def failOut : OutCb := fun _ _ _ => pure 1
97
98theorem cbContract_fail (win : Nat) :
99    CbContract eofIn .null failOut .null win (fun _ => False) (fun _ => False) (fun _ => True) :=
100  ⟨⟨fun h => h.elim, fun h => h.elim, fun _ h => h.elim⟩, fun _ _ _ => Iff.rfl,
101   fun h nx _ => ⟨0, nx, h, rfl, CbFrame.refl _ _, trivial, fun e => absurd rfl e⟩,
102   fun h _ _ _ _ => ⟨1, h, rfl, CbFrame.refl _ _, trivial⟩⟩
103
104/-! ### Non-vacuity on a heap made by the real `inflateBackInit_`
105
106The heap has all static tables of the library, a stream record (block 0), a window of 256 bytes (block 1) and the
107release string `"1.3.2"` (block 2). -/
108
109/-- `Heap.empty` with every static table of the library installed. -/
110def staticHeap : Heap :=
111  { Heap.empty with static :=
112      Zlib.Crc32.initStatics (Zlib.Inftrees.initStatics (Zlib.Trees.trees_statics Heap.empty.static)) }
113
114/-- The initial heap: `staticHeap`, the stream `ZStream.zeroed` (so `zalloc`, `zfree` are `NULL`), the window block and
115the release string, with every allocation succeeding. -/
116def wit0 : Heap :=
117  { staticHeap with
118    bytes := upd (upd staticHeap.bytes 1 (some (Array.replicate 256 0))) 2 (some #[49, 46, 51, 46, 50, 0]),
119    streams := upd staticHeap.streams 0 (some ZStream.zeroed),
120    nextBlk := 3,
121    allocOk := fun _ => true }
122
123theorem wit0_uniq : Uniq wit0 := by
124  intro b
125  by_cases h1 : b = 1
126  · subst h1; simp [wit0, staticHeap, Heap.empty, cnt]
127  by_cases h2 : b = 2
128  · subst h2; simp [wit0, staticHeap, Heap.empty, cnt]
129  by_cases h0 : b = 0
130  · subst h0; simp [wit0, staticHeap, Heap.empty, cnt]
131  simp [wit0, staticHeap, Heap.empty, cnt, upd_ne _ _ _ _ h1, upd_ne _ _ _ _ h2, upd_ne _ _ _ _ h0]
132
133theorem wit0_fresh : Fresh wit0 := by
134  intro b hb hl
135  have h1 : b ≠ 1 := by simp [wit0] at hb; omega
136  have h2 : b ≠ 2 := by simp [wit0] at hb; omega
137  have h0 : b ≠ 0 := by simp [wit0] at hb; omega
138  simp [Heap.live, wit0, staticHeap, Heap.empty, upd_ne _ _ _ _ h1, upd_ne _ _ _ _ h2, upd_ne _ _ _ _ h0] at hl
139
140/-- **Witness.** The real `inflateBackInit_(strm, 8, window, "1.3.2", 112)` runs on `wit0` and returns `Z_OK`, and on the
141resulting heap the invariant `BackGood` holds together with the call-back contract for `eofIn` with `okOut` (and
142with `failOut`). So the hypotheses of the `inflateBack` theorems are satisfiable by a real `inflateBackInit_` heap. -/
143theorem backInit_witness :
144    ∃ h' z st, C.run (inflateBackInit_ (some (.tab 0)) 8 (.ref (.blk 1) 0) (.ref (.blk 2) 0) 112) wit0 = .ok (Z_OK, h') ∧
145      BackGood h' (.tab 0) 3 z st ∧
146      CbContract eofIn .null okOut .null 1 (fun _ => False) (fun _ => False) (fun _ => True) ∧
147      CbContract eofIn .null failOut .null 1 (fun _ => False) (fun _ => False) (fun _ => True) := by
148  have hz : (ZStreamRef.tab 0).get wit0 = some ZStream.zeroed := by
149    simp [ZStreamRef.get, wit0]
150  have hwin : WindowOk wit0 (.ref (.blk 1) 0) (2 ^ (i2u 8).toNat) :=
151    ⟨1, 0, Array.replicate 256 0, rfl, by simp [wit0], by simp [wit0, staticHeap, Heap.empty], by rw [Array.size_replicate]; decide⟩
152  obtain ⟨h', hr, -, hG, -⟩ := inflateBackInit__ok (r := .tab 0) (z := ZStream.zeroed) (wb := 8) (window := .ref (.blk 1) 0)
153    (version := .ref (.blk 2) 0) wit0_uniq wit0_fresh hz (by simp [wit0]) (Or.inl rfl) (Or.inl rfl) (by intro c; cases c)
154    (by unfold OkOn; simp [index8, wit0]; rfl) (by decide) (by decide) hwin
155  exact ⟨h', _, _, hr, by simpa [wit0] using hG, cbContract_eof 1, cbContract_fail 1⟩
156
157end Zlib.Infback.Proofs