Record `baa9fb38c985`

reference: par, not an entryreference: par, not an entry scored at the one fixed size

Recorded by the maintainers from the proved reference sbox_bp: its design and its proof sbox_bp.lean (202 code lines). The Boyar-Peralta 113-gate circuit, translated gate for gate from the authors' netlist. The record shows that reference passing the whole checker. It is par, the bar to beatpar, the bar to beat, not a player's entry, and it is not ranked among the submissions (proved references).

Area

892.11µm²

892.1056 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: this design is par
on this page: 2nd of 5 designs

cells: 123
flops: 0
repair: 0 buffers, 0 tie cells
GE: 200.986 extra
A1′: 1 094.80 µm² research

Performance · time

4 297ps

the delay: the latest output arrival, y[6] rising

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: this design is par
on this page: 5th of 5 designs

Fmax-eq.: 232.7 MHz derived
critical path: 18 cells
unit depth: 21 extra
A1′: 4 160 ps research

Score · area × time

3833µm²·ns

892.1056 µm² × 4 297 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: this design is par
on this page: 3rd of 5 designs
board: par, the bar to beat: never ranked
Pareto: dominated on this page by tower-shuffle

On the board, of 1 other player: 0 beaten, 0 level, 0 trade off, 1 ahead.

how these numbers are measured and compared

Area: sky130 A0′, the repaired netlist. Time: NLDM, inputs driven by buf_8, 10 fF per output bit, no wires.

Area, time and score are ranked (the leaderboard orders by the score); a number tagged extra, derived or research is shown, never ranked. Fmax-equivalent = 10⁶ / time in ps, for comparison with sites that quote Fmax.

The field is the ranked records of aes_sbox's other players at this revision (1 player, 1 record), never the references, the baselines or a rejected design; each player counts once, at their best, and ties are exact at the recorded unit; advisory, recomputed at every build, never stored in a record and never used by the ranking.

On the board, another player is beaten when this design dominates every record of theirs, level when none of theirs is better and one is identical (the rest dominated), ahead when a record of theirs dominates this design, and a trade off otherwise (one of theirs better on one axis, worse on the other).

“On this page” and “Pareto” compare with the 5 designs of the area-time plot (2 references, 1 submission and 2 baselines): not a ranking.

Area

13.355µm²

13.35528 µm² exactly

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par: this design is par
on this page: smallest of 5 designs

cells: 141
flops: 0
repair: 0 buffers, 0 tie cells
GE: 200.986 extra

Performance · time

704ps

the delay: the latest output arrival

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: this design is par
on this page: 5th of 5 designs

Fmax-eq.: 1420.5 MHz derived
unit depth: 21 extra

Score · area × time

9.402µm²·ns

13.35528 µm² × 704 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: this design is par
on this page: 3rd of 5 designs
board: par, the bar to beat: never ranked
Pareto: on the front

On the board, of 1 other player: 0 beaten, 0 level, 1 trade off, 0 ahead.

how these numbers are measured and compared

Area: ASAP7 A0′ (asap7_a0_v1), the same scored netlist, each gate its least-area ASAP7 build, repaired by buffering. Time: NLDM, inputs driven by BUFx8, 2.5 fF per output bit, no wires; a table read below its grid is read at its floor. ASAP7: a predictive 7 nm library, never fabricated; no wires, like sky130's score (how ASAP7 is scored, and its quirks).

Area, time and score order this view's board (by the score); the records' ranked score is sky130's, the default view; a number tagged extra, derived or research is shown, never ranked. Fmax-equivalent = 10⁶ / time in ps, for comparison with sites that quote Fmax.

“On this page” and “Pareto” compare with the 5 designs of the area-time plot (2 references, 1 submission and 2 baselines): not a ranking.

The sources

sbox_bp.svdownload

