2. The Processor Contract🔗

Honeycomb starts with a hardware-facing contract. The state is finite-width where RTL will be finite-width: scalar registers, accumulator, architectural addresses, local indexes, resident weights, streamed operands, and local data memory are all part of the architectural state. Scalar/control words and addresses are 64-bit by default; kernel operands remain 32-bit elements so the MAC path does not inherit unnecessary scalar width. The first cell keeps 16-bit local address ports but uses 8-bit physical indexes for its inferred local memories. The semantics below are executable Lean definitions.

namespace Honeycomb

structure Config where
  xlen : Nat := 64
  addrBits : Nat := 64
  localAddrBits : Nat := 16
  memIndexBits : Nat := 8
  elemBits : Nat := 32
  accBits : Nat := 64
  regCount : Nat := 8
  blockSize : Nat := 32

def defaultConfig : Config := {}

abbrev Reg (cfg : Config) := Fin cfg.regCount
abbrev Word (cfg : Config) := BitVec cfg.xlen
abbrev Elem (cfg : Config) := BitVec cfg.elemBits
abbrev Acc (cfg : Config) := BitVec cfg.accBits
abbrev Addr (cfg : Config) := BitVec cfg.addrBits
abbrev LocalAddr (cfg : Config) := BitVec cfg.localAddrBits
abbrev MemIndex (cfg : Config) := BitVec cfg.memIndexBits

structure State (cfg : Config) where
  acc : Acc cfg
  regs : Reg cfg -> Word cfg
  pc : Addr cfg
  weights : Nat -> Elem cfg
  stream : Nat -> Elem cfg
  data : Nat -> Word cfg
  wptr : LocalAddr cfg
  sptr : LocalAddr cfg
  halted : Bool
  cycles : Nat
  retired : Nat

The instruction set is a small accumulator machine with one kernel fast path. The ordinary control instructions load immediates, load and store local memory, MAC from registers, branch, and halt. The kernel instruction kmac does one resident-weight read, one streamed-operand read, one multiply-add, and pointer increments.

inductive Instr (cfg : Config) where
  | mac (ra rb : Reg cfg)
  | kmac
  | clracc
  | movacc (rd : Reg cfg)
  | li (rd : Reg cfg) (imm : Int)
  | ld (rd ra : Reg cfg)
  | st (ra rs : Reg cfg)
  | setwptr (addr : Nat)
  | setsptr (addr : Nat)
  | blz (rs : Reg cfg) (off : Int)
  | halt

def Program (cfg : Config) := Nat -> Instr cfg

def readReg {cfg : Config} (s : State cfg) (r : Reg cfg) : Word cfg :=
  s.regs r
def readWeight {cfg : Config} (s : State cfg) (a : Nat) : Elem cfg :=
  s.weights a
def readStream {cfg : Config} (s : State cfg) (a : Nat) : Elem cfg :=
  s.stream a
def readData {cfg : Config} (s : State cfg) (a : Nat) : Word cfg :=
  s.data a

def updReg {cfg : Config} (f : Reg cfg -> Word cfg)
    (i : Reg cfg) (v : Word cfg) : Reg cfg -> Word cfg :=
  fun j => if j = i then v else f j

def updMem {cfg : Config} (m : Nat -> Word cfg)
    (a : Nat) (v : Word cfg) : Nat -> Word cfg :=
  fun b => if b = a then v else m b

The arithmetic contract is explicit: scalar words, elements, and accumulators wrap through BitVec.ofInt, while products are interpreted through signed element toInt. Overflow is not hidden. A result is exact when it fits the signed range of the destination width, and the theorem below is the bridge future RTL refinement proofs will use.

def wordOfInt (cfg : Config) (x : Int) : Word cfg :=
  BitVec.ofInt cfg.xlen x
def elemOfInt (cfg : Config) (x : Int) : Elem cfg :=
  BitVec.ofInt cfg.elemBits x
