is_ASMcore predicate

is_ASMcore is a well-formedness predicate for assembler configurations represented by the ASMcoret record. In the referenced Isabelle model, register contents are integers and a register file is modeled as a list of such integers. The ASMcoret record contains delayed and current program-counter fields (dpc, pcp), general-purpose registers (gprs), special-purpose registers (sprs), and memory (mm). [C1]

The predicate exists because the assembler-level representation of addresses and values is less restrictive than the bit-vector representation, and because the registers type itself does not encode the required number of registers. is_ASMcore therefore restricts configurations to meaningful assembler states. [C2]