module Model.Word64

import Model.Parameter
import Std.Byte
import Std.Natural
import Std.Flag

family ModelWord64ArithmeticErrorCode : Type 0
constructor ModelWord64AdditionOverflow
constructor ModelWord64SubtractionUnderflow

end-family

family ModelWord64AddResult : Type 0
constructor ModelWord64AddResultValue
field unrestricted modelWord64AddValue : (family ModelWord64)
field unrestricted modelWord64AddCarry : Nat

end-family

family ModelWord64CheckedResult : Type 0
constructor ModelWord64CheckedSucceeded
field unrestricted modelWord64CheckedValue : (family ModelWord64)
constructor ModelWord64CheckedFailed
field unrestricted modelWord64CheckedError : (family ModelWord64ArithmeticErrorCode)

end-family

family ModelWord64MultiplyState : Type 0
constructor ModelWord64MultiplyStateValue
field unrestricted modelWord64MultiplyMultiplicand : (family ModelWord64)
field unrestricted modelWord64MultiplyMultiplier : (family ModelWord64)
field unrestricted modelWord64MultiplyProduct : (family ModelWord64)
field unrestricted modelWord64MultiplyOverflow : Nat

end-family

family ModelWord64MultiplyCheckedResult : Type 0
constructor ModelWord64MultiplySucceeded
field unrestricted modelWord64MultiplyValue : (family ModelWord64)
constructor ModelWord64MultiplyOverflow

end-family

def modelWord64ArithmeticErrorCodeBytes =
  (lambda unrestricted code : (family ModelWord64ArithmeticErrorCode) .
    (eliminate
      ModelWord64ArithmeticErrorCode
      (lambda unrestricted current : (family ModelWord64ArithmeticErrorCode) . Bytes)
      code
      (branch ModelWord64AdditionOverflow . b"ALPHA-MODEL-W64-001")
      (branch ModelWord64SubtractionUnderflow . b"ALPHA-MODEL-W64-002")))

def modelWord64Zero =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def modelWord64One =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 1)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

-- Delegates to the one owner (Std.Flag), which this file already had a
-- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d).
def modelWord64FlagAnd =
  inferenceFlagAnd

def modelWord64Select =
  (lambda unrestricted condition : Nat .
    (lambda unrestricted whenTrue : (family ModelWord64) .
      (lambda unrestricted whenFalse : (family ModelWord64) .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family ModelWord64))
          whenFalse
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family ModelWord64) . whenTrue))
          condition))))

def modelWord64And =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (eliminate
        ModelWord64
        (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
        left
        (branch
          ModelWord64Value
          l0
          l1
          l2
          l3
          l4
          l5
          l6
          l7
          .
          (eliminate
            ModelWord64
            (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
            right
            (branch
              ModelWord64Value
              r0
              r1
              r2
              r3
              r4
              r5
              r6
              r7
              .
              (constructor
                ModelWord64
                ModelWord64Value
                (byteAnd l0 r0)
                (byteAnd l1 r1)
                (byteAnd l2 r2)
                (byteAnd l3 r3)
                (byteAnd l4 r4)
                (byteAnd l5 r5)
                (byteAnd l6 r6)
                (byteAnd l7 r7))))))))

def modelWord64Xor =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (eliminate
        ModelWord64
        (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
        left
        (branch
          ModelWord64Value
          l0
          l1
          l2
          l3
          l4
          l5
          l6
          l7
          .
          (eliminate
            ModelWord64
            (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
            right
            (branch
              ModelWord64Value
              r0
              r1
              r2
              r3
              r4
              r5
              r6
              r7
              .
              (constructor
                ModelWord64
                ModelWord64Value
                (byteXor l0 r0)
                (byteXor l1 r1)
                (byteXor l2 r2)
                (byteXor l3 r3)
                (byteXor l4 r4)
                (byteXor l5 r5)
                (byteXor l6 r6)
                (byteXor l7 r7))))))))

