public-inflate-prime.lean

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

1import ZlibF.Proof.«public-inflate-small-queries»
2
3namespace ZlibF.Spec.Public.InflatePrimeProof
4open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs ZlibF.Spec.Public.InflateQueryProof
5
6def primeBits (bits value : Int32) : UInt64 :=
7  Zlib.Inflate.i2ul ((value.toInt64 &&& (((1 : Int64) <<< bits.toInt64) - 1)).toInt32)
8
9/-- The state after `inflatePrime` inserted `bits` bits (`1 ≤ bits ≤ 16`, they fit): `hold += value << bits_in_hold`. -/
10def primeState (bits value : Int32) (st : InflateState) : InflateState :=
11  { st with hold := st.hold + (primeBits bits value <<< st.bits.toUInt64), bits := st.bits + Zlib.Inflate.i2u bits }
12
13theorem i2u_toNat {b : Int32} (h0 : 0 ≤ b.toInt) : (i2u b).toNat = b.toInt.toNat := by
14  unfold i2u
15  rw [Int32.toNat_toUInt32_of_le (by rw [Int32.le_iff_toInt_le]; simpa using h0)]
16  rfl
17
18theorem int32_pos {b : Int32} (h : 0 < b) : 0 < b.toInt := by
19  have := Int32.lt_iff_toInt_lt.mp h; simpa using this
20
21theorem int32_neg_lt {b : Int32} (h : b < 0) : b.toInt < 0 := by
22  have := Int32.lt_iff_toInt_lt.mp h; simpa using this
23
24theorem int32_gt16 {b : Int32} : 16 < b ↔ 16 < b.toInt := by
25  rw [Int32.lt_iff_toInt_lt]
26  change (16 : Int) < b.toInt ↔ 16 < b.toInt
27  rfl
28
29theorem inflatePrime_record {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
30    (hl : Live h r zs z st) (hb39 : st.bits.toNat ≤ 39) (bits value : Int32) :
31    (bits = 0 → C.run (inflatePrime (some r) bits value) h = .ok (Z_OK, h)) ∧
32    (bits < 0 → C.run (inflatePrime (some r) bits value) h = .ok (Z_OK, setI h zs { st with hold := 0, bits := 0 })) ∧
33    (0 < bits → (16 < bits.toInt ∨ 32 < st.bits.toNat + bits.toInt.toNat) →
34      C.run (inflatePrime (some r) bits value) h = .ok (Z_STREAM_ERROR, h)) ∧
35    (0 < bits → bits.toInt ≤ 16 → st.bits.toNat + bits.toInt.toNat ≤ 32 →
36      C.run (inflatePrime (some r) bits value) h = .ok (Z_OK, setI h zs (primeState bits value st))) := by
37  refine ⟨fun h0 => ?_, fun hn => ?_, fun hp hbad => ?_, fun hp h16 hfit => ?_⟩
38  · subst h0
39    show inflatePrime (some r) 0 value h = _
40    unfold inflatePrime; isimp [stateCheck_live hl]
41  · have h0 : bits ≠ 0 := by intro e; subst e; have := int32_neg_lt hn; simp at this
42    show inflatePrime (some r) bits value h = _
43    unfold inflatePrime; isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, h0, hn]
44  · have hpi := int32_pos hp
45    have h0 : bits ≠ 0 := by intro e; subst e; simp at hpi
46    have hn : ¬ bits < 0 := fun hn => by have := int32_neg_lt hn; omega
47    show inflatePrime (some r) bits value h = _
48    unfold inflatePrime
49    by_cases h16 : 16 < bits
50    · isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, h0, hn, h16]
51    · have h16'' : ¬ 16 < bits.toInt := fun hh => h16 (int32_gt16.mpr hh)
52      have hgt : 32 < st.bits + i2u bits := by
53        rw [UInt32.lt_iff_toNat_lt, UInt32.toNat_add, i2u_toNat (by omega), Nat.mod_eq_of_lt (by omega)]
54        have : (32 : UInt32).toNat = 32 := rfl
55        omega
56      isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, h0, hn, h16, hgt]
57  · have hpi := int32_pos hp
58    have h0 : bits ≠ 0 := by intro e; subst e; simp at hpi
59    have hn : ¬ bits < 0 := fun hn => by have := int32_neg_lt hn; omega
60    have h16 : ¬ 16 < bits := fun hh => by have := int32_gt16.mp hh; omega
61    have hu := i2u_toNat (b := bits) (by omega)
62    have hgt : ¬ 32 < st.bits + i2u bits := by
63      rw [UInt32.lt_iff_toNat_lt, UInt32.toNat_add, hu, Nat.mod_eq_of_lt (by omega)]
64      have : (32 : UInt32).toNat = 32 := rfl
65      omega
66    have hlt : st.bits < 64 := by rw [UInt32.lt_iff_toNat_lt]; have : (64 : UInt32).toNat = 64 := rfl; omega
67    show inflatePrime (some r) bits value h = _
68    unfold inflatePrime
69    isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, h0, hn, h16, hgt, shl64, hlt, primeState, primeBits]
70
71/-- The source long-width mask agrees with the public unsigned mask for every
72accepted positive count. -/
73theorem primeBits_public (bits value : Int32) (h0 : 0 < bits.toInt) (h16 : bits.toInt ≤ 16) :
74    primeBits bits value = (value.toUInt32 &&& ((1 <<< bits.toUInt32) - 1)).toUInt64 := by
75  have hc : bits.toInt = 1 ∨ bits.toInt = 2 ∨ bits.toInt = 3 ∨ bits.toInt = 4 ∨ bits.toInt = 5 ∨ bits.toInt = 6 ∨ bits.toInt = 7 ∨ bits.toInt = 8 ∨ bits.toInt = 9 ∨ bits.toInt = 10 ∨ bits.toInt = 11 ∨ bits.toInt = 12 ∨ bits.toInt = 13 ∨ bits.toInt = 14 ∨ bits.toInt = 15 ∨ bits.toInt = 16 := by omega
76  have hb : bits = Int32.ofInt bits.toInt := (Int32.ofInt_toInt bits).symm
77  rcases hc with hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase
78  all_goals
79    rw [hcase] at hb
80    subst bits
81    unfold primeBits i2ul
82    apply UInt64.toBitVec_inj.mp
83    apply BitVec.eq_of_getLsbD_eq
84    intro i
85    by_cases hi : i < 32
86    · simp [BitVec.getLsbD_signExtend, hi]
87    · have hpow : 2 ^ 16 ≤ 2 ^ i := Nat.pow_le_pow_right (by decide) (by omega)
88      simp [BitVec.getLsbD_signExtend, BitVec.getLsbD_ofNat, hi,
89        Nat.testBit_lt_two_pow (show 1 < 2 ^ i by omega),
90        Nat.testBit_lt_two_pow (show 3 < 2 ^ i by omega),
91        Nat.testBit_lt_two_pow (show 7 < 2 ^ i by omega),
92        Nat.testBit_lt_two_pow (show 15 < 2 ^ i by omega),
93        Nat.testBit_lt_two_pow (show 31 < 2 ^ i by omega),
94        Nat.testBit_lt_two_pow (show 63 < 2 ^ i by omega),
95        Nat.testBit_lt_two_pow (show 127 < 2 ^ i by omega),
96        Nat.testBit_lt_two_pow (show 255 < 2 ^ i by omega),
97        Nat.testBit_lt_two_pow (show 511 < 2 ^ i by omega),
98        Nat.testBit_lt_two_pow (show 1023 < 2 ^ i by omega),
99        Nat.testBit_lt_two_pow (show 2047 < 2 ^ i by omega),
100        Nat.testBit_lt_two_pow (show 4095 < 2 ^ i by omega),
101        Nat.testBit_lt_two_pow (show 8191 < 2 ^ i by omega),
102        Nat.testBit_lt_two_pow (show 16383 < 2 ^ i by omega),
103        Nat.testBit_lt_two_pow (show 32767 < 2 ^ i by omega),
104        Nat.testBit_lt_two_pow (show 65535 < 2 ^ i by omega)]
105
106/-- `inflatePrime` rejects a state-check input that is not initialised. -/
107theorem inflatePrime_reject {h : Heap} {p : ZStreamPtr}
108    (hd : StreamDom h p) (hn : ¬ Initialised h p) (bits value : Int32) :
109    C.run (inflatePrime p bits value) h = .ok (Z_STREAM_ERROR, h) := by
110  show inflatePrime p bits value h = _
111  unfold inflatePrime
112  simp [bind_app, notInit_check hd hn, pure_app, Z_STREAM_ERROR]
113
114
115/-- `int inflatePrime(z_streamp strm, int bits, int value)`
116The exact public result, state, frame and ownership contract. -/
117theorem prime_public : Goal.inflatePrime := by
118  intro bits value
119  constructor
120  · intro h p hr
121    exact inflatePrime_reject (refused_dom hr) (refused_not_initialised hr) bits value
122  · intro h r i z s hv hbits
123    rcases hv with ⟨hz, hstate, hi, hb, ha, hf, hlo, hhi⟩
124    have hl : Live h r i z s := ⟨hz, hi, hstate, hb, ⟨hlo, hhi⟩, ha, hf⟩
125    have run := inflatePrime_record hl hbits bits value
126    by_cases hzero : bits = 0
127    · simpa [hzero] using run.1 hzero
128    · by_cases hneg : bits.toInt < 0
129      · have hn : bits < 0 := Int32.lt_iff_toInt_lt.mpr (by simpa using hneg)
130        simpa [hzero, hneg, putInflate, setI] using run.2.1 hn
131      · have hpos : 0 < bits := by
132          apply Int32.lt_iff_toInt_lt.mpr
133          have hne : bits.toInt ≠ 0 := fun h => hzero (Int32.toInt_inj.mp (by simpa using h))
134          simp only [Int32.toInt_zero]
135          omega
136        by_cases hbad : 16 < bits.toInt ∨ 32 < s.bits.toNat + bits.toInt.toNat
137        · rw [ite_eq_right hzero, ite_eq_right hneg, ite_eq_left hbad]
138          exact run.2.2.1 hpos hbad
139        · have hp := int32_pos hpos
140          have hh16 : bits.toInt ≤ 16 := by omega
141          have hfit : s.bits.toNat + bits.toInt.toNat ≤ 32 := by omega
142          have hpbit := primeBits_public bits value hp hh16
143          rw [ite_eq_right hzero, ite_eq_right hneg, ite_eq_right hbad]
144          simpa [primeState, hpbit, i2u, putInflate, setI] using run.2.2.2 hpos hh16 hfit
145
146
147#print axioms prime_public
148end ZlibF.Spec.Public.InflatePrimeProof