13. Kernel Execution🔗

Honeycomb has ordinary control flow, but the core throughput path is intentionally branch-free: a straight sequence of resident-weight MACs over a streamed operand block. This chapter gives that path its own compact executor and proves that it computes the source dot product for all inputs.

namespace Honeycomb

structure KernelState where
  acc : Int
  weights : Nat -> Int
  stream : Nat -> Int
  wptr : Nat
  sptr : Nat

def fsumFrom (w a : Nat -> Int) (wp sp : Nat) : Nat -> Int
  | 0 => 0
  | n + 1 => w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) n

def kstep (s : KernelState) : KernelState :=
  let x := s.weights s.wptr
  let y := s.stream s.sptr
  { s with acc := s.acc + x * y, wptr := s.wptr + 1, sptr := s.sptr + 1 }

def krun : Nat -> KernelState -> KernelState
  | 0, s => s
  | n + 1, s => krun n (kstep s)

def srun : Nat -> KernelState -> KernelState := krun

theorem run_eq_srun_branchFree (n : Nat) (s : KernelState) :
    krun n s = srun n s := rfl

The accumulator invariant says exactly what has happened after n kernel cycles: the initial accumulator plus the dot product of the n resident and streamed operands starting at the two pointers.

theorem krun_acc : forall (n : Nat) (s : KernelState),
    (krun n s).acc =
      s.acc + fsumFrom s.weights s.stream s.wptr s.sptr n
  | 0, s =>s:KernelState⊢ (krun 0 s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr 0 bys:KernelState⊢ (krun 0 s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr 0
      simp [krun, fsumFrom]All goals completed! 🐙
  | n + 1, s =>n:Nats:KernelState⊢ (krun (n + 1) s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (n + 1) byn:Nats:KernelState⊢ (krun (n + 1) s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (n + 1)
      rw [krun,n:Nats:KernelState⊢ (krun n (kstep s)).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (n + 1) krun_acc nn:Nats:KernelState⊢ (kstep s).acc + fsumFrom (kstep s).weights (kstep s).stream (kstep s).wptr (kstep s).sptr n =
  s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (n + 1)]n:Nats:KernelState⊢ (kstep s).acc + fsumFrom (kstep s).weights (kstep s).stream (kstep s).wptr (kstep s).sptr n =
  s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (n + 1)
      change s.acc + s.weights s.wptr * s.stream s.sptr +
          fsumFrom s.weights s.stream (s.wptr + 1) (s.sptr + 1) n =
        s.acc + (s.weights s.wptr * s.stream s.sptr +
          fsumFrom s.weights s.stream (s.wptr + 1) (s.sptr + 1) n)n:Nats:KernelState⊢ s.acc + s.weights s.wptr * s.stream s.sptr + fsumFrom s.weights s.stream (s.wptr + 1) (s.sptr + 1) n =
  s.acc + (s.weights s.wptr * s.stream s.sptr + fsumFrom s.weights s.stream (s.wptr + 1) (s.sptr + 1) n)
      omegaAll goals completed! 🐙

def dotSpec (w a : Nat -> Int) (n : Nat) : Int :=
  fsumFrom w a 0 0 n

theorem kernelDot_correct (w a : Nat -> Int) (n : Nat) :
    (krun n (KernelState.mk 0 w a 0 0)).acc = dotSpec w a n := byw:Nat → Inta:Nat → Intn:Nat⊢ (krun n { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }).acc = dotSpec w a n
  rw [krun_accw:Nat → Inta:Nat → Intn:Nat⊢ { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.acc +
    fsumFrom { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.weights
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.stream
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.wptr
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.sptr n =
  dotSpec w a n]w:Nat → Inta:Nat → Intn:Nat⊢ { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.acc +
    fsumFrom { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.weights
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.stream
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.wptr
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.sptr n =
  dotSpec w a n
  simp [dotSpec]All goals completed! 🐙

The integer proof above is the source-level claim. The fixed-width hardware claim needs an overflow obligation: every prefix sum that may enter the accumulator must fit the configured signed accumulator width. This is stronger than a final-result-only check, because wrapping at an intermediate cycle would already have changed the later computation.

def kernelPrefixFits (cfg : Config) (s : KernelState) (n : Nat) : Prop :=
  forall k, k <= n ->
    signedFits cfg.accBits
      (s.acc + fsumFrom s.weights s.stream s.wptr s.sptr k)

theorem kernel_final_fits_of_prefixFits (cfg : Config)
    (s : KernelState) (n : Nat)
    (hfit : kernelPrefixFits cfg s n) :
    signedFits cfg.accBits (krun n s).acc := bycfg:Configs:KernelStaten:Nathfit:kernelPrefixFits cfg s n⊢ signedFits cfg.accBits (krun n s).acc
  rw [krun_acccfg:Configs:KernelStaten:Nathfit:kernelPrefixFits cfg s n⊢ signedFits cfg.accBits (s.acc + fsumFrom s.weights s.stream s.wptr s.sptr n)]cfg:Configs:KernelStaten:Nathfit:kernelPrefixFits cfg s n⊢ signedFits cfg.accBits (s.acc + fsumFrom s.weights s.stream s.wptr s.sptr n)
  exact hfit n (Nat.le_refl n)All goals completed! 🐙

theorem kernel_accumulator_exact_when_prefixFits (cfg : Config)
    (hbits : 0 < cfg.accBits) (s : KernelState) (n : Nat)
    (hfit : kernelPrefixFits cfg s n) :
    (accOfInt cfg (krun n s).acc).toInt = (krun n s).acc := bycfg:Confighbits:0 < cfg.accBitss:KernelStaten:Nathfit:kernelPrefixFits cfg s n⊢ BitVec.toInt (accOfInt cfg (krun n s).acc) = (krun n s).acc
  exact accOfInt_exact cfg hbits
    (kernel_final_fits_of_prefixFits cfg s n hfit)All goals completed! 🐙

A small executable smoke test stays in the book. If the semantics change, this example changes with it.

def wDemo : Nat -> Int :=
  fun i => match i with | 0 => 1 | 1 => 2 | 2 => 3 | _ => 0
def aDemo : Nat -> Int :=
  fun i => match i with | 0 => 4 | 1 => 5 | 2 => 6 | _ => 0

theorem kernelDot_demo : dotSpec wDemo aDemo 3 = 32 := by⊢ dotSpec wDemo aDemo 3 = 32
  native_decideAll goals completed! 🐙

end Honeycomb

13.1. The machine computes this dot product🔗

Everything above lives in the unbounded-Int kernel model. The gap the review flagged (R5): no theorem stitched n iterations of the fixed-width machine's kmac to krun n. This section closes it. The abstraction function kernelOf reads a machine state as a kernel state — the accumulator's integer value, and the weight/stream sequences as the machine will actually read them, with both hardware wraps (the 16-bit pointer and the 8-bit physical index) folded into the indexing. Under the same kernelPrefixFits obligation that guards every intermediate sum, n ISA steps of a resident kmac loop compute exactly krun n: the fixed-width machine performs the exact integer dot product, end to end.

namespace Honeycomb

/-- Append one term at the far end of the running sum. -/
theorem fsumFrom_snoc (w a : Nat -> Int) (wp sp : Nat) : forall k,
    fsumFrom w a wp sp (k + 1)
      = fsumFrom w a wp sp k + w (wp + k) * a (sp + k)
  | 0 =>w:Nat → Inta:Nat → Intwp:Natsp:Nat⊢ fsumFrom w a wp sp (0 + 1) = fsumFrom w a wp sp 0 + w (wp + 0) * a (sp + 0) byw:Nat → Inta:Nat → Intwp:Natsp:Nat⊢ fsumFrom w a wp sp (0 + 1) = fsumFrom w a wp sp 0 + w (wp + 0) * a (sp + 0) simp [fsumFrom]All goals completed! 🐙
  | k + 1 =>w:Nat → Inta:Nat → Intwp:Natsp:Natk:Nat⊢ fsumFrom w a wp sp (k + 1 + 1) = fsumFrom w a wp sp (k + 1) + w (wp + (k + 1)) * a (sp + (k + 1)) byw:Nat → Inta:Nat → Intwp:Natsp:Natk:Nat⊢ fsumFrom w a wp sp (k + 1 + 1) = fsumFrom w a wp sp (k + 1) + w (wp + (k + 1)) * a (sp + (k + 1))
      show w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) (k + 1) = _w:Nat → Inta:Nat → Intwp:Natsp:Natk:Nat⊢ w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) (k + 1) = fsumFrom w a wp sp (k + 1) + w (wp + (k + 1)) * a (sp + (k + 1))
      rw [fsumFrom_snoc w a (wp + 1) (sp + 1) kw:Nat → Inta:Nat → Intwp:Natsp:Natk:Nat⊢ w wp * a sp + (fsumFrom w a (wp + 1) (sp + 1) k + w (wp + 1 + k) * a (sp + 1 + k)) =
  fsumFrom w a wp sp (k + 1) + w (wp + (k + 1)) * a (sp + (k + 1))]w:Nat → Inta:Nat → Intwp:Natsp:Natk:Nat⊢ w wp * a sp + (fsumFrom w a (wp + 1) (sp + 1) k + w (wp + 1 + k) * a (sp + 1 + k)) =
  fsumFrom w a wp sp (k + 1) + w (wp + (k + 1)) * a (sp + (k + 1))
      show _ = w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) k
        + w (wp + (k + 1)) * a (sp + (k + 1))w:Nat → Inta:Nat → Intwp:Natsp:Natk:Nat⊢ w wp * a sp + (fsumFrom w a (wp + 1) (sp + 1) k + w (wp + 1 + k) * a (sp + 1 + k)) =
  w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) k + w (wp + (k + 1)) * a (sp + (k + 1))
      have h1 : wp + 1 + k = wp + (k + 1) := byw:Nat → Inta:Nat → Intwp:Natsp:Natk:Nat⊢ fsumFrom w a wp sp (k + 1 + 1) = fsumFrom w a wp sp (k + 1) + w (wp + (k + 1)) * a (sp + (k + 1)) omegaw:Nat → Inta:Nat → Intwp:Natsp:Natk:Nath1:wp + 1 + k = wp + (k + 1)⊢ w wp * a sp + (fsumFrom w a (wp + 1) (sp + 1) k + w (wp + 1 + k) * a (sp + 1 + k)) =
  w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) k + w (wp + (k + 1)) * a (sp + (k + 1))
      have h2 : sp + 1 + k = sp + (k + 1) := byw:Nat → Inta:Nat → Intwp:Natsp:Natk:Nat⊢ fsumFrom w a wp sp (k + 1 + 1) = fsumFrom w a wp sp (k + 1) + w (wp + (k + 1)) * a (sp + (k + 1)) omegaw:Nat → Inta:Nat → Intwp:Natsp:Natk:Nath1:wp + 1 + k = wp + (k + 1)h2:sp + 1 + k = sp + (k + 1)⊢ w wp * a sp + (fsumFrom w a (wp + 1) (sp + 1) k + w (wp + 1 + k) * a (sp + 1 + k)) =
  w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) k + w (wp + (k + 1)) * a (sp + (k + 1))
      rw [h1,w:Nat → Inta:Nat → Intwp:Natsp:Natk:Nath1:wp + 1 + k = wp + (k + 1)h2:sp + 1 + k = sp + (k + 1)⊢ w wp * a sp + (fsumFrom w a (wp + 1) (sp + 1) k + w (wp + (k + 1)) * a (sp + 1 + k)) =
  w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) k + w (wp + (k + 1)) * a (sp + (k + 1)) h2w:Nat → Inta:Nat → Intwp:Natsp:Natk:Nath1:wp + 1 + k = wp + (k + 1)h2:sp + 1 + k = sp + (k + 1)⊢ w wp * a sp + (fsumFrom w a (wp + 1) (sp + 1) k + w (wp + (k + 1)) * a (sp + (k + 1))) =
  w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) k + w (wp + (k + 1)) * a (sp + (k + 1))]w:Nat → Inta:Nat → Intwp:Natsp:Natk:Nath1:wp + 1 + k = wp + (k + 1)h2:sp + 1 + k = sp + (k + 1)⊢ w wp * a sp + (fsumFrom w a (wp + 1) (sp + 1) k + w (wp + (k + 1)) * a (sp + (k + 1))) =
  w wp * a sp + fsumFrom w a (wp + 1) (sp + 1) k + w (wp + (k + 1)) * a (sp + (k + 1))
      omegaAll goals completed! 🐙

