Tasks / aes_sbox

AES S-box `aes_sbox`

The byte substitution of AES (FIPS 197): 8 bits in, 8 bits out.

open for submissions fixed size scored at the one fixed size

Par: 3833µm²·nssbox_bp · 892.1 µm² × 4.30 ns
Record: 2858µm²·nstower-shuffle · 890.9 µm² × 3.21 ns
Under par: −25%

Par: 9.402µm²·nssbox_bp · 13.355 µm² × 0.704 ns
Record: 7.458µm²·nstower-shuffle · 13.414 µm² × 0.556 ns
Under par: −21%

Score

ASAP7 · area × time · µm²·ns · lower is better

sbox_table 7884 not proved
sbox_bp_d16 3494 not proved

submission
proved reference
the best score so far
par
a baseline's score (not proved)

Score = area × time: the sky130 cell area of the scored netlist in µm² times the critical-path delay in ns, from the pinned flow, so µm²·ns. Lower is better. It is the one ranked number: Par (the best proved reference's score, the bar to beat), Record (the best accepted score so far, par while no submission beats it), Under par (how far the record is below par, as a share of par's score) and the leaderboard use it. The Pareto front, area in GE (NAND2 gate equivalents), depth and the other numbers are for exploring, under compare the designs; reproduce a score says how to get the same numbers. Rated with Yosys 0.53 (git 53c22ab7, the Homebrew build for macOS arm64, clang++ 17, -O3) and its yosys-abc (ABC 1.01 of 6 May 2025): the flow is deterministic on that build (measured on 52 designs). Another build of the same version can break ABC's ties differently (measured: 3 fdivp designs, up to 2.9% in delay), so a number made on another platform may differ slightly: the build and its hashes. Dots are the entries by date; the proved references are the first entries, dated by when they joined the task. The dotted levels are baselines: scored, never proved.

every entry by date

date	design	kind	score (µm²·ns)	area × time
2026-10-30	sbox_bp	proved reference · par	3833	892.1 µm² × 4.30 ns
2026-10-31	sbox_table	proved reference	7884	3445.8 µm² × 2.29 ns
2026-11-05	tower-shuffle	submission	2858	890.9 µm² × 3.21 ns
–	sbox_bp_d16	baseline, not proved	3494	952.2 µm² × 3.67 ns
–	sbox_table	baseline, not proved	7884	3445.8 µm² × 2.29 ns

sbox_table 19.33 not proved
sbox_bp_d16 8.931 not proved

submission
proved reference
the best score so far
par
a baseline's score (not proved)

Score = area × time: the ASAP7 cell area of the scored netlist in µm² times the critical-path delay in ns, from the pinned flow, so µm²·ns. Lower is better. In this view Par (the best proved reference's score, the bar to beat), Record (the best accepted score so far, par while no submission beats it), Under par (how far the record is below par, as a share of par's score) and the leaderboard use it; the records' ranked score is sky130's, the default view. The Pareto front, area in GE (NAND2 gate equivalents), depth and the other numbers are for exploring, under compare the designs; reproduce a score says how to get the same numbers. ASAP7 view. These numbers are on ASAP7 (asap7sc7p5t), a predictive 7 nm library made for research: it has never been fabricated, so no chip can confirm them. Like sky130's score they count no wires. sky130, a real 130 nm process, is the default view (how ASAP7 is scored, and its quirks). Rated with Yosys 0.53 (git 53c22ab7, the Homebrew build for macOS arm64, clang++ 17, -O3) and its yosys-abc (ABC 1.01 of 6 May 2025): the flow is deterministic on that build (measured on 52 designs). Another build of the same version can break ABC's ties differently (measured: 3 fdivp designs, up to 2.9% in delay), so a number made on another platform may differ slightly: the build and its hashes. Dots are the entries by date; the proved references are the first entries, dated by when they joined the task. The dotted levels are baselines: scored, never proved.

every entry by date

