Part of `sha256PadContext`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
334def sha256PadContextPart1 =
335 (lambda unrestricted validationTelemetry : (family SHA256ContextValidationTelemetry) .
336 (lambda unrestricted totalBytes : (family ModelWord64) .
337 (lambda unrestricted bitLength : (family ModelWord64) .
338 (lambda unrestricted pendingBytes : Nat .
339 (lambda unrestricted zeroBytes : Nat .
340 (lambda unrestricted lengthBytes : Bytes .
341 (lambda unrestricted suffix : Bytes .
342 (app
343 (lambda unrestricted finalBytes : Nat .
344 (app
345 (lambda unrestricted blockCount : Nat .
346 (nat-eliminate
347 (lambda unrestricted encodedLengthValid : Nat .
348 (family SHA256ContextPaddingResult))
349 (constructor
350 SHA256ContextPaddingResult
351 SHA256ContextPaddingFailed
352 (constructor SHA256ErrorCode SHA256LengthEncodingInvalid)
353 (succ (succ zero))
354 validationTelemetry)
355 (lambda unrestricted encodedPredecessor : Nat .
356 (lambda unrestricted encodedInduction : (family SHA256ContextPaddingResult) .
357 (nat-eliminate
358 (lambda unrestricted finalLengthValid : Nat .
359 (family SHA256ContextPaddingResult))
360 (constructor
361 SHA256ContextPaddingResult
362 SHA256ContextPaddingFailed
363 (constructor SHA256ErrorCode SHA256PaddingLengthInvalid)
364 (succ (succ (succ zero)))
365 validationTelemetry)
366 (lambda unrestricted finalPredecessor : Nat .
367 (lambda unrestricted finalInduction : (family SHA256ContextPaddingResult) .
368 (constructor
369 SHA256ContextPaddingResult
370 SHA256ContextPaddingSucceeded
371 suffix
372 (constructor
373 SHA256ContextPaddingTelemetry
374 SHA256ContextPaddingTelemetryValue
375 totalBytes
376 pendingBytes
377 bitLength
378 zeroBytes
379 finalBytes
380 blockCount))))
381 (naturalOr
382 (naturalEqual finalBytes sha256NaturalSixtyFour)
383 (naturalEqual
384 finalBytes
385 sha256PaddingNaturalOneHundredTwentyEight)))))
386 (naturalEqual (bytes-length lengthBytes) sha256PaddingNaturalEight)))
387 (naturalDivideUnchecked finalBytes sha256NaturalSixtyFour)))
388 (bytes-length suffix)))))))))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.