Api.lean

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

1import ZlibF.Spec.Api.Goals
2import ZlibF.Proof.Format.Wrapper
3
4/-!
5# Proofs: the format is deterministic and self-delimiting
6
7`Goal.format_deterministic` and `Goal.format_prefix_free`. Both follow from `Layer.ext`: if `z` and
8`z ++ t` are complete streams of the layer (same configuration and dictionary), then `t = []` and
9the outputs are equal. The proof does not use any window-size hypothesis: neither goal mentions
10`FullWindow`, and the dictionary and the window only select which back-references are allowed,
11never how the stream is cut into fields.
12-/
13
14namespace ZlibF.Spec.Api
15
16open ZlibF.Spec
17
18namespace Proofs
19
20/-- A complete stream of any layer has no complete extension, and its output is determined
21(the dictionary and the configuration are fixed). -/
22theorem Layer.ext {w : Wrap} {b : Nat} {d z t o1 o2 : List UInt8}
23    (h1 : Layer.Decodes w b d z o1) (h2 : Layer.Decodes w b d (z ++ t) o2) :
24    t = [] ∧ o1 = o2 := by
25  cases w with
26  | raw =>
27    obtain ⟨hl, ho⟩ := Prefix.ext h1 h2
28    exact ⟨List.eq_nil_of_length_eq_zero (by simp only [List.length_nil] at hl; omega), ho⟩
29  | zlib => exact Zlib.ext h1.1 h2.1
30  | gzip => exact Gzip.ext h1 h2
31  | auto =>
32    rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2
33    · exact Zlib.ext h1.1 h2.1
34    · exfalso
35      obtain ⟨cmf, r, hz, hc⟩ := zlib_head h1.1
36      obtain ⟨r2, hg⟩ := gzip_head h2
37      rw [hz] at hg
38      simp only [List.cons_append, List.cons.injEq] at hg
39      rw [hg.1] at hc
40      exact absurd hc (by decide)
41    · exfalso
42      obtain ⟨cmf, r, hz, hc⟩ := zlib_head h2.1
43      obtain ⟨r2, hg⟩ := gzip_head h1
44      rw [hg] at hz
45      simp only [List.cons_append, List.cons.injEq] at hz
46      rw [← hz.1] at hc
47      exact absurd hc (by decide)
48    · exact Gzip.ext h1 h2
49
50/-- Decoding is a function: one stream has one decoding. -/
51theorem format_deterministic : Goal.format_deterministic := by
52  intro w b d z o1 o2 h1 h2
53  exact (Layer.ext h1 (by simpa using h2) : [] = [] ∧ o1 = o2).2
54
55/-- A complete stream has no complete extension: where a stream ends is determined by its bytes. -/
56theorem format_prefix_free : Goal.format_prefix_free := by
57  intro w b d z t o1 o2 h1 h2
58  exact (Layer.ext h1 h2).1
59
60end Proofs
61
62end ZlibF.Spec.Api