svGolf

Golf scores on ASAP7, a predictive 7 nm library: never fabricated, and like sky130's score it counts no wires. sky130, a real 130 nm process, is the default. How ASAP7 is scored, and its quirks.

Tasks / sorter

Streaming sorter, clocked sorter

N unsigned W-bit values in, one per cycle; the same values out in ascending order, one per cycle.

open for submissions clocked, stream scored at N = 8, W = 8

Par
222 540µm²·nssorter_ins · 5512.8 µm² × 16 cycles × 2.52 ns period
Record
157 015µm²·nskestrel-golf · 4754.6 µm² × 16 cycles × 2.06 ns period
Under par
−29%
Par
701.9µm²·nssorter_ins · 85.687 µm² × 16 cycles × 0.512 ns period
Record
538.9µm²·nskestrel-golf · 74.854 µm² × 16 cycles × 0.450 ns period
Under par
−23%

Score

ASAP7 · area × time · µm²·ns · lower is better
sorter: the score of each entry by date2 entries by date (x) and score in µm²·ns (y); the line is the best score so far, the dashed line par. The table under the chart lists the same numbers.160k180k200k220k26 Oct2 Nov9 Novdate enteredscore (µm²·ns) · lower is betterpar: sorter_ins, 222 540 µm²·nsPAR222 540 · provedthe best score so farsorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 222 540 µm²·ns · Area: 5512.8 µm² · Time: 40 368 pskestrel-golf · submission · 2026-11-10 · Score: 157 015 µm²·ns · Area: 4754.6 µm² · Time: 33 024 ps
sorter: the score of each entry by date2 entries by date (x) and score in µm²·ns (y); the line is the best score so far, the dashed line par. The table under the chart lists the same numbers.160k180k200k220k26 Oct2 Nov9 Novdate enteredscore (µm²·ns) · lower is betterpar: sorter_ins, 222 540 µm²·nsPARthe best score so farsorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 222 540 µm²·ns · Area: 5512.8 µm² · Time: 40 368 pskestrel-golf · submission · 2026-11-10 · Score: 157 015 µm²·ns · Area: 4754.6 µm² · Time: 33 024 ps
  • submission
  • proved reference
  • the best score so far
  • par
Score = area × time: the sky130 cell area of the scored netlist in µm² (flip-flops included) times the latency in cycles × the register-to-register clock period 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. The clock period (what score/ppa.py calls the register-to-register period) is the longest path from an input or a flip-flop to an output or a flip-flop (clock-to-Q and setup included), so paths from the inputs and to the outputs count too, not only the paths between two flip-flops. 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.
every entry by date
datedesignkindscore (µm²·ns)area × time
2026-11-03sorter_insproved reference · par222 5405512.8 µm² × 16 × 2.52 ns
2026-11-10kestrel-golfsubmission157 0154754.6 µm² × 16 × 2.06 ns
sorter: the score of each entry by date2 entries by date (x) and score in µm²·ns (y); the line is the best score so far, the dashed line par. The table under the chart lists the same numbers.55060065070026 Oct2 Nov9 Novdate enteredscore (µm²·ns) · lower is betterpar: sorter_ins, 701.9 µm²·nsPAR701.9 · provedthe best score so farsorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 701.9 µm²·ns · Area: 85.687 µm² · Time: 8192 pskestrel-golf · submission · 2026-11-10 · Score: 538.9 µm²·ns · Area: 74.854 µm² · Time: 7200 ps
sorter: the score of each entry by date2 entries by date (x) and score in µm²·ns (y); the line is the best score so far, the dashed line par. The table under the chart lists the same numbers.55060065070026 Oct2 Nov9 Novdate enteredscore (µm²·ns) · lower is betterpar: sorter_ins, 701.9 µm²·nsPARthe best score so farsorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 701.9 µm²·ns · Area: 85.687 µm² · Time: 8192 pskestrel-golf · submission · 2026-11-10 · Score: 538.9 µm²·ns · Area: 74.854 µm² · Time: 7200 ps
  • submission
  • proved reference
  • the best score so far
  • par
Score = area × time: the ASAP7 cell area of the scored netlist in µm² (flip-flops included) times the latency in cycles × the register-to-register clock period 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). The clock period (what score/ppa.py calls the register-to-register period) is the longest path from an input or a flip-flop to an output or a flip-flop (clock-to-Q and setup included), so paths from the inputs and to the outputs count too, not only the paths between two flip-flops. 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.
every entry by date
datedesignkindscore (µm²·ns)area × time
2026-11-03sorter_insproved reference · par701.985.687 µm² × 16 × 0.512 ns
2026-11-10kestrel-golfsubmission538.974.854 µm² × 16 × 0.450 ns

First submission: How to submit

This task

Proving guide

Take N unsigned W-bit values, one per cycle, and give them back in ascending order, one per cycle, duplicates kept, behind a stream handshake: start, then in_valid and in_data in, out_valid and out_data out. out_data is claimed only at the cycles where out_valid = 1, which show the sorted values in order; out_valid is known at every cycle from the release and 0 until the first start. The proof covers every N, W ≥ 1 with N·W < 2^31 and proves the latency the submission declares; the score is taken at N = 8, W = 8.

The design is clocked by clk alone, on its rising edge, with the synchronous reset rst: no asynchronous process, and clk is never read as data. No output may depend combinationally on an input; the claims hold from every power-up value of every register, the first reset included; no construct may create an unknown value, and a register that is never loaded is refused. No operator is banned but run-time / % **, as in every task: comparisons are the task. Any schedule is allowed, and the score prices it: an insertion array, a sorting network behind serial-parallel buffers, a merge structure. No design can finish before 2N - 1 cycles, because the smallest value depends on the last input; the proved reference, an insertion-cell array, takes 2N (16 cycles at the scoring point) for 1288.819 GE.

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.

sorter.sv
module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
portdirectionwidth (bits)
clkinput1
rstinput1
startinput1
in_validinput1
in_datainputW
out_validoutput1
out_dataoutputW

The trusted statement #

A proof must establish the task's trusted statement, the constant SvGolf.Tasks.Sorter.Statement of Spec.lean (module tasks.sorter.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 and its declared latency meet the trusted statement exactly when, for every (N, W) in range, they have all of the properties below. The last four are guarantees the design owes an environment that follows the protocol: after a reset is released, start is raised only while the design is idle, and in_valid is 1, with one input value on in_data, in exactly the N cycles after each start. Lean checks that, together, the properties say exactly what the statement says, nothing less and nothing more (the theorem statement_iff_properties).

PARAMS_IN_RANGE is the range the statement covers, not a property: every other card must hold at each value in it.

PARAMS_IN_RANGErangeThe parameters the statement covers: N, W ≥ 1 and N·W below 2^31.

The statement covers every count N ≥ 1 of values of every width W ≥ 1, as long as N·W stays below 2^31: the parameters are 32-bit ints, and a design that buffers the whole stream declares N·W bits. One proof covers all of them; the design is scored at N = 8, W = 8.

ParamsInRange
/-- The parameters the statement covers: `N, W ≥ 1` and `N·W` below `2^31`. -/
def ParamsInRange (N W : Nat) : Prop :=
  1 ≤ N ∧ 1 ≤ W ∧ N * W < 2 ^ 31
svgolf/tasks/sorter/Properties.lean:27Open in code
INTERFACEExactly these ports, in this order, with these widths; no two declarations share a name.