// AES S-box as the 113-gate straight-line program of Boyar and Peralta, translated gate for gate.
//
// Source: the netlist file SLP_AES_113.txt of https://www.cs.yale.edu/homes/peralta/CircuitStuff/
// (fetched 2026-10-30, sha256 de1d21c8...b55c0; 113 gates: 32 AND, 77 XOR, 4 XNOR; depth 27, computed from the
// file). The technique: J. Boyar and R. Peralta, "A new combinational logic minimization technique with
// applications to cryptology", SEA 2010 (LNCS 6049); its journal version: J. Boyar, P. Matthews and
// R. Peralta, "Logic minimization techniques with applications to cryptology", J. Cryptology 26(2), 2013.
// Which of these first printed the 113-gate figure is recalled, not checked.
//
// Translation (tests/aes_sbox/validate/validate.py checks it gate for gate against the fetched file): the file's
// input U<i> is x[7-i] and its output S<i> is y[7-i] (U0 and S0 are the most significant bits, as in FIPS 197
// bit order); "+" is ^, "x" is &, "#" (XNOR) is written a ^ b ^ 1'b1; every name is kept. All 256 inputs
// agree with FIPS 197 Table 4 (validate.py, and Verilator in tests/aes_sbox/validate/).
module aes_sbox (input logic [7:0] x, output logic [7:0] y);
  logic y4, tc5, tc12, tc20, tc26, t37, t27, t4, y10, t23, tc1, y5, t40, z8, t5, t25, z10, t3, y9, t30, y11, t15, y8, t0, tc18, t28, t1, t9, tc7, z17, y3, t45, y6, z5, y18, tc10, t43, t26, t41, t31, z12, t29, t36, z13, tc17, tc13, y15, z7, t13, t44, tc16, y17, z2, z16, t12, t11, z9, y14, y2, z6, tc21, t17, t6, t34, t35, y16, z3, t33, y20, t2, y13, t8, z0, t42, tc2, tc9, tc3, t24, t18, t21, z1, t10, tc11, z4, t7, t32, t39, y12, y21, tc8, t20, y7, t22, z11, z14, t19, t38, y1, y19, z15, tc14, t14, tc6, tc4, t16;
  assign y14 = x[4] ^ x[2];
  assign y13 = x[7] ^ x[1];
  assign y9 = x[7] ^ x[4];
  assign y8 = x[7] ^ x[2];
  assign t0 = x[6] ^ x[5];
  assign y1 = t0 ^ x[0];
  assign y4 = y1 ^ x[4];
  assign y12 = y13 ^ y14;
  assign y2 = y1 ^ x[7];
  assign y5 = y1 ^ x[1];
  assign y3 = y5 ^ y8;
  assign t1 = x[3] ^ y12;
  assign y15 = t1 ^ x[2];
  assign y20 = t1 ^ x[6];
  assign y6 = y15 ^ x[0];
  assign y10 = y15 ^ t0;
  assign y11 = y20 ^ y9;
  assign y7 = x[0] ^ y11;
  assign y17 = y10 ^ y11;
  assign y19 = y10 ^ y8;
  assign y16 = t0 ^ y11;
  assign y21 = y13 ^ y16;
  assign y18 = x[7] ^ y16;
  assign t2 = y12 & y15;
  assign t3 = y3 & y6;
  assign t4 = t3 ^ t2;
  assign t5 = y4 & x[0];
  assign t6 = t5 ^ t2;
  assign t7 = y13 & y16;
  assign t8 = y5 & y1;
  assign t9 = t8 ^ t7;
  assign t10 = y2 & y7;
  assign t11 = t10 ^ t7;
  assign t12 = y9 & y11;
  assign t13 = y14 & y17;
  assign t14 = t13 ^ t12;
  assign t15 = y8 & y10;
  assign t16 = t15 ^ t12;
  assign t17 = t4 ^ y20;
  assign t18 = t6 ^ t16;
  assign t19 = t9 ^ t14;
  assign t20 = t11 ^ t16;
  assign t21 = t17 ^ t14;
  assign t22 = t18 ^ y19;
  assign t23 = t19 ^ y21;
  assign t24 = t20 ^ y18;
  assign t25 = t21 ^ t22;
  assign t26 = t21 & t23;
  assign t27 = t24 ^ t26;
  assign t28 = t25 & t27;
  assign t29 = t28 ^ t22;
  assign t30 = t23 ^ t24;
  assign t31 = t22 ^ t26;
  assign t32 = t31 & t30;
  assign t33 = t32 ^ t24;
  assign t34 = t23 ^ t33;
  assign t35 = t27 ^ t33;
  assign t36 = t24 & t35;
  assign t37 = t36 ^ t34;
  assign t38 = t27 ^ t36;
  assign t39 = t29 & t38;
  assign t40 = t25 ^ t39;
  assign t41 = t40 ^ t37;
  assign t42 = t29 ^ t33;
  assign t43 = t29 ^ t40;
  assign t44 = t33 ^ t37;
  assign t45 = t42 ^ t41;
  assign z0 = t44 & y15;
  assign z1 = t37 & y6;
  assign z2 = t33 & x[0];
  assign z3 = t43 & y16;
  assign z4 = t40 & y1;
  assign z5 = t29 & y7;
  assign z6 = t42 & y11;
  assign z7 = t45 & y17;
  assign z8 = t41 & y10;
  assign z9 = t44 & y12;
  assign z10 = t37 & y3;
  assign z11 = t33 & y4;
  assign z12 = t43 & y13;
  assign z13 = t40 & y5;
  assign z14 = t29 & y2;
  assign z15 = t42 & y9;
  assign z16 = t45 & y14;
  assign z17 = t41 & y8;
  assign tc1 = z15 ^ z16;
  assign tc2 = z10 ^ tc1;
  assign tc3 = z9 ^ tc2;
  assign tc4 = z0 ^ z2;
  assign tc5 = z1 ^ z0;
  assign tc6 = z3 ^ z4;
  assign tc7 = z12 ^ tc4;
  assign tc8 = z7 ^ tc6;
  assign tc9 = z8 ^ tc7;
  assign tc10 = tc8 ^ tc9;
  assign tc11 = tc6 ^ tc5;
  assign tc12 = z3 ^ z5;
  assign tc13 = z13 ^ tc1;
  assign tc14 = tc4 ^ tc12;
  assign y[4] = tc3 ^ tc11;
  assign tc16 = z6 ^ tc8;
  assign tc17 = z14 ^ tc10;
  assign tc18 = tc13 ^ tc14;
  assign y[0] = z12 ^ tc18 ^ 1'b1;
  assign tc20 = z15 ^ tc16;
  assign tc21 = tc2 ^ z11;
  assign y[7] = tc3 ^ tc16;
  assign y[1] = tc10 ^ tc18 ^ 1'b1;
  assign y[3] = tc14 ^ y[4];
  assign y[6] = y[4] ^ tc16 ^ 1'b1;
  assign tc26 = tc17 ^ tc20;
  assign y[5] = tc26 ^ z17 ^ 1'b1;
  assign y[2] = tc21 ^ tc17;
endmodule

sbox_bp.lean (202 code lines)

import Submission.Design
import SvGolf.Comb
import LeanModels.Sv.CombEqTactic
import LeanModels.Sv.CombLib

/-!
# Reference solution for task `aes_sbox`: the Boyar-Peralta 113-gate netlist

This is a submission file like any player's `Solution.lean`: the checker generates `Submission.Design`
(`Submission.design`, `Submission.Goal`) and this file proves `theorem Submission.solution : Submission.Goal`
for the fixed-size S-box statement (`SvGolf.Tasks.AesSbox.Statement`, i.e. `y = sbox x` for every known `x`).
The design is `reference/sbox_bp.sv`: 113 continuous assigns over `^` and `&` (XNOR as `a ^ b ^ 1'b1`),
no generate loop, 105 internal one-bit nets. This file is GENERATED from it by
`tests/aes_sbox/validate/gen_bp_proof.py` (`--check` regenerates it and compares); every line that
mentions a gate number is a table. `PROVING.md`, section "A flat 113-gate netlist", says what scaled and what did not.

## Route

1. **Structure** (`bp_struct`): `CombDesign` and `Acyclic` in one theorem, by `sv_structure`. The design has no
   parameter and no generate loop, so the tactic decides its four obligations (reads and windows in range, one
   driver per bit, rank decreases) as closed statements about the list of 113 sites instead of normalizing
   them. The rank is the gate's depth (`bpRank`).
