infback.c.pure.lean

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

1import ZlibF.Zlib.«inflate.c»
2
3/-!
4# infback.c: facts that do not mention the heap
5
6Migrated from the earlier attempt (`TableCL`, `StoredSpec`) and restated against the present translation: the table `order`
7of the code-length code lengths is a permutation of `0 .. 18`, and the check of a stored block header on a 32-bit `hold`.
8-/
9
10namespace Zlib.Infback.Proofs
11open C Zlib.Inflate
12
13/-- `order` has 19 entries, every one below 19. -/
14theorem order_lt : ∀ j, j < 19 → ∃ v, order[j]? = some v ∧ v.toNat < 19 := by decide
15
16/-- `order` is injective on `0 .. 18`. -/
17theorem order_inj : ∀ i, i < 19 → ∀ j, j < 19 → order[i]? = order[j]? → i = j := by decide
18
19/-- `order` hits every code length symbol `0 .. 18`: the loops of `case TABLE` that write `lens[order[have++]]` for
20`have = 0 .. 18` write every one of `lens[0 .. 18]` exactly once. -/
21theorem order_surj : ∀ k, k < 19 → ∃ j, j < 19 ∧ order[j]? = some k.toUInt16 := by decide
22
23/-- For `x < 2^16`, `x ^^^ 0xffff` is `0xffff - x`. -/
24theorem xor_ffff_blocks : ∀ a, a < 256 → ∀ b, b < 256 → (a * 256 + b) ^^^ 65535 = 65535 - (a * 256 + b) := by
25  decide +kernel
26
27theorem xor_ffff (x : Nat) (hx : x < 65536) : x ^^^ 65535 = 65535 - x := by
28  have := xor_ffff_blocks (x / 256) (by omega) (x % 256) (Nat.mod_lt _ (by decide))
29  have e : x / 256 * 256 + x % 256 = x := by omega
30  rwa [e] at this
31
32/-- **The stored block header check** (`if (hold & 0xffff) != ((hold >> 16) ^ 0xffff)`) on a bit buffer of at most 32 bits:
33it passes exactly when the length field and the field after it add up to `0xffff` (RFC 1951, 3.2.4: `NLEN` is the one's
34complement of `LEN`). -/
35theorem stored_check (hold : UInt64) (hh : hold.toNat < 2 ^ 32) :
36    ((hold &&& (0xffff : UInt64)) != ((hold >>> 16) ^^^ (0xffff : UInt64))) = false ↔ hold.toNat % 65536 + hold.toNat / 65536 = 65535 := by
37  have e1 : (hold &&& (0xffff : UInt64)).toNat = hold.toNat % 65536 := by
38    rw [UInt64.toNat_and]; exact Nat.and_two_pow_sub_one_eq_mod hold.toNat 16
39  have e2 : (hold >>> 16).toNat = hold.toNat / 65536 := by
40    rw [UInt64.toNat_shiftRight]; simp [Nat.shiftRight_eq_div_pow]
41  have e3 : ((hold >>> 16) ^^^ (0xffff : UInt64)).toNat = hold.toNat / 65536 ^^^ 65535 := by
42    rw [UInt64.toNat_xor, e2]; rfl
43  have hlt : hold.toNat / 65536 < 65536 := by omega
44  have hx := xor_ffff _ hlt
45  have hlo : hold.toNat % 65536 < 65536 := Nat.mod_lt _ (by decide)
46  simp only [bne_eq_false_iff_eq]
47  constructor
48  · intro e
49    have := congrArg UInt64.toNat e
50    rw [e1, e3, hx] at this
51    omega
52  · intro e
53    apply UInt64.toNat_inj.mp
54    rw [e1, e3, hx]
55    omega
56
57/-- The length field of a stored block: the low 16 bits. -/
58theorem stored_len_toNat (hold : UInt64) : (hold.toUInt32 &&& 0xffff).toNat = hold.toNat % 65536 := by
59  rw [UInt32.toNat_and]
60  simp only [UInt64.toNat_toUInt32]
61  have : (0xffff : UInt32).toNat = 2 ^ 16 - 1 := rfl
62  rw [this, Nat.and_two_pow_sub_one_eq_mod]
63  rw [Nat.mod_mod_of_dvd _ (by decide : 2 ^ 16 ∣ 2 ^ 32)]
64
65end Zlib.Infback.Proofs