/-- The 8-bit physical index ignores the 16-bit pointer wrap: reducing mod
`2^16` first changes nothing mod `2^8`. -/
theorem memIndexOfNat_mod65536 (x : Nat) :
    memIndexOfNat defaultConfig (x % 65536) = memIndexOfNat defaultConfig x := byx:Nat⊢ memIndexOfNat defaultConfig (x % 65536) = memIndexOfNat defaultConfig x
  simp [memIndexOfNat, BitVec.toNat_ofNat,
    show (2:Nat) ^ defaultConfig.memIndexBits = 256 from rfl]All goals completed! 🐙

/-- Likewise for the 64-bit program counter. -/
theorem memIndexOfNat_mod2_64 (x : Nat) :
    memIndexOfNat defaultConfig (x % 18446744073709551616)
      = memIndexOfNat defaultConfig x := byx:Nat⊢ memIndexOfNat defaultConfig (x % 18446744073709551616) = memIndexOfNat defaultConfig x
  simp [memIndexOfNat, BitVec.toNat_ofNat,
    show (2:Nat) ^ defaultConfig.memIndexBits = 256 from rfl]All goals completed! 🐙

/-- The kernel state a machine state denotes: the accumulator's integer value,
and the operand sequences as the machine will read them — index `i` is the
fixed-width read the hardware performs `i` kmacs from now, both wraps folded
in. -/
def kernelOf (s : State defaultConfig) : KernelState :=
  { acc := s.acc.toInt,
    weights := fun i =>
      (s.weights (memIndexOfNat defaultConfig (s.wptr.toNat + i))).toInt,
    stream := fun i =>
      (s.stream (memIndexOfNat defaultConfig (s.sptr.toNat + i))).toInt,
    wptr := 0, sptr := 0 }

