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

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/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 provedin main.bendsource · line 7 · raw

{0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/sha256.constants == 0xd9a2fae439ac7ff9e21e0853948f94fe/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 provedin main.bendsource · line 10 · raw

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

law digest_bytes_correct provedin main.bendsource · line 14 · raw

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

law sha256_bytes_correct provedin main.bendsource · line 18 · raw

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

law sha256_bytes_length provedin main.bendsource · line 22 · raw

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