Tilessa

4. Composing the Mosaic🔗

So far this book has studied one element at a time, with its four mailboxes described from the inside: may I send? is anything waiting? This chapter turns the picture inside out. We place many elements side by side, wire each mailbox to a neighbour, and define what one clock cycle means for the whole mosaic — every element stepping at once, words moving between them. No approximations remain: the constant environment of the previous chapters is replaced by the real thing.

The payoff is two theorems with a physical flavour. In a machine where every element acts simultaneously, the classic dangers are collision (two parties touching the same mailbox in the same instant) and loss (a word overwritten before it was read). We prove neither can happen — not by adding interlocks, but because the strap discipline already forbids it: you may only put a word into an empty mailbox, and only take one from a full one, and a mailbox is never both.

4.1. Wiring🔗

Who is whose neighbour? We keep the answer abstract — a wiring is any assignment of a neighbouring element to each side of each element — and the torus of the specification chapter becomes one instance among many. Two elements are joined when my east is your west; a word I push east appears in your west-side mailbox.

namespace Tilessa /-- The opposite side: a word sent east arrives on a west-facing mailbox. -/ def Dir.opp : Dir → Dir | .east => .west | .west => .east | .north => .south | .south => .north /-- A wiring: for each element and each of its sides, the neighbouring element on that side. The torus is one instance; a 1-D ring or a test harness with self-loops are others. -/ structure Wiring (ι : Type) where next : ι → Dir → ι

4.2. The mosaic's state, and one shared clock cycle🔗

The state of a mosaic is the state of its elements, a halted flag per element (halting is per-element and permanent — a stopped element keeps its mailbox contents, and neighbours may still collect words it sent before stopping), and one strap per element per side: the mailbox for words leaving that element on that side.

/-- The whole mosaic: element states, per-element halt flags, and each element's four outgoing straps. -/ structure MeshState (ι : Type) (cfg : CoreConfig) where elem : ι → State cfg halted : ι → Bool strap : ι → Dir → Strap cfg.wordBits /-- What element `i` sees this cycle: it may send on side `d` when its own outgoing strap there is empty, and its inbox on side `d` is whatever its `d`-neighbour's facing strap holds. -/ def meshEnv {ι : Type} (w : Wiring ι) {cfg : CoreConfig} (ms : MeshState ι cfg) (i : ι) : MeshIn cfg.wordBits where canSend d := (ms.strap i d).canPush inbox d := (ms.strap (w.next i d) (Dir.opp d)).q

One cycle of the mosaic: every non-halted element takes one step with its real environment, all at once; then every strap settles — filled by its owner's push, emptied by its consumer's pop, or held.

/-- Element `i`'s outcome this cycle (halted elements rest, permanently). -/ def elemResult {ι : Type} (w : Wiring ι) {cfg : CoreConfig} (progs : ι → Program) (ms : MeshState ι cfg) (i : ι) : StepResult cfg := if ms.halted i then .stall else step cfg (progs i) (meshEnv w ms i) (ms.elem i) /-- One clock cycle of the whole mosaic. -/ def mstep {ι : Type} (w : Wiring ι) {cfg : CoreConfig} (progs : ι → Program) (ms : MeshState ι cfg) : MeshState ι cfg := let res := elemResult w progs ms { elem := fun i => match res i with | .next s _ => s | _ => ms.elem i halted := fun i => ms.halted i || match res i with | .halt => true | _ => false strap := fun i d => let pushed : Option (BitVec cfg.wordBits) := match res i with | .next _ out => match out.push with | some (d', v) => if d' = d then some v else none | none => none | _ => none let popped : Bool := match res (w.next i d) with | .next _ out => out.pop = some (Dir.opp d) | _ => false match pushed with | some v => (ms.strap i d).push v | none => if popped then (ms.strap i d).pop else ms.strap i d } /-- Run the mosaic for a bounded number of cycles. -/ def mrunFor {ι : Type} (w : Wiring ι) {cfg : CoreConfig} (progs : ι → Program) : Nat → MeshState ι cfg → MeshState ι cfg | 0, ms => ms | n + 1, ms => mrunFor w progs n (mstep w progs ms) /-- Executor bookkeeping, not mathematics: `mstep` describes each new state in terms of the old one, so running many cycles lazily would re-derive earlier cycles over and over. For a finite mosaic, `snap` materialises the three fields (forcing every entry once), keeping long runs linear. -/ def MeshState.snap {n : Nat} {cfg : CoreConfig} (ms : MeshState (Fin n) cfg) : MeshState (Fin n) cfg := let e := Vector.ofFn ms.elem let h := Vector.ofFn ms.halted let s := Vector.ofFn fun i => (ms.strap i .east, ms.strap i .west, ms.strap i .north, ms.strap i .south) { elem := fun i => e.get i halted := fun i => h.get i strap := fun i d => match d with | .east => (s.get i).1 | .west => (s.get i).2.1 | .north => (s.get i).2.2.1 | .south => (s.get i).2.2.2 } /-- `mrunFor`, snapshotting each cycle (finite mosaics). -/ def mrunSnap {n : Nat} (w : Wiring (Fin n)) {cfg : CoreConfig} (progs : Fin n → Program) : Nat → MeshState (Fin n) cfg → MeshState (Fin n) cfg | 0, ms => ms | k + 1, ms => mrunSnap w progs k (MeshState.snap (mstep w progs ms)) /-- Power-on: every element at reset, nothing halted, all mailboxes empty. -/ def MeshState.init (ι : Type) (cfg : CoreConfig) : MeshState ι cfg where elem := fun _ => State.init cfg halted := fun _ => false strap := fun _ _ => {}

