Skip to content

gds.verification

Engine

Run verification checks against a SystemIR.

Parameters:

Name Type Description Default
system SystemIR

The system to verify.

 required
checks list[Callable[[SystemIR], list[Finding]]] | None

Optional subset of checks. Defaults to all generic checks.

 None
Source code in packages/gds-framework/gds/verification/engine.py 
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
def verify(
    system: SystemIR,
    checks: list[Callable[[SystemIR], list[Finding]]] | None = None,
) -> VerificationReport:
    """Run verification checks against a SystemIR.

    Args:
        system: The system to verify.
        checks: Optional subset of checks. Defaults to all generic checks.
    """
    checks = checks or ALL_CHECKS
    findings: list[Finding] = []
    for check_fn in checks:
        findings.extend(check_fn(system))
    return VerificationReport(system_name=system.name, findings=findings)

Findings

Bases: BaseModel

A single verification check result — pass or fail with context.

Source code in packages/gds-framework/gds/verification/findings.py 
16
17
18
19
20
21
22
23
24
class Finding(BaseModel):
    """A single verification check result — pass or fail with context."""

    check_id: str
    severity: Severity
    message: str
    source_elements: list[str] = Field(default_factory=list)
    passed: bool
    exportable_predicate: str = ""

Bases: StrEnum

Severity level of a verification finding.

Source code in packages/gds-framework/gds/verification/findings.py 
 8
 9
10
11
12
13
class Severity(StrEnum):
    """Severity level of a verification finding."""

    ERROR = "error"
    WARNING = "warning"
    INFO = "info"

Bases: BaseModel

Aggregated verification results for a system.

Source code in packages/gds-framework/gds/verification/findings.py 
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
class VerificationReport(BaseModel):
    """Aggregated verification results for a system."""

    system_name: str
    findings: list[Finding] = Field(default_factory=list)

    @property
    def errors(self) -> int:
        return sum(
            1 for f in self.findings if not f.passed and f.severity == Severity.ERROR
        )

    @property
    def warnings(self) -> int:
        return sum(
            1 for f in self.findings if not f.passed and f.severity == Severity.WARNING
        )

    @property
    def info_count(self) -> int:
        return sum(
            1 for f in self.findings if not f.passed and f.severity == Severity.INFO
        )

    @property
    def checks_passed(self) -> int:
        return sum(1 for f in self.findings if f.passed)

    @property
    def checks_total(self) -> int:
        return len(self.findings)

Generic Checks

Generic verification checks G-001 through G-006.

These checks operate on the domain-neutral SystemIR. They verify type consistency, structural completeness, and graph topology without referencing any domain-specific block types or semantics.

check_g001_domain_codomain_matching(system)

G-001: Domain/Codomain Matching.

For every covariant block-to-block wiring, verify the label is consistent with source forward_out or target forward_in. Contravariant wirings are skipped (handled by G-003).

Property: For every wiring w where w.direction = COVARIANT and both endpoints are blocks: tokens(w.label) is a subset of tokens(source.forward_out) OR tokens(target.forward_in).

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/generic_checks.py 
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
def check_g001_domain_codomain_matching(system: SystemIR) -> list[Finding]:
    """G-001: Domain/Codomain Matching.

    For every covariant block-to-block wiring, verify the label is consistent
    with source forward_out or target forward_in. Contravariant wirings are
    skipped (handled by G-003).

    Property: For every wiring w where w.direction = COVARIANT and both
    endpoints are blocks: tokens(w.label) is a subset of
    tokens(source.forward_out) OR tokens(target.forward_in).

    See: docs/framework/design/check-specifications.md
    """
    findings = []
    block_sigs = {b.name: b.signature for b in system.blocks}

    for wiring in system.wirings:
        if wiring.direction != FlowDirection.COVARIANT:
            continue
        if wiring.source not in block_sigs or wiring.target not in block_sigs:
            continue

        src_out = block_sigs[wiring.source][1]  # forward_out
        tgt_in = block_sigs[wiring.target][0]  # forward_in

        if not src_out or not tgt_in:
            findings.append(
                Finding(
                    check_id="G-001",
                    severity=Severity.ERROR,
                    message=(
                        f"Cannot verify domain/codomain: "
                        f"{wiring.source} out={src_out!r}, "
                        f"{wiring.target} in={tgt_in!r}"
                    ),
                    source_elements=[wiring.source, wiring.target],
                    passed=False,
                )
            )
            continue

        compatible = tokens_subset(wiring.label, src_out) or tokens_subset(
            wiring.label, tgt_in
        )
        findings.append(
            Finding(
                check_id="G-001",
                severity=Severity.ERROR,
                message=(
                    f"Wiring {wiring.label!r}: "
                    f"{wiring.source} out={src_out!r} -> {wiring.target} in={tgt_in!r}"
                    + ("" if compatible else " — MISMATCH")
                ),
                source_elements=[wiring.source, wiring.target],
                passed=compatible,
            )
        )

    return findings

