rot13 (verified!)

rot13.hs

{-# LANGUAGE DeriveDataTypeable #-}

import Data.SBV
import Control.Monad.IO.Class
import Data.Foldable
import Data.Generics

-------------------------------------------------------------------------------
-- Rot13 over an array of 8 bit words.
--
-- This simplifies the implementation, but means that the types don't constrain
-- the values to be between 0 and 25. Rather this is declared as an assumption
-- in the theorems.
-------------------------------------------------------------------------------

-- A message is a list of 8 bit words.
type Message = [SWord8]

rot13 :: SWord8 -> SWord8
rot13 x = (x+13) `sMod` 26

rot13Msg :: Message -> Message
rot13Msg = fmap rot13

-- Performing rot13 twice returns the original message for a given message
-- length.
rot13TwiceDoesNotChangeMessage l = do
  clearTxt <- mkFreeVars l
  traverse_ (\x -> constrain (x .< 26)) clearTxt
  return $ (rot13Msg . rot13Msg) clearTxt .== clearTxt

-- Rot13 doesn't just return the plaintext.
rot13IsNotANoOp l = do
  clearTxt <- mkFreeVars l
  traverse_ (\x -> constrain (x .< 26)) clearTxt
  return $ (rot13Msg) clearTxt ./= clearTxt

-------------------------------------------------------------------------------
-- Rot13 over an Alpha sum type, one value for each character.
--
-- Here a sum type is used to represent the alphabet rather than an 8 bit word.
-------------------------------------------------------------------------------

data Alpha = A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
            deriving (Eq, Ord, Data, Typeable, Read, Show)

-- Give Alpha a symbolic representation.
instance SymWord Alpha
instance HasKind Alpha
instance SatModel Alpha

-- Alias for the symbolic representation of Alpha.
type SAlpha = SBV Alpha

-- Symbolically map each character from clear text -> cipher text.
-- Since we need to use the symbolic operators, I'm not sure if there's
-- a cleaner way to do this.
rot13' :: SAlpha -> SAlpha
rot13' x =
  ite (x .== (literal A))
    (literal N)
    (ite (x .== (literal B))
      (literal O)
      (ite (x .== (literal Main.C))
        (literal P)
        (ite (x .== (literal D))
          (literal Q)
          (ite (x .== (literal E))
            (literal R)
            (ite (x .== (literal F))
              (literal S)
              (ite (x .== (literal G))
                (literal T)
                (ite (x .== (literal H))
                  (literal U)
                  (ite (x .== (literal I))
                    (literal V)
                    (ite (x .== (literal J))
                      (literal W)
                      (ite (x .== (literal K))
                        (literal X)
                        (ite (x .== (literal L))
                          (literal Y)
                          (ite (x .== (literal M))
                            (literal Z)
                            (ite (x .== (literal N))
                              (literal A)
                              (ite (x .== (literal O))
                                (literal B)
                                (ite (x .== (literal P))
                                  (literal Main.C)
                                  (ite (x .== (literal Q))
                                    (literal D)
                                    (ite (x .== (literal R))
                                      (literal E)
                                      (ite (x .== (literal S))
                                        (literal F)
                                        (ite (x .== (literal T))
                                          (literal G)
                                          (ite (x .== (literal U))
                                            (literal H)
                                            (ite (x .== (literal V))
                                              (literal I)
                                              (ite (x .== (literal W))
                                                (literal J)
                                                (ite (x .== (literal X))
                                                  (literal K)
                                                  (ite (x .== (literal Y))
                                                    (literal L)
                                                    (literal M)))))))))))))))))))))))))

rot13Msg' :: [SAlpha] -> [SAlpha]
rot13Msg' = fmap rot13'

-- Performing rot13 twice returns the original message for a given message
-- length.
-- Notice that the values don't need to be contrained since the type
-- enforces this contraint.
rot13TwiceDoesNotChangeMessage' l = do
  clearTxt <- mkFreeVars l
  return $ (rot13Msg' . rot13Msg') clearTxt .== clearTxt

-- Rot13 doesn't just return the plaintext.
rot13IsNotANoOp' l = do
  clearTxt <- mkFreeVars l
  return $ (rot13Msg') clearTxt ./= clearTxt

proveWithMessage :: Provable a => String -> a -> IO ()
proveWithMessage msg pred = do
  putStrLn msg
  res <- prove pred
  print res
  putStrLn ""

main = do
  proveWithMessage "Proving rot13 twice over bytes returns the original message, for a message length of 10." (rot13TwiceDoesNotChangeMessage 10)
  proveWithMessage "Proving rot13 over bytes does not just return the clear text, for a message length of 10." (rot13IsNotANoOp 10)
  proveWithMessage "Proving rot13 twice over Alpha returns the original message, for a message length of 10." (rot13TwiceDoesNotChangeMessage' 10)
  proveWithMessage "Proving rot13 over Alpha does not just return the clear text, for a message length of 10." (rot13IsNotANoOp' 10)