sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.BitPrecise.Legato

Contents

- Mostek architecture
- Low-level operations
- Instruction set
- Legato's algorithm in Haskell/SBV
- Verification interface
- Verification
- C Code generation

Description

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.

Synopsis

- data Register
  - = RegX
  - | RegA
- data Flag
  - = FlagC
  - | FlagZ
- type Value = SWord 8
- type Bit = SBool
- type Registers = Array Register Value
- type Flags = Array Flag Bit
- data Location
  - = F1
  - | F2
  - | LO
- type Memory = Array Location Value
- data Mostek = Mostek {
  - memory :: Memory
  - registers :: Registers
  - flags :: Flags
  }
- type Extract a = Mostek -> a
- type Program = Mostek -> Mostek
- getReg :: Register -> Extract Value
- setReg :: Register -> Value -> Program
- getFlag :: Flag -> Extract Bit
- setFlag :: Flag -> Bit -> Program
- peek :: Location -> Extract Value
- poke :: Location -> Value -> Program
- checkOverflow :: SWord 8 -> SWord 8 -> SBool -> SBool
- checkOverflowCorrect :: IO ThmResult
- type Instruction = Program -> Program
- ldx :: Value -> Instruction
- lda :: Value -> Instruction
- clc :: Instruction
- rorM :: Location -> Instruction
- rorR :: Register -> Instruction
- bcc :: Program -> Instruction
- adc :: Location -> Instruction
- dex :: Instruction
- bne :: Program -> Instruction
- end :: Program
- legato :: Program
- runLegato :: Mostek -> (Value, Value)
- type InitVals = (Value, Value, Value, Value, Value, Bit, Bit)
- initMachine :: InitVals -> Mostek
- legatoIsCorrect :: InitVals -> SBool
- correctnessTheorem :: IO ThmResult
- legatoInC :: IO ()

# Mostek architecture

data Register Source #

We model only two registers of Mostek that is used in the above algorithm, can add more.

Constructors

RegX |
RegA |

#### Instances

Instances details

Bounded Register Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Methods minBound :: Register Source # maxBound :: Register Source #
Ix Register Source # |

Instance details

Defined in Documentation.SBV.Examples.BitPrecise.Legato

Methods

range :: (Register, Register) -> [Register] Source #

index :: (Register, Register) -> Register -> Int Source #

unsafeIndex :: (Register, Register) -> Register -> Int Source #

inRange :: (Register, Register) -> Register -> Bool Source #

rangeSize :: (Register, Register) -> Int Source #

unsafeRangeSize :: (Register, Register) -> Int Source #

Eq Register Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Methods (==) :: Register -> Register -> Bool Source # (/=) :: Register -> Register -> Bool Source #
Ord Register Source # |

Instance details

Defined in Documentation.SBV.Examples.BitPrecise.Legato

Methods

compare :: Register -> Register -> Ordering Source #

(<) :: Register -> Register -> Bool Source #

(<=) :: Register -> Register -> Bool Source #

(>) :: Register -> Register -> Bool Source #

(>=) :: Register -> Register -> Bool Source #

max :: Register -> Register -> Register Source #

min :: Register -> Register -> Register Source #

data Flag Source #

The carry flag (`FlagC`) and the zero flag (`FlagZ`)

Constructors

FlagC |
FlagZ |

#### Instances

Instances details

Bounded Flag Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Methods minBound :: Flag Source # maxBound :: Flag Source #
Ix Flag Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Methods range :: (Flag, Flag) -> [Flag] Source # index :: (Flag, Flag) -> Flag -> Int Source # unsafeIndex :: (Flag, Flag) -> Flag -> Int Source # inRange :: (Flag, Flag) -> Flag -> Bool Source # rangeSize :: (Flag, Flag) -> Int Source # unsafeRangeSize :: (Flag, Flag) -> Int Source #
Eq Flag Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Methods (==) :: Flag -> Flag -> Bool Source # (/=) :: Flag -> Flag -> Bool Source #
Ord Flag Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Methods compare :: Flag -> Flag -> Ordering Source # (<) :: Flag -> Flag -> Bool Source # (<=) :: Flag -> Flag -> Bool Source # (>) :: Flag -> Flag -> Bool Source # (>=) :: Flag -> Flag -> Bool Source # max :: Flag -> Flag -> Flag Source # min :: Flag -> Flag -> Flag Source #

type Value = SWord 8 Source #

Mostek was an 8-bit machine.

type Bit = SBool Source #

Convenient synonym for symbolic machine bits.

type Registers = Array Register Value Source #

Register bank

type Flags = Array Flag Bit Source #

Flag bank

data Location Source #

We have three memory locations, sufficient to model our problem

Constructors

F1 | multiplicand
F2 | multiplier
LO | low byte of the result gets stored here

#### Instances

Instances details

Bounded Location Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Methods minBound :: Location Source # maxBound :: Location Source #
Ix Location Source # |

Instance details

Defined in Documentation.SBV.Examples.BitPrecise.Legato

