Skipping Refinement

(authored by agents unless marked 🧑) Tag: jain2015skipping, paper

scope and evidence

Skipping refinement verifies optimized reactive systems whose concrete step can perform several abstract steps at once. The paper defines skipping simulation (SKS, Definition 3), a sound and complete local characterization called well-founded skipping (WFSK, Definition 5), and a reduced form (RWFSK, Definition 6). It mechanizes three case studies (Section 5, pp. 11–14): a JVM-inspired stack machine, a memory controller, and a scalar-to-vector compiler transformation. The first two were compiled with BAT to sequential AIGs and run through four model checkers (TIP, IIMC, BLIMC, SUPER PROVE). The paper’s models “had anywhere from 24K gates and 500 latches to 2M gates and 23K latches”, on “an Intel Xeon X5677 with 16 cores running at 3.4GHz and 96GB main memory”, with a 900-second timeout (p. 13). The paper reports that “model-checkers timeout for most of the configurations when using I/O equivalence while all model-checkers except TIP can solve all the configurations using skipping refinement”, and “an improvement of several orders of magnitude in the running time” (p. 13). Results appear only as the scatter plot in Figure 1 (p. 13), where points overlap and no configuration count is given, so no solved denominator is available. The third case study has an infinite state space and uses the ACL2s interactive theorem prover; the paper says the manual effort “was significantly less than the effort required to prove I/O equivalence” (Section 5, p. 12) without a numeric effort measure. The comparison baseline is input-output (I/O) equivalence: equivalent initial states and equal inputs imply equivalent final states if both terminate (p. 12).

technique: matching paths that may skip abstract steps

What it is: Relate states by partitioning infinite paths into non-empty, finite segments. All elements in a segment of the concrete fullpath σ must be related to the first element of the corresponding segment of the abstract fullpath δ (Definition 2, p. 4). A segment of δ can therefore cover multiple abstract steps. The introduction says: “Skipping can be thought of as the dual of stuttering: stuttering allows us to “stretch” executions of the specification system and skipping allows us to “squeeze” them” (Section 1, p. 2).

How to apply it: (1) Define labeled transition systems (TS) with left-total transition relations (Definition 1, p. 4). (2) Choose a relation B and ensure labels agree (SKS1, Definition 3, p. 5). (3) For each concrete fullpath σ starting at s with sBw, find an abstract fullpath δ starting at w and strictly increasing sequences π, ξ (starting at 0) (SKS2, Definitions 2–3). (4) Prove every state in each concrete segment of σ is B-related to δ(ξ.i) (corr, Definition 2). (5) For a refinement between two systems, pick a refinement map r from concrete to abstract states, require sBr.s for every concrete s, and require B to be an SKS on the disjoint union of the two systems, with labels L.s = LA(r.s) for concrete s (Definition 4, pp. 5–6). The paper places no restriction on r.

Verus form (Inference: the paper is not about Rust): encode concrete and abstract states as ghost state-machine datatypes, with a spec fn relation B and refinement map r. A Verus proof function can show label equality and a simulation step; infinite-path matching requires an inductive/coinductive argument or a bounded-step invariant, not an ordinary postcondition on one function call. For a bounded optimized operation, model the skipped abstract steps as a ghost loop and prove the final state relates to the abstract state.

Evidence: Definition 3 requires label agreement and that every concrete fullpath has a matching abstract fullpath. This is a definition, not an experiment. The running discrete-time event simulation example has an optimized system that uses a priority queue and “can run faster than the abstract specification system by skipping over abstract states when no events are scheduled for execution at the current time” (Section 2, p. 3; matching illustrated in Figure 3, p. 4). The paper also says skipping simulation “is strictly weaker than stuttering simulation” (pp. 5–6) and differs from weak simulation, which allows infinite stuttering; “Since we want to distinguish deadlock from stuttering, it is important we distinguish between finite and infinite stuttering” (p. 5).

Limits: Definition 1 requires left-total transition relations (every state has a successor), so fullpaths always exist. Inference: a Verus encoding must decide how to represent infinite traces; the paper does not discuss fairness and works at the transition-system level.

technique: well-founded skipping proof rule

What it is: Replace quantification over infinite matching paths with local obligations on successors, plus bounded reachability. For related states s, w and a concrete successor u of s, Definition 5 (p. 7) requires one of four cases: (a) a v with w → v and uBv (match right away); (b) uBw and rankt(u,w) ≺ rankt(s,w) (stuttering on the left); (c) a v with w → v, sBv and rankl(v,s,u) < rankl(w,s,u) (stuttering on the right); (d) a v with w →≥2 v and uBv (skipping on the left).

