structure Sparkle.Core.Oracle.SelfLoopConfig : Type

Configuration for the self-loop detector

• threshold : Nat

  Cycles of near-same PC before triggering (>34 for divider safety)

• skipAmount : Nat

  Cycles to skip per trigger

• pcWireArrayIdx : Nat

  Index of PC wire in the wireValues array passed to the oracle

• pcTolerance : UInt64

  Max byte distance from anchor PC to consider "same location". 12 covers loops up to 4 instructions. Sequential execution resets every 4 instructions (16 bytes > 12), preventing false triggers.

• mtimeLoRegIdx : UInt32

  Register index for CLINT mtimeLo (SoCState field 46, offset by 8 divider regs = 54)

• mtimeHiRegIdx : UInt32

  Register index for CLINT mtimeHi (SoCState field 47, offset by 8 divider regs = 55)

• mtimecmpLoRegIdx : UInt32

  Register index for CLINT mtimecmpLo (SoCState field 48 + 8 divider regs = 56)

• mtimecmpHiRegIdx : UInt32

  Register index for CLINT mtimecmpHi (SoCState field 49 + 8 divider regs = 57)

• skipToTimerCompare : Bool

  When true, skip to mtimecmp instead of fixed skipAmount, and reset sameCount after each trigger so timer interrupt can fire

• maxSkip : Nat

  Maximum cycles to skip per trigger (caps skipToTimerCompare distance)

• checkInterruptEnable : Bool

  Guard: check MIE (global interrupt enable) and MTIE (timer interrupt enable) before performing timer-compare skip. Prevents skipping when interrupts are disabled (the timer interrupt wouldn't fire anyway).

• mstatusRegIdx : UInt32

  Register index for MSTATUS CSR (contains MIE at bit 3)

• mieRegIdx : UInt32

  Register index for MIE CSR (contains MTIE at bit 7)

• wfiWireArrayIdx : Option Nat

  WFI fast-path: when set, the oracle checks if the instruction at this wire index is WFI (0x10500073) and triggers immediately (threshold=1).

structure Sparkle.Core.Oracle.SelfLoopState : Type

Mutable state for the self-loop detector

• anchorPC : UInt64

  Anchor PC — the PC at the start of a suspected self-loop

• sameCount : Nat

  Count of consecutive cycles with PC near the anchor

• totalSkipped : Nat
• triggerCount : Nat

def Sparkle.Core.Oracle.mkSelfLoopOracle (config : SelfLoopConfig) : IO ((JIT.JITHandle → Nat → Array UInt64 → IO (Option Nat)) × IO.Ref SelfLoopState)

Create a self-loop detection oracle. Returns the oracle function (for JIT.runOptimized) and an IORef to the internal state (for post-run statistics).

The oracle monitors the PC wire. When PC stays within pcTolerance bytes of an anchor PC for config.threshold consecutive cycles, it skips forward by config.skipAmount cycles, advancing the CLINT timer to match. The oracle receives the JITHandle per-call and handles all state mutations (setReg) internally.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Core.Oracle.mkBootOracle (config : SelfLoopConfig := { }) : IO ((JIT.JITHandle → Nat → Array UInt64 → IO (Option Nat)) × IO.Ref SelfLoopState)

Create a boot-optimized oracle for Linux boot idle-loop skipping. Uses timer-compare-aware skipping with wider PC tolerance (32 bytes). Enables MIE/MTIE guard to avoid skipping when interrupts are disabled. Resets sameCount after each trigger so the timer interrupt can fire.

Equations

• One or more equations did not get rendered due to their size.