From abf4dd9f43b909ce961ea809653cb2fe0efaf8b7 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 5 Feb 2026 11:08:21 +0100 Subject: [PATCH 1/2] spec: DVRM: use NEG template for abs_r and abs_d This saves 4 columns. --- spec/dvrm.typ | 1 - spec/src/dvrm.toml | 46 +++++++++++++++------------------------------- 2 files changed, 15 insertions(+), 32 deletions(-) diff --git a/spec/dvrm.typ b/spec/dvrm.typ index e68f4bee8..54e71d771 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -67,7 +67,6 @@ Focusing on the first statement, we observe that this trivially holds when $#`si while R3 deals with the case that $#`signed` = 1$. The second statement is enforced by @dvrm:c:abs_r_lt_abs_d. @dvrm:c:abs_r_if_negative and @dvrm:c:abs_r_if_nonnegative (resp. @dvrm:c:abs_d_if_negative and @dvrm:c:abs_d_if_nonnegative) are included to ensure that `abs_r` (resp. `abs_d`) is the absolute values of `r` (resp. `d`). -@dvrm:c:abs_r_range_check and @dvrm:c:abs_d_range_check are required to uphold assumption @add:a:lhs required by the `SUB` chip. #render_constraint_table(chip, config, groups:("abs_diff", )) diff --git a/spec/src/dvrm.toml b/spec/src/dvrm.toml index ceeabf1e2..b510d4c01 100644 --- a/spec/src/dvrm.toml +++ b/spec/src/dvrm.toml @@ -51,13 +51,13 @@ pad = 0 [[variables.auxiliary]] name = "abs_r" -type = "DWordHL" +type = "DWordWL" desc = "Absolute value of `r`." pad = 0 [[variables.auxiliary]] name = "abs_d" -type = "DWordHL" +type = "DWordWL" desc = "Absolute value of `d`." pad = 0 @@ -215,55 +215,39 @@ name = "abs_diff" [[constraints.abs_diff]] kind = "interaction" tag = "LT" -input = [["cast", "abs_r", "DWordWL"], ["cast", "abs_d", "DWordWL"], 0] +input = ["abs_r", "abs_d", 0] output = ["not", "div_by_zero"] multiplicity = "μ_sum" ref ="dvrm:c:abs_r_lt_abs_d" -[[constraints.abs_diff]] -kind = "interaction" -tag = "IS_HALF" -input = [["idx", "abs_r", "i"]] -iter = ["i", 0, 3] -multiplicity = "sign_r" -ref = "dvrm:c:abs_r_range_check" - [[constraints.abs_diff]] kind = "template" -tag = "SUB" -input = [0, ["cast", "r", "DWordWL"]] -output = ["cast", "abs_r", "DWordWL"] +tag = "NEG" +input = ["r"] +output = "abs_r" cond = "sign_r" ref = "dvrm:c:abs_r_if_negative" [[constraints.abs_diff]] kind = "arith" -constraint = "$not#`sign_r` => #`abs_r[i]`=#`r[i]`$" -iter = ["i", 0, 3] -poly = ["*", ["-", 1, "sign_r"], ["-", ["idx", "abs_r", "i"], ["idx", "r", "i"]]] +constraint = "$not#`sign_r` => #`abs_r[i]`=#`(r as DWordWL)[i]`$" +poly = ["*", ["-", 1, "sign_r"], ["-", ["idx", "abs_r", "i"], ["idx", ["cast", "r", "DWordWL"], "i"]]] +iter = ["i", 0, 1] ref = "dvrm:c:abs_r_if_nonnegative" -[[constraints.abs_diff]] -kind = "interaction" -tag = "IS_HALF" -input = [["idx", "abs_d", "i"]] -iter = ["i", 0, 3] -multiplicity = "sign_d" -ref = "dvrm:c:abs_d_range_check" - [[constraints.abs_diff]] kind = "template" -tag = "SUB" -input = [0, ["cast", "d", "DWordWL"]] -output = ["cast", "abs_d", "DWordWL"] +tag = "NEG" +input = ["d"] +output = "abs_d" cond = "sign_d" ref = "dvrm:c:abs_d_if_negative" [[constraints.abs_diff]] kind = "arith" -constraint = "$not#`sign_d` => #`abs_d[i]`=#`d[i]`$" -iter = ["i", 0, 3] -poly = ["*", ["-", 1, "sign_d"], ["-", ["idx", "abs_d", "i"], ["idx", "d", "i"]]] +constraint = "$not#`sign_d` => #`abs_d[i]`=#`(d as DWordWL)[i]`$" +iter = ["i", 0, 1] +poly = ["*", ["-", 1, "sign_d"], ["-", ["idx", "abs_d", "i"], ["idx", ["cast", "d", "DWordWL"], "i"]]] ref = "dvrm:c:abs_d_if_nonnegative" [[constraint_groups]] From 542f1474540d0d3fc78a4753679471775d24ede1 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Fri, 6 Feb 2026 08:28:48 +0100 Subject: [PATCH 2/2] Apply suggestions from @RobinJadoul Co-authored-by: Robin Jadoul --- spec/src/dvrm.toml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src/dvrm.toml b/spec/src/dvrm.toml index b510d4c01..d93449228 100644 --- a/spec/src/dvrm.toml +++ b/spec/src/dvrm.toml @@ -230,8 +230,8 @@ ref = "dvrm:c:abs_r_if_negative" [[constraints.abs_diff]] kind = "arith" -constraint = "$not#`sign_r` => #`abs_r[i]`=#`(r as DWordWL)[i]`$" -poly = ["*", ["-", 1, "sign_r"], ["-", ["idx", "abs_r", "i"], ["idx", ["cast", "r", "DWordWL"], "i"]]] +constraint = "$not#`sign_r` => #`abs_r` = #`r`$" +poly = ["*", ["not", "sign_r"], ["-", ["idx", "abs_r", "i"], ["idx", ["cast", "r", "DWordWL"], "i"]]] iter = ["i", 0, 1] ref = "dvrm:c:abs_r_if_nonnegative" @@ -245,9 +245,9 @@ ref = "dvrm:c:abs_d_if_negative" [[constraints.abs_diff]] kind = "arith" -constraint = "$not#`sign_d` => #`abs_d[i]`=#`(d as DWordWL)[i]`$" +constraint = "$not#`sign_d` => #`abs_d` = #`d`$" iter = ["i", 0, 1] -poly = ["*", ["-", 1, "sign_d"], ["-", ["idx", "abs_d", "i"], ["idx", ["cast", "d", "DWordWL"], "i"]]] +poly = ["*", ["not", "sign_d"], ["-", ["idx", "abs_d", "i"], ["idx", ["cast", "d", "DWordWL"], "i"]]] ref = "dvrm:c:abs_d_if_nonnegative" [[constraint_groups]]