Ocelot: a solver for relational logic

7.7

top ← prev up next →

Ocelot: a solver for relational logic

James Bornholt <bornholt@cs.washington.edu>

package: ocelot

Ocelot provides an embedding of bounded relational logic in Rosette, a solver-aided programming language. Ocelot enables both verification and synthesis of relational logic expressions.

Ocelot’s flavor of bounded relational logic draws heavily on Alloy, so many concepts and examples from Alloy will also help in developing Ocelot programs.

1 Quick Start

Ocelot is best used with Rosette, so your file should begin:

#lang rosette

Using Ocelot involves first constructing a relational specification, then defining a scope in which to check the specification, and finally checking properties within that scope.

1.1 Constructing relational specifications

A relational logic specification consists of:

A universe of discourse
Declarations of relations
Constraints over those relations

1.1.1 Universe of discourse

A universe defines the set of atoms over which relations in a specification can range. All universes are finite. The universe constructor creates a new universe from a list of atoms.

Examples:

> (define U (universe '(a b c d)))
> (universe-atoms U)
'(a b c d)

1.1.2 Relation declarations

A relation declaration defines a new relation, whose value can later be constrained and then solved for. The declare-relation procedure creates a new relation of a given arity with a given name.

Examples:

> (define File (declare-relation 1 "File"))
> (define Dir (declare-relation 1 "Dir"))
> (define contents (declare-relation 2 "contents"))
> contents
(relation 2 "contents")

1.1.3 Constraints over relations

Ocelot offers a similar relational algebra to Alloy. Sentences in Ocelot can be either expressions (i.e., return a relation) or formulas (i.e., return a boolean).

Examples:

> (define DirsAndFiles (+ File Dir))
> (define nonEmptyDir (some (join Dir contents)))
> (define acyclic (no ([d Dir]) (in d (join d (^ contents)))))

1.2 Defining bounds on relations

By default, Ocelot requires explicit bounds on the possible relations. A bound for a relation consists of two sets of tuples: a lower bound defining tuples that must be in a relation, and an upper bound defining tuples that may be in a relation. A bounds instance is a list of bounds together with a universe of discourse.

Examples:

> (define bDir (make-exact-bound Dir '((a))))
> (define bFile (make-bound File '((b)) '((b) (c) (d))))
> (define bContents (make-product-bound contents '(a b c d) '(a b c d)))
> (define allBounds (bounds U (list bDir bFile bContents)))

1.3 Checking Relational Specifications

Finally, checking a relational specification involves interpreting the specification with respect to the bounds. The result is a Rosette expression, which can then be solved as normal.

The Ocelot interpreter translates Ocelot constraints into Rosette constraints with respect to a given bounds.

Solving the generated Rosette constraints with solve is similar to Alloy’s run command, while verifying the constraints with verify is similar to Alloy’s check.

Examples:

; There is a model in which a directory is non-empty
> (define formula1 (interpret nonEmptyDir allBounds))
> (define result1 (solve (assert formula1)))
> (sat? result1)
#t
; There is a counterexample to acyclicity
> (define formula2 (interpret acyclic allBounds))
> (define result2 (verify (assert formula2)))
> (sat? result2)
#t

2 Reference

Ocelot provides a language for constructing relational formulas, tools for defining possible values for those formulas, and an interpreter to reduce those formulas to Rosette terms.

2.1 Declaring Relations

procedure
(declare-relation arity name) → relation?
arity : natural-number/c
name : string?

Returns a new relation of the given arity and name.

2.2 Relational Logic

The Ocelot DSL embeds relational logic in Rosette. Many Ocelot operators (e.g., +) override their Rosette counterparts to also work over relations declared with declare-relation. These overridden operators should automatically fall back to their Rosette counterparts if their arguments are not relations. But this behavior can often be subtle, so only import the entire ocelot module when the enclosing context will not also be manipulating Rosette expressions.

2.2.1 Expressions

procedure
(+ a b ...) → node/expr?
a : node/expr?
b : node/expr?

Produces the union of two or more relations.

procedure
(& a b ...) → node/expr?
a : node/expr?
b : node/expr?

Produces the intersection of two or more relations.

procedure
(- a b ...) → node/expr?
a : node/expr?
b : node/expr?

Produces the first relation, but without any tuples present in the remaining relations (i.e., set difference).

(- a b c) is equivalent to (- (- a b) c).

procedure
(-> a b ...) → node/expr?
a : node/expr?
b : node/expr?

Produces the cross product of two or more relations.

procedure
(~ a) → node/expr?
a : node/expr?

Produces the inverse of a relation of arity 2.

If ⟨x,y⟩ is an element of a, then ⟨y,x⟩ is an element of (~ a).

procedure
(join a b ...) → node/expr?
a : node/expr?
b : node/expr?

Produces the relational join of two or more relations.

procedure
(<: a b) → node/expr?
a : node/expr?
b : node/expr?

Produces the relation containing all tuples in b whose first element is contained in a, which must have arity 1.

procedure
(:> a b) → node/expr?
a : node/expr?
b : node/expr?

Produces the relation containing all tuples in a whose last element is contained in b, which must have arity 1.

value
none : node/expr?

A relation of arity 1 that contains no tuples.

value
univ : node/expr?

A relation of arity 1 that contains the tuple ⟨x⟩ for every atom x in the universe.

value
iden : node/expr?

A relation of arity 2 that contains, for every atom x in the universe, the tuple ⟨x, x⟩.

iden is equivalent to (-> univ univ).

procedure
(^ expr) → node/expr?
expr : node/expr?

Produces the irreflexive transitive closure of a relation, which must have arity 2.

procedure
(* expr) → node/expr?
expr : node/expr?

Produces the reflexive transitive closure of a relation, which must have arity 2.

(* a) is equivalent to (+ (^ a) iden).

syntax
(set (decl ...) body-formula)

decl = [id domain-expr]

body-formula : node/formula?
domain-expr : (and/c node/expr? (equal? (node/expr/arity expr) 1))

Produces a set comprehension, which is a relation with arity equal to the number of decls provided. The set comprehension contains a tuple ⟨x1, ⋯, xn⟩ if and only if each xi is an element of the corresponding domain-expri (which must be an expression of arity 1) and, when each identifier idi is bound to the corresponding singleton tuple ⟨xi⟩, body-formula evaluates to true.

2.2.2 Formulas

procedure
(in a b) → node/formula?
a : node/expr?
b : node/expr?

Produces a formula that is true if and only if a is a subset of b.

procedure
(= a b) → node/formula?
a : node/expr?
b : node/expr?

Produces a formula that is true if and only if a and b contain the same elements.

procedure
(and a b ...) → node/formula?
a : node/formula?
b : node/formula?

Produces a formula that is true if and only if every input formula is true.

procedure
(or a b ...) → node/formula?
a : node/formula?
b : node/formula?

Produces a formula that is true if and only if at least one of the input formulas is true.

procedure
(=> a b) → node/formula?
a : node/formula?
b : node/formula?

Produces a formula that is true if and only if a implies b.

Equivalent to (or (! a) b).

procedure
(! f) → node/formula?
f : node/formula?
procedure
(not f) → node/formula?
f : node/formula?

Produces a formula that is true if and only if f is false.

2.2.3 Quantifiers and Multiplicities

Most quantifiers each come in two forms. One form takes no decls, and a body which is an expression, and evaluates to true if and only if the body has the appropriate cardinality. The second form takes decls, and a body which is a formula, and evaluate to true if and only if the number of bindings of the decls under which the body evaluates to true has the appropriate cardinality.

syntax
(all (decl ...) body-formula)

decl = [id domain-expr]

body-formula : node/formula?
domain-expr : (and/c node/expr? (equal? (node/expr/arity expr) 1))

Produces a formula that is true if and only if, for every binding of each id to a singleton subset of the corresponding domain-expr (which must be an expression of arity 1), body-formula-or-expr (which must be a formula) evaluates to true under that binding.

syntax
(some maybe-decls body-formula-or-expr)

maybe-decls =
| (decl ...)

decl = [id domain-expr]

body-formula-or-expr : (or/c node/formula? node/expr?)
domain-expr : (and/c node/expr? (equal? (node/expr/arity expr) 1))

If no decls are provided, produces a formula that is true if and only if body-formula-or-expr (which must be an expression) is not empty.

If decls are provided, produces a formula that is true if and only if there exists some binding of each id to a singleton subset of the corresponding domain-expr (which must be an expression of arity 1) such that body-formula-or-expr (which must be a formula) evaluates to true under that binding.

syntax
(no maybe-decls body-formula-or-expr)

maybe-decls =
| (decl ...)

decl = [id domain-expr]

body-formula-or-expr : (or/c node/formula? node/expr?)
domain-expr : (and/c node/expr? (equal? (node/expr/arity expr) 1))

If no decls are provided, produces a formula that is true if and only if body-formula-or-expr (which must be an expression) is empty.

If decls are provided, produces a formula that is true if and only if there exists no binding of each id to a singleton subset of the corresponding domain-expr (which must be an expression of arity 1) such that body-formula-or-expr (which must be a formula) evaluates to true under that binding.

In both cases, (no ...) is equivalent to the negation (! (some ...)).

syntax
(one maybe-decls body-formula-or-expr)

maybe-decls =
| (decl ...)

decl = [id domain-expr]

body-formula-or-expr : (or/c node/formula? node/expr?)
domain-expr : (and/c node/expr? (equal? (node/expr/arity expr) 1))

If no decls are provided, produces a formula that is true if and only if body-formula-or-expr (which must be an expression) contains exactly one tuple.

If decls are provided, produces a formula that is true if and only if there exists exactly one binding of the ids to a singleton subset of the corresponding domain-exprs (which must be expressions of arity 1) such that body-formula-or-expr (which must be a formula) evaluates to true under that binding.

syntax
(lone maybe-decls body-formula-or-expr)

maybe-decls =
| (decl ...)

decl = [id domain-expr]

body-formula-or-expr : (or/c node/formula? node/expr?)
domain-expr : (and/c node/expr? (equal? (node/expr/arity expr) 1))

If no decls are provided, produces a formula that is true if and only if body-formula-or-expr (which must be an expression) contains at most one tuple.

If decls are provided, produces a formula that is true if and only if there exists at most one binding of the ids to a singleton subset of the corresponding domain-exprs (which must be expressions of arity 1) such that body-formula-or-expr (which must be a formula) evaluates to true under that binding.

In both cases, (lone ...) is equivalent to the disjunction (or (no ...) (one ...)).

2.3 Scopes

Ocelot interprets relational expressions with respect to a set of bounds, which constrain the possible values of relations. The bounds, in turn, consist of tuples drawn from a universe of discourse.

2.3.1 Universes

procedure
(universe atoms) → universe?
atoms : (listof symbol?)

Creates a new universe with the given atoms.

procedure
(universe-atoms universe) → (listof symbol?)
universe : universe?

Returns the atoms for a given universe.

2.3.2 Bounds

procedure
(make-bound relation lower upper) → bound?
  relation : relation?
  lower : (listof (listof symbol?))
  upper : (listof (listof symbol?))

Create a new bound for relation that constrains it to always contain every tuple in lower, and only contain tuples in upper. Both lower and upper must be lists of tuples, where a tuple is a list of atoms and has the same length as the arity of relation.

procedure
(make-exact-bound relation contents) → bound?
relation : relation?
contents : (listof (listof symbol?))

Create a new bound for relation that constrains it to contain exactly the tuples in contents.

Equivalent to (make-bound relation contents contents).

procedure
(make-upper-bound relation contents) → bound?
relation : relation?
contents : (listof (listof symbol?))

Create a new bound for relation that constrains it to contain only the tuples in contents.

Equivalent to (make-bound relation '() contents).

procedure
(make-product-bound relation atoms ...) → bound?
relation : relation?
atoms : (listof symbol?)

Create a new bound for relation that constrains it to contain only the tuples in the cartesian product of the atoms. relation must have the same arity as the number of atoms.

Equivalent to (make-upper-bound relation (cartesian-product atoms ...)).

procedure
(bounds universe bnds) → bounds?
universe : universe?
bnds : (listof bound?)

Collect a set of relation bounds and a universe together for use by interpret.

procedure
(bounds? a) → boolean?
a : any/c

Return true if and only if a is an instance of bounds.

2.4 Solving

Ocelot compiles relational formulas to Rosette constraints, which can then be used directly with Rosette’s solving and verification features.

procedure
(interpret formula bounds) → term?
formula : node/formula?
bounds : bounds?

Translate formula into a Rosette formula that is satisfiable if and only if there exists a binding to each relation in bounds that satisfies its resepctive upper and lower bound such that formula evaluates to true under that binding.

The bounds must provide a bound for every free relation mentioned in formula.

procedure
(interpret* formula interp) → term?
formula : node/formula?
interp : interpretation?

Like interpret, but takes as input an interpretation instead of bounds.

interpret*, together with instantiate-bounds and interpretation->relations, are useful for lifting the results of a satisfiable Rosette query to a model for relations (see Interpretations below).

The interpretation must provide an interpretation for every free relation mentioned in formula.

2.4.1 Interpretations

Ocelot reduces relational formulas to boolean formulas by way of interpretations, which assign boolean variables for the presence of each possible tuple in a relation. Interpretations can be used to list a satisfying model from a Rosette query back to the relations that defined the solved formula.

procedure
(instantiate-bounds bounds) → interpretation?
bounds : bounds?

Create an interpretation for each relation bound by bounds. An inteerpretation of a relation a is a set of boolean variables, one for each potential tuple in the relation, that are true if and only if the corresponding tuple is present in a.

procedure
(interpretation->relations interp)
→ (hash/c relation? (listof (listof symbol?)))
interp : interpretation?

Returns a hash table that maps each relation bound by interp to a list of tuples contained in that relation under the interpretation interp.

interp must be fully concrete (contains no symbolic boolean variables).

Examples:

; Declare a cats relation and create an interpretation for it
> (define cats (declare-relation 1 "cats"))
> (define bCats (make-upper-bound cats '((a) (b) (c) (d))))
> (define allCatBounds (bounds U (list bCats)))
> (define iCats (instantiate-bounds allCatBounds))
; Find an interesting model for the cats relation
> (define F (and (some cats) (some (- univ cats))))
> (define resultCats (solve (assert (interpret* F iCats))))
> (sat? resultCats)
#t
; Lift the model to lists of tuples for each relation
> (define catsModel (interpretation->relations (evaluate iCats resultCats)))
> (hash-ref catsModel cats)
'((b))

2.5 Sketching and Synthesis

procedure
(expression-sketch depth
arity
operators
terminals) → node/expr?
  depth : natural-number/c
  arity : natural-number/c
  operators : (listof procedure?)
  terminals : (listof node/expr?)

Constructs an expression sketch, which is an unknown relational expression. Possible completions of the expression sketch are all relational expressions of arity arity whose AST is depth levels deep, with leaf nodes drawn from terminals and non-leaf nodes drawn from operators.

top ← prev up next →