holos_tda/coverage_synthesis/
specification.rs

1//! Coverage specifications and their finite state sources.
2
3use std::collections::BTreeMap;
4
5use crate::monotone_proof::ProofLimits;
6use crate::{
7    CoverageFence, CoverageLimits, Error, KineticEdge, KineticEdgeKey, KineticFiltration,
8    KineticLimits, PlanarCoverageModel, Result, SparseDistanceMatrix,
9};
10
11use super::super::evaluate::{find_set, union_sets, validate_actions};
12use super::types::{CoverageAction, CoverageComponent};
13
14pub(crate) const FORMAT_MAX_PROOF_NODES: usize = 10_000_000;
15pub(crate) const FORMAT_MAX_PROOF_TERMS: usize = 100_000_000;
16
17/// Resource limits for coverage optimization, proofs, and artifacts.
18#[derive(Debug, Clone, Copy, PartialEq, Eq)]
19#[non_exhaustive]
20pub struct CoverageSynthesisLimits {
21    /// Largest accepted artifact byte count.
22    pub max_bytes: usize,
23    /// Largest producer oracle-call count.
24    pub max_oracle_calls: usize,
25    /// Largest producer search-node count.
26    pub max_search_nodes: usize,
27    /// Largest proof-tree node count.
28    pub max_proof_nodes: usize,
29    /// Largest proof-tree depth.
30    pub max_proof_depth: usize,
31    /// Largest proof blocker term count.
32    pub max_proof_terms: usize,
33    /// Limits for every relative coverage calculation.
34    pub coverage: CoverageLimits,
35    /// Limits for replaying an affine communication source.
36    pub kinetic: KineticLimits,
37}
38
39impl Default for CoverageSynthesisLimits {
40    fn default() -> Self {
41        Self {
42            max_bytes: 1 << 30,
43            max_oracle_calls: 2_000_000,
44            max_search_nodes: 2_000_000,
45            max_proof_nodes: 2_000_000,
46            max_proof_depth: 1_024,
47            max_proof_terms: 10_000_000,
48            coverage: CoverageLimits::default(),
49            kinetic: KineticLimits::default(),
50        }
51    }
52}
53
54impl CoverageSynthesisLimits {
55    /// Set the largest producer oracle-call count.
56    #[must_use]
57    pub fn with_max_oracle_calls(mut self, maximum: usize) -> Self {
58        self.max_oracle_calls = maximum;
59        self
60    }
61
62    /// Set the largest producer search-node count.
63    #[must_use]
64    pub fn with_max_search_nodes(mut self, maximum: usize) -> Self {
65        self.max_search_nodes = maximum;
66        self
67    }
68
69    pub(crate) fn proof(self) -> ProofLimits {
70        ProofLimits {
71            nodes: self.max_proof_nodes.min(FORMAT_MAX_PROOF_NODES),
72            depth: self.max_proof_depth,
73            terms: self.max_proof_terms.min(FORMAT_MAX_PROOF_TERMS),
74            checks: self.max_oracle_calls,
75        }
76    }
77}
78
79/// Origin and completeness scope of a finite coverage state list.
80#[derive(Debug, Clone, PartialEq)]
81pub enum CoverageSource {
82    /// States were supplied directly. No claim is made between them.
83    Finite,
84    /// States are the complete threshold schedule of affine communication edges.
85    /// Affine edge weights need not have a Euclidean realization.
86    Affine {
87        /// Scenario identifier assigned to every compiled state.
88        scenario: u64,
89        /// Canonical affine edge trajectories.
90        edges: Vec<KineticEdge>,
91        /// First time in the closed interval.
92        start: f64,
93        /// Last time in the closed interval.
94        end: f64,
95    },
96}
97
98/// One finite communication state and its initially active sensors.
99#[derive(Debug, Clone, PartialEq, Eq)]
100pub struct CoverageState {
101    pub(crate) scenario: u64,
102    pub(crate) step: u64,
103    pub(crate) base_vertices: Vec<usize>,
104    pub(crate) possible_edges: Vec<KineticEdgeKey>,
105}
106
107impl CoverageState {
108    /// Construct a state from a graph of every possible communication edge.
109    pub fn new(
110        scenario: u64,
111        step: u64,
112        graph: &SparseDistanceMatrix,
113        mut base_vertices: Vec<usize>,
114        broadcast_radius: f64,
115    ) -> Result<Self> {
116        base_vertices.sort_unstable();
117        base_vertices.dedup();
118        if !broadcast_radius.is_finite()
119            || broadcast_radius <= 0.0
120            || base_vertices.iter().any(|vertex| *vertex >= graph.len())
121        {
122            return Err(Error::InvalidInput(
123                "coverage state has an invalid radius or base vertex".into(),
124            ));
125        }
126        Ok(Self {
127            scenario,
128            step,
129            base_vertices,
130            possible_edges: graph
131                .edges()
132                .filter(|edge| edge.2 <= broadcast_radius)
133                .map(|(u, v, _)| KineticEdgeKey::new(u, v))
134                .collect(),
135        })
136    }
137
138    /// Scenario identifier used to group related states.
139    pub fn scenario(&self) -> u64 {
140        self.scenario
141    }
142
143    /// Ordered step identifier inside the scenario.
144    pub fn step(&self) -> u64 {
145        self.step
146    }
147
148    /// Sensors active before selecting a plan.
149    pub fn base_vertices(&self) -> &[usize] {
150        &self.base_vertices
151    }
152
153    /// Communication edges available when both endpoints are active.
154    pub fn possible_edges(&self) -> &[KineticEdgeKey] {
155        &self.possible_edges
156    }
157}
158
159/// Finite or affine coverage specification over [`PlanarCoverageModel`].
160#[derive(Debug, Clone, PartialEq)]
161pub struct CoverageSpecification {
162    pub(crate) vertex_count: usize,
163    pub(crate) model: PlanarCoverageModel,
164    pub(crate) modulus: u32,
165    pub(crate) fence: CoverageFence,
166    pub(crate) failable_vertices: Vec<usize>,
167    pub(crate) failure_budget: usize,
168    pub(crate) source: CoverageSource,
169    pub(crate) states: Vec<CoverageState>,
170}
171
172impl CoverageSpecification {
173    /// Construct a finite coverage specification.
174    #[allow(clippy::too_many_arguments)]
175    pub fn new(
176        vertex_count: usize,
177        model: PlanarCoverageModel,
178        modulus: u32,
179        fence: CoverageFence,
180        mut failable_vertices: Vec<usize>,
181        failure_budget: usize,
182        mut states: Vec<CoverageState>,
183        limits: CoverageLimits,
184    ) -> Result<Self> {
185        failable_vertices.sort_unstable();
186        failable_vertices.dedup();
187        states.sort_by_key(|state| (state.scenario, state.step));
188        let specification = Self {
189            vertex_count,
190            model,
191            modulus,
192            fence,
193            failable_vertices,
194            failure_budget,
195            source: CoverageSource::Finite,
196            states,
197        };
198        specification.validate(limits)?;
199        Ok(specification)
200    }
201
202    /// Compile the complete affine communication threshold schedule.
203    #[allow(clippy::too_many_arguments)]
204    pub fn from_kinetic(
205        filtration: &KineticFiltration,
206        scenario: u64,
207        model: PlanarCoverageModel,
208        modulus: u32,
209        fence: CoverageFence,
210        failable_vertices: Vec<usize>,
211        failure_budget: usize,
212        base_vertices: Vec<usize>,
213        limits: CoverageLimits,
214    ) -> Result<Self> {
215        let states = filtration
216            .critical_graphs(model.broadcast_radius())?
217            .into_iter()
218            .enumerate()
219            .map(|(step, state)| {
220                CoverageState::new(
221                    scenario,
222                    step as u64,
223                    &state.graph,
224                    base_vertices.clone(),
225                    model.broadcast_radius(),
226                )
227            })
228            .collect::<Result<Vec<_>>>()?;
229        let mut specification = Self::new(
230            filtration.vertex_count(),
231            model,
232            modulus,
233            fence,
234            failable_vertices,
235            failure_budget,
236            states,
237            limits,
238        )?;
239        specification.source = CoverageSource::Affine {
240            scenario,
241            edges: filtration.edges().to_vec(),
242            start: filtration.start(),
243            end: filtration.end(),
244        };
245        Ok(specification)
246    }
247
248    /// Number of sensor labels shared by every state.
249    pub fn vertex_count(&self) -> usize {
250        self.vertex_count
251    }
252
253    /// Declared planar coverage model.
254    pub fn model(&self) -> PlanarCoverageModel {
255        self.model
256    }
257
258    /// Prime coefficient modulus.
259    pub fn modulus(&self) -> u32 {
260        self.modulus
261    }
262
263    /// Canonical protected fence cycle.
264    pub fn fence(&self) -> &CoverageFence {
265        &self.fence
266    }
267
268    /// Sensors that the failure quantifier may remove.
269    pub fn failable_vertices(&self) -> &[usize] {
270        &self.failable_vertices
271    }
272
273    /// Largest simultaneous failure count.
274    pub fn failure_budget(&self) -> usize {
275        self.failure_budget
276    }
277
278    /// Origin and completeness scope of the state list.
279    pub fn source(&self) -> &CoverageSource {
280        &self.source
281    }
282
283    /// Canonical state list.
284    pub fn states(&self) -> &[CoverageState] {
285        &self.states
286    }
287
288    pub(crate) fn validate(&self, limits: CoverageLimits) -> Result<()> {
289        PlanarCoverageModel::new(self.model.broadcast_radius(), self.model.sensing_radius())?;
290        self.validate_scope(limits)?;
291        if self
292            .states
293            .windows(2)
294            .any(|pair| (pair[0].scenario, pair[0].step) >= (pair[1].scenario, pair[1].step))
295        {
296            return Err(Error::InvalidInput(
297                "coverage states are not in canonical scenario and step order".into(),
298            ));
299        }
300        for state in &self.states {
301            self.validate_state(state, limits)?;
302        }
303        Ok(())
304    }
305
306    pub(super) fn validate_scope(&self, limits: CoverageLimits) -> Result<()> {
307        let invalid_failable = self
308            .failable_vertices
309            .iter()
310            .any(|vertex| *vertex >= self.vertex_count);
311        let failable_fence = self
312            .fence
313            .vertices()
314            .iter()
315            .any(|vertex| self.failable_vertices.binary_search(vertex).is_ok());
316        if self.vertex_count == 0
317            || self.vertex_count > limits.max_vertices
318            || self.states.is_empty()
319            || self.states.len() > limits.max_states
320            || self
321                .fence
322                .vertices()
323                .iter()
324                .any(|vertex| *vertex >= self.vertex_count)
325            || invalid_failable
326            || failable_fence
327            || self.failure_budget > self.failable_vertices.len()
328        {
329            Err(Error::InvalidInput(
330                "coverage specification has an invalid scope, fence, or failure model".into(),
331            ))
332        } else {
333            Ok(())
334        }
335    }
336
337    pub(super) fn validate_state(
338        &self,
339        state: &CoverageState,
340        limits: CoverageLimits,
341    ) -> Result<()> {
342        let invalid_edge = state
343            .possible_edges
344            .iter()
345            .any(|edge| edge.u >= edge.v || edge.v >= self.vertex_count);
346        let missing_fence = self
347            .fence
348            .vertices()
349            .iter()
350            .any(|vertex| state.base_vertices.binary_search(vertex).is_err());
351        if state
352            .base_vertices
353            .iter()
354            .any(|vertex| *vertex >= self.vertex_count)
355            || state.possible_edges.len() > limits.max_edges
356            || invalid_edge
357            || state
358                .possible_edges
359                .windows(2)
360                .any(|pair| pair[0] >= pair[1])
361            || missing_fence
362        {
363            Err(Error::InvalidInput(
364                "coverage state is not canonical or omits a fence vertex".into(),
365            ))
366        } else {
367            Ok(())
368        }
369    }
370
371    /// Decompose the state-action incidence relation into exact components.
372    pub fn components(&self, actions: &[CoverageAction]) -> Result<Vec<CoverageComponent>> {
373        validate_actions(self, actions, CoverageLimits::default())?;
374        let offset = self.states.len();
375        let mut parent = (0..offset + actions.len()).collect::<Vec<_>>();
376        for (action, candidate) in actions.iter().enumerate() {
377            for &state in &candidate.states {
378                union_sets(&mut parent, state, offset + action);
379            }
380        }
381        let mut components = BTreeMap::<usize, CoverageComponent>::new();
382        for state in 0..self.states.len() {
383            let root = find_set(&mut parent, state);
384            components.entry(root).or_default().states.push(state);
385        }
386        for action in 0..actions.len() {
387            let root = find_set(&mut parent, offset + action);
388            components.entry(root).or_default().actions.push(action);
389        }
390        let mut output = components.into_values().collect::<Vec<_>>();
391        output.sort_by_key(|component| {
392            (
393                component.states.first().copied().unwrap_or(usize::MAX),
394                component.actions.first().copied().unwrap_or(usize::MAX),
395            )
396        });
397        Ok(output)
398    }
399}
holos_tda/coverage_synthesis/specification.rs

holos_tda/coverage_synthesis/
specification.rs
