-----------------------------------------------------------------------------
-- |
-- 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
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
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
Ord, Ord 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]
Ix, 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
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
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
Ord, Ord 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]
Ix, 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
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
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
Ord, Ord 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]
Ix, 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. 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 -> SBV Bool -> Mostek -> Mostek -> Mostek
forall b.
(Ord b, SymVal b, Num b) =>
[Mostek] -> Mostek -> SBV b -> Mostek
forall a.
(Bool -> SBV Bool -> a -> a -> a)
-> (forall b. (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a)
-> Mergeable a
select :: forall b.
(Ord b, SymVal b, Num b) =>
[Mostek] -> Mostek -> SBV b -> Mostek
$cselect :: forall b.
(Ord b, SymVal b, Num b) =>
[Mostek] -> Mostek -> SBV b -> Mostek
symbolicMerge :: Bool -> SBV Bool -> Mostek -> Mostek -> Mostek
$csymbolicMerge :: Bool -> SBV Bool -> 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 (SBV (WordN 8))
getReg Register
r Mostek
m = Mostek -> Registers
registers Mostek
m 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 -> SBV (WordN 8) -> Mostek -> Mostek
setReg Register
r SBV (WordN 8)
v Mostek
m = Mostek
m {registers :: Registers
registers = Mostek -> Registers
registers Mostek
m forall i e. Ix i => Array i e -> [(i, e)] -> Array i e
// [(Register
r, SBV (WordN 8)
v)]}

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

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

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

