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

Documentation.SBV.Examples.BitPrecise.Legato

Description

Author : 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.

Synopsis

# 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
 Source # Instance details Methods Source # Instance details Methods Source # Instance details Methods(<) :: Register -> Register -> Bool #(>) :: Register -> Register -> Bool # Source # Instance details Methodsrange :: (Register, Register) -> [Register] #index :: (Register, Register) -> Register -> Int #unsafeIndex :: (Register, Register) -> Register -> IntinRange :: (Register, Register) -> Register -> Bool #rangeSize :: (Register, Register) -> Int #unsafeRangeSize :: (Register, Register) -> Int

data Flag Source #

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

Constructors

 FlagC FlagZ
Instances
 Source # Instance details Methods Source # Instance details Methods(==) :: Flag -> Flag -> Bool #(/=) :: Flag -> Flag -> Bool # Source # Instance details Methodscompare :: Flag -> Flag -> Ordering #(<) :: Flag -> Flag -> Bool #(<=) :: Flag -> Flag -> Bool #(>) :: Flag -> Flag -> Bool #(>=) :: Flag -> Flag -> Bool #max :: Flag -> Flag -> Flag #min :: Flag -> Flag -> Flag # Source # Instance details Methodsrange :: (Flag, Flag) -> [Flag] #index :: (Flag, Flag) -> Flag -> Int #unsafeIndex :: (Flag, Flag) -> Flag -> IntinRange :: (Flag, Flag) -> Flag -> Bool #rangeSize :: (Flag, Flag) -> Int #unsafeRangeSize :: (Flag, Flag) -> Int

type Value = SWord8 Source #

Mostek was an 8-bit machine.

type Bit = SBool Source #

Convenient synonym for symbolic machine bits.

Register bank

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
 Source # Instance details Methods Source # Instance details Methods Source # Instance details Methods(<) :: Location -> Location -> Bool #(>) :: Location -> Location -> Bool # Source # Instance details Methodsrange :: (Location, Location) -> [Location] #index :: (Location, Location) -> Location -> Int #unsafeIndex :: (Location, Location) -> Location -> IntinRange :: (Location, Location) -> Location -> Bool #rangeSize :: (Location, Location) -> Int #unsafeRangeSize :: (Location, Location) -> Int

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 Fieldsmemory :: Memory registers :: Registers flags :: Flags
Instances
 Source # Instance details Associated Typestype Rep Mostek :: Type -> Type # Methodsfrom :: Mostek -> Rep Mostek x #to :: Rep Mostek x -> Mostek # Source # Instance details Methodsselect :: (SymVal b, Num b) => [Mostek] -> Mostek -> SBV b -> Mostek Source # type Rep Mostek Source # Instance details type Rep Mostek = D1 (MetaData "Mostek" "Documentation.SBV.Examples.BitPrecise.Legato" "sbv-8.0-4OZZzEgTRNf59WYE3yYwTJ" 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

Get the value of a given register

Set the value of a given register

Get the value of a flag

Set the value of a flag

Write to memory

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.

Correctness theorem for our checkOverflow implementation.

We have:

>>> checkOverflowCorrect
Q.E.D.


# Instruction set

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

LDX: Set register X to value v

LDA: Set register A to value v

CLC: Clear the carry flag

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.

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

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

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: Decrement the value of register X

BNE: Branch if the zero-flag is sFalse

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

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

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

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

The correctness theorem.

# C Code generation

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