Initialize only the chaining words; saved registers and the round scratch
remain private to each compression call. Initialization does not erase them.
882def wordDigestInitializeFor =
883 (lambda erased A : Type 0 .
884 (lambda erased R : Type 0 .
885 (lambda unrestricted backend : (family WordDigestBackend A R) .
886 (lambda unrestricted tail : A .
887 (eliminate
888 WordDigestBackend
889 (lambda unrestricted current : (family WordDigestBackend A R) . A)
890 backend
891 (branch
892 WordDigestBackendValue
893 digestLoad32
894 digestLoad64
895 digestLoad8
896 digestStore32
897 digestStore64
898 digestStore8
899 digestMov
900 digestAdd
901 digestAnd
902 digestOr
903 digestXor
904 digestShl
905 digestShr
906 digestMovImm
907 digestAddImm
908 digestAndImm
909 digestCmpImm
910 digestMulImm
911 digestLabel
912 digestJumpIf
913 digestReturn
914 digestEnd
915 digestRAX
916 digestRBX
917 digestRCX
918 digestRDX
919 digestRSI
920 digestRDI
921 digestRBP
922 digestR8
923 digestR9
924 digestR10
925 digestR11
926 digestR12
927 digestR13
928 digestR14
929 digestR15
930 .
931 (wordDigestFor
932 A
933 digestStateWords
934 (lambda unrestricted i : Nat .
935 (lambda unrestricted rest : A .
936 (digestMovImm
937 digestRAX
938 (digestAt digestInitialHash i)
939 (digestStore32 digestR9 (digestH i) digestRAX rest))))
940 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.