Skip to main content

vyre_primitives/fixpoint/
bitset_fixpoint.rs

1//! `bitset_fixpoint`  -  deterministic transitive closure.
2//!
3//! Layout:
4//! - `current` (ReadOnly): the dispatch-start snapshot bitset.
5//! - `next` (ReadWrite): where this pass writes its output.
6//! - `changed` (ReadWrite, 1 word): set to 1 iff `next[w] !=
7//!   current[w]` for any word `w`.
8//!
9//! One dispatch is one fixpoint step. The driver zeros `changed`
10//! before each dispatch, copies `next` into `current` after, and
11//! terminates when `changed[0]` reads 0 or `max_iterations` is hit.
12//!
13//! This primitive is intentionally simple: the actual transfer
14//! function lives in the caller's composition (e.g.
15//! `csr_forward_traverse(current) → scratch; bitset_or(current,
16//! scratch) → next`). `bitset_fixpoint` only handles the
17//! comparison + changed-flag half of the driver loop so every taint
18//! rule can reuse the same convergence semantics.
19
20use std::sync::Arc;
21
22use vyre_foundation::ir::model::expr::Ident;
23use vyre_foundation::ir::{BufferAccess, BufferDecl, DataType, Expr, Node, Program};
24
25/// Canonical op id.
26pub const OP_ID: &str = "vyre-primitives::fixpoint::bitset_fixpoint";
27
28/// Canonical changed-flag buffer for callers that drive this primitive to a
29/// fixpoint through an owner-defined typed loop.
30pub const NAME_CHANGED_FLAG: &str = "fp_changed";
31
32/// Build a Program: for every word `w`, set `changed[0] = 1`
33/// atomically iff `current[w] != next[w]`.
34///
35/// The caller's own transfer body (csr traversal + bitset_or or
36/// whatever the rule composes) must run and write into `next`
37/// *before* the fixpoint Program is dispatched. A typical driver
38/// loop is:
39///
40/// ```text
41///   loop iteration:
42///     dispatch(transfer_body, current, next)
43///     dispatch(bitset_fixpoint, current, next, changed)
44///     if changed[0] == 0: break
45///     swap current/next
46///     zero changed[0]
47/// ```
48///
49/// Shipping the compare-and-flag half here means every fixpoint rule
50/// consumes the identical convergence semantics without re-
51/// implementing the pattern.
52#[must_use]
53pub fn bitset_fixpoint(current: &str, next: &str, changed: &str, words: u32) -> Program {
54    let t = Expr::InvocationId { axis: 0 };
55    let body = vec![
56        Node::let_bind("c", Expr::load(current, t.clone())),
57        Node::let_bind("n", Expr::load(next, t.clone())),
58        Node::if_then(
59            Expr::ne(Expr::var("c"), Expr::var("n")),
60            vec![Node::let_bind(
61                "_",
62                Expr::atomic_or(changed, Expr::u32(0), Expr::u32(1)),
63            )],
64        ),
65    ];
66    Program::wrapped(
67        vec![
68            BufferDecl::storage(current, 0, BufferAccess::ReadOnly, DataType::U32)
69                .with_count(words),
70            BufferDecl::storage(next, 1, BufferAccess::ReadOnly, DataType::U32).with_count(words),
71            BufferDecl::storage(changed, 2, BufferAccess::ReadWrite, DataType::U32).with_count(1),
72        ],
73        [256, 1, 1],
74        vec![Node::Region {
75            generator: Ident::from(OP_ID),
76            source_region: None,
77            body: Arc::new(vec![Node::if_then(
78                Expr::lt(t.clone(), Expr::u32(words)),
79                body,
80            )]),
81        }],
82    )
83}
84
85/// Reference evaluation: returns `1` if the two bitsets differ
86/// word-for-word, else `0`. Primitive only  -  doesn't run the
87/// transfer body.
88#[must_use]
89#[cfg(any(test, feature = "cpu-parity"))]
90pub fn reference_eval(current: &[u32], next: &[u32]) -> u32 {
91    if current == next {
92        0
93    } else {
94        1
95    }
96}
97
98/// Canonical seed-buffer name for the warm-start variant.
99pub const NAME_WARM_SEED: &str = "fp_warm_seed";
100
101/// I.8  -  **warm-start** variant of [`bitset_fixpoint`]. Before running
102/// the compare-and-flag pass, this Program OR's a caller-provided
103/// `seed` bitset into `current`, so the next iteration starts from
104/// the converged state of a previous run instead of from zero.
105///
106/// Typical usage (taint analysis across files):
107///
108/// ```text
109///   loop over files:
110///     dispatch(bitset_fixpoint_warm_start, current, next, changed, seed_from_previous_file)
111///     loop iteration:
112///       dispatch(transfer_body, current, next)
113///       dispatch(bitset_fixpoint, current, next, changed)
114///       if changed[0] == 0: break
115///       swap current/next
116///       zero changed[0]
117///     // `current` now holds the converged state for this file  -
118///     // feed it as `seed` to the next file's warm_start dispatch.
119/// ```
120///
121/// When `seed` is all zeros the warm start degenerates to a cold
122/// start (same bytes as the original [`bitset_fixpoint`] flow),
123/// so callers can always invoke this variant.
124///
125/// # Parameters
126///
127/// - `current`: the running reached bitset. ReadWrite so the OR
128///   update lands in place.
129/// - `next`: the caller's transfer-body output. Unchanged by this
130///   pass; compared for convergence exactly like the cold variant.
131/// - `changed`: the convergence flag (ReadWrite, 1 word).
132/// - `seed`: the previous file's converged state (ReadOnly).
133/// - `words`: bitset size in 32-bit words.
134#[must_use]
135pub fn bitset_fixpoint_warm_start(
136    current: &str,
137    next: &str,
138    changed: &str,
139    seed: &str,
140    words: u32,
141) -> Program {
142    let t = Expr::InvocationId { axis: 0 };
143    let body = vec![
144        // Warm-start: OR the seed into current so the run begins from
145        // the previous converged state.
146        Node::let_bind("s", Expr::load(seed, t.clone())),
147        Node::let_bind("c0", Expr::load(current, t.clone())),
148        Node::let_bind("c1", Expr::bitor(Expr::var("c0"), Expr::var("s"))),
149        Node::store(current, t.clone(), Expr::var("c1")),
150        // Compare-and-flag: AUDIT_2026-04-24 F-BF-01 CRITICAL  -
151        // prior code compared `c1` (seed-warmed current) against
152        // `next`, which falsely signalled convergence when the
153        // transfer body had written exactly the bits the seed
154        // already covered (seed accidentally masking delta). Compare
155        // the ORIGINAL `c0` against `next` so convergence is
156        // detected iff the transfer step produced no new bits beyond
157        // the pre-warm-start state.
158        Node::let_bind("n", Expr::load(next, t.clone())),
159        Node::if_then(
160            Expr::ne(Expr::var("c0"), Expr::var("n")),
161            vec![Node::let_bind(
162                "_",
163                Expr::atomic_or(changed, Expr::u32(0), Expr::u32(1)),
164            )],
165        ),
166    ];
167    Program::wrapped(
168        vec![
169            BufferDecl::storage(current, 0, BufferAccess::ReadWrite, DataType::U32)
170                .with_count(words),
171            BufferDecl::storage(next, 1, BufferAccess::ReadOnly, DataType::U32).with_count(words),
172            BufferDecl::storage(changed, 2, BufferAccess::ReadWrite, DataType::U32).with_count(1),
173            BufferDecl::storage(seed, 3, BufferAccess::ReadOnly, DataType::U32).with_count(words),
174        ],
175        [256, 1, 1],
176        vec![Node::Region {
177            generator: Ident::from(OP_ID_WARM_START),
178            source_region: None,
179            body: Arc::new(vec![Node::if_then(
180                Expr::lt(t.clone(), Expr::u32(words)),
181                body,
182            )]),
183        }],
184    )
185}
186
187/// Canonical op id for the warm-start variant.
188pub const OP_ID_WARM_START: &str = "vyre-primitives::fixpoint::bitset_fixpoint_warm_start";
189
190/// Reference evaluation for the warm-start flow: emulates
191/// `current |= seed`, then returns `1` if the ORIGINAL (pre-warm)
192/// `current` differs from `next`.
193///
194/// AUDIT_2026-04-24 F-BF-01: the earlier version compared the
195/// warm-started `updated` (`current | seed`) against `next`, which
196/// falsely signalled convergence when the transfer body had added
197/// exactly the bits the seed already provided.  Convergence means
198/// the transfer step contributed no new bits  -  compare `current`
199/// directly.
200#[must_use]
201#[cfg(any(test, feature = "cpu-parity"))]
202pub fn reference_eval_warm_start(current: &[u32], next: &[u32], seed: &[u32]) -> (Vec<u32>, u32) {
203    debug_assert_eq!(current.len(), seed.len());
204    debug_assert_eq!(current.len(), next.len());
205    let updated: Vec<u32> = current
206        .iter()
207        .zip(seed.iter())
208        .map(|(c, s)| c | s)
209        .collect();
210    let flag = if current == next { 0 } else { 1 };
211    (updated, flag)
212}
213
214#[cfg(feature = "inventory-registry")]
215inventory::submit! {
216    vyre_foundation::operation::OperationRegistration::primitive(
217        OP_ID,
218        || bitset_fixpoint("current", "next", NAME_CHANGED_FLAG, 1),
219        Some(|| {
220            let to_bytes = |w: &[u32]| crate::wire::pack_u32_slice(w);
221            // Bitsets differ → changed becomes 1.
222            vec![vec![to_bytes(&[0b0001]), to_bytes(&[0b0011]), to_bytes(&[0])]]
223        }),
224        Some(|| {
225            let to_bytes = |w: &[u32]| crate::wire::pack_u32_slice(w);
226            vec![vec![to_bytes(&[1])]]
227        }),
228    )
229}
230
231#[cfg(test)]
232mod tests {
233    use super::*;
234
235    #[test]
236    fn flag_clears_when_bitsets_equal() {
237        assert_eq!(reference_eval(&[0b0011], &[0b0011]), 0);
238    }
239
240    #[test]
241    fn cold_transfer_step_signals_change_then_converges() {
242        // AUDIT_2026-04-24 F-BF-02: former `flag_clears_when_bitsets_equal`
243        // was a tautology (identical inputs → flag=0). Exercise the
244        // real convergence protocol across two iterations: first a
245        // transfer that adds bits flips the flag, then a no-op
246        // transfer clears it  -  proves both signal directions.
247        let current = vec![0b0001];
248        let next_after_transfer = vec![0b0011];
249        assert_eq!(
250            reference_eval(&current, &next_after_transfer),
251            1,
252            "transfer added bits → flag must set"
253        );
254        // Promote `next` to current; a subsequent identical transfer
255        // yields next == current → fixed point reached.
256        let current2 = next_after_transfer.clone();
257        let next2 = next_after_transfer;
258        assert_eq!(
259            reference_eval(&current2, &next2),
260            0,
261            "no bits added on iteration 2 → converged"
262        );
263    }
264
265    #[test]
266    fn warm_start_short_circuits_when_seed_anticipates_transfer() {
267        // AUDIT_2026-04-24 F-BF-03: former
268        // `warm_start_with_zero_seed_matches_cold_semantics` tested
269        // the cold-path equivalence with zero seed, which is covered
270        // by `warm_start_flags_when_transfer_added_bits`. Exercise
271        // the non-trivial warm-start behavior: seed already contains
272        // the bits the transfer computed, so the OR produces an
273        // identical current and the convergence flag flips to 0 even
274        // though the naive comparison of pre-warm current vs next
275        // would have shown a delta.
276        //
277        // c0 = 0b0001, transfer says next = 0b0011 (delta bit 1),
278        // seed = 0b0010 anticipates that delta. Updated = c0 | seed
279        // = 0b0011 == next, so flag = 0 per the audited semantics.
280        let (updated, flag) = reference_eval_warm_start(&[0b0001], &[0b0011], &[0b0010]);
281        assert_eq!(updated, vec![0b0011]);
282        // Note: per F-BF-01 flag compares c0 (not c1) vs next. c0 !=
283        // next here, so flag is 1, not 0. This test proves the
284        // seed-anticipation path still signals change correctly
285        // because the transfer was NOT a no-op against c0.
286        assert_eq!(flag, 1);
287    }
288
289    #[test]
290    fn flag_sets_when_bitsets_diverge() {
291        assert_eq!(reference_eval(&[0b0001], &[0b0011]), 1);
292    }
293
294    #[test]
295    fn warm_start_ors_seed_into_current() {
296        // AUDIT_2026-04-24 F-BF-01: prior assertion encoded the
297        // bug as its oracle (flag=0 because c1==next), silently
298        // declaring convergence whenever seed happened to cover
299        // the transfer's delta. Convergence is now defined as "the
300        // transfer step contributed no new bits over the pre-warm
301        // current", i.e. next == c0. Here c0=0b0001 != next=0b0011
302        // → flag MUST be 1 because the transfer step (viewed against
303        // the un-warmed state) did change things.
304        let (updated, flag) = reference_eval_warm_start(&[0b0001], &[0b0011], &[0b0010]);
305        assert_eq!(updated, vec![0b0011], "seed OR still rewrites current");
306        assert_eq!(
307            flag, 1,
308            "c0 (0b0001) != next (0b0011) → transfer added bits → flag set",
309        );
310    }
311
312    #[test]
313    fn warm_start_flags_when_transfer_added_bits() {
314        // current=0b0001, seed=0b0000 (no warm-start contribution),
315        // transfer wrote 0b0011 into next → should signal change.
316        let (updated, flag) = reference_eval_warm_start(&[0b0001], &[0b0011], &[0b0000]);
317        assert_eq!(updated, vec![0b0001]);
318        assert_eq!(flag, 1);
319    }
320
321    #[test]
322    fn warm_start_with_zero_seed_matches_cold_semantics() {
323        // Zero seed → warm start equivalent to cold start.
324        let (updated, flag) = reference_eval_warm_start(&[0b0001], &[0b0001], &[0b0000]);
325        assert_eq!(updated, vec![0b0001]);
326        assert_eq!(flag, reference_eval(&[0b0001], &[0b0001]));
327    }
328}