202 lines
8.9 KiB
TeX
202 lines
8.9 KiB
TeX
%% Formal Verification Report — main.tex
|
|
%% SOURCE: proof/*.thy (24 Isabelle/HOL theory files)
|
|
%% docs/working/architecture/VM_FORMALIZATION_PLAN.adoc
|
|
%% NOTE: This publication is generated from the Isabelle/HOL proof corpus.
|
|
%% The canonical source is the proof/ directory at the repository root.
|
|
%% Run: isabelle build -D proof/
|
|
%% Do NOT edit .thy files via this publication — edit in proof/ directly.
|
|
%% TODO(bob): set version and date — tie to proof corpus tag
|
|
|
|
\input{../common/preamble}
|
|
|
|
\title{StarForth Formal Verification Report\\[0.4em]
|
|
\large Isabelle/HOL Machine-Checked Proofs of Determinism and Correctness}
|
|
\author{Robert A.\ James}
|
|
\date{%% TODO(bob): set edition date
|
|
}
|
|
|
|
\begin{document}
|
|
\frontmatter
|
|
\maketitle
|
|
\tableofcontents
|
|
|
|
\mainmatter
|
|
|
|
%%────────────────────────────────────────────────
|
|
%% Part I — Foundations
|
|
%%────────────────────────────────────────────────
|
|
\part{Foundations}
|
|
|
|
\chapter{Verification Methodology}
|
|
%% SOURCE: docs/working/architecture/VM_FORMALIZATION_PLAN.adoc
|
|
%% TODO(bob): promote the formalization plan — scope, tool chain, proof obligations.
|
|
|
|
\chapter{Base Definitions and Type System}
|
|
%% SOURCE: proof/StarForth_Base.thy
|
|
%% TODO(bob): extract key definitions and theorem statements from StarForth_Base.thy.
|
|
%% Include: VM state type, stack type, dictionary type, vaddr_t model.
|
|
|
|
%%────────────────────────────────────────────────
|
|
%% Part II — The Seven Feedback Loops
|
|
%%────────────────────────────────────────────────
|
|
\part{The Seven Feedback Loops}
|
|
|
|
\chapter{Loop 1 — Execution Heat}
|
|
%% SOURCE: proof/StarForth_Loop1_Heat.thy
|
|
%% TODO(bob): key theorem: heat is monotone non-negative; decay is bounded.
|
|
%% %% TODO(bob): PATENT — execution heat tracking is patent-adjacent.
|
|
|
|
\chapter{Loop 2 — Rolling Window of Truth}
|
|
%% SOURCE: proof/StarForth_Loop2_Window.thy
|
|
%% TODO(bob): key theorem: circular buffer preserves ordering; snapshot is consistent.
|
|
|
|
\chapter{Loop 3 — Linear Decay}
|
|
%% SOURCE: proof/StarForth_Loop3_Decay.thy
|
|
%% TODO(bob): key theorem: decay converges to zero in finite steps.
|
|
|
|
\chapter{Loop 4 — Pipelining and Prefetch}
|
|
%% SOURCE: proof/StarForth_Loop4_Pipeline.thy
|
|
%% TODO(bob): key theorem: prefetch accuracy is a non-decreasing function of history.
|
|
|
|
\chapter{Loop 5 — Window Width Inference}
|
|
%% SOURCE: proof/StarForth_Loop5_WinInf.thy
|
|
%% TODO(bob): key theorem: Levene's test terminates; binary chop converges.
|
|
|
|
\chapter{Loop 6 — Decay Slope Inference}
|
|
%% SOURCE: proof/StarForth_Loop6_DecayInf.thy
|
|
%% TODO(bob): key theorem: exponential regression produces bounded slope estimate.
|
|
|
|
\chapter{Loop 7 — Adaptive Heartrate}
|
|
%% SOURCE: proof/StarForth_Loop7_Heartrate.thy
|
|
%% TODO(bob): key theorem: heartrate stabilizes in finite time (steady-state convergence).
|
|
|
|
%%────────────────────────────────────────────────
|
|
%% Part III — Word Category Proofs
|
|
%%────────────────────────────────────────────────
|
|
\part{Word Category Correctness}
|
|
|
|
\chapter{Arithmetic Words}
|
|
%% SOURCE: proof/StarForth_Arithmetic_Words.thy
|
|
%% TODO(bob): key theorems for +, -, *, /, MOD, ABS, MIN, MAX.
|
|
|
|
\chapter{Stack Words}
|
|
%% SOURCE: proof/StarForth_Stack_Words.thy
|
|
%% TODO(bob): key theorems for DUP, DROP, SWAP, ROT, OVER, NIP, TUCK.
|
|
|
|
\chapter{Logical Words}
|
|
%% SOURCE: proof/StarForth_Logical_Words.thy
|
|
%% TODO(bob): key theorems for AND, OR, XOR, INVERT, LSHIFT, RSHIFT.
|
|
|
|
\chapter{Memory Words}
|
|
%% SOURCE: proof/StarForth_Memory_Words.thy
|
|
%% TODO(bob): key theorems for @, !, C@, C!, MOVE, FILL — memory safety.
|
|
|
|
\chapter{Return Stack Words}
|
|
%% SOURCE: proof/StarForth_Return_Stack_Words.thy
|
|
%% TODO(bob): key theorems for >R, R>, R@, RDROP — return stack discipline.
|
|
|
|
\chapter{Q48.16 Fixed-Point Arithmetic}
|
|
%% SOURCE: proof/StarForth_Q48_16.thy
|
|
%% TODO(bob): key theorems — overflow bounds, rounding correctness.
|
|
|
|
%%────────────────────────────────────────────────
|
|
%% Part IV — System-Level Proofs
|
|
%%────────────────────────────────────────────────
|
|
\part{System-Level Proofs}
|
|
|
|
\chapter{Overall Correctness}
|
|
%% SOURCE: proof/StarForth_Correctness.thy
|
|
%% TODO(bob): top-level correctness theorem — determinism across 90 runs.
|
|
|
|
\chapter{State Transitions}
|
|
%% SOURCE: proof/StarForth_Transition.thy
|
|
%% TODO(bob): state transition relation, reachability, invariant preservation.
|
|
|
|
\chapter{Concurrency Properties}
|
|
%% SOURCE: proof/StarForth_Concurrent.thy
|
|
%% TODO(bob): concurrency properties — heartbeat thread non-interference.
|
|
|
|
\chapter{Mutual Exclusion}
|
|
%% SOURCE: proof/StarForth_Mutex.thy
|
|
%% TODO(bob): mutex correctness — heartbeat + interpreter isolation.
|
|
|
|
%%────────────────────────────────────────────────
|
|
%% Part V — Word-Level ACL Proofs
|
|
%%────────────────────────────────────────────────
|
|
\part{Word-Level ACL Proofs}
|
|
|
|
\chapter{Pin Monotonicity}
|
|
%% SOURCE: proof/ACL_Pin_Monotone.thy
|
|
%% TODO(bob): ACL-PIN is one-way: once pinned, cannot be un-pinned.
|
|
%% %% TODO(bob): PATENT — pin mechanism is patent-adjacent.
|
|
|
|
\chapter{Inheritance Clears Pin}
|
|
%% SOURCE: proof/ACL_Inherit_Clears_Pin.thy
|
|
%% TODO(bob): inheritance protocol — pin is not propagated to child words.
|
|
|
|
\chapter{TTL Boundedness}
|
|
%% SOURCE: proof/ACL_TTL_Bounded.thy
|
|
%% TODO(bob): TTL counter is bounded and decreases monotonically.
|
|
|
|
\chapter{Emergency Bypass}
|
|
%% SOURCE: proof/ACL_Emergency_Bypass.thy
|
|
%% TODO(bob): emergency console bypass — sound under fault handler activation.
|
|
|
|
\chapter{No Privilege Escalation}
|
|
%% SOURCE: proof/ACL_No_Escalation.thy
|
|
%% TODO(bob): no unprivileged word can escalate to zuse privilege.
|
|
|
|
%%────────────────────────────────────────────────
|
|
%% Appendices
|
|
%%────────────────────────────────────────────────
|
|
\appendix
|
|
|
|
\chapter{Theory File Inventory}
|
|
\label{app:proof:inventory}
|
|
|
|
\begin{table}[ht]
|
|
\centering
|
|
\caption{Isabelle/HOL theory files (24 total)}
|
|
\label{tab:proof:inventory}
|
|
\begin{tabular}{ll}
|
|
\toprule
|
|
Theory file & Coverage \\
|
|
\midrule
|
|
\texttt{StarForth\_Base.thy} & Base definitions, type system \\
|
|
\texttt{StarForth\_Loop1\_Heat.thy} & Execution heat (Loop 1) \\
|
|
\texttt{StarForth\_Loop2\_Window.thy} & Rolling window (Loop 2) \\
|
|
\texttt{StarForth\_Loop3\_Decay.thy} & Linear decay (Loop 3) \\
|
|
\texttt{StarForth\_Loop4\_Pipeline.thy} & Pipelining (Loop 4) \\
|
|
\texttt{StarForth\_Loop5\_WinInf.thy} & Window inference (Loop 5) \\
|
|
\texttt{StarForth\_Loop6\_DecayInf.thy} & Decay inference (Loop 6) \\
|
|
\texttt{StarForth\_Loop7\_Heartrate.thy} & Adaptive heartrate (Loop 7) \\
|
|
\texttt{StarForth\_Arithmetic\_Words.thy} & Arithmetic word correctness \\
|
|
\texttt{StarForth\_Stack\_Words.thy} & Stack word correctness \\
|
|
\texttt{StarForth\_Logical\_Words.thy} & Logical word correctness \\
|
|
\texttt{StarForth\_Memory\_Words.thy} & Memory word correctness \\
|
|
\texttt{StarForth\_Return\_Stack\_Words.thy} & Return stack correctness \\
|
|
\texttt{StarForth\_Q48\_16.thy} & Q48.16 fixed-point \\
|
|
\texttt{StarForth\_Correctness.thy} & Overall correctness \\
|
|
\texttt{StarForth\_Transition.thy} & State transitions \\
|
|
\texttt{StarForth\_Concurrent.thy} & Concurrency properties \\
|
|
\texttt{StarForth\_Mutex.thy} & Mutual exclusion \\
|
|
\texttt{ACL\_Pin\_Monotone.thy} & ACL pin monotonicity \\
|
|
\texttt{ACL\_Inherit\_Clears\_Pin.thy} & ACL inheritance \\
|
|
\texttt{ACL\_TTL\_Bounded.thy} & ACL TTL bounds \\
|
|
\texttt{ACL\_Emergency\_Bypass.thy} & ACL emergency bypass \\
|
|
\texttt{ACL\_No\_Escalation.thy} & ACL no escalation \\
|
|
\texttt{ROOT} & Isabelle session manifest \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\end{table}
|
|
|
|
\chapter{Building and Checking Proofs}
|
|
%% TODO(bob): build instructions — isabelle build -D proof/
|
|
%% Expected output: all 23 theories check in < N minutes.
|
|
|
|
\backmatter
|
|
\bibliographystyle{plainnat}
|
|
\bibliography{../common/starship}
|
|
|
|
\end{document}
|