What the checker refuses, and what you can write

svGolf asks for two things about each design you submit: a Lean proof that it meets the task's trusted statement under the ls-sv semantics, and a score from a pinned Yosys flow. The checker refuses a design or a proof when the proof and the score could be about different circuits, or when the evidence could be forged. This document lists every refusal the checker makes, why, and what you can write instead, then says which refusals are meant to go away and which never will.

It has two halves that are easy to confuse. The checker's own stages (source gate, banlist, fourstate, statement, axioms, score, post-synthesis check) are described below stage by stage. The language tier (ls-sv, the semantics your proof is about) refuses more constructs than the checker does; those show up as extract or design failures and are summarised near the end and listed in full in docs/sv-refusals.md of the lean-surfaces repository.

This file is generated from docs/sv-refusals.json of lean-surfaces by tools/gen_sv_refusals.py and is written to be read without the rest of that repository: links to lean-surfaces documents are given as repository paths.

How to read this page

Every restriction has one of four states; a row marked proposed carries a classification that is not yet confirmed.

The never rows rest on these principles:

The pipeline: where a refusal can happen

check.py runs the stages in this order and stops at the first that refuses.

Policies

• Combinational tasks only for now. Clocked designs, registers and pipelines are refused until the sequential layer exists (decided 2026-10-29).
• Where the pipeline tools split, the design is refused, never decided for one side: slang / ls-sv (the proof), Yosys (the score), Verilator and Xcelium are compared, and a shape they read differently is a loud refusal. A difference that only Icarus shows is a declared departure, not a refusal (decided 2026-10-31), and so is one that only Xcelium shows against LRM text the other tools follow (decided 2026-11-01: \a \v \f are admitted).
• A program slang rejects is rejected, and LRM-legal nondeterminism is to be modelled rather than forbidden (decided 2026-10-31). No construct is admitted on the second ruling yet: the model does not exist, and the audit found that the rows it was first thought to cover are not LRM nondeterminism (self-reading always_comb: the LRM's answer is deterministic and the synthesizers compute another; settling combinational loops: refused by fourstate, and some hold state).
• Everything the proof and the score could read differently is refused exactly, before any proof is tried (the x/z rules, the source gate), and the post-synthesis check is the backstop for the disagreements nobody has found.
• No other restrictions. Beyond the per-task operator banlist and these safety gates, write any SystemVerilog ls-sv can load.
• Contestants may add features to ls-sv by pull request, and the maintainers approve every such PR. See 'How a refusal becomes allowed'.
• Proofs are symbolic and parametric (for all N). bv_decide is not supported for now (it runs an external SAT solver, which the checker does not support: decided 2026-11-01); native_decide is banned in submissions.
• No host access in the SystemVerilog text. A submitted design cannot read host files (decided 2026-10-31); by the same principle (proposed, to confirm) it cannot write them, run programs, read the environment, write dumps or call native code. The source gate refuses the constructs; the console tasks ($display, $write, $finish, ...) stay. The Lean file is not covered (see the limits).

Stage source: one program for both tools

Yosys and slang (the frontend your proof is about) read the same file differently when it contains directives, attributes or pragma comments. The gate refuses those and hands every later stage one canonical text with all comments stripped. It also refuses every construct that reaches the machine the checker runs on ($readmemh, $fopen, $system, $value$plusargs, $dumpfile, DPI, ...): Yosys opens a $readmemh file itself while it reads the design.

What you can write:

`timescale 1ns/1ps
module band #(parameter int N = 4)(input logic [N-1:0] a, b, output logic [N-1:0] y);
  // comments are fine: they are stripped
  assign y = a & b;
endmodule

What is refused:

`ifdef SYNTHESIS
  assign y = a & b;     // Yosys defines SYNTHESIS, slang does not
`else
  assign y = a | b;
`endif
(* keep *) wire t;      // attribute: Yosys gives it a meaning
// synopsys translate_off
initial $readmemh("/etc/hosts", mem);   // host file: refused
initial $system("id");                 // host program: refused
import "DPI-C" function int c_fn(int x);   // native code: refused

Stage source and fourstate: no x or z may arise

ls-sv computes with unknown values like an IEEE simulator; Yosys treats them as don't-cares. Wherever an x reaches a decision the proved and the scored circuits can differ, and you choose where. Every SOURCE of an x or z is refused, exactly. A casez item may use z and ?, a casex item x, z, ?.

What you can write:

always_comb begin
  casez (a[1:0])
    2'b1?: y = 1'b1;     // wildcard digit in a casez item: allowed
    default: y = 1'b0;
  endcase
end

What is refused:

assign y = a[0] ? 1'bz : a[1];     // z literal
localparam logic [1:0] K = 2'd1 / 2'd0;   // constant division by zero is x
logic [3:0] m; ... m[{1'b1, a[1:0]}]     // index can leave the range: x
logic u; assign y = u ? a : b;           // u is undriven

Stage banlist: the task's banned operators

A task bans the run-time operator that IS the task, plus whatever Yosys merges into the same cell (alumacc turns + and - chains into the cells of *). Constant arithmetic (parameters, genvar loops, index arithmetic over parameters and genvars) and comparisons stay allowed. Which operators are banned is per task: add, mul and _example ban + - * / % **; fdivp bans / % **.

What you can write:

for (genvar i = 0; i < N; i++) begin : g
  assign s[i] = a[i] ^ b[i] ^ c[i];     // gates, not +
  assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i]));   // i+1 is constant arithmetic
