hakorune/src/mir/join_ir/verify.rs

//! JoinIR Progress Carrier Verification (Phase 29 L-5.2)
//!
//! # Purpose
//!
//! ループの「進捗キャリア」が backedge で必ず更新されていることを検証する。
//! ゼロ進捗 backedge（progress carrier が変化しない再帰呼び出し）を検出し、
//! 無限ループの可能性を早期に警告する。
//!
//! # Phase 29 Strategy
//!
//! - まずは minimal skip_ws JoinIR のみを対象に、dev モードで警告を出す。
//! - 将来（Phase 30）では Verifier エラーに格上げする予定。
//!
//! # Usage
//!
//! ```ignore
//! // NYASH_JOINIR_EXPERIMENT=1 のときのみ有効
//! if let Err(e) = verify_progress_for_skip_ws(&join_module) {
//!     eprintln!("[joinir/progress] warning: {:?}", e);
//! }
//! ```

use crate::mir::join_ir::{BinOpKind, JoinFuncId, JoinInst, JoinModule, MirLikeInst};
use crate::mir::ValueId;

/// Progress verification error
#[derive(Debug, Clone)]
pub enum ProgressError {
    /// Progress carrier is not updated before backedge (recursive call)
    ZeroProgressBackedge {
        /// Progress variable name (for diagnostics)
        progress_var: String,
        /// Loop function ID
        loop_func_id: JoinFuncId,
        /// The recursive call that doesn't update progress
        call_index: usize,
    },
    /// No recursive call found in loop function
    NoRecursiveCall {
        loop_func_id: JoinFuncId,
    },
    /// Progress carrier not found
    ProgressCarrierNotFound {
        expected_param_index: usize,
        loop_func_id: JoinFuncId,
    },
}

/// Verify progress carrier for skip_ws JoinIR (Phase 29 minimal version)
///
/// This function checks that:
/// 1. The loop_step function has a recursive call
/// 2. The progress carrier (i, typically the 3rd parameter) is updated via BinOp::Add
///    before the recursive call
///
/// # Arguments
///
/// * `join_module` - The JoinModule containing skip_ws functions
///
/// # Returns
///
/// Ok(()) if progress carrier is properly updated, Err(ProgressError) otherwise.
///
/// # Skip_ws Structure Expected
///
/// ```text
/// fn loop_step(s: Str, n: Int, i: Int) -> Int {
///     if i >= n { return i }
///     let ch = s.substring(i, i+1)
///     if ch != " " { return i }
///     let next_i = i + 1     // ← progress update
///     loop_step(s, n, next_i) // ← recursive call with updated progress
/// }
/// ```
pub fn verify_progress_for_skip_ws(join_module: &JoinModule) -> Result<(), ProgressError> {
    // skip_ws では loop_step が JoinFuncId(1)
    let loop_func_id = JoinFuncId::new(1);

    let loop_func = match join_module.functions.get(&loop_func_id) {
        Some(f) => f,
        None => {
            // loop_step 関数が無ければ検証スキップ（エラーではない）
            return Ok(());
        }
    };

    // skip_ws の progress carrier は 3番目のパラメータ (i)
    // params = [s, n, i] → index 2
    let progress_param_index = 2;
    let progress_param = match loop_func.params.get(progress_param_index) {
        Some(&p) => p,
        None => {
            return Err(ProgressError::ProgressCarrierNotFound {
                expected_param_index: progress_param_index,
                loop_func_id,
            });
        }
    };

    // 1. 再帰呼び出し（loop_step への Call）を探す
    let mut recursive_call_indices: Vec<usize> = Vec::new();
    for (idx, inst) in loop_func.body.iter().enumerate() {
        if let JoinInst::Call { func, .. } = inst {
            if *func == loop_func_id {
                recursive_call_indices.push(idx);
            }
        }
    }

    if recursive_call_indices.is_empty() {
        return Err(ProgressError::NoRecursiveCall { loop_func_id });
    }

    // 2. 再帰呼び出しの前に progress carrier が更新されているか確認
    //    「BinOp::Add で progress_param を使った演算がある」ことを保守的にチェック
    for &call_idx in &recursive_call_indices {
        let has_progress_update =
            check_progress_update_before(&loop_func.body[..call_idx], progress_param);

        if !has_progress_update {
            return Err(ProgressError::ZeroProgressBackedge {
                progress_var: format!("param[{}]", progress_param_index),
                loop_func_id,
                call_index: call_idx,
            });
        }
    }

    Ok(())
}

