Concrete.lean

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

1import ZlibF.Spec.Api.Concrete
2
3namespace ZlibF.Spec.Api.Proofs
4
5/-- The concrete boundary exposes every fault of the translated computation.
6This equivalence requires no hypothesis that the computation succeeds. -/
7theorem execute_fault_iff {α : Type} (program : C.M α) (h : C.Heap) :
8    Concrete.execute program h = .fault ↔ ∃ fault, C.run program h = .error fault := by
9  cases hr : C.run program h with
10  | error fault => simp [Concrete.execute, hr]
11  | ok result => simp [Concrete.execute, hr]
12
13/-- The actual translated `compressBound_z` equals the saturated natural-number
14formula for every 64-bit input. The proof checks that the sum can wrap only once
15and that its increment is less than the modulus, so the C overflow test is exact. -/
16theorem compressBound_z_value (s : UInt64) :
17    (Zlib.Compress.compressBound_z s).toNat = compressBound s.toNat := by
18  have h12 : (s >>> 12).toNat = s.toNat / 4096 := by
19    rw [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow]
20    rfl
21  have h14 : (s >>> 14).toNat = s.toNat / 16384 := by
22    rw [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow]
23    rfl
24  have h25 : (s >>> 25).toNat = s.toNat / 33554432 := by
25    rw [UInt64.toNat_shiftRight, Nat.shiftRight_eq_div_pow]
26    rfl
27  have hs := s.toNat_lt
28  have hsum : (s + (s >>> 12) + (s >>> 14) + (s >>> 25) + 13).toNat =
29      (s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13) % 2 ^ 64 := by
30    simp only [UInt64.toNat_add, h12, h14, h25]
31    rw [show (13 : UInt64).toNat = 13 from rfl]
32    simp only [Nat.mod_add_mod]
33  have hinc : s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 < 2 ^ 64 := by
34    omega
35  have hB2 : s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 <
36      2 ^ 64 + 2 ^ 64 := by omega
37  unfold Zlib.Compress.compressBound_z compressBound
38  by_cases hB : s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 < 2 ^ 64
39  · have hm : (s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13) % 2 ^ 64 =
40        s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 := Nat.mod_eq_of_lt hB
41    have hnlt : ¬ s + (s >>> 12) + (s >>> 14) + (s >>> 25) + 13 < s := by
42      rw [UInt64.lt_iff_toNat_lt, hsum, hm]
43      omega
44    rw [ite_eq_right hnlt, hsum, hm, ite_eq_right (by omega)]
45  · have hm : (s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13) % 2 ^ 64 =
46        s.toNat + s.toNat / 4096 + s.toNat / 16384 + s.toNat / 33554432 + 13 - 2 ^ 64 := by
47      rw [Nat.mod_eq_sub_mod (by omega), Nat.mod_eq_of_lt (by omega)]
48    have hlt : s + (s >>> 12) + (s >>> 14) + (s >>> 25) + 13 < s := by
49      rw [UInt64.lt_iff_toNat_lt, hsum, hm]
50      omega
51    rw [ite_eq_left hlt, ite_eq_left (by omega)]
52    rfl
53
54/-- Both actual translated bound functions satisfy the concrete API goal on LP64.
55Unlike `compress_bound_adequate`, this theorem concerns the implementation's
56numeric result rather than an implication already required by `Compress2`. -/
57theorem compress_bound_value : Goal.compress_bound_value := by
58  intro sourceLen
59  exact ⟨compressBound_z_value sourceLen, compressBound_z_value sourceLen⟩
60
61end ZlibF.Spec.Api.Proofs