Lecture 19: Finitizing, Rosette

1 Purpose

Explore Rosette, Go over HW6A

2 Outline

This day, we did a from-scratch solution to HW6A, modeling how one could approach it.

Afterwards, we showed how by using BoundedList, a contract that allows you to construct a list bounded by a certain length, you can invoke verify-contract on a property that otherwise could not be handled by SMT as it involves unbounded data.

For example, if you have:

(: my-prop (-> (List Integer) True))

(define (my-prop l)   (= (length l) (length (reverse l))))

If you try to run (verify-contract my-prop), this will fail, as unbounded data like Lists cannot be handled by SMT. However, we can handle Tuples, and more helpfully, we can handle BoundedLists, for some finite bound, e.g.:

(: my-prop-bounded (-> (BoundedList 5 Integer) True)) (define (my-prop-bounded l)   (= (length l) (length (reverse l)))) (verify-contract my-prop-bounded)

1 success(es) 0 failure(s) 0 error(s) 1 test(s) run

But a better approach than defining separate properties for the bounded version is to define a bounded version that just calls the unbounded one. Since the initial contract is the one that will drive the SMT query generation, the fact that the property it calls has a more permissive contract doesn’t matter! i.e., I can write:

(: my-prop-wrapper (-> (BoundedList 5 Integer) True)) (define (my-prop-wrapper l)   (my-prop l)) (verify-contract my-prop-wrapper)

1 success(es) 0 failure(s) 0 error(s) 1 test(s) run

And that way we can use check-contract, using normal random generation, on our original property, and then use whatever finitization that is necessary to enable verify-contract on the wrapper that calls the original property.

Which is what we did with HW6A.