diff --git a/spec/add.typ b/spec/add.typ index 981a0ccb1..241ea8621 100644 --- a/spec/add.typ +++ b/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")) where `cond` is any value described by an expression _of degree at most $1$_. #highlighted_code("ADD") 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")) @@ -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") 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) diff --git a/spec/bitwise.typ b/spec/bitwise.typ index 9b5b4a638..36fe3b6e0 100644 --- a/spec/bitwise.typ +++ b/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]`. diff --git a/spec/branch.typ b/spec/branch.typ index f448f2da4..3e944ca63 100644 --- a/spec/branch.typ +++ b/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: diff --git a/spec/cpu.typ b/spec/cpu.typ index 9036593ac..ed6126388 100644 --- a/spec/cpu.typ +++ b/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,20 +62,20 @@ 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. @@ -83,7 +83,7 @@ Given that this difference is $0$ when both are equal, @cpu:c:is_equal ensures ` #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. diff --git a/spec/decode.typ b/spec/decode.typ index 586625226..87f6083f5 100644 --- a/spec/decode.typ +++ b/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()[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( diff --git a/spec/ebook.typ b/spec/ebook.typ index 835751163..f9ba76046 100644 --- a/spec/ebook.typ +++ b/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() diff --git a/spec/ecall.typ b/spec/ecall.typ index 9f2d96048..6908f768b 100644 --- a/spec/ecall.typ +++ b/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. diff --git a/spec/is_bit.typ b/spec/is_bit.typ index a12d62108..33477d377 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -21,17 +21,17 @@ #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")) where `cond` is any value described by an expression _of degree at most $1$_. Note that #highlighted_code("IS_BIT") 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*: @@ -39,7 +39,7 @@ It takes only one constraint to enforce that `X` must be either $0$ or $1$ whene - 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$. diff --git a/spec/load.typ b/spec/load.typ index 71c274d1b..bccb830f8 100644 --- a/spec/load.typ +++ b/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: diff --git a/spec/lt.typ b/spec/lt.typ index ea36eb4dc..3447efd70 100644 --- a/spec/lt.typ +++ b/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: diff --git a/spec/memory.typ b/spec/memory.typ index ec8735e49..1fcb7b54e 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -31,7 +31,7 @@ The initialization and finalization schemes together ensure both that (1) the ne for the lookup system are satisfied, and (2) the program is executed with the correct initial memory and register contents as specified by the ELF binary and the ISA. -== Memory types += Memory types A commonly made distinction of memory types is that of _read-only_ and _read-write_ memory, with the more restrictive read-only variant often allowing for more efficient solutions @@ -43,7 +43,7 @@ While there are some subsystems that can be modelled as read-only memory we opt to integrate these into the proof system via chip interactions (relying on techniques derived from table lookup arguments). As such, we only concern ourselves with read-write memory, moving forward. -== Memory operations += Memory operations Every memory operation has some conceptual attributes that are relevant to mention or discuss: @@ -75,7 +75,7 @@ For simplicity, we will always reserve a timestamp for every possible memory acc ] -== Permutation argument += Permutation argument We can conceptually organise the state of the memory as a collection of "tokens" that represent tuples $(serif("timestamp"), serif("address"), serif("value"))$, @@ -99,7 +99,7 @@ this "balancing" act of tokens can be integrated (with sufficient domain separat consuming a token corresponds to a "receive" and emitting a new token is a "send". #rj[properly link/refer to the logup spec] -== Temporal integrity += Temporal integrity To ensure temporal integrity, every memory operation needs to be constrained for the newly emitted token to have a strictly greater timestamp than the consumed token. @@ -125,7 +125,7 @@ We choose to represent timestamps as machine words, using the existing `LT` chip #rj[reference to CPU chip/timestamp column and MEMW chip] -== Initialization and Finalization += Initialization and Finalization Because the LogUp argument handling token consumption and emission needs to be fully balanced --- every token emitted should be consumed, and vice versa --- @@ -159,7 +159,7 @@ For each such table, the `page` variable is instantiated as the constant base ad The `offset` column is preprocessed, which helps the verifier ensure that each page has a single fixed size, but the verifier should still check that no pages overlap and all `page` values are page-aligned. -=== Page initialization +== Page initialization #rj[check whether we need `fini` to be range-checked] We present here a set of constraints on the `PAGE` table that @@ -211,7 +211,7 @@ and hence doesn't need a column, nor a range check. Most programs and compilers should however favor a memory locality that makes paged initialization/finalization comparable. ] -=== Register initialization/finalization +== Register initialization/finalization #rj[Properly link/reference ECALL/HALT chip] The initial and final state of registers can be entirely known by @@ -221,11 +221,11 @@ by the HALT ecall. As additionally, the number of registers is small, the verifier can directly add the required balancing terms to the LogUp sum. -== Notes and considerations += Notes and considerations - Register reads and writes may interact within a single cycle, so a correct and fixed ordering needs to be ensured - Correctness of initialization and completeness of finalization need to be ensured -== Future topics of interest += Future topics of interest - Optimize memory systems after determining factual bottlenecks (e.g. taking inspiration from Twist and Shout, or other recent research) diff --git a/spec/memw.typ b/spec/memw.typ index 77b786bf6..a3dfda42c 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -13,14 +13,14 @@ #show: book-page(chip.name) -== Columns += Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) The `MEMW` 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) @@ -29,7 +29,7 @@ as these are not necessary for the correctness of this chip in isolation. These properties are necessary for the consistency of the system as a whole, and therefore we document it here, keeping the type information as a reading help. -== Constraints += Constraints #render_constraint_table(chip, config, groups: "consistency") @@ -50,7 +50,7 @@ This chip contributes the following to the lookup argument. #render_constraint_table(chip, config, groups: "output") -== Future optimization ideas += Future optimization ideas - Fast path for aligned memory access where all bytes have the same old timestamp - MEMB chip that deals does a one-byte write to remove old_timestamp from here (uncertain tradeoffs) diff --git a/spec/mul.typ b/spec/mul.typ index b2fb53d92..a2fb7d1fc 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -16,7 +16,7 @@ #let mul = raw(chip.name) -== Columns += Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) @@ -27,12 +27,12 @@ The `MUL` chip is comprised of #nr_variables variables that are expressed using $mat(delim: #none, top; bottom)$ } -== Assumptions += Assumptions The following range checks are assumed to be performed/enforced outside of this chip: #render_chip_assumptions(chip, config) -== Constraints -=== Overview += Constraints +== Overview When `lhs` and `rhs` are _unsigned_ integers, computing their product $mod 2^128$ comes down to evaluating $ (sum_(j=0)^3 2^(16j) dot #`lhs`_j) dot (sum_(i=0)^3 2^(16i) dot #`rhs`_i) mod 2^128. @@ -79,25 +79,25 @@ However, there is some slack in how tight one has to constrain the `carry` value In fact, in this situation it suffices to assert that $#`carry`_i < frac(p, 2^32, style: "skewed") approx 2^31$, where $p$ denotes the field's modulus. Given that other chips also use 20-bit lookups, using `IS_B20` makes for a simpler design. -=== Definitions +== Definitions We constrain `lhs_is_negative` and `rhs_is_negative` according to their definition; `lo`, `hi` and `carry` are appropriately range checked. #render_constraint_table(chip, config, groups: "def") -=== Product +== Product @mul:c:raw_product defines `raw_product` in terms of the (sign extended) input values `lhs` and `rhs`. #render_constraint_table(chip, config, groups: "prod") -=== Lookup +== Lookup The #mul chip contributes the following to the lookup: #render_constraint_table(chip, config, groups: "lookup") -== Padding += Padding The table can be padded to the next power of two with the following value assignments: #render_chip_padding_table(chip, config) -== Notes += Notes - `lo` and `hi` are stored in `DWordHL`s (rather than `DWordWL`s) because of their values being range checked. Since it is not required that both `μ_lo` and `μ_hi` are non-zero at the same time, one cannot safely assume their range to be checked elsewhere. diff --git a/spec/shift.typ b/spec/shift.typ index 177ce6104..a2a3ec968 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -16,7 +16,7 @@ #show: book-page(chip.name) -== Interface += Interface The #shift chip has the following interface: #block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(240), ``` @@ -46,17 +46,17 @@ $ $ Here, `<<` and `>>` denote the _logical_ left and right shift operations, while `>>>` denotes the _arithmetic_ right shift operation. -== Columns += Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) The `SHIFT` 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) -== Explanation += Explanation This chip has a rather complex design as a result of designing it to fit in as few columns possible. We briefly discuss the intricacies of the design, attempting to illustrate its correctness. @@ -70,7 +70,7 @@ The output variable `out` is equivalent to `shifted`, but expressed using `Word` In the following, we cover how these two phases were designed to complement one another. Here, we start with discussing the _logical_ left/right shift operations only; the modifications required to compute the _arithmetic_ right shift will be discussed at the end. -=== First phase +== First phase We zoom in on the first step. Here, we make use of the two lookup operations - $#`HWSL[x: Half, y: B4]` := (#`x` #`<<` #`y`) mod 2^16$ (short for "HalfWord Shift Left"), and @@ -106,7 +106,7 @@ $ it only takes some rearranging and combining of the values $#`X[`i#`] := HWSL[in[`i#`], bit_shift]`$ and $#`Y[`i#`] := HWSLC[in[`i#`], bit_shift]`$ to form the limbs of $#`in <> shift` mod 16$. In the remaining case that $#`right` = 1$ and $#`shift` = 0 mod 16$, the limbs of $#`in <> shift` mod 16$ simply match those of `in`. -=== Second phase +== Second phase Since we're operating on 16-bit limbs, all the limbs in $#`in <> shift`$ must also occur somewhere in $#`in <> shift` mod 16$. The number of full-limbs we still need to shift is determined by the fifth and sixth least significant bit of `shift`. With `limb_shift` containing a unary decoding of the integer represented by these two bits, we find that the intermediate value needs to be shifted over by $i$ limbs (to the `left` or `right`) when $#`limb_shift[`i#`]` = 1$. @@ -114,13 +114,13 @@ These things combined yield `shifted`'s definition. Of course, when $#`word_instr` = 1$ and, thus, only $#`shift` mod 32$ should be considered, the bit-mask for the lookup constraining `limb_shift` is adjusted appropriately (see @shift:c:limb_shift_lookup). -=== Arithmetic right shift +== Arithmetic right shift Lastly, we discuss the case of performing the _arithmetic_ right shift. Here, `extension` is constrained to contain a repetition of `in`'s most significant bit. Copies of this variable are used for any full limbs shifted in when $#`right` = #`signed` = 1$. Moreover, `X[4]` contains a copy of `extension` shifted over by the right number of bits, to allow the construction of $#`in >>> shift` mod 16$ as the appropriate intermediate. -== Constraints += Constraints First, we constrain `bit_shift` based on whether we are left or right-shifting. @shift:c:zbs makes sure `zbs` is set to `1` if and only if `bit_shift = 0`. This flag is used to indicate the special case that $#`right` = 1$ and $#`shift` = 0 mod 16$. @@ -134,7 +134,7 @@ The case of `left`-shifting and $#`bit_shift` = 0$ will be used for padding rows To prevent unnecessary lookups in padding rows, we override $#`X[i]` := #`in[i]`$ and $#`Y[i]` := 0$ here. #render_constraint_table(chip, config, groups: "intra_limb_shift") -=== Full-limb shifting +== Full-limb shifting Next, we constrain that `limb_shift` is a proper unary encoding of the fifth (and sixth if $#`word_instr` = 0$) bit of `shift`. For this to be the case, three requirements must be satisfied: + *unary(0)*: $#`limb_shift[`i#`]` in {0, 1}$ for $i in [0, 3]$, @@ -164,16 +164,16 @@ This is the exact relation @shift:c:limb_shift_lookup enforces. Hereafter, one must only check that `out` is the proper cast of `shifted` into a `DWordWL`. #render_constraint_table(chip, config, groups: "limb_shifting") -=== Miscellaneous +== Miscellaneous #render_constraint_table(chip, config, groups: ("left_flag", "is_negative")) *Note*: `is_negative` is not used when `signed = 0`. As such, there is no problem with it being unconstrained in this case. -=== Lookups +== Lookups This chip adds the following interaction to the lookup. #render_constraint_table(chip, config, groups: "lookups") -== Padding += Padding The table can be padded to the next power of two with the following value assignments: diff --git a/spec/sign.typ b/spec/sign.typ index 6f8993f53..dcc941e47 100644 --- a/spec/sign.typ +++ b/spec/sign.typ @@ -20,20 +20,20 @@ #sign is a constraint template that is used to extract a `Half`word's sign. -== Interface += Interface The #sign constraint template has the following interface: #block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("SIGN")) It constrains that `sign` is set to `1` when both `X`'s most significant bit and `signed` are $1$, and $0$ otherwise. -== Variables += Variables The #sign template operates on three variables: #render_chip_column_table(chip, config) -== Assumptions += Assumptions The #sign template operates on the following assumptions: #render_chip_assumptions(chip, config) -== Constraints += Constraints It takes only two constraints to compute the `sign` of `X`, given whether `X` represents a `signed` value or not. When $#`signed` = 1$, the sign of `X` is equal to its most significant bit. This value is extracted in @sign:c:sign_if_signed.