diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ new file mode 100644 index 000000000..d2f55f55a --- /dev/null +++ b/spec/about_ecalls.typ @@ -0,0 +1,24 @@ +#import "/book.typ": book-page, aside +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, + render_chip_assumptions, + render_chip_padding_table, +) + +#let config = load_config() + +#show: book-page("about_ecalls.typ") + +ECALLs provide system-level functionalities to the guest program. + +When `ECALL` is executed, it is assumed that: +- register `A7` contains the system call number + #footnote([The RISC-V system call ABI; libriscv.no, #link("https://web.archive.org/web/20260128152107/https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[src]]]), +- the arguments are located in registers `A0`-`A6`, and +- the return value is written to `A0`, +where `A0`-`A7` are symbolic names for the registers `x10`-`x17` +#footnote([RISC-V - Register sets; en.wikipedia.org, #link("https://web.archive.org/web/20260209053447/https://en.wikipedia.org/wiki/RISC-V#Register_sets")[[src]]]). diff --git a/spec/book.typ b/spec/book.typ index bf8b044ec..38fec945c 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -8,31 +8,53 @@ authors: ("3MI Labs", "Aligned"), version: "0.2", summary: ( - ("logup.typ", [LogUp argument], ), - ("memory.typ", [Memory argument], ), - ("variables.typ", [Variables], ), - ("signatures.typ", [Signatures], ), - ("is_bit.typ", [IS_BIT template], ), - ("sign.typ", [SIGN template], ), - ("add.typ", [ADD/SUB template], ), - ("neg.typ", [NEG template], ), - ("decode.typ", [DECODE table], ), - ("cpu.typ", [CPU chip], ), - ("shift.typ", [SHIFT chip], ), - ("branch.typ", [BRANCH chip], ), - ("memw.typ", [MEMW chip], ), - ("lt.typ", [LT chip], ), - ("mul.typ", [MUL chip], ), - ("dvrm.typ", [DVRM chip], ), - ("load.typ", [LOAD chip], ), - ("ecall.typ", [ECALL chips], ), - ("bitwise.typ", [BITWISE chips], ), + ("PROOF SYSTEM", ( + ("logup.typ", [LogUp argument], ), + ("memory.typ", [Memory argument], ), + )), + ("OVERVIEW", ( + ("variables.typ", [Variables], ), + ("signatures.typ", [Signatures], ), + )), + ("TEMPLATES", ( + ("is_bit.typ", [IS_BIT template], ), + ("sign.typ", [SIGN template], ), + ("add.typ", [ADD/SUB template], ), + ("neg.typ", [NEG template], ), + )), + ("MEMORY", ( + ("memw.typ", [MEMW chip], ), + )), + ("CPU", ( + ("decode.typ", [DECODE table], ), + ("cpu.typ", [CPU chip], ), + )), + ("ALU", ( + ("shift.typ", [SHIFT chip], ), + ("branch.typ", [BRANCH chip], ), + ("lt.typ", [LT chip], ), + ("mul.typ", [MUL chip], ), + ("dvrm.typ", [DVRM chip], ), + ("load.typ", [LOAD chip], ), + ("bitwise.typ", [BITWISE chips], ), + )), + ("ECALLS", ( + ("about_ecalls.typ", [About ECALL], ), + ("halt.typ", [HALT chip], ), + ("commit.typ", [COMMIT chip], ), + )) ) ) +#let meta_sections = meta.summary.map(m => m.at(1)).sum() #book-meta( title: meta.title, authors: meta.authors, - summary: prefix-chapter("front.typ", meta.title) + meta.summary.map(((ch, title, _ref)) => chapter(ch, title)).join() + summary: prefix-chapter("front.typ", meta.title) + + meta.summary.map( + ((title, sections)) => { + heading(depth: 1, title) + sections.map(((ch, title, _ref)) => chapter(ch, title)).join() + } + ).join() ) #let common-formatting(body) = { @@ -93,11 +115,11 @@ #let xref(rf) = { assert(is-shiroa, message: "xref should only be used when compiling for shiroa") let lbl = rf.target - let found = meta.summary.find(((_, _, tag)) => str(lbl).starts-with(str(tag))) + let found = meta_sections.find(((_, _, tag)) => str(lbl).starts-with(str(tag))) context if found != none and found.at(0) != _toplevel.final() { let (ch, title, ref) = found if ref == lbl { - cross-link("/" + ch, [Chapter #(meta.summary.position(x => x == found) + 1)]) + cross-link("/" + ch, [Chapter #(meta_sections.position(x => x == found) + 1)]) } else { // Because shiroa does weird url escaping let shiroa-label = label(str(lbl).replace(":", "%3A")) @@ -130,12 +152,12 @@ } #let book-page(file, ..args) = { - let file = if file.ends-with(".typ") { - file - } else { - lower(file) + ".typ" + if not file.ends-with(".typ") { + file = lower(file) + ".typ" } - assert(meta.summary.find(((f, _, _)) => f == file) != none, message: "Couldn't resolve typst source file " + file) + + assert(meta_sections.find(s => s.at(0) == file) != none, message: "Couldn't resolve typst source file " + file) + if is-shiroa { (body) => { show: common-formatting @@ -147,7 +169,7 @@ } }) let cond() = _toplevel.final() == file - project.with(..args, title: context meta.summary.find(x => x.at(0) == _toplevel.final()).at(1), cond: cond)([ + project.with(..args, title: context meta_sections.find(x => x.at(0) == _toplevel.final()).at(1), cond: cond)([ #show ref: it => context if _toplevel.final() == file { xref(it) } diff --git a/spec/ecall.typ b/spec/commit.typ similarity index 70% rename from spec/ecall.typ rename to spec/commit.typ index 2a7759876..a5974e763 100644 --- a/spec/ecall.typ +++ b/spec/commit.typ @@ -10,80 +10,21 @@ render_chip_padding_table, ) -#let config = load_config() - -#show: book-page("ecall.typ") - -ECALLs provide system-level functionalities to the guest program. - -When `ECALL` is executed, it is assumed that: -- register `A7` contains the system call number - #footnote([The RISC-V system call ABI; libriscv.no, #link("https://web.archive.org/web/20260128152107/https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[src]]]), -- the arguments are located in registers `A0`-`A6`, and -- the return value is written to `A0`, -where `A0`-`A7` are symbolic names for the registers `x10`-`x17` -#footnote([RISC-V - Register sets; en.wikipedia.org, #link("https://web.archive.org/web/20260209053447/https://en.wikipedia.org/wiki/RISC-V#Register_sets")[[src]]]). - - -#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) -#let nr_halt_interactions = compute_nr_interactions(chip) - -The #halt chip leverages #nr_variables variable, spanning #nr_columns columns and leverages #nr_halt_interactions interaction(s): -#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 -In this VM, halting is considered equivalent to executing a `sys_exit`. -Hence, this chip responds to `ECALL`s with system call number 93. -#footnote([RISC-V GNU-toolchain, `unistd.h`; version 2026-01-23, #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/2026.01.23/linux-headers/include/asm-generic/unistd.h#L258")[[src]]]) -The HALT chip therefore contributes the following interaction to the lookup-argument: -#render_constraint_table(chip, config, groups: "lookup") - -== 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. - +#show: book-page("commit.typ") #let config = load_config() #let chip = load_chip("src/commit.toml", config) #let commit = raw(chip.name) -= #commit chip -== Columns += Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) -#let nr_commit_interactions = compute_nr_interactions(chip) +#let nr_interactions = compute_nr_interactions(chip) -The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_commit_interactions interactions: +The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions: #render_chip_column_table(chip, config) -== Constraints += Constraints In this VM, committing is considered equivalent to writing a value to `stdout`. Hence, this chip responds to `ECALL`s with system call number 64. #footnote([RISC-V GNU-toolchain, `unistd.h`; version 2026-01-23, #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/2026.01.23/linux-headers/include/asm-generic/unistd.h#L174")[[src]]]) @@ -152,11 +93,11 @@ Lastly, we must make sure `first`, `end` and `μ` are bits (@commit:c:range_firs These are required to ensure the multiplicities $-(#`μ` - #`first`)$ and $#`μ` - #`end`$ are binary. #render_constraint_table(chip, config, groups: "bits") -== Padding += Padding To pad this chip, use the below data. #render_chip_padding_table(chip, config) -== Notes/optimizations += Notes/optimizations - The current version only supports writing to `stdout`. This chip could potentially be extended to support writing to arbitrary `fd`s - One might be able to replace @commit:c:end by `end => count = 0`. diff --git a/spec/ebook.typ b/spec/ebook.typ index c176dcec3..1bd691b9f 100644 --- a/spec/ebook.typ +++ b/spec/ebook.typ @@ -6,15 +6,39 @@ #align(center, text(style: "italic", fill: luma(40%))[Version #meta.version]) #align(center, meta.authors.join(", ")) #pagebreak(weak: true) -#outline() + +// outline +#show outline.entry.where(level: 1): set outline.entry(fill: line(length: 100%, stroke: stroke(dash: "solid"))) +#show outline.entry.where(level: 1): it => { + v(15pt, weak: true) + strong(it) + v(5pt, weak: true) +} +#show outline.entry.where(level: 2): it => { + v(10pt, weak: true) + it +} +#outline(depth: 3) + +// chapter pages +#show heading.where(level: 1): it => align(center + horizon)[#underline(it, offset: 10pt, extent: 5pt)] #show: common-formatting -#show heading: set heading(numbering: "1.1") +#show heading: set heading(numbering: (..args) => { + let args = args.pos() + let skip_first = args.slice(calc.min(args.len(), 1)) + numbering("1.1", ..skip_first) +}) #show raw.where(block: true): set block(fill: luma(230)) -#meta.summary.map(((ch, title, ref)) => [ - #pagebreak(weak: true) - #heading(supplement: [Chapter], level: 1, title)#ref - #set heading(offset: 1) - #include ch -]).join() +#for (ch_title, sections) in meta.summary { + pagebreak(weak: true) + heading(supplement: [Chapter], level: 1, ch_title, numbering: none) + + for (sec, sec_title, ref) in sections { + pagebreak(weak: true) + [#heading(level: 2, supplement: [Section], sec_title)#ref] + set heading(offset: 2) + include sec + } +} diff --git a/spec/halt.typ b/spec/halt.typ new file mode 100644 index 000000000..803c06e60 --- /dev/null +++ b/spec/halt.typ @@ -0,0 +1,56 @@ +#import "/book.typ": book-page, aside +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + compute_nr_interactions, + render_constraint_table, + render_chip_assumptions, + render_chip_padding_table, +) + +#show: book-page("halt.typ") + +#let config = load_config() +#let chip = load_chip("src/halt.toml", config) +#let halt = raw(chip.name) + += Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) +#let nr_interactions = compute_nr_interactions(chip) + +The #halt chip leverages #nr_variables variable, spanning #nr_columns columns and leverages #nr_interactions interactions:: +#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 +In this VM, halting is considered equivalent to executing a `sys_exit`. +Hence, this chip responds to `ECALL`s with system call number 93. +#footnote([RISC-V GNU-toolchain, `unistd.h`; version 2026-01-23, #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/2026.01.23/linux-headers/include/asm-generic/unistd.h#L258")[[src]]]) +The HALT chip therefore contributes the following interaction to the lookup-argument: +#render_constraint_table(chip, config, groups: "lookup") + += 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.