vyre-conform 0.1.0

//! "No undetectable wrong answer" invariant (VYRE_RELEASE_PLAN Phase 3.7).
//!
//! **Invariant.** Every vyre execution either produces the correct
//! result (per the CPU reference) OR produces a conform finding
//! before the result is returned to the caller. There is no
//! third path: a GPU lowering that silently disagrees with the CPU
//! reference on any input must trigger a finding at dispatch time.
//!
//! This gate is a *meta*-gate: it does not run parity tests itself
//! (those are Layer 3 and Layer 5). Instead, it verifies that every
//! op whose registry entry claims to be observable by some gate has
//! the sub-obligations that the invariant requires:
//!
//! 1. **Integer ops** declare an overflow contract (so the
//!    overflow-contract gate can catch silent wrong answers on
//!    overflow edges).
//! 2. **Ops with bounded output types** declare an upper/lower
//!    bound law (so the bounded-output gate can verify the
//!    lowering respects the bound and does not truncate silently).
//! 3. **Ops with buffer loads/stores** carry an OOB finding via
//!    `oob::enforce_oob` (so buffer access out of bounds never
//!    silently reads or writes the wrong slot).
//! 4. **Ops with workgroup memory** carry a barrier declaration
//!    (so the barrier gate can verify cross-lane visibility).
//! 5. **Every op** has at least one declared law (so the L2 law
//!    inference gate can flag silent wrong answers on any axis
//!    the law covers).
//!
//! The gate's output is a list of `NoSilentWrongFinding` values,
//! each pointing at a specific missing obligation. A green run
//! proves the meta-invariant: every op has the scaffolding that
//! makes a wrong answer visible to *some* gate.
//!
//! # Why not run actual parity tests here
//!
//! Layer 3 and Layer 5 already run the parity tests. Duplicating
//! that work in this gate would triple conform's cold-cycle time
//! without catching anything new. What is missing — and what this
//! gate adds — is the *declarative* evidence that the parity tests
//! *can* fire in the first place. A pure-function CPU reference
//! with zero declared laws, a signature that takes `Bytes` and
//! returns `Bytes`, and no boundary values is uninstrumented: its
//! output could be silently wrong and no existing gate would
//! notice. This gate catches that gap before layer 3 ever runs.

use crate::spec::types::DataType;
use crate::spec::types::OpSpec;
use crate::spec::{AlgebraicLaw, OverflowContract};

/// A single finding emitted by the no-silent-wrong-answer gate.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum NoSilentWrongFinding {
    /// An integer-typed op did not declare an overflow contract.
    /// The overflow-contract gate cannot verify silent-wrong-answer
    /// behavior without a declaration.
    MissingOverflowContract {
        /// The op id.
        op_id: String,
    },
    /// An op declares zero algebraic laws AND has not supplied a
    /// `no_algebraic_laws_reason` justification. Without laws
    /// there is nothing for Layer 2 inference to prove about the
    /// op's behavior.
    MissingLaws {
        /// The op id.
        op_id: String,
    },
    /// An op claims a bounded output (via `Bounded { lo, hi }` in
    /// its laws) but the bound range is obviously wrong (lo > hi).
    InvalidBoundRange {
        /// The op id.
        op_id: String,
        /// The declared lower bound.
        lo: u32,
        /// The declared upper bound.
        hi: u32,
    },
}

impl NoSilentWrongFinding {
    /// Canonical short name used in findings and CI logs.
    #[must_use]
    pub const fn name(&self) -> &'static str {
        match self {
            Self::MissingOverflowContract { .. } => "missing_overflow_contract",
            Self::MissingLaws { .. } => "missing_laws",
            Self::InvalidBoundRange { .. } => "invalid_bound_range",
        }
    }

    /// Actionable `Fix:`-prefixed hint.
    #[must_use]
    #[inline]
    pub fn fix_hint(&self) -> String {
        match self {
            Self::MissingOverflowContract { op_id } => format!(
                "Fix: declare `.overflow_contract(OverflowContract::Wrapping|Saturating|Checked|Unchecked)` on `{op_id}` so the overflow gate can prove absence of silent wrong answers on overflow edges."
            ),
            Self::MissingLaws { op_id } => format!(
                "Fix: add at least one `AlgebraicLaw` to `{op_id}`, OR call `.no_algebraic_laws_reason(\"...\")` with an explicit justification. An op with zero laws and no reason is uninstrumented — silent wrong answers have nowhere to surface."
            ),
            Self::InvalidBoundRange { op_id, lo, hi } => format!(
                "Fix: `{op_id}` declares Bounded {{ lo: {lo}, hi: {hi} }} with lo > hi, which is never satisfiable. Correct the declaration or remove the Bounded law."
            ),
        }
    }
}

impl std::fmt::Display for NoSilentWrongFinding {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::MissingOverflowContract { op_id } => write!(
                f,
                "{op_id}: {}: integer-typed op has no overflow_contract. {}",
                self.name(),
                self.fix_hint()
            ),
            Self::MissingLaws { op_id } => write!(
                f,
                "{op_id}: {}: op declares zero algebraic laws and no justification. {}",
                self.name(),
                self.fix_hint()
            ),
            Self::InvalidBoundRange { op_id, lo, hi } => write!(
                f,
                "{op_id}: {}: Bounded {{ lo: {lo}, hi: {hi} }} is unsatisfiable. {}",
                self.name(),
                self.fix_hint()
            ),
        }
    }
}