check_g002_signature_completeness(system)

G-002: Signature Completeness.

Every block must have at least one non-empty input slot and at least one non-empty output slot. BoundaryAction blocks (block_type == "boundary") are exempt from the input requirement -- they have no inputs by design, since they model exogenous signals entering the system from outside.

Property: For every block b: has_output(b) is True, and (if b is not a BoundaryAction) has_input(b) is True, where has_input/has_output check that at least one of the forward/backward slots is non-empty.

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/generic_checks.py 
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
def check_g002_signature_completeness(system: SystemIR) -> list[Finding]:
    """G-002: Signature Completeness.

    Every block must have at least one non-empty input slot and at least one
    non-empty output slot. BoundaryAction blocks (block_type == "boundary") are
    exempt from the input requirement -- they have no inputs by design, since
    they model exogenous signals entering the system from outside.

    Property: For every block b: has_output(b) is True, and (if b is not
    a BoundaryAction) has_input(b) is True, where has_input/has_output check
    that at least one of the forward/backward slots is non-empty.

    See: docs/framework/design/check-specifications.md
    """
    findings = []
    for block in system.blocks:
        fwd_in, fwd_out, bwd_in, bwd_out = block.signature
        has_input = bool(fwd_in) or bool(bwd_in)
        has_output = bool(fwd_out) or bool(bwd_out)

        # BoundaryAction blocks have no inputs by design — only check outputs
        is_boundary = block.block_type == "boundary"
        has_required = has_output if is_boundary else has_input and has_output

        missing = []
        if not has_input:
            missing.append("no inputs")
        if not has_output:
            missing.append("no outputs")

        findings.append(
            Finding(
                check_id="G-002",
                severity=Severity.ERROR,
                message=(
                    f"{block.name}: signature "
                    f"({fwd_in!r}, {fwd_out!r}, "
                    f"{bwd_in!r}, {bwd_out!r})"
                    + (f" — {', '.join(missing)}" if missing else "")
                ),
                source_elements=[block.name],
                passed=has_required,
            )
        )

    return findings

check_g003_direction_consistency(system)

G-003: Direction Consistency.

Validate direction flag consistency and contravariant port-slot matching.

Two validations:

A) Flag consistency -- direction, is_feedback, is_temporal must not contradict: - COVARIANT + is_feedback -> ERROR (feedback implies contravariant) - CONTRAVARIANT + is_temporal -> ERROR (temporal implies covariant)

B) Contravariant port-slot matching -- for CONTRAVARIANT wirings, the label must be a token-subset of the source's backward_out (signature[3]) or the target's backward_in (signature[2]). G-001 already covers the covariant side.

