Record `84da5a4152db`

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

Recorded by the maintainers from the proved reference rr_mask: its design and its proof rr_mask.lean (487 code lines). A registered mask round-robin: the lowest requester above the last grant wins, else the lowest requester; proved for every number of clients. 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

769.49µm²

769.4880 µm² exactly

vs par: this design is par

cells: 103
flops: 16
repair: 0 buffers, 0 tie cells
GE: 188.979 extra

Performance · time

2 826ps

the register-to-register period, one decision per cycle: the latest arrival at an output, or at a flip-flop's D plus setup, ideal clock

vs par: this design is par

Fmax-eq.: 353.9 MHz derived
critical path: 15 cells
unit depth: 17 extra

Score · area × time

2175µm²·ns

769.4880 µm² × 2 826 ps

vs par: this design is par
board: par, the bar to beat: never ranked

No other player has a ranked record on arbiter yet: the beats and matches lines come with the first one.

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 arbiter's other players at this revision (0 players, 0 records), never the references, the baselines or a rejected design; advisory, recomputed at every build, never stored in a record and never used by the ranking.

This design is the only one with sky130 numbers on this page, so the cards have no “on this page” or “Pareto” row.

Area

12.160µm²

12.15972 µm² exactly

vs par: this design is par

cells: 138
flops: 16
repair: 0 buffers, 0 tie cells
GE: 188.979 extra

Performance · time

464ps

the register-to-register period, one decision per cycle: the latest arrival at an output, or at a flip-flop's D plus setup, ideal clock

vs par: this design is par

Fmax-eq.: 2155.2 MHz derived
unit depth: 17 extra

Score · area × time

5.642µm²·ns

12.15972 µm² × 464 ps

vs par: this design is par
board: par, the bar to beat: never ranked

No other player has a ranked record on arbiter yet: the beats and matches lines come with the first one.

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.

This design is the only one with ASAP7 numbers on this page, so the cards have no “on this page” or “Pareto” row.

The sources

rr_mask.svdownload

// Task `arbiter`: the reference (own code, 2026-11-04; proved for every N >= 1, rr_mask.lean, 2026-11-05). A registered
// round-robin arbiter, the textbook mask form: `mask` marks the clients above the last grant; the lowest
// masked requester wins, else the lowest requester (the wrap). Moore: gnt is a flop (the one comb block
// computes the pick from req and the mask and drives no output). Fair within N cycles: if
// client i requests and loses, the winner lies between the last grant and i, so i's cyclic distance from
// the mask's edge drops (the ranking of tasks/arbiter/README.md (e)).
// Why own code and not a real-world design (MEASURED 2026-11-05): the adapted OpenTitan prim_arbiter_tree
// (tests/arbiter/designs/arbiter_ot.sv) declares variables and localparams inside its generate blocks, which
// ls-sv does not instantiate yet; verilog-axis arbiter.v instantiates priority_encoder twice (hierarchy) over
// unpacked arrays. tasks/arbiter/README.md, "The reference".
module arbiter #(parameter int N = 8) (
  input  logic         clk, rst,
  input  logic [N-1:0] req,
  output logic [N-1:0] gnt
);
  logic [N-1:0] mask, mreq, pick;
  always_comb begin
    mreq = req & mask;
    pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1));
  end
  always_ff @(posedge clk) begin
    if (rst) begin
      gnt <= '0;
      mask <= '1;
    end else begin
      gnt <= pick;
      if (pick != '0) mask <= ~((pick << 1) - 1'b1);
    end
  end
endmodule

rr_mask.lean (487 code lines)

import Submission.Design
import LeanModels.Sv.Gen2
import LeanModels.Sv.Hier2Gen
import LeanModels.Sv.Known2
import LeanModels.Sv.Mono2
import LeanModels.Sv.SeqFamily
import SvGolf.Seq
import SvGolf.React
import SvGolf.RoundRobin

/-!
# Reference solution for task `arbiter`: the registered mask round-robin, every `N ≥ 1`

`reference/rr_mask.sv` (own code; the real-world candidates wait on ls-sv, `tasks/arbiter/README.md` (j)) keeps
`gnt` and a thermometer `mask` in one `always_ff`, and computes the pick in one `always_comb`: the lowest
requester among `req & mask`, else the lowest requester. Proved for every `N ≥ 1` (`N` stays a variable)
through `ReactTask.satisfiedAt_of_rank` (`SvGolf/React.lean`):

1. **Agreement** (`rr_sem_eq`): `design.sem N` is the hand-built `rrD N` (`sv2_inst_simp`; the comb
   block's self-read guard by `comb_admits`). One proof-side lemma, `inst_ne_fill`: `x != '0` lowers at
   `x`'s width. `sv2_inst_simp` alone stops there, because ls-sv's private `maxW2` has a simp lemma for two
   known widths only (`maxW2_some`) and a fill has none (`tasks/arbiter/README.md` F11).
2. **One cycle in closed form** (`rr_cycle`, any values, `x` included): the inputs applied, the comb settle
   (one pass computes the block, a second changes nothing: `settle_rr`), the edge (`ff_run`), the commit
   (`commit_ff`), the comb settle again. `Terminates2` and the shape follow (`rr_terminates`). ls-sv's
   clock-step library has this closed form for FF-only designs only (`cycleStep2_ffOnly`); a design with a
   comb process proves its own settle here (README F10).
3. **The cycle on known values** (`rrNext_reset`, `rrNext_run`): from a reset, `gnt = 0` and `mask` all
   ones; otherwise `gnt = pick req mask` and `mask` the thermometer above the pick
   (`SvGolf.RoundRobin.pick`, `next`).
4. **The rank model** (`model`): the invariant `ArbInv` (every signal but `clk` known, the mask a
   thermometer with edge `e`), the outputs `gnt`, the rank of client `i` its cyclic distance from the edge
   (`RoundRobin.dist`, at most `N - 1`). Safety is `pick_grants`; progress is `RoundRobin.step`: a
   requester that loses gets strictly closer to the edge.
5. **Every power-up** (txtask-v2's rule 2, 2026-11-06): every power-up state of `rrD N` has the shape
   (`rr_powerUp`, by `powerUp_cons` once per declaration), so the rank model's claim holds from each,
   and termination from each (`rr_terminates`, `TerminatesPU.of_invariant`). The reset lemma already
   held from ANY state of the shape, so nothing else changed.
6. **Structure**: `Interface` (`rfl` on `rrD`, the names distinct by `decide`), `ClockedBy clk none`,
   `MooreOut` (no comb process writes an output: `mooreOut_of_combTargets`), and rule 3 (`rr_xsafe`,
   `xsafeB` by `simp`: equal operand widths, no division, no dynamic index).
-/

namespace Submission

open LeanModels.Sv SvGolf

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

/-- The `N`-bit fills `'0`, `'1` and the literal `1'b1`. -/
abbrev z0 (N : Nat) : LVec := LVec.replicate N .l0
abbrev z1 (N : Nat) : LVec := LVec.replicate N .l1
abbrev one1 : LVec := ⟨#[.l1]⟩

/-- The `always_comb` body: `mreq = req & mask; pick = (mreq != '0) ? lowbit(mreq) : lowbit(req)`. -/
def combBody (N : Nat) : Stmt2 :=
  .block #[
    .blockingAssign (.ident "mreq") (.binary .and (.ident "req") (.ident "mask")),
    .blockingAssign (.ident "pick")
      (.ternary (.binary .ne (.ident "mreq") (.lit (z0 N)))
        (.binary .and (.ident "mreq") (.binary .add (.unary .bnot (.ident "mreq")) (.resize N (.lit one1))))
        (.binary .and (.ident "req") (.binary .add (.unary .bnot (.ident "req")) (.resize N (.lit one1)))))]

