44Verification

Repair a false always-ready contract

Situation

BufferedSink.put forwards an enqueue request to a one-entry FIFOF. The interface claims permanent readiness even though a bounded queue cannot accept another value while full. Compilation reports the contradiction before the public simulation can drain the value.

Only the interface contract is wrong. Preserve the queue, both method bodies, and the supplied mkTop sequence.

Read and predict before editing

Read in this order:

1. Find the protocol attribute on the put prototype.
2. Follow put into entries.enq and identify the queue depth.
3. Follow take through first and deq.
4. Trace step: one rule fills the queue, then another drains it.

Before Run, predict the compiler result rather than the final printed value. entries.enq has an implicit condition derived from free capacity, so the compiler cannot prove that put is ready in every state. The diagnostic names the assertion, but the root cause is the full state of the enclosed FIFOF.

Make the minimal change

Make the interface expose the real state-dependent handshake for put. Change only the inaccurate protocol declaration; do not replace FIFOF, enlarge it, add an explicit fullness test, or rewrite the enqueue method. A Ready signal is the intended representation of backpressure here.

The minimal reasoning is: empty permits enqueue, full blocks enqueue, therefore readiness is not a constant property. Removing a false promise does not remove functionality; it lets callers observe the condition already present in the method implementation.

Observable completion

Run compiles and simulates successfully. The value accepted by fill is the same value returned by drain, and the one-entry capacity remains unchanged. At the reusable module boundary, put is ready while capacity is available and not ready while the sole entry is occupied. This state contract prevents a solution that merely hard-codes the supplied 8'h5a observation.

Progressive hints

Transfer experiment

After the required repair, temporarily change the queue depth to two and imagine two consecutive put calls without take. Predict the occupancy after each accepted call and the cycle in which Ready becomes false. Revert the depth before submitting; the experiment is not graded.