1	# Generated by tools/generators/sha512_gen.py; do not edit by hand.
2	import Base
3	import ./types.bend as T
4	
5	# SHA-512 (FIPS 180-4) on byte lists. A 64-bit word is two native U32 halves
6	# (T.W{hi, lo}); every rotation is fused into its two half-word expressions,
7	# the message schedule lives in a rolling window of the last sixteen words
8	# (no 80-word list is built), and the round constants are one list walked
9	# once per block. Proved equal to spec/crypto/sha512.bend for every input in
10	# proofs/crypto/sha512/.
11	
12	# The sixteen most recent schedule words, newest first: W[t-1] .. W[t-16].
13	type Sched is Data:
14	  Win{a: T.Lane, b: T.Lane, c: T.Lane, d: T.Lane, e: T.Lane, f: T.Lane, g: T.Lane, h: T.Lane, i: T.Lane, j: T.Lane, k: T.Lane, l: T.Lane, m: T.Lane, n: T.Lane, o: T.Lane, p: T.Lane}
15	
16	# ---------------------------------------------------------------- 64-bit words
17	
18	# (a + b) mod 2^64: the carry out of the low halves is 1 exactly when their
19	# wrapped sum is below an addend.
20	def add(a: T.Lane, b: T.Lane) -> T.Lane:
21	  match a b:
22	    case T.W{ah, +al} T.W{bh, bl}:
23	      +lo = U32.add(al, bl)
24	      T.W{U32.add(U32.add(ah, bh), Bool.to_u32(U32.is_lt(lo, al))), lo}
25	
26	# FIPS 180-4 (4.10): ROTR28 ^ ROTR34 ^ ROTR39
27	def big0(x: T.Lane) -> T.Lane:
28	  match x:
29	    case T.W{+hi, +lo}:
30	      T.W{U32.xor(U32.xor(U32.or(U32.shrn(hi, 28n), U32.shln(lo, 4n)), U32.or(U32.shrn(lo, 2n), U32.shln(hi, 30n))), U32.or(U32.shrn(lo, 7n), U32.shln(hi, 25n))),
31	        U32.xor(U32.xor(U32.or(U32.shrn(lo, 28n), U32.shln(hi, 4n)), U32.or(U32.shrn(hi, 2n), U32.shln(lo, 30n))), U32.or(U32.shrn(hi, 7n), U32.shln(lo, 25n)))}
32	
33	# FIPS 180-4 (4.11): ROTR14 ^ ROTR18 ^ ROTR41
34	def big1(x: T.Lane) -> T.Lane:
35	  match x:
36	    case T.W{+hi, +lo}:
37	      T.W{U32.xor(U32.xor(U32.or(U32.shrn(hi, 14n), U32.shln(lo, 18n)), U32.or(U32.shrn(hi, 18n), U32.shln(lo, 14n))), U32.or(U32.shrn(lo, 9n), U32.shln(hi, 23n))),
38	        U32.xor(U32.xor(U32.or(U32.shrn(lo, 14n), U32.shln(hi, 18n)), U32.or(U32.shrn(lo, 18n), U32.shln(hi, 14n))), U32.or(U32.shrn(hi, 9n), U32.shln(lo, 23n)))}
39	
40	# FIPS 180-4 (4.12): ROTR1 ^ ROTR8 ^ SHR7
41	def small0(x: T.Lane) -> T.Lane:
42	  match x:
43	    case T.W{+hi, +lo}:
44	      T.W{U32.xor(U32.xor(U32.or(U32.shrn(hi, 1n), U32.shln(lo, 31n)), U32.or(U32.shrn(hi, 8n), U32.shln(lo, 24n))), U32.shrn(hi, 7n)),
45	        U32.xor(U32.xor(U32.or(U32.shrn(lo, 1n), U32.shln(hi, 31n)), U32.or(U32.shrn(lo, 8n), U32.shln(hi, 24n))), U32.or(U32.shrn(lo, 7n), U32.shln(hi, 25n)))}
46	
47	# FIPS 180-4 (4.13): ROTR19 ^ ROTR61 ^ SHR6
48	def small1(x: T.Lane) -> T.Lane:
49	  match x:
50	    case T.W{+hi, +lo}:
51	      T.W{U32.xor(U32.xor(U32.or(U32.shrn(hi, 19n), U32.shln(lo, 13n)), U32.or(U32.shrn(lo, 29n), U32.shln(hi, 3n))), U32.shrn(hi, 6n)),
52	        U32.xor(U32.xor(U32.or(U32.shrn(lo, 19n), U32.shln(hi, 13n)), U32.or(U32.shrn(hi, 29n), U32.shln(lo, 3n))), U32.or(U32.shrn(lo, 6n), U32.shln(hi, 26n)))}
53	
54	def choose(x: T.Lane, y: T.Lane, z: T.Lane) -> T.Lane:
55	  match x y z:
56	    case T.W{+xh, +xl} T.W{yh, yl} T.W{zh, zl}:
57	      T.W{U32.xor(U32.and(xh, yh), U32.and(U32.not(xh), zh)),
58	        U32.xor(U32.and(xl, yl), U32.and(U32.not(xl), zl))}
59	
60	def majority(x: T.Lane, y: T.Lane, z: T.Lane) -> T.Lane:
61	  match x y z:
62	    case T.W{+xh, +xl} T.W{+yh, +yl} T.W{+zh, +zl}:
63	      T.W{U32.xor(U32.xor(U32.and(xh, yh), U32.and(xh, zh)), U32.and(yh, zh)),
64	        U32.xor(U32.xor(U32.and(xl, yl), U32.and(xl, zl)), U32.and(yl, zl))}
65	
66	# ---------------------------------------------------------------- one round, one block
67	
68	def step(s: T.State, k: T.Lane, w: T.Lane) -> T.State:
69	  T.H{+a, +b, +c, d, +e, +f, +g, h} = s
70	  +t1 = add(add(add(add(h, big1(e)), choose(e, f, g)), k), w)
71	  t2 = add(big0(a), majority(a, b, c))
72	  T.H{add(t1, t2), a, b, c, add(d, t1), e, f, g}
73	
74	def feedforward(x: T.State, y: T.State) -> T.State:
75	  T.H{a, b, c, d, e, f, g, h} = x
76	  T.H{i, j, k, l, m, n, o, p} = y
77	  T.H{add(a, i), add(b, j), add(c, k), add(d, l), add(e, m), add(f, n), add(g, o), add(h, p)}
78	
79	# W[t] from W[t-2], W[t-7], W[t-15], W[t-16].
80	def next(+w2: T.Lane, w7: T.Lane, +w15: T.Lane, w16: T.Lane) -> T.Lane:
81	  add(add(add(small1(w2), w7), small0(w15)), w16)
82	
83	# The remaining q rounds (64 after the block's own sixteen): each derives its
84	# schedule word from the window, then drops the oldest word.
85	def window_rounds(q: Nat, win: Sched, ks: List<&2, T.Lane>, s: T.State) -> T.State:
86	  match q win ks:
87	    case 0n _ _:
88	      s
89	    case 1n+r _ Nil{}:
90	      s
91	    case 1n+r Win{a, +b, c, d, e, f, +g, h, i, j, k, l, m, n, +o, +p} x <> xt:
92	      +w = next(b, g, o, p)
93	      window_rounds(r, Win{w, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o}, xt, step(s, x, w))
94	
95	# The block's own words first, then q window rounds (q = 64 for SHA-512);
96	# win is the block reversed.
97	def block_rounds(ws: List<&2, T.Lane>, +q: Nat, win: Sched, ks: List<&2, T.Lane>, s: T.State) -> T.State:
98	  match ws ks:
99	    case Nil{} _:
100	      window_rounds(q, win, ks, s)
101	    case w <> wt Nil{}:
102	      s
103	    case w <> wt k <> kt:
104	      block_rounds(wt, q, win, kt, step(s, k, w))
105	
106	def compress16(+a: T.Lane, +b: T.Lane, +c: T.Lane, +d: T.Lane,
107	  +e: T.Lane, +f: T.Lane, +g: T.Lane, +h: T.Lane,
108	  +i: T.Lane, +j: T.Lane, +k: T.Lane, +l: T.Lane,
109	  +m: T.Lane, +n: T.Lane, +o: T.Lane, +p: T.Lane, +q: Nat, ks: List<&2, T.Lane>, +s: T.State) -> T.State:
110	  feedforward(s, block_rounds([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q,
111	    Win{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s))
112	
113	# Every whole block of sixteen words; a shorter tail is ignored (padded
114	# messages have none).
115	def blocks(ws: List<&2, T.Lane>, +q: Nat, +ks: List<&2, T.Lane>, s: T.State) -> T.State:
116	  match ws:
117	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest:
118	      blocks(rest, q, ks, compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s))
119	    case _:
120	      s
121	
122	# ---------------------------------------------------------------- bytes in and out
123	
124	def pack(a: U32, b: U32, c: U32, d: U32) -> U32:
125	  U32.or(U32.or(U32.or(U32.shln(U32.and(a, 255), 24n),
126	    U32.shln(U32.and(b, 255), 16n)), U32.shln(U32.and(c, 255), 8n)), U32.and(d, 255))
127	
128	# Big-endian 64-bit words, eight bytes each.
129	def lanes(bytes: List<&2, U32>) -> List<&2, T.Lane>:
130	  match bytes:
131	    case a <> b <> c <> d <> e <> f <> g <> h <> rest:
132	      T.W{pack(a, b, c, d), pack(e, f, g, h)} <> lanes(rest)
133	    case _:
134	      Nil{}
135	
136	def base256(width: Nat, +n: Nat) -> List<&2, U32>:
137	  match width:
138	    case 0n:
139	      Nil{}
140	    case 1n+p:
141	      List.append(&2, U32, base256(p, Nat.div(n, 256n)), [U32.from_nat(Nat.mod(n, 256n))])
142	
143	# 8n as sixteen big-endian octets: n div 32 in the top fifteen, 8 (n mod 32) last.
144	def bit_length(+n: Nat) -> List<&2, U32>:
145	  List.append(&2, U32, base256(15n, Nat.div(n, 32n)), [U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n)])
146	
147	def zeros_if(r: Nat, fits: Bool) -> Nat:
148	  match fits:
149	    case True{}:
150	      Nat.sub(111n, r)
151	    case False{}:
152	      Nat.sub(239n, r)
153	
154	def zeros(+r: Nat) -> Nat:
155	  zeros_if(r, Nat.is_le(r, 111n))
156	
157	# 0x80, zeros up to 112 mod 128, then the 128-bit bit length.
158	def suffix(+n: Nat) -> List<&2, U32>:
159	  128 <> List.append(&2, U32, List.replicate(U32, zeros(Nat.mod(n, 128n)), 0), bit_length(n))
160	
161	def octets(+x: U32, tail: List<&2, U32>) -> List<&2, U32>:
162	  U32.and(U32.shrn(x, 24n), 255) <> U32.and(U32.shrn(x, 16n), 255) <>
163	  U32.and(U32.shrn(x, 8n), 255) <> U32.and(x, 255) <> tail
164	
165	def lane_octets(l: T.Lane, tail: List<&2, U32>) -> List<&2, U32>:
166	  match l:
167	    case T.W{+hi, +lo}:
168	      octets(hi, octets(lo, tail))
169	
170	# The 64-byte digest H0 .. H7.
171	def digest_bytes(s: T.State) -> List<&2, U32>:
172	  T.H{a, b, c, d, e, f, g, h} = s
173	  lane_octets(a, lane_octets(b, lane_octets(c, lane_octets(d,
174	    lane_octets(e, lane_octets(f, lane_octets(g, lane_octets(h, Nil{}))))))))
175	
176	# ---------------------------------------------------------------- constants
177	
178	def initial() -> T.State:
179	  T.H{T.W{1779033703, 4089235720}, T.W{3144134277, 2227873595},
180	    T.W{1013904242, 4271175723}, T.W{2773480762, 1595750129},
181	    T.W{1359893119, 2917565137}, T.W{2600822924, 725511199},
182	    T.W{528734635, 4215389547}, T.W{1541459225, 327033209}}
183	
184	def round_constants() -> List<&2, T.Lane>:
185	  [T.W{1116352408, 3609767458}, T.W{1899447441, 602891725},
186	   T.W{3049323471, 3964484399}, T.W{3921009573, 2173295548},
187	   T.W{961987163, 4081628472}, T.W{1508970993, 3053834265},
188	   T.W{2453635748, 2937671579}, T.W{2870763221, 3664609560},
189	   T.W{3624381080, 2734883394}, T.W{310598401, 1164996542},
190	   T.W{607225278, 1323610764}, T.W{1426881987, 3590304994},
191	   T.W{1925078388, 4068182383}, T.W{2162078206, 991336113},
192	   T.W{2614888103, 633803317}, T.W{3248222580, 3479774868},
193	   T.W{3835390401, 2666613458}, T.W{4022224774, 944711139},
194	   T.W{264347078, 2341262773}, T.W{604807628, 2007800933},
195	   T.W{770255983, 1495990901}, T.W{1249150122, 1856431235},
196	   T.W{1555081692, 3175218132}, T.W{1996064986, 2198950837},
197	   T.W{2554220882, 3999719339}, T.W{2821834349, 766784016},
198	   T.W{2952996808, 2566594879}, T.W{3210313671, 3203337956},
199	   T.W{3336571891, 1034457026}, T.W{3584528711, 2466948901},
200	   T.W{113926993, 3758326383}, T.W{338241895, 168717936},
201	   T.W{666307205, 1188179964}, T.W{773529912, 1546045734},
202	   T.W{1294757372, 1522805485}, T.W{1396182291, 2643833823},
203	   T.W{1695183700, 2343527390}, T.W{1986661051, 1014477480},
204	   T.W{2177026350, 1206759142}, T.W{2456956037, 344077627},
205	   T.W{2730485921, 1290863460}, T.W{2820302411, 3158454273},
206	   T.W{3259730800, 3505952657}, T.W{3345764771, 106217008},
207	   T.W{3516065817, 3606008344}, T.W{3600352804, 1432725776},
208	   T.W{4094571909, 1467031594}, T.W{275423344, 851169720},
209	   T.W{430227734, 3100823752}, T.W{506948616, 1363258195},
210	   T.W{659060556, 3750685593}, T.W{883997877, 3785050280},
211	   T.W{958139571, 3318307427}, T.W{1322822218, 3812723403},
212	   T.W{1537002063, 2003034995}, T.W{1747873779, 3602036899},
213	   T.W{1955562222, 1575990012}, T.W{2024104815, 1125592928},
214	   T.W{2227730452, 2716904306}, T.W{2361852424, 442776044},
215	   T.W{2428436474, 593698344}, T.W{2756734187, 3733110249},
216	   T.W{3204031479, 2999351573}, T.W{3329325298, 3815920427},
217	   T.W{3391569614, 3928383900}, T.W{3515267271, 566280711},
218	   T.W{3940187606, 3454069534}, T.W{4118630271, 4000239992},
219	   T.W{116418474, 1914138554}, T.W{174292421, 2731055270},
220	   T.W{289380356, 3203993006}, T.W{460393269, 320620315},
221	   T.W{685471733, 587496836}, T.W{852142971, 1086792851},
222	   T.W{1017036298, 365543100}, T.W{1126000580, 2618297676},
223	   T.W{1288033470, 3409855158}, T.W{1501505948, 4234509866},
224	   T.W{1607167915, 987167468}, T.W{1816402316, 1246189591}]
225	
226	# ---------------------------------------------------------------- SHA-512
227	
228	def hash_padded(bytes: List<&2, U32>) -> List<&2, U32>:
229	  digest_bytes(blocks(lanes(bytes), 64n, round_constants(), initial()))
230	
231	def sha512(+bytes: List<&2, U32>) -> List<&2, U32>:
232	  hash_padded(List.append(&2, U32, bytes, suffix(List.length(&2, U32, bytes))))