/-- The `always_ff` body: reset, else `gnt <= pick` and the mask above the pick. -/
def ffBody (N : Nat) : Stmt2 :=
  .block #[
    .ifStmt (.ident "rst")
      (.block #[.nbaAssign (.ident "gnt") (.lit (z0 N)), .nbaAssign (.ident "mask") (.lit (z1 N))])
      (some (.block #[.nbaAssign (.ident "gnt") (.ident "pick"),
        .ifStmt (.binary .ne (.ident "pick") (.lit (z0 N)))
          (.nbaAssign (.ident "mask") (.unary .bnot (.binary .sub
            (.binary (.shl false) (.ident "pick") (.lit (LVec.ofInt 32 1))) (.resize N (.lit one1)))))
          none]))]

/-- The comb process. -/
def combP (N : Nat) : Process2 := .alwaysComb (combBody N)

/-- The flop process. -/
def ffP (N : Nat) : Process2 := .alwaysFF "clk" (ffBody N)

/-- The declarations at width `n`. -/
def rrDeclsW (n : Nat) : List Decl :=
  [{ name := "clk", width := 1, isInput := true }, { name := "rst", width := 1, isInput := true },
   { name := "req", width := n, isInput := true }, { name := "gnt", width := n, isOutput := true },
   { name := "mask", width := n }, { name := "mreq", width := n }, { name := "pick", width := n }]

/-- **The hand-built design** at `N`. -/
def rrD (N : Nat) : Design2 where
  name := "arbiter"
  decls := (rrDeclsW N).toArray
  processes := #[combP N, ffP N]

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

def rrEnv (N : Int) : IEnv := { rrScope N with dims := dimTable (rrScope N) design.pdesign.decls }

theorem rr_paramEnv (N : Int) : design.pdesign.paramEnv2 [N] = .ok (rrEnv N) := rfl

def rrElems : List (String × Nat) := ["clk", "rst", "req", "gnt", "mask", "mreq", "pick"].map (·, 1)

theorem rr_decls (N : Int) :
    buildDecls (rrEnv N) design.pdesign.decls = .ok (rrDeclsW ((N - 1).natAbs + 1)) := by
  simp [design.pdesign, buildDecls, instDecl, PType.width_packed_cons, PDim.width, evalInt,
    rrEnv, rrScope, List.lookup, rrDeclsW, Gen2.except_ok_bind]

theorem rr_elems (N : Int) : buildElems (rrEnv N) design.pdesign.decls = .ok rrElems := by
  simp [design.pdesign, buildElems, PType.width_packed_cons, PDim.width, evalInt, rrEnv,
    rrScope, List.lookup, rrElems, Gen2.except_ok_bind]

/-- The instantiation environment. -/
abbrev rrE (N : Nat) : IEnv := (rrEnv N).withDecls (rrDeclsW N)

/-- The source bodies of the two processes. -/
def combT : PStmt := match design.pdesign.processes with
  | [.alwaysComb b, _] => b
  | _ => .block []

def ffT : PStmt := match design.pdesign.processes with
  | [_, .alwaysFF _ b] => b
  | _ => .block []

theorem rr_procs_src : design.pdesign.processes = [.alwaysComb combT, .alwaysFF "clk" ffT] := rfl

