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 / record

Record 90919c7cd8f8

reference: par, not an entryreference: par, not an entry scored at N = 8, W = 8

Recorded by the maintainers from the proved reference sorter_ins: its design and its proof sorter_ins.lean (774 code lines). An 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. The record shows that reference passing the whole checker. It is par, the bar to beatpar, the bar to beat, not a player's entry, and it is not ranked among the submissions (proved references).

Area

5 512.79µm²

5 512.7872 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
this design is par
on this page
2nd of 2 designs
cells
713
flops
81
repair
0 buffers, 0 tie cells
GE
1 288.819 extra

Performance · time

40 368ps

16 cycles × 2 523 ps; the period is the latest arrival at an output, or at a flip-flop's D plus setup, ideal clock

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
this design is par
on this page
2nd of 2 designs
Fmax-eq.
24.8 MHz derived
critical path
11 cells
unit depth
15 extra

Score · area × time

222 540µm²·ns

5 512.7872 µm² × 40 368 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
this design is par
on this page
2nd of 2 designs
board
par, the bar to beat: never ranked
Pareto
dominated on this page by kestrel-golf

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

how these numbers are measured and compared

Area: sky130 A0′, the repaired netlist.

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

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

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

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

Area

85.687µm²

85.68666 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
this design is par
on this page
2nd of 2 designs
cells
998
flops
81
repair
0 buffers, 0 tie cells
GE
1 288.819 extra

Performance · time

8 192ps

16 cycles × 512 ps; the period is the latest arrival at an output, or at a flip-flop's D plus setup, ideal clock

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
this design is par
on this page
2nd of 2 designs
Fmax-eq.
122.1 MHz derived
unit depth
15 extra

Score · area × time

701.9µm²·ns

85.68666 µm² × 8 192 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
this design is par
on this page
2nd of 2 designs
board
par, the bar to beat: never ranked
Pareto
dominated on this page by kestrel-golf

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

how these numbers are measured and compared

Area: ASAP7 A0′ (asap7_a0_v1), the same scored netlist, each gate its least-area ASAP7 build, repaired by buffering. ASAP7: a predictive 7 nm library, never fabricated; no wires, like sky130's score (how ASAP7 is scored, and its quirks).

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

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

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

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

The sources

Adapted from licensed code (MIT): the copyright, provenance and licence notices and the list of changes are kept in the design file, shown in full below.

sorter_ins.svdownload
// svGolf task `sorter`, reference: a streaming insertion-cell sorter ("cell sort"), adapted from a
// real-world design.
//
// PROVENANCE. Adapted from andrewpeck/cell-sort, https://github.com/andrewpeck/cell-sort, commit
// cfc46709eaa911858136c2300327ca73bf1eb9a0, files cell_sort.sv and unit_cell.sv, MIT License,
// Copyright (c) 2024-2025 Andrew Peck (the notice is kept below, as the license requires). Kept
// from upstream: the cell rule. On an input, a cell takes its upper neighbour's value when that
// neighbour is pushed (input > neighbour), else the input when the input beats its own value
// (input > own), else it holds; the top ("best") cell is never pushed into; the reset clears every
// cell to 0, written after the cell's other writes so that it overrides them. CHANGES, with reasons:
//  1. One module `sorter #(N, W)` with the C8 ports (Spec.lean): DEPTH -> N, SORTB -> W,
//     data_i -> in_data, dav_i -> in_valid. METAB/metadata and REV are dropped: they are not in the
//     interface, and REV = 0 is the ascending order. `start` is not read (TIMING below).
//  2. unit_cell is inlined into a generate family of cells 0 .. N-2 plus the top cell N-1, cell k's
//     value at data[k*W +: W] of one flat vector: the statement is about flat designs, and ls-sv's
//     extractor refuses the upstream's unpacked port and wire arrays (measured).
//  3. The wires `comparator`, `neighbor_push_o` and the continuous assigns are inlined into the
//     always_ff bodies: the clock-step theorem's FF-only profile has always_ff processes only.
//  4. NEW streaming output (upstream: all cells in parallel on data_o[DEPTH]; C8 streams). When
//     in_valid = 0 every cell takes its upper neighbour's value and the top cell takes 0, the
//     upstream's empty value: the minimum leaves through cell 0 into out_data, one per cycle.
//  5. NEW valid token tok[k], one bit per cell, shifted down every cycle with in_valid entering at
//     the top: out_valid is in_valid delayed by N cycles. Upstream has no output valid.
//  6. Dropped: `updating` (a net assigned in always_ff, a slang error, and connected out of range
//     at updating[DEPTH]) and `resetall (refused by the source gate).
//
// INVARIANT. Let a start be sampled at entry s and x_0 .. x_{N-1} be in_data at entries s+1 .. s+N.
// Read the cells bottom-up (cell 0 first) as a list B of N values.
//  - Load: after the edge of entry s+t (0 <= t <= N), B = [0]^(N-t) ++ sortAsc [x_{t-1}, .., x_0].
//    Inserting x at that edge gives B' = tail (insertAsc x B): with q = #{k : B[k] < x}, cells
//    k < q-1 take B[k+1], cell q-1 takes x, cells k >= q hold; the dropped head is a padding 0 while
//    t < N, and x = 0 changes nothing, as tail (insertAsc 0 B) = B. The ties land where Spec.lean's
//    insertAsc puts them (before the first element the new value is <= to), so the step is
//    insertAsc itself; sortAsc (reverse xs) = sortAsc xs (insertions commute) closes the load.
//  - Drain: after the edge of entry s+N+j (1 <= j <= N), out_valid = 1, out_data = S[j-1] and
//    B = S[j..N) ++ [0]^j, where S = sortAsc [x_0, .., x_{N-1}]. So after s+2N every cell is 0.
//  - Token: tok[k] after the edge of entry c is in_valid at entry c-(N-1-k) (0 before that, from
//    the reset), and out_valid after the edge of entry c is in_valid at entry c-N.
//  - Known: reset writes every cell, token and out_valid; out_data is loaded from cell 0 at every
//    edge; every other write reads known state and in_valid/in_data, which the rely makes known.
//
// TIMING. lat(N, W) = 2N. out_valid = 1 exactly at snapshots s+N+1 .. s+2N, consecutive, carrying
// S in order. It is tight for this design: every transaction's last output is at s+2N. Any design
// needs at least 2N-1 (the minimum depends on x_{N-1}, sampled at entry s+N); this one spends one
// cycle on the registered out_data. `start` is not read: under the rely, in_valid = 1 exactly at
// the N entries after each start. Back-to-back (C2/C4, CONTRACT.md point 7): the earliest legal
// next start is entry s+2N+1, and by then the state is the reset state (cells 0, tokens 0), so
// back-to-back starts need nothing. A start during the drain is not Idle (a rely violation, no
// claim); this design would insert its values into the partly drained array.
//
// 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
  always_ff @(posedge clk) begin
    out_valid <= tok[0];
    out_data  <= data[0 +: W];
    if (rst) out_valid <= 1'b0;
  end
endmodule
sorter_ins.lean (774 code lines) 
-- svgolf-latency: 16
import Submission.Design
import LeanModels.Sv.Gen2
import LeanModels.Sv.Hier2Gen
import LeanModels.Sv.SeqProfile
import LeanModels.Sv.SeqFamily
import LeanModels.Sv.Known2
import LeanModels.Sv.Mono2
import SvGolf.SeqV2

/-!
# Reference solution for task `sorter`: the insertion-cell array (cell sort), latency `2N`

`reference/sorter_ins.sv` (adapted from andrewpeck/cell-sort, MIT; provenance in its header) keeps `N`
cells, cell `k` at `data[k*W +: W]`, a valid token per cell and a registered output from cell `0`.
Proved at every in-range `(N, W)` through `StreamTask.satisfiedAt_of_phases` (`SvGolf.Seq`):
1. **Agreement** (`so_sem_eq`): `design.sem N W` is the hand-built `soD` (no cell family at `N = 1`).
2. **G0's clock step** (`so_profile`, `so_cycle`): one cycle is the commit `soNext` of the queues
   `topQ`, `outQ`, `cellQ`, register by register (`nbaFold`); a reset's write wins (`next_reset`).
3. **The sort** (`hw_ins`, `ins_comm`, `sort_snoc`, `tail_ins`): a load is `tail ∘ insertAsc x` on the
   ascending cells, and insertions commute, so `t` loads give `[0]^(N-t) ++ sortAsc` of the inputs.
4. **The invariant** (`cv`, `tokv`, `ovb`, `at_step`): the cells, the token delay line and the output
   `j` cycles after a start; a drain shifts the sorted list down, so the state ends all zero.
5. **The protocol** (`model`): `Ready` (zero) and `At ys j`; txtask-v2's rules (section 9); then
   `solution`. The packed-family lemmas (`bvInsertAt_packBV`, `foldl_range_ofBitVec_packBV`,
   `LVec.foldl_range_insertAt_last`) are in `LeanModels.Sv.SeqFamily`, `nbaFold` in `LeanModels.Sv.NbaCommit`.
-/

namespace Submission

open LeanModels.Sv SvGolf

/-- The latency: the last output shows `2N` snapshots after the start's. -/
def lat (N _W : Nat) : Nat := 2 * N

/-! ## 1. Agreement: the loaded family is the hand-built `soD` -/

/-- `w` zero bits, and the select `data[lo +: W]`. -/
abbrev zW (w : Nat) : LVec := LVec.replicate w .l0
abbrev dw (lo W : Nat) : Expr2 := .slice (.ident "data") lo W

/-- The top cell `N - 1`: never pushed into; drains in `0`. -/
def topP (N W : Nat) : Process2 :=
  .alwaysFF "clk" (.block #[
    .ifStmt (.ident "in_valid")
      (.block #[.ifStmt (.binary .gt (.ident "in_data") (dw ((N - 1) * W) W))
        (.nbaAssign (.slice "data" ((N - 1) * W) W) (.ident "in_data")) none])
      (some (.nbaAssign (.slice "data" ((N - 1) * W) W) (.lit (zW W)))),
    .nbaAssign (.slice "tok" (N - 1) 1) (.ident "in_valid"),
    .ifStmt (.ident "rst") (.block #[.nbaAssign (.slice "data" ((N - 1) * W) W) (.lit (zW W)),
      .nbaAssign (.slice "tok" (N - 1) 1) (.lit (zW 1))]) none])

/-- The registered output: cell `0` and its token. -/
def outP (W : Nat) : Process2 :=
  .alwaysFF "clk" (.block #[.nbaAssign (.ident "out_valid") (.slice (.ident "tok") 0 1),
    .nbaAssign (.ident "out_data") (dw 0 W),
    .ifStmt (.ident "rst") (.nbaAssign (.ident "out_valid") (.lit (zW 1))) none])

/-- Cell `k < N - 1`: take the pushed neighbour's value, or the input, or hold; drain down. -/
def cellP (W k : Nat) : Process2 :=
  .alwaysFF "clk" (.block #[
    .ifStmt (.ident "in_valid")
      (.block #[.ifStmt (.binary .gt (.ident "in_data") (dw ((k + 1) * W) W))
        (.nbaAssign (.slice "data" (k * W) W) (dw ((k + 1) * W) W))
        (some (.ifStmt (.binary .gt (.ident "in_data") (dw (k * W) W))
          (.nbaAssign (.slice "data" (k * W) W) (.ident "in_data")) none))])
      (some (.nbaAssign (.slice "data" (k * W) W) (dw ((k + 1) * W) W))),
    .nbaAssign (.slice "tok" k 1) (.slice (.ident "tok") (k + 1) 1),
    .ifStmt (.ident "rst") (.block #[.nbaAssign (.slice "data" (k * W) W) (.lit (zW W)),
      .nbaAssign (.slice "tok" k 1) (.lit (zW 1))]) none])

/-- The declarations, `in_data`/`out_data` at `w`, `data` at `nw`, `tok` at `n` bits. -/
def soDeclsW (w nw n : Nat) : List Decl :=
  [{ name := "clk", width := 1, isInput := true }, { name := "rst", width := 1, isInput := true },
   { name := "start", width := 1, isInput := true }, { name := "in_valid", width := 1, isInput := true },
   { name := "in_data", width := w, isInput := true }, { name := "out_valid", width := 1, isOutput := true },
   { name := "out_data", width := w, isOutput := true }, { name := "data", width := nw },
   { name := "tok", width := n }]

abbrev soDecls (N W : Nat) : List Decl := soDeclsW W (N * W) N

def soD (N W : Nat) : Design2 where
  name := "sorter"
  decls := (soDecls N W).toArray
  processes := (topP N W :: outP W :: (List.range (N - 1)).map (cellP W)).toArray

def soScope (N W : Int) : IEnv := { vals := [("N", N), ("W", W)], pwidths := [("N", 32), ("W", 32)] }

def soEnv (N W : Int) : IEnv := { soScope N W with dims := dimTable (soScope N W) design.pdesign.decls }

theorem so_paramEnv (N W : Int) : design.pdesign.paramEnv2 [N, W] = .ok (soEnv N W) := rfl

def soElems : List (String × Nat) :=
  ["clk", "rst", "start", "in_valid", "in_data", "out_valid", "out_data", "data", "tok"].map (·, 1)

theorem so_decls (N W : Int) : buildDecls (soEnv N W) design.pdesign.decls =
    .ok (soDeclsW ((W - 1).natAbs + 1) ((N * W - 1).natAbs + 1) ((N - 1).natAbs + 1)) := by
  simp [design.pdesign, buildDecls, instDecl, PType.width_packed_cons, PDim.width, evalInt,
    soEnv, soScope, List.lookup, soDeclsW, Gen2.except_ok_bind]

