#The Hack ISA, Executed with Sail

Hack overview · 中文 · Next: Hack ISA →

This is an executable, educational model of the Hack ISA family. The default hack16 profile is the canonical nand2tetris machine; hack32 is a 32-bit Verylogic extension. Shared Sail semantics describe their ALU, registers, memory, and control flow, then Sail's C backend runs real Hack assembly programs.

If nand2tetris teaches how to build a computer from NAND gates, this repository explores the next abstraction boundary:

How do we turn the prose and encoding tables in a processor specification into a precise, testable, executable ISA model?

This tutorial focuses on the Hack module and its ISA-level behavior rather than gate-level circuitry or chip timing.

#Hack, nand2tetris, and Sail

#Where does Hack come from?

Hack is the 16-bit teaching computer from The Elements of Computing Systems, better known as nand2tetris. The course starts with NAND gates and proceeds through combinational logic, an ALU, registers, a CPU, an assembler, a virtual machine, a compiler, and an operating system.

The closest course units are:

• Project 05: Computer Architecture, which builds the Hack CPU, Memory, and Computer in HDL;
• Project 06: Assembler, which translates Hack assembly into 16-bit machine words;
• Chapters 4 and 5 of the book, which describe the machine language and hardware architecture.

nand2tetris is the course and project name. Hack is the CPU and ISA modeled here.

#What is Sail?

Sail is a strongly typed language for describing instruction-set architectures. A Sail model can express instruction encodings, decoded instruction forms, architectural state, and state transitions. Sail can type-check the model and generate implementations for backends including C and OCaml, as well as definitions for theorem-proving tools.

Sail resembles OCaml in places, but Sail is not OCaml. This repository uses Sail's type checker and C backend so that one compact ISA description serves as both readable specification and executable implementation. The workspace-level Why Sail guide compares this role with prose, C/C++, Verilog/SystemVerilog, ad hoc models, and proof assistants.

#Where does NandGame fit?

NandGame offers another excellent interactive route from a NAND gate to logic, arithmetic, a processor, and a computer. It is useful for building hardware intuition; nand2tetris provides the structured course and Hack platform; this repository focuses on executable ISA semantics. The three resources complement one another, but their circuit and instruction-set details should not be assumed to be identical.

#What you can learn here

By reading and running this repository, you can explore:

1. How Hack's two instruction forms map to hack16 and hack32 words.
2. Which parts of A, D, PC, and RAM form the architectural state.
3. How the C-instruction fields a, comp, dest, and jump define one state transition.
4. Why memory writes and jumps must use the old value of A when an instruction also updates A.
5. How assembly, machine code, a generated Sail driver, C code, and assertions form an end-to-end regression pipeline.

#Quick start

#1. Prepare the environment

Install Pixi, then run from the repository root:

pixi run just install
pixi run sail --version
pixi run just hack check

The repository pins Sail 0.20.2 under the Git-ignored .pixi/sail/; it never relies on an arbitrary Sail executable from the system PATH. Supported hosts are Windows AMD64, Linux x86_64, and Linux aarch64. This Sail release has no official macOS binary asset, so macOS is outside the supported host set.

Pixi also supplies Python, Pytest, Just, GCC or MinGW GCC, and GMP.

#2. Run the first Hack program

pixi run just hack list
pixi run just hack run multiply                    # defaults to hack16
pixi run just hack run multiply --profile hack32

The examples below continue with default hack16; hack32 follows the same source flow with 32-bit words and wider hexadecimal state output. multiply computes 6 × 7 with repeated addition. Its source is isa/hack/programs/multiply.asm:

.description Repeated-addition multiplication: 6 times 7

SET R0, 6
SET R1, 7
SET R2, 0

(LOOP)
JEQ R1, DONE
@R0
D=M
@R2
M=D+M
DEC R1
GOTO LOOP

(DONE)
HALT

.assert R2 == 42

SET, JEQ target, label, DEC, GOTO, and HALT are Hack+ pseudoinstructions supplied by this repository's assembler. The assembler replaces them with canonical A/C assembly before resolving labels, then emits machine words for the selected profile. For example:

// SET R0, 6
@6
D=A
@R0
M=D

// JEQ R1, DONE
@R1
D=M
@DONE
D;JEQ

Pseudoinstructions are therefore assembly conveniences, not additions to the ISA modeled in Sail. See How Hack+ lowers to real instructions for every expansion and its register side effects. .description emits no machine word: workflow uses it for discovery, and artifact.py preserves it as the annotated machine image manifest description.

#3. Observe .assert success and failure

The final line of multiply is:

.assert R2 == 42

The executor emits it as a Sail assertion in the generated driver. A successful run includes:

ASSERT PASS
A  = ...
D  = ...
PC = ...
R2 = 0x002A

If it is deliberately changed to .assert R2 == 43, the core diagnostic is similar to:

Assertion failed: assertion R2 == 0x002B from source line 20 failed

