proofs/crypto/sha/proof.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/proof.bend as Proof

import Base
import ../../../src/crypto/sha/sha256.bend as SHA
import ./correctness.bend as Correctness

Laws

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.sha256([]) == [3820012610, 2566659092, 2600203464, 2574235940, 665731556, 1687917388, 2761267483, 2018687061] : List<&2, U32>}

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.sha256([97, 98, 99]) == [3128432319, 2399260650, 1094795486, 1571693091, 2953011619, 2518121116, 3021012833, 4060091821] : List<&2, U32>}

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.sha256(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.ascii("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq")) == [613247585, 3523623096, 3854575251, 205414457, 2738676825, 1694441831, 4142722516, 433784513] : List<&2, U32>}

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.sha256(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.ascii("abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu")) == [3478853287, 2024768384, 57468318, 2063897143, 186948369, 3908074065, 2947302659, 2063526353] : List<&2, U32>}