cottax.core.realisation.proof module

What a graph answers to before anything runs it: every node carrying what runs it, over driven.DrivenGraph. It does not ask whether a backend can run what it finds – that is the backend’s proof, a level under this.

check_implemented[N: Label, V: Place](name: N, node: NodeDefinition[V])

Every node carries what runs it – a function its body, a problem its driver’s implementation. An executable graph holds no bare condition, so that is every node.

Return type:

Iterator[Violation]

class RealisedGraph[N: Label, V: Place](graph: NestingGraph[N, V])

Bases: DrivenGraph[N, V], Generic[N, V]

A driven graph with what runs every node: what a backend’s proof strengthens.

checks_node: PerLevel[tuple[Callable[[N, NodeDefinition[V]], Iterator[Violation]], ...]] = (<function check_implemented>,)

the one thing a level below adds.

Type:

(name, node) -> violations

class NoImplementation(node: object)

Bases: Violation

node: object

template: AbstractClassVar[str] = '{node!r} carries nothing that runs it -- `Implement` it. Drawing, rewriting, proving and exporting a graph holding one is fine; only running it is not'

e.g. ‘output {place!r} is owned by both {other!r} and {node!r}’

Type:

Wording