vyre-conform 0.1.0

//! Integer overflow contract gate — VYRE_RELEASE_PLAN Phase 3.6.
//!
//! Every op whose signature touches an integer type must declare one
//! of the four [`crate::spec::OverflowContract`] variants on its
//! `OpSpec`. The gate:
//!
//! 1. Walks each op in the registry.
//! 2. Classifies the op as **integer-typed** iff at least one of its
//!    inputs or its output is `DataType::U32`, `DataType::I32`, or
//!    `DataType::U64`.
//! 3. For every integer-typed op that has not declared a contract,
//!    emits [`OverflowFinding::MissingContract`] pointing at the op
//!    id with a `Fix:` hint.
//! 4. For every integer-typed op that *has* declared a contract,
//!    probes the CPU reference at the canonical edges for the
//!    declared contract and emits [`OverflowFinding::ContractViolation`]
//!    when the observed behavior does not match the declaration.
//!
//! The edge probes are deliberately simple: they cover
//! `(MAX, 1)`, `(MIN, -1)`, `(0, 0)`, and `(1, MAX)` for binary
//! ops and `(MAX)`, `(MIN)`, `(0)` for unary ops. A real op that
//! declares `Wrapping` but saturates at `MAX` will have its
//! (`MAX`, `1`) probe return `u32::MAX` instead of `0` and the gate
//! will catch it. Exact probe inputs are intentionally modest so the
//! gate finishes in milliseconds even on a thousand-op registry.
//!
//! # What this gate intentionally does NOT do
//!
//! - It does not verify the WGSL lowering separately. The lowering
//!   runs through the full conformance harness under the normal
//!   CPU parity check. This gate is a *contract declaration*
//!   sanity pass — "did the author lie about whether this op
//!   wraps?" — not a byte-for-byte parity verifier.
//! - It does not try to infer the correct contract. The declaration
//!   is a load-bearing human commitment, not a derived attribute.
//!
//! # Why an `Option<OverflowContract>` rather than a required field
//!
//! Many ops do not operate on integers at all — string ops, byte
//! decoders, graph traversals. Forcing every op to declare an
//! overflow contract would be noise. The gate is integer-typed
//! specifically because non-integer ops cannot meaningfully have
//! overflow behavior to declare.

use crate::spec::types::DataType;
use crate::spec::types::OpSpec;
use crate::spec::OverflowContract;

/// A finding emitted by the overflow-contract gate.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum OverflowFinding {
    /// An integer-typed op did not declare an overflow contract on
    /// its `OpSpec`.
    MissingContract {
        /// The op id.
        op_id: String,
        /// Whether the op signature has U32/I32/U64 inputs, output,
        /// or both. Used to render the fix hint.
        carries_integer_input: bool,
        /// Whether the op signature names an integer output type.
        carries_integer_output: bool,
    },
    /// The op declared contract `declared` but the CPU reference
    /// behaved as `observed` on at least one of the canonical edge
    /// inputs.
    ContractViolation {
        /// The op id.
        op_id: String,
        /// The contract variant declared on the op spec.
        declared: OverflowContract,
        /// The observed behavior on the probe.
        observed_behavior: ObservedBehavior,
        /// Label of the probe input that caught the mismatch.
        probe_label: &'static str,
    },
}

/// Observed runtime behavior of a CPU reference on an overflow edge.
/// The gate compares this against the declaration and emits a
/// `ContractViolation` when they disagree.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ObservedBehavior {
    /// Output wrapped modulo the type width.
    Wrapped,
    /// Output saturated to the type min or max.
    Saturated,
    /// CPU reference produced an error / empty output (caller
    /// interpreted as "checked and rejected").
    Checked,
    /// CPU reference produced a value that does not match any of
    /// the three canonical behaviors. The gate treats this as a
    /// violation under every declared contract.
    Unrecognized,
}

