~/bend-docscommunity

PROOF.bend checks

raw source on the hub · import 0x3bdc0c9f5265bb49f7fc76b61f529f24/PROOF.bend as PROOF

3 imports
import Base
import ./legacy_model.bend as SHA
import ./CORRECTNESS.bend as Correctness

Laws

law empty_vector provedsource · line 5 · raw

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

law abc_vector provedsource · line 9 · raw

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

law padding_boundary_vector provedsource · line 19 · raw

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

law multiblock_vector provedsource · line 25 · raw

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