A newcomer proposes to verify the FIFO by visiting every state. The FIFO has 39 state bits, and visiting 2 to the 39 states at a billion a second takes under ten minutes, so the idea sounds fine until the inputs and the storage are counted. The same newcomer then assumes away much of the input space without recording it, and the proof passes on a slice nobody can name. Both mistakes are arithmetic, and both are cheap to prevent once the numbers are written down.
Job of this lesson: compute state counts, show what explicit enumeration really costs, and quantify how assumptions shrink the input space.
N state bits mean 2 to the N states, and every extra bit doubles the space. Visiting the states is not the whole cost: every state has one successor for each input value (11 free input bits for the FIFO, so 2,048 successors), and the visited set must be stored. The tool therefore reasons about sets of states symbolically. Assumptions shrink the input space; for independent input fields the kept fractions multiply, and each excluded class must be verified elsewhere or the proof has a hole shaped exactly like the exclusion.
The first script derives the FIFO figures: 2 to the 39 states is 549,755,813,888, visited in about 550 seconds at a billion a second; times 2,048 input choices it is 1.1 times 10 to the 15 transitions, about 13 days; one bit per state of storage is 64 GiB. The 158-bit example (three 8-bit registers, a 4-bit counter, a 2-bit machine and a 16 by 8 memory) needs about 10 to the 31 years. The check is applied to the correct functions and to a mutant that squares the bit count, which it catches.
def states(bits):
return 2 ** bits
def years(bits):
return states(bits) / 1e9 / 31_557_600
def check(states_fn, years_fn):
assert states_fn(39) == 549755813888
assert states_fn(24) == 16777216 and states_fn(18) == 262144
seconds = states_fn(39) / 1e9
assert 549 < seconds < 550
inputs = 1 + 1 + 8 + 1
assert 2 ** inputs == 2048
days = states_fn(39) * 2 ** inputs / 1e9 / 86400
assert 13.0 < days < 13.1
assert states_fn(39) // 8 == 64 * 2 ** 30
bits = 24 + 4 + 2 + 128
assert bits == 158
assert 1.1e31 < years_fn(bits) < 1.2e31
check(states, years)
caught = False
try:
check(lambda b: b * b, years)
except AssertionError:
caught = True
assert caught
print("PASS: 2^39 is 550 s of visiting, 13 days with the input choices, 64 GiB of storage; 158 bits need about 1e31 years; a wrong power is caught")A 4-bit opcode with the assumption “opcodes above 10 never occur” keeps 11 of 16 values. A word-alignment assumption on the two low address bits keeps 1 of 4. For independent fields the kept fractions multiply: 11/16 times 1/4 is 11/64, about 17.2 percent, so 82.8 percent of the combined space is excluded and every bug that hides there is invisible. The product holds only for independent fields: an assumption that couples them, such as “an unaligned address is allowed only with opcode 0”, keeps 14/64, not 11/64. The script enumerates the combinations, checks the product, and catches the calculator that forgets to multiply.
from fractions import Fraction as F
def kept(opcode_ok, address_ok):
ok = total = 0
for opcode in range(16):
for low in range(4):
total += 1
ok += 1 if (opcode_ok(opcode) and address_ok(opcode, low)) else 0
return F(ok, total)
independent = kept(lambda o: o <= 10, lambda o, low: low == 0)
coupled = kept(lambda o: o <= 10, lambda o, low: low == 0 or o == 0)
def check(combine):
assert independent == combine(F(11, 16), F(1, 4)) == F(11, 64)
assert abs(float(independent) - 0.171875) < 1e-12
assert 1 - independent == F(53, 64)
assert coupled == F(14, 64) != combine(F(11, 16), F(1, 4))
check(lambda a, b: a * b)
caught = False
try:
check(lambda a, b: a)
except AssertionError:
caught = True
assert caught
print("PASS: 11 of 64 combinations remain for independent fields, 14 of 64 when the fields are coupled; forgetting the product is caught")State counts are quoted as powers of two with the reachable share beside the total.
No plan proposes enumeration without counting the input choices and the storage.
Every assumption that removes input space names the excluded class and where it is verified instead.
Recompute the kept fraction whenever an assumption is added: the excluded share is where the next bug hides. If a proof is suspiciously quick after a new assumption, suspect the fraction moved, not the engine. Record each excluded class in the assumption register, the list of every assumption with the reason it is safe and where it is checked.
11/64, about 17.2 percent. The reviewer demands each excluded class named with where it is verified instead: opcodes above 10 and unaligned addresses are now invisible here.
Each assumption compounds, so 68.8 percent kept and then a quarter of that leaves 17.2 percent, not 68.8. The product assumes independent fields; coupled assumptions must be enumerated.