spec: Update LT interaction signature so that it can be used properly for timestamps

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")
 

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"]
 

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 = "-μ"

spec/src/memw.toml

@@ -159,29 +159,29 @@ 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"
 
 [[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"