~/bend-docscommunity

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

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

10 imports
import Base
import ../../../../src/crypto/blake/blake3/types.bend as T
import ../../../../src/crypto/blake/blake3/blake3.bend as K
import ../../../lib/nat.bend as N
import ../../../../spec/lib/common.bend as SC
import ../../../../spec/crypto/blake/blake3.bend as S
import ./array.bend as A
import ./lists.bend as LS
import ./chunk.bend as CH
import ./tree.bend as TR

Laws

law fuse provedsource · line 135 · raw

@+n:Nat -> @+t:U32 -> @+index:U32 -> @+len:Nat -> @a:Array<U32> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.chunks(n, t, index, len, (a, s)) == run(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(n, t, index, len, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_at(n, t, index, len, a))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

Definitions

def run2 source · line 18 · raw

@rest:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out

The stack run over a list of outputs: every output but the last is pushed as a chaining value, the last one is pending.

def run source · line 23 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out

def init2 source · line 28 · raw

@rest:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out>

def last2 source · line 33 · raw

@rest:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out

def run2_split source · line 38 · raw

@+r:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {run2(r, s, x) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/tree.push_all(s, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/tree.cvs(init2(r, x))), last2(r, x)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def snoc2 source · line 43 · raw

@+r:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, init2(r, x), [last2(r, x)]) == x <> r : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out>}

def len_init2 source · line 48 · raw

@+r:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> @+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, init2(r, x)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, r) : Nat}

def run_tree_go source · line 53 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @+r:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/tree.push_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.StkNil{}, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/tree.cvs(init2(r, x))), last2(r, x)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, r), x <> r) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def run_tree source · line 59 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @+r:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> {run(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.StkNil{}, x <> r) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, x <> r), x <> r) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

A nonempty list of outputs: the stack run is the tree of height |list|.

def run_chunks source · line 65 · raw

@+n:Nat -> @+t:U32 -> @+index:U32 -> @+len:Nat -> @q:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out) -> {run(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.StkNil{}, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(n, t, index, len, q)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.tree(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(n, t, index, len, q)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(n, t, index, len, q)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

The specification's chunk list is never empty.

def base_run source · line 70 · raw

@+t:U32 -> @+index:U32 -> @+len:Nat -> @q:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out) -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> {run(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(0n, t, index, len, q)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.finish(s, Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out, q)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def run2_run source · line 74 · raw

@+p:Nat -> @+t:U32 -> @+index:U32 -> @+len:Nat -> @q:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out) -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> {run2(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(p, t, index, len, q), s, o) == run(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.push(s, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.out_cv(o)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(p, t, index, len, q)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def fuse_zero source · line 81 · raw

@+t:U32 -> @+index:U32 -> @+len:Nat -> @-a:Array<U32> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @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.chunks(0n, t, index, len, (a, s)) == run(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(0n, t, index, len, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_at(0n, t, index, len, a))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def fuse_step2 source · line 92 · raw

@+p:Nat -> @+t:U32 -> @+index:U32 -> @+len:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @-a:Array<U32> -> @+o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.Tree, x => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.thaw(x) : Array<U32>}> -> @rec:(@a2:Array<U32> -> @s2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.chunks(p, U32.inc(t), U32.add(index, 256), len, (a2, s2)) == run(s2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(p, U32.inc(t), U32.add(index, 256), len, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_at(p, U32.inc(t), U32.add(index, 256), len, a2))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.chunks(p, U32.inc(t), U32.add(index, 256), len, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.pushed(s, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/chunk.outcv((a, o)))) == run(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(1n+p, t, index, len, (a, o))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def fuse_step source · line 114 · raw

@+p:Nat -> @+t:U32 -> @+index:U32 -> @+len:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @q:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out) -> @rec:(@a2:Array<U32> -> @s2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.chunks(p, U32.inc(t), U32.add(index, 256), len, (a2, s2)) == run(s2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(p, U32.inc(t), U32.add(index, 256), len, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_at(p, U32.inc(t), U32.add(index, 256), len, a2))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.chunks(p, U32.inc(t), U32.add(index, 256), len, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.pushed(s, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/chunk.outcv(q))) == run(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(1n+p, t, index, len, q)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}

def fuse_one source · line 120 · raw

@+p:Nat -> @+t:U32 -> @+index:U32 -> @+len:Nat -> @-a:Array<U32> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.Tree, x => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.thaw(x) : Array<U32>}> -> @rec:(@a2:Array<U32> -> @s2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.Stack -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.chunks(p, U32.inc(t), U32.add(index, 256), len, (a2, s2)) == run(s2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(p, U32.inc(t), U32.add(index, 256), len, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_at(p, U32.inc(t), U32.add(index, 256), len, a2))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.chunks(1n+p, t, index, len, (a, s)) == run(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunks(1n+p, t, index, len, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.chunk_at(1n+p, t, index, len, a))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out}