spec: fix header levels

spec/add.typ

@@ -20,14 +20,14 @@
 
 #add is a constraint template that is used to assert that $#`sum` = #`lhs` + #`rhs` mod 2^64$, under the condition that `cond` is non-zero.
 
-== Notation
+= Notation
 The #add constraint template has the following interface:
 #block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => ADD<sum; lhs, rhs>"))
 where `cond` is any value described by an expression _of degree at most $1$_.
 #highlighted_code("ADD<sum; lhs, rhs>") can be used to denote the _unconditional_ application of the #add template to `lhs`, `rhs`, and `sum`.
 
 #let sub = raw("SUB")
-=== #sub
+== #sub
 For ease of notation, we moreover introduce the #sub constraint template.
 Its interface
 #block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => SUB<diff; lhs, rhs>"))
@@ -36,12 +36,12 @@ maps onto the #add template as
 It constrains that $#`diff` = #`lhs` - #`rhs` mod 2^64$ when the expression `cond` is non-zero.
 As with #add, #highlighted_code("SUB<diff; lhs, rhs>") can be used to denote the _unconditional_ application of the template.
 
-== Variables
+= Variables
 #render_chip_column_table(chip, config)
 
-== Assumptions
+= Assumptions
 #render_chip_assumptions(chip, config)
 
-== Constraints
+= Constraints
 This template introduces the following constraints
 #render_constraint_table(chip, config)

spec/bitwise.typ

@@ -15,7 +15,7 @@
 
 #show: book-page(chip.name)
 
