Data Abstraction II

In preparation for class 15, in this reading we practice one of our core software-construction competencies:

• Hallucination in order to imagine a useful abstraction and plan to build on top of it before any implementation even exists.

In class, we will practice another:

• Deception in order to implement that elegant abstraction with a grungy bit of code that fools the rest of the modules in the program: they think they have access to values of some abstract type when in fact all they have are some cleverly arranged bits and code that knows how to manipulate those bits.

A simple theorem prover

We’d like to implement a little theorem prover that works with simple formulas that are conjunctions of equalities over variables. So our prover should be able to answer questions like

Here is how we will formulate the problem in Dafny:

type Variable = string
datatype Expr = Var(variable: Variable)
datatype Pred = Equal(op1: Expr, op2: Expr) | And(conj1: Pred, conj2: Pred)

predicate Implies(hypothesis: Pred, conclusion: Pred)

And here is our idea for how to implement Implies using some, let’s call it, unknown funkiness data structure UF:

1. Create an empty data structure: uf := UF.Empty().
2. Add assumptions. Walk through the hypothesis and for each Equal, record in the data structure that those two variables are equal: UF.AssertEqual(uf, op1.variable, op2.variable).
3. Check conclusions. Walk through the conclusion and for each Equal, check whether the data structure agrees that given the recorded equalities those two variables must be equal: UF.CheckEqual(uf, op1.variable, op2.variable).

Our unknown funkiness is keeping track of a partition of a set into disjoint subsets. Consider the set of all variables in the formula, grouped into subsets where variables known to be equal are grouped together. If we have no information about equality, then each variable is in its own subset of size one. But when the hypothesis equates a pair of variables, their subsets are merged: those two variables and any variables already known to be equal to them are part of the same disjoint subset. This data structure is called a union-find after its two key operations:

• union together (merge) the subsets that contain two elements (our AssertEqual), and
• find the subset for a given element (which gives us our CheckEqual).

While our simple theorem prover is a toy example, programming languages that support type inference will need to solve a similar problem of equating unknown types called unification in their compilers. The Rust compiler, for example, uses a union-find for unification.

The plan

Here is a sketch of the interface of the UnionFind module:

module UnionFind {
  export
    provides UnionFind, Empty, AssertEqual, CheckEqual

  type UnionFind<K(==)>
  function Empty<K>(): UnionFind<K>
  function AssertEqual<K>(uf: UnionFind<K>, u: K, v: K): UnionFind<K>
  predicate CheckEqual<K>(uf: UnionFind<K>, u: K, v: K)
}

Now that we understand how we hope to use UnionFind, the plan for the rest of this reading is to write specifications for UnionFind. There will be some subtlety to this specification problem, where we need to dig into a relatively advanced Dafny feature, to make this problem fit our model of a representation invariant and abstraction function per module that uses data abstraction. In class, we will implement UnionFind with a classic algorithm, prove it correct, and see how to go on to prove the theorem prover correct.

Specifying UnionFind with an abstraction function

A union-find structure is supposed to maintain a partition of a set. Recall above the type parameter K for keys, threaded through many definitions. It would be a nuisance to require K to be finite. For instance, our theorem prover wants to set K to string, a very natural choice for variables… partly because there are so many darned strings to choose from, so we shouldn’t ever run out! Keep in mind, then, that K could signify an infinite set.

As a preliminary, here are two handy definitions about functions and consequences of known equalities.

module Functions {
  // First, here is what it means for a function to agree with a set of
  // required equalities. (*)
  ghost predicate Compatible<K(!new)>(f: K -> nat, eqs: set<(K, K)>) {
    forall u, v :: (u, v) in eqs ==> f(u) == f(v)
  }

  // Next, here is what it means for a set of equalities to imply that two
  // keys are equal *under all compatible functions*.
  ghost predicate ImpliedEqual<K(!new)>(eqs: set<(K, K)>, u: K, v: K) {
    forall f :: Compatible(f, eqs) ==> f(u) == f(v)
  }
}

Now we can give a beautiful (if we may say so ourselves) interface for union-find, based on sets.

module UnionFindSetAF {
  import F = Functions
  
  type State<K>

  ghost predicate Valid<K(==)>(s : State<K>)
  function Empty<K(!new)>(): State<K>
    ensures Valid(Empty<K>())
  function AssertEqual<K(!new)>(s: State<K>, u: K, v: K): State<K>
    requires Valid(s)
    ensures Valid(AssertEqual(s, u, v))
  predicate CheckEqual<K(!new)>(s: State<K>, u: K, v: K)
    requires Valid(s)
    
  ghost function Abstr<K(!new)>(s: State<K>): set<(K, K)>
  // Definition TBD!  It acts like `Elements` in last class' examples.

  // How to extend a set of equalities with all logical consequences that follow
  // from them:
  ghost function Closure<K(!new)>(eqs: set<(K, K)>): set<(K, K)>
  {
    set a: K, b: K | F.ImpliedEqual(eqs, a, b) :: (a, b)
  }

  // Now we can express requirements on each operation cleanly in terms of
  // `Abstr`.
  
  lemma EmptyCorrect<K(!new)>()
    ensures Abstr(Empty<K>()) == Closure<K>({})

  lemma CheckEqualCorrect<K(!new)>(s: State<K>, u: K, v: K)
    requires Valid(s)
    ensures CheckEqual(s, u, v) == ((u, v) in Abstr(s))

  lemma AssertEqualCorrect<K(!new)>(s: State<K>, u: K, v: K)
    requires Valid(s)
    ensures Abstr(AssertEqual(s, u, v)) == Closure(Abstr(s) + {(u, v)})
}

