@[reducible, inline]

abbrev Sparkle.Backend.CSim.TypeMap : Type

Name→type lookup used by the emitters. Backed by a Std.HashMap so lookupWidth is O(1): emitExpr/inferExprWidth probe it once per expression node. The old linear-scan List made emit O(N·M) over a module's N nodes and M wires — quadratic on large designs like Keccak's ~1600-wire round.

Equations

• Sparkle.Backend.CSim.TypeMap = Std.HashMap String Sparkle.IR.Type.HWType

def Sparkle.Backend.CSim.buildTypeMap (m : IR.AST.Module) : TypeMap

Build a name-to-type map from a module's ports and wires. insertIfNew preserves the first binding on a name clash, matching the old List.find? (inputs, then outputs, then wires) semantics.

Equations

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

def Sparkle.Backend.CSim.lookupWidth (typeMap : TypeMap) (name : String) : Nat

Look up bit-width for a name in the type map

Equations

• Sparkle.Backend.CSim.lookupWidth typeMap name = match Std.HashMap.get? typeMap name with | some ty => ty.bitWidth | none => 32

def Sparkle.Backend.CSim.sanitizeName (name : String) : String

Sanitize a name to be a valid C identifier

Equations

• Sparkle.Backend.CSim.sanitizeName name = ((((name.replace "." "_").replace "-" "_").replace " " "_").replace "'" "_prime").replace "#" ""

def Sparkle.Backend.CSim.emitScalarBase : IR.Type.HWType → String

Convert HWType to a C scalar type string. For wide integers (> 64 bits) and arrays we return a base scalar type; the surrounding declaration adds the array dimensions (see emitFieldDecl).

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.Backend.CSim.emitScalarBase Sparkle.IR.Type.HWType.bit = "uint8_t"
• Sparkle.Backend.CSim.emitScalarBase (Sparkle.IR.Type.HWType.array size elemType) = Sparkle.Backend.CSim.emitScalarBase elemType
• Sparkle.Backend.CSim.emitScalarBase (Sparkle.IR.Type.HWType.bitVectorDim width) = "SPARKLE_UNSUPPORTED_SYMBOLIC_WIDTH"

partial def Sparkle.Backend.CSim.emitArraySuffix : IR.Type.HWType → String

Total array length suffix for a HWType, e.g. [3] for a 96-bit wide type, [8][3] for array 8 (bitVector 96), or empty for a single ≤ 64-bit scalar.

def Sparkle.Backend.CSim.emitFieldDecl (ty : IR.Type.HWType) (name : String) : String

Emit a C field/local declaration like uint32_t foo[3] — the type goes on the left, the array dimensions on the right of the name (C array syntax).

Equations

• Sparkle.Backend.CSim.emitFieldDecl ty name = toString (Sparkle.Backend.CSim.emitScalarBase ty) ++ toString " " ++ toString name ++ toString (Sparkle.Backend.CSim.emitArraySuffix ty)

def Sparkle.Backend.CSim.emitTypeName (ty : IR.Type.HWType) : String

For situations where a parameter or declaration needs just the type and dimensions but no identifier, used by casts.

Equations

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

def Sparkle.Backend.CSim.needsMask (w : Nat) : Bool

True for widths that are not native C integer widths.

Equations

• Sparkle.Backend.CSim.needsMask w = (w != 8 && w != 16 && w != 32 && w != 64)

def Sparkle.Backend.CSim.emitMask (w : Nat) : String

Emit a bit mask expression for the given width

Equations

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

def Sparkle.Backend.CSim.applyMask (expr : String) (w : Nat) : String

Wrap an expression with a mask if the width requires it

Equations

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

partial def Sparkle.Backend.CSim.exprIsMasked (w : Nat) : IR.AST.Expr → Bool

Check if an IR expression produces a result that is already correctly masked. Invariant: every assignment applies a mask, so .ref reads yield masked values.

def Sparkle.Backend.CSim.emitCOperator (op : IR.AST.Operator) : String

Convert Operator to C operator symbol

Equations

• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.and = "&"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.or = "|"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.xor = "^"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.not = "~"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.add = "+"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.sub = "-"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.mul = "*"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.eq = "=="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.lt_u = "<"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.lt_s = "<"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.le_u = "<="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.le_s = "<="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.gt_u = ">"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.gt_s = ">"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.ge_u = ">="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.ge_s = ">="
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.shl = "<<"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.shr = ">>"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.asr = ">>"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.neg = "-"
• Sparkle.Backend.CSim.emitCOperator Sparkle.IR.AST.Operator.mux = "?"

def Sparkle.Backend.CSim.signedCastType (w : Nat) : String

Get signed cast type for a given width

Equations

• Sparkle.Backend.CSim.signedCastType w = if w ≤ 8 then "int8_t" else if w ≤ 16 then "int16_t" else if w ≤ 32 then "int32_t" else "int64_t"

partial def Sparkle.Backend.CSim.inferExprWidth (typeMap : TypeMap) : IR.AST.Expr → Nat

Best-effort width inference for an expression

partial def Sparkle.Backend.CSim.emitExpr (typeMap : TypeMap) (e : IR.AST.Expr) : String

Convert IR expression to C expression.

Wide (> 64 bit) values are represented as uint32_t[N] arrays in declarations. In expression contexts an "rvalue array" doesn't really exist in C, so the only ways we produce wide expressions are:

