paper(patch-bridge): qualify proof and evaluation claims for publication

- Abstract: machine-checked soundness/impossibility proofs → Idris2
  proof obligations (templates; full mechanisation is future work);
  73% → "substantially reduces" (figure retained in body with caveat)
- Classification body: downgrade "machine-checked" to "Idris2 proof
  obligation" for Mitigable and Unmitigable categories
- Evaluation: add explicit limitations paragraph noting the 73.2%
  figure is single-study and dataset-specific; not a general baseline

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

Author: hyperpolymath

arcvix-patch-bridge-cve-lifecycle.tex

@@ -114,17 +114,17 @@
 (2)~\emph{contextual taint analysis via miniKanren}, which determines
 whether a vulnerability class is actually reachable through
 source-to-sink data flow tracking in the developer's code; and
-(3)~\emph{three-way mitigation classification with formal proofs in
-Idris2}, where every CVE is classified as \textsc{Mitigable} (with a
-machine-checked soundness proof), \textsc{Unmitigable} (with a proof
-that no candidate mitigation preserves application behaviour while
-preventing exploitation), or \textsc{Concatenative} (where individually
-insufficient mitigations compose to become sufficient, verified by a
-compositional proof). Integrated as a pre-commit hook via the
-\texttt{assail} subcommand, \textsc{Patch Bridge} reduces false positive
-rates by 73\% through contextual reachability filtering while providing
-the first formally verified mitigation lifecycle for software supply
-chain vulnerabilities. Our implementation is open-source, written in Rust
+(3)~\emph{three-way mitigation classification with formal proof structure
+in Idris2}, where every CVE is classified as \textsc{Mitigable} (with an
+Idris2 proof obligation attesting mitigation soundness), \textsc{Unmitigable}
+(with a proof obligation that no candidate mitigation preserves application
+behaviour while preventing exploitation), or \textsc{Concatenative} (where
+individually insufficient mitigations compose to become sufficient, supported
+by a compositional argument). Integrated as a pre-commit hook via the
+\texttt{assail} subcommand, \textsc{Patch Bridge} substantially reduces
+false positive rates through contextual reachability filtering, providing
+the first formally structured mitigation lifecycle for software supply
+chain vulnerabilities with machine-checkable proof templates. Our implementation is open-source, written in Rust
 with an embedded miniKanren engine and Idris2 proof obligations.
 \end{abstract}
 
@@ -620,13 +620,15 @@ \subsection{Classification Categories}
     prevent exploitation, while preserving the application's required
     behaviour. Examples include input validation, sandboxing, feature
     disabling, configuration changes, and drop-in replacements from
-    verified repositories. The classification carries a
-    \emph{machine-checked soundness proof}.
+    verified repositories. The classification carries an
+    \emph{Idris2 proof obligation} (a proof template that is checked by
+    the Idris2 type checker; full mechanised closure is future work).
   \item[\textsc{Unmitigable}.] No feasible mitigation exists given the
     application's constraints. The vulnerability is reachable,
     exploitable, and every candidate mitigation either fails to prevent
     exploitation or breaks required application behaviour. The
-    classification carries a \emph{machine-checked impossibility proof}.
+    classification carries an \emph{Idris2 impossibility argument}
+    (proof template; full mechanisation is future work).
     The recommended actions are: replace the dependency, rearchitect
     the affected component, or accept the risk with documented
     justification.
@@ -1306,12 +1308,19 @@ \subsection{False Positive Reduction}
 additional 55.1\% by determining that the vulnerable code paths are
 not reachable from any untrusted input source.
 
-The combined 73.2\% reduction transforms the developer's experience
-from ``127 CVEs to investigate'' to ``34 CVEs that actually matter
-in my code.'' Manual verification of the filtered CVEs confirmed
+The combined 73.2\% reduction in this study transforms the developer's
+experience from ``127 CVEs to investigate'' to ``34 CVEs that actually
+matter in my code.'' Manual verification of the filtered CVEs confirmed
 zero true positives among the filtered set---all 93 removed CVEs were
 genuinely unreachable in their respective projects.
 
+\textbf{Limitations of this evaluation.}  This result is from a single
+study across a small set of projects; the 73.2\% figure is
+dataset-specific and should not be generalised without broader empirical
+validation.  The methodology (project selection, scanner configuration,
+manual verification procedure) is described below and should be
+replicated before the figure is treated as a general-case baseline.
+
 \subsection{Classification Breakdown}
 
 Of the 34 contextually reachable CVEs: