11def telemetrySealAssemblyFor =
12 (lambda erased A : Type 0 .
13 (lambda erased R : Type 0 .
14 (lambda unrestricted backend : (family WordDigestBackend A R) .
15 (eliminate
16 WordDigestBackend
17 (lambda unrestricted current : (family WordDigestBackend A R) . A)
18 backend
19 (branch
20 WordDigestBackendValue
21 sealLoad32
22 sealLoad64
23 sealLoad8
24 sealStore32
25 sealStore64
26 sealStore8
27 sealMov
28 sealAdd
29 sealAnd
30 sealOr
31 sealXor
32 sealShl
33 sealShr
34 sealMovImm
35 sealAddImm
36 sealAndImm
37 sealCmpImm
38 sealMulImm
39 sealLabel
40 sealJumpIf
41 sealReturn
42 sealEnd
43 sealRAX
44 sealRBX
45 sealRCX
46 sealRDX
47 sealRSI
48 sealRDI
49 sealRBP
50 sealR8
51 sealR9
52 sealR10
53 sealR11
54 sealR12
55 sealR13
56 sealR14
57 sealR15
58 .
59 (let unrestricted sealHexDigit =
60 (lambda unrestricted q : Nat .
61 (lambda unrestricted rest : A .
62 (let unrestricted skip =
63 (bytes-cons (nat-to-byte q) b"seal-hex-digit")
64 in
65 (sealLoad32
66 sealRAX
67 sealR9
68 (digestH (naturalDivideUnchecked q 8))
69 (sealShr
70 sealRAX
71 (naturalMultiply
72 4
73 (naturalSaturatingSubtract 7 (naturalModuloUnchecked q 8)))
74 (sealAndImm
75 sealRAX
76 15
77 (sealCmpImm
78 sealRAX
79 10
80 (sealJumpIf
81 (constructor WordDigestCondition WordDigestBelow)
82 skip
83 (sealAddImm
84 sealRAX
85 39
86 (sealLabel
87 skip
88 (sealAddImm sealRAX 48 (sealStore8 sealRDX q sealRAX rest))))))))))))
89 in
90 (wordDigestBlocksAssemblyFor
91 A
92 R
93 backend
94 (lambda unrestricted tail : A .
95 (sealLoad64
96 sealRAX
97 sealR8
98 0
99 (sealMulImm
100 sealRAX
101 1000000000
102 (sealLoad64
103 sealRBX
104 sealR8
105 8
106 (sealAdd sealRAX sealRBX (sealStore64 sealRDI sealMonotonicAt sealRAX tail))))))
107 (lambda unrestricted tail : A .
108 (sealAddImm
109 sealRDX
110 8
111 (sealLabel
112 b"seal-copy"
113 (sealLoad8
114 sealRAX
115 sealR15
116 0
117 (sealStore8
118 sealRDX
119 0
120 sealRAX
121 (sealAddImm
122 sealR15
123 1
124 (sealAddImm
125 sealRDX
126 1
127 (sealAddImm
128 sealRCX
129 0xFFFFFFFF
130 (sealJumpIf
131 (constructor WordDigestCondition WordDigestNotZero)
132 b"seal-copy"
133 (wordDigestFor A 64 sealHexDigit 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.