def modelWord64Complement =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
      value
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (constructor
          ModelWord64
          ModelWord64Value
          (byteXor b0 (byte 255))
          (byteXor b1 (byte 255))
          (byteXor b2 (byte 255))
          (byteXor b3 (byte 255))
          (byteXor b4 (byte 255))
          (byteXor b5 (byte 255))
          (byteXor b6 (byte 255))
          (byteXor b7 (byte 255))))))

def modelWord64IsZero =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . Nat)
      value
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (modelWord64FlagAnd
          (byte-equal b0 (byte 0))
          (modelWord64FlagAnd
            (byte-equal b1 (byte 0))
            (modelWord64FlagAnd
              (byte-equal b2 (byte 0))
              (modelWord64FlagAnd
                (byte-equal b3 (byte 0))
                (modelWord64FlagAnd
                  (byte-equal b4 (byte 0))
                  (modelWord64FlagAnd
                    (byte-equal b5 (byte 0))
                    (modelWord64FlagAnd (byte-equal b6 (byte 0)) (byte-equal b7 (byte 0))))))))))))

def modelWord64Equal =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (modelWord64IsZero (modelWord64Xor left right))))

def modelWord64OrderByte =
  (lambda unrestricted left : Byte .
    (lambda unrestricted right : Byte .
      (lambda unrestricted equalResult : Nat .
        (nat-eliminate
          (lambda unrestricted less : Nat . Nat)
          (nat-eliminate
            (lambda unrestricted greater : Nat . Nat)
            equalResult
            (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
            (byte-less-than right left))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : Nat . (succ zero)))
          (byte-less-than left right)))))

def modelWord64LessThan =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (eliminate
        ModelWord64
        (lambda unrestricted current : (family ModelWord64) . Nat)
        left
        (branch
          ModelWord64Value
          l0
          l1
          l2
          l3
          l4
          l5
          l6
          l7
          .
          (eliminate
            ModelWord64
            (lambda unrestricted current : (family ModelWord64) . Nat)
            right
            (branch
              ModelWord64Value
              r0
              r1
              r2
              r3
              r4
              r5
              r6
              r7
              .
              (modelWord64OrderByte
                l7
                r7
                (modelWord64OrderByte
                  l6
                  r6
                  (modelWord64OrderByte
                    l5
                    r5
                    (modelWord64OrderByte
                      l4
                      r4
                      (modelWord64OrderByte
                        l3
                        r3
                        (modelWord64OrderByte
                          l2
                          r2
                          (modelWord64OrderByte l1 r1 (modelWord64OrderByte l0 r0 zero))))))))))))))

def modelWord64AddWithCarry =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (eliminate
        ModelWord64
        (lambda unrestricted current : (family ModelWord64) . (family ModelWord64AddResult))
        left
        (branch
          ModelWord64Value
          l0
          l1
          l2
          l3
          l4
          l5
          l6
          l7
          .
          (eliminate
            ModelWord64
            (lambda unrestricted current : (family ModelWord64) . (family ModelWord64AddResult))
            right
            (branch
              ModelWord64Value
              r0
              r1
              r2
              r3
              r4
              r5
              r6
              r7
              .
              (eliminate
                ByteAddResult
                (lambda unrestricted current : (family ByteAddResult) .
                  (family ModelWord64AddResult))
                (byteAddWithCarry l0 r0 zero)
                (branch
                  ByteAddResultValue
                  s0
                  c0
                  .
                  (eliminate
                    ByteAddResult
                    (lambda unrestricted current : (family ByteAddResult) .
                      (family ModelWord64AddResult))
                    (byteAddWithCarry l1 r1 c0)
                    (branch
                      ByteAddResultValue
                      s1
                      c1
                      .
                      (eliminate
                        ByteAddResult
                        (lambda unrestricted current : (family ByteAddResult) .
                          (family ModelWord64AddResult))
                        (byteAddWithCarry l2 r2 c1)
                        (branch
                          ByteAddResultValue
                          s2
                          c2
                          .
                          (eliminate
                            ByteAddResult
                            (lambda unrestricted current : (family ByteAddResult) .
                              (family ModelWord64AddResult))
                            (byteAddWithCarry l3 r3 c2)
                            (branch
                              ByteAddResultValue
                              s3
                              c3
                              .
                              (eliminate
                                ByteAddResult
                                (lambda unrestricted current : (family ByteAddResult) .
                                  (family ModelWord64AddResult))
                                (byteAddWithCarry l4 r4 c3)
                                (branch
                                  ByteAddResultValue
                                  s4
                                  c4
                                  .
                                  (eliminate
                                    ByteAddResult
                                    (lambda unrestricted current : (family ByteAddResult) .
                                      (family ModelWord64AddResult))
                                    (byteAddWithCarry l5 r5 c4)
                                    (branch
                                      ByteAddResultValue
                                      s5
                                      c5
                                      .
                                      (eliminate
                                        ByteAddResult
                                        (lambda unrestricted current : (family ByteAddResult) .
                                        (family ModelWord64AddResult))
                                        (byteAddWithCarry l6 r6 c5)
                                        (branch
                                        ByteAddResultValue
                                        s6
                                        c6
                                        .
                                        (eliminate
                                        ByteAddResult
                                        (lambda unrestricted current : (family ByteAddResult) .
                                        (family ModelWord64AddResult))
                                        (byteAddWithCarry l7 r7 c6)
                                        (branch
                                        ByteAddResultValue
                                        s7
                                        c7
                                        .
                                        (constructor
                                        ModelWord64AddResult
                                        ModelWord64AddResultValue
                                        (constructor
                                        ModelWord64
                                        ModelWord64Value
                                        s0
                                        s1
                                        s2
                                        s3
                                        s4
                                        s5
                                        s6
                                        s7)
                                        c7)))))))))))))))))))))))