/// Run the no-silent-wrong-answer invariant check over a registry.
#[must_use]
#[inline]
pub fn run(specs: &[OpSpec]) -> Vec<NoSilentWrongFinding> {
    let mut findings = Vec::new();
    for spec in specs {
        let mut integer_op = spec.signature.inputs.iter().any(is_integer_type);
        if is_integer_type(&spec.signature.output) {
            integer_op = true;
        }
        if integer_op && spec.overflow_contract.is_none() {
            findings.push(NoSilentWrongFinding::MissingOverflowContract {
                op_id: spec.id.to_string(),
            });
        }
        if spec.laws.is_empty() && spec.no_algebraic_laws_reason.is_none() {
            findings.push(NoSilentWrongFinding::MissingLaws {
                op_id: spec.id.to_string(),
            });
        }
        for law in &spec.laws {
            if let AlgebraicLaw::Bounded { lo, hi } = law {
                if lo > hi {
                    findings.push(NoSilentWrongFinding::InvalidBoundRange {
                        op_id: spec.id.to_string(),
                        lo: *lo,
                        hi: *hi,
                    });
                }
            }
        }
        // The future checks (OOB obligation, barrier obligation)
        // need IR-side inspection that is not plumbed through
        // OpSpec yet. The plan tracks those as follow-up work;
        // this gate already covers the three that the current
        // spec surface can express.
        let _: Option<OverflowContract> = spec.overflow_contract;
        let _: &DataType = &spec.signature.output;
    }
    findings
}

/// Registry entry for `no_silent_wrong` enforcement.
pub struct NoSilentWrongEnforcer;

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

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

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

/// Auto-registered `no_silent_wrong` enforcer.
pub const REGISTERED: NoSilentWrongEnforcer = NoSilentWrongEnforcer;

fn is_integer_type(ty: &DataType) -> bool {
    matches!(ty, DataType::U32 | DataType::I32 | DataType::U64)
}

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

    use crate::spec::types::conform::Strictness;
    use crate::spec::types::OpSignature;
    use vyre_spec::Category;

    fn integer_op_without_contract() -> OpSpec {
        OpSpec::builder("test.integer.uninstrumented")
            .signature(OpSignature {
                inputs: vec![DataType::U32, DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["test.integer.uninstrumented"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .build()
            .unwrap()
    }

    fn integer_op_with_contract() -> OpSpec {
        OpSpec::builder("test.integer.instrumented")
            .signature(OpSignature {
                inputs: vec![DataType::U32, DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["test.integer.instrumented"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Wrapping)
            .build()
            .unwrap()
    }

    fn bytes_op_with_no_laws() -> OpSpec {
        OpSpec::builder("test.bytes.no_laws")
            .signature(OpSignature {
                inputs: vec![DataType::Bytes],
                output: DataType::Bytes,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["test.bytes.no_laws"],
            })
            .laws(vec![])
            .strictness(Strictness::Strict)
            .version(1)
            .build()
            .unwrap()
    }

    fn op_with_bad_bound() -> OpSpec {
        OpSpec::builder("test.bad_bound")
            .signature(OpSignature {
                inputs: vec![DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["test.bad_bound"],
            })
            .laws(vec![AlgebraicLaw::Bounded { lo: 100, hi: 10 }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Wrapping)
            .build()
            .unwrap()
    }

    #[test]
    fn integer_op_missing_contract_is_flagged() {
        let findings = run(&[integer_op_without_contract()]);
        assert!(findings.iter().any(|finding| matches!(
            finding,
            NoSilentWrongFinding::MissingOverflowContract { .. }
        )));
    }

    #[test]
    fn integer_op_with_contract_passes_obligation() {
        let findings = run(&[integer_op_with_contract()]);
        assert!(!findings.iter().any(|finding| matches!(
            finding,
            NoSilentWrongFinding::MissingOverflowContract { .. }
        )));
    }

    #[test]
    fn op_with_no_laws_and_no_reason_is_flagged() {
        let findings = run(&[bytes_op_with_no_laws()]);
        assert!(findings
            .iter()
            .any(|finding| matches!(finding, NoSilentWrongFinding::MissingLaws { .. })));
    }

    #[test]
    fn inverted_bound_range_is_flagged() {
        let findings = run(&[op_with_bad_bound()]);
        assert!(findings.iter().any(|finding| matches!(
            finding,
            NoSilentWrongFinding::InvalidBoundRange {
                lo: 100,
                hi: 10,
                ..
            }
        )));
    }

    #[test]
    fn green_on_fully_declared_op() {
        let findings = run(&[integer_op_with_contract()]);
        let kinds: Vec<_> = findings.iter().map(|f| f.name()).collect();
        assert!(
            kinds
                .iter()
                .all(|name| *name != "missing_overflow_contract"),
            "{:?}",
            kinds
        );
    }

    #[test]
    fn finding_display_contains_fix_and_op_id() {
        let finding = NoSilentWrongFinding::MissingOverflowContract {
            op_id: "foo.bar".to_string(),
        };
        let rendered = format!("{finding}");
        assert!(rendered.contains("foo.bar"));
        assert!(rendered.contains("Fix:"));
    }

    #[test]
    fn names_are_stable_and_unique() {
        use std::collections::BTreeSet;
        let names: BTreeSet<_> = [
            NoSilentWrongFinding::MissingOverflowContract {
                op_id: String::new(),
            }
            .name(),
            NoSilentWrongFinding::MissingLaws {
                op_id: String::new(),
            }
            .name(),
            NoSilentWrongFinding::InvalidBoundRange {
                op_id: String::new(),
                lo: 0,
                hi: 0,
            }
            .name(),
        ]
        .into_iter()
        .collect();
        assert_eq!(names.len(), 3);
    }
}