automation_structures/
composition_api.rs

1//! Checked public entry points for reusable named compositions.
2
3use crate::api::values_within_max;
4use crate::compositions::allocation_snapshot::AllocationSnapshot as AllocationSnapshotCarrier;
5use crate::compositions::bisection::Bisection as BisectionCarrier;
6use crate::compositions::equivalence_class::EquivalenceClass as EquivalenceClassCarrier;
7use crate::compositions::federated_budget::FederatedBudget as FederatedBudgetCarrier;
8use crate::compositions::rate_limit::RateLimit as RateLimitCarrier;
9use crate::compositions::reduction::Reducer as ReductionCarrier;
10use crate::compositions::relationship_graph::RelationshipGraph as RelationshipGraphCarrier;
11use crate::compositions::sampler::Sampler as SamplerCarrier;
12use crate::compositions::select_then_actuate::SelectThenActuate as SelectThenActuateCarrier;
13use crate::compositions::signal::Signal as SignalCarrier;
14use crate::compositions::traversal_engine::TraversalEngine as TraversalEngineCarrier;
15use vstd::prelude::*;
16
17verus! {
18
19/// A disabled allocation-snapshot transition.
20#[derive(Clone, Copy, Debug, Eq, PartialEq)]
21#[non_exhaustive]
22pub enum AllocationSnapshotError {
23    /// The node is outside the configured node universe.
24    NodeOutOfRange,
25    /// The node is already present in the snapshot.
26    NodeAlreadyAccepted,
27    /// Accepted nodes must have a positive cost.
28    ZeroCost,
29    /// The node cost exceeds the remaining budget.
30    InsufficientBudget,
31}
32
33/// A reusable accepted-node snapshot coupled to one capacity budget.
34///
35/// # Examples
36///
37/// ```rust
38/// use automation_structures::AllocationSnapshot;
39///
40/// let mut snapshot = AllocationSnapshot::new(7, 3);
41/// snapshot.accept(0, 3)?;
42/// assert_eq!(snapshot.accepted_entries().copied().collect::<Vec<_>>(), vec![(0, 3)]);
43/// # Ok::<(), automation_structures::AllocationSnapshotError>(())
44/// ```
45pub struct AllocationSnapshot {
46    inner: AllocationSnapshotCarrier,
47}
48
49impl AllocationSnapshot {
50    #[verifier::type_invariant]
51    closed spec fn well_formed(&self) -> bool {
52        self.inner.type_invariant() && self.inner.budget_consistency()
53    }
54
55    /// Construct an empty snapshot.
56    pub fn new(capacity: u64, num_nodes: u64) -> (snapshot: Self) {
57        Self { inner: AllocationSnapshotCarrier::new(capacity, num_nodes) }
58    }
59
60    /// Fixed capacity ceiling.
61    pub fn capacity(&self) -> u64 { self.inner.budget.capacity }
62
63    /// Size of the admitted node universe.
64    pub fn num_nodes(&self) -> u64 { self.inner.num_nodes }
65
66    /// Cost accepted into the snapshot.
67    pub fn total_cost(&self) -> u64 { self.inner.budget.allocated }
68
69    /// Capacity not yet consumed.
70    pub fn budget_remaining(&self) -> u64 {
71        proof { use_type_invariant(&*self); }
72        self.inner.budget.available()
73    }
74
75    /// Number of accepted nodes.
76    pub fn len(&self) -> usize { self.inner.registry.entries.len() }
77
78    /// Whether no nodes have been accepted.
79    pub fn is_empty(&self) -> bool { self.inner.registry.entries.is_empty() }
80
81    /// Whether a node has been accepted.
82    pub fn contains(&self, node: u64) -> bool {
83        proof { use_type_invariant(&*self); }
84        self.inner.contains_exec(node)
85    }
86
87    /// Read one accepted node by insertion order.
88    #[expect(clippy::indexing_slicing, reason = "the branch proves the accepted-node index is in bounds")]
89    pub fn accepted(&self, index: usize) -> Option<u64> {
90        if index < self.inner.registry.entries.len() {
91            Some(self.inner.registry.entries[index].0)
92        } else {
93            None
94        }
95    }
96
97    /// Read the cost registered for one accepted node by insertion order.
98    #[expect(clippy::indexing_slicing, reason = "the branch proves the registry index is in bounds")]
99    pub fn accepted_cost(&self, index: usize) -> Option<u64> {
100        if index < self.inner.registry.entries.len() {
101            Some(self.inner.registry.entries[index].1)
102        } else {
103            None
104        }
105    }
106
107    /// Accept a fresh node whose positive cost fits the remaining capacity.
108    ///
109    /// # Errors
110    ///
111    /// Returns an error when the node or cost violates the configured universe,
112    /// uniqueness, positivity, or capacity constraints.
113    pub fn accept(&mut self, node: u64, cost: u64) -> (result: Result<(), AllocationSnapshotError>) {
114        proof { use_type_invariant(&*self); }
115        if node >= self.inner.num_nodes { return Err(AllocationSnapshotError::NodeOutOfRange); }
116        if self.inner.contains_exec(node) { return Err(AllocationSnapshotError::NodeAlreadyAccepted); }
117        if cost == 0 { return Err(AllocationSnapshotError::ZeroCost); }
118        let available = self.inner.budget.available();
119        if cost > available { return Err(AllocationSnapshotError::InsufficientBudget); }
120        let mut carrier = allocation_snapshot_sentinel();
121        core::mem::swap(&mut self.inner, &mut carrier);
122        carrier.accept_node(node, cost);
123        core::mem::swap(&mut self.inner, &mut carrier);
124        Ok(())
125    }
126}
127
128/// A master capacity pool divided into reusable sub-pools.
129///
130/// # Examples
131///
132/// ```rust
133/// use automation_structures::FederatedBudget;
134///
135/// let mut budget = FederatedBudget::new(10, 2);
136/// assert!(budget.try_delegate(0, 6));
137/// assert!(budget.try_allocate(0, 4));
138/// assert_eq!(budget.pool_allocated(0), Some(4));
139/// ```
140pub struct FederatedBudget {
141    inner: FederatedBudgetCarrier,
142}
143
144impl FederatedBudget {
145    #[verifier::type_invariant]
146    closed spec fn well_formed(&self) -> bool { self.inner.inv() }
147
148    /// Construct an empty federation with `num_pools` sub-pools.
149    pub fn new(master_capacity: u64, num_pools: usize) -> (budget: Self) {
150        Self { inner: FederatedBudgetCarrier::new(master_capacity, num_pools) }
151    }
152
153    /// Fixed master capacity.
154    pub fn master_capacity(&self) -> u64 { self.inner.master.capacity }
155
156    /// Master capacity currently delegated to sub-pools.
157    pub fn master_allocated(&self) -> u64 { self.inner.master.allocated }
158
159    /// Number of sub-pools.
160    pub fn len(&self) -> usize { self.inner.sub_pools.len() }
161
162    /// Whether no sub-pools are configured.
163    pub fn is_empty(&self) -> bool { self.inner.sub_pools.is_empty() }
164
165    /// Read one sub-pool capacity.
166    #[expect(clippy::indexing_slicing, reason = "the branch proves the pool index is in bounds")]
167    pub fn pool_capacity(&self, pool: usize) -> Option<u64> {
168        proof { use_type_invariant(&*self); }
169        if pool < self.inner.sub_pools.len() {
170            Some(self.inner.sub_pools[pool].allocated + self.inner.sub_pools[pool].reserved)
171        } else {
172            None
173        }
174    }
175
176    /// Read one sub-pool allocation.
177    #[expect(clippy::indexing_slicing, reason = "the branch proves the pool index is in bounds")]
178    pub fn pool_allocated(&self, pool: usize) -> Option<u64> {
179        if pool < self.inner.sub_pools.len() {
180            Some(self.inner.sub_pools[pool].allocated)
181        } else {
182            None
183        }
184    }
185
186    /// Try to delegate master capacity to a sub-pool.
187    #[must_use]
188    pub fn try_delegate(&mut self, pool: usize, amount: u64) -> (accepted: bool) {
189        proof { use_type_invariant(&*self); }
190        let mut carrier = federated_budget_sentinel();
191        core::mem::swap(&mut self.inner, &mut carrier);
192        let accepted = carrier.allocate_sub_pool(pool, amount);
193        core::mem::swap(&mut self.inner, &mut carrier);
194        accepted
195    }
196
197    /// Try to consume capacity within a sub-pool.
198    #[must_use]
199    pub fn try_allocate(&mut self, pool: usize, amount: u64) -> (accepted: bool) {
200        proof { use_type_invariant(&*self); }
201        let mut carrier = federated_budget_sentinel();
202        core::mem::swap(&mut self.inner, &mut carrier);
203        let accepted = carrier.allocate_from_sub_pool(pool, amount);
204        core::mem::swap(&mut self.inner, &mut carrier);
205        accepted
206    }
207
208    /// Try to release capacity consumed within a sub-pool.
209    #[must_use]
210    pub fn try_release(&mut self, pool: usize, amount: u64) -> (accepted: bool) {
211        proof { use_type_invariant(&*self); }
212        let mut carrier = federated_budget_sentinel();
213        core::mem::swap(&mut self.inner, &mut carrier);
214        let accepted = carrier.release_from_sub_pool(pool, amount);
215        core::mem::swap(&mut self.inner, &mut carrier);
216        accepted
217    }
218}
219
220/// Invalid bisection configuration.
221#[derive(Clone, Copy, Debug, Eq, PartialEq)]
222#[non_exhaustive]
223pub enum BisectionBuildError {
224    /// The ordered domain must contain at least two points.
225    DomainTooSmall,
226    /// The threshold must be inside `1..domain_size`.
227    ThresholdOutOfRange,
228}
229
230/// A disabled bisection transition.
231#[derive(Clone, Copy, Debug, Eq, PartialEq)]
232#[non_exhaustive]
233pub enum BisectionError {
234    /// The candidate interval is already converged.
235    AlreadyConverged,
236}
237
238/// A bounded bisection model over an already-known monotone boundary.
239///
240/// The caller supplies the threshold at construction. Probes narrow the interval
241/// around that retained threshold; this type has no caller-supplied predicate or
242/// external probe-result interface.
243///
244/// # Examples
245///
246/// ```rust
247/// use automation_structures::Bisection;
248///
249/// let mut search = Bisection::new(16, 11)?;
250/// search.converge();
251/// assert!(search.lower() <= 11 && 11 <= search.upper());
252/// # Ok::<(), automation_structures::BisectionBuildError>(())
253/// ```
254pub struct Bisection {
255    inner: BisectionCarrier,
256}
257
258impl Bisection {
259    #[verifier::type_invariant]
260    closed spec fn well_formed(&self) -> bool { self.inner.invariant() }
261
262    /// Construct a full-domain bisection around a known threshold using the complete `u64` probe budget.
263    ///
264    /// # Errors
265    ///
266    /// Returns an error when the domain has fewer than two points or the threshold
267    /// is not strictly inside the domain.
268    pub fn new(domain_size: u64, threshold: u64) -> (result: Result<Self, BisectionBuildError>) {
269        if domain_size < 2 { return Err(BisectionBuildError::DomainTooSmall); }
270        if threshold < 1 || threshold >= domain_size {
271            return Err(BisectionBuildError::ThresholdOutOfRange);
272        }
273        proof { lemma_u64_domain_fits_64(domain_size); }
274        let inner = BisectionCarrier::new(0, domain_size, threshold, domain_size, 64);
275        Ok(Self { inner })
276    }
277
278    /// Current lower bound.
279    pub fn lower(&self) -> u64 { self.inner.lo }
280
281    /// Current upper bound.
282    pub fn upper(&self) -> u64 { self.inner.hi }
283
284    /// Hidden monotone boundary used by this executable carrier.
285    pub fn threshold(&self) -> u64 { self.inner.threshold }
286
287    /// Number of probes taken.
288    pub fn probes_taken(&self) -> u64 { self.inner.budget.allocated }
289
290    /// Maximum number of probes.
291    pub fn max_probes(&self) -> u64 { self.inner.budget.capacity }
292
293    /// Whether the candidate interval has width less than two.
294    pub fn is_converged(&self) -> bool {
295        proof { use_type_invariant(&*self); }
296        self.inner.converged()
297    }
298
299    /// Perform one midpoint probe.
300    ///
301    /// # Errors
302    ///
303    /// Returns [`BisectionError::AlreadyConverged`] when no further probe is enabled.
304    pub fn probe(&mut self) -> (result: Result<(), BisectionError>) {
305        proof { use_type_invariant(&*self); }
306        if self.inner.hi - self.inner.lo < 2 { return Err(BisectionError::AlreadyConverged); }
307        let mut carrier = bisection_sentinel();
308        core::mem::swap(&mut self.inner, &mut carrier);
309        carrier.probe();
310        core::mem::swap(&mut self.inner, &mut carrier);
311        Ok(())
312    }
313
314    /// Drive midpoint probes until the interval converges.
315    pub fn converge(&mut self) {
316        proof { use_type_invariant(&*self); }
317        let mut carrier = bisection_sentinel();
318        core::mem::swap(&mut self.inner, &mut carrier);
319        carrier.bisect();
320        core::mem::swap(&mut self.inner, &mut carrier);
321    }
322}
323
324/// An invalid equivalence-class element index.
325#[derive(Clone, Copy, Debug, Eq, PartialEq)]
326#[non_exhaustive]
327pub enum EquivalenceClassError {
328    /// The element is outside the configured universe.
329    ElementOutOfRange,
330}
331
332/// A bounded union-by-rank equivalence-class partition.
333///
334/// # Examples
335///
336/// ```rust
337/// use automation_structures::EquivalenceClass;
338///
339/// let mut classes = EquivalenceClass::new(3, 2);
340/// assert!(classes.union(0, 1)?);
341/// assert!(classes.equivalent(0, 1)?);
342/// # Ok::<(), automation_structures::EquivalenceClassError>(())
343/// ```
344pub struct EquivalenceClass {
345    inner: EquivalenceClassCarrier,
346}
347
348impl EquivalenceClass {
349    #[verifier::type_invariant]
350    closed spec fn well_formed(&self) -> bool { self.inner.inv() }
351
352    /// Construct a singleton partition with a merge-operation ceiling.
353    pub fn new(elements: usize, max_unions: u64) -> (classes: Self) {
354        Self { inner: EquivalenceClassCarrier::new(elements, max_unions) }
355    }
356
357    /// Number of elements in the partition.
358    pub fn len(&self) -> usize { self.inner.n }
359
360    /// Whether the partition contains no elements.
361    pub fn is_empty(&self) -> bool { self.inner.n == 0 }
362
363    /// Successful union operations performed.
364    pub fn unions_performed(&self) -> u64 { self.inner.budget.allocated }
365
366    /// Configured union-operation ceiling.
367    pub fn max_unions(&self) -> u64 { self.inner.budget.capacity }
368
369    /// Find an element's representative.
370    ///
371    /// # Errors
372    ///
373    /// Returns [`EquivalenceClassError::ElementOutOfRange`] for an unknown element.
374    pub fn representative(&self, element: usize) -> (result: Result<usize, EquivalenceClassError>) {
375        proof { use_type_invariant(&*self); }
376        if element >= self.inner.n { return Err(EquivalenceClassError::ElementOutOfRange); }
377        Ok(self.inner.find(element))
378    }
379
380    /// Merge two classes, returning false if equal or the operation ceiling is exhausted.
381    ///
382    /// # Errors
383    ///
384    /// Returns [`EquivalenceClassError::ElementOutOfRange`] when either element is unknown.
385    pub fn union(&mut self, left: usize, right: usize) -> (result: Result<bool, EquivalenceClassError>) {
386        proof { use_type_invariant(&*self); }
387        if left >= self.inner.n || right >= self.inner.n {
388            return Err(EquivalenceClassError::ElementOutOfRange);
389        }
390        let mut carrier = equivalence_class_sentinel();
391        core::mem::swap(&mut self.inner, &mut carrier);
392        let merged = carrier.union(left, right);
393        core::mem::swap(&mut self.inner, &mut carrier);
394        Ok(merged)
395    }
396
397    /// Test whether two elements have the same representative.
398    ///
399    /// # Errors
400    ///
401    /// Returns [`EquivalenceClassError::ElementOutOfRange`] when either element is unknown.
402    pub fn equivalent(&self, left: usize, right: usize) -> (result: Result<bool, EquivalenceClassError>) {
403        proof { use_type_invariant(&*self); }
404        if left >= self.inner.n || right >= self.inner.n {
405            return Err(EquivalenceClassError::ElementOutOfRange);
406        }
407        Ok(self.inner.same(left, right))
408    }
409}
410
411/// Invalid rate-limit configuration.
412#[derive(Clone, Copy, Debug, Eq, PartialEq)]
413#[non_exhaustive]
414pub enum RateLimitBuildError {
415    /// A rate limit must admit at least one operation per window.
416    ZeroLimit,
417    /// A rate-limiting window must span at least one logical-clock unit.
418    ZeroWindowDuration,
419}
420
421/// A disabled rate-limit transition.
422#[derive(Clone, Copy, Debug, Eq, PartialEq)]
423#[non_exhaustive]
424pub enum RateLimitError {
425    /// The bounded logical clock has reached its configured maximum.
426    ClockExhausted,
427}
428
429/// A logical-clock, fixed-window rate limit.
430///
431/// # Examples
432///
433/// ```rust
434/// use automation_structures::RateLimit;
435///
436/// let mut limit = RateLimit::new(2, 5, 10)?;
437/// assert!(limit.try_acquire());
438/// limit.tick()?;
439/// # Ok::<(), Box<dyn std::error::Error>>(())
440/// ```
441pub struct RateLimit {
442    inner: RateLimitCarrier,
443}
444
445impl RateLimit {
446    #[verifier::type_invariant]
447    closed spec fn well_formed(&self) -> bool {
448        self.inner.type_invariant()
449            && self.inner.window_start_not_future()
450            && self.inner.window_duration > 0
451    }
452
453    /// Construct a rate limit at logical clock zero with a positive window duration.
454    ///
455    /// # Errors
456    ///
457    /// Returns [`RateLimitBuildError::ZeroLimit`] when no operation can be admitted,
458    /// or [`RateLimitBuildError::ZeroWindowDuration`] for a zero-length window.
459    pub fn new(max_per_window: u64, window_duration: u64, max_clock: u64)
460        -> (result: Result<Self, RateLimitBuildError>) {
461        if max_per_window == 0 { return Err(RateLimitBuildError::ZeroLimit); }
462        if window_duration == 0 { return Err(RateLimitBuildError::ZeroWindowDuration); }
463        Ok(Self { inner: RateLimitCarrier::new(max_per_window, window_duration, max_clock) })
464    }
465
466    /// Per-window admission ceiling.
467    pub fn max_per_window(&self) -> u64 { self.inner.budget.capacity }
468
469    /// Window duration in logical-clock units.
470    pub fn window_duration(&self) -> u64 { self.inner.window_duration }
471
472    /// Acquisitions admitted in the current window.
473    pub fn count(&self) -> u64 { self.inner.budget.allocated }
474
475    /// Current logical clock.
476    pub fn clock(&self) -> u64 { self.inner.clock }
477
478    /// Current window anchor.
479    pub fn window_start(&self) -> u64 { self.inner.window_start }
480
481    /// Try to acquire one unit in the current or newly rolled window.
482    #[must_use]
483    pub fn try_acquire(&mut self) -> (accepted: bool) {
484        proof { use_type_invariant(&*self); }
485        let mut carrier = rate_limit_sentinel();
486        core::mem::swap(&mut self.inner, &mut carrier);
487        let accepted = carrier.try_acquire();
488        core::mem::swap(&mut self.inner, &mut carrier);
489        accepted
490    }
491
492    /// Advance the bounded logical clock by one.
493    ///
494    /// # Errors
495    ///
496    /// Returns [`RateLimitError::ClockExhausted`] at the configured clock ceiling.
497    pub fn tick(&mut self) -> (result: Result<(), RateLimitError>) {
498        proof { use_type_invariant(&*self); }
499        if self.inner.clock >= self.inner.max_clock { return Err(RateLimitError::ClockExhausted); }
500        let mut carrier = rate_limit_sentinel();
501        core::mem::swap(&mut self.inner, &mut carrier);
502        carrier.tick();
503        core::mem::swap(&mut self.inner, &mut carrier);
504        Ok(())
505    }
506}
507
508/// Invalid reduction input.
509#[derive(Clone, Copy, Debug, Eq, PartialEq)]
510#[non_exhaustive]
511pub enum ReductionBuildError {
512    /// The input exceeds the verified one-billion-item ceiling.
513    TooManyItems,
514    /// An input value exceeds the verified one-billion-unit ceiling.
515    ValueOutOfRange,
516}
517
518/// A disabled incremental reduction transition.
519#[derive(Clone, Copy, Debug, Eq, PartialEq)]
520#[non_exhaustive]
521pub enum ReductionError {
522    /// Every input item has already been consumed.
523    Complete,
524}
525
526/// An incremental additive ordered-prefix reduction.
527///
528/// # Examples
529///
530/// ```rust
531/// use automation_structures::Reduction;
532///
533/// let mut reduction = Reduction::new(vec![2, 3])?;
534/// reduction.process_next()?;
535/// assert_eq!(reduction.result(), 2);
536/// # Ok::<(), Box<dyn std::error::Error>>(())
537/// ```
538pub struct Reduction {
539    inner: ReductionCarrier,
540}
541
542impl Reduction {
543    #[verifier::type_invariant]
544    closed spec fn well_formed(&self) -> bool {
545        self.inner.inv()
546    }
547
548    /// Validate and construct an incremental sum reduction.
549    ///
550    /// # Errors
551    ///
552    /// Returns an error when the item count or an item value exceeds its verified ceiling.
553    pub fn new(items: Vec<u64>) -> (result: Result<Self, ReductionBuildError>) {
554        if items.len() > 1_000_000_000 { return Err(ReductionBuildError::TooManyItems); }
555        if !values_within_max(&items, 1_000_000_000) {
556            return Err(ReductionBuildError::ValueOutOfRange);
557        }
558        Ok(Self { inner: ReductionCarrier::new(items) })
559    }
560
561    /// Current additive result.
562    pub fn result(&self) -> u64 { self.inner.result() }
563
564    /// Number of consumed items.
565    pub fn processed_len(&self) -> usize { self.inner.position() }
566
567    /// Number of pending items.
568    pub fn remaining_len(&self) -> usize {
569        proof { use_type_invariant(&*self); }
570        self.inner.remaining_len()
571    }
572
573    /// Whether the whole input has been consumed.
574    pub fn is_complete(&self) -> bool {
575        proof { use_type_invariant(&*self); }
576        self.inner.done()
577    }
578
579    /// Consume the next item in original order.
580    ///
581    /// # Errors
582    ///
583    /// Returns [`ReductionError::Complete`] after every item has been consumed.
584    pub fn process_next(&mut self) -> (result: Result<(), ReductionError>) {
585        proof { use_type_invariant(&*self); }
586        if self.inner.done() { return Err(ReductionError::Complete); }
587        let mut carrier = reduction_sentinel();
588        core::mem::swap(&mut self.inner, &mut carrier);
589        carrier.process();
590        core::mem::swap(&mut self.inner, &mut carrier);
591        Ok(())
592    }
593}
594
595/// A disabled relationship-graph transition.
596#[derive(Clone, Copy, Debug, Eq, PartialEq)]
597#[non_exhaustive]
598pub enum RelationshipGraphError {
599    /// A source or destination node is outside the configured graph.
600    NodeOutOfRange,
601    /// The edge weight exceeds the configured maximum.
602    WeightOutOfRange,
603    /// Self-loops are not admitted.
604    SelfLoop,
605}
606
607/// A weighted directed graph with a consistent adjacency projection.
608///
609/// # Examples
610///
611/// ```rust
612/// use automation_structures::RelationshipGraph;
613///
614/// let mut graph = RelationshipGraph::new(3, 10);
615/// assert!(graph.add_edge(0, 1, 4)?);
616/// assert!(graph.contains(0, 1));
617/// # Ok::<(), automation_structures::RelationshipGraphError>(())
618/// ```
619pub struct RelationshipGraph {
620    inner: RelationshipGraphCarrier,
621}
622
623impl RelationshipGraph {
624    #[verifier::type_invariant]
625    closed spec fn well_formed(&self) -> bool { self.inner.inv() }
626
627    /// Construct an empty graph.
628    pub fn new(num_nodes: usize, max_weight: u64) -> (graph: Self) {
629        Self { inner: RelationshipGraphCarrier::new(num_nodes, max_weight) }
630    }
631
632    /// Number of nodes.
633    pub fn num_nodes(&self) -> usize { self.inner.num_nodes }
634
635    /// Maximum admitted edge weight.
636    pub fn max_weight(&self) -> u64 { self.inner.max_weight }
637
638    /// Number of concrete weighted edges.
639    pub fn edge_count(&self) -> usize { self.inner.registry.entries.len() }
640
641    /// Read a concrete weighted edge by insertion order.
642    pub fn edge(&self, index: usize) -> Option<(usize, usize, u64)> {
643        if index < self.inner.registry.entries.len() {
644            Some(self.inner.registry.entries[index].0)
645        } else {
646            None
647        }
648    }
649
650    /// Whether any weighted edge exists for a source-destination pair.
651    pub fn contains(&self, source: usize, destination: usize) -> bool {
652        proof { use_type_invariant(&*self); }
653        self.inner.contains_pair(source, destination)
654    }
655
656    /// Add one concrete weighted edge if it is not already present.
657    ///
658    /// # Errors
659    ///
660    /// Returns an error for an unknown endpoint, an excessive weight, or a self-loop.
661    pub fn add_edge(&mut self, source: usize, destination: usize, weight: u64)
662        -> (result: Result<bool, RelationshipGraphError>) {
663        proof { use_type_invariant(&*self); }
664        if source >= self.inner.num_nodes || destination >= self.inner.num_nodes {
665            return Err(RelationshipGraphError::NodeOutOfRange);
666        }
667        if weight > self.inner.max_weight { return Err(RelationshipGraphError::WeightOutOfRange); }
668        if source == destination { return Err(RelationshipGraphError::SelfLoop); }
669        let mut carrier = relationship_graph_sentinel();
670        core::mem::swap(&mut self.inner, &mut carrier);
671        let added = carrier.add_edge(source, destination, weight);
672        core::mem::swap(&mut self.inner, &mut carrier);
673        Ok(added)
674    }
675
676    /// Remove every weighted edge for one source-destination pair.
677    pub fn remove_edges(&mut self, source: usize, destination: usize) {
678        proof { use_type_invariant(&*self); }
679        let mut carrier = relationship_graph_sentinel();
680        core::mem::swap(&mut self.inner, &mut carrier);
681        carrier.remove_edge(source, destination);
682        core::mem::swap(&mut self.inner, &mut carrier);
683    }
684}
685
686/// A disabled sampler transition.
687#[derive(Clone, Copy, Debug, Eq, PartialEq)]
688#[non_exhaustive]
689pub enum SamplerError {
690    /// The item index is outside the distribution.
691    ItemOutOfRange,
692    /// The bounded sample is full.
693    SampleFull,
694    /// The item has zero support weight.
695    OutsideSupport,
696    /// The item has already been selected.
697    AlreadySelected,
698}
699
700/// A bounded without-replacement sampler over caller-supplied proposals.
701///
702/// # Examples
703///
704/// ```rust
705/// use automation_structures::Sampler;
706///
707/// let mut sampler = Sampler::new(vec![3, 1, 0], 2);
708/// sampler.sample(0)?;
709/// assert_eq!(sampler.selected().collect::<Vec<_>>(), vec![0]);
710/// # Ok::<(), automation_structures::SamplerError>(())
711/// ```
712pub struct Sampler {
713    inner: SamplerCarrier,
714}
715
716impl Sampler {
717    #[verifier::type_invariant]
718    closed spec fn well_formed(&self) -> bool { self.inner.inv() }
719
720    /// Construct an empty sample over a weight distribution.
721    pub fn new(distribution: Vec<u64>, sample_size: usize) -> (sampler: Self) {
722        Self { inner: SamplerCarrier::new(distribution, sample_size) }
723    }
724
725    /// Number of distribution items.
726    pub fn len(&self) -> usize { self.inner.actuation.num_seats }
727
728    /// Whether the distribution contains no items.
729    pub fn is_empty(&self) -> bool { self.inner.actuation.num_seats == 0 }
730
731    /// Maximum selected cardinality.
732    pub fn sample_size(&self) -> usize { self.inner.budget.capacity as usize }
733
734    /// Number of selected items.
735    pub fn selected_len(&self) -> usize { self.inner.budget.allocated as usize }
736
737    /// Read one distribution weight.
738    pub fn weight(&self, item: usize) -> Option<u64> {
739        proof { use_type_invariant(&*self); }
740        if item < self.inner.actuation.num_seats { Some(self.inner.weight(item)) } else { None }
741    }
742
743    /// Whether an item has already been selected.
744    pub fn contains(&self, item: usize) -> bool {
745        proof { use_type_invariant(&*self); }
746        self.inner.contains_exec(item)
747    }
748
749    /// Admit one supported item directly.
750    ///
751    /// # Errors
752    ///
753    /// Returns an error when the item is unknown, unsupported, already selected, or
754    /// the sample is full.
755    pub fn sample(&mut self, item: usize) -> (result: Result<(), SamplerError>) {
756        proof { use_type_invariant(&*self); }
757        if item >= self.inner.actuation.num_seats { return Err(SamplerError::ItemOutOfRange); }
758        if self.inner.budget.allocated >= self.inner.budget.capacity {
759            return Err(SamplerError::SampleFull);
760        }
761        if self.inner.weight(item) == 0 { return Err(SamplerError::OutsideSupport); }
762        if self.inner.contains_exec(item) { return Err(SamplerError::AlreadySelected); }
763        let mut carrier = sampler_sentinel();
764        core::mem::swap(&mut self.inner, &mut carrier);
765        carrier.sample(item);
766        core::mem::swap(&mut self.inner, &mut carrier);
767        Ok(())
768    }
769
770    /// Remove an unselected item from the live support.
771    #[must_use]
772    pub fn zero(&mut self, item: usize) -> (accepted: bool) {
773        proof { use_type_invariant(&*self); }
774        let mut carrier = sampler_sentinel();
775        core::mem::swap(&mut self.inner, &mut carrier);
776        let accepted = carrier.zero(item);
777        core::mem::swap(&mut self.inner, &mut carrier);
778        accepted
779    }
780
781    /// Apply weighted rejection to an externally proposed item and entropy value.
782    ///
783    /// # Errors
784    ///
785    /// Returns [`SamplerError::ItemOutOfRange`] for an unknown item.
786    pub fn draw_weighted(&mut self, item: usize, entropy: u64) -> (result: Result<bool, SamplerError>) {
787        proof { use_type_invariant(&*self); }
788        if item >= self.inner.actuation.num_seats { return Err(SamplerError::ItemOutOfRange); }
789        let mut carrier = sampler_sentinel();
790        core::mem::swap(&mut self.inner, &mut carrier);
791        let accepted = carrier.draw_weighted(item, entropy);
792        core::mem::swap(&mut self.inner, &mut carrier);
793        Ok(accepted)
794    }
795
796    /// Apply uniform-support admission to an externally proposed item.
797    ///
798    /// # Errors
799    ///
800    /// Returns [`SamplerError::ItemOutOfRange`] for an unknown item.
801    pub fn draw_uniform(&mut self, item: usize) -> (result: Result<bool, SamplerError>) {
802        proof { use_type_invariant(&*self); }
803        if item >= self.inner.actuation.num_seats { return Err(SamplerError::ItemOutOfRange); }
804        let mut carrier = sampler_sentinel();
805        core::mem::swap(&mut self.inner, &mut carrier);
806        let accepted = carrier.draw_uniform(item);
807        core::mem::swap(&mut self.inner, &mut carrier);
808        Ok(accepted)
809    }
810}
811
812/// Invalid signal configuration.
813#[derive(Clone, Copy, Debug, Eq, PartialEq)]
814#[non_exhaustive]
815pub enum SignalBuildError {
816    /// The initial value is outside the configured value universe.
817    InitialValueOutOfRange,
818}
819
820/// A disabled signal transition.
821#[derive(Clone, Copy, Debug, Eq, PartialEq)]
822#[non_exhaustive]
823pub enum SignalError {
824    /// A value is outside the configured value universe.
825    ValueOutOfRange,
826    /// A listener is outside the configured listener universe.
827    ListenerOutOfRange,
828    /// The listener has no pending notification.
829    ListenerNotPending,
830    /// The configured change log cannot accept another value change.
831    ChangeCapacityExhausted,
832}
833
834/// A change-detecting signal with per-listener notification provenance.
835///
836/// # Examples
837///
838/// ```rust
839/// use automation_structures::Signal;
840///
841/// let mut signal = Signal::new(0, 2, 1)?;
842/// assert!(signal.set_value(1)?);
843/// signal.notify(0)?;
844/// assert_eq!(signal.is_notified(0), Some(true));
845/// # Ok::<(), Box<dyn std::error::Error>>(())
846/// ```
847pub struct Signal {
848    inner: SignalCarrier,
849}
850
851impl Signal {
852    #[verifier::type_invariant]
853    closed spec fn well_formed(&self) -> bool {
854        self.inner.inv()
855    }
856
857    /// Construct a signal with no pending notification and the largest representable change log.
858    ///
859    /// # Errors
860    ///
861    /// Returns [`SignalBuildError::InitialValueOutOfRange`] when the initial value is
862    /// outside the configured value universe.
863    pub fn new(initial_value: u64, num_values: u64, num_listeners: usize)
864        -> (result: Result<Self, SignalBuildError>) {
865        Self::with_change_capacity(initial_value, num_values, num_listeners, usize::MAX)
866    }
867
868    /// Construct a signal with an explicit maximum number of retained value changes.
869    ///
870    /// # Errors
871    ///
872    /// Returns [`SignalBuildError::InitialValueOutOfRange`] when the initial value is
873    /// outside the configured value universe.
874    pub fn with_change_capacity(
875        initial_value: u64,
876        num_values: u64,
877        num_listeners: usize,
878        max_changes: usize,
879    ) -> (result: Result<Self, SignalBuildError>) {
880        if initial_value >= num_values { return Err(SignalBuildError::InitialValueOutOfRange); }
881        Ok(Self { inner: SignalCarrier::new(initial_value, num_values, num_listeners, max_changes) })
882    }
883
884    /// Current retained value.
885    pub fn value(&self) -> u64 {
886        proof { use_type_invariant(&*self); }
887        self.inner.current_value()
888    }
889
890    /// Number of listeners.
891    pub fn listener_count(&self) -> usize { self.inner.num_listeners }
892
893    /// Whether any actual value change has occurred.
894    pub fn change_observed(&self) -> bool { !self.inner.audit.log.is_empty() }
895
896    /// Maximum number of retained value changes.
897    pub fn change_capacity(&self) -> usize { self.inner.audit.max_log_len }
898
899    /// Number of retained value changes.
900    pub fn change_count(&self) -> usize { self.inner.audit.log.len() }
901
902    /// Whether one listener has a pending notification.
903    pub fn is_pending(&self, listener: usize) -> Option<bool> {
904        proof { use_type_invariant(&*self); }
905        if listener < self.inner.num_listeners { Some(self.inner.is_pending(listener)) } else { None }
906    }
907
908    /// Whether one listener has received the latest notification.
909    pub fn is_notified(&self, listener: usize) -> Option<bool> {
910        proof { use_type_invariant(&*self); }
911        if listener < self.inner.num_listeners { Some(self.inner.is_notified(listener)) } else { None }
912    }
913
914    /// Set a value, returning false for an unchanged value.
915    ///
916    /// # Errors
917    ///
918    /// Returns an error when the value is outside the configured universe or the
919    /// retained change log is full.
920    pub fn set_value(&mut self, value: u64) -> (result: Result<bool, SignalError>) {
921        proof { use_type_invariant(&*self); }
922        if value >= self.inner.num_values { return Err(SignalError::ValueOutOfRange); }
923        let current = self.inner.current_value();
924        if value == current { return Ok(false); }
925        if self.inner.audit.log.len() >= self.inner.audit.max_log_len {
926            return Err(SignalError::ChangeCapacityExhausted);
927        }
928        let mut carrier = signal_sentinel();
929        core::mem::swap(&mut self.inner, &mut carrier);
930        carrier.set_value(value);
931        core::mem::swap(&mut self.inner, &mut carrier);
932        Ok(true)
933    }
934
935    /// Move one listener's pending notification into delivered state.
936    ///
937    /// # Errors
938    ///
939    /// Returns an error when the listener is unknown or has no pending notification.
940    pub fn notify(&mut self, listener: usize) -> (result: Result<(), SignalError>) {
941        proof { use_type_invariant(&*self); }
942        if listener >= self.inner.num_listeners { return Err(SignalError::ListenerOutOfRange); }
943        if !self.inner.is_pending(listener) { return Err(SignalError::ListenerNotPending); }
944        let mut carrier = signal_sentinel();
945        core::mem::swap(&mut self.inner, &mut carrier);
946        carrier.notify_listener(listener);
947        core::mem::swap(&mut self.inner, &mut carrier);
948        Ok(())
949    }
950}
951
952/// Invalid traversal-engine configuration.
953#[derive(Clone, Copy, Debug, Eq, PartialEq)]
954#[non_exhaustive]
955pub enum TraversalBuildError {
956    /// At least one node is required.
957    NoNodes,
958    /// The root is outside the node universe.
959    RootOutOfRange,
960}
961
962/// A disabled traversal-engine transition.
963#[derive(Clone, Copy, Debug, Eq, PartialEq)]
964#[non_exhaustive]
965pub enum TraversalError {
966    /// The node is outside the configured universe.
967    NodeOutOfRange,
968    /// The node is not queued.
969    NodeNotQueued,
970    /// The node has already been visited.
971    NodeAlreadyVisited,
972    /// Termination is enabled only when the queue is empty.
973    QueueNotEmpty,
974}
975
976/// A budgeted star-graph traversal with accepted-subset tracking.
977///
978/// The root has an edge to every other node, and each accepted node costs two
979/// budget units. This checked profile fixes both the topology and node cost.
980///
981/// # Examples
982///
983/// ```rust
984/// use automation_structures::TraversalEngine;
985///
986/// let mut traversal = TraversalEngine::new(3, 0, 2)?;
987/// traversal.visit(0)?;
988/// assert!(traversal.is_visited(0));
989/// # Ok::<(), Box<dyn std::error::Error>>(())
990/// ```
991pub struct TraversalEngine {
992    inner: TraversalEngineCarrier,
993}
994
995impl TraversalEngine {
996    #[verifier::type_invariant]
997    closed spec fn well_formed(&self) -> bool {
998        self.inner.inv()
999    }
1000
1001    /// Construct a traversal rooted in the configured node universe.
1002    ///
1003    /// # Errors
1004    ///
1005    /// Returns an error when the node universe is empty or the root is outside it.
1006    pub fn new(num_nodes: usize, root: usize, budget: u64)
1007        -> (result: Result<Self, TraversalBuildError>) {
1008        if num_nodes == 0 { return Err(TraversalBuildError::NoNodes); }
1009        if root >= num_nodes { return Err(TraversalBuildError::RootOutOfRange); }
1010        Ok(Self { inner: TraversalEngineCarrier::new(num_nodes, root, budget) })
1011    }
1012
1013    /// Number of nodes.
1014    pub fn num_nodes(&self) -> usize { self.inner.num_nodes }
1015
1016    /// Traversal root.
1017    pub fn root(&self) -> usize { self.inner.root }
1018
1019    /// Remaining traversal budget.
1020    pub fn budget_remaining(&self) -> u64 {
1021        proof { use_type_invariant(&*self); }
1022        self.inner.budget_remaining()
1023    }
1024
1025    /// Number of queued nodes.
1026    pub fn queued_len(&self) -> usize { self.inner.queue.len() }
1027
1028    /// Number of visited nodes.
1029    pub fn visited_len(&self) -> usize { self.inner.visited_count() }
1030
1031    /// Number of budget-accepted nodes.
1032    pub fn accepted_len(&self) -> usize { self.inner.accepted.len() }
1033
1034    /// Total cost committed for budget-accepted nodes.
1035    pub fn accepted_cost(&self) -> u64 { self.inner.budget.allocated }
1036
1037    /// Whether a node is queued.
1038    pub fn is_queued(&self, node: usize) -> bool { self.inner.queue_contains(node) }
1039
1040    /// Whether a node was visited.
1041    pub fn is_visited(&self, node: usize) -> bool { self.inner.visited_contains(node) }
1042
1043    /// Whether a node was accepted under the budget.
1044    pub fn is_accepted(&self, node: usize) -> bool { self.inner.accepted_contains(node) }
1045
1046    /// Visit one queued, unvisited node.
1047    ///
1048    /// # Errors
1049    ///
1050    /// Returns an error when the node is unknown, not queued, or already visited.
1051    pub fn visit(&mut self, node: usize) -> (result: Result<(), TraversalError>) {
1052        proof { use_type_invariant(&*self); }
1053        if node >= self.inner.num_nodes { return Err(TraversalError::NodeOutOfRange); }
1054        if !self.inner.queue_contains(node) { return Err(TraversalError::NodeNotQueued); }
1055        if self.inner.visited_contains(node) { return Err(TraversalError::NodeAlreadyVisited); }
1056        let mut carrier = traversal_engine_sentinel();
1057        core::mem::swap(&mut self.inner, &mut carrier);
1058        carrier.visit_node(node);
1059        core::mem::swap(&mut self.inner, &mut carrier);
1060        Ok(())
1061    }
1062
1063    /// Remove one queued node without visiting it.
1064    ///
1065    /// # Errors
1066    ///
1067    /// Returns an error when the node is unknown, not queued, or already visited.
1068    pub fn skip(&mut self, node: usize) -> (result: Result<(), TraversalError>) {
1069        proof { use_type_invariant(&*self); }
1070        if node >= self.inner.num_nodes { return Err(TraversalError::NodeOutOfRange); }
1071        if !self.inner.queue_contains(node) { return Err(TraversalError::NodeNotQueued); }
1072        let mut carrier = traversal_engine_sentinel();
1073        core::mem::swap(&mut self.inner, &mut carrier);
1074        carrier.skip(node);
1075        core::mem::swap(&mut self.inner, &mut carrier);
1076        Ok(())
1077    }
1078
1079    /// Confirm the terminal stutter when no queued work remains.
1080    ///
1081    /// # Errors
1082    ///
1083    /// Returns [`TraversalError::QueueNotEmpty`] while work remains queued.
1084    pub fn terminate(&mut self) -> (result: Result<(), TraversalError>) {
1085        proof { use_type_invariant(&*self); }
1086        if !self.inner.queue.is_empty() { return Err(TraversalError::QueueNotEmpty); }
1087        let mut carrier = traversal_engine_sentinel();
1088        core::mem::swap(&mut self.inner, &mut carrier);
1089        carrier.terminate();
1090        core::mem::swap(&mut self.inner, &mut carrier);
1091        Ok(())
1092    }
1093}
1094
1095/// Invalid select-then-actuate configuration.
1096#[derive(Clone, Copy, Debug, Eq, PartialEq)]
1097#[non_exhaustive]
1098pub enum SelectThenActuateBuildError {
1099    /// Hard selection requires at least one candidate.
1100    NoCandidates,
1101}
1102
1103/// A disabled select-then-actuate transition.
1104#[derive(Clone, Copy, Debug, Eq, PartialEq)]
1105#[non_exhaustive]
1106pub enum SelectThenActuateError {
1107    /// The seat index is outside the configured seat universe.
1108    SeatOutOfRange,
1109    /// The candidate index is outside the configured candidate universe.
1110    CandidateOutOfRange,
1111    /// The pass has already committed its closure transition.
1112    PassComplete,
1113    /// The seat already has a selected allocation.
1114    SeatAlreadyAllocated,
1115    /// A score cannot change after the seat's effect has been applied.
1116    EffectAlreadyApplied,
1117    /// The seat has no selected allocation to actuate.
1118    SeatNotAllocated,
1119    /// The seat's selected allocation has already been actuated.
1120    SeatAlreadyActuated,
1121    /// At least one allocated seat still awaits actuation.
1122    PassNotReady,
1123}
1124
1125/// Hard selection per seat followed by the shared `ActuationPass` lifecycle.
1126///
1127/// # Examples
1128///
1129/// ```rust
1130/// use automation_structures::SelectThenActuate;
1131///
1132/// let mut pass = SelectThenActuate::new(1, 2)?;
1133/// pass.update_score(0, 1, 9)?;
1134/// assert_eq!(pass.evaluate(0)?, 1);
1135/// pass.actuate(0)?;
1136/// pass.finish()?;
1137/// assert!(pass.is_complete());
1138/// # Ok::<(), Box<dyn std::error::Error>>(())
1139/// ```
1140pub struct SelectThenActuate {
1141    inner: SelectThenActuateCarrier,
1142}
1143
1144impl SelectThenActuate {
1145    #[verifier::type_invariant]
1146    closed spec fn well_formed(&self) -> bool { self.inner.inv() }
1147
1148    /// Construct empty seat allocations over a nonempty candidate universe.
1149    ///
1150    /// # Errors
1151    ///
1152    /// Returns an error when either configured dimension is zero.
1153    pub fn new(num_seats: usize, num_candidates: usize)
1154        -> (result: Result<Self, SelectThenActuateBuildError>) {
1155        if num_candidates == 0 { return Err(SelectThenActuateBuildError::NoCandidates); }
1156        Ok(Self { inner: SelectThenActuateCarrier::new(num_seats, num_candidates) })
1157    }
1158
1159    /// Number of independently selected seats.
1160    pub fn seat_count(&self) -> usize { self.inner.selections.len() }
1161
1162    /// Number of candidates available to each seat.
1163    pub fn candidate_count(&self) -> usize { self.inner.num_candidates }
1164
1165    /// Read one score when both indices are in range.
1166    pub fn score(&self, seat: usize, candidate: usize) -> Option<u64> {
1167        proof { use_type_invariant(&*self); }
1168        if seat >= self.inner.selections.len() || candidate >= self.inner.num_candidates {
1169            None
1170        } else {
1171            Some(self.inner.score_at(seat, candidate))
1172        }
1173    }
1174
1175    /// Read one seat's current selected candidate.
1176    pub fn allocation(&self, seat: usize) -> Option<usize> {
1177        proof { use_type_invariant(&*self); }
1178        if seat >= self.inner.selections.len() { None } else { self.inner.allocation_at(seat) }
1179    }
1180
1181    /// Whether one in-range seat has applied its selected effect.
1182    pub fn is_actuated(&self, seat: usize) -> Option<bool> {
1183        proof { use_type_invariant(&*self); }
1184        if seat >= self.inner.selections.len() { None } else { Some(self.inner.is_actuated(seat)) }
1185    }
1186
1187    /// Whether the shared actuation pass is complete.
1188    pub fn is_complete(&self) -> bool { self.inner.is_complete() }
1189
1190    /// Revise one unapplied seat's candidate score.
1191    ///
1192    /// # Errors
1193    ///
1194    /// Returns an error for an unknown seat or candidate, or after evaluation has begun.
1195    pub fn update_score(
1196        &mut self,
1197        seat: usize,
1198        candidate: usize,
1199        value: u64,
1200    ) -> (result: Result<(), SelectThenActuateError>) {
1201        proof { use_type_invariant(&*self); }
1202        if seat >= self.inner.selections.len() {
1203            return Err(SelectThenActuateError::SeatOutOfRange);
1204        }
1205        if candidate >= self.inner.num_candidates {
1206            return Err(SelectThenActuateError::CandidateOutOfRange);
1207        }
1208        if self.inner.actuation.complete { return Err(SelectThenActuateError::PassComplete); }
1209        if self.inner.is_actuated(seat) {
1210            return Err(SelectThenActuateError::EffectAlreadyApplied);
1211        }
1212        let mut carrier = select_then_actuate_sentinel();
1213        core::mem::swap(&mut self.inner, &mut carrier);
1214        carrier.update_score(seat, candidate, value);
1215        core::mem::swap(&mut self.inner, &mut carrier);
1216        Ok(())
1217    }
1218
1219    /// Select the highest-scoring candidate for one empty seat.
1220    ///
1221    /// # Errors
1222    ///
1223    /// Returns an error when the seat is unknown, already evaluated, or evaluation is disabled.
1224    pub fn evaluate(&mut self, seat: usize) -> (result: Result<usize, SelectThenActuateError>) {
1225        proof { use_type_invariant(&*self); }
1226        if seat >= self.inner.selections.len() {
1227            return Err(SelectThenActuateError::SeatOutOfRange);
1228        }
1229        if self.inner.actuation.complete { return Err(SelectThenActuateError::PassComplete); }
1230        if self.inner.is_allocated(seat) {
1231            return Err(SelectThenActuateError::SeatAlreadyAllocated);
1232        }
1233        let mut carrier = select_then_actuate_sentinel();
1234        core::mem::swap(&mut self.inner, &mut carrier);
1235        carrier.evaluate(seat);
1236        let winner = match carrier.allocation_at(seat) {
1237            Some(candidate) => candidate,
1238            None => {
1239                core::mem::swap(&mut self.inner, &mut carrier);
1240                return Err(SelectThenActuateError::SeatNotAllocated);
1241            },
1242        };
1243        core::mem::swap(&mut self.inner, &mut carrier);
1244        Ok(winner)
1245    }
1246
1247    /// Apply one seat's selected candidate through ActuationPass.
1248    ///
1249    /// # Errors
1250    ///
1251    /// Returns an error when the seat is unknown, not evaluated, already actuated, or
1252    /// actuation is disabled.
1253    pub fn actuate(&mut self, seat: usize) -> (result: Result<(), SelectThenActuateError>) {
1254        proof { use_type_invariant(&*self); }
1255        if seat >= self.inner.selections.len() {
1256            return Err(SelectThenActuateError::SeatOutOfRange);
1257        }
1258        if self.inner.actuation.complete { return Err(SelectThenActuateError::PassComplete); }
1259        if !self.inner.is_allocated(seat) {
1260            return Err(SelectThenActuateError::SeatNotAllocated);
1261        }
1262        if self.inner.is_actuated(seat) {
1263            return Err(SelectThenActuateError::SeatAlreadyActuated);
1264        }
1265        let mut carrier = select_then_actuate_sentinel();
1266        core::mem::swap(&mut self.inner, &mut carrier);
1267        carrier.actuate(seat);
1268        core::mem::swap(&mut self.inner, &mut carrier);
1269        Ok(())
1270    }
1271
1272    /// Close the shared ActuationPass after every allocation is applied.
1273    ///
1274    /// # Errors
1275    ///
1276    /// Returns an error when the pass is already complete or not all seats were actuated.
1277    pub fn finish(&mut self) -> (result: Result<(), SelectThenActuateError>) {
1278        proof { use_type_invariant(&*self); }
1279        if self.inner.actuation.complete { return Err(SelectThenActuateError::PassComplete); }
1280        if !self.inner.can_finish() { return Err(SelectThenActuateError::PassNotReady); }
1281        let mut carrier = select_then_actuate_sentinel();
1282        core::mem::swap(&mut self.inner, &mut carrier);
1283        carrier.finish();
1284        core::mem::swap(&mut self.inner, &mut carrier);
1285        Ok(())
1286    }
1287}
1288
1289proof fn lemma_u64_domain_fits_64(value: u64)
1290    ensures value as int <= crate::compositions::bisection::pow2(64),
1291{
1292    assert(crate::compositions::bisection::pow2(64) == 18_446_744_073_709_551_616int) by (compute);
1293}
1294
1295fn allocation_snapshot_sentinel() -> (carrier: AllocationSnapshotCarrier)
1296    ensures carrier.type_invariant(), carrier.budget_consistency(),
1297{ AllocationSnapshotCarrier::new(0, 0) }
1298
1299fn federated_budget_sentinel() -> (carrier: FederatedBudgetCarrier)
1300    ensures carrier.inv(),
1301{ FederatedBudgetCarrier::new(0, 0) }
1302
1303fn bisection_sentinel() -> (carrier: BisectionCarrier)
1304    ensures carrier.invariant(),
1305{
1306    proof {
1307        assert(crate::compositions::bisection::pow2(1) == 2) by (compute);
1308    }
1309    BisectionCarrier::new(0, 2, 1, 2, 1)
1310}
1311
1312fn equivalence_class_sentinel() -> (carrier: EquivalenceClassCarrier)
1313    ensures carrier.inv(),
1314{ EquivalenceClassCarrier::new(0, 0) }
1315
1316fn rate_limit_sentinel() -> (carrier: RateLimitCarrier)
1317    ensures carrier.type_invariant(), carrier.window_start_not_future(),
1318        carrier.window_duration > 0,
1319{ RateLimitCarrier::new(1, 1, 0) }
1320
1321fn reduction_sentinel() -> (carrier: ReductionCarrier)
1322    ensures carrier.inv(),
1323{
1324    let values: Vec<u64> = Vec::new();
1325    ReductionCarrier::new(values)
1326}
1327
1328fn relationship_graph_sentinel() -> (carrier: RelationshipGraphCarrier)
1329    ensures carrier.inv(),
1330{ RelationshipGraphCarrier::new(0, 0) }
1331
1332fn sampler_sentinel() -> (carrier: SamplerCarrier)
1333    ensures carrier.inv(),
1334{
1335    let distribution: Vec<u64> = Vec::new();
1336    SamplerCarrier::new(distribution, 0)
1337}
1338
1339fn signal_sentinel() -> (carrier: SignalCarrier)
1340    ensures carrier.inv(),
1341{ SignalCarrier::new(0, 1, 0, 0) }
1342
1343fn traversal_engine_sentinel() -> (carrier: TraversalEngineCarrier)
1344    ensures carrier.inv(),
1345{ TraversalEngineCarrier::new(1, 0, 0) }
1346
1347fn select_then_actuate_sentinel() -> (carrier: SelectThenActuateCarrier)
1348    ensures carrier.inv(),
1349{ SelectThenActuateCarrier::new(0, 1) }
1350
1351}
1352
1353impl AllocationSnapshot {
1354    /// Iterate over accepted `(node, cost)` pairs in insertion order.
1355    pub fn accepted_entries(&self) -> impl ExactSizeIterator<Item = &(u64, u64)> {
1356        self.inner.registry.entries.iter()
1357    }
1358}
1359
1360impl FederatedBudget {
1361    /// Master capacity not yet delegated to a sub-pool.
1362    pub fn master_available(&self) -> u64 {
1363        self.inner.master.available()
1364    }
1365
1366    /// Iterate over `(delegated capacity, allocated capacity)` for each sub-pool.
1367    pub fn pools(&self) -> impl ExactSizeIterator<Item = (u64, u64)> + '_ {
1368        self.inner
1369            .sub_pools
1370            .iter()
1371            .map(|pool| (pool.allocated + pool.reserved, pool.allocated))
1372    }
1373}
1374
1375impl EquivalenceClass {
1376    /// Iterate over each element and its current representative.
1377    pub fn representatives(&self) -> impl ExactSizeIterator<Item = (usize, usize)> + '_ {
1378        (0..self.len()).map(|element| (element, self.inner.find(element)))
1379    }
1380}
1381
1382impl RateLimit {
1383    /// Inclusive ceiling of the logical clock.
1384    pub fn max_clock(&self) -> u64 {
1385        self.inner.max_clock
1386    }
1387
1388    /// Operations still available in the current window.
1389    pub fn available(&self) -> u64 {
1390        self.inner.budget.available()
1391    }
1392}
1393
1394impl Reduction {
1395    /// Borrow the immutable reduction input in original order.
1396    pub fn items(&self) -> &[u64] {
1397        self.inner.source.as_slice()
1398    }
1399
1400    /// Borrow the unprocessed suffix.
1401    pub fn remaining(&self) -> &[u64] {
1402        &self.inner.source[self.processed_len()..]
1403    }
1404}
1405
1406impl RelationshipGraph {
1407    /// Borrow exact weighted edges in insertion order.
1408    pub fn edges(&self) -> impl ExactSizeIterator<Item = (usize, usize, u64)> + '_ {
1409        self.inner.registry.entries.iter().map(|entry| entry.0)
1410    }
1411}
1412
1413impl Sampler {
1414    /// Iterate over support weights by item index.
1415    pub fn weights(&self) -> impl ExactSizeIterator<Item = u64> + '_ {
1416        self.inner
1417            .actuation
1418            .allocation
1419            .iter()
1420            .map(|entry| entry.unwrap_or(0))
1421    }
1422
1423    /// Iterate over selected item indices.
1424    pub fn selected(&self) -> impl Iterator<Item = usize> + '_ {
1425        self.inner
1426            .actuation
1427            .effects
1428            .iter()
1429            .enumerate()
1430            .filter_map(|(item, effect)| effect.is_some().then_some(item))
1431    }
1432}
1433
1434impl Signal {
1435    /// Exclusive upper bound of the signal value domain.
1436    pub fn value_domain_size(&self) -> u64 {
1437        self.inner.num_values
1438    }
1439
1440    /// Iterate over `(pending, notified)` listener states.
1441    pub fn listeners(&self) -> impl ExactSizeIterator<Item = (bool, bool)> + '_ {
1442        (0..self.listener_count()).map(|listener| {
1443            (
1444                self.inner.is_pending(listener),
1445                self.inner.is_notified(listener),
1446            )
1447        })
1448    }
1449}
1450
1451impl TraversalEngine {
1452    /// Iterate over queued nodes in frontier order.
1453    pub fn queued(&self) -> impl ExactSizeIterator<Item = &usize> {
1454        self.inner.queue.values.iter()
1455    }
1456
1457    /// Iterate over visited node indices.
1458    pub fn visited(&self) -> impl Iterator<Item = usize> + '_ {
1459        self.inner
1460            .visited
1461            .iter()
1462            .enumerate()
1463            .filter_map(|(node, marker)| marker.marked.then_some(node))
1464    }
1465
1466    /// Iterate over accepted nodes in traversal order.
1467    pub fn accepted(&self) -> impl ExactSizeIterator<Item = &usize> {
1468        self.inner.accepted.accumulated.iter()
1469    }
1470}
1471
1472impl SelectThenActuate {
1473    /// Borrow one seat's candidate scores.
1474    pub fn scores(&self, seat: usize) -> Option<&[u64]> {
1475        self.inner
1476            .selections
1477            .get(seat)
1478            .map(|selection| selection.scores.as_slice())
1479    }
1480
1481    /// Iterate over current seat allocations.
1482    pub fn allocations(&self) -> impl ExactSizeIterator<Item = Option<usize>> + '_ {
1483        self.inner
1484            .selections
1485            .iter()
1486            .map(|selection| selection.allocation)
1487    }
1488
1489    /// Borrow committed effects by seat.
1490    pub fn effects(&self) -> &[Option<u64>] {
1491        self.inner.actuation.effects.as_slice()
1492    }
1493}
1494
1495impl_observational_debug!(AllocationSnapshot, "AllocationSnapshot",
1496    "capacity" => capacity,
1497    "num_nodes" => num_nodes,
1498    "total_cost" => total_cost,
1499    "budget_remaining" => budget_remaining,
1500    "len" => len,
1501);
1502impl_observational_debug!(FederatedBudget, "FederatedBudget",
1503    "master_capacity" => master_capacity,
1504    "master_allocated" => master_allocated,
1505    "len" => len,
1506);
1507impl_observational_debug!(Bisection, "Bisection",
1508    "lower" => lower,
1509    "upper" => upper,
1510    "threshold" => threshold,
1511    "probes_taken" => probes_taken,
1512    "max_probes" => max_probes,
1513    "converged" => is_converged,
1514);
1515impl_observational_debug!(EquivalenceClass, "EquivalenceClass",
1516    "len" => len,
1517    "unions_performed" => unions_performed,
1518    "max_unions" => max_unions,
1519);
1520impl_observational_debug!(RateLimit, "RateLimit",
1521    "max_per_window" => max_per_window,
1522    "window_duration" => window_duration,
1523    "count" => count,
1524    "clock" => clock,
1525    "window_start" => window_start,
1526);
1527impl_observational_debug!(Reduction, "Reduction",
1528    "result" => result,
1529    "processed_len" => processed_len,
1530    "remaining_len" => remaining_len,
1531    "complete" => is_complete,
1532);
1533impl_observational_debug!(RelationshipGraph, "RelationshipGraph",
1534    "num_nodes" => num_nodes,
1535    "max_weight" => max_weight,
1536    "edge_count" => edge_count,
1537);
1538impl_observational_debug!(Sampler, "Sampler",
1539    "len" => len,
1540    "sample_size" => sample_size,
1541    "selected_len" => selected_len,
1542);
1543impl_observational_debug!(Signal, "Signal",
1544    "value" => value,
1545    "listener_count" => listener_count,
1546    "change_observed" => change_observed,
1547);
1548impl_observational_debug!(TraversalEngine, "TraversalEngine",
1549    "num_nodes" => num_nodes,
1550    "root" => root,
1551    "budget_remaining" => budget_remaining,
1552    "queued_len" => queued_len,
1553    "visited_len" => visited_len,
1554    "accepted_len" => accepted_len,
1555    "accepted_cost" => accepted_cost,
1556);
1557impl_observational_debug!(SelectThenActuate, "SelectThenActuate",
1558    "seat_count" => seat_count,
1559    "candidate_count" => candidate_count,
1560    "complete" => is_complete,
1561);
1562
1563impl_public_error!(AllocationSnapshotError, {
1564    Self::NodeOutOfRange => "node is outside the snapshot universe",
1565    Self::NodeAlreadyAccepted => "node is already accepted",
1566    Self::ZeroCost => "accepted node cost must be positive",
1567    Self::InsufficientBudget => "node cost exceeds the remaining budget",
1568});
1569impl_public_error!(BisectionBuildError, {
1570    Self::DomainTooSmall => "bisection domain must contain at least two points",
1571    Self::ThresholdOutOfRange => "bisection threshold is outside the domain",
1572});
1573impl_public_error!(BisectionError, { Self::AlreadyConverged => "bisection is already converged" });
1574impl_public_error!(EquivalenceClassError, { Self::ElementOutOfRange => "element is outside the partition" });
1575impl_public_error!(RateLimitBuildError, {
1576    Self::ZeroLimit => "rate limit must admit at least one operation",
1577    Self::ZeroWindowDuration => "rate-limit window duration must be positive",
1578});
1579impl_public_error!(RateLimitError, { Self::ClockExhausted => "rate-limit logical clock is exhausted" });
1580impl_public_error!(ReductionBuildError, {
1581    Self::TooManyItems => "reduction input exceeds the verified item ceiling",
1582    Self::ValueOutOfRange => "reduction input exceeds the verified value ceiling",
1583});
1584impl_public_error!(ReductionError, { Self::Complete => "reduction is already complete" });
1585impl_public_error!(RelationshipGraphError, {
1586    Self::NodeOutOfRange => "graph node is outside the configured universe",
1587    Self::WeightOutOfRange => "edge weight exceeds the configured maximum",
1588    Self::SelfLoop => "relationship graph does not admit self-loops",
1589});
1590impl_public_error!(SamplerError, {
1591    Self::ItemOutOfRange => "sample item is outside the distribution",
1592    Self::SampleFull => "bounded sample is full",
1593    Self::OutsideSupport => "sample item has zero support weight",
1594    Self::AlreadySelected => "sample item is already selected",
1595});
1596impl_public_error!(SignalBuildError, { Self::InitialValueOutOfRange => "initial signal value is outside its universe" });
1597impl_public_error!(SignalError, {
1598    Self::ValueOutOfRange => "signal value is outside its universe",
1599    Self::ListenerOutOfRange => "listener is outside the signal universe",
1600    Self::ListenerNotPending => "listener has no pending notification",
1601    Self::ChangeCapacityExhausted => "signal change capacity is exhausted",
1602});
1603impl_public_error!(TraversalBuildError, {
1604    Self::NoNodes => "traversal requires at least one node",
1605    Self::RootOutOfRange => "traversal root is outside the node universe",
1606});
1607impl_public_error!(TraversalError, {
1608    Self::NodeOutOfRange => "traversal node is outside the configured universe",
1609    Self::NodeNotQueued => "traversal node is not queued",
1610    Self::NodeAlreadyVisited => "traversal node was already visited",
1611    Self::QueueNotEmpty => "traversal queue is not empty",
1612});
1613impl_public_error!(SelectThenActuateBuildError, {
1614    Self::NoCandidates => "select-then-actuate requires at least one candidate",
1615});
1616impl_public_error!(SelectThenActuateError, {
1617    Self::SeatOutOfRange => "seat is outside the configured universe",
1618    Self::CandidateOutOfRange => "candidate is outside the configured universe",
1619    Self::PassComplete => "actuation pass is already complete",
1620    Self::SeatAlreadyAllocated => "seat already has an allocation",
1621    Self::EffectAlreadyApplied => "applied seat score cannot change",
1622    Self::SeatNotAllocated => "seat has no allocation",
1623    Self::SeatAlreadyActuated => "seat allocation is already actuated",
1624    Self::PassNotReady => "actuation pass still has unapplied allocations",
1625});
automation_structures/composition_api.rs

automation_structures/
composition_api.rs
