To install Rosette, please read the instructions at http://cs.brown.edu/courses/cs195y/2017/software.html
Z3 is the default SMT solver that powers Rosette. In this assignment, you will learn how to use Z3 (via Rosette) to solve or verify constraints.
Three positive integers (x, y, z) such that x^2 + y^2 = z^2 form a Pythagorean triple. Euclid's formula produces Pythageorean triples: given integers m and n such that m > n > 0, (m^2 - n^2, 2mn, m^2 + n^2) yields a Pythagorean triple.
Write a function part1 to verify Euclid's formula. Although this problem involves non-linear arithmetic, Z3 is able to make headway and prove Euclid's formula correct. Unlike Alloy which checks within the specified bounds, Z3 checks over all mathematical integers.
Write a function part2 to check whether Euclid's formula can produce non-primitive triples. A triple (x, y, z) is primitive if and only if x, y, and z share no common factors (other than 1).
In the template below, you should replace ... with constraints or symbol declarations, or remove it entirely if you wish. Note that with-asserts in the template will prevent assertions in part 1 from interfering with those in part 2 and vice versa. Thus, any shared assertions should be in the global section.
Although Rosette provides a lot of ways to solve or verify constraints, all of them are built on top of Z3's solve command. To mimic Z3's functionality, we only permit you to use solve in the most basic form (with no keyword argument like #:assume).
Because solve returns either an unsat or a model, you need to define part1-interp and part2-interp to indicate how to interpret the result from part1 and part2 respectively. See the template for more information.
To find a remainder of integer division, you can use %.
You should not modify the template except for the ... as that could cause the autograder to fail.
#lang rosette/safe
(current-bitwidth #f)
(define % remainder)
; variables for Euclid's formula
(define-symbolic m integer?)
(define-symbolic n integer?)
; variables for Pythagorean triple
(define-symbolic x integer?)
(define-symbolic y integer?)
(define-symbolic z integer?)
;; DO NOT MODIFY ABOVE THIS LINE
; global section: add assertions across Part 1 and Part 2 here
(assert ...)
; end assertions across Part 1 and Part 2
(define (part1)
; add assertions and/or declare additional symbols
; for part1 here
(assert ...)
; end assertions for part1
; write down a formula for verification
(solve (assert ...)))
; replace ... in `part1-interp` with
; - `sat?` if `solve` in `part1` returning a model means the formula works
; - `unsat?` if `solve` in `part1` returning unsat means the formula works
(define part1-interp ...)
(define (part2)
; add assertions and/or declare additional symbols
; for part2 here
(assert ...)
; end assertions for part2
; write down a formula to test the hypothesis
(solve (assert ...)))
; replace ... in `part2-interp` with
; - `sat?` if `solve` in `part2` returning a model means
; it can produce non-primitive
; - `unsat?` if `solve` in `part2` returning unsat means
; it can produce non-primitive
(define part2-interp ...)
;; DO NOT MODIFY BELOW THIS LINE
(define-values (part1-val _1) (with-asserts (part1)))
(define-values (part2-val _2) (with-asserts (part2)))
(printf "According to your interpretation\n")
; expect to see yes and yes
(printf "Part 1: ~a, Formula works?: ~a\n"
part1-val (if (part1-interp part1-val) "yes" "no"))
(printf "Part 2: ~a, Can produce non-primitive?: ~a\n"
part2-val (if (part2-interp part2-val) "yes" "no"))
Following is a pseudocode for a binary search algorithm to find an index of a given element, and return -1 if the element is not found.
def bsearch(A, x):
ans = -1
l = 0
r = len(A) - 1
while l <= r and ans == -1:
m = (l + r) / 2
if A[m] == x:
ans = m
elif A[m] < x:
l = m + 1
elif A[m] > x:
r = m - 1
return ans
We will verify that the algorithm is indeed correct.
In Alloy, to verify correctness of a system with several states (and transitions/events), we use the event idiom. The advantage is that we can see concrete state transitions. The disadvantage is that, as there are more events, the number of variables increase, so Alloy takes more time.
Another approach which we will use here is to use loop invariant (or induction if you will). Instead of talking about a sequence of transitions (and states), we will look at only one transition abstractly. This greatly reduces the verification time and allows us to verify a system with larger states (you can see that we can set the length of the vector to 50 and the verification will still take only a few seconds).
An invariant is a property which holds in every "possible" state. By "possible", we mean the state that can happen. Not every state is possible. As an example, in the binary search algorithm, it is impossible that the variable ans will be -2 in any state that can happen in the algorithm.
To be precise, let next(s) be the next state of a state s (in the context of the binary search algorithm, the function next is a transition function that consumes a before-an-iteration state and produces an after-an-iteration state). The definition of the possible state is the following:
s is a possible state where the next state is defined, then next(s) is also a possible state.Therefore, to show that the invariant holds in every possible state, we need to show that:
s, then the invariant holds for next(s) if next is defined for s. In other words, next preserves the invariant.There are several valid invariants. If our algorithm is not buggy and will eventually terminate, then there is a last state. What we are interested in is an invariant that is "expressive" enough to let us conclude the correctness of the system from the last state. The function invariant-hold? in file runner.rkt demonstrates such invariant.
If the algorithm is buggy and next causes an infinite loop, then there would be no last state that can be used to verify the correctness of the system. Therefore, we need to make sure that the algorithm terminates.
Termination analysis usually defines a function called measure which consumes a possible state and produces a natural number. Intuitively, this function measures how close the a possible state is from termination (that is the last state). We require that measure is a strictly decreasing function and produces 0 for the state that next is not defined (that is the last state). If we can define such function, then we have a proof that the algorithm terminates because initially, we have the measure being that of the initial state. Then, for each iteration, the measure will keep decreasing, but it could not go past 0 as we require that the measure returns only a natural (non-negative) number. So it must be the case that the last measure is 0 from the last state, proving the termination.
With the definition of measure, we can refine verification (b) to:
s and measure(s) > 0, then the invariant holds for next(s).Regarding the measure, we need to verify that:
s where the invariant holds is greater than 0, then the measure of next(s) is less that that.Lastly, we want to make sure that the last state implies the correctness of the system. That is,
s such that measure(s) = 0 and the invariant holds, we have that the system is correct.We are providing a framework for verifying correctness of the binary search algorithm and a correct implementation of the algorithm. Your job is to write 5 different implementations of binary search such that each implementation breaks exactly one verification (there are 5 verifications). You will not receive a full credit for any implementation that breaks more than one verification.
The following files can be downloaded at /course/cs1950y/src/rosette-bsearch
runner.rkt: This is the main file. You should run it to verify against an implementation. This is also the file that you need to read to understand the framework in detail. Only edit the require statement of this file to run against implementations and do not edit anywhere else.bsearch0.rkt: This file contains components of the correct implementation:
next defines what the next state should be for each iteration of the algorithm.measure is also used in the algorithm as a terminating conditioninitial-state defines the initial state.bsearch1.rkt, bsearch2.rkt, ..., bsearch5.rkt and edit these 3 functions in each file.bsearch-definitions.rkt: This file contains the declaration of a state shared across runner.rkt and the implementation. Feel free to read it, but you must not edit this file.cs1950y.rkt: This file contains utility functions. You must not edit this file, and you should not need to read it, as it is beyond the scope of the course.Running runner.rkt against your files should take no more than 15 seconds per file.
Run cs1950y_handin rosette from a directory holding your Rosette files (pythagorean.rkt, bsearch1.rkt, bsearch2.rkt, bsearch3.rkt, bsearch4.rkt, bsearch5.rkt). You should receive an email confirming that your handin has worked.
Following is a rough explanation of functions/forms used in Problem 2 that is not covered in the Racket tutorial that we provided.
(set! <id> <val>): set <id> to <val>. This is like <id> = <val> or <id> := <val> in some well-known programming languages.
(struct ... #:transparent) is like (define-struct ...) from the tutorial (this is used in bsearch-definitions.rkt and not files that you need to edit)
(define-match (<function-name> (<struct-name> <id-1> ... <id-n>)) <body>): this is a shorthand for:
(define (<function-name> s)
(define <id_1> (<struct-name-field-1> s))
...
(define <id_n> (<struct-name-field-n> s))
<body>)
In short, it's a way to obtain all fields of a struct in one go. Please notice that the function defined by define-match in fact accepts only one argument.
define-match is provided by us; Racket itself doesn't have this form.