def modelWord64Add =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (eliminate
        ModelWord64AddResult
        (lambda unrestricted result : (family ModelWord64AddResult) . (family ModelWord64))
        (modelWord64AddWithCarry left right)
        (branch ModelWord64AddResultValue value carry . value))))

def modelWord64AddChecked =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (eliminate
        ModelWord64AddResult
        (lambda unrestricted result : (family ModelWord64AddResult) .
          (family ModelWord64CheckedResult))
        (modelWord64AddWithCarry left right)
        (branch
          ModelWord64AddResultValue
          value
          carry
          .
          (nat-eliminate
            (lambda unrestricted current : Nat . (family ModelWord64CheckedResult))
            (constructor ModelWord64CheckedResult ModelWord64CheckedSucceeded value)
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (family ModelWord64CheckedResult) .
                (constructor
                  ModelWord64CheckedResult
                  ModelWord64CheckedFailed
                  (constructor ModelWord64ArithmeticErrorCode ModelWord64AdditionOverflow))))
            carry)))))

def modelWord64Subtract =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (modelWord64Add left (modelWord64Add (modelWord64Complement right) modelWord64One))))

def modelWord64SubtractChecked =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family ModelWord64CheckedResult))
        (constructor
          ModelWord64CheckedResult
          ModelWord64CheckedSucceeded
          (modelWord64Subtract left right))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family ModelWord64CheckedResult) .
            (constructor
              ModelWord64CheckedResult
              ModelWord64CheckedFailed
              (constructor ModelWord64ArithmeticErrorCode ModelWord64SubtractionUnderflow))))
        (modelWord64LessThan left right))))

-- Delegates to the one owner (Std.Flag): this body is alpha-equivalent to
-- Std.Flag.inferenceFlagNot (binder renamed value<->flag, otherwise
-- identical) -- missed by `alpha-ast duplicates`' exact (binder-name-
-- sensitive) shape digest, found by manual inspection after that tool
-- grouped it with Std.Natural.naturalIsZero instead (also alpha-equivalent
-- to inferenceFlagNot, coincidentally under the same binder name "value").
def modelWord64FlagNot =
  inferenceFlagNot

-- Delegates to the one owner (Std.Flag), which this file already had a
-- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d).
def modelWord64FlagOr =
  inferenceFlagOr

def modelWord64NaturalOne =
  (succ zero)

def modelWord64NaturalSeven =
  (byte-to-nat (byte 7))

def modelWord64NaturalSixtyFour =
  (byte-to-nat (byte 64))

