inftrees.c.decode.frame.lean

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

1import ZlibF.Spec.InflateDecodeTableFrame
2
3/-!
4# A later table preserves queries to an unchanged earlier extent
5
6The result concerns both successful and failed queries. In particular,
7it transports leaf meaning without assuming the whole backing array is
8unchanged. The actual later constructor must still establish the frame.
9-/
10
11set_option autoImplicit false
12
13namespace Zlib.Inftrees.Proofs
14open C Zlib.Inftrees.Spec Zlib.Inftrees.Spec.DecodeSemantics
15open Zlib.Inftrees.Spec.DecodeTableFrame ZlibF.Spec
16
17private theorem query_value_lt {n : Nat} {inp rest : List Bool} {v : Nat}
18    (hr : readBits n inp = some (v, rest)) : v < 2 ^ n := by
19  induction n generalizing inp v rest with
20  | zero => simp only [readBits, Option.some.injEq, Prod.mk.injEq] at hr; omega
21  | succ n ih =>
22    cases inp with
23    | nil => cases hr
24    | cons b r =>
25      cases hread : readBits n r with
26      | none => simp [readBits, hread] at hr
27      | some vr =>
28        rcases vr with ⟨v1, r1⟩
29        have hv := ih hread
30        simp only [readBits, hread, Option.some.injEq, Prod.mk.injEq] at hr
31        rcases hr with ⟨rfl, rfl⟩
32        rw [Nat.pow_succ]
33        cases b <;> simp only [Bool.false_eq_true, ite_false, ite_true] <;> omega
34
35private theorem link_guard {type : UInt32} (entry : Code)
36    (ht : type = LENS ∨ type = DISTS)
37    (hl : (if type = LENS then entry.op != 0 && (entry.op &&& 0xf0) == 0
38      else (entry.op &&& 0xf0) == 0) = true) :
39    (type = LENS ∧ Zlib.Inffast.Spec.LenLink entry) ∨
40      (type = DISTS ∧ Zlib.Inffast.Spec.DistLink entry) := by
41  have mask_bits (hm : entry.op &&& 0xf0 = 0) :
42      entry.op &&& 16 = 0 ∧ entry.op &&& 64 = 0 := by
43    have h16 := congrArg (fun x : UInt8 => x &&& 16) hm
44    have h64 := congrArg (fun x : UInt8 => x &&& 64) hm
45    rw [UInt8.and_assoc] at h16 h64
46    exact ⟨h16, h64⟩
47  rcases ht with rfl | rfl
48  · simp only [ite_true, Bool.and_eq_true, bne_iff_ne, beq_iff_eq] at hl
49    exact Or.inl ⟨rfl, hl.1, mask_bits hl.2⟩
50  · simp only [show DISTS ≠ LENS by decide, ite_false, beq_iff_eq] at hl
51    exact Or.inr ⟨rfl, mask_bits hl⟩
52
53/-- Every query is confined to the returned extent, so a later builder's
54cell frame transports the exact result, including input-short failures. -/
55theorem decode_table_read_preserved : Goal.decode_table_read_preserved := by
56  intro type before after offset root used ht hext hcells inp
57  unfold tableRead
58  cases hread : readBits root inp with
59  | none => simp
60  | some ir =>
61    rcases ir with ⟨i, rest⟩
62    have hi := query_value_lt hread
63    have hroot := hcells (offset + i) (by omega) (by have := hext.2.2.1; omega)
64    simp only [bind, Option.bind]
65    rw [hroot]
66    cases hfirst : before[offset + i]? with
67    | none => simp
68    | some entry =>
69      by_cases hl : (if type = LENS then entry.op != 0 && (entry.op &&& 0xf0) == 0
70        else (entry.op &&& 0xf0) == 0) = true
71      · simp only [ite_eq_left hl]
72        have hentry : before.getD (offset + i) default = entry := by
73          simp only [Array.getD_eq_getD_getElem?, hfirst, Option.getD_some]
74        have hend := hext.2.2.2 i hi
75        rw [hentry] at hend
76        have hbound := hend (link_guard entry ht hl)
77        cases hread2 : readBits entry.op.toNat (inp.drop entry.bits.toNat) with
78        | none => simp
79        | some jr =>
80          rcases jr with ⟨j, rest2⟩
81          have hj := query_value_lt hread2
82          dsimp only
83          rw [hcells (offset + entry.val.toNat + j) (by omega) (by omega)]
84      · simp only [ite_eq_right hl]
85
86end Zlib.Inftrees.Proofs