vyre-conform 0.1.0

//! Pipeline implementation for the contribution feedback loop.

use std::path::Path;
use std::time::Instant;

use crate::enforce::admission::check_admission;
use crate::enforce::category::{
    check_category_a_zero_overhead, check_category_b_tripwire, check_category_c_intrinsic,
};
use crate::enforce::enforcers::signature_match::enforce_signature;
use crate::meta::contribute::{
    ContributeFilter, ContributeReport, ContributeResult, Finding, StageStatus,
};
use crate::op_registry;
use crate::proof::algebra::checker::verify_laws;
use crate::proof::algebra::inference::{find_missing_laws, infer_binary_laws, infer_unary_laws};
use crate::spec::registry::verify::verify_specs;
use crate::spec::types::{ConstructionTime, DataType, OpSpec, ProofToken};

/// Run the full contribution pipeline against the requested operation(s).
#[inline]
pub fn run_contribute(filter: ContributeFilter, vyre_src_root: &Path) -> Vec<ContributeReport> {
    let start = Instant::now();
    let all_specs = op_registry::all_specs();

    let specs: Vec<OpSpec> = match filter {
        ContributeFilter::All => all_specs,
        ContributeFilter::Op(id) => all_specs.into_iter().filter(|s| s.id == id).collect(),
    };

    if specs.is_empty() {
        let target = match filter {
            ContributeFilter::Op(id) => id,
            ContributeFilter::All => "all",
        };
        return vec![ContributeReport {
            op_id: target.to_string(),
            total_duration_ms: start.elapsed().as_millis() as u64,
            stages: vec![ContributeResult {
                stage_name: "registry".to_string(),
                duration_ms: start.elapsed().as_millis() as u64,
                status: StageStatus::Fail,
                findings: vec![Finding {
                    message: format!("Fix: operation '{target}' not found in registry."),
                }],
            }],
            overall_status: StageStatus::Fail,
        }];
    }

    specs
        .into_iter()
        .map(|spec| run_pipeline_for_op(&spec, vyre_src_root))
        .collect()
}

fn run_pipeline_for_op(op: &OpSpec, vyre_src_root: &Path) -> ContributeReport {
    let total_start = Instant::now();
    let mut stages = Vec::with_capacity(8);
    let mut overall = StageStatus::Pass;

    // Stage 1: registry
    let (status, findings, dur) = timed(|| match verify_specs(std::slice::from_ref(op)) {
        Ok(()) => (StageStatus::Pass, vec![]),
        Err(errors) => {
            let findings: Vec<Finding> = errors
                .into_iter()
                .map(|e| Finding {
                    message: e.to_string(),
                })
                .collect();
            (StageStatus::Fail, findings)
        }
    });
    overall = max_status(overall, status);
    stages.push(result("registry", dur, status, findings));
    if status == StageStatus::Fail {
        return fail_fast_report(op, total_start, stages, "registry");
    }

    // Stage 2: signature enforcer
    let (status, findings, dur) = timed(|| match enforce_signature(op) {
        Ok(()) => (StageStatus::Pass, vec![]),
        Err(msg) => (StageStatus::Fail, vec![Finding { message: msg }]),
    });
    overall = max_status(overall, status);
    stages.push(result("signature", dur, status, findings));

    if status == StageStatus::Fail {
        return fail_fast_report(op, total_start, stages, "signature");
    }

    // Stage 3: category gate (A + B + C overhead)
    let (status, findings, dur) = timed(|| {
        let mut cat_findings = check_category_a_zero_overhead(std::slice::from_ref(op));
        cat_findings.extend(check_category_c_intrinsic(std::slice::from_ref(op)));
        cat_findings.extend(check_category_b_tripwire(vyre_src_root));

        let mapped: Vec<Finding> = cat_findings
            .into_iter()
            .filter(|f| f.op_id() == op.id || f.op_id() == "CategoryB")
            .map(|f| Finding {
                message: f.to_string(),
            })
            .collect();

        if mapped.is_empty() {
            (StageStatus::Pass, vec![])
        } else {
            (StageStatus::Fail, mapped)
        }
    });
    overall = max_status(overall, status);
    stages.push(result("category", dur, status, findings));

    if status == StageStatus::Fail {
        return fail_fast_report(op, total_start, stages, "category");
    }

    // Stage 4: admission gates 4-8 (category overhead removed; lives in stage 3)
    let (status, findings, dur) = timed(|| {
        let admissions = check_admission(std::slice::from_ref(op), vyre_src_root);
        let mapped: Vec<Finding> = admissions
            .into_iter()
            .filter(|f| f.op_id() == op.id || f.op_id() == "CategoryB")
            .map(|f| Finding {
                message: f.to_string(),
            })
            .collect();
        if mapped.is_empty() {
            (StageStatus::Pass, vec![])
        } else {
            (StageStatus::Fail, mapped)
        }
    });
    overall = max_status(overall, status);
    stages.push(result("admission", dur, status, findings));
    if status == StageStatus::Fail {
        return fail_fast_report(op, total_start, stages, "admission");
    }

    // Stage 5: mandatory inference
    let (status, findings, dur) = timed(|| run_inference(op));
    overall = max_status(overall, status);
    stages.push(result("inference", dur, status, findings));

    // Stage 6: exhaustive u8 law check
    let (status, findings, dur) = timed(|| run_exhaustive_laws(op));
    overall = max_status(overall, status);
    stages.push(result("laws", dur, status, findings));

    // Stage 7: composition proof check
    let (status, findings, dur) = timed(|| run_composition_check(op));
    overall = max_status(overall, status);
    stages.push(result("composition", dur, status, findings));

    // Stage 8: summary
    let pass_count = stages
        .iter()
        .filter(|s| s.status == StageStatus::Pass)
        .count();
    let fail_count = stages
        .iter()
        .filter(|s| s.status == StageStatus::Fail)
        .count();
    let skip_count = stages
        .iter()
        .filter(|s| s.status == StageStatus::Skip)
        .count();
    stages.push(result(
        "summary",
        0,
        overall,
        vec![Finding {
            message: format!(
                "Pipeline complete for {}: {pass_count} passed, {fail_count} failed, {skip_count} skipped. Overall: {overall:?}.",
                op.id
            ),
        }],
    ));

    ContributeReport {
        op_id: op.id.to_string(),
        total_duration_ms: total_start.elapsed().as_millis() as u64,
        stages,
        overall_status: overall,
    }
}

