A passing proof is a claim, and this section is how the claim is audited. Every implication gets a cover of its trigger so no pass is vacuous; coverage is measured over cones, proof cores, assumptions and mutants so no logic goes unexamined; bounded results carry justified bounds so no depth is arbitrary; and the whole package assembles into a ledger a reviewer can defend line by line. The running evidence comes from the arbiter, the skid-buffer bridge, the decade counter and the FIFO, with real runs at every step.
Topic | What it covers | After it you can... |
|---|---|---|
Trigger covers, witness traces, over-constraint alarms, bounded-miss wording, mutation checks. | Pair every check with a cover and read the witness. | |
Cone versus core, assumption influence, mutation score, and what the numbers cannot say. | Measure what the proofs touched, leaned on, and bit. | |
Bound justification, the status ledger, waivers with evidence, staleness control. | Accept a bounded result only with a defended bound and a clean ledger. | |
The full checklist, the worked FIFO package, and the joint ledger with simulation. | Assemble and defend a complete sign-off. |
Suggested order: top to bottom. Covers first, because every later topic assumes the vacuity habit; metrics next, because they qualify every number; bounded sign-off next, because it turns numbers into decisions; the package last, because it assembles everything. Readers under time pressure take seven lessons: Antecedent Covers and Witness Traces, Over-Constraint Seen Through Covers, Proof Core and Cone Coverage, Mutation-Based Formal Coverage, Justifying a Bound, and The Signoff Checklist in Full, in that order, then the worked package for sync_fifo.
The diagram is the evidence ledger a reviewer reads. A result sits at the root. Under it hang the evidence that the result means something: vacuity evidence (covers and mutants) and coverage (cone and proof core). Under those sit what the evidence rests on and what stays open: the assumption register and the waivers. Each topic of this section fills one box.
The result box: a bounded status is valid only with its bound and its justification, so the row stays open and cannot reach the package. The bounded-proof topic owns that rule, and the other boxes cannot make up for it.