//! hybrid_zeckendorf_normalize.rs
//!
//! Safe Rust transpilation from verified C (CAB pipeline).
//! Source: HeytingLean.Bridge.Veselov.HybridZeckendorf.Normalization
//!
//! Two-stage normalization:
//!   Stage 1 (intra-level): bounded rewrite iterations reducing
//!           duplicates and consecutives via Fibonacci identities
//!   Stage 2 (inter-level): Euclidean carry propagation across levels
//!
//! Provenance: Lean 4 → LambdaIR → MiniC → C → Rust
//! Correctness inherited from verified C source.

use crate::hybrid_zeckendorf_eval::{zeckendorf, HybridNumber, Payload, MAX_LEVELS};
use crate::hybrid_zeckendorf_fib::lazy_eval_fib;
use crate::hybrid_zeckendorf_weight::weight;

/// One intra-level normalization step: prefer duplicate rewrite,
/// then consecutive rewrite, otherwise no-op.
///
/// (Lean: `intraStep`)
///
/// Rewrites:
/// - `[0, 0, ...rest]` → `rest` (`fib(0)+fib(0) = 0`)
/// - `[1, 1, ...rest]` → `[3, ...rest]` (`fib(1)+fib(1) = fib(3)`)
/// - `[k+2, k+2, ...rest]` → `[k+3, k, ...rest]` (`2*fib(k+2) = fib(k+3)+fib(k)`)
/// - `[a, a+1, ...rest]` → `[a+2, ...rest]` (`fib(a)+fib(a+1) = fib(a+2)`)
///
/// Theorem preserved: `intraStep_preserves_eval`
pub fn intra_step(z: &mut Vec<u32>) {
    if z.len() < 2 {
        return;
    }

    let a = z[0];
    let b = z[1];

    if a == b {
        match a {
            0 => {
                // [0, 0, ...rest] → rest
                z.drain(0..2);
            }
            1 => {
                // [1, 1, ...rest] → [3, ...rest]
                z[0] = 3;
                z.remove(1);
            }
            k => {
                // [k, k, ...rest] → [k+1, k-2, ...rest]  (k >= 2)
                z[0] = k + 1;
                z[1] = k - 2;
            }
        }
    } else if b == a + 1 {
        // [a, a+1, ...rest] → [a+2, ...rest]
        z[0] = a + 2;
        z.remove(1);
    }
}

/// Bounded intra-level iteration.
///
/// (Lean: `intraIter n z` = iterate `intraStep` `n` times)
///
/// Theorem preserved: `intraIter_preserves_eval`
pub fn intra_iter(z: &mut Vec<u32>, n: usize) {
    for _ in 0..n {
        intra_step(z);
    }
}

/// Intra-level normalization: bounded rewrite pass followed by
/// canonical Zeckendorf re-encoding.
///
/// (Lean: `intraNormalize z = Nat.zeckendorf (lazyEvalFib (intraCore z))`)
///
/// Theorem preserved: `intraNormalize_sound` — `levelEval(result) = lazyEvalFib(z)`
/// Theorem preserved: `intraNormalize_canonical` — result is Zeckendorf-canonical
pub fn intra_normalize(z: &[u32]) -> Vec<u32> {
    let mut tmp = z.to_vec();
    let bound = 2 * tmp.len() + 1;
    intra_iter(&mut tmp, bound);
    let val = lazy_eval_fib(&tmp);
    zeckendorf(val)
}

/// One structural carry step at level `i`.
///
/// Divides level-i value by `weight(i)`, carries quotient to level `i+1`.
///
/// (Lean: `carryAt`)
///
/// Theorem preserved: `carryAt_preserves_eval`
/// Theorem preserved: `carryAt_preserves_canonical`
fn carry_at(i: usize, x: &mut HybridNumber) {
    if i == 0 || i >= MAX_LEVELS - 1 {
        return;
    }

    let ci = lazy_eval_fib(&x.levels[i].indices);
    let wi = weight(i as u32);
    if wi == 0 {
        return;
    }

    let q = ci / wi;
    let r = ci % wi;

    // Re-encode remainder at level i
    x.levels[i] = Payload::from_indices(zeckendorf(r));

    // Add quotient to level i+1
    if q > 0 && i + 1 < MAX_LEVELS {
        let cnext = lazy_eval_fib(&x.levels[i + 1].indices);
        x.levels[i + 1] = Payload::from_indices(zeckendorf(cnext + q));
    }
}

/// Bottom-up carry pass across all levels.
///
/// (Lean: `interCarryLoop` / `interCarry`)
///
/// Theorem preserved: `interCarryLoop_preserves_eval`
/// Theorem preserved: `interCarryLoop_preserves_canonical`
fn inter_carry(x: &mut HybridNumber) {
    for i in 1..MAX_LEVELS {
        carry_at(i, x);
    }
}

/// Full lazy-to-canonical normalization.
///
/// Stage 1: intra-normalize every level.
/// Stage 2: inter-level carry propagation.
///
/// (Lean: `normalize X = interCarry (normalizeIntra X)`)
///
/// Theorem preserved: `normalize_sound` — `eval(normalize X) = lazyEval X`
/// Theorem preserved: `normalize_canonical` — `IsCanonical(normalize X)`
pub fn normalize(lazy_in: &HybridNumber) -> HybridNumber {
    // Stage 1: intra-normalize each level
    let mut out = HybridNumber::zero();
    for i in 0..MAX_LEVELS {
        if !lazy_in.levels[i].is_empty() {
            out.levels[i] =
                Payload::from_indices(intra_normalize(&lazy_in.levels[i].indices));
        }
    }

    // Stage 2: inter-level carry
    inter_carry(&mut out);
    out
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::hybrid_zeckendorf_eval::{eval, from_nat};
    use crate::hybrid_zeckendorf_fib::lazy_eval_fib;

    #[test]
    fn test_intra_step_preserves_eval() {
        let z = vec![3u32, 3, 5];
        let original = lazy_eval_fib(&z);
        let mut z2 = z.clone();
        intra_step(&mut z2);
        assert_eq!(lazy_eval_fib(&z2), original);
    }

    #[test]
    fn test_normalize_preserves_eval() {
        let x = from_nat(12345);
        let normalized = normalize(&x);
        assert_eq!(eval(&normalized), eval(&x));
    }
}