def ap.trans

bend-osdev-aes@0.1.0.0 · PROOF.bend:1849

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

1849def ap.trans(+t00: U32, +t01: U32, +t02: U32, +t03: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t02, t03)), G.Gf8.add(G.Gf8.add(t10, t11), G.Gf8.add(t12, t13))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t22, t23)), G.Gf8.add(G.Gf8.add(t30, t31), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}:
1850  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t02, t03)), G.Gf8.add(G.Gf8.add(t10, t11), G.Gf8.add(t12, t13))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13))), ap.swap4(G.Gf8.add(t00, t01), G.Gf8.add(t02, t03), G.Gf8.add(t10, t11), G.Gf8.add(t12, t13))) : {G.Gf8.add(_, G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t22, t23)), G.Gf8.add(G.Gf8.add(t30, t31), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
1851  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t22, t23)), G.Gf8.add(G.Gf8.add(t30, t31), G.Gf8.add(t32, t33))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33))), ap.swap4(G.Gf8.add(t20, t21), G.Gf8.add(t22, t23), G.Gf8.add(t30, t31), G.Gf8.add(t32, t33))) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13))), _) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
1852  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))), G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))), ap.swap4(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) : {_ == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
1853  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t01, t11)), ap.swap4(t00, t01, t10, t11)) : {G.Gf8.add(G.Gf8.add(_, G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
1854  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31)), G.Gf8.add(G.Gf8.add(t20, t30), G.Gf8.add(t21, t31)), ap.swap4(t20, t21, t30, t31)) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t01, t11)), _), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
1855  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t01, t11)), G.Gf8.add(G.Gf8.add(t20, t30), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), ap.swap4(G.Gf8.add(t00, t10), G.Gf8.add(t01, t11), G.Gf8.add(t20, t30), G.Gf8.add(t21, t31))) : {G.Gf8.add(_, G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
1856  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t03, t13)), ap.swap4(t02, t03, t12, t13)) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(_, G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
1857  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)), G.Gf8.add(G.Gf8.add(t22, t32), G.Gf8.add(t23, t33)), ap.swap4(t22, t23, t32, t33)) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t03, t13)), _)) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
1858  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t03, t13)), G.Gf8.add(G.Gf8.add(t22, t32), G.Gf8.add(t23, t33))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33))), ap.swap4(G.Gf8.add(t02, t12), G.Gf8.add(t03, t13), G.Gf8.add(t22, t32), G.Gf8.add(t23, t33))) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), _) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
1859  {==}