weirflow 0.1.0

GPU-first dataflow analysis primitives for Vyre and Santh compiler pipelines.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

//! Property-based gates for `weir::oracle::summary::range_check`.
//!
//! Op id: `weir::tests::df::property::range_check`. Soundness:
//! `Exact`  -  bit n set iff `interval_hi[n] < bound[n]`. Properties
//! exercised: per-element correctness across 1024 random vectors,
//! truncation to the shorter input, all-zero behavior on bound=0,
//! and the totality property (every output bit is 0 or 1).

use proptest::prelude::*;
use weir::oracle::summary::range_check as cpu_ref;

proptest! {
    #![proptest_config(ProptestConfig::with_cases(10_000))]

    /// Element-wise predicate: out[i] = 1 iff hi[i] < bound[i].
    #[test]
    fn elementwise_strict_less_than(
        hi in proptest::collection::vec(any::<u32>(), 0..32),
        bnd in proptest::collection::vec(any::<u32>(), 0..32),
    ) {
        let out = cpu_ref(&hi, &bnd);
        let n = hi.len().min(bnd.len());
        prop_assert_eq!(out.len(), n);
        for i in 0..n {
            let expected = u32::from(hi[i] < bnd[i]);
            prop_assert_eq!(out[i], expected, "i={}: hi={} bnd={}", i, hi[i], bnd[i]);
        }
    }

    /// Output truncates to the shorter input.
    #[test]
    fn truncates_to_shorter_input(
        hi in proptest::collection::vec(any::<u32>(), 0..16),
        bnd in proptest::collection::vec(any::<u32>(), 0..16),
    ) {
        let out = cpu_ref(&hi, &bnd);
        prop_assert!(out.len() <= hi.len());
        prop_assert!(out.len() <= bnd.len());
        prop_assert_eq!(out.len(), hi.len().min(bnd.len()));
    }

    /// `bound == 0` makes the output all zeros  -  nothing is < 0 in u32.
    #[test]
    fn zero_bound_yields_all_zero(
        hi in proptest::collection::vec(any::<u32>(), 1..32),
    ) {
        let zero = vec![0u32; hi.len()];
        let out = cpu_ref(&hi, &zero);
        prop_assert!(out.iter().all(|&w| w == 0));
    }

    /// `hi[i] == 0 && bound[i] > 0` always sets bit i.
    #[test]
    fn zero_hi_with_positive_bound_yields_one(
        bnd in proptest::collection::vec(1u32..u32::MAX, 1..16),
    ) {
        let zero = vec![0u32; bnd.len()];
        let out = cpu_ref(&zero, &bnd);
        prop_assert!(out.iter().all(|&w| w == 1));
    }

    /// Output is a 0/1 indicator  -  no other values appear.
    #[test]
    fn output_is_bool_indicator(
        hi in proptest::collection::vec(any::<u32>(), 0..32),
        bnd in proptest::collection::vec(any::<u32>(), 0..32),
    ) {
        let out = cpu_ref(&hi, &bnd);
        for &w in &out {
            prop_assert!(w == 0 || w == 1, "non-boolean output: {}", w);
        }
    }
}