xlog_prob/compilation/

mod.rs

//! GPU-native knowledge compilation.
//!
//! This module is the home of GPU-native compilation + verification utilities.
//!
//! Production correctness requires the GPU CDCL equivalence verifier (see `validation`).

use std::sync::atomic::{AtomicU64, Ordering};
use std::sync::Arc;
use std::time::Instant;

use xlog_core::{resolve_bool, Result, XlogError};
use xlog_cuda::memory::TrackedCudaSlice;
use xlog_cuda::CudaKernelProvider;
use xlog_solve::{GpuCdclConfig, GpuCnf};

use crate::compilation::gpu_cache::{GpuCircuitCache, GpuCircuitCacheHandle};
use crate::gpu::{GpuCircuitBuilder, GpuCircuitLayout, GpuXgcf};

pub mod disk_cache;
pub mod gpu_cache;
pub mod gpu_cnf;
pub mod gpu_d4;
pub mod gpu_pir;
pub mod gpu_pir_intern;
pub mod gpu_weights;
pub mod validation;

pub use gpu_cnf::{encode_cnf_gpu, GpuCnfEncoding, GpuCnfVarTables};
pub use gpu_d4::GpuCompileConfig;
pub use gpu_pir::{GpuPirGraph, GpuPirRoots, PIR_AND, PIR_LIT, PIR_NEG_LIT, PIR_OR};
// PIR_CONST and PIR_DECISION are used within gpu_pir.rs and gpu_pir_intern.rs
// via direct module paths; no crate-level re-export needed.
pub use gpu_pir_intern::{GpuPirInterner, PirBatch};
pub use gpu_weights::GpuWeights;
pub use gpu_weights::{
    apply_query_vars_device, build_evidence_by_var_gpu, build_weights_gpu, map_nodes_to_vars_gpu,
    restore_query_vars_device,
};
pub use validation::{
    build_equivalence_queries_gpu, validate_equivalence_gpu, validate_equivalence_gpu_gated,
    GpuEquivalenceConfig, GpuEquivalenceQueries,
};
// check_equivalence_gpu and check_equivalence_gpu_gated are called only
// within validation.rs itself; no crate-level re-export needed.

/// Per-stage compilation timing (populated only when XLOG_WARMUP_PROFILE=1).
#[derive(Debug, Clone, Default)]
pub struct CircuitCompileProfile {
    /// Seconds spent computing the canonical CNF hash.
    pub cnf_hash_sec: f64,
    /// Seconds spent compiling the circuit.
    pub d4_compile_sec: f64,
    /// Seconds spent verifying logical equivalence.
    pub verify_sec: f64,
    /// Seconds spent smoothing the final circuit.
    pub smooth_sec: f64,
    /// Seconds spent storing the verified circuit in cache.
    pub cache_store_sec: f64,
    /// Seconds spent constructing the free-variable mask.
    pub free_var_mask_sec: f64,
    /// Whether the circuit came from the resident GPU cache.
    pub gpu_cache_hit: bool,
    /// Whether the circuit came from the verified disk cache.
    pub disk_cache_hit: bool,
    /// BFS frontier item count after `frontier_depth` expansion steps
    /// (0 on cache hits or when profiling is disabled).
    pub frontier_items: u32,
}

/// Monotonic event ledger for one exact-circuit materialization path.
///
/// Mutation is private to this module so counts can only change at the GPU
/// compiler, verified disk-restore, GPU-cache-hit, and successful
/// materialization boundaries below. The exact state retains this ledger and
/// snapshots it around every prepared evaluation.
#[derive(Debug, Default)]
pub(crate) struct CircuitCompilationLedger {
    compiler_invocations: AtomicU64,
    materializations: AtomicU64,
    disk_cache_restores: AtomicU64,
    gpu_cache_hits: AtomicU64,
}

#[cfg(feature = "host-io")]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) struct CircuitCompilationSnapshot {
    pub(crate) compiler_invocations: u64,
    pub(crate) materializations: u64,
    pub(crate) disk_cache_restores: u64,
    pub(crate) gpu_cache_hits: u64,
}

impl CircuitCompilationLedger {
    pub(crate) fn new() -> Self {
        Self::default()
    }

    #[cfg(feature = "host-io")]
    pub(crate) fn snapshot(&self) -> CircuitCompilationSnapshot {
        CircuitCompilationSnapshot {
            compiler_invocations: self.compiler_invocations.load(Ordering::Acquire),
            materializations: self.materializations.load(Ordering::Acquire),
            disk_cache_restores: self.disk_cache_restores.load(Ordering::Acquire),
            gpu_cache_hits: self.gpu_cache_hits.load(Ordering::Acquire),
        }
    }

