The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
At the moment, a number of rules are less efficient that they might otherwise be. There are a number of rules in which this is true:
Congruence Closure. Upon matching an equality (e.g. x == y + 1) we want to apply it to all active terms (e.g. x < 0 becomes y + 1 < 0). The key is that, from this point onwards, no rule should be able to see the original form of a term.
Type Closure. Upon matching a type test (e.g. x is int) we want to update all active terms to substitute any old variable accesses for x with new ones which employ an appropriate alias declaration. Any failure here can lead to runtime errors arising if type information is incorrectly calculated when required (e.g. we're expecting a record type but we currently have some union type).
The key pattern here is that the rules need to update what is visible in all past states, as well as those in "future" states (i.e. whose delta's have yet to be processed). A rough view of the world looks something like this:
Imagine we are currently processing the introduction from the second state (x == y+1). The first state is already processed and, hence, x < 0 is already asserted. The third state has not yet been processed, but will be at some point. The key is that the above rules need to somehow prevent those terms currently waiting in future states from being processed. Otherwise, those terms can introduce terms in a non-normal form.
The current solution for e.g. congruence closure is to act both when an equality is seen and also when any other term is seen which may be affected by some prior equality assertion. This is actually super expensive!!
The key is that the rule must rewrite history in order to ensure no future terms are inferred which have not been normalised. In fact, this shouldn't be so hard! The rule will subsume everything that it has substituted, and we'll end up in this situation:
This in essence works as it will process the delta between current and past. The key is that we have be sure to process the difference between the additions and removals, not just the additions.
NOTE: There is also the slight question of multiple additions being processed in the same step. These could include non-normalised terms and we need a way of accounting for this.
At the moment, a number of rules are less efficient that they might otherwise be. There are a number of rules in which this is true:
Congruence Closure. Upon matching an equality (e.g.
x == y + 1) we want to apply it to all active terms (e.g.x < 0becomesy + 1 < 0). The key is that, from this point onwards, no rule should be able to see the original form of a term.Type Closure. Upon matching a type test (e.g.
x is int) we want to update all active terms to substitute any old variable accesses forxwith new ones which employ an appropriate alias declaration. Any failure here can lead to runtime errors arising if type information is incorrectly calculated when required (e.g. we're expecting arecordtype but we currently have some union type).The key pattern here is that the rules need to update what is visible in all past states, as well as those in "future" states (i.e. whose delta's have yet to be processed). A rough view of the world looks something like this:
Imagine we are currently processing the introduction from the second state (
x == y+1). The first state is already processed and, hence,x < 0is already asserted. The third state has not yet been processed, but will be at some point. The key is that the above rules need to somehow prevent those terms currently waiting in future states from being processed. Otherwise, those terms can introduce terms in a non-normal form.The current solution for e.g. congruence closure is to act both when an equality is seen and also when any other term is seen which may be affected by some prior equality assertion. This is actually super expensive!!
The key is that the rule must rewrite history in order to ensure no future terms are inferred which have not been normalised. In fact, this shouldn't be so hard! The rule will subsume everything that it has substituted, and we'll end up in this situation:
+----------+ +-----------+ +----------+ +------------+ | +(x < 0) | | +(x==y+1) | | +(x > 0) | | +(y+1 < 0) | | | -------> | | -------> | | --------> | +(y+1 > 0) | | -(1 < 2) | | | | | | | | | | | | | | -(x < 0) | +----------+ +-----------+ +----------+ | -(x > 0) | +------------+ (past) (current)This in essence works as it will process the delta between
currentandpast. The key is that we have be sure to process the difference between theadditionsandremovals, not just theadditions.NOTE: There is also the slight question of multiple additions being processed in the same step. These could include non-normalised terms and we need a way of accounting for this.