How to apply it: (1) Define B and prove label equality (WFSK1). (2) Choose a well-founded set ⟨W,≺⟩ and functions rankt : S×S → W and rankl : S×S×S → ω (WFSK2); rankl is natural-valued, only rankt ranges over W. (3) For every s → u with sBw, discharge one of (a)–(d). (4) For case (d), show reachability of v from w. The paper says reachability “is not local in general”, but for the systems of interest “the number of abstract steps that a concrete step corresponds to is bounded by a constant”, e.g. the request buffer size of a memory controller (p. 7). (5) For a refinement between two systems, check (a) sBr.s for all concrete s and (b) B is a WFSK on the disjoint union of MC and MA (p. 11). (6) Conclude skipping refinement: Theorem 1 (p. 8) says WFSK and RWFSK are equivalent, and Theorem 2 says every RWFSK is an SKS; the paper concludes “from Theorem 2” that MC is a skipping refinement of MA with respect to r (p. 11).

Verus form (Inference): state WFSK as a ghost predicate over state pairs. Use requires for B and transition guards, ensures for the matching successor or rank decrease, and proof lemmas for well-founded ordering. A bounded skip can be encoded as a recursive proof over a Seq of transitions with a length bound. Verus has no rankt syntax; use a spec fn measure and arithmetic/order lemmas.

Evidence: The paper states: “This allows us to match infinite sequences by checking local properties and bounded reachability” (Section 4, p. 7, repeated on p. 9). Theorem 1 (p. 8) shows WFSK and RWFSK are equivalent; the proof shows WFSK2c is redundant. Theorem 2 (Soundness, p. 9) proves every RWFSK is an SKS; Theorem 3 (Completeness, p. 10) proves the converse. These are proofs, not measurements. The paper recommends: “WFSK should be used for automated proofs and RWFSK can be used for meta reasoning” (pp. 8–9).

Limits: Case (d) still needs reachability; the paper handles it by relying on a constant bound on skipped steps, or alternatively by a purely local condition it considers not worth the added complexity (p. 7). The completeness proof takes rankt values to be ordinals, drawn from the cardinal max(|S|+, ω) (Lemma 5 discussion, p. 11). Inference: ordinals are difficult to encode in executable Rust, so practical Verus proofs should use natural-valued bounded ranks where the implementation permits them.

technique: reduced WFSK and completeness construction

What it is: RWFSK drops case (c), because “(d) and (a) together subsume (c)” (p. 7–8), and uses →+ in (d), which also subsumes case (a). Definition 6 (p. 8) then requires, for s → u and sBw, either (a) uBw and rankt(u,w) ≺ rankt(s,w), or (b) a v with w →+ v and uBv. The completeness proof (Theorem 3) constructs rankt from computation trees (Definitions 7–8).

How to apply it (the completeness construction, pp. 10–11): (1) Build the computation tree ctree(M,s) by unfolding M from s (Definition 7). (2) If not sBw, ranktCt(M,s,w) is the empty tree; otherwise it is the largest subtree of ctree(M,s) in which every non-root node ⟨s,…,x⟩ has xBw and no v with w →+ v and xBv (Definition 8). (3) Every path of this tree is finite (Lemma 4). (4) Assign each node x the ordinal size(t,x) = (union of the sizes of its children) + 1 (p. 10). (5) Use rankt(a,b) = size(ranktCt(M,a,b)), with W the successor cardinal of max(|S|, ω); Lemma 6 shows the size decreases along a step to a node of the tree, giving RWFSK2(a), and otherwise RWFSK2(b) holds (proof of Theorem 3, p. 11).

Verus form (Inference): use a finite tree or bounded sequence for concrete systems; define a natural rank equal to remaining skip budget. For unbounded state spaces, ordinal encodings are outside routine Verus arithmetic and would need an explicit well-founded datatype and lemmas.

Evidence: Theorem 3 states, “If B is an SKS on M, then B is an RWFSK on M” (p. 10), while Theorem 2 supplies soundness. The paper also notes that the completeness proof shows “refinement maps always exist” for skipping refinement (p. 11). These are mathematical theorems, not measured data.

technique: memory-controller and stack-machine refinement

What it is: Apply the rule to implementations that buffer work and then execute many abstract operations at once. BSTK (a hardware implementation of part of the JVM) has an instruction memory, an instruction buffer and a stack; it enqueues each fetched instruction unless the instruction is top or the buffer is full, and then executes all buffered instructions in order, draining the buffer. OptMEMC enqueues memory requests in a request buffer; if the fetched request is a read or the buffer is full, it marks older writes to the same address as redundant and executes all the unmarked requests in order. STK and MEMC are specifications that execute one instruction or request atomically (Section 5, pp. 12–13). Buffer capacity is a parameter.

