Crate automation_structures

Expand description

§automation-structures

automation-structures is a Rust library of reusable structural building blocks for automation systems. It supplies checked state machines for admission, bounded resources, traversal, selection, propagation, coordination, and execution flow so applications can assemble these roles instead of implementing them repeatedly.

A structure owns its state, admissible transitions, and preserved obligations. Applications supply the identifiers, values, scores, costs, policies, and effects that give those transitions domain meaning.

§Install

cargo add automation-structures

The default feature set exposes the checked runtime API at the crate root.

§Quick start

use automation_structures::Budget;

let mut budget = Budget::new(8);
assert!(budget.try_reserve(3));
budget.commit_reservation(3)?;
assert_eq!(budget.allocated(), 3);
assert_eq!(budget.available(), 5);

Disabled transitions are explicit. Methods that can distinguish invalid input from disabled state return Result; conditional transitions named try_* return bool; indexed observations return Option.

§What composition means

Composition is the mechanical assembly of existing owners through explicit connective roles. A composition contains the structure owners, configuration, and only the coupling state needed to make their transitions commit together. It does not reimplement the component state machines.

For example, SelectThenActuate owns hard selection for each seat and one shared ActuationPass. Selection determines the allocation; actuation records the corresponding effect; the composition closes only after every selected allocation has been applied.

use automation_structures::SelectThenActuate;

let mut pass = SelectThenActuate::new(1, 2)?;
pass.update_score(0, 0, 4)?;
pass.update_score(0, 1, 9)?;
assert_eq!(pass.evaluate(0)?, 1);
pass.actuate(0)?;
pass.finish()?;
assert!(pass.is_complete());

Named compositions package recurring assemblies behind one checked contract. Applications can also compose the root types directly.

§Choose a structure

§Primitives

Need	Type	Structural guarantee
Own finite capacity through allocation, reservation, and eviction	`Budget`	Every capacity unit has one accounted lifecycle
Map unique resource identifiers to values	`ResourceRegistry`	At most one live value per key
Retain an append-only operation chain	`AuditSink`	Every entry names its predecessor and derived chain value
Run snapshot-local graph updates	`PropagationPass`	Each node updates once per round from the same snapshot
Separate allocation from effect commitment	`ActuationPass`	Each allocated seat actuates at most once before closure
Maintain ordered parent-child quality and cost constraints	`QualityHierarchy`	Single parent plus level and cost ordering
Traverse choices with exact undo	`BacktrackingTraversal`	Every descent records the inverse used by ascent
Select one highest-scoring candidate	`CompetitiveSelectionHard`	Argmax with deterministic lowest-index ties
Allocate unique winners across several seats	`CompetitiveSelectionHardExclusive`	Hard selection plus cross-seat mutual exclusion
Distribute a fixed weight total	`CompetitiveSelectionSoft`	Reserved-floor sequential Webster allocation
Select the top `k` candidates	`CompetitiveSelectionRanked`	Bounded multiplicity with score ordering
Settle and reawaken from a bounded delta history	`ConvergenceGovernor`	Phase-aware convergence and reawakening

§Connective forms

Need	Type or function	Structural guarantee
Preserve monotone progress	`Cursor`	Position never regresses
Move values from pending to retained history	`Accumulator<T>`	Order and membership are preserved across the boundary
Retain bounded FIFO state	`Buffer<T>`	Capacity, order, and head removal are owned once
Retain monotone numeric progress	`Counter`	Counter state and increment transition
Retain a binary fact	`Marker`	Marked/unmarked state
Relate an owner to a derived view	`projection_consistent`	The projection equals the owner-derived observation
Relate two ordered passes	`strictly_before`	The first position strictly precedes the second

§Named compositions

