vyre-conform 0.1.0

//! Mechanical checks for the extensibility admission gates.

use std::fmt;
use std::path::Path;
use std::thread;

use crate::enforce::category::{
    check_category_a_zero_overhead, check_category_b_tripwire, check_category_c_intrinsic,
};
use crate::generate::generators::default_generators;
use crate::spec::OpSpec;
use crate::spec::OracleKind;
use vyre_spec::Category;

const DETERMINISM_SEEDS: &[u64] = &[
    0xA6D1_5510_4DAD_0004,
    0xCAFE_BABE_DEAD_BEEF,
    0x0123_4567_89AB_CDEF,
    0xFEDC_BA98_7654_3210,
    0xA5A5_A5A5_A5A5_A5A5,
    0x5A5A_5A5A_5A5A_5A5A,
    0x1111_2222_3333_4444,
    0x5555_6666_7777_8888,
    0x9999_AAAA_BBBB_CCCC,
    0xDDDD_EEEE_FFFF_0000,
    0x0F0F_0F0F_0F0F_0F0F,
    0xF0F0_F0F0_F0F0_F0F0,
    0x1234_5678_9ABC_DEF0,
    0xFEDC_BA98_7654_3210,
    0xAAAA_BBBB_CCCC_DDDD,
    0xEEEE_FFFF_0000_1111,
    0x2222_3333_4444_5555,
    0x6666_7777_8888_9999,
    0xBAD0_BAD0_BAD0_BAD0,
    0xC0DE_C0DE_C0DE_C0DE,
    0xFACE_FACE_FACE_FACE,
    0xBEEF_BEEF_BEEF_BEEF,
    0xDEAD_DEAD_DEAD_DEAD,
    0xC0FF_EE00_C0FF_EE00,
    0x8BAD_F00D_8BAD_F00D,
    0x1BAD_B002_1BAD_B002,
    0xD15C_0DED_D15C_0DED,
    0xB105_F00D_B105_F00D,
    0x0D15_0D15_0D15_0D15,
    0xFEED_FACE_FEED_FACE,
    0xC0CA_C01A_C0CA_C01A,
    0xB8B8_B8B8_B8B8_B8B8,
];

const GATE_4_DEFAULT_MAX_GENERATED_INPUTS: usize = 10_000;

/// Admission gate failure for a proposed operation.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct AdmissionFinding {
    /// Operation ID associated with the finding.
    pub op_id: String,
    /// Gate number from the extensibility discipline.
    pub gate: u8,
    /// Human-readable failure text.
    pub message: String,
}

impl AdmissionFinding {
    fn new(op_id: &str, gate: u8, message: impl Into<String>) -> Self {
        Self {
            op_id: op_id.to_string(),
            gate,
            message: message.into(),
        }
    }

    /// Return the operation id associated with this admission finding.
    #[inline]
    pub fn op_id(&self) -> &str {
        &self.op_id
    }
}

impl fmt::Display for AdmissionFinding {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(
            f,
            "Op {} fails admission gate {}: {}",
            self.op_id, self.gate, self.message
        )
    }
}

/// Run mechanical admission gates 4, 5, 6, 7, 8, and 9.
///
/// Gates 1, 2, and 3 are represented by the contributor's category
/// declaration and remain human-reviewed.
#[inline]
pub fn check_admission(specs: &[OpSpec], vyre_src_root: &Path) -> Vec<AdmissionFinding> {
    let mut findings = Vec::new();
    findings.extend(check_gate_4_deterministic_semantics(specs));
    findings.extend(check_gate_5_cpu_reference(specs));
    findings.extend(check_gate_6_conformance_rules(specs));

    let root = vyre_src_root;
    if let Err(gate7_findings) =
        crate::enforce::enforcers::gate_7_coverage::enforce_gate_7_from_report(root)
    {
        for f in gate7_findings {
            findings.push(AdmissionFinding::new(&f.op_id, 7, f.fix));
        }
    }
    findings.extend(check_category_abc_overhead(specs, vyre_src_root));
    findings
}

/// Category A zero-overhead + B tripwire + C intrinsic validation.
fn check_category_abc_overhead(specs: &[OpSpec], vyre_src_root: &Path) -> Vec<AdmissionFinding> {
    let mut findings = Vec::new();
    findings.extend(
        check_category_a_zero_overhead(specs)
            .into_iter()
            .map(|finding| AdmissionFinding::new(finding.op_id(), 9, finding.to_string())),
    );
    findings.extend(
        check_category_c_intrinsic(specs)
            .into_iter()
            .map(|finding| AdmissionFinding::new(finding.op_id(), 9, finding.to_string())),
    );
    findings.extend(
        check_category_b_tripwire(vyre_src_root)
            .into_iter()
            .map(|finding| AdmissionFinding::new(finding.op_id(), 9, finding.to_string())),
    );
    findings
}

