263def wordDigestBytePaddingFor =
264 (lambda erased A : Type 0 .
265 (lambda erased R : Type 0 .
266 (lambda unrestricted backend : (family WordDigestBackend A R) .
267 (lambda unrestricted totalBytes : R .
268 (lambda unrestricted blocks : A .
269 (eliminate
270 WordDigestBackend
271 (lambda unrestricted current : (family WordDigestBackend A R) . A)
272 backend
273 (branch
274 WordDigestBackendValue
275 digestLoad32
276 digestLoad64
277 digestLoad8
278 digestStore32
279 digestStore64
280 digestStore8
281 digestMov
282 digestAdd
283 digestAnd
284 digestOr
285 digestXor
286 digestShl
287 digestShr
288 digestMovImm
289 digestAddImm
290 digestAndImm
291 digestCmpImm
292 digestMulImm
293 digestLabel
294 digestJumpIf
295 digestReturn
296 digestEnd
297 digestRAX
298 digestRBX
299 digestRCX
300 digestRDX
301 digestRSI
302 digestRDI
303 digestRBP
304 digestR8
305 digestR9
306 digestR10
307 digestR11
308 digestR12
309 digestR13
310 digestR14
311 digestR15
312 .
313 (digestCmpImm
314 digestRDI
315 0
316 (digestJumpIf
317 (constructor WordDigestCondition WordDigestNegative)
318 b"byte-digest-refused"
319 (digestJumpIf
320 (constructor WordDigestCondition WordDigestZero)
321 b"byte-digest-refused"
322 (digestMov
323 digestRAX
324 digestRSI
325 (digestShr
326 digestRAX
327 32
328 (digestCmpImm
329 digestRAX
330 0
331 (digestJumpIf
332 (constructor WordDigestCondition WordDigestNotZero)
333 b"byte-digest-refused"
334 (digestMov
335 digestR10
336 digestRDI
337 (digestAdd
338 digestR10
339 digestRSI
340 (digestMovImm
341 digestRAX
342 0
343 (wordDigestFor
344 A
345 (naturalDivideUnchecked
346 byteDigestPaddingBytes
347 digestAddressBytes)
348 (lambda unrestricted index : Nat .
349 (digestStore64
350 digestR10
351 (naturalMultiply index digestAddressBytes)
352 digestRAX))
353 (digestMovImm
354 digestRAX
355 128
356 (digestStore8
357 digestR10
358 0
359 digestRAX
360 (digestMov
361 digestRCX
362 totalBytes
363 (digestShl
364 digestRCX
365 3
366 (digestAddImm
367 digestRSI
368 (naturalAdd digestBlockBytes digestAddressBytes)
369 (digestShr
370 digestRSI
371 6
372 (digestMov
373 digestR10
374 digestRSI
375 (digestShl
376 digestR10
377 6
378 (digestAdd
379 digestR10
380 digestRDI
381 (digestAddImm
382 digestR10
383 4294967288
384 (wordDigestFor
385 A
386 digestAddressBytes
387 (lambda unrestricted index : Nat .
388 (lambda unrestricted rest : A .
389 (digestMov
390 digestRAX
391 digestRCX
392 (digestShr
393 digestRAX
394 (naturalMultiply 8 (naturalSaturatingSubtract 7 index))
395 (digestStore8 digestR10 index digestRAX rest)))))
396 blocks)))))))))))))))))))))))))))))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.