holos_tda/synthesis/model/
types.rs

1use std::fmt;
2
3use crate::{CohomologyLimits, Error, KineticEdge, KineticLimits, Result};
4
5/// Resource limits for synthesis search, proof construction, and decoding.
6#[derive(Debug, Clone, Copy, PartialEq, Eq)]
7#[non_exhaustive]
8pub struct SynthesisLimits {
9    /// Largest accepted artifact byte count.
10    pub max_bytes: usize,
11    /// Largest accepted vertex count.
12    pub max_vertices: usize,
13    /// Largest active edge count in one state.
14    pub max_edges_per_state: usize,
15    /// Largest state count.
16    pub max_states: usize,
17    /// Largest action count.
18    pub max_actions: usize,
19    /// Largest total coordinate and proof term count.
20    pub max_terms: usize,
21    /// Largest producer oracle-call count.
22    pub max_oracle_calls: usize,
23    /// Largest producer search-node count.
24    pub max_search_nodes: usize,
25    /// Largest proof-tree node count.
26    pub max_proof_nodes: usize,
27    /// Largest proof-tree depth.
28    pub max_proof_depth: usize,
29    /// Limits for each canonical cohomology computation.
30    pub cohomology: CohomologyLimits,
31    /// Limits for replaying an affine trajectory.
32    pub kinetic: KineticLimits,
33}
34
35impl Default for SynthesisLimits {
36    fn default() -> Self {
37        Self {
38            max_bytes: 1 << 30,
39            max_vertices: 1_000_000,
40            max_edges_per_state: 20_000_000,
41            max_states: 1_024,
42            max_actions: 16_384,
43            max_terms: 10_000_000,
44            max_oracle_calls: 2_000_000,
45            max_search_nodes: 2_000_000,
46            max_proof_nodes: 2_000_000,
47            max_proof_depth: 1_024,
48            cohomology: CohomologyLimits::default(),
49            kinetic: KineticLimits::default(),
50        }
51    }
52}
53
54/// Origin and completeness scope of the finite state list.
55#[derive(Debug, Clone, PartialEq)]
56pub enum SynthesisSource {
57    /// States were supplied directly. No completeness claim is made outside them.
58    Finite,
59    /// States are the complete fixed-scale schedule of an affine trajectory.
60    Affine {
61        /// Scenario identifier assigned to every retained state.
62        scenario: u64,
63        /// Canonical affine edge trajectories.
64        edges: Vec<KineticEdge>,
65        /// First time in the closed interval.
66        start: f64,
67        /// Last time in the closed interval.
68        end: f64,
69        /// Largest permitted rank throughout the interval.
70        maximum_rank: usize,
71    },
72}
73
74impl SynthesisLimits {
75    /// Set the largest producer oracle-call count.
76    #[must_use]
77    pub fn with_max_oracle_calls(mut self, maximum: usize) -> Self {
78        self.max_oracle_calls = maximum;
79        self
80    }
81
82    /// Set the largest producer search-node count.
83    #[must_use]
84    pub fn with_max_search_nodes(mut self, maximum: usize) -> Self {
85        self.max_search_nodes = maximum;
86        self
87    }
88}
89
90/// One nonzero coordinate in a canonical subspace generator.
91#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
92pub struct SynthesisCoordinate {
93    /// Position in the state's canonical cohomology basis.
94    pub basis: usize,
95    /// Coefficient in `1..modulus`.
96    pub coefficient: u32,
97}
98
99/// Completeness status of one synthesis result.
100#[derive(Debug, Clone, Copy, PartialEq, Eq)]
101pub enum SynthesisStatus {
102    /// The selected actions have minimum total cost.
103    Optimal,
104    /// No action set within the edit limit satisfies the specification.
105    Infeasible,
106    /// A producer work limit stopped the search before a complete proof.
107    SearchIncomplete,
108}
109
110impl SynthesisStatus {
111    pub(in crate::synthesis) fn code(self) -> u8 {
112        match self {
113            Self::Optimal => 1,
114            Self::Infeasible => 2,
115            Self::SearchIncomplete => 3,
116        }
117    }
118
119    pub(in crate::synthesis) fn from_code(code: u8) -> Result<Self> {
120        match code {
121            1 => Ok(Self::Optimal),
122            2 => Ok(Self::Infeasible),
123            3 => Ok(Self::SearchIncomplete),
124            _ => Err(Error::InvalidInput("synthesis status is invalid".into())),
125        }
126    }
127}
128
129impl fmt::Display for SynthesisStatus {
130    fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
131        formatter.write_str(match self {
132            Self::Optimal => "optimal",
133            Self::Infeasible => "infeasible",
134            Self::SearchIncomplete => "search incomplete",
135        })
136    }
137}
138
139#[derive(Debug, Clone, Copy, PartialEq, Eq)]
140pub(in crate::synthesis) enum BoundKind {
141    Cost,
142    Edits,
143}
144
145#[derive(Debug, Clone, PartialEq, Eq)]
146pub(in crate::synthesis) enum ProofNode {
147    Cost,
148    SurvivingMaximum,
149    SurvivingEditLimit,
150    BlockerBound {
151        kind: BoundKind,
152        blockers: Vec<Vec<usize>>,
153    },
154    Branch {
155        blocker: Vec<usize>,
156        children: Vec<ProofNode>,
157    },
158}
holos_tda/synthesis/model/types.rs

holos_tda/synthesis/model/
types.rs
