Decode exactly `pairs` pairs. The public caller first proves a 64-byte
source length, so the two heads in every one of the 32 steps are in range.
1403def sha256DigestDecodeHexPairs =
1404 (lambda unrestricted pairs : Nat .
1405 (nat-eliminate
1406 (lambda unrestricted current : Nat .
1407 (pi unrestricted input : Bytes . (family StdResult (family SHA256ErrorCode) Bytes)))
1408 (lambda unrestricted input : Bytes .
1409 (constructor StdResult StdSuccess (family SHA256ErrorCode) Bytes b""))
1410 (lambda unrestricted predecessor : Nat .
1411 (lambda unrestricted induction : (pi unrestricted input : Bytes . (family StdResult (family SHA256ErrorCode) Bytes)) .
1412 (lambda unrestricted input : Bytes .
1413 (app
1414 (lambda unrestricted high : Nat .
1415 (app
1416 (lambda unrestricted low : Nat .
1417 (nat-eliminate
1418 (lambda unrestricted invalid : Nat .
1419 (family StdResult (family SHA256ErrorCode) Bytes))
1420 (eliminate
1421 StdResult
1422 (lambda unrestricted current : (family StdResult (family SHA256ErrorCode) Bytes) .
1423 (family StdResult (family SHA256ErrorCode) Bytes))
1424 (induction (bytes-tail (bytes-tail input)))
1425 (branch
1426 StdFailure
1427 error
1428 .
1429 (constructor StdResult StdFailure (family SHA256ErrorCode) Bytes error))
1430 (branch
1431 StdSuccess
1432 decodedTail
1433 .
1434 (constructor
1435 StdResult
1436 StdSuccess
1437 (family SHA256ErrorCode)
1438 Bytes
1439 (bytes-cons
1440 (nat-to-byte (naturalAdd (naturalMultiply high 16) low))
1441 decodedTail))))
1442 (lambda unrestricted invalidPredecessor : Nat .
1443 (lambda unrestricted invalidInduction : (family StdResult (family SHA256ErrorCode) Bytes) .
1444 (constructor
1445 StdResult
1446 StdFailure
1447 (family SHA256ErrorCode)
1448 Bytes
1449 (constructor SHA256ErrorCode SHA256DigestHexInvalid))))
1450 (naturalOr
1451 (naturalIsZero (nat-less-than high 16))
1452 (naturalIsZero (nat-less-than low 16)))))
1453 (sha256DigestLowerHexNibble (bytes-head (bytes-tail input)))))
1454 (sha256DigestLowerHexNibble (bytes-head input))))))
1455 pairs))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.