1	import Base
2	import ../../src/crypto/sha/state.bend as Types
3	
4	# Executable specification of the byte-oriented SHA-256 algorithm in FIPS 180-4.
5	# Only the neutral state representation is shared with the implementation.
6	# No implementation arithmetic, padding, schedule, table, or hash is called.
7	# Base U32 has the required modulo-2^32 arithmetic and logical bit operations.
8	
9	def initial() -> Types.State:
10	  Types.H{1779033703, 3144134277, 1013904242, 2773480762,
11	    1359893119, 2600822924, 528734635, 1541459225}
12	
13	# FIPS 4.1.2: ROR_n(x) = SHR_n(x) OR SHL_(32-n)(x).
14	def rotate(+x: U32, +n: Nat) -> U32:
15	  U32.or(U32.shrn(x, n), U32.shln(x, Nat.sub(32n, n)))
16	
17	def sigma0(+x: U32) -> U32:
18	  U32.xor(U32.xor(rotate(x, 7n), rotate(x, 18n)), U32.shrn(x, 3n))
19	
20	def sigma1(+x: U32) -> U32:
21	  U32.xor(U32.xor(rotate(x, 17n), rotate(x, 19n)), U32.shrn(x, 10n))
22	
23	def sum0(+x: U32) -> U32:
24	  U32.xor(U32.xor(rotate(x, 2n), rotate(x, 13n)), rotate(x, 22n))
25	
26	def sum1(+x: U32) -> U32:
27	  U32.xor(U32.xor(rotate(x, 6n), rotate(x, 11n)), rotate(x, 25n))
28	
29	def ch(+x: U32, y: U32, z: U32) -> U32:
30	  U32.xor(U32.and(x, y), U32.and(U32.not(x), z))
31	
32	def maj(+x: U32, +y: U32, +z: U32) -> U32:
33	  U32.xor(U32.xor(U32.and(x, y), U32.and(x, z)), U32.and(y, z))
34	
35	# A base-256 representation, most significant digit first, of fixed width.
36	def octets(width: Nat, +n: Nat) -> List<&2, U32>:
37	  match width:
38	    case 0n:
39	      Nil{}
40	    case 1n+p:
41	      List.append(&2, U32, octets(p, Nat.div(n, 256n)),
42	        [U32.from_nat(Nat.mod(n, 256n))])
43	
44	# 8*n = 256*(n/32) + 8*(n mod 32); avoids overflowing runtime Nat.
45	def length_field(+n: Nat) -> List<&2, U32>:
46	  List.append(&2, U32, octets(7n, Nat.div(n, 32n)),
47	    [U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n)])
48	
49	# FIPS padding: a remainder of 0..55 leaves room in this block;
50	# a remainder of 56..63 needs another block. No modular shortcut is used.
51	def zero_count_if(r: Nat, fits: Bool) -> Nat:
52	  match fits:
53	    case True{}:
54	      Nat.sub(55n, r)
55	    case False{}:
56	      Nat.sub(119n, r)
57	
58	def zero_count(+r: Nat) -> Nat:
59	  zero_count_if(r, Nat.is_le(r, 55n))
60	
61	def padding_suffix(+n: Nat) -> List<&2, U32>:
62	  128 <> List.append(&2, U32,
63	    List.replicate(U32, zero_count(Nat.mod(n, 64n)), 0), length_field(n))
64	
65	def pad(+bytes: List<&2, U32>) -> List<&2, U32>:
66	  List.append(&2, U32, bytes, padding_suffix(List.length(&2, U32, bytes)))
67	
68	def decode(a: U32, b: U32, c: U32, d: U32) -> U32:
69	  U32.or(U32.or(U32.or(U32.shln(U32.and(a, 255), 24n),
70	    U32.shln(U32.and(b, 255), 16n)), U32.shln(U32.and(c, 255), 8n)), U32.and(d, 255))
71	
72	def words(bytes: List<&2, U32>) -> List<&2, U32>:
73	  match bytes:
74	    case a <> b <> c <> d <> rest:
75	      decode(a, b, c, d) <> words(rest)
76	    case _:
77	      Nil{}
78	
79	# In reverse history, index j denotes W[t-1-j]. Only valid indices are
80	# reached for the actual 16-word input blocks; default zero makes nth total.
81	def nth(history: List<&2, U32>, index: Nat) -> U32:
82	  match history index:
83	    case Nil{} _:
84	      0
85	    case w <> rest 0n:
86	      w
87	    case w <> rest 1n+p:
88	      nth(rest, p)
89	
90	# The FIPS recurrence names prior words by lags 2, 7, 15 and 16.
91	def previous(history: List<&2, U32>, lag: Nat) -> U32:
92	  nth(history, Nat.sub(lag, 1n))
93	
94	def recurrence(+history: List<&2, U32>) -> U32:
95	  (sigma1(previous(history, 2n)) + previous(history, 7n)
96	    + sigma0(previous(history, 15n)) + previous(history, 16n) : U32)
97	
98	def extension(rounds: Nat, +history: List<&2, U32>) -> List<&2, U32>:
99	  match rounds:
100	    case 0n:
101	      Nil{}
102	    case 1n+p:
103	      +w = recurrence(history)
104	      w <> extension(p, w <> history)
105	
106	# Standard SHA-256 instantiates extra=48, extending the initial 16 to 64.
107	def schedule(extra: Nat, +block: List<&2, U32>) -> List<&2, U32>:
108	  List.append(&2, U32, block, extension(extra, List.reverse(&2, U32, block)))
109	
110	def schedules(ws: List<&2, U32>, +extra: Nat) -> List<&2, List<&2, U32>>:
111	  match ws:
112	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest:
113	      schedule(extra, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]) <> schedules(rest, extra)
114	    case _:
115	      Nil{}
116	
117	def prepare(bytes: List<&2, U32>, extra: Nat) -> List<&2, List<&2, U32>>:
118	  schedules(words(pad(bytes)), extra)
119	
120	def step(s: Types.State, k: U32, w: U32) -> Types.State:
121	  Types.H{+a, +b, +c, d, +e, +f, +g, h} = s
122	  +t1 = (h + sum1(e) + ch(e, f, g) + k + w : U32)
123	  t2 = (sum0(a) + maj(a, b, c) : U32)
124	  Types.H{(t1 + t2 : U32), a, b, c, (d + t1 : U32), e, f, g}
125	
126	def rounds(ks: List<&2, U32>, ws: List<&2, U32>) -> Types.State -> Types.State:
127	  match ks ws:
128	    case Nil{} _:
129	      s => s
130	    case k <> kt Nil{}:
131	      s => s
132	    case k <> kt w <> wt:
133	      next = rounds(kt, wt)
134	      s => next(step(s, k, w))
135	
136	def feedforward(x: Types.State, y: Types.State) -> Types.State:
137	  Types.H{a, b, c, d, e, f, g, h} = x
138	  Types.H{i, j, k, l, m, n, o, p} = y
139	  Types.H{(a + i : U32), (b + j : U32), (c + k : U32), (d + l : U32),
140	    (e + m : U32), (f + n : U32), (g + o : U32), (h + p : U32)}
141	
142	def compress(ws: List<&2, U32>, ks: List<&2, U32>, +s: Types.State) -> Types.State:
143	  feedforward(s, rounds(ks, ws)(s))
144	
145	def blocks(prepared: List<&2, List<&2, U32>>, +ks: List<&2, U32>) -> Types.State -> Types.State:
146	  match prepared:
147	    case Nil{}:
148	      s => s
149	    case block <> rest:
150	      next = blocks(rest, ks)
151	      s => next(compress(block, ks, s))
152	
153	def digest(s: Types.State) -> List<&2, U32>:
154	  Types.H{a, b, c, d, e, f, g, h} = s
155	  [a, b, c, d, e, f, g, h]
156	
157	def hash(bytes: List<&2, U32>, extra: Nat, ks: List<&2, U32>) -> List<&2, U32>:
158	  digest(blocks(prepare(bytes, extra), ks)(initial()))
159	
160	# FIPS 180-4 section 4.2.2, transcribed separately from the implementation.
161	def constants() -> List<&2, U32>:
162	  [1116352408, 1899447441, 3049323471, 3921009573,
163	   961987163, 1508970993, 2453635748, 2870763221,
164	   3624381080, 310598401, 607225278, 1426881987,
165	   1925078388, 2162078206, 2614888103, 3248222580,
166	   3835390401, 4022224774, 264347078, 604807628,
167	   770255983, 1249150122, 1555081692, 1996064986,
168	   2554220882, 2821834349, 2952996808, 3210313671,
169	   3336571891, 3584528711, 113926993, 338241895,
170	   666307205, 773529912, 1294757372, 1396182291,
171	   1695183700, 1986661051, 2177026350, 2456956037,
172	   2730485921, 2820302411, 3259730800, 3345764771,
173	   3516065817, 3600352804, 4094571909, 275423344,
174	   430227734, 506948616, 659060556, 883997877,
175	   958139571, 1322822218, 1537002063, 1747873779,
176	   1955562222, 2024104815, 2227730452, 2361852424,
177	   2428436474, 2756734187, 3204031479, 3329325298]
178	
179	def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
180	  hash(bytes, 48n, constants())
181	
182	# FIPS digest serialization: most significant octet of each word first.
183	def word_octets(+w: U32) -> List<&2, U32>:
184	  [U32.and(U32.shrn(w, 24n), 255),
185	   U32.and(U32.shrn(w, 16n), 255),
186	   U32.and(U32.shrn(w, 8n), 255), U32.and(w, 255)]
187	
188	def digest_octets(ws: List<&2, U32>) -> List<&2, U32>:
189	  match ws:
190	    case Nil{}:
191	      Nil{}
192	    case w <> tail:
193	      List.append(&2, U32, word_octets(w), digest_octets(tail))
194	
195	def sha256_bytes(bytes: List<&2, U32>) -> List<&2, U32>:
196	  digest_octets(sha256(bytes))