inflate.c.input-cursor.lean

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

1import ZlibF.Proof.«inflate.c.main.macros»
2import ZlibF.Spec.Public.Memory
3
4namespace Zlib.Inflate.Proofs
5open C Zlib.Inflate
6set_option autoImplicit false
7
8/-- The cursor value after consuming bytes, without changing its byte view. -/
9def inputAdvance : BPtr → Nat → BPtr
10  | .null, _ => .null
11  | .ref ref off, used => .ref ref (off + used)
12
13theorem inputAdvance_zero (pointer : BPtr) : inputAdvance pointer 0 = pointer := by
14  cases pointer <;> rfl
15
16theorem inputAdvance_add (pointer : BPtr) (first second : Nat) :
17    inputAdvance (inputAdvance pointer first) second = inputAdvance pointer (first + second) := by
18  cases pointer <;> simp [inputAdvance, Nat.add_assoc]
19
20/-- Advancing within caller input preserves its public separation from the
21output range. Different allocations are not required. -/
22theorem inputAdvance_separate (input output : BPtr) (size room used : Nat)
23    (bound : used ≤ size) (separate : ZlibF.Spec.Public.Separate input size output room) :
24    ZlibF.Spec.Public.Separate (inputAdvance input used) (size - used) output room := by
25  rcases separate with empty | empty | separate
26  · exact Or.inl (by omega)
27  · exact Or.inr (Or.inl empty)
28  · right
29    right
30    cases input with
31    | null => trivial
32    | ref ref off =>
33      cases output with
34      | null => trivial
35      | ref dest outOffset =>
36        rcases separate with different | before | after
37        · exact Or.inl different
38        · exact Or.inr (Or.inl (by omega))
39        · exact Or.inr (Or.inr (by omega))
40
41/-- A retained cursor origin and the actual input count transport the
42public separation premise across any checked refill boundary. -/
43theorem BitInv.cursor_separate {h after : Heap} {l regs : IL} {bs : List UInt8} {used : Nat}
44    (before : BitInv h l bs) (current : BitInv after regs (bs.drop used)) (bound : used ≤ bs.length)
45    (cursor : regs.next = inputAdvance l.next used)
46    (separate : ZlibF.Spec.Public.Separate l.next l.have_.toNat l.put l.left.toNat) :
47    ZlibF.Spec.Public.Separate regs.next regs.have_.toNat l.put l.left.toNat := by
48  rw [before.have_eq] at separate
49  rw [current.have_eq, List.length_drop, cursor]
50  exact inputAdvance_separate l.next l.put bs.length l.left.toNat used bound separate
51
52/-- The actual input macro retains its byte-view identity and exact cursor
53offset, in addition to the earlier bit-stream facts. -/
54theorem PULLBYTE_succ_cursor {h : Heap} {l : IL} {b : UInt8} {bs : List UInt8}
55    (B : BitInv h l (b :: bs)) (hb : l.bits.toNat ≤ 56) :
56    ∃ nx, runX PULLBYTE l h = .ok ((.ok (), pulled l b nx), h) ∧
57      BitInv h (pulled l b nx) bs ∧ stream (pulled l b nx) bs = stream l (b :: bs) ∧
58      (pulled l b nx).bits.toNat = l.bits.toNat + 8 ∧ nx = inputAdvance l.next 1 := by
59  obtain ⟨nx, run, inv, bits, count⟩ := PULLBYTE_succ B hb
60  obtain ⟨ref, array, off, ptr, get, bound, _⟩ := B.next.resolve_left (by simp)
61  have fit : off < array.size := by simp only [List.length_cons] at bound; omega
62  have empty : (l.have_ == 0) = false := by
63    simp only [beq_eq_false_iff_ne]
64    intro zero
65    have length := B.have_eq
66    rw [zero] at length
67    simp at length
68  have load : load8 l.next h = .ok (array[off], h) := by rw [ptr]; exact Ptr.load_ok get fit
69  have add : l.next.add 1 h = .ok (.ref ref (off + 1), h) := by
70    rw [ptr]
71    exact Ptr.add_nat_ok (n := 1) get (by omega)
72  have shift : shl64 array[off].toUInt64 l.bits h = .ok (array[off].toUInt64 <<< l.bits.toUInt64, h) := by
73    rw [shl64_run _ _ (by omega : l.bits.toNat < 64)]
74    rfl
75  have actual : runX PULLBYTE l h = .ok ((.ok (), pulled l array[off] (.ref ref (off + 1))), h) := by
76    unfold PULLBYTE
77    rw [runX_bind, runX_get]
78    simp only [empty, Bool.false_eq_true, ↓reduceIte]
79    simp only [runX_bind, runX_set, runX_lift_ok load, runX_lift_ok add, runX_lift_ok shift]
80    rfl
81  have registers := congrArg (fun result => result.map (fun entry => entry.1.2.next)) (run.symm.trans actual)
82  have cursor : nx = inputAdvance l.next 1 := by
83    simp only [Except.map, pulled] at registers
84    rw [ptr]
85    exact Except.ok.inj registers
86  exact ⟨nx, run, inv, bits, count, cursor⟩
87
88end Zlib.Inflate.Proofs