Research-Stack/4-Infrastructure/shim/lake_compile_bridge/src/main.rs

// ── Lake Compile Bridge ────────────────────────────────────────────────
// Spawns `lake build <target>` with tamed parallelism, intercepts build
// events, and dispatches Q16_16 theorem verification to the GPU via wgpu.
//
// Architecture:
//   lake build ──stdout──► parser ──theorems──► GPU (wgpu + WGSL) ──► receipt
//
// Per AGENTS.md §4.1: Q16_16 integer arithmetic is deterministic across
// all substrates, so GPU verification is a valid accelerator for
// native_decide proof checking.
//
// The claim boundary is strict:
//   - GPU accelerates verification of finite UInt32 arithmetic theorems
//   - Lean/CPU remains authoritative for elaboration, type-checking, and
//     promotion of receipts

use std::process::{Command, Stdio};
use std::time::Instant;

use clap::Parser;
use serde::Serialize;

mod gpu;
mod q02_dispatch;

// ── Theorem Registry ────────────────────────────────────────────────────

/// FixedPoint theorems that can be GPU-verified.
const THEOREMS: &[(&str, u32)] = &[
    ("zero_mul", 0),
    ("mul_zero", 1),
    ("add_zero", 2),
    ("zero_add", 3),
    ("sub_self", 4),
    ("one_mul", 5),
    ("mul_one", 6),
    ("add_comm", 7),
    ("neg_involutive", 8),
    ("sub_via_neg", 9),
];

/// Q0_2 theorems for exhaustive GPU verification.
const Q02_THEOREMS: &[(&str, u32)] = &[
    ("q0_2_mul_self_nonneg", 10),
    ("q0_2_mul_nonneg", 11),
    ("q0_2_add_nonneg", 12),
];

// ── CLI ─────────────────────────────────────────────────────────────────

#[derive(Parser, Debug)]
#[command(
    name = "lake_compile_bridge",
    about = "GPU-accelerated Lean build bridge"
)]
struct Args {
    /// Lake build target (default: "Semantics.FixedPoint")
    #[arg(short, long, default_value = "Semantics.FixedPoint")]
    target: String,

    /// Parallel jobs for lake (default: 4)
    #[arg(short, long, default_value_t = 4)]
    jobs: u32,

    /// Number of random test vectors per theorem (default: 65536)
    #[arg(short, long, default_value_t = 65536)]
    vectors: u32,

    /// Write receipt to this path
    #[arg(short, long, default_value = "build_receipt.json")]
    receipt: String,

    /// Run Q0_2 exhaustive enumeration instead of FixedPoint random sampling
    #[arg(long, default_value_t = false)]
    q02: bool,

    /// Dry run: print what would be done without running
    #[arg(long, default_value_t = false)]
    dry_run: bool,
}

// ── Build Receipt ───────────────────────────────────────────────────────

#[derive(Serialize)]
struct BuildReceipt {
    schema: String,
    version: String,
    target: String,
    jobs: u32,
    vectors_per_theorem: u32,
    gpu_available: bool,
    gpu_device: String,
    theorems: Vec<TheoremReceipt>,
    total_theorems: usize,
    passed: usize,
    failed: usize,
    build_exit_code: Option<i32>,
    elapsed_ms: u64,
    timestamp_utc: String,
}

#[derive(Serialize)]
struct TheoremReceipt {
    name: String,
    theorem_id: u32,
    tested: u32,
    passed: bool,
}

fn timestamp_utc() -> String {
    chrono::Utc::now().format("%Y-%m-%dT%H:%M:%SZ").to_string()
}

// ── Main ────────────────────────────────────────────────────────────────

fn main() -> anyhow::Result<()> {
    let args = Args::parse();
    let start = Instant::now();

    eprintln!("═══ lake_compile_bridge ═══");
    eprintln!("  target: {}", args.target);
    eprintln!("  jobs: {}", args.jobs);
    eprintln!("  vectors/theorem: {}", args.vectors);
    eprintln!("  receipt: {}", args.receipt);

    // ── Stage 1: GPU probe ────────────────────────────────────────────
    let (gpu_available, gpu_device) = if !args.dry_run {
        match gpu::probe_gpu() {
            Ok(info) => {
                eprintln!("  GPU: {} ✓", info.name);
                (true, info.name)
            }
            Err(e) => {
                eprintln!("  GPU: unavailable ({}), falling back to CPU-only build", e);
                (false, format!("unavailable: {}", e))
            }
        }
    } else {
        (false, "dry-run".to_string())
    };

    // ── Stage 2: Spawn lake build ─────────────────────────────────────
    let build_exit_code = if !args.dry_run {
        eprintln!("  spawning: lake build {} -j {}", args.target, args.jobs);
        let status = Command::new("lake")
            .args(["build", &args.target, "-j", &args.jobs.to_string().as_str()])
            .stdout(Stdio::piped())
            .stderr(Stdio::piped())
            .status()?;
        Some(status.code().unwrap_or(-1))
    } else {
        eprintln!("  (dry-run, skipping lake build)");
        Some(0)
    };

    // ── Stage 3: GPU theorem verification ─────────────────────────────
    let theorems = if args.q02 {
        if gpu_available && !args.dry_run {
            eprintln!(
                "  dispatching {} Q0_2 theorems to GPU...",
                Q02_THEOREMS.len()
            );
            q02_dispatch::verify_q02_on_gpu()?
        } else {
            eprintln!("  (GPU unavailable or dry-run; marking all Q0_2 theorems as untested)");
            Q02_THEOREMS
                .iter()
                .map(|(name, id)| TheoremReceipt {
                    name: name.to_string(),
                    theorem_id: *id,
                    tested: 0,
                    passed: false,
                })
                .collect::<Vec<_>>()
        }
    } else if gpu_available && !args.dry_run {
        eprintln!("  dispatching {} theorems to GPU...", THEOREMS.len());
        gpu::verify_theorems_on_gpu(THEOREMS, args.vectors)?
    } else {
        eprintln!("  (GPU unavailable or dry-run; marking all theorems as untested)");
        THEOREMS
            .iter()
            .map(|(name, id)| TheoremReceipt {
                name: name.to_string(),
                theorem_id: *id,
                tested: 0,
                passed: false,
            })
            .collect::<Vec<_>>()
    };

    let total = theorems.len();
    let passed = theorems.iter().filter(|t| t.passed).count();
    let failed = total - passed;

    // ── Stage 4: Emit receipt ─────────────────────────────────────────
    let elapsed = start.elapsed().as_millis() as u64;
    let receipt = BuildReceipt {
        schema: "lake_compile_bridge_receipt_v1".to_string(),
        version: "0.1.0".to_string(),
        target: args.target.clone(),
        jobs: args.jobs,
        vectors_per_theorem: args.vectors,
        gpu_available,
        gpu_device,
        theorems,
        total_theorems: total,
        passed,
        failed,
        build_exit_code,
        elapsed_ms: elapsed,
        timestamp_utc: timestamp_utc(),
    };

    let receipt_json = serde_json::to_string_pretty(&receipt)?;
    if !args.dry_run {
        std::fs::write(&args.receipt, &receipt_json)?;
    }
    eprintln!("  receipt written to {}", args.receipt);
    eprintln!("  results: {}/{} theorems passed", passed, total);
    eprintln!("  elapsed: {} ms", elapsed);

    // Print receipt to stdout for piping
    println!("{}", receipt_json);

    Ok(())
}