proofs/crypto/sha/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 29 lines · 4 definitions

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