/-- **The kmac-loop invariant.** Stepping a resident `kmac` loop `k`
instructions deep: the machine is still running, its memories are untouched,
its pointers and program counter have advanced with their wraps, and its
accumulator holds — exactly, as an integer — the kernel model's running sum.
-/
theorem kmac_loop_invariant (s0 : State defaultConfig)
    (imem : Nat -> DecodedInstr) (n : Nat) (hhalt : s0.halted = false)
    (hprog : forall k, k < n ->
      (imem (memIndexOfNat defaultConfig (s0.pc.toNat + k))).op = .kmac)
    (hfit : kernelPrefixFits defaultConfig (kernelOf s0) n) :
    forall k, k <= n -> exists sk,
      stepN (programOf imem) k s0 = some sk
      /\ sk.halted = false
      /\ sk.weights = s0.weights
      /\ sk.stream = s0.stream
      /\ sk.wptr.toNat = (s0.wptr.toNat + k) % 65536
      /\ sk.sptr.toNat = (s0.sptr.toNat + k) % 65536
      /\ sk.pc.toNat = (s0.pc.toNat + k) % 18446744073709551616
      /\ sk.acc.toInt = (krun k (kernelOf s0)).acc := bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) n⊢ ∀ (k : Nat),
  k ≤ n →
    ∃ sk,
      stepN (programOf imem) k s0 = some sk ∧
        sk.halted = false ∧
          sk.weights = s0.weights ∧
            sk.stream = s0.stream ∧
              BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
                BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                  BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                    BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc
  intro ks0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Nat⊢ k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc
  induction k with
  | zero =>zeros0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) n⊢ 0 ≤ n →
  ∃ sk,
    stepN (programOf imem) 0 s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + 0) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + 0) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + 0) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun 0 (kernelOf s0)).acc
    intro _zeros0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ n⊢ ∃ sk,
  stepN (programOf imem) 0 s0 = some sk ∧
    sk.halted = false ∧
      sk.weights = s0.weights ∧
        sk.stream = s0.stream ∧
          BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + 0) % 65536 ∧
            BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + 0) % 65536 ∧
              BitVec.toNat sk.pc = (BitVec.toNat s0.pc + 0) % 18446744073709551616 ∧
                BitVec.toInt sk.acc = (krun 0 (kernelOf s0)).acc
    refine ⟨s0, rfl, hhalt, rfl, rfl, ?_, ?_, ?_, ?_⟩zero.refine_1s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ n⊢ BitVec.toNat s0.wptr = (BitVec.toNat s0.wptr + 0) % 65536zero.refine_2s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ n⊢ BitVec.toNat s0.sptr = (BitVec.toNat s0.sptr + 0) % 65536zero.refine_3s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ n⊢ BitVec.toNat s0.pc = (BitVec.toNat s0.pc + 0) % 18446744073709551616zero.refine_4s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ n⊢ BitVec.toInt s0.acc = (krun 0 (kernelOf s0)).acc
    ·zero.refine_1s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ n⊢ BitVec.toNat s0.wptr = (BitVec.toNat s0.wptr + 0) % 65536 have hlt : s0.wptr.toNat < 65536 := s0.wptr.isLtzero.refine_1s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ nhlt:BitVec.toNat s0.wptr < 65536⊢ BitVec.toNat s0.wptr = (BitVec.toNat s0.wptr + 0) % 65536
      simpzero.refine_1s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ nhlt:BitVec.toNat s0.wptr < 65536⊢ BitVec.toNat s0.wptr = BitVec.toNat s0.wptr % 65536; omegaAll goals completed! 🐙
    ·zero.refine_2s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ n⊢ BitVec.toNat s0.sptr = (BitVec.toNat s0.sptr + 0) % 65536 have hlt : s0.sptr.toNat < 65536 := s0.sptr.isLtzero.refine_2s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ nhlt:BitVec.toNat s0.sptr < 65536⊢ BitVec.toNat s0.sptr = (BitVec.toNat s0.sptr + 0) % 65536
      simpzero.refine_2s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ nhlt:BitVec.toNat s0.sptr < 65536⊢ BitVec.toNat s0.sptr = BitVec.toNat s0.sptr % 65536; omegaAll goals completed! 🐙
    ·zero.refine_3s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ n⊢ BitVec.toNat s0.pc = (BitVec.toNat s0.pc + 0) % 18446744073709551616 have hlt : s0.pc.toNat < 18446744073709551616 := s0.pc.isLtzero.refine_3s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ nhlt:BitVec.toNat s0.pc < 18446744073709551616⊢ BitVec.toNat s0.pc = (BitVec.toNat s0.pc + 0) % 18446744073709551616
      simpzero.refine_3s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ nhlt:BitVec.toNat s0.pc < 18446744073709551616⊢ BitVec.toNat s0.pc = BitVec.toNat s0.pc % 18446744073709551616; omegaAll goals completed! 🐙
    ·zero.refine_4s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) na✝:0 ≤ n⊢ BitVec.toInt s0.acc = (krun 0 (kernelOf s0)).acc simp [krun, kernelOf]All goals completed! 🐙
  | succ k ih =>succs0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc⊢ k + 1 ≤ n →
  ∃ sk,
    stepN (programOf imem) (k + 1) s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + (k + 1)) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + (k + 1)) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun (k + 1) (kernelOf s0)).acc
    intro hksuccs0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ n⊢ ∃ sk,
  stepN (programOf imem) (k + 1) s0 = some sk ∧
    sk.halted = false ∧
      sk.weights = s0.weights ∧
        sk.stream = s0.stream ∧
          BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + (k + 1)) % 65536 ∧
            BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + (k + 1)) % 65536 ∧
              BitVec.toNat sk.pc = (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616 ∧
                BitVec.toInt sk.acc = (krun (k + 1) (kernelOf s0)).acc
    obtain ⟨sk, hstep, hh, hw, hs, hwp, hsp, hpc, hacc⟩ := ih (bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ n⊢ k ≤ n omegaAll goals completed! 🐙)succs0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc⊢ ∃ sk,
  stepN (programOf imem) (k + 1) s0 = some sk ∧
    sk.halted = false ∧
      sk.weights = s0.weights ∧
        sk.stream = s0.stream ∧
          BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + (k + 1)) % 65536 ∧
            BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + (k + 1)) % 65536 ∧
              BitVec.toNat sk.pc = (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616 ∧
                BitVec.toInt sk.acc = (krun (k + 1) (kernelOf s0)).acc
    -- the next instruction is the loop's kmac
    have hd : (imem (memIndexOfNat defaultConfig sk.pc.toNat)).op = .kmac := bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) n⊢ ∀ (k : Nat),
  k ≤ n →
    ∃ sk,
      stepN (programOf imem) k s0 = some sk ∧
        sk.halted = false ∧
          sk.weights = s0.weights ∧
            sk.stream = s0.stream ∧
              BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
                BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                  BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                    BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc
      rw [hpc,s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc⊢ (imem (memIndexOfNat defaultConfig ((BitVec.toNat s0.pc + k) % 18446744073709551616))).op = CellOp.kmac memIndexOfNat_mod2_64s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc⊢ (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmac]s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc⊢ (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmac
      exact hprog k (bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc⊢ k < n omegaAll goals completed! 🐙)succs0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmac⊢ ∃ sk,
  stepN (programOf imem) (k + 1) s0 = some sk ∧
    sk.halted = false ∧
      sk.weights = s0.weights ∧
        sk.stream = s0.stream ∧
          BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + (k + 1)) % 65536 ∧
            BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + (k + 1)) % 65536 ∧
              BitVec.toNat sk.pc = (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616 ∧
                BitVec.toInt sk.acc = (krun (k + 1) (kernelOf s0)).acc
    -- one more ISA step
    have hone := execDecoded_refines_step imem sk hhsuccs0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ ∃ sk,
  stepN (programOf imem) (k + 1) s0 = some sk ∧
    sk.halted = false ∧
      sk.weights = s0.weights ∧
        sk.stream = s0.stream ∧
          BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + (k + 1)) % 65536 ∧
            BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + (k + 1)) % 65536 ∧
              BitVec.toNat sk.pc = (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616 ∧
                BitVec.toInt sk.acc = (krun (k + 1) (kernelOf s0)).acc
    refine ⟨execDecoded (imem (memIndexOfNat defaultConfig sk.pc.toNat)) sk,
      ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩succ.refine_1s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ stepN (programOf imem) (k + 1) s0 = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)succ.refine_2s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk).halted = falsesucc.refine_3s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk).weights = s0.weightssucc.refine_4s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk).stream = s0.streamsucc.refine_5s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ BitVec.toNat (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk).wptr =
  (BitVec.toNat s0.wptr + (k + 1)) % 65536succ.refine_6s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ BitVec.toNat (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk).sptr =
  (BitVec.toNat s0.sptr + (k + 1)) % 65536succ.refine_7s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ BitVec.toNat (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk).pc =
  (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ BitVec.toInt (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk).acc =
  (krun (k + 1) (kernelOf s0)).acc
    ·succ.refine_1s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ stepN (programOf imem) (k + 1) s0 = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk) rw [stepN_succ_right,succ.refine_1s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ ((stepN (programOf imem) k s0).bind fun s' => step defaultConfig (programOf imem) s') =
  some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk) hstepsucc.refine_1s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ ((some sk).bind fun s' => step defaultConfig (programOf imem) s') =
  some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)]succ.refine_1s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchd:(imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))).op = CellOp.kmachone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)⊢ ((some sk).bind fun s' => step defaultConfig (programOf imem) s') =
  some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)
      simpa using honeAll goals completed! 🐙
    all_goals (
      generalize hgen : imem (memIndexOfNat defaultConfig sk.pc.toNat) = d at hd ⊢succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ BitVec.toInt (execDecoded d sk).acc = (krun (k + 1) (kernelOf s0)).acc
      simp only [execDecoded]succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ BitVec.toInt
    (match d.op with
      | CellOp.mac =>
        retire
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.kmac =>
        retire
          (setPtrs
            (setAcc sk
              (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
                (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
            (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
          (nextPC defaultConfig sk.pc)
      | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
      | CellOp.movacc =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
          (nextPC defaultConfig sk.pc)
      | CellOp.li =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
      | CellOp.ld =>
        retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
          (nextPC defaultConfig sk.pc)
      | CellOp.st =>
        retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
          (nextPC defaultConfig sk.pc)
      | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
      | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
      | CellOp.blz =>
        retire sk
          (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm
          else nextPC defaultConfig sk.pc)
      | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
      | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
      | CellOp.stw =>
        retire
          (setWeights sk
            (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.halt => retireHalt sk).acc =
  (krun (k + 1) (kernelOf s0)).acc
      rw [hdsucc.refine_2s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ (match CellOp.kmac with
    | CellOp.mac =>
      retire
        (setAcc sk
          (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
            (elemOfWord defaultConfig (readReg sk d.rb))))
        (nextPC defaultConfig sk.pc)
    | CellOp.kmac =>
      retire
        (setPtrs
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
              (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
          (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
        (nextPC defaultConfig sk.pc)
    | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
    | CellOp.movacc =>
      retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
        (nextPC defaultConfig sk.pc)
    | CellOp.li =>
      retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
    | CellOp.ld =>
      retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
        (nextPC defaultConfig sk.pc)
    | CellOp.st =>
      retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
        (nextPC defaultConfig sk.pc)
    | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
    | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
    | CellOp.blz =>
      retire sk
        (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm else nextPC defaultConfig sk.pc)
    | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
    | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
    | CellOp.stw =>
      retire
        (setWeights sk
          (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
            (elemOfWord defaultConfig (readReg sk d.rb))))
        (nextPC defaultConfig sk.pc)
    | CellOp.halt => retireHalt sk).halted =
  false]succ.refine_7s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ BitVec.toNat
    (match CellOp.kmac with
      | CellOp.mac =>
        retire
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.kmac =>
        retire
          (setPtrs
            (setAcc sk
              (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
                (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
            (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
          (nextPC defaultConfig sk.pc)
      | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
      | CellOp.movacc =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
          (nextPC defaultConfig sk.pc)
      | CellOp.li =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
      | CellOp.ld =>
        retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
          (nextPC defaultConfig sk.pc)
      | CellOp.st =>
        retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
          (nextPC defaultConfig sk.pc)
      | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
      | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
      | CellOp.blz =>
        retire sk
          (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm
          else nextPC defaultConfig sk.pc)
      | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
      | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
      | CellOp.stw =>
        retire
          (setWeights sk
            (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.halt => retireHalt sk).pc =
  (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ BitVec.toInt
    (match CellOp.kmac with
      | CellOp.mac =>
        retire
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.kmac =>
        retire
          (setPtrs
            (setAcc sk
              (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
                (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
            (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
          (nextPC defaultConfig sk.pc)
      | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
      | CellOp.movacc =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
          (nextPC defaultConfig sk.pc)
      | CellOp.li =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
      | CellOp.ld =>
        retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
          (nextPC defaultConfig sk.pc)
      | CellOp.st =>
        retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
          (nextPC defaultConfig sk.pc)
      | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
      | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
      | CellOp.blz =>
        retire sk
          (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm
          else nextPC defaultConfig sk.pc)
      | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
      | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
      | CellOp.stw =>
        retire
          (setWeights sk
            (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.halt => retireHalt sk).acc =
  (krun (k + 1) (kernelOf s0)).acc)
    ·succ.refine_2s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ (match CellOp.kmac with
    | CellOp.mac =>
      retire
        (setAcc sk
          (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
            (elemOfWord defaultConfig (readReg sk d.rb))))
        (nextPC defaultConfig sk.pc)
    | CellOp.kmac =>
      retire
        (setPtrs
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
              (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
          (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
        (nextPC defaultConfig sk.pc)
    | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
    | CellOp.movacc =>
      retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
        (nextPC defaultConfig sk.pc)
    | CellOp.li =>
      retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
    | CellOp.ld =>
      retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
        (nextPC defaultConfig sk.pc)
    | CellOp.st =>
      retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
        (nextPC defaultConfig sk.pc)
    | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
    | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
    | CellOp.blz =>
      retire sk
        (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm else nextPC defaultConfig sk.pc)
    | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
    | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
    | CellOp.stw =>
      retire
        (setWeights sk
          (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
            (elemOfWord defaultConfig (readReg sk d.rb))))
        (nextPC defaultConfig sk.pc)
    | CellOp.halt => retireHalt sk).halted =
  false -- halted: retire preserves it
      simp [retire, setPtrs, setAcc, hh]All goals completed! 🐙
    ·succ.refine_3s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ (match CellOp.kmac with
    | CellOp.mac =>
      retire
        (setAcc sk
          (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
            (elemOfWord defaultConfig (readReg sk d.rb))))
        (nextPC defaultConfig sk.pc)
    | CellOp.kmac =>
      retire
        (setPtrs
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
              (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
          (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
        (nextPC defaultConfig sk.pc)
    | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
    | CellOp.movacc =>
      retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
        (nextPC defaultConfig sk.pc)
    | CellOp.li =>
      retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
    | CellOp.ld =>
      retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
        (nextPC defaultConfig sk.pc)
    | CellOp.st =>
      retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
        (nextPC defaultConfig sk.pc)
    | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
    | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
    | CellOp.blz =>
      retire sk
        (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm else nextPC defaultConfig sk.pc)
    | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
    | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
    | CellOp.stw =>
      retire
        (setWeights sk
          (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
            (elemOfWord defaultConfig (readReg sk d.rb))))
        (nextPC defaultConfig sk.pc)
    | CellOp.halt => retireHalt sk).weights =
  s0.weights simp [retire, setPtrs, setAcc, hw]All goals completed! 🐙
    ·succ.refine_4s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ (match CellOp.kmac with
    | CellOp.mac =>
      retire
        (setAcc sk
          (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
            (elemOfWord defaultConfig (readReg sk d.rb))))
        (nextPC defaultConfig sk.pc)
    | CellOp.kmac =>
      retire
        (setPtrs
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
              (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
          (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
        (nextPC defaultConfig sk.pc)
    | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
    | CellOp.movacc =>
      retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
        (nextPC defaultConfig sk.pc)
    | CellOp.li =>
      retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
    | CellOp.ld =>
      retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
        (nextPC defaultConfig sk.pc)
    | CellOp.st =>
      retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
        (nextPC defaultConfig sk.pc)
    | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
    | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
    | CellOp.blz =>
      retire sk
        (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm else nextPC defaultConfig sk.pc)
    | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
    | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
    | CellOp.stw =>
      retire
        (setWeights sk
          (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
            (elemOfWord defaultConfig (readReg sk d.rb))))
        (nextPC defaultConfig sk.pc)
    | CellOp.halt => retireHalt sk).stream =
  s0.stream simp [retire, setPtrs, setAcc, hs]All goals completed! 🐙
    ·succ.refine_5s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ BitVec.toNat
    (match CellOp.kmac with
      | CellOp.mac =>
        retire
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.kmac =>
        retire
          (setPtrs
            (setAcc sk
              (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
                (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
            (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
          (nextPC defaultConfig sk.pc)
      | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
      | CellOp.movacc =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
          (nextPC defaultConfig sk.pc)
      | CellOp.li =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
      | CellOp.ld =>
        retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
          (nextPC defaultConfig sk.pc)
      | CellOp.st =>
        retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
          (nextPC defaultConfig sk.pc)
      | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
      | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
      | CellOp.blz =>
        retire sk
          (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm
          else nextPC defaultConfig sk.pc)
      | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
      | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
      | CellOp.stw =>
        retire
          (setWeights sk
            (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.halt => retireHalt sk).wptr =
  (BitVec.toNat s0.wptr + (k + 1)) % 65536 -- wptr advances with its wrap
      simp [retire, setPtrs, setAcc, nextLocal, localAddrOfNat, BitVec.toNat_ofNat,
        show (2:Nat) ^ defaultConfig.localAddrBits = 65536 from rfl]succ.refine_5s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ (BitVec.toNat sk.wptr + 1) % 65536 = (BitVec.toNat s0.wptr + (k + 1)) % 65536
      rw [hwpsucc.refine_5s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ ((BitVec.toNat s0.wptr + k) % 65536 + 1) % 65536 = (BitVec.toNat s0.wptr + (k + 1)) % 65536]succ.refine_5s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ ((BitVec.toNat s0.wptr + k) % 65536 + 1) % 65536 = (BitVec.toNat s0.wptr + (k + 1)) % 65536
      omegaAll goals completed! 🐙
    ·succ.refine_6s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ BitVec.toNat
    (match CellOp.kmac with
      | CellOp.mac =>
        retire
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.kmac =>
        retire
          (setPtrs
            (setAcc sk
              (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
                (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
            (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
          (nextPC defaultConfig sk.pc)
      | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
      | CellOp.movacc =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
          (nextPC defaultConfig sk.pc)
      | CellOp.li =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
      | CellOp.ld =>
        retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
          (nextPC defaultConfig sk.pc)
      | CellOp.st =>
        retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
          (nextPC defaultConfig sk.pc)
      | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
      | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
      | CellOp.blz =>
        retire sk
          (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm
          else nextPC defaultConfig sk.pc)
      | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
      | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
      | CellOp.stw =>
        retire
          (setWeights sk
            (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.halt => retireHalt sk).sptr =
  (BitVec.toNat s0.sptr + (k + 1)) % 65536 simp [retire, setPtrs, setAcc, nextLocal, localAddrOfNat, BitVec.toNat_ofNat,
        show (2:Nat) ^ defaultConfig.localAddrBits = 65536 from rfl]succ.refine_6s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ (BitVec.toNat sk.sptr + 1) % 65536 = (BitVec.toNat s0.sptr + (k + 1)) % 65536
      rw [hspsucc.refine_6s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ ((BitVec.toNat s0.sptr + k) % 65536 + 1) % 65536 = (BitVec.toNat s0.sptr + (k + 1)) % 65536]succ.refine_6s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ ((BitVec.toNat s0.sptr + k) % 65536 + 1) % 65536 = (BitVec.toNat s0.sptr + (k + 1)) % 65536
      omegaAll goals completed! 🐙
    ·succ.refine_7s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ BitVec.toNat
    (match CellOp.kmac with
      | CellOp.mac =>
        retire
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.kmac =>
        retire
          (setPtrs
            (setAcc sk
              (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
                (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
            (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
          (nextPC defaultConfig sk.pc)
      | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
      | CellOp.movacc =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
          (nextPC defaultConfig sk.pc)
      | CellOp.li =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
      | CellOp.ld =>
        retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
          (nextPC defaultConfig sk.pc)
      | CellOp.st =>
        retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
          (nextPC defaultConfig sk.pc)
      | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
      | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
      | CellOp.blz =>
        retire sk
          (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm
          else nextPC defaultConfig sk.pc)
      | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
      | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
      | CellOp.stw =>
        retire
          (setWeights sk
            (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.halt => retireHalt sk).pc =
  (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616 simp [retire, setPtrs, setAcc, nextPC, addrOfNat, BitVec.toNat_ofNat,
        show (2:Nat) ^ defaultConfig.addrBits = 18446744073709551616 from rfl]succ.refine_7s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ (BitVec.toNat sk.pc + 1) % 18446744073709551616 = (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616
      rw [hpcsucc.refine_7s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ ((BitVec.toNat s0.pc + k) % 18446744073709551616 + 1) % 18446744073709551616 =
  (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616]succ.refine_7s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ ((BitVec.toNat s0.pc + k) % 18446744073709551616 + 1) % 18446744073709551616 =
  (BitVec.toNat s0.pc + (k + 1)) % 18446744073709551616
      omegaAll goals completed! 🐙
    ·succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ BitVec.toInt
    (match CellOp.kmac with
      | CellOp.mac =>
        retire
          (setAcc sk
            (accAddProduct defaultConfig sk.acc (elemOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.kmac =>
        retire
          (setPtrs
            (setAcc sk
              (accAddProduct defaultConfig sk.acc (readWeight sk (memIndexOfLocal defaultConfig sk.wptr))
                (readStream sk (memIndexOfLocal defaultConfig sk.sptr))))
            (nextLocal defaultConfig sk.wptr) (nextLocal defaultConfig sk.sptr))
          (nextPC defaultConfig sk.pc)
      | CellOp.clracc => retire (setAcc sk 0) (nextPC defaultConfig sk.pc)
      | CellOp.movacc =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig (BitVec.toInt sk.acc))))
          (nextPC defaultConfig sk.pc)
      | CellOp.li =>
        retire (setRegs sk (updReg sk.regs d.rd (wordOfInt defaultConfig d.imm))) (nextPC defaultConfig sk.pc)
      | CellOp.ld =>
        retire (setRegs sk (updReg sk.regs d.rd (readData sk (memIndexOfWord defaultConfig (readReg sk d.ra)))))
          (nextPC defaultConfig sk.pc)
      | CellOp.st =>
        retire (setData sk (updMem sk.data (memIndexOfWord defaultConfig (readReg sk d.ra)) (readReg sk d.rb)))
          (nextPC defaultConfig sk.pc)
      | CellOp.setwptr => retire (setPtrs sk (localAddrOfNat defaultConfig d.addr) sk.sptr) (nextPC defaultConfig sk.pc)
      | CellOp.setsptr => retire (setPtrs sk sk.wptr (localAddrOfNat defaultConfig d.addr)) (nextPC defaultConfig sk.pc)
      | CellOp.blz =>
        retire sk
          (if BitVec.toInt (readReg sk d.ra) ≤ 0 then branchPC defaultConfig sk.pc d.imm
          else nextPC defaultConfig sk.pc)
      | CellOp.alu => execAlu (functOf d.addr) d.rd d.ra d.rb sk
      | CellOp.jr => retire sk (jumpPC defaultConfig (readReg sk d.ra))
      | CellOp.stw =>
        retire
          (setWeights sk
            (updWeight sk.weights (memIndexOfWord defaultConfig (readReg sk d.ra))
              (elemOfWord defaultConfig (readReg sk d.rb))))
          (nextPC defaultConfig sk.pc)
      | CellOp.halt => retireHalt sk).acc =
  (krun (k + 1) (kernelOf s0)).acc -- the accumulator stays exact: the (k+1)-prefix fits
      simp only [retire, setPtrs, setAcc, accAddProduct, readWeight, readStream,
        memIndexOfLocal]succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (sk.weights (memIndexOfNat defaultConfig (BitVec.toNat sk.wptr)))
          (sk.stream (memIndexOfNat defaultConfig (BitVec.toNat sk.sptr))))) =
  (krun (k + 1) (kernelOf s0)).acc
      have hidxw : memIndexOfNat defaultConfig sk.wptr.toNat
          = memIndexOfNat defaultConfig (s0.wptr.toNat + k) := bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) n⊢ ∀ (k : Nat),
  k ≤ n →
    ∃ sk,
      stepN (programOf imem) k s0 = some sk ∧
        sk.halted = false ∧
          sk.weights = s0.weights ∧
            sk.stream = s0.stream ∧
              BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
                BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                  BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                    BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc
        rw [hwp,s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ memIndexOfNat defaultConfig ((BitVec.toNat s0.wptr + k) % 65536) =
  memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k) memIndexOfNat_mod65536s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmac⊢ memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)]succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (sk.weights (memIndexOfNat defaultConfig (BitVec.toNat sk.wptr)))
          (sk.stream (memIndexOfNat defaultConfig (BitVec.toNat sk.sptr))))) =
  (krun (k + 1) (kernelOf s0)).acc
      have hidxs : memIndexOfNat defaultConfig sk.sptr.toNat
          = memIndexOfNat defaultConfig (s0.sptr.toNat + k) := bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) n⊢ ∀ (k : Nat),
  k ≤ n →
    ∃ sk,
      stepN (programOf imem) k s0 = some sk ∧
        sk.halted = false ∧
          sk.weights = s0.weights ∧
            sk.stream = s0.stream ∧
              BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
                BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                  BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                    BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc
        rw [hsp,s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)⊢ memIndexOfNat defaultConfig ((BitVec.toNat s0.sptr + k) % 65536) =
  memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k) memIndexOfNat_mod65536s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)⊢ memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)]succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (sk.weights (memIndexOfNat defaultConfig (BitVec.toNat sk.wptr)))
          (sk.stream (memIndexOfNat defaultConfig (BitVec.toNat sk.sptr))))) =
  (krun (k + 1) (kernelOf s0)).acc
      rw [hidxw,succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (sk.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)))
          (sk.stream (memIndexOfNat defaultConfig (BitVec.toNat sk.sptr))))) =
  (krun (k + 1) (kernelOf s0)).acc hidxs,succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (sk.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)))
          (sk.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k))))) =
  (krun (k + 1) (kernelOf s0)).acc hw,succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)))
          (sk.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k))))) =
  (krun (k + 1) (kernelOf s0)).acc hssucc.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)))
          (s0.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k))))) =
  (krun (k + 1) (kernelOf s0)).acc]succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)))
          (s0.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k))))) =
  (krun (k + 1) (kernelOf s0)).acc
      have hsum : sk.acc.toInt
            + ((kernelOf s0).weights k) * ((kernelOf s0).stream k)
          = (krun (k + 1) (kernelOf s0)).acc := bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) n⊢ ∀ (k : Nat),
  k ≤ n →
    ∃ sk,
      stepN (programOf imem) k s0 = some sk ∧
        sk.halted = false ∧
          sk.weights = s0.weights ∧
            sk.stream = s0.stream ∧
              BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
                BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                  BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                    BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc
        rw [hacc,s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ (krun k (kernelOf s0)).acc + (kernelOf s0).weights k * (kernelOf s0).stream k = (krun (k + 1) (kernelOf s0)).acc krun_acc,s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ (kernelOf s0).acc + fsumFrom (kernelOf s0).weights (kernelOf s0).stream (kernelOf s0).wptr (kernelOf s0).sptr k +
    (kernelOf s0).weights k * (kernelOf s0).stream k =
  (krun (k + 1) (kernelOf s0)).acc krun_acc,s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ (kernelOf s0).acc + fsumFrom (kernelOf s0).weights (kernelOf s0).stream (kernelOf s0).wptr (kernelOf s0).sptr k +
    (kernelOf s0).weights k * (kernelOf s0).stream k =
  (kernelOf s0).acc + fsumFrom (kernelOf s0).weights (kernelOf s0).stream (kernelOf s0).wptr (kernelOf s0).sptr (k + 1) fsumFrom_snocs0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ (kernelOf s0).acc + fsumFrom (kernelOf s0).weights (kernelOf s0).stream (kernelOf s0).wptr (kernelOf s0).sptr k +
    (kernelOf s0).weights k * (kernelOf s0).stream k =
  (kernelOf s0).acc +
    (fsumFrom (kernelOf s0).weights (kernelOf s0).stream (kernelOf s0).wptr (kernelOf s0).sptr k +
      (kernelOf s0).weights ((kernelOf s0).wptr + k) * (kernelOf s0).stream ((kernelOf s0).sptr + k))]s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ (kernelOf s0).acc + fsumFrom (kernelOf s0).weights (kernelOf s0).stream (kernelOf s0).wptr (kernelOf s0).sptr k +
    (kernelOf s0).weights k * (kernelOf s0).stream k =
  (kernelOf s0).acc +
    (fsumFrom (kernelOf s0).weights (kernelOf s0).stream (kernelOf s0).wptr (kernelOf s0).sptr k +
      (kernelOf s0).weights ((kernelOf s0).wptr + k) * (kernelOf s0).stream ((kernelOf s0).sptr + k))
        simp [kernelOf]s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)⊢ BitVec.toInt s0.acc +
      fsumFrom (fun i => BitVec.toInt (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + i))))
        (fun i => BitVec.toInt (s0.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + i)))) 0 0 k +
    BitVec.toInt (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k))) *
      BitVec.toInt (s0.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k))) =
  BitVec.toInt s0.acc +
    (fsumFrom (fun i => BitVec.toInt (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + i))))
        (fun i => BitVec.toInt (s0.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + i)))) 0 0 k +
      BitVec.toInt (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k))) *
        BitVec.toInt (s0.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k))))
        omegasucc.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)hsum:BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k = (krun (k + 1) (kernelOf s0)).acc⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)))
          (s0.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k))))) =
  (krun (k + 1) (kernelOf s0)).acc
      have hfits : signedFits defaultConfig.accBits
          (sk.acc.toInt + ((kernelOf s0).weights k) * ((kernelOf s0).stream k)) := bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) n⊢ ∀ (k : Nat),
  k ≤ n →
    ∃ sk,
      stepN (programOf imem) k s0 = some sk ∧
        sk.halted = false ∧
          sk.weights = s0.weights ∧
            sk.stream = s0.stream ∧
              BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
                BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                  BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                    BitVec.toInt sk.acc = (krun k (kernelOf s0)).acc
        rw [hsum,s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)hsum:BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k = (krun (k + 1) (kernelOf s0)).acc⊢ signedFits defaultConfig.accBits (krun (k + 1) (kernelOf s0)).acc krun_accs0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)hsum:BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k = (krun (k + 1) (kernelOf s0)).acc⊢ signedFits defaultConfig.accBits
  ((kernelOf s0).acc +
    fsumFrom (kernelOf s0).weights (kernelOf s0).stream (kernelOf s0).wptr (kernelOf s0).sptr (k + 1))]s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)hsum:BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k = (krun (k + 1) (kernelOf s0)).acc⊢ signedFits defaultConfig.accBits
  ((kernelOf s0).acc +
    fsumFrom (kernelOf s0).weights (kernelOf s0).stream (kernelOf s0).wptr (kernelOf s0).sptr (k + 1))
        exact hfit (k + 1) (bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)hsum:BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k = (krun (k + 1) (kernelOf s0)).acc⊢ k + 1 ≤ n omegaAll goals completed! 🐙)succ.refine_8s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)hsum:BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k = (krun (k + 1) (kernelOf s0)).acchfits:signedFits defaultConfig.accBits (BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k)⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        product (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)))
          (s0.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k))))) =
  (krun (k + 1) (kernelOf s0)).acc
      calc (accOfInt defaultConfig
              (sk.acc.toInt
                + (s0.weights (memIndexOfNat defaultConfig (s0.wptr.toNat + k))).toInt
                  * (s0.stream (memIndexOfNat defaultConfig (s0.sptr.toNat + k))).toInt)).toInt
          = sk.acc.toInt
              + ((kernelOf s0).weights k) * ((kernelOf s0).stream k) := bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)hsum:BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k = (krun (k + 1) (kernelOf s0)).acchfits:signedFits defaultConfig.accBits (BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k)⊢ BitVec.toInt
    (accOfInt defaultConfig
      (BitVec.toInt sk.acc +
        BitVec.toInt (s0.weights (memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k))) *
          BitVec.toInt (s0.stream (memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k))))) =
  BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k
            exact accOfInt_exact defaultConfig (bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nk:Natih:k ≤ n →
  ∃ sk,
    stepN (programOf imem) k s0 = some sk ∧
      sk.halted = false ∧
        sk.weights = s0.weights ∧
          sk.stream = s0.stream ∧
            BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536 ∧
              BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536 ∧
                BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616 ∧
                  BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchk:k + 1 ≤ nsk:State defaultConfighstep:stepN (programOf imem) k s0 = some skhh:sk.halted = falsehw:sk.weights = s0.weightshs:sk.stream = s0.streamhwp:BitVec.toNat sk.wptr = (BitVec.toNat s0.wptr + k) % 65536hsp:BitVec.toNat sk.sptr = (BitVec.toNat s0.sptr + k) % 65536hpc:BitVec.toNat sk.pc = (BitVec.toNat s0.pc + k) % 18446744073709551616hacc:BitVec.toInt sk.acc = (krun k (kernelOf s0)).acchone:step defaultConfig (programOf imem) sk = some (execDecoded (imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc))) sk)d:DecodedInstrhgen:imem (memIndexOfNat defaultConfig (BitVec.toNat sk.pc)) = dhd:d.op = CellOp.kmachidxw:memIndexOfNat defaultConfig (BitVec.toNat sk.wptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.wptr + k)hidxs:memIndexOfNat defaultConfig (BitVec.toNat sk.sptr) = memIndexOfNat defaultConfig (BitVec.toNat s0.sptr + k)hsum:BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k = (krun (k + 1) (kernelOf s0)).acchfits:signedFits defaultConfig.accBits (BitVec.toInt sk.acc + (kernelOf s0).weights k * (kernelOf s0).stream k)⊢ 0 < defaultConfig.accBits decideAll goals completed! 🐙) hfits
        _ = (krun (k + 1) (kernelOf s0)).acc := hsum

