vj-codegen 0.1.0

//! T13 (`docs/superpowers/plans/2026-10-03-sva.md`): the local-variable FLOW
//! algebra of LRM Annex F.5.4, the rule set that decides whether a local
//! variable assigned by one part of a sequence is visible to a later part
//! (16.10: "flows out").
//!
//! F.5.4 defines three sets per sequence `R`: `sample(R)` (the variables `R`
//! assigns on SOME match), `block(R)` (the variables that can NOT flow out of
//! `R` because two threads of `R` would write them concurrently, or because
//! `R` can match without assigning them on every path that composes with a
//! later operand), and `flow(X, R)` (the variables definitely assigned after
//! `R` when `X` is definitely assigned before it). The Remark under the rules
//! gives `flow(X, R) = (X U flow({}, R)) - block(R)`, so a [`Flow`] stores only
//! the three X-independent sets `(sample, block, flow({}))` and
//! [`Flow::flow_out`] applies that identity. Every combinator below is the
//! F.5.4 rule re-derived over those three sets (the derivation is in each
//! doc comment), and the unit tests in this file pin each one against the LRM
//! text's own examples (s4-s8, 16.10).
//!
//! Variables are [`LocalVarId`]s, the builder's CANONICAL slots (one per
//! declared local per instance expansion), so two sets compose by plain set
//! algebra.
use std::collections::BTreeSet;

use sv_sim_sim::sva::ir::LocalVarId;

/// A set of local variables.
pub type VarSet = BTreeSet<LocalVarId>;

/// The F.5.4 triple of one sequence (see the module doc comment).
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub struct Flow {
    /// `sample(R)`: every variable some match of `R` may assign.
    pub sample: VarSet,
    /// `block(R)`: variables that cannot flow out of `R`.
    pub block: VarSet,
    /// `flow({}, R)`: variables `R` assigns on every match, ignoring what was
    /// assigned before `R`.
    pub flow0: VarSet,
}

fn union(a: &VarSet, b: &VarSet) -> VarSet {
    a.union(b).copied().collect()
}

fn minus(a: &VarSet, b: &VarSet) -> VarSet {
    a.difference(b).copied().collect()
}

fn inter(a: &VarSet, b: &VarSet) -> VarSet {
    a.intersection(b).copied().collect()
}

impl Flow {
    /// The identity of every combinator: a Boolean leaf `b`, the empty match,
    /// and `R[*0]` (F.5.4: `sample(b) = block(b) = {}`, `flow(X, b) = X`,
    /// `flow(X, R[*0]) = X`).
    pub fn identity() -> Flow {
        Flow::default()
    }

    /// `(1, v = e)`: assigns `v`. `sample = {v}`, `block = {}`,
    /// `flow(X, (1, v = e)) = X U {v}`.
    pub fn assign(v: LocalVarId) -> Flow {
        Flow {
            sample: VarSet::from([v]),
            block: VarSet::new(),
            flow0: VarSet::from([v]),
        }
    }

    /// `flow(X, R)` for the variables definitely assigned before `R`
    /// (`flow(X, R) = (X U flow({}, R)) - block(R)`, the F.5.4 Remark).
    pub fn flow_out(&self, x: &VarSet) -> VarSet {
        minus(&union(x, &self.flow0), &self.block)
    }

    /// `R1 ##n R2` (any delay; the delay itself assigns nothing).
    ///
    /// * `sample = sample(R1) U sample(R2)`;
    /// * `block = (block(R1) - flow({}, R2)) U block(R2)`, F.5.4 verbatim;
    /// * `flow({}, R1 ##1 R2) = flow(flow({}, R1), R2)`; applying the Remark's
    ///   `flow(X, R2) = (X U f2) - b2` to `X = flow({}, R1) = f1` gives
    ///   `(f1 U f2) - b2`.
    pub fn concat(&self, rhs: &Flow) -> Flow {
        Flow {
            sample: union(&self.sample, &rhs.sample),
            block: union(&minus(&self.block, &rhs.flow0), &rhs.block),
            flow0: minus(&union(&self.flow0, &rhs.flow0), &rhs.block),
        }
    }

    /// `R1 or R2`: a variable flows out only if BOTH branches assign it
    /// (`flow(X, or) = flow(X, R1) ∩ flow(X, R2)`), so `flow({}) = f1 ∩ f2`;
    /// `sample` and `block` are unions.
    pub fn or(&self, rhs: &Flow) -> Flow {
        Flow {
            sample: union(&self.sample, &rhs.sample),
            block: union(&self.block, &rhs.block),
            flow0: inter(&self.flow0, &rhs.flow0),
        }
    }