end

What is refused:

assign s = a + b + cin;          // run-time + in a task that bans it
assign y = a * b;                // run-time *
assign n = $countones(a);        // Yosys builds it from $add cells
assign p = arr.sum();            // array reduction = run-time +

Stages extract and design: the language tier and the parameter list

The proof is about what the pinned extractor and the ls-sv loader accept. A construct they refuse fails here with the tier's own message. The top module's overridable parameters must be exactly the task's, by name and order, because the scoring script overrides them by name.

What you can write:

module band #(parameter int N = 4)(input logic [N-1:0] a, b, output logic [N-1:0] y);

What is refused:

module band #(parameter int N = 4, parameter int M = 2)(...);   // an extra parameter
module band #(parameter bit [3:0] N = 4)(...);               // narrower than int: N = 16 reads as 0

Stage imports: the proof file

The checker builds only SvGolf, the task modules and the evaluator; a module outside the allowlist is unaudited code outside the trusted base. Mathlib and its packages (Batteries, Aesop, Qq, ProofWidgets, Plausible, ImportGraph, LeanSearchClient) are on the allowlist. One solution file in v0.

What you can write:

import Submission.Design
import LeanModels.Sv.Ingest2
import SvGolf.Comb
import Mathlib.Tactic.Ring

What is refused:

import Examples.python.tri.proof
import LeanModels.Python.Semantics
import Mathlib2.Tactic     -- a lookalike
import MyHelpers

The trusted statement: interface, clocks, termination, function, range

