proofs/crypto/keccak/laws.bend open laws/TODOs

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/laws.bend as Laws

6 imports

import Base
import ../../../src/crypto/keccak/types.bend as T
import ../../../src/crypto/keccak/permutation.bend as P
import ../../../spec/crypto/keccak/permutation.bend as S
import ../../../src/crypto/keccak/keccak.bend as K
import ../../../spec/crypto/keccak/main.bend as Sponge

Laws

law permutation_rounds openits proof in laws_crypto.bend does not pass the checker (fails)source · line 9 · raw

@+n:Nat -> @+i:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/permutation.rounds(n, i, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/permutation.rounds(n, i, s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

Universal permutation refinement; instantiating n=24 and i=0 gives Keccak-f[1600].

law digest_size openits proof in laws_crypto.bend does not pass the checker (fails)source · line 15 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> {Pair.snd(Array<U32>, U32, Array.size(U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.digest(s))) == 8 : U32}

law capacity_rejection openits proof in laws_crypto.bend does not pass the checker (fails)source · line 19 · 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/keccak/keccak.sized(24n, n, (a, capacity)) == None{} : Maybe<&1, Array<U32>>}

law packed_sponge_correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 26 · raw

@+r:Nat -> @a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.keccak256_rounds(r, a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.keccak256_rounds(r, a, length) : Maybe<&1, Array<U32>>}

law ethereum_round_count openits proof in laws_crypto.bend does not pass the checker (fails)source · line 32 · raw

@a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.keccak256(a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.keccak256_rounds(24n, a, length) : Maybe<&1, Array<U32>>}

law ethereum_keccak256 openits proof in laws_crypto.bend does not pass the checker (fails)source · line 37 · raw

@a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.keccak256(a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.keccak256_rounds(24n, a, length) : Maybe<&1, Array<U32>>}