diff --git a/404.html b/404.html index bd3d9ba0..d311226d 100644 --- a/404.html +++ b/404.html @@ -97,7 +97,7 @@ diff --git a/concepts.html b/concepts.html index f389d4d2..db14ac50 100644 --- a/concepts.html +++ b/concepts.html @@ -95,7 +95,7 @@ diff --git a/concepts/preliminaries.html b/concepts/preliminaries.html index b767c4c8..dbc5a49d 100644 --- a/concepts/preliminaries.html +++ b/concepts/preliminaries.html @@ -95,7 +95,7 @@ diff --git a/design.html b/design.html index 13071ec2..47df8023 100644 --- a/design.html +++ b/design.html @@ -95,7 +95,7 @@ diff --git a/design/actions.html b/design/actions.html index 70789b05..4ba7285b 100644 --- a/design/actions.html +++ b/design/actions.html @@ -95,7 +95,7 @@ diff --git a/design/circuit.html b/design/circuit.html index 9a4ae59c..d555d21c 100644 --- a/design/circuit.html +++ b/design/circuit.html @@ -95,7 +95,7 @@ diff --git a/design/circuit/gadgets.html b/design/circuit/gadgets.html index 3e32e133..f92a3698 100644 --- a/design/circuit/gadgets.html +++ b/design/circuit/gadgets.html @@ -95,7 +95,7 @@ diff --git a/design/circuit/gadgets/decomposition.html b/design/circuit/gadgets/decomposition.html new file mode 100644 index 00000000..9246a5b7 --- /dev/null +++ b/design/circuit/gadgets/decomposition.html @@ -0,0 +1,246 @@ + + + + + + Decomposition - The Orchard Book + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ +
+ + + + + + + + + + + +
+
+ +

Decomposition

+

Given a field element , these gadgets decompose it into -bit windows where each a -bit value.

+

This is done using a running sum We initialize the running sum and compute subsequent terms This gives us:

+

+

Strict mode

+

Strict mode constrains the running sum output to be zero, thus range-constraining the field element to be within bits.

+

In strict mode, we are also assured that gives us the last window in the decomposition.

+

Lookup decomposition

+

This gadget makes use of a -bit lookup table to decompose a field element into -bit words. Each -bit word is range-constrained by a lookup in the -bit table.

+

Short range check

+

Using two -bit lookups, we can range-constrain a field element to be bits, where To do this:

+
    +
  1. Constrain to be within bits using a -bit lookup.
  2. +
  3. Constrain to be within bits using a -bit lookup.
  4. +
+

Short range decomposition

+

For a short range (for instance, ), we can range-constrain each word using a polynomial constraint instead of a lookup:

+

+where

+ +
+ + +
+
+ + + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/design/circuit/gadgets/ecc.html b/design/circuit/gadgets/ecc.html index 039fc3ab..c7114446 100644 --- a/design/circuit/gadgets/ecc.html +++ b/design/circuit/gadgets/ecc.html @@ -95,7 +95,7 @@ diff --git a/design/circuit/gadgets/ecc/addition.html b/design/circuit/gadgets/ecc/addition.html index c00dfa4f..fa68eb27 100644 --- a/design/circuit/gadgets/ecc/addition.html +++ b/design/circuit/gadgets/ecc/addition.html @@ -95,7 +95,7 @@ @@ -224,7 +224,7 @@ instead be computed as

Max degree: 6

Analysis of constraints

-

+

Propositions:

Test cases:

