SYS has software child

The check is sys_has_software_child. It is SPEC-stage. Default severity is warning. It loads every decomposable system requirement. Assumptions and constraints are out of the denominator. Tombstones are out. For each remaining SYS-REQ it asks whether any one of three holds: an active SW-REQ names it in traces.satisfies or the legacy parent field, the trace index carries an implemented_by link, or a test carries verified_by. An INT-REQ child does not count. It does not rewrite the YAML. It does not call Z3. It does not call Kind2.

The upward hop from each SW-REQ or INT-REQ stays on L2 software complete. That hop is error when a software or integration requirement has no live SYS parent. This hop is the reverse: whether each eligible SYS-REQ has some realization below it. The graph of declared levels stays on levels connected. The L1 body hop stays on L1 system complete. The STK-to-SYS child hop stays on cross level complete.

Each SW-REQ can look fine on its own. The Jama cell still names a parent. Reviewers signed the English in another tool. An L2 hop is green because every software row still cites a live SYS id. That SYS-REQ can already have only an INT-REQ under it. Other SPEC hops miss this because they never walk parent to child.

The expensive miss is a programme that treats the INT layer as the behavior. The system requirement stayed active. No live software child names it. No annotation names it. No test names it. This hop is the gate that prints the SYS ids that still have no downward realization.

# SYS-REQ-210
# status: approved
# req_type: guarantee
# INT-REQ-044 traces.satisfies: [SYS-REQ-210]
# a presence-only L2 hop
# pass. the INT-REQ has a live SYS parent
# proof audit --check sys_has_software_child
# [SPEC] sys_has_software_child
# 1 SYS-REQ(s) have no downward realization
# (no SW-REQ child, no implementing code, no verifying tests)
# in 1 decomposable SYS-REQ(s)
# SYS-REQ-210
# WARNING
# proof req new specs/software --parent SYS-REQ-210

The fix is a human authorization, not a rewrite of Go. Annotate the implementing function with // SYS-REQ-210. Add a // Verifies: SYS-REQ-210 test. Or add a live SW-REQ that satisfies that id. Do not treat the INT-REQ as the child. Do not delete the SYS-REQ to silence the checker. Then re-run SPEC.

proof audit --check sys_has_software_child --verbose
proof workflow check --stage spec --only sys_has_software_child
proof help sys_has_software_child

The teaching graph is still one eligible SYS-REQ that no live SW-REQ, annotation, or test realizes. Close it by adding a software child, annotating the Go, or adding a verifying test. Do not delete the YAML. Do not invent a second SYS-REQ. An INT-REQ only does not count. Zero decomposable SYS-REQs is a pass, not completeness. Assumptions and constraints are out of the count. One live SW-REQ among extra historical links is enough. Direct code realization is enough. A verifying test is enough.

# SYS-REQ-210 kept. SW-REQ-318 satisfies SYS-REQ-210 (live)
# proof audit --check sys_has_software_child
# 1 SYS-REQ(s) have a downward realization
# (SW-REQ child, implementing code, or verifying tests)
# SPEC may move on. pass sits on a live child

The upward hop stays on L2 software complete. The graph hop stays on levels connected. The L1 hop stays on L1 system complete. The STK hop stays on cross level complete. The rewrite hop stays on characterization testing and mirrors. Jama still authors. Proof vs Jama.

Warning when an eligible SYS-REQ lacks all three realizations. Default severity does not fail the merge. You can still advance. Zero decomposable system requirements is a pass, not a complete L1-to-L2 chain. --skip-level L1 or --skip-level L2 skips the hop. An audit_ignore entry with a recorded reason removes that SYS-REQ from the count. The hop does not write the satisfies list. It does not add a shall. It does not write a description. It does not prove the Go. It does not run Kind2. It does not measure independence. It does not say every SW-REQ has a live SYS parent. That hop is L2 software complete, and that hop is error. A quiet hop is not a proof that Jama's shall matches the Go, only that every in-scope SYS-REQ currently has some downward realization. We have not scored this floor against a frozen Jama pack or a VectorCAST corpus. The loss is named, not scored.

The L2 hop stays on L2 software complete. The rewrite hop stays on characterization testing and mirrors. The engagement stays on software correctness audit. Jama still authors.

What is SYS has software child? Same question. Same URL.

Is this L2 software complete? No. That hop is whether each SW-REQ or INT-REQ has a live SYS parent, and it is error. This hop is whether each eligible SYS-REQ has a SW-REQ, code, or a test, and it is warning. See L2 software complete.

Is this levels connected? No. That hop is whether declared L0, L1, and L2 join as one graph. This hop is whether each eligible SYS-REQ is itself realized. See levels connected.

Is this L1 system complete? No. That hop is whether each active SYS-REQ has a description and an upward edge. This hop is whether each eligible SYS-REQ still has a downward realization. See L1 system complete.

Is this cross level complete? No. That hop is whether each active STK-REQ has a live SYS child. This hop is the SYS-to-software realization. See cross level complete.

Is this interface coverage? No. That hop is whether a boundary has an INT-REQ. An INT-REQ does not satisfy this hop. See interface coverage.

Does an INT-REQ child satisfy this hop? No. Integration requirements capture a boundary. They do not capture component-owned behavior.

Does a code annotation satisfy this hop without an SW-REQ? Yes. Direct implemented_by is a realization. The software-requirement layer is not mandatory.

Does a verifying test satisfy this hop without an SW-REQ? Yes. verified_by is a realization. A passing test cannot exercise an absent implementation.

Does an assumption or a constraint fail this hop? No. Those kinds are out of the denominator. Only a guarantee (or an unset req_type, which reads as guarantee) is asked.

Does a historical tombstone next to a live SW-REQ fail this hop? No. One live software child is enough. Extra retired ids do not fail the row.

Does a quiet hop prove the named SW-REQ is the right child? No. The hop observes that a live software id, a code link, or a test link is present. It does not score the sentence.

Does a quiet hop prove the Go matches the shall? No. The hop observes links. It does not prove the Go.

Does an unrealized SYS-REQ fail the merge? No by default. The check keeps warning severity. You can still advance.

Is zero SYS-REQs a complete chain? No. Zero decomposable rows is a pass of this hop, not a system-to-software chain.

Is this characterization testing? No. That page is rewrite-with-a-ledger. This hop is a SYS-REQ with no downward realization. See characterization testing and mirrors.

Is Proof an LDRA alternative for the instrument? No. LDRA still owns the avionics toolchain. Proof vs LDRA.

Is Proof a Jama alternative for the shall? No. Jama still authors. Proof vs Jama.