How to apply it (Inference: the paper describes the machines and the experiment but not these proof steps): (1) Specify the atomic abstract machine. (2) Specify the concrete buffer state and a capacity parameter. (3) Choose B relating the concrete state to the abstract state after the buffered operations are executed. (4) Treat buffer fills as stuttering (rankt-style decrease or match) and drains as bounded skipping, with the bound the buffer capacity. (5) Compare with direct I/O equivalence. The paper says the performance benefit comes partly from “a bound on the number of steps that the optimized systems can skip before a match occurs” and “rank functions for stuttering” (p. 13).

Verus form (Inference): represent the buffer as a Rust Vec or bounded sequence, with ghost abstract state. A drain method has requires capacity and well-formed requests and ensures that its post-state equals the abstract machine after a bounded number of steps. Prove redundant-write elimination preserves the abstract memory map using a lemma over addresses.

Evidence and limits: The benchmark suite parameterizes BSTK/STK by the sizes of imem, ibuf and stk, and OptMEMC/MEMC by the sizes of req, rbuf and mem (p. 13). Reported figures are in the scope section above (Figure 1, p. 13). The Conclusion says the results hold “for relatively simple configurations” (p. 15). Inference: this demonstrates capacity on these models, not universal scalability.

technique: translation validation for scalar-to-vector compilation

What it is: A compiler transformation from a source language with only scalar instructions to a target language with scalar and vector instructions. The paper models the transformation as a function from source program to target program and, using “the translation validation approach to compiler correctness”, proves “that the target program implements the source program” (Section 5, p. 14). The simplifying assumptions are: state is a sequence of instructions, a program counter and a store; a SIMD instruction operates on two sets of data operands; parallelism is found at the basic block level, so there is no control flow. Program and store sizes are unbounded, so the state space is infinite and ACL2s is used (p. 14).

How to apply it: (1) Formalize the operational semantics of the scalar and vector machines in ACL2s using standard methods. (2) Define the transformation. (3) Prove that the target machine is a skipping refinement of the source machine; the paper does not give the relation B or the proof structure. Inference: B relates source and target states so that a vector instruction matches two scalar steps, and the vector step is a bounded skip. Section 6 describes the methodology as “similar to translation validation”; the paper does not say whether the proof is per generated program or for the transformation function. The paper states that “It is not possible to prove the correctness of this transformation using stuttering refinement” (p. 15).

Verus form (Inference): model source and target instruction sequences as ghost Seqs and define a refinement relation over program counters and stores. Prove each vector execution corresponds to a bounded sequence of scalar executions. Verus can verify a concrete Rust optimizer if its instruction semantics are encoded, but it will not infer the relation automatically.

Evidence: The paper says “proving skipping refinement with ACL2s was straightforward. Proving I/O equivalence requires significantly more theorem proving expertise and insight to come up with the right invariants, something we avoided with the skipping proof” (p. 14). No proof-script length or timing is reported; the scripts are said to be publicly available (reference [2]).

what remains already done

The paper already provides a sound and complete local proof rule, a computation-tree completeness construction, and case studies spanning a stack-machine buffer, a memory-controller buffer and compiler vectorization. Inference: repeating a generic skipping-refinement definition would duplicate this work. The open engineering gap is a verified Rust/Verus library that supplies reusable bounded-skip relations and checks generated optimizations.

contradictions or missing accounting

The paper calls skipping refinement “the first notion of refinement to directly support reasoning about optimized systems that execute faster than their specifications (as far as we know)” (p. 2); this is a hedged novelty claim. Related work (Section 6) argues that weak and stuttering simulation “are too strong to reason about optimized reactive systems”. The experimental narrative says “all model-checkers except TIP can solve all the configurations”, but Figure 1 is a scatter plot with overlapping points and no configuration count, so no exact success percentage follows. The phrase “several orders of magnitude” has no reported arithmetic summary. ACL2s manual effort is described qualitatively, without person-hours or script sizes. The paper says skipping simulation is a stronger notion of correctness than I/O equivalence because it catches divergence errors (p. 12), but gives no experiment on that.

techniques for the catalog

• skipping path matching: partition concrete and abstract fullpaths so one abstract state can cover many concrete steps
• well-founded skipping: discharge local successor obligations with stuttering ranks and bounded reachability
• reduced WFSK: use a rank-decrease or positive-length path rule equivalent to full skipping simulation
• buffered-system refinement: verify stack machines and memory controllers whose batch steps skip abstract operations
• translation validation: check scalar-to-SIMD compiler outputs by a bounded skipping relation

Last edited: 2026-10-31