fn gate_4_witness_cap(spec: &OpSpec) -> usize {
    spec.admission_witness_cap.unwrap_or({
        if matches!(spec.category, Category::A { .. }) {
            u32::MAX as usize
        } else {
            GATE_4_DEFAULT_MAX_GENERATED_INPUTS
        }
    })
}

fn check_gate_4_deterministic_semantics(specs: &[OpSpec]) -> Vec<AdmissionFinding> {
    let generators = default_generators();
    let mut findings = Vec::new();

    for spec in specs {
        let cap = gate_4_witness_cap(spec);
        let mut tested_inputs = 0usize;
        let mut capped = false;

        for seed in DETERMINISM_SEEDS {
            if capped {
                break;
            }
            for generator in &generators {
                if tested_inputs >= cap {
                    capped = true;
                    break;
                }
                generator.generate_for_op_streaming(
                    spec.id,
                    &spec.signature,
                    *seed,
                    &mut |label, input| {
                        if tested_inputs >= cap {
                            capped = true;
                            return;
                        }
                        tested_inputs += 1;

                        let first = (spec.cpu_fn)(&input);
                        let second = (spec.cpu_fn)(&input);
                        if first != second {
                            findings.push(AdmissionFinding::new(
                                spec.id,
                                4,
                                format!(
                                    "CPU reference is nondeterministic on witness {label}. Fix: define strict deterministic semantics."
                                ),
                            ));
                            return;
                        }

                        // Thread-local determinism stub (A6).
                        let thread_result = thread::scope(|s| {
                            s.spawn(|| (spec.cpu_fn)(&input)).join().expect("thread panicked")
                        });
                        if thread_result != first {
                            findings.push(AdmissionFinding::new(
                                spec.id,
                                4,
                                format!(
                                    "CPU reference differs across threads on witness {label}. Fix: remove thread-local or global mutable state."
                                ),
                            ));
                        }
                    },
                );
            }
        }

        if capped {
            findings.push(AdmissionFinding::new(
                spec.id,
                4,
                format!(
                    "generated more than {cap} deterministic witness inputs. Fix: bound TOML generator rules for this spec before admission."
                ),
            ));
            continue;
        }
        if tested_inputs == 0 {
            findings.push(AdmissionFinding::new(
                spec.id,
                4,
                "no deterministic witness inputs were generated. Fix: add a generator or TOML rule that produces at least one input for this signature.",
            ));
        }
    }

    findings
}

fn check_gate_5_cpu_reference(specs: &[OpSpec]) -> Vec<AdmissionFinding> {
    let generators = default_generators();
    let mut findings = Vec::new();

    for spec in specs {
        let mut total = 0usize;
        let mut non_empty = 0usize;

        for seed in DETERMINISM_SEEDS {
            for generator in &generators {
                generator.generate_for_op_streaming(
                    spec.id,
                    &spec.signature,
                    *seed,
                    &mut |_label, input| {
                        total += 1;
                        if !(spec.cpu_fn)(&input).is_empty() {
                            non_empty += 1;
                        }
                    },
                );
            }
        }

        if total == 0 {
            findings.push(AdmissionFinding::new(
                spec.id,
                5,
                "no witnesses were generated. Fix: add a generator or TOML rule that produces at least one input for this signature.",
            ));
            continue;
        }

        let ratio = non_empty as f64 / total as f64;
        let has_declared_oracle = matches!(
            spec.oracle_override,
            Some(OracleKind::SpecTable)
                | Some(OracleKind::External)
                | Some(OracleKind::Law)
                | Some(OracleKind::Composition)
        );

        if has_declared_oracle {
            if ratio < 0.8 {
                findings.push(AdmissionFinding::new(
                    spec.id,
                    5,
                    format!(
                        "only {:.1}% of generated witnesses produced non-empty output against the declared oracle (need >= 80%). Fix: ensure the oracle covers the input space or tighten generators.",
                        ratio * 100.0
                    ),
                ));
            }
            continue;
        }

        // No declared oracle: require a fingerprint match.
        if let Some(expected) = spec.cpu_fingerprint {
            let actual = cpu_fn_fingerprint(spec.cpu_fn, spec.signature.inputs.len() >= 2);
            if actual != expected {
                findings.push(AdmissionFinding::new(
                    spec.id,
                    5,
                    format!(
                        "CPU fingerprint mismatch: expected 0x{expected:016X}, got 0x{actual:016X}. Fix: update the fingerprint or the CPU reference function.",
                    ),
                ));
            }
        } else {
            findings.push(AdmissionFinding::new(
                spec.id,
                5,
                "no oracle declared and no cpu_fingerprint provided. Fix: declare an oracle (SpecTable, External, Law, or Composition) or provide a cpu_fingerprint.",
            ));
        }
    }

    findings
}