• .ref to a wide variable — emits the bare identifier, which C decays to a pointer in most contexts; the wide-assign code below indexes it slot-by-slot rather than copying.
• .const with width > 64 — emits a C99 compound literal (uint32_t[N]){w0, w1, …}, which is a valid rvalue only at statement scope.
• .concat over wide totals — same compound-literal shape.

All wide assignments (see emitStmt) must therefore either: (a) be element-wise slot writes (lhs[j] = …), or (b) wrap the RHS in memcpy(lhs, RHS, sizeof(lhs)) when RHS is a compound literal — lhs = RHS on a C array is rejected by the compiler.

structure Sparkle.Backend.CSim.StmtParts : Type

Parts of a C struct + helper-set generated from a single statement

• declarations : List String
• evalBody : List String
• tickBody : List String
• resetBody : List String
• evalTickLocals : List String

@[implicit_reducible]

instance Sparkle.Backend.CSim.instInhabitedStmtParts : Inhabited StmtParts

Equations

• Sparkle.Backend.CSim.instInhabitedStmtParts = { default := Sparkle.Backend.CSim.instInhabitedStmtParts.default }

@[implicit_reducible]

instance Sparkle.Backend.CSim.instAppendStmtParts : Append StmtParts

Equations

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

def Sparkle.Backend.CSim.StmtParts.empty : StmtParts

Equations

• Sparkle.Backend.CSim.StmtParts.empty = { declarations := [], evalBody := [], tickBody := [], resetBody := [], evalTickLocals := [] }

def Sparkle.Backend.CSim.emitInitScalar (initValue : Int) (width : Nat) : String

Emit a C reset value for a register init.

For ≤ 64-bit widths returns a scalar cast.

For wide (> 64-bit) widths returns a list of slot assignments like lhs[0] = 0x…u; lhs[1] = 0x…u; since C does not let you assign a compound literal to an array-typed lvalue. The caller (register reset path) threads these through resetBody.

Equations

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

def Sparkle.Backend.CSim.emitInitWideLines (name : String) (initValue : Int) (width : Nat) : List String

Per-slot reset lines for a wide register name.

Equations

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

def Sparkle.Backend.CSim.emitMuxAsIfElse (typeMap : TypeMap) (lhsName : String) (width : Nat) (rhs : IR.AST.Expr) (minArms : Nat := 4) : List String

Emit a MUX chain as if-else block for better branch prediction.

Equations

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

partial def Sparkle.Backend.CSim.emitStmt (stmt : IR.AST.Stmt) (typeMap : TypeMap) (design : Option IR.AST.Design := none) : StmtParts

Split a statement into declaration/eval/tick/reset parts

partial def Sparkle.Backend.CSim.emitStmt.matWide (typeMap : TypeMap) (sn : String) (nWords : Nat) (constAmt : IR.AST.Expr → Nat) (shlSlot : String → Nat → Nat → String) (shrSlot : String → Nat → Nat → Nat → String) (label : String) (e : IR.AST.Expr) : List String × String

partial def Sparkle.Backend.CSim.collectExprRefs : IR.AST.Expr → List String

Collect all wire name references from an IR expression

def Sparkle.Backend.CSim.collectTickRefWires (body : List IR.AST.Stmt) : List String

Collect all wire names referenced in tick() bodies.

Equations

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

partial def Sparkle.Backend.CSim.exprHasSymbolicWidth : IR.AST.Expr → Bool

Parameterized IR is intentionally Verilog-only in P1. Reject it at CSim module boundaries before concrete-width helpers can observe it.

def Sparkle.Backend.CSim.moduleHasSymbolicWidth (m : IR.AST.Module) : Bool

Equations

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

def Sparkle.Backend.CSim.unsupportedSymbolicWidthError : String

Equations

• Sparkle.Backend.CSim.unsupportedSymbolicWidthError = "#error \"Sparkle CSim does not support native symbolic-width modules; use the Verilog backend\"\n"

def Sparkle.Backend.CSim.emitModule (m : IR.AST.Module) (design : Option IR.AST.Design := none) (observableWires : Option (List String) := none) (funcQual : String := "") : String

Emit a complete C struct + static helpers for a module. Returns the full C source fragment (no includes; callers add those at design level).

Equations

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

def Sparkle.Backend.CSim.toCDesign (d : IR.AST.Design) (observableWires : Option (List String) := none) (funcQual : String := "") : String

Convert a full design to C simulation code (no JIT wrapper)

Equations

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

def Sparkle.Backend.CSim.toC (m : IR.AST.Module) : String

Convert a single module to C simulation code with includes

Equations

• Sparkle.Backend.CSim.toC m = "#include <stdint.h>\n" ++ "#include <stdlib.h>\n" ++ "#include <string.h>\n\n" ++ Sparkle.Backend.CSim.emitModule m

JIT FFI wrapper

Each .so exports exactly ONE symbol — jit_vtable — which returns a pointer to a JitVTable containing function pointers for every operation. Everything else is static, so dlsym cannot reach it. This sidesteps the collision-on- shared-symbol problem from Issue #70: two .so files with the same internal jit_eval cannot conflict because neither publishes that name.

def Sparkle.Backend.CSim.toCJIT (d : IR.AST.Design) (observableWires : Option (List String) := none) : String

Equations

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