File size: 4,002 Bytes
4953a87 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 | {-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Wno-orphans #-}
-- ============================================================
-- PROPRIETARY AND CONFIDENTIAL -- PRIOR ART SEALED
-- Copyright (C) 2026 SNAPKITTYWEST / SnapKitty (Jessica).
-- All Rights Reserved. Author: Ahmad Ali Parr
-- License: SNAPKITTYWEST-PROPRIETARY-2026-001
-- Extracted from: lean/WalkAA/WalkAmplitudeAmplification.lean
-- johnsonWalk = pure permutation reindexing (unitary by construction)
-- Corresponds to Lean theorem: johnsonWalk_unitary (zero sorry)
--
-- Build: ghc -O2 JohnsonWalk.hs -o johnsonWalk
-- Run: ./johnsonWalk <L> <b> <w> < state.txt
-- ============================================================
module Main where
import Data.Complex
import Data.Vector (Vector)
import qualified Data.Vector as V
import Numeric (showFFloat)
import System.Environment (getArgs)
--------------------------------------------------------------------
-- 1. Sizes
--------------------------------------------------------------------
msgSize :: Int -> Int -> Int
msgSize l b = 2 ^ (l * b)
cvSize :: Int -> Int
cvSize w = 2 ^ w
totalSize :: Int -> Int -> Int -> Int
totalSize l b w = msgSize l b * cvSize w * 2 -- ×2 for Flag
--------------------------------------------------------------------
-- 2. Cyclic shift on message index: m ↦ (m+1) mod msgSize
-- Corresponds to Lean: msgShift (Equiv.Perm on Msg L b)
--------------------------------------------------------------------
msgShift :: Int -> Int -> Int -> Int
msgShift l b m = (m + 1) `mod` msgSize l b
--------------------------------------------------------------------
-- 3. Lift to full state permutation
-- Corresponds to Lean: statePerm (Equiv.prodCongr msgShift Equiv.refl)
--------------------------------------------------------------------
statePerm :: Int -> Int -> Int -> Int -> Int
statePerm l b w idx =
let cv' = cvSize w
msg' = msgSize l b
msg = idx `div` (cv' * 2)
rest = idx `mod` (cv' * 2)
newMsg = msgShift l b msg
in newMsg * (cv' * 2) + rest
--------------------------------------------------------------------
-- 4. Walk operator: ψ(x) → ψ(statePerm x) (pure reindexing)
-- Corresponds to Lean: johnsonWalk ψ = fun x => ψ (statePerm L b w x)
-- Unitary: permutation of basis preserves ‖ψ‖₂ exactly.
--------------------------------------------------------------------
johnsonWalk :: Int -> Int -> Int -> Vector (Complex Double) -> Vector (Complex Double)
johnsonWalk l b w psi =
V.generate (totalSize l b w) $ \i ->
V.unsafeIndex psi (statePerm l b w i)
--------------------------------------------------------------------
-- 5. I/O
--------------------------------------------------------------------
readState :: Int -> IO (Vector (Complex Double))
readState n = do
nums <- map read . words <$> getContents
let pairs = zip (evens nums) (odds nums)
comps = [ r :+ im | (r, im) <- pairs ]
if length comps /= n
then error $ "Expected " ++ show n ++ " complex numbers, got " ++ show (length comps)
else return $ V.fromList comps
where
evens xs = [ xs !! i | i <- [0,2..length xs - 1] ]
odds xs = [ xs !! i | i <- [1,3..length xs - 1] ]
printState :: Vector (Complex Double) -> IO ()
printState vec = V.forM_ vec $ \c ->
putStrLn $ fmt (realPart c) ++ " " ++ fmt (imagPart c)
where fmt x = showFFloat (Just 6) x ""
main :: IO ()
main = do
args <- getArgs
case args of
[ls, bs, ws] -> do
let l = read ls; b = read bs; w = read ws
n = totalSize l b w
putStrLn $ "State size: " ++ show n ++ " amplitudes"
psi <- readState n
let psi' = johnsonWalk l b w psi
putStrLn "After Johnson walk (cyclic message shift):"
printState psi'
_ -> putStrLn "Usage: ./johnsonWalk <L> <b> <w>\n\
\Provide state vector on stdin as real imag pairs.\n\
\Example (L=1,b=2,w=1 => N=16):\n\
\ ./johnsonWalk 1 2 1 < state16.txt"
|