LAWS.bend open laws/TODOs

raw source on the hub · import 0x48cee57f42dae6ba4c727fbf982cdd4d/LAWS.bend as LAWS

6 imports

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

Laws

law permutation_rounds provedin PROOF.bendsource · line 9 · raw

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

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

law digest_size provedin PROOF.bendsource · line 15 · raw

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

law capacity_rejection provedin PROOF.bendsource · line 19 · raw

@a:Array<U32> -> @+n:Nat -> @+capacity:U32 -> @invalid:{Nat.is_le(n, Nat.mul(4n, U32.to_nat(capacity))) == False{} : Bool} -> {0x48cee57f42dae6ba4c727fbf982cdd4d/src/keccak.sized(24n, n, (a, capacity)) == None{} : Maybe<&1, Array<U32>>}

law packed_sponge_correct provedin PROOF.bendsource · line 26 · raw

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

law ethereum_round_count provedin PROOF.bendsource · line 32 · raw

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

law ethereum_keccak256 provedin PROOF.bendsource · line 37 · raw

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