~/bend-docscommunity

proofs/crypto/hash/proof.bend checks

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

15 imports
import Base
import ../../../src/crypto/sha/state.bend as S256
import ../../../src/crypto/sha/core.bend as C256
import ../../../src/crypto/sha/sha256.bend as SHA256
import ../../../src/crypto/sha512/core.bend as C512
import ../../../src/crypto/sha3/core.bend as C3
import ../../../src/crypto/hash.bend as Hash
import ../sha/conformance.bend as SC
import ../sha/laws.bend as SL
import ../sha/correctness.bend as SCorr
import ../sha512/conformance.bend as S512
import ../sha3/conformance.bend as S3
import ./lists.bend as L
import ./incremental.bend as I
import ./laws.bend as Laws

Laws

law oneshot256 provedsource · line 42 · raw

@+m:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha256(m) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.digest_bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.block_bytes(List.append(&2, U32, m, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.suffix(List.length(&2, U32, m))), 48n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.round_constants, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.initial))) : List<&2, U32>}

The one-shot SHA-256 is its block loop over the padded message (the SHA-256 package's stream_correct, with nothing hashed before).