proofs/crypto/blake/blake3/proof.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/proof.bend as Proof

8 imports

import Base
import ../../../../src/crypto/blake/blake3/types.bend as T
import ../../../../src/crypto/blake/blake3/blake3.bend as K
import ../../../../spec/lib/common.bend as SC
import ../../../../spec/crypto/blake/blake3.bend as S
import ./array.bend as A
import ./compress.bend as P
import ./loop.bend as LP

Laws

law root_correct provedsource · line 21 · raw

@+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.root_cv(o) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.root(o) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV}

law unchecked_view provedsource · line 29 · raw

@-a:Array<U32> -> @+length:Nat -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.Tree, x => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.thaw(x) : Array<U32>}> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.unchecked(a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.hash(a, length) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV}

law digest_correct provedsource · line 54 · raw

@+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.digest(c) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.digest(c) : Array<U32>}

law checked_view provedsource · line 62 · raw

@-a:Array<U32> -> @+length:Nat -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.Tree, x => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.thaw(x) : Array<U32>}> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.checked(True{}, a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.checked(True{}, a, length) : Maybe<&1, Array<U32>>}

law checked_correct provedsource · line 79 · raw

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

law sized_correct provedsource · line 90 · raw

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

law blake3_correct provedsource · line 100 · raw

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

The public API: for every packed word array and every byte length.

law blake3_rejects provedsource · line 109 · 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/blake3/blake3.sized(n, (a, capacity)) == None{} : Maybe<&1, Array<U32>>}

Rejection: a length past 4 * capacity gives None.

law digest_size provedsource · line 120 · raw

@+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> {Pair.snd(Array<U32>, U32, Array.size(U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.digest(c))) == 8 : U32}

The digest is eight words.