1	import Base
2	import ../../../src/crypto/sha/sha256.bend as SHA
3	import ./correctness.bend as Correctness
4	
5	law empty_vector:
6	  {SHA.sha256([]) == [3820012610, 2566659092, 2600203464, 2574235940,
7	    665731556, 1687917388, 2761267483, 2018687061] : List<&2, U32>}
8	
9	law abc_vector:
10	  {SHA.sha256([97, 98, 99]) == [3128432319, 2399260650, 1094795486, 1571693091,
11	    2953011619, 2518121116, 3021012833, 4060091821] : List<&2, U32>}
12	
13	def empty_vector():
14	  {==}
15	
16	def abc_vector():
17	  {==}
18	
19	law padding_boundary_vector:
20	  {SHA.sha256(SHA.ascii("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq")) == [613247585, 3523623096, 3854575251, 205414457, 2738676825, 1694441831, 4142722516, 433784513] : List<&2, U32>}
21	
22	def padding_boundary_vector():
23	  {==}
24	
25	law multiblock_vector:
26	  {SHA.sha256(SHA.ascii("abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu")) == [3478853287, 2024768384, 57468318, 2063897143, 186948369, 3908074065, 2947302659, 2063526353] : List<&2, U32>}
27	
28	def multiblock_vector():
29	  {==}