This article describes some preliminary work on an invariant generation technique for Lustre. I gave a talk on this at Synchron 2022 in late November 2022. Slides are available here (PDF), but the slides are quite large (25MB) as they contain many bird photographs. I intend to do more evaluation and write this up as a paper in the future.
For safety-critical programs written in Lustre, we can prove that they satisfy certain correctness properties using model checking. Most model checkers for Lustre first transform the program into a transition system and prove properties on the transition system, rather than proving them directly on the streaming semantics of Lustre, because the streaming semantics becomes complex for streams with arbitrary clocks. However, some properties which are obvious on the streaming semantics require extra inductive invariants on the transition system. These invariants may need to refer to internal state of components, which makes them difficult to write in the source language. For such properties, if the model checker's invariant generation techniques do not find the required invariants within the time limit, the proof attempt will time out. I introduce an invariant generation technique called Applicative Invariants for Lustre (AIL) which uses equivalence graphs (e-graphs) to find invariants that hold on the streaming semantics but require inductive invariants on the transition system. This invariant generation technique is designed to work in cooperation with other techniques, as the invariants it proposes are not as diverse as those proposed by instantiation-based invariants [Kahsai11] or counterexample-based invariants such as IC3 [Bradley12]. The advantage is that it draws from a smaller set of possible invariants so that the whole set can be explored exhaustively, making it more resiliant to minor program changes.
Introduction
Properties that refer to multiple instances of modal operators are particularly sensitive to the timing and order of generated candidate invariants, as each modal operator instance has its own internal state that may be related to the other states in some way.
One example of such a property uses the modal operator LastN(n, e), which takes a time period n and a predicate e, and returns true if the predicate has been true for the specified time period.
We would generally expect to be able to prove that for any reasonable time period and predicate, LastN(n, e) => LastN(n, e).
This property is trivial on a semantics that allows equational reasoning, as we know that p => p holds for any predicate p.
However, LastN includes some internal state, and the generated transition system contains two instances of the LastN stream transformer with distinct states.
Using only local reasoning on the transition system, it is not possible to show that the two instances have equivalent state or produce equivalent results.
Although we might not write such a property by hand, similar properties can arise as part of a larger system.
A program might contain a subnode whose contract guarantees that LastN holds, and then we might want to re-state it as a guarantee of the top-level main node.
We could have rewritten the original predicate to be easier to prove by introducing a variable binding for the result of LastN with something like let l = LastN(n, e) in l => l.
This sort of restructuring is not as simple when the two instances occur in the contracts of different nodes; introducing shared bindings across multiple nodes would also obscure the high-level meaning of the contract.
In cases like this, if the invariant generation does not find the required invariants, then the user does not have many options of how to proceed.
They may need to resort to disabling the property and proving it by hand.
Applicative invariants
I introduce an invariant generation technique, Applicative Invariants for Lustre, which recovers certain invariants which are obvious on the streaming semantics but not on the transition system. The goal is to make composition of contracts more reliable by making certain limited guarantees about what can be proven. The high level idea is to convert the node into an equivalence graph, apply some rewrite rules, and then extract the interesting equivalences that were not obvious before any rewriting was applied.
Equivalence graph generation
Converting a Lustre node into an equivalence graph is straightforward. A Lustre node is effectively a set of equations, while an equivalence graph is an efficient representation of a set of equations. Lustre supports node invocations, which cannot be directly represented in an equivalence graph, so for each instance the node definition must be inlined into its use-site. This unfolding could lead to a large graph, but the user can limit the size of the equivalence graph by adding a contract to a node, in which case only its contract needs to be inlined.
Rewriting
We then apply rewrites to the equivalence graph, as it will expose more interesting equivalences.
One such rewrite is the fact that primitive applications distribute over pre, which can be written as forall f e. map f (pre e) = pre (map f e).
Here, map f is some pure non-streaming computation such as a primitive application.
We perform a similar rewrite for the arrow construct e -> e'.
We also rewrite recursive definitions to use explicit fixpoint operators. This rewriting exposes the sharing between different instances of recursive bindings that have the same structure, but have different names.
We also have a set of pure rewrites which do not take advantage of the streaming nature of the program, but should hold for any pure computation. Constant propagation, identity laws, commutativity, associativity and so on are pure rewrites. We call these rewrites the "boring" rewrites as they are not interesting from a streaming perspective, but they are still useful as applying them might expose opportunities for interesting rewrites.
We apply both sets of rewrites -- the boring and the interesting rules -- up to saturation.
We can use the equality saturation technique introduced in egg [Willsey20], which defers rebuilding the internal congruence relation until after a batch of rewrites, rather than rebuilding after each single rewrite.
Invariant extraction
The resulting equality graph contains many equivalences, but not all of these are useful for proving properties on the transition system.
Some equivalences we expect the SMT solver to be able to figure out, such as that x + y = y + x.
Other equivalences will be consequences of others, for example if we know that x.count = y.count then we know that (x.count > 5) = (y.count > 5).
We wish to minimise the number of invariants to avoid flooding the SMT solver and the user with inane facts.
To avoid the obvious facts, we create a second graph from the Lustre definition, which we call the "boring" graph. We apply only the boring rewrites to the boring graph, and do not perform any interesting streaming rewrites. This idea is similar to rewrite rule synthesis for mathematical identities [Briggs22], which creates a second graph with some definitions hidden to find a set of obvious rewrite rules to avoid.
To actually extract the invariants, we look for equivalences in the interesting graph that aren't in the boring graph. When we find such an equivalence, we can use it as an invariant. We also add the invariant to the boring graph and rebuild the congruence relation, so that we do not also add any other invariants that are a trivial consequence of the new invariant.
This extraction heuristic tries to greedily minimise the number of required invariants. In this case, we are not so interested in the absolute minimum number of invariants, so a greedy technique is probably sufficient.
The extracted invariants may refer to pre expressions, such as pre x.count = pre y.count.
In this case, both pre expressions are undefined at the first step, and trying to prove the base case of the invariant will fail as the two undefined values are not necessarily equal.
We can resolve this by ignoring the first step for pre expressions, which we write as the invariant true -> pre x.count = pre y.count.
In fact, we can ignore the first step for all invariants, whether or not they contain a pre, as the interesting invariants are obvious for the inductive base case.
Modularity
We can perform the entire applicative invariant generation compositionally, on one node at a time, and then reuse the equivalence graphs from subnodes. This reuse avoids having to extract the whole node and apply the rewrites to saturation again. For nodes with contracts, we would need to perform invariant generation twice: first on the node with all of its definitions, and then again on the node with its implementation hidden. Contracts are not yet implemented in Songlark.
Evaluation
Initial experiments show promising results, but evaluation on larger test cases is needed for a quantitative evaluation. Applicative invariant generation for Lustre (AIL) is strictly weaker than instantiation-based invariants [Kashsai11] and IC3 [Bradley12], in that there are invariant candidates proposed by the others that will never be proposed by AIL. I believe that AIL will be more useful for checking larger systems where the heuristic-based invariant generation is unable to explore the whole search space and so misses vital invariants, but I have not yet validated this claim. Because the heuristic-based invariant generation mainly breaks down on larger systems, it is difficult to find small self-contained problems that demonstrate the issue.
Interestingly, AIL is sometimes stronger and sometimes weaker than k-induction.
There are some properties that cannot be proved by k-induction for any finite k, such as when dealing with the SoFar(e) modal operator which is a past-bounded version of Always(e).
For arbitrary predicates e and p, the property (SoFar(e) => p) => (SoFar(e) => p) cannot be proved with k-induction alone as the two instances of SoFar have different states that are not necessarily related.
The SoFar(e) operator has to look some unbounded distance into the past to see if e has always been true, so no amount of k-induction will be able to show that the two SoFar instances are equivalent.
The simpler property SoFar(e) => SoFar(e) also contains two different instances of SoFar, but the property itself adequately describes the relationship between the two states, so it can be proven fine with 1-induction.
This example is not entirely synthetic, either: suppose that we have composed together two subcontrollers which both have bounded-input-bounded-output properties of the form SoFar(input < 100) => SoFar(middle < 100) and SoFar(middle < 100) => SoFar(output < 100).
We expect to be able to prove that the composition is also bounded-input-bounded-output, that is, SoFar(input < 100) => SoFar(output < 100).
We can't prove the composition with k-induction alone and proving it with heuristic-based invariant generation is a gamble, but we can be sure that AIL will find the necessary invariants.
On the other hand, there are some invariants that k-induction can prove which AIL cannot, as AIL only infers equivalence invariants.
Future work
Applicative invariants for Lustre is currently implemented in Songlark. For a fair evaluation with other techniques, it might be necessary to implement it in another system such as Kind2. This would also involve extending the clock support, as Songlark supports only limited clocks (the bare minimum required to implement automata).
An obvious extension would be to allow user-defined rules: for example, we could rewrite modal operators such as SoFar to distribute over conjunction.
Conclusion
By taking advantage of equational reasoning on the source language of Lustre, we can get a certain class of invariants for "free". These invariants are deliberately limited in scope so that they can provide stronger guarantees than heuristic invariant searches. I have shown some examples where such simple invariants are needed to compose systems together, but further evaluation is needed to show that it is truly adequate.
References
- [Bradley12] Bradley, Aaron R. "Understanding IC3." International Conference on Theory and Applications of Satisfiability Testing. Springer, Berlin, Heidelberg, 2012.
- [Briggs22] Briggs, Ian, and Pavel Panchekha. "Synthesizing mathematical identities with e-graphs." Proceedings of the 1st ACM SIGPLAN International Symposium on E-Graph Research, Applications, Practices, and Human-factors. 2022.
- [Kahsai11] Kahsai, Temesghen, Yeting Ge, and Cesare Tinelli. "Instantiation-based invariant discovery." NASA Formal Methods Symposium. Springer, Berlin, Heidelberg, 2011.
- [Willsey20] Willsey, Max, et al. "Egg: Fast and extensible equality saturation." arXiv preprint arXiv:2004.03082 (2020).