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..d93449228 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` = #`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" -[[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` = #`d`$" +iter = ["i", 0, 1] +poly = ["*", ["not", "sign_d"], ["-", ["idx", "abs_d", "i"], ["idx", ["cast", "d", "DWordWL"], "i"]]] ref = "dvrm:c:abs_d_if_nonnegative" [[constraint_groups]]