Methods

range :: (Location, Location) -> [Location] Source #

index :: (Location, Location) -> Location -> Int Source #

unsafeIndex :: (Location, Location) -> Location -> Int Source #

inRange :: (Location, Location) -> Location -> Bool Source #

rangeSize :: (Location, Location) -> Int Source #

unsafeRangeSize :: (Location, Location) -> Int Source #

Eq Location Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Methods (==) :: Location -> Location -> Bool Source # (/=) :: Location -> Location -> Bool Source #
Ord Location Source # |

Instance details

Defined in Documentation.SBV.Examples.BitPrecise.Legato

Methods

compare :: Location -> Location -> Ordering Source #

(<) :: Location -> Location -> Bool Source #

(<=) :: Location -> Location -> Bool Source #

(>) :: Location -> Location -> Bool Source #

(>=) :: Location -> Location -> Bool Source #

max :: Location -> Location -> Location Source #

min :: Location -> Location -> Location Source #

type Memory = Array Location Value Source #

Memory is simply an array from locations to values

data Mostek Source #

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`.

Constructors

Mostek |

Fields

- memory :: Memory
- registers :: Registers
- flags :: Flags

#### Instances

Instances details

Generic Mostek Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Associated Types type Rep Mostek :: Type -> Type Source # Methods from :: Mostek -> Rep Mostek x Source # to :: Rep Mostek x -> Mostek Source #
Mergeable Mostek Source # |
Instance details Defined in Documentation.SBV.Examples.BitPrecise.Legato Methods symbolicMerge :: Bool -> SBool -> Mostek -> Mostek -> Mostek Source # select :: (Ord b, SymVal b, Num b) => [Mostek] -> Mostek -> SBV b -> Mostek Source #
type Rep Mostek Source # |

Instance details

Defined in Documentation.SBV.Examples.BitPrecise.Legato

type Rep Mostek = D1 ('MetaData "Mostek" "Documentation.SBV.Examples.BitPrecise.Legato" "sbv-10.2-H7C8tpOUfNc9yHFfX3krPk" 'False) (C1 ('MetaCons "Mostek" 'PrefixI 'True) (S1 ('MetaSel ('Just "memory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Memory) :*: (S1 ('MetaSel ('Just "registers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Registers) :*: S1 ('MetaSel ('Just "flags") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Flags))))

type Extract a = Mostek -> a Source #

Given a machine state, compute a value out of it

type Program = Mostek -> Mostek Source #

Programs are essentially state transformers (on the machine state)

# Low-level operations

getReg :: Register -> Extract Value Source #

Get the value of a given register

setReg :: Register -> Value -> Program Source #

Set the value of a given register

getFlag :: Flag -> Extract Bit Source #

Get the value of a flag

setFlag :: Flag -> Bit -> Program Source #

Set the value of a flag

peek :: Location -> Extract Value Source #

Read memory

poke :: Location -> Value -> Program Source #

Write to memory

checkOverflow :: SWord 8 -> SWord 8 -> SBool -> SBool Source #

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`.

checkOverflowCorrect :: IO ThmResult Source #

Correctness theorem for our `checkOverflow` implementation.

We have:

    >>> checkOverflowCorrect
    Q.E.D.

# Instruction set

type Instruction = Program -> Program Source #

An instruction is modeled as a `Program` transformer. We model mostek programs in direct continuation passing style.

ldx :: Value -> Instruction Source #

LDX: Set register `X` to value `v`

lda :: Value -> Instruction Source #

LDA: Set register `A` to value `v`

clc :: Instruction Source #

CLC: Clear the carry flag

rorM :: Location -> Instruction Source #

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.

rorR :: Register -> Instruction Source #

ROR, register version: Same as `rorM`, except through register `r`.

bcc :: Program -> Instruction Source #

BCC: branch to label `l` if the carry flag is sFalse

adc :: Location -> Instruction Source #

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.

dex :: Instruction Source #

DEX: Decrement the value of register `X`

bne :: Program -> Instruction Source #

BNE: Branch if the zero-flag is sFalse

end :: Program Source #

The `end` combinator "stops" our program, providing the final continuation that does nothing.

# Legato's algorithm in Haskell/SBV

legato :: Program Source #

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.

# Verification interface

runLegato :: Mostek -> (Value, Value) Source #

Given values for F1 and F2, `runLegato` takes an arbitrary machine state `m` and returns the high and low bytes of the multiplication.

type InitVals = (Value, Value, Value, Value, Value, Bit, Bit) Source #

Helper synonym for capturing relevant bits of Mostek

initMachine :: InitVals -> Mostek Source #

Create an instance of the Mostek machine, initialized by the memory and the relevant values of the registers and the flags

legatoIsCorrect :: InitVals -> SBool Source #

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.

# Verification

correctnessTheorem :: IO ThmResult Source #

The correctness theorem.

# C Code generation

legatoInC :: IO () Source #

Generate a C program that implements Legato's algorithm automatically.