RDI: total u32 bytes; RSI: writable two-word chunk plan; R9: private
work area. Reject oversized totals before writes, initialize chaining words,
return 32. Valid disjoint destination/work buffers are the caller contract.
1070def wordDigestStreamStartFor =
1071 (lambda erased A : Type 0 .
1072 (lambda erased R : Type 0 .
1073 (lambda unrestricted backend : (family WordDigestBackend A R) .
1074 (eliminate
1075 WordDigestBackend
1076 (lambda unrestricted current : (family WordDigestBackend A R) . A)
1077 backend
1078 (branch
1079 WordDigestBackendValue
1080 digestLoad32
1081 digestLoad64
1082 digestLoad8
1083 digestStore32
1084 digestStore64
1085 digestStore8
1086 digestMov
1087 digestAdd
1088 digestAnd
1089 digestOr
1090 digestXor
1091 digestShl
1092 digestShr
1093 digestMovImm
1094 digestAddImm
1095 digestAndImm
1096 digestCmpImm
1097 digestMulImm
1098 digestLabel
1099 digestJumpIf
1100 digestReturn
1101 digestEnd
1102 digestRAX
1103 digestRBX
1104 digestRCX
1105 digestRDX
1106 digestRSI
1107 digestRDI
1108 digestRBP
1109 digestR8
1110 digestR9
1111 digestR10
1112 digestR11
1113 digestR12
1114 digestR13
1115 digestR14
1116 digestR15
1117 .
1118 (digestMov
1119 digestRAX
1120 digestRDI
1121 (digestShr
1122 digestRAX
1123 32
1124 (digestCmpImm
1125 digestRAX
1126 0
1127 (digestJumpIf
1128 (constructor WordDigestCondition WordDigestZero)
1129 b"stream-start"
1130 (digestMovImm
1131 digestRAX
1132 0
1133 (digestReturn
1134 (digestLabel
1135 b"stream-start"
1136 (digestMov
1137 digestRAX
1138 digestRDI
1139 (digestShr
1140 digestRAX
1141 byteDigestChunkShift
1142 (digestStore64
1143 digestRSI
1144 0
1145 digestRAX
1146 (digestMov
1147 digestRAX
1148 digestRDI
1149 (digestAndImm
1150 digestRAX
1151 (naturalSaturatingSubtract byteDigestChunkBytes 1)
1152 (digestStore64
1153 digestRSI
1154 digestAddressBytes
1155 digestRAX
1156 (wordDigestInitializeFor
1157 A
1158 R
1159 backend
1160 (digestMovImm
1161 digestRAX
1162 digestStateBytes
1163 (digestReturn digestEnd)))))))))))))))))))))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.