use bpfanalysis::verifier_log::{
    arg_number_from_verifier_error, helper_name_from_verifier_error, latest_reg_state_before,
    latest_register_with_type_before, map_value_access_error, parse_i64_after,
    register_from_verifier_error, scalar_range_summary, verifier_value_summary,
};
use bpfanalysis::VerifierInsn;

use crate::family::ProofObligation;

#[derive(Clone, Debug, PartialEq, Eq)]
pub struct RequiredProof {
    pub obligation: ProofObligation,
    pub register: Option<u8>,
    pub description: String,
    pub rejection_detail: String,
}

pub(crate) fn instantiate_required_proof(
    terminal_error: &str,
    terminal_call_target: Option<&str>,
    terminal_pc: Option<usize>,
    states: &[VerifierInsn],
    obligation: ProofObligation,
) -> RequiredProof {
    let register = register_from_verifier_error(terminal_error);
    match obligation {
        ProofObligation::PacketBounds => packet_bounds_required_proof(terminal_error, register),
        ProofObligation::ScalarRange => {
            scalar_range_required_proof(terminal_error, terminal_pc, states, register)
        }
        ProofObligation::NullablePointer => nullable_required_proof(terminal_error, register),
        ProofObligation::StackInitialized => stack_required_proof(terminal_error, register),
        ProofObligation::ReferenceLifecycle => reference_required_proof(terminal_error, register),
        ProofObligation::DynptrSafety => {
            dynptr_required_proof(terminal_error, terminal_call_target, register)
        }
        ProofObligation::EnvironmentCapability => environment_required_proof(terminal_error),
        _ => RequiredProof {
            obligation,
            register,
            description: obligation.default_required_proof().to_string(),
            rejection_detail: obligation.rejected_detail().to_string(),
        },
    }
}

fn dynptr_required_proof(
    message: &str,
    call_target: Option<&str>,
    register: Option<u8>,
) -> RequiredProof {
    let lower = message.to_ascii_lowercase();
    let arg = arg_number_from_verifier_error(message);
    let arg_label = arg.map(|arg| format!("arg #{arg}"));
    let helper_label = call_target
        .filter(|target| target.contains("dynptr"))
        .unwrap_or("this dynptr helper");

    let (description, rejection_detail) = if lower.contains("unacquired reference") {
        match arg_label {
            Some(arg) => (
                format!(
                    "release or discard dynptr-backed references only while they are acquired, exactly once; {arg} is not acquired at {helper_label}"
                ),
                format!(
                    "rejected here: {arg} is an unacquired dynptr-backed reference at this helper call"
                ),
            ),
            None => (
                format!(
                    "release or discard dynptr-backed references only while they are acquired, exactly once before calling {helper_label}"
                ),
                "rejected here: dynptr-backed reference is not acquired at this helper call".to_string(),
            ),
        }
    } else if lower.contains("expected an initialized dynptr") {
        match arg_label {
            Some(arg) => (
                format!(
                    "pass the exact initialized dynptr stack slot as {arg}; avoid interior pointers such as &ptr + offset or overwritten dynptr storage"
                ),
                format!(
                    "rejected here: {arg} is not the exact initialized dynptr stack slot expected by this helper"
                ),
            ),
            None => (
                "pass the exact initialized dynptr stack slot to the helper; avoid interior pointers such as &ptr + offset or overwritten dynptr storage".to_string(),
                "rejected here: helper argument is not the exact initialized dynptr stack slot".to_string(),
            ),
        }
    } else if lower.contains("dynptr has to be an uninitialized dynptr") {
        (
            "pass a clean dynptr stack slot at the exact declared address to the initializer helper; do not pass an interior or already-initialized dynptr slot".to_string(),
            "rejected here: dynptr initializer did not receive an uninitialized dynptr stack slot".to_string(),
        )
    } else if lower.contains("cannot pass in dynptr at an offset")
        || lower.contains("dynptr has to be at a constant offset")
        || lower.contains("expected pointer to stack or const struct bpf_dynptr")
    {
        match arg_label {
            Some(arg) => (
                format!(
                    "pass the exact dynptr stack slot address as {arg} at a verifier-visible constant offset, not an interior or variable pointer"
                ),
                format!(
                    "rejected here: {arg} points inside or variably around the dynptr stack slot"
                ),
            ),
            None => (
                "pass the exact dynptr stack slot address at a verifier-visible constant offset, not an interior or variable pointer".to_string(),
                "rejected here: helper argument points inside or variably around the dynptr stack slot".to_string(),
            ),
        }
    } else if lower.contains("cannot overwrite referenced dynptr") {
        (
            "do not overwrite or reinitialize a dynptr stack slot while verifier-tracked dynptr state is still live".to_string(),
            "rejected here: live referenced dynptr state would be overwritten".to_string(),
        )
    } else if lower.contains("expected a dynptr of type") {
        (
            "pass a dynptr with the helper-required backing type and read/write mode".to_string(),
            "rejected here: dynptr backing type or mode does not match this helper".to_string(),
        )
    } else if lower.contains("must be a known constant") {
        (
            "pass a verifier-known constant length to the dynptr slice helper, or split variable-length handling into verifier-visible constant-size cases".to_string(),
            "rejected here: dynptr slice length is not a verifier-known constant".to_string(),
        )
    } else if lower.contains("does not allow writes to packet data") {
        (
            "use a read-only dynptr slice helper in this program context, or move the write path to a hook where packet writes are allowed".to_string(),
            "rejected here: read-write dynptr access is not allowed for this packet context".to_string(),
        )
    } else if lower.contains("potential write to dynptr") {
        (
            "keep ordinary writes and helper outputs away from stack bytes that store live dynptr state".to_string(),
            "rejected here: write may clobber verifier-tracked dynptr storage".to_string(),
        )
    } else {
        (
            ProofObligation::DynptrSafety
                .default_required_proof()
                .to_string(),
            ProofObligation::DynptrSafety.rejected_detail().to_string(),
        )
    };

    RequiredProof {
        obligation: ProofObligation::DynptrSafety,
        register,
        description,
        rejection_detail,
    }
}