Property: (A) NOT (COVARIANT AND is_feedback) and NOT (CONTRAVARIANT AND is_temporal). (B) For contravariant wirings: tokens(label) is a subset of tokens(source.backward_out) OR tokens(target.backward_in).

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/generic_checks.py 
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
def check_g003_direction_consistency(system: SystemIR) -> list[Finding]:
    """G-003: Direction Consistency.

    Validate direction flag consistency and contravariant port-slot matching.

    Two validations:

    A) Flag consistency -- ``direction``, ``is_feedback``, ``is_temporal`` must
       not contradict:
       - COVARIANT + is_feedback -> ERROR (feedback implies contravariant)
       - CONTRAVARIANT + is_temporal -> ERROR (temporal implies covariant)

    B) Contravariant port-slot matching -- for CONTRAVARIANT wirings, the label
       must be a token-subset of the source's backward_out (signature[3]) or
       the target's backward_in (signature[2]). G-001 already covers the
       covariant side.

    Property: (A) NOT (COVARIANT AND is_feedback) and NOT (CONTRAVARIANT AND
    is_temporal). (B) For contravariant wirings: tokens(label) is a subset of
    tokens(source.backward_out) OR tokens(target.backward_in).

    See: docs/framework/design/check-specifications.md
    """
    findings = []
    block_sigs = {b.name: b.signature for b in system.blocks}

    for wiring in system.wirings:
        # A) Flag consistency
        if wiring.direction == FlowDirection.COVARIANT and wiring.is_feedback:
            findings.append(
                Finding(
                    check_id="G-003",
                    severity=Severity.ERROR,
                    message=(
                        f"Wiring {wiring.label!r} "
                        f"({wiring.source} -> {wiring.target}): "
                        f"COVARIANT + is_feedback — contradiction"
                    ),
                    source_elements=[wiring.source, wiring.target],
                    passed=False,
                )
            )
            continue

        if wiring.direction == FlowDirection.CONTRAVARIANT and wiring.is_temporal:
            findings.append(
                Finding(
                    check_id="G-003",
                    severity=Severity.ERROR,
                    message=(
                        f"Wiring {wiring.label!r} "
                        f"({wiring.source} -> {wiring.target}): "
                        f"CONTRAVARIANT + is_temporal — contradiction"
                    ),
                    source_elements=[wiring.source, wiring.target],
                    passed=False,
                )
            )
            continue

        # B) Contravariant port-slot matching (G-001 covers covariant)
        if wiring.direction == FlowDirection.CONTRAVARIANT:
            if wiring.source not in block_sigs or wiring.target not in block_sigs:
                # Non-block endpoints — G-004 handles dangling references
                continue

            src_bwd_out = block_sigs[wiring.source][3]  # backward_out
            tgt_bwd_in = block_sigs[wiring.target][2]  # backward_in

            if not src_bwd_out and not tgt_bwd_in:
                findings.append(
                    Finding(
                        check_id="G-003",
                        severity=Severity.ERROR,
                        message=(
                            f"Wiring {wiring.label!r} "
                            f"({wiring.source} -> {wiring.target}): "
                            f"CONTRAVARIANT but both backward "
                            f"ports are empty"
                        ),
                        source_elements=[wiring.source, wiring.target],
                        passed=False,
                    )
                )
                continue

            compatible = tokens_subset(wiring.label, src_bwd_out) or tokens_subset(
                wiring.label, tgt_bwd_in
            )
            findings.append(
                Finding(
                    check_id="G-003",
                    severity=Severity.ERROR,
                    message=(
                        f"Wiring {wiring.label!r}: "
                        f"{wiring.source} bwd_out={src_bwd_out!r} -> "
                        f"{wiring.target} bwd_in={tgt_bwd_in!r}"
                        + ("" if compatible else " — MISMATCH")
                    ),
                    source_elements=[wiring.source, wiring.target],
                    passed=compatible,
                )
            )

    return findings

check_g004_dangling_wirings(system)

G-004: Dangling Wirings.

Flag wirings whose source or target is not in the system's block or input set. A dangling reference indicates a typo or missing block.