-- | Write to memory
poke :: Location -> Value -> Program
poke :: Location -> SBV (WordN 8) -> Mostek -> Mostek
poke Location
a SBV (WordN 8)
v Mostek
m = Mostek
m {memory :: Memory
memory = Mostek -> Memory
memory Mostek
m forall i e. Ix i => Array i e -> [(i, e)] -> Array i e
// [(Location
a, SBV (WordN 8)
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 :: SBV (WordN 8) -> SBV (WordN 8) -> SBV Bool -> SBV Bool
checkOverflow SBV (WordN 8)
x SBV (WordN 8)
y SBV Bool
c = SBV (WordN 8)
s forall a. OrdSymbolic a => a -> a -> SBV Bool
.< SBV (WordN 8)
x SBV Bool -> SBV Bool -> SBV Bool
.|| SBV (WordN 8)
s forall a. OrdSymbolic a => a -> a -> SBV Bool
.< SBV (WordN 8)
y SBV Bool -> SBV Bool -> SBV Bool
.|| SBV (WordN 8)
s' forall a. OrdSymbolic a => a -> a -> SBV Bool
.< SBV (WordN 8)
s
  where s :: SBV (WordN 8)
s  = SBV (WordN 8)
x forall a. Num a => a -> a -> a
+ SBV (WordN 8)
y
        s' :: SBV (WordN 8)
s' = SBV (WordN 8)
s forall a. Num a => a -> a -> a
+ forall a. Mergeable a => SBV Bool -> a -> a -> a
ite SBV Bool
c SBV (WordN 8)
1 SBV (WordN 8)
0

-- | Correctness theorem for our `checkOverflow` implementation.
--
--   We have:
--
--   >>> checkOverflowCorrect
--   Q.E.D.
checkOverflowCorrect :: IO ThmResult
checkOverflowCorrect :: IO ThmResult
checkOverflowCorrect = SBV (WordN 8) -> SBV (WordN 8) -> SBV Bool -> SBV Bool
checkOverflow forall a. Equality a => a -> a -> IO ThmResult
=== SBV (WordN 8) -> SBV (WordN 8) -> SBV Bool -> SBV Bool
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 :: SBV (WordN 8) -> SBV (WordN 8) -> SBV Bool -> SBV Bool
overflow SBV (WordN 8)
x SBV (WordN 8)
y SBV Bool
c = (SBV (WordN 8)
0 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))
# SBV (WordN 8)
x) forall a. Num a => a -> a -> a
+ (SBV (WordN 8)
0 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))
# SBV (WordN 8)
y) forall a. Num a => a -> a -> a
+ forall a. Mergeable a => SBV Bool -> a -> a -> a
ite SBV Bool
c SWord 16
1 SWord 16
0 forall a. OrdSymbolic a => a -> a -> SBV Bool
.> (SWord 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 :: SBV (WordN 8) -> Instruction
ldx SBV (WordN 8)
v Mostek -> Mostek
k = Mostek -> Mostek
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> SBV (WordN 8) -> Mostek -> Mostek
setReg Register
RegX SBV (WordN 8)
v

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

-- | CLC: Clear the carry flag
clc :: Instruction
clc :: Instruction
clc Mostek -> Mostek
k = Mostek -> Mostek
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBV Bool -> Mostek -> Mostek
setFlag Flag
FlagC SBV Bool
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBV Bool -> Mostek -> Mostek
setFlag Flag
FlagC SBV Bool
c' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Location -> SBV (WordN 8) -> Mostek -> Mostek
poke Location
a SBV (WordN 8)
v' forall a b. (a -> b) -> a -> b
$ Mostek
m
  where v :: SBV (WordN 8)
v  = Location -> Extract (SBV (WordN 8))
peek Location
a Mostek
m
        c :: SBV Bool
c  = Flag -> Extract (SBV Bool)
getFlag Flag
FlagC Mostek
m
        v' :: SBV (WordN 8)
v' = forall a. SFiniteBits a => SBV a -> Int -> SBV Bool -> SBV a
setBitTo (SBV (WordN 8)
v forall a. Bits a => a -> Int -> a
`rotateR` Int
1) Int
7 SBV Bool
c
        c' :: SBV Bool
c' = forall a. SFiniteBits a => SBV a -> Int -> SBV Bool
sTestBit SBV (WordN 8)
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBV Bool -> Mostek -> Mostek
setFlag Flag
FlagC SBV Bool
c' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> SBV (WordN 8) -> Mostek -> Mostek
setReg Register
r SBV (WordN 8)
v' forall a b. (a -> b) -> a -> b
$ Mostek
m
  where v :: SBV (WordN 8)
v  = Register -> Extract (SBV (WordN 8))
getReg Register
r Mostek
m
        c :: SBV Bool
c  = Flag -> Extract (SBV Bool)
getFlag Flag
FlagC Mostek
m
        v' :: SBV (WordN 8)
v' = forall a. SFiniteBits a => SBV a -> Int -> SBV Bool -> SBV a
setBitTo (SBV (WordN 8)
v forall a. Bits a => a -> Int -> a
`rotateR` Int
1) Int
7 SBV Bool
c
        c' :: SBV Bool
c' = forall a. SFiniteBits a => SBV a -> Int -> SBV Bool
sTestBit SBV (WordN 8)
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 = forall a. Mergeable a => SBV Bool -> a -> a -> a
ite (SBV Bool
c forall a. EqSymbolic a => a -> a -> SBV Bool
.== SBV Bool
sFalse) (Mostek -> Mostek
l Mostek
m) (Mostek -> Mostek
k Mostek
m)
  where c :: SBV Bool
c = Flag -> Extract (SBV Bool)
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBV Bool -> Mostek -> Mostek
setFlag Flag
FlagZ (SBV (WordN 8)
v' forall a. EqSymbolic a => a -> a -> SBV Bool
.== SBV (WordN 8)
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBV Bool -> Mostek -> Mostek
setFlag Flag
FlagC SBV Bool
c' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> SBV (WordN 8) -> Mostek -> Mostek
setReg Register
RegA SBV (WordN 8)
v' forall a b. (a -> b) -> a -> b
$ Mostek
m
  where v :: SBV (WordN 8)
v  = Location -> Extract (SBV (WordN 8))
peek Location
a Mostek
m
        ra :: SBV (WordN 8)
ra = Register -> Extract (SBV (WordN 8))
getReg Register
RegA Mostek
m
        c :: SBV Bool
c  = Flag -> Extract (SBV Bool)
getFlag Flag
FlagC Mostek
m
        v' :: SBV (WordN 8)
v' = SBV (WordN 8)
v forall a. Num a => a -> a -> a
+ SBV (WordN 8)
ra forall a. Num a => a -> a -> a
+ forall a. Mergeable a => SBV Bool -> a -> a -> a
ite SBV Bool
c SBV (WordN 8)
1 SBV (WordN 8)
0
        c' :: SBV Bool
c' = SBV (WordN 8) -> SBV (WordN 8) -> SBV Bool -> SBV Bool
checkOverflow SBV (WordN 8)
v SBV (WordN 8)
ra SBV Bool
c

-- | DEX: Decrement the value of register @X@
dex :: Instruction
dex :: Instruction
dex Mostek -> Mostek
k Mostek
m = Mostek -> Mostek
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flag -> SBV Bool -> Mostek -> Mostek
setFlag Flag
FlagZ (SBV (WordN 8)
x forall a. EqSymbolic a => a -> a -> SBV Bool
.== SBV (WordN 8)
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register -> SBV (WordN 8) -> Mostek -> Mostek
setReg Register
RegX SBV (WordN 8)
x forall a b. (a -> b) -> a -> b
$ Mostek
m
  where x :: SBV (WordN 8)
x = Register -> Extract (SBV (WordN 8))
getReg Register
RegX Mostek
m forall a. Num a => a -> a -> a
- SBV (WordN 8)
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 = forall a. Mergeable a => SBV Bool -> a -> a -> a
ite (SBV Bool
z forall a. EqSymbolic a => a -> a -> SBV Bool
.== SBV Bool
sFalse) (Mostek -> Mostek
l Mostek
m) (Mostek -> Mostek
k Mostek
m)
  where z :: SBV Bool
z = Flag -> Extract (SBV Bool)
getFlag Flag
FlagZ Mostek
m

-- | The 'end' combinator "stops" our program, providing the final continuation
-- that does nothing.
end :: Program
end :: Mostek -> Mostek
end = 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   =    SBV (WordN 8) -> Instruction
ldx SBV (WordN 8)
8
                   forall a b. (a -> b) -> a -> b
$ SBV (WordN 8) -> Instruction
lda SBV (WordN 8)
0
                   forall a b. (a -> b) -> a -> b
$ Mostek -> Mostek
loop
        loop :: Mostek -> Mostek
loop    =    Location -> Instruction
rorM Location
F1
                   forall a b. (a -> b) -> a -> b
$ (Mostek -> Mostek) -> Instruction
bcc Mostek -> Mostek
zeroCoef
                   forall a b. (a -> b) -> a -> b
$ Instruction
clc
                   forall a b. (a -> b) -> a -> b
$ Location -> Instruction
adc Location
F2
                   forall a b. (a -> b) -> a -> b
$ Mostek -> Mostek
zeroCoef
        zeroCoef :: Mostek -> Mostek
zeroCoef =   Register -> Instruction
rorR Register
RegA
                   forall a b. (a -> b) -> a -> b
$ Location -> Instruction
rorM Location
LO
                   forall a b. (a -> b) -> a -> b
$ Instruction
dex
                   forall a b. (a -> b) -> a -> b
$ (Mostek -> Mostek) -> Instruction
bne Mostek -> Mostek
loop
                   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 -> (SBV (WordN 8), SBV (WordN 8))
runLegato Mostek
m = (Register -> Extract (SBV (WordN 8))
getReg Register
RegA Mostek
m', Location -> Extract (SBV (WordN 8))
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 (SBV (WordN 8)
f1, SBV (WordN 8)
f2, SBV (WordN 8)
lo, SBV (WordN 8)
rx, SBV (WordN 8)
ra, SBV Bool
fc, SBV Bool
fz) = Mostek { memory :: Memory
memory    = forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (forall a. Bounded a => a
minBound, forall a. Bounded a => a
maxBound) [(Location
F1, SBV (WordN 8)
f1), (Location
F2, SBV (WordN 8)
f2), (Location
LO, SBV (WordN 8)
lo)]
                                                  , registers :: Registers
registers = forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (forall a. Bounded a => a
minBound, forall a. Bounded a => a
maxBound) [(Register
RegX, SBV (WordN 8)
rx),  (Register
RegA, SBV (WordN 8)
ra)]
                                                  , flags :: Flags
flags     = forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (forall a. Bounded a => a
minBound, forall a. Bounded a => a
maxBound) [(Flag
FlagC, SBV Bool
fc), (Flag
FlagZ, SBV Bool
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 -> SBV Bool
legatoIsCorrect initVals :: InitVals
initVals@(SBV (WordN 8)
x, SBV (WordN 8)
y, SBV (WordN 8)
_, SBV (WordN 8)
_, SBV (WordN 8)
_, SBV Bool
_, SBV Bool
_) = SWord 16
result forall a. EqSymbolic a => a -> a -> SBV Bool
.== SWord 16
expected
    where (SBV (WordN 8)
hi, SBV (WordN 8)
lo) = Mostek -> (SBV (WordN 8), SBV (WordN 8))
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 :: SWord 16
result   = SWord 16
256 forall a. Num a => a -> a -> a
* (SBV (WordN 8)
0 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))
# SBV (WordN 8)
hi) forall a. Num a => a -> a -> a
+ (SBV (WordN 8)
0 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))
# SBV (WordN 8)
lo)
          expected :: SWord 16
expected = (SBV (WordN 8)
0 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))
# SBV (WordN 8)
x) forall a. Num a => a -> a -> a
* (SBV (WordN 8)
0 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))
# SBV (WordN 8)
y)

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

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

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

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

        SBV Bool
flagC <- String -> SymbolicT IO (SBV Bool)
sBool String
"flagC"
        SBV Bool
flagZ <- String -> SymbolicT IO (SBV Bool)
sBool String
"flagZ"

        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ InitVals -> SBV Bool
legatoIsCorrect (SBV (WordN 8)
x, SBV (WordN 8)
y, SBV (WordN 8)
lo, SBV (WordN 8)
regX, SBV (WordN 8)
regA, SBV Bool
flagC, SBV Bool
flagZ)

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

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

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