oxiz_proof/
recorder.rs

1//! Generic proof step recorder.
2//!
3//! This module provides a lightweight recorder over the core [`Proof`] DAG.
4//! The existing incremental recorder remains available in [`crate::incremental`].
5
6use crate::proof::{Proof, ProofNodeId, ProofStep};
7
8#[cfg(feature = "arena")]
9use bumpalo::Bump;
10#[cfg(feature = "arena")]
11use std::ptr::NonNull;
12
13/// Arena-backed proof step identifier.
14#[cfg(feature = "arena")]
15#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
16pub struct ArenaProofStepId(pub u32);
17
18/// A lightweight proof recorder over [`ProofStep`] values.
19#[derive(Debug, Default)]
20pub struct Recorder {
21    proof: Proof,
22    #[cfg(feature = "arena")]
23    arena: Bump,
24    #[cfg(feature = "arena")]
25    arena_steps: Vec<NonNull<ProofStep>>,
26}
27
28impl Recorder {
29    /// Create a new recorder.
30    #[must_use]
31    pub fn new() -> Self {
32        Self {
33            proof: Proof::new(),
34            #[cfg(feature = "arena")]
35            arena: Bump::new(),
36            #[cfg(feature = "arena")]
37            arena_steps: Vec::new(),
38        }
39    }
40
41    /// Record a proof step into the owned proof DAG.
42    pub fn record_step(&mut self, step: ProofStep) -> ProofNodeId {
43        match step {
44            ProofStep::Axiom { conclusion } => self.proof.add_axiom(conclusion),
45            ProofStep::Inference {
46                rule,
47                premises,
48                conclusion,
49                args,
50            } => self.proof.add_inference_with_args(
51                rule,
52                premises.into_vec(),
53                args.into_vec(),
54                conclusion,
55            ),
56        }
57    }
58
59    /// Return the recorded proof.
60    #[must_use]
61    pub const fn proof(&self) -> &Proof {
62        &self.proof
63    }
64
65    /// Return the recorded proof mutably.
66    pub fn proof_mut(&mut self) -> &mut Proof {
67        &mut self.proof
68    }
69
70    /// Consume the recorder and return the proof.
71    #[must_use]
72    pub fn into_proof(self) -> Proof {
73        self.proof
74    }
75
76    /// Reset the recorder state.
77    pub fn clear(&mut self) {
78        self.proof.clear();
79        #[cfg(feature = "arena")]
80        {
81            self.arena.reset();
82            self.arena_steps.clear();
83        }
84    }
85
86    /// Record a step in the bump arena and return its arena-local ID.
87    #[cfg(feature = "arena")]
88    pub fn record_step_arena(&mut self, step: ProofStep) -> Option<ArenaProofStepId> {
89        let index = u32::try_from(self.arena_steps.len()).ok()?;
90        let allocated = self.arena.alloc(step);
91        self.arena_steps.push(NonNull::from(allocated));
92        Some(ArenaProofStepId(index))
93    }
94
95    /// Fetch an arena-recorded step by ID.
96    #[cfg(feature = "arena")]
97    #[must_use]
98    pub fn get(&self, id: ArenaProofStepId) -> Option<&ProofStep> {
99        self.arena_steps.get(id.0 as usize).map(|ptr| {
100            // SAFETY: pointers come from `self.arena.alloc` and stay valid until reset/drop.
101            unsafe { ptr.as_ref() }
102        })
103    }
104}
105
106#[cfg(all(test, feature = "arena"))]
107mod arena_tests {
108    use super::*;
109    use crate::validation::FormatValidator;
110    use smallvec::SmallVec;
111
112    #[test]
113    fn arena_recorded_proof_passes_checker() {
114        let mut recorder = Recorder::new();
115
116        let left = recorder.record_step(ProofStep::Axiom {
117            conclusion: "p".to_string(),
118        });
119        let right = recorder.record_step(ProofStep::Axiom {
120            conclusion: "q".to_string(),
121        });
122
123        let arena_id = recorder.record_step_arena(ProofStep::Inference {
124            rule: "and_intro".to_string(),
125            premises: SmallVec::from_vec(vec![left, right]),
126            conclusion: "(and p q)".to_string(),
127            args: SmallVec::new(),
128        });
129        assert!(arena_id.is_some());
130
131        recorder.record_step(ProofStep::Inference {
132            rule: "and_intro".to_string(),
133            premises: SmallVec::from_vec(vec![left, right]),
134            conclusion: "(and p q)".to_string(),
135            args: SmallVec::new(),
136        });
137
138        let validator = FormatValidator::new();
139        assert!(validator.validate_proof(recorder.proof()).is_ok());
140    }
141
142    #[test]
143    fn arena_step_returns_valid_id() {
144        let mut recorder = Recorder::new();
145
146        let maybe_step_id = recorder.record_step_arena(ProofStep::Axiom {
147            conclusion: "p".to_string(),
148        });
149
150        let Some(step_id) = maybe_step_id else {
151            panic!("arena should allocate a proof step id");
152        };
153
154        match recorder.get(step_id) {
155            Some(ProofStep::Axiom { conclusion }) => assert_eq!(conclusion, "p"),
156            _ => panic!("expected arena-recorded axiom"),
157        }
158    }
159}
oxiz_proof/recorder.rs

oxiz_proof/
recorder.rs