    fn record_compiler_invocation(&self) -> Result<()> {
        increment_circuit_event(
            &self.compiler_invocations,
            "GPU circuit compiler invocation",
        )
    }

    fn record_materialization(&self) -> Result<()> {
        increment_circuit_event(&self.materializations, "exact circuit materialization")
    }

    fn record_disk_cache_restore(&self) -> Result<()> {
        increment_circuit_event(&self.disk_cache_restores, "verified disk-cache restoration")
    }

    fn record_gpu_cache_hit(&self) -> Result<()> {
        increment_circuit_event(&self.gpu_cache_hits, "GPU circuit-cache hit")
    }
}

/// Cache identity and authoritative event ledger for one compilation attempt.
pub(crate) struct CircuitCompilationContext<'a> {
    pub(crate) canonical_cnf_hash: Option<u64>,
    pub(crate) ledger: &'a CircuitCompilationLedger,
}

fn increment_circuit_event(counter: &AtomicU64, event: &str) -> Result<()> {
    counter
        .try_update(Ordering::AcqRel, Ordering::Acquire, |value| {
            value.checked_add(1)
        })
        .map(|_| ())
        .map_err(|_| XlogError::Compilation(format!("{event} counter overflowed")))
}

pub(crate) fn warmup_profiling_enabled() -> Result<bool> {
    resolve_bool(None, "XLOG_WARMUP_PROFILE", false)
}

/// Device-resident random-variable list for GPU smoothing.
pub struct DeviceRandomVarList {
    list: TrackedCudaSlice<u32>,
    count: u32,
}

/// Circuit whose exact topology has passed equivalence verification.
///
/// The field is private so topology-changing code cannot construct this type
/// without going through [`certify_final_circuit`].
struct CertifiedGpuCircuit(GpuXgcf);

impl CertifiedGpuCircuit {
    fn as_xgcf(&self) -> &GpuXgcf {
        &self.0
    }
}

impl DeviceRandomVarList {
    /// Constructs a validated list from an existing device allocation and logical count.
    pub fn from_device(list: TrackedCudaSlice<u32>, count: u32) -> Result<Self> {
        let len = u32::try_from(list.len()).map_err(|_| {
            XlogError::Compilation("DeviceRandomVarList: list length exceeds u32".to_string())
        })?;
        if count > len {
            return Err(XlogError::Compilation(format!(
                "DeviceRandomVarList: count {} exceeds list len {}",
                count, len
            )));
        }
        Ok(Self { list, count })
    }

    /// Uploads a host list of random-variable identifiers.
    pub fn from_host(provider: &CudaKernelProvider, host: &[u32]) -> Result<Self> {
        let memory = provider.memory();
        let mut list = memory.alloc::<u32>(host.len())?;
        if !host.is_empty() {
            provider
                .htod_sync_copy_into_tracked(host, &mut list)
                .map_err(|e| {
                    XlogError::Kernel(format!("DeviceRandomVarList upload failed: {}", e))
                })?;
        }
        let count = u32::try_from(host.len()).map_err(|_| {
            XlogError::Compilation("DeviceRandomVarList: host len exceeds u32".to_string())
        })?;
        Ok(Self { list, count })
    }

    /// Returns whether the logical list is empty.
    pub fn is_empty(&self) -> bool {
        self.count == 0
    }

    /// Returns the logical number of random variables.
    pub fn count(&self) -> u32 {
        self.count
    }

    /// Returns the device-resident variable identifiers.
    pub fn list(&self) -> &TrackedCudaSlice<u32> {
        &self.list
    }
}

fn certify_final_circuit(
    cnf: &GpuCnf,
    decision_var_limit: &TrackedCudaSlice<u32>,
    circuit: GpuXgcf,
    provider: &Arc<CudaKernelProvider>,
    config: GpuEquivalenceConfig,
    gate: &TrackedCudaSlice<u32>,
) -> Result<CertifiedGpuCircuit> {
    validate_equivalence_gpu_gated(cnf, decision_var_limit, &circuit, provider, config, gate)?;
    Ok(CertifiedGpuCircuit(circuit))
}

fn upload_disk_artifact_for_verification(
    artifact: &disk_cache::CircuitArtifact,
    provider: &Arc<CudaKernelProvider>,
) -> Result<GpuXgcf> {
    let memory = provider.memory().clone();

    macro_rules! upload {
        ($field:expr, $ty:ty, $name:literal) => {{
            let mut device = memory.alloc::<$ty>($field.len())?;
            provider
                .htod_sync_copy_into_tracked($field, &mut device)
                .map_err(|e| {
                    XlogError::Kernel(format!("disk cache verify upload {} failed: {}", $name, e))
                })?;
            device
        }};
    }

    let builder = GpuCircuitBuilder {
        node_type: upload!(&artifact.node_type, u8, "node_type"),
        child_offsets: upload!(&artifact.child_offsets, u32, "child_offsets"),
        child_indices: upload!(&artifact.child_indices, u32, "child_indices"),
        lit: upload!(&artifact.lit, i32, "lit"),
        decision_var: upload!(&artifact.decision_var, u32, "decision_var"),
        decision_child_false: upload!(&artifact.decision_child_false, u32, "decision_child_false"),
        decision_child_true: upload!(&artifact.decision_child_true, u32, "decision_child_true"),
    };
    let layout = GpuCircuitLayout {
        num_nodes: artifact.num_nodes,
        num_edges: artifact.num_edges,
        num_levels: artifact.num_levels,
        level_offsets: upload!(&artifact.level_offsets, u32, "level_offsets"),
        level_nodes: upload!(&artifact.level_nodes, u32, "level_nodes"),
        root: artifact.root,
        max_var: artifact.max_var,
        num_nodes_device: None,
        num_edges_device: None,
    };

    GpuXgcf::from_device(builder, layout, provider)
}

/// Compile CNF on GPU, then verify equivalence with GPU CDCL.
pub fn compile_gpu_d4_and_verify(
    cnf: &GpuCnf,
    decision_var_limit: &TrackedCudaSlice<u32>,
    provider: &Arc<CudaKernelProvider>,
    config: &GpuCompileConfig,
) -> Result<GpuXgcf> {
    if config.cdcl_conflict_budget.is_some() {
        return Err(XlogError::Compilation(
            "cdcl_conflict_budget is not supported by the GPU CDCL verifier".to_string(),
        ));
    }
    // Size guard BEFORE compile — the D4 compile itself can crash with a
    // context-poisoning launch failure on a large CNF, earlier than the verify.
    validation::check_verify_size_bound(cnf, "compile_gpu_d4_and_verify")?;
    let circuit = gpu_d4::compile_gpu_d4(cnf, provider, config)?;
    let cdcl = cdcl_config_from_compile(config)?;
    validate_equivalence_gpu(
        cnf,
        decision_var_limit,
        &circuit,
        provider,
        GpuEquivalenceConfig {
            cdcl,
            reuse_workspace: config.incremental_verify,
        },
    )?;
    Ok(circuit)
}

/// Compile CNF on GPU, cache the circuit, then verify equivalence with GPU CDCL.
///
/// `canonical_cnf_hash`: a process-independent hash of the PIR structure, used as
/// the `cnf_hash` in the disk cache key. Computed via [`crate::cnf::canonical_pir_hash`].
/// If `None`, disk caching is skipped.
pub fn compile_gpu_d4_and_verify_cached(
    cnf: &GpuCnf,
    decision_var_limit: &TrackedCudaSlice<u32>,
    provider: &Arc<CudaKernelProvider>,
    config: &GpuCompileConfig,
    cache: &mut GpuCircuitCache,
    random_vars: &DeviceRandomVarList,
    canonical_cnf_hash: Option<u64>,
) -> Result<(GpuCircuitCacheHandle, Option<CircuitCompileProfile>)> {
    let ledger = CircuitCompilationLedger::new();
    compile_gpu_d4_and_verify_cached_with_ledger(
        cnf,
        decision_var_limit,
        provider,
        config,
        cache,
        random_vars,
        CircuitCompilationContext {
            canonical_cnf_hash,
            ledger: &ledger,
        },
    )
}

