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. 8 import Base 9 import ../../../../src/math/u64.bend as W 10 import ../../../../src/math/random/chacha8/block.bend as B 11 import ../../../../spec/math/random/chacha8rand.bend as S 12 import ../../../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 17 def 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 22 def 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 26 def 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 31 def 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 37 def 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 51 def 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}: {==}