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);

# Ok::<(), automation_structures::BudgetError>(())

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());

# Ok::<(), Box<dyn std::error::Error>>(())

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.

automation-structures 0.2.0