structure Sparkle.Core.OracleSpec.RegRole : Type

A register role in an oracle specification.

• role : String

  Logical name (e.g., "rs1")

• namePattern : String

  Glob pattern to match IR register names. "*" = prefix wildcard.

• isOutput : Bool

  True if this register is written by the oracle (output).

def Sparkle.Core.OracleSpec.instReprRegRole.repr : RegRole → Nat → Std.Format

Equations

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

instance Sparkle.Core.OracleSpec.instReprRegRole : Repr RegRole

Equations

• Sparkle.Core.OracleSpec.instReprRegRole = { reprPrec := Sparkle.Core.OracleSpec.instReprRegRole.repr }

def Sparkle.Core.OracleSpec.instInhabitedRegRole.default : RegRole

Equations

• Sparkle.Core.OracleSpec.instInhabitedRegRole.default = { role := default, namePattern := default, isOutput := default }

instance Sparkle.Core.OracleSpec.instInhabitedRegRole : Inhabited RegRole

Equations

• Sparkle.Core.OracleSpec.instInhabitedRegRole = { default := Sparkle.Core.OracleSpec.instInhabitedRegRole.default }

def Sparkle.Core.OracleSpec.iterateN {α : Sort u_1} (f : α → α) : Nat → α → α

Iterate a function n times.

Equations

• Sparkle.Core.OracleSpec.iterateN f 0 x✝ = x✝
• Sparkle.Core.OracleSpec.iterateN f n.succ x✝ = Sparkle.Core.OracleSpec.iterateN f n (f x✝)

class Sparkle.Core.OracleSpec.OracleReduction (tag : String) (State Input Output : Type) : Type

Type class for oracle-driven FSM reductions with mandatory proof.

Type parameters:

• tag: string literal identifying this reduction (e.g., "pcpi_mul")
• State: internal FSM state type (e.g., rd × rdx × rs1 × rs2)
• Input: input type extracted from registers (e.g., rs1 × rs2)
• Output: result type to inject back (e.g., product)

The equiv field requires a proof that iterating step for numCycles from initState input and extracting the result equals compute input. Without this proof, the instance cannot be constructed.

• step : State → State

  One cycle of the FSM (pure Lean function modeling the hardware)

• initState : Input → State

  Map input register values to the FSM's initial state

• extractResult : State → Output

  Extract the final result from the FSM state

• compute : Input → Output

  Direct computation (what the oracle actually executes)

• numCycles : Nat

  Number of cycles the FSM takes

• equiv (input : Input) : extractResult tag Input (iterateN (step tag Input Output) (numCycles tag State Input Output) (initState tag Output input)) = compute tag State input

  MANDATORY PROOF: iterating step = direct compute. This is the soundness guarantee. Without it, the instance cannot be constructed (unless sorry is used, which is explicit).

• registers : List RegRole

  Register roles for pattern matching

• encodeInputs : Array UInt64 → Input

  Encode JIT register values → typed Input

• decodeResult : Output → List (String × UInt64)

  Decode typed Output → (role, value) pairs to write back

• trigger : Array UInt64 → Bool

  Trigger condition on raw register values

• deadWirePatterns : List String

  Wire patterns to eliminate from IR (optional)

structure Sparkle.Core.OracleSpec.ResolvedOracle : Type

Resolved oracle: type class instance with register indices bound.

• tag : String
• regIndices : Array UInt32
• roleToIdx : List (String × Nat)

structure Sparkle.Core.OracleSpec.OracleState : Type

Mutable state for a running oracle.

• totalSkipped : Nat
• triggerCount : Nat

def Sparkle.Core.OracleSpec.matchPattern (pattern name : String) : Bool

Match a name against a glob pattern. Splits pattern on * and checks that all segments appear in order. Examples: *pcpi_mul*_seq* matches _gen_picorv32_pcpi_mul_next_rd_seq42.

Equations

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

def Sparkle.Core.OracleSpec.resolve (tag : String) {State Input Output : Type} [inst : OracleReduction tag State Input Output] (handle : JIT.JITHandle) : IO (Option ResolvedOracle)

Resolve an OracleReduction instance against a JITHandle.

Equations

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

def Sparkle.Core.OracleSpec.mkOracle (tag : String) {State Input Output : Type} [inst : OracleReduction tag State Input Output] (resolved : ResolvedOracle) : IO ((JIT.JITHandle → Nat → Array UInt64 → IO (Option Nat)) × IO.Ref OracleState)

Create a runtime oracle from a resolved OracleReduction.

Equations

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

def Sparkle.Core.OracleSpec.mkOracleAuto (tag : String) (State Input Output : Type) [OracleReduction tag State Input Output] (handle : JIT.JITHandle) : IO (Option ((JIT.JITHandle → Nat → Array UInt64 → IO (Option Nat)) × IO.Ref OracleState))

One-shot: resolve + create oracle.

Equations

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

def Sparkle.Core.OracleSpec.composeOracles (oracles : List (JIT.JITHandle → Nat → Array UInt64 → IO (Option Nat))) : JIT.JITHandle → Nat → Array UInt64 → IO (Option Nat)

Compose multiple oracle callbacks: first match wins.

Equations

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

def Sparkle.Core.OracleSpec.reduceIR (tag : String) (State Input Output : Type) [inst : OracleReduction tag State Input Output] (body : List IR.AST.Stmt) : List IR.AST.Stmt

IR reduction: remove dead wires and stub output registers.

Equations

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