module Model.Word32Logic

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

def modelWord32And =
  (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
                (byteAnd l0 r0)
                (byteAnd l1 r1)
                (byteAnd l2 r2)
                (byteAnd l3 r3))))))))

def modelWord32Or =
  (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
                (byteOr l0 r0)
                (byteOr l1 r1)
                (byteOr l2 r2)
                (byteOr l3 r3))))))))

def modelWord32Not =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
      value
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (constructor
          ModelWord32
          ModelWord32Value
          (byteXor b0 (byte 255))
          (byteXor b1 (byte 255))
          (byteXor b2 (byte 255))
          (byteXor b3 (byte 255))))))

def modelWord32RotateRight =
  (lambda unrestricted value : (family ModelWord32) .
    (lambda unrestricted amount : Nat .
      (app
        (lambda unrestricted normalized : Nat .
          (modelWord32Or
            (modelWord32ShiftRight value normalized)
            (modelWord32ShiftLeft
              value
              (naturalSaturatingSubtract modelWord32NaturalThirtyTwo normalized))))
        (naturalModuloUnchecked amount modelWord32NaturalThirtyTwo))))

def modelWord32Choose =
  (lambda unrestricted choose : (family ModelWord32) .
    (lambda unrestricted whenSet : (family ModelWord32) .
      (lambda unrestricted whenClear : (family ModelWord32) .
        (modelWord32Xor
          (modelWord32And choose whenSet)
          (modelWord32And (modelWord32Not choose) whenClear)))))

def modelWord32Majority =
  (lambda unrestricted first : (family ModelWord32) .
    (lambda unrestricted second : (family ModelWord32) .
      (lambda unrestricted third : (family ModelWord32) .
        (modelWord32Xor
          (modelWord32Xor (modelWord32And first second) (modelWord32And first third))
          (modelWord32And second third)))))

def modelWord32AddThree =
  (lambda unrestricted first : (family ModelWord32) .
    (lambda unrestricted second : (family ModelWord32) .
      (lambda unrestricted third : (family ModelWord32) .
        (modelWord32Add (modelWord32Add first second) third))))

def modelWord32AddFour =
  (lambda unrestricted first : (family ModelWord32) .
    (lambda unrestricted second : (family ModelWord32) .
      (lambda unrestricted third : (family ModelWord32) .
        (lambda unrestricted fourth : (family ModelWord32) .
          (modelWord32Add (modelWord32AddThree first second third) fourth)))))

def modelWord32AddFive =
  (lambda unrestricted first : (family ModelWord32) .
    (lambda unrestricted second : (family ModelWord32) .
      (lambda unrestricted third : (family ModelWord32) .
        (lambda unrestricted fourth : (family ModelWord32) .
          (lambda unrestricted fifth : (family ModelWord32) .
            (modelWord32Add (modelWord32AddFour first second third fourth) fifth))))))