Every proof is relative: it holds under its assumptions, and an assumption is a promise that something else keeps. A wrong assumption does not make a proof fail. It makes the proof pass while the chip fails. This topic turns assumptions into a managed contract: six kinds with owners, the rule that places each assumption and assertion on its side of an interface, a review that probes for over-constraint, and the conversion that checks at integration what each block assumed.
Lesson | After it you can... |
|---|---|
Classify an assumption by kind, owner, discharge target and lifetime, and show it is load-bearing. | |
Place a rule on the right side of an interface and see both wrong placements fail. | |
Run the review: ledger, discharge, covers, mutation and the share of input space removed. | |
Convert a block-level assumption into an assertion on the neighbour and find the bug the unit proof hid. |
Suggested order: top to bottom. The taxonomy gives the vocabulary, the side rule removes most placement errors, the review is the gate, and the conversion checks at integration what the review lists.
Suspicious. Either the block really is self-contained, or the rules it depends on were never written down. Check what the design assumes about reset, inputs and configuration.