~/bend-docscommunity

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

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

8 imports
import Base
import ../../../../src/crypto/blake/blake3/types.bend as T
import ../../../../src/crypto/blake/blake3/compress.bend as C
import ../../../../src/crypto/blake/blake3/blake3.bend as K
import ../../../../spec/crypto/blake/blake3.bend as S
import ./compress.bend as P
import ./read.bend as R
import ./array.bend as A

Laws

law compress_full provedsource · line 20 · raw

@+cv:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block -> @+t:U32 -> @+flags:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/compress.compress(cv, b, t, 64, flags) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.compress(cv, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.zero_tail(b, 64n), t, 64, flags) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV}

A full (64-byte) block: the implementation compresses the raw block, the specification the block truncated to 64 bytes.

law last_step provedsource · line 33 · raw

@+p:Nat -> @+t:U32 -> @+index:U32 -> @+flags:U32 -> @+len:Nat -> @+cv:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @-a:Array<U32> -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.Tree, x => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.thaw(x) : Array<U32>}> -> @recurse:(@c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @q:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.last_go(p, t, U32.add(index, 16), 0, len, c, q) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_blocks(p, t, U32.add(index, 16), 0, len, c, q) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out)}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.last_go(1n+p, t, index, flags, len, cv, (a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_blocks(1n+p, t, index, flags, len, cv, (a, b)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out)}

law last_base provedsource · line 64 · raw

@+t:U32 -> @+index:U32 -> @+flags:U32 -> @+len:Nat -> @+cv:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @-a:Array<U32> -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.last_go(0n, t, index, flags, len, cv, (a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_blocks(0n, t, index, flags, len, cv, (a, b)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out)}

law last_go_correct provedsource · line 78 · raw

@+n:Nat -> @+t:U32 -> @+index:U32 -> @+flags:U32 -> @+len:Nat -> @+cv:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.last_go(n, t, index, flags, len, cv, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_blocks(n, t, index, flags, len, cv, pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out)}

law full_step provedsource · line 96 · raw

@+p:Nat -> @+t:U32 -> @+index:U32 -> @+flags:U32 -> @+cv:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @-a:Array<U32> -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.Tree, x => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.thaw(x) : Array<U32>}> -> @recurse:(@c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @q:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.full_go(p, t, U32.add(index, 16), 0, c, q) == outcv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_blocks(p, t, U32.add(index, 16), 0, 64n, c, q)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV)}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.full_go(1n+p, t, index, flags, cv, (a, b)) == outcv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_blocks(1n+p, t, index, flags, 64n, cv, (a, b))) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV)}

law full_base provedsource · line 126 · raw

@+t:U32 -> @+index:U32 -> @+flags:U32 -> @+cv:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @-a:Array<U32> -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.full_go(0n, t, index, flags, cv, (a, b)) == outcv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_blocks(0n, t, index, flags, 64n, cv, (a, b))) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV)}

law full_go_correct provedsource · line 138 · raw

@+n:Nat -> @+t:U32 -> @+index:U32 -> @+flags:U32 -> @+cv:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.full_go(n, t, index, flags, cv, pair) == outcv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_blocks(n, t, index, flags, 64n, cv, pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV)}

law full_chunk_view provedsource · line 155 · raw

@-a:Array<U32> -> @+t:U32 -> @+index:U32 -> @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.full_chunk(a, t, index) == outcv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk(a, t, index, 1024n)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV)}

law full_chunk_correct provedsource · line 174 · raw

@a:Array<U32> -> @+t:U32 -> @+index:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.full_chunk(a, t, index) == outcv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk(a, t, index, 1024n)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV)}

law last_chunk_view provedsource · line 183 · raw

@-a:Array<U32> -> @+t:U32 -> @+index:U32 -> @+len: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.last_chunk(a, t, index, len) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk(a, t, index, len) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out)}

law last_chunk_correct provedsource · line 203 · raw

@a:Array<U32> -> @+t:U32 -> @+index:U32 -> @+len:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.last_chunk(a, t, index, len) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk(a, t, index, len) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out)}

Definitions

def outcv source · line 14 · raw

@q:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out) -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV)