-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.BitPrecise.Legato
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- An encoding and correctness proof of Legato's multiplier in Haskell. Bill Legato came
-- up with an interesting way to multiply two 8-bit numbers on Mostek, as described here:
--   <http://www.cs.utexas.edu/~moore/acl2/workshop-2004/contrib/legato/Weakest-Preconditions-Report.pdf>
--
-- Here's Legato's algorithm, as coded in Mostek assembly:
--
-- @
--    step1 :       LDX #8         ; load X immediate with the integer 8 
--    step2 :       LDA #0         ; load A immediate with the integer 0 
--    step3 : LOOP  ROR F1         ; rotate F1 right circular through C 
--    step4 :       BCC ZCOEF      ; branch to ZCOEF if C = 0 
--    step5 :       CLC            ; set C to 0 
--    step6 :       ADC F2         ; set A to A+F2+C and C to the carry 
--    step7 : ZCOEF ROR A          ; rotate A right circular through C 
--    step8 :       ROR LOW        ; rotate LOW right circular through C 
--    step9 :       DEX            ; set X to X-1 
--    step10:       BNE LOOP       ; branch to LOOP if Z = 0 
-- @
--
-- This program came to be known as the Legato's challenge in the community, where
-- the challenge was to prove that it indeed does perform multiplication. This file
-- formalizes the Mostek architecture in Haskell and proves that Legato's algorithm
-- is indeed correct.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric  #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.BitPrecise.Legato where

import Data.Array (Array, Ix(..), (!), (//), array)

import Data.SBV
import Data.SBV.Tools.CodeGen

import GHC.Generics (Generic)

------------------------------------------------------------------
-- * Mostek architecture
------------------------------------------------------------------

-- | We model only two registers of Mostek that is used in the above algorithm, can add more.
data Register = RegX  | RegA  deriving (Register -> Register -> Bool
(Register -> Register -> Bool)
-> (Register -> Register -> Bool) -> Eq Register
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Register -> Register -> Bool
$c/= :: Register -> Register -> Bool
== :: Register -> Register -> Bool
$c== :: Register -> Register -> Bool
Eq, Eq Register
Eq Register
-> (Register -> Register -> Ordering)
-> (Register -> Register -> Bool)
-> (Register -> Register -> Bool)
-> (Register -> Register -> Bool)
-> (Register -> Register -> Bool)
-> (Register -> Register -> Register)
-> (Register -> Register -> Register)
-> Ord Register
Register -> Register -> Bool
Register -> Register -> Ordering
Register -> Register -> Register
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Register -> Register -> Register
$cmin :: Register -> Register -> Register
max :: Register -> Register -> Register
$cmax :: Register -> Register -> Register
>= :: Register -> Register -> Bool
$c>= :: Register -> Register -> Bool
> :: Register -> Register -> Bool
$c> :: Register -> Register -> Bool
<= :: Register -> Register -> Bool
$c<= :: Register -> Register -> Bool
< :: Register -> Register -> Bool
$c< :: Register -> Register -> Bool
compare :: Register -> Register -> Ordering
$ccompare :: Register -> Register -> Ordering
$cp1Ord :: Eq Register
Ord, Ord Register
Ord Register
-> ((Register, Register) -> [Register])
-> ((Register, Register) -> Register -> Int)
-> ((Register, Register) -> Register -> Int)
-> ((Register, Register) -> Register -> Bool)
-> ((Register, Register) -> Int)
-> ((Register, Register) -> Int)
-> Ix Register
(Register, Register) -> Int
(Register, Register) -> [Register]
(Register, Register) -> Register -> Bool
(Register, Register) -> Register -> Int
forall a.
Ord a
-> ((a, a) -> [a])
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Bool)
-> ((a, a) -> Int)
-> ((a, a) -> Int)
-> Ix a
unsafeRangeSize :: (Register, Register) -> Int
$cunsafeRangeSize :: (Register, Register) -> Int
rangeSize :: (Register, Register) -> Int
$crangeSize :: (Register, Register) -> Int
inRange :: (Register, Register) -> Register -> Bool
$cinRange :: (Register, Register) -> Register -> Bool
unsafeIndex :: (Register, Register) -> Register -> Int
$cunsafeIndex :: (Register, Register) -> Register -> Int
index :: (Register, Register) -> Register -> Int
$cindex :: (Register, Register) -> Register -> Int
range :: (Register, Register) -> [Register]
$crange :: (Register, Register) -> [Register]
$cp1Ix :: Ord Register
Ix, Register
Register -> Register -> Bounded Register
forall a. a -> a -> Bounded a
maxBound :: Register
$cmaxBound :: Register
minBound :: Register
$cminBound :: Register
Bounded)

-- | The carry flag ('FlagC') and the zero flag ('FlagZ')
data Flag = FlagC | FlagZ deriving (Flag -> Flag -> Bool
(Flag -> Flag -> Bool) -> (Flag -> Flag -> Bool) -> Eq Flag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Flag -> Flag -> Bool
$c/= :: Flag -> Flag -> Bool
== :: Flag -> Flag -> Bool
$c== :: Flag -> Flag -> Bool
Eq, Eq Flag
Eq Flag
-> (Flag -> Flag -> Ordering)
-> (Flag -> Flag -> Bool)
-> (Flag -> Flag -> Bool)
-> (Flag -> Flag -> Bool)
-> (Flag -> Flag -> Bool)
-> (Flag -> Flag -> Flag)
-> (Flag -> Flag -> Flag)
-> Ord Flag
Flag -> Flag -> Bool
Flag -> Flag -> Ordering
Flag -> Flag -> Flag
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Flag -> Flag -> Flag
$cmin :: Flag -> Flag -> Flag
max :: Flag -> Flag -> Flag
$cmax :: Flag -> Flag -> Flag
>= :: Flag -> Flag -> Bool
$c>= :: Flag -> Flag -> Bool
> :: Flag -> Flag -> Bool
$c> :: Flag -> Flag -> Bool
<= :: Flag -> Flag -> Bool
$c<= :: Flag -> Flag -> Bool
< :: Flag -> Flag -> Bool
$c< :: Flag -> Flag -> Bool
compare :: Flag -> Flag -> Ordering
$ccompare :: Flag -> Flag -> Ordering
$cp1Ord :: Eq Flag
Ord, Ord Flag
Ord Flag
-> ((Flag, Flag) -> [Flag])
-> ((Flag, Flag) -> Flag -> Int)
-> ((Flag, Flag) -> Flag -> Int)
-> ((Flag, Flag) -> Flag -> Bool)
-> ((Flag, Flag) -> Int)
-> ((Flag, Flag) -> Int)
-> Ix Flag
(Flag, Flag) -> Int
(Flag, Flag) -> [Flag]
(Flag, Flag) -> Flag -> Bool
(Flag, Flag) -> Flag -> Int
forall a.
Ord a
-> ((a, a) -> [a])
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Bool)
-> ((a, a) -> Int)
-> ((a, a) -> Int)
-> Ix a
unsafeRangeSize :: (Flag, Flag) -> Int
$cunsafeRangeSize :: (Flag, Flag) -> Int
rangeSize :: (Flag, Flag) -> Int
$crangeSize :: (Flag, Flag) -> Int
inRange :: (Flag, Flag) -> Flag -> Bool
$cinRange :: (Flag, Flag) -> Flag -> Bool
unsafeIndex :: (Flag, Flag) -> Flag -> Int
$cunsafeIndex :: (Flag, Flag) -> Flag -> Int
index :: (Flag, Flag) -> Flag -> Int
$cindex :: (Flag, Flag) -> Flag -> Int
range :: (Flag, Flag) -> [Flag]
$crange :: (Flag, Flag) -> [Flag]
$cp1Ix :: Ord Flag
Ix, Flag
Flag -> Flag -> Bounded Flag
forall a. a -> a -> Bounded a
maxBound :: Flag
$cmaxBound :: Flag
minBound :: Flag
$cminBound :: Flag
Bounded)

-- | Mostek was an 8-bit machine.
type Value = SWord 8

-- | Convenient synonym for symbolic machine bits.
type Bit = SBool

-- | Register bank
type Registers = Array Register Value

-- | Flag bank
type Flags = Array Flag Bit

-- | We have three memory locations, sufficient to model our problem
data Location = F1   -- ^ multiplicand
              | F2   -- ^ multiplier
              | LO   -- ^ low byte of the result gets stored here
              deriving (Location -> Location -> Bool
(Location -> Location -> Bool)
-> (Location -> Location -> Bool) -> Eq Location
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Location -> Location -> Bool
$c/= :: Location -> Location -> Bool
== :: Location -> Location -> Bool
$c== :: Location -> Location -> Bool
Eq, Eq Location
Eq Location
-> (Location -> Location -> Ordering)
-> (Location -> Location -> Bool)
-> (Location -> Location -> Bool)
-> (Location -> Location -> Bool)
-> (Location -> Location -> Bool)
-> (Location -> Location -> Location)
-> (Location -> Location -> Location)
-> Ord Location
Location -> Location -> Bool
Location -> Location -> Ordering
Location -> Location -> Location
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Location -> Location -> Location
$cmin :: Location -> Location -> Location
max :: Location -> Location -> Location
$cmax :: Location -> Location -> Location
>= :: Location -> Location -> Bool
$c>= :: Location -> Location -> Bool
> :: Location -> Location -> Bool
$c> :: Location -> Location -> Bool
<= :: Location -> Location -> Bool
$c<= :: Location -> Location -> Bool
< :: Location -> Location -> Bool
$c< :: Location -> Location -> Bool
compare :: Location -> Location -> Ordering
$ccompare :: Location -> Location -> Ordering
$cp1Ord :: Eq Location
Ord, Ord Location
Ord Location
-> ((Location, Location) -> [Location])
-> ((Location, Location) -> Location -> Int)
-> ((Location, Location) -> Location -> Int)
-> ((Location, Location) -> Location -> Bool)
-> ((Location, Location) -> Int)
-> ((Location, Location) -> Int)
-> Ix Location
(Location, Location) -> Int
(Location, Location) -> [Location]
(Location, Location) -> Location -> Bool
(Location, Location) -> Location -> Int
forall a.
Ord a
-> ((a, a) -> [a])
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Bool)
-> ((a, a) -> Int)
-> ((a, a) -> Int)
-> Ix a
unsafeRangeSize :: (Location, Location) -> Int
$cunsafeRangeSize :: (Location, Location) -> Int
rangeSize :: (Location, Location) -> Int
$crangeSize :: (Location, Location) -> Int
inRange :: (Location, Location) -> Location -> Bool
$cinRange :: (Location, Location) -> Location -> Bool
unsafeIndex :: (Location, Location) -> Location -> Int
$cunsafeIndex :: (Location, Location) -> Location -> Int
index :: (Location, Location) -> Location -> Int
$cindex :: (Location, Location) -> Location -> Int
range :: (Location, Location) -> [Location]
$crange :: (Location, Location) -> [Location]
$cp1Ix :: Ord Location
Ix, Location
Location -> Location -> Bounded Location
forall a. a -> a -> Bounded a
maxBound :: Location
$cmaxBound :: Location
minBound :: Location
$cminBound :: Location
Bounded)

-- | Memory is simply an array from locations to values
type Memory = Array Location Value

