module Model.Word32

import Model.Config
import Std.Byte
import Std.Natural

family ModelWord32ArithmeticErrorCode : Type 0
constructor ModelWord32ModuloByZero

end-family

family ModelWord32ModuloResult : Type 0
constructor ModelWord32ModuloSucceeded
field unrestricted modelWord32ModuloValue : Nat
constructor ModelWord32ModuloFailed
field unrestricted modelWord32ModuloError : (family ModelWord32ArithmeticErrorCode)

end-family

family ModelWord32MultiplyState : Type 0
constructor ModelWord32MultiplyStateValue
field unrestricted modelWord32MultiplyMultiplicand : (family ModelWord32)
field unrestricted modelWord32MultiplyMultiplier : (family ModelWord32)
field unrestricted modelWord32MultiplyProduct : (family ModelWord32)

end-family

def modelWord32ArithmeticErrorCodeBytes =
  (lambda unrestricted code : (family ModelWord32ArithmeticErrorCode) .
    (eliminate
      ModelWord32ArithmeticErrorCode
      (lambda unrestricted current : (family ModelWord32ArithmeticErrorCode) . Bytes)
      code
      (branch ModelWord32ModuloByZero . b"ALPHA-MODEL-001")))

def modelWord32Zero =
  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 0))

def modelWord32NaturalOne =
  (succ zero)

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

def modelWord32NaturalThirtyTwo =
  (byte-to-nat (byte 32))

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

def modelWord32Xor =
  (lambda unrestricted left : (family ModelWord32) .
    (lambda unrestricted right : (family ModelWord32) .
      (eliminate
        ModelWord32
        (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
        left
        (branch
          ModelWord32Value
          l0
          l1
          l2
          l3
          .
          (eliminate
            ModelWord32
            (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
            right
            (branch
              ModelWord32Value
              r0
              r1
              r2
              r3
              .
              (constructor
                ModelWord32
                ModelWord32Value
                (byteXor l0 r0)
                (byteXor l1 r1)
                (byteXor l2 r2)
                (byteXor l3 r3))))))))

def modelWord32Add =
  (lambda unrestricted left : (family ModelWord32) .
    (lambda unrestricted right : (family ModelWord32) .
      (eliminate
        ModelWord32
        (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
        left
        (branch
          ModelWord32Value
          l0
          l1
          l2
          l3
          .
          (eliminate
            ModelWord32
            (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
            right
            (branch
              ModelWord32Value
              r0
              r1
              r2
              r3
              .
              (eliminate
                ByteAddResult
                (lambda unrestricted current : (family ByteAddResult) . (family ModelWord32))
                (byteAddWithCarry l0 r0 zero)
                (branch
                  ByteAddResultValue
                  sum0
                  carry0
                  .
                  (eliminate
                    ByteAddResult
                    (lambda unrestricted current : (family ByteAddResult) . (family ModelWord32))
                    (byteAddWithCarry l1 r1 carry0)
                    (branch
                      ByteAddResultValue
                      sum1
                      carry1
                      .
                      (eliminate
                        ByteAddResult
                        (lambda unrestricted current : (family ByteAddResult) .
                          (family ModelWord32))
                        (byteAddWithCarry l2 r2 carry1)
                        (branch
                          ByteAddResultValue
                          sum2
                          carry2
                          .
                          (eliminate
                            ByteAddResult
                            (lambda unrestricted current : (family ByteAddResult) .
                              (family ModelWord32))
                            (byteAddWithCarry l3 r3 carry2)
                            (branch
                              ByteAddResultValue
                              sum3
                              carry3
                              .
                              (constructor ModelWord32 ModelWord32Value sum0 sum1 sum2 sum3)))))))))))))))

def modelWord32ShiftRightOne =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
      value
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (constructor
          ModelWord32
          ModelWord32Value
          (byteOr
            (byteShiftRight b0 modelWord32NaturalOne)
            (byteShiftLeftTruncated (byteAnd b1 (byte 1)) modelWord32NaturalSeven))
          (byteOr
            (byteShiftRight b1 modelWord32NaturalOne)
            (byteShiftLeftTruncated (byteAnd b2 (byte 1)) modelWord32NaturalSeven))
          (byteOr
            (byteShiftRight b2 modelWord32NaturalOne)
            (byteShiftLeftTruncated (byteAnd b3 (byte 1)) modelWord32NaturalSeven))
          (byteShiftRight b3 modelWord32NaturalOne)))))

def modelWord32ShiftLeftOne =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
      value
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (constructor
          ModelWord32
          ModelWord32Value
          (byteShiftLeftTruncated b0 modelWord32NaturalOne)
          (byteOr
            (byteShiftLeftTruncated b1 modelWord32NaturalOne)
            (byteShiftRight b0 modelWord32NaturalSeven))
          (byteOr
            (byteShiftLeftTruncated b2 modelWord32NaturalOne)
            (byteShiftRight b1 modelWord32NaturalSeven))
          (byteOr
            (byteShiftLeftTruncated b3 modelWord32NaturalOne)
            (byteShiftRight b2 modelWord32NaturalSeven))))))

