def xor_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/blamka.bend:119

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as S

119# X XOR Y, row by row.
120def xor_correct(+x: A.Block, +y: A.Block) -> {I.xor(x, y) == S.xor(x, y) : A.Block}:
121  match x y:
122    case A.B{+x0,+x1,+x2,+x3,+x4,+x5,+x6,+x7} A.B{+y0,+y1,+y2,+y3,+y4,+y5,+y6,+y7}:
123      %Equal.sym(T.State, I.xs(x0, y0), S.xor_state(x0, y0), xs_correct(x0, y0)) : {A.B{_, I.xs(x1, y1), I.xs(x2, y2), I.xs(x3, y3), I.xs(x4, y4), I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
124      %Equal.sym(T.State, I.xs(x1, y1), S.xor_state(x1, y1), xs_correct(x1, y1)) : {A.B{S.xor_state(x0, y0), _, I.xs(x2, y2), I.xs(x3, y3), I.xs(x4, y4), I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
125      %Equal.sym(T.State, I.xs(x2, y2), S.xor_state(x2, y2), xs_correct(x2, y2)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), _, I.xs(x3, y3), I.xs(x4, y4), I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
126      %Equal.sym(T.State, I.xs(x3, y3), S.xor_state(x3, y3), xs_correct(x3, y3)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), _, I.xs(x4, y4), I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
127      %Equal.sym(T.State, I.xs(x4, y4), S.xor_state(x4, y4), xs_correct(x4, y4)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), S.xor_state(x3, y3), _, I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
128      %Equal.sym(T.State, I.xs(x5, y5), S.xor_state(x5, y5), xs_correct(x5, y5)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), S.xor_state(x3, y3), S.xor_state(x4, y4), _, I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
129      %Equal.sym(T.State, I.xs(x6, y6), S.xor_state(x6, y6), xs_correct(x6, y6)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), S.xor_state(x3, y3), S.xor_state(x4, y4), S.xor_state(x5, y5), _, I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
130      %Equal.sym(T.State, I.xs(x7, y7), S.xor_state(x7, y7), xs_correct(x7, y7)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), S.xor_state(x3, y3), S.xor_state(x4, y4), S.xor_state(x5, y5), S.xor_state(x6, y6), _} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
131      {==}