-== Columns
+= Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 #let nr_precomputed = ("input", "output").map(c => chip.variables.at(c)).flatten().len()
@@ -27,11 +27,11 @@ Of these, the _input_ and _output_ variables (#nr_precomputed in total) are prec
 *Note*: This table contains one row for every possible value of `(X, Y, Z)`.
 As such, it has length $2^8 dot 2^8 dot 2^4 = 2^(20)$.
 
-== Lookup
+= Lookup
 This chip adds the following interactions to the lookup:
 #render_constraint_table(chip, config)
 
-== Areas of Optimization
+= Areas of Optimization
 The following ideas may prove to be optimizations for the #bitwise chip:
 + Extend `IS_BYTE[X]` to `ARE_BYTES[X, Y]`, such that two bytes are range checked at once. 
   When only a single check is required, one can still execute `IS_BYTE[X] := ARE_BYTES[X, 0]`.

spec/branch.typ

@@ -14,18 +14,18 @@
 
 #show: book-page(chip.name)
 
-== Columns
+= Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 
 The `BRANCH` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
 #render_chip_column_table(chip, config)
 
-== Assumptions
+= Assumptions
 
 #render_chip_assumptions(chip, config)
 
-== Constraints
+= Constraints
 
 #rj[Check correspondence with CPU for passing in `offset` as word or dword]
 We constrain `next_pc` to be $#`base_address` + #`offset`$,
@@ -37,7 +37,7 @@ The range checks on `unmasked_low_byte` and `next_pc_low[0]` are performed impli
 This chip contributes the following to the lookup argument.
 #render_constraint_table(chip, config, groups: "output")
 
-== Padding
+= Padding
 
 The table can be padded to the next power of two with the following value assignments:
 

spec/cpu.typ

@@ -14,24 +14,24 @@
 
 #show: book-page(chip.name)
 
-== Columns
+= Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 
 The `CPU` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
 #render_chip_column_table(chip, config)
 
-== Assumptions
+= Assumptions
 #render_chip_assumptions(chip, config)
 
-== Constraints
+= Constraints
 First, we perform a decoding lookup for the current PC.
 
 #render_constraint_table(chip, config, groups: "decode")
 
 #rj[All casts for interactions will have to be reviewed once other chip interfaces stabilise]
 
-=== Range checks
+== Range checks
 
 We constrain all columns to have the appropriate ranges.
 The flags and register indices looked up from the decoding need to be checked,
@@ -46,13 +46,13 @@ The ranges of the other auxiliary columns are enforced through later constraints
 
 #render_constraint_table(chip, config, groups: "range")
 
-=== ALU
+== ALU
 
 The ALU functionality is then obtained through judicious dispatching to the corresponding chips.
 
 #render_constraint_table(chip, config, groups: "alu")
 
-=== Memory
+== Memory
 
 The interactions with the memory, both for register loading and storing, as for `LOAD` and `STORE` instructions are handled.
 Note that since registers need no byte-addressing, we store them in the memory argument with `Word` limbs.
@@ -62,28 +62,28 @@ to ensure the access is disjoint with the `pc` read into `rv1` as part of the `A
 
 #render_constraint_table(chip, config, groups: "mem")
 
-=== System
+== System
 
 The interactions with the wider system.
 
 #render_constraint_table(chip, config, groups: "sys")
 
-=== Input and output to the ALU
+== Input and output to the ALU
 
 We constrain `arg1`, `arg2` and `rvd` to correspond to the wanted values,
 including the appropriate sign/zero extension, depending on `word_instr`.
 
 #render_constraint_table(chip, config, groups: "ext")
 
-=== Other constraints
+== Other constraints
 For @cpu:c:is_equal, note that @cpu:c:sub sets `res` to be the difference between `arg1` and `arg2` whenever `BEQ` is $1$.
 Given that this difference is $0$ when both are equal, @cpu:c:is_equal ensures `is_equal` is set to $1$ if and only if $#`arg1` = #`arg2`$ and `BEQ` is set.
 
 #render_constraint_table(chip, config, groups: "misc")
 
 #rj[Document the choice to not have a multiplicity column here for padding]
 
-== Padding
+= Padding
 
 The CPU can be padded with the following values, which have a corresponding row
 in the DECODE table, at the _odd_ address 1, only reachable through a HALT ecall.

spec/decode.typ

@@ -21,14 +21,14 @@ For reasons of efficiency, data in this table is significantly compressed.
 Since reasoning about this compressed form is needlessly complex, the `decode (uncompressed)` section presents the same table in uncompressed form, and explains how to decode `RV64IM` assembly instructions to it.
 Instructions on how to compress the uncompressed table to form the compressed decode table, can be derived from the `packed_decode` variable provided below.
 
-== Columns
+= Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 
 The #decode table is comprised of #nr_variables variables that are expressed using #nr_columns columns:
 #render_chip_column_table(chip, config)
 
-== Padding
+= Padding
 The #decode table must be padded to a length that is a power of two.
 Empty rows with the following content can be added to achieve this:
 
@@ -39,7 +39,7 @@ Given that `CPU` asserts that `EBREAK = 0` (see @cpu:c:ebreak_traps), using this
 Note moreover that the `pc` is set to $7$.
 This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link(<cpu-padding-decode-row>)[additional instruction] referred to by `CPU`-padding lines).
 
-== Decoding
+= Decoding
 For the purposes of explaining decoding, we decompress #decode's `packed_decode` variable into its constituent variables.
 Note that the below table is _not_ used in practice: it is solely used for the purposes of this explanation.
 
@@ -64,7 +64,7 @@ For the purpose of brevity and readability, the table uses the following rules-o
 
 Further clarification is provided in the notes following the table.
 
-=== C-type instructions
+== C-type instructions
 The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size.
 This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$.
 To indicate an instruction is provided in compressed form, the `c_type` flag is introduced.
@@ -159,7 +159,7 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is
   [#figure(kind: "note", supplement: [], [#note]) #label(lbl)]
 }
 
-==== Notes
+== Notes
 We note the following about the above decoding table:
 #enum(numbering: "[1]",
   enum.item(

spec/ebook.typ

@@ -15,5 +15,6 @@
 #meta.summary.map(((ch, title, ref)) => [
   #pagebreak(weak: true)
   #heading(supplement: [Chapter], level: 1, title)#ref
+  #set heading(offset: 1)
   #include ch
 ]).join()

spec/ecall.typ

@@ -16,20 +16,20 @@
 #let config = load_config()
 #let chip = load_chip("src/halt.toml", config)
 #let halt = raw(chip.name)
-== #halt chip
+= #halt chip
 
-=== Columns
+== 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
+== Assumptions
 It is assumed the input is range checked:
 #render_chip_assumptions(chip, config)
 
-=== Constraints
+== 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
@@ -44,13 +44,13 @@ This prevents any other operation involving memory from being executed hereafter
   Alternatively, one could add 31 lookups to the "memory" table to remove the _known_ final tokens for the registers there.
 ])
 
-==== Lookup
+=== 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
+== 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.

spec/is_bit.typ

@@ -21,25 +21,25 @@
 #is_bit is a constraint template that is used to assert that a variable lies in the range ${0, 1}$ if some second variable is non-zero.
 Barring exceptional cases, this template is used to assert that a variable of type `Bit` assumes a valid value under some condition.
 
-== Interface
+= Interface
 The #is_bit constraint template has the following interface:
 #block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => IS_BIT<X>"))
 where `cond` is any value described by an expression _of degree at most $1$_.
 Note that #highlighted_code("IS_BIT<X>") can be used to denote the _unconditional_ application of the #is_bit template to `X`.
 
-== Variables
+= Variables
 The #is_bit template operates on two variables: `cond` and `X`:
 #render_chip_column_table(chip, config)
 
-== Constraints
+= Constraints
 It takes only one constraint to enforce that `X` must be either $0$ or $1$ whenever $#`cond` eq.not 0$:
 #render_constraint_table(chip, config)
 *Note*: 
 - In case of _unconditional_ template application, `cond` can be dropped from the constraint, simplifying it to $#`X` (1- #`X`) = 0$.
 - As described earlier, the `cond` variable must be describable by a degree-1 (i.e., linear) expression.
   This is to make sure that @isbit:c:isbit's expression has degree at most 3.
 
-== Proof of correctness
+= Proof of correctness
 If `cond` is $0$, @isbit:c:isbit is trivially satisfied: `X` can assume any value and the polynomial constraint will evaluate to $0$ regardless. 
 When $#`cond` eq.not 0$, it follows that the statement can only be proven when $#`X` (1-#`X`) equiv 0 mod p$, with $p$ the modulus of the field.
 Because `BaseField` is a prime field, this equality is only satisfied if either $#`X` equiv 0 mod p$ or $1-#`X` equiv 0 mod p$.

spec/load.typ

@@ -14,17 +14,17 @@
 
 #show: book-page(chip.name)
 
-== Columns
+= Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 
 The `LOAD` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
 #render_chip_column_table(chip, config)
 
-== Assumptions
+= Assumptions
 #render_chip_assumptions(chip, config)
 
-== Constraints
+= Constraints
 The chip delegates the actual memory interaction to the `MEMW` chip,
 and ensures correctness of the requested sign/zero extension.
 The output `res` is correctly range-checked as long as the memory contents are.
@@ -35,7 +35,7 @@ The chip contributes the following to the lookup argument.
 
 #render_constraint_table(chip, config, groups: "output")
 
-== Padding
+= Padding
 
 The table can be padded to the next power of two with the following value assignments:
 

spec/lt.typ

@@ -14,18 +14,18 @@
 
 #show: book-page(chip.name)
 
-== Columns
+= Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 
 The `LT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
 #render_chip_column_table(chip, config)
 
-== Assumptions
+= Assumptions
 We assume the inputs `lhs`, `rhs` and `signed` are partially range checked.
 #render_chip_assumptions(chip, config)
 
-== Constraints
+= Constraints
 We first constrain that all variables correspond to their definition.
 For the defining constraint of `lt`, @lt:c:lt, observe that it is a choice
 between two options, depending on the input flag `signed`.
@@ -80,7 +80,7 @@ The chip contributes the following to the lookup argument.
 
 #render_constraint_table(chip, config, groups: "output")
 
-== Padding
+= Padding
 
 The table can be padded to the next power of two with the following value assignments: