fix(paper): qualify abstract claims for publication safety

Four fixes to align the abstract and limitations section with reality:

1. Abstract: "machine-checkable proof that it can be reversed" →
   "proof of reversibility *in a formal abstract model*" — the Rust
   implementation is validated by property-based testing, not
   mechanically verified against the Lean/Agda/Coq model.

2. Abstract: clarified "multi-prover cross-validation" means the same
   theorems are independently proved in 6 systems (not 6 independent
   theorem families), and added parenthetical noting the Rust gap.

3. Abstract + keywords: RMO/GDPR changed from "GDPR-compliant
   irreversible deletion with proofs of non-recoverability" to
   "formally-specified mode designed for GDPR compliance (currently a
   stub; full proof is future work)" — RMO is unimplemented per
   CLAUDE.md.

4. Limitations §9: updated proof hole count from stale "10 across 8
   files: 4 gaps, 4 axioms, 2 structural" to the actual 3 obligations
   across 3 files: 1 genuine gap (OpCreateDir permissions round-trip),
   1 justified axiom (is_empty_dir_dec decidability), 1 standard axiom
   (funext in Agda, consistent with cubical).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

arcvix-formally-verified-reversible-shell.tex

@@ -142,25 +142,29 @@
 A mistyped \texttt{rm -rf} can destroy months of work in milliseconds, and the
 traditional response---backups, snapshots, ``be careful''---shifts the burden of
 correctness entirely onto the human operator. We present \valence{}, an
-interactive shell in which every filesystem operation possesses a
-machine-checkable mathematical proof that it can be reversed. The core
-contribution is a \emph{reversible operation algebra} formalised in six
-independent proof assistants (\lean{}, Coq, Agda, Isabelle/HOL, Mizar, and F*),
-yielding over 200 verified theorems with multi-prover cross-validation. We
+interactive shell in which every built-in filesystem operation has a
+machine-checkable mathematical proof of reversibility \emph{in a formal
+abstract model}. The core contribution is a \emph{reversible operation algebra}
+formalised in six independent proof assistants (\lean{}, Coq, Agda,
+Isabelle/HOL, Mizar, and F*), yielding over 200 verified theorems; the same
+theorems are independently cross-validated across all six systems, providing
+confidence through prover diversity (the Rust implementation is validated by
+property-based testing, not mechanically verified against the model). We
 introduce the \emph{Mutually Assured Accountability} (\maa{}) framework, which
 decomposes shell operations into two formally distinct modes:
 \emph{Remove-Match-Reverse} (\rmr{}), providing proven undo/redo with
-transaction grouping, and \emph{Remove-Match-Obliterate} (\rmo{}), providing
-GDPR-compliant irreversible deletion with proofs of non-recoverability. We
-describe the Rust implementation (15,720 lines, 602 passing tests), the
+transaction grouping, and \emph{Remove-Match-Obliterate} (\rmo{}), a
+formally-specified irreversible deletion mode designed for GDPR compliance
+(currently a stub; full proof of non-recoverability is future work).
+We describe the Rust implementation (15,720 lines, 602 passing tests), the
 multi-prover verification strategy, and the algebraic structure---including
 Certified Null Operations (\cno{}), operation commutativity, and sequence
 composition---that makes reversibility a first-class mathematical property of
 the shell rather than an ad-hoc afterthought.
 \end{abstract}
 
 \noindent\textbf{Keywords:} formal verification, reversible computing, shell
-design, interactive systems, proof assistants, GDPR compliance, undo mechanisms
+design, interactive systems, proof assistants, undo mechanisms, GDPR (planned)
 
 % =============================================================================
 % 1. INTRODUCTION
@@ -1223,10 +1227,14 @@ \subsection{Known Limitations and Proof Gaps}
         match the model. Bridging this gap (e.g., via Creusot, Prusti, or
         Aeneas~\citep{ho2022}) is the most important future work.
 
-  \item \textbf{Proof holes}: The current proof suite contains 10 proof
-        obligations across 8 files: 4 genuine gaps requiring additional
-        lemmas, 4 stated axioms about list operations, and 2 structural
-        obligations that are trivially dischargeable.
+  \item \textbf{Proof holes}: The current proof suite contains 3 proof
+        obligations across 3 files: 1 genuine gap (Coq \texttt{filesystem\_composition.v}
+        — \texttt{OpCreateDir} permissions not preserved under round-trip in the
+        abstract model), 1 stated axiom (\texttt{is\_empty\_dir\_dec}
+        decidability in \texttt{posix\_errors.v}; justified, requires
+        finite-map refactor), and 1 standard axiom (functional extensionality
+        in Agda \texttt{FilesystemModel.agda}; consistent with cubical type
+        theory).
 
   \item \textbf{External operations}: Operations executed via
         \texttt{PATH} lookup (e.g., \texttt{gcc}, \texttt{curl}) are