InflateTableContent.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Proof.«inftrees.c.main»
2
3/-!
4# Contents of the table built by the actual `inflate_table`
5
6The execution, frame and return classification are retained from the existing safety proof.
7The extra obligation retains every leaf and subtable link written by the main loop. Its
8environment is tied to the input lengths, table location, kind and returned root width.
9No geometry condition or callee contract is assumed by the caller.
10-/
11
12namespace Zlib.Inftrees.Spec
13open C Zlib.Inftrees Zlib.Inftrees.Proofs
14
15/-- A successful empty code writes two one-bit invalid entries. A successful nonempty code
16writes the canonical leaves and links associated with the supplied lengths. The internal
17environment is an existential result of the execution, not an input assumption. -/
18def TableContent (type : UInt32) (f : Nat → Nat) (n : Nat) (rc : CodeRef) (oc : Nat)
19    (r : Int32 × CodePtr × UInt32) (after : Heap) : Prop :=
20  r.1 = 0 →
21    (Tc f n 15 = 0 ∧ r.2.2 = 1 ∧ r.2.1 = .ref rc (oc + 2) ∧
22      ∃ ca : Array Code, Space.get after rc = some ca ∧
23        ca[oc]? = some ⟨64, 1, 0⟩ ∧ ca[oc + 1]? = some ⟨64, 1, 0⟩) ∨
24    (0 < Tc f n 15 ∧ ∃ (e : Env) (ca : Array Code),
25      e.f = f ∧ e.n = n ∧ e.R = r.2.2.toNat ∧ e.rc = rc ∧ e.oc = oc ∧
26      e.c.type = type ∧ Space.get after rc = some ca ∧
27      Written e e.m ca ∧ Links e e.m ca)
28
29/-- On every existing `CallPre`, the real translated function returns and retains both the
30safety result and its constructed table contents. Rejected and oversized tables are allowed.
31This is an internal table-builder obligation; it does not by itself establish decoder safety. -/
32def Goal.inflate_table_content : Prop :=
33  ∀ (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32)
34    (rc : CodeRef) (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat)
35    (pre : CallPre h type rl ol codes rc oc bits rw ow),
36    ∃ r after,
37      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
38        .ok (r, after) ∧
39      Result h rw rc ow oc (capOf type) codes.toNat pre.wa pre.ca (.ref rc oc) bits r after ∧
40      RetInfo type pre.f codes.toNat r ∧ TableContent type pre.f codes.toNat rc oc r after
41
42end Zlib.Inftrees.Spec