module Data.SHA256Compress

import Data.SHA256
import Data.SHA256Constants
import Data.SHA256Core
import Data.SHA256Schedule
import Data.SHA256ScheduleExpand
import Model.Config
import Model.Word32
import Std.Natural

family SHA256CompressionRoundState : Type 0
constructor SHA256CompressionRoundStateValue
field unrestricted sha256CompressionWorkingState : (family SHA256State)
field unrestricted sha256CompressionRoundIndex : Nat
field unrestricted sha256CompressionRotateCount : Nat
field unrestricted sha256CompressionShiftCount : Nat
field unrestricted sha256CompressionBooleanCount : Nat
field unrestricted sha256CompressionAddCount : Nat

end-family

family SHA256CompressionRoundsResult : Type 0
constructor SHA256CompressionRoundsSucceeded
field unrestricted sha256CompressionRoundsState : (family SHA256CompressionRoundState)
constructor SHA256CompressionRoundsFailed
field unrestricted sha256CompressionRoundsError : (family SHA256ErrorCode)
field unrestricted sha256CompressionRoundsFailureIndex : Nat

end-family

family SHA256CompressionTelemetry : Type 0
constructor SHA256CompressionTelemetryValue
field unrestricted sha256CompressionTelemetryDecodedWords : Nat
field unrestricted sha256CompressionTelemetryExpandedWords : Nat
field unrestricted sha256CompressionTelemetryRounds : Nat
field unrestricted sha256CompressionTelemetryLookups : Nat
field unrestricted sha256CompressionTelemetrySigmas : Nat
field unrestricted sha256CompressionTelemetryRotates : Nat
field unrestricted sha256CompressionTelemetryShifts : Nat
field unrestricted sha256CompressionTelemetryBooleans : Nat
field unrestricted sha256CompressionTelemetryAdds : Nat

end-family

family SHA256CompressionResult : Type 0
constructor SHA256CompressionSucceeded
field unrestricted sha256CompressionResultState : (family SHA256State)
field unrestricted sha256CompressionResultTelemetry : (family SHA256CompressionTelemetry)
constructor SHA256CompressionFailed
field unrestricted sha256CompressionError : (family SHA256ErrorCode)
field unrestricted sha256CompressionFailureIndex : Nat

end-family

def sha256StateAdd =
  (lambda unrestricted left : (family SHA256State) .
    (lambda unrestricted right : (family SHA256State) .
      (eliminate
        SHA256State
        (lambda unrestricted current : (family SHA256State) . (family SHA256State))
        left
        (branch
          SHA256StateValue
          l0
          l1
          l2
          l3
          l4
          l5
          l6
          l7
          .
          (eliminate
            SHA256State
            (lambda unrestricted current : (family SHA256State) . (family SHA256State))
            right
            (branch
              SHA256StateValue
              r0
              r1
              r2
              r3
              r4
              r5
              r6
              r7
              .
              (constructor
                SHA256State
                SHA256StateValue
                (modelWord32Add l0 r0)
                (modelWord32Add l1 r1)
                (modelWord32Add l2 r2)
                (modelWord32Add l3 r3)
                (modelWord32Add l4 r4)
                (modelWord32Add l5 r5)
                (modelWord32Add l6 r6)
                (modelWord32Add l7 r7))))))))

def sha256CompressionRounds =
  (lambda unrestricted schedule : (family SHA256Schedule) .
    (eliminate
      SHA256Schedule
      (lambda unrestricted current : (family SHA256Schedule) .
        (pi unrestricted constants : (family SHA256Schedule) .
          (pi unrestricted roundState : (family SHA256CompressionRoundState) .
            (family SHA256CompressionRoundsResult))))
      schedule
      (branch
        SHA256ScheduleEnd
        .
        (lambda unrestricted constants : (family SHA256Schedule) .
          (lambda unrestricted roundState : (family SHA256CompressionRoundState) .
            (eliminate
              SHA256Schedule
              (lambda unrestricted current : (family SHA256Schedule) .
                (family SHA256CompressionRoundsResult))
              constants
              (branch
                SHA256ScheduleEnd
                .
                (eliminate
                  SHA256CompressionRoundState
                  (lambda unrestricted current : (family SHA256CompressionRoundState) .
                    (family SHA256CompressionRoundsResult))
                  roundState
                  (branch
                    SHA256CompressionRoundStateValue
                    state
                    index
                    rotates
                    shifts
                    booleans
                    adds
                    .
                    (nat-eliminate
                      (lambda unrestricted validCount : Nat .
                        (family SHA256CompressionRoundsResult))
                      (constructor
                        SHA256CompressionRoundsResult
                        SHA256CompressionRoundsFailed
                        (constructor SHA256ErrorCode SHA256RoundCountInvalid)
                        index)
                      (lambda unrestricted predecessor : Nat .
                        (lambda unrestricted induction : (family SHA256CompressionRoundsResult) .
                          (constructor
                            SHA256CompressionRoundsResult
                            SHA256CompressionRoundsSucceeded
                            roundState)))
                      (naturalEqual index sha256NaturalSixtyFour)))))
              (branch
                SHA256ScheduleNext
                constant
                tail
                induction
                .
                (eliminate
                  SHA256CompressionRoundState
                  (lambda unrestricted current : (family SHA256CompressionRoundState) .
                    (family SHA256CompressionRoundsResult))
                  roundState
                  (branch
                    SHA256CompressionRoundStateValue
                    state
                    index
                    rotates
                    shifts
                    booleans
                    adds
                    .
                    (constructor
                      SHA256CompressionRoundsResult
                      SHA256CompressionRoundsFailed
                      (constructor SHA256ErrorCode SHA256RoundCountInvalid)
                      index))))))))
      (branch
        SHA256ScheduleNext
        scheduleWord
        scheduleTail
        induction
        .
        (lambda unrestricted constants : (family SHA256Schedule) .
          (lambda unrestricted roundState : (family SHA256CompressionRoundState) .
            (eliminate
              SHA256Schedule
              (lambda unrestricted current : (family SHA256Schedule) .
                (family SHA256CompressionRoundsResult))
              constants
              (branch
                SHA256ScheduleEnd
                .
                (eliminate
                  SHA256CompressionRoundState
                  (lambda unrestricted current : (family SHA256CompressionRoundState) .
                    (family SHA256CompressionRoundsResult))
                  roundState
                  (branch
                    SHA256CompressionRoundStateValue
                    state
                    index
                    rotates
                    shifts
                    booleans
                    adds
                    .
                    (constructor
                      SHA256CompressionRoundsResult
                      SHA256CompressionRoundsFailed
                      (constructor SHA256ErrorCode SHA256RoundCountInvalid)
                      index))))
              (branch
                SHA256ScheduleNext
                constant
                constantTail
                constantInduction
                .
                (eliminate
                  SHA256CompressionRoundState
                  (lambda unrestricted current : (family SHA256CompressionRoundState) .
                    (family SHA256CompressionRoundsResult))
                  roundState
                  (branch
                    SHA256CompressionRoundStateValue
                    state
                    index
                    rotates
                    shifts
                    booleans
                    adds
                    .
                    (induction
                      constantTail
                      (constructor
                        SHA256CompressionRoundState
                        SHA256CompressionRoundStateValue
                        (sha256RoundState constant scheduleWord state)
                        (succ index)
                        (naturalAdd (byte-to-nat (byte 6)) rotates)
                        shifts
                        (naturalAdd (byte-to-nat (byte 2)) booleans)
                        (naturalAdd (byte-to-nat (byte 7)) adds))))))))))))

