Rosette Learning Notes

Excerpts from The Rosette Guide.

Rosette Essentials

Symbolic Values

(define-symbolic b boolean?)

Specification

(define (check-mid impl lo hi)     ; Assuming that
  (assume (bvsle (int32 0) lo))    ; 0 ≤ lo and
  (assume (bvsle lo hi))           ; lo ≤ hi,
  (define mi (impl lo hi))         ; and letting mi = impl(lo, hi) and
  (define diff                     ; diff = (hi - mi) - (mi - lo),
    (bvsub (bvsub hi mi)
           (bvsub mi lo)))         ; we require that
  (assert (bvsle lo mi))           ; lo ≤ mi,
  (assert (bvsle mi hi))           ; mi ≤ hi,
  (assert (bvsle (int32 0) diff))  ; 0 ≤ diff, and
  (assert (bvsle diff (int32 1)))) ; diff ≤ 1.

Verification

(define-symbolic l h int32?)

(define cex (verify (check-mid bvmid l h)))

Synthesis

Grammar:

(require rosette/lib/synthax)     ; Require the sketching library.
(define-grammar (fast-int32 x y)  ; Grammar of int32 expressions over two inputs:
  [expr
   (choose x y (?? int32?)        ; <expr> := x | y | <32-bit integer constant> |
           ((bop) (expr) (expr))  ;           (<bop> <expr> <expr>) |
           ((uop) (expr)))]       ;           (<uop> <expr>)
  [bop
   (choose bvadd bvsub bvand      ; <bop>  := bvadd  | bvsub | bvand |
           bvor bvxor bvshl       ;           bvor   | bvxor | bvshl |
           bvlshr bvashr)]        ;           bvlshr | bvashr
  [uop
   (choose bvneg bvnot)])         ; <uop>  := bvneg | bvnot

syntactic sugar:

• (?? int32?): (let () (define-symbolic id int32?) id)
• (choose bvneg bvnot): (if (?? boolean?) bvneg bvnot)

synthesize:

(define sol
    (synthesize
     #:forall    (list l h)
     #:guarantee (check-mid bvmid-fast l h)))

(print-forms sol)

Angelic Execution

(define (bvmid-fast lo hi)
    (bvlshr (bvadd hi lo) (bv 1 32)))
(define sol
    (solve
    (begin
        (assume (not (equal? l h)))
        (assume (bvsle (int32 0) l))
        (assume (bvsle l h))
        (assert (equal? (bvand l h) (bvmid-fast l h))))))

Symbolic Reasoning

Reasoning Percision

(current-bitwidth 64)

With this setting, integers (and reals) are treated as infinite precision values during evaluation, but when solving queries, they are translated to bitvectors of length k for better performance.

Symbolic Evaluation

In general, recursion terminates under symbolic evaluation only when the stopping condition is reached with concrete values.

Syntactic Form

Symbolic Constants

define-symbolic:

define-symbolic*: creates a stream of distinct symbolic constants

Assertions and Assumptions

VC: track of all assertions and assumptions

Verification

(verify expr) searches for a model of the formula (vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q) ∧ ¬ (vc-asserts Q)
– P is the verification condition before the call to verify,
– Q is the verification condition generated by evaluating expr.

Synthesis

(synthesize input expr)

Angelic Execution

(solve expr) searches for a model of the formula (vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q) ∧ (vc-asserts Q)

(solve+) Returns a stateful procedure that uses a fresh solver? instance to incrementally solve a sequence of constraints.

> (define-symbolic x y integer?)
> (define inc (solve+))
> (inc (< x y))   ; Push (< x y) and solve.
(model
 [x 0]
 [y 1])
> (inc (> x 5))   ; Push (> x 5) and solve.
(model
 [x 6]
 [y 7])
> (inc (< y 4))   ; Push (< y 4) and solve.
(unsat)
> (inc 1)         ; Pop  (< y 4) and solve.
(model
 [x 6]
 [y 7])

Optimize

(define-symbolic x y integer?)
; This query maximizes x + y while ensuring that y - x < 1 whenever x < 2:
(optimize
   #:maximize (list (+ x y))
   #:guarantee
   (begin
     (assume (< x 2))
     (assert (< (- y x) 1))))