fn check_gate_6_conformance_rules(specs: &[OpSpec]) -> Vec<AdmissionFinding> {
    specs
        .iter()
        .filter(|spec| spec.laws.is_empty() && spec.no_algebraic_laws_reason.is_none())
        .map(|spec| {
            AdmissionFinding::new(
                spec.id,
                6,
                "declares no algebraic laws and provides no no_algebraic_laws_reason. Fix: declare verifiable conformance laws or document why none apply.",
            )
        })
        .collect()
}

/// Compute a deterministic hash of a CPU function on a canonical input set.
fn cpu_fn_fingerprint(cpu_fn: fn(&[u8]) -> Vec<u8>, is_binary: bool) -> u64 {
    let mut hash: u64 = 0xcbf29ce484222325; // FNV-1a offset basis
    let inputs: Vec<Vec<u8>> = if is_binary {
        vec![
            vec![0, 0, 0, 0, 0, 0, 0, 0],
            vec![0xFF, 0xFF, 0xFF, 0xFF, 0x01, 0x00, 0x00, 0x00],
            vec![0xDE, 0xAD, 0xBE, 0xEF, 0xCA, 0xFE, 0xBA, 0xBE],
        ]
    } else {
        vec![
            vec![0, 0, 0, 0],
            vec![0xFF, 0xFF, 0xFF, 0xFF],
            vec![0xDE, 0xAD, 0xBE, 0xEF],
        ]
    };
    for input in &inputs {
        let output = cpu_fn(input);
        for byte in &output {
            hash ^= u64::from(*byte);
            hash = hash.wrapping_mul(0x100000001b3); // FNV prime
        }
    }
    hash
}

/// Registry entry for `admission` enforcement.
pub struct AdmissionEnforcer;

impl crate::enforce::EnforceGate for AdmissionEnforcer {
    fn id(&self) -> &'static str {
        "admission"
    }

    fn name(&self) -> &'static str {
        "admission"
    }

    fn run(&self, ctx: &crate::enforce::EnforceCtx<'_>) -> Vec<crate::enforce::Finding> {
        let findings = check_admission(ctx.specs, &ctx.workspace_root.join("core/src"));
        let messages = findings
            .into_iter()
            .map(|finding| finding.to_string())
            .collect::<Vec<_>>();
        crate::enforce::finding_result(self.id(), messages)
    }
}

/// Auto-registered `admission` enforcer.
pub const REGISTERED: AdmissionEnforcer = AdmissionEnforcer;

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

    use crate::spec::types::conform::Strictness;
    use crate::spec::types::{DataType, OpSignature};

    fn dummy_cpu(_input: &[u8]) -> Vec<u8> {
        vec![1, 2, 3]
    }

    fn dummy_wgsl() -> String {
        String::new()
    }

    fn dummy_spec(id: &'static str) -> OpSpec {
        OpSpec::builder(id)
            .signature(OpSignature {
                inputs: vec![DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(dummy_cpu)
            .wgsl_fn(dummy_wgsl)
            .category(Category::A {
                composition_of: vec![id],
            })
            .laws(vec![])
            .strictness(Strictness::Strict)
            .version(1)
            .build()
            .expect("valid spec")
    }

    #[test]
    fn gate_6_fails_when_laws_empty_and_no_reason() {
        let spec = dummy_spec("test.op");
        let findings = check_gate_6_conformance_rules(&[spec]);
        assert_eq!(findings.len(), 1);
        assert_eq!(findings[0].gate, 6);
    }

    #[test]
    fn gate_6_passes_when_laws_present() {
        let mut spec = dummy_spec("test.op");
        spec.laws = vec![crate::spec::law::AlgebraicLaw::Commutative];
        let findings = check_gate_6_conformance_rules(&[spec]);
        assert!(findings.is_empty());
    }

    #[test]
    fn gate_6_passes_when_reason_present() {
        let mut spec = dummy_spec("test.op");
        spec.no_algebraic_laws_reason = Some("laws are verified by external proof");
        let findings = check_gate_6_conformance_rules(&[spec]);
        assert!(findings.is_empty());
    }

    #[test]
    fn gate_4_cap_defaults_to_10k_for_non_a() {
        let mut spec = dummy_spec("test.op");
        spec.category = Category::C {
            hardware: "test.intrinsic",
            backend_availability: |_| true,
        };
        assert_eq!(gate_4_witness_cap(&spec), 10_000);
    }

    #[test]
    fn gate_4_cap_defaults_to_exhaustive_for_a() {
        let spec = dummy_spec("test.op");
        assert_eq!(gate_4_witness_cap(&spec), u32::MAX as usize);
    }

    #[test]
    fn gate_4_cap_respects_spec_override() {
        let mut spec = dummy_spec("test.op");
        spec.admission_witness_cap = Some(500);
        assert_eq!(gate_4_witness_cap(&spec), 500);
    }

    #[test]
    fn fingerprint_is_deterministic() {
        let a = cpu_fn_fingerprint(dummy_cpu, false);
        let b = cpu_fn_fingerprint(dummy_cpu, false);
        assert_eq!(a, b);
    }
}