This task
This text quotes sky130 numbers and compares the designs on sky130, the default library; the score, the boards and the charts of this page are on ASAP7, where the order of the designs can differ.
Multiply two polynomials over GF(2): bit k of the 2N-1-bit result is the XOR, over all i + j = k,
of a[i] AND b[j]. This is multiplication with the carries removed, the operation behind GHASH, CRCs and
binary-field cryptography. The proof covers every N ≥ 1; the score is taken at N = 16.
Run-time + - * / % ** and the ordering comparisons < <= > >= are banned. The proved N × N AND/XOR array has 3429.5 µm² and a 1.11 ns
critical path on sky130 (772.267 GE, depth 6). It is the first task whose best known designs
are recursive: an unproved Karatsuba circuit is about a fifth smaller, 2756.4 µm², but slower,
1.81 ns (621.959 GE, depth 8).
Interface #
Write a module with exactly this header: port names, directions, widths and order matter, and so do the module's name and its parameters.
module clmul_n #(parameter int N = 16) (
input logic [N-1:0] a, b,
output logic [2*N-2:0] p
);| port | direction | width (bits) |
|---|---|---|
a | input | N |
b | input | N |
p | output | 2*N-1 |
The trusted statement #
A proof must establish the task's trusted statement, the constant SvGolf.Tasks.Clmul.Statement of Spec.lean (module tasks.clmul.Spec). Below it is split into the properties a circuit must have, one card each: what the property guarantees in plain words, and its exact Lean text. Every proved reference has all of them. The last tab, what does not count, lists the designs the checker rejects.
Properties
A design meets the trusted statement exactly when, for every width N with 1 ≤ N < 2^30, it has all of the properties below. Lean checks that, together, they say exactly what the statement says, nothing less and nothing more (the theorem statement_iff_properties).
PARAMS_IN_RANGE is the range the statement covers, not a property: every other card must hold at each value in it.
PARAMS_IN_RANGErangeThe widths the statement covers: every N with 1 ≤ N < 2^30 (so that the widths 2N-1 and 2N-2, int expressions of the module, stay below 2^31, the values an int holds).
The statement covers every width N with 1 ≤ N < 2^30 at once (the module's port widths are int expressions of N, such as 2N, and an int holds no value of 2^31 or more): one proof works for all of them, not just for the width the design is scored at (N = 16). Every property below must hold at each width.
/-- The widths the statement covers: every `N` with `1 ≤ N < 2^30` (so that the widths `2N-1` and
`2N-2`, `int` expressions of the module, stay below `2^31`, the values an `int` holds). -/
def ParamsInRange (N : Nat) : Prop :=
1 ≤ N ∧ N < 2 ^ 30INTERFACEExactly these ports, in this order, with these widths.
The module has exactly the input ports a and b (N bits each) and exactly the output port p (2N − 1 bits), with these widths, in this order. Nothing is missing and nothing is extra: an extra input could serve as a hidden mode pin, and the checker and the scoring tools drive and read the design by these names and widths.
/-- Exactly these ports, in this order, with these widths. -/
def Interface (N : Nat) (d : Design2) : Prop :=
inputPorts d = [("a", N), ("b", N)] ∧ outputPorts d = [("p", 2 * N - 1)]UNCLOCKEDNo process runs at a clock edge (no always_ff, no always @(posedge …)).
No process of the design runs at a clock edge: no always_ff, no always @(posedge …), no asynchronous-reset block; only continuous assignments and always_comb blocks. The task is combinational, so it never needs one. The rule closes a gap between Lean's model of SystemVerilog, which the proof is about, and real tools: the model runs every clocked block once per cycle whatever its clock does, so a design that registers correct outputs on a clock nothing drives would look right there, while a simulator sees a clock that never ticks and synthesis removes the registers.
/-- No process runs at a clock edge (no `always_ff`, no `always @(posedge …)`). -/
def Unclocked (d : Design2) : Prop :=
∀ p ∈ d.processes.toList, p.isEdgePhase = falseLOOP_FREENo combinational loop: the design lowers to continuous assigns (Design2.lowerComb) that are ranked (Acyclic): each reads only what lower-ranked ones write.
The design has no combinational loop: written as continuous assignments (each always_comb block becomes one), its processes can be ranked so that each reads only what lower-ranked ones write. A latch (an always_comb block that keeps a value on some path) is refused with it. Lean's model starts every signal at x and settles, so it would read a loop at one state, while a circuit powers up in any 0/1 state the loop can hold and keeps it; the rule removes that question instead of answering it. The ranking is of processes, not bits, so a process that reads a part of a signal it writes itself is refused too, even when no bit depends on itself: write such bits as separate assignments.
/-- No combinational loop: the design lowers to continuous assigns (`Design2.lowerComb`) that are
ranked (`Acyclic`): each reads only what lower-ranked ones write. -/
def LoopFree (d : Design2) : Prop :=
∃ d', d.lowerComb = some d' ∧ Acyclic d'TERMINATESUnder every schedule and every stimulus, the run completes.
Whatever order the simulator picks for processes that are ready at the same moment (the schedule), and whatever values the inputs take, simulating the design completes: every cycle settles. A combinational loop that oscillates fails this, and so does a design the tools could not read. It is also what gives the next property its teeth: that one is about completed runs, and a design with no completed run would satisfy it without computing anything.
/-- Under every schedule and every stimulus, the run completes. -/
def Terminates (d : Design2) : Prop :=
∀ (σ : ScheduleOracle) (stim : List SvState), ∃ tr, Runs2 d σ stim trCOMPUTES_CARRYLESS_PRODUCTIn every completed run, every cycle whose stimulus drives a and b with known values ends with p holding the coefficients of their product as polynomials over GF(2).
In every cycle in which the inputs a and b are driven with known 0/1 values, the output p settles to their carry-less product: reading bit i of a vector as the coefficient of x^i, p is the product of the two polynomials over GF(2), so bit k of p is the XOR of a[i] AND b[j] over all i + j = k. It is a × b with every carry dropped, and its 2N − 1 bits hold the whole product (no reduction modulo a polynomial). The outputs must be fully known 0/1 values in every cycle of every run, whatever the earlier cycles were, so they cannot depend on history.
/-- In every completed run, every cycle whose stimulus drives `a` and `b` with known values ends
with `p` holding the coefficients of their product as polynomials over GF(2). -/
def ComputesCarrylessProduct (N : Nat) (d : Design2) : Prop :=
d ⊨₂ spec2 fun stim tr =>
∀ (c : Nat) (inputs st : SvState), stim[c]? = some inputs → tr[c]? = some st →
∀ (a b : BitVec N),
HoldAll inputs [("a", N), ("b", N)] (a, b, ()) →
HoldAll st [("p", 2 * N - 1)] (ofBits (2 * N - 1) (coeff N a b), ())Definitions
The names the properties use, each with its Lean text. Trusted text is what a proof is about; a helper of Properties.lean is not trusted: Lean checks it as part of statement_iff_properties.
This task's trusted text
coeffSpec.leancoeff N a b k: coefficient k of the product polynomial, the XOR over all pairs of bit positions i, j below N with i + j = k of a[i] AND b[j].
/-- Coefficient `k` of the product polynomial: the XOR, over all pairs `(i, j)` of positions below `N`
with `i + j = k`, of `a_i AND b_j`. -/
def coeff (N : Nat) (a b : BitVec N) (k : Nat) : Bool :=
(List.range N).foldl (fun acc i =>
(List.range N).foldl (fun acc j => acc ^^ (decide (i + j = k) && a.getLsbD i && b.getLsbD j)) acc) falseofBitsSpec.leanofBits n f: the n-bit vector whose bit k is f k.
/-- The `n`-bit vector whose bit `k` (counted from the least significant end) is `f k`. -/
def ofBits : (n : Nat) → (Nat → Bool) → BitVec n
| 0, _ => 0#0
| n + 1, f => ofBits n (fun k => f (k + 1)) ++ BitVec.ofBool (f 0)StatementSpec.leanThe trusted challenge statement that these properties restate, part by part.
/-- **The challenge statement.** A submission proves `SvGolf.Tasks.Clmul.Statement Submission.design.sem`. -/
abbrev Statement : (Nat → LeanModels.Sv.Design2) → Prop := task.StatementtaskSpec.leanThe task as data: the parameter range, the ports at each parameter value, and the function the outputs must compute.
/-- The task: inputs `a b : BitVec N`, output `p = a (x) b` on `2N-1` bits, for `1 ≤ N < 2^30`. -/
def task : CombTask where
inRange N := 1 ≤ N ∧ N < 2 ^ 30
inputs N := [("a", N), ("b", N)]
outputs N := [("p", 2 * N - 1)]
fn N := fun (a, b, ()) => (ofBits (2 * N - 1) (coeff N a b), ())The shared trusted base
CombTask.SatisfiedAtTask.leanThe trusted form of a combinational statement at one parameter value: the interface, then no clock and termination, then the function.
/-- The statement at one parameter value: interface; no clocked process, no
combinational loop and termination; function. Conjunct 2 is the triple
`Unclocked d ∧ LoopFree d ∧ Terminates2 d`. -/
def SatisfiedAt (N : Nat) (d : Design2) : Prop :=
t.Interface N d ∧ (Unclocked d ∧ LoopFree d ∧ Terminates2 d) ∧ t.Computes N dinputPortsTask.leanThe design's input ports, each with its declared width, in declaration order.
/-- The input ports of `d` with their declared widths, in declaration order.
`instantiate2` lists the ports first, in port-list order. A declaration is
an input port iff its `isInput` flag is set. -/
def inputPorts (d : Design2) : List Sig :=
d.decls.toList.filterMap fun dc => if dc.isInput then some (dc.name, dc.width) else noneoutputPortsTask.leanThe design's output ports, each with its declared width, in declaration order.
/-- The output ports of `d` with their declared widths, in declaration order.
A declaration is an output port iff its `isOutput` flag is set. -/
def outputPorts (d : Design2) : List Sig :=
d.decls.toList.filterMap fun dc => if dc.isOutput then some (dc.name, dc.width) else noneHoldAllTask.leanHoldAll st ports values: in the state st, every listed port holds its value as a known bit vector (no x, no z) of exactly the port's width.
/-- `HoldAll st sigs v`: in state `st`, every port `(n, w)` of `sigs` is bound
to the fully known `w`-bit vector that `v` assigns it. -/
def HoldAll (st : SvState) : (sigs : List Sig) → Vals (sigs.map Prod.snd) → Prop
| [], _ => True
| (n, _) :: sigs, v => SvState.lookup st n = some (LVec.ofBitVec v.1) ∧ HoldAll st sigs v.2⊨₂Spec2.leand ⊨₂ P: in every completed run of the design d, under every schedule and every stimulus, the stimulus and the trace satisfy P.
/-- `d ⊨₂ P` — for **every** legal schedule, every stimulus, and every
completed run (`Runs2`), the trace satisfies `P`. Introduce from a raw
∀-fuel fact with `Models2.of_run`; eliminate against a concrete run with
`Models2.run` / `Models2.runs`. Says nothing about whether runs complete —
pair it with `Terminates2`. -/
def Models2 (d : Design2) (P : TraceProp2) : Prop :=
∀ (σ : ScheduleOracle) (stim tr : List SvState), Runs2 d σ stim tr → P d stim tr
@[inherit_doc] scoped infix:50 " ⊨₂ " => Models2spec2Spec2.leanTurns a property of a stimulus (one input entry per cycle) and a trace (one snapshot of every signal per cycle) into the form ⊨₂ takes.
/-- Lift a design-agnostic stimulus/trace predicate into `⊨₂`
(`d ⊨₂ spec2 fun stim tr => …`). -/
def spec2 (P : List SvState → List SvState → Prop) : TraceProp2 := fun _ stim tr => P stim trRuns2Spec2.leanRuns2 d σ stim tr: simulating d under the schedule σ on the stimulus stim completes, with the trace tr.
/-- The fuel-abstracted Design2 run judgment: *some* fuel completes the run
of `d` under schedule `σ` and stimulus `stim` with trace `tr`. The only place
fuel appears in a Design2 spec. -/
def Runs2 (d : Design2) (σ : ScheduleOracle) (stim tr : List SvState) : Prop :=
∃ fuel, run2 d σ fuel stim = .ok trScheduleOracleSemantics.leanA legal schedule: the order in which the simulator runs the processes that are ready at the same moment. The statement quantifies over all of them.
/-- A legal schedule: at invocation `k`, orders the ready process list.
`choose_perm` is the legality proof — every invocation is a permutation of
the ready list — so `∀ σ : ScheduleOracle` ranges over exactly the legal
schedules. See the module docstring for the invocation-counter protocol. -/
structure ScheduleOracle where
/-- Invocation counter and ready process indices in, execution order out. -/
choose : Nat → List Nat → List Nat
/-- Every invocation yields a permutation of the ready list. -/
choose_perm : ∀ (k : Nat) (ready : List Nat), (choose k ready).Perm readyProcess2.isEdgePhaseSem2.leanTrue for the processes that run at the clock edge: always_ff, always @(posedge …) and asynchronous-reset blocks.
/-- Edge-phase processes: every posedge-clocked block, INCLUDING the
async-reset ones (the posedge fires with reset asserted too — the body's
reset branch is what holds the state, pin3 CYCLE 4). -/
def Process2.isEdgePhase : Process2 → Bool
| .alwaysFF _ _ | .alwaysPlain _ _ | .alwaysFFR _ _ _ _ => true
| _ => falseWhat does not count
Designs that try to score without meeting the statement (negatives), or that exploit a place where the proof's reading and the scored netlist could differ (attacks). The checker stops at the first stage that refuses; each design is listed with that stage.
- Refused before any proof is tried: 4 designs (by stage:
extract1,banlist3) - Rejected at the proof: 5 designs (by stage:
solution5)
Refused before any proof is tried
The checker's static stages read the text itself and refuse it: an operator the task bans, a construct that two tools read differently, an unknown (x or z) value that could arise, or a program the language forbids.
wide_out.sv(negative, stopped atextract): The outputpis 2N bits wide instead of 2N - 1.the design, with its comments left out
module clmul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-1:0] p ); logic [N-1:0][N-1:0] r; assign p[2*N-1] = 1'b0; genvar i, j, m; generate for (j = 0; j < N; j++) begin : g_row0 assign r[0][j] = a[0] & b[j]; end for (i = 1; i < N; i++) begin : g_row for (j = 0; j < N-1; j++) begin : g_bit assign r[i][j] = r[i-1][j+1] ^ (a[i] & b[j]); end assign r[i][N-1] = a[i] & b[N-1]; end for (i = 0; i < N; i++) begin : g_lo assign p[i] = r[i][0]; end for (m = 0; m < N-1; m++) begin : g_hi assign p[N+m] = r[N-1][m+1]; end endgenerate endmodulediv_zero_x.sv(attack, stopped atbanlist): The right product, plus a run-time division whose divisor is zero on one input pair in 2^32: the proof sees an unknown value there and the synthesized circuit a different, defined one. Run-time/ % **are banned in every task.the design, with its comments left out
module clmul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-2:0] p ); logic [N-1:0][N-1:0] r; logic [2*N-2:0] pp; genvar i, j, m; generate for (j = 0; j < N; j++) begin : g_row0 assign r[0][j] = a[0] & b[j]; end for (i = 1; i < N; i++) begin : g_row for (j = 0; j < N-1; j++) begin : g_bit assign r[i][j] = r[i-1][j+1] ^ (a[i] & b[j]); end assign r[i][N-1] = a[i] & b[N-1]; end for (i = 0; i < N; i++) begin : g_lo assign pp[i] = r[i][0]; end for (m = 0; m < N-1; m++) begin : g_hi assign pp[N+m] = r[N-1][m+1]; end endgenerate logic [2*N-1:0] wa; logic [3*N-1:0] wb; logic [N-1:0] pa, pb; logic rare; logic q; assign wa = {N{2'b10}}; assign wb = {N{3'b011}}; assign pa = wa[N-1:0]; assign pb = wb[N-1:0]; assign rare = (&(~(a ^ pa))) & (&(~(b ^ pb))); assign q = 1'b1 / ~rare; always_comb if (q) p = pp ^ {{(2*N-2){1'b0}}, rare}; else p = pp; endmodulekronecker_mul.sv(negative, stopped atbanlist): The right function through the integer multiplier on bit-spread operands, using the banned run-time*.the design, with its comments left out
module clmul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-2:0] p ); localparam int K = 8; logic [K*N-1:0] sa, sb; logic [2*K*N-1:0] sp; genvar i, k; generate for (i = 0; i < K*N; i++) begin : g_spread if (i % K == 0) begin : g_bit assign sa[i] = a[i/K]; assign sb[i] = b[i/K]; end else begin : g_zero assign sa[i] = 1'b0; assign sb[i] = 1'b0; end end endgenerate assign sp = sa * sb; generate for (k = 0; k < 2*N-1; k++) begin : g_parity assign p[k] = sp[K*k]; end endgenerate endmoduleplus_xor.sv(negative, stopped atbanlist): The right function, with each row's XOR written as a one-bit run-time+, which is banned.the design, with its comments left out
module clmul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-2:0] p ); logic [N-1:0][N-1:0] r; genvar i, j, m; generate for (j = 0; j < N; j++) begin : g_row0 assign r[0][j] = a[0] & b[j]; end for (i = 1; i < N; i++) begin : g_row for (j = 0; j < N-1; j++) begin : g_bit assign r[i][j] = r[i-1][j+1] + (a[i] & b[j]); end assign r[i][N-1] = a[i] & b[N-1]; end for (i = 0; i < N; i++) begin : g_lo assign p[i] = r[i][0]; end for (m = 0; m < N-1; m++) begin : g_hi assign p[N+m] = r[N-1][m+1]; end endgenerate endmodule
Rejected at the proof
These pass every static check. The proof that comes with each one does not compile, or does not prove the statement: a design that is wrong somewhere in the task's range (or has other ports) has no proof at all, and a proof that leaves a goal unproved is never accepted.
drop_top.sv(negative, stopped atsolution): Off by one: every row after the first drops its top term.the design, with its comments left out
module clmul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-2:0] p ); logic [N-1:0][N-1:0] r; genvar i, j, m; generate for (j = 0; j < N; j++) begin : g_row0 assign r[0][j] = a[0] & b[j]; end for (i = 1; i < N; i++) begin : g_row for (j = 0; j < N-1; j++) begin : g_bit assign r[i][j] = r[i-1][j+1] ^ (a[i] & b[j]); end assign r[i][N-1] = 1'b0; end for (i = 0; i < N; i++) begin : g_lo assign p[i] = r[i][0]; end for (m = 0; m < N-1; m++) begin : g_hi assign p[N+m] = r[N-1][m+1]; end endgenerate endmoduleonly_n16.sv(negative, stopped atsolution): Correct only at the scoring width N = 16, zero elsewhere.the design, with its comments left out
module clmul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-2:0] p ); logic [N-1:0][N-1:0] r; genvar i, j, m; generate if (N == 16) begin : g_scored for (j = 0; j < N; j++) begin : g_row0 assign r[0][j] = a[0] & b[j]; end for (i = 1; i < N; i++) begin : g_row for (j = 0; j < N-1; j++) begin : g_bit assign r[i][j] = r[i-1][j+1] ^ (a[i] & b[j]); end assign r[i][N-1] = a[i] & b[N-1]; end for (i = 0; i < N; i++) begin : g_lo assign p[i] = r[i][0]; end for (m = 0; m < N-1; m++) begin : g_hi assign p[N+m] = r[N-1][m+1]; end end else begin : g_other assign p = '0; end endgenerate endmoduleor_accumulate.sv(negative, stopped atsolution): Accumulates the rows with OR instead of XOR.the design, with its comments left out
module clmul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-2:0] p ); logic [N-1:0][N-1:0] r; genvar i, j, m; generate for (j = 0; j < N; j++) begin : g_row0 assign r[0][j] = a[0] & b[j]; end for (i = 1; i < N; i++) begin : g_row for (j = 0; j < N-1; j++) begin : g_bit assign r[i][j] = r[i-1][j+1] | (a[i] & b[j]); end assign r[i][N-1] = a[i] & b[N-1]; end for (i = 0; i < N; i++) begin : g_lo assign p[i] = r[i][0]; end for (m = 0; m < N-1; m++) begin : g_hi assign p[N+m] = r[N-1][m+1]; end endgenerate endmodulereversed_p.sv(negative, stopped atsolution): Delivers the result bits in reverse order (coefficient k atp[2N-2-k]).the design, with its comments left out
module clmul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-2:0] p ); logic [N-1:0][N-1:0] r; genvar i, j, m; generate for (j = 0; j < N; j++) begin : g_row0 assign r[0][j] = a[0] & b[j]; end for (i = 1; i < N; i++) begin : g_row for (j = 0; j < N-1; j++) begin : g_bit assign r[i][j] = r[i-1][j+1] ^ (a[i] & b[j]); end assign r[i][N-1] = a[i] & b[N-1]; end for (i = 0; i < N; i++) begin : g_lo assign p[2*N-2-i] = r[i][0]; end for (m = 0; m < N-1; m++) begin : g_hi assign p[N-2-m] = r[N-1][m+1]; end endgenerate endmoduletop_shift.sv(negative, stopped atsolution): The top N - 1 output bits are read from the wrong position.the design, with its comments left out
module clmul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-2:0] p ); logic [N-1:0][N-1:0] r; genvar i, j, m; generate for (j = 0; j < N; j++) begin : g_row0 assign r[0][j] = a[0] & b[j]; end for (i = 1; i < N; i++) begin : g_row for (j = 0; j < N-1; j++) begin : g_bit assign r[i][j] = r[i-1][j+1] ^ (a[i] & b[j]); end assign r[i][N-1] = a[i] & b[N-1]; end for (i = 0; i < N; i++) begin : g_lo assign p[i] = r[i][0]; end for (m = 0; m < N-1; m++) begin : g_hi assign p[N+m] = r[N-1][m]; end endgenerate endmodule
Spec.lean, verbatim (98 lines)
import SvGolf.Task
/-!
# Task `clmul`: N-bit carry-less multiplier, the product of polynomials over GF(2) (TRUSTED)
`mul` with the carries removed: AND for the partial products, XOR for the sums, no adder. Module (port
order as written; `N` is the module's only parameter):
```systemverilog
module clmul_n #(parameter int N = 16) (
input logic [N-1:0] a, b,
output logic [2*N-2:0] p
);
```
Statement: for every `N` with `1 ≤ N < 2^30` (so that the widths `2N-1` and `2N-2`, `int` expressions
of the module, stay below `2^31`, the values an `int` holds), the design has
exactly the ports `a`, `b` (inputs, `N` bits) and `p` (output, `2N-1` bits), no process is clocked, there
is no combinational loop, every run terminates, and in every cycle whose stimulus
drives `a` and `b` with known values the snapshot's `p` is the coefficient vector of the product of the
two polynomials over GF(2) that `a` and `b` encode (bit `i` of a vector is the coefficient of `x^i`):
p_k = XOR over i + j = k, 0 ≤ i, j < N, of (a_i AND b_j), for 0 ≤ k ≤ 2N-2.
The product of two polynomials of degree below `N` has degree at most `2N-2`, so `p` loses nothing (and
there is no constant-zero top bit). The same bits are the unsigned product `a * b` with every carry
dropped (`PCLMULQDQ`, the GHASH core, the polynomial multiplication of every binary-field and CRC/BCH
construction); this task is the UNREDUCED product, no modulus. The bit orientation is the usual
(little-endian) one, the opposite of GHASH's reflected convention.
The function is DEFINED by the double sum above, as `coeff` below, without natural-number subtraction or
any reliance on out-of-range bit reads. Sources used to cross-check (none trusted): `oracle.py`
(shift-and-XOR in Python), an implementation by Kronecker substitution (spread the bits `k = bit_length(N)
+ 1` apart, multiply as integers, read the parity of each group; `tests/checker/test_advisories.py`),
FIPS 197 Section 4.2's two products (`examples` below), and exhaustive agreement with the Lean spec
(`tests/clmul/validate/validate.py`).
-/
namespace SvGolf.Tasks.Clmul
open SvGolf
/-- The `n`-bit vector whose bit `k` (counted from the least significant end) is `f k`. -/
def ofBits : (n : Nat) → (Nat → Bool) → BitVec n
| 0, _ => 0#0
| n + 1, f => ofBits n (fun k => f (k + 1)) ++ BitVec.ofBool (f 0)
/-- Coefficient `k` of the product polynomial: the XOR, over all pairs `(i, j)` of positions below `N`
with `i + j = k`, of `a_i AND b_j`. -/
def coeff (N : Nat) (a b : BitVec N) (k : Nat) : Bool :=
(List.range N).foldl (fun acc i =>
(List.range N).foldl (fun acc j => acc ^^ (decide (i + j = k) && a.getLsbD i && b.getLsbD j)) acc) false
/-- The task: inputs `a b : BitVec N`, output `p = a (x) b` on `2N-1` bits, for `1 ≤ N < 2^30`. -/
def task : CombTask where
inRange N := 1 ≤ N ∧ N < 2 ^ 30
inputs N := [("a", N), ("b", N)]
outputs N := [("p", 2 * N - 1)]
fn N := fun (a, b, ()) => (ofBits (2 * N - 1) (coeff N a b), ())
/-- **The challenge statement.** A submission proves `SvGolf.Tasks.Clmul.Statement Submission.design.sem`. -/
abbrev Statement : (Nat → LeanModels.Sv.Design2) → Prop := task.Statement
/-! ## Sanity checks (closed; `decide +kernel` is kernel evaluation, no axiom) -/
/-- The scoring point `N = 16` (and the reported points 8 and 32) are in range. -/
example : task.inRange 16 ∧ task.inRange 8 ∧ task.inRange 32 := by simp [task]
/-- The range ends below `2^30`: the output's bound `2*N-2` (the port's `[2*N-2:0]`, evaluated as an
`int`) and the product `2*N` it is computed from stay below `2^31`, the values an `int` holds. -/
example : task.inRange (2 ^ 30 - 1) ∧ ¬ task.inRange (2 ^ 30) := by simp [task]
/-- At the top of the range `2*N` is still an `int`. -/
example : 2 * (2 ^ 30 - 1) < 2 ^ 31 := by decide
/-- The input names are distinct (the non-vacuity theorem `CombTask.SatisfiedAt.exists_run` needs it),
at every `N`. -/
example (N : Nat) : ((task.inputs N).map Prod.fst).Nodup := by simp [task]
/-- `(x + 1)^2 = x^2 + 1` over GF(2), at `N = 2`. -/
example : (task.fn 2 (0b11#2, 0b11#2, ())).1 = 0b101#3 := by decide
/-- `(x^2 + 1)(x + 1) = x^3 + x^2 + x + 1`, at `N = 3` (five output bits). -/
example : (task.fn 3 (0b101#3, 0b011#3, ())).1 = 0b01111#5 := by decide
/-- `N = 1` is the AND of two bits, on ONE output bit. -/
example : (task.fn 1 (1#1, 1#1, ())).1 = 1#1 ∧ (task.fn 1 (1#1, 0#1, ())).1 = 0#1 := by decide
/-- `(1 + x + ... + x^15)^2 = 1 + x^2 + ... + x^30` over GF(2), at `N = 16` (31 output bits). -/
example : (task.fn 16 (0xffff#16, 0xffff#16, ())).1 = 0x55555555#31 := by decide +kernel
/-- FIPS 197 Section 4.2 (2001 edition: `{57} * {83} = {c1}`; 2023 edition, Eq. (4.7): `{57} * {13} = {fe}`):
the unreduced products are `0x2b79` and `0x0589`; reduced modulo `x^8+x^4+x^3+x+1` (`0x11b`) they give
those bytes (`tests/clmul/validate/validate.py` does the reduction). -/
example : (task.fn 8 (0x57#8, 0x83#8, ())).1 = 0x2b79#15 := by decide +kernel
example : (task.fn 8 (0x57#8, 0x13#8, ())).1 = 0x0589#15 := by decide +kernel
end SvGolf.Tasks.Clmul
Its trusted text
The modules specific to this task. Like every task, it also rests on the shared trusted base (the ls-sv semantics of SystemVerilog and svGolf's statement helpers), and a proof may import any module of the ls-sv library. Nothing else is trusted: proof helpers are kernel-checked like any submission.
| module | role | lines | sha256 |
|---|---|---|---|
tasks.clmul.Spec | task statement | 98 | 7f8461a613cd |
How to participate #
- Write a circuit with the task's exact interface.
- Prove in Lean 4 that it meets the trusted statement; Start a new design, below, gives the route, and the proving guide shows how.
- Check and record it (how to submit): the checker accepts the pair or says which stage refused it, as it does for each design under what does not count.
- Beat par: an accepted design whose score (area × time) is below that of the best proved reference. The leaderboard ranks by it.