/-- **The machine computes the exact dot product.** A resident `kmac` loop, run
`n` ISA steps under the prefix-fit obligation, leaves in the fixed-width
accumulator exactly the kernel model's integer result — the hardware's wraps
never touch the value. Composed with `kernelDot_correct`, the machine's
accumulator *is* the mathematical dot product. -/
theorem kmac_loop_exact (s0 : State defaultConfig)
    (imem : Nat -> DecodedInstr) (n : Nat) (hhalt : s0.halted = false)
    (hprog : forall k, k < n ->
      (imem (memIndexOfNat defaultConfig (s0.pc.toNat + k))).op = .kmac)
    (hfit : kernelPrefixFits defaultConfig (kernelOf s0) n) :
    exists sn,
      stepN (programOf imem) n s0 = some sn
      /\ sn.acc.toInt = (krun n (kernelOf s0)).acc := bys0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) n⊢ ∃ sn, stepN (programOf imem) n s0 = some sn ∧ BitVec.toInt sn.acc = (krun n (kernelOf s0)).acc
  obtain ⟨sn, hstep, _, _, _, _, _, _, hacc⟩ :=
    kmac_loop_invariant s0 imem n hhalt hprog hfit n (Nat.le_refl n)s0:State defaultConfigimem:Nat → DecodedInstrn:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < n → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) nsn:State defaultConfighstep:stepN (programOf imem) n s0 = some snleft✝⁵:sn.halted = falseleft✝⁴:sn.weights = s0.weightsleft✝³:sn.stream = s0.streamleft✝²:BitVec.toNat sn.wptr = (BitVec.toNat s0.wptr + n) % 65536left✝¹:BitVec.toNat sn.sptr = (BitVec.toNat s0.sptr + n) % 65536left✝:BitVec.toNat sn.pc = (BitVec.toNat s0.pc + n) % 18446744073709551616hacc:BitVec.toInt sn.acc = (krun n (kernelOf s0)).acc⊢ ∃ sn, stepN (programOf imem) n s0 = some sn ∧ BitVec.toInt sn.acc = (krun n (kernelOf s0)).acc
  exact ⟨sn, hstep, hacc⟩All goals completed! 🐙

