proofs/math/random/chacha8/rounds.bend

bend-collections-laws-math@1.0.0.0 · 53 lines · 6 definitions

1# Generated by tools/generators/chacha8rand_gen.py; do not edit.
2# The unrolled ChaCha8 pieces of src/math/random/chacha8/block.bend against
3# the list-based RFC 8439 / C2SP specification spec/math/random/chacha8rand.bend,
4# for every state and key: one double round (both sides symbolic in the
5# sixteen words, so the checker compares one double round at a time), the
6# initial state, the final additions with C2SP's subtractions, and the
7# four-block interleaving.
8import Base
9import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
10import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend as B
11import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as S
12import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
13
14# the state as the RFC list x[0..15]; like S.key_list on a key, it is stuck
15# on an abstract state, so the checker never unfolds rounds of symbolic
16# words it does not have to compare
17def vec(v: B.Vector) -> List<&2,U32>:
18  match v:
19    case B.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: [a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15]
20
21# one double round is RFC 8439's inner_block
22def dr_correct(+v: B.Vector) -> {vec(B.dr(v)) == S.double_round(vec(v)) : List<&2,U32>}:
23  match v:
24    case B.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
25
26def init_correct(+k: B.Key, +ctr: U32) -> {vec(B.init(k,ctr)) == S.initial(S.key_list(k),ctr) : List<&2,U32>}:
27  match k:
28    case B.K{k0,k1,k2,k3,k4,k5,k6,k7}: {==}
29
30# x + c - c = x
31def cancel(+x: U32, +c: U32) -> {U32.sub(U32.add(x,c),c) == x : U32}:
32  %A.comm(c,x) : {U32.sub(_,c) == x : U32}
33  A.add_sub(c,x)
34
35# the key words added back, C2SP's subtractions of the constants and the
36# counter, and the zero nonce words: the words the implementation keeps
37def finish_correct(+k: B.Key, +v: B.Vector, +ctr: U32) -> {vec(B.finish(k,v)) == S.subtract(S.add_words(vec(v),vec(B.init(k,ctr))),ctr) : List<&2,U32>}:
38  match k v:
39    case B.K{k0,k1,k2,k3,k4,k5,k6,k7} B.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}:
40      %Equal.sym(U32,U32.sub(U32.add(v0,1634760805),1634760805),v0,cancel(v0,1634760805)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [_,U32.sub(U32.add(v1,857760878),857760878),U32.sub(U32.add(v2,2036477234),2036477234),U32.sub(U32.add(v3,1797285236),1797285236),U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),U32.sub(U32.add(v12,ctr),ctr),U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
41      %Equal.sym(U32,U32.sub(U32.add(v1,857760878),857760878),v1,cancel(v1,857760878)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,_,U32.sub(U32.add(v2,2036477234),2036477234),U32.sub(U32.add(v3,1797285236),1797285236),U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),U32.sub(U32.add(v12,ctr),ctr),U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
42      %Equal.sym(U32,U32.sub(U32.add(v2,2036477234),2036477234),v2,cancel(v2,2036477234)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,_,U32.sub(U32.add(v3,1797285236),1797285236),U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),U32.sub(U32.add(v12,ctr),ctr),U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
43      %Equal.sym(U32,U32.sub(U32.add(v3,1797285236),1797285236),v3,cancel(v3,1797285236)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,_,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),U32.sub(U32.add(v12,ctr),ctr),U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
44      %Equal.sym(U32,U32.sub(U32.add(v12,ctr),ctr),v12,cancel(v12,ctr)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),_,U32.add(v13,0),U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
45      %Equal.sym(U32,U32.add(v13,0),v13,A.add_zero(v13)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,_,U32.add(v14,0),U32.add(v15,0)] : List<&2,U32>}
46      %Equal.sym(U32,U32.add(v14,0),v14,A.add_zero(v14)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,_,U32.add(v15,0)] : List<&2,U32>}
47      %Equal.sym(U32,U32.add(v15,0),v15,A.add_zero(v15)) : {[v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,v15] == [v0,v1,v2,v3,U32.add(v4,k0),U32.add(v5,k1),U32.add(v6,k2),U32.add(v7,k3),U32.add(v8,k4),U32.add(v9,k5),U32.add(v10,k6),U32.add(v11,k7),v12,v13,v14,_] : List<&2,U32>}
48      {==}
49
50# the interleaving is C2SP's permutation read as little-endian 64-bit words
51def interleave_correct(+a: B.Vector, +b: B.Vector, +c: B.Vector, +d: B.Vector) -> {B.interleave(a,b,c,d) == S.words64(S.interleave(16n,0n,vec(a),vec(b),vec(c),vec(d))) : List<&2,W.U64>}:
52  match a b c d:
53    case B.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15} B.V{b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15} B.V{c0,c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15} B.V{d0,d1,d2,d3,d4,d5,d6,d7,d8,d9,d10,d11,d12,d13,d14,d15}: {==}