def finish_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/chacha8/rounds.bend:35

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A

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      {==}