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

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

3 imports

import Base
import ../../../src/crypto/sha/sha256.bend as SHA
import ../../../spec/crypto/sha.bend as FIPS

Laws

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

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.constants == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha.constants : List<&2, U32>}

These claims mention the actual public API and the complete independent spec. There are no arbitrary preprocessing functions, tables, or correctness premises.

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

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

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

@+ws:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.digest_bytes(ws) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha.digest_octets(ws) : List<&2, U32>}

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

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

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

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