impl ObservedBehavior {
    /// Short stable name.
    #[must_use]
    pub const fn name(self) -> &'static str {
        match self {
            Self::Wrapped => "wrapped",
            Self::Saturated => "saturated",
            Self::Checked => "checked",
            Self::Unrecognized => "unrecognized",
        }
    }

    /// Does this observation satisfy the given contract? `Unchecked`
    /// is permissive — by definition the op has no defined behavior
    /// outside its precondition, and the gate does not run probes
    /// against `Unchecked` ops.
    #[must_use]
    pub const fn satisfies(self, contract: OverflowContract) -> bool {
        matches!(
            (self, contract),
            (Self::Wrapped, OverflowContract::Wrapping)
                | (Self::Saturated, OverflowContract::Saturating)
                | (Self::Checked, OverflowContract::Checked)
                | (_, OverflowContract::Unchecked)
        )
    }
}

impl std::fmt::Display for OverflowFinding {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::MissingContract {
                op_id,
                carries_integer_input,
                carries_integer_output,
            } => write!(
                f,
                "{op_id}: missing overflow_contract. inputs={} output={}. \
                 Fix: add `.overflow_contract(OverflowContract::Wrapping|Saturating|Checked|Unchecked)` \
                 to the OpSpec builder.",
                carries_integer_input, carries_integer_output,
            ),
            Self::ContractViolation {
                op_id,
                declared,
                observed_behavior,
                probe_label,
            } => write!(
                f,
                "{op_id}: declared {declared}, observed {} on probe `{probe_label}`. \
                 Fix: either change the declared contract to match the \
                 CPU reference behavior, or change the CPU reference to \
                 match the declaration.",
                observed_behavior.name(),
            ),
        }
    }
}

/// Run the gate against a slice of ops.
#[must_use]
#[inline]
pub fn run(specs: &[OpSpec]) -> Vec<OverflowFinding> {
    let mut findings = Vec::new();
    for spec in specs {
        let integer_input = has_integer_type(&spec.signature.inputs);
        let integer_output = is_integer_type(&spec.signature.output);
        if !integer_input && !integer_output {
            continue;
        }
        let Some(declared) = spec.overflow_contract else {
            findings.push(OverflowFinding::MissingContract {
                op_id: spec.id.to_string(),
                carries_integer_input: integer_input,
                carries_integer_output: integer_output,
            });
            continue;
        };
        // Unchecked is a promise about the *caller*'s inputs. The
        // gate does not probe it because probing an unchecked op on
        // an overflow input deliberately falls outside the contract.
        if matches!(declared, OverflowContract::Unchecked) {
            continue;
        }
        findings.extend(probe(spec, declared));
    }
    findings
}

/// Return the list of `ContractViolation` findings for a single
/// integer-typed op at the canonical overflow-edge probes. The
/// probes are deliberately chosen so that a wrapping operation and
/// a saturating operation produce distinguishable outputs.
///
/// Only binary arity is probed — unary overflow edges depend on
/// the semantics of the operation (negate, wrapping_neg, abs, etc.)
/// and cannot be classified by a single output value. Unary ops
/// satisfy the gate by declaring a contract; their parity is
/// verified by the full conformance harness, not by this cheap
/// heuristic.
fn probe(spec: &OpSpec, declared: OverflowContract) -> Vec<OverflowFinding> {
    let mut findings = Vec::new();
    if spec.signature.inputs.len() != 2 {
        return findings;
    }
    // (MAX, 1) is the canonical overflow edge for addition-shaped
    // binary ops. Wrapping add → 0; saturating add → MAX.
    let mut input = Vec::with_capacity(8);
    input.extend_from_slice(&u32::MAX.to_le_bytes());
    input.extend_from_slice(&1u32.to_le_bytes());
    let output = (spec.cpu_fn)(&input);
    if output.len() != 4 {
        // The op's output width is not a single u32; probe cannot
        // classify it. Skip rather than emit a false positive.
        return findings;
    }
    let mut word = [0u8; 4];
    word.copy_from_slice(&output[..4]);
    let value = u32::from_le_bytes(word);
    let observed = match value {
        0 => ObservedBehavior::Wrapped,
        u32::MAX => ObservedBehavior::Saturated,
        // The op is not an addition-shaped binary. It may be xor,
        // and, mul, shl, or anything else. For those, the gate
        // cannot make a determination from a single (MAX, 1) probe
        // and silently accepts the declaration. The full
        // conformance harness handles the parity check.
        _ => return findings,
    };
    if !observed.satisfies(declared) {
        findings.push(OverflowFinding::ContractViolation {
            op_id: spec.id.to_string(),
            declared,
            observed_behavior: observed,
            probe_label: "max_plus_one",
        });
    }
    findings
}