def modelWord32ShiftRight =
  (lambda unrestricted value : (family ModelWord32) .
    (lambda unrestricted amount : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family ModelWord32))
        value
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family ModelWord32) .
            (modelWord32ShiftRightOne induction)))
        amount)))

def modelWord32ShiftLeft =
  (lambda unrestricted value : (family ModelWord32) .
    (lambda unrestricted amount : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family ModelWord32))
        value
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family ModelWord32) .
            (modelWord32ShiftLeftOne induction)))
        amount)))

def modelWord32LeastBit =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . Nat)
      value
      (branch ModelWord32Value b0 b1 b2 b3 . (byte-to-nat (byteAnd b0 (byte 1))))))

def modelWord32MultiplyStep =
  (lambda unrestricted state : (family ModelWord32MultiplyState) .
    (eliminate
      ModelWord32MultiplyState
      (lambda unrestricted current : (family ModelWord32MultiplyState) .
        (family ModelWord32MultiplyState))
      state
      (branch
        ModelWord32MultiplyStateValue
        multiplicand
        multiplier
        product
        .
        (constructor
          ModelWord32MultiplyState
          ModelWord32MultiplyStateValue
          (modelWord32ShiftLeftOne multiplicand)
          (modelWord32ShiftRightOne multiplier)
          (modelWord32Select
            (modelWord32LeastBit multiplier)
            (modelWord32Add product multiplicand)
            product)))))

def modelWord32MultiplyStateRun =
  (lambda unrestricted left : (family ModelWord32) .
    (lambda unrestricted right : (family ModelWord32) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family ModelWord32MultiplyState))
        (constructor
          ModelWord32MultiplyState
          ModelWord32MultiplyStateValue
          left
          right
          modelWord32Zero)
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family ModelWord32MultiplyState) .
            (modelWord32MultiplyStep induction)))
        modelWord32NaturalThirtyTwo)))

def modelWord32Multiply =
  (lambda unrestricted left : (family ModelWord32) .
    (lambda unrestricted right : (family ModelWord32) .
      (eliminate
        ModelWord32MultiplyState
        (lambda unrestricted current : (family ModelWord32MultiplyState) . (family ModelWord32))
        (modelWord32MultiplyStateRun left right)
        (branch ModelWord32MultiplyStateValue multiplicand multiplier product . product))))

def modelWord32ModuloStep =
  (lambda unrestricted remainder : Nat .
    (lambda unrestricted value : Byte .
      (lambda unrestricted divisor : Nat .
        (naturalModuloUnchecked
          (naturalAdd (naturalMultiply remainder byteNaturalTwoHundredFiftySix) (byte-to-nat value))
          divisor))))

def modelWord32ModuloUnchecked =
  (lambda unrestricted value : (family ModelWord32) .
    (lambda unrestricted divisor : Nat .
      (eliminate
        ModelWord32
        (lambda unrestricted current : (family ModelWord32) . Nat)
        value
        (branch
          ModelWord32Value
          b0
          b1
          b2
          b3
          .
          (modelWord32ModuloStep
            (modelWord32ModuloStep
              (modelWord32ModuloStep (modelWord32ModuloStep zero b3 divisor) b2 divisor)
              b1
              divisor)
            b0
            divisor)))))

def modelWord32Modulo =
  (lambda unrestricted value : (family ModelWord32) .
    (lambda unrestricted divisor : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family ModelWord32ModuloResult))
        (constructor
          ModelWord32ModuloResult
          ModelWord32ModuloFailed
          (constructor ModelWord32ArithmeticErrorCode ModelWord32ModuloByZero))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family ModelWord32ModuloResult) .
            (constructor
              ModelWord32ModuloResult
              ModelWord32ModuloSucceeded
              (modelWord32ModuloUnchecked value divisor))))
        divisor)))

