227def sha256EncodeBitLength =
228 (lambda unrestricted bitLength : Nat .
229 (eliminate
230 SHA256LengthEncodingState
231 (lambda unrestricted current : (family SHA256LengthEncodingState) .
232 (family SHA256LengthEncodingResult))
233 (app
234 (nat-eliminate
235 (lambda unrestricted current : Nat .
236 (pi unrestricted state : (family SHA256LengthEncodingState) .
237 (family SHA256LengthEncodingState)))
238 (lambda unrestricted state : (family SHA256LengthEncodingState) . state)
239 (lambda unrestricted predecessor : Nat .
240 (lambda unrestricted induction : (pi unrestricted state : (family SHA256LengthEncodingState) . (family SHA256LengthEncodingState)) .
241 (lambda unrestricted state : (family SHA256LengthEncodingState) .
242 (induction (sha256LengthEncodingStep state)))))
243 sha256PaddingNaturalEight)
244 (constructor
245 SHA256LengthEncodingState
246 SHA256LengthEncodingStateValue
247 bitLength
248 b""
249 zero))
250 (branch
251 SHA256LengthEncodingStateValue
252 remaining
253 encoded
254 count
255 .
256 (nat-eliminate
257 (lambda unrestricted remainingZero : Nat . (family SHA256LengthEncodingResult))
258 (constructor
259 SHA256LengthEncodingResult
260 SHA256LengthEncodingFailed
261 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
262 remaining)
263 (lambda unrestricted predecessor : Nat .
264 (lambda unrestricted induction : (family SHA256LengthEncodingResult) .
265 (nat-eliminate
266 (lambda unrestricted validBytes : Nat . (family SHA256LengthEncodingResult))
267 (constructor
268 SHA256LengthEncodingResult
269 SHA256LengthEncodingFailed
270 (constructor SHA256ErrorCode SHA256DigestLengthInvalid)
271 remaining)
272 (lambda unrestricted bytePredecessor : Nat .
273 (lambda unrestricted byteInduction : (family SHA256LengthEncodingResult) .
274 (constructor
275 SHA256LengthEncodingResult
276 SHA256LengthEncodingSucceeded
277 encoded
278 bitLength)))
279 (naturalEqual (bytes-length encoded) sha256PaddingNaturalEight))))
280 (naturalIsZero remaining)))))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.