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