Property: For every wiring w: w.source in N and w.target in N, where N = {b.name for b in blocks} union {i.name for i in inputs}.

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/generic_checks.py 
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
def check_g004_dangling_wirings(system: SystemIR) -> list[Finding]:
    """G-004: Dangling Wirings.

    Flag wirings whose source or target is not in the system's block or input
    set. A dangling reference indicates a typo or missing block.

    Property: For every wiring w: w.source in N and w.target in N, where
    N = {b.name for b in blocks} union {i.name for i in inputs}.

    See: docs/framework/design/check-specifications.md
    """
    findings = []
    known_names = {b.name for b in system.blocks}
    for inp in system.inputs:
        known_names.add(inp.name)

    for wiring in system.wirings:
        src_ok = wiring.source in known_names
        tgt_ok = wiring.target in known_names
        ok = src_ok and tgt_ok

        issues = []
        if not src_ok:
            issues.append(f"source {wiring.source!r} unknown")
        if not tgt_ok:
            issues.append(f"target {wiring.target!r} unknown")

        findings.append(
            Finding(
                check_id="G-004",
                severity=Severity.ERROR,
                message=(
                    f"Wiring {wiring.label!r} ({wiring.source} -> {wiring.target})"
                    + (f" — {', '.join(issues)}" if issues else "")
                ),
                source_elements=[wiring.source, wiring.target],
                passed=ok,
            )
        )

    return findings

check_g005_sequential_type_compatibility(system)

G-005: Sequential Type Compatibility.

In stack (sequential) composition, the wiring label must be a token-subset of BOTH the source's forward_out AND the target's forward_in. This is stricter than G-001, which only requires matching one side.

Property: For every covariant, non-temporal wiring w between blocks: tokens(w.label) is a subset of tokens(source.forward_out) AND tokens(w.label) is a subset of tokens(target.forward_in).

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/generic_checks.py 
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
def check_g005_sequential_type_compatibility(system: SystemIR) -> list[Finding]:
    """G-005: Sequential Type Compatibility.

    In stack (sequential) composition, the wiring label must be a token-subset
    of BOTH the source's forward_out AND the target's forward_in. This is
    stricter than G-001, which only requires matching one side.

    Property: For every covariant, non-temporal wiring w between blocks:
    tokens(w.label) is a subset of tokens(source.forward_out) AND
    tokens(w.label) is a subset of tokens(target.forward_in).

    See: docs/framework/design/check-specifications.md
    """
    findings = []
    block_sigs = {b.name: b.signature for b in system.blocks}
    block_names = set(block_sigs.keys())

    for wiring in system.wirings:
        if wiring.direction != FlowDirection.COVARIANT:
            continue
        if wiring.is_temporal:
            continue
        if wiring.source not in block_names or wiring.target not in block_names:
            continue

        src_out = block_sigs[wiring.source][1]  # forward_out
        tgt_in = block_sigs[wiring.target][0]  # forward_in

        if not src_out or not tgt_in:
            continue

        label_in_out = tokens_subset(wiring.label, src_out)
        label_in_in = tokens_subset(wiring.label, tgt_in)
        compatible = label_in_out and label_in_in

        findings.append(
            Finding(
                check_id="G-005",
                severity=Severity.ERROR,
                message=(
                    f"Stack {wiring.source} ; {wiring.target}: "
                    f"out={src_out!r}, in={tgt_in!r}, wiring={wiring.label!r}"
                    + ("" if compatible else " — type mismatch")
                ),
                source_elements=[wiring.source, wiring.target],
                passed=compatible,
            )
        )

    return findings

check_g006_covariant_acyclicity(system)

G-006: Covariant Acyclicity.

The covariant (forward) flow graph must be a directed acyclic graph (DAG). Temporal wirings and contravariant wirings are excluded because they do not create within-evaluation algebraic dependencies.

