~/bend-docscommunity

proofs/crypto/blake/blake2s/laws.bend open laws/TODOs

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

5 imports
import Base
import ../../../../src/crypto/blake/blake2s/types.bend as T
import ../../../../src/crypto/blake/blake2s/compress.bend as C
import ../../../../src/crypto/blake/blake2s/blake2s.bend as K
import ../../../../spec/crypto/blake/blake2s.bend as R

Laws

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

@a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.blake2s(a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.blake2s(a, length) : Maybe<&1, Array<U32>>}

The public API: for every packed input array and every byte length, the implementation returns exactly what the RFC 7693 specification returns (Some digest when length <= 4 * capacity, None otherwise).

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

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+m0:U32 -> @+m1:U32 -> @+m2:U32 -> @+m3:U32 -> @+m4:U32 -> @+m5:U32 -> @+m6:U32 -> @+m7:U32 -> @+m8:U32 -> @+m9:U32 -> @+m10:U32 -> @+m11:U32 -> @+m12:U32 -> @+m13:U32 -> @+m14:U32 -> @+m15:U32 -> @+t0:U32 -> @+t1:U32 -> @+last:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/compress.compress(h, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15, t0, t1, last) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.compress(10n, h, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], t0, t1, last) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

The unrolled compression function is F with r = 10 rounds, for every chaining value, message block, counter and final-block flag.

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

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> {Pair.snd(Array<U32>, U32, Array.size(U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.digest(s))) == 8 : U32}

law capacity_rejection openits proof in laws_crypto.bend does not pass the checker (fails)source · line 44 · 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/blake2s/blake2s.sized(n, (a, capacity)) == None{} : Maybe<&1, Array<U32>>}