QueryLayout.lean

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

1import ZlibF.Spec.Public.StreamQueries
2import ZlibF.Proof.«inflate.c.misc»
3
4/-! Fixed C array layout for the public decode-table query. The legacy counterexample
5is an impossible C object shape, not a reachable library bug. -/
6namespace ZlibF.Spec.Public.Proofs
7open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs
8
9private theorem refused_dom {h : Heap} {p : ZStreamPtr} (hr : RefusedInflate h p) : StreamDom h p := by
10  rcases hr with hnull | ⟨r,z,rfl,hz,hbad⟩
11  · exact Or.inl hnull
12  · refine Or.inr ⟨r,z,rfl,hz,?_⟩
13    rcases hbad with hza | hzf | hs | ⟨i,s,hstate,hsi,_⟩
14    · exact Or.inl hza
15    · exact Or.inr (Or.inl hzf)
16    · exact Or.inr (Or.inr (Or.inl hs))
17    · exact Or.inr (Or.inr (Or.inr ⟨i,s,hstate,hsi⟩))
18
19private theorem refused_not_initialised {h : Heap} {p : ZStreamPtr} (hr : RefusedInflate h p) : ¬ Initialised h p := by
20  intro ⟨r',i',z',s',hp,hL⟩
21  rcases hr with hn | ⟨r,z,hp',hz,hbad⟩
22  · rw [hn] at hp; cases hp
23  · rw [hp'] at hp
24    cases hp
25    have heq : z = z' := Option.some.inj (hz.symm.trans hL.hz)
26    subst z'
27    rcases hbad with ha | hf | hstate | ⟨i,s,hi,hs,hfail⟩
28    · exact hL.zalloc ha
29    · exact hL.zfree hf
30    · have hh := hL.zst
31      rw [hstate] at hh; cases hh
32    · have hieq : i = i' := by
33        have hh := hL.zst
34        rw [hi] at hh
35        cases hh
36        rfl
37      subst i'
38      have hseq : s = s' := Option.some.inj (hs.symm.trans hL.hs)
39      subst s'
40      rcases hfail with hback | hlo | hhi
41      · exact hback hL.back
42      · exact (UInt32.not_lt.mpr hL.mode.1) hlo
43      · exact (UInt32.not_lt.mpr hL.mode.2) hhi
44
45private theorem refused_state_check {h : Heap} {p : ZStreamPtr} (hr : RefusedInflate h p) :
46    inflateStateCheck p h = .ok (1, h) := by
47  obtain ⟨v, hv, hclass⟩ := inflateStateCheck_total (refused_dom hr)
48  rcases hclass with ⟨_, hi⟩ | ⟨rfl, _⟩
49  · exact (refused_not_initialised hr hi).elim
50  · exact hv
51
52/-- The fixed C array bounds make pointer subtraction representable. No callee contract is assumed. -/
53theorem codes_used_record {h : Heap} {r : ZStreamRef} {i : Nat}
54    {z : ZStream} {s : InflateState} {n : Nat}
55    (hv : InflateView h r i z s) (hsize : s.codes.size = 1444)
56    (hnext : s.next = .ref (.istate_codes i) n) (hn : n ≤ s.codes.size) :
57    C.run (inflateCodesUsed (some r)) h = .ok (UInt64.ofNat n, h) := by
58  rcases hv with ⟨hz,hstate,hi,hback,ha,hf,hlo,hhi⟩
59  have hl : Live h r i z s := ⟨hz,hi,hstate,hback,⟨hlo,hhi⟩,ha,hf⟩
60  have hc : Space.get h (CodeRef.istate_codes i) = some s.codes := by simp [Space.get, hl.hs]
61  have hd := Ptr.diff_ok hc (show n ≤ s.codes.size from hn)
62    (show 0 ≤ s.codes.size by omega)
63    (show -(2 ^ 63 : Int) ≤ (n : Int) - (0 : Nat) ∧ (n : Int) - (0 : Nat) < 2 ^ 63 by omega)
64  have hd' : Ptr.diff (Ptr.ref (CodeRef.istate_codes i) n) (Ptr.ref (CodeRef.istate_codes i) 0) h =
65      .ok (Int64.ofInt ((n : Int) - (0 : Nat)), h) := hd
66  unfold C.run inflateCodesUsed
67  isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, hnext, codesP, hd']
68  simp [ofInt_toUInt64]
69
70/-- `unsigned long inflateCodesUsed(z_streamp strm)` includes clean refusal and the source's fixed array layout. -/
71theorem inflate_codes_used : Goal.inflateCodesUsed := by
72  constructor
73  · intro h p hr
74    unfold C.run inflateCodesUsed
75    isimp [refused_state_check hr]
76  · intro h r i z s n hv hsize hnext hn
77    exact codes_used_record hv hsize hnext hn
78
79/-- The ordinary init-established invariant entails the fixed-layout condition. -/
80theorem codes_layout_of_good {h : Heap} {r : ZStreamRef} {i : Nat}
81    {z : ZStream} {s : InflateState} (hg : Good h r i z s) : s.codes.size = 1444 :=
82  hg.inv.wf.2.2
83
84/-- The former query condition omitted the fixed C array layout. -/
85def legacyCodesUsed : Prop :=
86  CheckedInflate Zlib.Inflate.inflateCodesUsed 0xffffffffffffffff <|
87  ∀ h r i z s n, InflateView h r i z s →
88    s.next = .ref (.istate_codes i) n → n ≤ s.codes.size →
89    C.run (Zlib.Inflate.inflateCodesUsed (some r)) h = .ok (UInt64.ofNat n, h)
90
91def badSize : Nat := 2 ^ 63
92
93def hugeZ : ZStream := { (default : ZStream) with
94  zalloc := .fn "zcalloc", zfree := .fn "zcfree", state := some (.inflate 1) }
95def hugeS (a : Array Code) : InflateState := { (default : InflateState) with
96  strm := some (.tab 0), mode := HEAD, next := .ref (.istate_codes 1) badSize, codes := a }
97def hugeH (a : Array Code) : Heap := { Heap.empty with
98  streams := ⟨#[some hugeZ]⟩, istates := ⟨#[none, some (hugeS a)]⟩ }
99
100theorem huge_view (a : Array Code) : InflateView (hugeH a) (.tab 0) 1 hugeZ (hugeS a) := by
101  simp [InflateView, hugeH, hugeS, hugeZ, ZStreamRef.get, Tbl.get, StateRef.ofInflateState, HEAD, SYNC]
102
103theorem huge_result (a : Array Code) (ha : badSize ≤ a.size) :
104    C.run (inflateCodesUsed (some (.tab 0))) (hugeH a) =
105      .error (.ub "pointer difference is not a ptrdiff_t") := by
106  have hl : Live (hugeH a) (.tab 0) 1 hugeZ (hugeS a) := by
107    obtain ⟨hz,hstate,hi,hback,ha,hf,hlo,hhi⟩ := huge_view a
108    exact ⟨hz,hi,hstate,hback,⟨hlo,hhi⟩,ha,hf⟩
109  have hd : Ptr.diff (Ptr.ref (CodeRef.istate_codes 1) badSize) (Ptr.ref (CodeRef.istate_codes 1) 0) (hugeH a) =
110      .error (.ub "pointer difference is not a ptrdiff_t") := by
111    have hb : 9223372036854775808 ≤ a.size := by simpa [badSize] using ha
112    simp [Ptr.diff, Space.get, hugeH, hugeS, Tbl.get, hb, badSize]
113  unfold C.run inflateCodesUsed
114  isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, hugeS, codesP, hd]
115
116theorem legacy_codes_used_false (a : Array Code) (ha : badSize ≤ a.size) : ¬ legacyCodesUsed := by
117  intro hg
118  have hp := hg.2 (hugeH a) (.tab 0) 1 hugeZ (hugeS a) badSize (huge_view a) rfl ha
119  rw [huge_result a ha] at hp
120  cases hp
121
122/-- The old public condition admits a pointer difference outside ptrdiff_t. -/
123theorem legacy_codes_used_impossible : ¬ legacyCodesUsed := by
124  apply legacy_codes_used_false (Array.replicate badSize (default : Code))
125  simp
126
127
128end ZlibF.Spec.Public.Proofs