~/bend-docscommunity

proofs/permutation.bend checks

raw source on the hub · import 0x48cee57f42dae6ba4c727fbf982cdd4d/proofs/permutation.bend as Permutation

4 imports
import Base
import ../src/types.bend as T
import ../src/permutation.bend as P
import ../spec/permutation.bend as S

Laws

law round_correct provedsource · line 6 · raw

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

law constants_correct provedsource · line 15 · raw

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

law pair_step provedsource · line 48 · raw

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

law single_step provedsource · line 58 · raw

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

law step_correct provedsource · line 66 · raw

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

law two_correct provedsource · line 76 · raw

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

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