diff --git a/spec/lt.typ b/spec/lt.typ index cb4f9c141..ea36eb4dc 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -22,7 +22,7 @@ The `LT` chip is comprised of #nr_variables variables that are expressed using # #render_chip_column_table(chip, config) == Assumptions -We assume the inputs `lhs`, `rhs` and `signed` are appropriately range checked. +We assume the inputs `lhs`, `rhs` and `signed` are partially range checked. #render_chip_assumptions(chip, config) == Constraints @@ -71,7 +71,8 @@ Therefore, we can use $Q$ to constrain `lt` when `signed = 1`. #render_constraint_table(chip, config, groups: "defs") -And then we constrain the subtraction. +And then we constrain the subtraction, +taking care of the remaining range checking not yet covered by the assumptions or the `MSB16` lookup. #render_constraint_table(chip, config, groups: "sub") diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index d8609e935..c151b6eff 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -567,7 +567,7 @@ ref = "cpu:c:sub" [[constraints.alu]] kind = "interaction" tag = "LT" -input = [["cast", "arg1", "DWordHHW"], ["cast", "arg2", "DWordHHW"], "signed"] +input = [["cast", "arg1", "DWordWL"], ["cast", "arg2", "DWordWL"], "signed"] output = ["idx", "res", 0] multiplicity = ["+", "SLT", "BLT"] diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 3836cdd13..10497b637 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -78,13 +78,11 @@ pad = 0 [[assumptions]] -desc = "`IS_HALFWORD[lhs[i]]` and `IS_WORD[lhs[0]]`" -iter = ["i", 1, 2] +desc = "`IS_WORD[lhs[0]]`" ref = "lt:a:range_lhs" [[assumptions]] -desc = "`IS_HALFWORD[rhs[i]]` and `IS_WORD[rhs[0]]`" -iter = ["i", 1, 2] +desc = "`IS_WORD[rhs[0]]`" ref = "lt:a:range_rhs" [[assumptions]] @@ -130,6 +128,20 @@ tag = "IS_BIT" input = [["idx", "carry", "i"]] iter = ["i", 0, 1] +[[constraints.defs]] +kind = "interaction" +tag = "IS_HALFWORD" +input = [["idx", "lhs", 1]] +multiplicity = "μ" +ref = "lt:c:range_lhs" + +[[constraints.defs]] +kind = "interaction" +tag = "IS_HALFWORD" +input = [["idx", "rhs", 1]] +multiplicity = "μ" +ref = "lt:c:range_rhs" + [[constraints.sub]] kind = "interaction" tag = "IS_HALFWORD" @@ -146,6 +158,6 @@ desc = "Each row contributes the following to the LogUp sum" [[constraints.output]] kind = "interaction" tag = "LT" -input = ["lhs", "rhs", "signed"] +input = [["cast", "lhs", "DWordWL"], ["cast", "rhs", "DWordWL"], "signed"] output = "lt" multiplicity = "-μ" diff --git a/spec/src/memw.toml b/spec/src/memw.toml index 9aa9cd592..f7276a9cd 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -159,21 +159,21 @@ iters = [ [[constraints.consistency]] kind = "interaction" tag = "LT" -input = [["idx", "old_timestamp", 0], "timestamp"] +input = [["idx", "old_timestamp", 0], "timestamp", 0] output = 1 multiplicity = "μ_sum" [[constraints.consistency]] kind = "interaction" tag = "LT" -input = [["idx", "old_timestamp", 1], "timestamp"] +input = [["idx", "old_timestamp", 1], "timestamp", 0] output = 1 multiplicity = "w2" [[constraints.consistency]] kind = "interaction" tag = "LT" -input = [["idx", "old_timestamp", "i"], "timestamp"] +input = [["idx", "old_timestamp", "i"], "timestamp", 0] output = 1 iter = ["i", 2, 3] multiplicity = "w4" @@ -181,7 +181,7 @@ multiplicity = "w4" [[constraints.consistency]] kind = "interaction" tag = "LT" -input = [["idx", "old_timestamp", "i"], "timestamp"] +input = [["idx", "old_timestamp", "i"], "timestamp", 0] output = 1 iter = ["i", 4, 7] multiplicity = "write8" @@ -194,21 +194,21 @@ prefix = "R" [[constraints.overflow]] kind = "interaction" tag = "LT" -input = ["base_address", ["cast", ["idx", "address_add", 0], "DWordWL"]] +input = ["base_address", ["cast", ["idx", "address_add", 0], "DWordWL"], 0] output = 1 multiplicity = "write2" [[constraints.overflow]] kind = "interaction" tag = "LT" -input = ["base_address", ["cast", ["idx", "address_add", 2], "DWordWL"]] +input = ["base_address", ["cast", ["idx", "address_add", 2], "DWordWL"], 0] output = 1 multiplicity = "write4" [[constraints.overflow]] kind = "interaction" tag = "LT" -input = ["base_address", ["cast", ["idx", "address_add", 6], "DWordWL"]] +input = ["base_address", ["cast", ["idx", "address_add", 6], "DWordWL"], 0] output = 1 multiplicity = "write8"