rmpca 0.1.1

//! Lean 4 FFI Bridge
//!
//! This module provides the boundary between Rust and Lean 4 for verified optimization.
//!
//! THE PROBLEM:
//! Passing complex Rust data structures (petgraph, `HashMap`, `HashSet`) to Lean 4
//! via C FFI is notoriously difficult due to:
//! - Different memory layouts (Rust struct packing vs C ABI)
//! - Ownership semantics (Rust RAII vs manual C memory management)
//! - Iterators and complex types dont have C equivalents
//!
//! THE SOLUTION:
//! Flatten data structures before crossing the FFI boundary. We extract minimal
//! information needed for the Eulerian path problem and pass it as simple
//! C-compatible arrays (contiguous memory + length).
//!
//! Data flow:
//!   Rust Graph -> `FlatArrays` -> Lean 4 -> `VerifiedResult` -> Rust
//!
//! // Aligns with Lean4: FFI boundary specification
//!
//! SAFETY DESIGN:
//! `FlatGraph` and `VerifiedResult` use raw pointers for C ABI compatibility.
//! They are NOT Send/Sync because raw pointers with unknown ownership
//! cannot be safely shared across threads. All FFI operations are confined
//! to a single thread. If parallel verification is needed, the graph
//! should be cloned per thread (immutable snapshot pattern).

use crate::optimizer::error::RouteError;
use std::os::raw::{c_double, c_int, c_uint};

/// Flattened graph representation for FFI.
///
/// This structure contains only primitive C-compatible types
/// that can be safely passed to Lean 4 via C FFI.
///
/// # Ownership
/// The `nodes` and `edges` pointers are owned by this struct when constructed
/// via `FlatGraph::from_vecs`. The `Drop` implementation frees them.
///
/// # Thread Safety
/// This type deliberately does NOT implement Send or Sync. Raw pointers
/// with ownership semantics cannot be safely shared across threads.
/// If you need to pass a `FlatGraph` to another thread, serialize it first
/// or clone the source data on the target thread.
#[allow(dead_code)]
#[repr(C)]
pub struct FlatGraph {
    /// Contiguous array of node coordinates: [lat1, lon1, lat2, lon2, ...]
    pub nodes: *mut c_double,

    /// Number of nodes (array length / 2)
    pub node_count: c_uint,

    /// Contiguous array of edges: [`from_idx`, `to_idx`, `from_idx`, `to_idx`, ...]
    pub edges: *mut c_uint,

    /// Number of edges (array length / 2)
    pub edge_count: c_uint,

    /// Starting node index for circuit
    pub start_node: c_uint,
}

// DELIBERATELY NOT implementing Send/Sync for FlatGraph.
// Raw pointers with ownership semantics are not thread-safe.
// If cross-thread transfer is needed, serialize the data instead.

impl FlatGraph {
    /// Create a `FlatGraph` from Rust Vecs, taking ownership of the data.
    ///
    /// This is the safe constructor. The resulting `FlatGraph` owns its
    /// pointers and will free them on drop.
    ///
    /// # Panics
    /// Panics if the number of node coordinates is odd or if the number of
    /// edge indices is odd, since they cannot be evenly divided into pairs.
    #[allow(dead_code)]
    #[must_use]
    pub fn from_vecs(node_coords: Vec<c_double>, edge_indices: Vec<c_uint>, start_node: c_uint) -> Self {
        let node_count: c_uint = (node_coords.len() / 2).try_into().unwrap();
        let edge_count: c_uint = (edge_indices.len() / 2).try_into().unwrap();

        let nodes_ptr = Box::into_raw(node_coords.into_boxed_slice()).cast::<c_double>();
        let edges_ptr = Box::into_raw(edge_indices.into_boxed_slice()).cast::<c_uint>();

        FlatGraph {
            nodes: nodes_ptr,
            node_count,
            edges: edges_ptr,
            edge_count,
            start_node,
        }
    }

    /// Create a null/empty `FlatGraph`.
    #[allow(dead_code)]
    #[must_use]
    pub fn empty() -> Self {
        Self::from_vecs(Vec::new(), Vec::new(), 0)
    }
}

