Prefer mathematical notation

* Use `[0, end)` instead of `range(end)` * Use `[start, end)` instead of `range(start,end)` * Use `[start, end]` instead of `range(start,end+1)` * Use `^` to denote exponentiation rather than `**` Co-authored-by: David Cook <[email protected]>
cfrg · Oct 8, 2024 · b00bb72 · b00bb72
1 parent 576762b
commit b00bb72
Show file tree

Hide file tree

Showing 6 changed files with 62 additions and 61 deletions.
diff --git a/draft-irtf-cfrg-vdaf.md b/draft-irtf-cfrg-vdaf.md
@@ -801,11 +801,12 @@ Some common functionalities:
   and `right`. An exception is raised if the inputs are not the same length.
 
 * `to_be_bytes(val: int, length: int) -> bytes` converts `val` to big-endian
-  bytes; its value MUST be at least `0` but less than `2**(8*length)`. Function
-  `from_be_bytes(encoded: bytes) -> int` computes the inverse.
+  bytes; its value MUST be in the range `[0, 2^(8*length))`, i.e., at least `0`
+  but less than `2^(8*length)`. Function `from_be_bytes(encoded: bytes) -> int`
+  computes the inverse.
 
 * `to_le_bytes(val: int, length: int) -> bytes` converts `val` to little-endian
-  bytes; its value MUST be at least `0` but less than `2**(8*length)`. Function
+  bytes; its value MUST be in the range `[0, 2^(8*length))`. Function
   `from_le_bytes(encoded: bytes) -> int` computes the inverse.
 
 * `next_power_of_2(n: int) -> int` returns the smallest integer
@@ -941,7 +942,7 @@ types enumerated in the following table.
 
 | Parameter         | Description                                                    |
 |:------------------|:---------------------------------------------------------------|
-| `ID: int`         | Algorithm identifier for this DAF, in `range(2**32)`.          |
+| `ID: int`         | Algorithm identifier for this DAF, in `[0, 2^32)`.             |
 | `SHARES: int`     | Number of input shares into which each measurement is sharded. |
 | `NONCE_SIZE: int` | Size of the nonce passed by the application.                   |
 | `RAND_SIZE: int`  | Size of the random byte string passed to sharding algorithm.   |
@@ -1033,7 +1034,7 @@ accomplished using the following algorithm:
 
   Pre-conditions:
 
-    * `agg_id` MUST be in `range(SHARES)` and match the index of
+    * `agg_id` MUST be in `[0, SHARES)` and match the index of
       `input_share` in the sequence of input shares produced by the Client.
     * `nonce` MUST have length `NONCE_SIZE`.
 
@@ -1272,7 +1273,7 @@ def domain_separation_tag(self, usage: int, ctx: bytes) -> bytes:
 
     Pre-conditions:
 
