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

raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/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 main.bend does not pass the checker (fails)source · line 7 · raw

{0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/sha256.constants == 0xe4067e0d858024083f36a7abe7281e89/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 main.bend does not pass the checker (fails)source · line 10 · raw

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

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

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

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

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

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

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