fn packet_bounds_required_proof(message: &str, register: Option<u8>) -> RequiredProof {
    let proven_range = parse_i64_after(message, "r=");
    let required_end = packet_required_range(message).map(i64::from);
    let description = match (register, required_end, proven_range) {
        (Some(reg), Some(required), Some(range)) => format!(
            "prove R{reg} has packet range at least {required} bytes before this access; verifier currently has range {range}"
        ),
        (Some(reg), Some(required), None) => {
            format!("prove R{reg} has packet range at least {required} bytes before this access")
        }
        _ => ProofObligation::PacketBounds
            .default_required_proof()
            .to_string(),
    };
    let rejection_detail = match (register, required_end, proven_range) {
        (Some(reg), Some(required), Some(range)) => format!(
            "rejected here: verifier needs R{reg} packet range >= {required}, but only {range} bytes are proven"
        ),
        (Some(reg), Some(required), None) => format!(
            "rejected here: verifier needs R{reg} packet range >= {required} before this access"
        ),
        _ => ProofObligation::PacketBounds.rejected_detail().to_string(),
    };
    RequiredProof {
        obligation: ProofObligation::PacketBounds,
        register,
        description,
        rejection_detail,
    }
}

pub(crate) fn packet_required_range(message: &str) -> Option<u32> {
    let off = parse_i64_after(message, "off=")?;
    let size = parse_i64_after(message, "size=")?;
    u32::try_from(off.checked_add(size)?).ok()
}

fn scalar_range_required_proof(
    message: &str,
    terminal_pc: Option<usize>,
    states: &[VerifierInsn],
    register: Option<u8>,
) -> RequiredProof {
    if let Some(proof) = map_value_access_required_proof(message, terminal_pc, states, register) {
        return proof;
    }

    let register =
        register.or_else(|| latest_register_with_type_before(states, terminal_pc, "scalar"));
    let state = register.and_then(|reg| latest_reg_state_before(states, terminal_pc, reg));
    let description = if message.contains("value -") {
        "prove the scalar used for pointer arithmetic cannot be negative on any path".to_string()
    } else {
        match (register, state) {
            (Some(reg), Some(state)) => format!(
                "prove R{reg} has a bounded non-negative scalar range before this pointer arithmetic or helper memory access; verifier sees {}",
                scalar_range_summary(state)
            ),
            (Some(reg), None) => {
                format!("prove R{reg} has a bounded non-negative scalar range before this pointer arithmetic or helper memory access")
            }
            _ => ProofObligation::ScalarRange
                .default_required_proof()
                .to_string(),
        }
    };
    let rejection_detail = match (register, state) {
        (Some(reg), Some(state)) => format!(
            "rejected here: verifier still sees R{reg} as {}",
            scalar_range_summary(state)
        ),
        (Some(reg), None) => {
            format!("rejected here: R{reg} is not proven to have a safe scalar range")
        }
        (None, _) => ProofObligation::ScalarRange.rejected_detail().to_string(),
    };
    RequiredProof {
        obligation: ProofObligation::ScalarRange,
        register,
        description,
        rejection_detail,
    }
}

