proofs/crypto/keccak/permutation.bend checks

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

4 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

Laws

law round_correct provedsource · line 6 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+rc:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/permutation.round(s, rc) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/permutation.round(s, rc) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law constants_correct provedsource · line 15 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/permutation.constant(n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/permutation.constant(n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane}

law pair_step provedsource · line 48 · raw

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

law single_step provedsource · line 58 · raw

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

law step_correct provedsource · line 66 · raw

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

law two_correct provedsource · line 76 · raw

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

law rounds_correct provedsource · line 89 · 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}