Data.SHA256Core

1module Data.SHA256Core
2
3import Data.SHA256
4import Model.Config
5import Model.Word32
6import Model.Word32Logic
7
8family SHA256RoundTelemetry : Type 0
9constructor SHA256RoundTelemetryValue
10field unrestricted sha256RoundTelemetryIndex : (family ModelWord32)
11field unrestricted sha256RoundTelemetryRotateCount : Nat
12field unrestricted sha256RoundTelemetryShiftCount : Nat
13field unrestricted sha256RoundTelemetryBooleanCount : Nat
14field unrestricted sha256RoundTelemetryAddCount : Nat
15
16end-family
17
18family SHA256RoundOutput : Type 0
19constructor SHA256RoundOutputValue
20field unrestricted sha256RoundOutputState : (family SHA256State)
21field unrestricted sha256RoundOutputTelemetry : (family SHA256RoundTelemetry)
22
23end-family
24
25def sha256XorThree =
26  (lambda unrestricted first : (family ModelWord32) .
27    (lambda unrestricted second : (family ModelWord32) .
28      (lambda unrestricted third : (family ModelWord32) .
29        (modelWord32Xor (modelWord32Xor first second) third))))
30
31def sha256BigSigma0 =
32  (lambda unrestricted value : (family ModelWord32) .
33    (sha256XorThree
34      (modelWord32RotateRight value (byte-to-nat (byte 2)))
35      (modelWord32RotateRight value (byte-to-nat (byte 13)))
36      (modelWord32RotateRight value (byte-to-nat (byte 22)))))
37
38def sha256BigSigma1 =
39  (lambda unrestricted value : (family ModelWord32) .
40    (sha256XorThree
41      (modelWord32RotateRight value (byte-to-nat (byte 6)))
42      (modelWord32RotateRight value (byte-to-nat (byte 11)))
43      (modelWord32RotateRight value (byte-to-nat (byte 25)))))
44
45def sha256SmallSigma0 =
46  (lambda unrestricted value : (family ModelWord32) .
47    (sha256XorThree
48      (modelWord32RotateRight value (byte-to-nat (byte 7)))
49      (modelWord32RotateRight value (byte-to-nat (byte 18)))
50      (modelWord32ShiftRight value (byte-to-nat (byte 3)))))
51
52def sha256SmallSigma1 =
53  (lambda unrestricted value : (family ModelWord32) .
54    (sha256XorThree
55      (modelWord32RotateRight value (byte-to-nat (byte 17)))
56      (modelWord32RotateRight value (byte-to-nat (byte 19)))
57      (modelWord32ShiftRight value (byte-to-nat (byte 10)))))
58
59def sha256RoundState =
60  (lambda unrestricted roundConstant : (family ModelWord32) .
61    (lambda unrestricted scheduleWord : (family ModelWord32) .
62      (lambda unrestricted state : (family SHA256State) .
63        (eliminate
64          SHA256State
65          (lambda unrestricted current : (family SHA256State) . (family SHA256State))
66          state
67          (branch
68            SHA256StateValue
69            a
70            b
71            c
72            d
73            e
74            f
75            g
76            h
77            .
78            (app
79              (lambda unrestricted sigma1 : (family ModelWord32) .
80                (app
81                  (lambda unrestricted choose : (family ModelWord32) .
82                    (app
83                      (lambda unrestricted temp1 : (family ModelWord32) .
84                        (app
85                          (lambda unrestricted sigma0 : (family ModelWord32) .
86                            (app
87                              (lambda unrestricted majority : (family ModelWord32) .
88                                (app
89                                  (lambda unrestricted temp2 : (family ModelWord32) .
90                                    (constructor
91                                      SHA256State
92                                      SHA256StateValue
93                                      (modelWord32Add temp1 temp2)
94                                      a
95                                      b
96                                      c
97                                      (modelWord32Add d temp1)
98                                      e
99                                      f
100                                      g))
101                                  (modelWord32Add sigma0 majority)))
102                              (modelWord32Majority a b c)))
103                          (sha256BigSigma0 a)))
104                      (modelWord32AddFive h sigma1 choose roundConstant scheduleWord)))
105                  (modelWord32Choose e f g)))
106              (sha256BigSigma1 e)))))))
107
108def sha256Round =
109  (lambda unrestricted input : (family SHA256RoundInput) .
110    (eliminate
111      SHA256RoundInput
112      (lambda unrestricted current : (family SHA256RoundInput) . (family SHA256RoundOutput))
113      input
114      (branch
115        SHA256RoundInputValue
116        index
117        constant
118        schedule
119        a
120        b
121        c
122        d
123        e
124        f
125        g
126        h
127        .
128        (constructor
129          SHA256RoundOutput
130          SHA256RoundOutputValue
131          (sha256RoundState
132            constant
133            schedule
134            (constructor SHA256State SHA256StateValue a b c d e f g h))
135          (constructor
136            SHA256RoundTelemetry
137            SHA256RoundTelemetryValue
138            index
139            (byte-to-nat (byte 6))
140            zero
141            (byte-to-nat (byte 2))
142            (byte-to-nat (byte 7)))))))