proofs/crypto/blake/blake2s/bytes.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend as Bytes

Generated by tools/generators/blake2s_gen.py; do not edit. Bytes and words: the specification reassembles block words from little-endian bytes and zero-pads the last block byte by byte; the implementation reads whole words and masks the last partial word. The bit-level facts are proven on the 32 Bool digits of a U32.

3 imports

import Base
import ../../../../src/crypto/blake/blake2s/blake2s.bend as K
import ../../../../spec/crypto/blake/blake2s.bend as R

Laws

law bits32 provedsource · line 11 · raw

@-y0:Bool -> @-y1:Bool -> @-y2:Bool -> @-y3:Bool -> @-y4:Bool -> @-y5:Bool -> @-y6:Bool -> @-y7:Bool -> @-y8:Bool -> @-y9:Bool -> @-y10:Bool -> @-y11:Bool -> @-y12:Bool -> @-y13:Bool -> @-y14:Bool -> @-y15:Bool -> @-y16:Bool -> @-y17:Bool -> @-y18:Bool -> @-y19:Bool -> @-y20:Bool -> @-y21:Bool -> @-y22:Bool -> @-y23:Bool -> @-y24:Bool -> @-y25:Bool -> @-y26:Bool -> @-y27:Bool -> @-y28:Bool -> @-y29:Bool -> @-y30:Bool -> @-y31:Bool -> @-z0:Bool -> @-z1:Bool -> @-z2:Bool -> @-z3:Bool -> @-z4:Bool -> @-z5:Bool -> @-z6:Bool -> @-z7:Bool -> @-z8:Bool -> @-z9:Bool -> @-z10:Bool -> @-z11:Bool -> @-z12:Bool -> @-z13:Bool -> @-z14:Bool -> @-z15:Bool -> @-z16:Bool -> @-z17:Bool -> @-z18:Bool -> @-z19:Bool -> @-z20:Bool -> @-z21:Bool -> @-z22:Bool -> @-z23:Bool -> @-z24:Bool -> @-z25:Bool -> @-z26:Bool -> @-z27:Bool -> @-z28:Bool -> @-z29:Bool -> @-z30:Bool -> @-z31:Bool -> @e0:{y0 == z0 : Bool} -> @e1:{y1 == z1 : Bool} -> @e2:{y2 == z2 : Bool} -> @e3:{y3 == z3 : Bool} -> @e4:{y4 == z4 : Bool} -> @e5:{y5 == z5 : Bool} -> @e6:{y6 == z6 : Bool} -> @e7:{y7 == z7 : Bool} -> @e8:{y8 == z8 : Bool} -> @e9:{y9 == z9 : Bool} -> @e10:{y10 == z10 : Bool} -> @e11:{y11 == z11 : Bool} -> @e12:{y12 == z12 : Bool} -> @e13:{y13 == z13 : Bool} -> @e14:{y14 == z14 : Bool} -> @e15:{y15 == z15 : Bool} -> @e16:{y16 == z16 : Bool} -> @e17:{y17 == z17 : Bool} -> @e18:{y18 == z18 : Bool} -> @e19:{y19 == z19 : Bool} -> @e20:{y20 == z20 : Bool} -> @e21:{y21 == z21 : Bool} -> @e22:{y22 == z22 : Bool} -> @e23:{y23 == z23 : Bool} -> @e24:{y24 == z24 : Bool} -> @e25:{y25 == z25 : Bool} -> @e26:{y26 == z26 : Bool} -> @e27:{y27 == z27 : Bool} -> @e28:{y28 == z28 : Bool} -> @e29:{y29 == z29 : Bool} -> @e30:{y30 == z30 : Bool} -> @e31:{y31 == z31 : Bool} -> {U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{z0, WCon{z1, WCon{z2, WCon{z3, WCon{z4, WCon{z5, WCon{z6, WCon{z7, WCon{z8, WCon{z9, WCon{z10, WCon{z11, WCon{z12, WCon{z13, WCon{z14, WCon{z15, WCon{z16, WCon{z17, WCon{z18, WCon{z19, WCon{z20, WCon{z21, WCon{z22, WCon{z23, WCon{z24, WCon{z25, WCon{z26, WCon{z27, WCon{z28, WCon{z29, WCon{z30, WCon{z31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}

Two words are equal when their digits are.

law or1 proved
Also proved in bend-mathlib as bool.or_false: `import bend-mathlib@0.7.2.0/bool.bend as MBool`, then `MBool.or_false`.
source · line 145 · raw

@+x:Bool -> {Bool.or(x, False{}) == x : Bool}

law or2 provedsource · line 154 · raw

@+x:Bool -> {Bool.or(Bool.or(x, False{}), False{}) == x : Bool}

law or3 provedsource · line 163 · raw

@+x:Bool -> {Bool.or(Bool.or(Bool.or(x, False{}), False{}), False{}) == x : Bool}

law full provedsource · line 172 · raw

@+w:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.word(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 2n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 3n)) == w : U32}

law part3 provedsource · line 181 · raw

@+w:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.word(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 2n), 0) == U32.and(16777215, w) : U32}

law part2 provedsource · line 190 · raw

@+w:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.word(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 1n), 0, 0) == U32.and(65535, w) : U32}

law part1 provedsource · line 199 · raw

@+w:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.word(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.byte(w, 0n), 0, 0, 0) == U32.and(255, w) : U32}

law pad_word_correct provedsource · line 212 · raw

@+w:U32 -> @+i:Nat -> @+len:Nat -> {kept(w, i, len) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w, i, len) : U32}

law words_serialize provedsource · line 229 · raw

@+ws:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.words(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.serialize(ws)) == ws : List<&2, U32>}

Whole blocks: reassembling the serialized words gives the words back.

law words_pad provedsource · line 250 · raw

@+ws:List<&2, U32> -> @+i:Nat -> @+len:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.words(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.pad(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.serialize(ws), i, len)) == masked(ws, i, len) : List<&2, U32>}

Definitions

def kept source · line 209 · raw

@+w:U32 -> @+i:Nat -> @+len:Nat -> U32

The bytes at message offsets i..i+3 of one word, zeroed from offset len on.

def masked source · line 245 · raw

@ws:List<&2, U32> -> @+i:Nat -> @+len:Nat -> List<&2, U32>

The last block: the implementation masks word j with pad_word(w, i + 4j, len).