The native type, KeyTree, has an empty constructor and a node with two
children and a word key. Its functions count nodes, sum keys, compute height, increment keys,
replace a root key, insert a key by binary-search-tree comparisons, select the left child, and
split the root into its children. Word results wrap modulo 2^64.
The encoding represents an empty tree by null and a node by a record with
fixed word and child fields. The compiled module proves execution under
the verified compiler's representation, ownership, memory, and recursion premises. The
derivation runs verified_recursive_type for KeyTree in a module apart
from the encoding, so that the verified compiler's programs over the type share one set of
conversions and lemmas. Ordering and membership proofs for search-tree insertion remain future
work.
The tree example adds operations of its own over KeyTree, which
no verified module compiles. Its test support constructs and renders arbitrary trees, including
trees that exceed the guarded recursion limit. The recursive-type
cases use that support to test size, incr,
setKey, leftChild, and splitRoot on chains of up to 4,096 nodes and on arbitrary trees, and
tests/verified/run.sh runs those cases on the library's module as well, as
tests/verified/library-cases.txt maps them.