-- | Abstraction of the machine: The CPU consists of memory, registers, and flags.
-- Unlike traditional hardware, we assume the program is stored in some other memory area that
-- we need not model. (No self modifying programs!)
--
-- 'Mostek' is equipped with an automatically derived 'Mergeable' instance
-- because each field is 'Mergeable'.
data Mostek = Mostek { Mostek -> Memory
memory    :: Memory
                     , Mostek -> Registers
registers :: Registers
                     , Mostek -> Flags
flags     :: Flags
                     } deriving ((forall x. Mostek -> Rep Mostek x)
-> (forall x. Rep Mostek x -> Mostek) -> Generic Mostek
forall x. Rep Mostek x -> Mostek
forall x. Mostek -> Rep Mostek x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Mostek x -> Mostek
$cfrom :: forall x. Mostek -> Rep Mostek x
Generic, Bool -> SBool -> Mostek -> Mostek -> Mostek
(Bool -> SBool -> Mostek -> Mostek -> Mostek)
-> (forall b.
    (Ord b, SymVal b, Num b) =>
    [Mostek] -> Mostek -> SBV b -> Mostek)
-> Mergeable Mostek
forall b.
(Ord b, SymVal b, Num b) =>
[Mostek] -> Mostek -> SBV b -> Mostek
forall a.
(Bool -> SBool -> a -> a -> a)
-> (forall b. (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a)
-> Mergeable a
select :: [Mostek] -> Mostek -> SBV b -> Mostek
$cselect :: forall b.
(Ord b, SymVal b, Num b) =>
[Mostek] -> Mostek -> SBV b -> Mostek
symbolicMerge :: Bool -> SBool -> Mostek -> Mostek -> Mostek
$csymbolicMerge :: Bool -> SBool -> Mostek -> Mostek -> Mostek
Mergeable)

-- | Given a machine state, compute a value out of it
type Extract a = Mostek -> a

-- | Programs are essentially state transformers (on the machine state)
type Program = Mostek -> Mostek

------------------------------------------------------------------
-- * Low-level operations
------------------------------------------------------------------

-- | Get the value of a given register
getReg :: Register -> Extract Value
getReg :: Register -> Extract Value
getReg Register
r Mostek
m = Mostek -> Registers
registers Mostek
m Registers -> Register -> Value
forall i e. Ix i => Array i e -> i -> e
! Register
r

-- | Set the value of a given register
setReg :: Register -> Value -> Program
setReg :: Register -> Value -> Mostek -> Mostek
setReg Register
r Value
v Mostek
m = Mostek
m {registers :: Registers
registers = Mostek -> Registers
registers Mostek
m Registers -> [(Register, Value)] -> Registers
forall i e. Ix i => Array i e -> [(i, e)] -> Array i e
// [(Register
r, Value
v)]}

-- | Get the value of a flag
getFlag :: Flag -> Extract Bit
getFlag :: Flag -> Extract SBool
getFlag Flag
f Mostek
m = Mostek -> Flags
flags Mostek
m Flags -> Flag -> SBool
forall i e. Ix i => Array i e -> i -> e
! Flag
f

-- | Set the value of a flag
setFlag :: Flag -> Bit -> Program
setFlag :: Flag -> SBool -> Mostek -> Mostek
setFlag Flag
f SBool
b Mostek
m = Mostek
m {flags :: Flags
flags = Mostek -> Flags
flags Mostek
m Flags -> [(Flag, SBool)] -> Flags
forall i e. Ix i => Array i e -> [(i, e)] -> Array i e
// [(Flag
f, SBool
b)]}

-- | Read memory
peek :: Location -> Extract Value
peek :: Location -> Extract Value
peek Location
a Mostek
m = Mostek -> Memory
memory Mostek
m Memory -> Location -> Value
forall i e. Ix i => Array i e -> i -> e
! Location
a

-- | Write to memory
poke :: Location -> Value -> Program
poke :: Location -> Value -> Mostek -> Mostek
poke Location
a Value
v Mostek
m = Mostek
m {memory :: Memory
memory = Mostek -> Memory
memory Mostek
m Memory -> [(Location, Value)] -> Memory
forall i e. Ix i => Array i e -> [(i, e)] -> Array i e
// [(Location
a, Value
v)]}

-- | Checking overflow. In Legato's multiplier the @ADC@ instruction
-- needs to see if the expression x + y + c overflowed, as checked
-- by this function. Note that we verify the correctness of this check
-- separately below in `checkOverflowCorrect`.
checkOverflow :: SWord 8 -> SWord 8 -> SBool -> SBool
checkOverflow :: Value -> Value -> SBool -> SBool
checkOverflow Value
x Value
y SBool
c = Value
s Value -> Value -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< Value
x SBool -> SBool -> SBool
.|| Value
s Value -> Value -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< Value
y SBool -> SBool -> SBool
.|| Value
s' Value -> Value -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< Value
s
  where s :: Value
s  = Value
x Value -> Value -> Value
forall a. Num a => a -> a -> a
+ Value
y
        s' :: Value
