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	import ./state.bend as S
6	import bend-kit-bytes@0.3.2.0/bytes.bend as Packed
7	
8	# The core refinement theorem quantifies over every constant table.
9	# Instantiate the verified core with the FIPS 180-4 constants.
10	def constants() -> List<&2, U32>:
11	  [1116352408, 1899447441, 3049323471, 3921009573,
12	   961987163, 1508970993, 2453635748, 2870763221,
13	   3624381080, 310598401, 607225278, 1426881987,
14	   1925078388, 2162078206, 2614888103, 3248222580,
15	   3835390401, 4022224774, 264347078, 604807628,
16	   770255983, 1249150122, 1555081692, 1996064986,
17	   2554220882, 2821834349, 2952996808, 3210313671,
18	   3336571891, 3584528711, 113926993, 338241895,
19	   666307205, 773529912, 1294757372, 1396182291,
20	   1695183700, 1986661051, 2177026350, 2456956037,
21	   2730485921, 2820302411, 3259730800, 3345764771,
22	   3516065817, 3600352804, 4094571909, 275423344,
23	   430227734, 506948616, 659060556, 883997877,
24	   958139571, 1322822218, 1537002063, 1747873779,
25	   1955562222, 2024104815, 2227730452, 2361852424,
26	   2428436474, 2756734187, 3204031479, 3329325298]
27	
28	# SHA-256 for the reference octet-list input.
29	def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
30	  Core.sha256(bytes)
31	
32	# Convert ASCII text to the reference octet-list input.
33	def ascii(text: String) -> List<&2, U32>:
34	  Core.ascii(text)
35	
36	# Format eight digest words as lowercase hexadecimal.
37	def hex(ws: List<&2, U32>) -> String:
38	  Core.hex(ws)
39	
40	# Big-endian octets, represented as U32 values in 0..255.
41	def digest_bytes(ws: List<&2, U32>) -> List<&2, U32>:
42	  match ws:
43	    case Nil{}:
44	      Nil{}
45	    case +w <> tail:
46	      U32.and(U32.shrn(w, 24n), 255) <>
47	      U32.and(U32.shrn(w, 16n), 255) <>
48	      U32.and(U32.shrn(w, 8n), 255) <>
49	      U32.and(w, 255) <> digest_bytes(tail)
50	
51	# Return the reference digest as eight big-endian octets per word.
52	def sha256_bytes(bytes: List<&2, U32>) -> List<&2, U32>:
53	  digest_bytes(sha256(bytes))
54	
55	# Compress one packed block using sixteen transient big-endian words. The file
56	# buffer stays packed; no per-byte List is constructed for complete blocks.
57	def packed.compress(words: List<&2, U32>, state: S.State) -> S.State:
58	  match words:
59	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> Nil{}:
60	      Core.fips_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, 48n, state)
61	    case _:
62	      state
63	
64	# Read complete 64-byte blocks directly through a bounded package cursor.
65	def packed.blocks(
66	  remaining: Nat,
67	  in_block: Nat,
68	  pair: Packed.Cursor & Maybe<&2, U32>,
69	  acc: List<&2, U32>,
70	  state: S.State
71	) -> Packed.Cursor & S.State:
72	  match remaining:
73	    case 0n:
74	      match pair:
75	        case (cursor, _):
76	          (cursor, state)
77	    case 1n:
78	      match in_block:
79	        case 0n:
80	          match pair:
81	            case (cursor, _):
82	              (cursor, state)
83	        case 1n:
84	          match pair:
85	            case (cursor, Some{word}):
86	              (cursor, packed.compress(List.reverse(&2, U32, word <> acc), state))
87	            case (cursor, None{}):
88	              (cursor, state)
89	        case 1n+more:
90	          match pair:
91	            case (cursor, _):
92	              (cursor, state)
93	    case 1n+more:
94	      match in_block:
95	        case 0n:
96	          match pair:
97	            case (cursor, _):
98	              (cursor, state)
99	        case 1n:
100	          match pair:
101	            case (cursor, Some{word}):
102	              packed.blocks(more, 16n, Packed.Cursor.u32be(cursor), Nil{},
103	                packed.compress(List.reverse(&2, U32, word <> acc), state))
104	            case (cursor, None{}):
105	              (cursor, state)
106	        case 1n+left:
107	          match pair:
108	            case (cursor, Some{word}):
109	              packed.blocks(more, left, Packed.Cursor.u32be(cursor), word <> acc, state)
110	            case (cursor, None{}):
111	              (cursor, state)
112	
113	# Read the remaining fewer than 64 bytes for the existing constant-space tail
114	# padding routines. This list is bounded by 63 octets, regardless of file size.
115	def packed.tail(
116	  remaining: Nat,
117	  pair: Packed.Cursor & Maybe<&2, U32>,
118	  acc: List<&2, U32>
119	) -> Packed.Cursor & List<&2, U32>:
120	  match remaining:
121	    case 0n:
122	      match pair:
123	        case (cursor, _):
124	          (cursor, List.reverse(&2, U32, acc))
125	    case 1n:
126	      match pair:
127	        case (cursor, Some{byte}):
128	          (cursor, List.reverse(&2, U32, byte <> acc))
129	        case (cursor, None{}):
130	          (cursor, Nil{})
131	    case 1n+more:
132	      match pair:
133	        case (cursor, Some{byte}):
134	          packed.tail(more, Packed.Cursor.u8(cursor), byte <> acc)
135	        case (cursor, None{}):
136	          (cursor, Nil{})
137	
138	def packed.finish.tail(total: U32, pair: Packed.Cursor & List<&2, U32>, state: S.State) -> S.State:
139	  match pair:
140	    case (_, tail):
141	      Core.finish_n(tail, U32.to_nat(total), 48n, state)
142	
143	def packed.final.tail(total: U32, tail_len: Nat, cursor: Packed.Cursor, state: S.State) -> S.State:
144	  match tail_len:
145	    case 0n:
146	      packed.finish.tail(total, (cursor, Nil{}), state)
147	    case 1n+more:
148	      packed.finish.tail(total, packed.tail(1n+more, Packed.Cursor.u8(cursor), Nil{}), state)
149	
150	def packed.final(total: U32, tail_len: Nat, cursor: Packed.Cursor, state: S.State) -> List<&2, U32>:
151	  Core.digest(packed.final.tail(total, tail_len, cursor, state))
152	
153	def packed.after_blocks(total: U32, tail_len: Nat, pair: Packed.Cursor & S.State) -> List<&2, U32>:
154	  match pair:
155	    case (cursor, state):
156	      packed.final(total, tail_len, cursor, state)
157	
158	def packed.start.blocks(+total: U32, cursor: Packed.Cursor, blocks: Nat, +tail_len: Nat) -> List<&2, U32>:
159	  match blocks:
160	    case 0n:
161	      packed.final(total, tail_len, cursor, Core.initial())
162	    case 1n+more:
163	      packed.after_blocks(total, tail_len,
164	        packed.blocks(((1n+more) * 16n : Nat), 16n, Packed.Cursor.u32be(cursor), Nil{}, Core.initial()))
165	
166	def packed.start(+total: U32, cursor: Packed.Cursor) -> List<&2, U32>:
167	  packed.start.blocks(total, cursor,
168	    Nat.div(U32.to_nat(total), 64n), Nat.mod(U32.to_nat(total), 64n))
169	
170	# SHA-256 directly over packed bytes. Full blocks are read as sixteen u32be
171	# words; only the final 0..63 octets use the existing tail padding interface.
172	def sha256_packed(bytes: Packed.Bytes) -> List<&2, U32>:
173	  match bytes:
174	    case Packed.Bytes{+len, buf}:
175	      packed.start(len, Packed.Cursor.new(Packed.Bytes{len, buf}))
176	
177	def packed.digest.finish.bytes(pair: Packed.Bytes & U32) -> Packed.Bytes:
178	  match pair:
179	    case (bytes, _):
180	      bytes
181	
182	def packed.digest.finish(pair: Packed.Cursor & Bool) -> Packed.Bytes:
183	  match pair:
184	    case (cursor, _):
185	      packed.digest.finish.bytes(Packed.Cursor.finish(cursor))
186	
187	def packed.digest.words(words: List<&2, U32>, pair: Packed.Cursor & Bool) -> Packed.Bytes:
188	  match words:
189	    case Nil{}:
190	      packed.digest.finish(pair)
191	    case word <> rest:
192	      match pair:
193	        case (cursor, _) :
194	          packed.digest.words(rest, Packed.Cursor.put.u32be(cursor, word))
195	
196	# Return the SHA-256 digest as packed bytes in canonical big-endian order.
197	def sha256_packed_bytes(bytes: Packed.Bytes) -> Packed.Bytes:
198	  packed.digest.words(sha256_packed(bytes),
199	    (Packed.Cursor.new(Packed.Bytes{32, Packed.alloc(32)}), True{}))