Lab 2: Going Pro with SolverAided Programming
The following exercises explore the concepts covered in Part 2 of the tutorial on solveraided programming presented at CAV 2019.
A shallow circuit SDSL
Consider the problem of building a simple language for testing, verifying, and synthesizing boolean circuits. We are interested in circuit programs that are in static single assignment (SSA) form, and that use one of the following operations: Not, And, Or, Iff, and Xor, with their usual meaning.
Here is what a shallow embedding of this language would look like in Rosette:
#lang rosette
(define (Not a) (if a #f #t))
(define (And a b) (if a b #f))
(define (Or a b) (if a #t b))
(define (Iff a b) (if a b (! b)))
(define (Xor a b) (if a (! b) b))
And here are a few programs in this language:
(define (Niffp a b c d)
(define r1 (Iff a b))
(define r2 (Iff c d))
(define r3 (Iff r1 r2))
(define r4 (Not r3))
r4)
(define (NXp a b c d)
(define r1 (Xor a b))
(define r2 (Not r1))
(define r3 (Xor c d))
(define r4 (Not r3))
(define r5 (Xor r2 r4))
r5)
(define (AIGp a b c d)
(define r1 (Not a))
(define r2 (Not b))
(define r3 (And r1 r2))
(define r4 (Not r3))
(define r5 (And a b))
(define r6 (Not r5))
(define r7 (And r4 r6))
(define r8 (Not r7))
(define r9 (Not c))
(define r10 (Not d))
(define r11 (And r9 r10))
(define r12 (Not r11))
(define r13 (And c d))
(define r14 (Not r13))
(define r15 (And r12 r14))
(define r16 (Not r15))
(define r17 (Not r8))
(define r18 (Not r16))
(define r19 (And r17 r18))
(define r20 (Not r19))
(define r21 (And r8 r16))
(define r22 (Not r21))
(define r23 (And r20 r22))
(define r24 (Not r23))
(define r25 (Not r24))
r25)

Define a procedure
(ver impl spec)
that takes as input an implementation and a specification circuit, and checks that they produce the same output on all inputs. If not,ver
should return a counterexample; otherwise, it should return#f
. 
Use
ver
to check ifNIffp
andNXp
programs are equivalent. 
Use definesynthax to define a hole
(??inst arg ...)
that will select some instruction from the circuit language and apply it to the given arguments. 
Define a procedure
(syn impl spec)
that takes as input an implementation with holes and completes it (if possible) to satisfy the specification. Thesyn
procedure should return the synthesized code (hint, use generateforms to extract the code from a model), or#f
if no model exists. 
Use
??inst
andsyn
to synthesize the shortest possible implementation ofAIGp
.
A deep circuit SDSL
The above exercise show that a shallow embedding makes it cumbersome to specify sketches of arbitrary length. In general, it’s a good rule of thumb to use deep embedding if you want to do synthesis; shallow embedding works well for verification and solving.
Let’s build a deep embedding of the circuit SDSL, reusing the semantics of the circuit operations we defined in the previous part of the lab.
To do so, add the following line to the module containing your shallow embedding and save it as, say, “shallow.rkt”:
#lang rosette
(provide Not And Or Xor Iff ver syn ??inst)
...
Now, create a file “deep.rkt” that imports the shallow semantic operations, but prefixes each operation’s name with “s” (for “shallow” or “semantics”), so that we can reuse the original names in the new implementation:
#lang rosette
(require
rosette/lib/match
(prefixin s (onlyin "shallow.rkt" Not And Or Iff Xor)))
(struct Not (a) #:transparent)
(struct And (a b) #:transparent)
(struct Or (a b) #:transparent)
(struct Iff (a b) #:transparent)
(struct Xor (a b) #:transparent)
(define (interpret prog in)
(define reg (makevector (+ (car prog) (length (cdr prog))) #f))
(define (store i v) (vectorset! reg i v))
(define (load i) (vectorref reg i))
(define (last) (sub1 (vectorlength reg)))
(for ([(i idx) (inindexed in)])
(store idx i))
(for ([(inst idx) (inindexed (cdr prog))])
(store
(+ idx (car prog))
(match inst
[(Not a) (sNot (load a))]
[(And a b) (sAnd (load a) (load b))]
[(Or a b) (sOr (load a) (load b))]
[(Xor a b) (sXor (load a) (load b))]
[(Iff a b) (sIff (load a) (load b))])))
(load (last)))
Circuit programs are now represented as a list where the first element is the number of arguments to the program, and the remaining elements are instructions. Each instruction’s fields are integers that identify the registers containing the instruction’s inputs. For example:
(define NXp
(list 4 (Xor 0 1) (Not 4) (Xor 2 3) (Not 6) (Xor 5 7)))
(define Niffp
(list 4 (Iff 0 1) (Iff 2 3) (Iff 4 5) (Not 6)))

Define a procedure
(ver impl spec)
that takes as input an implementation and a specification circuit, and checks that they produce the same output on all inputs. If not,ver
should return a counterexample; otherwise, it should return#f
. 
Use
ver
to check if the two example programs are equivalent.  Complete the following definition of the sketch procedure so that it returns a symbolic ciricut program with
n
inputs andk
instructions:(define sketch (caselambda [(n k) (sketch n k Not And Or Xor Iff)] [(n k . insts) ...]))

Define a procedure
(syn impl spec)
that takes as input an implementation with holes and completes it (if possible) to satisfy the specification. Thesyn
procedure should return the synthesized program (hint, use evaluate to extract the code from a model), or#f
if no model exists.  Use
sketch
andsyn
to build a superoptimizer, and applysuperopt
to automatically synthesize the shortest possible implementation ofNXp
. Specifically,superopt
should take as input a specification circuit and produce the shortest equivalent circuit.