4.3. Conservation of words🔗

The two safety facts. First, at the level of one element: step only ever pushes when it was told it may (the strap is empty), and only ever pops when there was something to take. These are facts about the semantics of send and recv — no other instruction touches a mailbox.

theorem step_push_guard {cfg : CoreConfig} {p : Program} {env : MeshIn cfg.wordBits} {s : State cfg} {s' : State cfg} {out : MeshOut cfg.wordBits} {d : Dir} {v : BitVec cfg.wordBits} (hstep : step cfg p env s = .next s' out) (hpush : out.push = some (d, v)) : env.canSend d = true := cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)op✝:AluOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.alu op✝ rd✝ rs1✝ rs2✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Regimm✝:BitVec 32hi:p s.pc = Instr.li rd✝ imm✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs1✝:Regrs2✝:Reghi:p s.pc = Instr.mac rs1✝ rs2✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)hi:p s.pc = Instr.macz⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Reghi:p s.pc = Instr.rdacc rd✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)op✝:FpOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.fp op✝ rd✝ rs1✝ rs2✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Regrs✝:Reghi:p s.pc = Instr.itof rd✝ rs✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Regrs✝:Reghi:p s.pc = Instr.ftoi rd✝ rs✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.ldw rd✝ addr✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)d✝:Dirrs✝:Reghi:p s.pc = Instr.send d✝ rs✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)d✝:Dirrd✝:Reghi:p s.pc = Instr.recv d✝ rd✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.beq rs1✝ rs2✝ offset✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.bne rs1✝ rs2✝ offset✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.blt rs1✝ rs2✝ offset✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)target✝:BitVec 12hi:p s.pc = Instr.jmp target✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)hi:p s.pc = Instr.nop⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)hi:p s.pc = Instr.halt⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)op✝:AluOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.alu op✝ rd✝ rs1✝ rs2✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Regimm✝:BitVec 32hi:p s.pc = Instr.li rd✝ imm✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs1✝:Regrs2✝:Reghi:p s.pc = Instr.mac rs1✝ rs2✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)hi:p s.pc = Instr.macz⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Reghi:p s.pc = Instr.rdacc rd✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)op✝:FpOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.fp op✝ rd✝ rs1✝ rs2✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Regrs✝:Reghi:p s.pc = Instr.itof rd✝ rs✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Regrs✝:Reghi:p s.pc = Instr.ftoi rd✝ rs✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rd✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.ldw rd✝ addr✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)d✝:Dirrs✝:Reghi:p s.pc = Instr.send d✝ rs✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)d✝:Dirrd✝:Reghi:p s.pc = Instr.recv d✝ rd✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.beq rs1✝ rs2✝ offset✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.bne rs1✝ rs2✝ offset✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)rs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.blt rs1✝ rs2✝ offset✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)target✝:BitVec 12hi:p s.pc = Instr.jmp target✝⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)hi:p s.pc = Instr.nop⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshstep:step cfg p env s = StepResult.next s' outhpush:out.push = some (d, v)hi:p s.pc = Instr.halt⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)hi:p s.pc = Instr.halthstep:StepResult.halt = StepResult.next s' out⊢ env.canSend d = true case li | nop cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)hi:p s.pc = Instr.nophstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := s.scratch } { } = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirv:BitVec cfg.wordBitshi:p s.pc = Instr.nophpush:{ }.push = some (d, v)⊢ env.canSend d = true; All goals completed! 🐙 case alu | fp cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)op✝:FpOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.fp op✝ rd✝ rs1✝ rs2✝hstep:StepResult.halt = StepResult.next s' out⊢ env.canSend d = true first | (All goals completed! 🐙; All goals completed! 🐙) | All goals completed! 🐙 case itof | ftoi | halt cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)hi:p s.pc = Instr.halthstep:StepResult.halt = StepResult.next s' out⊢ env.canSend d = true All goals completed! 🐙 case mac | macz | rdacc cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rd✝:Reghi:p s.pc = Instr.rdacc rd✝hstep:(if cfg.hasMAC = true then StepResult.next { pc := s.pc + 1, regs := upd s.regs rd✝ (BitVec.setWidth cfg.wordBits s.acc), acc := s.acc, scratch := s.scratch } { } else StepResult.halt) = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:cfg.hasMAC = truehstep:StepResult.next { pc := s.pc + 1, regs := upd s.regs rd✝ (BitVec.setWidth cfg.wordBits s.acc), acc := s.acc, scratch := s.scratch } { } = StepResult.next s' out⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:¬cfg.hasMAC = truehstep:StepResult.halt = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:cfg.hasMAC = truehstep:StepResult.next { pc := s.pc + 1, regs := upd s.regs rd✝ (BitVec.setWidth cfg.wordBits s.acc), acc := s.acc, scratch := s.scratch } { } = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirv:BitVec cfg.wordBitsrd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:cfg.hasMAC = truehpush:{ }.push = some (d, v)⊢ env.canSend d = true; All goals completed! 🐙 cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:¬cfg.hasMAC = truehstep:StepResult.halt = StepResult.next s' out⊢ env.canSend d = true All goals completed! 🐙 case ldw | stw cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝hstep:(if h : addr✝.toNat < cfg.scratchWords then StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := upd s.scratch ⟨addr✝.toNat, ⋯⟩ (s.regs rs✝) } { } else StepResult.halt) = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:addr✝.toNat < cfg.scratchWordshstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := upd s.scratch ⟨addr✝.toNat, ⋯⟩ (s.regs rs✝) } { } = StepResult.next s' out⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:¬addr✝.toNat < cfg.scratchWordshstep:StepResult.halt = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:addr✝.toNat < cfg.scratchWordshstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := upd s.scratch ⟨addr✝.toNat, ⋯⟩ (s.regs rs✝) } { } = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirv:BitVec cfg.wordBitsrs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:addr✝.toNat < cfg.scratchWordshpush:{ }.push = some (d, v)⊢ env.canSend d = true; All goals completed! 🐙 cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)rs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:¬addr✝.toNat < cfg.scratchWordshstep:StepResult.halt = StepResult.next s' out⊢ env.canSend d = true All goals completed! 🐙 case beq | bne | blt | jmp cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)target✝:BitVec 12hi:p s.pc = Instr.jmp target✝hstep:StepResult.next { pc := target✝, regs := s.regs, acc := s.acc, scratch := s.scratch } { } = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirv:BitVec cfg.wordBitstarget✝:BitVec 12hi:p s.pc = Instr.jmp target✝hpush:{ }.push = some (d, v)⊢ env.canSend d = true; All goals completed! 🐙 case send d0 rs cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝hstep:(if env.canSend d0 = true then StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := s.scratch } { push := some (d0, s.regs rs) } else StepResult.stall) = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h✝:env.canSend d0 = truehstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := s.scratch } { push := some (d0, s.regs rs) } = StepResult.next s' out⊢ env.canSend d = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h✝:¬env.canSend d0 = truehstep:StepResult.stall = StepResult.next s' out⊢ env.canSend d = true case isTrue h' cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h':env.canSend d0 = truehstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := s.scratch } { push := some (d0, s.regs rs) } = StepResult.next s' out⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirv:BitVec cfg.wordBitsd0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h':env.canSend d0 = truehpush:{ push := some (d0, s.regs rs) }.push = some (d, v)⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirv:BitVec cfg.wordBitsd0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h':env.canSend d0 = truehpush:d0 = d ∧ s.regs rs = v⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgv:BitVec cfg.wordBitsd0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h':env.canSend d0 = trueright✝:s.regs rs = v⊢ env.canSend d0 = true All goals completed! 🐙 case isFalse cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h✝:¬env.canSend d0 = truehstep:StepResult.stall = StepResult.next s' out⊢ env.canSend d = true All goals completed! 🐙 case recv d0 rd cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝hstep:(match env.inbox d0 with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' out⊢ env.canSend d = true cases henv : env.inbox d0 with cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝hstep:(match env.inbox d0 with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' outw0:BitVec cfg.wordBitshenv:env.inbox d0 = some w0⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝w0:BitVec cfg.wordBitshstep:(match some w0 with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' outhenv:env.inbox d0 = some w0⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirv:BitVec cfg.wordBitsd0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝w0:BitVec cfg.wordBitshenv:env.inbox d0 = some w0hpush:{ pop := some d0 }.push = some (d, v)⊢ env.canSend d = true All goals completed! 🐙 cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝hstep:(match env.inbox d0 with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' outhenv:env.inbox d0 = none⊢ env.canSend d = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirv:BitVec cfg.wordBitshpush:out.push = some (d, v)d0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝hstep:(match none with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' outhenv:env.inbox d0 = none⊢ env.canSend d = true; All goals completed! 🐙 theorem step_pop_guard {cfg : CoreConfig} {p : Program} {env : MeshIn cfg.wordBits} {s : State cfg} {s' : State cfg} {out : MeshOut cfg.wordBits} {d : Dir} (hstep : step cfg p env s = .next s' out) (hpop : out.pop = some d) : (env.inbox d).isSome := cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some d⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dop✝:AluOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.alu op✝ rd✝ rs1✝ rs2✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Regimm✝:BitVec 32hi:p s.pc = Instr.li rd✝ imm✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs1✝:Regrs2✝:Reghi:p s.pc = Instr.mac rs1✝ rs2✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dhi:p s.pc = Instr.macz⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Reghi:p s.pc = Instr.rdacc rd✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dop✝:FpOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.fp op✝ rd✝ rs1✝ rs2✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Regrs✝:Reghi:p s.pc = Instr.itof rd✝ rs✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Regrs✝:Reghi:p s.pc = Instr.ftoi rd✝ rs✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.ldw rd✝ addr✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dd✝:Dirrs✝:Reghi:p s.pc = Instr.send d✝ rs✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dd✝:Dirrd✝:Reghi:p s.pc = Instr.recv d✝ rd✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.beq rs1✝ rs2✝ offset✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.bne rs1✝ rs2✝ offset✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.blt rs1✝ rs2✝ offset✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dtarget✝:BitVec 12hi:p s.pc = Instr.jmp target✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dhi:p s.pc = Instr.nop⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dhi:p s.pc = Instr.halt⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dop✝:AluOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.alu op✝ rd✝ rs1✝ rs2✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Regimm✝:BitVec 32hi:p s.pc = Instr.li rd✝ imm✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs1✝:Regrs2✝:Reghi:p s.pc = Instr.mac rs1✝ rs2✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dhi:p s.pc = Instr.macz⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Reghi:p s.pc = Instr.rdacc rd✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dop✝:FpOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.fp op✝ rd✝ rs1✝ rs2✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Regrs✝:Reghi:p s.pc = Instr.itof rd✝ rs✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Regrs✝:Reghi:p s.pc = Instr.ftoi rd✝ rs✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drd✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.ldw rd✝ addr✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dd✝:Dirrs✝:Reghi:p s.pc = Instr.send d✝ rs✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dd✝:Dirrd✝:Reghi:p s.pc = Instr.recv d✝ rd✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.beq rs1✝ rs2✝ offset✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.bne rs1✝ rs2✝ offset✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some drs1✝:Regrs2✝:Regoffset✝:BitVec 12hi:p s.pc = Instr.blt rs1✝ rs2✝ offset✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dtarget✝:BitVec 12hi:p s.pc = Instr.jmp target✝⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dhi:p s.pc = Instr.nop⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhstep:step cfg p env s = StepResult.next s' outhpop:out.pop = some dhi:p s.pc = Instr.halt⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dhi:p s.pc = Instr.halthstep:StepResult.halt = StepResult.next s' out⊢ (env.inbox d).isSome = true case li | nop cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dhi:p s.pc = Instr.nophstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := s.scratch } { } = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirhi:p s.pc = Instr.nophpop:{ }.pop = some d⊢ (env.inbox d).isSome = true; All goals completed! 🐙 case alu | fp cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dop✝:FpOprd✝:Regrs1✝:Regrs2✝:Reghi:p s.pc = Instr.fp op✝ rd✝ rs1✝ rs2✝hstep:StepResult.halt = StepResult.next s' out⊢ (env.inbox d).isSome = true first | (All goals completed! 🐙; All goals completed! 🐙) | All goals completed! 🐙 case itof | ftoi | halt cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dhi:p s.pc = Instr.halthstep:StepResult.halt = StepResult.next s' out⊢ (env.inbox d).isSome = true All goals completed! 🐙 case mac | macz | rdacc cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drd✝:Reghi:p s.pc = Instr.rdacc rd✝hstep:(if cfg.hasMAC = true then StepResult.next { pc := s.pc + 1, regs := upd s.regs rd✝ (BitVec.setWidth cfg.wordBits s.acc), acc := s.acc, scratch := s.scratch } { } else StepResult.halt) = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:cfg.hasMAC = truehstep:StepResult.next { pc := s.pc + 1, regs := upd s.regs rd✝ (BitVec.setWidth cfg.wordBits s.acc), acc := s.acc, scratch := s.scratch } { } = StepResult.next s' out⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:¬cfg.hasMAC = truehstep:StepResult.halt = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:cfg.hasMAC = truehstep:StepResult.next { pc := s.pc + 1, regs := upd s.regs rd✝ (BitVec.setWidth cfg.wordBits s.acc), acc := s.acc, scratch := s.scratch } { } = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirrd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:cfg.hasMAC = truehpop:{ }.pop = some d⊢ (env.inbox d).isSome = true; All goals completed! 🐙 cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drd✝:Reghi:p s.pc = Instr.rdacc rd✝h✝:¬cfg.hasMAC = truehstep:StepResult.halt = StepResult.next s' out⊢ (env.inbox d).isSome = true All goals completed! 🐙 case ldw | stw cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝hstep:(if h : addr✝.toNat < cfg.scratchWords then StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := upd s.scratch ⟨addr✝.toNat, ⋯⟩ (s.regs rs✝) } { } else StepResult.halt) = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:addr✝.toNat < cfg.scratchWordshstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := upd s.scratch ⟨addr✝.toNat, ⋯⟩ (s.regs rs✝) } { } = StepResult.next s' out⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:¬addr✝.toNat < cfg.scratchWordshstep:StepResult.halt = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:addr✝.toNat < cfg.scratchWordshstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := upd s.scratch ⟨addr✝.toNat, ⋯⟩ (s.regs rs✝) } { } = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirrs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:addr✝.toNat < cfg.scratchWordshpop:{ }.pop = some d⊢ (env.inbox d).isSome = true; All goals completed! 🐙 cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some drs✝:Regaddr✝:BitVec 8hi:p s.pc = Instr.stw rs✝ addr✝h✝:¬addr✝.toNat < cfg.scratchWordshstep:StepResult.halt = StepResult.next s' out⊢ (env.inbox d).isSome = true All goals completed! 🐙 case beq | bne | blt | jmp cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dtarget✝:BitVec 12hi:p s.pc = Instr.jmp target✝hstep:StepResult.next { pc := target✝, regs := s.regs, acc := s.acc, scratch := s.scratch } { } = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dirtarget✝:BitVec 12hi:p s.pc = Instr.jmp target✝hpop:{ }.pop = some d⊢ (env.inbox d).isSome = true; All goals completed! 🐙 case send d0 rs cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝hstep:(if env.canSend d0 = true then StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := s.scratch } { push := some (d0, s.regs rs) } else StepResult.stall) = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h✝:env.canSend d0 = truehstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := s.scratch } { push := some (d0, s.regs rs) } = StepResult.next s' out⊢ (env.inbox d).isSome = truecfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h✝:¬env.canSend d0 = truehstep:StepResult.stall = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h✝:env.canSend d0 = truehstep:StepResult.next { pc := s.pc + 1, regs := s.regs, acc := s.acc, scratch := s.scratch } { push := some (d0, s.regs rs) } = StepResult.next s' out⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dird0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h✝:env.canSend d0 = truehpop:{ push := some (d0, s.regs rs) }.pop = some d⊢ (env.inbox d).isSome = true; All goals completed! 🐙 cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrs:Reghi:p s.pc = Instr.send d✝ rs✝h✝:¬env.canSend d0 = truehstep:StepResult.stall = StepResult.next s' out⊢ (env.inbox d).isSome = true All goals completed! 🐙 case recv d0 rd cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝hstep:(match env.inbox d0 with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' out⊢ (env.inbox d).isSome = true cases henv : env.inbox d0 with cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝hstep:(match env.inbox d0 with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' outw0:BitVec cfg.wordBitshenv:env.inbox d0 = some w0⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝w0:BitVec cfg.wordBitshstep:(match some w0 with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' outhenv:env.inbox d0 = some w0⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dird0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝w0:BitVec cfg.wordBitshenv:env.inbox d0 = some w0hpop:{ pop := some d0 }.pop = some d⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd:Dird0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝w0:BitVec cfg.wordBitshenv:env.inbox d0 = some w0hpop:d0 = d⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgd0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝w0:BitVec cfg.wordBitshenv:env.inbox d0 = some w0⊢ (env.inbox d0).isSome = true All goals completed! 🐙 cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝hstep:(match env.inbox d0 with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' outhenv:env.inbox d0 = none⊢ (env.inbox d).isSome = true cfg:CoreConfigp:Programenv:MeshIn cfg.wordBitss:State cfgs':State cfgout:MeshOut cfg.wordBitsd:Dirhpop:out.pop = some dd0:Dirrd:Reghi:p s.pc = Instr.recv d✝ rd✝hstep:(match none with | some v => StepResult.next { pc := s.pc + 1, regs := upd s.regs rd v, acc := s.acc, scratch := s.scratch } { pop := some d0 } | none => StepResult.stall) = StepResult.next s' outhenv:env.inbox d0 = none⊢ (env.inbox d).isSome = true; All goals completed! 🐙

Lifted to the mosaic, they become the physical guarantees: no strap is ever overwritten while full, and no strap is ever popped while empty — words are neither lost nor invented, in any mosaic, under any wiring, in any cycle.

theorem mesh_no_overwrite {ι : Type} (w : Wiring ι) {cfg : CoreConfig} (progs : ι → Program) (ms : MeshState ι cfg) (i : ι) (d : Dir) {s' : State cfg} {out : MeshOut cfg.wordBits} {v : BitVec cfg.wordBits} (hres : elemResult w progs ms i = .next s' out) (hpush : out.push = some (d, v)) : (ms.strap i d).q = none := ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshres:elemResult w progs ms i = StepResult.next s' outhpush:out.push = some (d, v)⊢ (ms.strap i d).q = none ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshres:(if ms.halted i = true then StepResult.stall else step cfg (progs i) (meshEnv w ms i) (ms.elem i)) = StepResult.next s' outhpush:out.push = some (d, v)⊢ (ms.strap i d).q = none ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:ms.halted i = truehres:StepResult.stall = StepResult.next s' out⊢ (ms.strap i d).q = noneι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:¬ms.halted i = truehres:step cfg (progs i) (meshEnv w ms i) (ms.elem i) = StepResult.next s' out⊢ (ms.strap i d).q = none ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:ms.halted i = truehres:StepResult.stall = StepResult.next s' out⊢ (ms.strap i d).q = none All goals completed! 🐙 ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:¬ms.halted i = truehres:step cfg (progs i) (meshEnv w ms i) (ms.elem i) = StepResult.next s' out⊢ (ms.strap i d).q = none ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitsv:BitVec cfg.wordBitshpush:out.push = some (d, v)h✝:¬ms.halted i = truehres:step cfg (progs i) (meshEnv w ms i) (ms.elem i) = StepResult.next s' outthis:(meshEnv w ms i).canSend d = true⊢ (ms.strap i d).q = none All goals completed! 🐙 theorem mesh_no_lost_pop {ι : Type} (w : Wiring ι) {cfg : CoreConfig} (progs : ι → Program) (ms : MeshState ι cfg) (i : ι) (d : Dir) {s' : State cfg} {out : MeshOut cfg.wordBits} (hres : elemResult w progs ms i = .next s' out) (hpop : out.pop = some d) : ((ms.strap (w.next i d) (Dir.opp d)).q).isSome := ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:elemResult w progs ms i = StepResult.next s' outhpop:out.pop = some d⊢ (ms.strap (w.next i d) d.opp).q.isSome = true ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshres:(if ms.halted i = true then StepResult.stall else step cfg (progs i) (meshEnv w ms i) (ms.elem i)) = StepResult.next s' outhpop:out.pop = some d⊢ (ms.strap (w.next i d) d.opp).q.isSome = true ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:ms.halted i = truehres:StepResult.stall = StepResult.next s' out⊢ (ms.strap (w.next i d) d.opp).q.isSome = trueι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:¬ms.halted i = truehres:step cfg (progs i) (meshEnv w ms i) (ms.elem i) = StepResult.next s' out⊢ (ms.strap (w.next i d) d.opp).q.isSome = true ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:ms.halted i = truehres:StepResult.stall = StepResult.next s' out⊢ (ms.strap (w.next i d) d.opp).q.isSome = true All goals completed! 🐙 ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:¬ms.halted i = truehres:step cfg (progs i) (meshEnv w ms i) (ms.elem i) = StepResult.next s' out⊢ (ms.strap (w.next i d) d.opp).q.isSome = true ι:Typew:Wiring ιcfg:CoreConfigprogs:ι → Programms:MeshState ι cfgi:ιd:Dirs':State cfgout:MeshOut cfg.wordBitshpop:out.pop = some dh✝:¬ms.halted i = truehres:step cfg (progs i) (meshEnv w ms i) (ms.elem i) = StepResult.next s' outthis:((meshEnv w ms i).inbox d).isSome = true⊢ (ms.strap (w.next i d) d.opp).q.isSome = true All goals completed! 🐙

4.4. The first conversation🔗

The book can now run a two-element mosaic during its own build. Element 0 loads 42 and sends it east; element 1 receives from the west and stops. The wiring is the smallest possible: 0's east side faces 1, 1's west side faces 0, and every other side loops back to its owner (a mailbox nobody reads).

/-- Two elements joined east–west. -/ def pairWiring : Wiring (Fin 2) where next i d := match i, d with | 0, .east => 1 | 1, .west => 0 | i, _ => i def senderProg : Program := fun pc => match pc.toNat with | 0 => .li 1 42 | 1 => .send .east 1 | _ => .halt def receiverProg : Program := fun pc => match pc.toNat with | 0 => .recv .west 2 | _ => .halt def pairProgs : Fin 2 → Program | 0 => senderProg | 1 => receiverProg /-- After a handful of cycles, the word has crossed: element 1's register 2 holds 42, and both elements have halted. Checked on every build. -/ example : let fin := mrunSnap pairWiring pairProgs 8 (MeshState.init (Fin 2) tessera) (fin.elem 1).regs 2 = 42 ∧ fin.halted 0 = true ∧ fin.halted 1 = true := ⊢ let fin := mrunSnap pairWiring pairProgs 8 (MeshState.init (Fin 2) tessera); (fin.elem 1).regs 2 = 42 ∧ fin.halted 0 = true ∧ fin.halted 1 = true All goals completed! 🐙

A word left one machine and arrived in another, inside a theorem prover, as a side effect of compiling a book. The remaining chapters of the mesh story build on exactly this: the boundary converters that turn floats into blocks at the edge, the serialized chip-edge strap — and the theorem that crossing a package boundary changes nothing, because nothing about a strap ever depended on where its two ends live.

end Tilessa