From b00bb72ab782b6a0132940c05dc622940e608838 Mon Sep 17 00:00:00 2001 From: Christopher Patton Date: Mon, 7 Oct 2024 08:02:14 -0700 Subject: [PATCH] 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 --- draft-irtf-cfrg-vdaf.md | 91 ++++++++++++++++++------------------ poc/vdaf_poc/common.py | 6 +-- poc/vdaf_poc/daf.py | 4 +- poc/vdaf_poc/flp_bbcggi19.py | 4 +- poc/vdaf_poc/idpf.py | 8 ++-- poc/vdaf_poc/vdaf.py | 10 ++-- 6 files changed, 62 insertions(+), 61 deletions(-) diff --git a/draft-irtf-cfrg-vdaf.md b/draft-irtf-cfrg-vdaf.md index 7293ee7d..5dfcf2f7 100644 --- 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 index 56a7e613..2c9362d9 100644 --- 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 index 8c6165a8..104f83db 100644 --- 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 index a6754fa9..ec0b9711 100644 --- 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 index 99ca9075..dc32a2ac 100644 --- 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 index 1b9f5091..51d97582 100644 --- 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