From ba295724ded1efeb135ce0f3a2764bcd61575f14 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 26 Jan 2026 15:59:13 +0100 Subject: [PATCH 1/8] spec: HALT: first draft --- spec/book.typ | 1 + spec/halt.typ | 47 ++++++++++++++++++++++++++++ spec/src/halt.toml | 76 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 124 insertions(+) create mode 100644 spec/halt.typ create mode 100644 spec/src/halt.toml diff --git a/spec/book.typ b/spec/book.typ index 29e61350c..ed7e3a621 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -19,6 +19,7 @@ #chapter("dvrm.typ")[DVRM chip] #chapter("load.typ")[LOAD chip] #chapter("ecall.typ")[ECALL chips] + #chapter("halt.typ")[HALT chips] #chapter("bitwise.typ")[BITWISE] ] ) diff --git a/spec/halt.typ b/spec/halt.typ new file mode 100644 index 000000000..00e1e766f --- /dev/null +++ b/spec/halt.typ @@ -0,0 +1,47 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_column_table, + render_chip_padding_table, + render_constraint_table, + total_nr_instantiated_columns, + total_nr_variables, +) + +#let config = load_config() +#let chip = load_chip("src/halt.toml", config) +#let halt = raw(chip.name) + +#show: book-page.with(title: "Halt chip") + += #halt chip + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The #halt chip leverages #nr_variables variables, spanning #nr_columns columns: +#render_chip_column_table(chip, config) + +== Assumptions +It is assumed the input is range checked: +#render_chip_assumptions(chip, config) + +== Constraints +The #halt chip: ++ makes sure register `x10` (containing the exit code) equals $0$ (@halt:c:read_zero_exit_code), ++ writes $0$ to all other registers (@halt:c:zeroize_registers_lo/@halt:c:zeroize_registers_hi), and ++ sets `pc` equal to $1$ (@halt:c:pc). +#render_constraint_table(chip, config, groups: "all") + +=== Lookup +The HALT chip contributes the following interaction to the lookup-argument: +#render_constraint_table(chip, config, groups: "lookup") + +*Note*: $93$ is the system call number corresponding to `sys_exit`. + +== Padding +This chip should only contain a single row. +Given that $2^0 = 1$, this chip does not need to be padded. +As such, no padding is defined. diff --git a/spec/src/halt.toml b/spec/src/halt.toml new file mode 100644 index 000000000..3f19a66f0 --- /dev/null +++ b/spec/src/halt.toml @@ -0,0 +1,76 @@ +name = "HALT" + +[[variables.input]] +name = "pc" +type = "DWordWL" +desc = "program counter containing the HALT call." + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "timestamp at which to halt the program" + +[[variables.input]] +name = "rv2" +type = "DWordWL" +desc = "value of register two at the point of calling HALT." + +[[constraint_groups]] +name = "all" + + +[[assumptions]] +desc = "`IS_WORD[pc[i]]`" +iter = ["i", 0, 1] + +[[assumptions]] +desc = "`IS_WORD[timestamp[i]]`" +iter = ["i", 0, 1] + +[[assumptions]] +desc = "`IS_WORD[rv2[i]]`" +iter = ["i", 0, 1] + + + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [1, 10, 0, ["-", ["^", 2, 64], 1], 1, 0, 0] +output = 0 +multiplicity = 1 +ref = "halt:c:read_zero_exit_code" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [1, "i", 0, ["-", ["^", 2, 64], 1], 1, 0, 0] +iter = ["i", 1, 9] +multiplicity = 1 +ref = "halt:c:zeroize_registers_lo" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [1, "i", 0, ["-", ["^", 2, 64], 1], 1, 0, 0] +iter = ["i", 11, 31] +multiplicity = 1 +ref = "halt:c:zeroize_registers_hi" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [1, 255, 1, ["-", ["^", 2, 64], 1], 1, 0, 0] +multiplicity = 1 +ref = "halt:c:pc" + +[[constraint_groups]] +name = "lookup" + +[[constraints.lookup]] +kind = "interaction" +tag = "ECALL" +input = [93, "pc", "timestamp", "rv2"] +output = 0 +multiplicity = ["-", 1] +ref = "halt:c:lookup" \ No newline at end of file From de2535da53c43ad0d9ccd02d4a428850d2bf3bf6 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 27 Jan 2026 09:18:50 +0100 Subject: [PATCH 2/8] spec: HALT: add link to sys call number --- spec/halt.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/halt.typ b/spec/halt.typ index 00e1e766f..a32bbc877 100644 --- a/spec/halt.typ +++ b/spec/halt.typ @@ -39,7 +39,7 @@ The #halt chip: The HALT chip contributes the following interaction to the lookup-argument: #render_constraint_table(chip, config, groups: "lookup") -*Note*: $93$ is the system call number corresponding to `sys_exit`. +*Note*: #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/master/linux-headers/include/asm-generic/unistd.h#L258")[$93$ is the system call number corresponding to `sys_exit`.] == Padding This chip should only contain a single row. From f0c0dd2a682538013b0bac7e49c2475311a08d92 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 27 Jan 2026 14:39:14 +0100 Subject: [PATCH 3/8] spec: HALT: update ECALL signature --- spec/src/halt.toml | 26 +++----------------------- 1 file changed, 3 insertions(+), 23 deletions(-) diff --git a/spec/src/halt.toml b/spec/src/halt.toml index 3f19a66f0..3e3c54513 100644 --- a/spec/src/halt.toml +++ b/spec/src/halt.toml @@ -1,37 +1,18 @@ name = "HALT" -[[variables.input]] -name = "pc" -type = "DWordWL" -desc = "program counter containing the HALT call." - [[variables.input]] name = "timestamp" type = "DWordWL" desc = "timestamp at which to halt the program" -[[variables.input]] -name = "rv2" -type = "DWordWL" -desc = "value of register two at the point of calling HALT." - -[[constraint_groups]] -name = "all" - - -[[assumptions]] -desc = "`IS_WORD[pc[i]]`" -iter = ["i", 0, 1] [[assumptions]] desc = "`IS_WORD[timestamp[i]]`" iter = ["i", 0, 1] -[[assumptions]] -desc = "`IS_WORD[rv2[i]]`" -iter = ["i", 0, 1] - +[[constraint_groups]] +name = "all" [[constraints.all]] kind = "interaction" @@ -70,7 +51,6 @@ name = "lookup" [[constraints.lookup]] kind = "interaction" tag = "ECALL" -input = [93, "pc", "timestamp", "rv2"] -output = 0 +input = ["timestamp", 93] multiplicity = ["-", 1] ref = "halt:c:lookup" \ No newline at end of file From 73ccdbd97bb34027c75b7736fb3697f6ee3b3ca5 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 27 Jan 2026 14:44:05 +0100 Subject: [PATCH 4/8] spec: HALT: minor update --- spec/halt.typ | 2 ++ spec/src/halt.toml | 12 ++++++------ 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/spec/halt.typ b/spec/halt.typ index a32bbc877..7a6e3d230 100644 --- a/spec/halt.typ +++ b/spec/halt.typ @@ -33,6 +33,8 @@ The #halt chip: + makes sure register `x10` (containing the exit code) equals $0$ (@halt:c:read_zero_exit_code), + writes $0$ to all other registers (@halt:c:zeroize_registers_lo/@halt:c:zeroize_registers_hi), and + sets `pc` equal to $1$ (@halt:c:pc). +Note that the writes performed by all these interactions are accompanied by the timestamp $2^64-1$; the maximum timestamp. +This prevents any other operation involving memory from being executed hereafter. #render_constraint_table(chip, config, groups: "all") === Lookup diff --git a/spec/src/halt.toml b/spec/src/halt.toml index 3e3c54513..716ebd75f 100644 --- a/spec/src/halt.toml +++ b/spec/src/halt.toml @@ -17,18 +17,18 @@ name = "all" [[constraints.all]] kind = "interaction" tag = "MEMW" -input = [1, 10, 0, ["-", ["^", 2, 64], 1], 1, 0, 0] -output = 0 +input = [1, "i", 0, ["-", ["^", 2, 64], 1], 1, 0, 0] +iter = ["i", 1, 9] multiplicity = 1 -ref = "halt:c:read_zero_exit_code" +ref = "halt:c:zeroize_registers_lo" [[constraints.all]] kind = "interaction" tag = "MEMW" -input = [1, "i", 0, ["-", ["^", 2, 64], 1], 1, 0, 0] -iter = ["i", 1, 9] +input = [1, 10, 0, ["-", ["^", 2, 64], 1], 1, 0, 0] +output = 0 multiplicity = 1 -ref = "halt:c:zeroize_registers_lo" +ref = "halt:c:read_zero_exit_code" [[constraints.all]] kind = "interaction" From 721c698d72d205e601fb1e57108465b7dc2e381a Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 27 Jan 2026 15:33:01 +0100 Subject: [PATCH 5/8] spec: HALT: document cleanup verification alternative --- spec/halt.typ | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/spec/halt.typ b/spec/halt.typ index 7a6e3d230..0a4134566 100644 --- a/spec/halt.typ +++ b/spec/halt.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, rj +#import "/book.typ": book-page, rj, aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -37,6 +37,12 @@ Note that the writes performed by all these interactions are accompanied by the This prevents any other operation involving memory from being executed hereafter. #render_constraint_table(chip, config, groups: "all") +#aside("Note on register clean up", +[ + Observe that --- in its current state --- this solution puts the burden of verifying the register cleanup on the verifier inside of the lookup argument. + Alternatively, one could add 31 lookups to the "memory" table to remove the _known_ final tokens for the registers there. +]) + === Lookup The HALT chip contributes the following interaction to the lookup-argument: #render_constraint_table(chip, config, groups: "lookup") @@ -46,4 +52,4 @@ The HALT chip contributes the following interaction to the lookup-argument: == Padding This chip should only contain a single row. Given that $2^0 = 1$, this chip does not need to be padded. -As such, no padding is defined. +As such, no padding is defined. \ No newline at end of file From 59f9d0e9b5220fe7c7ece81f4adeb9a31c7d324f Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 27 Jan 2026 15:58:35 +0100 Subject: [PATCH 6/8] adapt to new chapter format --- spec/halt.typ | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/spec/halt.typ b/spec/halt.typ index 0a4134566..5fa429b96 100644 --- a/spec/halt.typ +++ b/spec/halt.typ @@ -13,9 +13,7 @@ #let chip = load_chip("src/halt.toml", config) #let halt = raw(chip.name) -#show: book-page.with(title: "Halt chip") - -= #halt chip +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) From 89b0a5e1f9b72b7b7c2ad0bce8699db37638a429 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 27 Jan 2026 16:31:39 +0100 Subject: [PATCH 7/8] spec: HALT: fix MEMW register indexing --- spec/src/halt.toml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src/halt.toml b/spec/src/halt.toml index 716ebd75f..b0606e3e4 100644 --- a/spec/src/halt.toml +++ b/spec/src/halt.toml @@ -17,7 +17,7 @@ name = "all" [[constraints.all]] kind = "interaction" tag = "MEMW" -input = [1, "i", 0, ["-", ["^", 2, 64], 1], 1, 0, 0] +input = [1, ["*", 2, "i"], 0, ["-", ["^", 2, 64], 1], 1, 0, 0] iter = ["i", 1, 9] multiplicity = 1 ref = "halt:c:zeroize_registers_lo" @@ -25,7 +25,7 @@ ref = "halt:c:zeroize_registers_lo" [[constraints.all]] kind = "interaction" tag = "MEMW" -input = [1, 10, 0, ["-", ["^", 2, 64], 1], 1, 0, 0] +input = [1, ["*", 2, 10], 0, ["-", ["^", 2, 64], 1], 1, 0, 0] output = 0 multiplicity = 1 ref = "halt:c:read_zero_exit_code" @@ -33,7 +33,7 @@ ref = "halt:c:read_zero_exit_code" [[constraints.all]] kind = "interaction" tag = "MEMW" -input = [1, "i", 0, ["-", ["^", 2, 64], 1], 1, 0, 0] +input = [1, ["*", 2, "i"], 0, ["-", ["^", 2, 64], 1], 1, 0, 0] iter = ["i", 11, 31] multiplicity = 1 ref = "halt:c:zeroize_registers_hi" @@ -41,7 +41,7 @@ ref = "halt:c:zeroize_registers_hi" [[constraints.all]] kind = "interaction" tag = "MEMW" -input = [1, 255, 1, ["-", ["^", 2, 64], 1], 1, 0, 0] +input = [1, ["*", 2, 255], 1, ["-", ["^", 2, 64], 1], 1, 0, 0] multiplicity = 1 ref = "halt:c:pc" From 624bcbf8126ca0f71b70030b8e9e7e619844ac16 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 27 Jan 2026 16:36:28 +0100 Subject: [PATCH 8/8] spec: HALT: move halt.typ into ecall.typ --- spec/book.typ | 1 - spec/ecall.typ | 44 +++++++++++++++++++++++++++++++++++++++-- spec/halt.typ | 53 -------------------------------------------------- 3 files changed, 42 insertions(+), 56 deletions(-) delete mode 100644 spec/halt.typ diff --git a/spec/book.typ b/spec/book.typ index ce1891881..b194b7f70 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -21,7 +21,6 @@ ("dvrm.typ", [DVRM chip], ), ("load.typ", [LOAD chip], ), ("ecall.typ", [ECALL chips], ), - ("halt.typ", [HALT chip], ), ("bitwise.typ", [BITWISE chips], ), ) ) diff --git a/spec/ecall.typ b/spec/ecall.typ index 3bf2d3b69..9f2d96048 100644 --- a/spec/ecall.typ +++ b/spec/ecall.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page +#import "/book.typ": book-page, aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_column_table, @@ -13,5 +13,45 @@ #show: book-page("ecall.typ") -*placeholder chapter: WIP* +#let config = load_config() +#let chip = load_chip("src/halt.toml", config) +#let halt = raw(chip.name) +== #halt chip + +=== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The #halt chip leverages #nr_variables variable, spanning #nr_columns columns: +#render_chip_column_table(chip, config) + +=== Assumptions +It is assumed the input is range checked: +#render_chip_assumptions(chip, config) + +=== Constraints +The #halt chip: ++ makes sure register `x10` (containing the exit code) equals $0$ (@halt:c:read_zero_exit_code), ++ writes $0$ to all other registers (@halt:c:zeroize_registers_lo/@halt:c:zeroize_registers_hi), and ++ sets `pc` equal to $1$ (@halt:c:pc). +Note that the writes performed by all these interactions are accompanied by the timestamp $2^64-1$; the maximum timestamp. +This prevents any other operation involving memory from being executed hereafter. +#render_constraint_table(chip, config, groups: "all") + +#aside("Note on register clean up", +[ + Observe that --- in its current state --- this solution puts the burden of verifying the register cleanup on the verifier inside of the lookup argument. + Alternatively, one could add 31 lookups to the "memory" table to remove the _known_ final tokens for the registers there. +]) + +==== Lookup +The HALT chip contributes the following interaction to the lookup-argument: +#render_constraint_table(chip, config, groups: "lookup") + +*Note*: #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/master/linux-headers/include/asm-generic/unistd.h#L258")[$93$ is the system call number corresponding to `sys_exit`.] + +=== Padding +This chip should only contain a single row. +Given that $2^0 = 1$, this chip does not need to be padded. +As such, no padding is defined. diff --git a/spec/halt.typ b/spec/halt.typ deleted file mode 100644 index 5fa429b96..000000000 --- a/spec/halt.typ +++ /dev/null @@ -1,53 +0,0 @@ -#import "/book.typ": book-page, rj, aside -#import "/src.typ": load_config, load_chip -#import "/chip.typ": ( - render_chip_assumptions, - render_chip_column_table, - render_chip_padding_table, - render_constraint_table, - total_nr_instantiated_columns, - total_nr_variables, -) - -#let config = load_config() -#let chip = load_chip("src/halt.toml", config) -#let halt = raw(chip.name) - -#show: book-page(chip.name) - -== Columns -#let nr_variables = total_nr_variables(chip) -#let nr_columns = total_nr_instantiated_columns(chip, config) - -The #halt chip leverages #nr_variables variables, spanning #nr_columns columns: -#render_chip_column_table(chip, config) - -== Assumptions -It is assumed the input is range checked: -#render_chip_assumptions(chip, config) - -== Constraints -The #halt chip: -+ makes sure register `x10` (containing the exit code) equals $0$ (@halt:c:read_zero_exit_code), -+ writes $0$ to all other registers (@halt:c:zeroize_registers_lo/@halt:c:zeroize_registers_hi), and -+ sets `pc` equal to $1$ (@halt:c:pc). -Note that the writes performed by all these interactions are accompanied by the timestamp $2^64-1$; the maximum timestamp. -This prevents any other operation involving memory from being executed hereafter. -#render_constraint_table(chip, config, groups: "all") - -#aside("Note on register clean up", -[ - Observe that --- in its current state --- this solution puts the burden of verifying the register cleanup on the verifier inside of the lookup argument. - Alternatively, one could add 31 lookups to the "memory" table to remove the _known_ final tokens for the registers there. -]) - -=== Lookup -The HALT chip contributes the following interaction to the lookup-argument: -#render_constraint_table(chip, config, groups: "lookup") - -*Note*: #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/master/linux-headers/include/asm-generic/unistd.h#L258")[$93$ is the system call number corresponding to `sys_exit`.] - -== Padding -This chip should only contain a single row. -Given that $2^0 = 1$, this chip does not need to be padded. -As such, no padding is defined. \ No newline at end of file