sim_incremental_core/dataflow/engine/
contracts.rs

1/// The operation whose contract failed while solving a graph.
2#[derive(Clone, Copy, Debug, Eq, PartialEq)]
3pub enum DataflowFailure {
4    /// A transfer retracted facts from its input.
5    Transfer,
6    /// A join was not an upper bound of both operands.
7    Join,
8}
9/// A stable observation from one fixpoint run.
10#[derive(Clone, Debug, Eq, Hash, PartialEq)]
11pub enum DataflowEvent<N, E, C> {
12    /// A node was removed from the ordered worklist.
13    Visit(N),
14    /// Facts were propagated across an edge.
15    Propagate {
16        /// Stable edge identity.
17        edge: E,
18        /// Semantic edge class, including consumer-defined exceptional classes.
19        class: EdgeClass<C>,
20    },
21}
22
23/// Exact resources consumed by a completed run.
24#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
25pub struct DataflowUsage {
26    /// Node visits, joins, and transfers performed.
27    pub work: usize,
28    /// Edge propagations performed.
29    pub observations: usize,
30    /// Maximum number of simultaneously retained node states.
31    pub depth: usize,
32    /// State payload units retained over the run.
33    pub output: usize,
34}
35
36/// A located fixpoint refusal.
37#[derive(Clone, Debug, Eq, PartialEq)]
38pub enum DataflowError<N, E, L> {
39    /// A seed names no node in the immutable graph.
40    UnknownSeed(N),
41    /// A continuation was presented to inputs other than the ones it captured.
42    ContinuationMismatch {
43        /// Fingerprint category that changed.
44        changed: ContinuationFingerprint,
45        /// Fingerprint captured by the continuation.
46        expected: ValueFingerprint,
47        /// Fingerprint supplied while resuming.
48        actual: ValueFingerprint,
49    },
50    /// A declared budget was exhausted at a node or edge.
51    BudgetExceeded {
52        /// Exhausted core budget class.
53        kind: BudgetKind,
54        /// Configured limit.
55        limit: usize,
56        /// Units that the rejected operation would consume.
57        attempted: usize,
58        /// Node active at the refusal, when applicable.
59        node: Option<N>,
60        /// Edge active at the refusal, when applicable.
61        edge: Option<E>,
62        /// Source/artifact location of `node`, or the edge predecessor.
63        location: L,
64        /// Edge successor location, when the refusal occurred on an edge.
65        target_location: Option<L>,
66    },
67    /// An admitted transfer violated its contract at a precise node.
68    NodeFailure {
69        /// Failed operation.
70        failure: DataflowFailure,
71        /// Stable node identity.
72        node: N,
73        /// Consumer-neutral node location.
74        location: L,
75    },
76    /// A lattice join violated its contract while propagating a precise edge.
77    EdgeFailure {
78        /// Failed operation.
79        failure: DataflowFailure,
80        /// Stable edge identity.
81        edge: E,
82        /// Edge predecessor location in propagation order.
83        location: L,
84        /// Edge successor location in propagation order.
85        target_location: L,
86    },
87}
88
89/// Content identity checked before a suspended solve may resume.
90#[derive(Clone, Copy, Debug, Eq, PartialEq)]
91pub enum ContinuationFingerprint {
92    /// Immutable graph structure and locations.
93    Graph,
94    /// Admitted transfer semantics and configuration.
95    Policy,
96    /// Bottom value and canonical seed set.
97    Dependencies,
98}
99
100/// One causal predecessor retained for a changed node state.
101#[derive(Clone, Debug, Eq, Hash, PartialEq)]
102pub struct CausalPredecessor<N, E> {
103    /// Node whose output caused the change, or the seeded node itself.
104    pub node: N,
105    /// Propagation edge, absent for a seed fact.
106    pub edge: Option<E>,
107}
108
109/// A bounded explanation that cannot masquerade as complete after truncation.
110#[derive(Clone, Debug, Eq, PartialEq)]
111pub struct DataflowExplanation<N, E> {
112    predecessors: Box<[CausalPredecessor<N, E>]>,
113    omitted: usize,
114}
115
116#[derive(Clone, Debug, Eq, Hash, PartialEq)]
117struct CausalRecord<N, E> {
118    retained: Vec<CausalPredecessor<N, E>>,
119    omitted: usize,
120}
121
122impl<N, E> DataflowExplanation<N, E> {
123    /// Returns the retained causal predecessors in deterministic discovery order.
124    pub fn predecessors(&self) -> &[CausalPredecessor<N, E>] {
125        &self.predecessors
126    }
127
128    /// Returns whether causal evidence was omitted by the requested bound.
129    pub const fn truncated(&self) -> bool {
130        self.omitted != 0
131    }
132
133    /// Returns the exact number of causal predecessors omitted by the bound.
134    pub const fn omitted(&self) -> usize {
135        self.omitted
136    }
137}
138
139/// A content-bound snapshot of an incomplete deterministic worklist solve.
140#[derive(Clone, Debug, Eq, PartialEq)]
141pub struct DataflowContinuation<N, E, C, S> {
142    token: ContinuationToken,
143    graph: ValueFingerprint,
144    policy: ValueFingerprint,
145    dependencies: ValueFingerprint,
146    states: BTreeMap<N, S>,
147    pending: BTreeSet<N>,
148    events: Vec<DataflowEvent<N, E, C>>,
149    causes: BTreeMap<N, CausalRecord<N, E>>,
150    cause_limit: usize,
151    usage: DataflowUsage,
152}
153
154impl<N, E, C, S> DataflowContinuation<N, E, C, S> {
155    /// Returns the canonical core continuation handle bound to this snapshot.
156    pub const fn token(&self) -> ContinuationToken {
157        self.token
158    }
159
160    /// Returns the graph fingerprint captured by this snapshot.
161    pub const fn graph_fingerprint(&self) -> ValueFingerprint {
162        self.graph
163    }
164}
165
166/// Outcome of a resumable solve step.
167#[derive(Clone, Debug, Eq, PartialEq)]
168pub enum DataflowProgress<N, E, C, S> {
169    /// The worklist converged.
170    Complete(DataflowSolution<N, E, C, S>),
171    /// Work remains and is captured without loss.
172    Suspended(DataflowContinuation<N, E, C, S>),
173}
174
175/// Result of one resumable fixpoint step.
176pub type DataflowProgressResult<N, E, L, C, S> =
177    Result<DataflowProgress<N, E, C, S>, DataflowError<N, E, L>>;
178
179#[derive(Clone, Copy)]
180struct ContinuationIdentity {
181    graph: ValueFingerprint,
182    policy: ValueFingerprint,
183    dependencies: ValueFingerprint,
184}
185
186/// Result of one fixpoint solve.
187pub type DataflowResult<N, E, L, C, S> =
188    Result<DataflowSolution<N, E, C, S>, DataflowError<N, E, L>>;
189
190/// Result of a clean or incremental proof-producing fixpoint solve.
191pub type CompletionProofResult<N, E, L, C, S> =
192    Result<DataflowCompletionProof<N, E, C, S>, DataflowError<N, E, L>>;
193
194struct ChargeLocation<N, E, L> {
195    node: Option<N>,
196    edge: Option<E>,
197    location: L,
198    target_location: Option<L>,
199}
200
201/// A converged, fully accounted dataflow solution.
202#[derive(Clone, Debug, Eq, PartialEq)]
203pub struct DataflowSolution<N, E, C, S> {
204    states: BTreeMap<N, S>,
205    events: Vec<DataflowEvent<N, E, C>>,
206    usage: DataflowUsage,
207    causes: BTreeMap<N, CausalRecord<N, E>>,
208}
209
210/// Schema revision mixed into every completion-proof identity.
211pub const DATAFLOW_PROOF_SCHEMA_REVISION: u64 = 1;
212
213/// An immutable witness that a precise set of dataflow inputs reached a fixpoint.
214///
215/// The witness is deliberately content based: clean and incremental evaluation
216/// of the same inputs mint the same identity.  Execution history and visit counts
217/// remain diagnostics and cannot change what the proof says.
218#[derive(Clone, Debug, Eq, PartialEq)]
219pub struct DataflowCompletionProof<N, E, C, S> {
220    identity: ValueFingerprint,
221    graph: ValueFingerprint,
222    lattice: ValueFingerprint,
223    policy: ValueFingerprint,
224    boundaries: ValueFingerprint,
225    limits: ValueFingerprint,
226    dependencies: ValueFingerprint,
227    seed_fingerprints: BTreeMap<N, ValueFingerprint>,
228    observations: Box<[(N, E, N)]>,
229    node_fingerprints: BTreeMap<N, ValueFingerprint>,
230    solution: DataflowSolution<N, E, C, S>,
231}
232
233impl<N: Ord, E, C, S> DataflowCompletionProof<N, E, C, S> {
234    /// Returns the canonical semantic identity of this completed fixpoint.
235    pub const fn identity(&self) -> ValueFingerprint {
236        self.identity
237    }
238
239    /// Returns the exact dependency edges observed while reaching the fixpoint.
240    pub fn observations(&self) -> &[(N, E, N)] {
241        &self.observations
242    }
243
244    /// Returns the converged node fingerprints used for incremental cutoff.
245    pub fn node_fingerprints(&self) -> &BTreeMap<N, ValueFingerprint> {
246        &self.node_fingerprints
247    }
248
249    /// Returns the proven solution.
250    pub const fn solution(&self) -> &DataflowSolution<N, E, C, S> {
251        &self.solution
252    }
253}
254
255/// Why a completion proof cannot be presented for the supplied inputs.
256#[derive(Clone, Copy, Debug, Eq, PartialEq)]
257pub enum CompletionProofMismatch {
258    /// The immutable graph or its boundary declarations changed.
259    Graph,
260    /// The lattice bottom or state representation changed.
261    Lattice,
262    /// The admitted transfer policy changed.
263    Policy,
264    /// The declared resource limits changed.
265    Limits,
266    /// Entry or external facts changed.
267    Dependencies,
268}
269
270impl<N: Ord, E, C, S> DataflowSolution<N, E, C, S> {
271    /// Returns the converged state for a node.
272    pub fn state(&self, node: &N) -> Option<&S> {
273        self.states.get(node)
274    }
275    /// Iterates converged states in stable node order.
276    pub fn states(&self) -> impl ExactSizeIterator<Item = (&N, &S)> {
277        self.states.iter()
278    }
279    /// Returns the deterministic visit and propagation sequence.
280    pub fn events(&self) -> &[DataflowEvent<N, E, C>] {
281        &self.events
282    }
283    /// Returns exact resource consumption.
284    pub const fn usage(&self) -> DataflowUsage {
285        self.usage
286    }
287
288    /// Explains a node with at most `limit` causal predecessors.
289    pub fn explain(&self, node: &N, limit: usize) -> Option<DataflowExplanation<N, E>>
290    where
291        N: Clone,
292        E: Clone,
293    {
294        let causes = self.causes.get(node)?;
295        let retained = causes
296            .retained
297            .iter()
298            .take(limit)
299            .cloned()
300            .collect::<Vec<_>>();
301        Some(DataflowExplanation {
302            omitted: causes
303                .omitted
304                .saturating_add(causes.retained.len().saturating_sub(retained.len())),
305            predecessors: retained.into_boxed_slice(),
306        })
307    }
308}
309
310/// Deterministic worklist solver for admitted monotone analyses.
311#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
312pub struct FixpointEngine;
sim_incremental_core/dataflow/engine/contracts.rs

sim_incremental_core/dataflow/engine/
contracts.rs
