Struct SideConditionChecker 

pub struct SideConditionChecker<'a> { /* private fields */ }

Answers side-condition queries for plan rewrites.

Used by the certificate verifier and rewrite engine to check whether a rewrite is safe to apply.

Implementations

impl<'a> SideConditionChecker<'a>

pub fn new(dag: &'a PlanDag) -> Self

Creates a new checker, running the analysis eagerly.

pub fn analysis(&self) -> &PlanAnalysis

Returns the underlying analysis.

pub fn obligations_safe(&self, id: PlanId) -> bool

Check if a node’s children are obligation-safe (no cancel leaks).

pub fn cancel_safe(&self, id: PlanId) -> bool

Check if a node’s cancel behavior is safe (losers drained).

pub fn are_independent(&self, a: PlanId, b: PlanId) -> bool

Check if two subtrees are independent (no shared mutable state).

Conservative: returns true only if neither subtree contains nodes that appear in the other’s reachable set. This is a structural check — it cannot detect aliased external state.

pub fn rewrite_preserves_obligations( &self, before: PlanId, after: PlanId, ) -> bool

Check if a rewrite from before to after preserves obligation safety.

Conservative: requires both the before and after nodes to be obligation-safe.

pub fn rewrite_preserves_cancel(&self, before: PlanId, after: PlanId) -> bool

Check if a rewrite preserves cancel safety.

pub fn rewrite_preserves_budget(&self, before: PlanId, after: PlanId) -> bool

Check if a rewrite preserves budget monotonicity.

pub fn rewrite_preserves_deadline(&self, before: PlanId, after: PlanId) -> bool

Check if a rewrite preserves deadline guarantees specifically.

This is a more focused check than rewrite_preserves_budget:

• If the original has no deadline, any deadline is acceptable
• If the original has a deadline, the rewritten must have one that is at least as tight

pub fn effective_deadline(&self, id: PlanId) -> Option<DeadlineMicros>

Returns the effective deadline for a node, if any.

pub fn deadline_within_tolerance( &self, before: PlanId, after: PlanId, tolerance_micros: u64, ) -> bool

Check if a rewrite does not worsen the deadline by more than a given amount.

Useful for allowing small deadline relaxations in exchange for other benefits.

pub fn rewrite_preserves_loser_drain( &self, before: PlanId, after: PlanId, ) -> bool

Returns true when a rewrite preserves the loser-drain property.

A rewrite is safe if it does not degrade cancel-safety (Safe → non-Safe) and does not introduce new obligation leak candidates on the cancel path.

pub fn rewrite_preserves_finalize_order( &self, before: PlanId, after: PlanId, ) -> bool

Returns true when a rewrite preserves the relative order of obligation-bearing children inside a Join node.

For Race/Timeout/Leaf rewrites this always returns true (no ordering contract). Race → Join (e.g., DedupRaceJoin) is allowed because a Race imposes no finalize ordering on its children; any ordering in the resulting Join is valid.

pub fn rewrite_no_new_obligation_leaks( &self, before: PlanId, after: PlanId, ) -> bool

Returns true when a rewrite does not introduce new obligation leaks.

This checks three properties:

1. Obligation safety does not degrade (safe → unsafe).
2. The all_paths_resolve flag does not become false.
3. The set of leak_on_cancel obligations does not grow.
4. Previously must_resolve obligations are not demoted to leak-or-reserve.

pub fn children_pairwise_independent(&self, children: &[PlanId]) -> bool

Check whether all children are pairwise independent.

impl SideConditionChecker<'_>

pub fn check_independence(&self, a: PlanId, b: PlanId) -> IndependenceResult

Check if two nodes are independent (can be safely reordered).

Two nodes are independent if:

• They don’t share any common descendants (structural independence)
• They don’t have data dependencies through obligations
• Reordering them doesn’t change observable behavior

This is a conservative analysis: if uncertain, returns Uncertain.

pub fn commutes(&self, a: PlanId, b: PlanId) -> bool

Check if two nodes commute (can be reordered without changing semantics).

This is an alias for check_independence with a clearer name for users thinking in terms of commutativity.

pub fn compute_independence_relation(&self) -> IndependenceRelation

Compute the independence relation for all leaf nodes in the DAG.

This builds a relation that can be used for Mazurkiewicz trace equivalence checking: two sequences are equivalent if one can be transformed into the other by commuting independent operations.

pub fn rewrite_valid_up_to_trace(&self, before: PlanId, after: PlanId) -> bool

Check if a rewrite is valid up to Mazurkiewicz trace equivalence.

A rewrite is valid if:

1. The structural transformation is correct
2. The rewrite preserves the independence relation
3. The observable behavior is preserved (up to reordering of independent operations)

This is useful for rewrites like Join[a, b] -> Join[b, a] where the order doesn’t matter if a and b are independent.

pub fn reorderable_join_children(&self, children: &[PlanId]) -> Vec<Vec<usize>>

Check if the children of a Join can be reordered.

Returns the indices of children that can be freely reordered (all pairs in the returned set are mutually independent).

pub fn trace_equivalence_hint(&self, id: PlanId) -> TraceEquivalenceHint

Get a trace equivalence hint for a node.

Returns a summary of which operations can commute, useful for the rewrite engine to know when certain rewrites are safe.