The statement is a Lean Prop fixed by the task (SvGolf/Task.lean). A design that satisfies it must have exactly the task's ports, no edge-phase process, a completed run for every schedule and stimulus, and the task's function at every cycle, for every N in the range. These are not rules you can argue with: a design that breaks one has no proof of the statement, and the repository checks the refutations in tests/*/negative/Refute.lean.

What is refused:

module adder(input logic [N-1:0] a, b, input logic ci, ...);   // port named ci, not cin
output logic [N:0] s;                                           // merged {cout, sum}
always_ff @(posedge clk) s <= a ^ b;                           // any edge process

Stages comparator, leanchecker, integrity: the proof itself

The kernel must accept your theorem from the task's allowed axioms alone. Everything that would let a proof depend on something other than the kernel is refused.

What you can write:

theorem solution : Submission.Goal := by
  -- induction on bit indices, decide +kernel for fixed-size subgoals
  ...

What is refused:

theorem solution : Submission.Goal := by native_decide   -- trusts the compiler
theorem solution : Submission.Goal := by sorry
axiom cheat : Submission.Goal

Stages score and postsynth: the scored netlist

The score is area in NAND2 gate equivalents and depth, measured on the pinned Yosys + ABC netlist. The post-synthesis check then simulates ls-sv and the scored netlist on the task's vector budget and rejects any difference; it is sampling, so a difference confined to a tiny input region can slip through, which is what the static rules above are for. A rejection here is a bug report: either ls-sv or Yosys is wrong.

What is refused:

always_ff @(posedge clk) y <= a & b;    // a flip-flop in the netlist: not priced

Task authors: task.json

Mistakes in a task definition fail loudly so a typo cannot silently change the vector budget or the banlist.

What is refused:

"banlist": {"operators": ["<<"]}     // unknown operator
"allow_bv_decide": true                  // an infrastructure error: no external solvers

Constructs the ls-sv tier refuses, as seen from svGolf

The extract and design stages pass on the refusals of the language tier (ls-sv). The ones a task is most likely to run into, with what has to exist first:

And what will not be accepted for as long as the tools disagree or the construct is not hardware:

• Anything the PIPELINE tools read differently (slang and ls-sv for the proof, Yosys for the score, Verilator and Xcelium as simulators; P-NO-SILENT-PICK, and P-SAME-PROGRAM where Yosys differs from slang): narrow net actuals into wider net inputs, partly out-of-range part selects, bit-select indexes wider than 32 bits, context-width port actuals, instance-parameter overrides evaluated at different widths, initialized variables with a second writer, the hex string escape \xHH (Yosys and Xcelium read the letter x; the named control escapes \a \v \f are admitted since 2026-11-01, Xcelium alone differs), self-reading always_comb (the event-driven simulators against the synthesizers). A difference that only Icarus (or only Xcelium, against LRM text the others follow) shows is a declared departure, not a refusal.
• Programs slang rejects (P-SAME-PROGRAM; what the slang driver reports: parse and elaboration errors always, analysis errors too since 2026-11-01 (the banlist front check and the fourstate stage read them), with what is still unread listed under 'limits'): undeclared names, two writers of one bit when one of them is always_comb/always_ff, writing an input port, an undefined module, an always without timing control. Yosys alone would accept several of them silently.
• Tool directives of any kind (P-NO-TOOL-DIRECTIVES): `ifdef SYNTHESIS, attributes, synthesis-pragma comments.
• Delays, timing and randomness in a combinational task (P-NO-TIME, P-DETERMINISM); non-hardware constructs such as classes, strings, reals, dynamic memory and fork/join (P-SYNTHESIZABLE: out of scope while the scored frontend is Yosys read_verilog -sv). Host access (reading files, system calls, DPI) is disallowed by its own policy (decided 2026-10-31).
• Anything that lets a submission change what the checker trusts (P-TRUSTED-BASE): sorry, user axioms, extern / implemented_by, a player-supplied envelope.
• Anything in the SystemVerilog text that reaches the machine the checker runs on (P-NO-HOST-ACCESS; the Lean file is not covered, see the limits): $readmemh / $readmemb / $writemem*, $fopen and the file I/O family, $system, $test$plusargs / $value$plusargs, dump writers ($dumpfile, ...), DPI imports and exports, and escaped $-names that Yosys reads as system tasks.

How a refusal becomes allowed

• Every refusal above has a state. refused-now means no change is planned. later names the prerequisite that has to exist first; when it exists, the refusal is lifted by a pull request.
• How to propose it. Open a pull request against lean-surfaces that adds the feature to ls-sv (extractor, LeanModels/Sv), with differential cases against independent oracles (Xcelium pinned data, Icarus, Verilator, Yosys): a disagreement is fixed or declared, never ignored. The maintainers approve every such PR.
• If the construct brings an x source (a function local read before assignment, a latch that is never loaded, always @*), a rule in score/fourstate.py must land first or in the same PR; the post-synthesis check is the backstop, not the plan.
• For the checker's own rules (the source gate, the banlist, the statement), changing a refusal changes what every earlier submission means: the PR must say so, and leaderboard entries record the lean-surfaces revision they were checked against.
• Update the register. Add or edit the row in docs/sv-refusals.json, run python3 tools/gen_sv_refusals.py --write, and --check must pass.

Known limits (not refusals)

• The post-synthesis check is sampling (fixed corners, task corners, harvested comparison constants, seeded random): a difference confined to a region no comparison constant selects can pass (oob_rare.sv, zpair_add_rare.sv pass it alone; the static rules are the only line there).
• There is no sandbox: import Lean is allowed, so a Solution.lean can run #eval with checker privileges. The integrity snapshot is a tripwire, not a defence. Run untrusted submissions in a throwaway container. Measured (2026-10-31): a reference Solution.lean with an added #eval IO.FS.readFile "/etc/hosts" and an IO.FS.writeFile was ACCEPTED and did both, so the host-access refusals (P-NO-HOST-ACCESS) are a rule about the SystemVerilog text only.
• Open: should the Lean file be gated against host access too (#eval, IO, run_cmd, elab, initialize, unsafe; import Lean is allowed)? Nothing gates it today.
• The parameter's declared type is not pinned by the statement; the multi-point cross-check at the scoring point keeps the scored design one ls-sv and slang agree on, elsewhere the statement is about ls-sv's reading.
• The banlist front check is heuristic (a variable copied from a loop counter counts as run-time); the Yosys backstop covers the scored points only.
• The fourstate stage checks the SCORING POINT only (not the probe points) and filters tri-state warnings out of Yosys check. Its run-time index rule reasons from index TYPES: a[i-1] with a 2-bit i is a 32-bit index and is refused on any declared range (over-refusal), as is any procedural loop counter used as an index.
• A gate hole not yet measured: x/z digits are exempt anywhere inside a casez/casex item EXPRESSION, not only as the item's own literal (casez (a[1:0]) (a[0] == 1'bz) ? 2'b00 : 2'b01: ... passes the gate). Whether ls-sv and Yosys then differ was not measured; do not rely on it.
• A plain syntax error is reported by the gate as preprocessor-skipped text before the extractor or Yosys see it; always @(*) passes the gate (the (*) is exempt) and is refused later by the language tier.
• ARITH_PRIMITIVES ($alu $macc $macc_v2 $lcu $fa) in the banlist backstop are dead entries: the backstop reads without -icells, so instantiating one fails earlier with yosys failed.
• --no-gate in score.py and postsynth.py is a research flag: the result says gated: false and is not a svGolf score. Missing Verilator, make, a C++ compiler, Yosys or svgolf-eval is an infrastructure error (exit 2), never a rejection.
• Open policy question: comparisons are not banned in add / mul; a carry written as a comparison is Yosys's own alu logic and scores lower depth than the proved ripple reference.
• Open: must challenge proofs be parametric (for all N)? The README treats it as decided; svgolf/PLAN.md still lists it as a question for the maintainers.
• slang's ANALYSIS-pass errors (multiple-always-assigns, mixed-var-assigns, multiple-cont-assigns, "cannot assign to input port", "'always' procedure does not advance time") are read since 2026-11-01 by the banlist front check and the fourstate stage (score/slangdriver.py, the Driver's own severities, per parameter point) and by the extractor. Still unread: the elaboration warnings the driver promotes to errors (IndexOOB, RangeOOB, ...: fourstate's rule (c) refuses the out-of-range ones as x sources); a task with an EMPTY banlist skips the banlist front check, so fourstate is the only stage that reads them there; a module the design does not instantiate (docs/sv-refusals.json, holes).

Where to read more

Paths in the proglib repository:

• svgolf/README.md: rules, checker stages, scoring, task.json fields, checker v0 limits
• svgolf/PLAN.md: decisions with dates, the task ladder, the day-by-day plan
• svgolf/SvGolf/Task.lean: the trusted statement and why each conjunct exists
• svgolf/tests/expected.json: every attack and negative design, its stage and why
• svgolf/tests/_example/attacks/README.md: the attacks, one paragraph each
• svgolf/design/nondeterminism/NOTE.md: design note: how LRM-legal nondeterminism would be modelled, and what the golfer would prove
• docs/sv-refusals.md: (lean-surfaces) the register of the language tier's refusals
• docs/sv-oracle-disagreements.md: (lean-surfaces) where the oracles split and what is refused or declared
• docs/sv-xcelium-audit.md: (lean-surfaces) the Xcelium reference audit behind the round-6 refusals
• docs/sv-envelope-schema.md: (lean-surfaces) the envelope contract and the Unsupported vocabulary
• docs/sv-tools-split-audit.md: (lean-surfaces) the tools-split audit behind the 2026-10-31 category changes