2. **Ports** (`bp_interface`): `sv_interface`.
3. **Equations** (`solution`): `CombTask.satisfiedAt_of_comb`, then `sv_equations`, which hands over the 113
   equations and knownness facts under their stable names (`eq_<net>_<k>`, `known_<net>_<k>`; the nets
   `y[0] .. y[7]` are `eq_y_1 .. eq_y_8` in source order). `gok_chain` chains them into `GOK`. The design is a
   flat netlist (every site plain, no parameter), so `sv_equations` also DECIDES its other obligations (in
   range, widths, bit reads, and the coverage of all 221 reads) and returns only `inputsKnown`.
4. **Arithmetic**: the netlist is also a plain-Lean straight-line program (`bpProg`) whose environment is
   packed in one natural number (`runN`, one bit per net); the kernel evaluates it on all 256 inputs
   (`bp_correct`, GMP arithmetic on a 121-bit natural; no native-code decision procedure), and `bp_vals` (an induction over
   the gate list) says that a state meeting the gates' equations holds the program's values.
-/

namespace Submission

open LeanModels.Sv LeanModels.Sv.CombView LeanModels.Sv.CombLib LeanModels.Sv.CombEq SvGolf
open SvGolf.Tasks.AesSbox


/-! ## 0. The netlist as data (plain Lean)

The 113 gates of `reference/sbox_bp.sv`, in source order: gate `k` computes the value of environment
index `8 + k` from two earlier indices; indices `0 .. 7` are the input bits `x[0] .. x[7]`. -/

inductive GOp | xor | and | xnor

structure Gate where
  op : GOp
  a : Nat
  b : Nat

def evalGate : GOp → Bool → Bool → Bool
  | .xor, u, v => u ^^ v
  | .and, u, v => u && v
  | .xnor, u, v => u ^^ v ^^ true

/-- The gates, in the order of the `assign`s of `sbox_bp.sv` (`plain#k` is gate `k`). -/
def bpProg : List Gate :=
  [⟨.xor, 4, 2⟩, ⟨.xor, 7, 1⟩, ⟨.xor, 7, 4⟩, ⟨.xor, 7, 2⟩,
   ⟨.xor, 6, 5⟩, ⟨.xor, 12, 0⟩, ⟨.xor, 13, 4⟩, ⟨.xor, 9, 8⟩,
   ⟨.xor, 13, 7⟩, ⟨.xor, 13, 1⟩, ⟨.xor, 17, 11⟩, ⟨.xor, 3, 15⟩,
   ⟨.xor, 19, 2⟩, ⟨.xor, 19, 6⟩, ⟨.xor, 20, 0⟩, ⟨.xor, 20, 12⟩,
   ⟨.xor, 21, 10⟩, ⟨.xor, 0, 24⟩, ⟨.xor, 23, 24⟩, ⟨.xor, 23, 11⟩,
   ⟨.xor, 12, 24⟩, ⟨.xor, 9, 28⟩, ⟨.xor, 7, 28⟩, ⟨.and, 15, 20⟩,
   ⟨.and, 18, 22⟩, ⟨.xor, 32, 31⟩, ⟨.and, 14, 0⟩, ⟨.xor, 34, 31⟩,
   ⟨.and, 9, 28⟩, ⟨.and, 17, 13⟩, ⟨.xor, 37, 36⟩, ⟨.and, 16, 25⟩,
   ⟨.xor, 39, 36⟩, ⟨.and, 10, 24⟩, ⟨.and, 8, 26⟩, ⟨.xor, 42, 41⟩,
   ⟨.and, 11, 23⟩, ⟨.xor, 44, 41⟩, ⟨.xor, 33, 21⟩, ⟨.xor, 35, 45⟩,
   ⟨.xor, 38, 43⟩, ⟨.xor, 40, 45⟩, ⟨.xor, 46, 43⟩, ⟨.xor, 47, 27⟩,
   ⟨.xor, 48, 29⟩, ⟨.xor, 49, 30⟩, ⟨.xor, 50, 51⟩, ⟨.and, 50, 52⟩,
   ⟨.xor, 53, 55⟩, ⟨.and, 54, 56⟩, ⟨.xor, 57, 51⟩, ⟨.xor, 52, 53⟩,
   ⟨.xor, 51, 55⟩, ⟨.and, 60, 59⟩, ⟨.xor, 61, 53⟩, ⟨.xor, 52, 62⟩,
   ⟨.xor, 56, 62⟩, ⟨.and, 53, 64⟩, ⟨.xor, 65, 63⟩, ⟨.xor, 56, 65⟩,
   ⟨.and, 58, 67⟩, ⟨.xor, 54, 68⟩, ⟨.xor, 69, 66⟩, ⟨.xor, 58, 62⟩,
   ⟨.xor, 58, 69⟩, ⟨.xor, 62, 66⟩, ⟨.xor, 71, 70⟩, ⟨.and, 73, 20⟩,
   ⟨.and, 66, 22⟩, ⟨.and, 62, 0⟩, ⟨.and, 72, 28⟩, ⟨.and, 69, 13⟩,
   ⟨.and, 58, 25⟩, ⟨.and, 71, 24⟩, ⟨.and, 74, 26⟩, ⟨.and, 70, 23⟩,
   ⟨.and, 73, 15⟩, ⟨.and, 66, 18⟩, ⟨.and, 62, 14⟩, ⟨.and, 72, 9⟩,
   ⟨.and, 69, 17⟩, ⟨.and, 58, 16⟩, ⟨.and, 71, 10⟩, ⟨.and, 74, 8⟩,
   ⟨.and, 70, 11⟩, ⟨.xor, 90, 91⟩, ⟨.xor, 85, 93⟩, ⟨.xor, 84, 94⟩,
   ⟨.xor, 75, 77⟩, ⟨.xor, 76, 75⟩, ⟨.xor, 78, 79⟩, ⟨.xor, 87, 96⟩,
   ⟨.xor, 82, 98⟩, ⟨.xor, 83, 99⟩, ⟨.xor, 100, 101⟩, ⟨.xor, 98, 97⟩,
   ⟨.xor, 78, 80⟩, ⟨.xor, 88, 93⟩, ⟨.xor, 96, 104⟩, ⟨.xor, 95, 103⟩,
   ⟨.xor, 81, 100⟩, ⟨.xor, 89, 102⟩, ⟨.xor, 105, 106⟩, ⟨.xnor, 87, 110⟩,
   ⟨.xor, 90, 108⟩, ⟨.xor, 94, 86⟩, ⟨.xor, 95, 108⟩, ⟨.xnor, 102, 110⟩,
   ⟨.xor, 106, 107⟩, ⟨.xnor, 107, 108⟩, ⟨.xor, 109, 112⟩, ⟨.xnor, 118, 92⟩,
   ⟨.xor, 113, 109⟩]

