~/bend-docscommunity

proofs/crypto/sha512/words.bend checks

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

7 imports
import Base
import ../../../src/crypto/sha512/types.bend as T
import ../../../spec/crypto/sha512.bend as FIPS
import ../../../spec/lib/common.bend as C
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../math/typed/w64add.bend as W64A

Laws

law carry_bit provedsource · line 20 · raw

@+b:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.b32(b) == Bool.to_u32(b) : U32}

law add_value provedsource · line 31 · raw

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

Definitions

def value source · line 15 · raw

@w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> Nat