%% 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.
