AlphaGitHub
Source/Packages

Checkpoint.Schema

packages/execution/persistence/src/Checkpoint/Schema.alpha

2,376 lines254 declarations94.9 KiBSHA-256 c49b7c5718ad
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 612–643

checkpointWord64ToNatural

Full file
612def checkpointWord64ToNatural =
613  (lambda unrestricted value : (family ModelWord64) .
614    (eliminate
615      ModelWord64
616      (lambda unrestricted current : (family ModelWord64) . Nat)
617      value
618      (branch
619        ModelWord64Value
620        b0
621        b1
622        b2
623        b3
624        b4
625        b5
626        b6
627        b7
628        .
629        (naturalAdd
630          (byte-to-nat b0)
631          (naturalAdd
632            (naturalMultiply (byte-to-nat b1) (naturalPowerOfTwo (byte-to-nat (byte 8))))
633            (naturalAdd
634              (naturalMultiply (byte-to-nat b2) (naturalPowerOfTwo (byte-to-nat (byte 16))))
635              (naturalAdd
636                (naturalMultiply (byte-to-nat b3) (naturalPowerOfTwo (byte-to-nat (byte 24))))
637                (naturalAdd
638                  (naturalMultiply (byte-to-nat b4) (naturalPowerOfTwo (byte-to-nat (byte 32))))
639                  (naturalAdd
640                    (naturalMultiply (byte-to-nat b5) (naturalPowerOfTwo (byte-to-nat (byte 40))))
641                    (naturalAdd
642                      (naturalMultiply (byte-to-nat b6) (naturalPowerOfTwo (byte-to-nat (byte 48))))
643                      (naturalMultiply (byte-to-nat b7) (naturalPowerOfTwo (byte-to-nat (byte 56))))))))))))))

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.