weir/
range_check.rs

1//! `range_check`  -  interval-VSA bound check. Composes the per-node
2//! interval table with a comparison against a known bound.
3//!
4//! Per node `n`, write 1 to `out[n]` iff `interval(n).hi < bound[n]`.
5//! Dataflow consumers use this for CWE-787 / CWE-190 to assert "size is
6//! bounded by destination buffer length."
7
8use std::sync::Arc;
9use vyre::ir::Program;
10use vyre_foundation::ir::model::expr::Ident;
11use vyre_foundation::ir::{BufferAccess, BufferDecl, DataType, Expr, Node};
12
13pub(crate) const OP_ID: &str = "weir::range_check";
14
15/// Build a range-check Program. Inputs:
16/// - `interval_hi`: per-node u32 buffer of interval upper bounds.
17/// - `bound`:       per-node u32 buffer of allowed maxima.
18/// - `out`:         per-node bitset; bit `n` set iff `interval_hi[n] < bound[n]`.
19#[must_use]
20pub fn range_check(node_count: u32, interval_hi: &str, bound: &str, out: &str) -> Program {
21    let domain = crate::graph_layout::LinearDomain::new(node_count);
22    let t = Expr::InvocationId { axis: 0 };
23    let body = vec![Node::store(
24        out,
25        t.clone(),
26        Expr::select(
27            Expr::lt(
28                Expr::load(interval_hi, t.clone()),
29                Expr::load(bound, t.clone()),
30            ),
31            Expr::u32(1),
32            Expr::u32(0),
33        ),
34    )];
35    Program::wrapped(
36        vec![
37            BufferDecl::storage(interval_hi, 0, BufferAccess::ReadOnly, DataType::U32)
38                .with_count(domain.element_count()),
39            BufferDecl::storage(bound, 1, BufferAccess::ReadOnly, DataType::U32)
40                .with_count(domain.element_count()),
41            BufferDecl::storage(out, 2, BufferAccess::ReadWrite, DataType::U32)
42                .with_count(domain.element_count()),
43        ],
44        [256, 1, 1],
45        vec![Node::Region {
46            generator: Ident::from(OP_ID),
47            source_region: None,
48            body: Arc::new(vec![Node::if_then(
49                Expr::lt(t.clone(), Expr::u32(node_count)),
50                body,
51            )]),
52        }],
53    )
54}
55
56/// reference oracle.
57#[must_use]
58#[cfg(any(test, feature = "cpu-parity"))]
59#[deprecated(
60    note = "reference oracle only; production code must dispatch the Weir Program on a concrete GPU backend or use weir::oracle for parity evidence"
61)]
62pub(crate) fn cpu_ref(interval_hi: &[u32], bound: &[u32]) -> Vec<u32> {
63    let n = interval_hi.len().min(bound.len());
64    let mut out = crate::staging_reserve::reserved_vec(n, "range-check CPU oracle output")
65        .unwrap_or_else(|error| {
66            panic!("range-check CPU oracle output reservation failed: {error}")
67        });
68    out.extend((0..n).map(|i| u32::from(interval_hi[i] < bound[i])));
69    out
70}
71
72/// Soundness marker for [`range_check`].
73#[derive(Clone, Copy, Debug, PartialEq, Eq)]
74pub struct RangeCheck;
75impl super::soundness::SoundnessTagged for RangeCheck {
76    fn soundness(&self) -> super::soundness::Soundness {
77        super::soundness::Soundness::Exact
78    }
79}
80
81inventory::submit! {
82    vyre_harness::OpEntry::new(
83        OP_ID,
84        || range_check(4, "hi", "bound", "out"),
85        Some(|| {
86            let u32s = crate::dispatch_decode::pack_u32;
87            vec![vec![
88                u32s(&[5, 10, 11, 0]),
89                u32s(&[6, 10, 9, 1]),
90                u32s(&[0; 4]),
91            ]]
92        }),
93        Some(|| {
94            let u32s = crate::dispatch_decode::pack_u32;
95            vec![vec![u32s(&[1, 0, 0, 1])]]
96        }),
97    )
98}
99
100#[cfg(test)]
101#[allow(deprecated)]
102mod tests {
103    use super::*;
104
105    #[test]
106    fn within_bound_returns_one() {
107        assert_eq!(cpu_ref(&[5, 10, 15], &[10, 20, 30]), vec![1, 1, 1]);
108    }
109
110    #[test]
111    fn at_bound_returns_zero() {
112        assert_eq!(cpu_ref(&[10, 20], &[10, 20]), vec![0, 0]);
113    }
114
115    #[test]
116    fn over_bound_returns_zero() {
117        assert_eq!(cpu_ref(&[100], &[10]), vec![0]);
118    }
119
120    #[test]
121    fn mixed_bounds() {
122        assert_eq!(cpu_ref(&[1, 100, 5], &[10, 10, 100]), vec![1, 0, 1]);
123    }
124}
weir/range_check.rs

weir/
range_check.rs