Property: Let G_cov = (V, E_cov) where V = {b.name for b in blocks} and E_cov = {(w.source, w.target) for w in wirings if w.direction = COVARIANT and not w.is_temporal}. G_cov is acyclic.

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/generic_checks.py 
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
def check_g006_covariant_acyclicity(system: SystemIR) -> list[Finding]:
    """G-006: Covariant Acyclicity.

    The covariant (forward) flow graph must be a directed acyclic graph (DAG).
    Temporal wirings and contravariant wirings are excluded because they do not
    create within-evaluation algebraic dependencies.

    Property: Let G_cov = (V, E_cov) where V = {b.name for b in blocks} and
    E_cov = {(w.source, w.target) for w in wirings if w.direction = COVARIANT
    and not w.is_temporal}. G_cov is acyclic.

    See: docs/framework/design/check-specifications.md
    """
    block_names = {b.name for b in system.blocks}
    adj: dict[str, list[str]] = {name: [] for name in block_names}

    for wiring in system.wirings:
        if wiring.direction != FlowDirection.COVARIANT:
            continue
        if wiring.is_temporal:
            continue
        if wiring.source in block_names and wiring.target in block_names:
            adj[wiring.source].append(wiring.target)

    # DFS cycle detection
    WHITE, GRAY, BLACK = 0, 1, 2
    color = {name: WHITE for name in block_names}
    cycle_path: list[str] = []
    has_cycle = False

    def dfs(node: str) -> bool:
        nonlocal has_cycle
        color[node] = GRAY
        cycle_path.append(node)
        for neighbor in adj[node]:
            if color[neighbor] == GRAY:
                has_cycle = True
                return True
            if color[neighbor] == WHITE and dfs(neighbor):
                return True
        cycle_path.pop()
        color[node] = BLACK
        return False

    for node in block_names:
        if color[node] == WHITE and dfs(node):
            break

    if has_cycle:
        return [
            Finding(
                check_id="G-006",
                severity=Severity.ERROR,
                message=(
                    f"Covariant flow graph contains a cycle: {' -> '.join(cycle_path)}"
                ),
                source_elements=cycle_path,
                passed=False,
            )
        ]

    return [
        Finding(
            check_id="G-006",
            severity=Severity.ERROR,
            message="Covariant flow graph is acyclic (DAG)",
            source_elements=[],
            passed=True,
        )
    ]

Spec Checks

SC-001: Completeness.

Every entity variable is updated by at least one mechanism. Detects orphan state variables that can never change -- a likely specification error.

Property: Let U = {(e, v) for m in Mechanisms for (e, v) in m.updates}. For every entity e and variable v in e.variables: (e.name, v) in U. The mechanism update map is surjective onto the state variable set.

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/spec_checks.py 
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
def check_completeness(spec: GDSSpec) -> list[Finding]:
    """SC-001: Completeness.

    Every entity variable is updated by at least one mechanism. Detects orphan
    state variables that can never change -- a likely specification error.

    Property: Let U = {(e, v) for m in Mechanisms for (e, v) in m.updates}.
    For every entity e and variable v in e.variables: (e.name, v) in U.
    The mechanism update map is surjective onto the state variable set.

    See: docs/framework/design/check-specifications.md
    """
    findings: list[Finding] = []

    all_updates: set[tuple[str, str]] = set()
    for block in spec.blocks.values():
        if isinstance(block, Mechanism):
            for entity_name, var_name in block.updates:
                all_updates.add((entity_name, var_name))

    orphans: list[str] = []
    for entity in spec.entities.values():
        for var_name in entity.variables:
            if (entity.name, var_name) not in all_updates:
                orphans.append(f"{entity.name}.{var_name}")

    if orphans:
        findings.append(
            Finding(
                check_id="SC-001",
                severity=Severity.WARNING,
                message=(
                    f"Orphan state variables never updated by any mechanism: {orphans}"
                ),
                source_elements=orphans,
                passed=False,
            )
        )
    else:
        findings.append(
            Finding(
                check_id="SC-001",
                severity=Severity.INFO,
                message="All state variables are updated by at least one mechanism",
                passed=True,
            )
        )

    return findings

SC-002: Determinism.

Within each wiring, no two mechanisms update the same variable. Detects write conflicts where multiple mechanisms try to modify the same state variable within the same composition.