/-- `x != '0` lowers at the width of `x` (the fill takes the comparison's width). Stated with the
width lookup itself, so that `sv2_inst_simp` meets no `max` of a width and the fill's none. -/
theorem inst_ne_fill (E : IEnv) (el : List (String × Nat)) (n : String) (b : Logic) :
    instExpr2 E el none (.binary (.m0 .ne) (.ident n) (.fill b)) =
      .binary .ne (fitExpr2 E el (E.widths.lookup n) (.ident n))
        (fitExpr2 E el (E.widths.lookup n) (.fill b)) := by
  simp only [instExpr2, selfWidth2]
  cases E.widths.lookup n <;> rfl

macro "rr_inst_simp" : tactic => `(tactic| sv2_inst_simp [↓ inst_ne_fill, evalSized, ctype, evalAt,
  ctypeList, evalAtList, SymBinOp.constClass, PExpr.pushedTarget, PExpr.readsSignal, PExpr.readsSignalList,
  Gen2.except_pure, instStmt2, instStmts2, design.pdesign, rrEnv, rrScope, rrDeclsW, rrElems, combT, ffT,
  combBody, ffBody, dimTable, dimTableStep, PType.width_packed_cons, PDim.width, ctxOpWidth2, rigidMax2,
  PExpr.ctxPropagates, PExpr.constLeaf, PExpr.negGenvarWidened, LVec.width, divOperandWidth2,
  instDivOperand2, fitDivOperand2, *])

theorem comb_inst (N : Nat) (hN : 1 ≤ N) : instStmt2 (rrE N) rrElems combT = combBody N := by
  have h0 : (0 : Int) < N := by omega
  rr_inst_simp
  try and_intros
  all_goals first | rfl | (change fitExpr2 _ _ (some N) _ = _; rr_inst_simp) | skip

theorem ff_inst (N : Nat) (hN : 1 ≤ N) : instStmt2 (rrE N) rrElems ffT = ffBody N := by
  have h0 : (0 : Int) < N := by omega
  rr_inst_simp
  try and_intros
  all_goals first | rfl | (change fitExpr2 _ _ (some N) _ = _; rr_inst_simp) | skip

/-- The comb block's self-read guard admits the body at every `N` (every read the walk compares is
on another signal than the bits written after it). -/
theorem comb_admits (N : Nat) : (combBody N).combAdmits (fun n => (rrE N).widths.lookup n) = true := by
  simp [Stmt2.combAdmits, combBody, Stmt2.combViol, Stmt2.listCombViol, Stmt2.mayW,
    Stmt2.listMayW, Stmt2.mustW, Lhs2.mayW, Lhs2.mustW, Lhs2.rdW, Expr2.rdW, CombGuard.readsViol,
    CombGuard.whole, CombGuard.BWin.inter, CombGuard.BWin.sub, CombGuard.BWin.subAll, List.lookup,
    rrDeclsW]

theorem rr_static (N : Nat) (hN : 1 ≤ N) :
    design.pdesign.processes.map (instProcess2 (rrE N) rrElems) = [combP N, ffP N] := by
  rw [rr_procs_src]
  simp only [List.map_cons, List.map_nil, instProcess2, comb_inst N hN, ff_inst N hN,
    combGuardProc_of_admits (comb_admits N), combP, ffP]

theorem rr_instantiate2 (N : Nat) (hN : 1 ≤ N) :
    design.pdesign.instantiate2 [(N : Int)] (PDesign.surfaceFuel [(N : Int)]) =
      .ok (design.pdesign.assemble2 (rrEnv N) (rrDeclsW N) rrElems []) := by
  have hd := rr_decls N
  rw [Lib.natAbs_sub_one_add_one hN] at hd
  exact PDesign.instantiate2_of_ok rfl (rr_paramEnv _) hd (rr_elems _)
    (by simp [design.pdesign])

theorem rr_processes (N : Nat) (hN : 1 ≤ N) :
    (design.pdesign.instantiateD2 [(N : Int)]).processes.toList = [combP N, ffP N] := by
  rw [PDesign.instantiateD2_of_ok (rr_instantiate2 N hN), PDesign.assemble2_processes,
    rr_static N hN]
  simp [design.pdesign]

theorem rr_driversOk (N : Nat) :
    driversOk design.pdesign.declNames design.pdesign.inputNames [combP N, ffP N] = true := by
  first
  | (simp [driversOk, driverWins, Process2.drvWins, Process2.procWins, Process2.procWrites,
      Process2.exclusive, Process2.exclClash, Process2.procWinsOn, procExclusiveOk,
      drvWinsDisjoint, DrvWin.overlaps, Stmt2.drvWins, Stmt2.drvWinsOpt, Stmt2.drvWinsList,
      Lhs2.drvWins, combP, combBody, ffP, ffBody, design.pdesign, PDesign.declNames, PDesign.inputNames]; done)
  | rfl

/-- **The loaded family is `rrD`**, at every `N ≥ 1`. -/
theorem rr_sem_eq (N : Nat) (hN : 1 ≤ N) : design.sem N = rrD N := by
  have h1 : design.sem N = design.pdesign.instantiateD2 [(N : Int)] := by
    show design.pdesign.instantiateGD2 [(N : Int)] = _
    exact PDesign.instantiateGD2_of_driversOk (by rw [rr_processes N hN]; exact rr_driversOk N)
  rw [h1, PDesign.instantiateD2_of_ok (rr_instantiate2 N hN)]
  simp only [PDesign.assemble2, rr_static N hN, rrD]
  simp [design.pdesign]

/-! ## 2. One cycle, in closed form (any values, `x` included) -/

/-- The seven signals of `rrD`, in declaration order. -/
def SS (ck r q g m mr pk : LVec) : SvState :=
  [("clk", ck), ("rst", r), ("req", q), ("gnt", g), ("mask", m), ("mreq", mr), ("pick", pk)]

theorem apply_rr (N : Nat) (e : SvState) (ck r q g m mr pk : LVec) :
    applyInputs2 (rrD N) e (SS ck r q g m mr pk) =
      SS (appIn e "clk" ck) (appIn e "rst" r) (appIn e "req" q) g m mr pk := by
  unfold applyInputs2
  rw [← Array.foldl_toList]
  cases h1 : SvState.lookup e "clk" <;> cases h2 : SvState.lookup e "rst" <;>
    cases h3 : SvState.lookup e "req" <;>
    simp [rrD, rrDeclsW, SS, appIn, h1, h2, h3, SvState.set]

/-- A write of a full-width part at bit `0` is the part. -/
theorem insertAt_zero_full (v p : LVec) (h : p.width = v.width) : v.insertAt 0 p = p := by
  apply LVec.ext_getElem?
  intro i
  simp only [LVec.insertAt, Array.getElem?_ofFn]
  by_cases hi : i < v.width
  · have hp : i < p.bits.size := by simp only [LVec.width] at h hi; omega
    rw [dif_pos hi, Array.getElem?_eq_getElem hp]
    simp [h, hi, Array.getElem?_eq_getElem hp]
  · have hp : p.bits.size ≤ i := by simp only [LVec.width] at h hi; omega
    rw [dif_neg hi, Array.getElem?_eq_none hp]

theorem width_resizeU' (v : LVec) (w : Nat) : (v.resizeU w).width = w := by
  simp [LVec.resizeU, LVec.width]

/-- The pick the comb block computes from `req` and `mreq`. -/
def pickV (N : Nat) (q mr : LVec) : LVec :=
  LVec.ternary (.ofLogic (mr.neLogical (z0 N))) (mr.and (mr.not.add (one1.resizeU N)))
    (q.and (q.not.add (one1.resizeU N)))

/-- `mreq` after the comb block. -/
def MRv (q m mr : LVec) : LVec := (q.and m).resizeU mr.width

/-- `pick` after the comb block. -/
def PKv (N : Nat) (q m mr pk : LVec) : LVec := (pickV N q (MRv q m mr)).resizeU pk.width

/-- The state after the comb block. -/
def combS (N : Nat) (ck r q g m mr pk : LVec) : SvState :=
  SS ck r q g m (MRv q m mr) (PKv N q m mr pk)

theorem MRv_width (q m mr : LVec) : (MRv q m mr).width = mr.width := width_resizeU' _ _
theorem PKv_width (N : Nat) (q m mr pk : LVec) : (PKv N q m mr pk).width = pk.width :=
  width_resizeU' _ _

theorem comb_run (N F : Nat) (hF : 20 ≤ F) (ck r q g m mr pk : LVec) :
    runCombProcess2 F (SS ck r q g m mr pk) (combP N) = .ok (combS N ck r q g m mr pk) := by
  obtain ⟨f, rfl⟩ : ∃ f, F = f + 20 := ⟨F - 20, by omega⟩
  simp [combP, combBody, combS, MRv, PKv, pickV, runCombProcess2, execStmt2, execStmts2, evalExpr2,
    resolveLhs2, readSignal, SS, SvState.lookup, SvState.set, insertAt_zero_full]

theorem choose_single (σ : ScheduleOracle) (k i : Nat) : σ.choose k [i] = [i] :=
  List.perm_singleton.mp (σ.choose_perm k [i])

/-- **The comb settle**: one pass computes the block, a second pass changes nothing. -/
theorem settle_rr (N : Nat) (σ : ScheduleOracle) (F k : Nat) (hF : 24 ≤ F) (ck r q g m mr pk : LVec) :
    ∃ k', combSettle2 (rrD N) σ F (SS ck r q g m mr pk) k = .ok (combS N ck r q g m mr pk, k') := by
  have hci : (rrD N).combIndices = [0] := rfl
  have hp0 : (rrD N).processes[0]? = some (combP N) := rfl
  have hpass : ∀ f', 20 ≤ f' → ∀ (ck r q g m mr pk : LVec) (j : Nat),
      combPass2 (rrD N) f' (SS ck r q g m mr pk) (σ.choose j (rrD N).combIndices) =
        .ok (combS N ck r q g m mr pk) := by
    intro f' hf' ck r q g m mr pk j
    rw [hci, choose_single]
    simp only [combPass2, hp0, comb_run N f' hf', Res.ok_bind]
  have hidem : combS N ck r q g m (MRv q m mr) (PKv N q m mr pk) = combS N ck r q g m mr pk := by
    simp only [combS, MRv, PKv, width_resizeU']
  have hpass2 : ∀ f', 20 ≤ f' → ∀ j, combPass2 (rrD N) f' (combS N ck r q g m mr pk)
      (σ.choose j (rrD N).combIndices) = .ok (combS N ck r q g m mr pk) := by
    intro f' hf' j
    show combPass2 (rrD N) f' (SS ck r q g m (MRv q m mr) (PKv N q m mr pk)) _ = _
    rw [hpass f' hf', hidem]
  obtain ⟨f, rfl⟩ : ∃ f, F = f + 24 := ⟨F - 24, by omega⟩
  rw [combSettle2.eq_2, hpass (f + 23) (by omega)]
  simp only [Res.ok_bind]
  by_cases hb : (combS N ck r q g m mr pk == SS ck r q g m mr pk) = true
  · rw [if_pos hb]; exact ⟨_, rfl⟩
  · rw [if_neg hb, combSettle2.eq_2, hpass2 (f + 22) (by omega)]
    simp only [Res.ok_bind]
    rw [beq_self_eq_true, if_pos rfl]
    exact ⟨_, rfl⟩

/-- `pick != '0`, the mask-update condition. -/
def NZ (N : Nat) (pk : LVec) : Bool := (LVec.ofLogic (pk.neLogical (z0 N))).condTrue

/-- The next mask `~((pick << 1) - 1)`. -/
def MaskV (N : Nat) (pk : LVec) : LVec :=
  ((pk.shl (LVec.ofInt 32 1)).sub (one1.resizeU N)).not

/-- The flop updates of a cycle, from the pre-edge `rst`, `gnt`, `mask` and `pick`. -/
def ffQ (N : Nat) (r g m pk : LVec) : NbaQueue2 :=
  if r.condTrue then [("gnt", 0, (z0 N).resizeU g.width), ("mask", 0, (z1 N).resizeU m.width)]
  else ("gnt", 0, pk.resizeU g.width) ::
    (if NZ N pk then [("mask", 0, (MaskV N pk).resizeU m.width)] else [])

theorem ff_run (N F : Nat) (hF : 30 ≤ F) (ck r q g m mr pk : LVec) :
    runEdgeProcess2 F (SS ck r q g m mr pk) [] (ffP N) = .ok (SS ck r q g m mr pk, ffQ N r g m pk) := by
  obtain ⟨f, rfl⟩ : ∃ f, F = f + 30 := ⟨F - 30, by omega⟩
  unfold ffQ NZ
  by_cases h1 : r.condTrue = true <;>
    by_cases h2 : (LVec.ofLogic (pk.neLogical (LVec.ofBitVec (0#N)))).condTrue = true <;>
    simp [ffP, ffBody, MaskV, runEdgeProcess2, execStmt2, execStmts2, evalExpr2, resolveLhs2, readSignal, SS,
      SvState.lookup, evalBinOp, h1, h2]

/-- `gnt` after the edge. -/
def Gv (N : Nat) (r g pk : LVec) : LVec :=
  if r.condTrue then (z0 N).resizeU g.width else pk.resizeU g.width

/-- `mask` after the edge. -/
def Mv (N : Nat) (r m pk : LVec) : LVec :=
  if r.condTrue then (z1 N).resizeU m.width else if NZ N pk then (MaskV N pk).resizeU m.width else m

theorem commit_ff (N : Nat) (ck r q g m mr pk : LVec) :
    commitNba2 (SS ck r q g m mr pk) (ffQ N r g m pk) = SS ck r q (Gv N r g pk) (Mv N r m pk) mr pk := by
  unfold ffQ Gv Mv
  by_cases h1 : r.condTrue = true <;> by_cases h2 : NZ N pk = true <;>
    simp [h1, h2, commitNba2, SS, SvState.lookup, SvState.set, insertAt_zero_full]

/-- **One cycle of `rrD`**, in closed form: the inputs, the comb block, the edge, the commit,
the comb block again. -/
def rrNext (N : Nat) (e : SvState) (ck r q g m mr pk : LVec) : SvState :=
  combS N (appIn e "clk" ck) (appIn e "rst" r) (appIn e "req" q)
    (Gv N (appIn e "rst" r) g (PKv N (appIn e "req" q) m mr pk))
    (Mv N (appIn e "rst" r) m (PKv N (appIn e "req" q) m mr pk))
    (MRv (appIn e "req" q) m mr) (PKv N (appIn e "req" q) m mr pk)

theorem rr_cycle (N : Nat) (σ : ScheduleOracle) (e : SvState) (ck r q g m mr pk : LVec)
    (kk F : Nat) (hF : 64 ≤ F) :
    ∃ k', cycleStep2 (rrD N) σ F e (SS ck r q g m mr pk) kk = .ok (rrNext N e ck r q g m mr pk, k') := by
  have hF' : 24 ≤ F := by omega
  obtain ⟨k1, h1⟩ := settle_rr N σ F kk hF' (appIn e "clk" ck) (appIn e "rst" r) (appIn e "req" q)
    g m mr pk
  obtain ⟨k2, h2⟩ := settle_rr N σ F (k1 + 1) hF' (appIn e "clk" ck) (appIn e "rst" r)
    (appIn e "req" q) (Gv N (appIn e "rst" r) g (PKv N (appIn e "req" q) m mr pk))
    (Mv N (appIn e "rst" r) m (PKv N (appIn e "req" q) m mr pk))
    (MRv (appIn e "req" q) m mr) (PKv N (appIn e "req" q) m mr pk)
  have hE : edgePass2 (rrD N) F (combS N (appIn e "clk" ck) (appIn e "rst" r) (appIn e "req" q) g m mr pk)
      [] (σ.choose k1 (rrD N).edgeIndices) =
      .ok (combS N (appIn e "clk" ck) (appIn e "rst" r) (appIn e "req" q) g m mr pk,
        ffQ N (appIn e "rst" r) g m (PKv N (appIn e "req" q) m mr pk)) := by
    rw [show (rrD N).edgeIndices = [1] from rfl, choose_single]
    simp only [edgePass2, combS, show (rrD N).processes[1]? = some (ffP N) from rfl,
      ff_run N F (by omega), Res.ok_bind]
  have hC : commitNba2 (combS N (appIn e "clk" ck) (appIn e "rst" r) (appIn e "req" q) g m mr pk)
      (ffQ N (appIn e "rst" r) g m (PKv N (appIn e "req" q) m mr pk)) =
      SS (appIn e "clk" ck) (appIn e "rst" r) (appIn e "req" q)
        (Gv N (appIn e "rst" r) g (PKv N (appIn e "req" q) m mr pk))
        (Mv N (appIn e "rst" r) m (PKv N (appIn e "req" q) m mr pk))
        (MRv (appIn e "req" q) m mr) (PKv N (appIn e "req" q) m mr pk) :=
    commit_ff N _ _ _ g m _ _
  have hre : ∀ a b, (rrD N).resetIndices a b = [] := fun _ _ => rfl
  refine ⟨k2, ?_⟩
  simp only [cycleStep2, apply_rr, h1, Res.ok_bind, Res.pure_eq, hre, hE, hC, h2] <;> rfl

/-! ## 3. The state shape, initially and through a cycle -/

/-- The states the design can be in: the seven signals, the registers and nets `N` bits wide. -/
def Shp (N : Nat) (st : SvState) : Prop :=
  ∃ ck r q g m mr pk, st = SS ck r q g m mr pk ∧ g.width = N ∧ m.width = N ∧ mr.width = N ∧ pk.width = N

theorem width_xVec (w : Nat) : (LVec.xVec w).width = w := by
  simp [LVec.xVec, LVec.replicate, LVec.width]

theorem rr_init (N : Nat) : Shp N (initState2 (rrD N)) :=
  ⟨LVec.xVec 1, LVec.xVec 1, LVec.xVec N, LVec.xVec N, LVec.xVec N, LVec.xVec N, LVec.xVec N, rfl,
    width_xVec N, width_xVec N, width_xVec N, width_xVec N⟩

theorem Gv_width (N : Nat) (r g pk : LVec) : (Gv N r g pk).width = g.width := by
  unfold Gv; split <;> exact width_resizeU' _ _

theorem Mv_width (N : Nat) (r m pk : LVec) : (Mv N r m pk).width = m.width := by
  unfold Mv
  split
  · exact width_resizeU' _ _
  · split
    · exact width_resizeU' _ _
    · rfl

theorem rrNext_shp {N : Nat} {e : SvState} {ck r q g m mr pk : LVec} (hg : g.width = N)
    (hm : m.width = N) (hmr : mr.width = N) (hpk : pk.width = N) :
    Shp N (rrNext N e ck r q g m mr pk) :=
  ⟨_, _, _, _, _, _, _, rfl, by rw [Gv_width, hg], by rw [Mv_width, hm],
    by rw [MRv_width, MRv_width, hmr], by rw [PKv_width, PKv_width, hpk]⟩

/-- One cycle from a state of the shape. -/
def Stp (N : Nat) (e prev st : SvState) : Prop :=
  ∃ ck r q g m mr pk, prev = SS ck r q g m mr pk ∧
    (g.width = N ∧ m.width = N ∧ mr.width = N ∧ pk.width = N) ∧ st = rrNext N e ck r q g m mr pk

/-! ## 4. The cycle on known values -/

theorem one_resize {N : Nat} : one1.resizeU N = LVec.ofBitVec (1#N) := by
  have h : one1 = LVec.ofBitVec (BitVec.ofBool true) := LVec.ofLogic_l1
  rw [h, LVec.resizeU_ofBitVec]
  congr 1
  apply BitVec.eq_of_getLsbD_eq
  intro i hi
  simp [hi]

theorem ofInt_one : LVec.ofInt 32 1 = LVec.ofBitVec (1#32) := by
  first | decide | simp [LVec.ofInt] | rfl

/-- `<<` of known vectors (a known shift amount) is `BitVec`'s left shift by the amount's value. -/
theorem shl_ofBitVec {w v : Nat} (x : BitVec w) (y : BitVec v) :
    (LVec.ofBitVec x).shl (LVec.ofBitVec y) = LVec.ofBitVec (x <<< y.toNat) := by
  rw [LVec.eq_ofBitVec_iff]
  refine ⟨by simp [LVec.shl, LVec.shiftAmount?, LVec.width]; exact LVec.width_ofBitVec x, fun i hi => ?_⟩
  simp only [LVec.shl, LVec.shiftAmount?, LVec.toNat?_ofBitVec, Array.getElem?_ofFn,
    LVec.width_ofBitVec, hi, dite_true, BitVec.getLsbD_shiftLeft]
  by_cases h : i < y.toNat
  · simp [h, Logic.ofBool]
  · have h2 : i - y.toNat < w := by omega
    simp [h, h2, LVec.getElem?_ofBitVec]

theorem mr_val {N : Nat} (x m : BitVec N) (mr : LVec) (hmr : mr.width = N) :
    MRv (LVec.ofBitVec x) (LVec.ofBitVec m) mr = LVec.ofBitVec (x &&& m) := by
  simp [MRv, hmr]

theorem pickV_val {N : Nat} (x s : BitVec N) :
    pickV N (LVec.ofBitVec x) (LVec.ofBitVec s) =
      LVec.ofBitVec (if s = 0#N then x &&& (~~~x + 1#N) else s &&& (~~~s + 1#N)) := by
  unfold pickV
  rw [one_resize]
  by_cases h : s = 0#N <;>
    simp [h, LVec.add_ofBitVec]

theorem pk_val {N : Nat} (x m : BitVec N) (mr pk : LVec) (hmr : mr.width = N)
    (hpk : pk.width = N) :
    PKv N (LVec.ofBitVec x) (LVec.ofBitVec m) mr pk = LVec.ofBitVec (RoundRobin.pick x m) := by
  unfold PKv RoundRobin.pick
  rw [mr_val x m mr hmr, pickV_val, hpk, LVec.resizeU_ofBitVec, BitVec.setWidth_eq]

theorem NZ_val {N : Nat} (p : BitVec N) : NZ N (LVec.ofBitVec p) = decide (p ≠ 0#N) := by
  by_cases h : p = 0#N <;> simp [NZ, h]

theorem MaskV_val {N : Nat} (p : BitVec N) :
    MaskV N (LVec.ofBitVec p) = LVec.ofBitVec (~~~((p <<< 1) - 1#N)) := by
  unfold MaskV
  rw [ofInt_one, shl_ofBitVec, one_resize, LVec.sub_ofBitVec, LVec.not_ofBitVec]
  simp

theorem Gv_reset {N : Nat} {g : LVec} (pk : LVec) (hg : g.width = N) :
    Gv N (knownBit true) g pk = LVec.ofBitVec 0#N := by
  simp [Gv, hg]

theorem Mv_reset {N : Nat} {m : LVec} (pk : LVec) (hm : m.width = N) :
    Mv N (knownBit true) m pk = LVec.ofBitVec (BitVec.allOnes N) := by
  simp [Mv, hm]

theorem Gv_run {N : Nat} {g : LVec} (p : BitVec N) (hg : g.width = N) :
    Gv N (knownBit false) g (LVec.ofBitVec p) = LVec.ofBitVec p := by
  simp [Gv, hg]

theorem Mv_run {N : Nat} (x mk : BitVec N) :
    Mv N (knownBit false) (LVec.ofBitVec mk) (LVec.ofBitVec (RoundRobin.pick x mk)) =
      LVec.ofBitVec (RoundRobin.next x mk) := by
  unfold Mv RoundRobin.next
  rw [condTrue_knownBit, NZ_val, MaskV_val]
  by_cases h : RoundRobin.pick x mk = 0#N <;> simp [h]

theorem rrNext_reset {N : Nat} {e : SvState} {ck r q g m mr pk : LVec} {x : BitVec N}
    (hb : BitIs e "rst" true) (hq : SvState.lookup e "req" = some (LVec.ofBitVec x))
    (hg : g.width = N) (hm : m.width = N) (hmr : mr.width = N) (hpk : pk.width = N) :
    rrNext N e ck r q g m mr pk = SS (appIn e "clk" ck) (knownBit true) (LVec.ofBitVec x)
      (LVec.ofBitVec 0#N) (LVec.ofBitVec (BitVec.allOnes N))
      (LVec.ofBitVec (x &&& BitVec.allOnes N))
      (LVec.ofBitVec (RoundRobin.pick x (BitVec.allOnes N))) := by
  have hr : appIn e "rst" r = knownBit true := BitIs.appIn_eq hb r
  have hq' : appIn e "req" q = LVec.ofBitVec x := by simp only [appIn, hq, Option.getD_some]
  unfold rrNext combS
  rw [hr, hq', Gv_reset _ hg, Mv_reset _ hm,
    mr_val x _ (MRv (LVec.ofBitVec x) m mr) (by rw [MRv_width, hmr]),
    pk_val x _ (MRv (LVec.ofBitVec x) m mr) (PKv N (LVec.ofBitVec x) m mr pk)
      (by rw [MRv_width, hmr]) (by rw [PKv_width, hpk])]

theorem rrNext_run {N : Nat} {e : SvState} {ck r q g m mr pk : LVec} {x mk : BitVec N}
    (hb : BitIs e "rst" false) (hq : SvState.lookup e "req" = some (LVec.ofBitVec x))
    (hm : m = LVec.ofBitVec mk) (hg : g.width = N) (hmr : mr.width = N) (hpk : pk.width = N) :
    rrNext N e ck r q g m mr pk = SS (appIn e "clk" ck) (knownBit false) (LVec.ofBitVec x)
      (LVec.ofBitVec (RoundRobin.pick x mk)) (LVec.ofBitVec (RoundRobin.next x mk))
      (LVec.ofBitVec (x &&& RoundRobin.next x mk))
      (LVec.ofBitVec (RoundRobin.pick x (RoundRobin.next x mk))) := by
  subst hm
  have hr : appIn e "rst" r = knownBit false := BitIs.appIn_eq hb r
  have hq' : appIn e "req" q = LVec.ofBitVec x := by simp only [appIn, hq, Option.getD_some]
  unfold rrNext combS
  rw [hr, hq', pk_val x mk mr pk hmr hpk, mr_val x mk mr hmr, Gv_run _ hg, Mv_run,
    mr_val x _ (LVec.ofBitVec (x &&& mk)) (LVec.width_ofBitVec _),
    pk_val x _ (LVec.ofBitVec (x &&& mk)) (LVec.ofBitVec (RoundRobin.pick x mk))
      (LVec.width_ofBitVec _) (LVec.width_ofBitVec _)]

/-! ## 5. The rank model -/

/-- The known `N`-bit value of signal `n` (`0`-filled where unknown; read only in invariant states). -/
def bvOf (N : Nat) (n : String) (st : SvState) : BitVec N :=
  BitVec.ofNat N ((SvState.lookup st n).getD (LVec.xVec N)).toNat

theorem bvOf_gnt {N : Nat} {ck r q m mr pk : LVec} {g : BitVec N} :
    bvOf N "gnt" (SS ck r q (LVec.ofBitVec g) m mr pk) = g := by
  simp [bvOf, SS, SvState.lookup, BitVec.ofNat_toNat]

theorem bvOf_mask {N : Nat} {ck r q g mr pk : LVec} {mk : BitVec N} :
    bvOf N "mask" (SS ck r q g (LVec.ofBitVec mk) mr pk) = mk := by
  simp [bvOf, SS, SvState.lookup, BitVec.ofNat_toNat]

theorem SS_mask {ck r q g m mr pk ck' r' q' g' m' mr' pk' : LVec}
    (h : SS ck r q g m mr pk = SS ck' r' q' g' m' mr' pk') : m = m' := by
  simp only [SS, List.cons.injEq, Prod.mk.injEq, true_and, and_true] at h
  exact h.2.2.2.2.1

open Classical in
/-- The edge of a thermometer mask (`0` for any other vector). -/
noncomputable def edgeOf {N : Nat} (mk : BitVec N) : Nat :=
  if h : ∃ e, RoundRobin.Thermo mk e then Classical.choose h else 0

theorem edgeOf_eq {N : Nat} {mk : BitVec N} {e : Nat} (h : RoundRobin.Thermo mk e) : edgeOf mk = e := by
  have hex : ∃ e, RoundRobin.Thermo mk e := ⟨e, h⟩
  unfold edgeOf
  rw [dif_pos hex]
  exact (Classical.choose_spec hex).unique h

/-- **The invariant** of the snapshots from a reset on: every signal but `clk` known, the mask a
thermometer, `mreq` and `pick` the comb block's values. -/
def ArbInv (N : Nat) (st : SvState) : Prop :=
  ∃ (ck : LVec) (b : Bool) (x g mk : BitVec N) (e : Nat),
    st = SS ck (knownBit b) (LVec.ofBitVec x) (LVec.ofBitVec g) (LVec.ofBitVec mk)
      (LVec.ofBitVec (x &&& mk)) (LVec.ofBitVec (RoundRobin.pick x mk)) ∧ RoundRobin.Thermo mk e

theorem pick_grants {N : Nat} (x mk : BitVec N) : Tasks.Arbiter.Grants x (RoundRobin.pick x mk) :=
  ⟨fun _ _ hi hj => RoundRobin.pick_atMostOne hi hj, fun _ hi => RoundRobin.pick_sub hi,
    fun hx h => hx (RoundRobin.pick_eq_zero.1 h)⟩

/-- **The rank model** of the reference at `N`, with the response bound `N - 1`. -/
noncomputable def model (N : Nat) (hN : 1 ≤ N) :
    Tasks.Arbiter.task.RankModel N (N - 1) (design.sem N) where
  Shape := Shp N
  Step := Stp N
  init := by rw [rr_sem_eq N hN]; exact rr_init N
  cycle := by
    rintro σ F e prev k st k' ⟨ck, r, q, g, m, mr, pk, rfl, hw⟩ hc
    rw [rr_sem_eq N hN] at hc
    obtain ⟨k2, h2⟩ := rr_cycle N σ e ck r q g m mr pk k 64 (Nat.le_refl _)
    exact ⟨ck, r, q, g, m, mr, pk, rfl, hw, (Prod.mk.inj (cycleStep2_det hc h2)).1⟩
  shape := by
    rintro e prev st - ⟨ck, r, q, g, m, mr, pk, -, ⟨hg, hm, hmr, hpk⟩, rfl⟩
    exact rrNext_shp hg hm hmr hpk
  Inv := fun _ st => ArbInv N st
  out := fun st => (bvOf N "gnt" st, ())
  shows := by
    rintro - st ⟨ck, b, x, g, mk, e, rfl, -⟩
    show SvState.lookup _ "gnt" = some (LVec.ofBitVec (bvOf N "gnt" _)) ∧ True
    rw [bvOf_gnt]
    exact ⟨by simp [SS, SvState.lookup], trivial⟩
  rank := fun o st => RoundRobin.dist N (edgeOf (bvOf N "mask" st)) o.val
  rank_le := by
    rintro o - st ⟨ck, b, x, g, mk, e, rfl, hth⟩
    show RoundRobin.dist N (edgeOf (bvOf N "mask" _)) o.val ≤ N - 1
    rw [bvOf_mask, edgeOf_eq hth]
    exact RoundRobin.dist_le hth.1 o.isLt
  reset := by
    rintro e prev st ⟨x, ⟨⟩⟩ - ⟨ck, r, q, g, m, mr, pk, -, ⟨hg, hm, hmr, hpk⟩, rfl⟩ hb hx
    have hq : SvState.lookup e "req" = some (LVec.ofBitVec x) := hx.1
    rw [rrNext_reset hb hq hg hm hmr hpk]
    refine ⟨⟨_, true, x, 0#N, BitVec.allOnes N, 0, rfl, RoundRobin.thermo_allOnes N⟩, ?_⟩
    show bvOf N "gnt" _ = 0#N
    rw [bvOf_gnt]
  step := by
    rintro e prev st - ⟨x, ⟨⟩⟩ - ⟨ck, r, q, g, m, mr, pk, rfl, ⟨hg, hm, hmr, hpk⟩, rfl⟩
      ⟨ck', b', xp, gp, mk, ed, hprev, hth⟩ hb hx
    have hq : SvState.lookup e "req" = some (LVec.ofBitVec x) := hx.1
    have hmm : m = LVec.ofBitVec mk := SS_mask hprev
    have hmask : bvOf N "mask" (SS ck r q g m mr pk) = mk := by rw [hmm, bvOf_mask]
    rw [rrNext_run hb hq hmm hg hmr hpk]
    obtain ⟨e', hth', hprog⟩ := RoundRobin.step (x := x) hth
    refine ⟨⟨_, false, x, _, _, e', rfl, hth'⟩, ?_, fun o ho => ?_⟩
    · show Tasks.Arbiter.Grants x (bvOf N "gnt" _)
      rw [bvOf_gnt]
      exact pick_grants x mk
    · have ho' : x.getLsbD o.val = true := ho
      by_cases hp : (RoundRobin.pick x mk).getLsbD o.val = true
      · left
        show (bvOf N "gnt" _).getLsbD o.val = true
        rw [bvOf_gnt]
        exact hp
      · right
        show RoundRobin.dist N (edgeOf (bvOf N "mask" _)) o.val <
          RoundRobin.dist N (edgeOf (bvOf N "mask" _)) o.val
        rw [bvOf_mask, hmask, edgeOf_eq hth', edgeOf_eq hth]
        exact hprog o.val o.isLt ho' (by simpa using hp)

/-! ## 6. Structure, and the statement -/

theorem rr_interface (N : Nat) (hN : 1 ≤ N) : Tasks.Arbiter.task.Interface N (design.sem N) := by
  rw [rr_sem_eq N hN]
  exact ⟨rfl, rfl, by show (["clk", "rst", "req", "gnt", "mask", "mreq", "pick"] : List String).Nodup; decide⟩

theorem rr_moore (N : Nat) : MooreOut (rrD N) := by
  apply mooreOut_of_combTargets
  · simp [rrD, rrDeclsW, Design2.outputNames, Design2.inputNames]
  · simp [rrD, combP, combBody, ffP, ffBody, Process2.isCombPhase, processTargets, stmtTargets, stmtListTargets,
      stmtOptTargets, lhsTargets, Design2.outputNames, rrDeclsW]

theorem rr_disciplined (N : Nat) (hN : 1 ≤ N) : Tasks.Arbiter.task.Disciplined (design.sem N) := by
  rw [rr_sem_eq N hN]
  refine ⟨⟨by simp [Tasks.Arbiter.task, rrD, rrDeclsW, Design2.inputNames], fun p hp => ?_⟩, rr_moore N⟩
  have hm : p = combP N ∨ p = ffP N := by simpa [rrD] using hp
  rcases hm with rfl | rfl <;>
    simp [Tasks.Arbiter.task, combP, combBody, ffP, ffBody, edgeClock, asyncReset, processDataNames, stmtNames,
      stmtOptNames, stmtListNames, lhsNames, exprNames, Process2.isEdgePhase]

/-- **Every power-up state has the shape** (txtask-v2's rule 2): the seven signals in declaration
order, each at its declared width. -/
theorem rr_powerUp (N : Nat) : ∀ st, PowerUp (rrD N) st → Shp N st := by
  intro st h
  have h' : st.map Prod.fst = (rrDeclsW N).map Decl.name ∧
      ∀ b ∈ st.zip (rrDeclsW N), b.1.2.width = b.2.width ∧ b.1.2.allKnown = true := h
  rw [rrDeclsW] at h'
  obtain ⟨ck, r1, rfl, -, -, h1⟩ := powerUp_cons.mp h'
  obtain ⟨r, r2, rfl, -, -, h2⟩ := powerUp_cons.mp h1
  obtain ⟨q, r3, rfl, -, -, h3⟩ := powerUp_cons.mp h2
  obtain ⟨g, r4, rfl, hg, -, h4⟩ := powerUp_cons.mp h3
  obtain ⟨m, r5, rfl, hm, -, h5⟩ := powerUp_cons.mp h4
  obtain ⟨mr, r6, rfl, hmr, -, h6⟩ := powerUp_cons.mp h5
  obtain ⟨pk, r7, rfl, hpk, -, h7⟩ := powerUp_cons.mp h6
  obtain rfl := powerUp_nil.mp h7
  exact ⟨ck, r, q, g, m, mr, pk, rfl, hg, hm, hmr, hpk⟩

theorem rr_terminates (N : Nat) (hN : 1 ≤ N) : TerminatesPU (design.sem N) := by
  rw [rr_sem_eq N hN]
  refine TerminatesPU.of_invariant (Shp N) (rr_powerUp N) (fun σ => ⟨64, ?_⟩) ?_
  · rintro e _ kk ⟨ck, r, q, g, m, mr, pk, rfl, hg, hm, hmr, hpk⟩
    obtain ⟨k', h⟩ := rr_cycle N σ e ck r q g m mr pk kk 64 (Nat.le_refl _)
    exact ⟨_, _, h, rrNext_shp hg hm hmr hpk⟩
  · first
    | rfl
    | simp [rrD, combP, combBody, ffP, ffBody, Process2.hasQualifiedCase, Stmt2.hasQualifiedCase,
        Stmt2.listHasQualifiedCase]

theorem one1_allKnown : one1.allKnown = true := by
  rw [show one1 = LVec.ofBitVec (BitVec.ofBool true) from LVec.ofLogic_l1]
  exact LVec.allKnown_ofBitVec _
theorem one1_width : one1.width = 1 := rfl

/-- **Rule 3**: no construct of the design can create an `x` from known operands (every operand
pair of `&`, `!=`, `?:` has one width; no division, no dynamic index). -/
theorem rr_xsafe (N : Nat) (hN : 1 ≤ N) : XSafe (design.sem N) := by
  rw [rr_sem_eq N hN]
  simp [XSafe, xsafeB, rrD, rrDeclsW, combP, ffP, combBody, ffBody, xsProc, xsStmt, xsStmts, xsOpt,
    xsLhs, xsWidth, binW, sigWidth, ofInt_one, one1_allKnown, one1_width]

/-- **The reference satisfies the arbiter statement**, at every `N` in range. -/
theorem solution : Goal := by
  intro N hN
  obtain ⟨hN1, -⟩ := hN
  exact Tasks.Arbiter.task.satisfiedAt_of_rank (rr_interface N hN1) (rr_disciplined N hN1)
    (rr_terminates N hN1) (model N hN1)
    (fun st h => rr_powerUp N st (by rw [rr_sem_eq N hN1] at h; exact h)) (rr_xsafe N hN1)

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

end Submission

The netlist

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

Schematic

drawn at N = 4

Drawn at N = 4, a display instance; scored at N = 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.

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: 48 cells here, 103 at the scoring point. The register-to-register critical path at N = 4 (11 cells, ending at the flip-flop input _05_ falling; a period of 1 869 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: 48 cells, 15 nand2_1, 11 and2_1, 8 dfxtp_1, 6 nor2_1, 5 nor2b_1, 2 or2_1, 1 nand2b_1. There (measured, not ranked): 357.84 µm², 1 869 ps. Open the drawing on its own (SVG, 32.4 KB) to pan and zoom it with the browser's own controls.

Critical path

at N = 8 · scored

The path the ranked register-to-register period ends on, at the scoring point N = 8: 16 nets, 15 cells, to the flip-flop input _009_ falling; the period, 2 826 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, the critical path is 11 cells to the flip-flop input _05_ falling (a period of 1 869 ps there); each cell is a link to it in the drawing:

\_0_[0]
_41_ nand2_1
_44_ and2_1
_46_ nor2b_1
_47_ and2_1
_53_ nand2_1
_54_ and2_1
_67_ and2_1
_68_ and2_1
_69_ and2_1
_70_ and2_1
_71_ or2_1
_05_ flip-flop D

#	net	edge	driven by	cell	arrival (ps)	transition (ps)	stage (ps)
0	`\_0_[1]`	rise	flop Q	–	314.6	59.1
1	`_037_`	fall	`_094_`	`nand2_1`	362.6	33.5	48.0
2	`_038_`	fall	`_095_`	`and2_1`	512.7	40.1	150.1
3	`_039_`	fall	`_096_`	`and2_1`	665.6	40.1	152.9
4	`_040_`	fall	`_097_`	`and2_1`	818.4	40.0	152.8
5	`_042_`	fall	`_099_`	`nor2b_1`	945.3	37.2	126.9
6	`_043_`	fall	`_100_`	`and2_1`	1 097.0	40.1	151.7
7	`_044_`	fall	`_101_`	`and2_1`	1 249.7	40.0	152.7
8	`_045_`	fall	`_102_`	`and2_1`	1 452.1	90.8	202.4
9	`_050_`	fall	`_108_`	`mux2_1`	1 779.7	61.6	327.6
10	`_080_`	fall	`_145_`	`and2_1`	1 937.5	36.4	157.8
11	`_081_`	fall	`_146_`	`nor2b_1`	2 059.0	33.6	121.5
12	`_082_`	fall	`_147_`	`and2_1`	2 204.5	36.3	145.5
13	`_086_`	fall	`_151_`	`and2_1`	2 374.1	76.9	169.6
14	`_087_`	fall	`_152_`	`and2_1`	2 530.2	29.7	156.1
15	`_009_`	fall	`_153_`	`or2_1`	2 718.1	42.8	187.9

Cells

at N = 8 · scored

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

cell	count	µm² each	µm² in all	share
`dfxtp_1`	16	20.0192	320.3072	41.6%
`and2_1`	26	6.2560	162.6560	21.1%
`nand2_1`	32	3.7536	120.1152	15.6%
`nor2b_1`	12	6.2560	75.0720	9.8%
`nand2b_1`	6	6.2560	37.5360	4.9%
`nor2_1`	8	3.7536	30.0288	3.9%
`or2_1`	2	6.2560	12.5120	1.6%
`mux2_1`	1	11.2608	11.2608	1.5%
total	103		769.4880

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

Legality: worst load 0.107 × max_capacitance, worst transition 0.118 × 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)

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

cell	count	GE each	GE total
`NAND`	32	1.000	32.000
`AND`	26	1.333	34.658
`DFF_P`	16	5.333	85.328
`ANDNOT`	12	1.333	15.996
`NOR`	8	1.000	8.000
`ORNOT`	6	1.333	7.998
`OR`	2	1.333	2.666
`MUX`	1	2.333	2.333
total	103		188.979

The record

task: arbiter
player: svgolf-reference
assisted by: Claude (Anthropic)
submitted: 2026-11-09
notes: reference solution
scoring point: N = 8
design: rr_mask.sv sha256 f8b02272b7f264d935673b0fa5522fbfb877bdf2985b5c1ad27b861b3a5de784
proof: rr_mask.lean sha256 e082faec9a4fd3c5c00c4ebadace2e3d3007e320a0b5f886b2d4e23c8bc52004: the proof of the reference rr_mask (rr_mask.lean, 487 code lines)
canonical text: sha256 b0bbcf311076bbbb383739ead07fde6ae639ee5deb284c643b1e943ab7d0af67
record hash: 84da5a4152db28e4aed74c6cb7f37ec329dc636a4433aff3946fc34e6f60453b
downloads: 84da5a4152db.sv 84da5a4152db.lean 84da5a4152db.json

The proof

code lines: 487
build time: 4.26 s
axioms: Classical.choice, Quot.sound, propext
tactics seen: decide, omega, simp
imports: Submission.Design, LeanModels.Sv.Gen2, LeanModels.Sv.Hier2Gen, LeanModels.Sv.Known2, LeanModels.Sv.Mono2, LeanModels.Sv.SeqFamily, SvGolf.Seq, SvGolf.React, SvGolf.RoundRobin

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: a60960b454b2b36f8f70de80cc69bd944808d6b5f553fb2dd66f21c1507c372a

the checker's files (sha256)

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

Post-synthesis check

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 segments: a reset entry, then entries with rst = 0, the last segment a long run without a reset. On every cycle of every run the netlist's outputs met the task's guarantee, and the outputs sampled just before each rising edge equalled the snapshot before (the Moore sample). Where the two runs start from the same state (seed 0, the all-zeros power-up, unless the pinned flow turned a register into a constant 1) the netlist's outputs equalled ls-sv's bit for bit; from two different power-ups a correct design may answer differently, and ls-sv's outputs met the guarantee too. The check found no mismatch. The stimulus is a sample of the input traces: a guard against the two tools disagreeing, not a proof.

mode: full
points: N = 3, N = 5, N = 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 segments per seed
clock cycles: 1 687 035 in all
mismatches: 0
salted: no (the default empty salt: anyone can run this exact stimulus again)
scored netlist: sha256 e072fb19e91c79f0adcdfa0ef3709731d0c642bc4c38b853cbedd53cc6f85d0e

point	seeds	clock cycles	segments	netlist sha256
N = 3	8	561 435	192	`c5d0e3505f40`
N = 5	8	562 046	192	`2903b644d97e`
N = 8	8	563 554	192	`e072fb19e91c`

every seed's run (24)

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.

point	seed	ls-sv power-up	netlist randSeed	clock cycles	segments	draw
N = 3	0	`zeros`	`51693527`	70 191	24	`91e7bd9c85d2`
N = 3	1	`seed:7789121772795600815`	`1467165941`	70 194	24	`ff4494b3cb58`
N = 3	2	`seed:14490556364649400802`	`507060241`	70 134	24	`6e9e9dab38e7`
N = 3	3	`seed:5524233232498431859`	`1310969194`	70 213	24	`59f4eb1b3a7f`
N = 3	4	`seed:16777839557804680643`	`1451429604`	70 166	24	`b70ed7f8dc34`
N = 3	5	`seed:2322128566058997970`	`1850555024`	70 185	24	`9fd37805cb9e`
N = 3	6	`seed:7311075774938213980`	`2061637034`	70 185	24	`5854ccc01bce`
N = 3	7	`seed:12684631304222669956`	`1154632371`	70 167	24	`b8adc5781f9d`
N = 5	0	`zeros`	`1924181115`	70 218	24	`a2926a835c5a`
N = 5	1	`seed:11902293005348841532`	`391878814`	70 264	24	`97821ffe52f8`
N = 5	2	`seed:9315066348523995232`	`422314970`	70 201	24	`1687ae38eb15`
N = 5	3	`seed:6069459429182239504`	`112963290`	70 262	24	`4a4508272d7d`
N = 5	4	`seed:10194850246807243092`	`2058360770`	70 248	24	`f52d4d97d7b8`
N = 5	5	`seed:17594728819290675883`	`120123748`	70 262	24	`32c058f0e81e`
N = 5	6	`seed:18225073965911655590`	`877776761`	70 310	24	`a4d17808209a`
N = 5	7	`seed:6263245331832618504`	`841388205`	70 281	24	`fb8ef5561734`
N = 8	0	`zeros`	`295690157`	70 507	24	`ed6b3ddc4f33`
N = 8	1	`seed:1510559514096927918`	`1551029803`	70 423	24	`67b30be23a85`
N = 8	2	`seed:13010624561886874679`	`251704913`	70 597	24	`751e5f9acdad`
N = 8	3	`seed:18261098257774128044`	`1203556423`	70 454	24	`fbdd7938d96b`
N = 8	4	`seed:14402032186337480843`	`1616705840`	70 415	24	`4beefbb0c098`
N = 8	5	`seed:9660298031941446966`	`510464552`	70 398	24	`726e04a4aefc`
N = 8	6	`seed:6798390078260723393`	`1450385479`	70 385	24	`e009927d95a5`
N = 8	7	`seed:14968646365065069664`	`386874794`	70 375	24	`42dcc9951d74`

Area against time

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

proved reference
the Pareto front of the entries

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

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

the designs as numbers, by score

design	kind	area (µm²)	time (ps)	score (µm²·ns)
`rr_mask` · this design	proved reference · par	769.49	2 826	2175

proved reference
the Pareto front of the entries

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

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

the designs as numbers, by score

design	kind	area (µm²)	time (ps)	score (µm²·ns)
`rr_mask` · this design	proved reference · par	12.160	464	5.642

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/arbiter/reference/rr_mask.sv --task tasks/arbiter --seq --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256: a60960b454b2b36f8f70de80cc69bd944808d6b5f553fb2dd66f21c1507c372a
ppa.netlist_sha256: e072fb19e91c79f0adcdfa0ef3709731d0c642bc4c38b853cbedd53cc6f85d0e
ppa.repair.netlist_sha256: 54e9b0edaecf4e3c51a9b662f32499c955f2ccb7db4f1e9647c3ba25d0050792
ppa.area_e4um2_sky130: 7694880
ppa.delay_ps_sky130: 2826

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

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/arbiter/reference/rr_mask.sv --task tasks/arbiter --seq --pdk asap7 --no-mapped \
    --json out.json

Expect, in out.json:

ppa.netlist_sha256: e072fb19e91c79f0adcdfa0ef3709731d0c642bc4c38b853cbedd53cc6f85d0e
ppa.repair.netlist_sha256: 35b5e4557491b5cd59938c64b6398742f05c14168f684945f444942c7ddd2992
ppa.area_e5um2_asap7: 1215972
ppa.delay_ps_asap7: 464

leaderboard/asap7/arbiter.json keeps these numbers; python3.12 leaderboard/leaderboard.py asap7 --rescore --task arbiter 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=84da5a4152db28e4aed74c6cb7f37ec329dc636a4433aff3946fc34e6f60453b
mkdir -p rec/arbiter && cp "$H.json" "$H.sv" "$H.lean" rec/arbiter/
python3.12 leaderboard/leaderboard.py verify --data-dir rec --task arbiter --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.