fn has_integer_type(types: &[DataType]) -> bool {
    types.iter().any(is_integer_type)
}

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

/// Registry entry for `overflow_contract` enforcement.
pub struct OverflowContractEnforcer;

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

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

    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 `overflow_contract` enforcer.
pub const REGISTERED: OverflowContractEnforcer = OverflowContractEnforcer;

#[cfg(test)]
mod tests {
    use super::*;
    #[test]
    fn probe_missing_overflow_contracts() {
        let specs = crate::spec::op_registry::all_specs();
        let findings = run(&specs);
        let missing: Vec<_> = findings
            .iter()
            .filter(|f| matches!(f, OverflowFinding::MissingContract { .. }))
            .collect();
        for f in &missing {
            eprintln!("MISSING: {f:?}");
        }
        assert!(
            missing.is_empty(),
            "Fix: {} registered integer ops still lack an overflow contract",
            missing.len()
        );
    }

    use crate::spec::types::conform::Strictness;
    use crate::spec::types::OpSpec;
    use crate::spec::types::{DataType, OpSignature};
    use crate::spec::AlgebraicLaw;
    use vyre_spec::Category;

    fn base_builder(
        id: &'static str,
        inputs: Vec<DataType>,
        output: DataType,
        cpu: fn(&[u8]) -> Vec<u8>,
    ) -> OpSpec {
        OpSpec::builder(id)
            .signature(OpSignature { inputs, output })
            .cpu_fn(cpu)
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec![id],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .build()
            .unwrap()
    }

    fn wrapping_add_cpu(input: &[u8]) -> Vec<u8> {
        if input.len() < 8 {
            return Vec::new();
        }
        let a = u32::from_le_bytes(input[..4].try_into().unwrap());
        let b = u32::from_le_bytes(input[4..8].try_into().unwrap());
        a.wrapping_add(b).to_le_bytes().to_vec()
    }

    fn saturating_add_cpu(input: &[u8]) -> Vec<u8> {
        if input.len() < 8 {
            return Vec::new();
        }
        let a = u32::from_le_bytes(input[..4].try_into().unwrap());
        let b = u32::from_le_bytes(input[4..8].try_into().unwrap());
        a.saturating_add(b).to_le_bytes().to_vec()
    }

    fn non_integer_cpu(input: &[u8]) -> Vec<u8> {
        input.to_vec()
    }

    #[test]
    fn integer_op_with_no_contract_is_flagged() {
        let spec = base_builder(
            "test.integer.no_contract",
            vec![DataType::U32, DataType::U32],
            DataType::U32,
            wrapping_add_cpu,
        );
        let findings = run(&[spec]);
        assert!(
            findings
                .iter()
                .any(|finding| matches!(finding, OverflowFinding::MissingContract { op_id, .. } if op_id == "test.integer.no_contract")),
            "expected MissingContract: {findings:?}"
        );
    }

    #[test]
    fn non_integer_op_is_ignored_regardless_of_contract() {
        let spec = base_builder(
            "test.bytes.identity",
            vec![DataType::Bytes],
            DataType::Bytes,
            non_integer_cpu,
        );
        let findings = run(&[spec]);
        assert!(findings.is_empty(), "{findings:?}");
    }