fn fail_fast_report(
    op: &OpSpec,
    total_start: Instant,
    mut stages: Vec<ContributeResult>,
    failed_stage: &str,
) -> ContributeReport {
    stages.push(result(
        "summary",
        0,
        StageStatus::Fail,
        vec![Finding {
            message: format!(
                "Fix: {failed_stage} stage failed for {}. Skipping remaining stages.",
                op.id
            ),
        }],
    ));
    ContributeReport {
        op_id: op.id.to_string(),
        total_duration_ms: total_start.elapsed().as_millis() as u64,
        stages,
        overall_status: StageStatus::Fail,
    }
}

fn timed<F>(f: F) -> (StageStatus, Vec<Finding>, u64)
where
    F: FnOnce() -> (StageStatus, Vec<Finding>),
{
    let start = Instant::now();
    let (status, findings) = f();
    let dur = start.elapsed().as_millis() as u64;
    (status, findings, dur)
}

fn result(name: &str, dur: u64, status: StageStatus, findings: Vec<Finding>) -> ContributeResult {
    ContributeResult {
        stage_name: name.to_string(),
        duration_ms: dur,
        status,
        findings,
    }
}

fn max_status(a: StageStatus, b: StageStatus) -> StageStatus {
    match (a, b) {
        (StageStatus::Fail, _) | (_, StageStatus::Fail) => StageStatus::Fail,
        (StageStatus::Skip, _) | (_, StageStatus::Skip) => StageStatus::Skip,
        _ => StageStatus::Pass,
    }
}

fn run_inference(op: &OpSpec) -> (StageStatus, Vec<Finding>) {
    let is_binary = op.signature.inputs.len() == 2
        && op.signature.inputs.iter().all(|t| *t == DataType::U32)
        && op.signature.output == DataType::U32;

    let is_unary = op.signature.inputs.len() == 1
        && op.signature.inputs[0] == DataType::U32
        && op.signature.output == DataType::U32;

    if !is_binary && !is_unary {
        return (
            StageStatus::Skip,
            vec![Finding {
                message: format!(
                    "Inference only supports unary/binary u32 ops. {} has signature {:?} -> {:?}.",
                    op.id, op.signature.inputs, op.signature.output
                ),
            }],
        );
    }

    let report = if is_binary {
        infer_binary_laws(op.id, op.cpu_fn)
    } else {
        infer_unary_laws(op.id, op.cpu_fn)
    };

    let missing = find_missing_laws(&op.laws, &report);
    if missing.is_empty() {
        (
            StageStatus::Pass,
            vec![Finding {
                message: format!("{}: all inferred laws are already declared.", op.id),
            }],
        )
    } else {
        let names: Vec<String> = missing.iter().map(|m| m.name.to_string()).collect();
        let recs: Vec<String> = missing
            .iter()
            .map(|m| format!("  {}", m.recommendation))
            .collect();
        (
            StageStatus::Fail,
            vec![Finding {
                message: format!(
                    "{}: missing inferred laws [{}]. Recommended declarations:\n{}",
                    op.id,
                    names.join(", "),
                    recs.join("\n")
                ),
            }],
        )
    }
}