pub(crate) fn compile_gpu_d4_and_verify_cached_with_ledger(
    cnf: &GpuCnf,
    decision_var_limit: &TrackedCudaSlice<u32>,
    provider: &Arc<CudaKernelProvider>,
    config: &GpuCompileConfig,
    cache: &mut GpuCircuitCache,
    random_vars: &DeviceRandomVarList,
    context: CircuitCompilationContext<'_>,
) -> Result<(GpuCircuitCacheHandle, Option<CircuitCompileProfile>)> {
    let CircuitCompilationContext {
        canonical_cnf_hash,
        ledger,
    } = context;
    if config.cdcl_conflict_budget.is_some() {
        return Err(XlogError::Compilation(
            "cdcl_conflict_budget is not supported by the GPU CDCL verifier".to_string(),
        ));
    }
    // Size guard BEFORE compile (the D4 compile can crash earlier than
    // the verify on a large CNF).
    validation::check_verify_size_bound(cnf, "compile_gpu_d4_and_verify_cached")?;

    let profiling = warmup_profiling_enabled()?;
    let mut profile = CircuitCompileProfile::default();

    // --- CNF hash stage ---
    #[cfg(debug_assertions)]
    eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: hash_cnf_gpu");
    let t_hash = if profiling {
        Some(Instant::now())
    } else {
        None
    };
    let key = gpu_cache::hash_cnf_gpu(cnf, provider)?;
    if let Some(t0) = t_hash {
        provider
            .device()
            .synchronize()
            .map_err(|e| XlogError::Kernel(format!("sync after hash_cnf_gpu: {}", e)))?;
        profile.cnf_hash_sec = t0.elapsed().as_secs_f64();
    }
    #[cfg(debug_assertions)]
    {
        if !profiling {
            provider
                .device()
                .synchronize()
                .map_err(|e| XlogError::Kernel(format!("sync after hash_cnf_gpu failed: {}", e)))?;
        }
    }
    #[cfg(debug_assertions)]
    eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: lookup_or_insert_device");
    let lookup = cache.lookup_or_insert_device(&key)?;
    let mut handle = lookup.into_handle()?;

    // --- Disk cache check (only on GPU cache miss) ---
    //
    // D→H copy compile_needed to decide whether we need to compile at all.
    // If compile_needed == 0, the GPU cache already has the circuit (GPU cache hit).
    // If compile_needed == 1, we check the disk cache before falling through to the
    // GPU-native Decision-DNNF compiler.
    let compile_needed_host: Vec<u32> = provider
        .device()
        .inner()
        .dtoh_sync_copy(handle.compile_needed_device())
        .map_err(|e| XlogError::Kernel(format!("dtoh compile_needed: {}", e)))?;
    let compile_needed = compile_needed_host[0];

    // GPU cache hit — short-circuit the entire compile pipeline.
    if compile_needed == 0 {
        profile.gpu_cache_hit = true;
        ledger.record_gpu_cache_hit()?;
        ledger.record_materialization()?;
        let out_profile = if profiling { Some(profile) } else { None };
        return Ok((handle, out_profile));
    }

    // Build the disk cache key (we know compile_needed == 1 at this point).
    // The canonical PIR hash keeps semantically stable cache identity, while the encoded CNF
    // hash guards symmetric conditioned programs whose PIR shape is identical but whose CNF is not.
    let cache_key = if compile_needed == 1 {
        if let Some(canonical_hash) = canonical_cnf_hash {
            let config_hash = hash_compile_config(config);
            let random_vars_hash = hash_random_vars(random_vars, provider)?;
            let gpu_cnf_hash = read_gpu_cnf_hash(&key, provider)?;
            let cnf_hash = combine_disk_cnf_hash(canonical_hash, gpu_cnf_hash);
            let sm = detect_compute_capability(provider)?;
            Some(disk_cache::CircuitCacheKey {
                cnf_hash,
                config_hash,
                random_vars_hash,
                sm,
            })
        } else {
            None
        }
    } else {
        None
    };

    // Check disk cache on GPU cache miss
    if let Some(ref disk_key) = cache_key {
        #[cfg(debug_assertions)]
        eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: checking disk cache");
        if let Ok(Some(artifact)) = disk_cache::read_artifact(disk_key) {
            #[cfg(debug_assertions)]
            eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: disk cache hit");
            // Stale-artifact guard: the canonical PIR hash keeps semantically-stable
            // cache identity, so an entry written by an earlier engine whose ENCODING
            // differed (different var universe) can be served for the same key. A
            // cached circuit referencing vars beyond the freshly-encoded CNF is
            // staleness, not an engine bug — evict and fall through to a fresh
            // compile (which overwrites the entry). Fail-closed equivalence checking
            // stays authoritative for freshly-compiled circuits below.
            if artifact.max_var > cnf.var_cap {
                #[cfg(debug_assertions)]
                eprintln!(
                    "[xlog-prob] compile_gpu_d4_and_verify_cached: stale disk artifact \
                     (max_var {} > cnf var_cap {}), evicting",
                    artifact.max_var, cnf.var_cap
                );
                disk_cache::evict_artifact(disk_key);
            } else {
                let circuit = upload_disk_artifact_for_verification(&artifact, provider)?;
                let verifier_decision_var_limit = if random_vars.is_empty() {
                    &cnf.num_vars
                } else {
                    decision_var_limit
                };
                let cdcl = cdcl_config_from_compile(config)?;
                let t_verify = if profiling {
                    Some(Instant::now())
                } else {
                    None
                };
                match certify_final_circuit(
                    cnf,
                    verifier_decision_var_limit,
                    circuit,
                    provider,
                    GpuEquivalenceConfig {
                        cdcl,
                        reuse_workspace: config.incremental_verify,
                    },
                    handle.compile_needed_device(),
                ) {
                    Ok(_certified_circuit) => {
                        if let Some(t0) = t_verify {
                            provider.device().synchronize().map_err(|e| {
                                XlogError::Kernel(format!("sync after disk cache verify: {}", e))
                            })?;
                            profile.verify_sec = t0.elapsed().as_secs_f64();
                        }
                        cache.restore_from_host_arrays(&mut handle, &artifact)?;
                        provider.device().synchronize().map_err(|e| {
                            XlogError::Kernel(format!("sync after disk cache restore: {}", e))
                        })?;
                        profile.disk_cache_hit = true;
                        ledger.record_disk_cache_restore()?;
                        ledger.record_materialization()?;
                        let out_profile = if profiling { Some(profile) } else { None };
                        return Ok((handle, out_profile));
                    }
                    Err(_stale) => {
                        // A cached artifact failing equivalence against the current
                        // CNF is a stale entry (fresh-compile verification below
                        // remains fail-closed). Evict and recompile.
                        #[cfg(debug_assertions)]
                        eprintln!(
                            "[xlog-prob] compile_gpu_d4_and_verify_cached: cached circuit \
                             failed equivalence against current CNF ({_stale}), evicting"
                        );
                        disk_cache::evict_artifact(disk_key);
                    }
                }
            }
        }
        #[cfg(debug_assertions)]
        eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: disk cache miss");
    }

    let d4_config = d4_config_for_smoothing(config, random_vars.count())?;

    // --- GPU-native Decision-DNNF compile stage ---
    #[cfg(debug_assertions)]
    eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: compile_gpu_d4_gated");
    let t_d4 = if profiling {
        Some(Instant::now())
    } else {
        None
    };
    ledger.record_compiler_invocation()?;
    let (circuit_base, frontier_items) = gpu_d4::compile_gpu_d4_gated_with_stats(
        cnf,
        provider,
        &d4_config,
        handle.compile_needed_device(),
    )?;
    profile.frontier_items = frontier_items;
    if let Some(t0) = t_d4 {
        provider
            .device()
            .synchronize()
            .map_err(|e| XlogError::Kernel(format!("sync after d4 compile: {}", e)))?;
        profile.d4_compile_sec = t0.elapsed().as_secs_f64();
    }
    #[cfg(debug_assertions)]
    {
        if !profiling {
            provider.device().synchronize().map_err(|e| {
                XlogError::Kernel(format!("sync after compile_gpu_d4_gated failed: {}", e))
            })?;
        }
    }
    if circuit_base.num_nodes() == 0 || circuit_base.num_levels() == 0 {
        // Defensive: the GPU-native Decision-DNNF compiler returned an empty circuit
        // (the primary GPU cache hit is handled by the compile_needed == 0 early return
        // above; this catches degenerate CNFs).
        ledger.record_materialization()?;
        let out_profile = if profiling { Some(profile) } else { None };
        return Ok((handle, out_profile));
    }

    // --- Smoothing stage ---
    let t_smooth = if profiling {
        Some(Instant::now())
    } else {
        None
    };
    let circuit_eval = if random_vars.is_empty() {
        circuit_base
    } else {
        #[cfg(debug_assertions)]
        eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: smooth_random_vars_device");
        let smoothed = circuit_base.smooth_random_vars_device(
            provider,
            random_vars.list(),
            random_vars.count(),
            config.smooth_node_cap,
            config.smooth_edge_cap,
        )?;
        #[cfg(debug_assertions)]
        {
            if !profiling {
                provider.device().synchronize().map_err(|e| {
                    XlogError::Kernel(format!(
                        "sync after smooth_random_vars_device failed: {}",
                        e
                    ))
                })?;
            }
        }
        smoothed
    };
    if let Some(t0) = t_smooth {
        provider
            .device()
            .synchronize()
            .map_err(|e| XlogError::Kernel(format!("sync after smooth: {}", e)))?;
        profile.smooth_sec = t0.elapsed().as_secs_f64();
    }

    // --- Verify final-circuit equivalence stage ---
    //
    // Certification is deliberately after every topology-changing pass. The
    // exact `circuit_eval` value verified here is the value cached below and
    // consumed by weighted model counting and gradients.
    //
    // `encode_cnf_gpu` sets `decision_var_limit` to the end of the leaf+choice var range. For
    // deterministic programs with no probabilistic vars, this range is empty (limit=0). In that
    // case, the verifier must still be able to branch, so fall back to `cnf.num_vars` (all CNF
    // vars are semantically meaningful when there is no probabilistic decision set).
    let verifier_decision_var_limit = if random_vars.is_empty() {
        &cnf.num_vars
    } else {
        decision_var_limit
    };
    let cdcl = cdcl_config_from_compile(config)?;
    #[cfg(debug_assertions)]
    eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: validate_equivalence_gpu_gated");
    let t_verify = if profiling {
        Some(Instant::now())
    } else {
        None
    };
    let certified_circuit = certify_final_circuit(
        cnf,
        verifier_decision_var_limit,
        circuit_eval,
        provider,
        GpuEquivalenceConfig {
            cdcl,
            reuse_workspace: config.incremental_verify,
        },
        handle.compile_needed_device(),
    )?;
    if let Some(t0) = t_verify {
        provider
            .device()
            .synchronize()
            .map_err(|e| XlogError::Kernel(format!("sync after verify: {}", e)))?;
        profile.verify_sec = t0.elapsed().as_secs_f64();
    }
    #[cfg(debug_assertions)]
    {
        if !profiling {
            provider.device().synchronize().map_err(|e| {
                XlogError::Kernel(format!(
                    "sync after validate_equivalence_gpu_gated failed: {}",
                    e
                ))
            })?;
        }
    }

    // --- Cache store stage ---
    #[cfg(debug_assertions)]
    eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: store_from_xgcf");
    let t_store = if profiling {
        Some(Instant::now())
    } else {
        None
    };
    cache.store_from_xgcf(&mut handle, certified_circuit.as_xgcf())?;
    if let Some(t0) = t_store {
        provider
            .device()
            .synchronize()
            .map_err(|e| XlogError::Kernel(format!("sync after cache store: {}", e)))?;
        profile.cache_store_sec = t0.elapsed().as_secs_f64();
    }
    #[cfg(debug_assertions)]
    {
        if !profiling {
            provider.device().synchronize().map_err(|e| {
                XlogError::Kernel(format!("sync after store_from_xgcf failed: {}", e))
            })?;
        }
    }

    // --- Free-var mask stage ---
    #[cfg(debug_assertions)]
    eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: compute_free_var_mask_gpu_gated");
    let t_fvm = if profiling {
        Some(Instant::now())
    } else {
        None
    };
    let free_var_mask = gpu_d4::compute_free_var_mask_gpu_gated(
        cnf,
        certified_circuit.as_xgcf(),
        provider,
        handle.compile_needed_device(),
    )?;
    #[cfg(debug_assertions)]
    {
        if !profiling {
            provider.device().synchronize().map_err(|e| {
                XlogError::Kernel(format!(
                    "sync after compute_free_var_mask_gpu_gated failed: {}",
                    e
                ))
            })?;
        }
    }
    // Only enable free-var correction if there are actual free variables.
    // When the mask is all-zero (common for smoothed d-DNNF circuits),
    // skipping this keeps has_free_var_mask[slot]=false, which avoids unnecessary
    // free-var correction kernel launches on every subsequent eval.
    let mask_host: Vec<u8> = provider
        .device()
        .inner()
        .dtoh_sync_copy(&free_var_mask)
        .map_err(|e| XlogError::Kernel(format!("Failed to read free_var_mask: {}", e)))?;
    let has_free_vars = mask_host.iter().any(|&b| b != 0);
    #[cfg(debug_assertions)]
    eprintln!(
        "[xlog-prob] free_var_mask: {} free vars, batched eval {}",
        if has_free_vars { "has" } else { "no" },
        if has_free_vars { "DISABLED" } else { "ENABLED" },
    );
    if has_free_vars {
        cache.store_free_var_mask(&handle, &free_var_mask)?;
        #[cfg(debug_assertions)]
        {
            if !profiling {
                provider.device().synchronize().map_err(|e| {
                    XlogError::Kernel(format!("sync after store_free_var_mask failed: {}", e))
                })?;
            }
        }
    }
    if let Some(t0) = t_fvm {
        provider
            .device()
            .synchronize()
            .map_err(|e| XlogError::Kernel(format!("sync after free_var_mask: {}", e)))?;
        profile.free_var_mask_sec = t0.elapsed().as_secs_f64();
    }

    // --- Disk cache write (opportunistic) ---
    //
    // After a successful compilation, write the artifact to disk for next warm start.
    // Errors are silently ignored — the disk cache is best-effort.
    if let Some(ref disk_key) = cache_key {
        if let Ok(artifact) = cache.build_artifact_from_device(&handle, provider) {
            let _ = disk_cache::write_artifact(disk_key, &artifact);
            #[cfg(debug_assertions)]
            eprintln!("[xlog-prob] compile_gpu_d4_and_verify_cached: wrote disk cache artifact");
        }
    }

    ledger.record_materialization()?;
    let out_profile = if profiling { Some(profile) } else { None };
    Ok((handle, out_profile))
}