Property: For every wiring w and every (entity, variable) pair (e, v): |{m in w.block_names : m is Mechanism, (e, v) in m.updates}| <= 1. The state transition f must be a function, not a multi-valued relation.

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/spec_checks.py 
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
def check_determinism(spec: GDSSpec) -> list[Finding]:
    """SC-002: Determinism.

    Within each wiring, no two mechanisms update the same variable. Detects
    write conflicts where multiple mechanisms try to modify the same state
    variable within the same composition.

    Property: For every wiring w and every (entity, variable) pair (e, v):
    |{m in w.block_names : m is Mechanism, (e, v) in m.updates}| <= 1.
    The state transition f must be a function, not a multi-valued relation.

    See: docs/framework/design/check-specifications.md
    """
    findings: list[Finding] = []

    for wiring in spec.wirings.values():
        update_map: dict[tuple[str, str], list[str]] = defaultdict(list)
        for bname in wiring.block_names:
            block = spec.blocks.get(bname)
            if block is not None and isinstance(block, Mechanism):
                for entity_name, var_name in block.updates:
                    update_map[(entity_name, var_name)].append(bname)

        for (ename, vname), mechs in update_map.items():
            if len(mechs) > 1:
                findings.append(
                    Finding(
                        check_id="SC-002",
                        severity=Severity.ERROR,
                        message=(
                            f"Write conflict in wiring '{wiring.name}': "
                            f"{ename}.{vname} updated by {mechs}"
                        ),
                        source_elements=mechs,
                        passed=False,
                    )
                )

    if not any(f.check_id == "SC-002" for f in findings):
        findings.append(
            Finding(
                check_id="SC-002",
                severity=Severity.INFO,
                message="No write conflicts detected",
                passed=True,
            )
        )

    return findings

SC-003: Reachability.

Can signals reach from one block to another through the wiring graph? Maps to the GDS attainability correspondence.

Property: There exists a directed path in the wire graph from from_block to to_block, where edges are (wire.source, wire.target) across all SpecWiring instances. Unlike other semantic checks, requires explicit from_block and to_block arguments.

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/spec_checks.py 
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
def check_reachability(spec: GDSSpec, from_block: str, to_block: str) -> list[Finding]:
    """SC-003: Reachability.

    Can signals reach from one block to another through the wiring graph?
    Maps to the GDS attainability correspondence.

    Property: There exists a directed path in the wire graph from from_block
    to to_block, where edges are (wire.source, wire.target) across all
    SpecWiring instances. Unlike other semantic checks, requires explicit
    from_block and to_block arguments.

    See: docs/framework/design/check-specifications.md
    """
    adj: dict[str, set[str]] = defaultdict(set)
    for wiring in spec.wirings.values():
        for wire in wiring.wires:
            adj[wire.source].add(wire.target)

    visited: set[str] = set()
    queue = [from_block]
    reachable = False
    while queue:
        current = queue.pop(0)
        if current == to_block:
            reachable = True
            break
        if current in visited:
            continue
        visited.add(current)
        queue.extend(adj.get(current, set()))

    if reachable:
        return [
            Finding(
                check_id="SC-003",
                severity=Severity.INFO,
                message=f"Block '{from_block}' can reach '{to_block}'",
                source_elements=[from_block, to_block],
                passed=True,
            )
        ]
    return [
        Finding(
            check_id="SC-003",
            severity=Severity.WARNING,
            message=f"Block '{from_block}' cannot reach '{to_block}'",
            source_elements=[from_block, to_block],
            passed=False,
        )
    ]

SC-004: Type Safety.

Wire spaces match source and target block expectations. Verifies that space references on wires correspond to registered spaces.

Property: For every wire in every SpecWiring: if wire.space is non-empty, then wire.space is in spec.spaces. Referential integrity of space declarations on wiring channels.

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/spec_checks.py 
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
def check_type_safety(spec: GDSSpec) -> list[Finding]:
    """SC-004: Type Safety.

    Wire spaces match source and target block expectations. Verifies that space
    references on wires correspond to registered spaces.

    Property: For every wire in every SpecWiring: if wire.space is non-empty,
    then wire.space is in spec.spaces. Referential integrity of space
    declarations on wiring channels.

    See: docs/framework/design/check-specifications.md
    """
    findings: list[Finding] = []

    for wiring in spec.wirings.values():
        for wire in wiring.wires:
            if wire.space and wire.space not in spec.spaces:
                findings.append(
                    Finding(
                        check_id="SC-004",
                        severity=Severity.ERROR,
                        message=(
                            f"Wire {wire.source} -> {wire.target} references "
                            f"unregistered space '{wire.space}'"
                        ),
                        source_elements=[wire.source, wire.target],
                        passed=False,
                    )
                )

    if not any(f.check_id == "SC-004" for f in findings):
        findings.append(
            Finding(
                check_id="SC-004",
                severity=Severity.INFO,
                message="All wire space references are valid",
                passed=True,
            )
        )

    return findings

