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

//! Property-based gates for the bitset-AND-style reference oracles.
//!
//! Op id: `weir::tests::df::property::bitset_oracles`. Soundness:
//! `Exact`  -  these primitives compute pure word-wise AND of two
//! input bitsets, so the oracle output is fully determined by the
//! inputs. Proptest generates 1000+ random word vectors and asserts
//! the AND identity, idempotence, commutativity, and intersection
//! with the empty set.

use proptest::prelude::*;

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

    /// `weir::oracle::bitset::must_init(a, b)` is word-wise AND of `a` and `b`.
    #[test]
    fn must_init_is_word_wise_and(
        a in proptest::collection::vec(any::<u32>(), 0..16),
        b in proptest::collection::vec(any::<u32>(), 0..16),
    ) {
        let out = weir::oracle::bitset::must_init(&a, &b);
        let n = a.len().min(b.len());
        prop_assert_eq!(out.len(), n);
        for i in 0..n {
            prop_assert_eq!(out[i], a[i] & b[i]);
        }
    }

    /// AND with an all-zero set is all-zero.
    #[test]
    fn scc_query_with_zero_query_yields_zero(
        same_scc in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        let zero = vec![0u32; same_scc.len()];
        let out = weir::oracle::bitset::scc_query(&same_scc, &zero);
        prop_assert!(out.iter().all(|w| *w == 0));
    }

    /// AND with all-ones returns the original (truncated to the shorter input).
    #[test]
    fn live_at_with_all_ones_query_returns_original(
        live in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        let ones = vec![u32::MAX; live.len()];
        let out = weir::oracle::bitset::live_at(&live, &ones);
        prop_assert_eq!(out, live);
    }

    /// Word-wise AND is commutative.
    #[test]
    fn post_dominates_is_commutative(
        a in proptest::collection::vec(any::<u32>(), 1..8),
        b in proptest::collection::vec(any::<u32>(), 1..8),
    ) {
        let ab = weir::oracle::bitset::post_dominates(&a, &b);
        let ba = weir::oracle::bitset::post_dominates(&b, &a);
        prop_assert_eq!(ab, ba);
    }

    /// Word-wise AND is idempotent on equal inputs.
    #[test]
    fn must_init_idempotent_on_self(
        a in proptest::collection::vec(any::<u32>(), 0..16),
    ) {
        let out = weir::oracle::bitset::must_init(&a, &a);
        prop_assert_eq!(out, a);
    }
}