| -- Braid-word surfaces used by the resource backend. | |
| namespace BraidCompilation | |
| structure BraidOp where | |
| sigma : Nat | |
| forward : Bool | |
| deriving Repr, DecidableEq | |
| def op (sigma : Nat) : BraidOp := { sigma := sigma, forward := true } | |
| def H : List BraidOp := [op 0, op 1, op 0, op 1, op 0] | |
| def X : List BraidOp := [op 0, op 0] | |
| def S : List BraidOp := [op 0, op 0] | |
| def CNOT : List BraidOp := [op 2, op 1, op 0, op 1, op 2] | |
| def CCX : List BraidOp := | |
| [op 4, op 5, op 4, op 5, op 4, | |
| op 2, op 3, op 4, op 2, op 3, op 4, | |
| op 4, op 5, op 4, op 5, op 4] | |
| def invertOp (b : BraidOp) : BraidOp := { b with forward := !b.forward } | |
| def invertWord (word : List BraidOp) : List BraidOp := | |
| word.reverse.map invertOp | |
| theorem cnot_braid_length : CNOT.length = 5 := by | |
| rfl | |
| theorem ccx_braid_length : CCX.length = 16 := by | |
| rfl | |
| end BraidCompilation | |