There’s only one problem: Dafny set is for finite sets only, and Abstr returns infinite sets!

How to get around the finiteness limitation? Up to any point in a program using union-find, only finitely many keys have been passed as function arguments. Let’s track that set at the specification level and simply disallow queries that step outside the set (those queries aren’t very interesting, anyway).

module UnionFindSetAF {
  import F = Functions
  
  type State<K>

  ghost predicate Valid<K(==)>(s : State<K>)
  function Empty<K(!new)>(): State<K>
    ensures Valid(Empty<K>())
  function AssertEqual<K(!new)>(s: State<K>, u: K, v: K): State<K>
    requires Valid(s)
    ensures Valid(AssertEqual(s, u, v))
  predicate CheckEqual<K(!new)>(s: State<K>, u: K, v: K)
    requires Valid(s)

  // New function, to extract which finite set of keys have been mentioned so far.
  ghost function Keys<K(==)>(s: State<K>): set<K>

  ghost function Abstr<K(!new)>(s: State<K>): set<(K, K)>
  // Definition TBD!  It acts like `Elements` in last class' examples.

  // How to extend a set of equalities with all logical consequences that follow
  // from them:
  ghost function Closure<K(!new)>(keys: set<K>, eqs: set<(K, K)>): set<(K, K)>
  {
    set a: K, b: K | F.ImpliedEqual(eqs, a, b)
                     && a in keys && b in keys :: (a, b)
  }

  // Note how the following now constrain both `Keys` and `Abstr`.
  
  lemma EmptyCorrect<K(!new)>()
    ensures Keys(Empty<K>()) == {}
    ensures Abstr(Empty<K>()) == Closure<K>({}, {})

  lemma CheckEqualCorrect<K(!new)>(s: State<K>, u: K, v: K)
    requires Valid(s)
    requires u in Keys(s) && v in Keys(s)
    ensures CheckEqual(s, u, v) == ((u, v) in Abstr(s))

  lemma AssertEqualCorrect<K(!new)>(s: State<K>, u: K, v: K)
    requires Valid(s)
    ensures Keys(AssertEqual(s, u, v)) == Keys(s) + {u, v}
    ensures Abstr(AssertEqual(s, u, v)) ==
              Closure(Keys(s) + {u, v}, Abstr(s) + {(u, v)})
}

Specifying UnionFind with an abstraction relation

In class, we’ll sidestep the headache of maintaining a keys set by using an abstraction relation instead of an abstraction function. That is, we will allow one concrete data-structure value to represent many abstract values! Our abstract values will be exactly the sets of asserted equalities that we already worked with above, with types like set<(K, K)>. A concrete union-find value maps to those sets of equalities that are consistent with it.

So we’ll use the following interface for this version of union-find.

module UnionFind {
  import F = Functions
  
  type UnionFind<K>
  ghost predicate Valid<K>(uf: UnionFind<K>)

  function Empty<K>(): UnionFind<K>
  predicate CheckEqual<K>(uf: UnionFind<K>, u: K, v: K)
  function AssertEqual<K>(uf: UnionFind<K>, u: K, v: K): UnionFind<K>

  // Now here is our *abstraction relation*:
  ghost predicate Represents<K(!new)>(uf: UnionFind<K>, eqs: set<(K, K)>)

  // And correctness of the main functions is easily phrased in terms of
  // `Represents` and `ImpliedEqual`.

  lemma EmptyCorrect<K(!new)>()
    ensures Represents<K>(Empty(), {})

  lemma CheckEqualCorrect<K(!new)>(uf: UnionFind<K>, eqs: set<(K, K)>, u: K, v: K)
    requires Valid(uf)
    requires Represents(uf, eqs)
    ensures CheckEqual(uf, u, v) == F.ImpliedEqual(eqs, u, v)

  lemma AssertEqualCorrect<K(!new)>(uf: UnionFind<K>, eqs: set<(K, K)>, u: K, v: K)
    requires Valid(uf)
    requires Represents(uf, eqs)
    ensures Represents(AssertEqual(uf, u, v), eqs + {(u, v)})
}

Other strategies

It is actually possible to work with infinite sets to encode and prove this example in Dafny.

One option is to represent sets of K equalities with type (K, K) -> bool: Boolean predicates over possible equalities. The nuisance with this choice is that Dafny doesn’t in general admit functional extensionality, where functions are equal if they map equal inputs to equal outputs. Hence, we can’t use simple equality to explain what the abstraction function does to a concrete value.

Another option is to use Dafny’s iset type, for infinite sets, which are allowed only in ghost code that doesn’t really need to run. Then we can pretty much repair our broken set example above.

We found the proofs to be a little longer with any of these alternatives, but we only explored them as wrappers over our version with a representation relation. That is, we took the representation-relation module as a black box and proved the three other versions on top of it, without any new recursion in the implementations. Maybe the proofs would be shorter if going after any of these alternative interfaces directly. We kind of like having avoided either of encoding infinite sets or tracking keys that are legal to mention, though your taste may vary. The implementation details for all four versions will be revealed in class (though we will probably tour briskly through the ones with abstraction functions)!

Summary

It’s in the eye of the beholder which abstractions and specifications are pleasant to work with. All of the following sound intuitively appealing:

• The mapping from a concrete value to an abstract value should be a function.
• We’d rather not talk about infinite sets to explain abstraction.
• We’d rather not have to do extra tracking of which arguments are legal to pass to functions.

There can be tradeoffs between these goals, and union-find showcases them well. Luckily, Dafny bakes in very little of the specifics of abstraction in specification, so we can pick and choose styles to taste.