| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.BitPrecise.Legato
Contents
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
- data Flag
- type Value = SWord8
- type Bit = SBool
- type Registers = Array Register Value
- type Flags = Array Flag Bit
- data Location
- type Memory = Array Location Value
- data Mostek = Mostek {}
- 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 :: SWord8 -> SWord8 -> 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
We model only two registers of Mostek that is used in the above algorithm, can add more.
We have three memory locations, sufficient to model our problem
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.
Instances
| Generic Mostek # | |
| Mergeable Mostek # | |
| type Rep Mostek # | |
Defined in Documentation.SBV.Examples.BitPrecise.Legato type Rep Mostek = D1 (MetaData "Mostek" "Documentation.SBV.Examples.BitPrecise.Legato" "sbv-7.12-8x7q036bgmy9UKzt81fC7j" 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)))) | |
Low-level operations
checkOverflow :: SWord8 -> SWord8 -> SBool -> SBool #
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.
Instruction set
type Instruction = Program -> Program #
An instruction is modeled as a Program transformer. We model
mostek programs in direct continuation passing style.
ldx :: Value -> Instruction #
LDX: Set register X to value v
lda :: Value -> Instruction #
LDA: Set register A to value v
clc :: Instruction #
CLC: Clear the carry flag
rorM :: Location -> Instruction #
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 #
ROR, register version: Same as rorM, except through register r.
bcc :: Program -> Instruction #
BCC: branch to label l if the carry flag is false
adc :: Location -> Instruction #
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 #
DEX: Decrement the value of register X
bne :: Program -> Instruction #
BNE: Branch if the zero-flag is false
The end combinator "stops" our program, providing the final continuation
that does nothing.
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.
Verification interface
runLegato :: Mostek -> (Value, Value) #
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) #
Helper synonym for capturing relevant bits of Mostek
initMachine :: InitVals -> Mostek #
Create an instance of the Mostek machine, initialized by the memory and the relevant values of the registers and the flags
legatoIsCorrect :: InitVals -> SBool #
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 #
The correctness theorem.