source 2008.02.25 Hisil--Wong--Carter--Dawson, page 8
parameter k
assume k c = 1
assume Z2 = 1
compute A = X1
compute B = Y1
compute C = Z1 X2
compute D = Z1 Y2
compute E = A B
compute F = C D
compute G = E+F
compute H = E-F
compute J = (A-C)(B+D)-H
compute K = (A+D)(B+C)-G
compute X3 = G J
compute Y3 = H K
compute Z3 = k J K