Need	Type	Assembly
Admit nodes while charging their costs	`AllocationSnapshot`	`ResourceRegistry + Budget`
Delegate master capacity to sub-pools	`FederatedBudget`	One master `Budget` plus one `Budget` per pool
Find a monotone boundary	`Bisection`	Probe `Budget` plus interval cursor relation
Maintain a merge-bounded partition	`EquivalenceClass`	Parent/rank registries plus operation `Budget`
Enforce a fixed logical-clock window	`RateLimit`	Operation `Budget` plus clock and window configuration
Incrementally reduce an ordered input	`Reduction`	`AuditSink` instantiated with the reduction operation
Store weighted edges and derive adjacency	`RelationshipGraph`	Edge `ResourceRegistry` plus projection relation
Select a bounded sample without replacement	`Sampler`	`ActuationPass + Budget`
Notify listeners after real value changes	`Signal`	Value-change `AuditSink` plus one `Cursor` per listener
Traverse queued graph work under a budget	`TraversalEngine`	Graph, budget, marker, accumulator, and buffer owners
Select allocations and commit their effects	`SelectThenActuate`	Hard selection owners plus one `ActuationPass`

§Execution modalities

Need	Type	Structural guarantee
Execute a fixed sequence	`Sequential`	One active step and ordered committed history
Run workers behind a join barrier	`ForkJoin`	Worker lifecycle, barrier, and stable output snapshot
Execute dependency-governed steps	`StepGraph`	A step becomes ready only after its predecessors complete
Move bounded records through FIFO stages	`StreamGraph`	Backpressure, FIFO order, and exact progress counters

The runnable catalog example constructs and exercises every checked root type:

cargo run --example catalog

§Observation and ownership

Public checked types encapsulate their state owner. They expose scalar observations, borrowed slices, and iterators without returning mutable access to invariant-bearing state. Small value-like connectives implement the standard traits their semantics support, including Debug, Default, equality, conversions, and iteration.

Authority-bearing state machines are not Clone. Cloning one would duplicate the apparent owner of a budget, allocation pass, audit chain, or execution lifecycle. Transfer them by move or place them behind the application’s chosen shared-ownership and synchronization policy.

Every public error enum implements Debug, Display, std::error::Error, equality, and copy semantics. Error enums are non-exhaustive so new diagnostic distinctions can be added without breaking downstream matches.

§Features

Feature	Contents
default	Checked runtime types and relations at the crate root
`proof-api`	Verus carriers, specifications, and proof relations under `primitives`, `connectives`, `compositions`, `modalities`, and `integration`

Verified downstream crates can enable the proof API directly:

[dependencies]
automation-structures = { version = "0.2", features = ["proof-api"] }

The checked API remains available when proof-api is enabled. docs.rs builds all features.

§Formal basis

The distributed Rust source contains Verus contracts for the carrier state, enabled transitions, and preserved invariants. The formal workflow verifies the real crate root and an external proof consumer against the unpacked .crate archive. Known-answer executables and ordinary downstream consumers exercise the same archive.

Formal definitions, refinement mappings, correspondence checks, and the theory behind the catalog are maintained in automation-structures-research. Changes to structure definitions, transition semantics, or preserved obligations originate there and flow downstream into this crate.

The verification guide records the exact verifier identity, package boundary, and reproducible commands.

§Compatibility

The minimum supported Rust version is 1.95.0. CI tests Rust 1.95.0 and current stable Rust on Linux, Windows, and macOS. Public API compatibility is checked against the latest crates.io release.

The crate follows Cargo semantic versioning. Before 1.0, a change from 0.x to 0.(x + 1) may contain API changes; patch releases preserve the public API. Changes to formal semantics are called out independently of Rust API compatibility.

§Contributing and security

The contribution guide defines the downstream implementation and evidence workflow. State ownership and composition are mapped in MAINTAINER_ARCHITECTURE.md.

Report suspected vulnerabilities through the private process in the security policy.

§License

Licensed under either of