date	design	kind	score (µm²·ns)	area × time
2026-10-30	sbox_bp	proved reference · par	9.402	13.355 µm² × 0.704 ns
2026-10-31	sbox_table	proved reference	19.33	51.817 µm² × 0.373 ns
2026-11-05	tower-shuffle	submission	7.458	13.414 µm² × 0.556 ns
–	sbox_bp_d16	baseline, not proved	8.931	14.245 µm² × 0.627 ns
–	sbox_table	baseline, not proved	19.33	51.817 µm² × 0.373 ns

First submission: How to submit

This task

Proving guide

This text quotes sky130 numbers and compares the designs on sky130, the default library; the score, the boards and the charts of this page are on ASAP7, where the order of the designs can differ.

Compute the AES S-box (FIPS 197, Section 5.1.1): eight bits in, eight bits out, y = S(x). The statement defines S the way the standard does, algebraically (the multiplicative inverse in GF(2^8), then an affine map), so a lookup table and a gate network are judged against the same mathematics.

The task has one fixed size, bans no operator but the run-time / % ** every task bans, and its post-synthesis check covers all 256 inputs. The proved Boyar-Peralta 113-gate circuit has 892.1 µm² and a 4.30 ns critical path on sky130 (200.986 GE, depth 21), 3833 µm²·ns: par. The proved 256-entry table is almost four times larger and nearly twice as fast, 3445.8 µm² at 2.29 ns (786.894 GE, depth 11). The S-box is the most golfed Boolean function in cryptography, so the published circuits are strong comparison points.

Interface #

Write a module with exactly this header: port names, directions, widths and order matter, and so do the module's name and its parameters.

aes_sbox.sv

module aes_sbox (
  input  logic [7:0] x,
  output logic [7:0] y
);

port	direction	width (bits)
`x`	input	8
`y`	output	8

The trusted statement #

A proof must establish the task's trusted statement, the constant SvGolf.Tasks.AesSbox.Statement of Spec.lean (module tasks.aes_sbox.Spec). Below it is split into the properties a circuit must have, one card each: what the property guarantees in plain words, and its exact Lean text. Every proved reference has all of them. The last tab, what does not count, lists the designs the checker rejects.

Properties

A design meets the trusted statement exactly when it has all of the properties below. Lean checks that, together, they say exactly what the statement says, nothing less and nothing more (the theorem statement_iff_properties).

INTERFACEExactly these ports, in this order, with these widths.

The module has exactly the input port x (8 bits) and exactly the output port y (8 bits), with these widths, in this order. Nothing is missing and nothing is extra: an extra input could serve as a hidden mode pin, and the checker and the scoring tools drive and read the design by these names and widths.

Interface

/-- Exactly these ports, in this order, with these widths. -/
def Interface (d : Design2) : Prop :=
  inputPorts d = [("x", 8)] ∧ outputPorts d = [("y", 8)]

svgolf/tasks/aes_sbox/Properties.lean:17Open in code

UNCLOCKEDNo process runs at a clock edge (no always_ff, no always @(posedge …)).

No process of the design runs at a clock edge: no always_ff, no always @(posedge …), no asynchronous-reset block; only continuous assignments and always_comb blocks. The task is combinational, so it never needs one. The rule closes a gap between Lean's model of SystemVerilog, which the proof is about, and real tools: the model runs every clocked block once per cycle whatever its clock does, so a design that registers correct outputs on a clock nothing drives would look right there, while a simulator sees a clock that never ticks and synthesis removes the registers.

Unclocked

/-- No process runs at a clock edge (no `always_ff`, no `always @(posedge …)`). -/
def Unclocked (d : Design2) : Prop :=
  ∀ p ∈ d.processes.toList, p.isEdgePhase = false

svgolf/tasks/aes_sbox/Properties.lean:21Open in code

LOOP_FREENo combinational loop: the design lowers to continuous assigns (Design2.lowerComb) that are ranked (Acyclic): each reads only what lower-ranked ones write.