    /// `R1 intersect R2`, and by the LRM's own equivalences `R1 and R2`,
    /// `R1 within R2` and `R1 throughout R2` (`g[*0:$] intersect R`): both
    /// threads run concurrently, so a variable assigned by both is blocked.
    ///
    /// * `block = block(R1) U block(R2) U (sample(R1) ∩ sample(R2))`;
    /// * `flow(X, intersect) = (flow(X, R1) U flow(X, R2)) - block`, hence
    ///   `flow({}) = (f1 U f2) - block`.
    pub fn intersect(&self, rhs: &Flow) -> Flow {
        let block = union(
            &union(&self.block, &rhs.block),
            &inter(&self.sample, &rhs.sample),
        );
        Flow {
            sample: union(&self.sample, &rhs.sample),
            flow0: minus(&union(&self.flow0, &rhs.flow0), &block),
            block,
        }
    }

    /// `(t v; R)`: a sequence-scoped declaration. `v` is out of scope after
    /// the sequence, so it leaves every set (`sample((t v; R)) = sample(R) -
    /// {v}`, `block((t v; R)) = block(R) - {v}`; `flow` removes it from the
    /// result).
    pub fn scoped(&self, vars: &VarSet) -> Flow {
        Flow {
            sample: minus(&self.sample, vars),
            block: minus(&self.block, vars),
            flow0: minus(&self.flow0, vars),
        }
    }

