diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 49645ba0..0011cfc2 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -38,7 +38,7 @@ jobs:
     runs-on: [self-hosted, linux, flyweight]
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: 'Run code quality checks'
         run: make check
       - name: 'Run pyupgrade'
@@ -52,7 +52,7 @@ jobs:
       CONTAINER: riscv-integration-${{ github.sha }}
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
           submodules: recursive
diff --git a/README.md b/README.md
index f0576f40..7b93245a 100644
--- a/README.md
+++ b/README.md
@@ -1,23 +1,41 @@
-# kriscv
-
+# KRISC-V: Semantics of RISC-V in K
+This repository presents an executable formal semantics of the [RISC-V ISA](https://riscv.org/) using the [K framework](https://kframework.org/). It is currently under construction.
+
+Presently, we support the [unprivileged RV32E base ISA](https://github.com/riscv/riscv-isa-manual/releases/tag/20240411) under the following assumptions:
+- Memory is little-endian.
+- There is a single hart with access to all of physical memory.
+- All memory is readable, writeable, and executable.
+- Instruction fetch is the only implicit memory access.
+- Instruction memory is always coherent with main memory.
+
+## Repository Structure
+The following files constitute the KRISC-V semantics:
+- [word.md](src/kriscv/kdist/riscv-semantics/word.md) provides a `Word` datatype representing `XLEN`-bit values, along with associated numeric operations.
+- [riscv-instructions.md](src/kriscv/kdist/riscv-semantics/riscv-instructions.md) defines the syntax of disassembled instructions.
+- [riscv-disassemble.md](src/kriscv/kdist/riscv-semantics/riscv-disassemble.md) implements the disassembler.
+- [riscv.md](src/kriscv/kdist/riscv-semantics/riscv.md) is the main KRISC-V semantics, defining the configuration and transition rules to fetch and execute instructions.
 
 ## Installation
-
 Prerequsites: `python >= 3.10`, `pip >= 20.0.2`, `poetry >= 1.3.2`.
 
 ```bash
-make build
-pip install dist/*.whl
+poetry install
+make kdist-build
 ```
-
+## Usage
+Execute a compiled RISC-V ELF file with the following command:
+```bash
+poetry -C kriscv run test.elf
+```
+The output shows the final K configuration, including the state of memory, all registers, and any encountered errors. Execution can also be halted at a particular global symbol by providing the `--end-symbol` flag.
 
 ## For Developers
-
 Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets).
 
 * `make build`: Build wheel
 * `make check`: Check code style
 * `make format`: Format code
 * `make test-unit`: Run unit tests
+* `make test-integration`: Run integration tests
 
 For interactive use, spawn a shell with `poetry shell` (after `poetry install`), then run an interpreter.
diff --git a/package/version b/package/version
index 04c5555c..f8bc4c62 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.17
+0.1.18
diff --git a/pyproject.toml b/pyproject.toml
index 1dcf24d3..24f52f06 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.17"
+version = "0.1.18"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kriscv/elf_parser.py b/src/kriscv/elf_parser.py
index 92a9ff21..4392bab5 100644
--- a/src/kriscv/elf_parser.py
+++ b/src/kriscv/elf_parser.py
@@ -5,6 +5,8 @@
 from pyk.prelude.collections import map_of
 from pyk.prelude.kint import intToken
 
+from kriscv.term_builder import word
+
 if TYPE_CHECKING:
     from elftools.elf.elffile import ELFFile  # type: ignore
     from pyk.kast.inner import KInner
@@ -26,12 +28,12 @@ def memory_map(elf: ELFFile) -> KInner:
     for addr_range, data in _memory_segments(elf).items():
         start, end = addr_range
         for addr in range(start, end):
-            mem_map[intToken(addr)] = intToken(data[addr - start])
+            mem_map[word(addr)] = intToken(data[addr - start])
     return map_of(mem_map)
 
 
 def entry_point(elf: ELFFile) -> KInner:
-    return intToken(elf.header['e_entry'])
+    return word(elf.header['e_entry'])
 
 
 def read_symbol(elf: ELFFile, symbol: str) -> list[int]:
diff --git a/src/kriscv/kdist/riscv-semantics/riscv-disassemble.md b/src/kriscv/kdist/riscv-semantics/riscv-disassemble.md
index c21ecd99..f6891361 100644
--- a/src/kriscv/kdist/riscv-semantics/riscv-disassemble.md
+++ b/src/kriscv/kdist/riscv-semantics/riscv-disassemble.md
@@ -1,11 +1,37 @@
+# Disassembler
+In this file, we implement the instruction disassembler, converting raw instruction bits to the syntax defined in [riscv-intructions.md](./riscv-instructions.md).
 ```k
 requires "riscv-instructions.md"
+requires "word.md"
 
 module RISCV-DISASSEMBLE
   imports RISCV-INSTRUCTIONS
   imports INT
   imports STRING
+  imports WORD
+```
+The input is given as an `Int` with the instruction stored in the 32 least-significant bits.
+```k
+  syntax Instruction ::= disassemble(Int) [symbol(disassemble), function, total, memo]
+  rule disassemble(I:Int) => disassemble(decode(I))
+```
+Disassembly is then done in two phases:
+- Separate out the component fields of the instruction based on its format (R, I, S, B, U, or J), returning an `InstructionFormat` value.
+- Inspect the fields of the resulting `InstructionFormat` to produce the disassembled instruction.
 
+The various `InstructionFormat`s are defined below.
+```k
+  syntax InstructionFormat ::=
+      RType(opcode: RTypeOpCode, funct3: Int, funct7: Int, rd: Register, rs1: Register, rs2: Register)
+    | IType(opcode: ITypeOpCode, funct3: Int, rd: Register, rs1: Register, imm: Int)
+    | SType(opcode: STypeOpCode, funct3: Int, rs1: Register, rs2: Register, imm: Int)
+    | BType(opcode: BTypeOpCode, funct3: Int, rs1: Register, rs2: Register, imm: Int)
+    | UType(opcode: UTypeOpCode, rd: Register, imm: Int)
+    | JType(opcode: JTypeOpCode, rd: Register, imm: Int)
+    | UnrecognizedInstructionFormat(Int)
+```
+We determine the correct format by decoding the op code from the 7 least-signficant bits,
+```k
   syntax OpCode ::=
       RTypeOpCode
     | ITypeOpCode
@@ -48,21 +74,15 @@ module RISCV-DISASSEMBLE
   rule decodeOpCode(15 ) => MISC-MEM
   rule decodeOpCode(115) => SYSTEM
   rule decodeOpCode(_  ) => UNRECOGNIZED [owise]
-
-  syntax EncodingType ::=
-      RType(opcode: RTypeOpCode, funct3: Int, funct7: Int, rd: Register, rs1: Register, rs2: Register)
-    | IType(opcode: ITypeOpCode, funct3: Int, rd: Register, rs1: Register, imm: Int)
-    | SType(opcode: STypeOpCode, funct3: Int, rs1: Register, rs2: Register, imm: Int)
-    | BType(opcode: BTypeOpCode, funct3: Int, rs1: Register, rs2: Register, imm: Int)
-    | UType(opcode: UTypeOpCode, rd: Register, imm: Int)
-    | JType(opcode: JTypeOpCode, rd: Register, imm: Int)
-    | UnrecognizedEncodingType(Int)
-
-  syntax EncodingType ::=
-      decode(Int) [function, total]
-    | decodeWithOp(OpCode, Int) [function]
-
+```
+matching on the type of the resulting opcode,
+```k
+  syntax InstructionFormat ::= decode(Int) [function, total]
   rule decode(I) => decodeWithOp(decodeOpCode(I &Int 127), I >>Int 7)
+```
+then finally bit-fiddling to mask out the appropriate bits for each field.
+```k
+  syntax InstructionFormat ::= decodeWithOp(OpCode, Int) [function]
 
   rule decodeWithOp(OPCODE:RTypeOpCode, I) =>
     RType(OPCODE, (I >>Int 5) &Int 7, (I >>Int 18) &Int 127, I &Int 31, (I >>Int 8) &Int 31, (I >>Int 13) &Int 31)
@@ -77,12 +97,11 @@ module RISCV-DISASSEMBLE
   rule decodeWithOp(OPCODE:JTypeOpCode, I) =>
     JType(OPCODE, I &Int 31, (((I >>Int 24) &Int 1) <<Int 19) |Int (((I >>Int 5) &Int 255) <<Int 11) |Int (((I >>Int 13) &Int 1) <<Int 10) |Int ((I >>Int 14) &Int 1023))
   rule decodeWithOp(_:UnrecognizedOpCode, I) =>
-    UnrecognizedEncodingType(I)
-
-  syntax Instruction ::= disassemble(Int) [symbol(disassemble), function, total, memo]
-                       | disassemble(EncodingType) [function, total]
-
-  rule disassemble(I:Int) => disassemble(decode(I))
+    UnrecognizedInstructionFormat(I)
+```
+Finally, we can disassemble the instruction by inspecting the fields for each format. Note that, where appropriate, we infinitely sign extend immediates to represent them as K `Int`s.
+```k
+  syntax Instruction ::= disassemble(InstructionFormat) [function, total]
 
   rule disassemble(RType(OP, 0, 0,  RD, RS1, RS2)) => ADD  RD , RS1 , RS2
   rule disassemble(RType(OP, 0, 32, RD, RS1, RS2)) => SUB  RD , RS1 , RS2
@@ -95,24 +114,23 @@ module RISCV-DISASSEMBLE
   rule disassemble(RType(OP, 6, 0,  RD, RS1, RS2)) => OR   RD , RS1 , RS2
   rule disassemble(RType(OP, 7, 0,  RD, RS1, RS2)) => AND  RD , RS1 , RS2
 
-  rule disassemble(IType(OP-IMM, 0, RD, RS1, IMM)) => ADDI  RD , RS1 , chopAndExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 0, RD, RS1, IMM)) => ADDI  RD , RS1 , infSignExtend(IMM, 12)
   rule disassemble(IType(OP-IMM, 1, RD, RS1, IMM)) => SLLI  RD , RS1 , IMM &Int 31 requires (IMM >>Int 5) &Int 127 ==Int 0
-  rule disassemble(IType(OP-IMM, 2, RD, RS1, IMM)) => SLTI  RD , RS1 , chopAndExtend(IMM, 12)
-  rule disassemble(IType(OP-IMM, 3, RD, RS1, IMM)) => SLTIU RD , RS1 , chopAndExtend(IMM, 12)
-  rule disassemble(IType(OP-IMM, 4, RD, RS1, IMM)) => XORI  RD , RS1 , chopAndExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 2, RD, RS1, IMM)) => SLTI  RD , RS1 , infSignExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 3, RD, RS1, IMM)) => SLTIU RD , RS1 , infSignExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 4, RD, RS1, IMM)) => XORI  RD , RS1 , infSignExtend(IMM, 12)
   rule disassemble(IType(OP-IMM, 5, RD, RS1, IMM)) => SRLI  RD , RS1 , IMM &Int 31 requires (IMM >>Int 5) &Int 127 ==Int 0
   rule disassemble(IType(OP-IMM, 5, RD, RS1, IMM)) => SRAI  RD , RS1 , IMM &Int 31 requires (IMM >>Int 5) &Int 127 ==Int 32
-  rule disassemble(IType(OP-IMM, 6, RD, RS1, IMM)) => ORI   RD , RS1 , chopAndExtend(IMM, 12)
-  rule disassemble(IType(OP-IMM, 7, RD, RS1, IMM)) => ANDI  RD , RS1 , chopAndExtend(IMM, 12)
-
+  rule disassemble(IType(OP-IMM, 6, RD, RS1, IMM)) => ORI   RD , RS1 , infSignExtend(IMM, 12)
+  rule disassemble(IType(OP-IMM, 7, RD, RS1, IMM)) => ANDI  RD , RS1 , infSignExtend(IMM, 12)
 
-  rule disassemble(IType(JALR, 0, RD, RS1, IMM)) => JALR RD , chopAndExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(JALR, 0, RD, RS1, IMM)) => JALR RD , infSignExtend(IMM, 12) ( RS1 )
 
-  rule disassemble(IType(LOAD, 0, RD, RS1, IMM)) => LB  RD , chopAndExtend(IMM, 12) ( RS1 )
-  rule disassemble(IType(LOAD, 1, RD, RS1, IMM)) => LH  RD , chopAndExtend(IMM, 12) ( RS1 )
-  rule disassemble(IType(LOAD, 2, RD, RS1, IMM)) => LW  RD , chopAndExtend(IMM, 12) ( RS1 )
-  rule disassemble(IType(LOAD, 4, RD, RS1, IMM)) => LBU RD , chopAndExtend(IMM, 12) ( RS1 )
-  rule disassemble(IType(LOAD, 5, RD, RS1, IMM)) => LHU RD , chopAndExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(LOAD, 0, RD, RS1, IMM)) => LB  RD , infSignExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(LOAD, 1, RD, RS1, IMM)) => LH  RD , infSignExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(LOAD, 2, RD, RS1, IMM)) => LW  RD , infSignExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(LOAD, 4, RD, RS1, IMM)) => LBU RD , infSignExtend(IMM, 12) ( RS1 )
+  rule disassemble(IType(LOAD, 5, RD, RS1, IMM)) => LHU RD , infSignExtend(IMM, 12) ( RS1 )
 
   rule disassemble(IType(MISC-MEM, 0, 0, 0, 2099)) => FENCE.TSO
   rule disassemble(IType(MISC-MEM, 0, 0, 0, IMM)) => FENCE (IMM >>Int 4) &Int 15 , IMM &Int 15 requires (IMM >>Int 8) &Int 15 ==Int 0
@@ -120,22 +138,22 @@ module RISCV-DISASSEMBLE
   rule disassemble(IType(SYSTEM, 0, 0, 0, 0)) => ECALL
   rule disassemble(IType(SYSTEM, 0, 0, 0, 1)) => EBREAK
 
-  rule disassemble(SType(STORE, 0, RS1, RS2, IMM)) => SB RS2 , chopAndExtend(IMM, 12) ( RS1 )
-  rule disassemble(SType(STORE, 1, RS1, RS2, IMM)) => SH RS2 , chopAndExtend(IMM, 12) ( RS1 )
-  rule disassemble(SType(STORE, 2, RS1, RS2, IMM)) => SW RS2 , chopAndExtend(IMM, 12) ( RS1 )
+  rule disassemble(SType(STORE, 0, RS1, RS2, IMM)) => SB RS2 , infSignExtend(IMM, 12) ( RS1 )
+  rule disassemble(SType(STORE, 1, RS1, RS2, IMM)) => SH RS2 , infSignExtend(IMM, 12) ( RS1 )
+  rule disassemble(SType(STORE, 2, RS1, RS2, IMM)) => SW RS2 , infSignExtend(IMM, 12) ( RS1 )
 
-  rule disassemble(BType(BRANCH, 0, RS1, RS2, IMM)) => BEQ  RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
-  rule disassemble(BType(BRANCH, 1, RS1, RS2, IMM)) => BNE  RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
-  rule disassemble(BType(BRANCH, 4, RS1, RS2, IMM)) => BLT  RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
-  rule disassemble(BType(BRANCH, 5, RS1, RS2, IMM)) => BGE  RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
-  rule disassemble(BType(BRANCH, 6, RS1, RS2, IMM)) => BLTU RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
-  rule disassemble(BType(BRANCH, 7, RS1, RS2, IMM)) => BGEU RS1 , RS2 , chopAndExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 0, RS1, RS2, IMM)) => BEQ  RS1 , RS2 , infSignExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 1, RS1, RS2, IMM)) => BNE  RS1 , RS2 , infSignExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 4, RS1, RS2, IMM)) => BLT  RS1 , RS2 , infSignExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 5, RS1, RS2, IMM)) => BGE  RS1 , RS2 , infSignExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 6, RS1, RS2, IMM)) => BLTU RS1 , RS2 , infSignExtend(IMM, 12) *Int 2
+  rule disassemble(BType(BRANCH, 7, RS1, RS2, IMM)) => BGEU RS1 , RS2 , infSignExtend(IMM, 12) *Int 2
 
   rule disassemble(UType(LUI, RD, IMM))   => LUI   RD , IMM
   rule disassemble(UType(AUIPC, RD, IMM)) => AUIPC RD , IMM
 
-  rule disassemble(JType(JAL, RD, IMM)) => JAL RD , chopAndExtend(IMM, 20) *Int 2
+  rule disassemble(JType(JAL, RD, IMM)) => JAL RD , infSignExtend(IMM, 20) *Int 2
 
-  rule disassemble(_:EncodingType) => INVALID_INSTR [owise]
+  rule disassemble(_:InstructionFormat) => INVALID_INSTR [owise]
 endmodule
 ```
diff --git a/src/kriscv/kdist/riscv-semantics/riscv-instructions.md b/src/kriscv/kdist/riscv-semantics/riscv-instructions.md
index 97da29d0..7fae1f0d 100644
--- a/src/kriscv/kdist/riscv-semantics/riscv-instructions.md
+++ b/src/kriscv/kdist/riscv-semantics/riscv-instructions.md
@@ -1,3 +1,14 @@
+# Instruction Syntax
+In this file, we define the basic syntax for disassembled instructions.
+
+We closely mirror the ASM syntax as output by the RISC-V GNU Toolchain's `objdump`. In particular,
+- I-Type and S-Type instructions with 12-bit signed immediates (e.g., `addi` but not `slli`) take an immediate argument in the range `[-2048, 2047]`.
+- Shift instructions take a shift amount argument in the range `[0, XLEN - 1]`.
+- U-Type instruction take an immediate argument in the range `[0x0, 0xfffff]`, i.e., not representing the zeroed-out 12 least-significant bits.
+- B-Type instructions take an immediate argument as an even integer in the range `[-4096, 4094]`, i.e., explicitly representing the zeroed-out least-significant bit.
+- J-Type instructions take an immediate argument as an even integer in the range `[-1048576, 1048574]`, i.e., explicitly representing the zeroed-out least-significant bit.
+
+A register `xi` is simply represented by the `Int` value `i`.
 ```k
 module RISCV-INSTRUCTIONS
   imports INT
@@ -71,10 +82,5 @@ module RISCV-INSTRUCTIONS
     | "EBREAK"    [symbol(EBREAK)]
 
   syntax InvalidInstr ::= "INVALID_INSTR" [symbol(INVALID_INSTR)]
-
-  // Truncate to length bits, then sign extend
-  syntax Int ::= chopAndExtend(bits: Int, length: Int) [function, total]
-  rule chopAndExtend(B, L) => (-1 <<Int L) |Int B requires (B >>Int (L -Int 1)) &Int 1 ==Int 1
-  rule chopAndExtend(B, L) => B &Int (2 ^Int L -Int 1) [owise]
 endmodule
 ```
diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md
index cf169780..a86e8c02 100644
--- a/src/kriscv/kdist/riscv-semantics/riscv.md
+++ b/src/kriscv/kdist/riscv-semantics/riscv.md
@@ -1,51 +1,78 @@
+# RISC-V Execution
+## Configuration
+The configuration is divided into two sections:
+- `<riscv>`, containing the state of the abstract machine
+- `<test>`, containing any additional state needed to run tests
+
+The `<riscv>` section contain the following cells:
+- `<instrs>`, a K-sequence of fetched instruction to be executed
+- `<regs>`, a map from each initialized `Register` to its current value
+- `<pc>`, the program counter register
+- `<mem>`, a map from initialized `Word` addresses to the byte stored at the address
+
+The `<test>` section currently contains on a single cell:
+- `<haltCond>`, a value indicating under which conditions the program should be halted
+- `<halt>`, whether to halt the program
 ```k
 requires "riscv-disassemble.md"
 requires "riscv-instructions.md"
+requires "word.md"
 
 module RISCV-CONFIGURATION
+  imports BOOL
   imports INT
   imports MAP
   imports RANGEMAP
+  imports WORD
 
   syntax HaltCondition
 
-  syntax Int ::= XLEN() [macro]
-  rule XLEN() => 32
-
   configuration
     <riscv>
       <instrs> .K </instrs>
-      <mem> $MEM:Map </mem> // Map{Int, Int}
-      <regs> .Map </regs> // Map{Int, Int}
-      <pc> $PC:Int </pc>
+      <regs> .Map </regs> // Map{Register, Word}
+      <pc> $PC:Word </pc>
+      <mem> $MEM:Map </mem> // Map{Word, Int}
     </riscv>
     <test>
-      <halt> $HALT:HaltCondition </halt>
+      <haltCond> $HALT:HaltCondition </haltCond>
+      <halt> false:Bool </halt>
     </test>
 endmodule
+```
+
+## Termination
+RISC-V does not provide a `halt` instruction,  instead relying on the surrounding environment, e.g., making a sys-call to exit with a particular exit code.
+For testing purposes, we then add our own custom halting mechanism denoted by a `HaltCondition` value.
 
+Currently, we support:
+- Never halting unless a trap or exception is reached
+- Halting when the `PC` reaches a particular address
+```k
 module RISCV-TERMINATION
   imports RISCV-CONFIGURATION
   imports BOOL
   imports INT
 
-  syntax Bool ::= shouldHalt(HaltCondition) [function]
-  syntax HaltCondition ::=
-      "NEVER"               [symbol(HaltNever)]
-    | "ADDRESS" "(" Int ")" [symbol(HaltAtAddress)]
-
+  syntax Instruction ::= "CHECK_HALT"
 
-  rule shouldHalt(NEVER) => false
+  syntax HaltCondition ::=
+      "NEVER"                [symbol(HaltNever)]
+    | "ADDRESS" "(" Word ")" [symbol(HaltAtAddress)]
 
-  rule [[ shouldHalt(ADDRESS(END)) => true ]]
-       <pc> PC </pc>
-       requires END ==Int PC
+  rule <instrs> CHECK_HALT => .K ...</instrs>
+       <haltCond> NEVER </haltCond>
 
-  rule [[ shouldHalt(ADDRESS(END)) => false ]]
+  rule <instrs> CHECK_HALT => .K ...</instrs>
        <pc> PC </pc>
-       requires END =/=Int PC
+       <haltCond> ADDRESS(END) </haltCond>
+       <halt> _ => PC ==Word END </halt>
 endmodule
+```
 
+## Memory and Registers
+RISC-V uses a circular, byte-adressable memory space containing `2^XLEN` bytes.
+```k
 module RISCV-MEMORY
   imports INT
   imports MAP
@@ -53,49 +80,62 @@ module RISCV-MEMORY
   imports RISCV-CONFIGURATION
   imports RISCV-DISASSEMBLE
   imports RISCV-INSTRUCTIONS
-
-  syntax Int ::= wrapAddr(address: Int) [function]
-  rule wrapAddr(A) => A modInt (2 ^Int XLEN())
-
-  syntax Int ::= loadByte(memory: Map, address: Int) [function]
-  rule loadByte(MEM, ADDR) => { MEM [ wrapAddr(ADDR) ] } :>Int
-
-  syntax Instruction ::= fetchInstr(memory: Map, address: Int) [function]
+  imports WORD
+```
+We abstract the particular memory representation behind a `loadByte` function which return the byte stored at a particular address.
+```k
+  syntax Int ::= loadByte(memory: Map, address: Word) [function]
+  rule loadByte(MEM, ADDR) => { MEM[ADDR] } :>Int
+```
+Instructions are always 32-bits, and are stored in little-endian format regardless of the endianness of the overall architecture.
+```k
+  syntax Instruction ::= fetchInstr(memory: Map, address: Word) [function]
   rule fetchInstr(MEM, ADDR) =>
-    disassemble((loadByte(MEM, ADDR +Int 3) <<Int 24) |Int
-                (loadByte(MEM, ADDR +Int 2) <<Int 16) |Int
-                (loadByte(MEM, ADDR +Int 1) <<Int 8 ) |Int
+    disassemble((loadByte(MEM, ADDR +Word W(3)) <<Int 24) |Int
+                (loadByte(MEM, ADDR +Word W(2)) <<Int 16) |Int
+                (loadByte(MEM, ADDR +Word W(1)) <<Int 8 ) |Int
                  loadByte(MEM, ADDR       ))
-
-
-  syntax Map ::= writeReg(regs: Map, rd: Int, value: Int) [function]
+```
+Registers should be manipulated with the `writeReg` and `readReg` functions, which account for `x0` always being hard-wired to contain all `0`s.
+```k
+  syntax Map ::= writeReg(regs: Map, rd: Int, value: Word) [function]
   rule writeReg(REGS, 0 , _  ) => REGS
-  rule writeReg(REGS, RD, VAL) => REGS[RD <- VAL] requires RD =/=Int 0
+  rule writeReg(REGS, RD, VAL) => REGS[RD <- VAL] [owise]
 
-  syntax Int ::= readReg(regs: Map, rs: Int) [function]
-  rule readReg(_   , 0 ) => 0
-  rule readReg(REGS, RS) => { REGS[RS] } :>Int requires RS =/=Int 0
+  syntax Word ::= readReg(regs: Map, rs: Int) [function]
+  rule readReg(_   , 0 ) => W(0)
+  rule readReg(REGS, RS) => { REGS[RS] } :>Word [owise]
 endmodule
+```
 
+## Instruction Execution
+The actual execution semantics has two components:
+- The instruction fetch cycle, which disassembles an instruction from the current `PC` so long as the `HaltCondition` fails, placing it into the `<instrs>` cell
+- Rules to implement each instruction, removing the instruction from the top of the `<instrs>` cell and updating any state as necessary.
+```k
 module RISCV
   imports RISCV-CONFIGURATION
   imports RISCV-DISASSEMBLE
   imports RISCV-INSTRUCTIONS
   imports RISCV-MEMORY
   imports RISCV-TERMINATION
+  imports WORD
 
-  rule <instrs> .K => fetchInstr(MEM, PC) </instrs>
-       <mem> MEM </mem>
+  rule <instrs> .K => fetchInstr(MEM, PC) ~> CHECK_HALT </instrs>
        <pc> PC </pc>
-       <halt> H </halt>
-       requires notBool shouldHalt(H)
-
+       <mem> MEM </mem>
+       <halt> false </halt>
+```
+`ADDI` adds the immediate `IMM` to the value in register `RS`, storing the result in register `RD`. Note that we must use `chop` to convert `IMM` from an infinitely sign-extended K `Int` to an `XLEN`-bit `Word`.
+```k
   rule <instrs> ADDI RD , RS , IMM => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, chopAndExtend(readReg(REGS, RS) +Int IMM, XLEN())) </regs>
-       <pc> PC => wrapAddr(PC +Int 4) </pc>
-
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) +Word chop(IMM)) </regs>
+       <pc> PC => PC +Word W(4) </pc>
+```
+`LUI` builds a 32-bit constant from the 20-bit immediate by setting the 12 least-significant bits to `0`, then sign extends to `XLEN` bits and places the result in register `RD`.
+```k
   rule <instrs> LUI RD , IMM => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, chopAndExtend(IMM <<Int 12, XLEN())) </regs>
-       <pc> PC => wrapAddr(PC +Int 4) </pc>
+       <regs> REGS => writeReg(REGS, RD, W(IMM <<Int 12)) </regs>
+       <pc> PC => PC +Word W(4) </pc>
 endmodule
 ```
diff --git a/src/kriscv/kdist/riscv-semantics/word.md b/src/kriscv/kdist/riscv-semantics/word.md
new file mode 100644
index 00000000..21e92345
--- /dev/null
+++ b/src/kriscv/kdist/riscv-semantics/word.md
@@ -0,0 +1,102 @@
+# `XLEN`-bit Word Datatype
+
+In this file, we define a `Word` datatype representing a sequence of `XLEN` bits, where `XLEN=32` for `RV32*` ISAs and `XLEN=64` for `RV64*` ISAs.
+```k
+module WORD
+  imports BOOL
+  imports BYTES
+  imports INT
+
+  syntax Int ::= "XLEN" [macro]
+  rule XLEN => 32
+```
+Throughout the semantics, we use K's arbitrary-precision, infinitely sign-extended, two's-complement integer type `Int` to store arbitrary bit sequences. A `Word` consists of a single `Int`, with the `XLEN` least-signficant bits storing the desired bit sequence and all other bits zeroed.
+```k
+  syntax Word ::= W(Int) [format(%3), symbol(W)]
+```
+A `Word` can be interpreted as an unsigned integer by directly returning the underlying `Int`,
+```k
+  syntax Int ::= Word2UInt(Word) [function, total]
+  rule Word2UInt(W(I)) => I
+```
+or interpreted as an `XLEN`-bit signed two's complement integer by infinitely sign extending.
+```k
+  syntax Int ::= Word2SInt(Word) [function, total]
+  rule Word2SInt(W(I)) => infSignExtend(I, XLEN)
+
+  syntax Int ::= infSignExtend(bits: Int, signBitIdx: Int) [function, total]
+  rule infSignExtend(B, L) => (-1 <<Int L) |Int B requires (B >>Int (L -Int 1)) &Int 1 ==Int 1
+  rule infSignExtend(B, _) => B [owise]
+```
+`N`-bit signed two's complement integers with `N <= XLEN` can also be sign extended to `XLEN`-bits.
+```k
+  syntax Word ::= signExtend(bits: Int, signBitIdx: Int) [function, total]
+  rule signExtend(B, L) => W(((2 ^Int (XLEN -Int L) -Int 1) <<Int L) |Int B) requires (B >>Int (L -Int 1)) &Int 1 ==Int 1
+  rule signExtend(B, _) => W(B) [owise]
+```
+Booleans can be encoded as `Word`s in the obvious way
+```k
+  syntax Word ::= Bool2Word(Bool) [function, total]
+  rule Bool2Word(false) => W(0)
+  rule Bool2Word(true ) => W(1)
+```
+The rest of this file defines various numeric and bitwise operations over `Word`. Most of these are straightforwad operations on the underlying `Int`.
+```k
+  syntax Bool ::= Word "==Word" Word [function, total]
+  rule W(I1) ==Word W(I2) => I1 ==Int I2
+
+  syntax Bool ::= Word "=/=Word" Word [function, total]
+  rule W(I1) =/=Word W(I2) => I1 =/=Int I2
+```
+The `s` prefix denotes a signed operation while `u` denotes an unsigned operation.
+```k
+  syntax Bool ::= Word "<sWord" Word [function, total]
+  rule W1 <sWord W2 => Word2SInt(W1) <Int Word2SInt(W2)
+
+  syntax Bool ::= Word ">=sWord" Word [function, total]
+  rule W1 >=sWord W2 => Word2SInt(W1) >=Int Word2SInt(W2)
+
+  syntax Bool ::= Word "<uWord" Word [function, total]
+  rule W(I1) <uWord W(I2) => I1 <Int I2
+
+  syntax Bool ::= Word ">=uWord" Word [function, total]
+  rule W(I1) >=uWord W(I2) => I1 >=Int I2
+```
+Note that two's complement enables us to use a single addition or subtraction operation for both signed and unsigned values.
+```k
+  syntax Word ::= Word "+Word" Word [function, total]
+  rule W(I1) +Word W(I2) => chop(I1 +Int I2)
+
+  syntax Word ::= Word "-Word" Word [function, total]
+  rule W(I1) -Word W(I2) => chop(I1 -Int I2)
+```
+Above, the `chop` utility function
+```k
+  syntax Word ::= chop(Int) [function, total]
+  rule chop(I) => W(I &Int (2 ^Int XLEN -Int 1))
+```
+is used to zero-out all but the least-significant `XLEN`-bits in case of overflow.
+```k
+  syntax Word ::= Word "&Word" Word [function, total]
+  rule W(I1) &Word W(I2) => W(I1 &Int I2)
+
+  syntax Word ::= Word "|Word" Word [function, total]
+  rule W(I1) |Word W(I2) => W(I1 |Int I2)
+
+  syntax Word ::= Word "xorWord" Word [function, total]
+  rule W(I1) xorWord W(I2) => W(I1 xorInt I2)
+
+  syntax Word ::= Word "<<Word" Int [function]
+  rule W(I1) <<Word I2 => chop(I1 <<Int I2)
+```
+For right shifts, we provide both arithmetic and logical variants
+```k
+  syntax Word ::= Word ">>aWord" Int [function]
+  rule W(I1) >>aWord I2 => W(I1 >>Int I2)
+```
+Because K does not provide a logical right shift for `Int`, we implement it as an arithmetic shift followed by zeroing-out all the sign bits.
+```k
+  syntax Word ::= Word ">>lWord" Int [function]
+  rule W(I1) >>lWord I2 => W((I1 >>Int I2) &Int (2 ^Int (XLEN -Int I2) -Int 1))
+endmodule
+```
diff --git a/src/kriscv/term_builder.py b/src/kriscv/term_builder.py
index 81fd1a92..0b63443a 100644
--- a/src/kriscv/term_builder.py
+++ b/src/kriscv/term_builder.py
@@ -2,15 +2,13 @@
 
 from typing import TYPE_CHECKING
 
-from pyk.kast.inner import KApply, KSort
+from pyk.kast.inner import KApply, KInner, KSort
 from pyk.prelude.kint import intToken
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
     from typing import TypeVar
 
-    from pyk.kast.inner import KInner
-
     T = TypeVar('T')
 
 
@@ -228,3 +226,17 @@ def ebreak_instr() -> KInner:
 
 def invalid_instr() -> KInner:
     return KApply('INVALID_INSTR')
+
+
+def word(bits: KInner | int | str | bytes) -> KInner:
+    match bits:
+        case KInner():
+            val = bits
+        case int():
+            assert bits >= 0
+            val = intToken(bits)
+        case str():
+            val = intToken(int(bits, 2))
+        case bytes():
+            val = intToken(int.from_bytes(bits, 'big', signed=False))
+    return KApply('W', val)
diff --git a/src/kriscv/tools.py b/src/kriscv/tools.py
index c8887c2c..b6f7f2b4 100644
--- a/src/kriscv/tools.py
+++ b/src/kriscv/tools.py
@@ -6,7 +6,6 @@
 from pyk.kast.inner import Subst
 from pyk.ktool.krun import KRun
 from pyk.prelude.k import GENERATED_TOP_CELL
-from pyk.prelude.kint import intToken
 
 from kriscv import elf_parser, term_builder
 
@@ -62,7 +61,7 @@ def run_elf(self, elf_file: Path, *, end_symbol: str | None = None) -> KInner:
                     raise AssertionError(
                         f'End symbol {end_symbol!r} should be unique, but found multiple instances: {elf_file}'
                     )
-                halt_cond = term_builder.halt_at_address(intToken(end_values[0]))
+                halt_cond = term_builder.halt_at_address(term_builder.word(end_values[0]))
             else:
                 halt_cond = term_builder.halt_never()
             config_vars = {
diff --git a/tests/simple/addi-overflow.S.out b/tests/simple/addi-overflow.S.out
index 75fb36be..7a0545fd 100644
--- a/tests/simple/addi-overflow.S.out
+++ b/tests/simple/addi-overflow.S.out
@@ -3,19 +3,22 @@
     <instrs>
       .K
     </instrs>
-    <mem>
-      65536 |-> 127 65537 |-> 69 65538 |-> 76 65539 |-> 70 65540 |-> 1 65541 |-> 1 65542 |-> 1 65543 |-> 0 65544 |-> 0 65545 |-> 0 65546 |-> 0 65547 |-> 0 65548 |-> 0 65549 |-> 0 65550 |-> 0 65551 |-> 0 65552 |-> 2 65553 |-> 0 65554 |-> 243 65555 |-> 0 65556 |-> 1 65557 |-> 0 65558 |-> 0 65559 |-> 0 65560 |-> 84 65561 |-> 0 65562 |-> 1 65563 |-> 0 65564 |-> 52 65565 |-> 0 65566 |-> 0 65567 |-> 0 65568 |-> 208 65569 |-> 1 65570 |-> 0 65571 |-> 0 65572 |-> 8 65573 |-> 0 65574 |-> 0 65575 |-> 0 65576 |-> 52 65577 |-> 0 65578 |-> 32 65579 |-> 0 65580 |-> 1 65581 |-> 0 65582 |-> 40 65583 |-> 0 65584 |-> 5 65585 |-> 0 65586 |-> 4 65587 |-> 0 65588 |-> 1 65589 |-> 0 65590 |-> 0 65591 |-> 0 65592 |-> 0 65593 |-> 0 65594 |-> 0 65595 |-> 0 65596 |-> 0 65597 |-> 0 65598 |-> 1 65599 |-> 0 65600 |-> 0 65601 |-> 0 65602 |-> 1 65603 |-> 0 65604 |-> 108 65605 |-> 0 65606 |-> 0 65607 |-> 0 65608 |-> 108 65609 |-> 0 65610 |-> 0 65611 |-> 0 65612 |-> 5 65613 |-> 0 65614 |-> 0 65615 |-> 0 65616 |-> 0 65617 |-> 16 65618 |-> 0 65619 |-> 0 65620 |-> 183 65621 |-> 240 65622 |-> 255 65623 |-> 127 65624 |-> 147 65625 |-> 128 65626 |-> 240 65627 |-> 127 65628 |-> 147 65629 |-> 128 65630 |-> 240 65631 |-> 127 65632 |-> 147 65633 |-> 128 65634 |-> 16 65635 |-> 0 65636 |-> 19 65637 |-> 129 65638 |-> 16 65639 |-> 0 65640 |-> 19 65641 |-> 0 65642 |-> 0 65643 |-> 0
-    </mem>
     <regs>
-      1 |-> 2147483647 2 |-> -2147483648
+      1 |-> W ( 2147483647 ) 2 |-> W ( 2147483648 )
     </regs>
     <pc>
-      65640
+      W ( 65640 )
     </pc>
+    <mem>
+      W ( 65536 ) |-> 127 W ( 65537 ) |-> 69 W ( 65538 ) |-> 76 W ( 65539 ) |-> 70 W ( 65540 ) |-> 1 W ( 65541 ) |-> 1 W ( 65542 ) |-> 1 W ( 65543 ) |-> 0 W ( 65544 ) |-> 0 W ( 65545 ) |-> 0 W ( 65546 ) |-> 0 W ( 65547 ) |-> 0 W ( 65548 ) |-> 0 W ( 65549 ) |-> 0 W ( 65550 ) |-> 0 W ( 65551 ) |-> 0 W ( 65552 ) |-> 2 W ( 65553 ) |-> 0 W ( 65554 ) |-> 243 W ( 65555 ) |-> 0 W ( 65556 ) |-> 1 W ( 65557 ) |-> 0 W ( 65558 ) |-> 0 W ( 65559 ) |-> 0 W ( 65560 ) |-> 84 W ( 65561 ) |-> 0 W ( 65562 ) |-> 1 W ( 65563 ) |-> 0 W ( 65564 ) |-> 52 W ( 65565 ) |-> 0 W ( 65566 ) |-> 0 W ( 65567 ) |-> 0 W ( 65568 ) |-> 208 W ( 65569 ) |-> 1 W ( 65570 ) |-> 0 W ( 65571 ) |-> 0 W ( 65572 ) |-> 8 W ( 65573 ) |-> 0 W ( 65574 ) |-> 0 W ( 65575 ) |-> 0 W ( 65576 ) |-> 52 W ( 65577 ) |-> 0 W ( 65578 ) |-> 32 W ( 65579 ) |-> 0 W ( 65580 ) |-> 1 W ( 65581 ) |-> 0 W ( 65582 ) |-> 40 W ( 65583 ) |-> 0 W ( 65584 ) |-> 5 W ( 65585 ) |-> 0 W ( 65586 ) |-> 4 W ( 65587 ) |-> 0 W ( 65588 ) |-> 1 W ( 65589 ) |-> 0 W ( 65590 ) |-> 0 W ( 65591 ) |-> 0 W ( 65592 ) |-> 0 W ( 65593 ) |-> 0 W ( 65594 ) |-> 0 W ( 65595 ) |-> 0 W ( 65596 ) |-> 0 W ( 65597 ) |-> 0 W ( 65598 ) |-> 1 W ( 65599 ) |-> 0 W ( 65600 ) |-> 0 W ( 65601 ) |-> 0 W ( 65602 ) |-> 1 W ( 65603 ) |-> 0 W ( 65604 ) |-> 108 W ( 65605 ) |-> 0 W ( 65606 ) |-> 0 W ( 65607 ) |-> 0 W ( 65608 ) |-> 108 W ( 65609 ) |-> 0 W ( 65610 ) |-> 0 W ( 65611 ) |-> 0 W ( 65612 ) |-> 5 W ( 65613 ) |-> 0 W ( 65614 ) |-> 0 W ( 65615 ) |-> 0 W ( 65616 ) |-> 0 W ( 65617 ) |-> 16 W ( 65618 ) |-> 0 W ( 65619 ) |-> 0 W ( 65620 ) |-> 183 W ( 65621 ) |-> 240 W ( 65622 ) |-> 255 W ( 65623 ) |-> 127 W ( 65624 ) |-> 147 W ( 65625 ) |-> 128 W ( 65626 ) |-> 240 W ( 65627 ) |-> 127 W ( 65628 ) |-> 147 W ( 65629 ) |-> 128 W ( 65630 ) |-> 240 W ( 65631 ) |-> 127 W ( 65632 ) |-> 147 W ( 65633 ) |-> 128 W ( 65634 ) |-> 16 W ( 65635 ) |-> 0 W ( 65636 ) |-> 19 W ( 65637 ) |-> 129 W ( 65638 ) |-> 16 W ( 65639 ) |-> 0 W ( 65640 ) |-> 19 W ( 65641 ) |-> 0 W ( 65642 ) |-> 0 W ( 65643 ) |-> 0
+    </mem>
   </riscv>
   <test>
+    <haltCond>
+      ADDRESS ( W ( 65640 ) )
+    </haltCond>
     <halt>
-      ADDRESS ( 65640 )
+      true
     </halt>
   </test>
   <generatedCounter>
diff --git a/tests/simple/addi.S.out b/tests/simple/addi.S.out
index 86967e63..250f5b29 100644
--- a/tests/simple/addi.S.out
+++ b/tests/simple/addi.S.out
@@ -3,19 +3,22 @@
     <instrs>
       .K
     </instrs>
-    <mem>
-      65536 |-> 127 65537 |-> 69 65538 |-> 76 65539 |-> 70 65540 |-> 1 65541 |-> 1 65542 |-> 1 65543 |-> 0 65544 |-> 0 65545 |-> 0 65546 |-> 0 65547 |-> 0 65548 |-> 0 65549 |-> 0 65550 |-> 0 65551 |-> 0 65552 |-> 2 65553 |-> 0 65554 |-> 243 65555 |-> 0 65556 |-> 1 65557 |-> 0 65558 |-> 0 65559 |-> 0 65560 |-> 84 65561 |-> 0 65562 |-> 1 65563 |-> 0 65564 |-> 52 65565 |-> 0 65566 |-> 0 65567 |-> 0 65568 |-> 200 65569 |-> 1 65570 |-> 0 65571 |-> 0 65572 |-> 8 65573 |-> 0 65574 |-> 0 65575 |-> 0 65576 |-> 52 65577 |-> 0 65578 |-> 32 65579 |-> 0 65580 |-> 1 65581 |-> 0 65582 |-> 40 65583 |-> 0 65584 |-> 5 65585 |-> 0 65586 |-> 4 65587 |-> 0 65588 |-> 1 65589 |-> 0 65590 |-> 0 65591 |-> 0 65592 |-> 0 65593 |-> 0 65594 |-> 0 65595 |-> 0 65596 |-> 0 65597 |-> 0 65598 |-> 1 65599 |-> 0 65600 |-> 0 65601 |-> 0 65602 |-> 1 65603 |-> 0 65604 |-> 100 65605 |-> 0 65606 |-> 0 65607 |-> 0 65608 |-> 100 65609 |-> 0 65610 |-> 0 65611 |-> 0 65612 |-> 5 65613 |-> 0 65614 |-> 0 65615 |-> 0 65616 |-> 0 65617 |-> 16 65618 |-> 0 65619 |-> 0 65620 |-> 147 65621 |-> 0 65622 |-> 128 65623 |-> 0 65624 |-> 147 65625 |-> 128 65626 |-> 128 65627 |-> 0 65628 |-> 19 65629 |-> 129 65630 |-> 0 65631 |-> 0 65632 |-> 19 65633 |-> 0 65634 |-> 0 65635 |-> 0
-    </mem>
     <regs>
-      1 |-> 16 2 |-> 16
+      1 |-> W ( 16 ) 2 |-> W ( 16 )
     </regs>
     <pc>
-      65632
+      W ( 65632 )
     </pc>
+    <mem>
+      W ( 65536 ) |-> 127 W ( 65537 ) |-> 69 W ( 65538 ) |-> 76 W ( 65539 ) |-> 70 W ( 65540 ) |-> 1 W ( 65541 ) |-> 1 W ( 65542 ) |-> 1 W ( 65543 ) |-> 0 W ( 65544 ) |-> 0 W ( 65545 ) |-> 0 W ( 65546 ) |-> 0 W ( 65547 ) |-> 0 W ( 65548 ) |-> 0 W ( 65549 ) |-> 0 W ( 65550 ) |-> 0 W ( 65551 ) |-> 0 W ( 65552 ) |-> 2 W ( 65553 ) |-> 0 W ( 65554 ) |-> 243 W ( 65555 ) |-> 0 W ( 65556 ) |-> 1 W ( 65557 ) |-> 0 W ( 65558 ) |-> 0 W ( 65559 ) |-> 0 W ( 65560 ) |-> 84 W ( 65561 ) |-> 0 W ( 65562 ) |-> 1 W ( 65563 ) |-> 0 W ( 65564 ) |-> 52 W ( 65565 ) |-> 0 W ( 65566 ) |-> 0 W ( 65567 ) |-> 0 W ( 65568 ) |-> 200 W ( 65569 ) |-> 1 W ( 65570 ) |-> 0 W ( 65571 ) |-> 0 W ( 65572 ) |-> 8 W ( 65573 ) |-> 0 W ( 65574 ) |-> 0 W ( 65575 ) |-> 0 W ( 65576 ) |-> 52 W ( 65577 ) |-> 0 W ( 65578 ) |-> 32 W ( 65579 ) |-> 0 W ( 65580 ) |-> 1 W ( 65581 ) |-> 0 W ( 65582 ) |-> 40 W ( 65583 ) |-> 0 W ( 65584 ) |-> 5 W ( 65585 ) |-> 0 W ( 65586 ) |-> 4 W ( 65587 ) |-> 0 W ( 65588 ) |-> 1 W ( 65589 ) |-> 0 W ( 65590 ) |-> 0 W ( 65591 ) |-> 0 W ( 65592 ) |-> 0 W ( 65593 ) |-> 0 W ( 65594 ) |-> 0 W ( 65595 ) |-> 0 W ( 65596 ) |-> 0 W ( 65597 ) |-> 0 W ( 65598 ) |-> 1 W ( 65599 ) |-> 0 W ( 65600 ) |-> 0 W ( 65601 ) |-> 0 W ( 65602 ) |-> 1 W ( 65603 ) |-> 0 W ( 65604 ) |-> 100 W ( 65605 ) |-> 0 W ( 65606 ) |-> 0 W ( 65607 ) |-> 0 W ( 65608 ) |-> 100 W ( 65609 ) |-> 0 W ( 65610 ) |-> 0 W ( 65611 ) |-> 0 W ( 65612 ) |-> 5 W ( 65613 ) |-> 0 W ( 65614 ) |-> 0 W ( 65615 ) |-> 0 W ( 65616 ) |-> 0 W ( 65617 ) |-> 16 W ( 65618 ) |-> 0 W ( 65619 ) |-> 0 W ( 65620 ) |-> 147 W ( 65621 ) |-> 0 W ( 65622 ) |-> 128 W ( 65623 ) |-> 0 W ( 65624 ) |-> 147 W ( 65625 ) |-> 128 W ( 65626 ) |-> 128 W ( 65627 ) |-> 0 W ( 65628 ) |-> 19 W ( 65629 ) |-> 129 W ( 65630 ) |-> 0 W ( 65631 ) |-> 0 W ( 65632 ) |-> 19 W ( 65633 ) |-> 0 W ( 65634 ) |-> 0 W ( 65635 ) |-> 0
+    </mem>
   </riscv>
   <test>
+    <haltCond>
+      ADDRESS ( W ( 65632 ) )
+    </haltCond>
     <halt>
-      ADDRESS ( 65632 )
+      true
     </halt>
   </test>
   <generatedCounter>
diff --git a/tests/simple/lui.S.out b/tests/simple/lui.S.out
index 9d628bdc..d51fdd81 100644
--- a/tests/simple/lui.S.out
+++ b/tests/simple/lui.S.out
@@ -3,19 +3,22 @@
     <instrs>
       .K
     </instrs>
-    <mem>
-      65536 |-> 127 65537 |-> 69 65538 |-> 76 65539 |-> 70 65540 |-> 1 65541 |-> 1 65542 |-> 1 65543 |-> 0 65544 |-> 0 65545 |-> 0 65546 |-> 0 65547 |-> 0 65548 |-> 0 65549 |-> 0 65550 |-> 0 65551 |-> 0 65552 |-> 2 65553 |-> 0 65554 |-> 243 65555 |-> 0 65556 |-> 1 65557 |-> 0 65558 |-> 0 65559 |-> 0 65560 |-> 84 65561 |-> 0 65562 |-> 1 65563 |-> 0 65564 |-> 52 65565 |-> 0 65566 |-> 0 65567 |-> 0 65568 |-> 200 65569 |-> 1 65570 |-> 0 65571 |-> 0 65572 |-> 8 65573 |-> 0 65574 |-> 0 65575 |-> 0 65576 |-> 52 65577 |-> 0 65578 |-> 32 65579 |-> 0 65580 |-> 1 65581 |-> 0 65582 |-> 40 65583 |-> 0 65584 |-> 5 65585 |-> 0 65586 |-> 4 65587 |-> 0 65588 |-> 1 65589 |-> 0 65590 |-> 0 65591 |-> 0 65592 |-> 0 65593 |-> 0 65594 |-> 0 65595 |-> 0 65596 |-> 0 65597 |-> 0 65598 |-> 1 65599 |-> 0 65600 |-> 0 65601 |-> 0 65602 |-> 1 65603 |-> 0 65604 |-> 100 65605 |-> 0 65606 |-> 0 65607 |-> 0 65608 |-> 100 65609 |-> 0 65610 |-> 0 65611 |-> 0 65612 |-> 5 65613 |-> 0 65614 |-> 0 65615 |-> 0 65616 |-> 0 65617 |-> 16 65618 |-> 0 65619 |-> 0 65620 |-> 55 65621 |-> 0 65622 |-> 1 65623 |-> 0 65624 |-> 183 65625 |-> 0 65626 |-> 0 65627 |-> 128 65628 |-> 55 65629 |-> 1 65630 |-> 0 65631 |-> 112 65632 |-> 19 65633 |-> 0 65634 |-> 0 65635 |-> 0
-    </mem>
     <regs>
-      1 |-> -2147483648 2 |-> 1879048192
+      1 |-> W ( 2147483648 ) 2 |-> W ( 1879048192 )
     </regs>
     <pc>
-      65632
+      W ( 65632 )
     </pc>
+    <mem>
+      W ( 65536 ) |-> 127 W ( 65537 ) |-> 69 W ( 65538 ) |-> 76 W ( 65539 ) |-> 70 W ( 65540 ) |-> 1 W ( 65541 ) |-> 1 W ( 65542 ) |-> 1 W ( 65543 ) |-> 0 W ( 65544 ) |-> 0 W ( 65545 ) |-> 0 W ( 65546 ) |-> 0 W ( 65547 ) |-> 0 W ( 65548 ) |-> 0 W ( 65549 ) |-> 0 W ( 65550 ) |-> 0 W ( 65551 ) |-> 0 W ( 65552 ) |-> 2 W ( 65553 ) |-> 0 W ( 65554 ) |-> 243 W ( 65555 ) |-> 0 W ( 65556 ) |-> 1 W ( 65557 ) |-> 0 W ( 65558 ) |-> 0 W ( 65559 ) |-> 0 W ( 65560 ) |-> 84 W ( 65561 ) |-> 0 W ( 65562 ) |-> 1 W ( 65563 ) |-> 0 W ( 65564 ) |-> 52 W ( 65565 ) |-> 0 W ( 65566 ) |-> 0 W ( 65567 ) |-> 0 W ( 65568 ) |-> 200 W ( 65569 ) |-> 1 W ( 65570 ) |-> 0 W ( 65571 ) |-> 0 W ( 65572 ) |-> 8 W ( 65573 ) |-> 0 W ( 65574 ) |-> 0 W ( 65575 ) |-> 0 W ( 65576 ) |-> 52 W ( 65577 ) |-> 0 W ( 65578 ) |-> 32 W ( 65579 ) |-> 0 W ( 65580 ) |-> 1 W ( 65581 ) |-> 0 W ( 65582 ) |-> 40 W ( 65583 ) |-> 0 W ( 65584 ) |-> 5 W ( 65585 ) |-> 0 W ( 65586 ) |-> 4 W ( 65587 ) |-> 0 W ( 65588 ) |-> 1 W ( 65589 ) |-> 0 W ( 65590 ) |-> 0 W ( 65591 ) |-> 0 W ( 65592 ) |-> 0 W ( 65593 ) |-> 0 W ( 65594 ) |-> 0 W ( 65595 ) |-> 0 W ( 65596 ) |-> 0 W ( 65597 ) |-> 0 W ( 65598 ) |-> 1 W ( 65599 ) |-> 0 W ( 65600 ) |-> 0 W ( 65601 ) |-> 0 W ( 65602 ) |-> 1 W ( 65603 ) |-> 0 W ( 65604 ) |-> 100 W ( 65605 ) |-> 0 W ( 65606 ) |-> 0 W ( 65607 ) |-> 0 W ( 65608 ) |-> 100 W ( 65609 ) |-> 0 W ( 65610 ) |-> 0 W ( 65611 ) |-> 0 W ( 65612 ) |-> 5 W ( 65613 ) |-> 0 W ( 65614 ) |-> 0 W ( 65615 ) |-> 0 W ( 65616 ) |-> 0 W ( 65617 ) |-> 16 W ( 65618 ) |-> 0 W ( 65619 ) |-> 0 W ( 65620 ) |-> 55 W ( 65621 ) |-> 0 W ( 65622 ) |-> 1 W ( 65623 ) |-> 0 W ( 65624 ) |-> 183 W ( 65625 ) |-> 0 W ( 65626 ) |-> 0 W ( 65627 ) |-> 128 W ( 65628 ) |-> 55 W ( 65629 ) |-> 1 W ( 65630 ) |-> 0 W ( 65631 ) |-> 112 W ( 65632 ) |-> 19 W ( 65633 ) |-> 0 W ( 65634 ) |-> 0 W ( 65635 ) |-> 0
+    </mem>
   </riscv>
   <test>
+    <haltCond>
+      ADDRESS ( W ( 65632 ) )
+    </haltCond>
     <halt>
-      ADDRESS ( 65632 )
+      true
     </halt>
   </test>
   <generatedCounter>