# Changeset 3557 for Papers

Ignore:
Timestamp:
Apr 24, 2015, 1:31:35 PM (4 years ago)
Message:

bit more on bitvectortrie

File:
1 edited

### Legend:

Unmodified
 r3555 A central design decision in our formalisation is the choice of how to encode memory. The MCS-51 has various memory spaces and registers that can be addressed with bytes and words. \begin{lstlisting} inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] := Leaf: A -> BitVectorTrie A O | Node: $\forall$n: nat. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n) | Stub: $\forall$n: nat. BitVectorTrie A n. \end{lstlisting} Using a complete associative map to capture an entire memory space, including large swathes of uninitialised data, would be incredibly inefficient and make any proof incredibly difficult due to the strain placed on Matita. However, using a na\"ive data structured like an association-list to encode memory would lead to inefficiencies when stepping through the semantics of a machine code program inside Matita. We therefore use an indexed type, \texttt{BitVectorTrie}, to efficiently represent a memory space that may have holes' of uninitialised or unspecified data: \begin{lstlisting} inductive BitVectorTrie (A: Type[0]): $\mathbb{N}$ $\rightarrow$ Type[0] := Leaf: A $\rightarrow$ BitVectorTrie A O | Node: $\forall$n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n) | Stub: $\forall$n. BitVectorTrie A n. \end{lstlisting} The $\mathbb{N}$ index of the \texttt{BitVectorTrie} family records the maximum length of any path to stored data through the tree. For a dependently-typed encoding of a trie data structure, the \texttt{Leaf} and \texttt{Node} constructors are standard. The novelty of \texttt{BitVectorTrie} lies in the \texttt{Stub} constructor, which intuitively represents a hole' in the tree, and can appear % Trie data structure and use of dependent types