inffast.c.frame.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«inffast.c.match»
2
3/-!
4# inffast.c: the frame of pure match-copy arrays
5
6Each copied byte stays inside the requested destination interval. These are
7theorems about the existing array functions, with no new semantic definitions.
8-/
9
10namespace Zlib.Inffast.Proofs
11open C Zlib.Inffast Zlib.Inffast.Spec
12
13theorem blitN_frame (S : Array UInt8) : ∀ k fo oo (A : Array UInt8) j,
14    j < oo ∨ oo + k ≤ j → (blitN S k fo oo A)[j]? = A[j]?
15  | 0, _, _, _, _, _ => rfl
16  | k + 1, fo, oo, A, j, hj => by
17    rw [blitN, blitN_frame S k (fo + 1) (oo + 1) (A.set! oo (S.getD fo 0)) j (by omega)]
18    have hne : oo ≠ j := by omega
19    simp [Array.set!, hne]
20
21theorem cpyN_frame : ∀ k fo oo (A : Array UInt8) j,
22    j < oo ∨ oo + k ≤ j → (cpyN k fo oo A)[j]? = A[j]?
23  | 0, _, _, _, _, _ => rfl
24  | k + 1, fo, oo, A, j, hj => by
25    rw [cpyN, cpyN_frame k (fo + 1) (oo + 1) (A.set! oo (A.getD fo 0)) j (by omega)]
26    have hne : oo ≠ j := by omega
27    simp [Array.set!, hne]
28
29theorem matchArr_frame (wsize wnext woff : Nat) (W : Array UInt8)
30    (bg o dist len : Nat) (A : Array UInt8) (j : Nat) (hj : j < o ∨ o + len ≤ j) :
31    (matchArr wsize wnext woff W bg o dist len A)[j]? = A[j]? := by
32  unfold matchArr
33  dsimp only
34  repeat' split
35  all_goals
36    repeat' first
37      | rw [cpyN_frame _ _ _ _ _ (by omega)]
38      | rw [blitN_frame _ _ _ _ _ _ (by omega)]
39
40end Zlib.Inffast.Proofs