~/bend-docscommunity

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

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

5 imports
import Base
import ../../../../src/crypto/blake/blake2b/types.bend as T
import ../../../../src/crypto/blake/blake2b/compress.bend as F
import ../../../../src/crypto/blake/blake2b/blake2b.bend as I
import ../../../../spec/crypto/blake/blake2b.bend as S

Laws

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

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

The public BLAKE2b-512 API equals the RFC 7693 specification of spec/crypto/blake/blake2b.bend for every packed input array and every byte length: the same digest, or None for both when byte_length exceeds 4 * the array's capacity.

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

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.compress(h, t, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.compress(h, [0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w0, w1}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w2, w3}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w4, w5}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w6, w7}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w8, w9}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w10, w11}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w12, w13}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w14, w15}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w16, w17}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w18, w19}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w20, w21}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w22, w23}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w24, w25}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w26, w27}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w28, w29}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w30, w31}], t, False{}) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

The compression function F on a block that is not the last, for every chaining value h, counter t and message block.

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

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.compress_last(h, t, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.compress(h, [0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w0, w1}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w2, w3}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w4, w5}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w6, w7}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w8, w9}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w10, w11}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w12, w13}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w14, w15}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w16, w17}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w18, w19}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w20, w21}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w22, w23}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w24, w25}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w26, w27}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w28, w29}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w30, w31}], t, True{}) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

The compression function F on the last block, for every chaining value h, counter t and message block.

law digest_size openits proof in laws_crypto.bend does not pass the checker (fails)source · line 94 · 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}

Every digest is sixteen words (64 bytes).

law capacity_rejection openits proof in laws_crypto.bend does not pass the checker (fails)source · line 99 · 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>>}

Lengths past the array's capacity are rejected.