An overview over the KIV project can be found here
The graph in the heap consists of nodes that store a value (of an unspecified element) and a map from the same element type to successors, that are given by references to the heap. The heap maps from references to nodes (it is instantiated here. The map from nodes to nodes thus maps references.
Specification functions contains several auxiliary definitions
- A predicate
closedthat specifies that the heap is closed wrt. lookup of successor nodes
- Injectivity of maps
applyfunction that applies a map to a heap. Its purpose is to get the cloned part of the heap
- A recursive definition of paths, i.e., lists of elements, and a derived predicate for reachability
We have solved subchallenges 1 to 4 for copy and 1 to 3 for eval. Specifically, under the assumption that the heap is closed wrt. lookup we have proved
- termination (lemma copy-term)
- locations reachable from the copy are fresh (lemma copy-all-reachable-are-fresh)
- the old heap is a subheap of the resulting one (lemma copy-no-effects)
KIVs logic is total and access to non-allocated references in formulas yields unspecified results. The procedures
alloc that are defined in the library detect invalid heap access and abort in such a case. Hence, termination proves memory safety. In the same specification there is an axiom that postulates infinite memory (so allocation succeeds always).
The proofs are by induction, the measure is the size of the domain of the original heap minus the size of the map. Termination needs a fairly strong invarinat, that is specified in copy as two predicates
copy-edges-prepost. These predicates state that the current heap can be split disjointly into the original heap and a new part. The domain of the map is bounded by the new heap, whereas the range of the map corresponds to the new part. Furthermore, the two subheaps are closed on their own and the map is injective.
For eval, we prove
- termination (lemma eval-term)
- an existing path is found (lemma existing-path)
- a nonexisting path gives no result (lemma eval-nonexisting-path)
Since we don’t use integers, the success of eval is encoded by an option type with alternatives some/none. The proofs we have done for eval are trivial.
We have not proved that the copied graph is isomorphic. However, there is a theorem map-path in specification functions that states that for an injective map that contains at least the references reachable from the path in the originial sub-graph in its domain, the mapped path equi-exists.
Since we have proved that the map is injective, it remains to be shown that it is a homomorphism (it is surjective as well as its range is exactly the new heap).