Relate concrete service steps to an abstract contract

Suppose concrete state contains staged requests and a durable set D of committed logical identifiers, each associated with one immutable increment amount. An abstract counter can be the sum of amounts for identifiers in D. Staging packets and retransmitting them leave that sum unchanged; recording a new committed identifier changes it once. This definition relies on durable membership and payload uniqueness, not on the number of received packets. A bag of duplicate log records cannot be substituted for a set of unique committed effects without another invariant explaining their interpretation.

The abstract observation set limits the conclusion. If the abstraction includes only the counter, sending a response may leave abstract state unchanged. That can support a counter-state argument but cannot alone establish that responses have correct contents or timing. If client-visible replies are part of the contract, include their relevant history or state and map them too. Likewise a durable record that can disappear after an allowed restart may not justify a permanent abstract commitment. Specify recovery and the evidence that the chosen durable boundary actually preserves the mapped fact.

First show that each concrete initial state maps to an abstract initial state. Then show that every concrete step from the maintained concrete invariant maps either to an allowed abstract step or to no change in the abstract variables. The latter is stuttering: an internal implementation step makes no difference at this abstraction level. The concrete invariant may be essential to the simulation argument, because arbitrary malformed concrete states can map to impossible abstract transitions. Check message delivery, duplicate handling, recovery, and exceptional responses rather than proving only the happy-path commit case.

One source-level function of current state is not always enough for a convenient refinement proof. Auxiliary history can retain information that the implementation discarded, and prophecy-style constructions can help relate nondeterministic choices whose justification depends on later behavior. Such variables need their own sound introduction rules; they must not constrain implementation behavior merely to make a proof pass. For practical review, start with a clear mapping and state exactly which invariant and observable traces it preserves before introducing more sophisticated machinery.

A concrete machine may perform internal retries forever while its abstract counter never changes. Every concrete step could then satisfy the stuttering branch of the safety simulation, yet an abstract promise of eventual commitment would fail. Prove that the concrete progress assumptions imply the abstract progress requirements; a safety mapping does not supply this automatically. Similar care is needed when a response action is abstractly visible: calling it stuttering by omitting the response variable weakens the specification rather than proving the original client contract.

The quadratic instrument illustrates a many-to-one observation map. Reset, set a=1 and x=1, predict y=1, then Play or Step. Separately Reset, set a=1 and x=−1, predict y=1 again, then Play or Step. Distinct input states can have the same chosen output observation, while tangent slopes and signed areas differ. The instrument is only y=ax² and does not implement service refinement, history variables, or temporal proofs. It makes the narrower point that an abstraction can deliberately forget distinctions, so the preserved observations must be named.