Experiment with nonterminating programs

[OwenConoly]

I am not actually requesting that this be pulled, but maybe it is interesting.

This branch's version of MetricLeakageSemantics uses a version of omnisemantics that allows proving things about nonterminating programs. There are two ingredients to this:

• First: a mechanism ("midconditions", perhaps) to assert things about programs that haven't terminated. This is done by adding an extra "quitting rule" to the exec predicate; this rule allows the program to quit executing at an arbitrary point, so that a "midcondition" may be asserted about the state at this point. This also requires an extra bit q of program state, a boolean tracking whether the program is still executing or has already quit.
• Second: midconditions alone are not sufficient to assert arbitrary predicates about nonterminating programs. To get around this, we basically take the predicate we'd like to prove, and we declare that it's part of the program's state. In MetricLeakageSemantics, this extra piece of program state has been called aep, of type AEP. This (unfortunate) name alludes to the type's three constructors: one constructor representing a for-All quantifier, one constructor representing an Exists quantifier, and one constructor (the base case) representing a Predicate---this predicate is, more or less, a midcondition. (For no real reason, quantifiers here are restricted to bind nats.)

The idea is that the predicate to be proved evolves as the program runs. For-all quantifiers are discharged via demonic nondeterminism, and exists quantifiers are discharged via angelic nondeterminism. After discharging all quantifiers, you are left with a midcondition, which may be then asserted upon the program's state.

For example, the eventual_one_printer picks a random natural number x, prints the zero character x times, and then prints the one character in an infinite loop. The spec of the eventual one printer says that its I/O trace has a tail of ones.

This way of talking about nonterminating programs seems a bit strange, but the nice thing is that it's not much bother when writing compiler proofs. The extra proof obligations generated by the quit rule are a bit annoying but straightforward to handle. On the other hand, the proof obligations coming from the exists and forall quantifier-discharging rules tend to be trivial.

One difficulty caused by adding the extra inference rules to exec is that exec then fails to be syntax-directed: the quit rule, the forall-discharging rule, and the exists-discharging rule always apply, regardless of which command is being considered. This means that using the inversion tactic on hypotheses of the form exec s q aep k t m l mc post gives multiple goals (some of which are no easier than the original), even when the head of s is known. To do inversion effectively, you can prove an "inversion lemma" like this.

I proved that augmenting the program state with the AEP thing allows you to express, using small-step omnisemantics, any desired predicate about the trace of a program---provided that the program is either reactive (infinite trace) or terminating. I didn't write a formal proof that just as many trace predicates are expressible using big-step omnisemantics, but it is obviously true. However, there are limitations about diverging programs (i.e., nonterminating programs with finite traces); for instance, one cannot write a postcondition saying that a program diverges with a particular finite trace.

The compiler theorem in this branch has a source language defined by an exec predicate involving the AEP and quit things, but it's reassuring that the target language does not involve these things. The target language is still just regular small-step omnisemantics. For example, the high-level spec of the eventual one printer implies this low-level spec.

[OwenConoly]

Actually, the problem I was trying to solve here, using the formulas-embedded-in-program-states thing, has a much simpler solution.

Given a predicate P : stream event -> Prop, how do you state that the trace of a machine starting in state s will satisfy P? In terms of small-step omnisemantics, it's easy.

(Here, we assume some function trace : state -> list event.)

forall (x : stream event), P x \/ runsTo s (fun s' => ~exists (x' : stream event), x = trace s' ++ x')

alternatively:

forall x, runsTo s (fun s' => forall x', x = trace s' ++ x' -> P x)

The same trick works with big-step omnisemantics, assuming it's been augmented with the quit thing as described above.