proofs/math/random/chacha8/block.bend

bend-collections-laws-math@1.0.0.0 · 54 lines · 5 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
3import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend as B
4import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as S
5import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/rounds.bend as R
6
7# The ChaCha8Rand block and group of src/math/random/chacha8/block.bend are
8# C2SP's (spec/math/random/chacha8rand.bend) for every key and counter.
9
10# n double rounds, the model of the implementation's dr(dr(dr(dr(x))))
11def drs(n: Nat, v: B.Vector) -> B.Vector:
12  match n:
13    case 0n:
14      v
15    case 1n+p:
16      drs(p, B.dr(v))
17
18def drs_correct(+n: Nat, +v: B.Vector) -> {R.vec(drs(n, v)) == S.double_rounds(n, R.vec(v)) : List<&2, U32>}:
19  match n:
20    case 0n:
21      {==}
22    case 1n+p:
23      Equal.trans(List<&2, U32>, R.vec(drs(p, B.dr(v))), S.double_rounds(p, R.vec(B.dr(v))), S.double_rounds(p, S.double_round(R.vec(v))),
24        drs_correct(p, B.dr(v)),
25        Equal.cong(List<&2, U32>, List<&2, U32>, x => S.double_rounds(p, x), R.vec(B.dr(v)), S.double_round(R.vec(v)), R.dr_correct(v)))
26
27# the eight rounds on the initial state
28def rounds_correct(+k: B.Key, +ctr: U32) -> {R.vec(B.dr(B.dr(B.dr(B.dr(B.init(k, ctr)))))) == S.double_rounds(4n, S.initial(S.key_list(k), ctr)) : List<&2, U32>}:
29  Equal.trans(List<&2, U32>, R.vec(drs(4n, B.init(k, ctr))), S.double_rounds(4n, R.vec(B.init(k, ctr))), S.double_rounds(4n, S.initial(S.key_list(k), ctr)),
30    drs_correct(4n, B.init(k, ctr)),
31    Equal.cong(List<&2, U32>, List<&2, U32>, x => S.double_rounds(4n, x), R.vec(B.init(k, ctr)), S.initial(S.key_list(k), ctr), R.init_correct(k, ctr)))
32
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))))
41
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)