def elemOfWord (cfg : Config) (x : Word cfg) : Elem cfg :=
  elemOfInt cfg x.toInt
def accOfInt (cfg : Config) (x : Int) : Acc cfg :=
  BitVec.ofInt cfg.accBits x
def addrOfNat (cfg : Config) (x : Nat) : Addr cfg :=
  BitVec.ofNat cfg.addrBits x
def localAddrOfNat (cfg : Config) (x : Nat) : LocalAddr cfg :=
  BitVec.ofNat cfg.localAddrBits x
def memIndexOfNat (cfg : Config) (x : Nat) : Nat :=
  (BitVec.ofNat cfg.memIndexBits x : MemIndex cfg).toNat
def memIndexOfAddr (cfg : Config) (x : Addr cfg) : Nat :=
  memIndexOfNat cfg x.toNat
def memIndexOfLocal (cfg : Config) (x : LocalAddr cfg) : Nat :=
  memIndexOfNat cfg x.toNat
def memIndexOfWord (cfg : Config) (x : Word cfg) : Nat :=
  memIndexOfNat cfg x.toNat
def memDepth (cfg : Config) : Nat := 2 ^ cfg.memIndexBits
def nextPC (cfg : Config) (pc : Addr cfg) : Addr cfg :=
  addrOfNat cfg (pc.toNat + 1)
def nextLocal (cfg : Config) (a : LocalAddr cfg) : LocalAddr cfg :=
  localAddrOfNat cfg (a.toNat + 1)
def branchPC (cfg : Config) (pc : Addr cfg) (off : Int) : Addr cfg :=
  BitVec.ofInt cfg.addrBits (pc.toInt + off)
def product {cfg : Config} (a b : Elem cfg) : Int :=
  a.toInt * b.toInt
def accAddProduct (cfg : Config)
    (acc : Acc cfg) (a b : Elem cfg) : Acc cfg :=
  accOfInt cfg (acc.toInt + product a b)

def signedFits (bits : Nat) (x : Int) : Prop :=
  -2 ^ (bits - 1) <= x /\ x < 2 ^ (bits - 1)

theorem accOfInt_exact (cfg : Config) (hbits : 0 < cfg.accBits)
    {x : Int} (hx : signedFits cfg.accBits x) :
    (accOfInt cfg x).toInt = x := bycfg:Confighbits:0 < cfg.accBitsx:Inthx:signedFits cfg.accBits x⊢ BitVec.toInt (accOfInt cfg x) = x
  exact BitVec.toInt_ofInt_eq_self hbits hx.1 hx.2All goals completed! 🐙

theorem accAddProduct_exact (cfg : Config) (hbits : 0 < cfg.accBits)
    (acc : Acc cfg) (a b : Elem cfg)
    (hfit : signedFits cfg.accBits (acc.toInt + product a b)) :
    (accAddProduct cfg acc a b).toInt = acc.toInt + product a b := bycfg:Confighbits:0 < cfg.accBitsacc:Acc cfga:Elem cfgb:Elem cfghfit:signedFits cfg.accBits (BitVec.toInt acc + product a b)⊢ BitVec.toInt (accAddProduct cfg acc a b) = BitVec.toInt acc + product a b
  exact accOfInt_exact cfg hbits hfitAll goals completed! 🐙

The helper updates name each part of state that a future RTL block must drive. That keeps multi-field changes readable and makes proofs local.

def setAcc {cfg : Config} (s : State cfg) (a : Acc cfg) : State cfg :=
  { s with acc := a }
def setRegs {cfg : Config}
    (s : State cfg) (r : Reg cfg -> Word cfg) : State cfg :=
  { s with regs := r }
def setData {cfg : Config}
    (s : State cfg) (m : Nat -> Word cfg) : State cfg :=
  { s with data := m }
def setPtrs {cfg : Config} (s : State cfg)
    (wp sp : LocalAddr cfg) : State cfg :=
  { s with wptr := wp, sptr := sp }
