REFERENCE / ZLIB × LEAN
inffixed.h.lean
Source snapshot ·
fd194f505fde95d1 · Source at the matching commit ↗Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.
1-- GENERATED by scripts/gen_inffixed.py from inffixed.h of the verified source. Do not edit.
2import ZlibF.Runtime.Schema
3
4/-!
5# inffixed.h: the fixed decoding tables
6
7`lenfix[512]` and `distfix[32]`, entry for entry as in the C header (they are not the output of
8`inflate_table`: four entries of `lenfix` differ, see `docs/proof/inftrees.md#c-correspondence-checks`).
9-/
10
11namespace Zlib.InffixedH
12open C
13
14/-- `static const code lenfix[512]` -/
15def lenfix : Array Code := #[
16 ⟨96, 7, 0⟩, ⟨0, 8, 80⟩, ⟨0, 8, 16⟩, ⟨20, 8, 115⟩,
17 ⟨18, 7, 31⟩, ⟨0, 8, 112⟩, ⟨0, 8, 48⟩, ⟨0, 9, 192⟩,
18 ⟨16, 7, 10⟩, ⟨0, 8, 96⟩, ⟨0, 8, 32⟩, ⟨0, 9, 160⟩,
19 ⟨0, 8, 0⟩, ⟨0, 8, 128⟩, ⟨0, 8, 64⟩, ⟨0, 9, 224⟩,
20 ⟨16, 7, 6⟩, ⟨0, 8, 88⟩, ⟨0, 8, 24⟩, ⟨0, 9, 144⟩,
21 ⟨19, 7, 59⟩, ⟨0, 8, 120⟩, ⟨0, 8, 56⟩, ⟨0, 9, 208⟩,
22 ⟨17, 7, 17⟩, ⟨0, 8, 104⟩, ⟨0, 8, 40⟩, ⟨0, 9, 176⟩,
23 ⟨0, 8, 8⟩, ⟨0, 8, 136⟩, ⟨0, 8, 72⟩, ⟨0, 9, 240⟩,
24 ⟨16, 7, 4⟩, ⟨0, 8, 84⟩, ⟨0, 8, 20⟩, ⟨21, 8, 227⟩,
25 ⟨19, 7, 43⟩, ⟨0, 8, 116⟩, ⟨0, 8, 52⟩, ⟨0, 9, 200⟩,
26 ⟨17, 7, 13⟩, ⟨0, 8, 100⟩, ⟨0, 8, 36⟩, ⟨0, 9, 168⟩,
27 ⟨0, 8, 4⟩, ⟨0, 8, 132⟩, ⟨0, 8, 68⟩, ⟨0, 9, 232⟩,
28 ⟨16, 7, 8⟩, ⟨0, 8, 92⟩, ⟨0, 8, 28⟩, ⟨0, 9, 152⟩,
29 ⟨20, 7, 83⟩, ⟨0, 8, 124⟩, ⟨0, 8, 60⟩, ⟨0, 9, 216⟩,
30 ⟨18, 7, 23⟩, ⟨0, 8, 108⟩, ⟨0, 8, 44⟩, ⟨0, 9, 184⟩,
31 ⟨0, 8, 12⟩, ⟨0, 8, 140⟩, ⟨0, 8, 76⟩, ⟨0, 9, 248⟩,
32 ⟨16, 7, 3⟩, ⟨0, 8, 82⟩, ⟨0, 8, 18⟩, ⟨21, 8, 163⟩,
33 ⟨19, 7, 35⟩, ⟨0, 8, 114⟩, ⟨0, 8, 50⟩, ⟨0, 9, 196⟩,
34 ⟨17, 7, 11⟩, ⟨0, 8, 98⟩, ⟨0, 8, 34⟩, ⟨0, 9, 164⟩,
35 ⟨0, 8, 2⟩, ⟨0, 8, 130⟩, ⟨0, 8, 66⟩, ⟨0, 9, 228⟩,
36 ⟨16, 7, 7⟩, ⟨0, 8, 90⟩, ⟨0, 8, 26⟩, ⟨0, 9, 148⟩,
37 ⟨20, 7, 67⟩, ⟨0, 8, 122⟩, ⟨0, 8, 58⟩, ⟨0, 9, 212⟩,
38 ⟨18, 7, 19⟩, ⟨0, 8, 106⟩, ⟨0, 8, 42⟩, ⟨0, 9, 180⟩,
39 ⟨0, 8, 10⟩, ⟨0, 8, 138⟩, ⟨0, 8, 74⟩, ⟨0, 9, 244⟩,
40 ⟨16, 7, 5⟩, ⟨0, 8, 86⟩, ⟨0, 8, 22⟩, ⟨64, 8, 0⟩,
41 ⟨19, 7, 51⟩, ⟨0, 8, 118⟩, ⟨0, 8, 54⟩, ⟨0, 9, 204⟩,
42 ⟨17, 7, 15⟩, ⟨0, 8, 102⟩, ⟨0, 8, 38⟩, ⟨0, 9, 172⟩,
43 ⟨0, 8, 6⟩, ⟨0, 8, 134⟩, ⟨0, 8, 70⟩, ⟨0, 9, 236⟩,
44 ⟨16, 7, 9⟩, ⟨0, 8, 94⟩, ⟨0, 8, 30⟩, ⟨0, 9, 156⟩,
45 ⟨20, 7, 99⟩, ⟨0, 8, 126⟩, ⟨0, 8, 62⟩, ⟨0, 9, 220⟩,
46 ⟨18, 7, 27⟩, ⟨0, 8, 110⟩, ⟨0, 8, 46⟩, ⟨0, 9, 188⟩,
47 ⟨0, 8, 14⟩, ⟨0, 8, 142⟩, ⟨0, 8, 78⟩, ⟨0, 9, 252⟩,
48 ⟨96, 7, 0⟩, ⟨0, 8, 81⟩, ⟨0, 8, 17⟩, ⟨21, 8, 131⟩,
49 ⟨18, 7, 31⟩, ⟨0, 8, 113⟩, ⟨0, 8, 49⟩, ⟨0, 9, 194⟩,
50 ⟨16, 7, 10⟩, ⟨0, 8, 97⟩, ⟨0, 8, 33⟩, ⟨0, 9, 162⟩,
51 ⟨0, 8, 1⟩, ⟨0, 8, 129⟩, ⟨0, 8, 65⟩, ⟨0, 9, 226⟩,
52 ⟨16, 7, 6⟩, ⟨0, 8, 89⟩, ⟨0, 8, 25⟩, ⟨0, 9, 146⟩,
53 ⟨19, 7, 59⟩, ⟨0, 8, 121⟩, ⟨0, 8, 57⟩, ⟨0, 9, 210⟩,
54 ⟨17, 7, 17⟩, ⟨0, 8, 105⟩, ⟨0, 8, 41⟩, ⟨0, 9, 178⟩,
55 ⟨0, 8, 9⟩, ⟨0, 8, 137⟩, ⟨0, 8, 73⟩, ⟨0, 9, 242⟩,
56 ⟨16, 7, 4⟩, ⟨0, 8, 85⟩, ⟨0, 8, 21⟩, ⟨16, 8, 258⟩,
57 ⟨19, 7, 43⟩, ⟨0, 8, 117⟩, ⟨0, 8, 53⟩, ⟨0, 9, 202⟩,
58 ⟨17, 7, 13⟩, ⟨0, 8, 101⟩, ⟨0, 8, 37⟩, ⟨0, 9, 170⟩,
59 ⟨0, 8, 5⟩, ⟨0, 8, 133⟩, ⟨0, 8, 69⟩, ⟨0, 9, 234⟩,
60 ⟨16, 7, 8⟩, ⟨0, 8, 93⟩, ⟨0, 8, 29⟩, ⟨0, 9, 154⟩,
61 ⟨20, 7, 83⟩, ⟨0, 8, 125⟩, ⟨0, 8, 61⟩, ⟨0, 9, 218⟩,
62 ⟨18, 7, 23⟩, ⟨0, 8, 109⟩, ⟨0, 8, 45⟩, ⟨0, 9, 186⟩,
63 ⟨0, 8, 13⟩, ⟨0, 8, 141⟩, ⟨0, 8, 77⟩, ⟨0, 9, 250⟩,
64 ⟨16, 7, 3⟩, ⟨0, 8, 83⟩, ⟨0, 8, 19⟩, ⟨21, 8, 195⟩,
65 ⟨19, 7, 35⟩, ⟨0, 8, 115⟩, ⟨0, 8, 51⟩, ⟨0, 9, 198⟩,
66 ⟨17, 7, 11⟩, ⟨0, 8, 99⟩, ⟨0, 8, 35⟩, ⟨0, 9, 166⟩,
67 ⟨0, 8, 3⟩, ⟨0, 8, 131⟩, ⟨0, 8, 67⟩, ⟨0, 9, 230⟩,
68 ⟨16, 7, 7⟩, ⟨0, 8, 91⟩, ⟨0, 8, 27⟩, ⟨0, 9, 150⟩,
69 ⟨20, 7, 67⟩, ⟨0, 8, 123⟩, ⟨0, 8, 59⟩, ⟨0, 9, 214⟩,
70 ⟨18, 7, 19⟩, ⟨0, 8, 107⟩, ⟨0, 8, 43⟩, ⟨0, 9, 182⟩,
71 ⟨0, 8, 11⟩, ⟨0, 8, 139⟩, ⟨0, 8, 75⟩, ⟨0, 9, 246⟩,
72 ⟨16, 7, 5⟩, ⟨0, 8, 87⟩, ⟨0, 8, 23⟩, ⟨64, 8, 0⟩,
73 ⟨19, 7, 51⟩, ⟨0, 8, 119⟩, ⟨0, 8, 55⟩, ⟨0, 9, 206⟩,
74 ⟨17, 7, 15⟩, ⟨0, 8, 103⟩, ⟨0, 8, 39⟩, ⟨0, 9, 174⟩,
75 ⟨0, 8, 7⟩, ⟨0, 8, 135⟩, ⟨0, 8, 71⟩, ⟨0, 9, 238⟩,
76 ⟨16, 7, 9⟩, ⟨0, 8, 95⟩, ⟨0, 8, 31⟩, ⟨0, 9, 158⟩,
77 ⟨20, 7, 99⟩, ⟨0, 8, 127⟩, ⟨0, 8, 63⟩, ⟨0, 9, 222⟩,
78 ⟨18, 7, 27⟩, ⟨0, 8, 111⟩, ⟨0, 8, 47⟩, ⟨0, 9, 190⟩,
79 ⟨0, 8, 15⟩, ⟨0, 8, 143⟩, ⟨0, 8, 79⟩, ⟨0, 9, 254⟩,
80 ⟨96, 7, 0⟩, ⟨0, 8, 80⟩, ⟨0, 8, 16⟩, ⟨20, 8, 115⟩,
81 ⟨18, 7, 31⟩, ⟨0, 8, 112⟩, ⟨0, 8, 48⟩, ⟨0, 9, 193⟩,
82 ⟨16, 7, 10⟩, ⟨0, 8, 96⟩, ⟨0, 8, 32⟩, ⟨0, 9, 161⟩,
83 ⟨0, 8, 0⟩, ⟨0, 8, 128⟩, ⟨0, 8, 64⟩, ⟨0, 9, 225⟩,
84 ⟨16, 7, 6⟩, ⟨0, 8, 88⟩, ⟨0, 8, 24⟩, ⟨0, 9, 145⟩,
85 ⟨19, 7, 59⟩, ⟨0, 8, 120⟩, ⟨0, 8, 56⟩, ⟨0, 9, 209⟩,
86 ⟨17, 7, 17⟩, ⟨0, 8, 104⟩, ⟨0, 8, 40⟩, ⟨0, 9, 177⟩,
87 ⟨0, 8, 8⟩, ⟨0, 8, 136⟩, ⟨0, 8, 72⟩, ⟨0, 9, 241⟩,
88 ⟨16, 7, 4⟩, ⟨0, 8, 84⟩, ⟨0, 8, 20⟩, ⟨21, 8, 227⟩,
89 ⟨19, 7, 43⟩, ⟨0, 8, 116⟩, ⟨0, 8, 52⟩, ⟨0, 9, 201⟩,
90 ⟨17, 7, 13⟩, ⟨0, 8, 100⟩, ⟨0, 8, 36⟩, ⟨0, 9, 169⟩,
91 ⟨0, 8, 4⟩, ⟨0, 8, 132⟩, ⟨0, 8, 68⟩, ⟨0, 9, 233⟩,
92 ⟨16, 7, 8⟩, ⟨0, 8, 92⟩, ⟨0, 8, 28⟩, ⟨0, 9, 153⟩,
93 ⟨20, 7, 83⟩, ⟨0, 8, 124⟩, ⟨0, 8, 60⟩, ⟨0, 9, 217⟩,
94 ⟨18, 7, 23⟩, ⟨0, 8, 108⟩, ⟨0, 8, 44⟩, ⟨0, 9, 185⟩,
95 ⟨0, 8, 12⟩, ⟨0, 8, 140⟩, ⟨0, 8, 76⟩, ⟨0, 9, 249⟩,
96 ⟨16, 7, 3⟩, ⟨0, 8, 82⟩, ⟨0, 8, 18⟩, ⟨21, 8, 163⟩,
97 ⟨19, 7, 35⟩, ⟨0, 8, 114⟩, ⟨0, 8, 50⟩, ⟨0, 9, 197⟩,
98 ⟨17, 7, 11⟩, ⟨0, 8, 98⟩, ⟨0, 8, 34⟩, ⟨0, 9, 165⟩,
99 ⟨0, 8, 2⟩, ⟨0, 8, 130⟩, ⟨0, 8, 66⟩, ⟨0, 9, 229⟩,
100 ⟨16, 7, 7⟩, ⟨0, 8, 90⟩, ⟨0, 8, 26⟩, ⟨0, 9, 149⟩,
101 ⟨20, 7, 67⟩, ⟨0, 8, 122⟩, ⟨0, 8, 58⟩, ⟨0, 9, 213⟩,
102 ⟨18, 7, 19⟩, ⟨0, 8, 106⟩, ⟨0, 8, 42⟩, ⟨0, 9, 181⟩,
103 ⟨0, 8, 10⟩, ⟨0, 8, 138⟩, ⟨0, 8, 74⟩, ⟨0, 9, 245⟩,
104 ⟨16, 7, 5⟩, ⟨0, 8, 86⟩, ⟨0, 8, 22⟩, ⟨64, 8, 0⟩,
105 ⟨19, 7, 51⟩, ⟨0, 8, 118⟩, ⟨0, 8, 54⟩, ⟨0, 9, 205⟩,
106 ⟨17, 7, 15⟩, ⟨0, 8, 102⟩, ⟨0, 8, 38⟩, ⟨0, 9, 173⟩,
107 ⟨0, 8, 6⟩, ⟨0, 8, 134⟩, ⟨0, 8, 70⟩, ⟨0, 9, 237⟩,
108 ⟨16, 7, 9⟩, ⟨0, 8, 94⟩, ⟨0, 8, 30⟩, ⟨0, 9, 157⟩,
109 ⟨20, 7, 99⟩, ⟨0, 8, 126⟩, ⟨0, 8, 62⟩, ⟨0, 9, 221⟩,
110 ⟨18, 7, 27⟩, ⟨0, 8, 110⟩, ⟨0, 8, 46⟩, ⟨0, 9, 189⟩,
111 ⟨0, 8, 14⟩, ⟨0, 8, 142⟩, ⟨0, 8, 78⟩, ⟨0, 9, 253⟩,
112 ⟨96, 7, 0⟩, ⟨0, 8, 81⟩, ⟨0, 8, 17⟩, ⟨21, 8, 131⟩,
113 ⟨18, 7, 31⟩, ⟨0, 8, 113⟩, ⟨0, 8, 49⟩, ⟨0, 9, 195⟩,
114 ⟨16, 7, 10⟩, ⟨0, 8, 97⟩, ⟨0, 8, 33⟩, ⟨0, 9, 163⟩,
115 ⟨0, 8, 1⟩, ⟨0, 8, 129⟩, ⟨0, 8, 65⟩, ⟨0, 9, 227⟩,
116 ⟨16, 7, 6⟩, ⟨0, 8, 89⟩, ⟨0, 8, 25⟩, ⟨0, 9, 147⟩,
117 ⟨19, 7, 59⟩, ⟨0, 8, 121⟩, ⟨0, 8, 57⟩, ⟨0, 9, 211⟩,
118 ⟨17, 7, 17⟩, ⟨0, 8, 105⟩, ⟨0, 8, 41⟩, ⟨0, 9, 179⟩,
119 ⟨0, 8, 9⟩, ⟨0, 8, 137⟩, ⟨0, 8, 73⟩, ⟨0, 9, 243⟩,
120 ⟨16, 7, 4⟩, ⟨0, 8, 85⟩, ⟨0, 8, 21⟩, ⟨16, 8, 258⟩,
121 ⟨19, 7, 43⟩, ⟨0, 8, 117⟩, ⟨0, 8, 53⟩, ⟨0, 9, 203⟩,
122 ⟨17, 7, 13⟩, ⟨0, 8, 101⟩, ⟨0, 8, 37⟩, ⟨0, 9, 171⟩,
123 ⟨0, 8, 5⟩, ⟨0, 8, 133⟩, ⟨0, 8, 69⟩, ⟨0, 9, 235⟩,
124 ⟨16, 7, 8⟩, ⟨0, 8, 93⟩, ⟨0, 8, 29⟩, ⟨0, 9, 155⟩,
125 ⟨20, 7, 83⟩, ⟨0, 8, 125⟩, ⟨0, 8, 61⟩, ⟨0, 9, 219⟩,
126 ⟨18, 7, 23⟩, ⟨0, 8, 109⟩, ⟨0, 8, 45⟩, ⟨0, 9, 187⟩,
127 ⟨0, 8, 13⟩, ⟨0, 8, 141⟩, ⟨0, 8, 77⟩, ⟨0, 9, 251⟩,
128 ⟨16, 7, 3⟩, ⟨0, 8, 83⟩, ⟨0, 8, 19⟩, ⟨21, 8, 195⟩,
129 ⟨19, 7, 35⟩, ⟨0, 8, 115⟩, ⟨0, 8, 51⟩, ⟨0, 9, 199⟩,
130 ⟨17, 7, 11⟩, ⟨0, 8, 99⟩, ⟨0, 8, 35⟩, ⟨0, 9, 167⟩,
131 ⟨0, 8, 3⟩, ⟨0, 8, 131⟩, ⟨0, 8, 67⟩, ⟨0, 9, 231⟩,
132 ⟨16, 7, 7⟩, ⟨0, 8, 91⟩, ⟨0, 8, 27⟩, ⟨0, 9, 151⟩,
133 ⟨20, 7, 67⟩, ⟨0, 8, 123⟩, ⟨0, 8, 59⟩, ⟨0, 9, 215⟩,
134 ⟨18, 7, 19⟩, ⟨0, 8, 107⟩, ⟨0, 8, 43⟩, ⟨0, 9, 183⟩,
135 ⟨0, 8, 11⟩, ⟨0, 8, 139⟩, ⟨0, 8, 75⟩, ⟨0, 9, 247⟩,
136 ⟨16, 7, 5⟩, ⟨0, 8, 87⟩, ⟨0, 8, 23⟩, ⟨64, 8, 0⟩,
137 ⟨19, 7, 51⟩, ⟨0, 8, 119⟩, ⟨0, 8, 55⟩, ⟨0, 9, 207⟩,
138 ⟨17, 7, 15⟩, ⟨0, 8, 103⟩, ⟨0, 8, 39⟩, ⟨0, 9, 175⟩,
139 ⟨0, 8, 7⟩, ⟨0, 8, 135⟩, ⟨0, 8, 71⟩, ⟨0, 9, 239⟩,
140 ⟨16, 7, 9⟩, ⟨0, 8, 95⟩, ⟨0, 8, 31⟩, ⟨0, 9, 159⟩,
141 ⟨20, 7, 99⟩, ⟨0, 8, 127⟩, ⟨0, 8, 63⟩, ⟨0, 9, 223⟩,
142 ⟨18, 7, 27⟩, ⟨0, 8, 111⟩, ⟨0, 8, 47⟩, ⟨0, 9, 191⟩,
143 ⟨0, 8, 15⟩, ⟨0, 8, 143⟩, ⟨0, 8, 79⟩, ⟨0, 9, 255⟩]
144
145/-- `static const code distfix[32]` -/
146def distfix : Array Code := #[
147 ⟨16, 5, 1⟩, ⟨23, 5, 257⟩, ⟨19, 5, 17⟩, ⟨27, 5, 4097⟩,
148 ⟨17, 5, 5⟩, ⟨25, 5, 1025⟩, ⟨21, 5, 65⟩, ⟨29, 5, 16385⟩,
149 ⟨16, 5, 3⟩, ⟨24, 5, 513⟩, ⟨20, 5, 33⟩, ⟨28, 5, 8193⟩,
150 ⟨18, 5, 9⟩, ⟨26, 5, 2049⟩, ⟨22, 5, 129⟩, ⟨64, 5, 0⟩,
151 ⟨16, 5, 2⟩, ⟨23, 5, 385⟩, ⟨19, 5, 25⟩, ⟨27, 5, 6145⟩,
152 ⟨17, 5, 7⟩, ⟨25, 5, 1537⟩, ⟨21, 5, 97⟩, ⟨29, 5, 24577⟩,
153 ⟨16, 5, 4⟩, ⟨24, 5, 769⟩, ⟨20, 5, 49⟩, ⟨28, 5, 12289⟩,
154 ⟨18, 5, 13⟩, ⟨26, 5, 3073⟩, ⟨22, 5, 193⟩, ⟨64, 5, 0⟩]
155
156end Zlib.InffixedH