fn d4_config_for_smoothing(
    config: &GpuCompileConfig,
    random_var_count: u32,
) -> Result<GpuCompileConfig> {
    if random_var_count == 0 {
        return Ok(*config);
    }
    let headroom = 2u32
        .checked_add(random_var_count)
        .ok_or_else(|| XlogError::Compilation("smooth headroom overflow".to_string()))?;
    if config.smooth_node_cap <= headroom {
        return Err(XlogError::Compilation(format!(
            "GpuCompileConfig smooth_node_cap {} too small for smoothing headroom {}",
            config.smooth_node_cap, headroom
        )));
    }
    let base_cap = config
        .smooth_node_cap
        .checked_sub(headroom)
        .ok_or_else(|| XlogError::Compilation("smooth node cap underflow".to_string()))?;
    if base_cap < 3 {
        return Err(XlogError::Compilation(
            "GpuCompileConfig smooth_node_cap leaves <3 base nodes".to_string(),
        ));
    }
    let mut out = *config;
    out.smooth_node_cap = base_cap;
    Ok(out)
}

fn cdcl_config_from_compile(config: &GpuCompileConfig) -> Result<GpuCdclConfig> {
    if config.cdcl_restart_interval == 0 {
        return Err(XlogError::Compilation(
            "cdcl_restart_interval must be > 0".to_string(),
        ));
    }
    if config.cdcl_learned_bytes == 0 {
        return Err(XlogError::Compilation(
            "cdcl_learned_bytes must be > 0".to_string(),
        ));
    }

    // Deterministic sizing: assume average learned clause length = 4.
    const AVG_LEN: u64 = 4;
    const META_BYTES_PER_CLAUSE: u64 = 24; // offsets + lbd + activity + flags + proof offsets (rounded up)
    const PROOF_BYTES_PER_CLAUSE: u64 = 8 + (8 * AVG_LEN); // (conflict, steps) + 2*u32 per lit
    const LIT_BYTES_PER_CLAUSE: u64 = 4 * AVG_LEN;

    let bytes_per_clause = META_BYTES_PER_CLAUSE
        .checked_add(PROOF_BYTES_PER_CLAUSE)
        .and_then(|v| v.checked_add(LIT_BYTES_PER_CLAUSE))
        .ok_or_else(|| XlogError::Compilation("cdcl bytes per clause overflow".to_string()))?;

    let max_clauses = config
        .cdcl_learned_bytes
        .checked_div(bytes_per_clause)
        .ok_or_else(|| XlogError::Compilation("cdcl_learned_bytes div overflow".to_string()))?;
    if max_clauses == 0 {
        return Err(XlogError::Compilation(
            "cdcl_learned_bytes too small for learned clause arena".to_string(),
        ));
    }

    let max_lits = max_clauses
        .checked_mul(AVG_LEN)
        .ok_or_else(|| XlogError::Compilation("max_learned_lits overflow".to_string()))?;
    let max_proof_u32 = max_clauses
        .checked_mul(2 + 2 * AVG_LEN)
        .ok_or_else(|| XlogError::Compilation("max_proof_u32 overflow".to_string()))?;

    let max_learned_clauses = u32::try_from(max_clauses)
        .map_err(|_| XlogError::Compilation("max_learned_clauses exceeds u32::MAX".to_string()))?;
    let max_learned_lits = u32::try_from(max_lits)
        .map_err(|_| XlogError::Compilation("max_learned_lits exceeds u32::MAX".to_string()))?;
    let max_proof_u32 = u32::try_from(max_proof_u32)
        .map_err(|_| XlogError::Compilation("max_proof_u32 exceeds u32::MAX".to_string()))?;

    let reduce_interval = config
        .cdcl_restart_interval
        .checked_mul(20)
        .ok_or_else(|| XlogError::Compilation("cdcl reduce_interval overflow".to_string()))?;

    let mut gpu_cdcl = GpuCdclConfig::default();
    gpu_cdcl.max_learned_clauses = max_learned_clauses;
    gpu_cdcl.max_learned_lits = max_learned_lits;
    gpu_cdcl.max_proof_u32 = max_proof_u32;
    gpu_cdcl.restart_base = config.cdcl_restart_interval;
    gpu_cdcl.reduce_interval = reduce_interval;
    // Fail-closed conflict budget. Treewidth-hard equivalence verifies can
    // spin past the GPU watchdog and crash with a context-poisoning launch
    // failure; a finite budget makes them decline (VerifyBudgetExceeded) before
    // that. Default 0 = unlimited (no behavior change). A recommended value is a
    // calibration follow-up (between a completing verify's conflict count and
    // the watchdog boundary); operators opt in via XLOG_D4_VERIFY_MAX_CONFLICTS.
    gpu_cdcl.max_conflicts = verify_max_conflicts();
    Ok(gpu_cdcl)
}

