101def sha256CompressionRounds =
102 (lambda unrestricted schedule : (family SHA256Schedule) .
103 (eliminate
104 SHA256Schedule
105 (lambda unrestricted current : (family SHA256Schedule) .
106 (pi unrestricted constants : (family SHA256Schedule) .
107 (pi unrestricted roundState : (family SHA256CompressionRoundState) .
108 (family SHA256CompressionRoundsResult))))
109 schedule
110 (branch
111 SHA256ScheduleEnd
112 .
113 (lambda unrestricted constants : (family SHA256Schedule) .
114 (lambda unrestricted roundState : (family SHA256CompressionRoundState) .
115 (eliminate
116 SHA256Schedule
117 (lambda unrestricted current : (family SHA256Schedule) .
118 (family SHA256CompressionRoundsResult))
119 constants
120 (branch
121 SHA256ScheduleEnd
122 .
123 (eliminate
124 SHA256CompressionRoundState
125 (lambda unrestricted current : (family SHA256CompressionRoundState) .
126 (family SHA256CompressionRoundsResult))
127 roundState
128 (branch
129 SHA256CompressionRoundStateValue
130 state
131 index
132 rotates
133 shifts
134 booleans
135 adds
136 .
137 (nat-eliminate
138 (lambda unrestricted validCount : Nat .
139 (family SHA256CompressionRoundsResult))
140 (constructor
141 SHA256CompressionRoundsResult
142 SHA256CompressionRoundsFailed
143 (constructor SHA256ErrorCode SHA256RoundCountInvalid)
144 index)
145 (lambda unrestricted predecessor : Nat .
146 (lambda unrestricted induction : (family SHA256CompressionRoundsResult) .
147 (constructor
148 SHA256CompressionRoundsResult
149 SHA256CompressionRoundsSucceeded
150 roundState)))
151 (naturalEqual index sha256NaturalSixtyFour)))))
152 (branch
153 SHA256ScheduleNext
154 constant
155 tail
156 induction
157 .
158 (eliminate
159 SHA256CompressionRoundState
160 (lambda unrestricted current : (family SHA256CompressionRoundState) .
161 (family SHA256CompressionRoundsResult))
162 roundState
163 (branch
164 SHA256CompressionRoundStateValue
165 state
166 index
167 rotates
168 shifts
169 booleans
170 adds
171 .
172 (constructor
173 SHA256CompressionRoundsResult
174 SHA256CompressionRoundsFailed
175 (constructor SHA256ErrorCode SHA256RoundCountInvalid)
176 index))))))))
177 (branch
178 SHA256ScheduleNext
179 scheduleWord
180 scheduleTail
181 induction
182 .
183 (lambda unrestricted constants : (family SHA256Schedule) .
184 (lambda unrestricted roundState : (family SHA256CompressionRoundState) .
185 (eliminate
186 SHA256Schedule
187 (lambda unrestricted current : (family SHA256Schedule) .
188 (family SHA256CompressionRoundsResult))
189 constants
190 (branch
191 SHA256ScheduleEnd
192 .
193 (eliminate
194 SHA256CompressionRoundState
195 (lambda unrestricted current : (family SHA256CompressionRoundState) .
196 (family SHA256CompressionRoundsResult))
197 roundState
198 (branch
199 SHA256CompressionRoundStateValue
200 state
201 index
202 rotates
203 shifts
204 booleans
205 adds
206 .
207 (constructor
208 SHA256CompressionRoundsResult
209 SHA256CompressionRoundsFailed
210 (constructor SHA256ErrorCode SHA256RoundCountInvalid)
211 index))))
212 (branch
213 SHA256ScheduleNext
214 constant
215 constantTail
216 constantInduction
217 .
218 (eliminate
219 SHA256CompressionRoundState
220 (lambda unrestricted current : (family SHA256CompressionRoundState) .
221 (family SHA256CompressionRoundsResult))
222 roundState
223 (branch
224 SHA256CompressionRoundStateValue
225 state
226 index
227 rotates
228 shifts
229 booleans
230 adds
231 .
232 (induction
233 constantTail
234 (constructor
235 SHA256CompressionRoundState
236 SHA256CompressionRoundStateValue
237 (sha256RoundState constant scheduleWord state)
238 (succ index)
239 (naturalAdd (byte-to-nat (byte 6)) rotates)
240 shifts
241 (naturalAdd (byte-to-nat (byte 2)) booleans)
242 (naturalAdd (byte-to-nat (byte 7)) adds))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.