def modelWord64ShiftRightOne =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
      value
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (constructor
          ModelWord64
          ModelWord64Value
          (byteOr
            (byteShiftRight b0 modelWord64NaturalOne)
            (byteShiftLeftTruncated (byteAnd b1 (byte 1)) modelWord64NaturalSeven))
          (byteOr
            (byteShiftRight b1 modelWord64NaturalOne)
            (byteShiftLeftTruncated (byteAnd b2 (byte 1)) modelWord64NaturalSeven))
          (byteOr
            (byteShiftRight b2 modelWord64NaturalOne)
            (byteShiftLeftTruncated (byteAnd b3 (byte 1)) modelWord64NaturalSeven))
          (byteOr
            (byteShiftRight b3 modelWord64NaturalOne)
            (byteShiftLeftTruncated (byteAnd b4 (byte 1)) modelWord64NaturalSeven))
          (byteOr
            (byteShiftRight b4 modelWord64NaturalOne)
            (byteShiftLeftTruncated (byteAnd b5 (byte 1)) modelWord64NaturalSeven))
          (byteOr
            (byteShiftRight b5 modelWord64NaturalOne)
            (byteShiftLeftTruncated (byteAnd b6 (byte 1)) modelWord64NaturalSeven))
          (byteOr
            (byteShiftRight b6 modelWord64NaturalOne)
            (byteShiftLeftTruncated (byteAnd b7 (byte 1)) modelWord64NaturalSeven))
          (byteShiftRight b7 modelWord64NaturalOne)))))

def modelWord64ShiftLeftOne =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
      value
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (constructor
          ModelWord64
          ModelWord64Value
          (byteShiftLeftTruncated b0 modelWord64NaturalOne)
          (byteOr
            (byteShiftLeftTruncated b1 modelWord64NaturalOne)
            (byteShiftRight b0 modelWord64NaturalSeven))
          (byteOr
            (byteShiftLeftTruncated b2 modelWord64NaturalOne)
            (byteShiftRight b1 modelWord64NaturalSeven))
          (byteOr
            (byteShiftLeftTruncated b3 modelWord64NaturalOne)
            (byteShiftRight b2 modelWord64NaturalSeven))
          (byteOr
            (byteShiftLeftTruncated b4 modelWord64NaturalOne)
            (byteShiftRight b3 modelWord64NaturalSeven))
          (byteOr
            (byteShiftLeftTruncated b5 modelWord64NaturalOne)
            (byteShiftRight b4 modelWord64NaturalSeven))
          (byteOr
            (byteShiftLeftTruncated b6 modelWord64NaturalOne)
            (byteShiftRight b5 modelWord64NaturalSeven))
          (byteOr
            (byteShiftLeftTruncated b7 modelWord64NaturalOne)
            (byteShiftRight b6 modelWord64NaturalSeven))))))

def modelWord64LeastBit =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . Nat)
      value
      (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (byte-to-nat (byteAnd b0 (byte 1))))))

def modelWord64HighBit =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . Nat)
      value
      (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (byte-less-than (byte 127) b7))))

def modelWord64MultiplyStep =
  (lambda unrestricted state : (family ModelWord64MultiplyState) .
    (eliminate
      ModelWord64MultiplyState
      (lambda unrestricted current : (family ModelWord64MultiplyState) .
        (family ModelWord64MultiplyState))
      state
      (branch
        ModelWord64MultiplyStateValue
        multiplicand
        multiplier
        product
        overflow
        .
        (app
          (lambda unrestricted leastBit : Nat .
            (app
              (lambda unrestricted nextMultiplier : (family ModelWord64) .
                (eliminate
                  ModelWord64AddResult
                  (lambda unrestricted result : (family ModelWord64AddResult) .
                    (family ModelWord64MultiplyState))
                  (modelWord64AddWithCarry product multiplicand)
                  (branch
                    ModelWord64AddResultValue
                    sum
                    carry
                    .
                    (constructor
                      ModelWord64MultiplyState
                      ModelWord64MultiplyStateValue
                      (modelWord64ShiftLeftOne multiplicand)
                      nextMultiplier
                      (modelWord64Select leastBit sum product)
                      (modelWord64FlagOr
                        overflow
                        (modelWord64FlagOr
                          (modelWord64FlagAnd leastBit carry)
                          (modelWord64FlagAnd
                            (modelWord64HighBit multiplicand)
                            (modelWord64FlagNot (modelWord64IsZero nextMultiplier)))))))))
              (modelWord64ShiftRightOne multiplier)))
          (modelWord64LeastBit multiplier)))))

