Automatic Function Annotations for Hoare Logic

TL;DR

This paper introduces a function annotation logic extending Hoare logic, enabling automatic storage and reuse of intermediate reasoning in program proofs, demonstrated on the seL4 microkernel to improve proof efficiency.

Contribution

It presents a novel extension to Hoare logic that automates and reuses intermediate proof steps, reducing proof complexity and duplication.

Findings

Significantly reduced proof size for seL4 microkernel

Automated storage of intermediate reasoning in proofs

Enhanced proof reuse across multiple properties

Abstract

In systems verification we are often concerned with multiple, inter-dependent properties that a program must satisfy. To prove that a program satisfies a given property, the correctness of intermediate states of the program must be characterized. However, this intermediate reasoning is not always phrased such that it can be easily re-used in the proofs of subsequent properties. We introduce a function annotation logic that extends Hoare logic in two important ways: (1) when proving that a function satisfies a Hoare triple, intermediate reasoning is automatically stored as function annotations, and (2) these function annotations can be exploited in future Hoare logic proofs. This reduces duplication of reasoning between the proofs of different properties, whilst serving as a drop-in replacement for traditional Hoare logic to avoid the costly process of proof refactoring. We explain how this was implemented in Isabelle/HOL and applied to an experimental branch of the seL4 microkernel to significantly reduce the size and complexity of existing proofs.