holos_tda/
proof.rs

1//! Unified proof DAGs for checked persistence trajectories.
2//!
3//! `HOLOSPF` stores unique local `D V = R` nodes once and references them
4//! from each graph snapshot. The separate `holos-tda-check` crate and
5//! `holos-check` binary decode and verify this format without depending on
6//! the persistence solver.
7
8use std::collections::BTreeMap;
9use std::fmt;
10
11use sha2::{Digest, Sha256};
12
13use crate::{
14    Bar, CertificateLimits, ChangeColumn, CorrespondenceMode, PersistenceProgram, RipsParams,
15    SparseDistanceMatrix,
16};
17
18const MAGIC: &[u8; 8] = b"HOLOSPF\0";
19const VERSION: u16 = 1;
20const F64_BITS_CODEC: u8 = 1;
21
22/// Failure while producing or encoding a unified proof.
23#[derive(Debug, Clone, PartialEq, Eq)]
24pub struct ProofArtifactError {
25    message: String,
26}
27
28impl ProofArtifactError {
29    fn new(message: impl Into<String>) -> Self {
30        Self {
31            message: message.into(),
32        }
33    }
34
35    /// Description of the violated producer rule.
36    pub fn message(&self) -> &str {
37        &self.message
38    }
39}
40
41impl fmt::Display for ProofArtifactError {
42    fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
43        write!(formatter, "unified proof: {}", self.message)
44    }
45}
46
47impl std::error::Error for ProofArtifactError {}
48
49#[derive(Debug, Clone)]
50struct ProofNode {
51    digest: [u8; 32],
52    vertices: Vec<usize>,
53    edges: Vec<[usize; 2]>,
54    edge_columns: Vec<ChangeColumn>,
55    triangle_columns: Vec<ChangeColumn>,
56}
57
58impl ProofNode {
59    fn from_state(state: &crate::program::ProgramAtomState) -> Self {
60        let mut node = Self {
61            digest: [0; 32],
62            vertices: state.vertices.clone(),
63            edges: state.edges.iter().map(|edge| [edge.u, edge.v]).collect(),
64            edge_columns: state
65                .artifact
66                .reduction_certificate()
67                .edge_columns()
68                .to_vec(),
69            triangle_columns: state
70                .artifact
71                .reduction_certificate()
72                .triangle_columns()
73                .to_vec(),
74        };
75        node.digest = node.compute_digest();
76        node
77    }
78
79    fn compute_digest(&self) -> [u8; 32] {
80        let mut hash = Sha256::new();
81        hash.update(b"holos-proof-atom-v1");
82        hash.update((self.vertices.len() as u64).to_be_bytes());
83        for &vertex in &self.vertices {
84            hash.update((vertex as u64).to_be_bytes());
85        }
86        hash.update((self.edges.len() as u64).to_be_bytes());
87        for &[u, v] in &self.edges {
88            hash.update((u as u64).to_be_bytes());
89            hash.update((v as u64).to_be_bytes());
90        }
91        digest_columns(&mut hash, &self.edge_columns);
92        digest_columns(&mut hash, &self.triangle_columns);
93        hash.finalize().into()
94    }
95}
96
97#[derive(Debug, Clone)]
98struct ProofSnapshot {
99    graph: SparseDistanceMatrix,
100    atom_refs: Vec<[u8; 32]>,
101    diagram: Vec<Bar>,
102}
103
104/// Size and reuse counts for a unified proof DAG.
105#[derive(Debug, Clone, Copy, PartialEq, Eq)]
106pub struct ProofArtifactSummary {
107    /// Graph snapshots in the proof trajectory.
108    pub snapshots: usize,
109    /// Unique algebraic reduction nodes.
110    pub unique_nodes: usize,
111    /// Node references across all snapshots.
112    pub node_references: usize,
113    /// References also present in the preceding snapshot.
114    pub reused_references: usize,
115}
116
117/// Proof DAG for a program and its update trajectory.
118#[derive(Debug, Clone)]
119pub struct ProofArtifact {
120    modulus: u32,
121    threshold: Option<f64>,
122    nodes: Vec<ProofNode>,
123    snapshots: Vec<ProofSnapshot>,
124}
125
126impl ProofArtifact {
127    /// Compile an initial program and every requested update into one DAG.
128    pub fn build(
129        initial: &SparseDistanceMatrix,
130        updates: &[SparseDistanceMatrix],
131        params: &RipsParams,
132        limits: CertificateLimits,
133    ) -> Result<Self, ProofArtifactError> {
134        let mut program = PersistenceProgram::compile(initial, params, limits)
135            .map_err(|error| ProofArtifactError::new(error.to_string()))?;
136        let mut builder = ProofBuilder::new(params.modulus, params.threshold);
137        builder.push(&program)?;
138        for graph in updates {
139            program
140                .advance_with(graph, CorrespondenceMode::Omit)
141                .map_err(|error| ProofArtifactError::new(error.to_string()))?;
142            builder.push(&program)?;
143        }
144        Ok(builder.finish())
145    }
146
147    /// Capture one already compiled program.
148    pub fn from_program(program: &PersistenceProgram) -> Result<Self, ProofArtifactError> {
149        let mut builder = ProofBuilder::new(program.params().modulus, program.params().threshold);
150        builder.push(program)?;
151        Ok(builder.finish())
152    }
153
154    /// Structural size and node-reuse counts.
155    pub fn summary(&self) -> ProofArtifactSummary {
156        let node_references = self
157            .snapshots
158            .iter()
159            .map(|snapshot| snapshot.atom_refs.len())
160            .sum();
161        let mut previous = std::collections::BTreeSet::new();
162        let mut reused_references = 0usize;
163        for snapshot in &self.snapshots {
164            let current: std::collections::BTreeSet<_> =
165                snapshot.atom_refs.iter().copied().collect();
166            reused_references += current.intersection(&previous).count();
167            previous = current;
168        }
169        ProofArtifactSummary {
170            snapshots: self.snapshots.len(),
171            unique_nodes: self.nodes.len(),
172            node_references,
173            reused_references,
174        }
175    }
176
177    /// Encode the canonical `HOLOSPF` version 1 envelope.
178    pub fn encode(&self) -> Result<Vec<u8>, ProofArtifactError> {
179        let mut output = Vec::new();
180        encode_proof_header(&mut output, self)?;
181        encode_nodes(&mut output, &self.nodes)?;
182        encode_snapshots(&mut output, &self.snapshots)?;
183        Ok(output)
184    }
185}
186
187fn encode_proof_header(
188    output: &mut Vec<u8>,
189    artifact: &ProofArtifact,
190) -> Result<(), ProofArtifactError> {
191    output.extend_from_slice(MAGIC);
192    put_u16(output, VERSION);
193    output.push(F64_BITS_CODEC);
194    put_u32(output, artifact.modulus);
195    put_optional_f64(output, artifact.threshold);
196    put_usize(output, artifact.nodes.len())?;
197    put_usize(output, artifact.snapshots.len())?;
198    Ok(())
199}
200
201fn encode_nodes(output: &mut Vec<u8>, nodes: &[ProofNode]) -> Result<(), ProofArtifactError> {
202    for node in nodes {
203        encode_node(output, node)?;
204    }
205    Ok(())
206}
207
208fn encode_node(output: &mut Vec<u8>, node: &ProofNode) -> Result<(), ProofArtifactError> {
209    output.extend_from_slice(&node.digest);
210    encode_node_counts(output, node)?;
211    encode_usizes(output, &node.vertices)?;
212    encode_edges(output, &node.edges)?;
213    encode_columns(output, &node.edge_columns)?;
214    encode_columns(output, &node.triangle_columns)
215}
216
217fn encode_node_counts(output: &mut Vec<u8>, node: &ProofNode) -> Result<(), ProofArtifactError> {
218    put_usize(output, node.vertices.len())?;
219    put_usize(output, node.edges.len())?;
220    put_usize(output, node.edge_columns.len())?;
221    put_usize(output, node.triangle_columns.len())?;
222    Ok(())
223}
224
225fn encode_usizes(output: &mut Vec<u8>, values: &[usize]) -> Result<(), ProofArtifactError> {
226    for &value in values {
227        put_usize(output, value)?;
228    }
229    Ok(())
230}
231
232fn encode_edges(output: &mut Vec<u8>, edges: &[[usize; 2]]) -> Result<(), ProofArtifactError> {
233    for &[u, v] in edges {
234        put_usize(output, u)?;
235        put_usize(output, v)?;
236    }
237    Ok(())
238}
239
240fn encode_snapshots(
241    output: &mut Vec<u8>,
242    snapshots: &[ProofSnapshot],
243) -> Result<(), ProofArtifactError> {
244    for snapshot in snapshots {
245        encode_snapshot(output, snapshot)?;
246    }
247    Ok(())
248}
249
250fn encode_snapshot(
251    output: &mut Vec<u8>,
252    snapshot: &ProofSnapshot,
253) -> Result<(), ProofArtifactError> {
254    encode_snapshot_counts(output, snapshot)?;
255    encode_graph(output, &snapshot.graph)?;
256    encode_digests(output, &snapshot.atom_refs);
257    encode_diagram(output, &snapshot.diagram)
258}
259
260fn encode_snapshot_counts(
261    output: &mut Vec<u8>,
262    snapshot: &ProofSnapshot,
263) -> Result<(), ProofArtifactError> {
264    put_usize(output, snapshot.graph.len())?;
265    put_usize(output, snapshot.graph.num_edges())?;
266    put_usize(output, snapshot.atom_refs.len())?;
267    put_usize(output, snapshot.diagram.len())?;
268    Ok(())
269}
270
271fn encode_graph(
272    output: &mut Vec<u8>,
273    graph: &SparseDistanceMatrix,
274) -> Result<(), ProofArtifactError> {
275    for (u, v, value) in graph.edges() {
276        put_usize(output, u)?;
277        put_usize(output, v)?;
278        put_u64(output, value.to_bits());
279    }
280    Ok(())
281}
282
283fn encode_digests(output: &mut Vec<u8>, digests: &[[u8; 32]]) {
284    for digest in digests {
285        output.extend_from_slice(digest);
286    }
287}
288
289fn encode_diagram(output: &mut Vec<u8>, diagram: &[Bar]) -> Result<(), ProofArtifactError> {
290    for bar in diagram {
291        put_usize(output, bar.dim)?;
292        put_u64(output, bar.birth.to_bits());
293        put_u64(output, bar.death.to_bits());
294    }
295    Ok(())
296}
297
298struct ProofBuilder {
299    modulus: u32,
300    threshold: Option<f64>,
301    nodes: Vec<ProofNode>,
302    positions: BTreeMap<[u8; 32], usize>,
303    snapshots: Vec<ProofSnapshot>,
304}
305
306impl ProofBuilder {
307    fn new(modulus: u32, threshold: Option<f64>) -> Self {
308        Self {
309            modulus,
310            threshold,
311            nodes: Vec::new(),
312            positions: BTreeMap::new(),
313            snapshots: Vec::new(),
314        }
315    }
316
317    fn push(&mut self, program: &PersistenceProgram) -> Result<(), ProofArtifactError> {
318        if program.params().modulus != self.modulus
319            || program.params().threshold.map(f64::to_bits) != self.threshold.map(f64::to_bits)
320        {
321            return Err(ProofArtifactError::new(
322                "all proof snapshots must share a field and threshold",
323            ));
324        }
325        let mut atom_refs = Vec::with_capacity(program.states().len());
326        for state in program.states() {
327            let node = ProofNode::from_state(state);
328            let digest = node.digest;
329            match self.positions.get(&digest).copied() {
330                Some(position) => {
331                    if self.nodes[position].vertices != node.vertices
332                        || self.nodes[position].edges != node.edges
333                        || self.nodes[position].edge_columns != node.edge_columns
334                        || self.nodes[position].triangle_columns != node.triangle_columns
335                    {
336                        return Err(ProofArtifactError::new("reduction-node digest collision"));
337                    }
338                }
339                None => {
340                    self.positions.insert(digest, self.nodes.len());
341                    self.nodes.push(node);
342                }
343            }
344            atom_refs.push(digest);
345        }
346        self.snapshots.push(ProofSnapshot {
347            graph: program.current_graph().clone(),
348            atom_refs,
349            diagram: program.result().diagram.bars.clone(),
350        });
351        Ok(())
352    }
353
354    fn finish(self) -> ProofArtifact {
355        ProofArtifact {
356            modulus: self.modulus,
357            threshold: self.threshold,
358            nodes: self.nodes,
359            snapshots: self.snapshots,
360        }
361    }
362}
363
364fn digest_columns(hash: &mut Sha256, columns: &[ChangeColumn]) {
365    hash.update((columns.len() as u64).to_be_bytes());
366    for column in columns {
367        hash.update((column.terms.len() as u64).to_be_bytes());
368        for term in &column.terms {
369            hash.update((term.index as u64).to_be_bytes());
370            hash.update(term.coefficient.to_be_bytes());
371        }
372    }
373}
374
375fn encode_columns(
376    output: &mut Vec<u8>,
377    columns: &[ChangeColumn],
378) -> Result<(), ProofArtifactError> {
379    for column in columns {
380        put_usize(output, column.terms.len())?;
381        for term in &column.terms {
382            put_usize(output, term.index)?;
383            put_u32(output, term.coefficient);
384        }
385    }
386    Ok(())
387}
388
389fn put_u16(output: &mut Vec<u8>, value: u16) {
390    output.extend_from_slice(&value.to_be_bytes());
391}
392
393fn put_u32(output: &mut Vec<u8>, value: u32) {
394    output.extend_from_slice(&value.to_be_bytes());
395}
396
397fn put_u64(output: &mut Vec<u8>, value: u64) {
398    output.extend_from_slice(&value.to_be_bytes());
399}
400
401fn put_usize(output: &mut Vec<u8>, value: usize) -> Result<(), ProofArtifactError> {
402    let value = u64::try_from(value)
403        .map_err(|_| ProofArtifactError::new("integer does not fit the proof format"))?;
404    put_u64(output, value);
405    Ok(())
406}
407
408fn put_optional_f64(output: &mut Vec<u8>, value: Option<f64>) {
409    match value {
410        None => output.push(0),
411        Some(value) => {
412            output.push(1);
413            put_u64(output, value.to_bits());
414        }
415    }
416}
417
418#[cfg(test)]
419mod tests {
420    use super::*;
421    use crate::ProgramUpdateMode;
422
423    fn graph(offset: f64) -> SparseDistanceMatrix {
424        SparseDistanceMatrix::from_triplets(
425            7,
426            &[
427                (0, 1, 1.0 + offset),
428                (1, 2, 2.0 + offset),
429                (2, 3, 3.0 + offset),
430                (0, 3, 4.0 + offset),
431                (3, 4, 1.5),
432                (4, 5, 2.5),
433                (5, 6, 3.5),
434                (3, 6, 4.5),
435            ],
436        )
437        .unwrap()
438    }
439
440    #[test]
441    fn proof_dag_reuses_unchanged_atom_nodes() {
442        let initial = graph(0.0);
443        let updated = graph(0.01);
444        let artifact = ProofArtifact::build(
445            &initial,
446            &[updated],
447            &RipsParams::new(1),
448            CertificateLimits::default(),
449        )
450        .unwrap();
451        let summary = artifact.summary();
452        assert_eq!(summary.snapshots, 2);
453        assert_eq!(summary.node_references, 4);
454        assert!(summary.unique_nodes < summary.node_references);
455        assert!(summary.reused_references >= 1);
456        assert!(artifact.encode().unwrap().starts_with(MAGIC));
457
458        let mut program = PersistenceProgram::compile(
459            &initial,
460            &RipsParams::new(1),
461            CertificateLimits::default(),
462        )
463        .unwrap();
464        assert_eq!(
465            program.advance(&graph(0.02)).unwrap().mode,
466            ProgramUpdateMode::Reused
467        );
468        ProofArtifact::from_program(&program).unwrap();
469    }
470}
holos_tda/proof.rs

holos_tda/
proof.rs
