Byte-digest ABI, with the original total in R8 and only the final window
tail at RDI/RSI. Prior full windows must have been compressed in this work
region. Zero-fill padding uses the original bit count, never the tail count.
1168def wordDigestStreamFinishFor =
1169 (lambda erased A : Type 0 .
1170 (lambda erased R : Type 0 .
1171 (lambda unrestricted backend : (family WordDigestBackend A R) .
1172 (eliminate
1173 WordDigestBackend
1174 (lambda unrestricted current : (family WordDigestBackend A R) . A)
1175 backend
1176 (branch
1177 WordDigestBackendValue
1178 digestLoad32
1179 digestLoad64
1180 digestLoad8
1181 digestStore32
1182 digestStore64
1183 digestStore8
1184 digestMov
1185 digestAdd
1186 digestAnd
1187 digestOr
1188 digestXor
1189 digestShl
1190 digestShr
1191 digestMovImm
1192 digestAddImm
1193 digestAndImm
1194 digestCmpImm
1195 digestMulImm
1196 digestLabel
1197 digestJumpIf
1198 digestReturn
1199 digestEnd
1200 digestRAX
1201 digestRBX
1202 digestRCX
1203 digestRDX
1204 digestRSI
1205 digestRDI
1206 digestRBP
1207 digestR8
1208 digestR9
1209 digestR10
1210 digestR11
1211 digestR12
1212 digestR13
1213 digestR14
1214 digestR15
1215 .
1216 (digestMov
1217 digestRAX
1218 digestR8
1219 (digestShr
1220 digestRAX
1221 32
1222 (digestCmpImm
1223 digestRAX
1224 0
1225 (digestJumpIf
1226 (constructor WordDigestCondition WordDigestNotZero)
1227 b"byte-digest-refused"
1228 (digestMov
1229 digestRAX
1230 digestR8
1231 (digestAndImm
1232 digestRAX
1233 (naturalSaturatingSubtract byteDigestChunkBytes 1)
1234 (digestXor
1235 digestRAX
1236 digestRSI
1237 (digestCmpImm
1238 digestRAX
1239 0
1240 (digestJumpIf
1241 (constructor WordDigestCondition WordDigestNotZero)
1242 b"byte-digest-refused"
1243 (wordDigestBytePaddingFor
1244 A
1245 R
1246 backend
1247 digestR8
1248 (wordDigestContinueAssemblyFor 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.