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(¤t, &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(¤t2, &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}