-        - `usage` in `range(2**16)`
+        - `usage` in `[0, 2^16)`
     """
     return format_dst(0, self.ID, usage) + ctx
 ~~~
@@ -1389,7 +1390,7 @@ methods:
   Pre-conditions:
 
     * `verify_key` MUST have length `vdaf.VERIFY_KEY_SIZE`.
-    * `agg_id` MUST be the integer in `range(vdaf.SHARES)` that matches the
+    * `agg_id` MUST be the integer in `[0, vdaf.SHARES)` that matches the
       index of `input_share` in the sequence of input shares output by the
       Client.
     * `nonce` MUST have length `vdaf.NONCE_SIZE`.
@@ -2341,9 +2342,9 @@ def format_dst(algo_class: int,
 
     Pre-conditions:
 
-        - `algo_class` in `range(0, 2 ** 8)`
-        - `algo` in `range(0, 2 ** 32)`
-        - `usage` in `range(0, 2 ** 16)`
+        - `algo_class` in `[0, 2^8)`
+        - `algo` in `[0, 2^32)`
+        - `usage` in `[0, 2^16)`
     """
     return concat([
         to_be_bytes(VERSION, 1),
@@ -2550,7 +2551,7 @@ elements:
 For some FLPs, the encoded measurement also includes redundant field elements
 that are useful for checking the proof, but which are not needed after the
 proof has been checked. An example is the "integer sum" data type from
-{{CGB17}} in which an integer in `range(2**k)` is encoded as a vector of `k`
+{{CGB17}} in which an integer in `[0, 2^k)` is encoded as a vector of `k`
 field elements, each representing a bit of the integer (this type is also
 defined in {{prio3sum}}). After consuming this vector, all that is needed is
 the integer it represents. Thus the FLP defines an algorithm for truncating the
@@ -2601,10 +2602,10 @@ of proofs.
 ## Construction {#prio3-construction}
 
 This section specifies `Prio3`, an implementation of the `Vdaf` interface
-({{vdaf}}). It has three generic parameters: an `NttField ({{ntt-field}}), an
-`Flp` ({{flp}}) and a `Xof` ({{xof}}). It also has an associated constant,
-`PROOFS`, with a value in `range(1, 256)`, denoting the number of FLPs
-generated by the Client ({{multiproofs}}).
+({{vdaf}}). It has three generic parameters: an `NttField`
+({field-ntt-friendly}}), an `Flp` ({{flp}}) and a `Xof` ({{xof}}). It also has
+an associated constant, `PROOFS`, with a value in the range `[1, 256)`,
+denoting the number of FLPs generated by the Client ({{multiproofs}}).
 
 The associated constants and types required by the `Vdaf` interface are
 defined in {{prio3-param}}. The methods required for sharding,
@@ -3346,7 +3347,7 @@ C(x) = x * (x-1)
 ~~~
 
 This circuit contains one subtraction gate (`x-1`) and one multiplication gate
-(`x * (x-1)`). Observe that `C(x) = 0` if and only if `x` is in `range(2)`.
+(`x * (x-1)`). Observe that `C(x) = 0` if and only if `x` is in `[0, 2)`.
 
 The goal of the proof system is to allow each Aggregator to privately and
 correctly compute a secret share of `C(x)` from its secret share of `x`. This
@@ -3433,8 +3434,8 @@ C(x, r) = r * Range2(x[0]) + ... + r^N * Range2(x[N-1])
 the length-`N` input and `r` is a random field element. The gadget circuit
 `Range2` is the "range-check" polynomial described above, i.e., `Range2(x) =
 x^2 - x`. The idea is that, if `x` is valid (i.e., each `x[j]` is in
-`range(2)`), then the circuit will evaluate to zero regardless of the value of
-`r`; but if some `x[j]` is not in `range(2)`, then the output will be non-zero
+`[0, 2)`), then the circuit will evaluate to zero regardless of the value of
+`r`; but if some `x[j]` is not in `[0, 2)`, then the output will be non-zero
 with high probability.
 
 The second extension implemented by our FLP allows the validity circuit to
@@ -3449,9 +3450,9 @@ C(x, r) = r * Range2(x[0]) + ... + r^L * Range2(x[L-1]) + \
 ~~~
 
 where `Range3(x) = x^3 - 3x^2 + 2x`. This circuit checks that the first `L`
-inputs are in `range(2)` and the last `N-L` inputs are in `range(3)`. The
-same circuit can be expressed using a simpler gadget, namely multiplication,
-but the resulting proof would be longer.
+inputs are in `[0, 2)` and the last `N-L` inputs are in `[0, 3)`. The same
+circuit can be expressed using a simpler gadget, namely multiplication, but the
+resulting proof would be longer.
 
 Third, rather than interpolate the gadget polynomial at inputs `1`, `2`, ...,
 `j`, ..., where `j` is the `j`-th invocation of the gadget, we use powers of
@@ -3853,7 +3854,7 @@ way. The parameters for this circuit are summarized below.
 | `OUTPUT_LEN`      | `1`                    |
 | `JOINT_RAND_LEN`  | `0`                    |
 | `EVAL_OUTPUT_LEN` | `1`                    |
-| `Measurement`     | `int` in `range(2)`    |
+| `Measurement`     | `int` in `[0, 2)`      |
 | `AggResult`       | `int`                  |
 {: title="Parameters of validity circuit Count."}
 
@@ -3868,8 +3869,8 @@ way. The parameters for this circuit are summarized below.
 {: title="Parameters for Prio3Sum."}
 
 The next instance of Prio3 supports summing of integers in a pre-determined
-range. Each measurement is an integer in `range(max_measurement+1)`, where
-`max_measurement` is an associated parameter equal to the largest valid
+range. Each measurement is an integer in the range `[0, max_measurement]`,
+where `max_measurement` is an associated parameter equal to the largest valid
 measurement.
 
 The range check is accomplished by encoding the measurement as a bit vector,
@@ -3879,20 +3880,20 @@ two encoded integers are consistent. Let
 * `bits = max_measurement.bit_length()`, the number of bits needed to encode
   the largest valid measurement
 
-* `offset = 2**bits - 1 - max_measurement`
+* `offset = 2^bits - 1 - max_measurement`
 
 The first bit-encoded integer is the measurement itself. Note that only
-measurements between `0` and `2**bits - 1` can be encoded this way with
-`bits` bits. The second bit-encoded integer is the sum of the measurement and
-`offset`. Observe that this sum can only be encoded this way if it is between `0`
-and `2**bits - 1`, which implies that the measurement is between `-offset` and
-`max_measurement`.
+measurements between `0` and `2^bits - 1` can be encoded this way with `bits`
+bits. The second bit-encoded integer is the sum of the measurement and
+`offset`. Observe that this sum can only be encoded this way if it is between
+`0` and `2^bits - 1`, which implies that the measurement is between `-offset`
+and `max_measurement`.
 
 The circuit, denoted `Sum`, first checks that each entry of both bit vectors is
 a one or a zero. It then decodes both the measurement and the offset
 measurement, and subtracts `offset` from the latter. It then checks if these
 two values are equal. Since both the measurement and the measurement plus
-`offset` are in the same range of `range(2**bits)`, this means that the
+`offset` are in the same range of `[0, 2^bits)`, this means that the
 measurement itself is between `0` and `max_measurement`.
 
 The measurement is encoded in `2*bits` field elements as follows:
@@ -3955,7 +3956,7 @@ def eval(
 | `OUTPUT_LEN`      | `1`                                 |
 | `JOINT_RAND_LEN`  | `0`                                 |
 | `EVAL_OUTPUT_LEN` | `2*bits + 1`                        |
-| `Measurement`     | `int` in `range(max_measurement+1)` |
+| `Measurement`     | `int` in `[0, max_measurement]`     |
 | `AggResult`       | `int`                               |
 {: title="Parameters of validity circuit Sum."}
 
@@ -3972,7 +3973,7 @@ def eval(
 This instance of Prio3 supports summing a vector of integers. It has three
 parameters, `length`, `bits`, and `chunk_length`. Each measurement is a vector
 of positive integers with length equal to the `length` parameter. Each element
-of the measurement is an integer in the `range(2**bits)`. It is RECOMMENDED
+of the measurement is an integer in the range `[0, 2^bits)`. It is RECOMMENDED
 to set `chunk_length` to an integer near the square root of `length * bits`
 (see {{parallel-sum-chunk-length}}).
 
@@ -4093,7 +4094,7 @@ def eval(
 | `OUTPUT_LEN`      | `length`                                               |
 | `JOINT_RAND_LEN`  | `GADGET_CALLS[0]`                                      |
 | `EVAL_OUTPUT_LEN` | `1`                                                    |
-| `Measurement`     | `list[int]`, each element in `range(2**bits)`          |
+| `Measurement`     | `list[int]`, each element in `[0, 2^bits)`             |
 | `AggResult`       | `list[int]`                                            |
 {: title="Parameters of validity circuit SumVec."}
 
@@ -4249,7 +4250,7 @@ maximum number of non-zero entries (i.e., the weight must be at most
 Validation works as follows. Let
 
 * `bits_for_weight = max_weight.bit_length()`
-* `offset = 2**bits_for_weight - 1 - max_weight`
+* `offset = 2^bits_for_weight - 1 - max_weight`
 
 The Client reports the weight of the count vector by adding `offset` to it and
 bit-encoding the result. Observe that only a weight of at most `max_weight` can
@@ -4418,7 +4419,7 @@ An IDPF is defined over a domain of size `2^BITS`, where `BITS` is a constant.
 Indices into the IDPF tree are bit strings. (In Poplar1, each Client's bit
 string is an index; see {{poplar1-idpf-index-encoding}} for details.) The Client
 specifies an index `alpha` and a vector of values `beta`, one for each "level"
-`L` in `range(BITS)`. The key generation algorithm generates one IDPF "key" for
+`L` in `[0, BITS)`. The key generation algorithm generates one IDPF "key" for
 each Aggregator. When evaluated at level `L` and index `prefix`, each IDPF key
 returns an additive share of `beta[L]` if `prefix` is the `L`-bit prefix of
 `alpha` and shares of zero otherwise.
@@ -4452,7 +4453,7 @@ elements.) The scheme is comprised of the following algorithms:
     * `alpha` MUST have length `BITS`.
     * `beta_inner` MUST have length `BITS - 1`.
     * `beta_inner[level]` MUST have length `VALUE_LEN` for each `level` in
-       `range(BITS - 1)`.
+       `[0, BITS - 1)`.
     * `beta_leaf` MUST have length `VALUE_LEN`.
     * `rand` MUST be generated by a CSPRNG and have length `RAND_SIZE`.
     * `nonce` MUST be of length `Idpf.NONCE_SIZE` and chosen uniformly at
@@ -4474,9 +4475,9 @@ elements.) The scheme is comprised of the following algorithms:
 
   Pre-conditions:
 
-  * `agg_id` MUST be in `range(SHARES)` and match the index of `key` in
+  * `agg_id` MUST be in `[0, SHARES)` and match the index of `key` in
     the sequence of IDPF keys output by the Client.
-  * `level` MUST be in `range(0, BITS)`.
+  * `level` MUST be in `[0, BITS)`.
   * Each `prefix` in `prefixes` MUST be distinct and have length `level + 1`.
 
 In addition, the following method is derived for each concrete `Idpf`:
@@ -5811,7 +5812,7 @@ are generated and verified. In general the soundness error of the FLP is given
 by the following formula:
 
 ~~~
-(circuit_soundness + flp_soundness) ** PROOFS
+(circuit_soundness + flp_soundness)^PROOFS
 ~~~
 
 where:
@@ -6103,8 +6104,8 @@ VDAF. These are listed in the subsections below.
  : The number of shares, an integer.
 
 `max_measurement`:
- : The largest measurement, an integer. Each element is in range
-   `range(max_measurement+1)`.
+ : The largest measurement, an integer. Each element is in the range
+  `[0, max_measurement]`.
 
 ### Prio3SumVec
 
@@ -6118,8 +6119,8 @@ VDAF. These are listed in the subsections below.
 : the length of each vector chunk, an integer.
 
 `bits`:
-: the bit length of each element of the vector, an integer. each element is in
-  `range(2 ** bits)`.
+: the bit length of each element of the vector, an integer. Each element is in
+  `[0, 2^bits)`.
 
 ### Prio3Histogram
 
@@ -6145,7 +6146,7 @@ VDAF. These are listed in the subsections below.
 
 `max_weight`:
 : The largest vector weight, an integer. The sum of the elements must be in
-  `range(max_weight+1)`.
+  `[0, max_weight]`.
 
 ### Poplar1 {#poplar1-test-vec-param}
 

diff --git a/poc/vdaf_poc/common.py b/poc/vdaf_poc/common.py
@@ -150,9 +150,9 @@ def format_dst(algo_class: int,
 
     Pre-conditions:
 
-        - `algo_class` in `range(0, 2 ** 8)`
-        - `algo` in `range(0, 2 ** 32)`
-        - `usage` in `range(0, 2 ** 16)`
+        - `algo_class` in `[0, 2^8)`
+        - `algo` in `[0, 2^32)`
+        - `usage` in `[0, 2^16)`
     """
     return concat([
         to_be_bytes(VERSION, 1),

diff --git a/poc/vdaf_poc/daf.py b/poc/vdaf_poc/daf.py
@@ -99,8 +99,8 @@ def prep(
 
         Pre-conditions:
 
-            - `agg_id in range(0, Daf.SHARES)`
-            - `len(nonce) == Daf.NONCE_SIZE`
+            - `agg_id` in `[0, daf.SHARES)`
+            - `len(nonce) == daf.NONCE_SIZE`
         """
         pass
 

diff --git a/poc/vdaf_poc/flp_bbcggi19.py b/poc/vdaf_poc/flp_bbcggi19.py
@@ -1073,8 +1073,8 @@ class Sum(
 
     def __init__(self, field: type[F], max_measurement: int):
         """
-        A circuit that checks that the measurement is in
-        `range(max_measurement+1)`. This is accomplished by encoding the
+        A circuit that checks that the measurement is in range `[0,
+        max_measurement]`. This is accomplished by encoding the
         measurement as a bit vector, encoding the measurement plus an
         offset as a bit vector, then checking that the two encoded
         integers are consistent.

diff --git a/poc/vdaf_poc/idpf.py b/poc/vdaf_poc/idpf.py
@@ -88,7 +88,7 @@ def gen(self,
             - `len(alpha) == self.BITS`
             - `len(beta_inner) == self.BITS - 1`
             - `len(beta_inner[level]) == self.VALUE_LEN` for each `level` in
-              `range(self.BITS - 1)`
+              `[0, self.BITS - 1)`
             - `len(beta_leaf) == self.VALUE_LEN`
             - `len(rand) == self.RAND_SIZE`
         """
@@ -121,8 +121,8 @@ def eval(self,
 
         Pre-conditions:
 
-            - `agg_id` in `range(self.SHARES)`
-            - `level` in `range(self.BITS)`
+            - `agg_id` in `[0, self.SHARES)`
+            - `level` in `[0, self.BITS)`
             - `len(prefix) == level + 1` for each `prefix` in `prefixes`
         """
         pass
@@ -144,7 +144,7 @@ def is_prefix(self, x: tuple[bool, ...], y: tuple[bool, ...], level: int) -> boo
 
         Pre-conditions:
 
-            - `level` in `range(self.BITS)`
+            - `level` in `[0, self.BITS)`
         """
         return x == y[:level + 1]
 

diff --git a/poc/vdaf_poc/vdaf.py b/poc/vdaf_poc/vdaf.py
@@ -45,7 +45,7 @@ class Vdaf(
     """
 
     # Algorithm identifier for this VDAF, a 32-bit integer.
-    ID: int  # `range(2**32)`
+    ID: int  # `[0, 2^32)`
 
     # Length of the verification key shared by the Aggregators.
     VERIFY_KEY_SIZE: int
@@ -111,9 +111,9 @@ def prep_init(self,
 
         Pre-conditions:
 
-            - `len(verify_key) == Vdaf.VERIFY_KEY_SIZE`
-            - `agg_id` in `range(0, Vdaf.SHARES)`
-            - `len(nonce) == Vdaf.NONCE_SIZE`
+            - `len(verify_key) == vdaf.VERIFY_KEY_SIZE`
+            - `agg_id` in `[0, vdaf.SHARES)`
+            - `len(nonce) == vdaf.NONCE_SIZE`
         """
         pass
 
@@ -179,7 +179,7 @@ def domain_separation_tag(self, usage: int, ctx: bytes) -> bytes:
 
         Pre-conditions:
 
-            - `usage` in `range(2**16)`
+            - `usage` in `[0, 2^16)`
         """
         return format_dst(0, self.ID, usage) + ctx