Raw digest ABI: padded blocks at RDI, positive count at RSI, 32-byte output
at RDX, private work area at R9. RCX/R8 are unused. The caller proves valid
padding and nonoverlap. Returns 32; no timestamp write and no payload copy.
1027def wordDigestAssemblyFor =
1028 (lambda erased A : Type 0 .
1029 (lambda erased R : Type 0 .
1030 (lambda unrestricted backend : (family WordDigestBackend A R) .
1031 (wordDigestBlocksAssemblyFor
1032 A
1033 R
1034 backend
1035 (lambda unrestricted tail : A . tail)
1036 (wordDigestOutputFor A R backend)))))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.