Hi Nicholas,
Nicholas Mc Guire wrote:
What did supprise me a bit is that:
7500 LoC yield 200k Lines of formal proof 7500 LoC yield "more than 10k intermediate theorems
I wonder how scalable such an approach is... And of course raising (from a safety perspective) the question if the complexity and potential failures of 7.5k of Code were not replaced by a even higher complexity (of course its a diverse representation - which takes out a lot of this imediately)
the question is whether lines of Isabelle code, lines of Isabelle proof script and number of intermediate theorems is really a good metric to judge about the trustworthiness of the model and the corresponding proofs.
In Robin (sources are here: http://robin.tudos.org/robin-hw-model-2008-05-15.tgz), we ended up with approx. 20K LOC of PVS code for the somewhat detailed C++ / Hardware model. However, most of this code is not to describe the model but to establish higher level results. There is for example a rather lengthy proof that establishes that under a bunch of preconditions virtual memory behaves as normal unaliased memory. That is reading and writing have the desired property and do not cause side effects (e.g., due to virtual memory aliases).
The specification of the page-table walker is only about 50 LOC (plus another 50-100 LOC for the reading and writing page-table entries rather than bytes). The actual lemma boils down to a number of results such as:
data(read (a1) ; read (a2)) = data(read (a2))
which means the first read to address a1 has no side effects on the data returned by the second read.
The LOCs for the auxiliary lemmas that were necessary to produce these results are however in the order of 1500 LOC (proof commands not included).
If you would trust PVS to work correctly (which is critical due to some reported soundness bugs) all you need to do is to agree with the +- 100 lines of specification and with the lemma results. The intermediate stuff you can just skip.
A second point is that proof commands in PVS (and also in Isabelle) have different power. For example, the comand expand just replaces a lemma with its definition --- a step you can easily follow --- the command grind however applies almost all known simplification techniques at once. Thus you have a 1 line proof is grind works and a 100+ line proof if you would apply the respective simplification steps by hand.
I would therefore very much like to see Nicta's Isabelle code for the model and for the final lemmas at least.
Best Regards
Marcus