390def sha256PadContext =
391 (lambda unrestricted context : (family SHA256Context) .
392 (eliminate
393 SHA256ContextValidationResult
394 (lambda unrestricted current : (family SHA256ContextValidationResult) .
395 (family SHA256ContextPaddingResult))
396 (sha256ValidateContext context)
397 (branch
398 SHA256ContextValidated
399 validated
400 validationTelemetry
401 .
402 (eliminate
403 SHA256Context
404 (lambda unrestricted current : (family SHA256Context) .
405 (family SHA256ContextPaddingResult))
406 validated
407 (branch
408 SHA256ContextValue
409 state
410 totalBytes
411 pending
412 .
413 (eliminate
414 ModelWord64MultiplyCheckedResult
415 (lambda unrestricted current : (family ModelWord64MultiplyCheckedResult) .
416 (family SHA256ContextPaddingResult))
417 (modelWord64MultiplyChecked totalBytes sha256Word64Eight)
418 (branch
419 ModelWord64MultiplySucceeded
420 bitLength
421 .
422 (app
423 (lambda unrestricted pendingBytes : Nat .
424 (app
425 (lambda unrestricted zeroBytes : Nat .
426 (app
427 (lambda unrestricted lengthBytes : Bytes .
428 (sha256PadContextPart1
429 validationTelemetry
430 totalBytes
431 bitLength
432 pendingBytes
433 zeroBytes
434 lengthBytes
435 (bytes-append
436 pending
437 (bytes-cons
438 (byte 128)
439 (bytes-append (sha256ZeroBytes zeroBytes) lengthBytes)))))
440 (dataBytesWord64BE bitLength)))
441 (sha256PaddingZeroCount pendingBytes)))
442 (bytes-length pending)))
443 (branch
444 ModelWord64MultiplyOverflow
445 .
446 (constructor
447 SHA256ContextPaddingResult
448 SHA256ContextPaddingFailed
449 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
450 (succ zero)
451 validationTelemetry))))))
452 (branch
453 SHA256ContextValidationFailed
454 error
455 telemetry
456 .
457 (constructor SHA256ContextPaddingResult SHA256ContextPaddingFailed error zero telemetry))))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.