Abstract State

In the context of verified faithful simulation of processors, an abstract state is the formal, machine-checked representation of a processor's state used as the reference specification, against which a concrete implementation is verified.

Definition and Role

In the work on verified faithful simulation of the ARM V6 instruction set, the abstract state is the state of the ARM V6 processor as defined in the Coq formal model. It is paired with a concrete state, which is the same processor state represented using C data structures and the CompCert C memory model.

"The state of the ARM V6 processor defined in the formal model is called the abstract state. Alternatively, the same state is represented by the data structures corresponding to C semantics that we shall call the concrete state."

The abstract state is the reference artifact: the C instruction-set simulator (ISS) is considered correct only if its executions can be projected back to the abstract state in a way that matches the formal specification.

Components

The abstract state models the relevant pieces of the ARM V6 architecture, including:

• A processor state field (with subfields such as Proc_state, SCC)
• The status registers CPSR and SPSR
• The register file reg
• The memory mem
• An exceptions field exns

In the abstract Coq model, the processor state is referenced directly as st.

Projection to the Concrete State

Because the C implementation uses complex, optimized data structures (large embedded structs expressing the ARM processor state), relating it back to the abstract model is non-trivial. This is done through a projection — a function that constructs a formal structure from the concrete one.

"The formal structure obtained should be identical to that obtained through the formal model, otherwise the C code is incorrect."

The proof of projection must cover each variant case of the concrete representation. For example, the projection of a register performs a case analysis on possible values, while the projection of saved data upon exceptions depends on the exception mode. The C-side model of the state is a complex Coq record type, including not only data fields but also proofs verifying access permission, next-block pointer, etc.

Characteristics of the Abstract Model

Several design choices are highlighted for the abstract state and its transitions:

• The global state is based on a memory model with load and store functions used for read/write operations.
• Transitions are defined in a relational style rather than a functional one. Relational style is more flexible, especially when dealing with constraints, and fits well with operational semantics.
• The C implementation uses two environments consistent with CompCert C semantics:
  • A global environment genv mapping global function and variable identifiers to memory blocks, and function pointers to function definition bodies.
  • A local environment env mapping local variables of a function to their memory block references, with values stored in the associated memory blocks.

Verification Method

The correctness theorem for an ARM instruction states that executing the same instruction on a pair of equivalent states (one concrete, one abstract, related by the projection) should produce a new pair of equivalent states. Formally, for each instruction, the proof demonstrates that:

1. The operational semantics of the C code (the concrete state) corresponds to the ARM formal specification (the abstract state).
2. The projection from the resulting concrete state is related to the new abstract state produced by running the formal model.

The proof proceeds in a top-down manner, following the definition of the instruction: the function body is split into statements and then into expressions, tracking how the memory state changes on the concrete side and comparing the results against the abstract side.