Struct FixpointEngine 

pub struct FixpointEngine;

Deterministic worklist solver for admitted monotone analyses.

Implementations

impl FixpointEngine

pub fn solve_proven<N, E, L, C, S, P>( graph: &DataflowGraph<N, E, L, C>, transfer: &AdmittedTransfer<P>, bottom: S, seeds: impl IntoIterator<Item = (N, S)>, budgets: QueryBudgets, ) -> CompletionProofResult<N, E, L, C, S>

where N: Clone + Hash + Ord, E: Clone + Hash + Ord, L: Clone + Hash + Ord, C: Clone + Hash + Ord, S: JoinSemilattice + Hash, P: TransferPolicy<S>,

Solves to a stable fixpoint and mints its content-bound completion proof.

pub fn present<'a, N, E, L, C, S, P>( proof: &'a DataflowCompletionProof<N, E, C, S>, graph: &DataflowGraph<N, E, L, C>, transfer: &AdmittedTransfer<P>, bottom: &S, seeds: impl IntoIterator<Item = (N, S)>, budgets: QueryBudgets, ) -> Result<&'a DataflowSolution<N, E, C, S>, CompletionProofMismatch>

where N: Clone + Hash + Ord, E: Clone + Hash + Ord, L: Hash + Ord, C: Hash + Ord, S: Hash, P: TransferPolicy<S>,

Presents a proof only when every semantic input still matches.

pub fn solve_incremental<N, E, L, C, S, P>( previous: &DataflowCompletionProof<N, E, C, S>, graph: &DataflowGraph<N, E, L, C>, transfer: &AdmittedTransfer<P>, bottom: S, seeds: impl IntoIterator<Item = (N, S)>, budgets: QueryBudgets, ) -> CompletionProofResult<N, E, L, C, S>

where N: Clone + Hash + Ord, E: Clone + Hash + Ord, L: Clone + Hash + Ord, C: Clone + Hash + Ord, S: JoinSemilattice + Hash, P: TransferPolicy<S>,

Recomputes exactly the observed successor cone of changed entry facts.

Structural, lattice, policy, or limit changes are intentionally refused: callers must perform a clean solve for those semantic edits. Dependency edits reuse unaffected states and their observations, then remint a proof from the complete final state rather than blessing the old witness.

pub fn solve<N, E, L, C, S, P>( graph: &DataflowGraph<N, E, L, C>, transfer: &AdmittedTransfer<P>, bottom: S, seeds: impl IntoIterator<Item = (N, S)>, budgets: QueryBudgets, ) -> DataflowResult<N, E, L, C, S>

where N: Clone + Hash + Ord, E: Clone + Hash + Ord, L: Clone + Hash + Ord, C: Clone + Hash + Ord, S: JoinSemilattice, P: TransferPolicy<S>,

Solves from explicit entry/exit facts; nodes not reached from a seed stay at bottom.

pub fn start_resumable<N, E, L, C, S, P>( graph: &DataflowGraph<N, E, L, C>, transfer: &AdmittedTransfer<P>, bottom: S, seeds: impl IntoIterator<Item = (N, S)>, max_visits: usize, explanation_limit: usize, ) -> DataflowProgressResult<N, E, L, C, S>

where N: Clone + Hash + Ord, E: Clone + Hash + Ord, L: Clone + Hash + Ord, C: Clone + Hash + Ord, S: JoinSemilattice + Hash, P: TransferPolicy<S>,

Starts a solve and executes at most max_visits complete worklist nodes.

Unlike resource refusal inside Self::solve, this cooperative boundary snapshots only between nodes, so resumption never repeats callbacks or presents a shortened event stream as complete.

pub fn resume<N, E, L, C, S, P>( graph: &DataflowGraph<N, E, L, C>, transfer: &AdmittedTransfer<P>, bottom: &S, seeds: impl IntoIterator<Item = (N, S)>, continuation: DataflowContinuation<N, E, C, S>, max_visits: usize, ) -> DataflowProgressResult<N, E, L, C, S>

where N: Clone + Hash + Ord, E: Clone + Hash + Ord, L: Clone + Hash + Ord, C: Clone + Hash + Ord, S: JoinSemilattice + Hash, P: TransferPolicy<S>,

Resumes a content-bound snapshot, refusing every changed input identity.

Trait Implementations

impl Clone for FixpointEngine

fn clone(&self) -> FixpointEngine

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for FixpointEngine

impl Debug for FixpointEngine

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for FixpointEngine

fn default() -> FixpointEngine

Returns the “default value” for a type.

impl Eq for FixpointEngine

impl PartialEq for FixpointEngine

fn eq(&self, other: &FixpointEngine) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for FixpointEngine