~/bend-docscommunity

proofs/crypto/sha3/laws.bend open laws/TODOs

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha3/laws.bend as Laws

3 imports
import Base
import ../../../src/crypto/sha3/sha3_256.bend as SHA3
import ../../../spec/crypto/sha3.bend as FIPS

Laws

law sha3_256_correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 9 · raw

@+bytes:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/sha3_256.sha3_256(bytes) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.sha3_256(bytes) : List<&2, U32>}

The digest of every byte list is the specification's.

law sha3_256_length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 14 · raw

@+bytes:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/sha3_256.sha3_256(bytes)) == 32n : Nat}

Every digest is 32 bytes.