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

//! Property-based gates for `weir::oracle::bitset::value_set`.
//!
//! Op id: `weir::tests::df::property::value_set`. Soundness:
//! `MayOver`  -  value_set is the constant-set query reduction over
//! a host-supplied bitset. Properties exercised: subset of both
//! inputs, commutativity, identity element (all-ones), and
//! absorption (zero).

use proptest::prelude::*;
use weir::oracle::bitset::value_set as cpu_ref;

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

    /// Output is subset of both inputs (per-word).
    #[test]
    fn output_is_subset_of_inputs(
        consts in proptest::collection::vec(any::<u32>(), 1..16),
        query in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        let out = cpu_ref(&consts, &query);
        let n = consts.len().min(query.len());
        for i in 0..n {
            prop_assert_eq!(out[i] & consts[i], out[i]);
            prop_assert_eq!(out[i] & query[i], out[i]);
        }
    }

    /// Operator is commutative.
    #[test]
    fn cpu_ref_is_commutative(
        a in proptest::collection::vec(any::<u32>(), 1..16),
        b in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        prop_assert_eq!(cpu_ref(&a, &b), cpu_ref(&b, &a));
    }

    /// AND with all-ones is identity.
    #[test]
    fn and_with_all_ones_is_identity(
        a in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        let ones = vec![u32::MAX; a.len()];
        prop_assert_eq!(cpu_ref(&a, &ones), a);
    }

    /// AND with zero is zero.
    #[test]
    fn and_with_zero_is_zero(
        a in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        let zero = vec![0u32; a.len()];
        let out = cpu_ref(&a, &zero);
        prop_assert!(out.iter().all(|&w| w == 0));
    }

    /// AND is idempotent on equal inputs.
    #[test]
    fn cpu_ref_is_idempotent(
        a in proptest::collection::vec(any::<u32>(), 0..16),
    ) {
        prop_assert_eq!(cpu_ref(&a, &a), a);
    }
}