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.Puzzles.AOC_2021_24

Contents

- Registers, values, and the ALU
- Operations
- Running a program
- Solving the puzzle

Description

A solution to the advent-of-code problem, 2021, day 24: http://adventofcode.com/2021/day/24.

Here is a high-level summary: We are essentially modeling the ALU of a fictional computer with 4 integer registers (w, x, y, z), and 6 instructions (inp, add, mul, div, mod, eql). You are given a program (hilariously called "monad"), and your goal is to figure out what the maximum and minimum inputs you can provide to this program such that when it runs register z ends up with the value 1. Please refer to the above link for the full description.

While there are multiple ways to solve this problem in SBV, the solution here demonstrates how to turn programs in this fictional language into actual Haskell/SBV programs, i.e., developing a little EDSL (embedded domain-specific language) for it. Hopefully this should provide a template for other similar programs.

Synopsis

- type Register = String
- type Value = SInt64
- data Data
  - = Reg {
    - register :: Register
    }
  - | Imm Int64
- w :: Data
- x :: Data
- y :: Data
- z :: Data
- data State = State {
  - env :: Map Register Value
  - inputs :: [Value]
  }
- type ALU = StateT State Symbolic
- read :: Data -> ALU Value
- write :: Data -> Value -> ALU ()
- inp :: Data -> ALU ()
- add :: Data -> Data -> ALU ()
- mul :: Data -> Data -> ALU ()
- div :: Data -> Data -> ALU ()
- mod :: Data -> Data -> ALU ()
- eql :: Data -> Data -> ALU ()
- run :: ALU () -> Symbolic State
- puzzle :: Bool -> IO ()
- monad :: ALU ()

# Registers, values, and the ALU

type Register = String Source #

A Register in the machine, identified by its name.

type Value = SInt64 Source #

We operate on 64-bit signed integers. It is also possible to use the unbounded integers here as the problem description doesn't mention any size limitations. But performance isn't as good with unbounded integers, and 64-bit signed bit-vectors seem to fit the bill just fine, much like any other modern processor these days.

data Data Source #

An item of data to be processed. We can either be referring to a named register, or an immediate value.

Constructors

Reg |

Fields

- register :: Register

Imm Int64 |

#### Instances

Instances details

Num Data Source # | `Num` instance for `Data`. This is merely there for us to be able to represent programs in a natural way, i.e, lifting integers (positive and negative). Other methods are neither implemented nor needed.
Instance details Defined in Documentation.SBV.Examples.Puzzles.AOC_2021_24 Methods (+) :: Data -> Data -> Data Source # (-) :: Data -> Data -> Data Source # (*) :: Data -> Data -> Data Source # negate :: Data -> Data Source # abs :: Data -> Data Source # signum :: Data -> Data Source # fromInteger :: Integer -> Data Source #

w :: Data Source #

Shorthand for the `w` register.

x :: Data Source #

Shorthand for the `x` register.

y :: Data Source #

Shorthand for the `y` register.

z :: Data Source #

Shorthand for the `z` register.

data State Source #

The state of the machine. We keep track of the data values, along with the input parameters.

Constructors

State |

Fields

- env :: Map Register Value

  Values of registers

- inputs :: [Value]

  Input parameters, stored in reverse.

type ALU = StateT State Symbolic Source #

The ALU is simply a state transformer, manipulating the state, wrapped around SBV's `Symbolic` monad.

# Operations

read :: Data -> ALU Value Source #

Reading a value. For a register, we simply look it up in the environment. For an immediate, we simply return it.

write :: Data -> Value -> ALU () Source #

Writing a value. We update the registers.

inp :: Data -> ALU () Source #

Reading an input value. In this version, we simply write a free symbolic value to the specified register, and keep track of the inputs explicitly.

add :: Data -> Data -> ALU () Source #

Addition.

mul :: Data -> Data -> ALU () Source #

Multiplication.

div :: Data -> Data -> ALU () Source #

Division.

mod :: Data -> Data -> ALU () Source #

Modulus.

eql :: Data -> Data -> ALU () Source #

Equality.

# Running a program

run :: ALU () -> Symbolic State Source #

Run a given program, returning the final state. We simply start with the initial environment mapping all registers to zero, as specified in the problem specification.

# Solving the puzzle

puzzle :: Bool -> IO () Source #

We simply run the `monad` program, and specify the constraints at the end. We take a boolean as a parameter, choosing whether we want to minimize or maximize the model-number. Note that this test takes rather long to run. We get:

    ghci> puzzle True
    Optimal model:
      Maximum model number = 96918996924991 :: Int64
    ghci> puzzle False
    Optimal model:
      Minimum model number = 91811241911641 :: Int64

monad :: ALU () Source #

The program we need to crack. Note that different users get different programs on the Advent-Of-Code site, so this is simply one example. You can simply cut-and-paste your version instead. (Don't forget the pragma `NegativeLiterals` to GHC so `add x -1` parses correctly as `add x (-1)`.)