145 lines
8.2 KiB
TeX
145 lines
8.2 KiB
TeX
%% SCRAP: architecture/VM_FORMALIZATION_PLAN
|
|
%% SOURCE: docs/working/architecture/VM_FORMALIZATION_PLAN.adoc
|
|
%% STATUS: WORKING
|
|
%% FITS: dev-guide/ch-verification
|
|
%% EDITORIAL: lifted — prose rewritten to press voice
|
|
|
|
\section{VM Formalization Roadmap}
|
|
|
|
This roadmap records the staged approach to formally proving the StarForth virtual
|
|
machine in Isabelle/HOL. It grows alongside the \texttt{.thy} theory files in the
|
|
formal proof tree and serves as the architecture map for VM-level verification.
|
|
|
|
\subsection{Objectives}
|
|
|
|
The plan pursues three goals. It preserves room for architectural refactoring while
|
|
the proofs evolve. It treats the physics-metadata proofs ---
|
|
\texttt{Physics\_StateMachine} and \texttt{Physics\_Observation} --- as the first
|
|
pillar, onto which additional modules snap within the same Isabelle session. And it
|
|
keeps proof obligations discoverable from the C headers, documenting invariants close
|
|
to the runtime code they constrain.
|
|
|
|
\subsection{Session Layout}
|
|
|
|
The verification workspace is organized as a layered set of theories. The lower
|
|
layers are scaffolded and build independently of the physics layer; the physics
|
|
theories remain fluid; the upper layers are planned.
|
|
|
|
\begin{center}
|
|
\begin{tabular}{ll}
|
|
\toprule
|
|
Theory & Purpose (current status) \\
|
|
\midrule
|
|
\texttt{VM\_Core} & VM state record, pointer accounting, control-flag helpers (scaffolding). \\
|
|
\texttt{VM\_Stacks} & List-backed stack model locale and depth lemmas (scaffolding). \\
|
|
\texttt{VM\_Words} & Abstract wrappers for \texttt{>R}/\texttt{R>} transfers (scaffolding). \\
|
|
\texttt{VM\_Register} & Dictionary model for \texttt{register\_word} (scaffolding). \\
|
|
\texttt{Physics\_StateMachine} & Ring-buffer and mailbox invariants for HOLA (fluid). \\
|
|
\texttt{Physics\_Observation} & Per-word physics updates, frame composition (fluid). \\
|
|
\texttt{VM\_Dictionary} & \textit{Planned:} dictionary lifecycle, physics wiring. \\
|
|
\texttt{VM\_Interpreter} & \textit{Planned:} interpreter state machine, semantics. \\
|
|
\texttt{VM\_IO} & \textit{Planned:} host capability shims, scheduler obligations. \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
The \texttt{VM\_Formal} session captures \texttt{VM\_Core} through
|
|
\texttt{VM\_Register} and builds without the physics layer. \texttt{Physics\_Formal}
|
|
extends it, keeping the observation machinery available while acknowledging that
|
|
those theories remain fluid. Each planned theory imports the prior layers so the
|
|
whole workspace stays incrementally checkable via \texttt{isabelle build}.
|
|
|
|
\subsection{Development Guidelines}
|
|
|
|
\begin{itemize}
|
|
\item \textbf{Pair source and proof} --- when a C module gains an invariant, add or
|
|
update the matching theory and cross-reference it in file-level comments.
|
|
\item \textbf{Prefer locales} --- define subsystem properties as locales and extend
|
|
them in follow-up theories rather than rewriting existing ones.
|
|
\item \textbf{Document assumptions} --- every lemma states the runtime assumptions
|
|
it relies on, such as stack-depth bounds or profiler hooks.
|
|
\item \textbf{Keep proofs fast} --- favor algebraic lemmas over brute-force tactics
|
|
so developers can replay the session during normal builds.
|
|
\item \textbf{Track TODOs} --- leave \texttt{text} blocks or FIXME notes in the
|
|
theory files marking which invariants still need encoding.
|
|
\end{itemize}
|
|
|
|
\subsection{Next Actions}
|
|
|
|
The immediate agenda is to land a green \texttt{VM\_Formal} build before layering
|
|
physics obligations; flesh out \texttt{VM\_Core} with stack-depth and dictionary
|
|
invariants once the C helpers stabilize; introduce a \texttt{VM\_Stacks} theory
|
|
capturing data and return-stack well-formedness and pointer safety (aligned with
|
|
\texttt{STRICT\_PTR}); model dictionary entries against \texttt{DictEntry} and connect
|
|
the physics-metadata lemmas to the compiler pipeline; decide the C-to-Isabelle
|
|
modeling path (AutoCorres versus manual abstraction) before tackling the interpreter
|
|
loop; and wire a Makefile target to \texttt{isabelle build} so CI can gate on proofs
|
|
as they expand.
|
|
|
|
\subsection{Multi-Day Proof Checklist}
|
|
|
|
The longer-horizon checklist proceeds in stages. A \textbf{session baseline} records
|
|
the theory order in the project \texttt{ROOT} and snapshots current failures.
|
|
\textbf{VM core invariants} expand \texttt{VM\_Core} with pointer and limit
|
|
invariants and error-flag rules, each phrased as a lemma inside the \texttt{vm\_core}
|
|
locale for reuse. \textbf{Stack model helpers} add peek/push/pop transfer lemmas for
|
|
each stack direction, proving both success and guard-failure variants alongside
|
|
runtime versions that expose the \texttt{dsp}/\texttt{rsp} relationship.
|
|
\textbf{Word semantic wrappers} split per-module theories that import
|
|
\texttt{VM\_Words} and derive success and no-op lemmas in one or two lines.
|
|
\textbf{Dictionary registration} centralizes lemmas in \texttt{VM\_Register},
|
|
guarding reserved names. A \textbf{module-march template} repeats, for each of the
|
|
roughly nineteen word modules, the cycle of identifying the C helper, confirming an
|
|
Isabelle helper, creating the wrapper lemma, registering the word, and rerunning the
|
|
session, with progress tracked in a status table. \textbf{IO and external hooks} stub
|
|
locale assumptions for side-effecting words, and \textbf{housekeeping} rebuilds the
|
|
session nightly, treating a green build as the commit gate. The \textbf{stretch goal}
|
|
is a consolidated theorem: that all registered words satisfy their claimed semantics,
|
|
combining the lookup lemmas with the per-word proofs.
|
|
|
|
\subsection{VM-First Verification Roadmap}
|
|
|
|
The proof order works upward from primitives. It begins with the \textbf{stack
|
|
primitives} (\texttt{vm\_push}, \texttt{vm\_pop}, \texttt{vm\_rpush},
|
|
\texttt{vm\_rpop}), proving they refine the abstract transfers and raise
|
|
\texttt{vm\_error\_active} precisely on overflow and underflow. It then proves the
|
|
\textbf{return-stack words}, the \textbf{data-stack transfer words}
|
|
(\texttt{DROP}, \texttt{DUP}, \texttt{SWAP}), the \textbf{arithmetic and logic
|
|
modules}, the \textbf{dictionary and lookup words} (\texttt{CREATE}, \texttt{FIND},
|
|
\texttt{IMMEDIATE}), the \textbf{control-flow words}, the \textbf{compiler and
|
|
interpreter infrastructure} (proving the interpreter halts on
|
|
\texttt{vm\_error\_active} and honors abort and exit flags), and finally the
|
|
\textbf{system and I/O words}, stubbing the required capabilities.
|
|
|
|
\subsection{Status Snapshot}
|
|
|
|
Stack and return-stack semantics are complete:
|
|
\texttt{vm\_push\_sem}, \texttt{vm\_pop\_sem}, \texttt{vm\_rpush\_sem}, and
|
|
\texttt{vm\_rpop\_sem} carry success, overflow, and underflow lemmas in
|
|
\texttt{VM\_StackRuntime.thy}. The parameter-stack words \texttt{DROP}, \texttt{DUP},
|
|
\texttt{?DUP}, \texttt{SWAP}, \texttt{OVER}, \texttt{ROT}, \texttt{-ROT},
|
|
\texttt{DEPTH}, \texttt{PICK}, and \texttt{ROLL} have proven abstract semantics,
|
|
runtime correspondence, and wired dictionary registration. The return-stack words
|
|
\texttt{>R}, \texttt{R>}, and \texttt{R@} have established abstract semantics and
|
|
runtime equality. The model now exposes \texttt{cell\_to\_int}/\texttt{int\_to\_cell}
|
|
conversions, and the \texttt{VM\_Formal} session builds cleanly with the theories
|
|
ordered \texttt{VM\_Core} $\to$ \texttt{VM\_Stacks} $\to$ \texttt{VM\_StackRuntime}
|
|
$\to$ \texttt{VM\_DataStack\_Words} $\to$ \texttt{VM\_ReturnStack\_Words} $\to$
|
|
\texttt{VM\_Words} $\to$ \texttt{VM\_Register}.
|
|
|
|
The next milestones introduce an instruction-pointer and memory abstraction so
|
|
\texttt{(BRANCH)} and \texttt{(0BRANCH)} can be specified without referencing C
|
|
internals; model loop frames on the return stack (\texttt{?DO}, \texttt{DO},
|
|
\texttt{LOOP}, \texttt{+LOOP}, \texttt{LEAVE}, \texttt{I}, \texttt{J}); formalize the
|
|
compile-time control-flow stack so \texttt{IF}, \texttt{ELSE}, and \texttt{WHILE} can
|
|
be reasoned about at registration time; and then extend the dictionary lemmas toward
|
|
the arithmetic and logical modules.
|
|
|
|
Achieving these steps positions the project to claim that StarForth is, to the
|
|
authors' knowledge, the first open-source FORTH VM accompanied by a full proof corpus
|
|
of its core primitives in Isabelle/HOL, enabling proof-carrying reference builds and
|
|
machine-verified stack discipline.
|
|
|
|
%% TODO(bob): The source status snapshot is dated "Week of YYYY-MM-DD" — supply the
|
|
%% real date when promoting this scrap.
|