Crate mary 

Executable kernel for the color-adjustment example.

This crate is intentionally safe, sequential, and free of I/O. Aeneas translates it into Lean; proofs and the richer semantic model remain in the Lean package.

Example

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

Structs

Rgb

An RGB color whose channels are bounded by construction.

StepCount

A caller-supplied transition count capped at 255 steps.

Enums

Adaptation

The complete adaptation state for the executable kernel.

Functions

advance

Advances the adaptation state by one observation.

advance_by

Applies exactly steps state transitions using constant stack space.

gain

Returns the appearance gain selected by an adaptation state.

profile

Computes the standardized matching coordinate.

profile_after

Computes the profile after a bounded number of state transitions.