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

automation_structures/
composition_api.rs
