// Lean 4 → LambdaIR → MiniC → C → Rust
// Module: HeytingLean.PadicDecoupling.Padic.RandomWalk
// Theorem preserved: walk_bounded

use crate::valuation::padic_norm;

/// position(walk, n): cumulative sum of first n steps.
pub fn walk_position(steps: &[i64], n: usize) -> i64 {
    steps[..n].iter().sum()
}

/// Theorem preserved: walk_bounded
/// (∀n, |w_n|_p ≤ r) ⟹ (∀n, |pos(n)|_p ≤ r)
pub fn check_walk_bounded(p: u64, steps: &[i64], r: f64) -> bool {
    for n in 0..=steps.len() {
        let pos = walk_position(steps, n);
        if padic_norm(p, pos) > r + 1e-12 {
            return false;
        }
    }
    true
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn position_cumulative() {
        let steps = [1, 2, 3];
        assert_eq!(walk_position(&steps, 0), 0);
        assert_eq!(walk_position(&steps, 2), 3);
        assert_eq!(walk_position(&steps, 3), 6);
    }

    #[test]
    fn bounded_walk() {
        // Steps all have |·|_2 ≤ 1.0, so trajectory stays bounded
        let steps = [1, 3, 5];
        assert!(check_walk_bounded(2, &steps, 1.0));
    }
}