s' = Value
s Value -> Value -> Value
forall a. Num a => a -> a -> a
+ SBool -> Value -> Value -> Value
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
c Value
1 Value
0

-- | Correctness theorem for our `checkOverflow` implementation.
--
--   We have:
--
--   >>> checkOverflowCorrect
--   Q.E.D.
checkOverflowCorrect :: IO ThmResult
checkOverflowCorrect :: IO ThmResult
checkOverflowCorrect = Value -> Value -> SBool -> SBool
checkOverflow (Value -> Value -> SBool -> SBool)
-> (Value -> Value -> SBool -> SBool) -> IO ThmResult
forall a. Equality a => a -> a -> IO ThmResult
=== Value -> Value -> SBool -> SBool
overflow
  where -- Reference spec for overflow. We do the addition
        -- using 16 bits and check that it's larger than 255
        overflow :: SWord 8 -> SWord 8 -> SBool -> SBool
        overflow :: Value -> Value -> SBool -> SBool
overflow Value
x Value
y SBool
c = (Value
0 Value -> Value -> SBV (WordN (8 + 8))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# Value
x) SBV (WordN 16) -> SBV (WordN 16) -> SBV (WordN 16)
forall a. Num a => a -> a -> a
+ (Value
0 Value -> Value -> SBV (WordN (8 + 8))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# Value
y) SBV (WordN 16) -> SBV (WordN 16) -> SBV (WordN 16)
forall a. Num a => a -> a -> a
+ SBool -> SBV (WordN 16) -> SBV (WordN 16) -> SBV (WordN 16)
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
c SBV (WordN 16)
1 SBV (WordN 16)
0 SBV (WordN 16) -> SBV (WordN 16) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> (SBV (WordN 16)
255 :: SWord 16)
------------------------------------------------------------------
-- * Instruction set
------------------------------------------------------------------

-- | An instruction is modeled as a 'Program' transformer. We model
-- mostek programs in direct continuation passing style.
type Instruction = Program -> Program