Apache License, Version 2.0 (LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0)
MIT license (LICENSE-MIT or https://opensource.org/licenses/MIT)

at your option.

Re-exports§

pub use api::ConvergencePhase;
pub use api::ConvergenceState;
pub use api::PropagationRound;

Modules§

compositions: Named-composition carriers and proof relations for verified consumers. Named-composition carriers and their proof relations.
connectives: Connective owners and relations for verified consumers. Reusable connective roles used to assemble verified structures.
integration: Retained cross-structure verification assemblies. Retained cross-structure verification assemblies.
modalities: Execution-modality carriers and proof relations for verified consumers. Execution-modality carriers.
primitives: Primitive carriers and proof relations for verified consumers. Primitive carriers.
value_eq: Equality adapter for generic proof-facing carriers. Executable equality adapters whose contracts are tied to Verus equality.

Structs§

Accumulator: An ordered partial result paired with its pending suffix.
ActuationPass: A governed resource actuation pass.
AllocationSnapshot: A reusable accepted-node snapshot coupled to one capacity budget.
AuditRecord: A public immutable audit record.
AuditSink: A bounded append-only audit chain.
BacktrackingTraversal: A checked paired do-undo backtracking traversal.
Bisection: A bounded monotone-boundary bisection machine.
Budget: A checked budget whose three claims cannot exceed its fixed capacity.
Buffer: A bounded first-in, first-out connective.
CompetitiveSelectionHard: Lowest-index argmax selection for one set of candidate scores.
CompetitiveSelectionHardExclusive: Lowest-index argmax selection across seats with exclusive candidates.
CompetitiveSelectionRanked: Stable top-k selection by descending score and ascending candidate index.
CompetitiveSelectionSoft: Reserved-floor sequential Webster apportionment over mutable scores.
ConvergenceGovernor: A moving-window convergence state machine with peak-aware phases.
Counter: A retained nonnegative occurrence or generation count.
Cursor: A checked retained position for consumer progress.
EquivalenceClass: A bounded union-by-rank equivalence-class partition.
FederatedBudget: A master capacity pool divided into reusable sub-pools.
ForkJoin: A barriered fork-join execution with a stable output snapshot.
Marker: A reusable retained boolean marker.
PropagationPass: A snapshot-local bounded propagation pass.
QualityHierarchy: A checked refinement forest over levels, costs, parents, and child edges.
RateLimit: A logical-clock, fixed-window rate limit.
Reduction: An incremental additive ordered-prefix reduction.
RelationshipGraph: A weighted directed graph with a consistent adjacency projection.
ResourceRegistry: A unique-key resource registry.
Sampler: A bounded without-replacement sampler over caller-supplied proposals.
SelectThenActuate: Hard selection per seat followed by the shared ActuationPass lifecycle.
Sequential: A totally ordered, finite-step execution modality.
Signal: A change-detecting signal with per-listener notification provenance.
StepGraph: A predecessor-governed directed step graph.
StreamGraph: A bounded three- or four-stage FIFO stream graph.
TraversalEngine: A budgeted star-graph traversal with accepted-subset tracking.

Enums§

ActuationError: A disabled actuation transition.
AllocationSnapshotError: A disabled allocation-snapshot transition.
BacktrackingBuildError: Invalid BacktrackingTraversal construction input.
BacktrackingError: A disabled BacktrackingTraversal transition.
BisectionBuildError: Invalid bisection configuration.
BisectionError: A disabled bisection transition.
BudgetError: A disabled budget transition.
CompetitiveSelectionError: Invalid competitive-selection configuration or input.
ConvergenceBuildError: Invalid convergence-governor construction input.
ConvergenceError: A disabled convergence-governor transition.
CursorError: A rejected monotone Cursor movement.
EquivalenceClassError: An invalid equivalence-class element index.
ForkJoinBuildError: Invalid fork-join configuration.
ForkJoinPhase: The global fork-join phase.
PropagationBuildError: Invalid construction input for a propagation pass.
PropagationError: A disabled propagation transition.
QualityHierarchyError: A disabled quality-hierarchy transition.
RateLimitBuildError: Invalid rate-limit configuration.
RateLimitError: A disabled rate-limit transition.
ReductionBuildError: Invalid reduction input.
ReductionError: A disabled incremental reduction transition.
RelationshipGraphError: A disabled relationship-graph transition.
SamplerError: A disabled sampler transition.
SelectThenActuateBuildError: Invalid select-then-actuate configuration.
SelectThenActuateError: A disabled select-then-actuate transition.
SequentialBuildError: Invalid sequential-execution configuration.
SignalBuildError: Invalid signal configuration.
SignalError: A disabled signal transition.
StepGraphBuildError: Invalid step-graph configuration.
StepState: One step’s lifecycle state.
StreamGraphBuildError: Invalid stream-graph configuration.
TraversalBuildError: Invalid traversal-engine configuration.
TraversalError: A disabled traversal-engine transition.
WorkerState: One worker’s fork-join lifecycle state.

Functions§

projection_consistent: Test agreement between a projected membership answer and its source.
strictly_before: Test the strict ordering relation between two positions.