/// Per-verify conflict budget, read once from
/// `XLOG_D4_VERIFY_MAX_CONFLICTS`. Default 0 = unlimited.
fn verify_max_conflicts() -> u32 {
    static BUDGET: std::sync::OnceLock<u32> = std::sync::OnceLock::new();
    *BUDGET.get_or_init(|| {
        std::env::var("XLOG_D4_VERIFY_MAX_CONFLICTS")
            .ok()
            .and_then(|v| v.trim().parse::<u32>().ok())
            .unwrap_or(0)
    })
}

// ---------------------------------------------------------------------------
// Disk cache helpers
// ---------------------------------------------------------------------------

/// FNV-1a 64-bit hash — deterministic across processes and Rust versions.
/// Matches the FNV-1a algorithm used in the GPU hash kernel (kernels/cache.cu).
fn fnv1a_u64(bytes: &[u8]) -> u64 {
    const FNV_OFFSET: u64 = 0xcbf29ce484222325;
    const FNV_PRIME: u64 = 0x100000001b3;
    let mut h = FNV_OFFSET;
    for &b in bytes {
        h ^= b as u64;
        h = h.wrapping_mul(FNV_PRIME);
    }
    h
}

fn combine_disk_cnf_hash(canonical_hash: u64, gpu_cnf_hash: u64) -> u64 {
    let mut buf = Vec::with_capacity(16);
    buf.extend_from_slice(&canonical_hash.to_le_bytes());
    buf.extend_from_slice(&gpu_cnf_hash.to_le_bytes());
    fnv1a_u64(&buf)
}

