mary 0.1.0

//! 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));
//! ```

/// An RGB color whose channels are bounded by construction.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct Rgb {
    /// Red channel.
    pub r: u8,
    /// Green channel.
    pub g: u8,
    /// Blue channel.
    pub b: u8,
}

impl Rgb {
    /// Constructs an RGB color.
    #[must_use]
    pub const fn new(r: u8, g: u8, b: u8) -> Self {
        Self { r, g, b }
    }

    /// Adds a gain without allowing a channel to wrap.
    #[must_use]
    pub const fn add_sat(self, gain: Self) -> Self {
        Self {
            r: self.r.saturating_add(gain.r),
            g: self.g.saturating_add(gain.g),
            b: self.b.saturating_add(gain.b),
        }
    }
}

/// The complete adaptation state for the executable kernel.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum Adaptation {
    /// No adjustment has occurred.
    Bleary,
    /// Adjustment has begun but has not settled.
    Adjusting,
    /// Adjustment is complete. This state is absorbing.
    Settled,
}

/// A caller-supplied transition count capped at 255 steps.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct StepCount(u8);

impl StepCount {
    /// The largest representable transition count.
    pub const MAX: Self = Self(u8::MAX);

    /// Constructs a bounded transition count.
    #[must_use]
    pub const fn new(steps: u8) -> Self {
        Self(steps)
    }

    /// Returns the underlying transition count.
    #[must_use]
    pub const fn get(self) -> u8 {
        self.0
    }
}

/// Advances the adaptation state by one observation.
#[must_use]
pub const fn advance(state: Adaptation) -> Adaptation {
    match state {
        Adaptation::Bleary => Adaptation::Adjusting,
        Adaptation::Adjusting | Adaptation::Settled => Adaptation::Settled,
    }
}

/// Applies exactly `steps` state transitions using constant stack space.
#[must_use]
pub const fn advance_by(mut state: Adaptation, steps: StepCount) -> Adaptation {
    let mut remaining = steps.get();
    while remaining != 0 {
        state = advance(state);
        remaining -= 1;
    }
    state
}

/// Returns the appearance gain selected by an adaptation state.
#[must_use]
pub const fn gain(state: Adaptation) -> Rgb {
    match state {
        Adaptation::Bleary => Rgb::new(0, 0, 0),
        Adaptation::Adjusting => Rgb::new(4, 5, 4),
        Adaptation::Settled => Rgb::new(8, 9, 8),
    }
}

/// Computes the standardized matching coordinate.
#[must_use]
pub const fn profile(state: Adaptation, stimulus: Rgb) -> Rgb {
    stimulus.add_sat(gain(state))
}

/// Computes the profile after a bounded number of state transitions.
#[must_use]
pub const fn profile_after(state: Adaptation, stimulus: Rgb, steps: StepCount) -> Rgb {
    profile(advance_by(state, steps), stimulus)
}

#[cfg(test)]
mod tests {
    use super::{Adaptation, Rgb, StepCount, advance, advance_by, profile, profile_after};

    const ADAPTATION_STATES: [Adaptation; 3] = [
        Adaptation::Bleary,
        Adaptation::Adjusting,
        Adaptation::Settled,
    ];
    const SHOWN_BLUE: Rgb = Rgb::new(0, 29, 247);

    fn expected_state(initial: Adaptation, steps: u8) -> Adaptation {
        match (initial, steps) {
            (state, 0) => state,
            (Adaptation::Bleary, 1) => Adaptation::Adjusting,
            _ => Adaptation::Settled,
        }
    }

    fn expected_channel(channel: u8, gain: u8) -> u8 {
        let sum = u16::from(channel) + u16::from(gain);
        u8::try_from(sum.min(u16::from(u8::MAX))).expect("bounded by u8::MAX")
    }

    #[test]
    fn adjustment_trajectory_matches_the_lean_example() {
        let initial = Adaptation::Bleary;
        let adjusting = advance(initial);
        let settled = advance(adjusting);

        assert_eq!(profile(initial, SHOWN_BLUE), Rgb::new(0, 29, 247));
        assert_eq!(profile(adjusting, SHOWN_BLUE), Rgb::new(4, 34, 251));
        assert_eq!(profile(settled, SHOWN_BLUE), Rgb::new(8, 38, 255));
        assert_eq!(advance(settled), settled);
    }

    #[test]
    fn channel_addition_is_saturating() {
        for channel in u8::MIN..=u8::MAX {
            for gain in u8::MIN..=u8::MAX {
                let actual = Rgb::new(channel, 0, 0).add_sat(Rgb::new(gain, 0, 0));
                let expected = u16::from(channel) + u16::from(gain);
                assert_eq!(u16::from(actual.r), expected.min(u16::from(u8::MAX)));
            }
        }
    }

    #[test]
    fn bounded_iteration_matches_repeated_advance() {
        for initial in ADAPTATION_STATES {
            let mut expected = initial;
            for steps in u8::MIN..=u8::MAX {
                let steps = StepCount::new(steps);
                assert_eq!(advance_by(initial, steps), expected);
                expected = advance(expected);
            }
        }
    }

    #[test]
    fn bounded_profile_uses_the_final_state() {
        for initial in ADAPTATION_STATES {
            for steps in u8::MIN..=u8::MAX {
                let steps = StepCount::new(steps);
                assert_eq!(
                    profile_after(initial, SHOWN_BLUE, steps),
                    profile(advance_by(initial, steps), SHOWN_BLUE)
                );
            }
        }
    }

    #[test]
    fn bounded_profile_matches_independent_finite_oracle() {
        for initial in ADAPTATION_STATES {
            for steps in u8::MIN..=u8::MAX {
                let expected_gain = match expected_state(initial, steps) {
                    Adaptation::Bleary => Rgb::new(0, 0, 0),
                    Adaptation::Adjusting => Rgb::new(4, 5, 4),
                    Adaptation::Settled => Rgb::new(8, 9, 8),
                };
                for channel in u8::MIN..=u8::MAX {
                    let stimulus = Rgb::new(channel, channel, channel);
                    let expected = Rgb::new(
                        expected_channel(channel, expected_gain.r),
                        expected_channel(channel, expected_gain.g),
                        expected_channel(channel, expected_gain.b),
                    );
                    assert_eq!(
                        profile_after(initial, stimulus, StepCount::new(steps)),
                        expected
                    );
                }
            }
        }
    }
}