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

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

5 imports

import Base
import ../../../src/crypto/hash.bend as Hash
import ../../../spec/crypto/sha.bend as FIPS180
import ../../../spec/crypto/sha512.bend as FIPS180_512
import ../../../spec/crypto/sha3.bend as FIPS202

Laws

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

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

Each one-shot function is its standard's executable specification.

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

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

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

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

law Sha256.length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 23 · raw

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

Digest sizes: 32, 64 and 32 bytes.

law Sha512.length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 27 · raw

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

law Sha3_256.length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 31 · raw

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

law Incremental.sha256 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 37 · raw

@+chunks:List<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.new_sha256, chunks)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha256(List.concat(&2, U32, chunks)) : List<&2, U32>}

Incremental hashing equals one-shot hashing for every split of the input: the chunks, in order, digest to the hash of their concatenation.

law Incremental.sha512 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 41 · raw

@+chunks:List<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.new_sha512, chunks)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha512(List.concat(&2, U32, chunks)) : List<&2, U32>}

law Incremental.sha3_256 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 45 · raw

@+chunks:List<&2, List<&2, U32>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.new_sha3_256, chunks)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha3_256(List.concat(&2, U32, chunks)) : List<&2, U32>}

law Split.sha256 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 50 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.new_sha256, a), b)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha256(List.append(&2, U32, a, b)) : List<&2, U32>}

The two-chunk case, spelled with update.

law Split.sha512 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 55 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.new_sha512, a), b)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha512(List.append(&2, U32, a, b)) : List<&2, U32>}

law Split.sha3_256 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 60 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.digest(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.update(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.new_sha3_256, a), b)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha3_256(List.append(&2, U32, a, b)) : List<&2, U32>}