From 97b1a15cfabf6f67bc0a73976b5f4c77a5c3b773 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 27 Jan 2026 15:38:49 +0100 Subject: [PATCH 1/4] spec: Update LT interaction signature so that it can be used properly for timestamps --- spec/lt.typ | 5 +++-- spec/src/cpu.toml | 2 +- spec/src/lt.toml | 20 +++++++++++++++++--- 3 files changed, 21 insertions(+), 6 deletions(-) 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..422c547b4 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -78,12 +78,12 @@ pad = 0 [[assumptions]] -desc = "`IS_HALFWORD[lhs[i]]` and `IS_WORD[lhs[0]]`" +desc = "`IS_WORD[lhs[0]]`" iter = ["i", 1, 2] ref = "lt:a:range_lhs" [[assumptions]] -desc = "`IS_HALFWORD[rhs[i]]` and `IS_WORD[rhs[0]]`" +desc = "`IS_WORD[rhs[0]]`" iter = ["i", 1, 2] ref = "lt:a:range_rhs" @@ -130,6 +130,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 +160,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 = "-μ" From 22e23c00ee6104552581bd6823d45da2530b841c Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 27 Jan 2026 15:45:40 +0100 Subject: [PATCH 2/4] fix(spec): add missing signed argument to LT from MEMW --- spec/src/memw.toml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) 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" From c85e0580cbe21c466cafe04ca20e86f8ddd3c52d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 27 Jan 2026 16:05:48 +0100 Subject: [PATCH 3/4] Update spec/src/lt.toml Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/src/lt.toml | 1 - 1 file changed, 1 deletion(-) diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 422c547b4..b6e60a9cd 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -79,7 +79,6 @@ pad = 0 [[assumptions]] desc = "`IS_WORD[lhs[0]]`" -iter = ["i", 1, 2] ref = "lt:a:range_lhs" [[assumptions]] From 8809d813d7bd5a678f8f6562885e825e74f098b9 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 27 Jan 2026 16:05:55 +0100 Subject: [PATCH 4/4] Update spec/src/lt.toml Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/src/lt.toml | 1 - 1 file changed, 1 deletion(-) diff --git a/spec/src/lt.toml b/spec/src/lt.toml index b6e60a9cd..10497b637 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -83,7 +83,6 @@ ref = "lt:a:range_lhs" [[assumptions]] desc = "`IS_WORD[rhs[0]]`" -iter = ["i", 1, 2] ref = "lt:a:range_rhs" [[assumptions]]