The design has no combinational loop: written as continuous assignments (each always_comb block becomes one), its processes can be ranked so that each reads only what lower-ranked ones write. A latch (an always_comb block that keeps a value on some path) is refused with it. Lean's model starts every signal at x and settles, so it would read a loop at one state, while a circuit powers up in any 0/1 state the loop can hold and keeps it; the rule removes that question instead of answering it. The ranking is of processes, not bits, so a process that reads a part of a signal it writes itself is refused too, even when no bit depends on itself: write such bits as separate assignments.

LoopFree

/-- No combinational loop: the design lowers to continuous assigns (`Design2.lowerComb`) that are
ranked (`Acyclic`): each reads only what lower-ranked ones write. -/
def LoopFree (d : Design2) : Prop :=
  ∃ d', d.lowerComb = some d' ∧ Acyclic d'

svgolf/tasks/aes_sbox/Properties.lean:25Open in code

TERMINATESUnder every schedule and every stimulus, the run completes.

Whatever order the simulator picks for processes that are ready at the same moment (the schedule), and whatever values the inputs take, simulating the design completes: every cycle settles. A combinational loop that oscillates fails this, and so does a design the tools could not read. It is also what gives the next property its teeth: that one is about completed runs, and a design with no completed run would satisfy it without computing anything.

Terminates

/-- Under every schedule and every stimulus, the run completes. -/
def Terminates (d : Design2) : Prop :=
  ∀ (σ : ScheduleOracle) (stim : List SvState), ∃ tr, Runs2 d σ stim tr

svgolf/tasks/aes_sbox/Properties.lean:30Open in code

COMPUTES_SBOXIn every completed run, every cycle whose stimulus drives x with a known value ends with y holding the AES S-box of x.

In every cycle in which the input x is driven with a known 0/1 value, the output y settles to S(x), the AES S-box of FIPS 197: the multiplicative inverse of x in GF(2^8) (with 0 mapped to 0) followed by the standard affine transformation. For example S(0x53) = 0xed, the standard's own worked example. The outputs must be fully known 0/1 values in every cycle of every run, whatever the earlier cycles were, so they cannot depend on history.

ComputesSbox

/-- In every completed run, every cycle whose stimulus drives `x` with a known value ends with
`y` holding the AES S-box of `x`. -/
def ComputesSbox (d : Design2) : Prop :=
  d ⊨₂ spec2 fun stim tr =>
    ∀ (c : Nat) (inputs st : SvState), stim[c]? = some inputs → tr[c]? = some st →
      ∀ (x : BitVec 8),
        HoldAll inputs [("x", 8)] (x, ()) →
        HoldAll st [("y", 8)] (sbox x, ())

svgolf/tasks/aes_sbox/Properties.lean:34Open in code

Definitions

The names the properties use, each with its Lean text. Trusted text is what a proof is about; a helper of Properties.lean is not trusted: Lean checks it as part of statement_iff_properties.

This task's trusted text

sboxSpec.leanThe AES S-box: affine (ginv x). Defined algebraically, as the standard defines it; the standard's 256-entry table is only a cross-check.

sbox

/-- **The AES S-box.** -/
def sbox (x : BitVec 8) : BitVec 8 := affine (ginv x)

svgolf/tasks/aes_sbox/Spec.lean:68Open in code

ginvSpec.leanThe multiplicative inverse in GF(2^8), computed as a^254 (0 for 0).

ginv

/-- The multiplicative inverse, `0` for `0`: `a^254 = a^2 * a^4 * ... * a^128` (the group has order 255). -/
def ginv (a : BitVec 8) : BitVec 8 :=
  let a2 := gmul a a
  let a4 := gmul a2 a2
  let a8 := gmul a4 a4
  let a16 := gmul a8 a8
  let a32 := gmul a16 a16
  let a64 := gmul a32 a32
  let a128 := gmul a64 a64
  gmul (gmul (gmul a2 a4) (gmul a8 a16)) (gmul (gmul a32 a64) a128)

svgolf/tasks/aes_sbox/Spec.lean:52Open in code

gmulSpec.leanMultiplication in GF(2^8) = GF(2)[x]/(x^8 + x^4 + x^3 + x + 1), by shift and add.

gmul