    /// The number of repetitions may be zero, so the body's assignments are not
    /// guaranteed (`R[*0:n]` is the `or` of `R[*0]` and the rest).
    pub fn or_empty(&self) -> Flow {
        self.or(&Flow::identity())
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    fn v(n: u32) -> LocalVarId {
        LocalVarId(n)
    }

    fn set(ns: &[u32]) -> VarSet {
        ns.iter().map(|&n| v(n)).collect()
    }

    #[test]
    fn the_identity_is_neutral_for_concat_on_both_sides() {
        let a = Flow::assign(v(0));
        assert_eq!(Flow::identity().concat(&a), a);
        assert_eq!(a.concat(&Flow::identity()), a);
    }

    #[test]
    fn an_assignment_samples_and_flows_its_variable() {
        let a = Flow::assign(v(3));
        assert_eq!(a.sample, set(&[3]));
        assert!(a.block.is_empty());
        assert_eq!(a.flow_out(&VarSet::new()), set(&[3]));
        // flow(X, (1, v = e)) = X U {v}.
        assert_eq!(a.flow_out(&set(&[1])), set(&[1, 3]));
    }

    /// F.5.4: `flow(X, b) = X` for a Boolean leaf.
    #[test]
    fn a_boolean_leaf_passes_x_through() {
        assert_eq!(Flow::identity().flow_out(&set(&[1, 2])), set(&[1, 2]));
    }

    /// 16.10 `s5`: `(a ##1 (b, x = 1) or c) ##1 x` -- `x` is assigned on only
    /// one branch of the `or`, so it does NOT flow out.
    #[test]
    fn or_flows_only_what_both_branches_assign() {
        let one = Flow::assign(v(0));
        let none = Flow::identity();
        let o = one.or(&none);
        assert!(o.flow_out(&VarSet::new()).is_empty());
        // Both branches assigning flows it.
        let both = one.or(&Flow::assign(v(0)));
        assert_eq!(both.flow_out(&VarSet::new()), set(&[0]));
        // Something assigned before the `or` stays assigned.
        assert_eq!(o.flow_out(&set(&[0])), set(&[0]));
    }

    /// 16.10 `s7`: `(a, x = 1) and (b, x = 2)` blocks `x`.
    #[test]
    fn intersect_blocks_a_variable_both_operands_assign() {
        let l = Flow::assign(v(0));
        let r = Flow::assign(v(0));
        let i = l.intersect(&r);
        assert_eq!(i.block, set(&[0]));
        assert!(i.flow_out(&VarSet::new()).is_empty());
        // Assigned before the `and`: also blocked afterwards (F.5.4 subtracts
        // block from X as well).
        assert!(i.flow_out(&set(&[0])).is_empty());
    }

    /// 16.10 `s6`: a variable assigned by only ONE `and` operand flows out.
    #[test]
    fn intersect_flows_a_variable_one_operand_assigns() {
        let l = Flow::assign(v(0));
        let r = Flow::identity();
        let i = l.intersect(&r);
        assert!(i.block.is_empty());
        assert_eq!(i.flow_out(&VarSet::new()), set(&[0]));
        assert_eq!(r.intersect(&l), i, "intersect is symmetric");
    }

    /// Two operands assigning DIFFERENT variables both sample and both flow.
    /// (That one operand cannot READ what the other assigns, 16.10 `s4`, is the
    /// builder's per-operand flow-in set, not this algebra.)
    #[test]
    fn intersect_samples_the_union() {
        let l = Flow::assign(v(0));
        let r = Flow::assign(v(1));
        let i = l.intersect(&r);
        assert_eq!(i.sample, set(&[0, 1]));
        assert_eq!(i.flow_out(&VarSet::new()), set(&[0, 1]));
    }

    /// F.5.4: `block(R1 ##1 R2) = (block(R1) - flow({}, R2)) U block(R2)`: a
    /// variable blocked inside `R1` is unblocked again if `R2` reassigns it.
    #[test]
    fn concat_unblocks_a_variable_the_second_operand_reassigns() {
        let blocked = Flow::assign(v(0)).intersect(&Flow::assign(v(0)));
        assert_eq!(blocked.block, set(&[0]));
        let after = blocked.concat(&Flow::assign(v(0)));
        assert!(after.block.is_empty());
        assert_eq!(after.flow_out(&VarSet::new()), set(&[0]));
        // Without the reassignment it stays blocked.
        let still = blocked.concat(&Flow::identity());
        assert_eq!(still.block, set(&[0]));
    }

    /// `flow(flow(X, R1), R2)`: the second operand's block removes an earlier
    /// assignment too (`flow0 = (f1 U f2) - b2`).
    #[test]
    fn concat_applies_the_second_operands_block_to_the_first_operands_flow() {
        let blocked = Flow::assign(v(0)).intersect(&Flow::assign(v(0)));
        let c = Flow::assign(v(0)).concat(&blocked);
        assert!(c.flow_out(&VarSet::new()).is_empty());
    }

    #[test]
    fn concat_is_associative_on_representative_triples() {
        let a = Flow::assign(v(0));
        let b = Flow::assign(v(1)).or(&Flow::identity());
        let c = Flow::assign(v(0)).intersect(&Flow::assign(v(0)));
        assert_eq!(a.concat(&b).concat(&c), a.concat(&b.concat(&c)));
        assert_eq!(b.concat(&c).concat(&a), b.concat(&c.concat(&a)));
        assert_eq!(c.concat(&a).concat(&b), c.concat(&a.concat(&b)));
    }

    #[test]
    fn or_is_commutative_and_intersect_is_commutative() {
        let a = Flow::assign(v(0)).concat(&Flow::assign(v(1)));
        let b = Flow::assign(v(1)).or(&Flow::identity());
        assert_eq!(a.or(&b), b.or(&a));
        assert_eq!(a.intersect(&b), b.intersect(&a));
    }

    /// `(t v; R)`: `v` is removed from every set.
    #[test]
    fn a_scoped_variable_leaves_every_set() {
        let f = Flow::assign(v(0)).concat(&Flow::assign(v(1)));
        let s = f.scoped(&set(&[0]));
        assert_eq!(s.sample, set(&[1]));
        assert_eq!(s.flow_out(&VarSet::new()), set(&[1]));
        let blocked = Flow::assign(v(0)).intersect(&Flow::assign(v(0)));
        assert!(blocked.scoped(&set(&[0])).block.is_empty());
    }

    /// F.5.4: `R[*0]` has the identity flow, and `R[*0:n]` is `R[*0] or R[*1:n]`
    /// so a variable assigned by `R` does not flow out of an optional `R`.
    #[test]
    fn an_optional_body_does_not_flow_its_assignments() {
        let r = Flow::assign(v(0));
        let o = r.or_empty();
        assert_eq!(o.sample, set(&[0]));
        assert!(o.flow_out(&VarSet::new()).is_empty());
    }

    /// The F.5.4 Remark, checked against the rules it abbreviates:
    /// `flow(X, R) = (X U flow({}, R)) - block(R)` on a composite.
    #[test]
    fn the_remark_identity_holds_for_a_composite() {
        let r = Flow::assign(v(0))
            .concat(&Flow::assign(v(1)).or(&Flow::identity()))
            .intersect(&Flow::assign(v(2)));
        for x in [set(&[]), set(&[0]), set(&[1, 2]), set(&[0, 1, 2])] {
            assert_eq!(r.flow_out(&x), minus(&union(&x, &r.flow0), &r.block));
        }
    }
}