proofs/crypto/sha3/conformance.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha3/conformance.bend as Conformance

Generated by tools/generators/sha3_gen.py; do not edit by hand.

7 imports

import Base
import ../../../src/crypto/keccak/types.bend as T
import ../../../src/crypto/keccak/permutation.bend as P
import ../../../src/crypto/sha3/core.bend as C
import ../../../spec/crypto/sha3.bend as F
import ../../../spec/crypto/keccak/permutation.bend as K
import ../keccak/permutation.bend as KP

Laws

law inject_correct provedsource · line 16 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+l0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> @+l16:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.of_lanes(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.xor_lanes(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.to_lanes(s), [l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16])) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law absorb_correct provedsource · line 42 · raw

@+ls:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane> -> @+rounds:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.absorb(ls, rounds, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.absorb(ls, rounds, s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law lanes_correct provedsource · line 92 · raw

@+bytes:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.lanes(bytes) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.lanes(bytes) : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.Lane>}

law tail_correct provedsource · line 119 · raw

@+q:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.tail(q) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.padding_bytes(q) : List<&2, U32>}

law suffix_correct provedsource · line 132 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.suffix(n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.padding(n) : List<&2, U32>}

law digest_correct provedsource · line 139 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.digest_bytes(s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.squeeze(s) : List<&2, U32>}

law digest_length provedsource · line 148 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.digest_bytes(s)) == 32n : Nat}

law keccak_correct provedsource · line 157 · raw

@+bytes:List<&2, U32> -> @+rounds:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.keccak(bytes, rounds) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.keccak(bytes, rounds) : List<&2, U32>}