def modelWord32ToNatural =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . Nat)
      value
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (naturalAdd
          (byte-to-nat b0)
          (naturalMultiply
            byteNaturalTwoHundredFiftySix
            (naturalAdd
              (byte-to-nat b1)
              (naturalMultiply
                byteNaturalTwoHundredFiftySix
                (naturalAdd
                  (byte-to-nat b2)
                  (naturalMultiply byteNaturalTwoHundredFiftySix (byte-to-nat b3))))))))))

-- General path: four divisions by 256 (a fold over the value each). Reached
-- only for values of 256 and above; `modelWord32FromNaturalTruncated` takes
-- the O(1) byte path below that (D17).
def modelWord32FromNaturalDivided =
  (lambda unrestricted value : Nat .
    (app
      (lambda unrestricted quotient1 : Nat .
        (app
          (lambda unrestricted quotient2 : Nat .
            (app
              (lambda unrestricted quotient3 : Nat .
                (constructor
                  ModelWord32
                  ModelWord32Value
                  (nat-to-byte (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
                  (nat-to-byte (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
                  (nat-to-byte (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
                  (nat-to-byte (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))))
              (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
          (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
      (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)))

def modelWord32FromNaturalTruncated =
  (lambda unrestricted value : Nat .
    (app
      (nat-eliminate
        (lambda unrestricted small : Nat . (pi unrestricted unit : Nat . (family ModelWord32)))
        (lambda unrestricted unit : Nat . (modelWord32FromNaturalDivided value))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (pi unrestricted unit : Nat . (family ModelWord32)) .
            (lambda unrestricted unit : Nat .
              (constructor
                ModelWord32
                ModelWord32Value
                (nat-to-byte value)
                (byte 0)
                (byte 0)
                (byte 0)))))
        (nat-less-than value byteNaturalTwoHundredFiftySix))
      zero))

-- Successor modulo 2^32: one carry chain, no fold over the value (D17).
def modelWord32Increment =
  (lambda unrestricted value : (family ModelWord32) . (modelWord32Add value modelWord32One))

-- Order one byte position: 1 when left is below right, 0 when above, and the
-- lower positions' verdict when equal (most significant position outermost).
def modelWord32OrderByte =
  (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)))))

-- Unsigned order in four byte comparisons (D17).
def modelWord32LessThan =
  (lambda unrestricted left : (family ModelWord32) .
    (lambda unrestricted right : (family ModelWord32) .
      (eliminate
        ModelWord32
        (lambda unrestricted current : (family ModelWord32) . Nat)
        left
        (branch
          ModelWord32Value
          l0
          l1
          l2
          l3
          .
          (eliminate
            ModelWord32
            (lambda unrestricted current : (family ModelWord32) . Nat)
            right
            (branch
              ModelWord32Value
              r0
              r1
              r2
              r3
              .
              (modelWord32OrderByte
                l3
                r3
                (modelWord32OrderByte
                  l2
                  r2
                  (modelWord32OrderByte l1 r1 (modelWord32OrderByte l0 r0 zero))))))))))

def modelWord32Equal =
  (lambda unrestricted left : (family ModelWord32) .
    (lambda unrestricted right : (family ModelWord32) .
      (naturalAnd
        (naturalIsZero (modelWord32LessThan left right))
        (naturalIsZero (modelWord32LessThan right left)))))

-- value × 10 = (value << 3) + (value << 1), modulo 2^32.
def modelWord32TimesTen =
  (lambda unrestricted value : (family ModelWord32) .
    (modelWord32Add
      (modelWord32ShiftLeftOne (modelWord32ShiftLeftOne (modelWord32ShiftLeftOne value)))
      (modelWord32ShiftLeftOne value)))

-- The value of one ASCII decimal digit byte (0x30..0x39) as a word.
def modelWord32DecimalDigit =
  (lambda unrestricted digit : Byte .
    (constructor ModelWord32 ModelWord32Value (byteAnd digit (byte 15)) (byte 0) (byte 0) (byte 0)))

-- Decimal digit bytes, most significant first, to a word modulo 2^32; one
-- step per digit. Callers check the bytes are digits and the value fits.
def modelWord32FromDecimalDigitsTruncated =
  (lambda unrestricted digits : Bytes .
    (app
      (bytes-eliminate
        (lambda unrestricted current : Bytes .
          (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)))
        (lambda unrestricted accumulator : (family ModelWord32) . accumulator)
        (lambda unrestricted head : Byte .
          (lambda unrestricted tail : Bytes .
            (lambda unrestricted induction : (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)) .
              (lambda unrestricted accumulator : (family ModelWord32) .
                (induction
                  (modelWord32Add (modelWord32TimesTen accumulator) (modelWord32DecimalDigit head)))))))
        digits)
      modelWord32Zero))