[
  (builtins.bitXor 0 0)
  (builtins.bitXor 1 0)
  (builtins.bitXor 0 1)
  (builtins.bitXor 1 1)
  (builtins.bitXor 8 0)
  (builtins.bitXor 0 8)
  (builtins.bitXor 8 8)
  (builtins.bitXor 8 (builtins.add 4 4))
  (builtins.bitXor (builtins.add 4 4) 8)
  (builtins.bitXor (builtins.add 4 4) (builtins.add 4 4))
]