/// Check if there's a BinOp::Add that uses the progress parameter before the call
///
/// This is a conservative check: we look for any BinOp::Add where progress_param
/// is the LHS. The result should be used as an argument to the recursive call.
fn check_progress_update_before(instructions: &[JoinInst], progress_param: ValueId) -> bool {
    for inst in instructions {
        if let JoinInst::Compute(MirLikeInst::BinOp {
            op: BinOpKind::Add,
            lhs,
            ..
        }) = inst
        {
            if *lhs == progress_param {
                return true;
            }
        }
    }
    false
}

/// Verify progress carrier for a generic loop (future extension)
///
/// This is a placeholder for Phase 30 where we'll support arbitrary loops.
#[allow(dead_code)]
pub fn verify_progress_generic(
    _join_module: &JoinModule,
    _loop_func_id: JoinFuncId,
    _progress_param_index: usize,
) -> Result<(), ProgressError> {
    // Phase 30: 汎用ループの progress チェック
    // 現在は未実装（skip_ws 専用版のみ）
    Ok(())
}

// ============================================================================
// Unit Tests
// ============================================================================

#[cfg(test)]
mod tests {
    use super::*;
    use crate::mir::join_ir::{ConstValue, JoinFunction, JoinModule};

    fn build_valid_skip_ws_loop() -> JoinModule {
        let mut module = JoinModule::new();

        // loop_step(s, n, i) with proper progress update
        let loop_func_id = JoinFuncId::new(1);
        let s_param = ValueId(4000);
        let n_param = ValueId(4001);
        let i_param = ValueId(4002);
        let const_1 = ValueId(4010);
        let next_i = ValueId(4011);

        let mut loop_func = JoinFunction::new(
            loop_func_id,
            "loop_step".to_string(),
            vec![s_param, n_param, i_param],
        );

        // const 1
        loop_func.body.push(JoinInst::Compute(MirLikeInst::Const {
            dst: const_1,
            value: ConstValue::Integer(1),
        }));

        // next_i = i + 1 (progress update)
        loop_func.body.push(JoinInst::Compute(MirLikeInst::BinOp {
            dst: next_i,
            op: BinOpKind::Add,
            lhs: i_param, // progress carrier as LHS
            rhs: const_1,
        }));

        // recursive call: loop_step(s, n, next_i)
        loop_func.body.push(JoinInst::Call {
            func: loop_func_id,
            args: vec![s_param, n_param, next_i],
            k_next: None,
            dst: None,
        });

        module.add_function(loop_func);
        module
    }

    fn build_invalid_skip_ws_loop() -> JoinModule {
        let mut module = JoinModule::new();

        // loop_step(s, n, i) WITHOUT progress update
        let loop_func_id = JoinFuncId::new(1);
        let s_param = ValueId(4000);
        let n_param = ValueId(4001);
        let i_param = ValueId(4002);

        let mut loop_func = JoinFunction::new(
            loop_func_id,
            "loop_step".to_string(),
            vec![s_param, n_param, i_param],
        );

        // recursive call with SAME i (no progress!)
        loop_func.body.push(JoinInst::Call {
            func: loop_func_id,
            args: vec![s_param, n_param, i_param], // i is not updated!
            k_next: None,
            dst: None,
        });

        module.add_function(loop_func);
        module
    }

    #[test]
    fn test_valid_progress_passes() {
        let module = build_valid_skip_ws_loop();
        let result = verify_progress_for_skip_ws(&module);
        assert!(result.is_ok(), "Valid progress should pass: {:?}", result);
    }

    #[test]
    fn test_zero_progress_detected() {
        let module = build_invalid_skip_ws_loop();
        let result = verify_progress_for_skip_ws(&module);
        assert!(result.is_err(), "Zero progress should be detected");
        match result {
            Err(ProgressError::ZeroProgressBackedge { .. }) => {
                // Expected
            }
            other => panic!("Expected ZeroProgressBackedge, got {:?}", other),
        }
    }

    #[test]
    fn test_empty_module_ok() {
        let module = JoinModule::new();
        let result = verify_progress_for_skip_ws(&module);
        assert!(
            result.is_ok(),
            "Empty module should pass (no loop_step to verify)"
        );
    }
}