The module has exactly the input ports clk, rst, start, in_valid (1 bit each) and in_data (W bits) and exactly the output ports out_valid (1 bit) and out_data (W 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. No two declarations of the module (ports or internal signals) share a name, so every port has exactly one declared width.

Interface
/-- Exactly these ports, in this order, with these widths; no two declarations share a name. -/
def Interface (W : Nat) (d : Design2) : Prop :=
  inputPorts d = [("clk", 1), ("rst", 1), ("start", 1), ("in_valid", 1), ("in_data", W)] ∧
    outputPorts d = [("out_valid", 1), ("out_data", W)] ∧ (d.decls.toList.map Decl.name).Nodup
svgolf/tasks/sorter/Properties.lean:31Open in code
CLOCK_DISCIPLINEclk is an input; every process that runs at a clock edge is clocked by clk; no process has an asynchronous reset (rst is synchronous); no process reads clk as data.

The clock is the input clk: every register is clocked by it, no register has an asynchronous reset (rst is synchronous, read inside the clocked processes), and no logic reads clk as a data signal. Together these make one cycle of Lean's model exactly one rising edge of clk in the real circuit: a clock that is gated, derived from logic, tied off or never driven is ruled out. One consequence to know: the registers have to sit in the top module, because connecting clk to a child instance copies it as data.

ClockDiscipline
/-- `clk` is an input; every process that runs at a clock edge is clocked by `clk`; no process
has an asynchronous reset (`rst` is synchronous); no process reads `clk` as data. -/
def ClockDiscipline (d : Design2) : Prop :=
  "clk" ∈ d.inputNames.toList ∧
    ∀ p ∈ d.processes.toList,
      (p.isEdgePhase = true → edgeClock p = some "clk") ∧
      asyncReset p = none ∧
      "clk" ∉ processDataNames p
svgolf/tasks/sorter/Properties.lean:36Open in code
TERMINATESFrom every power-up state, under every schedule and every known stimulus, the run completes.

From every power-up state (every register and variable, 2-state ones included, holding some 0 or 1), whatever order the simulator picks for processes that are ready at the same moment (the schedule), and whatever known values the environment drives on the inputs, simulating the design completes: every clock 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 guarantees below their teeth: they are about completed runs, and a design with no completed run would satisfy them without doing anything.

Terminates
/-- From every power-up state, under every schedule and every known stimulus, the run completes. -/
def Terminates (d : Design2) : Prop :=
  ∀ st0, PowerUp d st0 → ∀ (σ : ScheduleOracle) (stim : List SvState), KnownStim d stim →
    ∃ tr, RunsAt d σ st0 stim tr
svgolf/tasks/sorter/Properties.lean:45Open in code
LATENCY_AT_LEAST_ONEThe declared latency is at least one cycle.

Besides the design, a submission declares its latency: the number of cycles it may take to answer a start, as a function of the parameters. It must be at least one cycle. The checker pins its value at the scoring point, and the score uses it (time = latency × clock period), so declaring a larger latency than needed only costs score.

LatencyAtLeastOne
/-- The declared latency is at least one cycle. -/
def LatencyAtLeastOne (lat : Nat) : Prop :=
  1 ≤ lat
svgolf/tasks/sorter/Properties.lean:50Open in code
MOORE_OUTPUTSNo combinational path leads from an input port, rst included, to an output port (MooreOutDep with nothing exempt, txtask-v2 rule 1): out_valid and out_data are functions of the registers, so every snapshot is what the wires show for the whole next period.

No combinational path leads from any input, rst included, to out_valid and out_data: the outputs are functions of the registers only. The proof reads the outputs in the snapshot just after a clock edge, with that cycle's inputs still applied; on the wire the inputs change before the next edge. Without this rule an output that reads an input directly would be proved on one value and seen on another; an output gated by rst could hide a transaction's last value from a consumer when a reset follows (txtask-v2 rule 1).

MooreOutputs
/-- No combinational path leads from an input port, `rst` included, to an output port
(`MooreOutDep` with nothing exempt, txtask-v2 rule 1): `out_valid` and `out_data` are functions of
the registers, so every snapshot is what the wires show for the whole next period. -/
def MooreOutputs (d : Design2) : Prop :=
  MooreOutDep d []
svgolf/tasks/sorter/Properties.lean:54Open in code
NO_X_CREATINGNo construct of the design can create an x or z from known operands (XSafe, txtask-v2 rule 3): with the power-up rule, every value of every run is known.

No construct of the design can make an unknown value out of known ones: no run-time / or % except by a nonzero constant, no ** that could be x, no run-time index that can leave its range, no slice beyond its operand, no bitwise or equality operator on operands of different widths, no x or z literal outside a casez/casex pattern. Together with the power-up rule, every value the design computes in Lean's model is then a known 0 or 1, so every if, case and ?: decides on a known value, where the hardware decides too (txtask-v2 rule 3).

NoXCreating
/-- No construct of the design can create an `x` or `z` from known operands (`XSafe`, txtask-v2
rule 3): with the power-up rule, every value of every run is known. -/
def NoXCreating (d : Design2) : Prop :=
  XSafe d
svgolf/tasks/sorter/Properties.lean:68Open in code
OUT_VALID_KNOWNout_valid is a known bit at every cycle from the release.

As long as the environment follows the protocol, out_valid is a known bit, 0 or 1, in every cycle from the release of the reset on; never x.

OutValidKnown
/-- `out_valid` is a known bit at every cycle from the release. -/
def OutValidKnown (N W : Nat) (d : Design2) : Prop :=
  UnderProtocol N W d fun _ tr c1 h =>
    ∀ c, c1 ≤ c → c < h → ∃ b, TraceBit tr c "out_valid" b
svgolf/tasks/sorter/Properties.lean:73Open in code
SILENT_BEFORE_FIRST_STARTout_valid is 0 at every cycle from the release up to the first start.

As long as the environment follows the protocol, out_valid is 0 in every cycle after the release of the reset and before the first start: nothing comes out before there is anything to sort, and nothing left over from before the reset comes out.

SilentBeforeFirstStart
/-- `out_valid` is 0 at every cycle from the release up to the first start. -/
def SilentBeforeFirstStart (N W : Nat) (d : Design2) : Prop :=
  UnderProtocol N W d fun stim tr c1 h =>
    ∀ c, c1 ≤ c → c < h → (∀ s, c1 ≤ s → s ≤ c → ¬ StimBit stim s "start" true) →
      TraceBit tr c "out_valid" false
svgolf/tasks/sorter/Properties.lean:78Open in code
EMITS_SORTEDFrom each start to the next, the values shown on out_data while out_valid is 1 are, in order, the transaction's input values sorted ascending.

As long as the environment follows the protocol, for every start whose latency window has passed, the values on out_data in the cycles where out_valid is 1, from that start up to the next one, are, in order, exactly the N input values of the transaction sorted ascending as unsigned numbers, duplicates kept. So exactly N values come out; gaps between them are allowed, and out_data may hold anything while out_valid is 0.

EmitsSorted
/-- From each start to the next, the values shown on `out_data` while `out_valid` is 1 are, in
order, the transaction's input values sorted ascending. -/
def EmitsSorted (N W lat : Nat) (d : Design2) : Prop :=
  UnderProtocol N W d fun stim tr c1 h =>
    ∀ s xs e, s + lat < h → Transaction N W stim c1 h s xs e →
      ∃ obs : List (Bool × BitVec W), obs.length = e - s ∧ task.Shows (N, W) tr s obs ∧
        task.emitted (N, W) obs = sortAsc xs
svgolf/tasks/sorter/Properties.lean:95Open in code
SILENT_AFTER_LATENCYFrom each start to the next, out_valid is 0 at every cycle more than lat cycles after the start.

As long as the environment follows the protocol, after every start, out_valid is 0 in every cycle more than lat cycles later, up to the next start (the cycle in which start is sampled is cycle 0). With EMITS_SORTED, this says that all N values come out within the declared latency.

SilentAfterLatency
/-- From each start to the next, `out_valid` is 0 at every cycle more than `lat` cycles after
the start. -/
def SilentAfterLatency (N W lat : Nat) (d : Design2) : Prop :=
  UnderProtocol N W d fun stim tr c1 h =>
    ∀ s xs e, s + lat < h → Transaction N W stim c1 h s xs e →
      ∀ c, s + lat < c → c < e → TraceBit tr c "out_valid" false
svgolf/tasks/sorter/Properties.lean:103Open 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

sortAscSpec.leanInsertion sort, ascending as unsigned numbers, duplicates kept: the function of a transaction.
sortAsc
/-- Insertion sort, ascending, unsigned: `List.insertionSort (· ≤ ·)` (C8), written out here
because the trusted text imports no Mathlib (structural recursion: the kernel evaluates it). -/
def sortAsc {W : Nat} : List (BitVec W) → List (BitVec W)
  | [] => []
  | a :: as => insertAsc a (sortAsc as)
svgolf/tasks/sorter/Spec.lean:58Open in code
insertAscSpec.leanInserts a value into an ascending list, before the first element it is at most.
insertAsc
/-- Insert `a` into an ascending list (unsigned order), before the first element it is `≤` to. -/
def insertAsc {W : Nat} (a : BitVec W) : List (BitVec W) → List (BitVec W)
  | [] => [a]
  | b :: bs => if a.toNat ≤ b.toNat then a :: b :: bs else b :: insertAsc a bs
svgolf/tasks/sorter/Spec.lean:53Open in code
StatementSpec.leanThe trusted challenge statement that these properties restate, part by part.
Statement
/-- **The challenge statement**, for the two-parameter design family `sem N W` and the latency
function `lat N W`. -/
abbrev Statement (sem : Nat → Nat → LeanModels.Sv.Design2) (lat : Nat → Nat → Nat) : Prop :=
  task.StatementV2 (fun p => sem p.1 p.2) (fun p => lat p.1 p.2)
svgolf/tasks/sorter/Spec.lean:78Open in code
taskSpec.leanThe task as data: the parameter range, the port names and widths, and the function of a transaction.
task
/-- **The task** (C8). -/
def task : StreamTask Params where
  inRange p := 1 ≤ p.1 ∧ 1 ≤ p.2 ∧ p.1 * p.2 < 2 ^ 31
  clk := "clk"
  rst := "rst"
  start := "start"
  inValid := "in_valid"
  inData := "in_data"
  outValid := "out_valid"
  outData := "out_data"
  width p := p.2
  count p := p.1
  spec _ xs := sortAsc xs
svgolf/tasks/sorter/Spec.lean:64Open in code

Helpers in Properties.lean (proved, not trusted)

TransactionProperties.leanTransaction N W stim c1 h s xs e: s is a start after the release c1, xs are the N values on in_data in the cycles after it, and e is the next start, or the horizon h if there is none before it.
Transaction
/-- `Transaction N W stim c1 h s xs e`: `s` is a start after the release `c1`, `xs` are the `N`
values on `in_data` in the cycles after it, and `e` is the next start, or the horizon `h` if
there is none before it. -/
def Transaction (N W : Nat) (stim : List SvState) (c1 h s : Nat) (xs : List (BitVec W))
    (e : Nat) : Prop :=
  c1 ≤ s ∧ StimBit stim s "start" true ∧ xs.length = N ∧
    (∀ j v, xs[j]? = some v → ∃ en, stim[s + 1 + j]? = some en ∧
      SvState.lookup en "in_data" = some (LVec.ofBitVec v)) ∧
    s < e ∧ e ≤ h ∧ (∀ s', s < s' → s' < e → ¬ StimBit stim s' "start" true) ∧
    (e < h → StimBit stim e "start" true)
svgolf/tasks/sorter/Properties.lean:84Open in code
UnderProtocolProperties.leanUnderProtocol d G: in every completed run from every power-up state on every known stimulus, from every release of the reset, up to every later cycle h before which the environment followed the protocol (the task's Rely), G holds up to h. Every guarantee is stated in this frame, so a protocol violation can only void claims about later cycles.
UnderProtocol
/-- `G` holds in every completed run from every power-up state on every known stimulus, from every
release `c1` of the reset, up to every horizon `h` before which the environment kept the protocol
(`StreamTask.Rely`). -/
def UnderProtocol (N W : Nat) (d : Design2)
    (G : List SvState → List SvState → Nat → Nat → Prop) : Prop :=
  ModelsPU d fun stim tr =>
    ∀ c1 h, Released "rst" stim c1 h → task.Rely (N, W) stim tr c1 h → G stim tr c1 h
svgolf/tasks/sorter/Properties.lean:60Open in code

The shared trusted base

StreamTask.RelyTaskSeq.leanThe environment's side of the protocol, up to a horizon: start, in_valid and in_data are driven with known values in every cycle, start is 1 only while the design is idle, and in_valid is 1 exactly in the N cycles after each start.
Rely
/-- **The rely, up to the horizon `h`**: every entry from the release drives
`start`, `in_valid` and `in_data` with known values; `start` only when `Idle`;
`in_valid` is 1 exactly at the `count p` entries after each start. -/
def Rely (p : P) (stim tr : List SvState) (c1 h : Nat) : Prop :=
  ∀ c, c1 ≤ c → c < h →
    (∃ b, StimBit stim c t.start b) ∧
    (∃ e v, stim[c]? = some e ∧ t.DataIs p e t.inData v) ∧
    (StimBit stim c t.start true → t.Idle p stim tr c1 c) ∧
    (∀ s, c1 ≤ s → s < c → c ≤ s + t.count p → StimBit stim s t.start true →
      StimBit stim c t.inValid true) ∧
    ((∀ s, c1 ≤ s → s < c → c ≤ s + t.count p → ¬ StimBit stim s t.start true) →
      StimBit stim c t.inValid false)
svgolf/SvGolf/TaskSeq.lean:607Open in code
StreamTask.IdleTaskSeq.leanThe design is idle: every start since the release has had all N of its values emitted.
Idle
/-- **C2 for streams, `Idle`**: from the release `c1`, every start before `c`
has had all its `count p` outputs emitted before `c`. -/
def Idle (p : P) (stim tr : List SvState) (c1 c : Nat) : Prop :=
  ∀ s, c1 ≤ s → s < c → StimBit stim s t.start true →
    ∃ obs : List (t.Obs p), s + obs.length ≤ c ∧ t.Shows p tr s obs ∧
      (t.emitted p obs).length = t.count p
svgolf/SvGolf/TaskSeq.lean:600Open in code
StreamTask.ShowsTaskSeq.leanShows tr s obs: the snapshots from cycle s on show the observations obs, one per cycle: out_valid as a known bit, and out_data as a known value where out_valid is 1.
Shows
/-- The snapshots `a, a+1, ...` show the observations `obs`: `out_valid` known,
and `out_data` known where valid. -/
def Shows (p : P) (tr : List SvState) (a : Nat) (obs : List (t.Obs p)) : Prop :=
  ∀ k o, obs[k]? = some o → ∃ st, tr[a + k]? = some st ∧ BitIs st t.outValid o.1 ∧
    (o.1 = true → t.DataIs p st t.outData o.2)
svgolf/SvGolf/TaskSeq.lean:590Open in code
StreamTask.emittedTaskSeq.leanThe values emitted in a list of observations: the out_data of the cycles with out_valid = 1, in order.
emitted
/-- The values emitted in a list of observations, in order. -/
def emitted (p : P) (obs : List (t.Obs p)) : List (BitVec (t.width p)) :=
  (obs.filter (·.1)).map (·.2)
svgolf/SvGolf/TaskSeq.lean:596Open in code
StreamTask.GuarTaskSeq.leanThe trusted guarantee, one conjunction; OUT_VALID_KNOWN, SILENT_BEFORE_FIRST_START, EMITS_SORTED and SILENT_AFTER_LATENCY are its parts.
Guar
/-- **The guarantee, up to the horizon `h`**: `out_valid` is known at every
cycle from the release, and 0 before the first start; for every start `s`
whose latency window ends before `h`, with input values `xs` (the `in_data`
of the `count p` entries after it), the observations from `s` to the next
start (or to `h`) emit exactly `spec xs`, none after `s + lat`. -/
def Guar (p : P) (lat : Nat) (stim tr : List SvState) (c1 h : Nat) : Prop :=
  (∀ c, c1 ≤ c → c < h → ∃ b, TraceBit tr c t.outValid b) ∧
  (∀ c, c1 ≤ c → c < h → (∀ s, c1 ≤ s → s ≤ c → ¬ StimBit stim s t.start true) →
    TraceBit tr c t.outValid false) ∧
  ∀ s (xs : List (BitVec (t.width p))), c1 ≤ s → s + lat < h → StimBit stim s t.start true →
    xs.length = t.count p →
    (∀ j v, xs[j]? = some v → ∃ e, stim[s + 1 + j]? = some e ∧ t.DataIs p e t.inData v) →
    ∀ e, s < e → e ≤ h → (∀ s', s < s' → s' < e → ¬ StimBit stim s' t.start true) →
      (e < h → StimBit stim e t.start true) →
      ∃ obs : List (t.Obs p), obs.length = e - s ∧ t.Shows p tr s obs ∧
        t.emitted p obs = t.spec p xs ∧ ∀ k o, obs[k]? = some o → lat < k → o.1 = false
svgolf/SvGolf/TaskSeq.lean:620Open in code
ReleasedTaskSeq.leanReleased rst stim c1 h: rst was 1 in the cycle before c1 and is 0 in every cycle from c1 up to h. Claims start at every release, so nothing may survive a reset.
Released
/-- **C1**: `c1` is a release cycle of the synchronous reset `rst` within the
first `h` entries: the entry before `c1` asserts it, every entry in `[c1, h)`
deasserts it. -/
def Released (rst : String) (stim : List SvState) (c1 h : Nat) : Prop :=
  0 < c1 ∧ StimBit stim (c1 - 1) rst true ∧ ∀ c, c1 ≤ c → c < h → StimBit stim c rst false
svgolf/SvGolf/TaskSeq.lean:424Open in code
TraceBitTaskSeq.leanTraceBit tr c n b: in cycle c the design shows the 1-bit signal n as the known bit b.
TraceBit
/-- The snapshot `c` exists and binds `n` to `b`. -/
def TraceBit (tr : List SvState) (c : Nat) (n : String) (b : Bool) : Prop :=
  ∃ st, tr[c]? = some st ∧ BitIs st n b
svgolf/SvGolf/TaskSeq.lean:420Open in code
StimBitTaskSeq.leanStimBit stim c n b: in cycle c the environment drives the 1-bit input n with the known bit b.
StimBit
/-- The stimulus entry `c` exists and binds `n` to `b`. -/
def StimBit (stim : List SvState) (c : Nat) (n : String) (b : Bool) : Prop :=
  ∃ e, stim[c]? = some e ∧ BitIs e n b
svgolf/SvGolf/TaskSeq.lean:416Open in code
ClockedByTaskSeq.leanThe trusted clock discipline that CLOCK_DISCIPLINE restates.
ClockedBy
/-- **The clock discipline** (replaces `Unclocked` for a task with a clock):
`k` is an input port of `d`; every edge-phase process (the processes ls-sv
runs at the clock edge, `Process2.isEdgePhase`) is clocked by `k`; an edge
process with an asynchronous reset uses the reset port `rst`; and no process
reads `k` as data. Under it, "one stimulus entry is one rising edge of `k`"
is the protocol, so an undriven, tied, derived or gated clock cannot occur. -/
def ClockedBy (k : String) (rst : Option String) (d : Design2) : Prop :=
  k ∈ d.inputNames.toList ∧
  ∀ p ∈ d.processes.toList,
    (p.isEdgePhase = true → edgeClock p = some k) ∧
    (∀ r, asyncReset p = some r → rst = some r) ∧
    k ∉ processDataNames p
svgolf/SvGolf/TaskSeq.lean:255Open in code
edgeClockTaskSeq.leanThe clock of a clocked process (always_ff @(posedge c) and the like); none for any other process.
edgeClock
/-- The clock of an edge process (`always_ff @(posedge c)`, `always
@(posedge c)`, `always_ff @(posedge c or negedge rn)`, `always_ff @(posedge c
or posedge r)`); `none` for every other process. -/
def edgeClock : Process2 → Option String
  | .alwaysFF c _ | .alwaysPlain c _ | .alwaysFFR c _ _ _ => some c
  | _ => none
svgolf/SvGolf/TaskSeq.lean:240Open in code
asyncResetTaskSeq.leanThe asynchronous reset of a clocked process (the rn of posedge c or negedge rn), if it has one.
asyncReset
/-- The asynchronous reset of an edge process (the `rn` of `posedge c or
negedge rn`, or the `r` of `posedge c or posedge r`), if it has one. Both
polarities name their reset, so the clock discipline below holds an
active-high reset to the task's reset port too. -/
def asyncReset : Process2 → Option String
  | .alwaysFFR _ r _ _ => some r
  | _ => none
svgolf/SvGolf/TaskSeq.lean:247Open in code
processDataNamesTaskSeq.leanEvery signal a process reads or writes as data: its body, or its assignment. The clock and reset in the event control do not count.
processDataNames
/-- The names a process mentions as DATA: everything in its body (or its
target and value). The clock and reset names in an edge process's event
control are not data. -/
def processDataNames : Process2 → List String
  | .alwaysFF _ b | .alwaysPlain _ b | .alwaysFFR _ _ b _ | .alwaysComb b => stmtNames b
  | .assign t e => lhsNames t ++ exprNames e
  | .unsupported _ _ => []
svgolf/SvGolf/TaskSeq.lean:232Open 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
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
MooreOutDepTaskSeq.leanThe trusted rule 1 of txtask-v2 that MOORE_OUTPUTS restates: a set of signals that holds every input port outside the exempt list (here the list is empty: every input port, rst included), is closed along every combinational dependency and holds no output port.
MooreOutDep
/-- **Rule 1, Moore outputs**: no combinational path leads from an input port outside `exempt`
to an output port. `S` is a set of signals that contains every such input, is closed along the
combinational dependencies (if an assignment depends on a signal in `S`, every signal it writes
is in `S`) and contains no output port. Every v2 statement exempts nothing (`SeqTask`'s from the
start; `TxTask`'s and `StreamTask`'s since 2026-11-09, see `TxTask.SatisfiedAtV2`). -/
def MooreOutDep (d : Design2) (exempt : List String) : Prop :=
  ∃ S : String → Prop,
    (∀ n ∈ d.inputNames.toList, n ∉ exempt → S n) ∧
    (∀ e ∈ combDeps d, (∃ r ∈ e.2, S r) → S e.1) ∧
    ∀ o ∈ d.outputNames.toList, ¬ S o
svgolf/SvGolf/TaskSeq.lean:889Open in code
combDepsTaskSeq.leanThe combinational dependencies of a design, by assignment: for each always_comb or continuous assign, every signal a write targets and every signal its value, its indices or an enclosing condition reads. A clocked process contributes none: its writes end a combinational path at the clock edge.
combDeps
/-- Every combinational dependency of a design, by assignment. -/
def combDeps (d : Design2) : List DepEdge := d.processes.toList.flatMap processDeps
svgolf/SvGolf/TaskSeq.lean:886Open in code
ModelsPUTaskSeq.leanModelsPU d P: from every power-up state, under every schedule, on every known stimulus, every completed run of d satisfies P. It replaces txtask-v1's runs from Lean's own start state, where an unreset register is x: an unreset register is a 0 or 1 nobody knows, so the claims must hold for every value it can have.
ModelsPU
/-- **Rule 2's judgment**: from every power-up state, under every schedule, on every known
stimulus, every completed run satisfies `P` (v1's `⊨₂`, whose runs start at `initState2 d`, with
the start quantified over the power-up states). -/
def ModelsPU (d : Design2) (P : List SvState → List SvState → Prop) : Prop :=
  ∀ st0, PowerUp d st0 → ∀ (σ : ScheduleOracle) (stim tr : List SvState), KnownStim d stim →
    RunsAt d σ st0 stim tr → P stim tr
svgolf/SvGolf/TaskSeq.lean:779Open in code
PowerUpTaskSeq.leanPowerUp d st: st binds every declared signal of d, in declaration order, to a value of its declared width whose every bit is 0 or 1 (2-state declarations included, initializers ignored).
PowerUp
/-- **A power-up state** of `d`: every declaration, in declaration order, bound to a value of its
declared width whose every bit is `0` or `1`. 2-state declarations are included (ls-sv's
`initState2` starts them at `0`, the standard's 2-state initial value; a flip-flop powers up 0 or
1), and declaration initializers play no part (the clocked source gate refuses them). -/
def PowerUp (d : Design2) (st : SvState) : Prop :=
  st.map Prod.fst = d.decls.toList.map Decl.name ∧
    ∀ b ∈ st.zip d.decls.toList, b.1.2.width = b.2.width ∧ b.1.2.allKnown = true
svgolf/SvGolf/TaskSeq.lean:725Open in code
KnownStimTaskSeq.leanKnownStim d stim: every stimulus entry binds each input port it drives to a value of the port's width whose every bit is 0 or 1. An x on an input is a value the environment does not know; each of its resolutions is a known entry.
KnownStim
/-- Every entry of a stimulus is known. -/
def KnownStim (d : Design2) (stim : List SvState) : Prop := ∀ e ∈ stim, KnownEntry d e
svgolf/SvGolf/TaskSeq.lean:755Open in code
KnownEntryTaskSeq.leanKnownEntry d e: every input port the entry e binds holds a known value of its declared width.
KnownEntry
/-- **A known stimulus entry**: every input port it binds holds a value of the port's declared
width whose every bit is `0` or `1`. An `x` on an input is a value the environment does not
know, and each of its resolutions is a known entry, so quantifying over known entries is the
formal reading of an `x` input. An input the entry does not bind keeps its value
(`applyInputs2`). -/
def KnownEntry (d : Design2) (e : SvState) : Prop :=
  ∀ n ∈ d.inputNames.toList,
    ((SvState.lookup e n).all fun v => v.allKnown && sigWidth d n == some v.width) = true
svgolf/SvGolf/TaskSeq.lean:742Open in code
sigWidthTaskSeq.leanThe declared width of a signal (its first declaration's).
sigWidth
/-- The declared width of the signal `n` (its first declaration's; `Design2.declWidth` of ls-sv's
comb layer, restated here so that this file imports no proof layer). -/
def sigWidth (d : Design2) (n : String) : Option Nat :=
  (d.decls.toList.find? fun dc => dc.name == n).map Decl.width
svgolf/SvGolf/TaskSeq.lean:737Open in code
RunsAtTaskSeq.leanRunsAt d σ st0 stim tr: simulating d from the state st0 under the schedule σ on the stimulus stim completes, with the trace tr.
RunsAt
/-- Some fuel completes the run of `d` from `st0` under `σ` on `stim` with the trace `tr` (the
`Runs2` of `run2At`). -/
def RunsAt (d : Design2) (σ : ScheduleOracle) (st0 : SvState) (stim tr : List SvState) : Prop :=
  ∃ fuel, run2At d σ fuel st0 stim = .ok tr
svgolf/SvGolf/TaskSeq.lean:774Open in code
run2AtTaskSeq.leanLean's run of a design (ls-sv's run2: the same clock cycles and checks) started from a given state instead of its own start state.
run2At
/-- **`run2` from the state `st0`** in place of `initState2 d`: the same cycles (`runFrom2`), the
same qualified-case validation (`run2_eq_run2At`: `run2` is `run2At` from `initState2 d`). -/
def run2At (d : Design2) (σ : ScheduleOracle) (fuel : Nat) (st0 : SvState)
    (stim : List SvState) : Res (List SvState) := do
  let tr ← runFrom2 d σ fuel st0 0 stim
  if d.processes.toList.any Process2.hasQualifiedCase then
    validateTraceChecks2 fuel d tr
  return tr
svgolf/SvGolf/TaskSeq.lean:761Open in code
TerminatesPUTaskSeq.leanThe trusted termination conjunct of txtask-v2 that TERMINATES restates: from every power-up state, under every schedule, every known stimulus completes.
TerminatesPU
/-- **Non-vacuity of `ModelsPU`**: from every power-up state, under every schedule, every known
stimulus completes (v1's `Terminates2` from the power-up states: a design that settles from the
x start but oscillates from a concrete one fails it). -/
def TerminatesPU (d : Design2) : Prop :=
  ∀ st0, PowerUp d st0 → ∀ (σ : ScheduleOracle) (stim : List SvState), KnownStim d stim →
    ∃ tr, RunsAt d σ st0 stim tr
svgolf/SvGolf/TaskSeq.lean:786Open in code
XSafeTaskSeq.leanThe trusted rule 3 of txtask-v2 that NO_X_CREATING restates: every process passes the structural check xsafeB.
XSafe
/-- **Rule 3**: no construct of `d` can create an `x` or a `z` from known operands. -/
def XSafe (d : Design2) : Prop := xsafeB d = true
svgolf/SvGolf/TaskSeq.lean:1085Open in code
xsafeBTaskSeq.leanThe structural check of rule 3, a Boolean function of the design's text and declared widths: every expression of every process has a rule-3 width (xsWidth), and every case pattern is an admitted expression or a casez/casex literal.
xsafeB
/-- **Rule 3, decided**: no process of `d` has a construct that can create an `x` from known
operands. -/
def xsafeB (d : Design2) : Bool := d.processes.toList.all (xsProc d)
svgolf/SvGolf/TaskSeq.lean:1081Open in code
xsWidthTaskSeq.leanThe width of an expression's value when no construct in it can create an x from known operands, and none otherwise: literals without x/z digits, declared signals, slices in range, run-time indices whose every value is in range, equal widths for bitwise and equality operators and for the two arms of ?:, and the operator rules of binW.
xsWidth
/-- **Rule 3 for an expression**: `some w` when no construct in `e` can create an `x` from known
operands, `w` being the width of its value on a state that binds every signal at its declared
width; `none` otherwise. -/
def xsWidth (d : Design2) : Expr2 → Option Nat
  | .lit v => if v.allKnown then some v.width else none
  | .ident n => sigWidth d n
  | .unary .lnot a => (xsWidth d a).map fun _ => 1
  | .unary _ a => xsWidth d a
  | .resizeSigned w a => (xsWidth d a).map fun _ => w
  | .squash2 a => xsWidth d a
  | .binary op l r => binW op l r (xsWidth d l) (xsWidth d r)
  | .scmp op l r => if scmpOp op then (do let _ ← xsWidth d l; let _ ← xsWidth d r; pure 1) else none
  | .logical _ l r => do let _ ← xsWidth d l; let _ ← xsWidth d r; pure 1
  | .ternary c t f => do
      let _ ← xsWidth d c; let a ← xsWidth d t; let b ← xsWidth d f; if a = b then pure a else none
  | .concat parts => xsWidthList d parts.toList
  | .slice b lo w => do let a ← xsWidth d b; if lo + w ≤ a then pure w else none
  | .index b i ew => do
      let a ← xsWidth d b; let k ← xsWidth d i
      if unsignedIdx d i = true ∧ 2 ^ k * ew ≤ a then pure ew else none
  | .repl n a => (xsWidth d a).map (· * n)
  | .reduce _ a => (xsWidth d a).map fun _ => 1
  | .resize w a => (xsWidth d a).map fun _ => w
  | .unsupported _ _ => none
termination_by structural e => e
svgolf/SvGolf/TaskSeq.lean:987Open in code
binWTaskSeq.leanRule 3 at a binary operator: / and % only by a nonzero constant, ** with a signed exponent only on a nonzero constant base, &, |, ^, ==, !=, ==?, !=? only on equal widths; every other operator is known on known operands.
binW
/-- Rule 3 at a binary operator, from its operands `l`, `r` and their rule-3 widths `wl`, `wr`:
the width of the result, or `none` if the operator can create an `x` from known operands. -/
def binW (op : BinOp) (l r : Expr2) (wl wr : Option Nat) : Option Nat :=
  match op with
  | .add | .sub | .mul => do let a ← wl; let b ← wr; pure (max a b)
  | .div | .sdiv | .rem | .srem => do
      let a ← wl; let b ← wr; if constNZ r then pure (max a b) else none
  | .pow _ se => do let a ← wl; let _ ← wr; if !se || constNZ l then pure a else none
  | .shl _ | .shr _ | .ashl _ | .ashr _ => do let a ← wl; let _ ← wr; pure a
  | .and | .or | .xor => do let a ← wl; let b ← wr; if a = b then pure a else none
  | .eq | .ne => do let a ← wl; let b ← wr; if a = b then pure 1 else none
  | .wildEq | .wildNe => do let a ← wl; let b ← wr; if a = b then pure 1 else none
  | .caseEq | .caseNe | .casez | .casex => do let _ ← wl; let _ ← wr; pure 1
  | .land | .lor | .lt | .le | .gt | .ge | .slt | .sle | .sgt | .sge => do
      let _ ← wl; let _ ← wr; pure 1
svgolf/SvGolf/TaskSeq.lean:957Open 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.

Rejected at the proof

These pass every static check. The proof that comes with each one does not compile, or does not prove the statement: a design that is wrong somewhere in the task's range (or has other ports) has no proof at all, and a proof that leaves a goal unproved is never accepted.

  • early_valid.sv (attack, stopped at solution): The valid token enters with start, one cycle before the first value: one output too many (the padding 0).

    the design, with its licence and provenance notices 
    // Attack for task sorter (tests/expected.json, `attacks`; PLAN4.md Gate 5, the sorter): the proved
// reference tasks/sorter/reference/sorter_ins.sv with ONE change (1 site), a correct-looking design
// that is wrong for some N, W: the valid token enters with the start (`tok[N-1] <= in_valid | start`), one cycle before the first value.
// Wrong: out_valid rises one cycle early, at the snapshot N after the start, and stays up N + 1 cycles: one value too many (the padding 0 in cell 0), every N.
// Every check up to the proof passes it; the reference's proof (reference/sorter_ins.lean) must FAIL on it.
// Derived from andrewpeck/cell-sort (MIT, cfc46709; the reference's header has the provenance and changes):
//
// MIT License
//
// Copyright (c) 2024-2025 Andrew Peck
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

`timescale 1ns / 1ps
`default_nettype none

module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
  logic [N*W-1:0] data;  // cell k's value: data[k*W +: W]; cell N-1 is the top ("best") cell
  logic [N-1:0]   tok;   // cell k's valid token

  // cells 0 .. N-2: upstream's unit_cell; the upper neighbour is cell k+1
  for (genvar k = 0; k < N-1; k++) begin : gen_cell
    always_ff @(posedge clk) begin
      if (in_valid) begin
        if (in_data > data[(k+1)*W +: W])         // the neighbour is pushed: take its value
          data[k*W +: W] <= data[(k+1)*W +: W];
        else if (in_data > data[k*W +: W])        // the input beats this cell's value
          data[k*W +: W] <= in_data;
      end else
        data[k*W +: W] <= data[(k+1)*W +: W];     // drain: shift down
      tok[k] <= tok[k+1];
      if (rst) begin
        data[k*W +: W] <= '0;
        tok[k] <= 1'b0;
      end
    end
  end

  // the top cell N-1: never pushed into (upstream's push[DEPTH] = 0); drains in the empty value 0
  always_ff @(posedge clk) begin
    if (in_valid) begin
      if (in_data > data[(N-1)*W +: W])
        data[(N-1)*W +: W] <= in_data;
    end else
      data[(N-1)*W +: W] <= '0;
    tok[N-1] <= in_valid | start;
    if (rst) begin
      data[(N-1)*W +: W] <= '0;
      tok[N-1] <= 1'b0;
    end
  end

  // the streaming output: cell 0 and its token, registered
  always_ff @(posedge clk) begin
    out_valid <= tok[0];
    out_data  <= data[0 +: W];
    if (rst) out_valid <= 1'b0;
  end
endmodule

  • missing_else.sv (attack, stopped at solution): A cell's second test lost its else: when the input beats both its neighbour and its own value, it is copied into several cells and the neighbour's value is lost.

    the design, with its licence and provenance notices 
    // Attack for task sorter (tests/expected.json, `attacks`; PLAN4.md Gate 5, the sorter): the proved
// reference tasks/sorter/reference/sorter_ins.sv with ONE change (1 site), a correct-looking design
// that is wrong for some N, W: the cell's second test lost its `else`: when the input beats both the upper neighbour and the cell's own value, both writes fire and the later one (the input) wins.
// Wrong: a value larger than two stored ones is copied into several cells and the neighbour's value is lost (N >= 2); right at N = 1.
// Every check up to the proof passes it; the reference's proof (reference/sorter_ins.lean) must FAIL on it.
// Derived from andrewpeck/cell-sort (MIT, cfc46709; the reference's header has the provenance and changes):
//
// MIT License
//
// Copyright (c) 2024-2025 Andrew Peck
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

`timescale 1ns / 1ps
`default_nettype none

module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
  logic [N*W-1:0] data;  // cell k's value: data[k*W +: W]; cell N-1 is the top ("best") cell
  logic [N-1:0]   tok;   // cell k's valid token

  // cells 0 .. N-2: upstream's unit_cell; the upper neighbour is cell k+1
  for (genvar k = 0; k < N-1; k++) begin : gen_cell
    always_ff @(posedge clk) begin
      if (in_valid) begin
        if (in_data > data[(k+1)*W +: W])         // the neighbour is pushed: take its value
          data[k*W +: W] <= data[(k+1)*W +: W];
        if (in_data > data[k*W +: W])        // the input beats this cell's value
          data[k*W +: W] <= in_data;
      end else
        data[k*W +: W] <= data[(k+1)*W +: W];     // drain: shift down
      tok[k] <= tok[k+1];
      if (rst) begin
        data[k*W +: W] <= '0;
        tok[k] <= 1'b0;
      end
    end
  end

  // the top cell N-1: never pushed into (upstream's push[DEPTH] = 0); drains in the empty value 0
  always_ff @(posedge clk) begin
    if (in_valid) begin
      if (in_data > data[(N-1)*W +: W])
        data[(N-1)*W +: W] <= in_data;
    end else
      data[(N-1)*W +: W] <= '0;
    tok[N-1] <= in_valid;
    if (rst) begin
      data[(N-1)*W +: W] <= '0;
      tok[N-1] <= 1'b0;
    end
  end

  // the streaming output: cell 0 and its token, registered
  always_ff @(posedge clk) begin
    out_valid <= tok[0];
    out_data  <= data[0 +: W];
    if (rst) out_valid <= 1'b0;
  end
endmodule

  • push_own_value.sv (attack, stopped at solution): The neighbour-push test compares the input with the cell's own value instead of its upper neighbour's, so the input is never stored below the top cell.

    the design, with its licence and provenance notices 
    // Attack for task sorter (tests/expected.json, `attacks`; PLAN4.md Gate 5, the sorter): the proved
// reference tasks/sorter/reference/sorter_ins.sv with ONE change (1 site), a correct-looking design
// that is wrong for some N, W: the neighbour-push test compares the input with the cell's OWN value instead of its upper neighbour's.
// Wrong: a cell takes its neighbour's value whenever the input beats its own value, so the input itself is never stored below the top cell (N >= 2); right at N = 1.
// Every check up to the proof passes it; the reference's proof (reference/sorter_ins.lean) must FAIL on it.
// Derived from andrewpeck/cell-sort (MIT, cfc46709; the reference's header has the provenance and changes):
//
// MIT License
//
// Copyright (c) 2024-2025 Andrew Peck
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

`timescale 1ns / 1ps
`default_nettype none

module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
  logic [N*W-1:0] data;  // cell k's value: data[k*W +: W]; cell N-1 is the top ("best") cell
  logic [N-1:0]   tok;   // cell k's valid token

  // cells 0 .. N-2: upstream's unit_cell; the upper neighbour is cell k+1
  for (genvar k = 0; k < N-1; k++) begin : gen_cell
    always_ff @(posedge clk) begin
      if (in_valid) begin
        if (in_data > data[k*W +: W])         // the neighbour is pushed: take its value
          data[k*W +: W] <= data[(k+1)*W +: W];
        else if (in_data > data[k*W +: W])        // the input beats this cell's value
          data[k*W +: W] <= in_data;
      end else
        data[k*W +: W] <= data[(k+1)*W +: W];     // drain: shift down
      tok[k] <= tok[k+1];
      if (rst) begin
        data[k*W +: W] <= '0;
        tok[k] <= 1'b0;
      end
    end
  end

  // the top cell N-1: never pushed into (upstream's push[DEPTH] = 0); drains in the empty value 0
  always_ff @(posedge clk) begin
    if (in_valid) begin
      if (in_data > data[(N-1)*W +: W])
        data[(N-1)*W +: W] <= in_data;
    end else
      data[(N-1)*W +: W] <= '0;
    tok[N-1] <= in_valid;
    if (rst) begin
      data[(N-1)*W +: W] <= '0;
      tok[N-1] <= 1'b0;
    end
  end

  // the streaming output: cell 0 and its token, registered
  always_ff @(posedge clk) begin
    out_valid <= tok[0];
    out_data  <= data[0 +: W];
    if (rst) out_valid <= 1'b0;
  end
endmodule

  • reset_keeps_cells.sv (attack, stopped at solution): The reset clears the tokens and the top cell but not the other cells: the first transaction after a reset sorts in whatever they held.

    the design, with its licence and provenance notices 
    // Attack for task sorter (tests/expected.json, `attacks`; PLAN4.md Gate 5, the sorter): the proved
// reference tasks/sorter/reference/sorter_ins.sv with ONE change (1 site), a correct-looking design
// that is wrong for some N, W: the reset clears the tokens and the top cell but not cells 0 .. N-2.
// Wrong: the first transaction after a reset sorts the input together with whatever the cells held (N >= 2; the drain clears them, so later transactions are right); right at N = 1.
// Every check up to the proof passes it; the reference's proof (reference/sorter_ins.lean) must FAIL on it.
// Derived from andrewpeck/cell-sort (MIT, cfc46709; the reference's header has the provenance and changes):
//
// MIT License
//
// Copyright (c) 2024-2025 Andrew Peck
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

`timescale 1ns / 1ps
`default_nettype none

module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
  logic [N*W-1:0] data;  // cell k's value: data[k*W +: W]; cell N-1 is the top ("best") cell
  logic [N-1:0]   tok;   // cell k's valid token

  // cells 0 .. N-2: upstream's unit_cell; the upper neighbour is cell k+1
  for (genvar k = 0; k < N-1; k++) begin : gen_cell
    always_ff @(posedge clk) begin
      if (in_valid) begin
        if (in_data > data[(k+1)*W +: W])         // the neighbour is pushed: take its value
          data[k*W +: W] <= data[(k+1)*W +: W];
        else if (in_data > data[k*W +: W])        // the input beats this cell's value
          data[k*W +: W] <= in_data;
      end else
        data[k*W +: W] <= data[(k+1)*W +: W];     // drain: shift down
      tok[k] <= tok[k+1];
      if (rst) begin
        tok[k] <= 1'b0;
      end
    end
  end

  // the top cell N-1: never pushed into (upstream's push[DEPTH] = 0); drains in the empty value 0
  always_ff @(posedge clk) begin
    if (in_valid) begin
      if (in_data > data[(N-1)*W +: W])
        data[(N-1)*W +: W] <= in_data;
    end else
      data[(N-1)*W +: W] <= '0;
    tok[N-1] <= in_valid;
    if (rst) begin
      data[(N-1)*W +: W] <= '0;
      tok[N-1] <= 1'b0;
    end
  end

  // the streaming output: cell 0 and its token, registered
  always_ff @(posedge clk) begin
    out_valid <= tok[0];
    out_data  <= data[0 +: W];
    if (rst) out_valid <= 1'b0;
  end
endmodule

  • rst_gate.sv (attack, stopped at solution): The outputs are registered, but out_valid is gated by the reset (assign out_valid = ov_q & ~rst): no output may read an input combinationally, the reset included, so the last output before a reset cannot vanish from the wire.

    the design, with its licence and provenance notices 
    // Attack for task sorter (tests/expected.json, `attacks`; review L1 of 2026-11-08, the rule-1 decision of
// 2026-11-09): the proved reference tasks/sorter/reference/sorter_ins.sv with ONE change (the output stage),
// a design whose every claimed snapshot is the reference's: the outputs are registered as ov_q and od_q, and
// out_valid is ov_q gated by the reset (`assign out_valid = ov_q & ~rst`).
// Wrong on the wire: in the cycle of a reset entry the snapshot before it is still claimed, but the wire shows
// out_valid = 0, so a transaction's last output is hidden from a consumer when a reset follows it. Rule 1 with
// nothing exempt (`MooreOutDep d []`, since 2026-11-09) refuses the path from rst to out_valid, for every N, W.
// Every check that needs no proof passes it; the reference's proof (reference/sorter_ins.lean) must FAIL on it.
// Derived from andrewpeck/cell-sort (MIT, cfc46709; the reference's header has the provenance and changes):
//
// MIT License
//
// Copyright (c) 2024-2025 Andrew Peck
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

`timescale 1ns / 1ps
`default_nettype none

module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
  logic [N*W-1:0] data;  // cell k's value: data[k*W +: W]; cell N-1 is the top ("best") cell
  logic [N-1:0]   tok;   // cell k's valid token

  // cells 0 .. N-2: upstream's unit_cell; the upper neighbour is cell k+1
  for (genvar k = 0; k < N-1; k++) begin : gen_cell
    always_ff @(posedge clk) begin
      if (in_valid) begin
        if (in_data > data[(k+1)*W +: W])         // the neighbour is pushed: take its value
          data[k*W +: W] <= data[(k+1)*W +: W];
        else if (in_data > data[k*W +: W])        // the input beats this cell's value
          data[k*W +: W] <= in_data;
      end else
        data[k*W +: W] <= data[(k+1)*W +: W];     // drain: shift down
      tok[k] <= tok[k+1];
      if (rst) begin
        data[k*W +: W] <= '0;
        tok[k] <= 1'b0;
      end
    end
  end

  // the top cell N-1: never pushed into (upstream's push[DEPTH] = 0); drains in the empty value 0
  always_ff @(posedge clk) begin
    if (in_valid) begin
      if (in_data > data[(N-1)*W +: W])
        data[(N-1)*W +: W] <= in_data;
    end else
      data[(N-1)*W +: W] <= '0;
    tok[N-1] <= in_valid;
    if (rst) begin
      data[(N-1)*W +: W] <= '0;
      tok[N-1] <= 1'b0;
    end
  end

  // the streaming output: cell 0 and its token, registered
  logic ov_q;
  logic [W-1:0] od_q;
  always_ff @(posedge clk) begin
    ov_q <= tok[0];
    od_q <= data[0 +: W];
    if (rst) ov_q <= 1'b0;
  end
  assign out_valid = ov_q & ~rst;
  assign out_data = od_q;
endmodule

  • signed_order.sv (attack, stopped at solution): The comparisons are signed, so values with the top bit set sort below the padding 0 and are lost.

    the design, with its licence and provenance notices 
    // Attack for task sorter (tests/expected.json, `attacks`; PLAN4.md Gate 5, the sorter): the proved
// reference tasks/sorter/reference/sorter_ins.sv with ONE change (3 sites), a correct-looking design
// that is wrong for some N, W: the comparisons are signed (`$signed(in_data) > $signed(data[...])`) instead of unsigned.
// Wrong: values with the top bit set sort below the others (and below the padding 0, so they are lost), every N and W.
// Every check up to the proof passes it; the reference's proof (reference/sorter_ins.lean) must FAIL on it.
// Derived from andrewpeck/cell-sort (MIT, cfc46709; the reference's header has the provenance and changes):
//
// MIT License
//
// Copyright (c) 2024-2025 Andrew Peck
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

`timescale 1ns / 1ps
`default_nettype none

module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
  logic [N*W-1:0] data;  // cell k's value: data[k*W +: W]; cell N-1 is the top ("best") cell
  logic [N-1:0]   tok;   // cell k's valid token

  // cells 0 .. N-2: upstream's unit_cell; the upper neighbour is cell k+1
  for (genvar k = 0; k < N-1; k++) begin : gen_cell
    always_ff @(posedge clk) begin
      if (in_valid) begin
        if ($signed(in_data) > $signed(data[(k+1)*W +: W]))         // the neighbour is pushed: take its value
          data[k*W +: W] <= data[(k+1)*W +: W];
        else if ($signed(in_data) > $signed(data[k*W +: W]))        // the input beats this cell's value
          data[k*W +: W] <= in_data;
      end else
        data[k*W +: W] <= data[(k+1)*W +: W];     // drain: shift down
      tok[k] <= tok[k+1];
      if (rst) begin
        data[k*W +: W] <= '0;
        tok[k] <= 1'b0;
      end
    end
  end

  // the top cell N-1: never pushed into (upstream's push[DEPTH] = 0); drains in the empty value 0
  always_ff @(posedge clk) begin
    if (in_valid) begin
      if ($signed(in_data) > $signed(data[(N-1)*W +: W]))
        data[(N-1)*W +: W] <= in_data;
    end else
      data[(N-1)*W +: W] <= '0;
    tok[N-1] <= in_valid;
    if (rst) begin
      data[(N-1)*W +: W] <= '0;
      tok[N-1] <= 1'b0;
    end
  end

  // the streaming output: cell 0 and its token, registered
  always_ff @(posedge clk) begin
    out_valid <= tok[0];
    out_data  <= data[0 +: W];
    if (rst) out_valid <= 1'b0;
  end
endmodule

  • token_self.sv (attack, stopped at solution): Each cell's token shift reads its own token instead of its neighbour's: the tokens never move and no value is emitted.

    the design, with its licence and provenance notices 
    // Attack for task sorter (tests/expected.json, `attacks`; PLAN4.md Gate 5, the sorter): the proved
// reference tasks/sorter/reference/sorter_ins.sv with ONE change (1 site), a correct-looking design
// that is wrong for some N, W: the token shift of cells 0 .. N-2 reads the cell's own token (`tok[k] <= tok[k]`) instead of its upper neighbour's.
// Wrong: the tokens below the top never move, so out_valid stays 0 and no value is emitted (N >= 2); right at N = 1, where the family is empty and out_valid reads the top token.
// Every check up to the proof passes it; the reference's proof (reference/sorter_ins.lean) must FAIL on it.
// Derived from andrewpeck/cell-sort (MIT, cfc46709; the reference's header has the provenance and changes):
//
// MIT License
//
// Copyright (c) 2024-2025 Andrew Peck
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

`timescale 1ns / 1ps
`default_nettype none

module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
  logic [N*W-1:0] data;  // cell k's value: data[k*W +: W]; cell N-1 is the top ("best") cell
  logic [N-1:0]   tok;   // cell k's valid token

  // cells 0 .. N-2: upstream's unit_cell; the upper neighbour is cell k+1
  for (genvar k = 0; k < N-1; k++) begin : gen_cell
    always_ff @(posedge clk) begin
      if (in_valid) begin
        if (in_data > data[(k+1)*W +: W])         // the neighbour is pushed: take its value
          data[k*W +: W] <= data[(k+1)*W +: W];
        else if (in_data > data[k*W +: W])        // the input beats this cell's value
          data[k*W +: W] <= in_data;
      end else
        data[k*W +: W] <= data[(k+1)*W +: W];     // drain: shift down
      tok[k] <= tok[k];
      if (rst) begin
        data[k*W +: W] <= '0;
        tok[k] <= 1'b0;
      end
    end
  end

  // the top cell N-1: never pushed into (upstream's push[DEPTH] = 0); drains in the empty value 0
  always_ff @(posedge clk) begin
    if (in_valid) begin
      if (in_data > data[(N-1)*W +: W])
        data[(N-1)*W +: W] <= in_data;
    end else
      data[(N-1)*W +: W] <= '0;
    tok[N-1] <= in_valid;
    if (rst) begin
      data[(N-1)*W +: W] <= '0;
      tok[N-1] <= 1'b0;
    end
  end

  // the streaming output: cell 0 and its token, registered
  always_ff @(posedge clk) begin
    out_valid <= tok[0];
    out_data  <= data[0 +: W];
    if (rst) out_valid <= 1'b0;
  end
endmodule

  • top_not_drained.sv (attack, stopped at solution): The drain does not clear the top cell: it keeps the transaction's maximum, and the next transaction's values never reach the top.

    the design, with its licence and provenance notices 
    // Attack for task sorter (tests/expected.json, `attacks`; PLAN4.md Gate 5, the sorter): the proved
// reference tasks/sorter/reference/sorter_ins.sv with ONE change (1 site), a correct-looking design
// that is wrong for some N, W: the top cell is not cleared by the drain (its `else` branch is gone): it keeps the transaction's maximum.
// Wrong: the stale maximum shifts down behind the sorted values and is still in the top cell for the next transaction, whose values below it never reach the top: wrong from the second transaction on, every N.
// Every check up to the proof passes it; the reference's proof (reference/sorter_ins.lean) must FAIL on it.
// Derived from andrewpeck/cell-sort (MIT, cfc46709; the reference's header has the provenance and changes):
//
// MIT License
//
// Copyright (c) 2024-2025 Andrew Peck
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

`timescale 1ns / 1ps
`default_nettype none

module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
  logic [N*W-1:0] data;  // cell k's value: data[k*W +: W]; cell N-1 is the top ("best") cell
  logic [N-1:0]   tok;   // cell k's valid token

  // cells 0 .. N-2: upstream's unit_cell; the upper neighbour is cell k+1
  for (genvar k = 0; k < N-1; k++) begin : gen_cell
    always_ff @(posedge clk) begin
      if (in_valid) begin
        if (in_data > data[(k+1)*W +: W])         // the neighbour is pushed: take its value
          data[k*W +: W] <= data[(k+1)*W +: W];
        else if (in_data > data[k*W +: W])        // the input beats this cell's value
          data[k*W +: W] <= in_data;
      end else
        data[k*W +: W] <= data[(k+1)*W +: W];     // drain: shift down
      tok[k] <= tok[k+1];
      if (rst) begin
        data[k*W +: W] <= '0;
        tok[k] <= 1'b0;
      end
    end
  end

  // the top cell N-1: never pushed into (upstream's push[DEPTH] = 0); drains in the empty value 0
  always_ff @(posedge clk) begin
    if (in_valid) begin
      if (in_data > data[(N-1)*W +: W])
        data[(N-1)*W +: W] <= in_data;
    end
    tok[N-1] <= in_valid;
    if (rst) begin
      data[(N-1)*W +: W] <= '0;
      tok[N-1] <= 1'b0;
    end
  end

  // the streaming output: cell 0 and its token, registered
  always_ff @(posedge clk) begin
    out_valid <= tok[0];
    out_data  <= data[0 +: W];
    if (rst) out_valid <= 1'b0;
  end
endmodule
Spec.lean, verbatim (97 lines) 
import SvGolf.TaskSeq

/-!
# Task `sorter`: a streaming sorter of N unsigned W-bit values
# (TRUSTED text, final, decided 2026-11-08, amended 2026-11-09; written 2026-11-04; contract C8 of `design/sequential/CONTRACT.md`)

Module (port order as written; `N`, `W` are the module's parameters, in this order):

```systemverilog
module sorter #(parameter int N = 8, parameter int W = 8) (
  input  logic         clk, rst,
  input  logic         start, in_valid,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  output logic [W-1:0] out_data
);
```

**Protocol** (`StreamTask`, `SvGolf/TaskSeq.lean`; C1, C2, C8): synchronous active-high reset `rst`;
claims from the cycle after its release; `start` a one-cycle pulse raised only when the design is
idle (no transaction yet, or the previous one's `N` outputs emitted); after a `start`, `in_valid`
is 1 for exactly the `N` cycles beginning the cycle after it (no gaps), carrying the values
`x[0] .. x[N-1]` on `in_data`, and 0 otherwise. There is no output backpressure.

**Guarantee.** `out_valid` is KNOWN at every cycle after the release, and 0 before the first
`start`. From each `start` to the next, `out_valid` is 1 on exactly `N` cycles, all at most `lat`
cycles after the edge that samples `start`, and the `out_data` values on those cycles, in order,
are the input values sorted ascending as unsigned numbers, duplicates kept. `out_data` is cared
about only where `out_valid` = 1; the valid cycles may have gaps.

The declared latency `lat` is the submission's; the checker pins its value at the scoring point and
the score uses it. Run-time `/ % **` are banned, as in every task (`task.json`).

**Range.** `N, W ≥ 1` and `N·W < 2^31`: the parameters are `int`, and a design that buffers the whole
stream declares `N·W` bits; every such width must stay in the 32-bit range, where a real elaboration
and ls-sv's unbounded constant tier agree (`PDesign.int32Agrees`; Task v2 decision 1).

**txtask-v2 (2026-11-05; final, decided 2026-11-08, amended 2026-11-09).** `Statement` is the v2
statement `StreamTask.StatementV2`: txtask-v1's interface, clock discipline and latency bound; its
claims and termination from EVERY power-up state on every known stimulus (rule 2); Moore outputs
(`MooreOutDep`, rule 1, nothing exempt: no combinational path from `rst`, `start`, `in_valid` or
`in_data` to `out_valid` or `out_data`); and no construct that creates an `x` from known operands
(`XSafe`, rule 3). `SvGolf/TaskSeq.lean`, last section, and `design/soundness/TXTASK-V2-REVIEW.md`.
-/

namespace SvGolf.Tasks.Sorter

open SvGolf

/-- The parameters `(N, W)`. -/
abbrev Params := Nat × Nat

/-- Insert `a` into an ascending list (unsigned order), before the first element it is `≤` to. -/
def insertAsc {W : Nat} (a : BitVec W) : List (BitVec W) → List (BitVec W)
  | [] => [a]
  | b :: bs => if a.toNat ≤ b.toNat then a :: b :: bs else b :: insertAsc a bs

/-- Insertion sort, ascending, unsigned: `List.insertionSort (· ≤ ·)` (C8), written out here
because the trusted text imports no Mathlib (structural recursion: the kernel evaluates it). -/
def sortAsc {W : Nat} : List (BitVec W) → List (BitVec W)
  | [] => []
  | a :: as => insertAsc a (sortAsc as)

/-- **The task** (C8). -/
def task : StreamTask Params where
  inRange p := 1 ≤ p.1 ∧ 1 ≤ p.2 ∧ p.1 * p.2 < 2 ^ 31
  clk := "clk"
  rst := "rst"
  start := "start"
  inValid := "in_valid"
  inData := "in_data"
  outValid := "out_valid"
  outData := "out_data"
  width p := p.2
  count p := p.1
  spec _ xs := sortAsc xs

/-- **The challenge statement**, for the two-parameter design family `sem N W` and the latency
function `lat N W`. -/
abbrev Statement (sem : Nat → Nat → LeanModels.Sv.Design2) (lat : Nat → Nat → Nat) : Prop :=
  task.StatementV2 (fun p => sem p.1 p.2) (fun p => lat p.1 p.2)

/-! ## Sanity checks on the statement's data (proved; they add nothing to the trusted base) -/

/-- Duplicates kept, unsigned order. -/
example : sortAsc [3#4, 15#4, 0#4, 3#4, 8#4] = [0#4, 3#4, 3#4, 8#4, 15#4] := by decide

/-- A typical point is in range; the 32-bit bound excludes `N·W ≥ 2^31`. -/
example : task.inRange (8, 8) ∧ ¬ task.inRange (2 ^ 16, 2 ^ 15) := by
  simp [task]

/-- The port names are distinct. -/
example : ["clk", "rst", "start", "in_valid", "in_data"].Nodup ∧
    ["out_valid", "out_data"].Nodup := by
  decide

end SvGolf.Tasks.Sorter

Its trusted text

The modules specific to this task. Like every task, it also rests on the shared trusted base (the ls-sv semantics of SystemVerilog and svGolf's statement helpers), and a proof may import any module of the ls-sv library. Nothing else is trusted: proof helpers are kernel-checked like any submission.

modulerolelinessha256
tasks.sorter.Specsvgolf/tasks/sorter/Spec.leantask statement976243e0673747

How to participate #

  1. Write a circuit with the task's exact interface.
  2. Prove in Lean 4 that it meets the trusted statement; Start a new design, below, gives the route, and the proving guide shows how.
  3. Check and record it (how to submit): the checker accepts the pair or says which stage refused it, as it does for each design under what does not count.
  4. Beat par: an accepted design whose score (area × time) is below that of the best proved reference. The leaderboard ranks by it.

How to submit

You hand in two files: solution.sv, a module with the exact header under Interface, and Solution.lean, a Lean 4 proof that it meets the trusted statement, at the latency you declare.

Step 0, once per machine. Install:

  • elan, which installs the Lean toolchain that lean-toolchain pins (leanprover/lean4:v4.33.0-rc1) on first use;
  • Yosys 0.53 with its yosys-abc (every pinned tool and file: Reproduce a score);
  • Verilator 5, a C++ compiler and make, for the post-synthesis check (it compiles Verilator's model of the netlist);
  • Python 3.12 with python3.12 -m pip install -r requirements.txt (pyslang==11.0.0, the extractor's SystemVerilog frontend).
step 0
git clone https://github.com/thomasnormal/svgolf
cd svgolf
python3.12 -m pip install -r requirements.txt
# the trusted Lean and the checker's evaluator
lake build
# the pinned sky130 liberty, checked by its hash
python3.12 score/ppa.py --fetch-liberty

lake build takes about 6 minutes and 1 GB of disk the first time, on a laptop that already had the Lean toolchain (README.md's Step 0 says what was measured where; elan's first download of the toolchain comes on top): Lake clones proglib (formerly lean-surfaces) and its packages from github.com, so it needs network access there, and builds the LeanModels.Sv modules svGolf uses; Mathlib is cloned, never built.

Start from the reference pair under Files, sorter_ins, a complete and accepted one: copy it, from the same directory:

shell
cp tasks/sorter/reference/sorter_ins.sv solution.sv
cp tasks/sorter/reference/sorter_ins.lean Solution.lean

Then, for each design, from the same directory: find it without Lean and check it once without a proof, at the latency you mean to claim (the golfing loop and step 1), write its proof (Start a new design, below, gives the route), then check the pair and record it (steps 2 and 3):

shell
# the golfing loop, no Lean: area and period, about a second
python3.12 score/ppa.py solution.sv --task tasks/sorter \
    --seq --path
# 1. no proof needed; never accepts; exits 0 when every
#    stage passed, ending with area x time and par;
#    --latency: the cycles you mean to claim (16: par's)
python3.12 check.py tasks/sorter solution.sv --unproved \
    --latency 16 --stage-dir stage
# 2. the real check: prints "accepted": true; its
#    post-synthesis check is LIGHT by default (a subset of
#    the vectors, for local feedback), so stderr also says
#    "accepted, but the check was INCOMPLETE ... rerun with
#    --postsynth full": expected, since step 3 runs the
#    full one itself
python3.12 check.py tasks/sorter solution.sv Solution.lean
# 3. record it: the whole check again, full and sandboxed
python3.12 leaderboard/leaderboard.py add --task sorter \
    --player YOUR_HANDLE --assisted-by "TOOL OR MODEL" \
    --sv solution.sv --lean Solution.lean \
    --notes "YOUR DESIGN IN ONE LINE"

Done: step 3 prints added sorter/HASH: YOUR_HANDLE, … once the pair has passed the whole check, full and sandboxed, and its record is written (what it writes, and where: below); otherwise it prints REFUSED with the reasons and records nothing. Step 2's "accepted": true, with its INCOMPLETE line, is feedback for you, not a record.

The golfing loop and step 1, the first two commands above. The first command weighs the design through the clocked flow (--seq): the area and the register-to-register period, with the critical path (--path). The second runs every stage that needs no proof: the clocked source rules, the check that no construct can create an x (clocked_rules), the never-loaded register check, the score, and the clocked post-synthesis check, which drives the scored netlist through oracle.py's transactions from random power-up states and holds every emitted list to sorted() and to the latency. A wrong design is named there, with the transaction, before any proof. It leaves the design staged in stage/ for probe files (PROVING.md, section 0). Rule 1 (Moore outputs) has no early check in this kind: the proof is what refuses a combinational path from an input to an output.

score/ppa.py is the inner loop of golfing; its ranked numbers are area_um2_sky130 and delay_ps_sky130 in what it prints. It runs only the source gate and the pinned flow: it does not check the banlist, the 4-state rules, whether ls-sv can read the design, the post-synthesis simulation or the task's function. Step 1 does, still without a proof.

The Lean file. The checker extracts your .sv itself and writes the trusted module Submission.Design; Goal lat unfolds to SvGolf.Tasks.Sorter.Statement Submission.design.sem lat ∧ lat 8 8 = n: the task's statement of your design at your latency lat (cycles, a function of the parameters), and its value at the scoring point (N = 8, W = 8), the n of your header line -- svgolf-latency: n, which the score takes as the cycles (the checker reads the latency from this file, never from the .sv):

Submission.Design (generated: you never write it)
import LeanModels.Sv.Ingest2
import tasks.sorter.Spec

namespace Submission
load_design_sv2 design from "<the envelope of your .sv>"
abbrev Goal (lat : …) : Prop :=
  SvGolf.Tasks.Sorter.Statement design.sem lat ∧ lat <scoring point> = <your latency>
end Submission

Your Solution.lean imports it and proves Goal lat, as the skeleton in Start a new design (The proof in detail) shows. File names and paths are free (here solution.sv and Solution.lean); the module name Submission, the import Submission.Design header, the definition lat (one Nat per parameter, in the task's order), the theorem solution : Goal lat (in namespace Submission, theorem Submission.solution : Submission.Goal Submission.lat) and exactly one line -- svgolf-latency: n (n a decimal number of cycles, at least 1) are fixed.

Step 3 writes your record's three files (.json, .sv and .lean, named by the record's hash) to leaderboard/data/sorter/, the directory a pull request adds. Then open a pull request against https://github.com/thomasnormal/svgolf that adds them; CI re-verifies it. There is no submission server: nothing is sent anywhere by these commands. For a private trial, add --data-dir DIR: the record then goes to DIR and the board stays as it is. Repeat --assisted-by for each tool or AI system that helped, or leave it out.

YOUR_HANDLE is your public name: the board and the record's page show it. It is 1 to 32 characters, letters, digits, ., _ or -, the first a letter or a digit ([A-Za-z0-9][A-Za-z0-9._-]{0,31}). --notes is optional: one line on the design (at most 2000 characters), shown on the record's page. In a private trial (--data-dir DIR), add --from-check RESULT.json records the JSON that a check.py … --postsynth full --ppa require run printed instead of checking again; the board's own leaderboard/data/ refuses a stored result.

the sandbox, and machines without one

leaderboard.py add runs the check with --sandbox require: the proof's Lean, the extractor, Yosys and Verilator must run inside the operating system's sandbox (Seatbelt on macOS, bubblewrap on Linux). Where that sandbox is missing or fails its self-test, the check stops with an infrastructure error and nothing is recorded. On such a machine, --sandbox auto runs the check without it (and says so on stderr), and --sandbox off skips it: your proof file then runs with your own privileges, and the record is for your own use, since an official record is made with the sandbox or not at all. add also weighs the ranked sky130 numbers, which need the pinned liberty (Step 0). On a shared machine whose Lean calls go through a wrapper, set SVGOLF_LEAN_WRAP; check.py and leaderboard.py both read it, and SVGOLF_LEAN_WRAP_ONCE=1 takes the wrapper once for a whole run.

Leaderboard

by score · ASAP7
  1. 1
    kestrel-golf
    2026-11-10
    157 0154754.6 µm² × 16 × 2.06 ns
  2. ⚑
    sorter_ins
    par proved reference
    222 5405512.8 µm² × 16 × 2.52 ns
every column: area, time, proof lines, assisted by, files
#playerdatescore (µm²·ns)area (µm²)time (ps)area (GE)depthproof linesassisted byrecordfiles
1kestrel-golf2026-11-10157 0154754.6330241159.53515816Claude Sonnet 5.561bf6f8d17f7.sv .lean
  1. 1
    kestrel-golf
    2026-11-10
    538.974.854 µm² × 16 × 0.450 ns
  2. ⚑
    sorter_ins
    par proved reference
    701.985.687 µm² × 16 × 0.512 ns
every column: area, time, proof lines, assisted by, files
#playerdatescore (µm²·ns)area (µm²)time (ps)area (GE)depthproof linesassisted byrecordfiles
1kestrel-golf2026-11-10538.974.85472001159.53515816Claude Sonnet 5.561bf6f8d17f7.sv .lean
score: area × time, µm²·nspar

At a glance

top module
sorter
parameters
N in range 1 <= N, N*W < 2^31, W in range 1 <= W, N*W < 2^31
scoring point
N = 8, W = 8
depth budget
none
banned run-time operators
/ % **

No task-specific ban: comparisons are the task, and nothing else builds a sorter for free. The score prices the schedule (cells, comparators, cycles). Run-time / % ** are banned here as in every task: a zero divisor or a negative exponent makes an unknown value from known operands.

allowed axioms
propext, Classical.choice, Quot.sound
proof time limit
300 s of CPU time (a wall-clock backstop of 1500 s stops a proof that waits)

Files

Spec.leanProperties.leansorter_ins.svsorter_ins.leansorter_ins.svsorter_ins.lean

sorter_ins.sv is adapted from licensed code (MIT): a design derived from it keeps the copyright and licence notices of its header.

Every reference and baseline is under proved references and baselines.

Start a new design

The route: a phase model, StreamTask.satisfiedAtV2_of_phases (PROVING.md, section 19; reference/sorter_ins.lean is a complete proof). The reduction in SvGolf/SeqV2.lean turns the statement at one point into facts about ONE clock cycle:

  1. Interface: the ports in order and distinct declaration names (rfl, and decide on the names);
  2. Disciplined: ClockedBy clk none (no asynchronous reset), a simp over the processes;
  3. TerminatesPU, by TerminatesPU.of_invariant from the clock step;
  4. the latency facts: 1 ≤ N, N ≤ lat, and that the spec keeps the length (sortAsc does);
  5. a StreamTask.PhaseModel: the clock step in closed form (its CycleModel: a Shape and the one-cycle Step), the phases Ready (after a reset, nothing to show) and At ys j (j cycles after a start, the inputs ys so far), the output schedule out xs j, and the one-cycle obligations reset, hold, start, feed and run;
  6. the shape at every power-up state (powerUp_cons once per declaration);
  7. rule 1, MooreOutDep: for a design whose every process is an always_ff, MooreOutDep.of_noComb with combDeps_of_ffOnly;
  8. rule 3, XSafe: a simp over xsafeB and its helpers (xsProc, xsStmt, xsWidth, ...).

reference/sorter_ins.lean, named above, is 774 code lines long.

The proof in detailLay the design out so the proof stays short · The skeleton · Library lemmas that exist today

Lay the design out so the proof stays short:

  • register every output: with only always_ff processes, rule 1 is one line (combDeps_of_ffOnly);
  • keep every process an always_ff whose body writes with nonblocking assignments only: the library's clock step in closed form (cycleStep2_ffOnly; the reference uses it through cycleStep2_profile) is for such designs only. A continuous assign or an always_comb block anywhere, an output driven by one included (assign out_valid = tok[0]), means proving the combinational settle yourself, as the arbiter's proof does (PROVING.md, section 20);
  • reset every register whose value matters: the claims hold from every power-up value, the first reset edge included (a design whose out_valid timing within the latency depends on an unreset register can still be correct: the post-synthesis check holds each power-up's run to the claims, not to another power-up's cycles);
  • nest generate loops: the loader gives each generate loop a fixed budget of (N + W + 2)² + 64 iterations at a point (the sum of the parameter values plus 2, squared, plus 64), and a nested loop gets the whole budget again. A loop over N, W, N·W or N² iterations always fits; one flat loop over N·N·W lanes or N³ iterations exceeds the budget at points in the range (at (100, 8): 80000 lanes against 12164), and there the loader gives up: the design reads as an empty one, so the statement is unprovable, however correct the circuit is. Write one loop per index and nest them;
  • for XSafe, operands of one width and run-time indices whose every value is in range, as in the arbiter's advice.

The skeleton (reference/sorter_ins.lean is it, filled in for the insertion array):

-- svgolf-latency: 16
import Submission.Design
import SvGolf.SeqV2

namespace Submission
open LeanModels.Sv SvGolf

def lat (N _W : Nat) : Nat := 2 * N   -- yours: your design's latency

-- 1. agreement: `design.sem N W = myD N W`, a hand-built Design2
-- 2. one cycle in closed form; 3. the invariant; 4. the phase model `model N W`

theorem solution : Goal lat := by
  refine ⟨fun p hp => ?_, rfl⟩
  obtain ⟨N, W⟩ := p
  obtain ⟨hN, hW, -⟩ := hp
  exact Tasks.Sorter.task.satisfiedAtV2_of_phases (my_interface N W hN hW) (my_disciplined N W hN hW)
    (my_terminatesPU N W hN hW) hN (show N ≤ 2 * N by omega) (fun xs h => (my_len_sort xs).trans h)
    (model N W hN hW) (my_powerUp N W hN hW) (my_moore N W hN hW) (my_xsafe N W hN hW)

end Submission

#print axioms solution must show propext, Classical.choice and Quot.sound only.

Library lemmas that exist today:

  • SvGolf.SeqV2: StreamTask.satisfiedAtV2_of_phases (the reduction), MooreOutDep.of_noComb, combDeps_of_ffOnly, MooreOutDep.of_check (rule 1 by evaluation, for a design with combinational logic), TerminatesPU.of_invariant, powerUp_cons, powerUp_nil;
  • SvGolf.Seq: StreamTask.PhaseModel and the v1 reduction it feeds (StreamTask.guar_of_phases);
  • LeanModels.Sv.SeqProfile, LeanModels.Sv.SeqFamily, LeanModels.Sv.NbaCommit: G0's clock step for a flip-flop-only design, the packed-family commit lemmas (bvInsertAt_packBV, foldl_range_ofBitVec_packBV, LVec.foldl_range_insertAt_last) and nbaFold.

Compare the designs

ASAP7 · any two numbers · lower is better

N = 8, W = 8, the scored point: the ranked numbers. The same designs are also measured at N = 4, W = 8 and N = 16, W = 8: measured, not ranked, the same proved designs through the same pinned flow at other parameters (the tables below, and how the designs scale).

sorter: area against time2 designs by Time (ps) (x) and Area (µm²) (y); lower is better on both. The table under the chart lists the same numbers.480050005200540034k36k38k40kTime (ps)Area (µm²) · lower is betterthe Pareto front of the proved designssorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 222 540 µm²·ns · Time: 40 368 ps · Area: 5512.8 µm²kestrel-golf · submission · 2026-11-10 · Score: 157 015 µm²·ns · Time: 33 024 ps · Area: 4754.6 µm²
sorter: area against time2 designs by Time (ps) (x) and Area (µm²) (y); lower is better on both. The table under the chart lists the same numbers.475050005250550032.5k35k37.5k40kTime (ps)Area (µm²) · lower is betterthe Pareto front of the proved designssorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 222 540 µm²·ns · Time: 40 368 ps · Area: 5512.8 µm²kestrel-golf · submission · 2026-11-10 · Score: 157 015 µm²·ns · Time: 33 024 ps · Area: 4754.6 µm²
  • submission
  • proved reference
  • the Pareto front of the proved designs
Lower is better on both axes. The step line joins the proved designs that no other proved design beats on both; baselines are shown for scale. Choose any two numbers to find the best design for your own trade-off. 2 of 2 designs have both numbers.
every design with all its numbers, by score (at N = 8, W = 8, ranked)
designScore (µm²·ns)Area (µm²)Time (ps)Clock period (ps)Latency (cycles)Flip-flopsArea (GE)Depth (gates)GatesProof (lines)
kestrel-golf submission157 0154754.633 024206416811159.53515697816
sorter_ins par222 5405512.840 368252316811288.81915713774
at N = 4, W = 8 (measured, not ranked): every design with all its numbers, by score
designScore (µm²·ns)Area (µm²)Time (ps)Clock period (ps)Latency (cycles)Flip-flopsArea (GE)Depth (gates)GatesProof (lines)
sorter_ins reference52 5842737.619 2082401845639.24415325774
at N = 16, W = 8 (measured, not ranked): every design with all its numbers, by score
designScore (µm²·ns)Area (µm²)Time (ps)Clock period (ps)Latency (cycles)Flip-flopsArea (GE)Depth (gates)GatesProof (lines)
sorter_ins reference888 89510 590.283 9362623321532445.957151315774
sorter: area against time2 designs by Time (ps) (x) and Area (µm²) (y); lower is better on both. The table under the chart lists the same numbers.7577.58082.585720074007600780080008200Time (ps)Area (µm²) · lower is betterthe Pareto front of the proved designssorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 701.9 µm²·ns · Time: 8192 ps · Area: 85.687 µm²kestrel-golf · submission · 2026-11-10 · Score: 538.9 µm²·ns · Time: 7200 ps · Area: 74.854 µm²
sorter: area against time2 designs by Time (ps) (x) and Area (µm²) (y); lower is better on both. The table under the chart lists the same numbers.75808575008000Time (ps)Area (µm²) · lower is betterthe Pareto front of the proved designssorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 701.9 µm²·ns · Time: 8192 ps · Area: 85.687 µm²kestrel-golf · submission · 2026-11-10 · Score: 538.9 µm²·ns · Time: 7200 ps · Area: 74.854 µm²
  • submission
  • proved reference
  • the Pareto front of the proved designs
Lower is better on both axes. The step line joins the proved designs that no other proved design beats on both; baselines are shown for scale. Choose any two numbers to find the best design for your own trade-off. 2 of 2 designs have both numbers.
every design with all its numbers, by score
designScore (µm²·ns)Area (µm²)Time (ps)Clock period (ps)Latency (cycles)Flip-flopsArea (GE)Depth (gates)GatesProof (lines)
kestrel-golf submission538.974.854720045016811159.53515697816
sorter_ins par701.985.687819251216811288.81915713774

How the designs scale #

On sky130 in either view: the designs are measured at the other points on sky130 alone (score/measured/), and the ASAP7 view weighs each design at the scoring point only.

sorter: score over par against N (W = 8), one line per design1 designs, Score ÷ par's (y) against N (W = 8) (x), one line each, named on the right; lower is better. The table under the chart lists the same numbers.0.90.9511.051.14816N (W = 8), log scaleScore ÷ par's · lower is betterpar: sorter_inssorter_ins · proved reference · measured, not rankedsorter_ins · N = 4, W = 8 · measured, not ranked · Score: 52 584 µm²·ns (×1.00 par)sorter_ins · N = 8, W = 8 · the scored point · Score: 222 540 µm²·ns (×1.00 par)sorter_ins · N = 16, W = 8 · measured, not ranked · Score: 888 895 µm²·ns (×1.00 par)sorter_ins
sorter: score over par against N (W = 8), one line per design1 designs, Score ÷ par's (y) against N (W = 8) (x), one line each, named on the right; lower is better. The table under the chart lists the same numbers.0.911.14816N (W = 8), log scaleScore ÷ par's · lower is betterpar: sorter_inssorter_ins · proved reference · measured, not rankedsorter_ins · N = 4, W = 8 · measured, not ranked · Score: 52 584 µm²·ns (×1.00 par)sorter_ins · N = 8, W = 8 · the scored point · Score: 222 540 µm²·ns (×1.00 par)sorter_ins · N = 16, W = 8 · measured, not ranked · Score: 888 895 µm²·ns (×1.00 par)sorter_ins
  • proved reference
  • par
Score of each design over par's (sorter_ins) at the same point, against N (W = 8): 1 is par, and a line under it beats par at that size, so where two lines cross one design starts to pay off against the other. One line per design, lower is better: the same proved design at each point, through the same pinned flow. Measured, not ranked: the board ranks at N = 8, W = 8 only. A dashed line is a baseline (not proved).
every design at every point: Score (µm²·ns)
designN = 4, W = 8N = 8, W = 8 (ranked)N = 16, W = 8
sorter_ins52 584222 540888 895

Proved references

Proved and accepted designs that ship with the task, written or adapted by the maintainers. They are the first entries, and par, the bar to beat, is the one with the best score (area × time, µm²·ns, from the sky130ASAP7 area and time; a design without a sky130an ASAP7 weighing has no score and comes after, by its extra GE columns). A reference that was also recorded links its record under its name: the record holds that reference's design and proof, matched by the sha256 of both files.

designscore (µm²·ns)area (µm²)time (ps)GE · depthvs parproof linesfiles
sorter_ins parparAn insertion-cell array (cell sort, adapted from andrewpeck/cell-sort, MIT): N cells, each comparing the broadcast input with its own value and its upper neighbour's, and a valid token per cell; latency 2N.tactics: decide, induction, omega, simprecord: 90919c7cd8f8222 540701.95512.885.68740 36881921288.819 · 15parpar774.sv .lean

Baselines

No baselines for this task.