  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.