diff --git a/design/circuit/gadgets/ecc/fixed-base-scalar-mul.html b/design/circuit/gadgets/ecc/fixed-base-scalar-mul.html index 854f451b..42042470 100644 --- a/design/circuit/gadgets/ecc/fixed-base-scalar-mul.html +++ b/design/circuit/gadgets/ecc/fixed-base-scalar-mul.html @@ -95,7 +95,7 @@ @@ -173,85 +173,20 @@
  • and bases for ; and
  • base for .
  • -

    Witness scalar

    -

    In most cases, we multiply the fixed bases by bit scalars from . We decompose a full-width scalar into -bit windows:

    +

    Decompose scalar

    +

    We support fixed-base scalar multiplication with three types of scalars:

    +

    Full-width scalar

    +

    A -bit scalar from . We decompose a full-width scalar into -bit windows:

    -

    The scalar multiplication will be computed correctly for representing any integer in the range . -If is witnessed directly then no issue of canonicity arises. If the scalar is given as a base field element, then -care must be taken to ensure a canonical representation, since . This occurs, for example, in the scalar -multiplication for the nullifier computation of the Action circuit.

    -

    -

    At the point of witnessing the scalar, we range-constrain each -bit word of its decomposition. - -where

    -

    Load fixed base

    -

    Then, we precompute multiples of the fixed base for each window. This takes the form of a window table: such that:

    - -

    The additional term lets us avoid adding the point at infinity in the case . We offset these accumulated terms by subtracting them in the final window, i.e. we subtract .

    -
    -

    Note: Although an offset of would naively suffice, it introduces an edge case when . -In this case, the window table entries evaluate to the same point:

    -
      -
    • -
    • -
    -

    In fixed-base scalar multiplication, we sum the multiples of at each window (except the last) using incomplete addition. -Since the point doubling case is not handled by incomplete addition, we avoid it by using an offset of

    -
    -

    For each window of fixed-base multiples :

    - -

    Repeating this for all windows, we end up with:

    - -

    We load these precomputed values into fixed columns whenever we do fixed-base scalar multiplication in the circuit.

    -

    Fixed-base scalar multiplication

    -

    Given a decomposed scalar and a fixed base , we compute as follows:

    -
      -
    1. For each in the scalar decomposition, witness the - and -coordinates
    2. -
    3. Check that is on the curve: .
    4. -
    5. Witness such that .
    6. -
    7. For all windows but the last, use incomplete addition to sum the 's, resulting in .
    8. -
    9. For the last window, use complete addition and return the final result.
    10. -
    -
    -

    Note: complete addition is required in the final step to correctly map to a representation of the point at infinity, ; and also to handle a corner case for which the last step is a doubling.

    -
    -

    Constraints: -

    -

    where (from the Pallas curve equation).

    -

    Fixed-base scalar multiplication with signed short exponent

    -

    This is used for . We want to compute , where -

    -

    and are each already constrained to bits (by their use as inputs to ).

    -

    Witness the sign and magnitude such that -

    -

    Then compute , and conditionally negate using .

    -

    We compute the window table in a similar way to full-width fixed-base scalar multiplication, -but with only windows:

    -

    -

    In addition to the full-width -bit constraints, we have two additional constraints:

    -

    -

    Fixed-base scalar multiplication using base field element

    -

    We support using a base field element as the scalar in fixed-base multiplication. -This is used in -: here, the scalar is the result of a base field addition.

    -

    Decompose the base field element into three-bit windows using a running sum , where for (This running sum is not to be confused with the array used to check the -coordinate of a fixed-base window.)

    -

    We set , which means: -

    -

    We must range-constrain the difference at each step of the running sum. We also constrain the final output of the running sum to be . -

    -

    We also enforce canonicity of this decomposition. That is, we want to check that where the is Pallas base field modulus Note that

    +

    The scalar multiplication will be computed correctly for representing any integer in the range .

    +

    +

    We range-constrain each -bit word of the scalar decomposition using a polynomial range-check constraint: + +where

    +

    Base field element

    +

    We support using a base field element as the scalar in fixed-base multiplication. This occurs, for example, in the scalar multiplication for the nullifier computation of the Action circuit : here, the scalar is the result of a base field addition.

    +

    Decompose the base field element into three-bit windows, and range-constrain each window, using the short range decomposition gadget in strict mode, with

    +

    If is witnessed directly then no issue of canonicity arises. However, because the scalar is given as a base field element here, care must be taken to ensure a canonical representation, since . That is, we must check that where the is Pallas base field modulus Note that

    To do this, we decompose into three pieces:

    We check the correctness of this decomposition by: @@ -271,8 +206,67 @@ If the MSB

  • Then, we constrain bits of to be zeroes; in other words, we constrain the three-bit word We make use of the running sum decomposition to obtain
  • -

    Define . To check that we use 13 ten-bit lookups, where we constrain the running sum output of the lookup to be if +

    Define . To check that we use 13 ten-bit lookups, where we constrain the running sum output of the lookup to be if

    +

    Short signed scalar

    +

    A short signed scalar is witnessed as a magnitude and sign such that +

    +

    This is used for . We want to compute , where +

    +

    and are each already constrained to bits (by their use as inputs to ).

    +

    Decompose the magnitude into three-bit windows, and range-constrain each window, using the short range decomposition gadget in strict mode, with

    +

    We have two additional constraints: +

    +

    Load fixed base

    +

    Then, we precompute multiples of the fixed base for each window. This takes the form of a window table: such that:

    + +

    The additional term lets us avoid adding the point at infinity in the case . We offset these accumulated terms by subtracting them in the final window, i.e. we subtract .

    +
    +

    Note: Although an offset of would naively suffice, it introduces an edge case when . +In this case, the window table entries evaluate to the same point:

    +
      +
    • +
    • +
    +

    In fixed-base scalar multiplication, we sum the multiples of at each window (except the last) using incomplete addition. +Since the point doubling case is not handled by incomplete addition, we avoid it by using an offset of

    +
    +

    For each window of fixed-base multiples :

    + +

    Repeating this for all windows, we end up with:

    + +

    We load these precomputed values into fixed columns whenever we do fixed-base scalar multiplication in the circuit.

    +

    Fixed-base scalar multiplication

    +

    Given a decomposed scalar and a fixed base , we compute as follows:

    +
      +
    1. For each in the scalar decomposition, witness the - and -coordinates
    2. +
    3. Check that is on the curve: .
    4. +
    5. Witness such that .
    6. +
    7. For all windows but the last, use incomplete addition to sum the 's, resulting in .
    8. +
    9. For the last window, use complete addition and return the final result.
    10. +
    +
    +

    Note: complete addition is required in the final step to correctly map to a representation of the point at infinity, ; and also to handle a corner case for which the last step is a doubling.

    +
    +

    Constraints: +

    +

    where (from the Pallas curve equation).

    +

    Signed short exponent

    +

    Recall that the signed short exponent is witnessed as a bit magnitude , and a sign Using the above algorithm, we compute . Then, to get the final result we conditionally negate using .

    +

    Constraints: +

    Layout

    Note: this doesn't include the last row that uses complete addition. In the implementation this is allocated in a different region.

    diff --git a/design/circuit/gadgets/ecc/var-base-scalar-mul.html b/design/circuit/gadgets/ecc/var-base-scalar-mul.html index 9d25de51..917d8465 100644 --- a/design/circuit/gadgets/ecc/var-base-scalar-mul.html +++ b/design/circuit/gadgets/ecc/var-base-scalar-mul.html @@ -95,7 +95,7 @@ @@ -306,7 +306,7 @@ where

    where can be computed by another running sum. Note that the factor of has no effect on the constraint, since the RHS is zero.

    Running sum range check

    -

    We make use of a -bit lookup range check in the circuit to subtract the low bits of . The range check subtracts the first bits of and right-shifts the result to give

    +

    We make use of a -bit lookup range check in the circuit to subtract the low bits of . The range check subtracts the first bits of and right-shifts the result to give

    diff --git a/design/circuit/gadgets/lookup_range_check.html b/design/circuit/gadgets/lookup_range_check.html deleted file mode 100644 index c797a1ef..00000000 --- a/design/circuit/gadgets/lookup_range_check.html +++ /dev/null @@ -1,240 +0,0 @@ - - - - - - Lookup Range Check - The Orchard Book - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
    - -
    - - - - - - - - - - - -
    -
    - -

    Lookup decomposition

    -

    This gadget makes use of a -bit lookup table to decompose a field element into -bit words. Firstly, express where each a -bit value.

    -

    We initialize the running sum and compute subsequent terms This gives us:

    -

    -

    Each -bit word is range-constrained by a lookup in the -bit table. This gadget takes in and returns

    -

    Strict mode

    -

    Strict mode constrains the running sum output to be zero, thus range-constraining the field element to be within bits.

    -

    Short range check

    -

    Using two -bit lookups, we can range-constrain a field element to be bits, where To do this:

    -
      -
    1. Constrain to be within bits using a -bit lookup.
    2. -
    3. Constrain to be within bits using a -bit lookup.
    4. -
    - -
    - - -
    -
    - - - -
    - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/design/circuit/gadgets/sinsemilla.html b/design/circuit/gadgets/sinsemilla.html index d124e27b..4fa066b6 100644 --- a/design/circuit/gadgets/sinsemilla.html +++ b/design/circuit/gadgets/sinsemilla.html @@ -95,7 +95,7 @@ @@ -264,7 +264,7 @@ - @@ -282,7 +282,7 @@ - diff --git a/design/commitment-tree.html b/design/commitment-tree.html index 3a03d9f8..c11debdb 100644 --- a/design/commitment-tree.html +++ b/design/commitment-tree.html @@ -95,7 +95,7 @@ diff --git a/design/commitments.html b/design/commitments.html index cdf1b5df..926682bc 100644 --- a/design/commitments.html +++ b/design/commitments.html @@ -95,7 +95,7 @@ diff --git a/design/keys.html b/design/keys.html index 597a5070..0ba2a5b5 100644 --- a/design/keys.html +++ b/design/keys.html @@ -95,7 +95,7 @@ diff --git a/design/nullifiers.html b/design/nullifiers.html index 415790e7..0672564d 100644 --- a/design/nullifiers.html +++ b/design/nullifiers.html @@ -95,7 +95,7 @@ diff --git a/design/signatures.html b/design/signatures.html index a9de1f3c..505376a1 100644 --- a/design/signatures.html +++ b/design/signatures.html @@ -95,7 +95,7 @@ diff --git a/index.html b/index.html index 2ef0b7f1..6a32b733 100644 --- a/index.html +++ b/index.html @@ -95,7 +95,7 @@ diff --git a/print.html b/print.html index ffe79351..d6f443fb 100644 --- a/print.html +++ b/print.html @@ -97,7 +97,7 @@ @@ -794,7 +794,7 @@ instead be computed as

    Max degree: 6

    Analysis of constraints

    -

    +

    Propositions:

    Test cases:

    @@ -886,85 +886,20 @@ because in all remaining cases, and bases for ; and
  • base for .
  • -

    Witness scalar

    -

    In most cases, we multiply the fixed bases by bit scalars from . We decompose a full-width scalar into -bit windows:

    +

    Decompose scalar

    +

    We support fixed-base scalar multiplication with three types of scalars:

    +

    Full-width scalar

    +

    A -bit scalar from . We decompose a full-width scalar into -bit windows:

    -

    The scalar multiplication will be computed correctly for representing any integer in the range . -If is witnessed directly then no issue of canonicity arises. If the scalar is given as a base field element, then -care must be taken to ensure a canonical representation, since . This occurs, for example, in the scalar -multiplication for the nullifier computation of the Action circuit.

    -

    -

    At the point of witnessing the scalar, we range-constrain each -bit word of its decomposition. - -where

    -

    Load fixed base

    -

    Then, we precompute multiples of the fixed base for each window. This takes the form of a window table: such that:

    -
      -
    • for the first 84 rows :
    • -
    • in the last row :
    • -
    -

    The additional term lets us avoid adding the point at infinity in the case . We offset these accumulated terms by subtracting them in the final window, i.e. we subtract .

    -
    -

    Note: Although an offset of would naively suffice, it introduces an edge case when . -In this case, the window table entries evaluate to the same point:

    -
      -
    • -
    • -
    -

    In fixed-base scalar multiplication, we sum the multiples of at each window (except the last) using incomplete addition. -Since the point doubling case is not handled by incomplete addition, we avoid it by using an offset of

    -
    -

    For each window of fixed-base multiples :

    -
      -
    • Define a Lagrange interpolation polynomial that maps to the -coordinate of the multiple , i.e. -
    • -
    • Find a value such that is a square in the field, but the wrong-sign -coordinate does not produce a square.
    • -
    -

    Repeating this for all windows, we end up with:

    -
      -
    • an table storing coefficients interpolating the coordinate for each window. Each -coordinate interpolation polynomial will be of the form - -where and 's are the coefficients for each power of ; and
    • -
    • a length- array of 's.
    • -
    -

    We load these precomputed values into fixed columns whenever we do fixed-base scalar multiplication in the circuit.

    -

    Fixed-base scalar multiplication

    -

    Given a decomposed scalar and a fixed base , we compute as follows:

    -
      -
    1. For each in the scalar decomposition, witness the - and -coordinates
    2. -
    3. Check that is on the curve: .
    4. -
    5. Witness such that .
    6. -
    7. For all windows but the last, use incomplete addition to sum the 's, resulting in .
    8. -
    9. For the last window, use complete addition and return the final result.
    10. -
    -
    -

    Note: complete addition is required in the final step to correctly map to a representation of the point at infinity, ; and also to handle a corner case for which the last step is a doubling.

    -
    -

    Constraints: -

    -

    where (from the Pallas curve equation).

    -

    Fixed-base scalar multiplication with signed short exponent

    -

    This is used for . We want to compute , where -

    -

    and are each already constrained to bits (by their use as inputs to ).

    -

    Witness the sign and magnitude such that -

    -

    Then compute , and conditionally negate using .

    -

    We compute the window table in a similar way to full-width fixed-base scalar multiplication, -but with only windows:

    -

    -

    In addition to the full-width -bit constraints, we have two additional constraints:

    -

    -

    Fixed-base scalar multiplication using base field element

    -

    We support using a base field element as the scalar in fixed-base multiplication. -This is used in -: here, the scalar is the result of a base field addition.

    -

    Decompose the base field element into three-bit windows using a running sum , where for (This running sum is not to be confused with the array used to check the -coordinate of a fixed-base window.)

    -

    We set , which means: -

    -

    We must range-constrain the difference at each step of the running sum. We also constrain the final output of the running sum to be . -

    -

    We also enforce canonicity of this decomposition. That is, we want to check that where the is Pallas base field modulus Note that

    +

    The scalar multiplication will be computed correctly for representing any integer in the range .

    +

    +

    We range-constrain each -bit word of the scalar decomposition using a polynomial range-check constraint: + +where

    +

    Base field element

    +

    We support using a base field element as the scalar in fixed-base multiplication. This occurs, for example, in the scalar multiplication for the nullifier computation of the Action circuit : here, the scalar is the result of a base field addition.

    +

    Decompose the base field element into three-bit windows, and range-constrain each window, using the short range decomposition gadget in strict mode, with

    +

    If is witnessed directly then no issue of canonicity arises. However, because the scalar is given as a base field element here, care must be taken to ensure a canonical representation, since . That is, we must check that where the is Pallas base field modulus Note that

    To do this, we decompose into three pieces:

    We check the correctness of this decomposition by: @@ -984,8 +919,67 @@ If the MSB

  • Then, we constrain bits of to be zeroes; in other words, we constrain the three-bit word We make use of the running sum decomposition to obtain
  • -

    Define . To check that we use 13 ten-bit lookups, where we constrain the running sum output of the lookup to be if +

    Define . To check that we use 13 ten-bit lookups, where we constrain the running sum output of the lookup to be if

    +

    Short signed scalar

    +

    A short signed scalar is witnessed as a magnitude and sign such that +

    +

    This is used for . We want to compute , where +

    +

    and are each already constrained to bits (by their use as inputs to ).

    +

    Decompose the magnitude into three-bit windows, and range-constrain each window, using the short range decomposition gadget in strict mode, with

    +

    We have two additional constraints: +

    +

    Load fixed base

    +

    Then, we precompute multiples of the fixed base for each window. This takes the form of a window table: such that:

    +
      +
    • for the first (W-1) rows :
    • +
    • in the last row :
    • +
    +

    The additional term lets us avoid adding the point at infinity in the case . We offset these accumulated terms by subtracting them in the final window, i.e. we subtract .

    +
    +

    Note: Although an offset of would naively suffice, it introduces an edge case when . +In this case, the window table entries evaluate to the same point:

    +
      +
    • +
    • +
    +

    In fixed-base scalar multiplication, we sum the multiples of at each window (except the last) using incomplete addition. +Since the point doubling case is not handled by incomplete addition, we avoid it by using an offset of

    +
    +

    For each window of fixed-base multiples :

    +
      +
    • Define a Lagrange interpolation polynomial that maps to the -coordinate of the multiple , i.e. +
    • +
    • Find a value such that is a square in the field, but the wrong-sign -coordinate does not produce a square.
    • +
    +

    Repeating this for all windows, we end up with:

    +
      +
    • an table storing coefficients interpolating the coordinate for each window. Each -coordinate interpolation polynomial will be of the form + +where and 's are the coefficients for each power of ; and
    • +
    • a length- array of 's.
    • +
    +

    We load these precomputed values into fixed columns whenever we do fixed-base scalar multiplication in the circuit.

    +

    Fixed-base scalar multiplication

    +

    Given a decomposed scalar and a fixed base , we compute as follows:

    +
      +
    1. For each in the scalar decomposition, witness the - and -coordinates
    2. +
    3. Check that is on the curve: .
    4. +
    5. Witness such that .
    6. +
    7. For all windows but the last, use incomplete addition to sum the 's, resulting in .
    8. +
    9. For the last window, use complete addition and return the final result.
    10. +
    +
    +

    Note: complete addition is required in the final step to correctly map to a representation of the point at infinity, ; and also to handle a corner case for which the last step is a doubling.

    +
    +

    Constraints: +

    +

    where (from the Pallas curve equation).

    +

    Signed short exponent

    +

    Recall that the signed short exponent is witnessed as a bit magnitude , and a sign Using the above algorithm, we compute . Then, to get the final result we conditionally negate using .

    +

    Constraints: +

    Layout

    Note: this doesn't include the last row that uses complete addition. In the implementation this is allocated in a different region.

    @@ -993,7 +987,7 @@ If the MSB