Extract instruction definitions from Intel manual instead of manually transcribing them

[andrew-johnson-4]

trafficstars

The verifier in Coq could utilize direct definitions provided by Intel.

https://www.felixcloutier.com/x86/pop

IF StackAddrSize = 32
    THEN
        IF OperandSize = 32
                THEN
                    DEST := SS:ESP; (* Copy a doubleword *)
                    ESP := ESP + 4;
                ELSE (* OperandSize = 16*)
                    DEST := SS:ESP; (* Copy a word *)
                    ESP := ESP + 2;
        FI;
    ELSE IF StackAddrSize = 64
        THEN
                IF OperandSize = 64
                    THEN
                        DEST := SS:RSP; (* Copy quadword *)
                        RSP := RSP + 8;
                    ELSE (* OperandSize = 16*)
                        DEST := SS:RSP; (* Copy a word *)
                        RSP := RSP + 2;
                FI;
        FI;
    ELSE StackAddrSize = 16
        THEN
                IF OperandSize = 16
                    THEN
                        DEST := SS:SP; (* Copy a word *)
                        SP := SP + 2;
                    ELSE (* OperandSize = 32 *)
                        DEST := SS:SP; (* Copy a doubleword *)
                        SP := SP + 4;
                FI;
FI;
Loading a segment register while in protected mode results in special actions, as described in the following listing.
These checks are performed on the segment selector and the segment descriptor it points to.
64-BIT_MODE
IF FS, or GS is loaded with non-NULL selector;
    THEN
        IF segment selector index is outside descriptor table limits
                OR segment is not a data or readable code segment
                OR ((segment is a data or nonconforming code segment)
                    AND ((RPL > DPL) or (CPL > DPL))
                        THEN #GP(selector);
                IF segment not marked present
                    THEN #NP(selector);
        ELSE
                SegmentRegister := segment selector;
                SegmentRegister := segment descriptor;
        FI;
FI;
IF FS, or GS is loaded with a NULL selector;
        THEN
                SegmentRegister := segment selector;
                SegmentRegister := segment descriptor;
FI;
PREOTECTED MODE OR COMPATIBILITY MODE;
IF SS is loaded;
    THEN
        IF segment selector is NULL
                THEN #GP(0);
        FI;
        IF segment selector index is outside descriptor table limits
                or segment selector's RPL ≠ CPL
                or segment is not a writable data segment
                or DPL ≠ CPL
                    THEN #GP(selector);
        FI;
        IF segment not marked present
                THEN #SS(selector);
                ELSE
                    SS := segment selector;
                    SS := segment descriptor;
        FI;
FI;
IF DS, ES, FS, or GS is loaded with non-NULL selector;
    THEN
        IF segment selector index is outside descriptor table limits
                or segment is not a data or readable code segment
                or ((segment is a data or nonconforming code segment)
                and ((RPL > DPL) or (CPL > DPL))
                    THEN #GP(selector);
        FI;
        IF segment not marked present
                THEN #NP(selector);
                ELSE
                    SegmentRegister := segment selector;
                    SegmentRegister := segment descriptor;
            FI;
FI;
IF DS, ES, FS, or GS is loaded with a NULL selector
    THEN
        SegmentRegister := segment selector;
        SegmentRegister := segment descriptor;
FI;