fn run_exhaustive_laws(op: &OpSpec) -> (StageStatus, Vec<Finding>) {
    if op.laws.is_empty() {
        return (
            StageStatus::Skip,
            vec![Finding {
                message: format!("{}: no laws declared to verify.", op.id),
            }],
        );
    }

    let is_binary = op.signature.inputs.len() >= 2;
    let law_results = verify_laws(op.id, op.cpu_fn, &op.laws, is_binary);
    let failures: Vec<_> = law_results.into_iter().filter(|r| !r.passed()).collect();

    if failures.is_empty() {
        (
            StageStatus::Pass,
            vec![Finding {
                message: format!(
                    "{}: all {} declared laws hold under exhaustive u8 verification.",
                    op.id,
                    op.laws.len()
                ),
            }],
        )
    } else {
        let findings: Vec<Finding> = failures
            .into_iter()
            .map(|f| {
                let msg = if let Some(v) = f.violation {
                    format!("Law '{}' violated: {}", v.law, v.message)
                } else {
                    format!("Law '{}' failed with unknown violation.", f.law_name)
                };
                Finding { message: msg }
            })
            .collect();
        (StageStatus::Fail, findings)
    }
}

fn run_composition_check(op: &OpSpec) -> (StageStatus, Vec<Finding>) {
    let can_self_compose = op
        .signature
        .inputs
        .first()
        .is_some_and(|input| *input == op.signature.output);

    if !can_self_compose {
        return (
            StageStatus::Skip,
            vec![Finding {
                message: format!(
                    "{}: output type does not match input type — self-composition not applicable.",
                    op.id
                ),
            }],
        );
    }

    let token = match ProofToken::from_specs(&[op.clone(), op.clone()], ConstructionTime::Manual) {
        Ok(t) => t,
        Err(err) => {
            return (
                StageStatus::Fail,
                vec![Finding {
                    message: format!("{}: proof-token verification failed: {}", op.id, err),
                }],
            );
        }
    };

    if token.theorem_chain.is_empty() {
        return (
            StageStatus::Fail,
            vec![Finding {
                message: format!(
                    "{}: self-composition produces no applicable theorems but the op is type-compatible with self-composition. Fix: declare commutative/associative/identity laws or explain why self-composition is not structurally valid.",
                    op.id
                ),
            }],
        );
    }

    if let Err(msg) = self_composition_witness_diff(op) {
        return (StageStatus::Fail, vec![Finding { message: msg }]);
    }

    (
        StageStatus::Pass,
        vec![Finding {
            message: format!(
                "{}: applicable composition theorems: [{}]",
                op.id,
                token.theorem_chain.join(", ")
            ),
        }],
    )
}

fn self_composition_witness_diff(op: &OpSpec) -> Result<(), String> {
    let inner_input_len = op.signature.min_input_bytes();
    let extra_input_len = op
        .signature
        .inputs
        .iter()
        .skip(1)
        .map(|t| t.min_bytes())
        .sum::<usize>();
    let total_input_len = inner_input_len + extra_input_len;

    if total_input_len == 0 {
        return Err(format!(
            "{}: cannot self-compose variable-length op without expected bytes.",
            op.id
        ));
    }

    let expected_output_len = if op.signature.output.min_bytes() > 0 {
        op.signature.output.min_bytes()
    } else {
        op.expected_output_bytes.unwrap_or(0)
    };

    let test_inputs: Vec<Vec<u8>> = vec![
        vec![0u8; total_input_len],
        (0..total_input_len).map(|i| i as u8).collect(),
        (0..total_input_len)
            .map(|i| (i as u8).wrapping_mul(17).wrapping_add(42))
            .collect(),
    ];

    for input in &test_inputs {
        let inner_out = (op.cpu_fn)(&input[..inner_input_len.min(input.len())]);
        let mut outer_in = inner_out;
        outer_in.extend_from_slice(&input[inner_input_len..]);
        let composed_out = (op.cpu_fn)(&outer_in);

        if expected_output_len > 0 && composed_out.len() != expected_output_len {
            return Err(format!(
                "{}: self-composition witness diff failed: expected output length {} but got {}.",
                op.id,
                expected_output_len,
                composed_out.len()
            ));
        }
    }

    Ok(())
}