oxiz_proof/
logging.rs

1//! Proof step logging to persistent binary log files.
2//!
3//! `ProofLogger` streams proof steps to disk in a compact binary format during
4//! solving.  The resulting log file can later be read by `ProofReplayer` in
5//! `crate::replay` for offline verification.
6//!
7//! # Binary Format
8//!
9//! Each log file begins with a fixed-size header, followed by zero or more
10//! *records*.  Every record encodes one `ProofStep`:
11//!
12//! ```text
13//! ┌──────────────────── FILE HEADER (32 bytes) ─────────────────────┐
14//! │ magic: [u8; 8]  = b"OXIZPROF"                                   │
15//! │ version: u32    = FORMAT_VERSION                                 │
16//! │ flags: u32      = 0 (reserved)                                   │
17//! │ reserved: [u8; 16]                                               │
18//! └─────────────────────────────────────────────────────────────────┘
19//!
20//! ┌──────────────── RECORD (variable length) ───────────────────────┐
21//! │ kind: u8        = 0 (Axiom) | 1 (Inference)                     │
22//! │ node_id: u32    (little-endian)                                  │
23//! │ conclusion_len: u32                                              │
24//! │ conclusion: [u8; conclusion_len]  (UTF-8)                        │
25//! │  ── if kind == Inference ──────────────────────────────────────  │
26//! │ rule_len: u32                                                    │
27//! │ rule: [u8; rule_len]             (UTF-8)                         │
28//! │ premise_count: u32                                               │
29//! │ premises: [u32; premise_count]   (node IDs, little-endian)      │
30//! │ arg_count: u32                                                   │
31//! │ for each arg:                                                    │
32//! │   arg_len: u32 + arg: [u8; arg_len]                              │
33//! └─────────────────────────────────────────────────────────────────┘
34//! ```
35
36use std::fs::{File, OpenOptions};
37use std::io::{self, BufWriter, Write};
38use std::path::{Path, PathBuf};
39
40use thiserror::Error;
41
42use crate::proof::{ProofNodeId, ProofStep};
43
44/// Magic bytes at the start of every OxiZ proof log.
45const MAGIC: &[u8; 8] = b"OXIZPROF";
46
47/// Current binary format version.
48const FORMAT_VERSION: u32 = 1;
49
50/// Record kind byte for `ProofStep::Axiom`.
51const KIND_AXIOM: u8 = 0;
52
53/// Record kind byte for `ProofStep::Inference`.
54const KIND_INFERENCE: u8 = 1;
55
56/// Errors produced by `ProofLogger`.
57#[derive(Error, Debug)]
58pub enum LoggingError {
59    /// Underlying I/O failure.
60    #[error("I/O error while logging proof: {0}")]
61    Io(#[from] io::Error),
62
63    /// Attempted to log a step after the logger has been closed.
64    #[error("attempted to write to a closed ProofLogger")]
65    AlreadyClosed,
66}
67
68/// Result type for logging operations.
69pub type LoggingResult<T> = Result<T, LoggingError>;
70
71/// Streams proof steps to a binary log file during solving.
72///
73/// # Examples
74///
75/// ```no_run
76/// use std::path::Path;
77/// use oxiz_proof::logging::ProofLogger;
78/// use oxiz_proof::proof::{ProofStep, ProofNodeId};
79///
80/// let mut logger = ProofLogger::create(Path::new("/tmp/proof.oxizlog"))
81///     .expect("failed to create log");
82///
83/// logger.log_step(ProofNodeId(0), &ProofStep::Axiom {
84///     conclusion: "true".to_string(),
85/// }).expect("failed to log step");
86///
87/// logger.close().expect("failed to close log");
88/// ```
89pub struct ProofLogger {
90    /// Buffered writer to the log file.
91    writer: Option<BufWriter<File>>,
92    /// Path to the log file (kept for diagnostics).
93    path: PathBuf,
94    /// Number of steps written so far.
95    step_count: u64,
96}
97
98impl ProofLogger {
99    /// Create a new proof log at `path`, overwriting any existing file.
100    ///
101    /// Writes the file header immediately.
102    pub fn create(path: &Path) -> LoggingResult<Self> {
103        let file = File::create(path)?;
104        let mut writer = BufWriter::new(file);
105        write_header(&mut writer)?;
106        writer.flush()?;
107
108        Ok(Self {
109            writer: Some(writer),
110            path: path.to_path_buf(),
111            step_count: 0,
112        })
113    }
114
115    /// Open an existing proof log for appending.
116    ///
117    /// Does **not** write a new header; the file must already have a valid header
118    /// written by a previous `ProofLogger::create` call.
119    pub fn append(path: &Path) -> LoggingResult<Self> {
120        let file = OpenOptions::new().append(true).open(path)?;
121        let writer = BufWriter::new(file);
122
123        Ok(Self {
124            writer: Some(writer),
125            path: path.to_path_buf(),
126            step_count: 0,
127        })
128    }
129
130    /// Append a single `ProofStep` to the log.
131    ///
132    /// `node_id` is the `ProofNodeId` assigned to this step in the live proof
133    /// DAG; it is recorded so that cross-references in `Inference` premises can
134    /// be resolved during replay.
135    ///
136    /// # Errors
137    ///
138    /// Returns `LoggingError::AlreadyClosed` if called after `close()`.
139    pub fn log_step(&mut self, node_id: ProofNodeId, step: &ProofStep) -> LoggingResult<()> {
140        let writer = self.writer.as_mut().ok_or(LoggingError::AlreadyClosed)?;
141
142        write_step(writer, node_id, step)?;
143        self.step_count += 1;
144        Ok(())
145    }
146
147    /// Flush the internal write buffer to the OS.
148    ///
149    /// Under normal operation you do not need to call this explicitly;
150    /// `close()` flushes before closing.  Call `flush()` for crash-safety
151    /// checkpointing during long-running solves.
152    pub fn flush(&mut self) -> LoggingResult<()> {
153        if let Some(ref mut w) = self.writer {
154            w.flush()?;
155        }
156        Ok(())
157    }
158
159    /// Flush and close the log file.
160    ///
161    /// After this call, further `log_step` calls will return
162    /// `LoggingError::AlreadyClosed`.
163    pub fn close(&mut self) -> LoggingResult<()> {
164        if let Some(mut writer) = self.writer.take() {
165            writer.flush()?;
166        }
167        Ok(())
168    }
169
170    /// Return the number of proof steps written since this logger was created.
171    #[must_use]
172    pub fn step_count(&self) -> u64 {
173        self.step_count
174    }
175
176    /// Return the path of the log file.
177    #[must_use]
178    pub fn path(&self) -> &Path {
179        &self.path
180    }
181
182    /// Return `true` if the logger has been closed.
183    #[must_use]
184    pub fn is_closed(&self) -> bool {
185        self.writer.is_none()
186    }
187}
188
189impl Drop for ProofLogger {
190    fn drop(&mut self) {
191        // Best-effort flush on drop; ignore errors since we can't propagate.
192        if let Some(ref mut w) = self.writer {
193            let _ = w.flush();
194        }
195    }
196}
197
198// ──────────────────────────────── helpers ────────────────────────────────────
199
200/// Write the 32-byte file header.
201fn write_header<W: Write>(w: &mut W) -> io::Result<()> {
202    w.write_all(MAGIC)?;
203    w.write_all(&FORMAT_VERSION.to_le_bytes())?;
204    // flags (reserved)
205    w.write_all(&0u32.to_le_bytes())?;
206    // 16 reserved bytes
207    w.write_all(&[0u8; 16])?;
208    Ok(())
209}
210
211/// Encode and write one proof step record.
212fn write_step<W: Write>(w: &mut W, node_id: ProofNodeId, step: &ProofStep) -> io::Result<()> {
213    match step {
214        ProofStep::Axiom { conclusion } => {
215            w.write_all(&[KIND_AXIOM])?;
216            w.write_all(&node_id.0.to_le_bytes())?;
217            write_bytes(w, conclusion.as_bytes())?;
218        }
219        ProofStep::Inference {
220            rule,
221            premises,
222            conclusion,
223            args,
224        } => {
225            w.write_all(&[KIND_INFERENCE])?;
226            w.write_all(&node_id.0.to_le_bytes())?;
227            write_bytes(w, conclusion.as_bytes())?;
228            write_bytes(w, rule.as_bytes())?;
229
230            // premises
231            let premise_count = premises.len() as u32;
232            w.write_all(&premise_count.to_le_bytes())?;
233            for p in premises.iter() {
234                w.write_all(&p.0.to_le_bytes())?;
235            }
236
237            // args
238            let arg_count = args.len() as u32;
239            w.write_all(&arg_count.to_le_bytes())?;
240            for arg in args.iter() {
241                write_bytes(w, arg.as_bytes())?;
242            }
243        }
244    }
245    Ok(())
246}
247
248/// Write a length-prefixed byte slice (u32 LE length + data).
249fn write_bytes<W: Write>(w: &mut W, data: &[u8]) -> io::Result<()> {
250    let len = data.len() as u32;
251    w.write_all(&len.to_le_bytes())?;
252    w.write_all(data)?;
253    Ok(())
254}
255
256#[cfg(test)]
257mod tests {
258    use super::*;
259    use crate::proof::{ProofNodeId, ProofStep};
260    use smallvec::SmallVec;
261
262    fn temp_log_path(name: &str) -> PathBuf {
263        std::env::temp_dir().join(format!("oxiz_proof_log_{}.oxizlog", name))
264    }
265
266    #[test]
267    fn test_create_and_close() {
268        let path = temp_log_path("create_close");
269        let _ = std::fs::remove_file(&path);
270
271        let mut logger = ProofLogger::create(&path).expect("create failed");
272        assert!(!logger.is_closed());
273        logger.close().expect("close failed");
274        assert!(logger.is_closed());
275        assert!(path.exists());
276
277        let _ = std::fs::remove_file(&path);
278    }
279
280    #[test]
281    fn test_log_axiom() {
282        let path = temp_log_path("log_axiom");
283        let _ = std::fs::remove_file(&path);
284
285        let mut logger = ProofLogger::create(&path).expect("create failed");
286        let step = ProofStep::Axiom {
287            conclusion: "(assert (= x 0))".to_string(),
288        };
289        logger.log_step(ProofNodeId(0), &step).expect("log failed");
290        logger.close().expect("close failed");
291
292        assert!(path.metadata().expect("stat failed").len() > 32);
293
294        let _ = std::fs::remove_file(&path);
295    }
296
297    #[test]
298    fn test_log_inference() {
299        let path = temp_log_path("log_inference");
300        let _ = std::fs::remove_file(&path);
301
302        let mut logger = ProofLogger::create(&path).expect("create failed");
303
304        let axiom = ProofStep::Axiom {
305            conclusion: "p".to_string(),
306        };
307        logger.log_step(ProofNodeId(0), &axiom).expect("log failed");
308
309        let inference = ProofStep::Inference {
310            rule: "mp".to_string(),
311            premises: SmallVec::from_vec(vec![ProofNodeId(0)]),
312            conclusion: "q".to_string(),
313            args: SmallVec::new(),
314        };
315        logger
316            .log_step(ProofNodeId(1), &inference)
317            .expect("log failed");
318
319        assert_eq!(logger.step_count(), 2);
320        logger.close().expect("close failed");
321
322        let _ = std::fs::remove_file(&path);
323    }
324
325    #[test]
326    fn test_write_after_close_fails() {
327        let path = temp_log_path("after_close");
328        let _ = std::fs::remove_file(&path);
329
330        let mut logger = ProofLogger::create(&path).expect("create failed");
331        logger.close().expect("close failed");
332
333        let step = ProofStep::Axiom {
334            conclusion: "p".to_string(),
335        };
336        let result = logger.log_step(ProofNodeId(0), &step);
337        assert!(matches!(result, Err(LoggingError::AlreadyClosed)));
338
339        let _ = std::fs::remove_file(&path);
340    }
341}
oxiz_proof/logging.rs

oxiz_proof/
logging.rs
