353def sha256PadContext =
354 (lambda unrestricted context : (family SHA256Context) .
355 (eliminate
356 SHA256ContextValidationResult
357 (lambda unrestricted current : (family SHA256ContextValidationResult) .
358 (family SHA256ContextPaddingResult))
359 (sha256ValidateContext context)
360 (branch
361 SHA256ContextValidated
362 validated
363 validationTelemetry
364 .
365 (eliminate
366 SHA256Context
367 (lambda unrestricted current : (family SHA256Context) .
368 (family SHA256ContextPaddingResult))
369 validated
370 (branch
371 SHA256ContextValue
372 state
373 totalBytes
374 pending
375 .
376 (eliminate
377 ModelWord64MultiplyCheckedResult
378 (lambda unrestricted current : (family ModelWord64MultiplyCheckedResult) .
379 (family SHA256ContextPaddingResult))
380 (modelWord64MultiplyChecked totalBytes sha256Word64Eight)
381 (branch
382 ModelWord64MultiplySucceeded
383 bitLength
384 .
385 (app
386 (lambda unrestricted pendingBytes : Nat .
387 (app
388 (lambda unrestricted zeroBytes : Nat .
389 (app
390 (lambda unrestricted lengthBytes : Bytes .
391 (sha256PadContextPart1
392 validationTelemetry
393 totalBytes
394 bitLength
395 pendingBytes
396 zeroBytes
397 lengthBytes
398 (bytes-append
399 pending
400 (bytes-cons
401 (byte 128)
402 (bytes-append (sha256ZeroBytes zeroBytes) lengthBytes)))))
403 (dataBytesWord64BE bitLength)))
404 (sha256PaddingZeroCount pendingBytes)))
405 (bytes-length pending)))
406 (branch
407 ModelWord64MultiplyOverflow
408 .
409 (constructor
410 SHA256ContextPaddingResult
411 SHA256ContextPaddingFailed
412 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
413 (succ zero)
414 validationTelemetry))))))
415 (branch
416 SHA256ContextValidationFailed
417 error
418 telemetry
419 .
420 (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.