inftrees.c.fixed.lean

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

1import ZlibF.Proof.«inflate.c.base»
2import ZlibF.Zlib.«inftrees.c»
3
4/-!
5# inftrees.c: `inflate_fixed`
6
7`inflate_fixed` does not build a table. It points the state at the two static tables (`lenfix`, `distfix`) and sets
8their root widths. The tables themselves are static data of the heap (installed by `initStatics`).
9-/
10
11namespace Zlib.Inftrees.Proofs
12open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs
13
14/-- The state record after `inflate_fixed`. -/
15def fixedState (st : InflateState) : InflateState :=
16  { st with lencode := .ref .st_lenfix 0, lenbits := 9, distcode := .ref .st_distfix 0, distbits := 5 }
17
18/-- **inflate_fixed.** On a live inflate state `zs` the call does not fault and changes exactly four fields of that
19record: `lencode` is the static `lenfix`, `lenbits` is 9, `distcode` is the static `distfix`, `distbits` is 5. No other
20table entry of the heap changes, and nothing is allocated or freed. -/
21theorem inflate_fixed_ok {h : Heap} {zs : Nat} {st : InflateState} (hs : h.istates zs = some st) :
22    C.run (inflate_fixed (some (.tab zs))) h = .ok ((), setI h zs (fixedState st)) := by
23  rw [C.run]
24  simp [inflate_fixed, bind_app, ldI_eq, stI_eq, hs, fixedState, setI, upd_upd]
25
26end Zlib.Inftrees.Proofs