SC-005: Parameter References.

All parameter references in blocks resolve to registered parameters. Validates that every params_used entry on blocks corresponds to a parameter definition in the spec's parameter_schema.

Property: For every block b implementing HasParams: {p for p in b.params_used} is a subset of spec.parameter_schema.names().

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/spec_checks.py 
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
def check_parameter_references(spec: GDSSpec) -> list[Finding]:
    """SC-005: Parameter References.

    All parameter references in blocks resolve to registered parameters.
    Validates that every ``params_used`` entry on blocks corresponds to a
    parameter definition in the spec's ``parameter_schema``.

    Property: For every block b implementing HasParams:
    {p for p in b.params_used} is a subset of spec.parameter_schema.names().

    See: docs/framework/design/check-specifications.md
    """
    findings: list[Finding] = []

    param_names = spec.parameter_schema.names()
    unresolved: list[str] = []
    for bname, block in spec.blocks.items():
        if isinstance(block, HasParams):
            for param in block.params_used:
                if param not in param_names:
                    unresolved.append(f"{bname} -> {param}")

    if unresolved:
        findings.append(
            Finding(
                check_id="SC-005",
                severity=Severity.ERROR,
                message=f"Unresolved parameter references: {unresolved}",
                source_elements=unresolved,
                passed=False,
            )
        )
    else:
        findings.append(
            Finding(
                check_id="SC-005",
                severity=Severity.INFO,
                message="All parameter references resolve to registered definitions",
                passed=True,
            )
        )

    return findings

SC-006/SC-007: Canonical Wellformedness.

Canonical projection structural validity. Two sub-checks:

  • SC-006: At least one mechanism exists (f is non-empty). Property: |project_canonical(spec).mechanism_blocks| >= 1.
  • SC-007: State space X is non-empty (entities with variables exist). Property: |project_canonical(spec).state_variables| >= 1.

Together these ensure the canonical form h = f . g is non-degenerate.

See: docs/framework/design/check-specifications.md

Source code in packages/gds-framework/gds/verification/spec_checks.py 
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
def check_canonical_wellformedness(spec: GDSSpec) -> list[Finding]:
    """SC-006/SC-007: Canonical Wellformedness.

    Canonical projection structural validity. Two sub-checks:

    - SC-006: At least one mechanism exists (f is non-empty).
      Property: |project_canonical(spec).mechanism_blocks| >= 1.
    - SC-007: State space X is non-empty (entities with variables exist).
      Property: |project_canonical(spec).state_variables| >= 1.

    Together these ensure the canonical form h = f . g is non-degenerate.

    See: docs/framework/design/check-specifications.md
    """
    findings: list[Finding] = []
    canonical = project_canonical(spec)

    if not canonical.mechanism_blocks:
        findings.append(
            Finding(
                check_id="SC-006",
                severity=Severity.WARNING,
                message="No mechanisms found — state transition f is empty",
                passed=False,
            )
        )
    else:
        findings.append(
            Finding(
                check_id="SC-006",
                severity=Severity.INFO,
                message=(
                    "State transition f has "
                    f"{len(canonical.mechanism_blocks)} mechanism(s)"
                ),
                passed=True,
            )
        )

    if not canonical.state_variables:
        findings.append(
            Finding(
                check_id="SC-007",
                severity=Severity.WARNING,
                message="State space X is empty — no entity variables defined",
                passed=False,
            )
        )
    else:
        findings.append(
            Finding(
                check_id="SC-007",
                severity=Severity.INFO,
                message=(
                    f"State space X has {len(canonical.state_variables)} variable(s)"
                ),
                passed=True,
            )
        )

    return findings