;; Register bitness.
(defconstant +bitness+ 32)
 
(defun make-reg (reg-name bitness)
 "Make algebraic representation of a register (bits in descending majority)"
 (loop for i from (1- bitness) downto 0 collect
 (make-symbol (format nil "~A~A" reg-name i))))
 
(defun integer-to-reg (n &optional (pad-width +bitness+))
 "Generate algebraic represenation of the given integer n."
 (let* ((bits '())
 (integer-bitness (integer-length n))
 (pad-bitness (- pad-width integer-bitness)))
 (dotimes (index integer-bitness bits)
 (push (if (logbitp index n) 1 0) bits))
 ;; Append padding zeros, if required to make full width:
 (loop repeat pad-bitness do (push 0 bits))
 bits))
 
(defun RL11 (reg)
 "Rotate given register leftward by 11."
 (append
 (subseq reg 11)
 (subseq reg 0 11)))
 
(defmacro reg-xor (&rest regs)
 "Make algebraic representation of the xor of given registers."
 `(map 'list #'(lambda (&rest args) (cons 'xor args)) ,@regs))
 
;; Define the input registers
(defvar *A* (make-reg "a" +bitness+))
(defvar *B* (make-reg "b" +bitness+))
(defvar *C* (make-reg "c" +bitness+))
(defvar *D* (make-reg "d" +bitness+))
(defvar *E* (make-reg "e" +bitness+))
(defvar *F* (make-reg "f" +bitness+))
(defvar *G* (make-reg "g" +bitness+))
(defvar *H* (make-reg "h" +bitness+))
 
;; Serpent's 'goldenratio' turd
(defconstant +serpent-const+ #x9E3779B9)
 
;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; from serpent.ada: ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;
;; for I in 0..7 loop
;; W(-8+I) := Bytes_To_Word(K(4*I .. 4*I+3));
;; end loop;
;; for I in 0..131 loop
;; W(I) := Rotate_Left(W(I-8) xor W(I-5) xor W(I-3) xor W(I-1) xor
;; 16#9e3779b9# xor Unsigned_32(I), 11);
;; end loop;
 
(defun serp-co-recur (k)
 "Co-recursive helper"
 (if (< k 0)
 (serpent-recurrence k)
 (make-reg (format nil "W~A-" k) +bitness+)))
 
(defun serpent-recurrence (k)
 "Generate k-th term of the Serpent key-expander recurrence equation."
 (case k
 ;; The key terms:
 (-8 *A*) (-7 *B*) (-6 *C*) (-5 *D*) (-4 *E*) (-3 *F*) (-2 *G*) (-1 *H*)
 ;; Any other term:
 (t
 (RL11 (reg-xor
 (integer-to-reg (logxor +serpent-const+ k))
 (serp-co-recur (- k 8))
 (serp-co-recur (- k 5))
 (serp-co-recur (- k 3))
 (serp-co-recur (- k 1)))))))
 
(defun print-reg-w (w reg stream)
 "Print algebraic register as table."
 (let ((l (1- (length reg))))
 (loop for i from 0 upto l do
 (let* ((expr (nth (- l i) reg))
 (const (cadr expr))
 (terms (cddr expr)))
 (loop for clause in terms do
 (format stream " ~7A " clause))
 (format stream "~A --> [W~A-~2d]~%" const w i)))))
 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Print recurrence terms:
(with-open-file (stream "serpent_proofolade.txt"
 :direction :output
 :if-exists :overwrite
 :if-does-not-exist :create)
 (loop for k from 0 upto 131 do
 (progn
 (format stream "~%Serpent W(~A):~%" k)
 (print-reg-w k (serpent-recurrence k) stream))))
 
(quit)

Serpent W(8):
 W0-21 W3-21 W5-21 W7-21 1 --> [W8- 0]
 W0-22 W3-22 W5-22 W7-22 0 --> [W8- 1]
 W0-23 W3-23 W5-23 W7-23 0 --> [W8- 2]
 W0-24 W3-24 W5-24 W7-24 0 --> [W8- 3]
 W0-25 W3-25 W5-25 W7-25 1 --> [W8- 4]
 W0-26 W3-26 W5-26 W7-26 1 --> [W8- 5]
 W0-27 W3-27 W5-27 W7-27 1 --> [W8- 6]
 W0-28 W3-28 W5-28 W7-28 1 --> [W8- 7]
 W0-29 W3-29 W5-29 W7-29 0 --> [W8- 8]
 W0-30 W3-30 W5-30 W7-30 0 --> [W8- 9]
 W0-31 W3-31 W5-31 W7-31 1 --> [W8-10]
 W0-0 W3-0 W5-0 W7-0 1 --> [W8-11]
 W0-1 W3-1 W5-1 W7-1 0 --> [W8-12]
 W0-2 W3-2 W5-2 W7-2 0 --> [W8-13]
 W0-3 W3-3 W5-3 W7-3 0 --> [W8-14]
 W0-4 W3-4 W5-4 W7-4 1 --> [W8-15]
 W0-5 W3-5 W5-5 W7-5 1 --> [W8-16]
 W0-6 W3-6 W5-6 W7-6 0 --> [W8-17]
 W0-7 W3-7 W5-7 W7-7 1 --> [W8-18]
 W0-8 W3-8 W5-8 W7-8 1 --> [W8-19]
 W0-9 W3-9 W5-9 W7-9 0 --> [W8-20]
 W0-10 W3-10 W5-10 W7-10 0 --> [W8-21]
 W0-11 W3-11 W5-11 W7-11 1 --> [W8-22]
 W0-12 W3-12 W5-12 W7-12 1 --> [W8-23]
 W0-13 W3-13 W5-13 W7-13 1 --> [W8-24]
 W0-14 W3-14 W5-14 W7-14 1 --> [W8-25]
 W0-15 W3-15 W5-15 W7-15 0 --> [W8-26]
 W0-16 W3-16 W5-16 W7-16 1 --> [W8-27]
 W0-17 W3-17 W5-17 W7-17 1 --> [W8-28]
 W0-18 W3-18 W5-18 W7-18 1 --> [W8-29]
 W0-19 W3-19 W5-19 W7-19 0 --> [W8-30]
 W0-20 W3-20 W5-20 W7-20 1 --> [W8-31]

Serpent W(7):
 h21 W2-21 W4-21 W6-21 1 --> [W7- 0]
 h22 W2-22 W4-22 W6-22 0 --> [W7- 1]
 h23 W2-23 W4-23 W6-23 0 --> [W7- 2]
 h24 W2-24 W4-24 W6-24 0 --> [W7- 3]
 h25 W2-25 W4-25 W6-25 1 --> [W7- 4]
 h26 W2-26 W4-26 W6-26 1 --> [W7- 5]
 h27 W2-27 W4-27 W6-27 1 --> [W7- 6]
 h28 W2-28 W4-28 W6-28 1 --> [W7- 7]
 h29 W2-29 W4-29 W6-29 0 --> [W7- 8]
 h30 W2-30 W4-30 W6-30 0 --> [W7- 9]
 h31 W2-31 W4-31 W6-31 1 --> [W7-10]
 h0 W2-0 W4-0 W6-0 0 --> [W7-11]
 h1 W2-1 W4-1 W6-1 1 --> [W7-12]
 h2 W2-2 W4-2 W6-2 1 --> [W7-13]
 h3 W2-3 W4-3 W6-3 1 --> [W7-14]
 h4 W2-4 W4-4 W6-4 1 --> [W7-15]
 h5 W2-5 W4-5 W6-5 1 --> [W7-16]
 h6 W2-6 W4-6 W6-6 0 --> [W7-17]
 h7 W2-7 W4-7 W6-7 1 --> [W7-18]
 h8 W2-8 W4-8 W6-8 1 --> [W7-19]
 h9 W2-9 W4-9 W6-9 0 --> [W7-20]
 h10 W2-10 W4-10 W6-10 0 --> [W7-21]
 h11 W2-11 W4-11 W6-11 1 --> [W7-22]
 h12 W2-12 W4-12 W6-12 1 --> [W7-23]
 h13 W2-13 W4-13 W6-13 1 --> [W7-24]
 h14 W2-14 W4-14 W6-14 1 --> [W7-25]
 h15 W2-15 W4-15 W6-15 0 --> [W7-26]
 h16 W2-16 W4-16 W6-16 1 --> [W7-27]
 h17 W2-17 W4-17 W6-17 1 --> [W7-28]
 h18 W2-18 W4-18 W6-18 1 --> [W7-29]
 h19 W2-19 W4-19 W6-19 0 --> [W7-30]
 h20 W2-20 W4-20 W6-20 1 --> [W7-31]

Serpent W(6):
 g21 W1-21 W3-21 W5-21 1 --> [W6- 0]
 g22 W1-22 W3-22 W5-22 0 --> [W6- 1]
 g23 W1-23 W3-23 W5-23 0 --> [W6- 2]
 g24 W1-24 W3-24 W5-24 0 --> [W6- 3]
 g25 W1-25 W3-25 W5-25 1 --> [W6- 4]
 g26 W1-26 W3-26 W5-26 1 --> [W6- 5]
 g27 W1-27 W3-27 W5-27 1 --> [W6- 6]
 g28 W1-28 W3-28 W5-28 1 --> [W6- 7]
 g29 W1-29 W3-29 W5-29 0 --> [W6- 8]
 g30 W1-30 W3-30 W5-30 0 --> [W6- 9]
 g31 W1-31 W3-31 W5-31 1 --> [W6-10]
 g0 W1-0 W3-0 W5-0 1 --> [W6-11]
 g1 W1-1 W3-1 W5-1 1 --> [W6-12]
 g2 W1-2 W3-2 W5-2 1 --> [W6-13]
 g3 W1-3 W3-3 W5-3 1 --> [W6-14]
 g4 W1-4 W3-4 W5-4 1 --> [W6-15]
 g5 W1-5 W3-5 W5-5 1 --> [W6-16]
 g6 W1-6 W3-6 W5-6 0 --> [W6-17]
 g7 W1-7 W3-7 W5-7 1 --> [W6-18]
 g8 W1-8 W3-8 W5-8 1 --> [W6-19]
 g9 W1-9 W3-9 W5-9 0 --> [W6-20]
 g10 W1-10 W3-10 W5-10 0 --> [W6-21]
 g11 W1-11 W3-11 W5-11 1 --> [W6-22]
 g12 W1-12 W3-12 W5-12 1 --> [W6-23]
 g13 W1-13 W3-13 W5-13 1 --> [W6-24]
 g14 W1-14 W3-14 W5-14 1 --> [W6-25]
 g15 W1-15 W3-15 W5-15 0 --> [W6-26]
 g16 W1-16 W3-16 W5-16 1 --> [W6-27]
 g17 W1-17 W3-17 W5-17 1 --> [W6-28]
 g18 W1-18 W3-18 W5-18 1 --> [W6-29]
 g19 W1-19 W3-19 W5-19 0 --> [W6-30]
 g20 W1-20 W3-20 W5-20 1 --> [W6-31]
 
Serpent W(5):
 f21 W0-21 W2-21 W4-21 1 --> [W5- 0]
 f22 W0-22 W2-22 W4-22 0 --> [W5- 1]
 f23 W0-23 W2-23 W4-23 0 --> [W5- 2]
 f24 W0-24 W2-24 W4-24 0 --> [W5- 3]
 f25 W0-25 W2-25 W4-25 1 --> [W5- 4]
 f26 W0-26 W2-26 W4-26 1 --> [W5- 5]
 f27 W0-27 W2-27 W4-27 1 --> [W5- 6]
 f28 W0-28 W2-28 W4-28 1 --> [W5- 7]
 f29 W0-29 W2-29 W4-29 0 --> [W5- 8]
 f30 W0-30 W2-30 W4-30 0 --> [W5- 9]
 f31 W0-31 W2-31 W4-31 1 --> [W5-10]
 f0 W0-0 W2-0 W4-0 0 --> [W5-11]
 f1 W0-1 W2-1 W4-1 0 --> [W5-12]
 f2 W0-2 W2-2 W4-2 1 --> [W5-13]
 f3 W0-3 W2-3 W4-3 1 --> [W5-14]
 f4 W0-4 W2-4 W4-4 1 --> [W5-15]
 f5 W0-5 W2-5 W4-5 1 --> [W5-16]
 f6 W0-6 W2-6 W4-6 0 --> [W5-17]
 f7 W0-7 W2-7 W4-7 1 --> [W5-18]
 f8 W0-8 W2-8 W4-8 1 --> [W5-19]
 f9 W0-9 W2-9 W4-9 0 --> [W5-20]
 f10 W0-10 W2-10 W4-10 0 --> [W5-21]
 f11 W0-11 W2-11 W4-11 1 --> [W5-22]
 f12 W0-12 W2-12 W4-12 1 --> [W5-23]
 f13 W0-13 W2-13 W4-13 1 --> [W5-24]
 f14 W0-14 W2-14 W4-14 1 --> [W5-25]
 f15 W0-15 W2-15 W4-15 0 --> [W5-26]
 f16 W0-16 W2-16 W4-16 1 --> [W5-27]
 f17 W0-17 W2-17 W4-17 1 --> [W5-28]
 f18 W0-18 W2-18 W4-18 1 --> [W5-29]
 f19 W0-19 W2-19 W4-19 0 --> [W5-30]
 f20 W0-20 W2-20 W4-20 1 --> [W5-31]

Serpent W(4):
 e21 h21 W1-21 W3-21 1 --> [W4- 0]
 e22 h22 W1-22 W3-22 0 --> [W4- 1]
 e23 h23 W1-23 W3-23 0 --> [W4- 2]
 e24 h24 W1-24 W3-24 0 --> [W4- 3]
 e25 h25 W1-25 W3-25 1 --> [W4- 4]
 e26 h26 W1-26 W3-26 1 --> [W4- 5]
 e27 h27 W1-27 W3-27 1 --> [W4- 6]
 e28 h28 W1-28 W3-28 1 --> [W4- 7]
 e29 h29 W1-29 W3-29 0 --> [W4- 8]
 e30 h30 W1-30 W3-30 0 --> [W4- 9]
 e31 h31 W1-31 W3-31 1 --> [W4-10]
 e0 h0 W1-0 W3-0 1 --> [W4-11]
 e1 h1 W1-1 W3-1 0 --> [W4-12]
 e2 h2 W1-2 W3-2 1 --> [W4-13]
 e3 h3 W1-3 W3-3 1 --> [W4-14]
 e4 h4 W1-4 W3-4 1 --> [W4-15]
 e5 h5 W1-5 W3-5 1 --> [W4-16]
 e6 h6 W1-6 W3-6 0 --> [W4-17]
 e7 h7 W1-7 W3-7 1 --> [W4-18]
 e8 h8 W1-8 W3-8 1 --> [W4-19]
 e9 h9 W1-9 W3-9 0 --> [W4-20]
 e10 h10 W1-10 W3-10 0 --> [W4-21]
 e11 h11 W1-11 W3-11 1 --> [W4-22]
 e12 h12 W1-12 W3-12 1 --> [W4-23]
 e13 h13 W1-13 W3-13 1 --> [W4-24]
 e14 h14 W1-14 W3-14 1 --> [W4-25]
 e15 h15 W1-15 W3-15 0 --> [W4-26]
 e16 h16 W1-16 W3-16 1 --> [W4-27]
 e17 h17 W1-17 W3-17 1 --> [W4-28]
 e18 h18 W1-18 W3-18 1 --> [W4-29]
 e19 h19 W1-19 W3-19 0 --> [W4-30]
 e20 h20 W1-20 W3-20 1 --> [W4-31]
 
Serpent W(3):
 d21 g21 W0-21 W2-21 1 --> [W3- 0]
 d22 g22 W0-22 W2-22 0 --> [W3- 1]
 d23 g23 W0-23 W2-23 0 --> [W3- 2]
 d24 g24 W0-24 W2-24 0 --> [W3- 3]
 d25 g25 W0-25 W2-25 1 --> [W3- 4]
 d26 g26 W0-26 W2-26 1 --> [W3- 5]
 d27 g27 W0-27 W2-27 1 --> [W3- 6]
 d28 g28 W0-28 W2-28 1 --> [W3- 7]
 d29 g29 W0-29 W2-29 0 --> [W3- 8]
 d30 g30 W0-30 W2-30 0 --> [W3- 9]
 d31 g31 W0-31 W2-31 1 --> [W3-10]
 d0 g0 W0-0 W2-0 0 --> [W3-11]
 d1 g1 W0-1 W2-1 1 --> [W3-12]
 d2 g2 W0-2 W2-2 0 --> [W3-13]
 d3 g3 W0-3 W2-3 1 --> [W3-14]
 d4 g4 W0-4 W2-4 1 --> [W3-15]
 d5 g5 W0-5 W2-5 1 --> [W3-16]
 d6 g6 W0-6 W2-6 0 --> [W3-17]
 d7 g7 W0-7 W2-7 1 --> [W3-18]
 d8 g8 W0-8 W2-8 1 --> [W3-19]
 d9 g9 W0-9 W2-9 0 --> [W3-20]
 d10 g10 W0-10 W2-10 0 --> [W3-21]
 d11 g11 W0-11 W2-11 1 --> [W3-22]
 d12 g12 W0-12 W2-12 1 --> [W3-23]
 d13 g13 W0-13 W2-13 1 --> [W3-24]
 d14 g14 W0-14 W2-14 1 --> [W3-25]
 d15 g15 W0-15 W2-15 0 --> [W3-26]
 d16 g16 W0-16 W2-16 1 --> [W3-27]
 d17 g17 W0-17 W2-17 1 --> [W3-28]
 d18 g18 W0-18 W2-18 1 --> [W3-29]
 d19 g19 W0-19 W2-19 0 --> [W3-30]
 d20 g20 W0-20 W2-20 1 --> [W3-31]

Serpent W(2):
 c21 f21 h21 W1-21 1 --> [W2- 0]
 c22 f22 h22 W1-22 0 --> [W2- 1]
 c23 f23 h23 W1-23 0 --> [W2- 2]
 c24 f24 h24 W1-24 0 --> [W2- 3]
 c25 f25 h25 W1-25 1 --> [W2- 4]
 c26 f26 h26 W1-26 1 --> [W2- 5]
 c27 f27 h27 W1-27 1 --> [W2- 6]
 c28 f28 h28 W1-28 1 --> [W2- 7]
 c29 f29 h29 W1-29 0 --> [W2- 8]
 c30 f30 h30 W1-30 0 --> [W2- 9]
 c31 f31 h31 W1-31 1 --> [W2-10]
 c0 f0 h0 W1-0 1 --> [W2-11]
 c1 f1 h1 W1-1 1 --> [W2-12]
 c2 f2 h2 W1-2 0 --> [W2-13]
 c3 f3 h3 W1-3 1 --> [W2-14]
 c4 f4 h4 W1-4 1 --> [W2-15]
 c5 f5 h5 W1-5 1 --> [W2-16]
 c6 f6 h6 W1-6 0 --> [W2-17]
 c7 f7 h7 W1-7 1 --> [W2-18]
 c8 f8 h8 W1-8 1 --> [W2-19]
 c9 f9 h9 W1-9 0 --> [W2-20]
 c10 f10 h10 W1-10 0 --> [W2-21]
 c11 f11 h11 W1-11 1 --> [W2-22]
 c12 f12 h12 W1-12 1 --> [W2-23]
 c13 f13 h13 W1-13 1 --> [W2-24]
 c14 f14 h14 W1-14 1 --> [W2-25]
 c15 f15 h15 W1-15 0 --> [W2-26]
 c16 f16 h16 W1-16 1 --> [W2-27]
 c17 f17 h17 W1-17 1 --> [W2-28]
 c18 f18 h18 W1-18 1 --> [W2-29]
 c19 f19 h19 W1-19 0 --> [W2-30]
 c20 f20 h20 W1-20 1 --> [W2-31]

Serpent W(1):
 b21 e21 g21 W0-21 1 --> [W1- 0]
 b22 e22 g22 W0-22 0 --> [W1- 1]
 b23 e23 g23 W0-23 0 --> [W1- 2]
 b24 e24 g24 W0-24 0 --> [W1- 3]
 b25 e25 g25 W0-25 1 --> [W1- 4]
 b26 e26 g26 W0-26 1 --> [W1- 5]
 b27 e27 g27 W0-27 1 --> [W1- 6]
 b28 e28 g28 W0-28 1 --> [W1- 7]
 b29 e29 g29 W0-29 0 --> [W1- 8]
 b30 e30 g30 W0-30 0 --> [W1- 9]
 b31 e31 g31 W0-31 1 --> [W1-10]
 b0 e0 g0 W0-0 0 --> [W1-11]
 b1 e1 g1 W0-1 0 --> [W1-12]
 b2 e2 g2 W0-2 0 --> [W1-13]
 b3 e3 g3 W0-3 1 --> [W1-14]
 b4 e4 g4 W0-4 1 --> [W1-15]
 b5 e5 g5 W0-5 1 --> [W1-16]
 b6 e6 g6 W0-6 0 --> [W1-17]
 b7 e7 g7 W0-7 1 --> [W1-18]
 b8 e8 g8 W0-8 1 --> [W1-19]
 b9 e9 g9 W0-9 0 --> [W1-20]
 b10 e10 g10 W0-10 0 --> [W1-21]
 b11 e11 g11 W0-11 1 --> [W1-22]
 b12 e12 g12 W0-12 1 --> [W1-23]
 b13 e13 g13 W0-13 1 --> [W1-24]
 b14 e14 g14 W0-14 1 --> [W1-25]
 b15 e15 g15 W0-15 0 --> [W1-26]
 b16 e16 g16 W0-16 1 --> [W1-27]
 b17 e17 g17 W0-17 1 --> [W1-28]
 b18 e18 g18 W0-18 1 --> [W1-29]
 b19 e19 g19 W0-19 0 --> [W1-30]
 b20 e20 g20 W0-20 1 --> [W1-31]

Serpent W(0):
 a21 d21 f21 h21 1 --> [W0- 0]
 a22 d22 f22 h22 0 --> [W0- 1]
 a23 d23 f23 h23 0 --> [W0- 2]
 a24 d24 f24 h24 0 --> [W0- 3]
 a25 d25 f25 h25 1 --> [W0- 4]
 a26 d26 f26 h26 1 --> [W0- 5]
 a27 d27 f27 h27 1 --> [W0- 6]
 a28 d28 f28 h28 1 --> [W0- 7]
 a29 d29 f29 h29 0 --> [W0- 8]
 a30 d30 f30 h30 0 --> [W0- 9]
 a31 d31 f31 h31 1 --> [W0-10]
 a0 d0 f0 h0 1 --> [W0-11]
 a1 d1 f1 h1 0 --> [W0-12]
 a2 d2 f2 h2 0 --> [W0-13]
 a3 d3 f3 h3 1 --> [W0-14]
 a4 d4 f4 h4 1 --> [W0-15]
 a5 d5 f5 h5 1 --> [W0-16]
 a6 d6 f6 h6 0 --> [W0-17]
 a7 d7 f7 h7 1 --> [W0-18]
 a8 d8 f8 h8 1 --> [W0-19]
 a9 d9 f9 h9 0 --> [W0-20]
 a10 d10 f10 h10 0 --> [W0-21]
 a11 d11 f11 h11 1 --> [W0-22]
 a12 d12 f12 h12 1 --> [W0-23]
 a13 d13 f13 h13 1 --> [W0-24]
 a14 d14 f14 h14 1 --> [W0-25]
 a15 d15 f15 h15 0 --> [W0-26]
 a16 d16 f16 h16 1 --> [W0-27]
 a17 d17 f17 h17 1 --> [W0-28]
 a18 d18 f18 h18 1 --> [W0-29]
 a19 d19 f19 h19 0 --> [W0-30]
 a20 d20 f20 h20 1 --> [W0-31]