/-! ## The wide kernel fold (milestone 5): `W` MACs per cycle

The throughput path folds one block-FP region per cycle — `W` resident weights
against `W` streamed operands, summed and added to the accumulator in a single
step, both pointers advanced by `W`. This is the hardware image of the
shared-exponent block: `W = 8` against an 8-byte weight-port read. Widening the
datapath reopens the block-float MAC obligation, and the obligation is a
conservation law — one `W`-wide step computes exactly what `W` one-wide `kstep`s
compute. Once that holds, `wrun` is *definitionally* `krun` at a stride, so
`kernelDot_correct` and the `kernelPrefixFits` overflow bound transfer to the
8-wide tile with no new arithmetic reasoning. -/

/-- Fold `W` products in one step; advance both pointers by `W`. -/
def wstep (W : Nat) (s : KernelState) : KernelState :=
  { s with acc := s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W,
           wptr := s.wptr + W, sptr := s.sptr + W }

def wrun (W : Nat) : Nat -> KernelState -> KernelState
  | 0, s => s
  | m + 1, s => wrun W m (wstep W s)

/-- `krun` advances the pointers by the step count and never touches the
operand memories. -/
theorem krun_ptrs : forall (n : Nat) (s : KernelState),
    (krun n s).weights = s.weights
    ∧ (krun n s).stream = s.stream
    ∧ (krun n s).wptr = s.wptr + n
    ∧ (krun n s).sptr = s.sptr + n
  | 0, s =>s:KernelState⊢ (krun 0 s).weights = s.weights ∧
  (krun 0 s).stream = s.stream ∧ (krun 0 s).wptr = s.wptr + 0 ∧ (krun 0 s).sptr = s.sptr + 0 bys:KernelState⊢ (krun 0 s).weights = s.weights ∧
  (krun 0 s).stream = s.stream ∧ (krun 0 s).wptr = s.wptr + 0 ∧ (krun 0 s).sptr = s.sptr + 0 simp [krun]All goals completed! 🐙
  | n + 1, s =>n:Nats:KernelState⊢ (krun (n + 1) s).weights = s.weights ∧
  (krun (n + 1) s).stream = s.stream ∧
    (krun (n + 1) s).wptr = s.wptr + (n + 1) ∧ (krun (n + 1) s).sptr = s.sptr + (n + 1) byn:Nats:KernelState⊢ (krun (n + 1) s).weights = s.weights ∧
  (krun (n + 1) s).stream = s.stream ∧
    (krun (n + 1) s).wptr = s.wptr + (n + 1) ∧ (krun (n + 1) s).sptr = s.sptr + (n + 1)
      obtain ⟨hw, hs, hwp, hsp⟩ := krun_ptrs n (kstep s)n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (krun (n + 1) s).weights = s.weights ∧
  (krun (n + 1) s).stream = s.stream ∧
    (krun (n + 1) s).wptr = s.wptr + (n + 1) ∧ (krun (n + 1) s).sptr = s.sptr + (n + 1)
      rw [krunn:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (krun n (kstep s)).weights = s.weights ∧
  (krun n (kstep s)).stream = s.stream ∧
    (krun n (kstep s)).wptr = s.wptr + (n + 1) ∧ (krun n (kstep s)).sptr = s.sptr + (n + 1)]n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (krun n (kstep s)).weights = s.weights ∧
  (krun n (kstep s)).stream = s.stream ∧
    (krun n (kstep s)).wptr = s.wptr + (n + 1) ∧ (krun n (kstep s)).sptr = s.sptr + (n + 1)
      refine ⟨hw, hs, ?_, ?_⟩refine_1n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (krun n (kstep s)).wptr = s.wptr + (n + 1)refine_2n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (krun n (kstep s)).sptr = s.sptr + (n + 1)
      ·refine_1n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (krun n (kstep s)).wptr = s.wptr + (n + 1) rw [hwprefine_1n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (kstep s).wptr + n = s.wptr + (n + 1)]refine_1n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (kstep s).wptr + n = s.wptr + (n + 1); show s.wptr + 1 + n = s.wptr + (n + 1)refine_1n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ s.wptr + 1 + n = s.wptr + (n + 1); omegaAll goals completed! 🐙
      ·refine_2n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (krun n (kstep s)).sptr = s.sptr + (n + 1) rw [hsprefine_2n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (kstep s).sptr + n = s.sptr + (n + 1)]refine_2n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ (kstep s).sptr + n = s.sptr + (n + 1); show s.sptr + 1 + n = s.sptr + (n + 1)refine_2n:Nats:KernelStatehw:(krun n (kstep s)).weights = (kstep s).weightshs:(krun n (kstep s)).stream = (kstep s).streamhwp:(krun n (kstep s)).wptr = (kstep s).wptr + nhsp:(krun n (kstep s)).sptr = (kstep s).sptr + n⊢ s.sptr + 1 + n = s.sptr + (n + 1); omegaAll goals completed! 🐙

