T0-1: Formalize verification check specifications as requirements

[rororowyourboat]

Problem

Each structural and semantic check (G-001..G-006, SC-001..SC-009) is described in code docstrings and prose. There is no formal statement of: (a) the property being checked, (b) the invariant it enforces, (c) the conditions under which a pass is sound vs. merely necessary. Until each check has an explicit property statement, a pass result cannot be soundly interpreted as verification of anything in particular.

Type

[MATH] [DOC]

Prioritization

• Criteria: C1 (Soundness)
• Tier: 0 — Correctness and Integrity
• Phase: 1 — Foundations
• Dependencies: None (critical path root)
• Blocks: T0-2, T0-4, T1-1, T1-2, T1-4, T2-2

Current State

15 checks exist (6 generic on SystemIR, 9 semantic on GDSSpec). All are implemented and tested. What's missing is the formal specification document linking each check to a mathematical property.

• Generic checks: gds/verification/generic_checks.py
• Semantic checks: gds/verification/spec_checks.py

Steps

1. Create check specification template. Structured format with: Check ID, Type, Statement, Rationale, Failure semantics, Proof/algorithm, Layer.

2. Write specifications for all 6 generic checks (G-001..G-006). Each must link to a property of the composition algebra or canonical form h = f ∘ g.

3. Write specifications for all 9 semantic checks (SC-001..SC-009). Each must link to a property of GDSSpec or the canonical decomposition. SC-008/SC-009 link to paper Defs 2.5 and 2.7.

4. Publish as docs/research/verification/check-specifications.md. One page, all 15 checks, structured per template. Cross-reference paper-implementation-gap.md for paper-linked checks.

5. Define requirement IDs. Each check specification becomes a traceable requirement for T0-2.

Deliverables

• Check specification template (standardized format)
• 6 generic check specifications (G-001..G-006)
• 9 semantic check specifications (SC-001..SC-009)
• docs/research/verification/check-specifications.md

Check Specification Template

Check ID:    G-003
Type:        Structural (Layer 0)
Statement:   The SystemIR covariant wiring graph contains no directed
             cycles. (Temporal wirings excluded from cycle detection.)
Rationale:   Acyclicity is necessary for the canonical projection
             h = f ∘ g to be well-defined as a function rather than
             an implicit equation.
Failure:     A cycle in covariant wirings implies the canonical form
             is undefined for this composition.
Proof:       Topological sort of covariant subgraph; cycle detection
             via DFS in generic_checks.py:check_covariant_acyclicity.
Layer:       Structural (SystemIR)

---

Part of the GDS-Core Improvement Roadmap

Scientific Context

Evidence level: Level 1 (Formal) — transforms check docstrings into verifiable mathematical claims.

After this item, the answer to "what does G-006 prove?" changes from a Python docstring to: "G-006 establishes that the covariant wiring graph is a DAG, which is a necessary condition for h = f ∘ g to be well-defined as a function rather than an implicit equation." That is a verifiable mathematical claim, not prose.

Verification Strategy

Correspondence proof. Two-column table where each row is independently verifiable by reading the check code and the mathematical statement:

Mathematical property	Software implementation
Covariant wiring graph is a DAG	check_covariant_acyclicity() — DFS on covariant subgraph of SystemIR
h = f ∘ g requires f non-empty	SC-006 verifies ≥1 Mechanism block exists
Admissible input constraints reference valid state	SC-008 validates AdmissibleInputConstraint entries

The correspondence table IS the deliverable — each row is the formal specification for one check.

Showcase

The completed check specifications feed directly into the verification pyramid artifact — the bottom two layers (structural + semantic) become fully documented with traceable properties.