theorem so_elems (N W : Int) : buildElems (soEnv N W) design.pdesign.decls = .ok soElems := by
  simp [design.pdesign, buildElems, PType.width_packed_cons, PDim.width, evalInt, soEnv,
    soScope, List.lookup, soElems, Gen2.except_ok_bind]

/-- The instantiation environment. -/
abbrev soE (N W : Nat) : IEnv := (soEnv N W).withDecls (soDecls N W)

/-- The cell template (the process inside `gen_cell`). -/
def cellT : PProcess :=
  match design.pdesign.generates with
  | [.genFor _ _ _ _ _ _ [.process p]] => p
  | _ => .alwaysFF "" (.block [])

macro "so_simp" : tactic => `(tactic| sv2_inst_simp [evalSized, ctype, evalAt, ctypeList, evalAtList,
  SymBinOp.constClass, PExpr.pushedTarget, PExpr.readsSignal, PExpr.readsSignalList, Gen2.except_pure,
  Lib.min_add_sub_one_self, Lib.max_add_sub_one_self, Lib.add_sub_one_sub_add_one, instStmt2, instStmts2,
  design.pdesign, soEnv, soScope, soDeclsW, soElems,
  topP, outP, cellP, cellT, dimTable, dimTableStep, PType.width_packed_cons, PDim.width, ctxOpWidth2, rigidMax2,
  PExpr.ctxPropagates, PExpr.constLeaf, PExpr.negGenvarWidened, LVec.width, *])

/-- Window facts of `data[lo +: W]` inside `N·W` bits, for the instantiation `simp`. -/
theorem so_win {N W lo : Nat} (h : lo + W ≤ N * W) (hW : 1 ≤ W) (x : Int) (hx : (lo : Int) = x) :
    0 ≤ x ∧ x.toNat = lo ∧ x + W - 1 < N * W ∧ 1 ≤ x + W ∧ (x + W).toNat = lo + W :=
  Lib.window_bounds_of_natCast x (N * W) h hW hx (by simp)

/-- The facts every instantiation `simp` here needs. -/
theorem inst_facts {N W : Nat} (hN : 1 ≤ N) (hW : 1 ≤ W) : ((0 : Int) < W ∧ 0 < W ∧ (1 : Int) ≤ N * W) ∧
    ((N : Int) * W - 1).natAbs + 1 = N * W ∧ (PartMode.up == PartMode.range) = false ∧
    ((N : Int) - 1).natAbs + 1 = N :=
  ⟨⟨by omega, hW, by have := Nat.mul_pos hN hW; omega⟩,
    by rw [← Int.natCast_mul]; exact Lib.natAbs_sub_one_add_one (Nat.mul_pos hN hW), rfl, Lib.natAbs_sub_one_add_one hN⟩

theorem so_static (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) :
    design.pdesign.processes.map (instProcess2 (soE N W) soElems) = [topP N W, outP W] := by
  obtain ⟨⟨h1, h2, h3⟩, h4, h5, h6⟩ := inst_facts hN hW
  obtain ⟨h7, h8, h9, h10, h11⟩ : ((1 : Int) ≤ N ∧ 0 < N ∧ (0 : Int) ≤ N - 1 ∧ (N : Int) - 1 < N) ∧
      ((N : Int) - 1).toNat = N - 1 ∧ max ((W : Int) - 1) 0 = W - 1 ∧ min ((W : Int) - 1) 0 = 0 ∧
      ((W : Int) - 1 - 0 + 1).toNat = W := by omega
  have hd := so_win (N := N) (W := W) (lo := (N - 1) * W)
    (Nat.le_of_eq (by rw [← Nat.succ_mul, Nat.succ_eq_add_one, Nat.sub_add_cancel hN])) hW
    (((N : Int) - 1) * W) (by rw [Int.natCast_mul, Int.ofNat_sub hN]; rfl)
  so_simp
  try and_intros
  all_goals first | rfl | decide | omega | skip

theorem cell_inst (N W k : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hk : k + 1 < N) :
    instProcess2 ((soE N W).bindVal "k" k) soElems cellT = cellP W k := by
  obtain ⟨⟨h1, h2, h3⟩, h4, h5, h6⟩ := inst_facts hN hW
  have hk : (k : Int) + 1 < N ∧ (k : Int) < N := by omega
  have hle := Nat.mul_le_mul_right W (show k + 1 + 1 ≤ N by omega)
  rw [Nat.add_mul, Nat.add_mul, Nat.one_mul] at hle
  have ha := so_win (N := N) (W := W) (lo := (k + 1) * W) (by rw [Nat.add_mul, Nat.one_mul]; omega) hW
    (((k : Int) + 1) * W) (by simp)
  have hb := so_win (N := N) (W := W) (lo := k * W) (by omega) hW ((k : Int) * W) (by simp)
  so_simp
  try and_intros
  all_goals first | rfl | decide

/-- `for (k = 0; k < N - 1; k++)` over the cell template. -/
theorem so_gens_src : design.pdesign.generates = [.genFor (some "gen_cell") "k" (.int 0)
    (.binary .slt (.genvarRef "k") (.binary (.m0 .sub) (.paramRef "N" none) (.int 1)))
    (.unary .inc (.genvarRef "k")) (some 7) ([cellT].map .process)] := rfl

/-- **The generate expands to the cells `0 … N-2`** (none at `N = 1`). -/
theorem so_gens (N W F : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hF : N < F) :
    expandList2 (soE N W) soElems F design.pdesign.generates = .ok ((List.range (N - 1)).map (cellP W)) := by
  have hNv : ∀ i : Int, ((soE N W).bindVal "k" i).vals.lookup "N" = some (N : Int) := fun i => rfl
  rw [so_gens_src]
  apply expandList2_singleton_ok
  rw [GenItem.expand2_genFor_ascending_processes (N := (N : Int) - 1) (evalInt_int 0)
    (fun i => isInt_binary_of rfl (isInt_paramRef_of (hNv i)) rfl)
    (fun i => evalInt_sub_of (isInt_paramRef_of (hNv i)) rfl (evalInt_paramRef_of (hNv i)) rfl) (by omega)]
  have ht : ((N : Int) - 1 - 0).toNat = N - 1 := by omega
  simp only [ht, intRange_zero, List.flatMap_map, List.map_cons, List.map_nil, Gen2.flatMap_singleton_map]
  congr 1
  exact List.map_congr_left fun k hk => cell_inst N W k hN hW (by have := List.mem_range.mp hk; omega)

theorem so_instantiate2 (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) :
    design.pdesign.instantiate2 [(N : Int), W] (PDesign.surfaceFuel [(N : Int), W]) =
      .ok (design.pdesign.assemble2 (soEnv N W) (soDecls N W) soElems ((List.range (N - 1)).map (cellP W))) := by
  have hd := so_decls N W
  rw [Lib.natAbs_sub_one_add_one hW, ← Int.natCast_mul, Lib.natAbs_sub_one_add_one (Nat.mul_pos hN hW),
    Lib.natAbs_sub_one_add_one hN] at hd
  refine PDesign.instantiate2_of_ok rfl (so_paramEnv _ _) hd (so_elems _ _) (so_gens N W _ hN hW ?_)
  simp only [PDesign.surfaceFuel, List.map, List.sum_cons, List.sum_nil, Int.natAbs_natCast]
  have := Nat.le_mul_self (N + (W + 0) + 2)
  omega

theorem so_processes (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) :
    (design.pdesign.instantiateD2 [(N : Int), W]).processes.toList =
      topP N W :: outP W :: (List.range (N - 1)).map (cellP W) := by
  rw [PDesign.instantiateD2_of_ok (so_instantiate2 N W hN hW), PDesign.assemble2_processes,
    so_static N W hN hW]
  simp [design.pdesign]

/-- Two cells drive disjoint windows. -/
theorem cell_disj {W k k' : Nat} (h : k < k') :
    ∀ a ∈ (cellP W k).procWins, ∀ b ∈ (cellP W k').procWins, a.overlaps b = false := by
  have := Nat.mul_le_mul_right W (show k + 1 ≤ k' by omega)
  rw [Nat.add_mul, Nat.one_mul] at this
  simp [cellP, Process2.procWins, Stmt2.drvWins, Stmt2.drvWinsOpt, Stmt2.drvWinsList, Lhs2.drvWins,
    DrvWin.overlaps]
  omega

/-- The top cell and the output register drive no window of a cell `k < N - 1`. -/
theorem top_disj {N W k : Nat} (h : k + 1 < N) :
    (∀ a ∈ (topP N W).procWins, ∀ b ∈ (cellP W k).procWins, a.overlaps b = false) ∧
      ∀ a ∈ (outP W).procWins, ∀ b ∈ (cellP W k).procWins, a.overlaps b = false := by
  have := Nat.mul_le_mul_right W (show k + 1 ≤ N - 1 by omega)
  rw [Nat.add_mul, Nat.one_mul] at this
  constructor <;>
  simp [topP, outP, cellP, Process2.procWins, Stmt2.drvWins, Stmt2.drvWinsOpt, Stmt2.drvWinsList,
    Lhs2.drvWins, DrvWin.overlaps] <;> omega

theorem so_pairwise (N W : Nat) : (topP N W :: outP W :: (List.range (N - 1)).map (cellP W)).Pairwise
    fun p q => ∀ a ∈ p.procWins, ∀ b ∈ q.procWins, a.overlaps b = false := by
  refine .cons (fun p hp => ?_) (.cons (fun p hp => ?_) ?_)
  · rcases List.mem_cons.mp hp with rfl | hp
    · simp [topP, outP, Process2.procWins, Stmt2.drvWins, Stmt2.drvWinsOpt, Stmt2.drvWinsList,
        Lhs2.drvWins, DrvWin.overlaps]
    · obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hp
      exact (top_disj (by have := List.mem_range.mp hk; omega)).1
  · obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hp
    exact (top_disj (N := N) (by have := List.mem_range.mp hk; omega)).2
  · exact List.pairwise_map.mpr (List.pairwise_lt_range.imp_of_mem fun _ _ h => cell_disj h)

theorem so_driversOk (N W : Nat) :
    driversOk design.pdesign.declNames design.pdesign.inputNames
      (topP N W :: outP W :: (List.range (N - 1)).map (cellP W)) = true := by
  apply driversOk_of_ff ?_ ?_ (so_pairwise N W)
  · intro p hp
    rcases List.mem_cons.mp hp with rfl | hp
    · exact ⟨_, _, rfl⟩
    rcases List.mem_cons.mp hp with rfl | hp
    · exact ⟨_, _, rfl⟩
    · obtain ⟨k, -, rfl⟩ := List.mem_map.mp hp; exact ⟨_, _, rfl⟩
  · simp only [List.mem_flatMap, List.mem_cons, List.mem_map]
    rintro n ⟨p, hp | hp | ⟨k, -, rfl⟩, hn⟩
    all_goals try subst hp
    all_goals revert n; simp [topP, outP, cellP, Process2.procWrites, Process2.procWins, Stmt2.drvWins,
      Stmt2.drvWinsOpt, Stmt2.drvWinsList, Lhs2.drvWins]; all_goals decide

/-- **The loaded family is `soD`**, at every `(N, W)` with positive parameters. -/
theorem so_sem_eq (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) : design.sem N W = soD N W := by
  have h1 : design.sem N W = design.pdesign.instantiateD2 [(N : Int), W] := by
    show design.pdesign.instantiateGD2 [(N : Int), W] = _
    exact PDesign.instantiateGD2_of_driversOk (by rw [so_processes N W hN hW]; exact so_driversOk N W)
  rw [h1, PDesign.instantiateD2_of_ok (so_instantiate2 N W hN hW)]
  simp only [PDesign.assemble2, so_static N W hN hW, soD]
  simp [design.pdesign]

/-! ## 2. G0's clock step for the loaded family -/

theorem so_profile (N W : Nat) (hN : 1 ≤ N) : (soD N W).ffOnlyProfileB = true := by
  simp only [Design2.ffOnlyProfileB, Bool.and_eq_true]
  refine ⟨?_, ffDisjB_of_pairwise (by simpa [soD] using so_pairwise N W)⟩
  have h1 := Nat.mul_le_mul_right W (show N - 1 + 1 ≤ N by omega)
  rw [Nat.add_mul, Nat.one_mul] at h1
  simp [soD, topP, outP, cellP, List.all_map, Stmt2.nbaOnly, Stmt2.optNbaOnly,
    Stmt2.listNbaOnly, Stmt2.nbaStaticB, Stmt2.optNbaStaticB, Stmt2.listNbaStaticB, Lhs2.window?,
    Design2.declWidth, Design2.inputNames, Stmt2.drvWins, Stmt2.drvWinsOpt, Stmt2.drvWinsList,
    Lhs2.drvWins, soDeclsW]

/-- The 9 signals of `soD`, in declaration order. -/
def SS (ck r s iv id ov od dt tk : LVec) : SvState :=
  [("clk", ck), ("rst", r), ("start", s), ("in_valid", iv), ("in_data", id), ("out_valid", ov),
    ("out_data", od), ("data", dt), ("tok", tk)]

theorem apply_so (N W : Nat) (e : SvState) (ck r s iv id ov od dt tk : LVec) :
    applyInputs2 (soD N W) e (SS ck r s iv id ov od dt tk) = SS (appIn e "clk" ck) (appIn e "rst" r)
      (appIn e "start" s) (appIn e "in_valid" iv) (appIn e "in_data" id) ov od dt tk := by
  unfold applyInputs2
  rw [← Array.foldl_toList]
  cases h1 : SvState.lookup e "clk" <;> cases h2 : SvState.lookup e "rst" <;>
    cases h3 : SvState.lookup e "start" <;> cases h4 : SvState.lookup e "in_valid" <;>
    cases h5 : SvState.lookup e "in_data" <;>
    simp [soD, soDeclsW, SS, appIn, h1, h2, h3, h4, h5, SvState.set]

/-- An `in_data > x` test, as the clock step evaluates it. -/
abbrev gtc (a b : LVec) : Bool := (LVec.ofLogic (a.gt b)).condTrue

/-- The top cell's updates, from the pre-edge values. -/
def topQ (N W : Nat) (r iv id dt : LVec) : NbaQueue2 :=
  (if iv.condTrue then (if gtc id (dt.extract ((N - 1) * W) W) then [("data", (N - 1) * W, id.resizeU W)] else [])
    else [("data", (N - 1) * W, .ofBitVec 0#W)]) ++ ("tok", N - 1, iv.resizeU 1) ::
  (if r.condTrue then [("data", (N - 1) * W, .ofBitVec 0#W), ("tok", N - 1, .ofBitVec 0#1)] else [])

/-- The output register's updates. -/
def outQ (W : Nat) (r ov od dt tk : LVec) : NbaQueue2 :=
  ("out_valid", 0, (tk.extract 0 1).resizeU ov.width) :: ("out_data", 0, (dt.extract 0 W).resizeU od.width) ::
  (if r.condTrue then [("out_valid", 0, .ofBitVec 0#ov.width)] else [])

/-- Cell `k`'s updates. -/
def cellQ (W : Nat) (r iv id dt tk : LVec) (k : Nat) : NbaQueue2 :=
  (if iv.condTrue then
      (if gtc id (dt.extract ((k + 1) * W) W) then [("data", k * W, (dt.extract ((k + 1) * W) W).resizeU W)]
      else if gtc id (dt.extract (k * W) W) then [("data", k * W, id.resizeU W)] else [])
    else [("data", k * W, (dt.extract ((k + 1) * W) W).resizeU W)]) ++
  ("tok", k, (tk.extract (k + 1) 1).resizeU 1) ::
  (if r.condTrue then [("data", k * W, .ofBitVec 0#W), ("tok", k, .ofBitVec 0#1)] else [])

section run
variable (F : Nat) (hF : 30 ≤ F) (ck r s iv id ov od dt tk : LVec)
include hF

theorem out_run (W : Nat) : runEdgeProcess2 F (SS ck r s iv id ov od dt tk) [] (outP W) =
    .ok (SS ck r s iv id ov od dt tk, outQ W r ov od dt tk) := by
  obtain ⟨f, rfl⟩ : ∃ f, F = f + 30 := ⟨F - 30, by omega⟩
  by_cases h1 : r.condTrue = true <;>
    simp [outP, outQ, runEdgeProcess2, execStmt2, execStmts2, evalExpr2, resolveLhs2, readSignal, SS,
      SvState.lookup, h1]

theorem top_run (N W : Nat) : runEdgeProcess2 F (SS ck r s iv id ov od dt tk) [] (topP N W) =
    .ok (SS ck r s iv id ov od dt tk, topQ N W r iv id dt) := by
  obtain ⟨f, rfl⟩ : ∃ f, F = f + 30 := ⟨F - 30, by omega⟩
  by_cases h1 : r.condTrue = true <;> by_cases h2 : iv.condTrue = true <;>
    by_cases h3 : gtc id (dt.extract ((N - 1) * W) W) = true <;>
    simp [topP, topQ, runEdgeProcess2, execStmt2, execStmts2, evalExpr2, resolveLhs2, readSignal, SS,
      SvState.lookup, evalBinOp, h1, h2, h3]

theorem cell_run (W k : Nat) : runEdgeProcess2 F (SS ck r s iv id ov od dt tk) [] (cellP W k) =
    .ok (SS ck r s iv id ov od dt tk, cellQ W r iv id dt tk k) := by
  obtain ⟨f, rfl⟩ : ∃ f, F = f + 30 := ⟨F - 30, by omega⟩
  by_cases h1 : r.condTrue = true <;> by_cases h2 : iv.condTrue = true <;>
    by_cases h3 : gtc id (dt.extract ((k + 1) * W) W) = true <;>
    by_cases h4 : gtc id (dt.extract (k * W) W) = true <;>
    simp [cellP, cellQ, runEdgeProcess2, execStmt2, execStmts2, evalExpr2, resolveLhs2, readSignal, SS,
      SvState.lookup, evalBinOp, h1, h2, h3, h4]

end run

/-- The cycle's updates, in process order. -/
def Q (N W : Nat) (r iv id ov od dt tk : LVec) : NbaQueue2 :=
  topQ N W r iv id dt ++ outQ W r ov od dt tk ++ (List.range (N - 1)).flatMap (cellQ W r iv id dt tk)

/-- One cycle's next state, from the pre-edge (inputs applied) values. -/
def soNext (N W : Nat) (ck r s iv id ov od dt tk : LVec) : SvState :=
  commitNba2 (SS ck r s iv id ov od dt tk) (Q N W r iv id ov od dt tk)

/-- **One cycle of the loaded design is G0's clock step**, evaluated (any schedule, any stimulus
entry, any state of the design's shape, every fuel from 30). -/
theorem so_cycle (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (σ : ScheduleOracle) (e : SvState)
    (ck r s iv id ov od dt tk : LVec) (kk F : Nat) (hF : 30 ≤ F) :
    cycleStep2 (design.sem N W) σ F e (SS ck r s iv id ov od dt tk) kk =
      .ok (soNext N W (appIn e "clk" ck) (appIn e "rst" r) (appIn e "start" s) (appIn e "in_valid" iv)
        (appIn e "in_data" id) ov od dt tk, kk + 3) := by
  have hmem : ∀ p ∈ (soD N W).processes.toList, p = topP N W ∨ p = outP W ∨ ∃ k, p = cellP W k := by
    intro p hp
    simp only [soD, List.toList_toArray, List.mem_cons, List.mem_map] at hp
    rcases hp with rfl | rfl | ⟨k, -, rfl⟩ <;>
      first | exact .inl rfl | exact .inr (.inl rfl) | exact .inr (.inr ⟨_, rfl⟩)
  have hedge : ∀ p ∈ (soD N W).processes.toList, p.isEdgePhase = true := by
    intro p hp; rcases hmem p hp with rfl | rfl | ⟨k, rfl⟩ <;> rfl
  rw [so_sem_eq N W hN hW, cycleStep2_profile (so_profile N W hN) σ e _ kk ?_ ?_ (by omega),
    apply_so, clockStep, flatMap_ffUpd F _ hedge]
  · simp only [soD, List.toList_toArray, List.flatMap_cons, top_run F hF, out_run F hF, List.flatMap_map,
      cell_run F hF, soNext, Q, List.append_assoc]
  · intro i p hp
    rw [apply_so]
    rcases hmem p (List.mem_of_getElem? (by simpa using hp)) with rfl | rfl | ⟨k, rfl⟩
    · exact ⟨_, top_run F hF _ _ _ _ _ _ _ _ _ N W⟩
    · exact ⟨_, out_run F hF _ _ _ _ _ _ _ _ _ W⟩
    · exact ⟨_, cell_run F hF _ _ _ _ _ _ _ _ _ W k⟩
  · rw [apply_so]; simp [SS]

/-! ## 3. The commit, register by register (`nbaFold`, `LeanModels.Sv.SeqFamily`) -/

section commit
variable {ck r s iv id ov od dt tk : LVec} {lo : Nat} {v : LVec}
theorem nb_ov : nbaStep (SS ck r s iv id ov od dt tk) ("out_valid", lo, v) = SS ck r s iv id (ov.insertAt lo v) od dt tk := by
  simp [nbaStep, SS, SvState.lookup, SvState.set]
theorem nb_od : nbaStep (SS ck r s iv id ov od dt tk) ("out_data", lo, v) = SS ck r s iv id ov (od.insertAt lo v) dt tk := by
  simp [nbaStep, SS, SvState.lookup, SvState.set]
theorem nb_dt : nbaStep (SS ck r s iv id ov od dt tk) ("data", lo, v) = SS ck r s iv id ov od (dt.insertAt lo v) tk := by
  simp [nbaStep, SS, SvState.lookup, SvState.set]
theorem nb_tk : nbaStep (SS ck r s iv id ov od dt tk) ("tok", lo, v) = SS ck r s iv id ov od dt (tk.insertAt lo v) := by
  simp [nbaStep, SS, SvState.lookup, SvState.set]
end commit

/-- Committing a queue of writes to the four registers. -/
theorem commit_SS {ck r s iv id : LVec} : ∀ (q : NbaQueue2) (ov od dt tk : LVec),
    (∀ u ∈ q, u.1 = "out_valid" ∨ u.1 = "out_data" ∨ u.1 = "data" ∨ u.1 = "tok") →
    commitNba2 (SS ck r s iv id ov od dt tk) q =
      SS ck r s iv id (nbaFold "out_valid" q ov) (nbaFold "out_data" q od) (nbaFold "data" q dt) (nbaFold "tok" q tk)
  | [], _, _, _, _, _ => rfl
  | ⟨n, lo, v⟩ :: q, ov, od, dt, tk, h => by
    have hq := @commit_SS ck r s iv id q
    have h' := fun u hu => h u (List.mem_cons_of_mem _ hu)
    rcases h _ List.mem_cons_self with h1 | h1 | h1 | h1 <;> simp only at h1 <;> subst h1 <;>
      simp [commitNba2_cons, nb_ov, nb_od, nb_dt, nb_tk, hq _ _ _ _ h', nbaFold]

/-! ## 4. The registers through a cycle -/

attribute [local simp] condTrue_knownBit

/-- A cell's load rule: take the pushed upper neighbour's value, or the input, or hold. -/
def hwCell {W : Nat} (N : Nat) (x : BitVec W) (v : Nat → BitVec W) (k : Nat) : BitVec W :=
  if k + 1 < N then (if v (k + 1) < x then v (k + 1) else if v k < x then x else v k)
  else if v k < x then x else v k

/-- The cells after a cycle without reset: a load of `x` (`b`), or a drain (shift down, `0` in). -/
def cstep {W : Nat} (N : Nat) (b : Bool) (x : BitVec W) (v : Nat → BitVec W) (k : Nat) : BitVec W :=
  if b then hwCell N x v k else if k + 1 < N then v (k + 1) else 0

/-- The tokens after a cycle without reset: shift down, `in_valid` in at the top. -/
def tstep (N : Nat) (b : Bool) (T : Nat → BitVec 1) (k : Nat) : BitVec 1 :=
  if k + 1 < N then T (k + 1) else BitVec.ofBool b

theorem so_names (N W : Nat) (r iv id ov od dt tk : LVec) : ∀ u ∈ Q N W r iv id ov od dt tk,
    u.1 = "out_valid" ∨ u.1 = "out_data" ∨ u.1 = "data" ∨ u.1 = "tok" := by
  have h : ∀ q : NbaQueue2, q.all (fun u => u.1 == "out_valid" || u.1 == "out_data" || u.1 == "data" ||
      u.1 == "tok") = true → ∀ u ∈ q, u.1 = "out_valid" ∨ u.1 = "out_data" ∨ u.1 = "data" ∨ u.1 = "tok" :=
    fun q h u hu => by simpa [or_assoc] using List.all_eq_true.mp h u hu
  refine h _ ?_
  simp only [Q, List.all_append, List.all_flatMap, Bool.and_eq_true]
  refine ⟨⟨?_, ?_⟩, List.all_eq_true.mpr fun k _ => ?_⟩
  · unfold topQ; (repeat' split) <;> simp
  · unfold outQ; (repeat' split) <;> simp
  · unfold cellQ; (repeat' split) <;> simp

section skip
variable {n : String} (x : LVec)
theorem top_skip (h1 : n ≠ "data") (h2 : n ≠ "tok") (N W : Nat) (r iv id dt : LVec) :
    nbaFold n (topQ N W r iv id dt) x = x := by
  unfold topQ; (repeat' split) <;> simp [nbaFold, Ne.symm h1, Ne.symm h2]
theorem cell_skip (h1 : n ≠ "data") (h2 : n ≠ "tok") (W : Nat) (r iv id dt tk : LVec) (k : Nat) :
    nbaFold n (cellQ W r iv id dt tk k) x = x := by
  unfold cellQ; (repeat' split) <;> simp [nbaFold, Ne.symm h1, Ne.symm h2]
end skip

/-- The output register's signals: only `outQ` writes them. -/
theorem fdQ_out (n : String) (h1 : n ≠ "data") (h2 : n ≠ "tok") {N W : Nat} {r iv id ov od dt tk : LVec}
    (x : LVec) : nbaFold n (Q N W r iv id ov od dt tk) x = nbaFold n (outQ W r ov od dt tk) x := by
  rw [Q, nbaFold_append, nbaFold_append, top_skip x h1 h2,
    nbaFold_flatMap_eq_self (fun k y => cell_skip y h1 h2 W r iv id dt tk k)]

/-- The cell array's signals: the top cell, then the cells `0 … N-2`. -/
theorem fdQ_reg (n : String) (h1 : n ≠ "out_valid") (h2 : n ≠ "out_data") {N W : Nat} {r iv id ov od dt tk : LVec}
    (x : LVec) : nbaFold n (Q N W r iv id ov od dt tk) x =
      (List.range (N - 1)).foldl (fun acc k => nbaFold n (cellQ W r iv id dt tk k) acc) (nbaFold n (topQ N W r iv id dt) x) := by
  have : nbaFold n (outQ W r ov od dt tk) = fun y => y := by
    funext y; unfold outQ; (repeat' split) <;> simp [nbaFold, Ne.symm h1, Ne.symm h2]
  rw [Q, nbaFold_append, nbaFold_append, this, nbaFold_flatMap]

theorem gtc_ofBitVec {W : Nat} (a b : BitVec W) : gtc (.ofBitVec a) (.ofBitVec b) = decide (b < a) := by
  by_cases h : b < a <;> simp [gtc, h]

attribute [local simp] gtc_ofBitVec

theorem cell_data {N W k : Nat} (hk : k + 1 < N) (b : Bool) (x : BitVec W) (v u : Nat → BitVec W)
    (hu : u k = v k) (id tk : LVec) (hid : b = true → id = .ofBitVec x) :
    nbaFold "data" (cellQ W (knownBit false) (knownBit b) id (.ofBitVec (packBV W N v)) tk k)
        (.ofBitVec (packBV W N u)) =
      .ofBitVec (packBV W N (fun i => if i = k then cstep N b x v k else u i)) := by
  have e1 := extract_ofBitVec_packBV (W := W) v hk rfl
  have e0 := extract_ofBitVec_packBV (W := W) v (show k < N by omega) rfl
  have hup := fun a => bvInsertAt_packBV (W := W) u a (show k < N by omega) rfl
  have hold : packBV W N (fun i => if i = k then v k else u i) = packBV W N u :=
    congrArg _ (funext fun i => by split <;> simp_all)
  cases b
  · simp [cellQ, nbaFold, e1, cstep, hk, hup]
  · obtain rfl := hid rfl
    by_cases h1 : v (k + 1) < x <;> by_cases h2 : v k < x <;>
      simp [cellQ, nbaFold, e1, e0, cstep, hwCell, hk, h1, h2, hup, hold]

theorem top_data {N W : Nat} (hN : 1 ≤ N) (b : Bool) (x : BitVec W) (v u : Nat → BitVec W)
    (hu : u (N - 1) = v (N - 1)) (id : LVec) (hid : b = true → id = .ofBitVec x) :
    nbaFold "data" (topQ N W (knownBit false) (knownBit b) id (.ofBitVec (packBV W N v))) (.ofBitVec (packBV W N u)) =
      .ofBitVec (packBV W N (fun i => if i = N - 1 then cstep N b x v (N - 1) else u i)) := by
  have e0 := extract_ofBitVec_packBV (W := W) v (show N - 1 < N by omega) rfl
  have hup := fun a => bvInsertAt_packBV (W := W) u a (show N - 1 < N by omega) rfl
  have hold : packBV W N (fun i => if i = N - 1 then v (N - 1) else u i) = packBV W N u :=
    congrArg _ (funext fun i => by split <;> simp_all)
  have hn : ¬ (N - 1 + 1 < N) := by omega
  cases b
  · simp [topQ, nbaFold, cstep, hn, hup]
  · obtain rfl := hid rfl
    by_cases h2 : v (N - 1) < x <;> simp [topQ, nbaFold, e0, cstep, hwCell, hn, h2, hup, hold]

theorem cell_tok {N W k : Nat} (hk : k + 1 < N) (iv id dt : LVec) (T u : Nat → BitVec 1) :
    nbaFold "tok" (cellQ W (knownBit false) iv id dt (.ofBitVec (packBV 1 N T)) k) (.ofBitVec (packBV 1 N u)) =
      .ofBitVec (packBV 1 N (fun i => if i = k then T (k + 1) else u i)) := by
  have e := extract_ofBitVec_packBV T hk (Nat.mul_one _).symm
  have hup := bvInsertAt_packBV u (T (k + 1)) (show k < N by omega) (Nat.mul_one k).symm
  simp only [cellQ, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte]; (repeat' split) <;> simp [nbaFold, e, hup]

theorem top_tok {N W : Nat} (hN : 1 ≤ N) (b : Bool) (id dt : LVec) (u : Nat → BitVec 1) :
    nbaFold "tok" (topQ N W (knownBit false) (knownBit b) id dt) (.ofBitVec (packBV 1 N u)) =
      .ofBitVec (packBV 1 N (fun i => if i = N - 1 then BitVec.ofBool b else u i)) := by
  have hup := bvInsertAt_packBV u (BitVec.ofBool b) (show N - 1 < N by omega) (Nat.mul_one _).symm
  simp only [topQ, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte]; (repeat' split) <;> simp [nbaFold, hup]

section reset
variable (x : LVec)
theorem top_reset (N W : Nat) (iv id dt : LVec) :
    nbaFold "data" (topQ N W (knownBit true) iv id dt) x = x.insertAt ((N - 1) * W) (.ofBitVec 0#W) ∧
      nbaFold "tok" (topQ N W (knownBit true) iv id dt) x = x.insertAt ((N - 1) * 1) (.ofBitVec 0#1) := by
  simp only [topQ, condTrue_knownBit, ↓reduceIte]; (repeat' split) <;>
    simp [nbaFold, LVec.insertAt_insertAt_of_width_le]
theorem cell_reset (W : Nat) (iv id dt tk : LVec) (k : Nat) :
    nbaFold "data" (cellQ W (knownBit true) iv id dt tk k) x = x.insertAt (k * W) (.ofBitVec 0#W) ∧
      nbaFold "tok" (cellQ W (knownBit true) iv id dt tk k) x = x.insertAt (k * 1) (.ofBitVec 0#1) := by
  simp only [cellQ, condTrue_knownBit, ↓reduceIte]; (repeat' split) <;>
    simp [nbaFold, LVec.insertAt_insertAt_of_width_le]
end reset

/-- The cells (or tokens) all `0`. -/
abbrev Z (W N : Nat) : LVec := .ofBitVec (packBV W N fun _ => 0)

/-- **A reset cycle** clears the cells, the tokens and `out_valid`. -/
theorem next_reset {N W : Nat} (hN : 1 ≤ N) (ck s iv id ov od dt tk : LVec) (hov : ov.width = 1)
    (hdt : dt.width = N * W) (htk : tk.width = N) :
    ∃ od', soNext N W ck (knownBit true) s iv id ov od dt tk =
      SS ck (knownBit true) s iv id (knownBit false) od' (Z W N) (Z 1 N) := by
  have h0 : LVec.ofBitVec 0#ov.width = knownBit false := by rw [← LVec.replicate_l0, hov]; decide
  rw [soNext, commit_SS _ _ _ _ _ (so_names _ _ _ _ _ _ _ _ _), fdQ_out "out_valid" (by decide) (by decide),
    fdQ_reg "data" (by decide) (by decide), fdQ_reg "tok" (by decide) (by decide), (top_reset ..).1, (top_reset ..).2]
  simp only [(cell_reset ..).1, (cell_reset ..).2]
  rw [LVec.foldl_range_insertAt_last hN _ dt (by simp), LVec.insertEntries_ofBitVec (fun _ => 0#W) dt hdt,
    LVec.foldl_range_insertAt_last hN _ tk (by simp), LVec.insertEntries_ofBitVec (fun _ => 0#1) tk (by simp [htk])]
  refine ⟨nbaFold "out_data" (Q N W (knownBit true) iv id ov od dt tk) od, ?_⟩
  congr 1
  simp [outQ, nbaFold, LVec.insertAt_zero_of_width_eq, hov, h0]

theorem data_fold {N W : Nat} (hN : 1 ≤ N) (b : Bool) (x : BitVec W) (v : Nat → BitVec W) (id tk : LVec)
    (hid : b = true → id = .ofBitVec x) :
    (List.range (N - 1)).foldl
        (fun acc k => nbaFold "data" (cellQ W (knownBit false) (knownBit b) id (.ofBitVec (packBV W N v)) tk k) acc)
      (nbaFold "data" (topQ N W (knownBit false) (knownBit b) id (.ofBitVec (packBV W N v)))
        (.ofBitVec (packBV W N v))) =
      .ofBitVec (packBV W N (cstep N b x v)) := by
  rw [top_data hN b x v v rfl id hid,
    foldl_range_ofBitVec_packBV (W := W) (N := N) _ (cstep N b x v) _ (N - 1) ?_]
  · refine congrArg _ (packBV_congr fun i hi => ?_)
    by_cases h : i < N - 1
    · simp [h]
    · obtain rfl : i = N - 1 := by omega
      simp
  · intro k u' hk hu'
    exact cell_data (by omega) b x v u' (by rw [hu']; simp [show k ≠ N - 1 by omega]) id tk hid

theorem tok_fold {N W : Nat} (hN : 1 ≤ N) (b : Bool) (T : Nat → BitVec 1) (id dt : LVec) :
    (List.range (N - 1)).foldl
        (fun acc k => nbaFold "tok" (cellQ W (knownBit false) (knownBit b) id dt (.ofBitVec (packBV 1 N T)) k) acc)
      (nbaFold "tok" (topQ N W (knownBit false) (knownBit b) id dt) (.ofBitVec (packBV 1 N T))) =
      .ofBitVec (packBV 1 N (tstep N b T)) := by
  rw [top_tok hN b id dt T,
    foldl_range_ofBitVec_packBV (W := 1) (N := N) _ (fun k => T (k + 1)) _ (N - 1) ?_]
  · refine congrArg _ (packBV_congr fun i hi => ?_)
    by_cases h : i < N - 1
    · simp [h, tstep, show i + 1 < N by omega]
    · obtain rfl : i = N - 1 := by omega
      simp [tstep, show ¬ (N - 1 + 1 < N) by omega]
  · intro k u' hk _
    exact cell_tok (by omega) _ _ _ T u'

/-- **A cycle without reset** on known cells and tokens: a load of `x` (`b`) or a drain. -/
theorem next_run {N W : Nat} (hN : 1 ≤ N) (b : Bool) (x : BitVec W) (v : Nat → BitVec W) (T : Nat → BitVec 1)
    (ck s id ov od : LVec) (hid : b = true → id = .ofBitVec x) (hov : ov.width = 1) (hod : od.width = W) :
    soNext N W ck (knownBit false) s (knownBit b) id ov od (.ofBitVec (packBV W N v)) (.ofBitVec (packBV 1 N T)) =
      SS ck (knownBit false) s (knownBit b) id (.ofBitVec (T 0)) (.ofBitVec (v 0))
        (.ofBitVec (packBV W N (cstep N b x v))) (.ofBitVec (packBV 1 N (tstep N b T))) := by
  rw [soNext, commit_SS _ _ _ _ _ (so_names _ _ _ _ _ _ _ _ _), fdQ_out "out_valid" (by decide) (by decide),
    fdQ_out "out_data" (by decide) (by decide), fdQ_reg "data" (by decide) (by decide),
    fdQ_reg "tok" (by decide) (by decide), data_fold hN b x v id _ hid, tok_fold hN b T id _]
  simp [outQ, nbaFold, extract_ofBitVec_packBV T (show 0 < N by omega) (Nat.zero_mul 1).symm,
    extract_ofBitVec_packBV v (show 0 < N by omega) (Nat.zero_mul W).symm, hov, hod, LVec.insertAt_zero_of_width_eq]

/-! ## 5. Shape and termination -/

/-- A snapshot of the design's shape (register widths; any values, `x` included). -/
def I (N W : Nat) (st : SvState) : Prop :=
  ∃ ck r s iv id ov od dt tk, st = SS ck r s iv id ov od dt tk ∧
    (ov.width = 1 ∧ od.width = W ∧ dt.width = N * W ∧ tk.width = N)

theorem next_I {N W : Nat} (ck r s iv id ov od dt tk : LVec)
    (hw : ov.width = 1 ∧ od.width = W ∧ dt.width = N * W ∧ tk.width = N) :
    I N W (soNext N W ck r s iv id ov od dt tk) := by
  rw [soNext, commit_SS _ _ _ _ _ (so_names _ _ _ _ _ _ _ _ _)]
  exact ⟨_, _, _, _, _, _, _, _, _, rfl, by simp [width_nbaFold, hw]⟩

theorem so_init (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) : I N W (initState2 (design.sem N W)) := by
  rw [so_sem_eq N W hN hW]
  exact ⟨.xVec 1, .xVec 1, .xVec 1, .xVec 1, .xVec W, .xVec 1, .xVec W, .xVec (N * W), .xVec N,
    by simp [initState2, soD, soDeclsW, SS], by simp⟩

/-- **Termination**: every schedule and every stimulus completes. -/
theorem so_terminates (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) : Terminates2 (design.sem N W) := by
  refine Terminates2.of_invariant (I N W) (so_init N W hN hW) (fun σ => ⟨30, ?_⟩) ?_
  · rintro e _ kk ⟨ck, r, s, iv, id, ov, od, dt, tk, rfl, hw⟩
    exact ⟨_, _, so_cycle N W hN hW σ e ck r s iv id ov od dt tk kk 30 (Nat.le_refl _), next_I _ _ _ _ _ _ _ _ _ hw⟩
  · rw [so_sem_eq N W hN hW]
    simp [soD, topP, outP, cellP, Process2.hasQualifiedCase, Stmt2.hasQualifiedCase, Stmt2.listHasQualifiedCase]

/-! ## 6. The sort: `insertAsc` and `sortAsc` (core Lean only) -/

open Tasks.Sorter (insertAsc sortAsc)

/-- Ascending in the unsigned order. -/
abbrev Srt {W : Nat} (l : List (BitVec W)) : Prop := l.Pairwise fun a b => a.toNat ≤ b.toNat

theorem mem_ins {W : Nat} (x y : BitVec W) : ∀ l, y ∈ insertAsc x l ↔ y = x ∨ y ∈ l
  | [] => by simp [insertAsc]
  | b :: l => by unfold insertAsc; split <;> simp [mem_ins x y l, or_left_comm]

theorem srt_ins {W : Nat} (x : BitVec W) : ∀ l, Srt l → Srt (insertAsc x l)
  | [], _ => by simp [insertAsc]
  | b :: l, h => by
    have ⟨hb, hl⟩ := List.pairwise_cons.mp h
    unfold insertAsc
    split
    · next hx =>
      refine .cons (fun y hy => ?_) h
      rcases List.mem_cons.mp hy with rfl | hy
      · exact hx
      · exact Nat.le_trans hx (hb y hy)
    · next hx =>
      refine .cons (fun y hy => ?_) (srt_ins x l hl)
      rcases (mem_ins x y l).mp hy with rfl | hy
      · omega
      · exact hb y hy

theorem len_ins {W : Nat} (x : BitVec W) : ∀ l, (insertAsc x l).length = l.length + 1
  | [] => rfl
  | b :: l => by unfold insertAsc; split <;> simp [len_ins x l]

theorem len_sort {W : Nat} : ∀ l : List (BitVec W), (sortAsc l).length = l.length
  | [] => rfl
  | a :: l => by simp [sortAsc, len_ins, len_sort l]

theorem srt_sort {W : Nat} : ∀ l : List (BitVec W), Srt (sortAsc l)
  | [] => .nil
  | _ :: l => srt_ins _ _ (srt_sort l)

theorem ins_comm_lt {W : Nat} {a b : BitVec W} (h : a.toNat < b.toNat) :
    ∀ l, insertAsc a (insertAsc b l) = insertAsc b (insertAsc a l)
  | [] => by simp [insertAsc, Nat.le_of_lt h, Nat.not_le.mpr h]
  | c :: l => by
    by_cases hb : b.toNat ≤ c.toNat
    · simp [insertAsc, hb, Nat.le_of_lt h, Nat.not_le.mpr h, show a.toNat ≤ c.toNat by omega]
    · by_cases ha : a.toNat ≤ c.toNat
      · simp [insertAsc, hb, ha, Nat.not_le.mpr h]
      · simp [insertAsc, hb, ha, ins_comm_lt h l]

/-- **Insertions commute** (equal values are equal: the unsigned order is total). -/
theorem ins_comm {W : Nat} (a b : BitVec W) (l : List (BitVec W)) :
    insertAsc a (insertAsc b l) = insertAsc b (insertAsc a l) := by
  rcases Nat.lt_trichotomy a.toNat b.toNat with h | h | h
  · exact ins_comm_lt h l
  · rw [BitVec.eq_of_toNat_eq h]
  · exact (ins_comm_lt h l).symm

/-- Inserting the last value last: `sortAsc (l ++ [x]) = insertAsc x (sortAsc l)`. -/
theorem sort_snoc {W : Nat} (x : BitVec W) : ∀ l : List (BitVec W), sortAsc (l ++ [x]) = insertAsc x (sortAsc l)
  | [] => rfl
  | a :: l => by simp only [List.cons_append, sortAsc, sort_snoc x l]; exact ins_comm ..

/-- The dropped head of a load is a padding `0` (or `x = 0` changes nothing). -/
theorem tail_ins {W : Nat} (x : BitVec W) (S : List (BitVec W)) (m : Nat) :
    (insertAsc x (List.replicate (m + 1) 0 ++ S)).tail = List.replicate m 0 ++ insertAsc x S := by
  by_cases hx : x.toNat = 0
  · obtain rfl : x = 0 := BitVec.eq_of_toNat_eq (by simp [hx])
    have h0 : ∀ L : List (BitVec W), insertAsc 0 L = 0 :: L := fun L => by cases L <;> simp [insertAsc]
    rw [h0, h0, List.tail_cons, List.replicate_succ', List.append_assoc]; rfl
  · have hz : ∀ m, insertAsc x (List.replicate m 0 ++ S) = List.replicate m 0 ++ insertAsc x S := by
      intro m; induction m with
      | zero => rfl
      | succ m ih => rw [List.replicate_succ, List.cons_append, insertAsc, if_neg (by simp [hx]), ih]; rfl
    rw [List.replicate_succ, List.cons_append, insertAsc, if_neg (by simp [hx]), List.tail_cons, hz]

theorem lt_or_le' (a b : Nat) : (a < b ∧ ¬ b ≤ a) ∨ (b ≤ a ∧ ¬ a < b) := by omega

/-- **The cell array's load is `tail ∘ insertAsc x`** on an ascending list. -/
theorem hw_ins {W : Nat} (x : BitVec W) : ∀ L : List (BitVec W), Srt L → ∀ k, k < L.length →
    hwCell L.length x (fun i => L.getD i 0) k = (insertAsc x L).tail.getD k 0
  | [], _, k, hk => absurd hk (Nat.not_lt_zero _)
  | b :: L, hs, k, hk => by
    have ⟨hb, hL⟩ := List.pairwise_cons.mp hs
    cases k with
    | zero =>
      cases L with
      | nil =>
        rcases lt_or_le' b.toNat x.toNat with ⟨h1, h1'⟩ | ⟨h1, h1'⟩ <;>
          simp [hwCell, insertAsc, BitVec.lt_def, h1, h1']
      | cons c L =>
        have hbc := hb c (by simp)
        rcases lt_or_le' b.toNat x.toNat with ⟨h1, h1'⟩ | ⟨h1, h1'⟩ <;>
          rcases lt_or_le' c.toNat x.toNat with ⟨h2, h2'⟩ | ⟨h2, h2'⟩ <;>
          simp [hwCell, insertAsc, BitVec.lt_def, h1, h1', h2, h2'] <;> omega
    | succ k =>
      have e : hwCell (L.length + 1) x (fun i => (b :: L).getD i 0) (k + 1) =
          hwCell L.length x (fun i => L.getD i 0) k := by simp [hwCell]
      rw [List.length_cons, e, hw_ins x L hL k (by simp at hk; omega)]
      by_cases h1 : x.toNat ≤ b.toNat
      · have : (insertAsc x L).tail = L := by
          cases L with
          | nil => rfl
          | cons c L => simp [insertAsc, Nat.le_trans h1 (hb c (by simp))]
        simp [insertAsc, h1, this]
      · cases h : insertAsc x L <;> simp [insertAsc, h1, h]

/-! ## 7. The invariant: the cells, the tokens, the output -/

/-- The cells `j` cycles after a start that received `ys`: `[0]^(N-j) ++ sortAsc ys` while loading,
then shifted down by `j - N` with `0`s in (`getD`). -/
def cv {W : Nat} (N : Nat) (ys : List (BitVec W)) (j k : Nat) : BitVec W :=
  (List.replicate (N - j) 0 ++ sortAsc ys).getD (k + (j - N)) 0

/-- Token `k`, `j` cycles after a start: `in_valid` of the entry `j - (N - 1 - k)` after it (a delay line). -/
def tokv (N j : Nat) (k : Nat) : BitVec 1 := BitVec.ofBool (decide (N ≤ j + k ∧ j + k + 1 ≤ 2 * N))

/-- `out_valid`, `j` cycles after a start. -/
def ovb (N j : Nat) : Bool := decide (N < j ∧ j ≤ 2 * N)

theorem srt_pad {W : Nat} (m : Nat) {S : List (BitVec W)} (h : Srt S) : Srt (List.replicate m 0 ++ S) :=
  List.pairwise_append.mpr ⟨List.pairwise_replicate.mpr (.inr (Nat.le_refl _)), h,
    fun a ha b _ => by simp [List.eq_of_mem_replicate ha]⟩

theorem feed_cells {W N j : Nat} (ys : List (BitVec W)) (x : BitVec W) (hj : j < N) (hl : ys.length = j)
    {k : Nat} (hk : k < N) : cstep N true x (cv N ys j) k = cv N (ys ++ [x]) (j + 1) k := by
  have hL : (List.replicate (N - j) 0 ++ sortAsc ys).length = N := by simp [len_sort, hl]; omega
  have hv : cv N ys j = fun i => (List.replicate (N - j) 0 ++ sortAsc ys).getD i 0 := by
    funext i; simp [cv, Nat.sub_eq_zero_of_le (Nat.le_of_lt hj)]
  have := hw_ins x _ (srt_pad (N - j) (srt_sort ys)) k (by omega)
  rw [hL] at this
  simp only [cstep, ↓reduceIte]
  rw [hv, this, show N - j = N - (j + 1) + 1 by omega, tail_ins]
  simp [cv, sort_snoc, Nat.sub_eq_zero_of_le (show j + 1 ≤ N by omega)]

theorem run_cells {W N j : Nat} (xs : List (BitVec W)) (x : BitVec W) (hj : N ≤ j) (hl : xs.length = N)
    {k : Nat} (hk : k < N) : cstep N false x (cv N xs j) k = cv N xs (j + 1) k := by
  simp only [cstep, cv, Bool.false_eq_true, ↓reduceIte, Nat.sub_eq_zero_of_le hj,
    Nat.sub_eq_zero_of_le (show N ≤ j + 1 by omega), List.replicate_zero, List.nil_append]
  split
  · congr 1; omega
  · simp [List.getD_eq_getElem?_getD, len_sort, hl, show N ≤ k + (j + 1 - N) by omega]

theorem tok_step {N j k : Nat} (b : Bool) (hb : b = decide (j + 1 ≤ N)) (hk : k < N) :
    tstep N b (tokv N j) k = tokv N (j + 1) k := by
  simp only [tstep, tokv]; split
  · congr 1; simp only [decide_eq_decide]; omega
  · rw [hb]; congr 1; simp only [decide_eq_decide]; omega

/-- **One cycle of a transaction** (a load with `b`, or a drain): the invariant at `j` gives it at `j + 1`. -/
theorem at_step {N W : Nat} (hN : 1 ≤ N) (b : Bool) (x : BitVec W) (ys ys' : List (BitVec W)) (j : Nat)
    (ck s id ov od : LVec) (hid : b = true → id = .ofBitVec x) (hov : ov.width = 1) (hod : od.width = W)
    (hc : ∀ k, k < N → cstep N b x (cv N ys j) k = cv N ys' (j + 1) k) (hb : b = decide (j + 1 ≤ N))
    (ho : ovb N (j + 1) = true → cv N ys j 0 = (sortAsc ys').getD (j + 1 - N - 1) 0) :
    ∃ od', soNext N W ck (knownBit false) s (knownBit b) id ov od (.ofBitVec (packBV W N (cv N ys j)))
        (.ofBitVec (packBV 1 N (tokv N j))) = SS ck (knownBit false) s (knownBit b) id (knownBit (ovb N (j + 1))) od'
        (.ofBitVec (packBV W N (cv N ys' (j + 1)))) (.ofBitVec (packBV 1 N (tokv N (j + 1)))) ∧
      (ovb N (j + 1) = true → od' = .ofBitVec ((sortAsc ys').getD (j + 1 - N - 1) 0)) := by
  have h0 : tokv N j 0 = BitVec.ofBool (ovb N (j + 1)) := by
    simp only [tokv, ovb]; congr 1; simp only [decide_eq_decide]; omega
  rw [next_run hN b x _ _ ck s id ov od hid hov hod, packBV_congr hc, packBV_congr fun k hk => tok_step b hb hk, h0]
  exact ⟨_, rfl, fun h => by rw [ho h]⟩

/-! ## 8. The protocol: the phases of `StreamTask.satisfiedAt_of_phases`, and the statement -/

/-- One cycle from a state of the shape, evaluated (`so_cycle`). -/
def Stp (N W : Nat) (e prev st : SvState) : Prop :=
  ∃ ck r s iv id ov od dt tk, prev = SS ck r s iv id ov od dt tk ∧
    (ov.width = 1 ∧ od.width = W ∧ dt.width = N * W ∧ tk.width = N) ∧
    st = soNext N W (appIn e "clk" ck) (appIn e "rst" r) (appIn e "start" s) (appIn e "in_valid" iv)
      (appIn e "in_data" id) ov od dt tk

theorem SS_inj {ck r s iv id ov od dt tk ck' r' s' iv' id' ov' od' dt' tk' : LVec}
    (h : SS ck r s iv id ov od dt tk = SS ck' r' s' iv' id' ov' od' dt' tk') : ov = ov' ∧ dt = dt' ∧ tk = tk' := by
  simp only [SS, List.cons.injEq, Prod.mk.injEq, true_and, and_true] at h
  exact ⟨h.2.2.2.2.2.1, h.2.2.2.2.2.2.2.1, h.2.2.2.2.2.2.2.2⟩

/-- From zero cells and tokens, a cycle without reset or input shows nothing and stays. -/
theorem next_zero {N W : Nat} (hN : 1 ≤ N) (ck s id ov od : LVec) (hov : ov.width = 1) (hod : od.width = W) :
    ∃ od', soNext N W ck (knownBit false) s (knownBit false) id ov od (Z W N) (Z 1 N) =
      SS ck (knownBit false) s (knownBit false) id (knownBit false) od' (Z W N) (Z 1 N) := by
  rw [next_run hN false 0 (fun _ => 0) (fun _ => 0) ck s id ov od (by simp) hov hod]
  have h1 : cstep N false 0 (fun _ : Nat => (0 : BitVec W)) = fun _ => 0 := funext fun k => by simp [cstep]
  have h2 : tstep N false (fun _ => 0) = fun _ => 0 := funext fun k => by simp [tstep]
  rw [h1, h2]
  exact ⟨_, rfl⟩

theorem zero_at {W N : Nat} : packBV W N (cv N ([] : List (BitVec W)) 0) = packBV W N (fun _ => 0) ∧
    packBV 1 N (tokv N 0) = packBV 1 N (fun _ => 0) :=
  ⟨packBV_congr fun k hk => by simp [cv, sortAsc, List.getD_eq_getElem?_getD, hk],
    packBV_congr fun k hk => by simp [tokv, show ¬ N ≤ k by omega]⟩

theorem zero_done {W N j : Nat} (xs : List (BitVec W)) (hl : xs.length = N) (hj : 2 * N ≤ j) :
    packBV W N (cv N xs j) = packBV W N (fun _ => 0) ∧ packBV 1 N (tokv N j) = packBV 1 N (fun _ => 0) :=
  ⟨packBV_congr fun k _ => by simp [cv, Nat.sub_eq_zero_of_le (show N ≤ j by omega), List.getD_eq_getElem?_getD,
      List.getElem?_eq_none (show (sortAsc xs).length ≤ k + (j - N) by rw [len_sort]; omega)],
    packBV_congr fun k _ => by simp only [tokv]; rw [decide_eq_false (by omega)]; rfl⟩

theorem out_spec_eq {N W : Nat} (xs : List (BitVec W)) (hx : xs.length = N) :
    List.map (·.2) (List.filter (·.1)
      ((List.range N).map fun i => (ovb N (N + 1 + i), (sortAsc xs).getD (N + 1 + i - N - 1) 0))) = sortAsc xs := by
  have h : ((List.range N).map fun i => (ovb N (N + 1 + i), (sortAsc xs).getD (N + 1 + i - N - 1) 0)) =
      (List.range N).map fun i => (true, (sortAsc xs).getD i 0) :=
    List.map_congr_left fun i hi => by
      have := List.mem_range.mp hi; simp [ovb, show N + 1 + i - N - 1 = i by omega]; omega
  rw [h, List.filter_eq_self.mpr (by simp), List.map_map]
  exact List.ext_getElem (by simp [len_sort, hx]) fun i _ h2 => by simp [List.getElem?_eq_getElem h2]

open Tasks.Sorter in
/-- **The phase model** at `(N, W)`, latency `2N`: `Ready` the zero state after a reset; `At ys j` the
cells, tokens and output `j` cycles after a start that received `ys` (`cv`, `tokv`, `ovb`). -/
def model (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) : task.PhaseModel (N, W) (lat N W) (design.sem N W) where
  Shape := I N W
  Step := Stp N W
  init := so_init N W hN hW
  cycle := by
    rintro σ F e prev k st k' ⟨ck, r, s, iv, id, ov, od, dt, tk, rfl, hw⟩ hc
    exact ⟨ck, r, s, iv, id, ov, od, dt, tk, rfl, hw, (Prod.mk.inj (cycleStep2_det hc
      (so_cycle N W hN hW σ e ck r s iv id ov od dt tk k 30 (Nat.le_refl _)))).1⟩
  shape := by
    rintro e prev st - ⟨ck, r, s, iv, id, ov, od, dt, tk, -, hw, rfl⟩
    exact next_I _ _ _ _ _ _ _ _ _ hw
  Ready st := ∃ ck r s iv id od, st = SS ck r s iv id (knownBit false) od (Z W N) (Z 1 N)
  At ys j st := ∃ ck r s iv id od, st = SS ck r s iv id (knownBit (ovb N j)) od
    (.ofBitVec (packBV W N (cv (W := W) N ys j))) (.ofBitVec (packBV 1 N (tokv N j))) ∧
    (ovb N j = true → od = .ofBitVec ((sortAsc (W := W) ys).getD (j - N - 1) 0))
  out ys j := (ovb N j, (sortAsc (W := W) ys).getD (j - N - 1) 0)
  out_feed _ j hj := by have : j < N := hj; simp [ovb]; omega
  out_lat _ j _ hj := by have : 2 * N < j := hj; simp [ovb]; omega
  out_spec xs hx := by
    rw [show lat N W + 1 = (N + 1) + N by simp [lat]; omega, task.emitted_add, task.emitted_nil ?_, List.nil_append]
    · exact out_spec_eq xs hx
    · intro k hk; simp [ovb]; omega
  ready_out := by rintro st ⟨ck, r, s, iv, id, od, rfl⟩; simp [BitIs, task, SS, SvState.lookup]
  at_out := by
    rintro ys j st ⟨ck, r, s, iv, id, od, rfl, hd⟩
    exact ⟨by simp [BitIs, task, SS, SvState.lookup],
      fun h => by simp [StreamTask.DataIs, task, SS, SvState.lookup, hd h]⟩
  reset := by
    rintro e prev st - ⟨ck, r, s, iv, id, ov, od, dt, tk, -, ⟨h1, -, h3, h4⟩, rfl⟩ hr
    rw [show appIn e "rst" r = knownBit true from BitIs.appIn_eq hr r]
    obtain ⟨od', h⟩ := next_reset hN (appIn e "clk" ck) (appIn e "start" s) (appIn e "in_valid" iv)
      (appIn e "in_data" id) ov od dt tk h1 h3 h4
    exact ⟨_, _, _, _, _, _, h⟩
  hold := by
    rintro e prev st - ⟨ck, r, s, iv, id, ov, od, dt, tk, rfl, ⟨h1, h2, -⟩, rfl⟩ ⟨_, _, _, _, _, _, hb⟩ hr - hiv
    obtain ⟨-, rfl, rfl⟩ := SS_inj hb
    rw [show appIn e "rst" r = knownBit false from BitIs.appIn_eq hr r,
      show appIn e "in_valid" iv = knownBit false from BitIs.appIn_eq hiv iv]
    obtain ⟨od', h⟩ := next_zero hN (appIn e "clk" ck) (appIn e "start" s) (appIn e "in_data" id) ov od h1 h2
    exact ⟨_, _, _, _, _, _, h⟩
  start := by
    rintro e prev st - ⟨ck, r, s, iv, id, ov, od, dt, tk, rfl, ⟨h1, h2, -⟩, rfl⟩ hp hr - hiv
    have hz : dt = Z W N ∧ tk = Z 1 N := by
      rcases hp with ⟨_, _, _, _, _, _, hb⟩ | ⟨xs, j, hl, ⟨_, _, _, _, _, _, hb, -⟩, hk⟩
      · obtain ⟨-, rfl, rfl⟩ := SS_inj hb; exact ⟨rfl, rfl⟩
      · obtain ⟨-, rfl, rfl⟩ := SS_inj hb
        have hj : 2 * N ≤ j := Nat.le_of_not_lt fun hc => by
          have := hk (max (j + 1) (N + 1)) (by omega); simp [ovb] at this; omega
        exact ⟨congrArg _ (zero_done (W := W) xs hl hj).1, congrArg _ (zero_done (W := W) xs hl hj).2⟩
    obtain ⟨rfl, rfl⟩ := hz
    rw [show appIn e "rst" r = knownBit false from BitIs.appIn_eq hr r,
      show appIn e "in_valid" iv = knownBit false from BitIs.appIn_eq hiv iv]
    obtain ⟨od', h⟩ := next_zero hN (appIn e "clk" ck) (appIn e "start" s) (appIn e "in_data" id) ov od h1 h2
    refine ⟨appIn e "clk" ck, knownBit false, appIn e "start" s, knownBit false, appIn e "in_data" id, od', ?_,
      by simp [ovb]⟩
    rw [h, show ovb N 0 = false by simp [ovb]]
    congr 1
    · exact congrArg _ (zero_at (W := W)).1.symm
    · exact congrArg _ (zero_at (W := W)).2.symm
  feed := by
    rintro e prev st ys j x - ⟨ck, r, s, iv, id, ov, od, dt, tk, rfl, ⟨h1, h2, -⟩, rfl⟩
      ⟨_, _, _, _, _, _, hb, -⟩ hl hj hr - hiv hx
    have hj' : j < N := hj
    obtain ⟨rfl, rfl, rfl⟩ := SS_inj hb
    have hid : appIn e "in_data" id = .ofBitVec x := by
      simp only [appIn, show SvState.lookup e "in_data" = _ from hx, Option.getD_some]
    rw [show appIn e "rst" r = knownBit false from BitIs.appIn_eq hr r,
      show appIn e "in_valid" iv = knownBit true from BitIs.appIn_eq hiv iv]
    obtain ⟨od', h, ho⟩ := at_step (W := W) hN true x ys (ys ++ [x]) j (appIn e "clk" ck) (appIn e "start" s) _ _ od
      (fun _ => hid) h1 h2 (fun k hk => feed_cells ys x hj' hl hk) (by simp; omega)
      (fun h => by simp [ovb] at h; omega)
    exact ⟨_, _, _, _, _, _, h, ho⟩
  run := by
    rintro e prev st xs j - ⟨ck, r, s, iv, id, ov, od, dt, tk, rfl, ⟨h1, h2, -⟩, rfl⟩
      ⟨_, _, _, _, _, _, hb, -⟩ hl hj hr - hiv
    have hl' : xs.length = N := hl
    have hj' : N ≤ j := hj
    obtain ⟨rfl, rfl, rfl⟩ := SS_inj hb
    rw [show appIn e "rst" r = knownBit false from BitIs.appIn_eq hr r,
      show appIn e "in_valid" iv = knownBit false from BitIs.appIn_eq hiv iv]
    obtain ⟨od', h, ho⟩ := at_step (W := W) hN false 0 xs xs j (appIn e "clk" ck) (appIn e "start" s) _ _ od
      (by simp) h1 h2 (fun k hk => run_cells xs 0 hj' hl' hk) (by simp; omega)
      (fun _ => by simp [cv, Nat.sub_eq_zero_of_le hj', show j + 1 - N - 1 = j - N by omega])
    exact ⟨_, _, _, _, _, _, h, ho⟩

theorem so_interface (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) :
    Tasks.Sorter.task.Interface (N, W) (design.sem N W) := by
  rw [so_sem_eq N W hN hW]
  exact ⟨rfl, rfl, by
    show (["clk", "rst", "start", "in_valid", "in_data", "out_valid", "out_data", "data", "tok"] :
      List String).Nodup
    decide⟩

theorem so_disciplined (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) : Tasks.Sorter.task.Disciplined (design.sem N W) := by
  rw [so_sem_eq N W hN hW]
  refine ⟨by simp [Tasks.Sorter.task, soD, soDeclsW, Design2.inputNames], fun p hp => ?_⟩
  have hm : p ∈ topP N W :: outP W :: (List.range (N - 1)).map (cellP W) := by simpa [soD] using hp
  simp only [List.mem_cons, List.mem_map] at hm
  rcases hm with rfl | rfl | ⟨k, -, rfl⟩ <;>
    simp [Tasks.Sorter.task, topP, outP, cellP, edgeClock, asyncReset, processDataNames, stmtNames,
      stmtOptNames, stmtListNames, lhsNames, exprNames]

/-! ## 9. txtask-v2: every power-up (rule 2), Moore outputs (rule 1), no x-creating construct (rule 3)

Rule 2: the phase model's shape `I` (the register widths, any values) holds at every power-up state
(`so_powerUp`), and every obligation of the model holds from any state of the shape (a reset clears
every cell and token), so the claim holds from every power-up (`StreamTask.satisfiedAtV2_of_phases`,
`SvGolf.SeqV2`); the same cycle gives termination from every power-up (`so_terminatesPU`). Rule 1:
every process is an `always_ff` (`so_profile`), so the design has no combinational dependency at all
(`combDeps_of_ffOnly`). Rule 3 (`so_xsafe`): every expression is a known literal, a declared signal,
an in-range window of `data` or `tok`, or a comparison. -/

/-- **Rule 1.** -/
theorem so_moore (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) :
    MooreOutDep (design.sem N W) [] := by
  rw [so_sem_eq N W hN hW]
  exact MooreOutDep.of_noComb (combDeps_of_ffOnly (FFOnly.ofProfile (so_profile N W hN)))
    (by simp [soD, soDeclsW, Design2.outputNames, Design2.inputNames])

/-- Every power-up state of the design has its shape. -/
theorem so_powerUp (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (st : SvState)
    (h : PowerUp (design.sem N W) st) : I N W st := by
  rw [so_sem_eq N W hN hW] at h
  obtain ⟨ck, r1, rfl, -, -, h1⟩ := powerUp_cons.mp h
  obtain ⟨r, r2, rfl, -, -, h2⟩ := powerUp_cons.mp h1
  obtain ⟨s, r3, rfl, -, -, h3⟩ := powerUp_cons.mp h2
  obtain ⟨iv, r4, rfl, -, -, h4⟩ := powerUp_cons.mp h3
  obtain ⟨id, r5, rfl, -, -, h5⟩ := powerUp_cons.mp h4
  obtain ⟨ov, r6, rfl, w6, -, h6⟩ := powerUp_cons.mp h5
  obtain ⟨od, r7, rfl, w7, -, h7⟩ := powerUp_cons.mp h6
  obtain ⟨dt, r8, rfl, w8, -, h8⟩ := powerUp_cons.mp h7
  obtain ⟨tk, r9, rfl, w9, -, h9⟩ := powerUp_cons.mp h8
  obtain rfl := powerUp_nil.mp h9
  exact ⟨ck, r, s, iv, id, ov, od, dt, tk, rfl, w6, w7, w8, w9⟩

/-- **Termination from every power-up** (the cycle of `so_terminates`). -/
theorem so_terminatesPU (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) : TerminatesPU (design.sem N W) := by
  refine TerminatesPU.of_invariant (I N W) (so_powerUp N W hN hW) (fun σ => ⟨30, ?_⟩) ?_
  · rintro e _ kk ⟨ck, r, s, iv, id, ov, od, dt, tk, rfl, hw⟩
    exact ⟨_, _, so_cycle N W hN hW σ e ck r s iv id ov od dt tk kk 30 (Nat.le_refl _),
      next_I _ _ _ _ _ _ _ _ _ hw⟩
  · rw [so_sem_eq N W hN hW]
    simp [soD, topP, outP, cellP, Process2.hasQualifiedCase, Stmt2.hasQualifiedCase,
      Stmt2.listHasQualifiedCase]

/-- **Rule 3.** -/
theorem so_xsafe (N W : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) : XSafe (design.sem N W) := by
  rw [so_sem_eq N W hN hW]
  have hTop : (N - 1) * W + W ≤ N * W := rowMajor_le (K := W) (show N - 1 < N by omega)
  have hOut : 0 + W ≤ N * W := by
    have := rowMajor_le (K := W) (show 0 < N by omega); simpa using this
  refine List.all_eq_true.mpr fun p hp => ?_
  have hm : p ∈ topP N W :: outP W :: (List.range (N - 1)).map (cellP W) := by simpa [soD] using hp
  simp only [List.mem_cons, List.mem_map, List.mem_range] at hm
  rcases hm with rfl | rfl | ⟨k, hk, rfl⟩
  · simp [xsProc, xsStmt, xsStmts, xsOpt, xsLhs, xsWidth, binW, sigWidth, topP, dw, zW, soD, soDeclsW,
      LVec.replicate_l0, hTop]
    all_goals omega
  · simp [xsProc, xsStmt, xsStmts, xsOpt, xsLhs, xsWidth, binW, sigWidth, outP, dw, zW, soD, soDeclsW,
      LVec.replicate_l0, hOut]
    all_goals omega
  · have h1 : (k + 1) * W + W ≤ N * W := rowMajor_le (K := W) (show k + 1 < N by omega)
    have h2 : k * W + W ≤ N * W := rowMajor_le (K := W) (show k < N by omega)
    simp [xsProc, xsStmt, xsStmts, xsOpt, xsLhs, xsWidth, binW, sigWidth, cellP, dw, zW, soD, soDeclsW,
      LVec.replicate_l0, h1, h2]
    all_goals omega

/-- **The reference satisfies the sorter statement (txtask-v2) at latency `2N`** (`16` at the
scoring point). -/
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 (so_interface N W hN hW) (so_disciplined N W hN hW)
    (so_terminatesPU N W hN hW) hN (show N ≤ 2 * N by omega) (fun xs h => (len_sort xs).trans h)
    (model N W hN hW) (so_powerUp N W hN hW) (so_moore N W hN hW) (so_xsafe N W hN hW)

end Submission

The netlist

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

Schematic

drawn at N = 4, W = 4

Drawn at N = 4, W = 4, a display instance; scored at N = 8, W = 8. Only this drawing and the notes under it are at the smaller size: the critical path, the cells and every other number on this page are the scored netlist's.

_0__reg[0] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[10] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[11] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[12] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[13] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[14] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[15] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[1] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[2] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[3] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[4] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[5] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[6] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[7] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[8] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[9] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _164_ · sky130_fd_sc_hd__inv_1 inv_1 _165_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _166_ · sky130_fd_sc_hd__or2_1 or2_1 _167_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _168_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _169_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _170_ · sky130_fd_sc_hd__and2_1 and2_1 _171_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _172_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _173_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _174_ · sky130_fd_sc_hd__nand2_1 nand2_1 _175_ · sky130_fd_sc_hd__nand2_1 nand2_1 _176_ · sky130_fd_sc_hd__nand2_1 nand2_1 _177_ · sky130_fd_sc_hd__nand2_1 nand2_1 _178_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _179_ · sky130_fd_sc_hd__and2_1 and2_1 _180_ · sky130_fd_sc_hd__nand2_1 nand2_1 _181_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _182_ · sky130_fd_sc_hd__nand2_1 nand2_1 _183_ · sky130_fd_sc_hd__nor2_1 nor2_1 _184_ · sky130_fd_sc_hd__nand2_1 nand2_1 _185_ · sky130_fd_sc_hd__nand2_1 nand2_1 _186_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _187_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _188_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _189_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _190_ · sky130_fd_sc_hd__nand2_1 nand2_1 _191_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _192_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _193_ · sky130_fd_sc_hd__and2_1 and2_1 _194_ · sky130_fd_sc_hd__nand2_1 nand2_1 _195_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _196_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _197_ · sky130_fd_sc_hd__and2_1 and2_1 _198_ · sky130_fd_sc_hd__and2_1 and2_1 _199_ · sky130_fd_sc_hd__and2_1 and2_1 _200_ · sky130_fd_sc_hd__or2_1 or2_1 _201_ · sky130_fd_sc_hd__and2_1 and2_1 _202_ · sky130_fd_sc_hd__and2_1 and2_1 _203_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _204_ · sky130_fd_sc_hd__or2_1 or2_1 _205_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _206_ · sky130_fd_sc_hd__and2_1 and2_1 _207_ · sky130_fd_sc_hd__and2_1 and2_1 _208_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _209_ · sky130_fd_sc_hd__or2_1 or2_1 _210_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _211_ · sky130_fd_sc_hd__and2_1 and2_1 _212_ · sky130_fd_sc_hd__and2_1 and2_1 _213_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _214_ · sky130_fd_sc_hd__or2_1 or2_1 _215_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _216_ · sky130_fd_sc_hd__and2_1 and2_1 _217_ · sky130_fd_sc_hd__and2_1 and2_1 _218_ · sky130_fd_sc_hd__and2_1 and2_1 _219_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _220_ · sky130_fd_sc_hd__and2_1 and2_1 _221_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _222_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _223_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _224_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _225_ · sky130_fd_sc_hd__nand2_1 nand2_1 _226_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _227_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _228_ · sky130_fd_sc_hd__and2_1 and2_1 _229_ · sky130_fd_sc_hd__nand2_1 nand2_1 _230_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _231_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _232_ · sky130_fd_sc_hd__and2_1 and2_1 _233_ · sky130_fd_sc_hd__nand2_1 nand2_1 _234_ · sky130_fd_sc_hd__nand2_1 nand2_1 _235_ · sky130_fd_sc_hd__nand2_1 nand2_1 _236_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _237_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _238_ · sky130_fd_sc_hd__and2_1 and2_1 _239_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _240_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _241_ · sky130_fd_sc_hd__and2_1 and2_1 _242_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _243_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _244_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _245_ · sky130_fd_sc_hd__or2_1 or2_1 _246_ · sky130_fd_sc_hd__and2_1 and2_1 _247_ · sky130_fd_sc_hd__and2_1 and2_1 _248_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _249_ · sky130_fd_sc_hd__and2_1 and2_1 _250_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _251_ · sky130_fd_sc_hd__nand2_1 nand2_1 _252_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _253_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _254_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _255_ · sky130_fd_sc_hd__nand2_1 nand2_1 _256_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _257_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _258_ · sky130_fd_sc_hd__and2_1 and2_1 _259_ · sky130_fd_sc_hd__nand2_1 nand2_1 _260_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _261_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _262_ · sky130_fd_sc_hd__and2_1 and2_1 _263_ · sky130_fd_sc_hd__nand2_1 nand2_1 _264_ · sky130_fd_sc_hd__nand2_1 nand2_1 _265_ · sky130_fd_sc_hd__or2_1 or2_1 _266_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _267_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _268_ · sky130_fd_sc_hd__and2_1 and2_1 _269_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _270_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _271_ · sky130_fd_sc_hd__and2_1 and2_1 _272_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _273_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _274_ · sky130_fd_sc_hd__and2_1 and2_1 _275_ · sky130_fd_sc_hd__and2_1 and2_1 _276_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _277_ · sky130_fd_sc_hd__and2_1 and2_1 _278_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _279_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _280_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _281_ · sky130_fd_sc_hd__and2_1 and2_1 _282_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _283_ · sky130_fd_sc_hd__and2_1 and2_1 _284_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _285_ · sky130_fd_sc_hd__and2_1 and2_1 _286_ · sky130_fd_sc_hd__and2_1 and2_1 _40__reg[0] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _40__reg[1] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _40__reg[2] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _40__reg[3] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q out_data_reg[0] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q out_data_reg[1] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q out_data_reg[2] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q out_data_reg[3] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q out_valid_reg · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q clk in_data in_valid out_data out_valid rst start 0 1 2 3 3 2 1 0

It is the same design through the same pinned flow at a smaller size (ppa.py --param), so that what it does can be seen: 148 cells here, 713 at the scoring point. The register-to-register critical path at N = 4, W = 4 (8 cells, ending at the flip-flop input _047_ falling; a period of 1 932 ps there) is in the accent colour. Drawn by netlistsvg with svGolf's sky130 skin (derived from netlistsvg's default skin, as the drawing is: MIT licence, Copyright (c) 2016 Neil Turley, the notice): one symbol per cell function, the cell above it, the instance on hover; nor2b and nand2b are drawn with the bubble on their inverted input. The cells of the path are listed under Critical path, each a link to the cell here.

The netlist at N = 4, W = 4: 148 cells, 34 and2_1, 28 nand2b_1, 25 dfxtp_1, 20 mux2_1, 20 nand2_1, 10 nor2b_1, 7 or2_1, 2 xnor2_1, 1 inv_1, 1 nor2_1. There (measured, not ranked): 1 320.02 µm², 1 932 ps. Open the drawing on its own (SVG, 102.8 KB) to pan and zoom it with the browser's own controls.

Critical path

at N = 8, W = 8 · scored

The path the ranked register-to-register period ends on, at the scoring point N = 8, W = 8: 12 nets, 11 cells, to the flip-flop input _0107_ falling; the period, 2 523 ps, is the last arrival plus that flip-flop's setup time (ideal clock). Each row is a net of the repaired netlist with the arrival and the transition the STA computed there (NLDM tables, the larger transition carried; no wires). The first row is a flip-flop's Q: its arrival is the flop's clock-to-Q delay after the clock edge. From ppa.py --path (critical_path_timing); the instance names are the scored netlist's, not the schematic's (drawn at a smaller size).

In the schematic, drawn at N = 4, W = 4, the critical path is 8 cells to the flip-flop input _047_ falling (a period of 1 932 ps there); each cell is a link to it in the drawing:

  1. \_0_[10]
  2. _196_ nand2b_1
  3. _197_ and2_1
  4. _198_ and2_1
  5. _199_ and2_1
  6. _200_ or2_1
  7. _236_ mux2_1
  8. _237_ mux2_1
  9. _238_ and2_1
  10. _047_ flip-flop D
#netedgedriven bycellarrival (ps)transition (ps)stage (ps)
0\_0_[45]fallflop Q–308.643.1
1_0270_fall_0839_nand2b_1448.948.5140.3
2_0274_fall_0843_and2_1574.129.9125.2
3_0275_fall_0844_and2_1709.529.9135.4
4_0276_fall_0845_and2_1861.543.4152.0
5_0292_rise_0861_nand2_1911.840.750.3
6_0297_fall_0866_nand2_1946.923.235.1
7_0302_fall_0871_and2_11 132.0100.3185.1
8_0305_rise_0874_nor2b_11 587.3538.6455.3
9_0377_rise_0955_nor2b_11 932.2289.9344.9
10_0407_fall_0992_mux2_12 272.648.8340.4
11_0107_fall_0993_and2_12 417.735.2145.1

Cells

at N = 8, W = 8 · scored

the cells of the repaired netlist, by area10 bars; the table beside the chart lists the same numbers.dfxtp_1: 1621.56 µm² (µm² · 81 cells)dfxtp_11621.56 µm² · 81 cellsand2_1: 1263.71 µm² (µm² · 202 cells)and2_11263.71 µm² · 202 cellsnand2b_1: 769.49 µm² (µm² · 123 cells)nand2b_1769.49 µm² · 123 cellsmux2_1: 641.87 µm² (µm² · 57 cells)mux2_1641.87 µm² · 57 cellsnand2_1: 518.0 µm² (µm² · 138 cells)nand2_1518.0 µm² · 138 cellsor2_1: 369.1 µm² (µm² · 59 cells)or2_1369.1 µm² · 59 cellsnor2b_1: 150.14 µm² (µm² · 24 cells)nor2b_1150.14 µm² · 24 cellsxnor2_1: 122.62 µm² (µm² · 14 cells)xnor2_1122.62 µm² · 14 cellsnor2_1: 45.04 µm² (µm² · 12 cells)nor2_145.04 µm² · 12 cellsinv_1: 11.26 µm² (µm² · 3 cells)inv_111.26 µm² · 3 cells
The area of each cell type in the repaired A0′ netlist, at the scoring point: the count times the cell's area in the pinned liberty. Their sum is the ranked area.
cellcountµm² eachµm² in allshare
dfxtp_18120.01921621.555229.4%
and2_12026.25601263.712022.9%
nand2b_11236.2560769.488014.0%
mux2_15711.2608641.865611.6%
nand2_11383.7536517.99689.4%
or2_1596.2560369.10406.7%
nor2b_1246.2560150.14402.7%
xnor2_1148.7584122.61762.2%
nor2_1123.753645.04320.8%
inv_133.753611.26080.2%
total7135512.7872

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

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

the gate mix of the extra GE column (the pinned GE table, score/ge_seq.json)
gate mix: cells of each type in the scored netlist10 bars; the table beside the chart lists the same numbers.AND: 202 cells (269.266 GE)AND202 269.266 GENAND: 138 cells (138.000 GE)NAND138 138.000 GEORNOT: 123 cells (163.959 GE)ORNOT123 163.959 GEDFF_P: 81 cells (431.973 GE)DFF_P81 431.973 GEOR: 59 cells (78.647 GE)OR59 78.647 GEMUX: 57 cells (132.981 GE)MUX57 132.981 GEANDNOT: 24 cells (31.992 GE)ANDNOT24 31.992 GEXNOR: 14 cells (28.000 GE)XNOR14 28.000 GENOR: 12 cells (12.000 GE)NOR12 12.000 GENOT: 3 cells (2.001 GE)NOT3 2.001 GE
Cells by type; area is the count weighted by the pinned GE table.
cellcountGE eachGE total
AND2021.333269.266
NAND1381.000138.000
ORNOT1231.333163.959
DFF_P815.333431.973
OR591.33378.647
MUX572.333132.981
ANDNOT241.33331.992
XNOR142.00028.000
NOR121.00012.000
NOT30.6672.001
total7131288.819

The record

task
sorter
player
svgolf-reference
assisted by
Claude (Anthropic)
submitted
2026-11-09
notes
reference solution
scoring point
N = 8, W = 8
design
sorter_ins.sv sha256 2f51939328bf61aa1ec44097e954bdf7616a9341555683dbddb1e6b9b439f8e2
proof
sorter_ins.lean sha256 ea41270a788d8b8d4f4e82a0929a190198a88e6279a4a3302c459383576fff3e: the proof of the reference sorter_ins (sorter_ins.lean, 774 code lines)
canonical text
sha256 dff57a68c0ba1fa14f57a5baa09c9a317425cced084aca0edcffe350f7cfc2fa
record hash
90919c7cd8f8f4362a84b1e460f0ca0f62f55d54fe22ab890e514f35b137d069
downloads
90919c7cd8f8.sv 90919c7cd8f8.lean 90919c7cd8f8.json

The proof

code lines
774
build time
5.66 s
axioms
Classical.choice, Quot.sound, propext
tactics seen
decide, induction, omega, simp
imports
Submission.Design, LeanModels.Sv.Gen2, LeanModels.Sv.Hier2Gen, LeanModels.Sv.SeqProfile, LeanModels.Sv.SeqFamily, LeanModels.Sv.Known2, LeanModels.Sv.Mono2, SvGolf.SeqV2

Checker and flow

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

Yosys
Yosys 0.53 (git sha1 53c22ab7c0ced80861c7536c5dae682c30fb5834, clang++ 17.0.0 -fPIC -O3)
Verilator
Verilator 5.042 2025-11-02 rev UNKNOWN.REV
Lean toolchain
leanprover/lean4:v4.33.0-rc1
svGolf revision
7fb4c3d844e0911b67cb6657e9dfdac8741e72d3
lean-surfaces revision
7fb4c3d844e0911b67cb6657e9dfdac8741e72d3
canonicalization script
bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b
scoring script
c3874dbfc85921a87df6eacdfc6b2c9a0e2b34edd5738951e0d8bdb51f4558b2
GE table
0a1aa1147b6916efa4a41e03aa3c8c70e68c1e3fd7a0e9c9a3cbc177edefd1f6
extractor
4930696021c588c75dc890034c534c95560ad9a28a4955b87d1f8d68b5edbc0c
canonical RTLIL
1a464656d5e071eaa18dfeb2416ec0c89615d0ce266992479b8b08c30affcf39
the checker's files (sha256)
filesha256
check.pyb0c939438a765c2ffeb679721c83ced6213c0a96bfef84759948d3857db9f431
check/Comparator.lean936f97636d6256374eaa4435d03321eeff29e22f808a72c7781375ab648600e8
check/SvEval.leanfb51d72510b515460866c2798aad3c6f55295536e627b92854c3580af215bb91
check/clocked_rules.py73856a45905724544247ad29042bdc2f1778271ec07b15cdb3a5f214685165c1
check/envelope.py076db01a9791bcc25ee84e9b0033604a4b675f00b212eab0c864078e6a4748b7
check/postsynth.pydd89805f9e8335ab15d6bb753eea76865bce47e84ccffa7e7280c91da8131d23
lakefile.tomlf35a88404367d22906effc14d644aac9a9cad47dfd3b704ea8fec88acfaf9c4d
lean-toolchain62c2d9c0fc1ec4c67e151c11eff41ca004ef38e179cf9476c230406e6defedef
score/banlist.pyf18c14c23a14d55db63e202f42cc424dc84c1dd1c337f132ad60859dc9d5d33a
score/canon.ysbbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b
score/fourstate.py95332451ae3754226fb87b46027385b46a91121e7eb9ae25b302bce756d90475
score/ge.json6a29196a3f4b58241f4c9af650c9141e4632b737214d563a11ba142a725c4bea
score/ge_seq.json0a1aa1147b6916efa4a41e03aa3c8c70e68c1e3fd7a0e9c9a3cbc177edefd1f6
score/ppa.py912031912c3e3f6790725161753e95415df34846bd8c27dde3eb707747ddbcbe
score/ppa_mapped.ys93547b343dbac135737e98516b1004a780e1cf2f579e1bd7fed82c908c6d4125
score/ppa_mapped_pins.json4b8688ba3f4d67681658e5944afe878592adf588cd416a8b47597ebe06deb045
score/ppa_pins.jsond66a6086a37a97f5985266057051979fb6a8a3c557d3ef9c42acc1b5e41502d8
score/score.py71d2e3b82f8813ec64a58f0a46909ca23dfab377db44eda6f294b713f45ae781
score/srcgate.py11952f61058051c9e8de91a801b672d07e66a29308e978156c04ffd9f0dbef45
score/svgolf.ysea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445
score/svgolf_seq.ysc3874dbfc85921a87df6eacdfc6b2c9a0e2b34edd5738951e0d8bdb51f4558b2

Post-synthesis check

At each point below, the check ran the scored netlist and ls-sv's reading of the design 8 times, once per seed, each run from a power-up state and through a seeded stimulus of 24 transactions. Each point ran against its own latency, the solution's lat at that point (the table's latency column): every transaction had to finish within it. The check found no mismatch. The stimulus is a sample of the inputs: a guard against the two tools disagreeing, not a proof.

mode
full
points
N = 3, W = 4, N = 8, W = 8 (the scoring point)
seeds
8 seeds per point: seed 0 from the all-zeros power-up, every other one from a random power-up drawn from its seed (below)
stimulus
24 transactions per seed
clock cycles
5 632 in all
mismatches
0
salted
no (the default empty salt: anyone can run this exact stimulus again)
scored netlist
sha256 426979cefe8d08cb30796c79bf5b4cdd1c6a9a179c011c677cbe471c094aedce
pointlatency (cycles)seedsclock cyclestransactionsmismatchesnetlist sha256
N = 3, W = 4681 642192078a848f59f52
N = 8, W = 81683 9901920426979cefe8d
every seed's run (16)

A seed's draw is sha256(salt, task, point, seed) (its first 12 digits below; check/postsynth.py seed_draw). Everything random in the seed's run comes from it: the stimulus, ls-sv's power-up (zeros for seed 0, else seed:<k>) and the netlist's Verilator randSeed, which the all-zeros power-up of seed 0 does not use.

pointseedls-sv power-upnetlist randSeedclock cyclestransactionsdraw
N = 3, W = 40zeros1952296509204248d70c02df6d3
N = 3, W = 41seed:141673043862026086702056395843201243f8139a09748
N = 3, W = 42seed:15349116756979067662276963801230245624ba4d1be9
N = 3, W = 43seed:1676413370634801160812901383831892487050d3f1330
N = 3, W = 44seed:15632086897789317647437986317193240f06f6bc65d1
N = 3, W = 45seed:99425911047128541001910572528202247a73c7d0eba8
N = 3, W = 46seed:3361653529102746091956717111202249e27a1eecb3d
N = 3, W = 47seed:104430671225837119261607289826221242425cc80c099
N = 8, W = 80zeros945474377533243e0b206fed95
N = 8, W = 81seed:15715876447011346204143434080544624c3c02390e760
N = 8, W = 82seed:141454546952489173461552466440518242c2bbb1edac6
N = 8, W = 83seed:1129258223950931663636955520343924c7ba34f38a68
N = 8, W = 84seed:234716312544032413357024862853724bf01aeb94c75
N = 8, W = 85seed:699032606065712769037618700150224156bb7d7a631
N = 8, W = 86seed:704803465167269034044063708451824dd22ce785d5d
N = 8, W = 87seed:43807601202661409063234476724972412f7aadf635a

Area against time

µm² × ps · lower left is better · ASAP7
sorter: this design's sky130 area against time, among the task's designs2 designs by sky130 area (µm²) (x) and time (ps) (y), this one ringed; lower left is better. The table under the chart lists the same numbers.34k36k38k40k4800500052005400sky130 area (µm²)time (ps) · lower is betterpar's score: area × time = 222 540 µm²·nsthe Pareto front of the entrieskestrel-golf · submission · 2026-11-10 · Score: 157 015 µm²·ns · Area: 4754.6 µm² · Time: 33 024 psthis design · sorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 222 540 µm²·ns · Area: 5512.8 µm² · Time: 40 368 psthis design · par
sorter: this design's sky130 area against time, among the task's designs2 designs by sky130 area (µm²) (x) and time (ps) (y), this one ringed; lower left is better. The table under the chart lists the same numbers.35k37.5k40k4750500052505500sky130 area (µm²)time (ps) · lower is betterpar's score: area × time = 222 540 µm²·nsthe Pareto front of the entrieskestrel-golf · submission · 2026-11-10 · Score: 157 015 µm²·ns · Area: 4754.6 µm² · Time: 33 024 psthis design · sorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 222 540 µm²·ns · Area: 5512.8 µm² · Time: 40 368 psthis design · par
  • submission
  • proved reference
  • the Pareto front of the entries
  • this design
  • par's score: area × time = 222 540 µm²·ns
sky130 area (x) against the ranked time (y); lower left is better on both. The step line is the Pareto front of the entries (the proved references and the players' ranked records); a design under par's score curve has a better score than par. Baselines are drawn for scale: scored, never proved. Every design is in view.
the designs as numbers, by score
designkindarea (µm²)time (ps)score (µm²·ns)
kestrel-golf submission4 754.5633 024157 015
sorter_ins · this designproved reference · par5 512.7940 368222 540
sorter: this design's ASAP7 area against time, among the task's designs2 designs by ASAP7 area (µm²) (x) and time (ps) (y), this one ringed; lower left is better. The table under the chart lists the same numbers.7200740076007800800082007577.58082.585ASAP7 area (µm²)time (ps) · lower is betterpar's score: area × time = 701.9 µm²·nsthe Pareto front of the entrieskestrel-golf · submission · 2026-11-10 · Score: 538.9 µm²·ns · Area: 74.854 µm² · Time: 7200 psthis design · sorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 701.9 µm²·ns · Area: 85.687 µm² · Time: 8192 psthis design · par
sorter: this design's ASAP7 area against time, among the task's designs2 designs by ASAP7 area (µm²) (x) and time (ps) (y), this one ringed; lower left is better. The table under the chart lists the same numbers.75008000758085ASAP7 area (µm²)time (ps) · lower is betterpar's score: area × time = 701.9 µm²·nsthe Pareto front of the entrieskestrel-golf · submission · 2026-11-10 · Score: 538.9 µm²·ns · Area: 74.854 µm² · Time: 7200 psthis design · sorter_ins · proved reference · par · 2026-11-03T22:01:22Z · Score: 701.9 µm²·ns · Area: 85.687 µm² · Time: 8192 psthis design · par
  • submission
  • proved reference
  • the Pareto front of the entries
  • this design
  • par's score: area × time = 701.9 µm²·ns
ASAP7 area (x) against the ASAP7 time (y); lower left is better on both. The step line is the Pareto front of the entries (the proved references and the players' ranked records); a design under par's score curve has a better score than par. Baselines are drawn for scale: scored, never proved. Every design is in view.
the designs as numbers, by score
designkindarea (µm²)time (ps)score (µm²·ns)
kestrel-golf submission74.8547 200538.9
sorter_ins · this designproved reference · par85.6878 192701.9

Reproduce and verify

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

shell
# the ranked numbers, at the scoring point (from svgolf/, with the pinned Yosys and liberty)
# a clocked task: the clocked flow, --seq (the time is the register-to-register period)
python3.12 score/ppa.py tasks/sorter/reference/sorter_ins.sv --task tasks/sorter --seq --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256
1a464656d5e071eaa18dfeb2416ec0c89615d0ce266992479b8b08c30affcf39
ppa.netlist_sha256
426979cefe8d08cb30796c79bf5b4cdd1c6a9a179c011c677cbe471c094aedce
ppa.repair.netlist_sha256
cbb32aa59a2dd0459b9d12e75ffb62347385a67750d64c420fd4012eae7a094a
ppa.area_e4um2_sky130
55127872
ppa.delay_ps_sky130
2523

The schematic and the critical-path data are site/schematics/sorter/2f51939328bf61aa.json and its .svg, written by site/gen_schematics.py (the display instance is ppa.py ... --param N=4 --param W=4 --repaired-netlist, drawn by netlistsvg 1.0.2; repaired netlist sha256 d9373e17bc7db7e4…).

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

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

Expect, in out.json:

ppa.netlist_sha256
426979cefe8d08cb30796c79bf5b4cdd1c6a9a179c011c677cbe471c094aedce
ppa.repair.netlist_sha256
616d75ed0732cc6d80d85e184ece13bafcd0de4649fc9891fb17f5e2ca95620c
ppa.area_e5um2_asap7
8568666
ppa.delay_ps_asap7
512

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

Verify the record

Download the three files, then from svgolf/:

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

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