/-- Iterating `kstep` is additive in the step count. -/
theorem krun_add : forall (a b : Nat) (s : KernelState),
    krun (a + b) s = krun b (krun a s)
  | 0, b, s =>b:Nats:KernelState⊢ krun (0 + b) s = krun b (krun 0 s) byb:Nats:KernelState⊢ krun (0 + b) s = krun b (krun 0 s) simp [krun]All goals completed! 🐙
  | a + 1, b, s =>a:Natb:Nats:KernelState⊢ krun (a + 1 + b) s = krun b (krun (a + 1) s) bya:Natb:Nats:KernelState⊢ krun (a + 1 + b) s = krun b (krun (a + 1) s)
      have h : a + 1 + b = (a + b) + 1 := by omegaa:Natb:Nats:KernelStateh:a + 1 + b = a + b + 1⊢ krun (a + 1 + b) s = krun b (krun (a + 1) s)
      rw [ha:Natb:Nats:KernelStateh:a + 1 + b = a + b + 1⊢ krun (a + b + 1) s = krun b (krun (a + 1) s)]a:Natb:Nats:KernelStateh:a + 1 + b = a + b + 1⊢ krun (a + b + 1) s = krun b (krun (a + 1) s)
      show krun (a + b) (kstep s) = krun b (krun a (kstep s))a:Natb:Nats:KernelStateh:a + 1 + b = a + b + 1⊢ krun (a + b) (kstep s) = krun b (krun a (kstep s))
      exact krun_add a b (kstep s)All goals completed! 🐙

