inffast.c.origin.lean

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

1import ZlibF.Spec.InflateFastOrigin
2import ZlibF.Proof.«inffast.c.final»
3
4/-!
5# Exact origin of the fast decoder's remaining input
6
7The accounting and bit-list equations are retained together. In particular,
8rollback recovers the actual unread input bytes, not an equal-length list.
9-/
10
11namespace Zlib.Inffast.Proofs
12open C Zlib.Inffast Zlib.Inffast.Spec Zlib.Inffast.Spec.Origin
13open ZlibF.Spec
14
15/-- The entry registers already represent the complete initial suffix. -/
16theorem initial_origin : Goal.initial_origin := by
17  intro e
18  exact ⟨by omega, by omega, e.hhold, by simp, by simp [initial]⟩
19
20/-- Pulling the actual input byte preserves both origin equations. -/
21theorem pull_preserves_origin : Goal.pull_preserves_origin := by
22  intro e hold bits input used P available
23  have byteBound : (e.IN.getD input 0).toNat + 1 ≤ 256 := by
24    have := (e.IN.getD input 0).toNat_lt
25    omega
26  have normalized : hold + (e.IN.getD input 0).toNat * 2 ^ bits < 2 ^ (bits + 8) := by
27    calc
28      hold + (e.IN.getD input 0).toNat * 2 ^ bits <
29          2 ^ bits + (e.IN.getD input 0).toNat * 2 ^ bits := Nat.add_lt_add_right P.normalized _
30      _ = ((e.IN.getD input 0).toNat + 1) * 2 ^ bits := by rw [Nat.add_mul]; omega
31      _ ≤ 256 * 2 ^ bits := Nat.mul_le_mul_right _ byteBound
32      _ = 2 ^ (bits + 8) := by rw [Nat.pow_add, Nat.mul_comm]
33  refine ⟨by have := P.inputLower; omega, by omega, normalized, ?_, ?_⟩
34  · have := P.accounting
35    have := P.inputLower
36    omega
37  · rw [Sg_pull e hold bits input P.normalized available]
38    exact P.stream
39
40/-- Dropping low bits consumes exactly that many original entry bits. -/
41theorem drop_preserves_origin : Goal.drop_preserves_origin := by
42  intro e hold bits input used count P available
43  refine ⟨P.inputLower, P.inputUpper, ?_, ?_, ?_⟩
44  · apply (Nat.div_lt_iff_lt_mul (Nat.two_pow_pos count)).mpr
45    rw [← Nat.pow_add, Nat.sub_add_cancel available]
46    exact P.normalized
47  · have := P.accounting
48    omega
49  · rw [Sg_drop hold bits input count available, P.stream, List.drop_drop]
50
51private theorem in_bits_drop_bytes (e : Env) :
52    ∀ (i k : Nat), i + k ≤ e.i0 + e.sm0.avail_in.toNat →
53      (inBits e i).drop (8 * k) = inBits e (i + k) := by
54  intro i k
55  induction k generalizing i with
56  | zero => simp
57  | succ k ih =>
58    intro available
59    have first : i < e.i0 + e.sm0.avail_in.toNat := by omega
60    rw [inBits_pull e i first, show 8 * (k + 1) = 8 + 8 * k by omega, ← List.drop_drop]
61    have removed : (byteBits (e.IN.getD i 0) ++ inBits e (i + 1)).drop 8 = inBits e (i + 1) := by
62      rw [List.drop_append]
63      simp [byteBits]
64    rw [removed, ih (i + 1) (by omega)]
65    congr 1
66    omega
67
68private theorem low_bits_take (hold bits count : Nat) (available : count ≤ bits) :
69    (bitsOfNat hold bits).take count = bitsOfNat hold count := by
70  simp only [bitsOfNat, ← List.map_take, List.take_range, Nat.min_eq_left available]
71
72private theorem low_bits_mask (hold count : Nat) :
73    bitsOfNat (hold % 2 ^ count) count = bitsOfNat hold count := by
74  unfold bitsOfNat
75  apply List.map_congr_left
76  intro j hj
77  have bound : j < count := List.mem_range.mp hj
78  simp [Nat.testBit_mod_two_pow, bound]
79
80/-- Returning unused whole bytes preserves the exact remaining input.
81Origin accounting identifies those bytes with the corresponding original
82input range, and the mask retains the same low residual bits. -/
83theorem rollback_preserves_origin : Goal.rollback_preserves_origin := by
84  intro e hold bits input used P
85  let returned := bits / 8
86  let residual := bits % 8
87  have decomposition : residual + 8 * returned = bits := Nat.mod_add_div bits 8
88  have residualBound : residual < 8 := Nat.mod_lt _ (by decide)
89  have rollbackBound : returned ≤ input - e.i0 := by
90    have entryBits := e.hbits
91    have accounting := P.accounting
92    omega
93  have newLower : e.i0 ≤ input - returned := by have := P.inputLower; omega
94  have newUpper : input - returned ≤ e.i0 + e.sm0.avail_in.toNat := by
95    have := P.inputUpper
96    omega
97  have residualAvailable : residual ≤ bits := by omega
98  have accounting : used + residual = e.s0.bits.toNat + 8 * (input - returned - e.i0) := by
99    have := P.accounting
100    have := P.inputLower
101    omega
102  have originDrop : (initial e).drop (used + residual) = inBits e (input - returned) := by
103    rw [accounting, initial, Sg, List.drop_append]
104    have removed : (bitsOfNat e.s0.hold.toNat e.s0.bits.toNat).drop
105        (e.s0.bits.toNat + 8 * (input - returned - e.i0)) = [] :=
106      List.drop_eq_nil_of_le (by rw [bitsOfNat_length]; omega)
107    rw [removed, List.nil_append, bitsOfNat_length, Nat.add_sub_cancel_left]
108    have h := in_bits_drop_bytes e e.i0 (input - returned - e.i0) (by omega)
109    simpa only [Nat.add_sub_of_le newLower] using h
110  have tail : (Sg e hold bits input).drop residual = inBits e (input - returned) := by
111    rw [P.stream, List.drop_drop]
112    exact originDrop
113  have head : (Sg e hold bits input).take residual = bitsOfNat hold residual := by
114    rw [Sg, List.take_append_of_le_length (by rw [bitsOfNat_length]; exact residualAvailable)]
115    exact low_bits_take hold bits residual residualAvailable
116  have streamSame : Sg e (hold % 2 ^ residual) residual (input - returned) = Sg e hold bits input := by
117    calc
118      Sg e (hold % 2 ^ residual) residual (input - returned) =
119          bitsOfNat hold residual ++ inBits e (input - returned) := by rw [Sg, low_bits_mask]
120      _ = (Sg e hold bits input).take residual ++ (Sg e hold bits input).drop residual := by rw [head, tail]
121      _ = Sg e hold bits input := List.take_append_drop _ _
122  exact ⟨rollbackBound, streamSame, newLower, newUpper,
123    Nat.mod_lt _ (Nat.two_pow_pos residual), accounting, streamSame.trans P.stream⟩
124
125/-- The actual byte load, pointer advance and bounded word updates preserve
126the same exact source suffix as the natural-number pull equation. -/
127theorem actual_pull_preserves_origin : Goal.actual_pull_preserves_origin := by
128  intro e bytes msg mode l i o used locals origin buffer available
129  let next := pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1))
130  refine ⟨next, ?_, LS.pullL locals buffer available, ?_⟩
131  · exact pull_run e (e.heap bytes msg mode) l i o locals buffer available
132      (e.heap_bytes_in bytes msg mode)
133  · have result := pull_preserves_origin e l.hold.toNat l.bits.toNat i used origin available
134    simpa only [next, pullL_hold l _ _ locals.hb locals.hH, pullL_bits l _ _ locals.hb] using result
135
136/-- The checked source shift and unsigned subtraction implement the
137already justified low-bit drop without changing the heap. -/
138theorem actual_drop_preserves_origin : Goal.actual_drop_preserves_origin := by
139  intro e h l i o used count locals origin available
140  have countBound : count.toNat < 64 := by have := locals.hb; omega
141  refine ⟨?_, LS.dropL locals count available countBound, ?_⟩
142  · simp only [C.run, shr64_eq (x := l.hold) (n := count.toUInt64)
143        (by simpa only [UInt32.toNat_toUInt64] using countBound),
144      bind_app, pure_app, dropL]
145  · have result := drop_preserves_origin e l.hold.toNat l.bits.toNat i used count.toNat origin available
146    simpa only [dropL_hold l count countBound, dropL_bits l count available] using result
147
148/-- The actual pointer subtraction and checked mask computation recover
149the same precise input suffix, including its returned whole bytes. -/
150theorem actual_rollback_preserves_origin : Goal.actual_rollback_preserves_origin := by
151  intro e bytes msg mode l i o used locals origin
152  let returned := l.bits >>> 3
153  let bits := l.bits - (returned <<< 3)
154  let hold := l.hold &&& (((1 : UInt32) <<< bits) - 1).toUInt64
155  change C.run (do
156      let input ← subn l.in_ returned
157      let mask ← shl32 1 bits
158      pure (input, l.hold &&& (mask - 1).toUInt64, bits)) (e.heap bytes msg mode) =
159      .ok ((.ref (.blk e.ib) (i - l.bits.toNat / 8), hold, bits), e.heap bytes msg mode) ∧
160    bits.toNat < 8 ∧ Inv e hold.toNat bits.toNat (i - l.bits.toNat / 8) used ∧
161    Sg e hold.toNat bits.toNat (i - l.bits.toNat / 8) = Sg e l.hold.toNat l.bits.toNat i
162  obtain ⟨rollbackBound, streamSame, rolledOrigin⟩ :=
163    rollback_preserves_origin e l.hold.toNat l.bits.toNat i used origin
164  have bitValue : bits.toNat = l.bits.toNat % 8 := bits_residual l.bits locals.hb
165  have bitBound : bits.toNat < 8 := by rw [bitValue]; omega
166  have maskValue : ((((1 : UInt32) <<< bits) - 1).toUInt64).toNat = 2 ^ bits.toNat - 1 := by
167    rw [UInt32.toNat_toUInt64]
168    exact u32_shl1_sub1 (by omega)
169  have holdValue : hold.toNat = l.hold.toNat % 2 ^ (l.bits.toNat % 8) := by
170    dsimp only [hold]
171    rw [u64_and_mask maskValue, bitValue]
172  have pointer : subn l.in_ returned (e.heap bytes msg mode) =
173      .ok (.ref (.blk e.ib) (i - l.bits.toNat / 8), e.heap bytes msg mode) := by
174    rw [locals.hin]
175    have result := subn_ok (h := e.heap bytes msg mode) (r := BRef.blk e.ib) (a := e.IN)
176      (e.heap_bytes_in bytes msg mode)
177      (n := returned) (off := i)
178      (by dsimp only [returned]; rw [bits_whole]; omega)
179      (by have := locals.hi1; have := e.hINsz; omega)
180    simpa only [returned, bits_whole, OkOn] using result
181  refine ⟨?_, bitBound, ?_, ?_⟩
182  · simp only [C.run, bind_app, pointer, pure_app,
183      shl32_eq (x := 1) (n := bits) (by omega : bits.toNat < 32), hold]
184  · simpa only [holdValue, bitValue] using rolledOrigin
185  · simpa only [holdValue, bitValue] using streamSame
186
187end Zlib.Inffast.Proofs