~/bend-docscommunity

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

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

6 imports
import Base
import ../../../src/crypto/sha512/types.bend as T
import ../../../src/crypto/sha512/sha512.bend as SHA
import ../../../spec/crypto/sha512.bend as FIPS
import ../../../spec/lib/common.bend as C
import ./words.bend as Words

Laws

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

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

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

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

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

Every digest is 64 bytes.

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

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha512/words.value(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.add(a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(64n, Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha512/words.value(a), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha512/words.value(b))) : Nat}

The specification's word addition is addition modulo 2^64 (FIPS 180-4 section 3.2), with W{hi, lo} read as lo + 2^32 hi.