Part of `sha256PadContext`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
297def sha256PadContextPart1 =
298 (lambda unrestricted validationTelemetry : (family SHA256ContextValidationTelemetry) .
299 (lambda unrestricted totalBytes : (family ModelWord64) .
300 (lambda unrestricted bitLength : (family ModelWord64) .
301 (lambda unrestricted pendingBytes : Nat .
302 (lambda unrestricted zeroBytes : Nat .
303 (lambda unrestricted lengthBytes : Bytes .
304 (lambda unrestricted suffix : Bytes .
305 (app
306 (lambda unrestricted finalBytes : Nat .
307 (app
308 (lambda unrestricted blockCount : Nat .
309 (nat-eliminate
310 (lambda unrestricted encodedLengthValid : Nat .
311 (family SHA256ContextPaddingResult))
312 (constructor
313 SHA256ContextPaddingResult
314 SHA256ContextPaddingFailed
315 (constructor SHA256ErrorCode SHA256LengthEncodingInvalid)
316 (succ (succ zero))
317 validationTelemetry)
318 (lambda unrestricted encodedPredecessor : Nat .
319 (lambda unrestricted encodedInduction : (family SHA256ContextPaddingResult) .
320 (nat-eliminate
321 (lambda unrestricted finalLengthValid : Nat .
322 (family SHA256ContextPaddingResult))
323 (constructor
324 SHA256ContextPaddingResult
325 SHA256ContextPaddingFailed
326 (constructor SHA256ErrorCode SHA256PaddingLengthInvalid)
327 (succ (succ (succ zero)))
328 validationTelemetry)
329 (lambda unrestricted finalPredecessor : Nat .
330 (lambda unrestricted finalInduction : (family SHA256ContextPaddingResult) .
331 (constructor
332 SHA256ContextPaddingResult
333 SHA256ContextPaddingSucceeded
334 suffix
335 (constructor
336 SHA256ContextPaddingTelemetry
337 SHA256ContextPaddingTelemetryValue
338 totalBytes
339 pendingBytes
340 bitLength
341 zeroBytes
342 finalBytes
343 blockCount))))
344 (naturalOr
345 (naturalEqual finalBytes sha256NaturalSixtyFour)
346 (naturalEqual
347 finalBytes
348 sha256PaddingNaturalOneHundredTwentyEight)))))
349 (naturalEqual (bytes-length lengthBytes) sha256PaddingNaturalEight)))
350 (naturalDivideUnchecked finalBytes sha256NaturalSixtyFour)))
351 (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.