# 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.
```rust
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
| `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. |
| `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:
```console
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](https://github.com/almanaculum/mary) for the complete Lean
model, trust boundary, pinned toolchains, and reproducibility checks.
## License
Licensed under the GNU Affero General Public License v3.0 only
(`AGPL-3.0-only`).