module Data.SHA256Core

import Data.SHA256
import Model.Config
import Model.Word32
import Model.Word32Logic

family SHA256RoundTelemetry : Type 0
constructor SHA256RoundTelemetryValue
field unrestricted sha256RoundTelemetryIndex : (family ModelWord32)
field unrestricted sha256RoundTelemetryRotateCount : Nat
field unrestricted sha256RoundTelemetryShiftCount : Nat
field unrestricted sha256RoundTelemetryBooleanCount : Nat
field unrestricted sha256RoundTelemetryAddCount : Nat

end-family

family SHA256RoundOutput : Type 0
constructor SHA256RoundOutputValue
field unrestricted sha256RoundOutputState : (family SHA256State)
field unrestricted sha256RoundOutputTelemetry : (family SHA256RoundTelemetry)

end-family

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

def sha256BigSigma0 =
  (lambda unrestricted value : (family ModelWord32) .
    (sha256XorThree
      (modelWord32RotateRight value (byte-to-nat (byte 2)))
      (modelWord32RotateRight value (byte-to-nat (byte 13)))
      (modelWord32RotateRight value (byte-to-nat (byte 22)))))

def sha256BigSigma1 =
  (lambda unrestricted value : (family ModelWord32) .
    (sha256XorThree
      (modelWord32RotateRight value (byte-to-nat (byte 6)))
      (modelWord32RotateRight value (byte-to-nat (byte 11)))
      (modelWord32RotateRight value (byte-to-nat (byte 25)))))

def sha256SmallSigma0 =
  (lambda unrestricted value : (family ModelWord32) .
    (sha256XorThree
      (modelWord32RotateRight value (byte-to-nat (byte 7)))
      (modelWord32RotateRight value (byte-to-nat (byte 18)))
      (modelWord32ShiftRight value (byte-to-nat (byte 3)))))

def sha256SmallSigma1 =
  (lambda unrestricted value : (family ModelWord32) .
    (sha256XorThree
      (modelWord32RotateRight value (byte-to-nat (byte 17)))
      (modelWord32RotateRight value (byte-to-nat (byte 19)))
      (modelWord32ShiftRight value (byte-to-nat (byte 10)))))

def sha256RoundState =
  (lambda unrestricted roundConstant : (family ModelWord32) .
    (lambda unrestricted scheduleWord : (family ModelWord32) .
      (lambda unrestricted state : (family SHA256State) .
        (eliminate
          SHA256State
          (lambda unrestricted current : (family SHA256State) . (family SHA256State))
          state
          (branch
            SHA256StateValue
            a
            b
            c
            d
            e
            f
            g
            h
            .
            (app
              (lambda unrestricted sigma1 : (family ModelWord32) .
                (app
                  (lambda unrestricted choose : (family ModelWord32) .
                    (app
                      (lambda unrestricted temp1 : (family ModelWord32) .
                        (app
                          (lambda unrestricted sigma0 : (family ModelWord32) .
                            (app
                              (lambda unrestricted majority : (family ModelWord32) .
                                (app
                                  (lambda unrestricted temp2 : (family ModelWord32) .
                                    (constructor
                                      SHA256State
                                      SHA256StateValue
                                      (modelWord32Add temp1 temp2)
                                      a
                                      b
                                      c
                                      (modelWord32Add d temp1)
                                      e
                                      f
                                      g))
                                  (modelWord32Add sigma0 majority)))
                              (modelWord32Majority a b c)))
                          (sha256BigSigma0 a)))
                      (modelWord32AddFive h sigma1 choose roundConstant scheduleWord)))
                  (modelWord32Choose e f g)))
              (sha256BigSigma1 e)))))))

def sha256Round =
  (lambda unrestricted input : (family SHA256RoundInput) .
    (eliminate
      SHA256RoundInput
      (lambda unrestricted current : (family SHA256RoundInput) . (family SHA256RoundOutput))
      input
      (branch
        SHA256RoundInputValue
        index
        constant
        schedule
        a
        b
        c
        d
        e
        f
        g
        h
        .
        (constructor
          SHA256RoundOutput
          SHA256RoundOutputValue
          (sha256RoundState
            constant
            schedule
            (constructor SHA256State SHA256StateValue a b c d e f g h))
          (constructor
            SHA256RoundTelemetry
            SHA256RoundTelemetryValue
            index
            (byte-to-nat (byte 6))
            zero
            (byte-to-nat (byte 2))
            (byte-to-nat (byte 7)))))))