def block_correct

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

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

33# THEOREM: the implementation's block is C2SP's block ctr
34def block_correct(+k: B.Key, +ctr: U32) -> {R.vec(B.block(k, ctr)) == S.c2sp_block(S.key_list(k), ctr) : List<&2, U32>}:
35  +v = B.dr(B.dr(B.dr(B.dr(B.init(k, ctr)))))
36  Equal.trans(List<&2, U32>, R.vec(B.finish(k, v)), S.subtract(S.add_words(R.vec(v), R.vec(B.init(k, ctr))), ctr), S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), S.initial(S.key_list(k), ctr)), ctr),
37    R.finish_correct(k, v, ctr),
38    Equal.trans(List<&2, U32>, S.subtract(S.add_words(R.vec(v), R.vec(B.init(k, ctr))), ctr), S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), R.vec(B.init(k, ctr))), ctr), S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), S.initial(S.key_list(k), ctr)), ctr),
39      Equal.cong(List<&2, U32>, List<&2, U32>, x => S.subtract(S.add_words(x, R.vec(B.init(k, ctr))), ctr), R.vec(v), S.double_rounds(4n, S.initial(S.key_list(k), ctr)), rounds_correct(k, ctr)),
40      Equal.cong(List<&2, U32>, List<&2, U32>, x => S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), x), ctr), R.vec(B.init(k, ctr)), S.initial(S.key_list(k), ctr), R.init_correct(k, ctr))))