impl Drop for FlatGraph {
    fn drop(&mut self) {
        // SAFETY: The pointers were created by Box::into_raw in from_vecs()
        // (or from_vecs was not used, in which case the pointers are null and
        // Vec::from_raw_parts is not called — we check for null first).
        // The capacity equals len because into_boxed_slice() produces a
        // slice with capacity == len.
        // This Drop runs exactly once, so no double-free.
        unsafe {
            if !self.nodes.is_null() && self.node_count > 0 {
                let len = (self.node_count * 2) as usize;
                let cap = len;
                let _ = Vec::from_raw_parts(
                    self.nodes.cast::<c_double>(),
                    len,
                    cap,
                );
            }
            if !self.edges.is_null() && self.edge_count > 0 {
                let len = (self.edge_count * 2) as usize;
                let cap = len;
                let _ = Vec::from_raw_parts(
                    self.edges.cast::<c_uint>(),
                    len,
                    cap,
                );
            }
        }
    }
}

/// Verified result from Lean 4.
///
/// # Ownership
/// When `success == 1`, the `circuit` pointer is owned by this struct
/// and will be freed on drop. When `success == 0`, circuit is null.
///
/// # Thread Safety
/// This type deliberately does NOT implement Send or Sync.
/// See `FlatGraph` safety rationale above.
#[allow(dead_code)]
#[repr(C)]
pub struct VerifiedResult {
    /// Ordered node indices forming the circuit
    pub circuit: *mut c_uint,

    /// Length of circuit array
    pub circuit_length: c_uint,

    /// Total distance in meters
    pub total_distance: c_double,

    /// Success flag (0 = error, 1 = success)
    pub success: c_int,
}

// DELIBERATELY NOT implementing Send/Sync for VerifiedResult.
// Same rationale as FlatGraph: raw pointers with ownership semantics.

impl Drop for VerifiedResult {
    fn drop(&mut self) {
        // SAFETY: circuit pointer was allocated by the Lean 4 runtime
        // using the same allocator (std::alloc via libc malloc).
        // We only free if success == 1 and the pointer is non-null.
        // The Lean 4 runtime guarantees the pointer is valid when success == 1.
        unsafe {
            if self.success == 1 && !self.circuit.is_null() && self.circuit_length > 0 {
                let len = self.circuit_length as usize;
                let cap = len;
                let _ = Vec::from_raw_parts(
                    self.circuit.cast::<c_uint>(),
                    len,
                    cap,
                );
            }
        }
    }
}

/// Lean 4 optimizer bridge.
///
/// This struct manages the Lean 4 runtime when compiled with the lean4 feature.
/// It is NOT Send/Sync because FFI interactions with the Lean 4 runtime
/// must be single-threaded.
#[allow(dead_code)]
pub struct Lean4Bridge {
    _marker: std::marker::PhantomData<*const ()>, // !Send !Sync
}

impl Lean4Bridge {
    /// Create a new Lean 4 bridge.
    ///
    /// Note: This is a placeholder for future Lean 4 integration.
    /// When Lean 4 proofs are ready, this will initialize
    /// the Lean 4 runtime.
    ///
    /// # Errors
    /// Returns a `RouteError` if the Lean 4 runtime fails to initialize.
    #[allow(dead_code)]
    #[allow(clippy::unnecessary_wraps)]
    pub fn new() -> Result<Self, RouteError> {
        Ok(Self {
            _marker: std::marker::PhantomData,
        })
    }

    /// Call Lean 4 optimizer via FFI.
    ///
    /// # Safety
    /// The caller must ensure:
    /// 1. `nodes` pointer is valid for `node_count * 2` elements
    /// 2. `edges` pointer is valid for `edge_count * 2` elements
    /// 3. `start_node` is a valid index into the node array
    /// 4. The Lean 4 runtime has been initialized
    /// 5. This is called from the same thread that created the bridge
    #[cfg(feature = "lean4")]
    pub unsafe fn optimize_lean4(
        &self,
        nodes: *const c_double,
        node_count: c_uint,
        edges: *const c_uint,
        edge_count: c_uint,
        start_node: c_uint,
    ) -> Result<VerifiedResult, RouteError> {
        // Call Lean 4 function via C FFI
        let result = self.call_optimize_eulerian(
            nodes,
            node_count,
            edges,
            edge_count,
            start_node,
        );

        if result.success == 0 {
            return Err(RouteError::FfiError("Lean 4 optimization failed".to_string()));
        }

        Ok(result)
    }

