We will build the machine from pure mathematical axioms, one atomic definition at a time. Every claim will be supported by its formal definition.

---

Axiom 1: The Machine State as a Tuple

A 64-bit x86-64 CPU is a discrete deterministic state machine.
Its core state at any discrete clock step $t$ is a mathematical tuple:

$\mathcal{S}_t = \langle \mathcal{R}, \mathcal{M}, \text{rip} \rangle$

1. Registers ($\mathcal{R}$): A finite set of sixteen named 64-bit words:

$\mathcal{R} = \{ \text{rax}, \text{rbx}, \text{rcx}, \text{rdx}, \text{rsi}, \text{rdi}, \text{rbp}, \text{rsp}, \text{r8} \dots \text{r15} \}$

Each register is a function mapping a register name to an integer in $\{0, \dots, 2^{64}-1\}$:

$\mathcal{R}: \text{Name} \to \mathbb{W}_{64}$

2. Memory ($\mathcal{M}$): A contiguous byte-addressable array:

$\mathcal{M}: \mathbb{W}_{64} \to \mathbb{W}_{8}$

Reading an 8-byte word (64 bits) from address $a$ means
fetching the 8 consecutive bytes starting at address $a$:

$\mathcal{M}_{64}[a] = \sum_{k=0}^{7} \mathcal{M}[a+k] \cdot 2^{8k} \quad (\text{Little-Endian representation})$

3. Instruction Pointer ($\text{rip}$): A single 64-bit scalar holding the memory address of the next instruction to execute:

$\text{rip} \in \mathbb{W}_{64}$

---

Axiom 2: Operand Syntax (Source $\to$ Destination)

In x86-64 AT&T syntax, an instruction is a transition function $\mathcal{T}: \mathcal{S}_t \to \mathcal{S}_{t+1}$.The general syntax is strictly:

$\text{OPCODE} \quad \text{Source}, \quad \text{Destination}$

• Rule of Data Flow:

The value is read from $\text{Source}$, modified by $\text{OPCODE}$, and written to $\text{Destination}$.

• The Dollar Sign Prefix ($):

Denotes an immediate constant (a pure mathematical scalar $c \in \mathbb{Z}$).

$$0 \implies \text{Value } 0$
$$4 \implies \text{Value } 4$

• The Percent Sign Prefix (%):

Denotes a register name in $\mathcal{R}$.

%rax

Concrete Evidence:

$\text{Instruction: } \texttt{movq \$0, \%rax}$

• Mathematical Definition: $\mathcal{R}_{t+1}[\text{rax}] \leftarrow 0$
• Proof of Direction:
  The source is $0 (left). The destination is %rax (right). The scalar 0 is placed into register rax.

---

Axiom 3: Address Calculation via Parentheses

Parentheses denote Memory Dereferencing (pointer arithmetic).
If $k \in \mathbb{Z}$ is an integer literal and $\text{reg} \in \mathcal{R}$, the notation:

$k(\text{\%reg})$

evaluates to the physical memory location at the address:

$\text{Effective Address} = \mathcal{R}[\text{reg}] + k$

Therefore:

$\texttt{movq } \text{Source}, \quad k(\text{\%reg}) \implies \mathcal{M}_{64}[\mathcal{R}[\text{reg}] + k] \leftarrow \text{Value}(\text{Source})$

Concrete Evidence for -8(%rbp) and -24(%rbp):

Suppose %rbp currently holds the address $1000$ (i.e., $\mathcal{R}[\text{rbp}] = 1000$).

• Case 1: -8(%rbp)

$\text{Effective Address} = 1000 + (-8) = 992$

The instruction movq $0, -8(%rbp) does:

$\mathcal{M}_{64}[992] \leftarrow 0$

• Case 2: -24(%rbp)

$\text{Effective Address} = 1000 + (-24) = 976$

The instruction subq $1, -24(%rbp) does:

$\mathcal{M}_{64}[976] \leftarrow \mathcal{M}_{64}[976] - 1$

Why did the compiler pick $992$ and $976$?

Because each 64-bit integer takes 8 bytes.

• Byte interval for slot 1: $[992, 999]$ (8 bytes wide $\implies$ called sum in C).
• Byte interval for slot 2: $[976, 983]$ (8 bytes wide $\implies$ called n in C).

---

Axiom 4: Arithmetic Transformation Rules

Let us formalize the four basic arithmetic instructions:

Instruction	Formal State Transformation	Plain Meaning
movq S, D	$D \leftarrow S$	Overwrite $D$ with $S$.
addq S, D	$D \leftarrow D + S$	Add $S$ to $D$, store result in $D$.
subq S, D	$D \leftarrow D - S$	Subtract $S$ from $D$, store result in $D$.
cmpq S2, S1	Discard $(S_1 - S_2)$, update $\text{Flags}$	Compare: compute $S_1 - S_2$ only to set flags.

Crucial Detail on cmpq S2, S1:

The comparison computes Destination minus Source ($\text{Second} - \text{First}$).
Therefore, cmpq $0, %rax computes:

If $\mathcal{R}[\text{rax}] > 0$, the result is positive, and the machine records "Greater Than".

Step-by-Step Mathematical Trace of 3 Instructions
Let the initial state at step $t=0$ be:

• $\mathcal{R}[\text{rbp}] = 1000$
• $\mathcal{M}_{64}[992] = 5$ (the value at -8(%rbp))
• $\mathcal{R}[\text{rax}] = 10$

Step 1: movq $0, -8(%rbp)

• Input State: $\mathcal{M}_{64}[992] = 5$
• Transformation: Write immediate constant $0$ to address $1000 - 8 = 992$.
• Output State: $\mathcal{M}_{64}[992] = 0$.

Step 2: addq $7, %rax

• Input State: $\mathcal{R}[\text{rax}] = 10$
• Transformation: $\mathcal{R}[\text{rax}] \leftarrow \mathcal{R}[\text{rax}] + 7 = 10 + 7 = 17$.
• Output State: $\mathcal{R}[\text{rax}] = 17$.

Step 3: subq $1, -8(%rbp)

• Input State: $\mathcal{M}_{64}[992] = 0$
• Transformation: $\mathcal{M}_{64}[992] \leftarrow \mathcal{M}_{64}[992] - 1 = 0 - 1 = -1$.
• Output State: $\mathcal{M}_{64}[992] = -1$ (stored as two's complement 0xFFFFFFFFFFFFFFFF).