inflate-init2-table-shape.lean

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

1import ZlibF.Proof.«public-inflate-init»
2
3open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs ZlibF.Spec.Public ZlibF.Spec
4open ZlibF.Spec.Public.Proofs.InflateInit
5
6/-! The invalid-window path allocates and frees a state. The finite table backing
7`istates` grows from zero entries to four. `SameObjects` requires structural
8equality, so the current public goal does not hold for this valid initial heap. -/
9namespace Init2Counterexample
10
11def r : ZStreamRef := .tab 0
12def v : BPtr := .ref (.blk 1) 0
13
14theorem domain : InitDomain witnessHeap r v := public_witness_domain
15
16theorem default_get : r.get witnessHeap = some default := by
17  rfl
18
19theorem defaults : DefaultOrNull (default : ZStream) := by
20  exact ⟨Or.inl rfl, Or.inl rfl⟩
21
22theorem alloc_ok : witnessHeap.allocOk witnessHeap.nalloc = true := by rfl
23
24theorem bad_params : reset2Params (1 : Int32) = none := by decide
25
26theorem actual : C.run (inflateInit2_ (some r) 1 v 112) witnessHeap =
27    .ok (Z_STREAM_ERROR, initBadHeap witnessHeap r default) := by
28  obtain ⟨hn, hv⟩ := version_value_read domain.2.2.2.1
29  exact inflateInit2_badbits default_get domain.1 alloc_ok defaults.1 defaults.2 hn hv bad_params
30
31theorem actual_table_size : (initBadHeap witnessHeap r default).istates.arr.size = 4 := by
32  rfl
33
34theorem expected_table_size :
35    (r.put witnessHeap { preparedStream default with state := none }).istates.arr.size = 0 := by
36  rfl
37
38theorem shapes_differ :
39    (initBadHeap witnessHeap r default).istates.arr.size ≠
40      (r.put witnessHeap { preparedStream default with state := none }).istates.arr.size := by
41  rw [actual_table_size, expected_table_size]
42  decide
43
44theorem goal_false : ¬ Goal.inflateInit2_ := by
45  intro goal
46  obtain ⟨hf, hu, hg, hv, _, _, _, _⟩ := domain
47  obtain ⟨rc, after, hr, _, post⟩ := (goal 1).2.2 witnessHeap r default v hf hu hg default_get defaults hv
48  rw [actual] at hr
49  cases hr
50  have same : SameObjects (r.put witnessHeap { preparedStream default with state := none })
51      (initBadHeap witnessHeap r default) := by
52    simpa [alloc_ok, Api.inflWbits] using post
53  have e := congrArg (fun table => table.arr.size) same.2.2.2.2.2.2.1
54  exact shapes_differ e
55
56#print axioms goal_false
57end Init2Counterexample