/-- The signal bit each environment index stands for: `("x", i)` for the inputs, then the target of
each gate. -/
def bpLocs : List (String × Nat) :=
  [("x", 0), ("x", 1), ("x", 2), ("x", 3), ("x", 4), ("x", 5),
   ("x", 6), ("x", 7), ("y14", 0), ("y13", 0), ("y9", 0), ("y8", 0),
   ("t0", 0), ("y1", 0), ("y4", 0), ("y12", 0), ("y2", 0), ("y5", 0),
   ("y3", 0), ("t1", 0), ("y15", 0), ("y20", 0), ("y6", 0), ("y10", 0),
   ("y11", 0), ("y7", 0), ("y17", 0), ("y19", 0), ("y16", 0), ("y21", 0),
   ("y18", 0), ("t2", 0), ("t3", 0), ("t4", 0), ("t5", 0), ("t6", 0),
   ("t7", 0), ("t8", 0), ("t9", 0), ("t10", 0), ("t11", 0), ("t12", 0),
   ("t13", 0), ("t14", 0), ("t15", 0), ("t16", 0), ("t17", 0), ("t18", 0),
   ("t19", 0), ("t20", 0), ("t21", 0), ("t22", 0), ("t23", 0), ("t24", 0),
   ("t25", 0), ("t26", 0), ("t27", 0), ("t28", 0), ("t29", 0), ("t30", 0),
   ("t31", 0), ("t32", 0), ("t33", 0), ("t34", 0), ("t35", 0), ("t36", 0),
   ("t37", 0), ("t38", 0), ("t39", 0), ("t40", 0), ("t41", 0), ("t42", 0),
   ("t43", 0), ("t44", 0), ("t45", 0), ("z0", 0), ("z1", 0), ("z2", 0),
   ("z3", 0), ("z4", 0), ("z5", 0), ("z6", 0), ("z7", 0), ("z8", 0),
   ("z9", 0), ("z10", 0), ("z11", 0), ("z12", 0), ("z13", 0), ("z14", 0),
   ("z15", 0), ("z16", 0), ("z17", 0), ("tc1", 0), ("tc2", 0), ("tc3", 0),
   ("tc4", 0), ("tc5", 0), ("tc6", 0), ("tc7", 0), ("tc8", 0), ("tc9", 0),
   ("tc10", 0), ("tc11", 0), ("tc12", 0), ("tc13", 0), ("tc14", 0), ("y", 4),
   ("tc16", 0), ("tc17", 0), ("tc18", 0), ("y", 0), ("tc20", 0), ("tc21", 0),
   ("y", 7), ("y", 1), ("y", 3), ("y", 6), ("tc26", 0), ("y", 5),
   ("y", 2)]

/-- The gate driving `y[j]`. -/
def bpYGate : List Nat := [103, 107, 112, 108, 99, 111, 109, 106]

/-- The site depths: the rank of `sv_structure`. -/
def bpRank : List Nat := [1, 1, 1, 1, 1, 2, 3, 2, 3, 3, 4, 3, 4, 4, 5, 5, 5, 6, 6, 6, 6, 7, 7, 5, 6, 7, 4, 6, 7, 4, 8, 7, 8, 6, 7, 8, 6, 7, 8, 8, 9, 9, 9, 9, 10, 10, 10, 11, 12, 13, 14, 11, 12, 13, 14, 15, 15, 16, 17, 17, 18, 19, 20, 15, 20, 18, 21, 19, 18, 15, 21, 20, 15, 16, 22, 21, 19, 18, 15, 21, 20, 15, 16, 22, 21, 23, 24, 25, 20, 20, 22, 22, 23, 23, 24, 23, 22, 24, 23, 26, 24, 25, 25, 26, 25, 25, 26, 26, 27, 27, 26, 27, 26]

/-! ## 1. Structure -/

/-- `CombDesign` and `Acyclic` of the netlist, with the rank `bpRank` (site `k` is gate `k`). -/
theorem bp_struct : CombDesign design.sem ∧ Acyclic design.sem := by
  sv_structure (rank := rippleRank (fun p => bpRank.getD p 0) (fun _ _ _ => 0))

/-! ## 2. The ports -/

/-- The task's interface: exactly the ports `x` (8 bits in) and `y` (8 bits out). -/
theorem bp_interface (hc : CombDesign design.sem) : task.Interface 0 design.sem := by
  sv_interface


/-- The packed environment after `gs` (starting at gate number `k`): bit `i` of the result is the
value of environment index `i`. -/
def stepN (e k : Nat) (g : Gate) : Nat :=
  if evalGate g.op (e.testBit g.a) (e.testBit g.b) then e ||| 2 ^ (8 + k) else e

def runN : Nat → List Gate → Nat → Nat
  | _, [], e => e
  | k, g :: gs, e => runN (k + 1) gs (stepN e k g)

/-- The gates of `gs` (numbered from `k`) read only earlier indices, and `P` satisfies each gate's
equation. -/
inductive GOK (P : Nat → Bool) : Nat → List Gate → Prop
  | nil (k : Nat) : GOK P k []
  | cons (k : Nat) (g : Gate) (gs : List Gate) (ha : g.a < 8 + k) (hb : g.b < 8 + k)
      (hp : P (8 + k) = evalGate g.op (P g.a) (P g.b)) (h : GOK P (k + 1) gs) : GOK P k (g :: gs)