def sha256CompressExpandedSchedule =
  (lambda unrestricted initialState : (family SHA256State) .
    (lambda unrestricted expandedSchedule : (family SHA256Schedule) .
      (lambda unrestricted expansionTelemetry : (family SHA256ScheduleExpansionTelemetry) .
        (eliminate
          SHA256CompressionRoundsResult
          (lambda unrestricted current : (family SHA256CompressionRoundsResult) .
            (family SHA256CompressionResult))
          (sha256CompressionRounds
            expandedSchedule
            sha256RoundConstants
            (constructor
              SHA256CompressionRoundState
              SHA256CompressionRoundStateValue
              initialState
              zero
              zero
              zero
              zero
              zero))
          (branch
            SHA256CompressionRoundsSucceeded
            roundState
            .
            (eliminate
              SHA256CompressionRoundState
              (lambda unrestricted current : (family SHA256CompressionRoundState) .
                (family SHA256CompressionResult))
              roundState
              (branch
                SHA256CompressionRoundStateValue
                workingState
                rounds
                rotates
                shifts
                booleans
                adds
                .
                (eliminate
                  SHA256ScheduleExpansionTelemetry
                  (lambda unrestricted current : (family SHA256ScheduleExpansionTelemetry) .
                    (family SHA256CompressionResult))
                  expansionTelemetry
                  (branch
                    SHA256ScheduleExpansionTelemetryValue
                    generated
                    lookups
                    sigmas
                    expansionRotates
                    expansionShifts
                    expansionAdds
                    .
                    (constructor
                      SHA256CompressionResult
                      SHA256CompressionSucceeded
                      (sha256StateAdd initialState workingState)
                      (constructor
                        SHA256CompressionTelemetry
                        SHA256CompressionTelemetryValue
                        sha256NaturalSixteen
                        generated
                        rounds
                        lookups
                        sigmas
                        (naturalAdd expansionRotates rotates)
                        (naturalAdd expansionShifts shifts)
                        booleans
                        (naturalAdd (byte-to-nat (byte 8)) (naturalAdd expansionAdds adds)))))))))
          (branch
            SHA256CompressionRoundsFailed
            error
            failedIndex
            .
            (constructor SHA256CompressionResult SHA256CompressionFailed error failedIndex))))))

def sha256CompressBlock =
  (lambda unrestricted initialState : (family SHA256State) .
    (lambda unrestricted block : Bytes .
      (eliminate
        SHA256BlockDecodeResult
        (lambda unrestricted current : (family SHA256BlockDecodeResult) .
          (family SHA256CompressionResult))
        (sha256DecodeBlockWords block)
        (branch
          SHA256BlockDecodeSucceeded
          initialSchedule
          decodedCount
          .
          (eliminate
            SHA256ScheduleExpansionResult
            (lambda unrestricted current : (family SHA256ScheduleExpansionResult) .
              (family SHA256CompressionResult))
            (sha256ExpandSchedule initialSchedule)
            (branch
              SHA256ScheduleExpansionSucceeded
              expandedSchedule
              telemetry
              .
              (sha256CompressExpandedSchedule initialState expandedSchedule telemetry))
            (branch
              SHA256ScheduleExpansionFailed
              error
              failedIndex
              .
              (constructor SHA256CompressionResult SHA256CompressionFailed error failedIndex))))
        (branch
          SHA256BlockDecodeFailed
          error
          failedOrdinal
          .
          (constructor SHA256CompressionResult SHA256CompressionFailed error failedOrdinal)))))