~/bend-docscommunity

proofs/crypto/blake/blake2b/api.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/api.bend as Api

3 imports
import Base
import ../../../../src/crypto/blake/blake2b/types.bend as T
import ../../../../src/crypto/blake/blake2b/blake2b.bend as I

Laws

law digest_size provedsource · line 5 · raw

@h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> {Pair.snd(Array<U32>, U32, Array.size(U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.digest(h))) == 16 : U32}

law capacity_gate provedsource · line 13 · raw

@a:Array<U32> -> @+n:Nat -> @+capacity:U32 -> @invalid:{Nat.is_le(n, Nat.mul(4n, U32.to_nat(capacity))) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.sized(n, (a, capacity)) == None{} : Maybe<&1, Array<U32>>}