108def sha256Round =
109 (lambda unrestricted input : (family SHA256RoundInput) .
110 (eliminate
111 SHA256RoundInput
112 (lambda unrestricted current : (family SHA256RoundInput) . (family SHA256RoundOutput))
113 input
114 (branch
115 SHA256RoundInputValue
116 index
117 constant
118 schedule
119 a
120 b
121 c
122 d
123 e
124 f
125 g
126 h
127 .
128 (constructor
129 SHA256RoundOutput
130 SHA256RoundOutputValue
131 (sha256RoundState
132 constant
133 schedule
134 (constructor SHA256State SHA256StateValue a b c d e f g h))
135 (constructor
136 SHA256RoundTelemetry
137 SHA256RoundTelemetryValue
138 index
139 (byte-to-nat (byte 6))
140 zero
141 (byte-to-nat (byte 2))
142 (byte-to-nat (byte 7)))))))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.