fn read_gpu_cnf_hash(
    hash: &TrackedCudaSlice<u64>,
    provider: &Arc<CudaKernelProvider>,
) -> Result<u64> {
    let host: Vec<u64> = provider
        .device()
        .inner()
        .dtoh_sync_copy(hash)
        .map_err(|e| XlogError::Kernel(format!("dtoh GPU CNF hash for disk cache key: {}", e)))?;
    host.first()
        .copied()
        .ok_or_else(|| XlogError::Kernel("empty GPU CNF hash for disk cache key".to_string()))
}

/// Hash the compile config fields that affect circuit topology output.
fn hash_compile_config(config: &GpuCompileConfig) -> u64 {
    let mut buf = Vec::new();
    buf.extend_from_slice(&config.frontier_depth.to_le_bytes());
    buf.extend_from_slice(&config.max_frontier_items.to_le_bytes());
    buf.extend_from_slice(&config.max_depth.to_le_bytes());
    buf.extend_from_slice(&config.smooth_node_cap.to_le_bytes());
    buf.extend_from_slice(&config.smooth_edge_cap.to_le_bytes());
    // CDCL verifier params do not affect the compiled circuit topology,
    // but we include them for safety so a verifier config change invalidates the cache.
    buf.extend_from_slice(&config.cdcl_restart_interval.to_le_bytes());
    buf.extend_from_slice(&config.cdcl_learned_bytes.to_le_bytes());
    fnv1a_u64(&buf)
}