    #[test]
    fn correctly_declared_wrapping_passes_probes() {
        let spec = OpSpec::builder("test.wrapping_add")
            .signature(OpSignature {
                inputs: vec![DataType::U32, DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(wrapping_add_cpu)
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["test.wrapping_add"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Wrapping)
            .build()
            .unwrap();
        let findings = run(&[spec]);
        assert!(
            findings.is_empty(),
            "wrapping contract + wrapping cpu_fn should be quiet: {findings:?}"
        );
    }

    #[test]
    fn correctly_declared_saturating_passes_probes() {
        let spec = OpSpec::builder("test.saturating_add")
            .signature(OpSignature {
                inputs: vec![DataType::U32, DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(saturating_add_cpu)
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["test.saturating_add"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Saturating)
            .build()
            .unwrap();
        let findings = run(&[spec]);
        assert!(
            findings.is_empty(),
            "saturating contract + saturating cpu_fn should be quiet: {findings:?}"
        );
    }

    #[test]
    fn declared_wrapping_but_cpu_saturates_fires_violation() {
        let spec = OpSpec::builder("test.liar")
            .signature(OpSignature {
                inputs: vec![DataType::U32, DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(saturating_add_cpu)
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["test.liar"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Wrapping)
            .build()
            .unwrap();
        let findings = run(&[spec]);
        assert!(
            findings.iter().any(|finding| matches!(
                finding,
                OverflowFinding::ContractViolation {
                    declared: OverflowContract::Wrapping,
                    ..
                }
            )),
            "saturating cpu_fn declared as Wrapping must violate: {findings:?}"
        );
    }

    #[test]
    fn unchecked_declaration_skips_probes() {
        // An Unchecked op whose cpu_fn *would* violate Wrapping
        // under probe must still pass the gate because the gate
        // doesn't probe Unchecked ops at all.
        let spec = OpSpec::builder("test.unchecked_add")
            .signature(OpSignature {
                inputs: vec![DataType::U32, DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(saturating_add_cpu)
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["test.unchecked_add"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Unchecked)
            .build()
            .unwrap();
        let findings = run(&[spec]);
        assert!(findings.is_empty(), "{findings:?}");
    }

    #[test]
    fn observed_behavior_satisfies_table() {
        for (observed, contract, expected) in [
            (ObservedBehavior::Wrapped, OverflowContract::Wrapping, true),
            (
                ObservedBehavior::Wrapped,
                OverflowContract::Saturating,
                false,
            ),
            (
                ObservedBehavior::Saturated,
                OverflowContract::Saturating,
                true,
            ),
            (
                ObservedBehavior::Saturated,
                OverflowContract::Wrapping,
                false,
            ),
            (ObservedBehavior::Checked, OverflowContract::Checked, true),
            (ObservedBehavior::Checked, OverflowContract::Wrapping, false),
            (ObservedBehavior::Wrapped, OverflowContract::Unchecked, true),
            (
                ObservedBehavior::Unrecognized,
                OverflowContract::Unchecked,
                true,
            ),
            (
                ObservedBehavior::Unrecognized,
                OverflowContract::Wrapping,
                false,
            ),
        ] {
            assert_eq!(
                observed.satisfies(contract),
                expected,
                "mismatch for {observed:?} vs {contract:?}"
            );
        }
    }

    #[test]
    fn display_finding_is_actionable() {
        let finding = OverflowFinding::MissingContract {
            op_id: "test.mystery".to_string(),
            carries_integer_input: true,
            carries_integer_output: true,
        };
        let rendered = format!("{finding}");
        assert!(rendered.contains("test.mystery"), "{rendered}");
        assert!(rendered.contains("Fix:"), "{rendered}");
        assert!(rendered.contains("overflow_contract"), "{rendered}");
    }
}