Module dataflow

Expand description

Deterministic, located dataflow graphs.

Structs§

AdmittedTransfer: A transfer policy that passed the public dataflow law suite.
CausalPredecessor: One causal predecessor retained for a changed node state.
DataflowCompletionProof: An immutable witness that a precise set of dataflow inputs reached a fixpoint.
DataflowContinuation: A content-bound snapshot of an incomplete deterministic worklist solve.
DataflowExplanation: A bounded explanation that cannot masquerade as complete after truncation.
DataflowGraph: Immutable, canonically ordered, content-identified dataflow structure.
DataflowSolution: A converged, fully accounted dataflow solution.
DataflowUsage: Exact resources consumed by a completed run.
Edge: One immutable graph edge.
EdgeSpec: An edge supplied to checked graph construction.
FixpointEngine: Deterministic worklist solver for admitted monotone analyses.
LawSuite: Public reusable law suite for lattice and transfer admission.
LawViolation: A precise admission refusal.
Node: One immutable graph node.
NodeSpec: A node supplied to checked graph construction.

Boundary: A node’s declared relationship to the graph boundary.
CompletionProofMismatch: Why a completion proof cannot be presented for the supplied inputs.
ContinuationFingerprint: Content identity checked before a suspended solve may resume.
DataflowError: A located fixpoint refusal.
DataflowEvent: A stable observation from one fixpoint run.
DataflowFailure: The operation whose contract failed while solving a graph.
DataflowLaw: A law whose failure makes a lattice or transfer policy inadmissible.
DataflowProgress: Outcome of a resumable solve step.
EdgeClass: The semantic class of an edge.
GraphBuildError: A checked graph-construction refusal.
GraphDirection: The direction in which an edge propagates.

DATAFLOW_PROOF_SCHEMA_REVISION: Schema revision mixed into every completion-proof identity.

JoinSemilattice: A join semilattice with a least element.
LocatedGraphAdapter: Projects an external located representation into neutral graph declarations.
StateSize: State that can report the memory it contributes to a dataflow solution.
TransferPolicy: A deterministic, inflationary dataflow transfer with stable proof identity.

AdaptedGraph: The neutral graph produced by a particular located adapter.
AdapterBuildResult: The checked construction result produced by a located adapter.
CompletionProofResult: Result of a clean or incremental proof-producing fixpoint solve.
DataflowProgressResult: Result of one resumable fixpoint step.
DataflowResult: Result of one fixpoint solve.