46Verification

Repair a false implicit-condition contract

Situation

consume has an explicit active predicate, but it also reads and removes an entry from a bounded FIFOF. Its scheduling attribute claims that called methods add no implicit conditions. Compilation rejects that claim because an empty queue cannot provide first or perform deq.

The queue behavior, state updates, interface, and supplied mkTop are trusted. Only the rule's scheduling contract is editable for this repair.

Read and predict before editing

Read in this order:

1. Record the initial values of active, doneReg, and resultReg.
2. Find every method called by consume, including value and action methods.
3. Separate the explicit active predicate from queue readiness.
4. Trace mkTop through fill, start, and show.

Before Run, predict compilation first. The source assertion requires active to be the only condition controlling consume, but queue.first and queue.deq are unavailable when the queue is empty. That contradiction is detected during scheduling; it is not a simulation timeout and not evidence that active is wrong.

Make the minimal change

Allow the compiler to retain the queue methods' actual implicit conditions. Preserve the explicit predicate, all queue operations, and every register update. Do not add queue.notEmpty to the rule guard: it can describe equivalent control, but it is unnecessary scope and would obscure the lesson that method readiness already participates in the rule condition.

The minimal reasoning is: consume may fire only when active is true and an entry is available. The rule needs that conjunction rather than an assertion that readiness is constant.

Observable completion

Run compiles and follows the intended state sequence: fill stores the supplied byte, start makes the consumer active, and consume later commits that byte to resultReg while setting doneReg. show observes the same byte only after done becomes true. If start occurred with an empty queue, consume would wait instead of reading invalid data; that empty-state behavior is part of completion.

Progressive hints

Transfer experiment

After completing the repair, temporarily reorder the top-level sequence so start happens before fill. Predict which rule waits, which implicit condition changes after enqueue, and why no invalid dequeue occurs. Revert the sequence before submitting; it is not graded.