# CS G379 Decision Procedures for Verification Fall 2007

### Extra Credit Problems

Below are two extra credit problems. You can send solutions before Dec. 7th and each is worth an extra 25 points on one of your homework assignments. You have to work on these alone.

1. Fair scheduler

The semantics of distributed systems are often given with respect to what is called the interleaved semantics. A state of a distributed system is just a configuration of the systems comprising the distributed system, which might also include the state of the network(s). The set of successor states of a distributed system state is the set of states obtained by selecting one of the systems and stepping it: letting it take a local, atomic step. A schedule is just a list of systems and defines a run, a sequence of states, of the distributed system, where the first state is the initial state, the second state is obtained by stepping the first system of the schedule starting in the first state of the run, the third state is obtained by stepping the second system of the schedule starting in the second state of the run, and so on. A scheduler defines a set of schedules. The semantics of a distributed system given some scheduler is the set of runs allowed by scheduler. Since some schedules can ignore certain systems (meaning that they never get a chance to make a move), schedulers are often required to be fair. Your job is to define a fair scheduler for an infinite number of processes. Provide a book that exports two constrained functions `f` and `nxt`, that satisfy the following constraints.

The function `f` is the scheduler, and given a natural number `i`, `(f i)` is the id of the process that takes a step at time `i`. One of the constraints is that `f` returns a natural number.

``````
(defthm natp-f
(natp (f i)))
```
```
That `f` is fair means that for any time `i` and process id `p`, there is another time `(nxt i p) >=i` at which `p` takes a step. This is expressed with the following two theorems. First, `i <= (nxt i p)`.
``````
(defthm <=-i-nxt
(implies (and (natp i)
(natp p))
(<= i (nxt i p))))
```
```
Second, `(f (nxt i p)) = p`.
``````
(defthm nxt-f
(implies (and (natp i)
(natp p))
(equal (f (nxt i p)) p))))
```
```
The only thing that your book should export are the above three theorems. Note that this means you will have to use local and encapsulate to exhibit functions that satisfy the above constraints. You may want to use the top-with-meta arithmetic book, which can be included with the following command.
``````
(include-book "arithmetic/top-with-meta" :dir :system)
```
```
2. Finite functions.

It is often useful to reason about finite functions; functions whose domain is essentially finite. I say "essentially" because the functions can be over an infinite domain, as long as only a finite number of elements in the domain have a non-default value (let's say that the default value is `nil`). Notice that such functions can be represented as alists. Also, notice that such functions generalize the notion of a structure, as a structure is just a finite function whose domain is the set of fields.

Develop a book that allows one to reason about finite functions. Start by defining the functions `val` and `set` such that if `f` is a finite function, then `(val elem f)` returns the value that `f` assigns to element `elem` and `(set elem val f)` is the finite function that is just like `f`, except that the value of `elem` is `val`.

The book should export the following events (and any others you need/ want).

``````
(defthm val-same-set
(equal (val elem (set elem x f))
x))

(defthm val-diff-set
(implies (not (equal elem elem2))
(equal (val elem (set elem2 x f))
(val elem f))))

(defthm set-same-val
(equal (set elem (val elem f) f)
f))

(defthm set-same-set
(equal (set elem y (set elem x f))
(set elem y f)))

(defthm set-diff-set
(implies (not (equal elem elem2))
(equal (set elem2 y (set elem x f))
(set elem x (set elem2 y f))))
:rule-classes ((:rewrite :loop-stopper ((elem2 elem set)))))
```
```
Note that the you cannot prove the above theorems using the obvious ways of representing finite functions. This exercise is hard, so if you have to, you can include additional hypotheses to the above theorems. You will want to familiarize yourself with ACL2's total order, because finite functions can have any type of elements in their domain. To get you started, here are the contents of a book that defines `<<` to be an irreflexive total order on the ACL2 universe.
``````
(in-package "ACL2")

(defun << (x y)
(and (lexorder x y)
(not (equal x y))))

(defthm <<-irreflexive
(not (<< x x)))

(defthm <<-transitive
(implies (and (<< x y)
(<< y z))
(<< x z)))

(defthm <<-asymmetric
(implies (<< x y)
(not (<< y x))))

(defthm <<-trichotomy
(implies (and (not (<< y x))
(not (equal x y)))
(<< x y)))

(defthm <<-implies-lexorder
(implies (<< x y)
(lexorder x y)))

(in-theory (disable <<))
```
```