2. The Processor Contract🔗

Janus 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 Janus

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 has two faces. The ordinary control face is a small accumulator machine: load immediates, load and store local memory, MAC from registers, branch, and halt. The kernel face is kmac: 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 Janus