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 is the sole Rust owner of its invariant-bearing state and admissible transitions. Its contract states the consequences that follow when callers satisfy the documented assumptions. Applications supply the identifiers, values, scores, costs, policies, effects, and operating boundary that give those consequences domain meaning. State ownership inside this crate is not, by itself, deployment accountability or authority to guarantee an application-level obligation.

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	Bounded contract consequence
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 recomputed chain value; collision resistance, durable custody, and tamper detection are outside this carrier
Run snapshot-local graph updates	`PropagationPass`	Each node updates once per round from the same snapshot
Separate allocation from recorded effect commitment	`ActuationPass`	Each allocated seat records at most one corresponding effect before closure; external effect execution is outside this carrier
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, and every recorded visit is a valid full-depth leaf; exhaustive coverage is not claimed
Choose among candidates using hard, hard-exclusive, soft, or ranked profiles	`CompetitiveSelectionHard`, `CompetitiveSelectionHardExclusive`, `CompetitiveSelectionSoft`, `CompetitiveSelectionRanked`	Each profile enforces its stated allocation rule and deterministic tie policy; the catalog's mutable-score proof profile is a soft-mode profile
Settle and reawaken from a bounded delta history	`ConvergenceGovernor`	Phase-aware convergence and reawakening

Connective forms

Need	Type or function	Bounded contract consequence
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 irreflexive edges and derive adjacency	`RelationshipGraph`	Edge `ResourceRegistry` plus projection relation; the public profile rejects self-loops
Select a bounded weighted sample without replacement	`Sampler`	`ActuationPass + Budget`; caller choices must be in support, but no randomness-quality claim is made
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	Bounded contract consequence
Execute a fixed sequence	`Sequential`	One active step and exact agreement between committed-history length and current position
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, count conservation, and a state-level enabled action; scheduler progress is not claimed

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.

State-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 an application policy that names one accountable owner and treats synchronization or delegated custody as a trust boundary. Several components may own disjoint state, but the same framed obligation does not acquire several accountable owners merely because they collaborate.

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 contract clauses 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.2