theorem testBit_stepN (e k : Nat) (g : Gate) (i : Nat) :
    (stepN e k g).testBit i =
      (e.testBit i || (decide (8 + k = i) && evalGate g.op (e.testBit g.a) (e.testBit g.b))) := by
  unfold stepN
  by_cases h : evalGate g.op (e.testBit g.a) (e.testBit g.b) = true
  · simp [h, Nat.testBit_or, Nat.testBit_two_pow]
  · simp at h
    simp [h]

theorem runN_inv (P : Nat → Bool) : ∀ (gs : List Gate) (k e : Nat), GOK P k gs →
    (∀ i, i < 8 + k → P i = e.testBit i) → (∀ i, 8 + k ≤ i → e.testBit i = false) →
    ∀ i, i < 8 + k + gs.length → P i = (runN k gs e).testBit i := by
  intro gs
  induction gs with
  | nil =>
    intro k e _ h1 _ i hi
    exact h1 i (by simpa using hi)
  | cons g gs ih =>
    intro k e hgok h1 h2 i hi
    cases hgok with
    | cons _ _ _ ha hb hp hrest =>
      have hstep : ∀ i, i < 8 + (k + 1) → P i = (stepN e k g).testBit i := by
        intro i hi
        rw [testBit_stepN]
        by_cases hik : i = 8 + k
        · subst hik
          rw [h2 _ (Nat.le_refl _)]
          simp [hp, h1 _ ha, h1 _ hb]
        · have hlt : i < 8 + k := by omega
          have hne : ¬ (8 + k = i) := fun h => hik h.symm
          simp [hne, h1 i hlt]
      have hzero : ∀ i, 8 + (k + 1) ≤ i → (stepN e k g).testBit i = false := by
        intro i hi
        rw [testBit_stepN]
        have hne : ¬ (8 + k = i) := by omega
        simp [hne, h2 i (by omega)]
      exact ih (k + 1) (stepN e k g) hrest hstep hzero i (by simp at hi ⊢; omega)

/-- **The environment of the netlist, from the equations.** If `P` agrees with the input bits of
`x` and satisfies every gate's equation, then at every environment index it is the packed
program's value. -/
theorem bp_vals (P : Nat → Bool) (x : BitVec 8) (hin : ∀ i, i < 8 → P i = x.getLsbD i)
    (hg : GOK P 0 bpProg) : ∀ i, i < 8 + bpProg.length → P i = (runN 0 bpProg x.toNat).testBit i := by
  intro i hi
  refine runN_inv P bpProg 0 x.toNat hg (fun i hi => ?_) (fun i hi => ?_) i (by omega)
  · rw [BitVec.testBit_toNat]; exact hin i (by omega)
  · exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le x.isLt (Nat.pow_le_pow_right (by omega) (by omega)))

/-- **The S-box, by evaluation**: on each of the 256 inputs, the packed program's outputs are the algebraic
`sbox` (kernel evaluation of a closed function; no native-code decision procedure). -/
theorem bp_correct : ∀ n : Fin 256, ∀ j : Fin 8,
    (runN 0 bpProg n.val).testBit (8 + bpYGate.getD j.val 0) =
      (sbox (BitVec.ofFin n)).getLsbD j.val := by
  decide +kernel

/-- The environment indices of the outputs are the bits of `y`; those of the inputs are the bits of `x`. -/
theorem bp_locs_y : ∀ j : Fin 8, bpLocs.getD (8 + bpYGate.getD j.val 0) ("", 0) = ("y", j.val) := by decide

theorem bp_locs_x : ∀ i : Fin 8, bpLocs.getD i.val ("", 0) = ("x", i.val) := by decide

theorem bp_len : bpProg.length = 113 := by decide