def modelWord64MultiplyStateRun =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family ModelWord64MultiplyState))
        (constructor
          ModelWord64MultiplyState
          ModelWord64MultiplyStateValue
          left
          right
          modelWord64Zero
          zero)
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family ModelWord64MultiplyState) .
            (modelWord64MultiplyStep induction)))
        modelWord64NaturalSixtyFour)))

def modelWord64MultiplyChecked =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (eliminate
        ModelWord64MultiplyState
        (lambda unrestricted current : (family ModelWord64MultiplyState) .
          (family ModelWord64MultiplyCheckedResult))
        (modelWord64MultiplyStateRun left right)
        (branch
          ModelWord64MultiplyStateValue
          multiplicand
          multiplier
          product
          overflow
          .
          (nat-eliminate
            (lambda unrestricted current : Nat . (family ModelWord64MultiplyCheckedResult))
            (constructor ModelWord64MultiplyCheckedResult ModelWord64MultiplySucceeded product)
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (family ModelWord64MultiplyCheckedResult) .
                (constructor ModelWord64MultiplyCheckedResult ModelWord64MultiplyOverflow)))
            overflow)))))

def modelWord64FromNaturalTruncated =
  (lambda unrestricted value : Nat .
    (app
      (lambda unrestricted quotient1 : Nat .
        (app
          (lambda unrestricted quotient2 : Nat .
            (app
              (lambda unrestricted quotient3 : Nat .
                (app
                  (lambda unrestricted quotient4 : Nat .
                    (app
                      (lambda unrestricted quotient5 : Nat .
                        (app
                          (lambda unrestricted quotient6 : Nat .
                            (app
                              (lambda unrestricted quotient7 : Nat .
                                (constructor
                                  ModelWord64
                                  ModelWord64Value
                                  (nat-to-byte
                                    (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
                                  (nat-to-byte
                                    (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
                                  (nat-to-byte
                                    (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
                                  (nat-to-byte
                                    (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))
                                  (nat-to-byte
                                    (naturalModuloUnchecked quotient4 byteNaturalTwoHundredFiftySix))
                                  (nat-to-byte
                                    (naturalModuloUnchecked quotient5 byteNaturalTwoHundredFiftySix))
                                  (nat-to-byte
                                    (naturalModuloUnchecked quotient6 byteNaturalTwoHundredFiftySix))
                                  (nat-to-byte
                                    (naturalModuloUnchecked quotient7 byteNaturalTwoHundredFiftySix))))
                              (naturalDivideUnchecked quotient6 byteNaturalTwoHundredFiftySix)))
                          (naturalDivideUnchecked quotient5 byteNaturalTwoHundredFiftySix)))
                      (naturalDivideUnchecked quotient4 byteNaturalTwoHundredFiftySix)))
                  (naturalDivideUnchecked quotient3 byteNaturalTwoHundredFiftySix)))
              (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
          (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
      (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)))

-- the natural a word holds (its bytes little-endian); below 2^64, so it is
-- a word of the build's naturals too
def modelWord64Natural =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . Nat)
      value
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (naturalAdd
          (byte-to-nat b0)
          (naturalMultiply
            256
            (naturalAdd
              (byte-to-nat b1)
              (naturalMultiply
                256
                (naturalAdd
                  (byte-to-nat b2)
                  (naturalMultiply
                    256
                    (naturalAdd
                      (byte-to-nat b3)
                      (naturalMultiply
                        256
                        (naturalAdd
                          (byte-to-nat b4)
                          (naturalMultiply
                            256
                            (naturalAdd
                              (byte-to-nat b5)
                              (naturalMultiply
                                256
                                (naturalAdd (byte-to-nat b6) (naturalMultiply 256 (byte-to-nat b7))))))))))))))))))