# Emina Torlak

## Lab 1: Getting Started with Solver-Aided Programming

The following exercises explore the concepts covered in Part 1 of the tutorial on solver-aided programming presented at CAV 2019.

### Warmup (solution)

Suppose that you are an app developer for a super low-power chip that achieves peak energy efficiency on programs with few or no branches. To build apps faster, you hire Ben Bitdiddle to create a library of efficient primitives for this chip, starting with a branch-free function that computes the absolute value of a 32-bit bitvector. Here is a reference implementation (specification) for this function in Rosette, using the built-in bitvector datatype:

#lang rosette

(define (abs-spec x)
(if (bvslt x (bv 0 32))
(bvneg x)
x))


Ben comes up with the following implementation that works on his test suite:

(define (abs-impl x)
(let* ([o1 (bvashr x (bv 31 32))]
[o3 (bvsub o2 o1)])
o3))

; zero, positive, negative ...
> (assert (equal? (abs-impl (bv #x00000000 32))
(abs-spec (bv #x00000000 32))))
> (assert (equal? (abs-impl (bv #x00000003 32))
(abs-spec (bv #x00000003 32))))
> (assert (equal? (abs-impl (bv #x80000000 32))
(abs-spec (bv #x80000000 32))))


Help review Ben’s code by answering the following questions. If a question requires you to modify his implementation in any way, do so on a fresh copy with a new name such as abs-impl-N where N is the question number.

• Does Ben’s implementation work on all 32-bit inputs? Use the verify query to check.

• The verifier will reveal that Ben’s implementation is buggy. Use debug to localize the fault found by the verifier (and remember to save your work to a file before invoking debug).

• Use synthesize to fix Ben’s implementation as suggested by the debugger. You can assume that if Ben has made an error, it is always of the same kind: using an arithmetic operator (such as addition or subtraction) instead of a bitwise operator that takes the same arguments. It is easiest to sketch this knowledge using the choose construct.

### Solving Sudoku (solution)

Rosette’s solve query implements a form of angelic execution. This idea dates back to a 1966 paper by Floyd who proposed it as an elegant way to hide the details of backtracking search behind a language construct he called choice.

Conceptually, the choice function non-determinstically chooses a value to return so that all subsequent assertions are satisfied.

For example, choice would pick the values #f and #t to execute the following program angelically:

#lang rosette

(define (choice type) ...) ; <-- implement choice

(define (more-or-less-1 x)
(if (choice boolean?)
(+ x 1)
(- x 1)))

(solve (assert (= 0 (more-or-less-1 1)))) ; #f
(solve (assert (= 2 (more-or-less-1 1)))) ; #t


Complete the above implementation of the choice function.

Now, consider the implementation of a checker for Sudoku solutions shown below: given a 9x9 Sudoku solution expressed a list of 81 integers, the check-sudoku procedure succeeds if and only if the solution satisfies the rules of Sudoku.

• Use your choice function, together with the solve query, to turn the Sudoku checker into a puzzle solver, and solve the puzzles p1-p4. Your sudoku-solve procedure should take as input a puzzle and produce a solution, if one exists, or return #f otherwise.

• Write a procedure valid-puzzle? that takes as input a puzzle and outputs #t if the puzzle has exactly one solution.

• How would you use valid-puzzle? to generate minimal Sudoku puzzles, which are valid (have a unique solution) but become invalid (have multiple solutions) if any of their filled cells are erased? Implement your idea if you have time.

; A puzzle is represented as a list of 81 digits,
; obtained by concatenating the rows of the puzzle,
; from first to last. This procedure takes as input
; a puzzle and checks that it satisfies the Sudoku rules.
(define (sudoku-check puzzle)
(for ([digit puzzle])             ; all digits between 1 and 9
(assert (and (<= 1 digit) (<= digit 9))))
(for ([row (rows puzzle)])        ; all different in a row
(assert (apply distinct? row)))
(for ([column (columns puzzle)])  ; all different in a column
(assert (apply distinct? column)))
(for ([region (regions puzzle)])  ; all different in a 3x3 region
(assert (apply distinct? region))))

(define (rows puzzle [n 9])
(if (null? puzzle)
null
(cons (take puzzle n)
(rows (drop puzzle n) n))))

(define (columns puzzle [n 9])
(if (null? puzzle)
(make-list n null)
(map cons
(take puzzle n)
(columns (drop puzzle n) n))))

(define (regions puzzle)
(define rows3 (curryr rows 3))
(define cols3 (curryr columns 3))
(map flatten
(append-map
append
(cols3
(append-map
rows3
(cols3
(append-map rows3 (rows puzzle))))))))

(define (char->digit c)
(- (char->integer c) (char->integer #\0)))

(define (string->puzzle p)
(map char->digit (string->list p)))

(define (show puzzle)
(pretty-print (rows puzzle)))

(define (solve-puzzle puzzle) ...)
(define (valid-puzzle? puzzle) ...)
(define (generate-puzzle) ...)

; Sample solved puzzle.
(define p0 (string->puzzle "693784512487512936125963874932651487568247391741398625319475268856129743274836159"))
; Sample unsolved puzzle where 0 represents unfilled cells.
(define p1 (string->puzzle "000000010400000000020000000000050604008000300001090000300400200050100000000807000"))

> (show p0)
'((6 9 3 7 8 4 5 1 2)
(4 8 7 5 1 2 9 3 6)
(1 2 5 9 6 3 8 7 4)
(9 3 2 6 5 1 4 8 7)
(5 6 8 2 4 7 3 9 1)
(7 4 1 3 9 8 6 2 5)
(3 1 9 4 7 5 2 6 8)
(8 5 6 1 2 9 7 4 3)
(2 7 4 8 3 6 1 5 9))
> (sudoku-check p0)
> (show p1)
'((0 0 0 0 0 0 0 1 0)
(4 0 0 0 0 0 0 0 0)
(0 2 0 0 0 0 0 0 0)
(0 0 0 0 5 0 6 0 4)
(0 0 8 0 0 0 3 0 0)
(0 0 1 0 9 0 0 0 0)
(3 0 0 4 0 0 2 0 0)
(0 5 0 1 0 0 0 0 0)
(0 0 0 8 0 7 0 0 0))
> (sudoku-check p1)
assert: failed


### Verifying a majority voting algorithm (solution)

The Boyer–Moore majority vote algorithm is a beautiful and tricky procedure for finding a majority element in a list, using linear time and constant space.

Complete the following Rosette implementation of Boyer-Moore and verify its correctness for any list of N arbitrary integers.

#lang rosette

(define (boyer-moore xs)
(define m ...)
(define i ...)
(for ([x xs])
(cond [...]
[...]
[else ...]))
m)

(define (check n [bw #f])
(current-bitwidth bw)
(define-symbolic* xs integer? [n])
...)

(time (check 10))