-- | LDX: Set register @X@ to value @v@
ldx :: Value -> Instruction
ldx :: Value -> Instruction
ldx Value
v Mostek -> Mostek
k = Mostek -> Mostek
k (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> Value -> Mostek -> Mostek
setReg Register
RegX Value
v

-- | LDA: Set register @A@ to value @v@
lda :: Value -> Instruction
lda :: Value -> Instruction
lda Value
v Mostek -> Mostek
k = Mostek -> Mostek
k (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> Value -> Mostek -> Mostek
setReg Register
RegA Value
v

-- | CLC: Clear the carry flag
clc :: Instruction
clc :: Instruction
clc Mostek -> Mostek
k = Mostek -> Mostek
k (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBool -> Mostek -> Mostek
setFlag Flag
FlagC SBool
sFalse

-- | ROR, memory version: Rotate the value at memory location @a@
-- to the right by 1 bit, using the carry flag as a transfer position.
-- That is, the final bit of the memory location becomes the new carry
-- and the carry moves over to the first bit. This very instruction
-- is one of the reasons why Legato's multiplier is quite hard to understand
-- and is typically presented as a verification challenge.
rorM :: Location -> Instruction
rorM :: Location -> Instruction
rorM Location
a Mostek -> Mostek
k Mostek
m = Mostek -> Mostek
k (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBool -> Mostek -> Mostek
setFlag Flag
FlagC SBool
c' (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Location -> Value -> Mostek -> Mostek
poke Location
a Value
v' Instruction
forall a b. (a -> b) -> a -> b
$ Mostek
m
  where v :: Value
v  = Location -> Extract Value
peek Location
a Mostek
m
        c :: SBool
c  = Flag -> Extract SBool
getFlag Flag
FlagC Mostek
m
        v' :: Value
v' = Value -> Int -> SBool -> Value
forall a. SFiniteBits a => SBV a -> Int -> SBool -> SBV a
setBitTo (Value
v Value -> Int -> Value
forall a. Bits a => a -> Int -> a
`rotateR` Int
1) Int
7 SBool
c
        c' :: SBool
c' = Value -> Int -> SBool
forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit Value
v Int
0

-- | ROR, register version: Same as 'rorM', except through register @r@.
rorR :: Register -> Instruction
rorR :: Register -> Instruction
rorR Register
r Mostek -> Mostek
k Mostek
m = Mostek -> Mostek
k (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBool -> Mostek -> Mostek
setFlag Flag
FlagC SBool
c' (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> Value -> Mostek -> Mostek
setReg Register
r Value
v' Instruction
forall a b. (a -> b) -> a -> b
$ Mostek
m
  where v :: Value
v  = Register -> Extract Value
getReg Register
r Mostek
m
        c :: SBool
c  = Flag -> Extract SBool
getFlag Flag
FlagC Mostek
m
        v' :: Value
v' = Value -> Int -> SBool -> Value
forall a. SFiniteBits a => SBV a -> Int -> SBool -> SBV a
setBitTo (Value
v Value -> Int -> Value
forall a. Bits a => a -> Int -> a
`rotateR` Int
1) Int
7 SBool
c
        c' :: SBool
c' = Value -> Int -> SBool
forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit Value
v Int
0

-- | BCC: branch to label @l@ if the carry flag is sFalse
bcc :: Program -> Instruction
bcc :: (Mostek -> Mostek) -> Instruction
bcc Mostek -> Mostek
l Mostek -> Mostek
k Mostek
m = SBool -> Mostek -> Mostek -> Mostek
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBool
c SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool
sFalse) (Mostek -> Mostek
l Mostek
m) (Mostek -> Mostek
k Mostek
m)
  where c :: SBool
c = Flag -> Extract SBool
getFlag Flag
FlagC Mostek
m

-- | ADC: Increment the value of register @A@ by the value of memory contents
-- at location @a@, using the carry-bit as the carry-in for the addition.
adc :: Location -> Instruction
adc :: Location -> Instruction
adc Location
a Mostek -> Mostek
k Mostek
m = Mostek -> Mostek
k (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBool -> Mostek -> Mostek
setFlag Flag
FlagZ (Value
v' Value -> Value -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Value
0) (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBool -> Mostek -> Mostek
setFlag Flag
FlagC SBool
c' (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> Value -> Mostek -> Mostek
setReg Register
RegA Value
v' Instruction
forall a b. (a -> b) -> a -> b
$ Mostek
m
  where v :: Value
v  = Location -> Extract Value
peek Location
a Mostek
m
        ra :: Value
ra = Register -> Extract Value
getReg Register
RegA Mostek
m
        c :: SBool
c  = Flag -> Extract SBool
getFlag Flag
FlagC Mostek
m
        v' :: Value
v' = Value
v Value -> Value -> Value
forall a. Num a => a -> a -> a
+ Value
ra Value -> Value -> Value
forall a. Num a => a -> a -> a
+ SBool -> Value -> Value -> Value
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
c Value
1 Value
0
        c' :: SBool
c' = Value -> Value -> SBool -> SBool
checkOverflow Value
v Value
ra SBool
c

-- | DEX: Decrement the value of register @X@
dex :: Instruction
dex :: Instruction
dex Mostek -> Mostek
k Mostek
m = Mostek -> Mostek
k (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBool -> Mostek -> Mostek
setFlag Flag
FlagZ (Value
x Value -> Value -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Value
0) (Mostek -> Mostek) -> Instruction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> Value -> Mostek -> Mostek
setReg Register
RegX Value
x Instruction
forall a b. (a -> b) -> a -> b
$ Mostek
m
  where x :: Value
x = Register -> Extract Value
getReg Register
RegX Mostek
m Value -> Value -> Value
forall a. Num a => a -> a -> a
- Value
1

-- | BNE: Branch if the zero-flag is sFalse
bne :: Program -> Instruction
bne :: (Mostek -> Mostek) -> Instruction
bne Mostek -> Mostek
l Mostek -> Mostek
k Mostek
m = SBool -> Mostek -> Mostek -> Mostek
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBool
z SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool
sFalse) (Mostek -> Mostek
l Mostek
m) (Mostek -> Mostek
k Mostek
m)
  where z :: SBool
z = Flag -> Extract SBool
getFlag Flag
FlagZ Mostek
m

-- | The 'end' combinator "stops" our program, providing the final continuation
-- that does nothing.
end :: Program
end :: Mostek -> Mostek
end = Mostek -> Mostek
forall a. a -> a
id

------------------------------------------------------------------
-- * Legato's algorithm in Haskell/SBV
------------------------------------------------------------------

-- | Multiplies the contents of @F1@ and @F2@, storing the low byte of the result
-- in @LO@ and the high byte of it in register @A@. The implementation is a direct
-- transliteration of Legato's algorithm given at the top, using our notation.
legato :: Program
legato :: Mostek -> Mostek
legato = Mostek -> Mostek
start
  where start :: Mostek -> Mostek
start   =    Value -> Instruction
ldx Value
8
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ Value -> Instruction
lda Value
0
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ Mostek -> Mostek
loop
        loop :: Mostek -> Mostek
loop    =    Location -> Instruction
rorM Location
F1
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ (Mostek -> Mostek) -> Instruction
bcc Mostek -> Mostek
zeroCoef
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ Instruction
clc
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ Location -> Instruction
adc Location
F2
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ Mostek -> Mostek
zeroCoef
        zeroCoef :: Mostek -> Mostek
zeroCoef =   Register -> Instruction
rorR Register
RegA
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ Location -> Instruction
rorM Location
LO
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ Instruction
dex
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ (Mostek -> Mostek) -> Instruction
bne Mostek -> Mostek
loop
                   Instruction -> Instruction
forall a b. (a -> b) -> a -> b
$ Mostek -> Mostek
end

------------------------------------------------------------------
-- * Verification interface
------------------------------------------------------------------
-- | Given values for  F1 and F2, @runLegato@ takes an arbitrary machine state @m@ and
-- returns the high and low bytes of the multiplication.
runLegato :: Mostek -> (Value, Value)
runLegato :: Mostek -> (Value, Value)
runLegato Mostek
m = (Register -> Extract Value
getReg Register
RegA Mostek
m', Location -> Extract Value
peek Location
LO Mostek
m')
  where m' :: Mostek
m' = Mostek -> Mostek
legato Mostek
m

-- | Helper synonym for capturing relevant bits of Mostek
type InitVals = ( Value      -- Contents of mem location F1
                , Value      -- Contents of mem location F2
                , Value      -- Contents of mem location LO
                , Value      -- Content of Register X
                , Value      -- Content of Register A
                , Bit        -- Value of FlagC
                , Bit        -- Value of FlagZ
                )

-- | Create an instance of the Mostek machine, initialized by the memory and the relevant
-- values of the registers and the flags
initMachine :: InitVals -> Mostek
initMachine :: InitVals -> Mostek
initMachine (Value
f1, Value
f2, Value
lo, Value
rx, Value
ra, SBool
fc, SBool
fz) = Mostek :: Memory -> Registers -> Flags -> Mostek
Mostek { memory :: Memory
memory    = (Location, Location) -> [(Location, Value)] -> Memory
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (Location
forall a. Bounded a => a
minBound, Location
forall a. Bounded a => a
maxBound) [(Location
F1, Value
f1), (Location
F2, Value
f2), (Location
LO, Value
lo)]
                                                  , registers :: Registers
registers = (Register, Register) -> [(Register, Value)] -> Registers
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (Register
forall a. Bounded a => a
minBound, Register
forall a. Bounded a => a
maxBound) [(Register
RegX, Value
rx),  (Register
RegA, Value
ra)]
                                                  , flags :: Flags
flags     = (Flag, Flag) -> [(Flag, SBool)] -> Flags
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (Flag
forall a. Bounded a => a
minBound, Flag
forall a. Bounded a => a
maxBound) [(Flag
FlagC, SBool
fc), (Flag
FlagZ, SBool
fz)]
                                                  }

-- | The correctness theorem. For all possible memory configurations, the factors (@x@ and @y@ below), the location
-- of the low-byte result and the initial-values of registers and the flags, this function will return True only if
-- running Legato's algorithm does indeed compute the product of @x@ and @y@ correctly.
legatoIsCorrect :: InitVals -> SBool
legatoIsCorrect :: InitVals -> SBool
legatoIsCorrect initVals :: InitVals
initVals@(Value
x, Value
y, Value
_, Value
_, Value
_, SBool
_, SBool
_) = SBV (WordN 16)
result SBV (WordN 16) -> SBV (WordN 16) -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV (WordN 16)
expected
    where (Value
hi, Value
lo) = Mostek -> (Value, Value)
runLegato (InitVals -> Mostek
initMachine InitVals
initVals)
          -- NB. perform the comparison over 16 bit values to avoid overflow!
          -- If Value changes to be something else, modify this accordingly.
          result, expected :: SWord 16
          result :: SBV (WordN 16)
result   = SBV (WordN 16)
256 SBV (WordN 16) -> SBV (WordN 16) -> SBV (WordN 16)
forall a. Num a => a -> a -> a
* (Value
0 Value -> Value -> SBV (WordN (8 + 8))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# Value
hi) SBV (WordN 16) -> SBV (WordN 16) -> SBV (WordN 16)
forall a. Num a => a -> a -> a
+ (Value
0 Value -> Value -> SBV (WordN (8 + 8))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# Value
lo)
          expected :: SBV (WordN 16)
expected = (Value
0 Value -> Value -> SBV (WordN (8 + 8))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# Value
x) SBV (WordN 16) -> SBV (WordN 16) -> SBV (WordN 16)
forall a. Num a => a -> a -> a
* (Value
0 Value -> Value -> SBV (WordN (8 + 8))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# Value
y)

------------------------------------------------------------------
-- * Verification
------------------------------------------------------------------

-- | The correctness theorem.
correctnessTheorem :: IO ThmResult
correctnessTheorem :: IO ThmResult
correctnessTheorem = SMTConfig -> SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => SMTConfig -> a -> IO ThmResult
proveWith SMTConfig
defaultSMTCfg{timing :: Timing
timing = Timing
PrintTiming} (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
        Value
lo <- String -> Symbolic Value
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord String
"lo"

        Value
x <- String -> Symbolic Value
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord  String
"x"
        Value
y <- String -> Symbolic Value
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord  String
"y"

        Value
regX  <- String -> Symbolic Value
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord String
"regX"
        Value
regA  <- String -> Symbolic Value
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord String
"regA"

        SBool
flagC <- String -> SymbolicT IO SBool
sBool String
"flagC"
        SBool
flagZ <- String -> SymbolicT IO SBool
sBool String
"flagZ"

        SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ InitVals -> SBool
legatoIsCorrect (Value
x, Value
y, Value
lo, Value
regX, Value
regA, SBool
flagC, SBool
flagZ)

------------------------------------------------------------------
-- * C Code generation
------------------------------------------------------------------

-- | Generate a C program that implements Legato's algorithm automatically.
legatoInC :: IO ()
legatoInC :: IO ()
legatoInC = Maybe String -> String -> SBVCodeGen () -> IO ()
forall a. Maybe String -> String -> SBVCodeGen a -> IO a
compileToC Maybe String
forall a. Maybe a
Nothing String
"runLegato" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                Value
x <- String -> SBVCodeGen Value
forall a. SymVal a => String -> SBVCodeGen (SBV a)
cgInput String
"x"
                Value
y <- String -> SBVCodeGen Value
forall a. SymVal a => String -> SBVCodeGen (SBV a)
cgInput String
"y"
                let (Value
hi, Value
lo) = Mostek -> (Value, Value)
runLegato (InitVals -> Mostek
initMachine (Value
x, Value
y, Value
0, Value
0, Value
0, SBool
sFalse, SBool
sFalse))
                String -> Value -> SBVCodeGen ()
forall a. String -> SBV a -> SBVCodeGen ()
cgOutput String
"hi" Value
hi
                String -> Value -> SBVCodeGen ()
forall a. String -> SBV a -> SBVCodeGen ()
cgOutput String
"lo" Value
lo

{-# ANN legato ("HLint: ignore Redundant $" :: String)        #-}
{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}