Simple Sudoku Solver in Assembly

Welcome back to another round of Simple Sudoku Solvers! If you are unfamiliar with the series, I suggest you start with the first post or by perusing the backlog. Last time, in Agda, the solver wasn’t allowed to hand us a board without a correctness proof. Today we go in the opposite direction: assembly, where nothing is checked at all, and the machine stares at us directly. To be quite specific, today we’ll write AArch64 assembly for macOS, because that’s the machine I’m sitting at1. Surprisingly, the solver is just a little over 200 lines, and as always, the code is on GitHub. Why assembly? Season three is about solvers, specifications, and constraints, and assembly might seem like the odd duck. But I think it fits! After a proof assistant that checks everything, it’s worth looking at what’s left when nothing is checked, and nothing is proven. Nothing is hidden. There is no allocator, no garbage collector, no runtime, and no compiler making choices for us. The board gets copied because we wrote exactly the instructions that copy it. The machine already knows our tricks! We’ve been doing bit-twiddling with candidate masks since the Common Lisp episode, and in Forth we had to roll our own popcount and lowest-bit search. The CPU has instructions for most of that, and today we get to use them directly. So, in many ways, we gain some abstractions! The stack is, uh, the stack. In Forth we built our own stack of boards for backtracking. Here, the machine stack is right there, so we might as well use it. Since there are no types, everything is a number, and the only thing standing between us and a wrong answer is our own diligence. Fun! A quick primer on reading AArch64 If you’ve never read ARM assembly before, here is what you need for this post. AArch64 has 31 general-purpose registers, x0 to x30, each 64 bits wide. Writing w0 instead of x0 means “the lower 32 bits of register 0”, and since all of our numbers are small, we’ll use w registers most of the time. sp is the stack pointer. Instructions read like op destination, source, source, so add w0, w1, w2 means w0 = w1 + w2. Memory is only touched by loads and stores: ldrb w9, [x19, w21, uxtw] loads the byte at address x19 + w21 into w9, and strb stores one. [x7], #1 means “load from x7, then add 1 to x7”, which is handy for walking through memory. We call functions with bl, which jumps and stores the return address in x30, and we return with ret, which jumps back to x30. Arguments go in x0 and up, and the …