/-- Multiplication in GF(2^8) (FIPS 197, Section 4.2). -/
def gmul (a b : BitVec 8) : BitVec 8 := gmulAux 8 a b 0

svgolf/tasks/aes_sbox/Spec.lean:49Open in code

affineSpec.leanThe affine transformation of the standard: b XOR (b rotated left by 1, 2, 3 and 4) XOR 0x63.

affine

/-- The affine transformation of Section 5.1.1, Equations (5.3) and (5.4) of the 2023 edition:
`b'_i = b_i ^ b_(i+4) ^ b_(i+5) ^ b_(i+6) ^ b_(i+7) ^ c_i` with `c = 0x63` (indices mod 8). -/
def affine (b : BitVec 8) : BitVec 8 :=
  b ^^^ b.rotateLeft 1 ^^^ b.rotateLeft 2 ^^^ b.rotateLeft 3 ^^^ b.rotateLeft 4 ^^^ 0x63#8

svgolf/tasks/aes_sbox/Spec.lean:63Open in code

StatementSpec.leanThe trusted challenge statement that these properties restate, part by part.

Statement

/-- **The challenge statement** for the parameterless design `Submission.design.sem : Design2`. -/
abbrev Statement : LeanModels.Sv.Design2 → Prop := task.StatementFixed

svgolf/tasks/aes_sbox/Spec.lean:80Open in code

taskSpec.leanThe task as data: the parameter range, the ports at each parameter value, and the function the outputs must compute.

task

/-- The task: input `x : BitVec 8`, output `y = sbox x`. Fixed size (statement at `N = 0`). -/
def task : CombTask where
  inRange N := N = 0
  inputs _ := [("x", 8)]
  outputs _ := [("y", 8)]
  fn _ := fun (x, ()) => (sbox x, ())

svgolf/tasks/aes_sbox/Spec.lean:73Open in code

The shared trusted base

CombTask.SatisfiedAtTask.leanThe trusted form of a combinational statement at one parameter value: the interface, then no clock and termination, then the function.

SatisfiedAt

/-- The statement at one parameter value: interface; no clocked process, no
combinational loop and termination; function. Conjunct 2 is the triple
`Unclocked d ∧ LoopFree d ∧ Terminates2 d`. -/
def SatisfiedAt (N : Nat) (d : Design2) : Prop :=
  t.Interface N d ∧ (Unclocked d ∧ LoopFree d ∧ Terminates2 d) ∧ t.Computes N d

svgolf/SvGolf/Task.lean:262Open in code

inputPortsTask.leanThe design's input ports, each with its declared width, in declaration order.

inputPorts

/-- The input ports of `d` with their declared widths, in declaration order.
`instantiate2` lists the ports first, in port-list order. A declaration is
an input port iff its `isInput` flag is set. -/
def inputPorts (d : Design2) : List Sig :=
  d.decls.toList.filterMap fun dc => if dc.isInput then some (dc.name, dc.width) else none

svgolf/SvGolf/Task.lean:178Open in code

outputPortsTask.leanThe design's output ports, each with its declared width, in declaration order.

outputPorts

/-- The output ports of `d` with their declared widths, in declaration order.
A declaration is an output port iff its `isOutput` flag is set. -/
def outputPorts (d : Design2) : List Sig :=
  d.decls.toList.filterMap fun dc => if dc.isOutput then some (dc.name, dc.width) else none

svgolf/SvGolf/Task.lean:184Open in code

HoldAllTask.leanHoldAll st ports values: in the state st, every listed port holds its value as a known bit vector (no x, no z) of exactly the port's width.

HoldAll

/-- `HoldAll st sigs v`: in state `st`, every port `(n, w)` of `sigs` is bound
to the fully known `w`-bit vector that `v` assigns it. -/
def HoldAll (st : SvState) : (sigs : List Sig) → Vals (sigs.map Prod.snd) → Prop
  | [], _ => True
  | (n, _) :: sigs, v => SvState.lookup st n = some (LVec.ofBitVec v.1) ∧ HoldAll st sigs v.2

svgolf/SvGolf/Task.lean:197Open in code