def setHalted {cfg : Config} (s : State cfg) : State cfg :=
  { s with halted := true }

def retire {cfg : Config} (s : State cfg) (pc : Addr cfg) : State cfg :=
  { s with pc := pc, cycles := s.cycles + 1, retired := s.retired + 1 }

def retireHalt {cfg : Config} (s : State cfg) : State cfg :=
  { setHalted s with cycles := s.cycles + 1, retired := s.retired + 1 }

The step function is the processor contract. Register mac multiplies the low element-width view of each scalar register. kmac is the v1 kernel primitive: it reads the resident weight and stream operand at the physical memory indexes selected by the current local pointers, accumulates their signed product, and post-increments both pointers. The step function is intentionally small enough that every instruction can have a direct effect lemma.

def step (cfg : Config) (p : Program cfg)
    (s : State cfg) : Option (State cfg) :=
  if s.halted then none else
    match p s.pc.toNat with
    | .mac ra rb =>
        let x := elemOfWord cfg (readReg s ra)
        let y := elemOfWord cfg (readReg s rb)
        some (retire (setAcc s (accAddProduct cfg s.acc x y))
          (nextPC cfg s.pc))
    | .kmac =>
        let x := readWeight s (memIndexOfLocal cfg s.wptr)
        let y := readStream s (memIndexOfLocal cfg s.sptr)
        let s1 := setAcc s (accAddProduct cfg s.acc x y)
        some (retire (setPtrs s1 (nextLocal cfg s.wptr) (nextLocal cfg s.sptr))
          (nextPC cfg s.pc))
    | .clracc =>
        some (retire (setAcc s 0) (nextPC cfg s.pc))
    | .movacc rd =>
        let v := wordOfInt cfg (BitVec.toInt s.acc)
        some (retire (setRegs s (updReg s.regs rd v))
          (nextPC cfg s.pc))
    | .li rd imm =>
        let v := wordOfInt cfg imm
        some (retire (setRegs s (updReg s.regs rd v))
          (nextPC cfg s.pc))
    | .ld rd ra =>
        let addr := memIndexOfWord cfg (readReg s ra)
        let value := readData s addr
        some (retire (setRegs s (updReg s.regs rd value))
          (nextPC cfg s.pc))
    | .st ra rs =>
        let addr := memIndexOfWord cfg (readReg s ra)
        let value := readReg s rs
        some (retire (setData s (updMem s.data addr value))
          (nextPC cfg s.pc))
    | .setwptr addr =>
        some (retire (setPtrs s (localAddrOfNat cfg addr) s.sptr)
          (nextPC cfg s.pc))
    | .setsptr addr =>
        some (retire (setPtrs s s.wptr (localAddrOfNat cfg addr))
          (nextPC cfg s.pc))
    | .blz rs off =>
        let pc' :=
          if (readReg s rs).toInt <= 0 then branchPC cfg s.pc off
          else nextPC cfg s.pc
        some (retire s pc')
    | .halt =>
        some (retireHalt s)

def run (cfg : Config) (p : Program cfg) :
    Nat -> State cfg -> State cfg × Nat
  | 0, s => (s, 0)
  | fuel + 1, s =>
      match step cfg p s with
      | some s' =>
          let (sf, k) := run cfg p fuel s'
          (sf, k + 1)
      | none => (s, 0)

Determinism is immediate because step is a function. The useful local lemmas pin down the MAC datapath and the fused kernel datapath.

theorem step_deterministic (cfg : Config) (p : Program cfg)
    (s a b : State cfg)
    (ha : step cfg p s = some a)
    (hb : step cfg p s = some b) : a = b := bycfg:Configp:Program cfgs:State cfga:State cfgb:State cfgha:step cfg p s = some ahb:step cfg p s = some b⊢ a = b
  rw [hacfg:Configp:Program cfgs:State cfga:State cfgb:State cfgha:step cfg p s = some ahb:some a = some b⊢ a = b] at hbcfg:Configp:Program cfgs:State cfga:State cfgb:State cfgha:step cfg p s = some ahb:some a = some b⊢ a = b
  injection hbAll goals completed! 🐙

theorem mac_effect (cfg : Config) (p : Program cfg)
    (s : State cfg) (ra rb : Reg cfg)
    (hhalt : s.halted = false)
    (hop : p s.pc.toNat = .mac ra rb) :
    (step cfg p s).map (fun t => t.acc) =
      some (accAddProduct cfg s.acc
        (elemOfWord cfg (readReg s ra)) (elemOfWord cfg (readReg s rb))) := bycfg:Configp:Program cfgs:State cfgra:Reg cfgrb:Reg cfghhalt:s.halted = falsehop:p (BitVec.toNat s.pc) = Instr.mac ra rb⊢ Option.map (fun t => t.acc) (step cfg p s) =
  some (accAddProduct cfg s.acc (elemOfWord cfg (readReg s ra)) (elemOfWord cfg (readReg s rb)))
  simp [step, hhalt, hop, retire, setAcc, readReg, elemOfWord]All goals completed! 🐙

theorem kmac_effect (cfg : Config) (p : Program cfg) (s : State cfg)
    (hhalt : s.halted = false)
    (hop : p s.pc.toNat = .kmac) :
    (step cfg p s).map (fun t => (t.acc, t.wptr, t.sptr)) =
      some (accAddProduct cfg s.acc
        (readWeight s (memIndexOfLocal cfg s.wptr))
        (readStream s (memIndexOfLocal cfg s.sptr)),
        nextLocal cfg s.wptr, nextLocal cfg s.sptr) := bycfg:Configp:Program cfgs:State cfghhalt:s.halted = falsehop:p (BitVec.toNat s.pc) = Instr.kmac⊢ Option.map (fun t => (t.acc, t.wptr, t.sptr)) (step cfg p s) =
  some
    (accAddProduct cfg s.acc (readWeight s (memIndexOfLocal cfg s.wptr)) (readStream s (memIndexOfLocal cfg s.sptr)),
      nextLocal cfg s.wptr, nextLocal cfg s.sptr)
  simp [step, hhalt, hop, retire, setAcc, setPtrs,
    readWeight, readStream, nextLocal, memIndexOfLocal, memIndexOfNat]All goals completed! 🐙

theorem kmac_postinc_effect (cfg : Config) (p : Program cfg)
    (s : State cfg) (hhalt : s.halted = false)
    (hop : p s.pc.toNat = .kmac) :
    (step cfg p s).map (fun t => (t.acc, t.wptr, t.sptr)) =
      some (accAddProduct cfg s.acc
        (readWeight s (memIndexOfLocal cfg s.wptr))
        (readStream s (memIndexOfLocal cfg s.sptr)),
        nextLocal cfg s.wptr, nextLocal cfg s.sptr) :=
  kmac_effect cfg p s hhalt hop

The debug counters are architectural observations, not inputs to computation. The noninterference theorem makes that explicit.

structure ArchView (cfg : Config) where
  acc : Acc cfg
  regs : Reg cfg -> Word cfg
  pc : Addr cfg
  weights : Nat -> Elem cfg
  stream : Nat -> Elem cfg
  data : Nat -> Word cfg
  wptr : LocalAddr cfg
  sptr : LocalAddr cfg
  halted : Bool

def view {cfg : Config} (s : State cfg) : ArchView cfg :=
  { acc := s.acc, regs := s.regs, pc := s.pc, weights := s.weights,
    stream := s.stream, data := s.data, wptr := s.wptr, sptr := s.sptr,
    halted := s.halted }

def withCounters {cfg : Config} (s : State cfg)
    (cycles retired : Nat) : State cfg :=
  { s with cycles := cycles, retired := retired }

theorem debug_counters_noninterfering {cfg : Config}
    (s : State cfg) (cycles retired : Nat) :
    view (withCounters s cycles retired) = view s := rfl

end Honeycomb