956def wordDigestOutputFor =
957 (lambda erased A : Type 0 .
958 (lambda erased R : Type 0 .
959 (lambda unrestricted backend : (family WordDigestBackend A R) .
960 (lambda unrestricted tail : A .
961 (eliminate
962 WordDigestBackend
963 (lambda unrestricted current : (family WordDigestBackend A R) . A)
964 backend
965 (branch
966 WordDigestBackendValue
967 digestLoad32
968 digestLoad64
969 digestLoad8
970 digestStore32
971 digestStore64
972 digestStore8
973 digestMov
974 digestAdd
975 digestAnd
976 digestOr
977 digestXor
978 digestShl
979 digestShr
980 digestMovImm
981 digestAddImm
982 digestAndImm
983 digestCmpImm
984 digestMulImm
985 digestLabel
986 digestJumpIf
987 digestReturn
988 digestEnd
989 digestRAX
990 digestRBX
991 digestRCX
992 digestRDX
993 digestRSI
994 digestRDI
995 digestRBP
996 digestR8
997 digestR9
998 digestR10
999 digestR11
1000 digestR12
1001 digestR13
1002 digestR14
1003 digestR15
1004 .
1005 (wordDigestFor
1006 A
1007 digestStateBytes
1008 (lambda unrestricted q : Nat .
1009 (lambda unrestricted rest : A .
1010 (digestLoad32
1011 digestRAX
1012 digestR9
1013 (digestH (naturalDivideUnchecked q digestWordBytes))
1014 (digestShr
1015 digestRAX
1016 (naturalMultiply
1017 8
1018 (naturalSaturatingSubtract
1019 (naturalSaturatingSubtract digestWordBytes 1)
1020 (naturalModuloUnchecked q digestWordBytes)))
1021 (digestStore8 digestRDX q digestRAX rest)))))
1022 (digestMovImm digestRAX digestStateBytes tail))))))))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.