Post Analysis Treatments

Post-analysis treatments are flag-activated Kind 2 features that are not directly related to verification. The current post-analysis treatments available are

  • certification,

  • compilation to Rust,

  • test generation,

  • contract generation,

  • assumption generation,

  • invariant printing, and

  • inductive validity core generation

All of them are deactivated by default. Post-analysis treatments run on the last analysis of a system. It is defined as the last analysis performed by Kind 2 on a given system. With the default settings, Kind 2 performs a single, monolithic analysis of the top node. In this case, the last analysis is this unique analysis.

This behavior is changed by the compositional flag. For example, say Kind 2 is asked to analyze node top calling two subnodes sub_1 and sub_2, in compositional mode. Say also sub_1 and sub_2 have contracts, and that refinement is possible. In this situation, Kind 2 will analyze top by abstracting its two subnodes. Assume for now that this analysis concludes the system is safe. Kind 2 has nothing left to do on top, so this compositional analysis is the last analysis of top, Kind 2 will run the post-analysis treatments. Assume now that this purely compositional analysis discovers a counterexample. Since refinement is possible, Kind 2 will refine sub_1 (and/or sub_2) and start a new analysis. Hence, the first, purely compositional analysis is not the last analysis of top. The analysis where sub_1 and sub_2 are refined is the last analysis of top regardless of its outcome (assuming no other refinement is possible).

Long story short, the last analysis of a system is either the first analysis allowing to prove the system safe, or the analysis where all refineable systems have been refined.

The modular flag forces Kind 2 to apply whatever analysis / treatment the rest of the flags specify to all the nodes of the system, bottom-up. Post-analysis treatments respect this behavior and will run on the last analysis of each node.

Prerequisites

Some treatments can fail (which results in a warning) because some conditions were not met by the system and/or the last analysis. The prerequisites for each treatment are:

Treatment

Conditions

Notes

certification

last analysis proved the system safe

will fail if node is partially defined

compilation to Rust

test generation

system has a contract with more than one mode and the last analysis proved the system safe

contract generation

experimental

assumption generation

last analysis falsified some property

generates non-temporal constraints

invariant printing

inductive validity core generation

last analysis proved the system safe