﻿ Rosette Learning Notes – DOFY's Blog

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


DOFY's Blog

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 (ass…

2022-06-02