trees.c.align.lean

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

1import ZlibF.Proof.«trees.c.emit»
2
3/-!
4# trees.c: `_tr_flush_bits`, `_tr_align`
5-/
6
7namespace Zlib.Trees.Proofs.Out
8open C Zlib.Trees
9
10theorem static_ltree_get {h : Heap} (hs : TreesStatic h.static) :
11    Space.get h (CtDataRef.st_static_ltree) = some static_ltree_tab := by
12  simp [Space.get, hs.static_ltree]
13
14theorem static_ltree_256_dl : (static_ltree_tab[256]'(by decide +kernel)).dl = 7 := by decide +kernel
15theorem static_ltree_256_fc : (static_ltree_tab[256]'(by decide +kernel)).fc = 0 := by decide +kernel
16
17/-- `static_ltree[END_BLOCK]` is the 7-bit code `0000000`. -/
18theorem static_end_block {h : Heap} (hs : TreesStatic h.static) :
19    getDl (.ref CtDataRef.st_static_ltree 0) ((256 : Nat) : Int) h = .ok (7, h) ∧
20    getFc (.ref CtDataRef.st_static_ltree 0) ((256 : Nat) : Int) h = .ok (0, h) := by
21  have hg := static_ltree_get hs
22  have hi : 256 < static_ltree_tab.size := by decide +kernel
23  constructor
24  · rw [getDl_gen hg hi, static_ltree_256_dl]
25  · rw [getFc_gen hg hi, static_ltree_256_fc]
26
27theorem tr_flush_bits_eq (s : DeflateStatePtr) : «_tr_flush_bits» s = bi_flush s := rfl
28
29/-- **`_tr_flush_bits`, safety and specification** (it is `bi_flush`). -/
30theorem tr_flush_bits_emit {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
31    (hI : TreesInvAt h id d b buf) (hroom : 8 * d.pending.toNat + d.bi_valid.toInt.toNat ≤ 8 * buf.size) :
32    Emit id b («_tr_flush_bits» (some (.tab id))) h d buf [] 2 :=
33  bi_flush_emit hI hroom
34
35theorem v16_static_trees : v16 (STATIC_TREES <<< 1) = 2 := by decide
36
37/-- **`_tr_align`, safety and specification.** `_tr_align(s)` appends the empty static block to the output: the 3
38header bits `BFINAL = 0`, `BTYPE = 01` (`natBits 2 3`: the bits 0, 1, 0, least significant first) and the 7-bit
39end-of-block code of the static literal/length tree (seven zero bits), then flushes complete bytes (`bi_flush`).
40Precondition: `TreesInvAt` and room for the 10 bits (`8 * pending + bi_valid + 10 <= 8 * pending_buf_size`;
41`deflate_stored` and `deflate` call it with an empty `pending`). -/
42theorem tr_align_emit {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
43    (hI : TreesInvAt h id d b buf)
44    (hroom : 8 * d.pending.toNat + d.bi_valid.toInt.toNat + 10 ≤ 8 * buf.size) :
45    Emit id b («_tr_align» (some (.tab id))) h d buf (natBits 2 3 ++ (natBits 0 7 ++ [])) (2 + (2 + 2)) := by
46  have h3 : (3 : Int32).toInt = 3 := by decide
47  have e1 := send_bits_emit hI (STATIC_TREES <<< 1) 3 (by rw [h3]; omega) (by rw [h3]; omega)
48    (by rw [v16_static_trees, h3]; decide) (by rw [h3]; omega)
49  rw [v16_static_trees, h3] at e1
50  change Emit _ _ _ _ _ _ (natBits 2 3) 2 at e1
51  unfold «_tr_align»
52  refine Emit.bind (m2 := send_code (some (.tab id)) END_BLOCK.toInt (.ref .st_static_ltree 0) >>= fun _ => bi_flush (some (.tab id))) e1 ?_
53  intro buf1 d1 i1 o1 s1
54  have l1 := congrArg List.length o1
55  simp only [outBits_length, List.length_append, natBits_length] at l1
56  have hE : END_BLOCK.toInt = ((256 : Nat) : Int) := by rw [END_BLOCK_toInt]; rfl
57  obtain ⟨hdl, hfc⟩ := static_end_block (h := setD (setB h b buf1) id d1) (by simpa using i1.base.static)
58  refine Emit.bind (m1 := send_code (some (.tab id)) END_BLOCK.toInt (.ref .st_static_ltree 0)) ?_ ?_
59  · rw [hE]
60    have h7 : (7 : UInt16).toNat = 7 := by decide
61    have h0 : (0 : UInt16).toNat = 0 := by decide
62    have hb1 := i1.run.bi_lo
63    exact send_code_emit i1 _ _ 7 0 hdl hfc (by omega) (by rw [h0, h7]; simp) (by rw [h7]; omega)
64  · intro buf2 d2 i2 o2 s2
65    have l2 := congrArg List.length o2
66    simp only [outBits_length, List.length_append, natBits_length] at l2
67    have hb1 := i1.run.bi_lo
68    have hb2 := i2.run.bi_lo
69    have h7 : (7 : UInt16).toNat = 7 := by decide
70    try simp only [h7] at l2
71    exact bi_flush_emit i2 (by omega)
72
73end Zlib.Trees.Proofs.Out