2. What Every Instruction Means
The previous chapter wrote down Tilessa's vocabulary: the instructions and the configurations. This chapter supplies the meaning — for every instruction, exactly what happens to an element when it executes. Computer architects call this the semantics of an instruction set, and the important thing about ours is that it is not prose: it is a Lean function. You can run it. One definition serves three masters at once — it is the specification the hardware will be proved against, it is the reference simulator, and it is the text you are reading. They cannot drift apart, because they are the same artifact.
2.1. Architectural state
Strip away a processor's wiring and pipelines, and what remains — the part a programmer can actually observe — is a small bundle of values: where we are in the program, what the registers hold, what memory contains. That bundle is the architectural state, and for an element it is exactly four things: the program counter, 32 registers, the 64-bit accumulator, and the scratchpad. Every width comes from the configuration, so this one definition serves the tessera, the narrow variant, and the conductor alike.
namespace Tilessa
/-- A program: a total map from the 12-bit PC space to instructions.
Unused cells should map to `Instr.halt`. -/
def Program : Type := BitVec 12 → Instr
/-- Pointwise function update — register files and scratchpads are functions. -/
def upd {ι α : Type} [DecidableEq ι] (f : ι → α) (i : ι) (v : α) : ι → α :=
fun j => if j = i then v else f j
/-- Architectural state of one element, parameterized by its configuration. -/
structure State (cfg : CoreConfig) where
pc : BitVec 12
regs : Fin 32 → BitVec cfg.wordBits
acc : BitVec 64
scratch : Fin cfg.scratchWords → BitVec cfg.wordBits
/-- Reset state: everything zero. -/
def State.init (cfg : CoreConfig) : State cfg where
pc := 0
regs := fun _ => 0
acc := 0
scratch := fun _ => 0
2.2. The mesh interface
An element never sees the whole mesh — only its own four mailboxes. Each cycle, the picture it gets is simple: for every direction, may I send? (is my outgoing mailbox empty?) and is anything waiting for me? It responds with at most one push and one pop. And when an element tries to send into a full mailbox, or receive from an empty one, nothing dramatic happens: it stalls — holds its state and retries next cycle. Waiting is not an error; it is how the mesh breathes.
/-- What the element sees of its straps this cycle. -/
structure MeshIn (w : Nat) where
/-- The outgoing strap in direction `d` is empty and can accept a word. -/
canSend : Dir → Bool
/-- The word held by the incoming strap in direction `d`, if any. -/
inbox : Dir → Option (BitVec w)
/-- What the element does to its straps this cycle. -/
structure MeshOut (w : Nat) where
push : Option (Dir × BitVec w) := none
pop : Option Dir := none
2.3. The step function
Everything so far has been nouns. Here is the verb: one cycle of one
element, as a function. Given the program, what the element sees of its
mailboxes, and the current state, step returns one of three outcomes — a
successor state (plus any mailbox effects), a stall, or a halt. If you have
ever written an interpreter for a toy language, you already know the shape
of what follows: a processor's semantics is an interpreter whose language
happens to be machine instructions.
/-- ALU semantics. Shift amounts use the low bits of the second operand,
modulo the word width. -/
def aluEval {w : Nat} (op : AluOp) (a b : BitVec w) : BitVec w :=
match op with
| .add => a + b
| .sub => a - b
| .and => a &&& b
| .or => a ||| b
| .xor => a ^^^ b
| .sll => a <<< (b.toNat % w)
| .srl => a >>> (b.toNat % w)
| .sra => a.sshiftRight (b.toNat % w)
/-- The MAC product: signed `macBits × macBits`, sign-extended into the
64-bit accumulator domain. -/
def macProduct (cfg : CoreConfig) (a b : BitVec cfg.wordBits) : BitVec 64 :=
((a.setWidth cfg.macBits).signExtend 64) * ((b.setWidth cfg.macBits).signExtend 64)
/-- The outcome of one cycle. -/
inductive StepResult (cfg : CoreConfig) where
/-- Architectural state advances; straps are updated per the effects. -/
| next (s : State cfg) (out : MeshOut cfg.wordBits)
/-- Blocked on a strap; state unchanged, instruction retries. -/
| stall
/-- The uniform fault/termination outcome. -/
| halt
The fp, itof, and ftoi instructions belong to the hasFP extension; no
M0 instantiation enables it, and its semantics are specified together with a
future FP-enabled instantiation. Until then these instructions HALT on every
configuration, exactly like any absent unit.
/-- One cycle of one element. -/
def step (cfg : CoreConfig) (p : Program) (env : MeshIn cfg.wordBits)
(s : State cfg) : StepResult cfg :=
let pc' := s.pc + 1
match p s.pc with
| .alu op rd rs1 rs2 =>
let s' := { s with pc := pc',
regs := upd s.regs rd (aluEval op (s.regs rs1) (s.regs rs2)) }
.next s' {}
| .li rd imm =>
let s' := { s with pc := pc',
regs := upd s.regs rd (imm.signExtend cfg.wordBits) }
.next s' {}
| .mac rs1 rs2 =>
if cfg.hasMAC then
.next { s with pc := pc', acc := s.acc + macProduct cfg (s.regs rs1) (s.regs rs2) } {}
else .halt
| .macz =>
if cfg.hasMAC then .next { s with pc := pc', acc := 0 } {} else .halt
| .rdacc rd =>
if cfg.hasMAC then
let s' := { s with pc := pc',
regs := upd s.regs rd (s.acc.setWidth cfg.wordBits) }
.next s' {}
else .halt
| .fp _ _ _ _ => .halt
| .itof _ _ => .halt
| .ftoi _ _ => .halt
| .ldw rd addr =>
if h : addr.toNat < cfg.scratchWords then
let s' := { s with pc := pc',
regs := upd s.regs rd (s.scratch ⟨addr.toNat, h⟩) }
.next s' {}
else .halt
| .stw rs addr =>
if h : addr.toNat < cfg.scratchWords then
let s' := { s with pc := pc',
scratch := upd s.scratch ⟨addr.toNat, h⟩ (s.regs rs) }
.next s' {}
else .halt
| .send d rs =>
if env.canSend d then
.next { s with pc := pc' } { push := some (d, s.regs rs) }
else .stall
| .recv d rd =>
match env.inbox d with
| some v =>
.next { s with pc := pc', regs := upd s.regs rd v } { pop := some d }
| none => .stall
| .beq rs1 rs2 off =>
.next { s with pc := if s.regs rs1 = s.regs rs2 then s.pc + off else pc' } {}
| .bne rs1 rs2 off =>
.next { s with pc := if s.regs rs1 ≠ s.regs rs2 then s.pc + off else pc' } {}
| .blt rs1 rs2 off =>
.next { s with pc := if (s.regs rs1).slt (s.regs rs2) then s.pc + off else pc' } {}
| .jmp target => .next { s with pc := target } {}
| .nop => .next { s with pc := pc' } {}
| .halt => .halt
2.3.1. Determinism is definitional
Notice what kind of thing step is: a function. Same inputs, same output,
always. In most processor specifications determinism is a property someone
has to argue for; here it is baked into the very type of the definition,
and the theorem prover accepts the claim in one line because there is
nothing left to prove:
theorem step_deterministic (cfg : CoreConfig) (p : Program)
(env : MeshIn cfg.wordBits) (s : State cfg) {r₁ r₂ : StepResult cfg}
(h₁ : step cfg p env s = r₁) (h₂ : step cfg p env s = r₂) : r₁ = r₂ :=
h₁.symm.trans h₂
2.4. The strap
Between two elements sits the strap — the one-word mailbox from the
previous chapter, now as code. Notice what is absent: nothing in this
interface mentions time. push requires an empty mailbox, pop empties
it, and any number of cycles may pass between them. The mesh chapter will
lean on exactly that silence when it proves that a strap stretched across a
chip boundary is still, in every way that matters, a strap.
/-- The mesh strap: 1-deep, hold-until-pop. -/
structure Strap (w : Nat) where
q : Option (BitVec w) := none
def Strap.canPush {w : Nat} (st : Strap w) : Bool := st.q.isNone
def Strap.push {w : Nat} (_ : Strap w) (v : BitVec w) : Strap w := { q := some v }
def Strap.pop {w : Nat} (_ : Strap w) : Strap w := { q := none }
2.5. Running programs
A semantics you can run is a semantics you can test. runFor executes a
program for a bounded number of cycles (blocking and halting both stop this
simple clock — running stalls to completion is the mesh chapter's job,
since it needs the neighbours):
/-- Run `n` cycles (stall and halt both stop the clock here; the mesh-level
semantics, where stalls resolve as straps drain, is the next chapter). -/
def runFor (cfg : CoreConfig) (p : Program) (env : MeshIn cfg.wordBits) :
Nat → State cfg → State cfg
| 0, s => s
| n + 1, s =>
match step cfg p env s with
| .next s' _ => runFor cfg p env n s'
| _ => s
/-- A quiet mesh: sends always accepted, nothing to receive. -/
def quietEnv (w : Nat) : MeshIn w where
canSend := fun _ => true
inbox := fun _ => none
And now the book can check its own arithmetic. Here is a three-term dot product — ⟨1,2,3⟩·⟨4,5,6⟩ — as eleven instructions, executed through the semantics while the book compiles. If this program did not leave 32 in register 3, this page would not exist:
/-- li r1,k ; li r2,k' ; mac ×3 ; rdacc r3 ; halt -/
def dotProg : Program := fun pc =>
match pc.toNat with
| 0 => .macz
| 1 => .li 1 1 | 2 => .li 2 4 | 3 => .mac 1 2
| 4 => .li 1 2 | 5 => .li 2 5 | 6 => .mac 1 2
| 7 => .li 1 3 | 8 => .li 2 6 | 9 => .mac 1 2
| 10 => .rdacc 3
| _ => .halt
example :
(runFor tessera dotProg (quietEnv tessera.wordBits) 12
(State.init tessera)).regs 3 = 32 := ⊢ (runFor tessera dotProg (quietEnv tessera.wordBits) 12 (State.init tessera)).regs 3 = 32
All goals completed! 🐙
2.6. What refinement will say
A chapter of honesty about what has and has not been established. The
function step describes what an element should do: one instruction at a
time, in one tidy motion. Real hardware does no such thing — it overlaps
instructions in a pipeline and juggles several operations in flight at
once, because that is what makes it fast. The central obligation of this
entire project is a proof that the fast, messy machine and the tidy
specification agree: that everything the pipeline can do is something
step allows. Computer scientists call such a proof a refinement, and it
is the next chapter's work. When it is done, the chain of trust will run
unbroken from the page you just read down to the gates.
end Tilessa