/-- **From the equations to the outputs.** `hx`: the state's `x` bits are those of `x`; `hg`: the state meets
every gate's equation; `hs`, `hsw`, `hks`: `y` is a known 8-bit vector. Then `y = sbox x`. -/
theorem bp_out {st : SvState} {x : BitVec 8}
    (hx : ∀ i, i < 8 → st.boolAt "x" i = x.getLsbD i)
    (hg : GOK (fun i => st.boolAt (bpLocs.getD i ("", 0)).1 (bpLocs.getD i ("", 0)).2) 0 bpProg)
    {vs : LVec} (hs : SvState.lookup st "y" = some vs) (hsw : vs.width = 8)
    (hks : ∀ k, k < 8 → KnownBit st "y" k) :
    SvState.lookup st "y" = some (LVec.ofBitVec (sbox x)) := by
  have hvals := bp_vals _ x (fun i hi => by rw [bp_locs_x ⟨i, hi⟩]; exact hx i hi) hg
  have hvs := SvState.lookup_eq_ofBitVec_bv hs hsw hks
  rw [hvs] at hs
  have hy : ∀ j : Fin 8, bpYGate.getD j.val 0 < 113 := by decide
  have hy' : ∀ j, j < 8 → bpYGate.getD j 0 < 113 := fun j hj => hy ⟨j, hj⟩
  have heq : XF.bv 8 (st.boolAt "y") = sbox x := by
    apply BitVec.eq_of_getLsbD_eq
    intro j hj
    rw [XF.getLsbD_bv hj]
    have h1 := hvals (8 + bpYGate.getD j 0) (by have := hy' j hj; rw [bp_len]; omega)
    rw [bp_locs_y ⟨j, hj⟩] at h1
    simp only at h1
    rw [h1]
    simpa using bp_correct x.toFin ⟨j, hj⟩
  rw [hs, heq]
/-! ## 4. The statement -/

open Lean Elab Tactic in
/-- `gok_chain h₀ … h₁₁₂` proves `GOK P 0 bpProg` from the equations of the gates, in order: one
`GOK.cons` per name (the side conditions `g.a < 8 + k`, `g.b < 8 + k` by `decide`), then `GOK.nil`. -/
elab "gok_chain " hs:ident* : tactic => do
  for h in hs do
    evalTactic (← `(tactic| refine GOK.cons _ _ _ (by decide) (by decide) $h ?_))
  evalTactic (← `(tactic| exact GOK.nil _))

-- `solution` takes about 400 M heartbeats (the default limit is 200 M): `sv_equations` 276 M, the rest 125 M.
set_option maxHeartbeats 1000000 in
/-- **The reference solution**: the `aes_sbox` statement for the Boyar-Peralta netlist. -/
theorem solution : Goal := by
  obtain ⟨hc, ha⟩ := bp_struct
  refine CombTask.satisfiedAt_of_comb (bp_interface hc) hc ha ?_
  intro st heqs hs v hv
  obtain ⟨x, ⟨⟩⟩ := v
  simp only [SvGolf.Tasks.AesSbox.task, HoldAll_cons, HoldAll_nil, and_true] at hv ⊢
  sv_equations
  · obtain ⟨vs, hvs, hvsw⟩ := (known_y_1).1
    exact bp_out (fun i hi => SvState.boolAt_ofBitVec hv hi)
      (by gok_chain
        eq_y14_1 eq_y13_1 eq_y9_1 eq_y8_1 eq_t0_1 eq_y1_1
        eq_y4_1 eq_y12_1 eq_y2_1 eq_y5_1 eq_y3_1 eq_t1_1
        eq_y15_1 eq_y20_1 eq_y6_1 eq_y10_1 eq_y11_1 eq_y7_1
        eq_y17_1 eq_y19_1 eq_y16_1 eq_y21_1 eq_y18_1 eq_t2_1
        eq_t3_1 eq_t4_1 eq_t5_1 eq_t6_1 eq_t7_1 eq_t8_1
        eq_t9_1 eq_t10_1 eq_t11_1 eq_t12_1 eq_t13_1 eq_t14_1
        eq_t15_1 eq_t16_1 eq_t17_1 eq_t18_1 eq_t19_1 eq_t20_1
        eq_t21_1 eq_t22_1 eq_t23_1 eq_t24_1 eq_t25_1 eq_t26_1
        eq_t27_1 eq_t28_1 eq_t29_1 eq_t30_1 eq_t31_1 eq_t32_1
        eq_t33_1 eq_t34_1 eq_t35_1 eq_t36_1 eq_t37_1 eq_t38_1
        eq_t39_1 eq_t40_1 eq_t41_1 eq_t42_1 eq_t43_1 eq_t44_1
        eq_t45_1 eq_z0_1 eq_z1_1 eq_z2_1 eq_z3_1 eq_z4_1
        eq_z5_1 eq_z6_1 eq_z7_1 eq_z8_1 eq_z9_1 eq_z10_1
        eq_z11_1 eq_z12_1 eq_z13_1 eq_z14_1 eq_z15_1 eq_z16_1
        eq_z17_1 eq_tc1_1 eq_tc2_1 eq_tc3_1 eq_tc4_1 eq_tc5_1
        eq_tc6_1 eq_tc7_1 eq_tc8_1 eq_tc9_1 eq_tc10_1 eq_tc11_1
        eq_tc12_1 eq_tc13_1 eq_tc14_1 eq_y_1 eq_tc16_1 eq_tc17_1
        eq_tc18_1 eq_y_2 eq_tc20_1 eq_tc21_1 eq_y_3 eq_y_4
        eq_y_5 eq_y_6 eq_tc26_1 eq_y_7 eq_y_8)
      hvs hvsw (fun k hk => match k, hk with
        | 0, _ => (known_y_2).2
        | 1, _ => (known_y_4).2
        | 2, _ => (known_y_8).2
        | 3, _ => (known_y_5).2
        | 4, _ => (known_y_1).2
        | 5, _ => (known_y_7).2
        | 6, _ => (known_y_6).2
        | 7, _ => (known_y_3).2
        | k + 8, hk => absurd hk (by omega))
  case inputsKnown => exact inKnown_ofBitVec hv (by omega)

/--
info: 'Submission.solution' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms solution

end Submission

The netlist

The netlist card shows the sky130 weighing (its cells, its critical path): the ASAP7 view changes the overview above, not this card.

Schematic

The repaired A0′ netlist that the score weighs: 123 cells. aes_sbox has one fixed size, so there is no smaller instance to draw.

The drawing is its critical path (18 cells, ending at y[6] rising, 4 297 ps), every cell of it, and each net that enters or leaves the path drawn as a port named after the net: the whole netlist at this size is a tangle of wires. The path's own nets are in the accent colour. Drawn by netlistsvg with svGolf's sky130 skin (derived from netlistsvg's default skin, as the drawing is: MIT licence, Copyright (c) 2016 Neil Turley, the notice): one symbol per cell function, the cell above it, the instance on hover; nor2b and nand2b are drawn with the bubble on their inverted input. The cells of the path are listed under Critical path, each a link to the cell here.

The netlist at its one fixed size: 123 cells, 45 xnor2_1, 21 and2_1, 17 nand2_1, 15 xor2_1, 9 nor2b_1, 5 nand2b_1, 5 or2_1, 4 mux2_1, 2 inv_1; 18 drawn. Open the drawing on its own (SVG, 17.9 KB) to pan and zoom it with the browser's own controls.

Critical path

at the one fixed size · scored

The path the ranked delay ends on, at the task's one size: 19 nets, 18 cells, to y[6] rising at 4 297 ps. Each row is a net of the repaired netlist with the arrival and the transition the STA computed there (NLDM tables, the larger transition carried; no wires). The first row is an input: its arrival is the input driver's own delay (buf_8 fed by a 50 ps ramp). From ppa.py --path (critical_path_timing); the instance names are the schematic's (the same netlist), each a link to its cell there.

#	net	edge	driven by	cell	arrival (ps)	transition (ps)	stage (ps)
0	`x[7]`	fall	input port	–	126.0	31.6
1	`_259_`	rise	`_342_`	`xnor2_1`	360.4	247.7	234.4
2	`_261_`	rise	`_344_`	`xnor2_1`	552.4	231.5	192.0
3	`_262_`	rise	`_345_`	`xor2_1`	802.3	228.9	249.9
4	`_263_`	rise	`_346_`	`xor2_1`	1 085.4	275.0	283.1
5	`_265_`	rise	`_348_`	`xor2_1`	1 435.8	360.1	350.4
6	`_274_`	fall	`_357_`	`xor2_1`	1 582.2	111.6	146.4
7	`_292_`	fall	`_375_`	`or2_1`	1 799.0	41.5	216.8
8	`_294_`	fall	`_377_`	`mux2_1`	2 087.4	65.7	288.4
9	`_295_`	rise	`_378_`	`xnor2_1`	2 359.9	303.9	272.5
10	`_296_`	fall	`_379_`	`inv_1`	2 473.9	90.8	114.0
11	`_315_`	fall	`_398_`	`mux2_1`	2 801.9	62.0	328.0
12	`_316_`	fall	`_399_`	`and2_1`	2 979.9	54.4	178.0
13	`_317_`	fall	`_400_`	`and2_1`	3 141.8	42.8	161.9
14	`_325_`	rise	`_408_`	`xnor2_1`	3 381.6	248.3	239.8
15	`_326_`	rise	`_409_`	`xnor2_1`	3 582.1	251.5	200.5
16	`_236_`	fall	`_434_`	`xnor2_1`	3 733.0	102.4	150.9
17	`_13_`	rise	`_450_`	`xnor2_1`	4 078.8	358.8	345.8
18	`_1_`	rise	`_451_`	`xnor2_1`	4 297.1	264.8	218.3

Cells

at the one fixed size · scored

The area of each cell type in the repaired A0′ netlist, at the scoring point: the count times the cell's area in the pinned liberty. Their sum is the ranked area.

cell	count	µm² each	µm² in all	share
`xnor2_1`	45	8.7584	394.1280	44.2%
`and2_1`	21	6.2560	131.3760	14.7%
`xor2_1`	15	8.7584	131.3760	14.7%
`nand2_1`	17	3.7536	63.8112	7.2%
`nor2b_1`	9	6.2560	56.3040	6.3%
`mux2_1`	4	11.2608	45.0432	5.0%
`nand2b_1`	5	6.2560	31.2800	3.5%
`or2_1`	5	6.2560	31.2800	3.5%
`inv_1`	2	3.7536	7.5072	0.8%
total	123		892.1056

Repair (buffer_trees_v1): 0 buffers on 0 nets, 0 tie cells, 1 weighing round; nothing is resized.

Legality: worst load 0.257 × max_capacitance, worst transition 0.285 × max_transition; 0 timing-table reads outside the characterized grid.

the gate mix of the extra GE column (the pinned GE table, score/ge.json)

Cells by type; area is the count weighted by the pinned GE table.

cell	count	GE each	GE total
`XNOR`	45	2.000	90.000
`AND`	21	1.333	27.993
`NAND`	17	1.000	17.000
`XOR`	15	2.000	30.000
`ANDNOT`	9	1.333	11.997
`OR`	5	1.333	6.665
`ORNOT`	5	1.333	6.665
`MUX`	4	2.333	9.332
`NOT`	2	0.667	1.334
total	123		200.986

The record

task: aes_sbox
player: svgolf-reference
assisted by: Claude (Anthropic)
submitted: 2026-11-07
notes: reference solution
scoring point: the one fixed size
design: sbox_bp.sv sha256 7296ab636b661b2a391fd69d059da0d337571d6b82b42f883f8389c2c02b11ac
proof: sbox_bp.lean sha256 603523fa2bf3bf3f91244bc065449b09ff2c2a4f08ee8146feb02a41843123ff: the proof of the reference sbox_bp (sbox_bp.lean, 202 code lines)
canonical text: sha256 e91f6f266276d4cf9f66901e7ab02693aef4f8ae08482da6a924790e139a0ddf
record hash: baa9fb38c98506e2a068eb66d3d280bb807d94f9117619ff3f662f7d8c86a08f
downloads: baa9fb38c985.sv baa9fb38c985.lean baa9fb38c985.json

The proof

code lines: 202
build time: 692.5 s
axioms: Classical.choice, Quot.sound, propext
tactics seen: decide, induction, omega, simp, sv_equations, sv_interface, sv_structure
imports: Submission.Design, SvGolf.Comb, LeanModels.Sv.CombEqTactic, LeanModels.Sv.CombLib

Checker and flow

Checked under the pinned flow of this site's boards.

Yosys: Yosys 0.53 (git sha1 53c22ab7c0ced80861c7536c5dae682c30fb5834, clang++ 17.0.0 -fPIC -O3)
Verilator: Verilator 5.042 2025-11-02 rev UNKNOWN.REV
Lean toolchain: leanprover/lean4:v4.33.0-rc1
svGolf revision: d1f3cae6f01a088007a57b31ff8baa6b839d6f74
lean-surfaces revision: d1f3cae6f01a088007a57b31ff8baa6b839d6f74
canonicalization script: bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b
scoring script: ea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445
GE table: 6a29196a3f4b58241f4c9af650c9141e4632b737214d563a11ba142a725c4bea
extractor: 4930696021c588c75dc890034c534c95560ad9a28a4955b87d1f8d68b5edbc0c
canonical RTLIL: 190742e59ade0547948019ccf28945d76258503e60ce462ce4fea0bfd58c33e5

the checker's files (sha256)

file	sha256
`check.py`	`e708084f72f955b0ae1aaabe469dba3eacc5a91484a1ed81bcc073b60f3c0b6d`
`check/Comparator.lean`	`3145eb578ca71e452eff05a398e8ad04673e6c72ca5343b234cb22e2cefe65a6`
`check/SvEval.lean`	`fb51d72510b515460866c2798aad3c6f55295536e627b92854c3580af215bb91`
`check/clocked_rules.py`	`73856a45905724544247ad29042bdc2f1778271ec07b15cdb3a5f214685165c1`
`check/envelope.py`	`076db01a9791bcc25ee84e9b0033604a4b675f00b212eab0c864078e6a4748b7`
`check/postsynth.py`	`4e1ee2110c63f24e033dd689c929ea686ddf10f4db23b9057c6fb711394c7558`
`lakefile.toml`	`f35a88404367d22906effc14d644aac9a9cad47dfd3b704ea8fec88acfaf9c4d`
`lean-toolchain`	`62c2d9c0fc1ec4c67e151c11eff41ca004ef38e179cf9476c230406e6defedef`
`score/banlist.py`	`f18c14c23a14d55db63e202f42cc424dc84c1dd1c337f132ad60859dc9d5d33a`
`score/canon.ys`	`bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b`
`score/fourstate.py`	`95332451ae3754226fb87b46027385b46a91121e7eb9ae25b302bce756d90475`
`score/ge.json`	`6a29196a3f4b58241f4c9af650c9141e4632b737214d563a11ba142a725c4bea`
`score/ge_seq.json`	`54b93ca63888009d0671c8978e8ab7bf4fb8ce303bc78d3b4e1f83d946cc3201`
`score/ppa.py`	`912031912c3e3f6790725161753e95415df34846bd8c27dde3eb707747ddbcbe`
`score/ppa_mapped.ys`	`93547b343dbac135737e98516b1004a780e1cf2f579e1bd7fed82c908c6d4125`
`score/ppa_mapped_pins.json`	`4b8688ba3f4d67681658e5944afe878592adf588cd416a8b47597ebe06deb045`
`score/ppa_pins.json`	`d66a6086a37a97f5985266057051979fb6a8a3c557d3ef9c42acc1b5e41502d8`
`score/score.py`	`71d2e3b82f8813ec64a58f0a46909ca23dfab377db44eda6f294b713f45ae781`
`score/srcgate.py`	`11952f61058051c9e8de91a801b672d07e66a29308e978156c04ffd9f0dbef45`
`score/svgolf.ys`	`ea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445`
`score/svgolf_seq.ys`	`c3874dbfc85921a87df6eacdfc6b2c9a0e2b34edd5738951e0d8bdb51f4558b2`

Post-synthesis check

ls-sv's reading of the design and the scored netlist, simulated on the same vectors, agreed on every one. The vectors are a sample of the inputs: a guard against the two tools disagreeing, not a proof.

mode: full
vectors: 256
full set: 256
mismatches: 0
point: default
seed: 4d4422acfd407fb386f300103a982f918587a399abaf2fce163a51b6d4029f23
salted: no

Area against time

µm² × ps · lower left is better · ASAP7

submission
proved reference
baseline (not proved)
the Pareto front of the entries

this design
par's score: area × time = 3833 µm²·ns

sky130 area (x) against the ranked time (y); lower left is better on both. The step line is the Pareto front of the entries (the proved references and the players' ranked records); a design under par's score curve has a better score than par. Baselines are drawn for scale: scored, never proved. Every design is in view.

the designs as numbers, by score

design	kind	area (µm²)	time (ps)	score (µm²·ns)
tower-shuffle	submission	890.85	3 208	2858
`sbox_bp_d16`	baseline, not proved	952.16	3 670	3494
`sbox_bp` · this design	proved reference · par	892.11	4 297	3833
`sbox_table`	proved reference	3 445.80	2 288	7884
`sbox_table`	baseline, not proved	3 445.80	2 288	7884

submission
proved reference
baseline (not proved)
the Pareto front of the entries

this design
par's score: area × time = 9.402 µm²·ns

ASAP7 area (x) against the ASAP7 time (y); lower left is better on both. The step line is the Pareto front of the entries (the proved references and the players' ranked records); a design under par's score curve has a better score than par. Baselines are drawn for scale: scored, never proved. Every design is in view.

the designs as numbers, by score

design	kind	area (µm²)	time (ps)	score (µm²·ns)
tower-shuffle	submission	13.414	556	7.458
`sbox_bp_d16`	baseline, not proved	14.245	627	8.931
`sbox_bp` · this design	proved reference · par	13.355	704	9.402
`sbox_table`	proved reference	51.817	373	19.33
`sbox_table`	baseline, not proved	51.817	373	19.33

Reproduce and verify

From svgolf/, with the pinned tools (reproduce a score lists them):

shell

# the ranked numbers, at the scoring point (from svgolf/, with the pinned Yosys and liberty)
python3.12 score/ppa.py tasks/aes_sbox/reference/sbox_bp.sv --task tasks/aes_sbox --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256: 190742e59ade0547948019ccf28945d76258503e60ce462ce4fea0bfd58c33e5
ppa.netlist_sha256: 22493fba30d824a3ea9939038185b2cb797dab4f1831b98ab9a251838ea1f2cb
ppa.repair.netlist_sha256: b27773491834eb758aa0bf6f5c828d8db7ada4057055fe6e078f1dc36c154da6
ppa.area_e4um2_sky130: 8921056
ppa.delay_ps_sky130: 4297

The schematic and the critical-path data are site/schematics/aes_sbox/7296ab636b661b2a.json and its .svg, written by site/gen_schematics.py (the display instance is ppa.py ... --repaired-netlist, drawn by netlistsvg 1.0.2; repaired netlist sha256 b27773491834eb75…).

From svgolf/, with the pinned tools (reproduce a score lists them):

shell

# the ASAP7 view's numbers, at the scoring point (from svgolf/, with the pinned Yosys; once:
# python3.12 score/ppa.py --pdk asap7 --fetch-liberty, the five pinned ASAP7 files into score/lib/asap7/)
python3.12 score/ppa.py tasks/aes_sbox/reference/sbox_bp.sv --task tasks/aes_sbox --pdk asap7 --no-mapped \
    --json out.json

Expect, in out.json:

ppa.netlist_sha256: 22493fba30d824a3ea9939038185b2cb797dab4f1831b98ab9a251838ea1f2cb
ppa.repair.netlist_sha256: 19f2288bdc50054aa83efde39b136fbfa0fdefdef2de8daa427e82ad13164be5
ppa.area_e5um2_asap7: 1335528
ppa.delay_ps_asap7: 704

leaderboard/asap7/aes_sbox.json keeps these numbers; python3.12 leaderboard/leaderboard.py asap7 --rescore --task aes_sbox weighs every design of the task again and compares, bit for bit.

Verify the record

Download the three files, then from svgolf/:

shell

# re-run the whole check on this record's files (the cost of the original check)
H=baa9fb38c98506e2a068eb66d3d280bb807d94f9117619ff3f662f7d8c86a08f
mkdir -p rec/aes_sbox && cp "$H.json" "$H.sv" "$H.lean" rec/aes_sbox/
python3.12 leaderboard/leaderboard.py verify --data-dir rec --task aes_sbox --full

verify --offline checks only the hashes and the arithmetic; plain verify also rescores the design (no Lean; seconds for most designs, a minute or more for the largest), on sky130 and on ASAP7.