    /// Internal method to call Lean 4 optimization.
    #[cfg(feature = "lean4")]
    unsafe fn call_optimize_eulerian(
        &self,
        _nodes: *const c_double,
        _node_count: c_uint,
        _edges: *const c_uint,
        _edge_count: c_uint,
        _start_node: c_uint,
    ) -> VerifiedResult {
        // TODO: Replace with actual Lean 4 FFI call
        // Placeholder result for testing
        VerifiedResult {
            circuit: std::ptr::null_mut(),
            circuit_length: 0,
            total_distance: 0.0,
            success: 0,
        }
    }
}

/// Extension trait for `RouteOptimizer` to flatten for FFI.
///
/// This trait provides methods to convert complex Rust graph structures
/// into simple C-compatible arrays for Lean 4 FFI integration.
// Aligns with Lean4: FFI boundary specification
#[allow(dead_code)]
pub trait FlattenForFFI {
    /// Convert graph to flat C-compatible arrays.
    #[must_use]
    fn flatten_for_ffi(&self) -> FlatGraph;

    /// Reconstruct optimization result from Lean 4 result.
    ///
    /// # Errors
    /// Returns a `RouteError` if the verified result indicates failure
    /// or if the result data is invalid.
    #[allow(clippy::wrong_self_convention)]
    fn from_verified_result(&self, result: VerifiedResult) -> Result<super::types::OptimizationResult, RouteError>;
}

/// Placeholder implementation for Node (testing only).
impl FlattenForFFI for super::types::Node {
    fn flatten_for_ffi(&self) -> FlatGraph {
        let node_coords: Vec<c_double> = vec![self.lat, self.lon];
        let edge_indices: Vec<c_uint> = Vec::new();
        FlatGraph::from_vecs(node_coords, edge_indices, 0)
    }

    fn from_verified_result(&self, _result: VerifiedResult) -> Result<super::types::OptimizationResult, RouteError> {
        Ok(super::types::OptimizationResult {
            route: vec![super::types::RoutePoint::new(self.lat, self.lon)],
            total_distance: 0.0,
            message: "Verified by Lean 4 (placeholder)".to_string(),
            stats: None,
        })
    }
}

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

    #[test]
    fn test_flat_graph_creation() {
        let node = super::super::types::Node::new("", 45.5, -73.6);
        let flat = node.flatten_for_ffi();

        assert_eq!(flat.node_count, 1);
        assert!(!flat.nodes.is_null());
        assert_eq!(flat.edge_count, 0);

        // Verify node coordinates
        // SAFETY: flatten_for_ffi creates a valid FlatGraph via from_vecs
        unsafe {
            assert_eq!(*flat.nodes, 45.5);
            assert_eq!(*flat.nodes.add(1), -73.6);
        }
    }

    #[test]
    fn test_flat_graph_from_vecs() {
        let coords = vec![45.5, -73.6, 45.6, -73.7];
        let edges = vec![0u32, 1u32];
        let flat = FlatGraph::from_vecs(
            coords.iter().map(|&v| v as c_double).collect(),
            edges.iter().map(|&v| v as c_uint).collect(),
            0,
        );
        assert_eq!(flat.node_count, 2);
        assert_eq!(flat.edge_count, 1);
    }

    #[test]
    fn test_lean4_bridge_creation() {
        let bridge = Lean4Bridge::new();
        assert!(bridge.is_ok());
    }

    #[test]
    fn test_verified_result_structure() {
        let result = VerifiedResult {
            circuit: std::ptr::null_mut(),
            circuit_length: 0,
            total_distance: 1000.0,
            success: 1,
        };

        assert_eq!(result.total_distance, 1000.0);
        assert_eq!(result.success, 1);
    }
}