/// Hash the random variable list (D→H copy + hash).
fn hash_random_vars(
    random_vars: &DeviceRandomVarList,
    provider: &Arc<CudaKernelProvider>,
) -> Result<u64> {
    let count = random_vars.count();
    let mut buf = Vec::new();
    buf.extend_from_slice(&count.to_le_bytes());
    if count > 0 {
        let host: Vec<u32> = provider
            .device()
            .inner()
            .dtoh_sync_copy(random_vars.list())
            .map_err(|e| {
                XlogError::Kernel(format!("dtoh random_vars for disk cache hash: {}", e))
            })?;
        // Hash only the valid elements (count may be less than the allocation).
        for &v in &host[..count as usize] {
            buf.extend_from_slice(&v.to_le_bytes());
        }
    }
    Ok(fnv1a_u64(&buf))
}

/// Query the device compute capability and encode as `major * 10 + minor` (e.g. 89 for sm_89).
fn detect_compute_capability(provider: &Arc<CudaKernelProvider>) -> Result<u32> {
    use cudarc::driver::sys::CUdevice_attribute;

    let device = provider.device().inner();
    let major = device
        .attribute(CUdevice_attribute::CU_DEVICE_ATTRIBUTE_COMPUTE_CAPABILITY_MAJOR)
        .map_err(|e| {
            XlogError::Kernel(format!("Failed to query compute capability major: {}", e))
        })?;
    let minor = device
        .attribute(CUdevice_attribute::CU_DEVICE_ATTRIBUTE_COMPUTE_CAPABILITY_MINOR)
        .map_err(|e| {
            XlogError::Kernel(format!("Failed to query compute capability minor: {}", e))
        })?;
    let major_u32: u32 = major.try_into().map_err(|_| {
        XlogError::Kernel(format!(
            "compute capability major {} cannot be converted to u32",
            major
        ))
    })?;
    let minor_u32: u32 = minor.try_into().map_err(|_| {
        XlogError::Kernel(format!(
            "compute capability minor {} cannot be converted to u32",
            minor
        ))
    })?;
    Ok(major_u32 * 10 + minor_u32)
}