1	# Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f
2	# (src/crypto/sha/sha256.bend), byte-identical. See core.bend header.
3	import Base
4	import ./core.bend as Core
5	
6	# The core refinement theorem quantifies over every constant table.
7	# Instantiate the verified core with the FIPS 180-4 constants.
8	def constants() -> List<&2, U32>:
9	  [1116352408, 1899447441, 3049323471, 3921009573,
10	   961987163, 1508970993, 2453635748, 2870763221,
11	   3624381080, 310598401, 607225278, 1426881987,
12	   1925078388, 2162078206, 2614888103, 3248222580,
13	   3835390401, 4022224774, 264347078, 604807628,
14	   770255983, 1249150122, 1555081692, 1996064986,
15	   2554220882, 2821834349, 2952996808, 3210313671,
16	   3336571891, 3584528711, 113926993, 338241895,
17	   666307205, 773529912, 1294757372, 1396182291,
18	   1695183700, 1986661051, 2177026350, 2456956037,
19	   2730485921, 2820302411, 3259730800, 3345764771,
20	   3516065817, 3600352804, 4094571909, 275423344,
21	   430227734, 506948616, 659060556, 883997877,
22	   958139571, 1322822218, 1537002063, 1747873779,
23	   1955562222, 2024104815, 2227730452, 2361852424,
24	   2428436474, 2756734187, 3204031479, 3329325298]
25	
26	def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
27	  Core.sha256(bytes)
28	
29	def ascii(s: String) -> List<&2, U32>:
30	  Core.ascii(s)
31	
32	def hex(ws: List<&2, U32>) -> String:
33	  Core.hex(ws)
34	
35	# Big-endian octets, represented as U32 values in 0..255.
36	def digest_bytes(ws: List<&2, U32>) -> List<&2, U32>:
37	  match ws:
38	    case Nil{}:
39	      Nil{}
40	    case +w <> tail:
41	      U32.and(U32.shrn(w, 24n), 255) <>
42	      U32.and(U32.shrn(w, 16n), 255) <>
43	      U32.and(U32.shrn(w, 8n), 255) <>
44	      U32.and(w, 255) <> digest_bytes(tail)
45	
46	def sha256_bytes(bytes: List<&2, U32>) -> List<&2, U32>:
47	  digest_bytes(sha256(bytes))