/-- **The conservation law.** One `W`-wide step equals `W` one-wide steps. -/
theorem wstep_eq_krun (W : Nat) (s : KernelState) : wstep W s = krun W s := byW:Nats:KernelState⊢ wstep W s = krun W s
  obtain ⟨hw, hs, hwp, hsp⟩ := krun_ptrs W sW:Nats:KernelStatehw:(krun W s).weights = s.weightshs:(krun W s).stream = s.streamhwp:(krun W s).wptr = s.wptr + Whsp:(krun W s).sptr = s.sptr + W⊢ wstep W s = krun W s
  have hacc := krun_acc W sW:Nats:KernelStatehw:(krun W s).weights = s.weightshs:(krun W s).stream = s.streamhwp:(krun W s).wptr = s.wptr + Whsp:(krun W s).sptr = s.sptr + Whacc:(krun W s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W⊢ wstep W s = krun W s
  show KernelState.mk (s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W)
        s.weights s.stream (s.wptr + W) (s.sptr + W) = krun W sW:Nats:KernelStatehw:(krun W s).weights = s.weightshs:(krun W s).stream = s.streamhwp:(krun W s).wptr = s.wptr + Whsp:(krun W s).sptr = s.sptr + Whacc:(krun W s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W⊢ { acc := s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W, weights := s.weights, stream := s.stream,
    wptr := s.wptr + W, sptr := s.sptr + W } =
  krun W s
  rw [← hacc,W:Nats:KernelStatehw:(krun W s).weights = s.weightshs:(krun W s).stream = s.streamhwp:(krun W s).wptr = s.wptr + Whsp:(krun W s).sptr = s.sptr + Whacc:(krun W s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W⊢ { acc := (krun W s).acc, weights := s.weights, stream := s.stream, wptr := s.wptr + W, sptr := s.sptr + W } = krun W s ← hw,W:Nats:KernelStatehw:(krun W s).weights = s.weightshs:(krun W s).stream = s.streamhwp:(krun W s).wptr = s.wptr + Whsp:(krun W s).sptr = s.sptr + Whacc:(krun W s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W⊢ { acc := (krun W s).acc, weights := (krun W s).weights, stream := s.stream, wptr := s.wptr + W, sptr := s.sptr + W } =
  krun W s ← hs,W:Nats:KernelStatehw:(krun W s).weights = s.weightshs:(krun W s).stream = s.streamhwp:(krun W s).wptr = s.wptr + Whsp:(krun W s).sptr = s.sptr + Whacc:(krun W s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W⊢ { acc := (krun W s).acc, weights := (krun W s).weights, stream := (krun W s).stream, wptr := s.wptr + W,
    sptr := s.sptr + W } =
  krun W s ← hwp,W:Nats:KernelStatehw:(krun W s).weights = s.weightshs:(krun W s).stream = s.streamhwp:(krun W s).wptr = s.wptr + Whsp:(krun W s).sptr = s.sptr + Whacc:(krun W s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W⊢ { acc := (krun W s).acc, weights := (krun W s).weights, stream := (krun W s).stream, wptr := (krun W s).wptr,
    sptr := s.sptr + W } =
  krun W s ← hspW:Nats:KernelStatehw:(krun W s).weights = s.weightshs:(krun W s).stream = s.streamhwp:(krun W s).wptr = s.wptr + Whsp:(krun W s).sptr = s.sptr + Whacc:(krun W s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr W⊢ { acc := (krun W s).acc, weights := (krun W s).weights, stream := (krun W s).stream, wptr := (krun W s).wptr,
    sptr := (krun W s).sptr } =
  krun W s]All goals completed! 🐙

/-- The `W`-wide fold over `m` steps is the one-wide fold over `W * m` steps —
so it inherits every `krun` theorem. -/
theorem wrun_eq_krun (W : Nat) : forall (m : Nat) (s : KernelState),
    wrun W m s = krun (W * m) s
  | 0, s =>W:Nats:KernelState⊢ wrun W 0 s = krun (W * 0) s byW:Nats:KernelState⊢ wrun W 0 s = krun (W * 0) s simp [wrun, krun]All goals completed! 🐙
  | m + 1, s =>W:Natm:Nats:KernelState⊢ wrun W (m + 1) s = krun (W * (m + 1)) s byW:Natm:Nats:KernelState⊢ wrun W (m + 1) s = krun (W * (m + 1)) s
      have h : W + W * m = W * (m + 1) := by rw [Nat.mul_succW:Natm:Nats:KernelState⊢ W + W * m = W * m + W]W:Natm:Nats:KernelState⊢ W + W * m = W * m + W; omegaW:Natm:Nats:KernelStateh:W + W * m = W * (m + 1)⊢ wrun W (m + 1) s = krun (W * (m + 1)) s
      rw [wrun,W:Natm:Nats:KernelStateh:W + W * m = W * (m + 1)⊢ wrun W m (wstep W s) = krun (W * (m + 1)) s wrun_eq_krun W m (wstep W s),W:Natm:Nats:KernelStateh:W + W * m = W * (m + 1)⊢ krun (W * m) (wstep W s) = krun (W * (m + 1)) s wstep_eq_krun,W:Natm:Nats:KernelStateh:W + W * m = W * (m + 1)⊢ krun (W * m) (krun W s) = krun (W * (m + 1)) s ← krun_add,W:Natm:Nats:KernelStateh:W + W * m = W * (m + 1)⊢ krun (W + W * m) s = krun (W * (m + 1)) s hW:Natm:Nats:KernelStateh:W + W * m = W * (m + 1)⊢ krun (W * (m + 1)) s = krun (W * (m + 1)) s]All goals completed! 🐙

/-- The 8-wide tile computes the exact dot product: `m` wide steps from a
cleared accumulator leave `dotSpec w a (8 * m)`, the same result the one-wide
loop computes, by conservation. -/
theorem wideKernel_dot_correct (w a : Nat -> Int) (m : Nat) :
    (wrun 8 m (KernelState.mk 0 w a 0 0)).acc = dotSpec w a (8 * m) := byw:Nat → Inta:Nat → Intm:Nat⊢ (wrun 8 m { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }).acc = dotSpec w a (8 * m)
  rw [wrun_eq_krun,w:Nat → Inta:Nat → Intm:Nat⊢ (krun (8 * m) { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }).acc = dotSpec w a (8 * m) krun_accw:Nat → Inta:Nat → Intm:Nat⊢ { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.acc +
    fsumFrom { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.weights
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.stream
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.wptr
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.sptr (8 * m) =
  dotSpec w a (8 * m)]w:Nat → Inta:Nat → Intm:Nat⊢ { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.acc +
    fsumFrom { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.weights
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.stream
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.wptr
      { acc := 0, weights := w, stream := a, wptr := 0, sptr := 0 }.sptr (8 * m) =
  dotSpec w a (8 * m)
  simp [dotSpec]All goals completed! 🐙

/-- The 8-wide fold never overflows when the one-wide prefix-fit holds: every
wide-step boundary accumulator is a one-wide prefix (at a multiple of 8), so
`kernelPrefixFits` up to `8 * m` already guards them. The widening reuses the
overflow proof verbatim — no new fit obligation is introduced by folding 8 at
a time. -/
theorem wideKernel_stepsFit (cfg : Config) (s : KernelState) (m : Nat)
    (hfit : kernelPrefixFits cfg s (8 * m)) :
    forall j, j ≤ m → signedFits cfg.accBits (wrun 8 j s).acc := bycfg:Configs:KernelStatem:Nathfit:kernelPrefixFits cfg s (8 * m)⊢ ∀ (j : Nat), j ≤ m → signedFits cfg.accBits (wrun 8 j s).acc
  intro j hjcfg:Configs:KernelStatem:Nathfit:kernelPrefixFits cfg s (8 * m)j:Nathj:j ≤ m⊢ signedFits cfg.accBits (wrun 8 j s).acc
  have hacc : (wrun 8 j s).acc
      = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j) := bycfg:Configs:KernelStatem:Nathfit:kernelPrefixFits cfg s (8 * m)⊢ ∀ (j : Nat), j ≤ m → signedFits cfg.accBits (wrun 8 j s).acc
    rw [wrun_eq_krun,cfg:Configs:KernelStatem:Nathfit:kernelPrefixFits cfg s (8 * m)j:Nathj:j ≤ m⊢ (krun (8 * j) s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j) krun_acccfg:Configs:KernelStatem:Nathfit:kernelPrefixFits cfg s (8 * m)j:Nathj:j ≤ m⊢ s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j) = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j)]cfg:Configs:KernelStatem:Nathfit:kernelPrefixFits cfg s (8 * m)j:Nathj:j ≤ mhacc:(wrun 8 j s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j)⊢ signedFits cfg.accBits (wrun 8 j s).acc
  rw [hacccfg:Configs:KernelStatem:Nathfit:kernelPrefixFits cfg s (8 * m)j:Nathj:j ≤ mhacc:(wrun 8 j s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j)⊢ signedFits cfg.accBits (s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j))]cfg:Configs:KernelStatem:Nathfit:kernelPrefixFits cfg s (8 * m)j:Nathj:j ≤ mhacc:(wrun 8 j s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j)⊢ signedFits cfg.accBits (s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j))
  exact hfit (8 * j) (bycfg:Configs:KernelStatem:Nathfit:kernelPrefixFits cfg s (8 * m)j:Nathj:j ≤ mhacc:(wrun 8 j s).acc = s.acc + fsumFrom s.weights s.stream s.wptr s.sptr (8 * j)⊢ 8 * j ≤ 8 * m omegaAll goals completed! 🐙)

/-- **The fixed-width machine realizes the wide fold.** A resident `kmac` loop
of `8 * m` steps leaves in the accumulator exactly `wrun 8 m (kernelOf s0)` —
so the 8-wide datapath computes the same architectural result as the
equivalent single-MAC sequence, by conservation (`wrun_eq_krun`) composed with
`kmac_loop_exact`. The wide *opcode/datapath* is a microarchitectural
refinement that folds 8 per issue; this theorem pins the exact value it must
produce, before any RTL exists. -/
theorem wide_loop_exact (s0 : State defaultConfig)
    (imem : Nat -> DecodedInstr) (m : Nat) (hhalt : s0.halted = false)
    (hprog : forall k, k < 8 * m ->
      (imem (memIndexOfNat defaultConfig (s0.pc.toNat + k))).op = .kmac)
    (hfit : kernelPrefixFits defaultConfig (kernelOf s0) (8 * m)) :
    exists sn,
      stepN (programOf imem) (8 * m) s0 = some sn
      /\ sn.acc.toInt = (wrun 8 m (kernelOf s0)).acc := bys0:State defaultConfigimem:Nat → DecodedInstrm:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < 8 * m → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) (8 * m)⊢ ∃ sn, stepN (programOf imem) (8 * m) s0 = some sn ∧ BitVec.toInt sn.acc = (wrun 8 m (kernelOf s0)).acc
  obtain ⟨sn, hstep, hacc⟩ := kmac_loop_exact s0 imem (8 * m) hhalt hprog hfits0:State defaultConfigimem:Nat → DecodedInstrm:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < 8 * m → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) (8 * m)sn:State defaultConfighstep:stepN (programOf imem) (8 * m) s0 = some snhacc:BitVec.toInt sn.acc = (krun (8 * m) (kernelOf s0)).acc⊢ ∃ sn, stepN (programOf imem) (8 * m) s0 = some sn ∧ BitVec.toInt sn.acc = (wrun 8 m (kernelOf s0)).acc
  exact ⟨sn, hstep, bys0:State defaultConfigimem:Nat → DecodedInstrm:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < 8 * m → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) (8 * m)sn:State defaultConfighstep:stepN (programOf imem) (8 * m) s0 = some snhacc:BitVec.toInt sn.acc = (krun (8 * m) (kernelOf s0)).acc⊢ BitVec.toInt sn.acc = (wrun 8 m (kernelOf s0)).acc rw [hacc,s0:State defaultConfigimem:Nat → DecodedInstrm:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < 8 * m → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) (8 * m)sn:State defaultConfighstep:stepN (programOf imem) (8 * m) s0 = some snhacc:BitVec.toInt sn.acc = (krun (8 * m) (kernelOf s0)).acc⊢ (krun (8 * m) (kernelOf s0)).acc = (wrun 8 m (kernelOf s0)).acc wrun_eq_kruns0:State defaultConfigimem:Nat → DecodedInstrm:Nathhalt:s0.halted = falsehprog:∀ (k : Nat), k < 8 * m → (imem (memIndexOfNat defaultConfig (BitVec.toNat s0.pc + k))).op = CellOp.kmachfit:kernelPrefixFits defaultConfig (kernelOf s0) (8 * m)sn:State defaultConfighstep:stepN (programOf imem) (8 * m) s0 = some snhacc:BitVec.toInt sn.acc = (krun (8 * m) (kernelOf s0)).acc⊢ (krun (8 * m) (kernelOf s0)).acc = (krun (8 * m) (kernelOf s0)).acc]All goals completed! 🐙⟩

end Honeycomb