proofs/math/random/chacha8/rounds.bend source
proofs/math/random/chacha8/rounds.bend on the hub · documented module
# Generated by tools/generators/chacha8rand_gen.py; do not edit.# The unrolled ChaCha8 pieces of src/math/random/chacha8/block.bend against# the list-based RFC 8439 / C2SP specification spec/math/random/chacha8rand.bend,# for every state and key: one double round (both sides symbolic in the# sixteen words, so the checker compares one double round at a time), the# initial state, the final additions with C2SP's subtractions, and the# four-block interleaving.import Baseimport ../../../../src/math/u64.bend as Wimport ../../../../src/math/random/chacha8/block.bend as Bimport ../../../../spec/math/random/chacha8rand.bend as Simport ../../../lib/u32alg.bend as A# the state as the RFC list x[0..15]; like S.key_list on a key, it is stuck# on an abstract state, so the checker never unfolds rounds of symbolic# words it does not have to comparedef vec(v: B.Vector) -> List<&2,U32>: match v: 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]# one double round is RFC 8439's inner_blockdef dr_correct(+v: B.Vector) -> {vec(B.dr(v)) == S.double_round(vec(v)) : List<&2,U32>}: match v: case B.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}def init_correct(+k: B.Key, +ctr: U32) -> {vec(B.init(k,ctr)) == S.initial(S.key_list(k),ctr) : List<&2,U32>}: match k: case B.K{k0,k1,k2,k3,k4,k5,k6,k7}: {==}# x + c - c = xdef cancel(+x: U32, +c: U32) -> {U32.sub(U32.add(x,c),c) == x : U32}: %A.comm(c,x) : {U32.sub(_,c) == x : U32} A.add_sub(c,x)# the key words added back, C2SP's subtractions of the constants and the# counter, and the zero nonce words: the words the implementation keepsdef 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>}: match k v: 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}: %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} {==}# the interleaving is C2SP's permutation read as little-endian 64-bit wordsdef 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>}: match a b c d: 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}: {==}