⊨₂Spec2.leand ⊨₂ P: in every completed run of the design d, under every schedule and every stimulus, the stimulus and the trace satisfy P.

Models2

/-- `d ⊨₂ P` — for **every** legal schedule, every stimulus, and every
completed run (`Runs2`), the trace satisfies `P`. Introduce from a raw
∀-fuel fact with `Models2.of_run`; eliminate against a concrete run with
`Models2.run` / `Models2.runs`. Says nothing about whether runs complete —
pair it with `Terminates2`. -/
def Models2 (d : Design2) (P : TraceProp2) : Prop :=
  ∀ (σ : ScheduleOracle) (stim tr : List SvState), Runs2 d σ stim tr → P d stim tr

@[inherit_doc] scoped infix:50 " ⊨₂ " => Models2

LeanModels/Sv/Spec2.lean:141Open in code

spec2Spec2.leanTurns a property of a stimulus (one input entry per cycle) and a trace (one snapshot of every signal per cycle) into the form ⊨₂ takes.

spec2

/-- Lift a design-agnostic stimulus/trace predicate into `⊨₂`
(`d ⊨₂ spec2 fun stim tr => …`). -/
def spec2 (P : List SvState → List SvState → Prop) : TraceProp2 := fun _ stim tr => P stim tr

LeanModels/Sv/Spec2.lean:151Open in code

Runs2Spec2.leanRuns2 d σ stim tr: simulating d under the schedule σ on the stimulus stim completes, with the trace tr.

Runs2

/-- The fuel-abstracted Design2 run judgment: *some* fuel completes the run
of `d` under schedule `σ` and stimulus `stim` with trace `tr`. The only place
fuel appears in a Design2 spec. -/
def Runs2 (d : Design2) (σ : ScheduleOracle) (stim tr : List SvState) : Prop :=
  ∃ fuel, run2 d σ fuel stim = .ok tr

LeanModels/Sv/Spec2.lean:121Open in code

ScheduleOracleSemantics.leanA legal schedule: the order in which the simulator runs the processes that are ready at the same moment. The statement quantifies over all of them.

ScheduleOracle

/-- A legal schedule: at invocation `k`, orders the ready process list.
`choose_perm` is the legality proof — every invocation is a permutation of
the ready list — so `∀ σ : ScheduleOracle` ranges over exactly the legal
schedules. See the module docstring for the invocation-counter protocol. -/
structure ScheduleOracle where
  /-- Invocation counter and ready process indices in, execution order out. -/
  choose : Nat → List Nat → List Nat
  /-- Every invocation yields a permutation of the ready list. -/
  choose_perm : ∀ (k : Nat) (ready : List Nat), (choose k ready).Perm ready

LeanModels/Sv/Semantics.lean:151Open in code

Process2.isEdgePhaseSem2.leanTrue for the processes that run at the clock edge: always_ff, always @(posedge …) and asynchronous-reset blocks.

isEdgePhase

/-- Edge-phase processes: every posedge-clocked block, INCLUDING the
async-reset ones (the posedge fires with reset asserted too — the body's
reset branch is what holds the state, pin3 CYCLE 4). -/
def Process2.isEdgePhase : Process2 → Bool
  | .alwaysFF _ _ | .alwaysPlain _ _ | .alwaysFFR _ _ _ _ => true
  | _ => false

LeanModels/Sv/Sem2.lean:650Open in code

What does not count

Designs that try to score without meeting the statement (negatives), or that exploit a place where the proof's reading and the scored netlist could differ (attacks). The checker stops at the first stage that refuses; each design is listed with that stage.

Refused before any proof is tried: 7 designs (by stage: source 4, extract 1, banlist 1, fourstate 1)
Rejected at the proof: 4 designs (by stage: solution 4)

Refused before any proof is tried

The checker's static stages read the text itself and refuse it: an operator the task bans, a construct that two tools read differently, an unknown (x or z) value that could arise, or a program the language forbids.

case_missing_x.sv (attack, stopped at source): A table that sends one input to a default of x, which Yosys may fill with any value.