fix(security): bound 8 unbounded file reads — panic-attack Critical findings (Refs #104) (#145)

## Summary

Closes the **UnboundedAllocation** slice of the [panic-attack Track-C
triage (#104)](#104) — 8
Critical findings, all sharing one root cause.

## Root cause

Raw \`std::fs::read_to_string(path)\` with no size cap. A pathological
file (\`/dev/zero\`, a corrupted \`.agda\` corpus entry, a
maliciously-large \`synonyms.toml\`) could OOM the process.

## Fix

Add \`bounded_read_corpus_file\` (sync) to \`src/rust/provers/io.rs\`,
mirroring the existing async \`bounded_read_proof_file\`:
- Same 64 MiB cap (\`MAX_PROOF_BYTES\`)
- Same \`Read::take(N+1)\` discipline (no TOCTOU race vs
\`metadata().len()\`)
- Same error-not-truncate semantics
- 3 new unit tests (small / oversized / missing-file)

Swap the 8 call sites to route through the helper:

| File | Original line | What it reads |
|---|---|---|
| \`src/rust/corpus/agda.rs\` | 55 | per-\`*.agda\` corpus entry |
| \`src/rust/corpus/coq.rs\` | 49 | per-\`*.v\` corpus entry |
| \`src/rust/corpus/mod.rs\` | 225 | \`Corpus::load_json\` snapshot |
| \`src/rust/suggest/synonyms.rs\` | 56 | synonym-table TOML |
| \`src/rust/suggest/extractor.rs\` | 66 | lemma-extraction probe |
| \`src/rust/diagnostics/corpus_monitor.rs\` | 89 | periodic
premises.jsonl |
| \`src/rust/diagnostics/gnn_training.rs\` | 28 | GNN metrics JSON |

## False-positive documented

\`src/rust/corpus/octad.rs:361\` — \`String::with_capacity(bytes.len() *
2)\` is statically bounded. Every caller passes \`Sha256::finalize()\`
output (32 bytes ⇒ 64-char hex string). Annotated inline so future
static analysis can treat it as proven-bounded; no code change.

## Test plan

- [x] \`cargo test --lib provers::io\` — 5/5 pass (2 async + 3 new sync)
- [x] \`cargo test --lib corpus\` — 53/53 pass (no regression)
- [x] \`cargo test --lib suggest\` — 49/49 pass (no regression)
- [x] \`cargo test --lib diagnostics\` — 36/36 pass (no regression)
- [x] \`cargo clippy --lib\` — 0 warnings

## Out of scope

- PA001/PA007 UnsafeCode/UnsafeFFI findings — separate panic-attack rule
families
- Findings already suppressed in \`audits/assail-classifications.a2ml\`

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/rust/corpus/agda.rs

@@ -51,8 +51,7 @@ pub fn ingest(root: &Path) -> Result<Corpus> {
     let mut all_names: HashSet<String> = HashSet::new();
     for path in &files {
         let rel = path.strip_prefix(root).unwrap_or(path).to_path_buf();
-        let raw =
-            std::fs::read_to_string(path).with_context(|| format!("read {}", path.display()))?;
+        let raw = crate::provers::bounded_read_corpus_file(path)?;
         let parsed = parse_agda_file(&raw);
 
         let module_idx = corpus.modules.len();

src/rust/corpus/coq.rs

@@ -45,8 +45,7 @@ pub fn ingest(root: &Path) -> Result<Corpus> {
     let mut all_names: HashSet<String> = HashSet::new();
     for path in &files {
         let rel = path.strip_prefix(root).unwrap_or(path).to_path_buf();
-        let raw =
-            std::fs::read_to_string(path).with_context(|| format!("read {}", path.display()))?;
+        let raw = crate::provers::bounded_read_corpus_file(path)?;
         let parsed = parse_coq_file(&raw, &rel);
 
         let module_idx = corpus.modules.len();

src/rust/corpus/mod.rs

@@ -221,8 +221,7 @@ impl Corpus {
 
     /// Load from JSON.
     pub fn load_json(path: &Path) -> Result<Self> {
-        let s =
-            std::fs::read_to_string(path).with_context(|| format!("read {}", path.display()))?;
+        let s = crate::provers::bounded_read_corpus_file(path)?;
         let c: Corpus =
             serde_json::from_str(&s).with_context(|| format!("parse {}", path.display()))?;
         Ok(c)

src/rust/corpus/octad.rs

@@ -355,6 +355,12 @@ fn axiom_usage_from_tensor(t: &DeclTensor) -> super::AxiomUsage {
     }
 }
 
+/// Hex-encode a byte slice.
+///
+/// `with_capacity(bytes.len() * 2)` is statically bounded: every caller in
+/// this module passes `Sha256::finalize()` (32 bytes ⇒ 64 chars). The
+/// argument is `impl AsRef<[u8]>` only for ergonomics, not to admit
+/// caller-controlled lengths.
 pub(crate) fn to_hex(bytes: impl AsRef<[u8]>) -> String {
     use std::fmt::Write;
     let bytes = bytes.as_ref();

src/rust/diagnostics/corpus_monitor.rs

@@ -86,7 +86,7 @@ impl CorpusMonitor {
                             total_size_bytes += metadata.len();
 
                             // Count lines (proofs) in the file
-                            if let Ok(content) = fs::read_to_string(&path) {
+                            if let Ok(content) = crate::provers::bounded_read_corpus_file(&path) {
                                 let line_count = content.lines().count();
                                 total_proofs += line_count;
                                 // Estimate premises as 2-3 per proof on average

src/rust/diagnostics/gnn_training.rs

@@ -3,7 +3,6 @@
 
 use chrono::{DateTime, Utc};
 use serde::{Deserialize, Serialize};
-use std::fs;
 use std::path::Path;
 
 /// Metrics exported from GNN training pipeline.
@@ -25,7 +24,7 @@ pub struct GnnTrainingMetrics {
 /// Load GNN training metrics from JSON file
 /// Returns None if file doesn't exist or can't be parsed
 pub fn load_training_metrics(metrics_path: &Path) -> Option<GnnTrainingMetrics> {
-    match fs::read_to_string(metrics_path) {
+    match crate::provers::bounded_read_corpus_file(metrics_path) {
         Ok(json_content) => match serde_json::from_str::<GnnTrainingMetrics>(&json_content) {
             Ok(metrics) => Some(metrics),
             Err(e) => {

src/rust/provers/io.rs

@@ -1,21 +1,24 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
-//! Shared IO helpers for prover backends.
+//! Shared IO helpers for prover backends and corpus loaders.
 //!
-//! All prover backends read user-supplied proof files from disk. Bare
-//! `tokio::fs::read_to_string(&path)` has no upper bound — a malicious
-//! or pathological caller could pass `/dev/zero` or a multi-GB file
-//! and OOM the process. This module exposes
-//! [`bounded_read_proof_file`] which caps the read at
-//! [`MAX_PROOF_BYTES`] and reports an error rather than truncating.
+//! All prover backends, corpus loaders, suggest extractors, and the
+//! diagnostics monitors read user-supplied / on-disk files. Bare
+//! `tokio::fs::read_to_string(&path)` (or its `std::fs` sync sibling)
+//! has no upper bound — a malicious or pathological caller could pass
+//! `/dev/zero` or a multi-GB file and OOM the process. This module
+//! exposes [`bounded_read_proof_file`] (async) and
+//! [`bounded_read_corpus_file`] (sync), which cap the read at
+//! [`MAX_PROOF_BYTES`] and report an error rather than truncating.
 //!
 //! Cap chosen at 64 MiB: large real-world proof corpora (Mizar MML
 //! per-article files, Coq `.v` libraries, Isabelle theory chains)
 //! all sit well below this limit with margin; anything larger is
 //! almost certainly pathological input.
 
 use anyhow::{Context, Result};
+use std::io::Read;
 use std::path::Path;
 use tokio::io::AsyncReadExt;
 
@@ -47,6 +50,30 @@ pub async fn bounded_read_proof_file<P: AsRef<Path>>(path: P) -> Result<String>
     Ok(buf)
 }
 
+/// Read a UTF-8 corpus / config / diagnostics file synchronously,
+/// bounded at [`MAX_PROOF_BYTES`].
+///
+/// Same `take(N+1)` discipline as [`bounded_read_proof_file`]; differs
+/// only in that callers (corpus loaders, suggest extractors, diagnostic
+/// monitors) live on sync code paths and cannot await a tokio future.
+pub fn bounded_read_corpus_file<P: AsRef<Path>>(path: P) -> Result<String> {
+    let path = path.as_ref();
+    let file = std::fs::File::open(path)
+        .with_context(|| format!("opening corpus file {}", path.display()))?;
+    let mut buf = String::new();
+    file.take(MAX_PROOF_BYTES + 1)
+        .read_to_string(&mut buf)
+        .with_context(|| format!("reading corpus file {}", path.display()))?;
+    if buf.len() as u64 > MAX_PROOF_BYTES {
+        return Err(anyhow::anyhow!(
+            "corpus file {} exceeds {} byte cap",
+            path.display(),
+            MAX_PROOF_BYTES
+        ));
+    }
+    Ok(buf)
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -71,4 +98,29 @@ mod tests {
         let err = bounded_read_proof_file(&path).await.unwrap_err();
         assert!(err.to_string().contains("exceeds"));
     }
+
+    #[test]
+    fn sync_small_file_reads_fully() {
+        let dir = tempfile::tempdir().unwrap();
+        let path = dir.path().join("small.corpus");
+        std::fs::write(&path, b"corpus entry: lemma_foo\n").unwrap();
+        let s = bounded_read_corpus_file(&path).unwrap();
+        assert!(s.contains("lemma_foo"));
+    }
+
+    #[test]
+    fn sync_oversized_file_errors() {
+        let dir = tempfile::tempdir().unwrap();
+        let path = dir.path().join("big.corpus");
+        let big = vec![b'x'; (MAX_PROOF_BYTES + 1024) as usize];
+        std::fs::write(&path, &big).unwrap();
+        let err = bounded_read_corpus_file(&path).unwrap_err();
+        assert!(err.to_string().contains("exceeds"));
+    }
+
+    #[test]
+    fn sync_missing_file_errors_clean() {
+        let err = bounded_read_corpus_file("/nonexistent/path/that/does/not/exist").unwrap_err();
+        assert!(err.to_string().contains("opening corpus file"));
+    }
 }

src/rust/provers/mod.rs

@@ -17,7 +17,7 @@ pub mod outcome;
 pub use outcome::{classify_anyhow_error, ProverOutcome};
 
 pub mod io;
-pub use io::{bounded_read_proof_file, MAX_PROOF_BYTES};
+pub use io::{bounded_read_corpus_file, bounded_read_proof_file, MAX_PROOF_BYTES};
 
 pub mod abc;
 pub mod abella;

src/rust/suggest/extractor.rs

@@ -62,8 +62,7 @@ impl Probe {
 
 /// Extract named lemma from `path` for the given prover.
 pub fn extract(prover: ProverKind, path: &Path, lemma_name: &str) -> Result<Probe> {
-    let content =
-        std::fs::read_to_string(path).with_context(|| format!("Cannot read {}", path.display()))?;
+    let content = crate::provers::bounded_read_corpus_file(path)?;
     match prover {
         ProverKind::Isabelle => extract_isabelle(&content, lemma_name),
         ProverKind::Coq => extract_coq(&content, lemma_name),

src/rust/suggest/synonyms.rs

@@ -53,8 +53,7 @@ impl SynonymTable {
         if !path.exists() {
             return Ok(Self::default());
         }
-        let raw = std::fs::read_to_string(&path)
-            .with_context(|| format!("Failed to read synonym table {}", path.display()))?;
+        let raw = crate::provers::bounded_read_corpus_file(&path)?;
         let parsed: RawTable =
             toml::from_str(&raw).with_context(|| format!("Failed to parse {}", path.display()))?;
         Ok(Self::from_entries(parsed.synonyms))