A binary has no obligation to resemble the source program that produced it. Variables have become registers. An integer comparison has become a subtraction followed by a test of condition flags. A source-level expression may have disappeared into an addressing calculation. Before we can simplify any of that, we need a precise account of what the remaining instructions do. HydIR makes these questions explicit at several levels. Its native pipeline carries decoded instructions through MachineIR, StateIR, FunctionIR, and CIR before producing C. A separate scalar compatibility path translates a restricted function into LLVM IR. The [architecture guide](/architecture) explains how those paths fit together. We will begin with a deliberately small example: a maximum function with two 64-bit inputs in RDI and RSI and a result in RAX. That projection lets us derive the arithmetic and branch conditions without carrying an entire machine through every equation. We will then extend the model to partial register writes and uncertain effects. These derivations are specifications and worked arguments; the implementation and its tests supply separate evidence. ## A word has two interpretations Let $\BV_w$ be the set of words with exactly $w$ bits. We write $u(x)$ for the unsigned integer represented by a word and $s(x)$ for its two's-complement signed interpretation. $$ {#word-interpretations} \begin{aligned} \BV_w &= \{0,1\}^{w}, \qquad M = 2^w,\\ u(x) &= \sum_{i=0}^{w-1} x_i 2^i,\\ s(x) &= \begin{cases} u(x), & u(x)<2^{w-1},\\ u(x)-2^w, & u(x)\ge 2^{w-1}. \end{cases} \end{aligned} $$ Neither interpretation changes the bits. For an eight-bit word, `11111111` represents $255$ under $u$ and $-1$ under $s$. Consequently, `11111111` is greater than `00000001` in unsigned order and less than it in signed order. Addition and subtraction have an especially useful property: their low $w$ result bits agree under either interpretation. We can calculate them in the quotient ring $\mathbb Z/2^w\mathbb Z$: $$ {#modular-arithmetic} \begin{aligned} u(a +_w b) &= \bigl(u(a)+u(b)\bigr)\bmod M,\\ u(a -_w b) &= \bigl(u(a)-u(b)\bigr)\bmod M. \end{aligned} $$ This is a ring, generally not a field: the nonzero residue $2$ has no multiplicative inverse modulo $2^w$ when $w>1$. Ordinary algebraic cancellation by a nonzero factor can therefore fail. For example, in eight bits, $2\cdot 0=2\cdot128=0$, although $0\ne128$. Cancellation of an additive term remains valid. Bitwise operations live alongside that arithmetic. XOR operates independently on each bit; it is not addition modulo $2^w$, because it does not propagate carries. Keeping those two algebras distinct prevents attractive but incorrect simplifications. In four bits, $1\mathbin{\oplus}1=0$, whereas $1+_4 1=2$. The worked maximum uses $w=64$. HydIR's native semantics also handle narrower operations; the width must come from the decoded instruction. Our eight-bit examples make wraparound visible without changing the formulas. The [SMT-LIB bitvector theory](https://smt-lib.org/theories-FixedSizeBitVectors.shtml) provides the standard vocabulary for expressing fixed-width operations to a solver. ## The state we choose to model A full x86 machine state includes memory, many registers, exceptional behavior, and environmental interactions. For the arithmetic examples, choose this smaller state: $$ {#scalar-state} \begin{aligned} \sigma &= (p,\rho,\varphi),\\ \rho &: \mathcal R \longrightarrow \BV_{64}, &\mathcal R &= \{\mathrm{RAX,RDI,RSI,RDX,RCX}\},\\ \varphi &: \mathcal F \longrightarrow \{0,1\}, &\mathcal F &= \{\mathrm{ZF,SF,OF,CF}\}. \end{aligned} $$ Here $p$ is the current instruction address, $\rho$ maps the selected registers to words, and $\varphi$ maps four condition flags to Boolean values. Our two-input example initially supplies RDI and RSI. A read of another field needs either an explicit input assumption or a preceding definition. This is a teaching model, not an inventory of HydIR's current state. The scalar backend tracks fourteen general-purpose registers, four flags, and eight proved stack slots, with six physical SysV integer argument registers at entry. Native StateIR tracks register, flag, memory-region, and control components. Restricting attention to five registers is justified for these examples by their reads and writes, not by claiming the rest of the architecture does not exist. A supported instruction at address $p$ supplies a state transformer $T_p$. A register-to-register move updates one coordinate and leaves the others unchanged: $$ {#move-semantics} \frac{\operatorname{decode}(p)=\operatorname{mov}\ d,s} {(p,\rho,\varphi)\longrightarrow (p+\ell_p,\rho[d\mapsto\rho(s)],\varphi)}. $$ The notation $\rho[d\mapsto v]$ means “the same register map, except that $d$ now maps to $v$.” The instruction length is $\ell_p$. Notice that the flags are preserved. Translating a move using an LLVM arithmetic expression does not license changing the modeled x86 flags. Likewise, a supported `lea` is arithmetic on register values: $$ {#lea-semantics} \rho'(d)= \rho(b)+_{64}\bigl(k\cdot_{64}\rho(i)\bigr)+_{64}\delta, \qquad \varphi'=\varphi. $$ An absent base or index contributes zero. The implementation restricts which forms of `lea` it accepts; this equation is not a model of arbitrary x86 addressing. In particular, calculating an address does not itself read the memory at that address. There is one important boundary convention. A hardware `ret` reads a return address from the stack. In this scalar model, `ret` ends the selected function and exposes RAX to the host caller. Relating that boundary to a real execution requires the calling convention and a valid call/return context. RSP and guest stack memory are not silently being simulated. ## Carry and overflow answer different questions Suppose an addition computes $r=a+_w b$. For this section, arithmetic inequalities use unsigned integer representatives unless $s$ appears explicitly. Write $A=\msb(a)$, $B=\msb(b)$, and $R=\msb(r)$ for the sign bits. The four flags used by our branch examples follow from the result and the operands: $$ {#addition-flags} \begin{aligned} \mathrm{ZF} &= [u(r)=0],\\ \mathrm{SF} &= R,\\ \mathrm{CF}_{+} &= [u(a)+u(b)\ge M]=[u(r)