def group_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/chacha8/block.bend:42

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/rounds.bend as R

42# THEOREM: the implementation's group is C2SP's four permuted blocks ctr ..
43# ctr + 3, read as little-endian 64-bit words
44def group_correct(+k: B.Key, +ctr: U32) -> {B.group(k, ctr) == S.words64(S.group(S.key_list(k), ctr)) : List<&2, W.U64>}:
45  +b0 = B.block(k, ctr)
46  +b1 = B.block(k, U32.add(ctr, 1))
47  +b2 = B.block(k, U32.add(ctr, 2))
48  +b3 = B.block(k, U32.add(ctr, 3))
49  +kl = S.key_list(k)
50  %block_correct(k, ctr) : {B.group(k, ctr) == S.words64(S.interleave(16n, 0n, _, S.c2sp_block(kl, U32.add(ctr, 1)), S.c2sp_block(kl, U32.add(ctr, 2)), S.c2sp_block(kl, U32.add(ctr, 3)))) : List<&2, W.U64>}
51  %block_correct(k, U32.add(ctr, 1)) : {B.group(k, ctr) == S.words64(S.interleave(16n, 0n, R.vec(b0), _, S.c2sp_block(kl, U32.add(ctr, 2)), S.c2sp_block(kl, U32.add(ctr, 3)))) : List<&2, W.U64>}
52  %block_correct(k, U32.add(ctr, 2)) : {B.group(k, ctr) == S.words64(S.interleave(16n, 0n, R.vec(b0), R.vec(b1), _, S.c2sp_block(kl, U32.add(ctr, 3)))) : List<&2, W.U64>}
53  %block_correct(k, U32.add(ctr, 3)) : {B.group(k, ctr) == S.words64(S.interleave(16n, 0n, R.vec(b0), R.vec(b1), R.vec(b2), _)) : List<&2, W.U64>}
54  R.interleave_correct(b0, b1, b2, b3)