The generated program then exits with status 1, failing run or test. The diagnostic points to the original .asm line. Python workflow does not compare printed text; the actual judgment happens inside Sail. See the common teaching contract for shared equality/ordering syntax and Execution and tests for Hack targets.

#4. Inspect the real machine code

Assemble without running:

pixi run just hack assemble multiply
pixi run just hack run multiply full

The default summary level shows normalized source for every A/C word, marks Hack+ expansion as [i/n] source => canonical, and keeps inline assembly comments at the far right. Explicit full preserves exact source text and adds more driver-stage and assertion explanations. Use none when a bare artifact is more useful than teaching annotations.

The default command writes isa/hack/.build/hack16/asm/multiply/multiply.hack, containing standard 16-bit machine words plus source annotations. --profile hack32 writes the 32-bit artifact under .build/hack32/asm/multiply/ instead:

0000000000000110 // ROM[0000] L5 [1/4] SET R0, 6 => @6 // RAM[0] = multiplicand
1110110000010000 // ROM[0001] L5 [2/4] SET R0, 6 => D=A // RAM[0] = multiplicand

This is a useful bridge between the Project 06 encoding tables, assembly source, and Sail's decoder.

#A guided reading of the profile model

The model is intentionally split by responsibility:

1. Start with model/profiles/hack16.sail: it defines profile widths and legality, then includes the shared core.
2. Follow that include into model/core.sail for instruction/exception types, architectural state, the total 64-control ALU, fetch/decode/encode/execute, and hack_step().
3. Return to the bottom of hack16.sail for its scattered A/C mapping clauses, then compare hack32.sail and its different C envelope.
4. Open projects/hack16.sail_project and projects/hack32.sail_project: each complete build closure names only its one profile entry.

Both profiles keep a 15-bit PC, 32768-word ROM/RAM, and use old A[14:0] for RAM writes and jumps. In hack32, upper A bits still participate in 32-bit ALU computation. The assembler exposes only canonical nand2tetris comp mnemonics, while the shared gate-control ALU defines all 64 six-bit controls.

#Execution pipeline

programs/*.asm
  │  two-pass assembly and Hack+ expansion
  ▼
.build/<profile>/asm/<program>/<program>.hack
  │  reload words, assertions, and HALT metadata
  ▼
generated .driver.sail + projects/<profile>.sail_project
  │  Sail type checking and C backend
  ▼
.build/<profile>/asm/<program>/<program>.exe
  │  execute until HALT or a step limit; leaving the loaded image is an error
  ▼
evaluate source .assert directives

Reloading the .hack artifact is intentional: execution consumes exactly the machine words and metadata written to disk, with no hidden assembler state.

Important components:

• isa/hack/model/ and projects/*.sail_project: shared semantics and profile compositions;
• isa/hack/tools/assembler.py: two-pass assembler, Hack+ expansion, and annotated machine code;
• isa/hack/tools/executor.py: Sail driver generation, C-backend invocation, and execution;
• isa/hack/programs/*.asm: examples and end-to-end regressions;
• isa/hack/tests/sail/<profile>/conformance.sail: direct profile encoding, ALU, jump, destination, and transition checks;
• isa/hack/tests/: Python tests for the assembler and executor.

For the complete assertion, max_steps, pseudoinstruction, and annotated-file syntax, see the Hack package reference.

#Suggested exercises

#Compare source with machine encoding

1. Read the selected profile's mapping clauses, use encdec(instruction) directly for encoding, then follow the include to the legality-checking decode_hack in model/core.sail.
2. Write or modify a small standard Hack assembly program.
3. Run pixi run just hack assemble <name>.
4. Compare each generated word with the Project 06 tables.

#Add a Sail-level ALU check

Add an assertion to the relevant tests/sail/<profile>/conformance.sail, then run the narrow check followed by the complete test:

pixi run just hack check --profile hack32
pixi run just hack test

These tests call the Sail functions directly; Python does not simulate the ISA.

#Add a program

1. Add isa/hack/programs/<name>.asm; the filename stem becomes the program name.
2. Add one .description <nonempty text> for automatic discovery.
3. Put at least one .assert directive beside the source.
4. Run pixi run just hack run <name>.
5. Run pixi run just hack test for the complete package regression.

#Scope and limitations

The model deliberately stays at the ISA level:

• It implements A/C instructions, the ALU, registers, RAM, and PC transitions.
• The model treats the 15-bit address space as plain RAM; Screen and Keyboard memory-mapped device behavior is outside its scope.
• NAND gates, chip timing, and nand2tetris HDL are not simulated.
• Hack+ is assembler convenience syntax, not an ISA extension.
• Execution uses Sail's C backend and makes no claim that the model has been formally proved correct.

For learning how gates compose into a CPU, start with NandGame or nand2tetris Projects 01–05. For learning how to specify exactly what each CPU instruction does, start with one profile entry, follow its include into model/core.sail, then return to its mapping clauses.

#Further resources

Next: understand the Hack machine contract.