Stage 4 closes the two arguments every earlier stage leaned on: the induction step with its helper assertions, and the signoff package with its ledger. The counter lesson shows why a true property can fail its induction step and what repairs it, the FIFO shows the same shape on a larger design, and a small counter module shows a proof that passes with a fault planted. The signoff lesson assembles bounds, discharged assumptions and waivers. The manifest lesson runs every ledger check and then points you to the Solutions topic, which holds the causes of all 16 planted faults and the reference ledger.
Lesson | After it you can... |
|---|---|
Find the helper that closes an induction, measure the minimal window, and judge a proof that passes with a fault planted. | |
Justify each bound from a cover step and check waivers for owner, age and revision. | |
Run the manifest, demonstrate that every check can fail, and prepare the review answers. |
Suggested order: top to bottom. Induction first, because ledger rows claim proven status that only a passing induction justifies; the package next; the manifest last. When your package passes, continue with Solutions and compare every cause, killing property and fix with your own.
Ledger rows claim proven status, and only a proof that closes justifies that word. The package files the claims the induction lesson earns.