~/bend-docscommunity

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

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

4 imports
import Base
import ../../../../src/crypto/blake/blake3/types.bend as T
import ../../../../src/crypto/blake/blake3/blake3.bend as K
import ../../../../spec/crypto/blake/blake3.bend as S

Laws

law read15_correct provedsource · line 13 · raw

@+index:U32 -> @+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 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read15(index, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(0n, index, 16, [w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read14_correct provedsource · line 37 · raw

@+index:U32 -> @+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 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read14(index, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(1n, index, 15, [w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read13_correct provedsource · line 60 · raw

@+index:U32 -> @+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 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read13(index, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(2n, index, 14, [w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read12_correct provedsource · line 82 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read12(index, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(3n, index, 13, [w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read11_correct provedsource · line 103 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read11(index, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(4n, index, 12, [w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read10_correct provedsource · line 123 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read10(index, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(5n, index, 11, [w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read9_correct provedsource · line 142 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read9(index, w0, w1, w2, w3, w4, w5, w6, w7, w8, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(6n, index, 10, [w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read8_correct provedsource · line 160 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read8(index, w0, w1, w2, w3, w4, w5, w6, w7, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(7n, index, 9, [w7, w6, w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read7_correct provedsource · line 177 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read7(index, w0, w1, w2, w3, w4, w5, w6, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(8n, index, 8, [w6, w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read6_correct provedsource · line 193 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read6(index, w0, w1, w2, w3, w4, w5, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(9n, index, 7, [w5, w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read5_correct provedsource · line 208 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read5(index, w0, w1, w2, w3, w4, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(10n, index, 6, [w4, w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read4_correct provedsource · line 222 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read4(index, w0, w1, w2, w3, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(11n, index, 5, [w3, w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read3_correct provedsource · line 235 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read3(index, w0, w1, w2, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(12n, index, 4, [w2, w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read2_correct provedsource · line 247 · raw

@+index:U32 -> @+w0:U32 -> @+w1:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read2(index, w0, w1, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(13n, index, 3, [w1, w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read1_correct provedsource · line 258 · raw

@+index:U32 -> @+w0:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read1(index, w0, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(14n, index, 2, [w0], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read0_correct provedsource · line 268 · raw

@+index:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read0(index, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.as_block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.gather(15n, index, 1, [], pair)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law read_block_correct provedsource · line 277 · raw

@a:Array<U32> -> @+index:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.read_block(a, index) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.read_block(a, index) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)}

law partial_low provedsource · line 285 · raw

@+w:U32 -> @+d:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.partial(w, d) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.low_bytes(w, Nat.min(4n, d)) : U32}

law mask_keep provedsource · line 298 · raw

@+w:U32 -> @+pos:Nat -> @+len:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.mask(w, pos, len) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.keep(w, pos, len) : U32}

law mask_block_correct provedsource · line 307 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block -> @+len:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.mask_block(b, len) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.zero_tail(b, len) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block}

law zero_tail_full provedsource · line 334 · raw

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

A full block keeps all 64 bytes.