fn map_value_access_required_proof(
    message: &str,
    terminal_pc: Option<usize>,
    states: &[VerifierInsn],
    register: Option<u8>,
) -> Option<RequiredProof> {
    if !message
        .to_ascii_lowercase()
        .contains("invalid access to map value")
    {
        return None;
    }

    let register =
        register.or_else(|| latest_register_with_type_before(states, terminal_pc, "map_value"));
    let state = register.and_then(|reg| latest_reg_state_before(states, terminal_pc, reg));
    let access = map_value_access_error(message);
    let value_size = access
        .map(|access| i64::from(access.value_size))
        .or_else(|| parse_i64_after(message, "value_size="))
        .or_else(|| state.and_then(|state| state.map_value_size.map(i64::from)));
    let access_off = access
        .map(|access| access.offset)
        .or_else(|| parse_i64_after(message, "off="));
    let access_size = access
        .map(|access| i64::from(access.size))
        .or_else(|| parse_i64_after(message, "size="));
    let access_end = access
        .and_then(|access| access.end())
        .or_else(|| access_off.and_then(|off| access_size.and_then(|size| off.checked_add(size))));
    let state_summary = state.map(verifier_value_summary);

    let description = match (register, value_size, access_off, access_size, state_summary) {
        (Some(reg), Some(value_size), Some(off), Some(size), Some(summary)) => format!(
            "prove R{reg}'s map-value byte range off={off} size={size} stays within value_size={value_size}; verifier sees {summary}"
        ),
        (Some(reg), Some(value_size), Some(off), Some(size), None) => format!(
            "prove R{reg}'s map-value byte range off={off} size={size} stays within value_size={value_size}"
        ),
        (Some(reg), Some(value_size), _, _, Some(summary)) => format!(
            "prove R{reg}'s computed map-value offset stays within value_size={value_size}; verifier sees {summary}"
        ),
        (Some(reg), Some(value_size), _, _, None) => format!(
            "prove R{reg}'s computed map-value offset stays within value_size={value_size}"
        ),
        _ => ProofObligation::ScalarRange
            .default_required_proof()
            .to_string(),
    };

    let rejection_detail = match (register, value_size, access_end, access_off, access_size) {
        (Some(reg), Some(value_size), Some(end), Some(off), Some(size)) => format!(
            "rejected here: R{reg} map-value access off={off} size={size} reaches byte {end}, past value_size={value_size}"
        ),
        (Some(reg), Some(value_size), _, _, _) => format!(
            "rejected here: R{reg} map-value offset is not proven within value_size={value_size}"
        ),
        _ => ProofObligation::ScalarRange.rejected_detail().to_string(),
    };

    Some(RequiredProof {
        obligation: ProofObligation::ScalarRange,
        register,
        description,
        rejection_detail,
    })
}

fn nullable_required_proof(message: &str, register: Option<u8>) -> RequiredProof {
    let description = match register {
        Some(reg) => {
            format!("prove R{reg} is non-null in the same verifier-visible branch before dereference, pointer arithmetic, or helper reuse")
        }
        None => ProofObligation::NullablePointer
            .default_required_proof()
            .to_string(),
    };
    let rejection_detail = match register {
        Some(reg) if message.contains("pointer arithmetic") => {
            format!("rejected here: R{reg} is still nullable, so pointer arithmetic is prohibited")
        }
        Some(reg) => format!("rejected here: R{reg} is still nullable at the use site"),
        None => ProofObligation::NullablePointer
            .rejected_detail()
            .to_string(),
    };
    RequiredProof {
        obligation: ProofObligation::NullablePointer,
        register,
        description,
        rejection_detail,
    }
}

fn stack_required_proof(message: &str, register: Option<u8>) -> RequiredProof {
    let description = match register {
        Some(reg) if message.contains("!read_ok") => {
            format!(
                "write a readable value to R{reg} on every path before this return or helper use"
            )
        }
        Some(reg) => {
            format!("initialize every stack byte reachable from R{reg} before it is read or passed to a helper")
        }
        None => ProofObligation::StackInitialized
            .default_required_proof()
            .to_string(),
    };
    let rejection_detail = match register {
        Some(reg) if message.contains("!read_ok") => {
            format!("rejected here: R{reg} is not readable on this path")
        }
        Some(reg) => {
            format!("rejected here: stack memory reachable from R{reg} is not fully initialized")
        }
        None => ProofObligation::StackInitialized
            .rejected_detail()
            .to_string(),
    };
    RequiredProof {
        obligation: ProofObligation::StackInitialized,
        register,
        description,
        rejection_detail,
    }
}

fn reference_required_proof(message: &str, register: Option<u8>) -> RequiredProof {
    let ref_id =
        parse_i64_after(message, "id=").or_else(|| parse_i64_after(message, "ref_obj_id="));
    let description = match ref_id {
        Some(id) => format!("release verifier-tracked reference id {id} on every path before exit"),
        None => ProofObligation::ReferenceLifecycle
            .default_required_proof()
            .to_string(),
    };
    let rejection_detail = match ref_id {
        Some(id) => format!("rejected here: reference id {id} is not released on every path"),
        None => ProofObligation::ReferenceLifecycle
            .rejected_detail()
            .to_string(),
    };
    RequiredProof {
        obligation: ProofObligation::ReferenceLifecycle,
        register,
        description,
        rejection_detail,
    }
}

fn environment_required_proof(message: &str) -> RequiredProof {
    let helper = helper_name_from_verifier_error(message);
    let description = match helper.as_deref() {
        Some(helper) => format!(
            "load this program with an attach type and kernel environment that allow {helper}, or avoid that helper on this path"
        ),
        None => ProofObligation::EnvironmentCapability
            .default_required_proof()
            .to_string(),
    };
    let rejection_detail = match helper {
        Some(helper) => format!("rejected here: this program type cannot use {helper}"),
        None => ProofObligation::EnvironmentCapability
            .rejected_detail()
            .to_string(),
    };
    RequiredProof {
        obligation: ProofObligation::EnvironmentCapability,
        register: register_from_verifier_error(message),
        description,
        rejection_detail,
    }
}
