InflateFastPlatform.lean

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

1import ZlibF.Spec.PlatformMemory
2import ZlibF.Spec.InflateFast
3
4/-!
5# Fast-decoder entry under the explicit platform object-size premise
6
7The entry retains the existing table, window and buffer obligations. The
8input/output size facts are derived from one named environment premise.
9This remains an internal raw-block, distinct-buffer interface.
10-/
11
12namespace Zlib.Inffast.Spec
13open C Zlib.Inffast.Proofs
14set_option autoImplicit false
15
16/-- Platform-scoped fast entry. Byte objects are smaller than `2^63`.
17This explicit premise includes caller storage; it is not derived from the
18unrestricted public history. Distinct raw input/output blocks, safe decoding
19tables and the existing fast margins remain required. -/
20structure PlatformEntry where
21  h0 : Heap
22  platform : ZlibF.PlatformMemory.ByteObjectsFit h0
23  strm : ZStreamPtr
24  start : UInt32
25  -- the stream record and the state
26  r : ZStreamRef
27  sm0 : ZStream
28  stid : Nat
29  s0 : InflateState
30  hstrm : strm = some r
31  hsm : r.get h0 = some sm0
32  hrw : r.isRo = false
33  hstate : sm0.state = some (StateRef.inflate stid)
34  hs0 : h0.istates stid = some s0
35  -- the input
36  ib : Nat
37  i0 : Nat
38  IN : Array UInt8
39  hnin : sm0.next_in = .ref (BRef.blk ib) i0
40  hIN : h0.bytes ib = some IN
41  hai : 6 ≤ sm0.avail_in.toNat
42  hINsz : i0 + sm0.avail_in.toNat ≤ IN.size
43  -- the output
44  ob : Nat
45  o0 : Nat
46  A0 : Array UInt8
47  hnout : sm0.next_out = .ref (BRef.blk ob) o0
48  hA0 : h0.bytes ob = some A0
49  hro : h0.ro ob = false
50  hao : 258 ≤ sm0.avail_out.toNat
51  hAsz : o0 + sm0.avail_out.toNat ≤ A0.size
52  hstart : sm0.avail_out.toNat ≤ start.toNat
53  hbeg : start.toNat - sm0.avail_out.toNat ≤ o0
54  hsep : ib ≠ ob
55  -- the bit buffer
56  hbits : s0.bits.toNat < 8
57  hhold : s0.hold.toNat < 2 ^ s0.bits.toNat
58  hsane : s0.sane ≠ 0
59  -- the window
60  hws : s0.wsize.toNat ≤ 32768
61  hwh : s0.whave.toNat ≤ s0.wsize.toNat
62  hwn : s0.wnext.toNat ≤ s0.wsize.toNat
63  wb : Nat
64  woff : Nat
65  W : Array UInt8
66  hwin : s0.whave ≠ 0 →
67    s0.window = .ref (BRef.blk wb) woff ∧ wb ≠ ob ∧ h0.bytes wb = some W ∧ woff + s0.wsize.toNat ≤ W.size
68  -- the tables
69  rl : CodeRef
70  ol : Nat
71  LCA : Array Code
72  hlc : s0.lencode = .ref rl ol
73  hLCA : Space.get h0 rl = some LCA
74  hlt : LenTableSafe LCA ol s0.lenbits.toNat
75  rd : CodeRef
76  od : Nat
77  DCA : Array Code
78  hdc : s0.distcode = .ref rd od
79  hDCA : Space.get h0 rd = some DCA
80  hdt : DistTableSafe DCA od s0.distbits.toNat
81
82/-- Supply the two existing size fields from the platform premise. -/
83def PlatformEntry.toEnv (e : PlatformEntry) : Env where
84  h0 := e.h0
85  strm := e.strm
86  start := e.start
87  r := e.r
88  sm0 := e.sm0
89  stid := e.stid
90  s0 := e.s0
91  hstrm := e.hstrm
92  hsm := e.hsm
93  hrw := e.hrw
94  hstate := e.hstate
95  hs0 := e.hs0
96  ib := e.ib
97  i0 := e.i0
98  IN := e.IN
99  hnin := e.hnin
100  hIN := e.hIN
101  hai := e.hai
102  hINsz := e.hINsz
103  hINbig := e.platform (.blk e.ib) e.IN e.hIN
104  ob := e.ob
105  o0 := e.o0
106  A0 := e.A0
107  hnout := e.hnout
108  hA0 := e.hA0
109  hro := e.hro
110  hao := e.hao
111  hAsz := e.hAsz
112  hAbig := e.platform (.blk e.ob) e.A0 e.hA0
113  hstart := e.hstart
114  hbeg := e.hbeg
115  hsep := e.hsep
116  hbits := e.hbits
117  hhold := e.hhold
118  hsane := e.hsane
119  hws := e.hws
120  hwh := e.hwh
121  hwn := e.hwn
122  wb := e.wb
123  woff := e.woff
124  W := e.W
125  hwin := e.hwin
126  rl := e.rl
127  ol := e.ol
128  LCA := e.LCA
129  hlc := e.hlc
130  hLCA := e.hLCA
131  hlt := e.hlt
132  rd := e.rd
133  od := e.od
134  DCA := e.DCA
135  hdc := e.hdc
136  hDCA := e.hDCA
137  hdt := e.hdt
138
139end Zlib.Inffast.Spec