    -----------------------------------------------------------------------------
    -- |
    -- 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 r :: Register
    r m :: 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 r :: Register
    r v :: Value
    v m :: 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 f :: Flag
    f m :: 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 f :: Flag
    f b :: SBool
    b m :: 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 a :: Location
    a m :: 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 a :: Location
    a v :: Value
    v m :: 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 multipler 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 x :: Value
    x y :: Value
    y c :: 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 1 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 x :: Value
    x y :: Value
    y c :: SBool
    c = (0 Value -> Value -> SBV (WordN (8 + 8))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero 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
    + (0 Value -> Value -> SBV (WordN (8 + 8))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero 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 1 0 SBV (WordN 16) -> SBV (WordN 16) -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .> (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 v :: Value
    v k :: 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 v :: Value
    v k :: 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 k :: 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 a :: Location
    a k :: Mostek -> Mostek
    k m :: 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` 1) 7 SBool
    c
            c' :: SBool
    c' = Value -> Int -> SBool
    forall a. SFiniteBits a => SBV a -> Int -> SBool
    sTestBit Value
    v 0

    -- | ROR, register version: Same as 'rorM', except through register @r@.
    rorR :: Register -> Instruction
    rorR :: Register -> Instruction
    rorR r :: Register
    r k :: Mostek -> Mostek
    k m :: 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` 1) 7 SBool
    c
            c' :: SBool
    c' = Value -> Int -> SBool
    forall a. SFiniteBits a => SBV a -> Int -> SBool
    sTestBit Value
    v 0

    -- | BCC: branch to label @l@ if the carry flag is sFalse
    bcc :: Program -> Instruction
    bcc :: (Mostek -> Mostek) -> Instruction
    bcc l :: Mostek -> Mostek
    l k :: Mostek -> Mostek
    k m :: 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 a :: Location
    a k :: Mostek -> Mostek
    k m :: 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
    .== 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 1 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 k :: Mostek -> Mostek
    k m :: 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
    .== 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
    - 1

    -- | BNE: Branch if the zero-flag is sFalse
    bne :: Program -> Instruction
    bne :: (Mostek -> Mostek) -> Instruction
    bne l :: Mostek -> Mostek
    l k :: Mostek -> Mostek
    k m :: 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 8
                       Instruction -> Instruction
    forall a b. (a -> b) -> a -> b
    $ Value -> Instruction
    lda 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 m :: 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 (f1 :: Value
    f1, f2 :: Value
    f2, lo :: Value
    lo, rx :: Value
    rx, ra :: Value
    ra, fc :: SBool
    fc, fz :: 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@(x :: Value
    x, y :: Value
    y, _, _, _, _, _) = SBV (WordN 16)
    result SBV (WordN 16) -> SBV (WordN 16) -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV (WordN 16)
    expected
        where (hi :: Value
    hi, lo :: 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   = 256 SBV (WordN 16) -> SBV (WordN 16) -> SBV (WordN 16)
    forall a. Num a => a -> a -> a
    * (0 Value -> Value -> SBV (WordN (8 + 8))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero 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
    + (0 Value -> Value -> SBV (WordN (8 + 8))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
     SymVal (bv m)) =>
    SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # Value
    lo)
              expected :: SBV (WordN 16)
    expected = (0 Value -> Value -> SBV (WordN (8 + 8))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero 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
    * (0 Value -> Value -> SBV (WordN (8 + 8))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero 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, IsNonZero n) =>
    String -> Symbolic (SWord n)
    sWord "lo"

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

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

            SBool
    flagC <- String -> SymbolicT IO SBool
    sBool "flagC"
            SBool
    flagZ <- String -> SymbolicT IO SBool
    sBool "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 "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 "x"
                    Value
    y <- String -> SBVCodeGen Value
    forall a. SymVal a => String -> SBVCodeGen (SBV a)
    cgInput "y"
                    let (hi :: Value
    hi, lo :: Value
    lo) = Mostek -> (Value, Value)
    runLegato (InitVals -> Mostek
    initMachine (Value
    x, Value
    y, 0, 0, 0, SBool
    sFalse, SBool
    sFalse))
                    String -> Value -> SBVCodeGen ()
    forall a. String -> SBV a -> SBVCodeGen ()
    cgOutput "hi" Value
    hi
                    String -> Value -> SBVCodeGen ()
    forall a. String -> SBV a -> SBVCodeGen ()
    cgOutput "lo" Value
    lo

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