# Requirements nothing can test, and a count of the ones nobody has tested yet.
#
# Read with docs/protocol/VERIFICATION.md section 1, which carries the
# reasoning. `cargo xtask check` sorts every **P-nnn** in PROTOCOL.md and every
# **L-nnn** in LINK.md into three buckets: covered by a test named after it that
# can actually fail, declared here, or uncovered.
#
# The two are different words. Uncovered means nobody has written the test.
# Untestable means no test can be written, and it needs a kind and a reason
# somebody argued for in review. Filling this file with `deferred` entries to
# make the count go down turns "we have not written tests" into "these are
# untestable", which is the graveyard this file exists to not become.

# The number somebody defends at each audit round: requirements that are neither
# covered nor declared below.
#
# The check fails when the real count goes above it, and fails when it drops
# below and this number was not lowered with it — a ratchet nobody tightens
# rusts open, and the slack quietly absorbs the next rules nobody covers. It
# started at nearly the whole specification, because when it was written not one
# test in the workspace stood behind a requirement, and a check that is red on
# its first run is a check somebody switches off before its second.
#
# It goes up for exactly one reason: the specification gained a rule. Anything
# else moving it up is a test that stopped standing behind something.
[ratchet]
uncovered = 73

# P-045 is the shape this file is for. Nothing can drive an implementation into
# transmitting a key it does not have, so the thing that stands behind it reads
# the corpus rather than an implementation: every derived key and the printed
# secret, hunted for in the bytes of every MAC'd body in the vectors. The check
# named here has to be one `cargo xtask check` actually runs, or the nomination
# reads as coverage forever.
[[entry]]
id = "P-045"
kind = "spec-check"
check = "no_response_carries_key_material"
reason = """
No test can prove a negative about every implementation. What can be proved is \
that no artefact we publish carries key material, which is what \
no_response_carries_key_material reads out of the vectors — the bytes, not the \
description of the bytes, because an early draft returned the client's \
long-term key in a perfectly well formed pairing response."""

# The subject of P-033 is a connector. A host test cannot tell a board that
# carries RTS/CTS from one that does not, because on the host both are a `Vec`.
[[entry]]
id = "P-033"
kind = "hardware"
reason = """
The requirement is about two wires. It is proved on the bench by a worst-case \
frame ten thousand times at 921600 with flow control, zero CRC failures, and \
the same run with the two lines disconnected, which must fail — proving the \
requirement by demonstrating its absence is the only thing that stops it being \
a sentence. The dated bench log that records it is named here once it exists; \
until a board with the production connector has been run, this entry is what \
says nobody has checked."""
