Ocelot: a solver for relational logic
(require ocelot) | 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.
> (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.
> (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).
> (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.
> (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.
; 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?
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?
procedure
(& a b ...) → node/expr?
a : node/expr? b : node/expr?
procedure
(- a b ...) → node/expr?
a : node/expr? b : node/expr?
(- a b c) is equivalent to (- (- a b) c).
procedure
(-> a b ...) → node/expr?
a : node/expr? b : node/expr?
procedure
(~ a) → node/expr?
a : node/expr?
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?
procedure
(<: a b) → node/expr?
a : node/expr? b : node/expr?
procedure
(:> a b) → node/expr?
a : node/expr? b : node/expr?
value
none : node/expr?
value
univ : node/expr?
value
iden : node/expr?
iden is equivalent to (-> univ univ).
procedure
(^ expr) → node/expr?
expr : node/expr?
procedure
(* expr) → node/expr?
expr : node/expr?
(* 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))
2.2.2 Formulas
procedure
(in a b) → node/formula?
a : node/expr? b : node/expr?
procedure
(= a b) → node/formula?
a : node/expr? b : node/expr?
procedure
(and a b ...) → node/formula?
a : node/formula? b : node/formula?
procedure
(or a b ...) → node/formula?
a : node/formula? b : node/formula?
procedure
(=> a b) → node/formula?
a : node/formula? b : node/formula?
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))
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 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 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 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 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?)
procedure
(universe-atoms universe) → (listof symbol?)
universe : universe?
2.3.2 Bounds
procedure
(make-bound relation lower upper) → bound?
relation : relation? lower : (listof (listof symbol?)) upper : (listof (listof symbol?))
procedure
(make-exact-bound relation contents) → bound?
relation : relation? contents : (listof (listof symbol?))
Equivalent to (make-bound relation contents contents).
procedure
(make-upper-bound relation contents) → bound?
relation : relation? contents : (listof (listof symbol?))
Equivalent to (make-bound relation '() contents).
procedure
(make-product-bound relation atoms ...) → bound?
relation : relation? atoms : (listof symbol?)
Equivalent to (make-upper-bound relation (cartesian-product atoms ...)).
procedure
(bounds? a) → boolean?
a : any/c
2.4 Solving
Ocelot compiles relational formulas to Rosette constraints, which can then be used directly with Rosette’s solving and verification features.
The bounds must provide a bound for every free relation mentioned in formula.
procedure
(interpret* formula interp) → term?
formula : node/formula? interp : interpretation?
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?
procedure
(interpretation->relations interp)
→ (hash/c relation? (listof (listof symbol?))) interp : interpretation?
interp must be fully concrete (contains no symbolic boolean variables).
; 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?)