Run `fuel` expansion steps, FIRST-ORDER.
The previous definition folded with a FUNCTION accumulator
(`pi state . Result`) and recursed by applying the induction hypothesis to the
next state. Because the VM normalizes a fold's function part before the
concrete state is supplied, it symbolically unrolled all 48 iterations of a
large step body (four schedule lookups + sigma arithmetic each) into one giant
term and only then evaluated it -- ~O(fuel^2 * body) work that kept expansion
slow even after the lookup itself was made linear.
This version folds with a first-order accumulator: the step-result VALUE
(`Succeeded state | Failed`). Each iteration runs exactly one `expandStep` on
the concrete accumulated state (or threads a failure through), so the whole
expansion is O(fuel) over concrete values with no symbolic term building. The
computed words -- and therefore the digest -- are unchanged.
246def sha256ExpandScheduleWithFuel =
247 (lambda unrestricted fuel : Nat .
248 (lambda unrestricted initialState : (family SHA256ScheduleExpansionState) .
249 (eliminate
250 SHA256ScheduleExpansionStepResult
251 (lambda unrestricted current : (family SHA256ScheduleExpansionStepResult) .
252 (family SHA256ScheduleExpansionResult))
253 (nat-eliminate
254 (lambda unrestricted current : Nat . (family SHA256ScheduleExpansionStepResult))
255 (constructor
256 SHA256ScheduleExpansionStepResult
257 SHA256ScheduleExpansionStepSucceeded
258 initialState)
259 (lambda unrestricted predecessor : Nat .
260 (lambda unrestricted induction : (family SHA256ScheduleExpansionStepResult) .
261 (eliminate
262 SHA256ScheduleExpansionStepResult
263 (lambda unrestricted current : (family SHA256ScheduleExpansionStepResult) .
264 (family SHA256ScheduleExpansionStepResult))
265 induction
266 (branch
267 SHA256ScheduleExpansionStepSucceeded
268 state
269 .
270 (sha256ExpandScheduleStep state))
271 (branch SHA256ScheduleExpansionStepFailed error failedIndex . induction))))
272 fuel)
273 (branch
274 SHA256ScheduleExpansionStepSucceeded
275 state
276 .
277 (eliminate
278 SHA256ScheduleExpansionState
279 (lambda unrestricted current : (family SHA256ScheduleExpansionState) .
280 (family SHA256ScheduleExpansionResult))
281 state
282 (branch
283 SHA256ScheduleExpansionStateValue
284 schedule
285 nextIndex
286 generated
287 lookups
288 sigmas
289 rotates
290 shifts
291 adds
292 .
293 (constructor
294 SHA256ScheduleExpansionResult
295 SHA256ScheduleExpansionSucceeded
296 schedule
297 (constructor
298 SHA256ScheduleExpansionTelemetry
299 SHA256ScheduleExpansionTelemetryValue
300 generated
301 lookups
302 sigmas
303 rotates
304 shifts
305 adds)))))
306 (branch
307 SHA256ScheduleExpansionStepFailed
308 error
309 failedIndex
310 .
311 (constructor
312 SHA256ScheduleExpansionResult
313 SHA256ScheduleExpansionFailed
314 error
315 failedIndex)))))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.