mary

mary is a small, safe, dependency-free Rust kernel for a bounded color-adaptation state machine. It is the executable core of the Daemon Mary example: Rust owns the finite deterministic computation, while the surrounding Lean project owns its semantic model and machine-checked refinement proofs.

use mary::{Adaptation, Rgb, StepCount, profile_after};

let stimulus = Rgb::new(0, 29, 247);
let result = profile_after(Adaptation::Bleary, stimulus, StepCount::new(2));

assert_eq!(result, Rgb::new(8, 38, 255));

Guarantees and scope

Rgb channels are u8; channel addition saturates rather than wrapping.
Adaptation has exactly three states, and Settled is absorbing.
StepCount is distinct from channel data and bounds a call to at most 255 transitions.
Every operation is total, deterministic, synchronous, allocation-free, and constant-stack.
The crate performs no I/O, uses no unsafe, and has no dependencies.

The crate does not contain trajectories, heap-backed collections, clocks, randomness, networking, filesystem access, asynchronous tasks, sparse graph execution, or proof witnesses. Those responsibilities belong to callers or to the repository's Lean and vision layers.

Public API

Capability	Contract
`advance`	Apply one adaptation transition.
`advance_by`	Apply exactly a bounded number of transitions.
`gain`	Select the RGB gain for an adaptation state.
`Rgb::add_sat`	Add gain channel-wise without wrapping.
`profile`	Evaluate the standardized matching coordinate.
`profile_after`	Advance by a bounded count, then evaluate the profile.

Type	Construction and access
`Rgb`	Public `r`, `g`, and `b` fields; `Rgb::new`.
`Adaptation`	Public `Bleary`, `Adjusting`, and `Settled` variants.
`StepCount`	`StepCount::new`, `StepCount::get`, and `StepCount::MAX`; the stored `u8` is private.

All three public types implement Clone, Copy, Debug, Eq, and PartialEq.

Verification boundary

The repository pins Aeneas and its Rust toolchain, translates the admitted call graph into Lean, proves refinement to the native model, audits the resulting theorems for unexpected axioms, and independently replays the exported proof environment with Comparator. The verified claim is source-level refinement of the admitted Rust functions; it does not extend to Rust code generation or final-binary correctness.

A boundary change is one atomic assurance slice: the Rust API and exhaustive tests, Aeneas roots and admission policy, generated Lean, refinement and axiom audits, Comparator statements, and integrity manifest must move together.

Development

From the repository root:

cargo test -p mary
cargo clippy -p mary --all-targets -- -D warnings
cargo doc -p mary --no-deps
cargo package -p mary
scripts/aeneas.sh check color_adjustment

See the repository for the complete Lean model, trust boundary, pinned toolchains, and reproducibility checks.

License