packages feed

symplectic-chp (empty) → 0.1.0.0

raw patch · 48 files changed

+4707/−0 lines, 48 filesdep +QuickCheckdep +basedep +containers

Dependencies added: QuickCheck, base, containers, deepseq, directory, filepath, finite-typelits, hspec, hspec-discover, mtl, primitive, random, stim-parser, symplectic-chp, transformers, vector, vector-sized

Files

+ CHANGELOG.md view
@@ -0,0 +1,86 @@+# Revision history for symplectic-chp++## 0.1.0.0 -- 2026-04-06++### Major Features++* **Symplectic Geometry Foundation**: Complete implementation of CHP simulator through the lens of symplectic geometry, revealing that Aaronson & Gottesman's CHP algorithm is a computational realization of the Symplectic Basis Theorem.++* **Mathematical Hierarchy**: Type class hierarchy encoding the geometric structure:+  - `Group` → `SymplecticGroup` → `AbelianLagrangianCorrespondence`+  - `SymplecticVectorSpace` → `IsotropicSubSpace` → `LagrangianSubSpace` → `SymplecticBasisTheorem`++* **Type-Safe Tableau**: Compile-time guarantees via GADTs and type-level naturals:+  - Dimensional checking with `Vector n` and `Finite n`+  - O(1) indexing with bounds guarantees+  - Zero-cost abstractions (< 5% runtime overhead)++### STIM Circuit Support++* **Parser Integration**: Full STIM circuit file parsing via `stim-parser` library+* **Supported Gates**: H, S, CNOT, X, Y, Z, CZ, SWAP, SQRT_Z, S_DAG, XCZ, ZCX, ZCZ, H_XZ+* **Gate Decomposition**: Automatic decomposition of non-native gates:+  - X = H·S·S·H+  - Y = S·X·S³+  - Z = S·S+  - CZ = H(t)·CNOT(c,t)·H(t)+  - SWAP = CNOT(a,b)·CNOT(b,a)·CNOT(a,b)+* **Measurements**: Z-basis (M/MZ), X-basis (MX), Y-basis (MY)+* **Multi-target Gates**: Support for `H 0 1 2`, `CNOT 0 1 2 3` syntax+* **Command-line Tool**: `symplectic-chp` executable with options:+  - `--seed N` for reproducible measurements+  - `--no-tableau` to hide tableau output+  - `-v` for verbose mode++### Bug Fixes++* **S Gate Phase Fix**: Corrected phase update in S gate to properly handle Y→-X transformation (was adding 0 phase, should add +1)+* **Phase Convention**: Stabilizer phases now correctly reflect canonical form (-Z instead of +iZ)++### Test Suite++* **68 Total Tests**:+  - 58 Haskell unit tests (symplectic properties, gate composition, measurement correctness)+  - 10 STIM circuit integration tests+* **Test Circuits**: bell-state, ghz-state, single-hadamard, stabilizer-cycle, cz-gate, swap-gate, multi-target, y-measurement, phase-gate, unsupported-rx+* **Mathematical Derivations**: Each test circuit includes `.derive.md` with step-by-step tableau evolution++### Documentation++* **Implementation Guide** (`doc/implement.md`): Complete mathematical hierarchy documentation+* **STIM Parser Implementation** (`doc/stim-parse-impl.md`): Real implementation documentation+* **Performance Analysis** (`doc/overhead.md`): Abstraction cost analysis+* **Theory Blog** (`doc/symplectic-blog-intuitive.md`): Intuitive explanation of symplectic geometry++### Formal Verification++* **Agda Formalization**: All test expectations derived from [symplectic-pauli](https://github.com/overshiki/symplectic-pauli) Agda proofs+* Machine-checked proofs of:+  - Symplectic Basis Theorem+  - Fundamental Correspondence (Pauli commutation ⟺ symplectic form)+  - All 10 circuit examples verified in Agda++---++## Pre-release History++### 2026-03 - Initial Development++* Core CHP simulator implementation with symplectic geometry foundation+* Type-safe vector implementation using `vector-sized`+* Basic gate support: H, S, CNOT+* Tableau operations: evolution, measurement++### 2026-03 - Mathematical Abstraction++* Refactored to use geometric hierarchy (Group, SymplecticGroup, etc.)+* Added `Clifford` monad for circuit composition+* Property-based testing with QuickCheck++### 2026-04 - STIM Integration++* Added STIM circuit file support+* Gate decomposition for X, Y, Z, CZ, SWAP+* Multi-target gate syntax+* Comprehensive test suite with derivations+* Bug fix for S gate phase calculation
+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2026 overshiki++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ README.md view
@@ -0,0 +1,261 @@+# Symplectic-CHP++A Haskell implementation of the CHP clifford simulator, **through the lens of symplectic geometry** with **type-safe, fixed-length vectors**, **higher-order mathematical abstractions**, and **minimal runtime overhead**.++## Overview++What if the CHP simulator isn't just an algorithm, but a **computational realization of the Symplectic Basis Theorem**?++This package reveals that Aaronson & Gottesman's CHP algorithm is actually doing symplectic linear algebra over 𝔽₂. The "tableau" is really a **symplectic basis**—a pair of transverse Lagrangian subspaces satisfying the elegant duality condition ω(Dᵢ, Sⱼ) = δᵢⱼ.++We encode this mathematical structure in Haskell's type system, achieving:+- **Compile-time guarantees** that your tableau is valid+- **Zero-cost abstractions** via GHC optimization+- **Mathematical clarity** where code mirrors geometric structure++> **Why Haskell?** This level of abstraction—encoding theorems as type classes, enforcing geometric invariants at compile time—is uniquely enabled by Haskell's expressive type system. The composition of dependent types, higher-kinded polymorphism, and type families makes such elegant encoding of mathematical structures possible.++## What Makes This Special?++### The Symplectic Basis Theorem, in Code++The CHP tableau **is** a symplectic basis:++```haskell+-- | The Symplectic Basis Theorem: {e₁,...,eₙ, f₁,...,fₙ} with ω(eᵢ,fⱼ) = δᵢⱼ+data Tableau (n :: Nat) v where+  Tableau ::+    { stabLagrangian   :: Lagrangian n v   -- S = {e₁,...,eₙ}+    , destabLagrangian :: Lagrangian n v   -- D = {f₁,...,fₙ}+    } -> Tableau n v++instance SymplecticBasisTheorem Tableau n v where+  firstLagrangian  = stabLagrangian+  secondLagrangian = destabLagrangian+```++The type system enforces the theorem's three conditions:+1. Stabilizers are isotropic: ω(Sᵢ, Sⱼ) = 0+2. Destabilizers are isotropic: ω(Dᵢ, Dⱼ) = 0+3. **Duality**: ω(Dᵢ, Sⱼ) = δᵢⱼ++### A Hierarchy of Mathematical Structures++Our type classes mirror the geometric hierarchy:++```+Group g+  └─ SymplecticGroup g v         -- group + symplectic structure+        ├─ Pauli (concrete)+        └─ AbelianLagrangianCorrespondence g n v+              └─ Maximal abelian  ⟷  Lagrangian++SymplecticVectorSpace v+  └─ IsotropicSubSpace s n v+        └─ LagrangianSubSpace s n v+              └─ SymplecticBasisTheorem s n v+                    └─ Tableau n v+```++The code *is* the mathematics.++## Mathematical Soundness: Formally Verified++The mathematical foundations of this implementation have been **machine-checked** in the [symplectic-pauli](https://github.com/overshiki/symplectic-pauli) Agda formalization project.++### What Does This Mean?++Every theorem underlying this codebase has been formally proven:++| Theorem | Status | Agda Proof |+|---------|--------|------------|+| **Symplectic Basis Theorem** | ✅ Complete | `symplecticBasisTheorem` |+| **Fundamental Correspondence** | ✅ Complete | Pauli commutation ⟺ symplectic form |+| **Tableau as Symplectic Basis** | ✅ Complete | Duality conditions verified |+| **All Circuit Examples** | ✅ Verified | 10/10 test circuits proven correct |++The Agda formalization translates our Haskell type class hierarchy into dependent type theory, providing **compile-time proof** that:+- Stabilizers are isotropic (ω(Sᵢ, Sⱼ) = 0)+- Destabilizers are isotropic (ω(Dᵢ, Dⱼ) = 0)  +- Duality holds (ω(Dᵢ, Sⱼ) = δᵢⱼ)+- Gate conjugations preserve the symplectic form+- Measurement outcomes match quantum mechanical predictions++> **Why this matters**: While Haskell gives us runtime verification via `verifyDuality`, Agda provides **mathematical certainty** at the type level. The test expectations in this repository are derived from these formal proofs.++### Minimal Overhead, Maximum Safety++The mathematical rigor of our haskell chp implementation comes with **< 5% runtime overhead**. GHC's optimizer eliminates abstraction costs through inlining, while `Vector`-based storage improves cache locality over traditional lists.++Type-level naturals (`Vector n`, `Finite n`) give us:+- Compile-time dimensional checking+- O(1) indexing with bounds guarantees+- No out-of-bounds errors at runtime++## Quick Start++### Library Usage++```haskell+-- Create a Bell state+bellCircuit :: Clifford Bool+bellCircuit = do+  gate (Local (Hadamard 0))     -- H ⊗ I+  gate (CNOT 0 1)                -- CNOT 0→1+  measurePauli (Pauli 3 0 0)     -- Measure X⊗X (should be +1)++-- Run it+main = do+  (tab, outcome) <- runWith 2 bellCircuit+  print outcome  -- True (+1 eigenvalue)+```++### STIM Circuit Files++The package includes a command-line tool to simulate [STIM](https://github.com/quantumlib/Stim) circuit files:++```bash+# Build and run+cabal build+cabal run symplectic-chp -- circuit.stim+```++Create a STIM circuit file (e.g., `bell.stim`):++```+# Bell state preparation+H 0+CNOT 0 1+M 0 1+```++Run the simulation:++```bash+$ cabal run symplectic-chp -- bell.stim++========================================+  CHP Simulation Results+========================================++Measurements performed: 2+Measurement outcomes:+  M0: +1 (|0⟩ or |+⟩)+  M1: +1 (|0⟩ or |+⟩)++Number of qubits: 2+Tableau valid: True++Stabilizers (generators of the stabilizer group):+  S0: +Z+  S1: +ZZ++Destabilizers (dual to stabilizers):+  D0: +XX+  D1: +IX+```++#### Supported STIM Features++| Feature | Status |+|---------|--------|+| **Gates** | H, S, CNOT, CZ, X, Y, Z, SWAP, SQRT_Z (S), S_DAG |+| **Measurements** | M (Z-basis), MX (X-basis), MY (Y-basis), MZ (Z-basis) |+| **Gates (decomposed)** | CZ, X, Y, Z, SWAP are decomposed into H/S/CNOT |++#### Unsupported Features (will report error)++- Non-Clifford gates (T, RX, RY, RZ, SQRT_X, etc.)+- Reset operations (R, MR, MRX, etc.)+- Pauli product measurements (MPP)+- Noise channels (X_ERROR, DEPOLARIZE1, etc.)+- REPEAT blocks+- Annotations (QUBIT_COORDS, DETECTOR, etc.)++#### Command-Line Options++```bash+symplectic-chp [OPTIONS] <input.stim>++Options:+  -h, --help         Show help message+  -v                 Enable verbose output+  --seed N           Use specific random seed for reproducibility+  --no-tableau       Don't show final tableau+```++#### Example: GHZ State++```+# ghz.stim+H 0+CNOT 0 1+CNOT 0 2+M 0 1 2+```++```bash+$ cabal run symplectic-chp -- ghz.stim+```++#### Test Circuits++Example circuits are available in `data/stim-circuits/`:++```bash+# List available test circuits+ls data/stim-circuits/*.stim++# Run a test circuit+cabal run symplectic-chp -- data/stim-circuits/bell-state.stim+```++Each circuit includes:+- `.stim` - The circuit file+- `.expected` - Expected results for automated testing+- `.derive.md` - Mathematical derivation of the circuit's behavior++## Learn More++- **[Theory Blog](https://overshiki.github.io/symplectic-blog-intuitive/)** — Why the Pauli group is symplectic+- **[Implementation Guide](doc/implement.md)** — The complete mathematical hierarchy+- **[Performance Analysis](doc/overhead.md)** — Why the abstractions are free+- **[STIM Parser Implementation](doc/stim-parse-impl.md)** — STIM circuit file parsing and simulation+- **[Agda Formalization](https://github.com/overshiki/symplectic-pauli)** — Machine-checked proofs of all theorems (symplectic-pauli)++## Testing++### Haskell Test Suite++```bash+cabal test+```++All **68 tests** pass:+- **58 unit tests** — verifying symplectic form properties, tableau validity, gate composition, and measurement correctness+- **10 integration tests** — STIM circuit files testing Bell states, GHZ states, gate decompositions, and error handling+++### Test Circuits++Example STIM circuits are provided in `data/stim-circuits/`:++| Circuit | Description |+|---------|-------------|+| `bell-state.stim` | Bell state \|Φ⁺⟩ preparation |+| `ghz-state.stim` | GHZ state preparation |+| `swap-gate.stim` | SWAP gate decomposition |+| `stabilizer-cycle.stim` | X gate via HSSH decomposition |+| `unsupported-rx.stim` | Error handling for non-Clifford gates |++The test suite automatically runs these circuits and verifies their outputs against expected results.++## References++- Aaronson & Gottesman, "Improved Simulation of Stabilizer Circuits," *Phys. Rev. A* 70, 052328 (2004)+- Artin, *Geometric Algebra* (symplectic groups)+- Gosson, *Symplectic Geometry and Quantum Mechanics*++## License++MIT License
+ app/CHPCircuit.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}++-- | Intermediate representation for CHP circuits translated from STIM.+-- This module defines a simple IR that bridges the gap between STIM AST+-- and the symplectic-chp simulator.+module CHPCircuit+  ( CHPCircuit(..)+  , CHPOperation(..)+  , emptyCircuit+  , addGate+  , addMeasure+  , circuitFromOps+  ) where++import Data.Bits (setBit, testBit)+import Data.Word (Word64)++import SymplecticCHP (Pauli(..), SymplecticGate(..), LocalSymplectic(..))++-- | A CHP circuit is a sequence of operations on qubits.+-- We track the number of qubits and the sequence of operations.+data CHPCircuit = CHPCircuit+  { numQubits :: Int+  , operations :: [CHPOperation]+  } deriving (Show)++-- | A single operation in a CHP circuit.+-- Either a Clifford gate or a Pauli measurement.+data CHPOperation+  = GateOp SymplecticGate+  | MeasureOp Pauli Int  -- ^ Pauli operator and measurement result index+  deriving (Show)++-- | Create an empty circuit for n qubits.+emptyCircuit :: Int -> CHPCircuit+emptyCircuit n = CHPCircuit n []++-- | Add a gate operation to a circuit.+addGate :: SymplecticGate -> CHPCircuit -> CHPCircuit+addGate g circ = circ { operations = operations circ ++ [GateOp g] }++-- | Add a measurement operation to a circuit.+addMeasure :: Pauli -> Int -> CHPCircuit -> CHPCircuit+addMeasure p idx circ = circ { operations = operations circ ++ [MeasureOp p idx] }++-- | Create a circuit from a list of operations.+-- Infers qubit count from operations.+circuitFromOps :: [CHPOperation] -> CHPCircuit+circuitFromOps ops = CHPCircuit n ops+  where+    n = maximum $ 0 : concatMap opQubits ops+    +    opQubits (GateOp g) = gateQubits g+    opQubits (MeasureOp p _) = pauliQubits p+    +    gateQubits (SymplecticCHP.Local (SymplecticCHP.Hadamard q)) = [q]+    gateQubits (SymplecticCHP.Local (SymplecticCHP.Phase q)) = [q]+    gateQubits (SymplecticCHP.CNOT c t) = [c, t]+    +    pauliQubits (Pauli x z _) = +      filter (testBitWord x) [0..63] ++ filter (testBitWord z) [0..63]+    testBitWord w i = (fromIntegral w :: Integer) `div` (2^i) `mod` 2 == 1
+ app/CLI.hs view
@@ -0,0 +1,144 @@+{-# LANGUAGE LambdaCase #-}++-- | Command-line interface for the STIM-to-CHP simulator.+-- Handles argument parsing, file I/O, and error reporting.+module CLI+  ( Config(..)+  , parseArgs+  , readStimFile+  , formatError+  , printUsage+  ) where++import System.Environment (getArgs)+import System.Exit (exitFailure)+import System.IO (hPutStrLn, stderr)++import StimParser.Expr (Stim)+import StimParser.Parse (parseStim)+import StimParser.ParseUtils (run)++import StimToCHP (TranslationError(..))++-- | Configuration for the simulator.+data Config = Config+  { inputFile :: FilePath+  , verbose :: Bool+  , showTableau :: Bool+  , seed :: Maybe Int  -- ^ Optional random seed for reproducibility+  } deriving (Show)++-- | Default configuration.+defaultConfig :: Config+defaultConfig = Config+  { inputFile = ""+  , verbose = False+  , showTableau = True+  , seed = Nothing+  }++-- | Parse command-line arguments.+parseArgs :: IO Config+parseArgs = getArgs >>= \case+  [] -> do+    printUsage+    exitFailure+    +  ["-h"] -> do+    printUsage+    exitFailure+    +  ["--help"] -> do+    printUsage+    exitFailure+    +  ["-v", file] -> return $ defaultConfig { inputFile = file, verbose = True }+  [file, "-v"] -> return $ defaultConfig { inputFile = file, verbose = True }+  +  ["--seed", s, file] -> +    case reads s of+      [(n, "")] -> return $ defaultConfig { inputFile = file, seed = Just n }+      _ -> do+        hPutStrLn stderr $ "Error: Invalid seed: " ++ s+        exitFailure+        +  [file, "--seed", s] -> +    case reads s of+      [(n, "")] -> return $ defaultConfig { inputFile = file, seed = Just n }+      _ -> do+        hPutStrLn stderr $ "Error: Invalid seed: " ++ s+        exitFailure+  +  ["--no-tableau", file] -> +    return $ defaultConfig { inputFile = file, showTableau = False }+  +  [file, "--no-tableau"] -> +    return $ defaultConfig { inputFile = file, showTableau = False }+  +  [file] -> return $ defaultConfig { inputFile = file }+  +  args -> do+    hPutStrLn stderr $ "Error: Unknown arguments: " ++ unwords args+    printUsage+    exitFailure++-- | Print usage information.+printUsage :: IO ()+printUsage = do+  putStrLn "STIM-to-CHP Simulator"+  putStrLn ""+  putStrLn "Usage: symplectic-chp [OPTIONS] <input.stim>"+  putStrLn ""+  putStrLn "Options:"+  putStrLn "  -h, --help         Show this help message"+  putStrLn "  -v                 Enable verbose output"+  putStrLn "  --seed N           Use specific random seed for measurements"+  putStrLn "  --no-tableau       Don't show final tableau"+  putStrLn ""+  putStrLn "Examples:"+  putStrLn "  symplectic-chp circuit.stim"+  putStrLn "  symplectic-chp -v circuit.stim"+  putStrLn "  symplectic-chp --seed 42 circuit.stim"++-- | Read and parse a STIM file.+-- Prepends "!!!Start " as required by the stim-parser.+readStimFile :: FilePath -> IO Stim+readStimFile path = do+  content <- readFile path+  -- stim-parser requires "!!!Start " prefix+  let prefixed = "!!!Start " ++ content+  return $ run parseStim prefixed++-- | Format a translation error for display.+formatError :: TranslationError -> String+formatError = \case+  UnsupportedGate gateType ->+    "Unsupported gate: " ++ show gateType ++ "\n" +++    "This gate is not a Clifford gate or is not yet implemented."+    +  UnsupportedMeasure measureType ->+    "Unsupported measurement: " ++ show measureType ++ "\n" +++    "Only single-qubit Pauli measurements (M, MX, MY, MZ) are supported."+    +  UnsupportedNoise noiseType ->+    "Unsupported noise: " ++ show noiseType ++ "\n" +++    "Noise channels are not supported by CHP simulator."+    +  UnsupportedGpp gppType ->+    "Unsupported Pauli product operation: " ++ show gppType ++ "\n" +++    "Pauli product measurements (MPP) are not yet supported."+    +  UnsupportedAnnotation annType ->+    "Unsupported annotation: " ++ show annType ++ "\n" +++    "Annotations like QUBIT_COORDS, DETECTOR, etc. are not supported."+    +  UnsupportedRepeat ->+    "REPEAT blocks are not supported.\n" +++    "Please unroll loops manually in your STIM file."+    +  OddCNOTTargets qubits ->+    "Invalid CNOT: odd number of targets (" ++ show (length qubits) ++ ")\n" +++    "CNOT requires an even number of targets: control1 target1 control2 target2 ..."+    +  EmptyCircuit ->+    "Empty circuit or no qubits found."
+ app/Main.hs view
@@ -0,0 +1,66 @@+{-# LANGUAGE LambdaCase #-}++-- | Main entry point for the STIM-to-CHP simulator.+-- +-- This executable parses STIM circuit files and simulates them using+-- the CHP Clifford simulator via symplectic geometry.+--+-- Supported STIM features:+--   - Clifford gates: H, S, CNOT, CZ, X, Y, Z, SWAP+--   - Measurements: M, MX, MY, MZ+--+-- Unsupported features (will report error):+--   - Non-Clifford gates (T, RX, RY, RZ, etc.)+--   - Noise channels+--   - Reset operations+--   - Pauli product measurements (MPP)+--   - Repeat blocks+--   - Annotations+module Main where++import System.Exit (exitFailure)+import System.IO (hPutStrLn, stderr)++import CHPCircuit (CHPCircuit(..))+import qualified CLI+import qualified Simulator+import StimToCHP (translateStim)++main :: IO ()+main = do+  -- Parse command-line arguments+  config <- CLI.parseArgs+  +  let path = CLI.inputFile config+  +  -- Step 1: Read and parse the STIM file+  whenVerbose config $ putStrLn $ "Reading STIM file: " ++ path+  stim <- CLI.readStimFile path+  whenVerbose config $ putStrLn "Successfully parsed STIM file"+  +  -- Step 2: Translate to CHP circuit+  whenVerbose config $ putStrLn "Translating to CHP circuit..."+  case translateStim stim of+    Left err -> do+      hPutStrLn stderr $ "Translation error:\n" ++ CLI.formatError err+      exitFailure+      +    Right circuit -> do+      whenVerbose config $ do+        putStrLn $ "Circuit has " ++ show (numQubits circuit) ++ " qubit(s)"+        putStrLn $ "Circuit has " ++ show (length (operations circuit)) ++ " operation(s)"+      +      -- Step 3: Run simulation+      whenVerbose config $ putStrLn "Running simulation..."+      result <- case CLI.seed config of+        Nothing -> Simulator.runCHPCircuit circuit+        Just s -> Simulator.runCHPCircuitWithSeed s circuit+      +      -- Step 4: Print results+      if CLI.showTableau config+        then Simulator.printResults result+        else putStrLn $ "Measurements: " ++ show (Simulator.measurementOutcomes result)++-- | Print message only in verbose mode.+whenVerbose :: CLI.Config -> IO () -> IO ()+whenVerbose config action = if CLI.verbose config then action else return ()
+ app/Simulator.hs view
@@ -0,0 +1,162 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- | Simulation runner for CHP circuits.+-- Executes translated circuits using the symplectic-chp simulator.+module Simulator+  ( runCHPCircuit+  , runCHPCircuitWithSeed+  , SimulationResult(..)+  , printResults+  ) where++import Control.Monad (foldM)+import System.Random (randomIO)++import SymplecticCHP+  ( Clifford+  , SomeTableau(..)+  , SymplecticGate+  , Pauli(..)+  , gate+  , measurePauli+  , runWith+  , getTableau+  , nQubitsSome+  , rowsSome+  , stabilizerSome+  , destabilizerSome+  , isValidSome+  )++import CHPCircuit (CHPCircuit(..), CHPOperation(..))++-- | Result of simulating a CHP circuit.+data SimulationResult = SimulationResult+  { finalTableau :: SomeTableau+  , measurementOutcomes :: [Bool]+  , measurementCount :: Int+  }++-- | Run a CHP circuit simulation.+-- Returns the final tableau and all measurement outcomes.+runCHPCircuit :: CHPCircuit -> IO SimulationResult+runCHPCircuit circuit = do+  -- Use random seed from IO+  seed <- randomIO+  runCHPCircuitWithSeed seed circuit++-- | Run a CHP circuit with a specific random seed (for reproducibility).+runCHPCircuitWithSeed :: Int -> CHPCircuit -> IO SimulationResult+runCHPCircuitWithSeed seed circuit = do+  let n = numQubits circuit+  (tableau, outcomes) <- runWith n (runOperations (operations circuit))+  return $ SimulationResult+    { finalTableau = tableau+    , measurementOutcomes = reverse outcomes  -- Reverse to get chronological order+    , measurementCount = length outcomes+    }++-- | Run a list of operations in the Clifford monad.+-- Collects measurement outcomes.+runOperations :: [CHPOperation] -> Clifford [Bool]+runOperations ops = foldM step [] ops+  where+    step :: [Bool] -> CHPOperation -> Clifford [Bool]+    step acc (GateOp g) = do+      gate g+      return acc+    step acc (MeasureOp p idx) = do+      result <- measurePauli p+      return (result : acc)++-- ============================================================================+-- Output Formatting+-- ============================================================================++-- | Print simulation results in a human-readable format.+printResults :: SimulationResult -> IO ()+printResults result = do+  putStrLn "========================================"+  putStrLn "  CHP Simulation Results"+  putStrLn "========================================"+  putStrLn ""+  +  -- Print measurement outcomes+  putStrLn $ "Measurements performed: " ++ show (measurementCount result)+  if measurementCount result > 0+    then do+      putStrLn "Measurement outcomes:"+      mapM_ (\(i, outcome) -> +        putStrLn $ "  M" ++ show i ++ ": " ++ showOutcome outcome) +        (zip [0..] (measurementOutcomes result))+    else putStrLn "No measurements performed."+  +  putStrLn ""+  +  -- Print tableau info+  let tab = finalTableau result+  putStrLn $ "Number of qubits: " ++ show (nQubitsSome tab)+  putStrLn $ "Tableau valid: " ++ show (isValidSome tab)+  +  putStrLn ""+  putStrLn "Stabilizers (generators of the stabilizer group):"+  printStabilizers tab+  +  putStrLn ""+  putStrLn "Destabilizers (dual to stabilizers):"+  printDestabilizers tab++-- | Format a measurement outcome (+1 or -1 eigenvalue).+showOutcome :: Bool -> String+showOutcome True  = "+1 (|0⟩ or |+⟩)"+showOutcome False = "-1 (|1⟩ or |-⟩)"++-- | Print stabilizer generators.+printStabilizers :: SomeTableau -> IO ()+printStabilizers (SomeTableau tab) = go 0+  where+    n = nQubitsSome (SomeTableau tab)+    go i+      | i >= n = return ()+      | otherwise = case stabilizerSome (SomeTableau tab) i of+          Just p -> do+            putStrLn $ "  S" ++ show i ++ ": " ++ showPauli p+            go (i + 1)+          Nothing -> go (i + 1)++-- | Print destabilizer generators.+printDestabilizers :: SomeTableau -> IO ()+printDestabilizers (SomeTableau tab) = go 0+  where+    n = nQubitsSome (SomeTableau tab)+    go i+      | i >= n = return ()+      | otherwise = case destabilizerSome (SomeTableau tab) i of+          Just p -> do+            putStrLn $ "  D" ++ show i ++ ": " ++ showPauli p+            go (i + 1)+          Nothing -> go (i + 1)++-- | Format a Pauli operator for display.+showPauli :: Pauli -> String+showPauli (Pauli x z phase) = +  let phaseStr = case phase `mod` 4 of+        0 -> "+"+        1 -> "+i"+        2 -> "-"+        3 -> "-i"+        _ -> "?"+      n = max (bitLength x) (bitLength z)+      n' = if n == 0 then 1 else n+      ops = [showSinglePauli (testBit x i) (testBit z i) | i <- [0..n'-1]]+  in phaseStr ++ concat ops+  where+    bitLength 0 = 0+    bitLength w = floor (logBase 2 (fromIntegral w)) + 1+    testBit w i = (w `div` (2^i)) `mod` 2 == 1+    +    showSinglePauli False False = "I"+    showSinglePauli True  False = "X"+    showSinglePauli False True  = "Z"+    showSinglePauli True  True  = "Y"
+ app/StimToCHP.hs view
@@ -0,0 +1,326 @@+{-# LANGUAGE LambdaCase #-}++-- | Translation from STIM AST to CHP circuit representation.+-- This module handles the conversion of stim-parser's AST into+-- operations that can be executed by the symplectic-chp simulator.+module StimToCHP+  ( TranslationError(..)+  , translateStim+  , translateGate+  , translateMeasure+  , countQubits+  ) where++import Data.Bits (setBit)+import Data.Word (Word64)+import qualified Data.Set as Set++import StimParser.Expr hiding (Pauli(..))++import qualified SymplecticCHP as CHP++import CHPCircuit (CHPCircuit(..), CHPOperation(..))++-- | Errors that can occur during translation from STIM to CHP.+data TranslationError+  = UnsupportedGate GateTy+  | UnsupportedMeasure MeasureTy+  | UnsupportedNoise NoiseTy+  | UnsupportedGpp GppTy+  | UnsupportedAnnotation AnnTy+  | UnsupportedRepeat+  | OddCNOTTargets [Q]  -- ^ CNOT requires even number of targets+  | EmptyCircuit+  deriving (Show)++-- | Translate a STIM AST into a CHP circuit.+-- Returns Left if the circuit contains unsupported features.+translateStim :: Stim -> Either TranslationError CHPCircuit+translateStim stim = do+  ops <- collectOperations stim+  let n = countQubits stim+  if n == 0+    then Left EmptyCircuit+    else Right $ CHPCircuit n ops++-- | Collect all operations from a STIM AST (flattening nested structures).+collectOperations :: Stim -> Either TranslationError [CHPOperation]+collectOperations = go 0+  where+    -- go tracks the next measurement index+    go :: Int -> Stim -> Either TranslationError [CHPOperation]+    go _ (StimList items) = concat <$> mapM (go 0) items+    go _idx (StimG gate) = do+      gates <- translateGate gate+      return $ map GateOp gates+    go idx (StimM measure) = do+      pauli <- translateMeasure measure+      return [MeasureOp pauli idx]+    go _ (StimNoise noise) = Left $ UnsupportedNoise (getNoiseType noise)+    go _ (StimGpp gpp) = Left $ UnsupportedGpp (getGppType gpp)+    go _ (StimAnn ann) = Left $ UnsupportedAnnotation (getAnnType ann)+    go _ (StimRepeat _ _) = Left UnsupportedRepeat++    getNoiseType (NoiseNormal ty _ _ _ _) = ty+    getNoiseType (NoiseE ty _ _ _) = ty+    +    getGppType (Gpp ty _ _ _) = ty+    +    getAnnType (Ann ty _ _ _) = ty++-- | Translate a STIM gate to a list of CHP symplectic gates.+-- May decompose gates into sequences of H, S, and CNOT.+translateGate :: Gate -> Either TranslationError [CHP.SymplecticGate]+translateGate (Gate gateType _ qubits) =+  case gateType of+    -- Directly supported gates+    H -> Right $ map (CHP.Local . CHP.Hadamard . qubitIndex) qubits+    S -> Right $ map (CHP.Local . CHP.Phase . qubitIndex) qubits+    CNOT -> translateCNOT qubits+    I -> Right []  -- Identity is a no-op+    +    -- Gates requiring decomposition+    X -> Right $ concatMap decomposeX qubits+    Y -> Right $ concatMap decomposeY qubits+    Z -> Right $ concatMap decomposeZ qubits+    CZ -> Right $ concatMap decomposeCZ (pairs qubits)+    SWAP -> Right $ concatMap decomposeSWAP (pairs qubits)+    +    -- Non-Clifford gates (unsupported)+    RX -> Left $ UnsupportedGate RX+    RY -> Left $ UnsupportedGate RY+    RZ -> Left $ UnsupportedGate RZ+    +    -- Other gates that might be Clifford but need verification+    SQRT_X -> Left $ UnsupportedGate SQRT_X+    SQRT_X_DAG -> Left $ UnsupportedGate SQRT_X_DAG+    SQRT_Y -> Left $ UnsupportedGate SQRT_Y+    SQRT_Y_DAG -> Left $ UnsupportedGate SQRT_Y_DAG+    SQRT_Z -> Right $ map (CHP.Local . CHP.Phase . qubitIndex) qubits  -- SQRT_Z = S+    SQRT_Z_DAG -> Right $ concatMap decomposeSdag qubits+    +    -- Two-qubit Clifford gates needing decomposition+    CY -> Left $ UnsupportedGate CY+    CX -> translateCNOT qubits  -- CX is another name for CNOT+    CZSWAP -> Left $ UnsupportedGate CZSWAP+    CXSWAP -> Left $ UnsupportedGate CXSWAP+    SWAPCX -> Left $ UnsupportedGate SWAPCX+    SWAPCZ -> Left $ UnsupportedGate SWAPCZ+    ISWAP -> Left $ UnsupportedGate ISWAP+    ISWAP_DAG -> Left $ UnsupportedGate ISWAP_DAG+    SQRT_XX -> Left $ UnsupportedGate SQRT_XX+    SQRT_XX_DAG -> Left $ UnsupportedGate SQRT_XX_DAG+    SQRT_YY -> Left $ UnsupportedGate SQRT_YY+    SQRT_YY_DAG -> Left $ UnsupportedGate SQRT_YY_DAG+    SQRT_ZZ -> Left $ UnsupportedGate SQRT_ZZ+    SQRT_ZZ_DAG -> Left $ UnsupportedGate SQRT_ZZ_DAG+    +    -- Controlled Pauli variants+    XCZ -> translateCNOT (reverse qubits)  -- XCZ = CNOT with reversed control/target+    XCY -> Left $ UnsupportedGate XCY+    YCX -> Left $ UnsupportedGate YCX+    YCY -> Left $ UnsupportedGate YCY+    YCZ -> Left $ UnsupportedGate YCZ+    ZCX -> translateCNOT qubits  -- ZCX = CNOT+    ZCY -> Left $ UnsupportedGate ZCY+    ZCZ -> Right $ concatMap decomposeCZ (pairs qubits)+    +    -- Hadamard variants+    H_XY -> Left $ UnsupportedGate H_XY+    H_XZ -> Right $ map (CHP.Local . CHP.Hadamard . qubitIndex) qubits  -- H_XZ = H+    H_YZ -> Left $ UnsupportedGate H_YZ+    H_NXY -> Left $ UnsupportedGate H_NXY+    H_NXZ -> Left $ UnsupportedGate H_NXZ+    H_NYZ -> Left $ UnsupportedGate H_NYZ+    +    -- Identity variants+    II -> Right []+    +    -- Controlled rotation variants+    C_XYZ -> Left $ UnsupportedGate C_XYZ+    C_ZYX -> Left $ UnsupportedGate C_ZYX+    C_XYNZ -> Left $ UnsupportedGate C_XYNZ+    C_XNYZ -> Left $ UnsupportedGate C_XNYZ+    C_NXYZ -> Left $ UnsupportedGate C_NXYZ+    C_NZYX -> Left $ UnsupportedGate C_NZYX+    C_ZYNX -> Left $ UnsupportedGate C_ZYNX+    C_ZNYX -> Left $ UnsupportedGate C_ZNYX+    +    -- S dagger (S^3)+    S_DAG -> Right $ concatMap decomposeSdag qubits+    +    -- Controlled Pauli variants (additional)+    XCX -> Left $ UnsupportedGate XCX+    +    -- Reset (not a unitary gate)+    R -> Left $ UnsupportedGate R++-- | Translate CNOT with multiple targets.+-- STIM allows CNOT 0 1 2 3 which means CNOT(0,1) and CNOT(2,3).+-- Odd number of targets is an error.+translateCNOT :: [Q] -> Either TranslationError [CHP.SymplecticGate]+translateCNOT qubits = +  if even (length qubits)+    then Right $ concatMap (\(c, t) -> [CHP.CNOT (qubitIndex c) (qubitIndex t)]) (pairs qubits)+    else Left $ OddCNOTTargets qubits++-- | Translate a STIM measurement to a Pauli operator.+translateMeasure :: Measure -> Either TranslationError CHP.Pauli+translateMeasure (Measure measureType _ _ qubits) =+  case measureType of+    M -> Right $ pauliZ qubits+    MZ -> Right $ pauliZ qubits+    MX -> Right $ pauliX qubits+    MY -> Right $ pauliY qubits+    -- Measure-reset operations (not supported)+    MR -> Left $ UnsupportedMeasure MR+    MRX -> Left $ UnsupportedMeasure MRX+    MRY -> Left $ UnsupportedMeasure MRY+    MRZ -> Left $ UnsupportedMeasure MRZ+    -- Pauli product measurements (would need different interface)+    MXX -> Left $ UnsupportedMeasure MXX+    MYY -> Left $ UnsupportedMeasure MYY+    MZZ -> Left $ UnsupportedMeasure MZZ++-- | Count the total number of qubits used in a STIM circuit.+-- Returns max qubit index + 1 (since indices are 0-based).+countQubits :: Stim -> Int+countQubits stim = +  let qs = collectQubits stim+  in if Set.null qs then 0 else Set.findMax qs + 1+  where+    collectQubits :: Stim -> Set.Set Int+    collectQubits = \case+      StimList items -> Set.unions $ map collectQubits items+      StimG gate -> gateQubits gate+      StimM measure -> measureQubits measure+      StimNoise noise -> noiseQubits noise+      StimGpp gpp -> gppQubits gpp+      StimAnn ann -> annotationQubits ann+      StimRepeat _ body -> collectQubits body++    gateQubits (Gate _ _ qs) = Set.fromList $ map qubitIndex qs+    measureQubits (Measure _ _ _ qs) = Set.fromList $ map qubitIndex qs+    noiseQubits (NoiseNormal _ _ _ _ qs) = Set.fromList $ map qubitIndex qs+    noiseQubits (NoiseE _ _ _ pauliInds) = Set.fromList $ map piQubit pauliInds+    gppQubits (Gpp _ _ _ pcs) = Set.fromList $ concatMap pcQubits pcs++    +    pcQubits (P pauliInds) = map piQubit pauliInds+    pcQubits (N pauliInds) = map piQubit pauliInds+    +    piQubit (PauliInd _ idx) = idx  -- PauliInd contains qubit index directly+    +    annotationQubits (Ann _ _ _ qs) = Set.fromList $ map qubitIndex qs++-- | Extract the qubit index from a Q value.+qubitIndex :: Q -> Int+qubitIndex (Q i) = i+qubitIndex (Not idx) = idx  -- Negated qubit (measurement inversion) - Not contains index+qubitIndex (QRec _) = error "Record references not supported"+qubitIndex (QSweep _) = error "Sweep qubits not supported"++-- ============================================================================+-- Gate Decompositions+-- ============================================================================++-- | Decompose Pauli X into H and S gates.+-- X = H * S * S * H+decomposeX :: Q -> [CHP.SymplecticGate]+decomposeX q =+  let i = qubitIndex q+  in [ CHP.Local (CHP.Hadamard i)+     , CHP.Local (CHP.Phase i)+     , CHP.Local (CHP.Phase i)+     , CHP.Local (CHP.Hadamard i)+     ]++-- | Decompose Pauli Y into H and S gates.+-- Y = iXZ = S * X * S^3 = S * (HSSS) * SSS+decomposeY :: Q -> [CHP.SymplecticGate]+decomposeY q =+  let i = qubitIndex q+      sOps = [CHP.Local (CHP.Phase i)]+      sDagOps = [CHP.Local (CHP.Phase i), CHP.Local (CHP.Phase i), CHP.Local (CHP.Phase i)]+      xOps = decomposeX q+  in sOps ++ xOps ++ sDagOps++-- | Decompose Pauli Z into S gates.+-- Z = S * S+decomposeZ :: Q -> [CHP.SymplecticGate]+decomposeZ q =+  let i = qubitIndex q+  in [ CHP.Local (CHP.Phase i)+     , CHP.Local (CHP.Phase i)+     ]++-- | Decompose S^dagger (S^† = S^3).+decomposeSdag :: Q -> [CHP.SymplecticGate]+decomposeSdag q =+  let i = qubitIndex q+  in [ CHP.Local (CHP.Phase i)+     , CHP.Local (CHP.Phase i)+     , CHP.Local (CHP.Phase i)+     ]++-- | Decompose CZ (controlled-Z) into H and CNOT.+-- CZ(c,t) = H(t) * CNOT(c,t) * H(t)+decomposeCZ :: (Q, Q) -> [CHP.SymplecticGate]+decomposeCZ (c, t) =+  let ci = qubitIndex c+      ti = qubitIndex t+  in [ CHP.Local (CHP.Hadamard ti)+     , CHP.CNOT ci ti+     , CHP.Local (CHP.Hadamard ti)+     ]++-- | Decompose SWAP into three CNOTs.+-- SWAP(a,b) = CNOT(a,b) * CNOT(b,a) * CNOT(a,b)+decomposeSWAP :: (Q, Q) -> [CHP.SymplecticGate]+decomposeSWAP (a, b) =+  let ai = qubitIndex a+      bi = qubitIndex b+  in [ CHP.CNOT ai bi+     , CHP.CNOT bi ai+     , CHP.CNOT ai bi+     ]++-- ============================================================================+-- Pauli Construction Helpers+-- ============================================================================++-- | Construct a Pauli Z measurement on multiple qubits.+-- For single qubit: Z; For multiple: tensor product of Z's.+pauliZ :: [Q] -> CHP.Pauli+pauliZ qs = +  let indices = map qubitIndex qs+      zVec = foldl setBit (0 :: Word64) indices+  in CHP.Pauli 0 zVec 0++-- | Construct a Pauli X measurement on multiple qubits.+pauliX :: [Q] -> CHP.Pauli+pauliX qs =+  let indices = map qubitIndex qs+      xVec = foldl setBit (0 :: Word64) indices+  in CHP.Pauli xVec 0 0++-- | Construct a Pauli Y measurement on multiple qubits.+-- Y = iXZ, so we set both X and Z bits.+pauliY :: [Q] -> CHP.Pauli+pauliY qs =+  let indices = map qubitIndex qs+      mask = foldl setBit (0 :: Word64) indices+      -- Phase 1 for Y (iXZ)+  in CHP.Pauli mask mask 1++-- ============================================================================+-- Utility Functions+-- ============================================================================++-- | Pair up elements of a list.+-- [a,b,c,d] -> [(a,b), (c,d)]+-- Fails if list has odd length.+pairs :: [a] -> [(a, a)]+pairs [] = []+pairs (x:y:rest) = (x, y) : pairs rest+pairs [_] = error "Odd number of elements in pairs"
+ data/stim-circuits/bell-state.derive.md view
@@ -0,0 +1,121 @@+# Bell State Preparation: Mathematical Derivation++## Circuit Specification++```+H 0+CNOT 0 1+M 0+M 1+```++## Objective++Prepare the maximally entangled Bell state $|\Phi^+\rangle = \frac{1}{\sqrt{2}}(|00\rangle + |11\rangle)$ and verify its properties through measurement.++---++## Step-by-Step Derivation++### Initial State++$$|\psi_0\rangle = |0\rangle_0 \otimes |0\rangle_1 = |00\rangle$$++**Tableau:**+```yaml+stabilizers: ["+ZI", "+IZ"]+destabilizers: ["+XI", "+IX"]+```++### Step 1: Hadamard Gate on Qubit 0++The Hadamard gate creates superposition:++$$H = \frac{1}{\sqrt{2}}\begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}$$++$$H|0\rangle = \frac{|0\rangle + |1\rangle}{\sqrt{2}} = |+\rangle$$++**State after H:**+$$|\psi_1\rangle = |+\rangle_0 \otimes |0\rangle_1 = \frac{1}{\sqrt{2}}(|00\rangle + |10\rangle)$$++**Tableau after H:**+```yaml+stabilizers: ["+XI", "+IZ"]+destabilizers: ["+ZI", "+IX"]+```++**Conjugation:** $HZH^\dagger = X$, so stabilizer $Z_0 \rightarrow X_0$++### Step 2: CNOT Gate (Control=0, Target=1)++The CNOT operation: $\text{CNOT}|a,b\rangle = |a, b \oplus a\rangle$++Applying to each term:+| Input | Output |+|-------|--------|+| $|00\rangle$ | $|00\rangle$ |+| $|10\rangle$ | $|11\rangle$ |++**State after CNOT:**+$$|\psi_2\rangle = \frac{1}{\sqrt{2}}(|00\rangle + |11\rangle) = |\Phi^+\rangle$$++**Tableau after CNOT (pre-measurement):**+```yaml+stabilizers: ["+XX", "+ZZ"]+destabilizers: ["+ZI", "+IX"]+```++**Conjugation:** +- $X \otimes I \rightarrow X \otimes X$ (control X propagates to target)+- $I \otimes Z \rightarrow Z \otimes Z$ (target Z propagates to control)++---++## Measurement Analysis++### Z-Basis Measurement++The Bell state in computational basis:+$$|\Phi^+\rangle = \frac{|00\rangle + |11\rangle}{\sqrt{2}}$$++**Measurement outcomes:**+- $|00\rangle$ with probability $|\frac{1}{\sqrt{2}}|^2 = \frac{1}{2}$ → Both outcomes +1+- $|11\rangle$ with probability $|\frac{1}{\sqrt{2}}|^2 = \frac{1}{2}$ → Both outcomes -1++**Case 1: Outcomes [+1, +1]**+```yaml+probability: 0.5+measurement_outcomes: [+1, +1]+post_measurement_tableau:+  stabilizers: ["+ZI", "+ZZ"]+  destabilizers: ["+XX", "+IX"]+```++**Case 2: Outcomes [-1, -1]**+```yaml+probability: 0.5+measurement_outcomes: [-1, -1]+post_measurement_tableau:+  stabilizers: ["-ZI", "-ZZ"]+  destabilizers: ["+XX", "+IX"]+```++**Correlation:** The outcomes are perfectly correlated:+$$\langle Z_0 Z_1 \rangle = +1$$++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Measurement Correlation** | Perfect (M0 = M1) |+| **Pre-measurement stabilizers** | `+XX`, `+ZZ` |+| **Pre-measurement destabilizers** | `+ZI`, `+IX` |+| **Tableau Validity** | True |+| **P(+1,+1)** | 0.5 |+| **P(-1,-1)** | 0.5 |+| **P(+1,-1)** | 0 |+| **P(-1,+1)** | 0 |++**Key Property:** $\Pr(M_0 = M_1) = 1$ (perfect correlation)
+ data/stim-circuits/bell-state.expected view
@@ -0,0 +1,17 @@+# bell-state: H 0; CNOT 0 1 creates |Φ⁺⟩+# Z measurements are perfectly correlated (both +1 or both -1)+deterministic: false+cases:+  - probability: 0.5+    measurement_outcomes: [+1, +1]+    post_measurement_tableau:+      stabilizers: ["+ZI", "+ZZ"]+      destabilizers: ["+XX", "+IX"]+  - probability: 0.5+    measurement_outcomes: [-1, -1]+    post_measurement_tableau:+      stabilizers: ["-ZI", "-ZZ"]+      destabilizers: ["+XX", "+IX"]+pre_measurement_tableau:+  stabilizers: ["+XX", "+ZZ"]+  destabilizers: ["+ZI", "+IX"]
+ data/stim-circuits/bell-state.stim view
@@ -0,0 +1,7 @@+# Bell State Preparation+# Expected: |Φ⁺⟩ = (|00⟩ + |11⟩)/√2+# Measurement outcomes: correlated (always same)+H 0+CNOT 0 1+M 0+M 1
+ data/stim-circuits/cz-gate.derive.md view
@@ -0,0 +1,162 @@+# CZ Gate: Mathematical Derivation++## Circuit Specification++```+H 0+H 1+CZ 0 1+MX 0+MX 1+```++## Objective++Demonstrate CZ gate creates phase entanglement and verify its decomposition.++---++## CZ Gate Decomposition++### Theorem+$$CZ(c, t) = H(t) \cdot CNOT(c, t) \cdot H(t)$$++### Proof+The CZ gate applies phase -1 when both qubits are |1⟩:+$$CZ|ab\rangle = (-1)^{a \cdot b}|ab\rangle$$++The circuit $H_t \cdot CNOT_{c,t} \cdot H_t$:++1. $H_t$ transforms target from Z to X basis+2. $CNOT_{c,t}$ creates controlled-X in X basis → controlled-phase in Z basis+3. $H_t$ transforms back to Z basis++**Verification via truth table:**++| $\|ab\rangle$ | After $H_t$ | After CNOT | After $H_t$ | CZ Target |+|-------------|-------------|-----------|-------------|-----------|+| $\|00\rangle$ | $\|0+\rangle$ | $\|0+\rangle$ | $\|00\rangle$ | $+\|00\rangle$ |+| $\|01\rangle$ | $\|0-\rangle$ | $\|0-\rangle$ | $\|01\rangle$ | $+\|01\rangle$ |+| $\|10\rangle$ | $\|1+\rangle$ | $\|1+\rangle$ | $\|10\rangle$ | $+\|10\rangle$ |+| $\|11\rangle$ | $\|1-\rangle$ | $\|0-\rangle$ | $-\|11\rangle$ | $-\|11\rangle$ |++Both give the same phase pattern. **Q.E.D.**++---++## State Evolution++### Initial State++$$|\psi_0\rangle = |00\rangle$$++**Tableau:**+```yaml+stabilizers: ["+ZI", "+IZ"]+destabilizers: ["+XI", "+IX"]+```++### Step 1: Hadamard on Both Qubits++$$|\psi_1\rangle = |+\rangle \otimes |+\rangle = \frac{1}{2}(|00\rangle + |01\rangle + |10\rangle + |11\rangle)$$++**Tableau after H⊗H:**+```yaml+stabilizers: ["+XI", "+IX"]+destabilizers: ["+ZI", "+IZ"]+```++### Step 2: CZ Gate++Applying $CZ|ab\rangle = (-1)^{ab}|ab\rangle$:++$$|\psi_2\rangle = \frac{1}{2}(|00\rangle + |01\rangle + |10\rangle - |11\rangle)$$++**Tableau after CZ (pre-measurement):**+```yaml+stabilizers: ["+XZ", "+ZX"]+destabilizers: ["+ZI", "+IZ"]+```++**Conjugation:**+- $X \otimes I \rightarrow X \otimes Z$+- $I \otimes X \rightarrow Z \otimes X$++---++## Measurement Analysis++### X-Basis Measurement++The stabilizers $g_1 = XZ$ and $g_2 = ZX$ do not commute with $X \otimes I$ or $I \otimes X$ individually:++$$[X \otimes I, X \otimes Z] = 0 \quad \text{(commute)}$$+$$[X \otimes I, Z \otimes X] \neq 0 \quad \text{(anticommute)}$$++**Result:** Measurements are **random** and **correlated**.++### Correlation Structure++The product $X \otimes X$ commutes with both stabilizers:+$$[X \otimes X, X \otimes Z] = [X \otimes X, Z \otimes X] = 0$$++Therefore:+$$\langle X \otimes X \rangle = \pm 1$$++The sign depends on the random outcomes of individual measurements.++**Case 1: Outcomes [+1, +1]**+```yaml+probability: 0.25+measurement_outcomes: [+1, +1]+post_measurement_tableau:+  stabilizers: ["+IX", "+XI"]+  destabilizers: ["+XZ", "+ZX"]+```++**Case 2: Outcomes [+1, -1]**+```yaml+probability: 0.25+measurement_outcomes: [+1, -1]+post_measurement_tableau:+  stabilizers: ["-IX", "+XI"]+  destabilizers: ["+XZ", "+ZX"]+```++**Case 3: Outcomes [-1, +1]**+```yaml+probability: 0.25+measurement_outcomes: [-1, +1]+post_measurement_tableau:+  stabilizers: ["+IX", "-XI"]+  destabilizers: ["+XZ", "+ZX"]+```++**Case 4: Outcomes [-1, -1]**+```yaml+probability: 0.25+measurement_outcomes: [-1, -1]+post_measurement_tableau:+  stabilizers: ["-IX", "-XI"]+  destabilizers: ["+XZ", "+ZX"]+```++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Final State** | $\frac{1}{2}(\|00\rangle + \|01\rangle + \|10\rangle - \|11\rangle)$ |+| **Pre-measurement stabilizers** | `+XZ`, `+ZX` |+| **Pre-measurement destabilizers** | `+ZI`, `+IZ` |+| **Measurement Type** | Random |+| **Tableau Validity** | True |+| **P(+1,+1)** | ≈ 0.25 |+| **P(+1,-1)** | ≈ 0.25 |+| **P(-1,+1)** | ≈ 0.25 |+| **P(-1,-1)** | ≈ 0.25 |++**Key Property:** The state is entangled with maximal entropy for reduced density matrices.++**Note:** Unlike Bell state, X measurements are not perfectly correlated. The test only verifies tableau validity, not specific outcomes.
+ data/stim-circuits/cz-gate.expected view
@@ -0,0 +1,28 @@+# cz-gate: H 0; H 1; CZ 0 1 creates phase-entangled |++⟩ state+# CZ = H(1)·CNOT(0,1)·H(1)+# MX measurements are independent and random+deterministic: false+cases:+  - probability: 0.25+    measurement_outcomes: [+1, +1]+    post_measurement_tableau:+      stabilizers: ["+IX", "+XI"]+      destabilizers: ["+XZ", "+ZX"]+  - probability: 0.25+    measurement_outcomes: [+1, -1]+    post_measurement_tableau:+      stabilizers: ["-IX", "+XI"]+      destabilizers: ["+XZ", "+ZX"]+  - probability: 0.25+    measurement_outcomes: [-1, +1]+    post_measurement_tableau:+      stabilizers: ["+IX", "-XI"]+      destabilizers: ["+XZ", "+ZX"]+  - probability: 0.25+    measurement_outcomes: [-1, -1]+    post_measurement_tableau:+      stabilizers: ["-IX", "-XI"]+      destabilizers: ["+XZ", "+ZX"]+pre_measurement_tableau:+  stabilizers: ["+XZ", "+ZX"]+  destabilizers: ["+ZI", "+IZ"]
+ data/stim-circuits/cz-gate.stim view
@@ -0,0 +1,7 @@+# CZ gate test+# CZ|++⟩ creates phase entanglement+H 0+H 1+CZ 0 1+MX 0+MX 1
+ data/stim-circuits/ghz-state.derive.md view
@@ -0,0 +1,146 @@+# GHZ State Preparation: Mathematical Derivation++## Circuit Specification++```+H 0+CNOT 0 1+CNOT 0 2+M 0+M 1+M 2+```++## Objective++Prepare the 3-qubit GHZ state $|GHZ\rangle = \frac{1}{\sqrt{2}}(|000\rangle + |111\rangle)$ and verify tripartite entanglement.++---++## Step-by-Step Derivation++### Initial State++$$|\psi_0\rangle = |000\rangle$$++**Tableau:**+```yaml+stabilizers: ["+ZII", "+IZI", "+IIZ"]+destabilizers: ["+XII", "+IXI", "+IIX"]+```++### Step 1: Hadamard on Qubit 0++$$|\psi_1\rangle = |+\rangle_0 \otimes |00\rangle_{12} = \frac{1}{\sqrt{2}}(|000\rangle + |100\rangle)$$++**Tableau after H:**+```yaml+stabilizers: ["+XII", "+IZI", "+IIZ"]+destabilizers: ["+ZII", "+IXI", "+IIX"]+```++### Step 2: CNOT(0, 1)++| Input | Output |+|-------|--------|+| $\|000\rangle$ | $\|000\rangle$ |+| $\|100\rangle$ | $\|110\rangle$ |++$$|\psi_2\rangle = \frac{1}{\sqrt{2}}(|000\rangle + |110\rangle)$$++**Tableau after CNOT(0,1):**+```yaml+stabilizers: ["+XXI", "+ZZI", "+IIZ"]+destabilizers: ["+ZII", "+IXI", "+IIX"]+```++### Step 3: CNOT(0, 2)++| Input | Output |+|-------|--------|+| $\|000\rangle$ | $\|000\rangle$ |+| $\|110\rangle$ | $\|111\rangle$ |++$$|\psi_3\rangle = \frac{1}{\sqrt{2}}(|000\rangle + |111\rangle) = |GHZ\rangle$$++**Tableau after CNOT(0,2) (pre-measurement):**+```yaml+stabilizers: ["+XXX", "+ZZI", "+ZIZ"]+destabilizers: ["+ZII", "+IXI", "+IIX"]+```++---++## Entanglement Properties++### Tripartite Entanglement++The GHZ state exhibits **genuine multipartite entanglement**:++$$|GHZ\rangle \neq |\phi\rangle_0 \otimes |\psi\rangle_{12}$$++**Reduced Density Matrix (trace out qubit 2):**+$$\rho_{01} = \text{Tr}_2(|GHZ\rangle\langle GHZ|) = \frac{1}{2}(|00\rangle\langle 00| + |11\rangle\langle 11|)$$++This is a **mixed state** (classical correlation only), demonstrating that the entanglement is truly tripartite.++---++## Measurement Analysis++### Z-Basis Measurements++The state in computational basis:+$$|GHZ\rangle = \frac{|000\rangle + |111\rangle}{\sqrt{2}}$$++**Possible outcomes:**+- $(+1, +1, +1)$ with probability $\frac{1}{2}$+- $(-1, -1, -1)$ with probability $\frac{1}{2}$++**Case 1: Outcomes [+1, +1, +1]**+```yaml+probability: 0.5+measurement_outcomes: [+1, +1, +1]+post_measurement_tableau:+  stabilizers: ["+ZII", "+ZZI", "+ZIZ"]+  destabilizers: ["+XXX", "+IXI", "+IIX"]+```++**Case 2: Outcomes [-1, -1, -1]**+```yaml+probability: 0.5+measurement_outcomes: [-1, -1, -1]+post_measurement_tableau:+  stabilizers: ["-ZII", "-ZZI", "-ZIZ"]+  destabilizers: ["+XXX", "+IXI", "+IIX"]+```++**Correlation Structure:**+$$\langle Z_i Z_j \rangle = +1 \quad \forall i \neq j$$++Any two qubits are perfectly correlated.++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Measurement Correlation** | All three outcomes equal |+| **Pre-measurement stabilizers** | `+XXX`, `+ZZI`, `+ZIZ` |+| **Pre-measurement destabilizers** | `+ZII`, `+IXI`, `+IIX` |+| **Tableau Validity** | True |+| **P(all +1)** | 0.5 |+| **P(all -1)** | 0.5 |+| **Any mixed outcome** | 0 |++**Key Property:** $\Pr(M_0 = M_1 = M_2) = 1$ (perfect 3-way correlation)++**Comparison with Bell State:**++| Feature | Bell State | GHZ State |+|---------|-----------|-----------|+| Qubits | 2 | 3 |+| Form | $\frac{|00\rangle+|11\rangle}{\sqrt{2}}$ | $\frac{|000\rangle+|111\rangle}{\sqrt{2}}$ |+| Entanglement | Bipartite | Tripartite |+| Stabilizers | 2 | 3 |
+ data/stim-circuits/ghz-state.expected view
@@ -0,0 +1,17 @@+# ghz-state: H 0; CNOT 0 1; CNOT 0 2 creates |GHZ⟩+# All three Z measurements are equal (all +1 or all -1)+deterministic: false+cases:+  - probability: 0.5+    measurement_outcomes: [+1, +1, +1]+    post_measurement_tableau:+      stabilizers: ["+ZII", "+ZZI", "+ZIZ"]+      destabilizers: ["+XXX", "+IXI", "+IIX"]+  - probability: 0.5+    measurement_outcomes: [-1, -1, -1]+    post_measurement_tableau:+      stabilizers: ["-ZII", "-ZZI", "-ZIZ"]+      destabilizers: ["+XXX", "+IXI", "+IIX"]+pre_measurement_tableau:+  stabilizers: ["+XXX", "+ZZI", "+ZIZ"]+  destabilizers: ["+ZII", "+IXI", "+IIX"]
+ data/stim-circuits/ghz-state.stim view
@@ -0,0 +1,8 @@+# GHZ State Preparation+# Expected: |GHZ⟩ = (|000⟩ + |111⟩)/√2+H 0+CNOT 0 1+CNOT 0 2+M 0+M 1+M 2
+ data/stim-circuits/multi-target.derive.md view
@@ -0,0 +1,159 @@+# Multi-Target Gates: Mathematical Derivation++## Circuit Specification++```+H 0+H 1+H 2+MX 0+MX 1+MX 2+```++## Objective++Demonstrate independent evolution of multiple qubits and verify product state structure.++---++## State Evolution++### Initial State++$$|\psi_0\rangle = |000\rangle$$++**Tableau:**+```yaml+stabilizers: ["+ZII", "+IZI", "+IIZ"]+destabilizers: ["+XII", "+IXI", "+IIX"]+```++### Step 1: Hadamard on All Qubits++Since $H^{\otimes 3} = H \otimes H \otimes H$:++$$\begin{aligned}+|\psi_1\rangle &= H|0\rangle \otimes H|0\rangle \otimes H|0\rangle \\+&= |+\rangle \otimes |+\rangle \otimes |+\rangle \\+&= |+++\rangle+\end{aligned}$$++**Tableau after H⊗H⊗H (pre-measurement):**+```yaml+stabilizers: ["+XII", "+IXI", "+IIX"]+destabilizers: ["+ZII", "+IZI", "+IIZ"]+```++### Product State Form++$$|+++\rangle = \frac{1}{\sqrt{8}}\sum_{x=0}^{7}|x\rangle$$++Explicitly:+$$|\psi_1\rangle = \frac{|000\rangle + |001\rangle + |010\rangle + |011\rangle + |100\rangle + |101\rangle + |110\rangle + |111\rangle}{\sqrt{8}}$$++**Key Property:** This is a **product state**, not entangled.++---++## Product vs. Entangled States++### Factorization Test++$$|+++\rangle = |+\rangle_0 \otimes |+\rangle_1 \otimes |+\rangle_2$$++**Separability:** The state can be written as a tensor product of single-qubit states.++**Reduced Density Matrix:**+$$\rho_0 = \text{Tr}_{12}(|+++\rangle\langle+++|) = |+\rangle\langle+|$$++This is a **pure state**, confirming no entanglement.++### Contrast with GHZ State++| Property | $|+++\rangle$ | $|GHZ\rangle$ |+|----------|---------------|---------------|+| **Form** | Product $\bigotimes_i |+\rangle_i$ | Entangled $\frac{\|000\rangle+\|111\rangle}{\sqrt{2}}$ |+| **Entanglement** | None | Tripartite |+| **Reduced ρ** | Pure | Mixed |+| **Stabilizers** | Independent | Correlated |++---++## Stabilizer Analysis++### Independent Stabilizers++The state $|+++\rangle$ has stabilizer generators:++$$\{+X_0, +X_1, +X_2\} = \{+XII, +IXI, +IIX\}$$++**Verification:**+$$X_i |+++\rangle = |+++\rangle \quad \forall i$$++Each stabilizer acts on only one qubit, confirming the product structure.++### Stabilizer Group++All stabilizers are of the form:+$$g = (+/-)X^{a_0} \otimes X^{a_1} \otimes X^{a_2}, \quad a_i \in \{0, 1\}$$++Total: $2^3 = 8$ stabilizer elements.++---++## Measurement Analysis++### X-Basis Eigenstates++For each qubit:+$$X|+\rangle = +|+\rangle$$++The state $|+\rangle$ is the +1 eigenstate of X.++### Measurement Outcomes++**Outcome Probabilities:**+$$\Pr(M_i = +1) = |\langle+|+\rangle|^2 = 1$$+$$\Pr(M_i = -1) = |\langle-|+\rangle|^2 = 0$$++All three measurements give **deterministic** outcome +1.++**Joint Probability:**+$$\Pr(M_0=+1, M_1=+1, M_2=+1) = 1$$++**Post-measurement tableau:**+```yaml+deterministic: true+measurement_outcomes: [+1, +1, +1]+post_measurement_tableau:+  stabilizers: ["+XII", "+IXI", "+IIX"]+  destabilizers: ["+ZII", "+IZI", "+IIZ"]+```++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Final State** | $\|+++\rangle = \|+\rangle^{\otimes 3}$ |+| **State Type** | Product state (not entangled) |+| **Pre-measurement stabilizers** | `+XII`, `+IXI`, `+IIX` |+| **Pre-measurement destabilizers** | `+ZII`, `+IZI`, `+IIZ` |+| **Measurement 0** | +1 (deterministic) |+| **Measurement 1** | +1 (deterministic) |+| **Measurement 2** | +1 (deterministic) |+| **Tableau Validity** | True |+| **P(+1,+1,+1)** | 1.0 |+| **All other outcomes** | 0.0 |++**Key Property:** Multi-target gate syntax `H 0 1 2` applies independent single-qubit gates.++**Physical Interpretation:**+Each qubit evolves independently in its own Bloch sphere:+- Initial: All at north pole $|0\rangle$+- After H: All at +X axis $|+\rangle$+- X measurement: Deterministic +1 for each++This tests the CHP simulator's handling of **product states** and **multi-target gate syntax**.
+ data/stim-circuits/multi-target.expected view
@@ -0,0 +1,7 @@+# multi-target: H on all qubits creates |+++⟩+# All MX measurements are deterministic +1+deterministic: true+measurement_outcomes: [+1, +1, +1]+post_measurement_tableau:+  stabilizers: ["+XII", "+IXI", "+IIX"]+  destabilizers: ["+ZII", "+IZI", "+IIZ"]
+ data/stim-circuits/multi-target.stim view
@@ -0,0 +1,8 @@+# Multi-target gate test+# Apply H to multiple qubits at once+H 0+H 1+H 2+MX 0+MX 1+MX 2
+ data/stim-circuits/phase-gate.derive.md view
@@ -0,0 +1,168 @@+# Phase Gate (S² = Z): Mathematical Derivation++## Circuit Specification++```+H 0+S 0+S 0+M 0+```++## Objective++Demonstrate that $S^2 = Z$ and verify phase kickback on superposition states.++---++## S Gate Properties++### Definition+$$S = \begin{pmatrix} 1 & 0 \\ 0 & i \end{pmatrix}, \quad S^2 = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix} = Z$$++### Action on Computational Basis+$$S|0\rangle = |0\rangle, \quad S|1\rangle = i|1\rangle$$++### Conjugation Relations+$$S X S^\dagger = Y, \quad S Y S^\dagger = -X, \quad S Z S^\dagger = Z$$++**Key Property:** S rotates around the Z-axis by $\pi/2$ in the Bloch sphere.++---++## State Evolution++### Initial State++$$|\psi_0\rangle = |0\rangle$$++**Tableau:**+```yaml+stabilizers: ["+Z"]+destabilizers: ["+X"]+```++### Step 1: Hadamard++$$|\psi_1\rangle = H|0\rangle = |+\rangle = \frac{|0\rangle + |1\rangle}{\sqrt{2}}$$++**Tableau after H:**+```yaml+stabilizers: ["+X"]+destabilizers: ["+Z"]+```++### Step 2: Apply S² = Z++Using the identity $S^2 = Z$:++$$|\psi_2\rangle = S^2 |+\rangle = Z|+\rangle = \frac{Z|0\rangle + Z|1\rangle}{\sqrt{2}} = \frac{|0\rangle - |1\rangle}{\sqrt{2}} = |-\rangle$$++**Phase Kickback:** The Z gate introduces a relative phase $\pi$ between $|0\rangle$ and $|1\rangle$.++**Tableau after first S:**+```yaml+stabilizers: ["+Y"]+destabilizers: ["+Z"]+```++**Conjugation:** $SXS^\dagger = Y$++**Tableau after second S (pre-measurement):**+```yaml+stabilizers: ["-X"]+destabilizers: ["+Z"]+```++**Conjugation:** $SYS^\dagger = -X$, so $+Y \rightarrow -X$++---++## Alternative: Two S Gates++Applying S twice:++**First S:**+$$S|+\rangle = \frac{|0\rangle + i|1\rangle}{\sqrt{2}} = |+i\rangle$$++This rotates from +X to +Y on Bloch sphere.++**Second S:**+$$S|+i\rangle = \frac{|0\rangle + i^2|1\rangle}{\sqrt{2}} = \frac{|0\rangle - |1\rangle}{\sqrt{2}} = |-\rangle$$++This rotates from +Y to -X on Bloch sphere.++**Combined:** +X → +Y → -X, equivalent to 180° rotation around Z-axis.++---++## Measurement Analysis++### Final State++$$|\psi_2\rangle = |-\rangle = \frac{|0\rangle - |1\rangle}{\sqrt{2}}$$++### Z-Basis Measurement++The state $|-\rangle$ is an equal superposition, not a Z eigenstate.++**Outcome Probabilities:**+$$\Pr(+1) = |\langle 0 | - \rangle|^2 = \frac{1}{2}$$+$$\Pr(-1) = |\langle 1 | - \rangle|^2 = \frac{1}{2}$$++**Interpretation:** The measurement outcome is **random**.++**Case 1: Outcome +1**+```yaml+probability: 0.5+measurement_outcomes: [+1]+post_measurement_tableau:+  stabilizers: ["+Z"]+  destabilizers: ["-X"]+```++**Case 2: Outcome -1**+```yaml+probability: 0.5+measurement_outcomes: [-1]+post_measurement_tableau:+  stabilizers: ["-Z"]+  destabilizers: ["-X"]+```++---++## Comparison: S vs S²++| Gate | Action on $\|+\rangle$ | Bloch Rotation |+|------|---------------------|----------------|+| S | $\|+\rangle \rightarrow \|+i\rangle$ | +90° around Z |+| S² | $\|+\rangle \rightarrow \|-\rangle$ | +180° around Z |+| S³ | $\|+\rangle \rightarrow \|-i\rangle$ | +270° around Z |+| S⁴ | $\|+\rangle \rightarrow \|+\rangle$ | +360° around Z (= I) |++**Periodicity:** $S^4 = I$ (order 4 in SU(2))++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Circuit Identity** | $S^2 = Z$ |+| **Final State** | $\|-\rangle = \frac{\|0\rangle - \|1\rangle}{\sqrt{2}}$ |+| **Final Stabilizer** | `-X` |+| **Pre-measurement destabilizer** | `+Z` |+| **Z-Basis Measurement** | Random |+| **P(+1)** | 0.5 |+| **P(-1)** | 0.5 |+| **Tableau Validity** | True |++**Key Insight:** The S gate's square is Z, which anti-commutes with X. This flips the stabilizer from +X to -X.++**Physical Interpretation:**+- Start at north pole $|0\rangle$+- Rotate to +X axis by Hadamard+- Rotate 180° around Z by S²+- End at -X axis $|-\rangle$+- Z measurement is random (state lies in XY plane)
+ data/stim-circuits/phase-gate.expected view
@@ -0,0 +1,17 @@+# phase-gate: H 0; S 0; S 0 = H·Z|0⟩ = |−⟩+# Z measurement is random+deterministic: false+cases:+  - probability: 0.5+    measurement_outcomes: [+1]+    post_measurement_tableau:+      stabilizers: ["+Z"]+      destabilizers: ["-X"]+  - probability: 0.5+    measurement_outcomes: [-1]+    post_measurement_tableau:+      stabilizers: ["-Z"]+      destabilizers: ["-X"]+pre_measurement_tableau:+  stabilizers: ["-X"]+  destabilizers: ["+Z"]
+ data/stim-circuits/phase-gate.stim view
@@ -0,0 +1,7 @@+# Phase gate test+# S†X S = Y, S†Z S = Z+# Prepare |+⟩, apply S twice (=Z), measure Z+H 0+S 0+S 0+M 0
+ data/stim-circuits/single-hadamard.derive.md view
@@ -0,0 +1,106 @@+# Single Hadamard Gate: Mathematical Derivation++## Circuit Specification++```+H 0+MX 0+```++## Objective++Demonstrate that $|+\rangle = H|0\rangle$ is the +1 eigenstate of $X$, giving deterministic measurement outcome.++---++## Step-by-Step Derivation++### Initial State++$$|\psi_0\rangle = |0\rangle$$++**Tableau:**+```yaml+stabilizers: ["+Z"]+destabilizers: ["+X"]+```++### Step 1: Hadamard Gate++$$H = \frac{1}{\sqrt{2}}\begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}$$++$$|\psi_1\rangle = H|0\rangle = \frac{1}{\sqrt{2}}\begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}\begin{pmatrix} 1 \\ 0 \end{pmatrix} = \frac{1}{\sqrt{2}}\begin{pmatrix} 1 \\ 1 \end{pmatrix} = |+\rangle$$++**Bloch Sphere Representation:**+- Initial: North pole ($|0\rangle$)+- After H: +X axis ($|+\rangle$)++**Tableau after H (pre-measurement):**+```yaml+stabilizers: ["+X"]+destabilizers: ["+Z"]+```++**Conjugation:** $HZH^\dagger = X$, so stabilizer flips from +Z to +X++---++## Eigenstate Analysis++### Pauli X Operator++$$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}$$++**Eigenvalue Equation:**+$$X|+\rangle = \frac{1}{\sqrt{2}}\begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}\begin{pmatrix} 1 \\ 1 \end{pmatrix} = \frac{1}{\sqrt{2}}\begin{pmatrix} 1 \\ 1 \end{pmatrix} = +1 \cdot |+\rangle$$++**Conclusion:** $|+\rangle$ is the +1 eigenstate of $X$.++### Complete Eigenbasis of X++| Eigenstate | Eigenvalue | Bloch Vector |+|-----------|-----------|--------------|+| $\|+\rangle = \frac{\|0\rangle + \|1\rangle}{\sqrt{2}}$ | +1 | $(1, 0, 0)$ |+| $\|-\rangle = \frac{\|0\rangle - \|1\rangle}{\sqrt{2}}$ | -1 | $(-1, 0, 0)$ |++---++## Measurement Analysis++### X-Basis Measurement (MX)++Projective measurement operators:+$$P_+ = |+\rangle\langle+|, \quad P_- = |-\rangle\langle-|$$++**Outcome Probabilities:**+$$\begin{aligned}+\Pr(+1) &= \langle\psi_1|P_+|\psi_1\rangle = |\langle+|+\rangle|^2 = 1 \\+\Pr(-1) &= \langle\psi_1|P_-|\psi_1\rangle = |\langle-|+\rangle|^2 = 0+\end{aligned}$$++**Result:** Deterministic outcome +1++**Post-measurement tableau:**+```yaml+deterministic: true+measurement_outcomes: [+1]+post_measurement_tableau:+  stabilizers: ["+X"]+  destabilizers: ["+Z"]+```++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Final State** | $\|+\rangle = \frac{\|0\rangle + \|1\rangle}{\sqrt{2}}$ |+| **Measurement Outcome** | +1 (deterministic) |+| **Pre-measurement stabilizer** | `+X` |+| **Pre-measurement destabilizer** | `+Z` |+| **Tableau Validity** | True |+| **P(+1)** | 1.0 |+| **P(-1)** | 0.0 |++**Key Insight:** Hadamard transforms a Z eigenstate into an X eigenstate. Measuring in the eigenbasis gives a deterministic outcome.
+ data/stim-circuits/single-hadamard.expected view
@@ -0,0 +1,6 @@+# single-hadamard: H|0⟩ = |+⟩, MX gives deterministic +1+deterministic: true+measurement_outcomes: [+1]+pre_measurement_tableau:+  stabilizers: ["+X"]+  destabilizers: ["+Z"]
+ data/stim-circuits/single-hadamard.stim view
@@ -0,0 +1,5 @@+# Single qubit Hadamard+# Input: |0⟩, Output: |+⟩+# Measurement in X-basis should be deterministic +1+H 0+MX 0
+ data/stim-circuits/stabilizer-cycle.derive.md view
@@ -0,0 +1,164 @@+# Stabilizer Cycle: X Gate Decomposition++## Circuit Specification++```+H 0+S 0+S 0+H 0+M 0+```++## Objective++Prove that $HSSH = X$ and verify the state evolution $|0\rangle \rightarrow |1\rangle$.++---++## Algebraic Proof: HSSH = X++### Key Identities++1. $S^2 = Z$ (Phase gate squared is Pauli Z)+2. $HZH = X$ (Hadamard conjugates Z to X)++### Derivation++$$\begin{aligned}+HSSH &= H(S^2)H \\+     &= HZH \quad \text{(using } S^2 = Z\text{)} \\+     &= X \quad \text{(using } HZH = X\text{)}+\end{aligned}$$++**Q.E.D.** The circuit implements the Pauli X gate.++---++## State Evolution++### Initial State++$$|\psi_0\rangle = |0\rangle$$++**Tableau:**+```yaml+stabilizers: ["+Z"]+destabilizers: ["+X"]+```++### Step 1: H++$$|\psi_1\rangle = H|0\rangle = |+\rangle = \frac{|0\rangle + |1\rangle}{\sqrt{2}}$$++**Tableau after H:**+```yaml+stabilizers: ["+X"]+destabilizers: ["+Z"]+```++### Step 2: S++$$S = \begin{pmatrix} 1 & 0 \\ 0 & i \end{pmatrix}$$++$$S|+\rangle = \frac{S|0\rangle + S|1\rangle}{\sqrt{2}} = \frac{|0\rangle + i|1\rangle}{\sqrt{2}} = |+i\rangle$$++This is the +i eigenstate of Y (Bloch sphere +Y axis).++**Tableau after first S:**+```yaml+stabilizers: ["+Y"]+destabilizers: ["+Z"]+```++### Step 3: S (again)++$$S|+i\rangle = \frac{|0\rangle + i^2|1\rangle}{\sqrt{2}} = \frac{|0\rangle - |1\rangle}{\sqrt{2}} = |-\rangle$$++This is the -1 eigenstate of X (Bloch sphere -X axis).++**Tableau after second S:**+```yaml+stabilizers: ["-X"]+destabilizers: ["+Z"]+```++### Step 4: H++$$H|-\rangle = \frac{H|0\rangle - H|1\rangle}{\sqrt{2}} = \frac{|+\rangle - |-\rangle}{\sqrt{2}} = |1\rangle$$++Since $H|+\rangle = |0\rangle$ and $H|-\rangle = |1\rangle$.++**Tableau after final H (post-measurement):**+```yaml+stabilizers: ["-Z"]+destabilizers: ["+X"]+```++---++## Stabilizer Evolution++The stabilizer transforms as:++| Step | Gate | Stabilizer | State | Bloch Vector |+|------|------|-----------|-------|--------------|+| 0 | — | $+Z$ | $\|0\rangle$ | $(0, 0, 1)$ |+| 1 | H | $+X$ | $\|+\rangle$ | $(1, 0, 0)$ |+| 2 | S | $+Y$ | $\|+i\rangle$ | $(0, 1, 0)$ |+| 3 | S | $-X$ | $\|-\rangle$ | $(-1, 0, 0)$ |+| 4 | H | $-Z$ | $\|1\rangle$ | $(0, 0, -1)$ |++### S Gate Conjugation++The S gate rotates around Z-axis:+- $SXS^\dagger = Y$+- $SYS^\dagger = -X$  +- $SZS^\dagger = Z$++**Verification:**+- Step 1→2: $S(+X)S^\dagger = +Y$ ✓+- Step 2→3: $S(+Y)S^\dagger = -X$ ✓++---++## Measurement Analysis++### Final State++$$|\psi_4\rangle = |1\rangle$$++### Z-Basis Measurement++Z operator eigenstates:+- $|0\rangle$ with eigenvalue +1+- $|1\rangle$ with eigenvalue -1++**Outcome:**+$$Z|1\rangle = -|1\rangle \Rightarrow \text{measurement outcome } -1$$++**Expected result:**+```yaml+deterministic: true+measurement_outcomes: [-1]+post_measurement_tableau:+  stabilizers: ["-Z"]+  destabilizers: ["+X"]+```++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Circuit Identity** | $HSSH = X$ |+| **Final State** | $\|1\rangle$ |+| **Measurement Outcome** | -1 (deterministic) |+| **Final Stabilizer** | `-Z` |+| **Final Destabilizer** | `+X` |+| **Tableau Validity** | True |+| **P(-1)** | 1.0 |+| **P(+1)** | 0.0 |++**Key Insight:** This circuit demonstrates Clifford group composition. Each gate permutes Pauli operators, and the composition $HSSH$ maps $Z \rightarrow -Z$, equivalent to the X gate conjugation: $XZX^\dagger = -Z$.
+ data/stim-circuits/stabilizer-cycle.expected view
@@ -0,0 +1,7 @@+# stabilizer-cycle: H 0; S 0; S 0; H 0 = HSSH = X+# X|0⟩ = |1⟩, so Z measurement gives deterministic -1+deterministic: true+measurement_outcomes: [-1]+post_measurement_tableau:+  stabilizers: ["-Z"]+  destabilizers: ["+X"]
+ data/stim-circuits/stabilizer-cycle.stim view
@@ -0,0 +1,8 @@+# Test that stabilizer cycle works correctly+# Apply H then S then S then H = X on |0⟩ should give |1⟩+# Z measurement should give -1+H 0+S 0+S 0+H 0+M 0
+ data/stim-circuits/swap-gate.derive.md view
@@ -0,0 +1,142 @@+# SWAP Gate: Mathematical Derivation++## Circuit Specification++```+X 1+SWAP 0 1+M 0+M 1+```++## Objective++Verify SWAP gate exchanges qubit states and prove SWAP = CNOT₁₂ ∘ CNOT₂₁ ∘ CNOT₁₂.++---++## SWAP Gate Decomposition++### Theorem+$$\text{SWAP}(a, b) = \text{CNOT}(a, b) \cdot \text{CNOT}(b, a) \cdot \text{CNOT}(a, b)$$++### Proof via Truth Table++| Step | State | After CNOT(a,b) | After CNOT(b,a) | After CNOT(a,b) |+|------|-------|-----------------|-----------------|-----------------|+| 1 | $\|00\rangle$ | $\|00\rangle$ | $\|00\rangle$ | $\|00\rangle$ |+| 2 | $\|01\rangle$ | $\|01\rangle$ | $\|11\rangle$ | $\|10\rangle$ |+| 3 | $\|10\rangle$ | $\|11\rangle$ | $\|01\rangle$ | $\|01\rangle$ |+| 4 | $\|11\rangle$ | $\|10\rangle$ | $\|10\rangle$ | $\|11\rangle$ |++**Result mapping:**+- $|00\rangle \rightarrow |00\rangle$ ✓+- $|01\rangle \rightarrow |10\rangle$ ✓+- $|10\rangle \rightarrow |01\rangle$ ✓+- $|11\rangle \rightarrow |11\rangle$ ✓++**Q.E.D.** The circuit swaps qubit states.++### Verification for |01⟩++1. **CNOT(0,1)**: Control=0, no flip → $|01\rangle$+2. **CNOT(1,0)**: Control=1, flip qubit 0 → $|11\rangle$+3. **CNOT(0,1)**: Control=1, flip qubit 1 → $|10\rangle$++Result: $|01\rangle \rightarrow |10\rangle$ ✓++---++## State Evolution++### Initial State++$$|\psi_0\rangle = |00\rangle$$++**Tableau:**+```yaml+stabilizers: ["+ZI", "+IZ"]+destabilizers: ["+XI", "+IX"]+```++### Step 1: X Gate on Qubit 1++$$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}$$++$$|\psi_1\rangle = |01\rangle$$++**Tableau after X₁:**+```yaml+stabilizers: ["+ZI", "-IZ"]+destabilizers: ["+XI", "+IX"]+```++### Step 2: SWAP(0, 1)++$$\text{SWAP}|01\rangle = |10\rangle$$++**Final state before measurement:**+$$|\psi_2\rangle = |10\rangle$$++**Tableau after SWAP (post-measurement):**+```yaml+stabilizers: ["+IZ", "-ZI"]+destabilizers: ["+IX", "+XI"]+```++### SWAP Action on Pauli Operators++The SWAP gate exchanges Pauli operators:+$$\text{SWAP} \cdot X_0 \cdot \text{SWAP}^\dagger = X_1$$+$$\text{SWAP} \cdot Z_0 \cdot \text{SWAP}^\dagger = Z_1$$+$$\text{SWAP} \cdot X_1 \cdot \text{SWAP}^\dagger = X_0$$+$$\text{SWAP} \cdot Z_1 \cdot \text{SWAP}^\dagger = Z_0$$++This is equivalent to exchanging rows in the CHP tableau.++---++## Measurement Analysis++### Final State++$$|\psi_2\rangle = |10\rangle = |1\rangle_0 \otimes |0\rangle_1$$++### Z-Basis Measurements++| Qubit | State | Z Eigenvalue | Outcome |+|-------|-------|-------------|---------|+| 0 | $\|1\rangle$ | -1 | **-1** |+| 1 | $\|0\rangle$ | +1 | **+1** |++**Expected result:**+```yaml+deterministic: true+measurement_outcomes: [-1, +1]+post_measurement_tableau:+  stabilizers: ["+IZ", "-ZI"]+  destabilizers: ["+IX", "+XI"]+```++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Circuit Identity** | SWAP = CNOT₁₂ ∘ CNOT₂₁ ∘ CNOT₁₂ |+| **Final State** | $\|10\rangle$ |+| **Measurement 0** | -1 (deterministic) |+| **Measurement 1** | +1 (deterministic) |+| **Final Stabilizers** | `+IZ`, `-ZI` |+| **Final Destabilizers** | `+IX`, `+XI` |+| **Tableau Validity** | True |+| **P(M₀=-1, M₁=+1)** | 1.0 |+| **All other outcomes** | 0.0 |++**Key Property:** The SWAP exchanges both the quantum state and the stabilizer assignments between qubits.++**Geometric Interpretation:**+- Initial: Qubit 0 at |0⟩ (north pole), Qubit 1 at |1⟩ (south pole)+- After SWAP: Qubit 0 at |1⟩ (south pole), Qubit 1 at |0⟩ (north pole)+- The SWAP is its own inverse: SWAP² = I
+ data/stim-circuits/swap-gate.expected view
@@ -0,0 +1,8 @@+# swap-gate: X 1; SWAP 0 1 exchanges |01⟩ → |10⟩+# X = H·S·S·H; SWAP = CNOT(0,1)·CNOT(1,0)·CNOT(0,1)+# Z measurements are deterministic: M0=-1, M1=+1+deterministic: true+measurement_outcomes: [-1, +1]+post_measurement_tableau:+  stabilizers: ["+IZ", "-ZI"]+  destabilizers: ["+IX", "+XI"]
+ data/stim-circuits/swap-gate.stim view
@@ -0,0 +1,6 @@+# SWAP gate test+# Prepare |01⟩, SWAP, measure should give |10⟩+X 1+SWAP 0 1+M 0+M 1
+ data/stim-circuits/unsupported-rx.derive.md view
@@ -0,0 +1,135 @@+# Unsupported RX Gate: Error Handling Test++## Circuit Specification++```+RX 0+M 0+```++## Objective++Verify that the CHP simulator correctly rejects non-Clifford gates with a clear error message.++---++## The RX Gate++### Definition++The RX gate is a rotation around the X-axis by angle $\theta$:++$$R_X(\theta) = e^{-i\theta X/2} = \cos\frac{\theta}{2} I - i\sin\frac{\theta}{2} X$$++### Matrix Form++$$R_X(\theta) = \begin{pmatrix} \cos\frac{\theta}{2} & -i\sin\frac{\theta}{2} \\ -i\sin\frac{\theta}{2} & \cos\frac{\theta}{2} \end{pmatrix}$$++---++## Clifford vs. Non-Clifford++### Clifford Group Definition++The Clifford group $\mathcal{C}_n$ consists of unitaries that:+1. Map Pauli group to itself under conjugation: $U P U^\dagger \in \mathcal{P}_n$ for all $P \in \mathcal{P}_n$+2. Can be generated by $\{H, S, \text{CNOT}\}$++### Testing if RX is Clifford++For RX to be Clifford, it must map Pauli operators to Pauli operators.++**Test on Z:**+$$R_X(\theta) Z R_X(-\theta) = \begin{pmatrix} \cos\theta & -i\sin\theta \\ i\sin\theta & -\cos\theta \end{pmatrix}$$++For this to be a Pauli matrix ($\pm X, \pm Y, \pm Z$), we need:+- $\sin\theta = 0$ AND $\cos\theta = \pm 1$ → $\theta \in \{0, \pi, 2\pi, ...\}$+- OR $\cos\theta = 0$ AND $\sin\theta = \pm 1$ → $\theta \in \{\pi/2, 3\pi/2, ...\}$++### Clifford Cases++| $\theta$ | $R_X(\theta)$ | Clifford? |+|-----------|---------------|-----------|+| 0 | $I$ | Yes |+| $\pi/2$ | $\sqrt{X}$ | Yes (if global phase ignored) |+| $\pi$ | $X$ | Yes |+| $3\pi/2$ | $\sqrt{X}^\dagger$ | Yes |+| Generic $\theta$ | — | **No** |++**Conclusion:** Generic $R_X(\theta)$ is **not** a Clifford gate.++---++## Why Non-Clifford Gates Break CHP++### CHP Algorithm Requirements++The CHP simulator uses the **stabilizer formalism**:+- States represented by stabilizer generators+- Evolution via conjugation: $g \rightarrow U g U^\dagger$+- Measurements via symplectic inner product++### The Problem with RX++For non-Clifford $U$:+$$U X U^\dagger \notin \{\pm X, \pm Y, \pm Z\}$$++The result is a **superposition of Pauli operators**:+$$R_X(\theta) Y R_X(-\theta) = \cos\theta \, Y + \sin\theta \, Z$$++This cannot be represented efficiently in the stabilizer formalism.++### Gottesman-Knill Theorem++The theorem states that circuits consisting of:+- Clifford gates (H, S, CNOT)+- Computational basis measurements+- Classical control++Can be simulated efficiently classically.++**Corollary:** Adding non-Clifford gates (like T or RX) enables universal quantum computation, which cannot be efficiently simulated (assuming standard complexity conjectures).++---++## Expected Behavior++### Translation Phase++The STIM-to-CHP translator should:+1. Parse the RX gate from STIM syntax+2. Check against supported gate list+3. Detect unsupported Clifford gate+4. Generate clear error message++### Expected Error Message++```+Translation error: Unsupported gate: RX+This gate is not a Clifford gate or is not yet implemented.+```++### Simulator Response++| Phase | Expected Behavior |+|-------|-------------------|+| Parse | Successfully parse STIM syntax |+| Translate | Detect unsupported gate, return error |+| Simulation | **Not executed** |+| Exit Code | Non-zero (failure) |++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Parse Status** | Success |+| **Translation Status** | Failure (expected) |+| **Error Type** | `UnsupportedGate RX` |+| **Simulation** | Not performed |+| **Test Result** | PASS (error caught as expected) |++**Key Insight:** This test verifies the simulator's error handling capability rather than its simulation capability.++**Safety:** Correct rejection of unsupported gates prevents silent production of incorrect results.
+ data/stim-circuits/unsupported-rx.expected view
@@ -0,0 +1,2 @@+# unsupported-rx: RX is non-Clifford and cannot be simulated in CHP+error_expected: "Unsupported gate: RX (non-Clifford)"
+ data/stim-circuits/unsupported-rx.stim view
@@ -0,0 +1,3 @@+# This circuit should fail - RX is not a Clifford gate+RX 0+M 0
+ data/stim-circuits/y-measurement.derive.md view
@@ -0,0 +1,167 @@+# Y-Basis Measurement: Mathematical Derivation++## Circuit Specification++```+H 0+S 0+H 0+S 0+MY 0+```++## Objective++Analyze the final state's Y-basis measurement and demonstrate non-deterministic outcomes.++---++## Pauli Y Operator++### Definition+$$Y = -iXZ = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}$$++### Eigenbasis++| Eigenstate | Eigenvalue | Form |+|-----------|-----------|------|+| $\|+i\rangle = \frac{\|0\rangle + i\|1\rangle}{\sqrt{2}}$ | +1 | $(1, 0, 1)/\sqrt{2}$ on Bloch sphere |+| $\|-i\rangle = \frac{\|0\rangle - i\|1\rangle}{\sqrt{2}}$ | -1 | $(1, 0, -1)/\sqrt{2}$ on Bloch sphere |++**Note:** $Y = -iXZ$ implies $|+i\rangle$ is eigenstate of both Y and the combination XZ.++---++## State Evolution Analysis++### Initial State++$$|\psi_0\rangle = |0\rangle$$++**Tableau:**+```yaml+stabilizers: ["+Z"]+destabilizers: ["+X"]+```++### Step 1: H++**Tableau after H:**+```yaml+stabilizers: ["+X"]+destabilizers: ["+Z"]+```++### Step 2: S++**Tableau after S:**+```yaml+stabilizers: ["+Y"]+destabilizers: ["+Z"]+```++### Step 3: H++**Tableau after H:**+```yaml+stabilizers: ["-Y"]+destabilizers: ["+Z"]+```++### Step 4: S++**Tableau after S (pre-measurement):**+```yaml+stabilizers: ["+X"]+destabilizers: ["+Y"]+```++### Stabilizer Evolution++| Step | Gate | Stabilizer | Bloch Vector |+|------|------|-----------|--------------|+| 0 | — | $+Z$ | $(0, 0, 1)$ |+| 1 | H | $+X$ | $(1, 0, 0)$ |+| 2 | S | $+Y$ | $(0, 1, 0)$ |+| 3 | H | $-Y$ | $(0, -1, 0)$ |+| 4 | S | $+X$ | $(1, 0, 0)$ |++### Conjugation Verification++**S gate action:**+- $SXS^\dagger = Y$+- $SYS^\dagger = -X$+- $SZS^\dagger = Z$++**H gate action:**+- $HXH^\dagger = Z$+- $HYH^\dagger = -Y$+- $HZH^\dagger = X$++**Verification:**+- Step 0→1: $HZH^\dagger = X$ ✓+- Step 1→2: $SXS^\dagger = Y$ ✓+- Step 2→3: $HYH^\dagger = -Y$ ✓+- Step 3→4: $S(-Y)S^\dagger = -SYS^\dagger = -(-X) = +X$ ✓++---++## Y-Basis Measurement++### Final State++$$|\psi_4\rangle = |+\rangle = \frac{|0\rangle + |1\rangle}{\sqrt{2}}$$++### Y Eigenstate Decomposition++$$|+\rangle = \frac{|+i\rangle + |-i\rangle}{\sqrt{2}} \cdot \frac{1+i}{\sqrt{2}}$$++More precisely:+$$\langle +i | + \rangle = \frac{1 + (-i)}{\sqrt{2}\sqrt{2}} = \frac{1-i}{2}$$++$$|\langle +i | + \rangle|^2 = \frac{|1-i|^2}{4} = \frac{2}{4} = \frac{1}{2}$$++$$|\langle -i | + \rangle|^2 = \frac{|1+i|^2}{4} = \frac{2}{4} = \frac{1}{2}$$++### Measurement Cases++**Case 1: Outcome +1**+```yaml+probability: 0.5+measurement_outcomes: [+1]+post_measurement_tableau:+  stabilizers: ["+Y"]+  destabilizers: ["+X"]+```++**Case 2: Outcome -1**+```yaml+probability: 0.5+measurement_outcomes: [-1]+post_measurement_tableau:+  stabilizers: ["-Y"]+  destabilizers: ["+X"]+```++---++## Expected Outcome++| Property | Expected Value |+|----------|---------------|+| **Final State** | $\|+\rangle$ |+| **Final Stabilizer** | `+X` |+| **Final Destabilizer** | `+Y` |+| **Y-Basis Measurement** | Random |+| **P(+1)** | 0.5 |+| **P(-1)** | 0.5 |+| **Tableau Validity** | True |++**Key Property:** The state $|+\rangle$ is **not** a Y eigenstate, so Y measurement gives random outcomes.++**Physical Interpretation:**+- $|+\rangle$ lies on the X-axis of the Bloch sphere+- Y measurement projects onto Y-axis (±Y poles)+- X and Y axes are orthogonal, giving equal probabilities++This tests the CHP simulator's handling of **non-deterministic measurements** in non-eigenbases.
+ data/stim-circuits/y-measurement.expected view
@@ -0,0 +1,17 @@+# y-measurement: H 0; S 0; H 0; S 0 prepares |+⟩+# Y measurement is random+deterministic: false+cases:+  - probability: 0.5+    measurement_outcomes: [+1]+    post_measurement_tableau:+      stabilizers: ["+Y"]+      destabilizers: ["+X"]+  - probability: 0.5+    measurement_outcomes: [-1]+    post_measurement_tableau:+      stabilizers: ["-Y"]+      destabilizers: ["+X"]+pre_measurement_tableau:+  stabilizers: ["+X"]+  destabilizers: ["+Y"]
+ data/stim-circuits/y-measurement.stim view
@@ -0,0 +1,8 @@+# Y-basis measurement test+# S|0⟩ = |0⟩ (eigenstate of Z), but Y|0⟩ = i|1⟩+# Need to prepare Y eigenstate+H 0+S 0+H 0+S 0+MY 0
+ src/SymplecticCHP.hs view
@@ -0,0 +1,742 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE AllowAmbiguousTypes #-}++module SymplecticCHP where++import Data.Bits+import Data.Word+import Data.Proxy (Proxy(..))+import Data.Kind (Type)+import System.Random (randomRIO)+import Data.List (sortOn, groupBy)+import Data.Function (on)+import Data.Maybe (fromJust, isJust)++-- vector-sized imports+import qualified Data.Vector.Sized as VS+import Data.Vector.Sized (Vector)+import qualified GHC.TypeNats+import GHC.TypeNats (Nat, KnownNat, natVal)++-- For type-safe finite indices+import Data.Finite (Finite)+import qualified Data.Finite as Finite++-- ============================================================================+-- PART I: GROUP STRUCTURE+-- ============================================================================++-- | A group (G, ·, e, ⁻¹) +-- +-- Mathematically, a group consists of:+-- 1. A set G+-- 2. A binary operation ·: G × G → G (multiplication)+-- 3. An identity element e ∈ G+-- 4. Inverses: for all g ∈ G, exists g⁻¹ ∈ G such that g·g⁻¹ = e+--+-- Satisfying: associativity, identity, inverse laws+class Group g where+  -- | Group multiplication+  mulG :: g -> g -> g+  +  -- | Identity element+  identityG :: g+  +  -- | Inverse+  invG :: g -> g+  +  -- | Commutator [a,b] = a·b·a⁻¹·b⁻¹+  commutatorG :: g -> g -> g+  commutatorG a b = mulG (mulG (mulG a b) (invG a)) (invG b)++-- | A group where every pair of elements either commutes or anticommutes+-- +-- This is a special property. For such groups, there exists a central+-- element z (of order 2) such that:+-- - Either [a,b] = e (commute)+-- - Or [a,b] = z (anticommute)+class Group g => BinaryCommutationGroup g where+  -- | The central element representing "anticommutation"+  -- For Pauli group, this is -I (phase 2)+  anticommutationMarker :: g+  +  -- | Check if two elements commute: [a,b] = e+  commuteG :: g -> g -> Bool+  +  -- | Check if two elements anticommute: [a,b] = z+  anticommuteG :: g -> g -> Bool+  anticommuteG a b = not (commuteG a b)++-- ============================================================================+-- PART II: SYMPLECTIC VECTOR SPACE STRUCTURE+-- ============================================================================++-- | A symplectic vector space (V, ω) over a field k.+-- +-- Mathematically, a symplectic vector space consists of:+-- 1. A vector space V over a field k+-- 2. A symplectic form ω: V × V → k that is:+--    - Bilinear+--    - Alternating: ω(v, v) = 0 for all v+--    - Non-degenerate: if ω(v, w) = 0 for all w, then v = 0+--+-- Note: "Commute" and "anticommute" are NOT part of this abstraction.+-- They are specific to the Pauli group interpretation where:+-- - ω(v1, v2) = 0 is interpreted as "commute"+-- - ω(v1, v2) = 1 is interpreted as "anticommute"+class Eq (Field v) => SymplecticVectorSpace v where+  type Field v :: Type+  +  -- | The zero element of the field (needed for isotropy checks)+  fieldZero :: proxy v -> Field v+  +  -- | The symplectic form ω(v1, v2)+  -- This is a bilinear, alternating, non-degenerate form+  omega :: v -> v -> Field v+  +  -- | Vector addition (abelian group operation)+  addV :: v -> v -> v+  +  -- | Zero vector (identity for addV)+  zeroV :: v+  +  -- | Negation (additive inverse)+  negateV :: v -> v++-- | Check if a vector is isotropic: ω(v, v) = fieldZero+-- In a symplectic vector space, ALL vectors are isotropic (alternating property)+isIsotropicElement :: (SymplecticVectorSpace v, Eq (Field v)) => proxy v -> v -> Bool+isIsotropicElement p v = omega v v == fieldZero p++-- | Check if two vectors are symplectically orthogonal: ω(v1, v2) = fieldZero+symplecticOrthogonal :: (SymplecticVectorSpace v, Eq (Field v)) => proxy v -> v -> v -> Bool+symplecticOrthogonal p v1 v2 = omega v1 v2 == fieldZero p++-- | For Pauli group specifically: two operators commute iff ω = 0+-- This is an interpretation specific to F_2+commuteV :: (SymplecticVectorSpace v, Field v ~ Bool) => v -> v -> Bool+commuteV v1 v2 = not (omega v1 v2)++-- | For Pauli group specifically: two operators anticommute iff ω = 1+-- This is an interpretation specific to F_2+anticommuteV :: (SymplecticVectorSpace v, Field v ~ Bool) => v -> v -> Bool+anticommuteV v1 v2 = omega v1 v2++-- ============================================================================+-- PART III: THE CRUCIAL CONNECTION - SYMPLECTIC GROUP+-- ============================================================================++-- | A group that is also a symplectic vector space via quotient by center.+--+-- The Pauli group is a central extension:+-- 1 → Z(G) → G → V → 1+-- where:+-- - Z(G) is the center (phases for Pauli: {±I, ±iI})+-- - V = G/Z(G) is the symplectic vector space (F_2)^(2n)+-- - The commutator [a,b] corresponds to the symplectic form ω(ā, b̄)+--+-- Key theorem: [a,b] = e ⟺ ω(ā, b̄) = 0+--              [a,b] = z ⟺ ω(ā, b̄) ≠ 0+-- where ā is the projection of a to V, z = anticommutationMarker+class (BinaryCommutationGroup g, SymplecticVectorSpace v) +      => SymplecticGroup g v | g -> v where+  -- | Project to the symplectic quotient (strip phases)+  toSymplectic :: g -> v+  +  -- | Lift from symplectic quotient (add phase, if possible)+  fromSymplectic :: v -> Maybe g+  +  -- | The fundamental theorem: commutator is determined by symplectic form+  -- [a,b] = e  ⟺  ω(ā, b̄) = 0+  symplecticCommutation :: g -> g -> Bool+  symplecticCommutation a b = +    let va = toSymplectic a+        vb = toSymplectic b+        p = Proxy :: Proxy v+    in omega va vb == fieldZero p++-- ============================================================================+-- PART IV: ISOTROPIC AND LAGRANGIAN SUBSPACES+-- ============================================================================++-- | An isotropic subspace: ω vanishes on all pairs+-- +-- Mathematically: W ⊂ V such that ω|_{W×W} = 0+-- Dimension bound: dim(W) ≤ n in a 2n-dimensional symplectic space+class (KnownNat n, SymplecticVectorSpace v) => IsotropicSubSpace s n v where+  -- | Get the underlying basis vectors+  toBasis :: s n v -> Vector n v+  +  -- | Check isotropy: ω(v_i, v_j) = fieldZero for all i, j+  verifyIsotropy :: s n v -> Bool+  verifyIsotropy s = +    let vs = toBasis s+        p = Proxy :: Proxy v+    in VS.all (\v_i -> VS.all (\v_j -> symplecticOrthogonal p v_i v_j) vs) vs+  +  -- | Get the dimension (always n for this representation)+  dimSubspace :: s n v -> Int+  dimSubspace _ = fromIntegral $ natVal (Proxy @n)++-- | Lagrangian subspace: maximal isotropic (dim = n in 2n-dim space)+-- +-- A Lagrangian subspace is isotropic and maximal with respect to inclusion.+-- These correspond to maximal abelian subgroups of the Pauli group.+class IsotropicSubSpace s n v => LagrangianSubSpace s n v++-- ============================================================================+-- PART V: THE ABELIAN-LAGRANGIAN CORRESPONDENCE+-- ============================================================================++-- | The fundamental correspondence:+-- Abelian subgroups of a SymplecticGroup ⟷ Isotropic subspaces of V+--+-- Key insight: +-- - Pauli operators P₁, P₂ commute  ⟺  ω(v₁, v₂) = 0+-- - A set of commuting Paulis forms an Abelian subgroup  ⟺  +--   The corresponding vectors form an Isotropic subspace+-- - A MAXIMAL commuting set  ⟺  A LAGRANGIAN subspace (dimension = n)+class SymplecticGroup g v => AbelianLagrangianCorrespondence g n v | g -> v where+  -- | The type representing abelian subgroups of g+  -- These correspond to isotropic subspaces of the quotient+  type IsotropicSubgroup g :: Nat -> Type+  +  -- | Convert an abelian subgroup to an isotropic subspace+  -- This strips phases and takes the span in V+  subgroupToIsotropic :: IsotropicSubgroup g n -> Lagrangian n v+  +  -- | Lift an isotropic subspace to an abelian subgroup+  -- This adds canonical phases (usually 0) to each generator+  isotropicToSubgroup :: Lagrangian n v -> IsotropicSubgroup g n+  +  -- | Verify the fundamental invariant: abelian ⟺ isotropic+  -- For all a, b in subgroup: [a,b] = e  ⟺  ω(ā, b̄) = 0+  abelianIffIsotropic :: IsotropicSubgroup g n -> Bool++-- | Maximal abelian subgroups correspond to Lagrangian subspaces+class AbelianLagrangianCorrespondence g n v => MaximalAbelianCorrespondence g n v where+  -- | Check if abelian subgroup is maximal (dimension = n)+  isMaximalAbelian :: IsotropicSubgroup g n -> Bool+  +  -- | The correspondence: maximal abelian ⟺ Lagrangian+  maximalAbelianIffLagrangian :: IsotropicSubgroup g n -> Bool++-- ============================================================================+-- PART VI: THE SYMPLECTIC BASIS THEOREM (The Crown Jewel)+-- ============================================================================++-- | The Symplectic Basis Theorem: Every symplectic vector space admits+-- a canonical basis (Darboux basis) that puts ω in standard form.+--+-- Mathematical Statement:+-- Let (V, ω) be a symplectic vector space over field k, dim(V) = 2n.+-- Then there exists a basis {e₁,...,eₙ, f₁,...,fₙ} such that:+--   ω(eᵢ, eⱼ) = 0         (e's span a Lagrangian)+--   ω(fᵢ, fⱼ) = 0         (f's span a Lagrangian)  +--   ω(eᵢ, fⱼ) = δᵢⱼ       (duality)+--+-- This is equivalent to saying V decomposes as L ⊕ L* where L is Lagrangian.+class (KnownNat n, SymplecticVectorSpace v) => SymplecticBasisTheorem s n v where+  -- | Get the first Lagrangian (traditionally "position" or stabilizers)+  firstLagrangian :: s n v -> Lagrangian n v+  +  -- | Get the second Lagrangian (traditionally "momentum" or destabilizers)+  secondLagrangian :: s n v -> Lagrangian n v+  +  -- | Verify the duality condition: ω(secondᵢ, firstⱼ) = δᵢⱼ+  verifyDuality :: s n v -> Bool++-- ============================================================================+-- PART VII: CONCRETE IMPLEMENTATION - PAULI GROUP+-- ============================================================================++-- | Pauli operator P = i^phase · X^x Z^z as symplectic vector (x|z) ∈ F_2^(2n)+-- The symplectic form ω((x1|z1), (x2|z2)) = x1·z2 + z1·x2 (mod 2)+-- ω = 0 ⟺ commute, ω = 1 ⟺ anti-commute+data Pauli = Pauli +  { xVec :: !Word64      -- ^ X-support bitmask+  , zVec :: !Word64      -- ^ Z-support bitmask  +  , phase :: !Int        -- ^ i^phase overall phase (0,1,2,3)+  } +  deriving (Eq, Show)++-- | Group instance: Pauli operators form a group under multiplication+instance Group Pauli where+  mulG = multiplyPauli+  identityG = Pauli 0 0 0+  invG (Pauli x z r) = Pauli x z ((4 - r) `mod` 4)++-- | Binary commutation: Pauli operators either commute or anticommute+instance BinaryCommutationGroup Pauli where+  -- The anticommutation marker is -I (phase 2)+  anticommutationMarker = Pauli 0 0 2+  +  -- Two Paulis commute iff ω = 0 (symplectic form vanishes)+  commuteG p1 p2 = not (omegaPauli p1 p2)++-- | Helper: compute omega for Pauli (ignoring phase)+omegaPauli :: Pauli -> Pauli -> Bool+omegaPauli (Pauli x1 z1 _) (Pauli x2 z2 _) = +  odd (popCount ((x1 .&. z2) `xor` (z1 .&. x2)))++-- | Pauli group multiplication with phase tracking+multiplyPauli :: Pauli -> Pauli -> Pauli+multiplyPauli (Pauli x1 z1 r1) (Pauli x2 z2 r2) =+  let x = x1 `xor` x2+      z = z1 `xor` z2+      -- Symplectic phase: i^{x1·z2} (-i)^{z1·x2} = i^{x1·z2 - z1·x2}+      symPhase = popCount (x1 .&. z2) - popCount (z1 .&. x2)+      r = (r1 + r2 + symPhase) `mod` 4+  in Pauli x z r++-- | Symplectic vector space structure on Pauli (modulo phases)+-- The quotient Pauli / {phases} ≅ (F_2)^(2n)+instance SymplecticVectorSpace Pauli where+  type Field Pauli = Bool  -- ^ F_2, represented as Bool+  +  -- | Zero element of F_2 (False = 0)+  fieldZero _ = False+  +  -- | Symplectic inner product ω: Pauli × Pauli → F_2+  -- ω(P₁, P₂) = x₁·z₂ + z₁·x₂ (mod 2)+  -- This is bilinear, alternating, and non-degenerate+  omega = omegaPauli+  +  -- | Pauli group multiplication is vector addition in (F_2)^(2n)+  -- (ignoring phase)+  addV = multiplyPauli+  +  -- | Identity element (zero vector)+  zeroV = Pauli 0 0 0+  +  -- | Inverse (negation) - conjugate by changing phase+  negateV (Pauli x z r) = Pauli x z ((4 - r) `mod` 4)++-- | The symplectic group connection: Pauli → (F_2)^(2n)+instance SymplecticGroup Pauli Pauli where+  -- The projection strips the phase, keeping only (x|z)+  toSymplectic (Pauli x z _) = Pauli x z 0+  +  -- Lift adds zero phase+  fromSymplectic (Pauli x z r) = Just (Pauli x z ((r `mod` 4 + 4) `mod` 4))+  +  -- The fundamental theorem: [P,Q] = I ⟺ ω(P,Q) = 0+  symplecticCommutation = commuteG++-- ============================================================================+-- PART VIII: LAGRANGIAN SUBSPACE DATA TYPE+-- ============================================================================++-- | A Lagrangian subspace is a maximal isotropic subspace of dimension n+-- in a 2n-dimensional symplectic vector space.+-- It is represented by n basis vectors.+newtype Lagrangian (n :: Nat) v = Lagrangian+  { lagrangianBasis :: Vector n v  -- ^ n basis vectors spanning the subspace+  }+  deriving (Show)++-- | Isotropic subspace instance+instance (KnownNat n, SymplecticVectorSpace v) => IsotropicSubSpace Lagrangian n v where+  toBasis = lagrangianBasis++-- | Lagrangian subspace instance+instance (KnownNat n, SymplecticVectorSpace v) => LagrangianSubSpace Lagrangian n v++-- | Map over a Lagrangian (apply symplectic transformation)+mapLagrangian :: (v -> v) -> Lagrangian n v -> Lagrangian n v+mapLagrangian f (Lagrangian vs) = Lagrangian (VS.map f vs)++-- | Index into a Lagrangian+indexLagrangian :: Lagrangian n v -> Finite n -> v+indexLagrangian (Lagrangian vs) i = VS.index vs i++-- | Convert Lagrangian to list+toListLagrangian :: Lagrangian n v -> [v]+toListLagrangian (Lagrangian vs) = VS.toList vs++-- ============================================================================+-- PART IX: TABLEAU AS SYMPLECTIC BASIS+-- ============================================================================++-- | The CHP Tableau is the computational realization of the +-- Symplectic Basis Theorem for the Pauli group.+--+-- Tableau n v = (Lagrangian n v, Lagrangian n v) with duality+-- where:+-- - First Lagrangian = Stabilizers S (isotropic)+-- - Second Lagrangian = Destabilizers D (isotropic)+-- - Duality: ω(Dᵢ, Sⱼ) = δᵢⱼ+data Tableau (n :: Nat) v where+  Tableau :: (SymplecticVectorSpace v, Field v ~ Bool) =>+    { stabLagrangian :: Lagrangian n v      -- ^ S: first Lagrangian (stabilizers)+    , destabLagrangian :: Lagrangian n v    -- ^ D: second Lagrangian (destabilizers)+    } -> Tableau n v++-- | Tableau implements the Symplectic Basis Theorem!+instance (KnownNat n, SymplecticVectorSpace v, Field v ~ Bool) +         => SymplecticBasisTheorem Tableau n v where+  firstLagrangian = stabLagrangian+  secondLagrangian = destabLagrangian+  +  -- Verify: ω(Dᵢ, Sⱼ) = δᵢⱼ+  verifyDuality tab =+    let s = stabLagrangian tab+        d = destabLagrangian tab+        vs = lagrangianBasis s+        vd = lagrangianBasis d+    in VS.and $ VS.imap (\i d_i ->+         VS.and $ VS.imap (\j s_j ->+           if i == j +           then omega d_i s_j == True   -- ω(Dᵢ, Sᵢ) = 1+           else omega d_i s_j == False  -- ω(Dᵢ, Sⱼ) = 0 for i≠j+         ) vs+       ) vd++-- ============================================================================+-- PART X: TABLEAU OPERATIONS+-- ============================================================================++-- | Get the number of qubits (dimension of each Lagrangian)+nQubits :: forall n v. KnownNat n => Tableau n v -> Int+nQubits _ = fromIntegral $ natVal (Proxy @n)++-- | Get a stabilizer by index+getStabilizer :: Tableau n v -> Finite n -> v+getStabilizer tab i = indexLagrangian (stabLagrangian tab) i++-- | Get a destabilizer by index  +getDestabilizer :: Tableau n v -> Finite n -> v+getDestabilizer tab i = indexLagrangian (destabLagrangian tab) i++-- | Get stabilizer by Int index (for backward compatibility)+stabilizer :: forall n v. (KnownNat n, SymplecticVectorSpace v, Field v ~ Bool) => Tableau n v -> Int -> Maybe v+stabilizer tab i = do+  fin <- intToFinite i+  return $ getStabilizer tab fin++-- | Get destabilizer by Int index (for backward compatibility)+destabilizer :: forall n v. (KnownNat n, SymplecticVectorSpace v, Field v ~ Bool) => Tableau n v -> Int -> Maybe v+destabilizer tab i = do+  fin <- intToFinite i+  return $ getDestabilizer tab fin++-- | Convert Int to Finite safely+intToFinite :: forall n. KnownNat n => Int -> Maybe (Finite n)+intToFinite i +  | i >= 0 = Finite.packFinite (fromIntegral i)+  | otherwise = Nothing++-- | Get all rows as a list [S_0..S_{n-1}, D_0..D_{n-1}] (for backward compatibility)+rows :: (KnownNat n, SymplecticVectorSpace v) => Tableau n v -> [v]+rows tab = toListLagrangian (stabLagrangian tab) ++ toListLagrangian (destabLagrangian tab)++-- | Initial state |0...0⟩: S_i = Z_i, D_i = X_i+-- This is the standard symplectic basis for the initial state+emptyTableau :: forall n. KnownNat n => Tableau n Pauli+emptyTableau = Tableau stabs destabs+  where+    stabs = Lagrangian $ VS.generate $ \i ->+      let idx = fromIntegral (Finite.getFinite i)+      in Pauli 0 (bit idx) 0        -- Z_i stabilizer+    destabs = Lagrangian $ VS.generate $ \i ->+      let idx = fromIntegral (Finite.getFinite i)+      in Pauli (bit idx) 0 0        -- X_i destabilizer++-- | Verify tableau validity (symplectic basis conditions)+-- This checks the three conditions from the Symplectic Basis Theorem:+-- 1. Stabilizers are isotropic: ω(Sᵢ, Sⱼ) = 0+-- 2. Destabilizers are isotropic: ω(Dᵢ, Dⱼ) = 0+-- 3. Duality: ω(Dᵢ, Sⱼ) = δᵢⱼ+isValid :: forall n v. (KnownNat n, SymplecticVectorSpace v, Field v ~ Bool, SymplecticBasisTheorem Tableau n v) +        => Tableau n v -> Bool+isValid tab = +  let s = stabLagrangian tab+      d = destabLagrangian tab+      vs = lagrangianBasis s+      vd = lagrangianBasis d+      p = Proxy :: Proxy v+      -- Check stabilizers are isotropic: ω(Sᵢ, Sⱼ) = 0+      stabIsotropic = VS.all (\s_i -> VS.all (\s_j -> symplecticOrthogonal p s_i s_j) vs) vs+      -- Check destabilizers are isotropic: ω(Dᵢ, Dⱼ) = 0+      destIsotropic = VS.all (\d_i -> VS.all (\d_j -> symplecticOrthogonal p d_i d_j) vd) vd+      -- Check dual pairing: ω(Dᵢ, Sⱼ) = δᵢⱼ (via SymplecticBasisTheorem)+      dualPairing = verifyDuality tab+  in stabIsotropic && destIsotropic && dualPairing++-- ============================================================================+-- PART XI: CLIFFORD GATES AS SYMPLECTIC TRANSFORMATIONS+-- ============================================================================++-- | Symplectic transformation on single qubit i+data LocalSymplectic +  = Hadamard !Int      -- ^ H: (x_i, z_i) ↦ (z_i, x_i)+  | Phase !Int         -- ^ S: (x_i, z_i) ↦ (x_i, x_i + z_i)+  deriving (Show)++-- | Two-qubit symplectic+data SymplecticGate+  = Local !LocalSymplectic+  | CNOT !Int !Int     -- ^ (x_c, z_c, x_t, z_t) ↦ (x_c, z_c+z_t, x_t+x_c, z_t)+  deriving (Show)++-- | Apply symplectic gate to Pauli operator (conjugation P ↦ U P U†)+-- This is a symplectic transformation on the vector space+applyGate :: SymplecticGate -> Pauli -> Pauli+applyGate (Local (Hadamard i)) (Pauli x z r) =+  let xi = testBit x i+      zi = testBit z i+      mask = complement (bit i)+      x' = (x .&. mask) .|. (if zi then bit i else 0)+      z' = (z .&. mask) .|. (if xi then bit i else 0)+      r' = (r + if xi && zi then 2 else 0) `mod` 4+  in Pauli x' z' r'++applyGate (Local (Phase i)) (Pauli x z r) =+  let xi = testBit x i+      z' = if xi then z `xor` bit i else z+      -- Phase update: X->Y (+1), Y->-X (+1), Z->Z (0)+      r' = (r + if xi then 1 else 0) `mod` 4+  in Pauli x z' r'++applyGate (CNOT c t) (Pauli x z r) =+  let xc = testBit x c; zc = testBit z c+      xt = testBit x t; zt = testBit z t+      x' = if xc then x `xor` bit t else x+      z' = if zt then z `xor` bit c else z+      phaseTerm = if xc && zt then (if xt `xor` zc then 2 else 0) + 1 else 0+      r' = (r + phaseTerm) `mod` 4+  in Pauli x' z' r'++-- | Apply gate to entire tableau (conjugate both Lagrangians)+-- Since Clifford gates preserve the symplectic form, they map+-- symplectic bases to symplectic bases (per Symplectic Basis Theorem).+evolveTableau :: KnownNat n => Tableau n Pauli -> SymplecticGate -> Tableau n Pauli+evolveTableau (Tableau s d) g = +  let s' = mapLagrangian (applyGate g) s+      d' = mapLagrangian (applyGate g) d+  in Tableau s' d'++-- ============================================================================+-- PART XII: MEASUREMENT VIA SYMPLECTIC DECOMPOSITION+-- ============================================================================++data MeasurementResult = Determinate Bool | Random Bool+  deriving (Show)++-- | Test if measurement is deterministic: P must commute with stabilizer subspace+isDeterminate :: KnownNat n => Tableau n Pauli -> Pauli -> Bool+isDeterminate tab p = +  VS.all (\s_i -> commuteG p s_i) (lagrangianBasis $ stabLagrangian tab)++-- | Find stabilizer index j such that P anti-commutes with S_j+findAntiCommutingStab :: forall n. KnownNat n => Tableau n Pauli -> Pauli -> Maybe Int+findAntiCommutingStab tab p =+  let s = stabLagrangian tab+  in VS.ifoldl' (\acc (i :: Finite n) s_i ->+    case acc of+      Just _ -> acc+      Nothing -> if anticommuteG p s_i then Just (fromIntegral $ Finite.getFinite i) else Nothing) Nothing (lagrangianBasis s)++-- | Update a vector at a specific index+updateVector :: KnownNat n => Int -> a -> Vector n a -> Vector n a+updateVector i v vec = VS.unsafeUpd vec [(i, v)]++-- | Update a Lagrangian at a specific index+updateLagrangian :: KnownNat n => Finite n -> v -> Lagrangian n v -> Lagrangian n v+updateLagrangian i v (Lagrangian vs) = Lagrangian (VS.unsafeUpd vs [(fromIntegral $ Finite.getFinite i, v)])++-- | Measurement as state update (symplectic transvection)+measure :: forall n. KnownNat n => Tableau n Pauli -> Pauli -> IO (Tableau n Pauli, MeasurementResult)+measure tab@(Tableau s d) p+  | isDeterminate tab p = do+      let outcome = computePhase tab p+      return (tab, Determinate outcome)+  +  | otherwise = do+      let Just j = findAntiCommutingStab tab p+          Just jFin = intToFinite j+          s_j = indexLagrangian s jFin+          +          newStabBasis = VS.imap (\(k :: Finite n) s_k ->+            if k == jFin +              then p+              else if anticommuteG p (indexLagrangian s k)+                   then multiplyPauli s_k s_j+                   else s_k) (lagrangianBasis s)+          +          newDestabBasis = updateVector j s_j (lagrangianBasis d)+      +      outcome <- randomRIO (0, 1) :: IO Int+      +      let Pauli x z r = p+          p' = Pauli x z ((r + if outcome == 0 then 2 else 0) `mod` 4)+          finalStabBasis = updateVector j p' newStabBasis+          finalStabs = Lagrangian finalStabBasis+          newDestabs = Lagrangian newDestabBasis+      +      return (Tableau finalStabs newDestabs, Random (outcome == 1))++-- | Compute deterministic measurement outcome via symplectic decomposition+computePhase :: forall n. KnownNat n => Tableau n Pauli -> Pauli -> Bool+computePhase (Tableau s d) p = +  let scratch = VS.ifoldl' (\acc (j :: Finite n) d_j ->+        if anticommuteG p d_j+          then multiplyPauli acc (indexLagrangian s j)+          else acc) (Pauli 0 0 0) (lagrangianBasis d)+      totalPhase = (phase p - phase scratch) `mod` 4+  in totalPhase == 0++-- ============================================================================+-- PART XIII: MONADIC INTERFACE+-- ============================================================================++data SomeTableau where+  SomeTableau :: KnownNat n => Tableau n Pauli -> SomeTableau++newtype Clifford a = Clifford { runClifford :: SomeTableau -> IO (SomeTableau, a) }++instance Functor Clifford where+  fmap f (Clifford g) = Clifford $ \t -> do (t', x) <- g t; return (t', f x)++instance Applicative Clifford where+  pure x = Clifford $ \t -> return (t, x)+  Clifford f <*> Clifford x = Clifford $ \t -> do+    (t', f') <- f t; (t'', x') <- x t'; return (t'', f' x')++instance Monad Clifford where+  return = pure+  Clifford x >>= f = Clifford $ \t -> do (t', x') <- x t; runClifford (f x') t'++gate :: SymplecticGate -> Clifford ()+gate g = Clifford $ \t -> case t of+  SomeTableau tab -> return (SomeTableau (evolveTableau tab g), ())++measurePauli :: Pauli -> Clifford Bool+measurePauli p = Clifford $ \t -> case t of+  SomeTableau tab -> do+    (t', res) <- measure tab p+    case res of+      Determinate b -> return (SomeTableau t', b)+      Random b      -> return (SomeTableau t', b)++getTableau :: Clifford SomeTableau+getTableau = Clifford $ \t -> return (t, t)++withNatProxy :: KnownNat n => Proxy n -> (KnownNat n => Tableau n Pauli) -> Tableau n Pauli+withNatProxy _ t = t++emptyTableauN :: Int -> SomeTableau+emptyTableauN n+  | n < 0 = error $ "Invalid qubit count: " ++ show n+  | otherwise = case GHC.TypeNats.someNatVal (fromIntegral n) of+      GHC.TypeNats.SomeNat (proxy :: Proxy n) -> +        SomeTableau (emptyTableau :: Tableau n Pauli)++runWith :: Int -> Clifford a -> IO (SomeTableau, a)+runWith n (Clifford f) = f (emptyTableauN n)++-- ============================================================================+-- PART XIV: BACKWARD COMPATIBILITY HELPERS+-- ============================================================================++rowsSome :: SomeTableau -> [Pauli]+rowsSome (SomeTableau tab) = rows tab++nQubitsSome :: SomeTableau -> Int+nQubitsSome (SomeTableau tab) = nQubits tab++stabilizerSome :: SomeTableau -> Int -> Maybe Pauli+stabilizerSome (SomeTableau tab) i = stabilizer tab i++destabilizerSome :: SomeTableau -> Int -> Maybe Pauli+destabilizerSome (SomeTableau tab) i = destabilizer tab i++isValidSome :: SomeTableau -> Bool+isValidSome (SomeTableau tab) = isValid tab++evolveTableauSome :: SomeTableau -> SymplecticGate -> SomeTableau+evolveTableauSome (SomeTableau tab) g = SomeTableau (evolveTableau tab g)++measureSome :: SomeTableau -> Pauli -> IO (SomeTableau, MeasurementResult)+measureSome (SomeTableau tab) p = do+  (tab', res) <- measure tab p+  return (SomeTableau tab', res)++isDeterminateSome :: SomeTableau -> Pauli -> Bool+isDeterminateSome (SomeTableau tab) p = isDeterminate tab p++findAntiCommutingStabSome :: SomeTableau -> Pauli -> Maybe Int+findAntiCommutingStabSome (SomeTableau tab) p = findAntiCommutingStab tab p++computePhaseSome :: SomeTableau -> Pauli -> Bool+computePhaseSome (SomeTableau tab) p = computePhase tab p++-- ============================================================================+-- PART XV: EXAMPLES AND HELPERS+-- ============================================================================++bellCircuit :: Clifford Bool+bellCircuit = do+  gate (Local (Hadamard 0))+  gate (CNOT 0 1)+  measurePauli (Pauli (bit 0) (bit 0) 0)++pauliX :: Int -> Pauli+pauliX i = Pauli (bit i) 0 0++pauliZ :: Int -> Pauli+pauliZ i = Pauli 0 (bit i) 0++pauliY :: Int -> Pauli+pauliY i = Pauli (bit i) (bit i) 1++-- | Backward compatibility: symplectic form+symplecticForm :: Pauli -> Pauli -> Bool+symplecticForm p1 p2 = not (omegaPauli p1 p2)++-- | Backward compatibility: commute+commute :: Pauli -> Pauli -> Bool+commute = commuteG++-- | Backward compatibility: anticommute+anticommute :: Pauli -> Pauli -> Bool+anticommute = anticommuteG++-- | Backward compatibility: multiply+multiply :: Pauli -> Pauli -> Pauli+multiply = multiplyPauli++-- ============================================================================+-- PART XVI: UTILITIES+-- ============================================================================++(//) :: [a] -> [(Int, a)] -> [a]+xs // [] = xs+xs // updates = +  let sorted = sortOn fst updates+      grouped = groupBy ((==) `on` fst) sorted+      finalUpdates = [(i, v) | grp@((i,_):_) <- grouped, let (_,v) = last grp]+      go _ [] [] = []+      go i (x:xs) ups@((ui,uv):us)+        | i == ui   = uv : go (i+1) xs us+        | i < ui    = x  : go (i+1) xs ups+        | otherwise = go i (x:xs) us+      go i xs [] = xs+      go _ [] _ = []+  in go 0 xs finalUpdates
+ symplectic-chp.cabal view
@@ -0,0 +1,168 @@+cabal-version:      3.0+-- The cabal-version field refers to the version of the .cabal specification,+-- and can be different from the cabal-install (the tool) version and the+-- Cabal (the library) version you are using. As such, the Cabal (the library)+-- version used must be equal or greater than the version stated in this field.+-- Starting from the specification version 2.2, the cabal-version field must be+-- the first thing in the cabal file.++-- Initial package description 'symplectic-chp' generated by+-- 'cabal init'. For further documentation, see:+--   http://haskell.org/cabal/users-guide/+--+-- The name of the package.+name:               symplectic-chp++-- Tested GHC versions+-- GHC 9.2 has compatibility issues with stim-parser dependency+tested-with:        GHC == 9.4.8+                  , GHC == 9.6.7+                  , GHC == 9.8.4+                  , GHC == 9.10.1+                  , GHC == 9.12.2++-- The package version.+-- See the Haskell package versioning policy (PVP) for standards+-- guiding when and how versions should be incremented.+-- https://pvp.haskell.org+-- PVP summary:     +-+------- breaking API changes+--                  | | +----- non-breaking API additions+--                  | | | +--- code changes with no API change+version:            0.1.0.0++-- A short (one-line) description of the package.+synopsis:           CHP Clifford simulator using symplectic geometry++-- A longer description of the package.+description:        A Haskell implementation of the CHP Clifford simulator through the lens of symplectic geometry. Includes a library for programmatic circuit construction and a command-line tool for simulating STIM circuit files.++-- The license under which the package is released.+license:            MIT++-- The file containing the license text.+license-file:       LICENSE++-- The package author(s).+author:             overshiki++-- An email address to which users can send suggestions, bug reports, and patches.+maintainer:         le.niu@hotmail.com++-- A copyright notice.+copyright:          2026 overshiki++-- Category for Hackage+category:           Physics, Quantum Computing, Math++-- Homepage and bug tracker+homepage:           https://github.com/overshiki/symplectic-chp+bug-reports:        https://github.com/overshiki/symplectic-chp/issues++-- Build information+build-type:         Simple++-- Extra doc files to be distributed with the package, such as a CHANGELOG or a README.+extra-doc-files:    CHANGELOG.md, README.md++-- Extra source files to be distributed with the package, such as examples, or a tutorial module.+extra-source-files: data/stim-circuits/*.stim,+                    data/stim-circuits/*.expected,+                    data/stim-circuits/*.derive.md++source-repository head+    type:     git+    location: https://github.com/overshiki/symplectic-chp++common warnings+    ghc-options: -Wall++common test-settings+  import:           warnings+  default-language: GHC2021+  ghc-options:+    -O0+    -threaded+    -rtsopts++library +    import:           warnings+    exposed-modules:+        SymplecticCHP+    build-depends:+        , base                >= 4.17    && < 4.22+        , vector              >= 0.12    && < 0.14+        , vector-sized        >= 1.5     && < 1.7+        , finite-typelits     >= 0.1     && < 0.3+        , primitive           >= 0.7     && < 0.10+        , random              >= 1.2     && < 1.3+        , mtl                 >= 2.2     && < 2.4+        , transformers        >= 0.5     && < 0.7+        , deepseq             >= 1.4     && < 1.6+    hs-source-dirs:     src+    default-language:   GHC2021++test-suite symplectic-chp-test+    import:           test-settings+    type:             exitcode-stdio-1.0+    hs-source-dirs:   test, app+    main-is:          Spec.hs+    other-modules:+        Test.TableauSpec+        Test.GatesSpec+        Test.MeasurementSpec+        Test.UtilsSpec+        Test.Examples+        Test.Arbitrary+        Test.StimCircuitSpec+        CHPCircuit+        CLI+        Simulator+        StimToCHP+    build-depends:+        , symplectic-chp+        , base                >= 4.17    && < 4.22+        , hspec               >= 2.10    && < 2.12+        , hspec-discover      >= 2.10    && < 2.12+        , QuickCheck          >= 2.14    && < 2.16+        , vector              >= 0.12    && < 0.14+        , vector-sized        >= 1.5     && < 1.7+        , finite-typelits     >= 0.1     && < 0.3+        , random              >= 1.2     && < 1.3+        , filepath            >= 1.4     && < 1.6+        , directory           >= 1.3     && < 1.4+        , containers          >= 0.6     && < 0.8+        , stim-parser         >= 0.1     && < 0.2+    build-tool-depends:+        hspec-discover:hspec-discover  >= 2.10 && < 2.12+    default-language: GHC2021++executable symplectic-chp+    -- Import common warning flags.+    import:           warnings++    -- .hs or .lhs file containing the Main module.+    main-is:          Main.hs++    -- Modules included in this executable, other than Main.+    other-modules:+        CHPCircuit+        CLI+        Simulator+        StimToCHP++    -- LANGUAGE extensions used by modules in this package.+    -- other-extensions:++    -- Other library packages from which modules are imported.+    build-depends:+          , base                >= 4.17    && < 4.22+          , stim-parser         >= 0.1     && < 0.2+          , containers          >= 0.6     && < 0.8+          , symplectic-chp+          , random              >= 1.2     && < 1.3++    -- Directories containing source files.+    hs-source-dirs:   app++    -- Base language which the package is written in.+    default-language: GHC2021
+ test/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+ test/Test/Arbitrary.hs view
@@ -0,0 +1,39 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}++module Test.Arbitrary where++import Test.QuickCheck+import SymplecticCHP+import Data.Bits ((.&.), bit)+import Data.Word (Word64)++instance Arbitrary Pauli where+  arbitrary = do+    x <- chooseInt (0, 0xFFFF) :: Gen Int+    z <- chooseInt (0, 0xFFFF) :: Gen Int+    p <- chooseInt (0, 3)+    return $ Pauli (fromIntegral x) (fromIntegral z) p+  +  shrink (Pauli x z p) = +    [Pauli x' z' p' | x' <- shrink x, x' >= 0, z' <- shrink z, z' >= 0, p' <- [0..p]]++instance Arbitrary LocalSymplectic where+  arbitrary = oneof +    [ Hadamard <$> chooseInt (0, 10)+    , Phase <$> chooseInt (0, 10)+    ]++instance Arbitrary SymplecticGate where+  arbitrary = frequency+    [ (3, Local <$> arbitrary)+    , (1, do c <- chooseInt (0, 10)+             t <- chooseInt (0, 10)+             return $ if c /= t then CNOT c t else Local (Hadamard 0))+    ]++newtype SmallN = SmallN { unSmallN :: Int }+  deriving (Show, Eq)++instance Arbitrary SmallN where+  arbitrary = SmallN <$> chooseInt (1, 10)+  shrink (SmallN n) = SmallN <$> [n' | n' <- shrink n, n' > 0]
+ test/Test/Examples.hs view
@@ -0,0 +1,17 @@+module Test.Examples where++import Test.Hspec+import SymplecticCHP+import Data.Maybe (fromJust)++spec :: Spec+spec = describe "SymplecticCHP Examples" $ do+  describe "Bell state" $ do+    it "prepares entangled state" $ do+      (tab, outcome) <- runWith 2 bellCircuit+      outcome `shouldBe` True  -- X⊗X should measure +1+      -- Check stabilizers using SomeTableau helper+      let s0 = fromJust $ stabilizerSome tab 0+          s1 = fromJust $ stabilizerSome tab 1+      -- Bell state has stabilizers XX and ZZ+      commute s0 s1 `shouldBe` True
+ test/Test/GatesSpec.hs view
@@ -0,0 +1,123 @@+module Test.GatesSpec where++import Test.Hspec+import Test.QuickCheck+import SymplecticCHP+import Data.Bits (bit, testBit, popCount, xor)+import Test.Arbitrary++spec :: Spec+spec = describe "SymplecticCHP.Gates" $ do+  describe "Hadamard gate" $ do+    it "converts X to Z" $ do+      let x0 = pauliX 0+          x0' = applyGate (Local (Hadamard 0)) x0+      xVec x0' `shouldBe` 0+      zVec x0' `shouldBe` 1+      xVec x0 `shouldBe` 1  -- original unchanged+    +    it "converts Z to X" $ do+      let z0 = pauliZ 0+          z0' = applyGate (Local (Hadamard 0)) z0+      xVec z0' `shouldBe` 1+      zVec z0' `shouldBe` 0+    +    it "converts Y to -Y (phase flip)" $ do+      let y0 = pauliY 0+          y0' = applyGate (Local (Hadamard 0)) y0+      xVec y0' `shouldBe` 1+      zVec y0' `shouldBe` 1+      phase y0' `shouldBe` (phase y0 + 2) `mod` 4+    +    it "is self-inverse up to phase" $ do+      property $ \(p :: Pauli) ->+        let p' = applyGate (Local (Hadamard 0)) p+            p'' = applyGate (Local (Hadamard 0)) p'+        in xVec p'' === xVec p .&&. zVec p'' === zVec p+    +    it "preserves commutation relations" $ do+      property $ \(p1 :: Pauli) (p2 :: Pauli) ->+        let g = Local (Hadamard 0)+            p1' = applyGate g p1+            p2' = applyGate g p2+        in symplecticForm p1 p2 === symplecticForm p1' p2'++  describe "Phase gate" $ do+    it "leaves Z unchanged" $ do+      let z0 = pauliZ 0+          z0' = applyGate (Local (Phase 0)) z0+      xVec z0' `shouldBe` 0+      zVec z0' `shouldBe` 1+    +    it "converts X to Y" $ do+      let x0 = pauliX 0+          x0' = applyGate (Local (Phase 0)) x0+      xVec x0' `shouldBe` 1+      zVec x0' `shouldBe` 1  -- X*Z = Y+    +    it "has correct phase for X->Y" $ do+      let x0 = pauliX 0+          yExpected = pauliY 0+          x0' = applyGate (Local (Phase 0)) x0+      xVec x0' `shouldBe` xVec yExpected+      zVec x0' `shouldBe` zVec yExpected++  describe "CNOT gate" $ do+    it "X_control -> X_control * X_target" $ do+      let xc = pauliX 0  -- control+          xc' = applyGate (CNOT 0 1) xc+      -- X on control becomes X⊗X+      testBit (xVec xc') 0 `shouldBe` True   -- control still X+      testBit (xVec xc') 1 `shouldBe` True   -- target now X too+      zVec xc' `shouldBe` 0+    +    it "Z_target -> Z_control * Z_target" $ do+      let zt = pauliZ 1  -- target+          zt' = applyGate (CNOT 0 1) zt+      -- Z on target becomes Z⊗Z+      testBit (zVec zt') 0 `shouldBe` True   -- control now Z+      testBit (zVec zt') 1 `shouldBe` True   -- target still Z+      xVec zt' `shouldBe` 0+    +    it "leaves X_target unchanged" $ do+      let xt = pauliX 1+          xt' = applyGate (CNOT 0 1) xt+      xVec xt' `shouldBe` bit 1  -- only target bit set+      zVec xt' `shouldBe` 0+    +    it "leaves Z_control unchanged" $ do+      let zc = pauliZ 0+          zc' = applyGate (CNOT 0 1) zc+      zVec zc' `shouldBe` bit 0  -- only control bit set+      xVec zc' `shouldBe` 0+    +    it "is self-inverse" $ do+      property $ \(p :: Pauli) ->+        let p' = applyGate (CNOT 0 1) p+            p'' = applyGate (CNOT 0 1) p'+        in xVec p'' === xVec p .&&. zVec p'' === zVec p+    +    it "preserves commutation relations" $ do+      property $ \(p1 :: Pauli) (p2 :: Pauli) ->+        let g = CNOT 0 1+            p1' = applyGate g p1+            p2' = applyGate g p2+        in symplecticForm p1 p2 === symplecticForm p1' p2'++  describe "Gate composition" $ do+    it "H then CNOT creates Bell stabilizers" $ do+      let tab0 = emptyTableauN 2+          tab1 = evolveTableauSome tab0 (Local (Hadamard 0))+          tab2 = evolveTableauSome tab1 (CNOT 0 1)+          rowsTab = rowsSome tab2+          s0 = rowsTab !! 0  -- First stabilizer+          s1 = rowsTab !! 1  -- Second stabilizer+      -- After H⊗CNOT, stabilizers should be XX and ZZ+      symplecticForm s0 s1 `shouldBe` True  -- They commute++  describe "Tableau evolution" $ do+    it "preserves tableau validity" $ do+      property $ \(gates :: [SymplecticGate]) ->+        let tab0 = emptyTableauN 3+            tab' = foldl evolveTableauSome tab0 (take 10 gates)+        in isValidSome tab'
+ test/Test/MeasurementSpec.hs view
@@ -0,0 +1,125 @@+module Test.MeasurementSpec where++import Test.Hspec+import Test.QuickCheck+import SymplecticCHP+import Data.Bits (bit, (.|.))+import Control.Monad (replicateM)+import Data.Maybe (fromJust)++spec :: Spec+spec = describe "SymplecticCHP.Measurement" $ do+  describe "isDeterminateSome" $ do+    it "Z measurement on |0> is determinate" $ do+      let tab = emptyTableauN 1+      isDeterminateSome tab (pauliZ 0) `shouldBe` True+    +    it "X measurement on |0> is random" $ do+      let tab = emptyTableauN 1+      isDeterminateSome tab (pauliX 0) `shouldBe` False+    +    it "I measurement is always determinate" $ do+      property $ \(Positive n') ->+        let n = (n' `mod` 10) + 1  -- Ensure 1-10 range+            tab = emptyTableauN n+            identity = Pauli 0 0 0+        in isDeterminateSome tab identity === True+    +    it "stabilizer measurement is determinate" $ do+      let n = 3+          tab = emptyTableauN n+          stab0 = rowsSome tab !! 0  -- Z_0+      isDeterminateSome tab stab0 `shouldBe` True+    +    it "product of stabilizers is determinate" $ do+      let n = 3+          tab = emptyTableauN n+          stab0 = rowsSome tab !! 0+          stab1 = rowsSome tab !! 1+          product = multiply stab0 stab1+      isDeterminateSome tab product `shouldBe` True++  describe "findAntiCommutingStabSome" $ do+    it "finds stabilizer for X on |0>" $ do+      let tab = emptyTableauN 1+          result = findAntiCommutingStabSome tab (pauliX 0)+      result `shouldBe` Just 0  -- S_0 = Z_0 anti-commutes with X_0+    +    it "returns Nothing for Z on |0>" $ do+      let tab = emptyTableauN 1+          result = findAntiCommutingStabSome tab (pauliZ 0)+      result `shouldBe` Nothing  -- Z_0 = S_0 commutes with itself+    +    it "returns Nothing for identity" $ do+      let tab = emptyTableauN 2+          result = findAntiCommutingStabSome tab (Pauli 0 0 0)+      result `shouldBe` Nothing++  describe "Measurement outcomes" $ do+    it "deterministic Z measurement gives +1 on |0>" $ do+      let tab = emptyTableauN 1+      (tab', result) <- measureSome tab (pauliZ 0)+      case result of+        Determinate True -> return ()  -- Expected +1+        _ -> expectationFailure "Expected determinate +1"+    +    it "deterministic outcome is reproducible" $ do+      let n = 3+          tab = emptyTableauN n+          p = pauliZ 0  -- determinate+      results <- replicateM 10 (measureSome tab p)+      all (\(_, res) -> case res of Determinate _ -> True; _ -> False) results+        `shouldBe` True+    +    it "random measurement changes tableau" $ do+      let tab0 = emptyTableauN 1+      (tab1, res1) <- measureSome tab0 (pauliX 0)  -- random+      (tab2, res2) <- measureSome tab1 (pauliX 0)  -- now determinate (should be)+      case (res1, res2) of+        (Random _, Determinate _) -> return ()  -- First random, second determinate+        _ -> expectationFailure "Expected random then determinate"++  describe "Measurement state update" $ do+    it "random measurement updates stabilizer" $ do+      let tab0 = emptyTableauN 2+      (tab1, _) <- measureSome tab0 (pauliX 0)+      -- Tableau should still be valid+      isValidSome tab1 `shouldBe` True+    +    it "measurement preserves number of qubits" $ do+      property $ \(Positive n') ->+        let n = n' `mod` 5 + 1  -- Ensure 1-5 range+        in ioProperty $ do+          let tab0 = emptyTableauN n+          (tab1, _) <- measureSome tab0 (pauliX 0)+          return $ nQubitsSome tab1 === n++    it "measurement preserves tableau validity" $ do+      property $ \(Positive n') ->+        let n = n' `mod` 5 + 1  -- Ensure 1-5 range+        in ioProperty $ do+            let tab0 = emptyTableauN n+                p = Pauli (bit 0) 0 0  -- X_0+            (tab1, _) <- measureSome tab0 p+            return $ isValidSome tab1 === True++  describe "computePhaseSome" $ do+    it "gives +1 for Z on |0>" $ do+      let tab = emptyTableauN 1+          outcome = computePhaseSome tab (pauliZ 0)+      outcome `shouldBe` True  -- +1+    +    it "gives -1 for -Z on |0>" $ do+      let tab = emptyTableauN 1+          minusZ = Pauli 0 (bit 0) 2  -- phase 2 = -1+          outcome = computePhaseSome tab minusZ+      outcome `shouldBe` False  -- -1++  describe "Bell state measurement" $ do+    it "XX stabilizer gives determinate +1 after Bell prep" $ do+      let tab0 = emptyTableauN 2+          tab1 = evolveTableauSome tab0 (Local (Hadamard 0))+          tab2 = evolveTableauSome tab1 (CNOT 0 1)+          xx = Pauli (bit 0 .|. bit 1) 0 0  -- X⊗X+      isDeterminateSome tab2 xx `shouldBe` True+      computePhaseSome tab2 xx `shouldBe` True  -- +1 eigenvalue
+ test/Test/StimCircuitSpec.hs view
@@ -0,0 +1,463 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RecordWildCards #-}++-- | Integration tests for STIM circuit files.+-- Tests circuits from data/stim-circuits/ directory.+-- Updated to support the new YAML-like .expected format.+module Test.StimCircuitSpec (spec) where++import Test.Hspec+import System.FilePath+import System.Directory+import Control.Monad (forM, forM_, when)+import Data.List (isPrefixOf, isSuffixOf, sort, stripPrefix)+import Data.Maybe (catMaybes, listToMaybe, fromMaybe)+import Data.Char (isSpace)+import Text.Read (readMaybe)++import SymplecticCHP+import StimToCHP+import CHPCircuit+import Simulator++import qualified StimParser.Expr as Stim+import qualified StimParser.Parse as Stim+import qualified StimParser.ParseUtils as Stim++-- ============================================================================+-- PARSER FOR .EXPECTED FILES+-- ============================================================================++-- | Measurement outcome: +1 or -1+data Outcome = Plus | Minus+  deriving (Eq, Show)++instance Read Outcome where+  readsPrec _ ('+':'1':rest) = [(Plus, rest)]+  readsPrec _ ('-':'1':rest) = [(Minus, rest)]+  readsPrec _ _ = []++outcomeToBool :: Outcome -> Bool+outcomeToBool Plus = True+outcomeToBool Minus = False++boolToOutcome :: Bool -> Outcome+boolToOutcome True = Plus+boolToOutcome False = Minus++-- | Tableau specification+data TableauSpec = TableauSpec+  { specStabilizers :: [String]+  , specDestabilizers :: [String]+  } deriving (Show, Eq)++-- | A possible outcome case for non-deterministic measurements+data OutcomeCase = OutcomeCase+  { caseProbability :: Double+  , caseOutcomes :: [Outcome]+  , caseTableau :: TableauSpec+  } deriving (Show, Eq)++-- | Expected results from .expected file+data ExpectedResults = ExpectedResults+  { expDeterministic :: Bool+  , expMeasurementOutcomes :: Maybe [Outcome]+  , expPreMeasurementTableau :: Maybe TableauSpec+  , expPostMeasurementTableau :: Maybe TableauSpec+  , expCases :: [OutcomeCase]+  , expErrorExpected :: Maybe String+  } deriving (Show, Eq)++-- | Parse a .expected file+parseExpectedFile :: String -> ExpectedResults+parseExpectedFile content =+  let ls = filter (not . isCommentOrEmpty) $ lines content+      -- Parse top-level fields+      deterministic = parseBoolField "deterministic:" ls+      errorExpected = parseStringField "error_expected:" ls+      outcomes = parseOutcomesField "measurement_outcomes:" ls+      preTableau = parseTableauSection "pre_measurement_tableau:" ls+      postTableau = parseTableauSection "post_measurement_tableau:" ls+      cases = parseCases ls+  in ExpectedResults+       { expDeterministic = fromMaybe False deterministic+       , expMeasurementOutcomes = outcomes+       , expPreMeasurementTableau = preTableau+       , expPostMeasurementTableau = postTableau+       , expCases = cases+       , expErrorExpected = errorExpected+       }++-- | Check if a line is a comment or empty+isCommentOrEmpty :: String -> Bool+isCommentOrEmpty line = +  let trimmed = trim line+  in null trimmed || "#" `isPrefixOf` trimmed++-- | Trim whitespace from both ends+trim :: String -> String+trim = dropWhile isSpace . reverse . dropWhile isSpace . reverse++-- | Drop a prefix from a string if it exists+dropPrefix :: String -> String -> String+dropPrefix prefix str = +  if prefix `isPrefixOf` str +  then drop (length prefix) str +  else str++-- | Parse a boolean field+parseBoolField :: String -> [String] -> Maybe Bool+parseBoolField prefix lines = +  case findLine prefix lines of+    Just line -> +      let val = trim $ drop (length prefix) line+      in case val of+           "true" -> Just True+           "false" -> Just False+           _ -> Nothing+    Nothing -> Nothing++-- | Parse a string field (remaining content after colon)+parseStringField :: String -> [String] -> Maybe String+parseStringField prefix lines =+  case findLine prefix lines of+    Just line -> Just $ trim $ drop (length prefix) line+    Nothing -> Nothing++-- | Parse measurement outcomes field+parseOutcomesField :: String -> [String] -> Maybe [Outcome]+parseOutcomesField prefix lines =+  case findLine prefix lines of+    Just line -> +      let val = trim $ drop (length prefix) line+      in parseOutcomeList val+    Nothing -> Nothing++-- | Parse a list of outcomes like [+1, -1, +1]+parseOutcomeList :: String -> Maybe [Outcome]+parseOutcomeList s = +  let trimmed = trim s+      inner = case trimmed of+                '[':rest -> reverse $ dropWhile (== ']') $ reverse rest+                _ -> trimmed+      parts = map trim $ splitOn ',' inner+  in mapM parseOutcome parts+  where+    parseOutcome "+1" = Just Plus+    parseOutcome "-1" = Just Minus+    parseOutcome _ = Nothing++-- | Parse a tableau section+tableauSectionNames :: [String]+tableauSectionNames = ["pre_measurement_tableau:", "post_measurement_tableau:"]++parseTableauSection :: String -> [String] -> Maybe TableauSpec+parseTableauSection sectionName lines =+  case findLine sectionName lines of+    Just _ -> +      let afterSection = dropWhile (not . isSectionHeader) $ dropWhile (not . (sectionName `isPrefixOf`)) lines+          -- Find the lines within this section (until next section or end)+          sectionLines = takeWhile (not . isTopLevelField) $ tail $ dropWhile (not . (sectionName `isPrefixOf`)) lines+          stabLine = findLine "stabilizers:" sectionLines+          destabLine = findLine "destabilizers:" sectionLines+          stabs = stabLine >>= parseStringList . dropPrefix ("stabilizers:" :: String) . trim+          destabs = destabLine >>= parseStringList . dropPrefix ("destabilizers:" :: String) . trim+      in case (stabs, destabs) of+           (Just s, Just d) -> Just $ TableauSpec s d+           (Just s, Nothing) -> Just $ TableauSpec s []+           (Nothing, Just d) -> Just $ TableauSpec [] d+           _ -> Nothing+    Nothing -> Nothing+  where+    isSectionHeader line = any (`isPrefixOf` trim line) tableauSectionNames+    isTopLevelField line = +      let t = trim line+      in any (`isPrefixOf` t) ["deterministic:", "cases:", "error_expected:", +                               "measurement_outcomes:", "pre_measurement_tableau:",+                               "post_measurement_tableau:"]++-- | Parse string list like ["+ZZ", "+XX"]+parseStringList :: String -> Maybe [String]+parseStringList s =+  let trimmed = trim s+      inner = case trimmed of+                '[':rest -> reverse $ dropWhile (== ']') $ reverse rest+                _ -> trimmed+      -- Handle quoted strings+      parseQuoted str = case str of+        '"':rest -> Just $ takeWhile (/= '"') rest+        _ -> Just str+      parts = map (trim . filter (/= '"')) $ splitOn ',' inner+  in if null inner then Just [] else Just parts++-- | Parse cases section for non-deterministic measurements+parseCases :: [String] -> [OutcomeCase]+parseCases lines =+  case findLine "cases:" lines of+    Just _ -> +      let afterCases = tail $ dropWhile (not . ("cases:" `isPrefixOf`)) lines+          -- Each case starts with "- probability:"+          caseBlocks = splitCases afterCases+      in catMaybes $ map parseCaseBlock caseBlocks+    Nothing -> []+  where+    splitCases :: [String] -> [[String]]+    splitCases [] = []+    splitCases ls = +      let (current, rest) = break (isPrefixOf "- probability:") $ dropWhile (not . isPrefixOf "- probability:") ls+      in if null rest then [] else +         let (thisCase, next) = span (not . isPrefixOf "- probability:") (tail rest)+         in (head rest : thisCase) : splitCases next++parseCaseBlock :: [String] -> Maybe OutcomeCase+parseCaseBlock block = do+  probLine <- findLine "- probability:" block <|> findLine "probability:" block+  prob <- readMaybe $ filter (/= '-') $ trim $ dropWhile (/= ':') probLine+  outcomes <- parseOutcomesField "measurement_outcomes:" block+  stabLine <- findLine "stabilizers:" block+  destabLine <- findLine "destabilizers:" block+  stabs <- parseStringList $ drop (length ("stabilizers:" :: String)) stabLine+  destabs <- parseStringList $ drop (length ("destabilizers:" :: String)) destabLine+  return $ OutcomeCase prob outcomes (TableauSpec stabs destabs)++-- | Find a line starting with given prefix+findLine :: String -> [String] -> Maybe String+findLine prefix lines = listToMaybe $ filter (isPrefixOf prefix . trim) lines++(<|>) :: Maybe a -> Maybe a -> Maybe a+(<|>) (Just x) _ = Just x+(<|>) Nothing y = y+infixr 1 <|>++-- | Split string on delimiter+splitOn :: Char -> String -> [String]+splitOn _ [] = []+splitOn delim str = +  let (first, rest) = break (== delim) str+  in first : case rest of+               [] -> []+               (_:xs) -> splitOn delim xs++-- ============================================================================+-- TEST INFRASTRUCTURE+-- ============================================================================++-- | Test case data+data TestCase = TestCase+  { testName :: String+  , stimPath :: FilePath+  , expectedPath :: FilePath+  , stimContent :: String+  , expectedContent :: Maybe String+  } deriving (Show)++-- | Find all test cases in the data directory+findTestCases :: IO [TestCase]+findTestCases = do+  let dataDir = "data" </> "stim-circuits"+  exists <- doesDirectoryExist dataDir+  if not exists+    then return []+    else do+      files <- listDirectory dataDir+      let stimFiles = sort $ filter (".stim" `isSuffixOf`) files+      +      forM stimFiles $ \stimFile -> do+        let baseName = dropExtension stimFile+            stimPath' = dataDir </> stimFile+            expectedPath' = dataDir </> (baseName ++ ".expected")+        +        stimContent <- readFile stimPath'+        expectedExists <- doesFileExist expectedPath'+        expectedContent <- if expectedExists +                           then Just <$> readFile expectedPath'+                           else return Nothing+        +        return $ TestCase+          { testName = baseName+          , stimPath = stimPath'+          , expectedPath = expectedPath'+          , stimContent = stimContent+          , expectedContent = expectedContent+          }++-- ============================================================================+-- SIMULATION AND CHECKING+-- ============================================================================++-- | Run a single test case+runTestCase :: TestCase -> IO (Maybe String)+runTestCase tc = do+  -- Parse expected results+  let expected = maybe (ExpectedResults False Nothing Nothing Nothing [] Nothing) +                       parseExpectedFile +                       (expectedContent tc)+  +  -- Try to read and parse STIM file+  stimResult <- tryReadStim (stimPath tc)+  +  case stimResult of+    Left parseErr ->+      case expErrorExpected expected of+        Just _ -> return Nothing  -- Error expected+        Nothing -> return $ Just $ "Parse error: " ++ parseErr+    +    Right stim -> +      -- Try to translate to CHP+      case translateStim stim of+        Left err -> +          case expErrorExpected expected of+            Just _ -> return Nothing  -- Error expected and got error = pass+            Nothing -> return $ Just $ "Translation error: " ++ show err+        +        Right circuit -> +          case expErrorExpected expected of+            Just _ -> return $ Just "Expected error but translation succeeded"+            Nothing -> do+              -- Run simulation+              result <- runCHPCircuit circuit+              +              -- Run all checks+              let checks = catMaybes +                    [ checkTableauValid result+                    , checkResults expected result+                    ]+              +              case concat checks of+                [] -> return Nothing+                errors -> return $ Just $ unlines errors++-- | Try to read STIM file+tryReadStim :: FilePath -> IO (Either String Stim.Stim)+tryReadStim path = do+  content <- readFile path+  let prefixed = "!!!Start " ++ content+  return $ Right $ Stim.run Stim.parseStim prefixed++-- | Check tableau validity+checkTableauValid :: SimulationResult -> Maybe [String]+checkTableauValid result = +  let valid = isValidSome (finalTableau result)+  in if valid +     then Nothing +     else Just ["Tableau is not valid"]++-- | Main checking function+checkResults :: ExpectedResults -> SimulationResult -> Maybe [String]+checkResults expected result =+  let actualOutcomes = map boolToOutcome $ measurementOutcomes result+      actualStabs = getStabilizerStrings $ finalTableau result+      actualDestabs = getDestabilizerStrings $ finalTableau result+      actualTableau = TableauSpec actualStabs actualDestabs+  in case expErrorExpected expected of+       Just _ -> Just ["Expected error but simulation succeeded"]+       Nothing ->+         if expDeterministic expected+         then checkDeterministic expected actualOutcomes actualTableau+         else checkNonDeterministic expected actualOutcomes actualTableau++-- | Check deterministic case+checkDeterministic :: ExpectedResults -> [Outcome] -> TableauSpec -> Maybe [String]+checkDeterministic expected actualOutcomes actualTableau =+  let errors = catMaybes+        [ checkField "measurement_outcomes" +            (expMeasurementOutcomes expected) (Just actualOutcomes)+        , checkField "post_measurement_tableau" +            (expPostMeasurementTableau expected) (Just actualTableau)+        ]+  in if null errors then Nothing else Just errors+  where+    checkField :: (Eq a, Show a) => String -> Maybe a -> Maybe a -> Maybe String+    checkField name (Just expected) (Just actual) =+      if expected == actual +      then Nothing +      else Just $ name ++ " mismatch: expected " ++ show expected ++ ", got " ++ show actual+    checkField name Nothing _ = Nothing+    checkField name (Just _) Nothing = Just $ name ++ " not found in actual result"++-- | Check non-deterministic case+checkNonDeterministic :: ExpectedResults -> [Outcome] -> TableauSpec -> Maybe [String]+checkNonDeterministic expected actualOutcomes actualTableau =+  let cases = expCases expected+      -- Check if actual outcome matches any case+      matchingCase = findMatchingCase actualOutcomes actualTableau cases+  in case matchingCase of+       Just _ -> Nothing  -- Found a matching case+       Nothing -> +         if null cases+         then Nothing  -- No cases specified, skip+         else Just ["No matching case found for outcomes: " ++ show actualOutcomes ++ +                   ", tableau: " ++ show actualTableau]++-- | Find a matching case for the actual results+findMatchingCase :: [Outcome] -> TableauSpec -> [OutcomeCase] -> Maybe OutcomeCase+findMatchingCase outcomes tableau = find matches+  where+    matches c = caseOutcomes c == outcomes && caseTableau c == tableau+    find _ [] = Nothing+    find p (x:xs) = if p x then Just x else find p xs++-- | Extract stabilizer strings from tableau+getStabilizerStrings :: SomeTableau -> [String]+getStabilizerStrings tab = +  let n = nQubitsSome tab+  in catMaybes [stabilizerString tab i | i <- [0..n-1]]++-- | Extract destabilizer strings from tableau  +getDestabilizerStrings :: SomeTableau -> [String]+getDestabilizerStrings tab =+  let n = nQubitsSome tab+  in catMaybes [destabilizerString tab i | i <- [0..n-1]]++-- | Get stabilizer as string+stabilizerString :: SomeTableau -> Int -> Maybe String+stabilizerString tab i = +  case stabilizerSome tab i of+    Nothing -> Nothing+    Just p -> Just $ showPauliCompact p (nQubitsSome tab)++-- | Get destabilizer as string+destabilizerString :: SomeTableau -> Int -> Maybe String+destabilizerString tab i =+  case destabilizerSome tab i of+    Nothing -> Nothing+    Just p -> Just $ showPauliCompact p (nQubitsSome tab)++-- | Show Pauli operator in compact format (+XX, -ZI, etc.)+showPauliCompact :: Pauli -> Int -> String+showPauliCompact (Pauli x z phase) n =+  let phaseStr = case phase `mod` 4 of+        0 -> "+"+        1 -> "+i"+        2 -> "-"+        3 -> "-i"+        _ -> "?"+      ops = [showSinglePauli (testBit x i) (testBit z i) | i <- [0..n-1]]+  in phaseStr ++ concat ops+  where+    testBit w i = (w `div` (2^i)) `mod` 2 == 1+    showSinglePauli False False = "I"+    showSinglePauli True  False = "X"+    showSinglePauli False True  = "Z"+    showSinglePauli True  True  = "Y"++-- ============================================================================+-- HSPEC SPEC+-- ============================================================================++spec :: Spec+spec = do+  testCases <- runIO findTestCases+  +  if null testCases+    then describe "STIM Circuit Tests" $ +         it "test circuits found" $ +         pendingWith "No STIM circuits found in data/stim-circuits/"+    else describe "STIM Circuit Tests" $ do+      forM_ testCases $ \tc -> do+        it (testName tc) $ do+          result <- runTestCase tc+          case result of+            Nothing -> return ()+            Just err -> expectationFailure err
+ test/Test/TableauSpec.hs view
@@ -0,0 +1,136 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}++module Test.TableauSpec where++import Test.Hspec+import Test.QuickCheck+import SymplecticCHP+import Data.Bits (bit)+import Data.Maybe (fromJust)++-- Local Pauli constructors+pauliX, pauliZ, pauliY :: Int -> Pauli+pauliX i = Pauli (bit i) 0 0+pauliZ i = Pauli 0 (bit i) 0+pauliY i = Pauli (bit i) (bit i) 1++-- Orphan instance (move to Test.Arbitrary if preferred)+instance Arbitrary Pauli where+  arbitrary = do+    x <- chooseInt (0, 255) :: Gen Int+    z <- chooseInt (0, 255) :: Gen Int+    p <- chooseInt (0, 3)+    return $ Pauli (fromIntegral x) (fromIntegral z) p++newtype SmallN = SmallN Int+  deriving (Show, Eq)++instance Arbitrary SmallN where+  arbitrary = SmallN <$> chooseInt (1, 10)+  shrink (SmallN n) = SmallN <$> [n' | n' <- shrink n, n' > 0]++spec :: Spec+spec = describe "SymplecticCHP.Tableau" $ do+  describe "emptyTableauN" $ do+    it "creates valid tableau for |0...0>" $ do+      let tab = emptyTableauN 5+      isValidSome tab `shouldBe` True+    +    it "has correct number of rows" $ do+      property $ \(SmallN n) ->+        let tab = emptyTableauN n+        in length (rowsSome tab) === 2 * n+    +    it "has correct qubit count" $ do+      property $ \(SmallN n) ->+        nQubitsSome (emptyTableauN n) === n++  describe "Stabilizer properties" $ do+    it "stabilizers commute with each other" $ do+      property $ \(SmallN n) ->+        n > 0 ==>+          let tab = emptyTableauN n+              stab i = fromJust $ stabilizerSome tab i+              -- FIX: Use 'and' with list of Bools, not ==>+              allCommute = and [ i == j || commute (stab i) (stab j)+                               | i <- [0..n-1], j <- [0..n-1] ]+          in allCommute === True+    +    it "destabilizers have correct commutation with stabilizers" $ do+      property $ \(SmallN n) ->+        n > 0 ==>+          let tab = emptyTableauN n+              stab i = fromJust $ stabilizerSome tab i+              destab i = fromJust $ destabilizerSome tab i+              -- FIX: Use if-then-else inside list comprehension, not ==>+              correctPairing = and +                [ if i == j then anticommute (destab i) (stab j)+                            else commute (destab i) (stab j)+                | i <- [0..n-1], j <- [0..n-1] ]+          in correctPairing === True++  describe "Initial state |0...0>" $ do+    it "has Z stabilizers on each qubit" $ do+      let n = 4+          tab = emptyTableauN n+          hasZStab i = xVec (fromJust $ stabilizerSome tab i) == 0 && zVec (fromJust $ stabilizerSome tab i) == bit i+      all hasZStab [0..n-1] `shouldBe` True+    +    it "has X destabilizers on each qubit" $ do+      let n = 4+          tab = emptyTableauN n+          hasXDestab i = xVec (fromJust $ destabilizerSome tab i) == bit i && zVec (fromJust $ destabilizerSome tab i) == 0+      all hasXDestab [0..n-1] `shouldBe` True+    +    it "all stabilizers have zero phase" $ do+      let n = 5+          tab = emptyTableauN n+      all (\i -> phase (fromJust $ stabilizerSome tab i) == 0) [0..n-1] `shouldBe` True++  describe "(//) operator for tableau rows" $ do+    it "updates single row correctly" $ do+      let tab = emptyTableauN 2+          newRow = Pauli 0 0 0+          rows' = rowsSome tab // [(0, newRow)]+      rows' !! 0 `shouldBe` newRow+      rows' !! 1 `shouldBe` (rowsSome tab !! 1)+      rows' !! 2 `shouldBe` (rowsSome tab !! 2)+      rows' !! 3 `shouldBe` (rowsSome tab !! 3)+    +    it "later update wins" $ do+      let tab = emptyTableauN 2+          rowA = Pauli 1 0 0+          rowB = Pauli 0 1 0+          rows' = rowsSome tab // [(0, rowA), (0, rowB)]+      rows' !! 0 `shouldBe` rowB++  describe "Tableau validity preservation" $ do+    it "remains valid after single-qubit gates" $ do+      property $ \(SmallN n) (q :: Int) ->+        let q' = q `mod` max 1 n  -- Ensure 0 <= q' < n+        in n > 0 ==>+            let tab0 = emptyTableauN n+                tabH = evolveTableauSome tab0 (Local (Hadamard q'))+                tabS = evolveTableauSome tabH (Local (Phase q'))+            in isValidSome tabH .&&. isValidSome tabS+++    it "remains valid after CNOT" $ do+      property $ \(SmallN n) (cRaw :: Int) (tRaw :: Int) ->+        let n' = max 2 n+            c = cRaw `mod` n'+            t = tRaw `mod` n'+        in c /= t ==>+            let tab0 = emptyTableauN n'+                tab' = evolveTableauSome tab0 (CNOT c t)+            in isValidSome tab'++  -- describe "Generate function" $ do+  --   it "produces list of correct length" $ do+  --     property $ \(n :: Int) ->+  --       n >= 0 && n <= 100 ==>+  --         length (generate n id) === n+  --   +  --   it "applies function correctly" $ do+  --     generate 5 (*2) `shouldBe` [0,2,4,6,8]
+ test/Test/UtilsSpec.hs view
@@ -0,0 +1,101 @@+module Test.UtilsSpec where++import Test.Hspec+import Test.QuickCheck+import SymplecticCHP ((//))+import qualified Data.List as L++spec :: Spec+spec = describe "SymplecticCHP.Utils" $ do+  describe "(//) list update operator" $ do+    it "basic example from Vector semantics" $ do+      let xs = [5,9,2,7 :: Int]+          updates = [(2,1),(0,3),(2,8)]+      xs // updates `shouldBe` [3,9,8,7]+    +    it "handles empty update list" $ do+      let xs = [1,2,3 :: Int]+      xs // [] `shouldBe` xs+    +    it "ignores out-of-bounds indices (too large)" $ do+      let xs = [1,2,3 :: Int]+      xs // [(5,99)] `shouldBe` xs+    +    it "ignores negative indices" $ do+      let xs = [1,2,3 :: Int]+      xs // [(-1,99)] `shouldBe` xs+    +    it "later update wins for same index" $ do+      let xs = [1,2,3 :: Int]+      xs // [(0,10),(0,20)] `shouldBe` [20,2,3]+      xs // [(1,5),(1,6),(1,7)] `shouldBe` [1,7,3]+    +    it "handles updates in any order" $ do+      let xs = [0,0,0,0 :: Int]+          updates1 = [(0,1),(2,3)]+          updates2 = [(2,3),(0,1)]  -- reversed+      xs // updates1 `shouldBe` xs // updates2+    +    it "handles single element list" $ do+      let xs = [42 :: Int]+      xs // [(0,100)] `shouldBe` [100]+      xs // [(1,100)] `shouldBe` [42]  -- out of bounds+    +    it "handles all indices updated" $ do+      let xs = [1,2,3 :: Int]+      xs // [(0,10),(1,20),(2,30)] `shouldBe` [10,20,30]++  describe "(//) property tests" $ do+    it "preserves list length" $ do+      property $ \xs updates -> +        let xs' :: [Int]+            xs' = take 50 xs+            updates' :: [(Int, Int)]+            updates' = take 20 updates+            result = xs' // updates'+        in length result === length xs'+    +    it "is idempotent when applying same updates twice" $ do+      property $ \xs updates -> +        let xs' :: [Int]+            xs' = take 30 xs+            updates' :: [(Int, Int)]+            updates' = [(i `mod` 40, v) | (i, v) <- take 10 updates, let ii = i `mod` 40, ii >= 0]+            xs'' = xs' // updates'+        in xs'' // updates' === xs''++    it "lookup finds updated values correctly" $ do+        property $ \xs updates (idx :: Int) -> +            let xs' :: [Int]+                xs' = take 20 xs+                len = length xs'+            in len > 0 ==>  -- GUARD: ensure non-empty list+                let -- Normalize indices to valid range [0, len-1]+                    updatesNorm = [(i `mod` len, v) | (i, v) <- take 10 updates]+                    +                    -- Build effective update map: for each index, find LAST value+                    -- This MUST match what (//) does internally+                    effectiveValue i = +                        case [v | (ii, v) <- reverse updatesNorm, ii == i] of+                            (v:_) -> Just v   -- first in reversed = last in original+                            []    -> Nothing+                    +                    result = xs' // updatesNorm+                    i = idx `mod` len+                    +                in case effectiveValue i of+                      Just v  -> result L.!! i === v+                      Nothing -> result L.!! i === (xs' L.!! i)++    it "later updates override earlier ones" $ do+      property $ \xs -> +        let xs' :: [Int]+            xs' = take 10 xs+            updates :: [(Int, Int)]+            updates = [(0, 1), (0, 2), (0, 3)]+        in xs' // updates === (xs' // [(0, 3)] :: [Int])+    +    it "empty updates is identity" $ do+      property $ \xs -> +        let xs' :: [Int] = take 100 xs+        in xs' // [] === xs'