sbv-0.9.6: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Portability portable experimental erkokl@gmail.com

Data.SBV.Examples.BitPrecise.Legato

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 :       CLC            ; set C to 0
step4 : LOOP  ROR F1         ; rotate F1 right circular through C
step5 :       BCC ZCOEF      ; branch to ZCOEF if C = 0
step6 :       CLC            ; set C to 0
step7 :       ADC F2         ; set A to A+F2+C and C to the carry
step8 : ZCOEF ROR A          ; rotate A right circular through C
step9 :       ROR LOW        ; rotate LOW right circular through C
step10:       DEX            ; set X to X-1
step11:       BNE LOOP       ; branch to LOOP if Z = 0
```

NB. The CLC in step3 was later added by Warren Hunt; the original spec did not include this statement. However, without this addition, the algorithm does not work correctly for all starting states, so we adopt this change as well.

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

type Address = SWord32Source

The memory is addressed by 32-bit words.

data Register Source

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

Constructors

 RegX RegA

Instances

 Bounded Register Enum Register Eq Register Ord Register Ix Register

data Flag Source

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

Constructors

 FlagC FlagZ

Instances

 Bounded Flag Enum Flag Eq Flag Ord Flag Ix Flag

type Value = SWord8Source

Mostek was an 8-bit machine.

type Bit = SBoolSource

Convenient synonym for symbolic machine bits.

Register bank

Flag bank

The memory maps 32-bit words to 8-bit words. (The `Model` data-type is defined later, depending on the verification model used.)

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!)

Constructors

 Mostek Fieldsmemory :: Memory registers :: Registers flags :: Flags

Instances

 Mergeable Mostek

type Extract a = Mostek -> aSource

Given a machine state, compute a value out of it

type Program = Mostek -> MostekSource

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

# 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 false

ADC: Increment the value of register `A` by the value of memory contents at address `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 false

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

# Legato's algorithm in Haskell/SBV

Parameterized by the addresses of locations of the factors (`F1` and `F2`), the following program multiplies them, storing the low-byte of the result in the memory location `lowAddr`, and the high-byte in register `A`. The implementation is a direct transliteration of Legato's algorithm given at the top, using our notation.

# Verification interface

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

Given address/value pairs for F1 and F2, and the location of where the low-byte of the result should go, `runLegato` takes an arbitrary machine state `m` and returns the high and low bytes of the multiplication.

type InitVals = (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

legatoIsCorrect :: Memory -> (Address, Value) -> (Address, Value) -> Address -> InitVals -> SBoolSource

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

type Model = SFunArraySource

Choose the appropriate array model to be used for modeling the memory. (See `Memory`.) The `SFunArray` is the function based model. `SArray` is the SMT-Lib array's based model.

The correctness theorem. On a decent MacBook Pro, this proof takes about 30 seconds with `SFunArray` memory model above and about 30 minutes with the `SArray` memory model