1module Data.SHA256
2
3import Model.Config
4import Model.Parameter
5import Std.Byte
6import Std.Foundation
7import Std.Natural
8
9family SHA256State : Type 0
10constructor SHA256StateValue
11field unrestricted sha256StateWord0 : (family ModelWord32)
12field unrestricted sha256StateWord1 : (family ModelWord32)
13field unrestricted sha256StateWord2 : (family ModelWord32)
14field unrestricted sha256StateWord3 : (family ModelWord32)
15field unrestricted sha256StateWord4 : (family ModelWord32)
16field unrestricted sha256StateWord5 : (family ModelWord32)
17field unrestricted sha256StateWord6 : (family ModelWord32)
18field unrestricted sha256StateWord7 : (family ModelWord32)
19
20end-family
21
22family SHA256Schedule : Type 0
23constructor SHA256ScheduleEnd
24constructor SHA256ScheduleNext
25field unrestricted sha256ScheduleWord : (family ModelWord32)
26recursive unrestricted sha256ScheduleTail
27
28end-family
29
30family SHA256Context : Type 0
31constructor SHA256ContextValue
32field unrestricted sha256ContextState : (family SHA256State)
33field unrestricted sha256ContextTotalBytes : (family ModelWord64)
34field unrestricted sha256ContextPendingBytes : Bytes
35
36end-family
37
38family SHA256DigestLengthValidity : Type 0
39constructor SHA256DigestLengthValid
40constructor SHA256DigestLengthInvalid
41
42end-family
43
44family SHA256Digest : Type 0
45constructor SHA256DigestValue
46field unrestricted sha256DigestBytes : Bytes
47field erased sha256DigestLengthProof : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length sha256DigestBytes) (byte-to-nat (byte 32)))) (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))
48
49end-family
50
51family SHA256CompressionInput : Type 0
52constructor SHA256CompressionInputValue
53field unrestricted sha256CompressionState : (family SHA256State)
54field unrestricted sha256CompressionBlock : Bytes
55
56end-family
57
58family SHA256RoundInput : Type 0
59constructor SHA256RoundInputValue
60field unrestricted sha256RoundIndex : (family ModelWord32)
61field unrestricted sha256RoundConstant : (family ModelWord32)
62field unrestricted sha256RoundScheduleWord : (family ModelWord32)
63field unrestricted sha256RoundA : (family ModelWord32)
64field unrestricted sha256RoundB : (family ModelWord32)
65field unrestricted sha256RoundC : (family ModelWord32)
66field unrestricted sha256RoundD : (family ModelWord32)
67field unrestricted sha256RoundE : (family ModelWord32)
68field unrestricted sha256RoundF : (family ModelWord32)
69field unrestricted sha256RoundG : (family ModelWord32)
70field unrestricted sha256RoundH : (family ModelWord32)
71
72end-family
73
74family SHA256ErrorCode : Type 0
75constructor SHA256InputLengthOverflow
76constructor SHA256PendingBlockTooLarge
77constructor SHA256ContextLengthMismatch
78constructor SHA256BlockLengthInvalid
79constructor SHA256ScheduleLengthInvalid
80constructor SHA256RoundCountInvalid
81constructor SHA256DigestLengthInvalid
82constructor SHA256LengthEncodingInvalid
83constructor SHA256PaddingLengthInvalid
84constructor SHA256FileOpenFailed
85constructor SHA256FileReadFailed
86constructor SHA256FileCloseFailed
87constructor SHA256DigestHexInvalid
88
89end-family
90
91family SHA256Result : Type 0
92constructor SHA256Succeeded
93field unrestricted sha256ResultDigest : (family SHA256Digest)
94constructor SHA256Failed
95field unrestricted sha256ResultError : (family SHA256ErrorCode)
96
97end-family
98
99def sha256ErrorCodeBytes =
100 (lambda unrestricted code : (family SHA256ErrorCode) .
101 (eliminate
102 SHA256ErrorCode
103 (lambda unrestricted current : (family SHA256ErrorCode) . Bytes)
104 code
105 (branch SHA256InputLengthOverflow . b"ALPHA-SHA256-001")
106 (branch SHA256PendingBlockTooLarge . b"ALPHA-SHA256-002")
107 (branch SHA256ContextLengthMismatch . b"ALPHA-SHA256-003")
108 (branch SHA256BlockLengthInvalid . b"ALPHA-SHA256-004")
109 (branch SHA256ScheduleLengthInvalid . b"ALPHA-SHA256-005")
110 (branch SHA256RoundCountInvalid . b"ALPHA-SHA256-006")
111 (branch SHA256DigestLengthInvalid . b"ALPHA-SHA256-007")
112 (branch SHA256LengthEncodingInvalid . b"ALPHA-SHA256-008")
113 (branch SHA256PaddingLengthInvalid . b"ALPHA-SHA256-009")
114 (branch SHA256FileOpenFailed . b"ALPHA-SHA256-010")
115 (branch SHA256FileReadFailed . b"ALPHA-SHA256-011")
116 (branch SHA256FileCloseFailed . b"ALPHA-SHA256-012")
117 (branch SHA256DigestHexInvalid . b"ALPHA-SHA256-013")))
118
119-- The only public Bytes -> SHA256Digest boundary. The equality witness is
120-- erased, but the ordinary kernel still checks that construction is possible
121-- only when the byte sequence is exactly 32 bytes long.
122def sha256DigestFromBytes : (pi unrestricted input : Bytes . (family SHA256Result)) =
123 (lambda unrestricted input : Bytes .
124 (app
125 (eliminate
126 SHA256DigestLengthValidity
127 (lambda unrestricted decision : (family SHA256DigestLengthValidity) .
128 (pi erased witness : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) decision) .
129 (family SHA256Result)))
130 (nat-eliminate
131 (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity))
132 (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid)
133 (lambda unrestricted predecessor : Nat .
134 (lambda unrestricted induction : (family SHA256DigestLengthValidity) .
135 (constructor SHA256DigestLengthValidity SHA256DigestLengthValid)))
136 (naturalEqual (bytes-length input) (byte-to-nat (byte 32))))
137 (branch
138 SHA256DigestLengthValid
139 .
140 (lambda erased witness : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) (constructor SHA256DigestLengthValidity SHA256DigestLengthValid)) .
141 (constructor
142 SHA256Result
143 SHA256Succeeded
144 (constructor SHA256Digest SHA256DigestValue input witness))))
145 (branch
146 SHA256DigestLengthInvalid
147 .
148 (lambda erased witness : (equal (family SHA256DigestLengthValidity) (nat-eliminate (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity)) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SHA256DigestLengthValidity) . (constructor SHA256DigestLengthValidity SHA256DigestLengthValid))) (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))) (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid)) .
149 (constructor
150 SHA256Result
151 SHA256Failed
152 (constructor SHA256ErrorCode SHA256DigestLengthInvalid)))))
153 (refl
154 (family SHA256DigestLengthValidity)
155 (nat-eliminate
156 (lambda unrestricted equalLength : Nat . (family SHA256DigestLengthValidity))
157 (constructor SHA256DigestLengthValidity SHA256DigestLengthInvalid)
158 (lambda unrestricted predecessor : Nat .
159 (lambda unrestricted induction : (family SHA256DigestLengthValidity) .
160 (constructor SHA256DigestLengthValidity SHA256DigestLengthValid)))
161 (naturalEqual (bytes-length input) (byte-to-nat (byte 32)))))))
162
163def sha256DigestToBytes =
164 (lambda unrestricted digest : (family SHA256Digest) .
165 (eliminate
166 SHA256Digest
167 (lambda unrestricted current : (family SHA256Digest) . Bytes)
168 digest
169 (branch SHA256DigestValue bytes proof . bytes)))
170
171def sha256DigestEqual =
172 (lambda unrestricted left : (family SHA256Digest) .
173 (lambda unrestricted right : (family SHA256Digest) .
174 (bytes-equal (sha256DigestToBytes left) (sha256DigestToBytes right))))
175
176def sha256InitialState =
177 (constructor
178 SHA256State
179 SHA256StateValue
180 (constructor ModelWord32 ModelWord32Value (byte 103) (byte 230) (byte 9) (byte 106))
181 (constructor ModelWord32 ModelWord32Value (byte 133) (byte 174) (byte 103) (byte 187))
182 (constructor ModelWord32 ModelWord32Value (byte 114) (byte 243) (byte 110) (byte 60))
183 (constructor ModelWord32 ModelWord32Value (byte 58) (byte 245) (byte 79) (byte 165))
184 (constructor ModelWord32 ModelWord32Value (byte 127) (byte 82) (byte 14) (byte 81))
185 (constructor ModelWord32 ModelWord32Value (byte 140) (byte 104) (byte 5) (byte 155))
186 (constructor ModelWord32 ModelWord32Value (byte 171) (byte 217) (byte 131) (byte 31))
187 (constructor ModelWord32 ModelWord32Value (byte 25) (byte 205) (byte 224) (byte 91)))
188
189def sha256InitialContext =
190 (constructor
191 SHA256Context
192 SHA256ContextValue
193 sha256InitialState
194 (constructor
195 ModelWord64
196 ModelWord64Value
197 (byte 0)
198 (byte 0)
199 (byte 0)
200 (byte 0)
201 (byte 0)
202 (byte 0)
203 (byte 0)
204 (byte 0))
205 b"")
206
207def sha256MaximumInputBytes =
208 (constructor
209 ModelWord64
210 ModelWord64Value
211 (byte 255)
212 (byte 255)
213 (byte 255)
214 (byte 255)
215 (byte 255)
216 (byte 255)
217 (byte 255)
218 (byte 31))
219
220def sha256Word64Eight =
221 (constructor
222 ModelWord64
223 ModelWord64Value
224 (byte 8)
225 (byte 0)
226 (byte 0)
227 (byte 0)
228 (byte 0)
229 (byte 0)
230 (byte 0)
231 (byte 0))
232
233def sha256BlockBytes =
234 (constructor ModelWord32 ModelWord32Value (byte 64) (byte 0) (byte 0) (byte 0))
235
236def sha256ScheduleWords =
237 (constructor ModelWord32 ModelWord32Value (byte 64) (byte 0) (byte 0) (byte 0))
238
239def sha256DigestBytes =
240 (constructor ModelWord32 ModelWord32Value (byte 32) (byte 0) (byte 0) (byte 0))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.