Audit of Penumbra's Circuits
July 28th, 2023

Description. Nullifier sets are global pools managed by each validator in order to ensure that no note is being spent more than once. Since delegator votes reveal nullifiers, but do not intend on spending them, delegator vote nullifiers are managed in separate per-proposal pools (as per the specification).

In addition to keeping track of nullifiers globally and checking nullifier-based actions against these global nullifier sets, validators must also check that within a transaction itself no nullifier is being used more than once. This is because transactions can contain multiple actions.

You can see this check in the ActionHandler::check_stateless implementation for a Transaction:

impl ActionHandler for Transaction {
    async fn check_stateless(&self, _context: ()) -> Result<()> {
        // TRUNCATED...

        no_duplicate_nullifiers(self)?;

This check only checks nullifiers released by spend and swap claim actions, which makes sense as delegator vote nullifiers must be checked separately.

Unfortunately no check seems to exist for checking duplicate delegator vote nullifiers within the same transactions, allowing users to vote multiple times with the same (then-)delegated notes as long as they do it within the same transaction.

Recommendations. Add a similar check as the no_duplicate_nullifiers check but for the delegator vote nullifiers.

In addition, add a negative test to ensure that voting twice using the same delegated note within the same transaction is not possible.

Client Response. The issue was fixed by adding the following function to the ActionHandler logic of the Transaction type, in order to check for duplicate delegator vote nullifiers:

fn no_duplicate_votes(tx: &Transaction) -> Result<()> {
    // Disallow multiple `DelegatorVotes`s with the same proposal and the same `Nullifier`.
    let mut nullifiers_by_proposal_id = BTreeMap::new();
    for vote in tx.delegator_votes() {
        // Get existing entries
        let nullifiers_for_proposal = nullifiers_by_proposal_id
            .entry(vote.body.proposal)
            .or_insert(BTreeSet::default());

        // If there was a duplicate nullifier for this proposal, this call will return `false`:
        let not_duplicate = nullifiers_for_proposal.insert(vote.body.nullifier);
        if !not_duplicate {
            return Err(anyhow::anyhow!(
                "Duplicate nullifier in transaction: {}",
                &vote.body.nullifier
            ));
        }
    }

    Ok(())
}

Notice that the set is per-proposal, in order to allow duplicate nullifiers when voting for different proposals that are happening at the same time.

Description. In shielded transactions, a spend action allows one to spend one of their committed notes, as long as it hasn't been spent before. Since the spending of a note is hidden via zero-knowledge proofs, it cannot be known whether a note was spent or not by just looking at the notes themselves. For this reason, Penumbra introduces the concept of "nullifiers", which can be released in the clear as part of spending a note, and prevent reuse of notes as they are strongly tied to the notes themselves (without leaking to which note they are tied to).

In order to produce a nullifier, users possess nullifier keys nks, which they can use with a note commitment in order to deterministically derive a nullifier.

In order to prove that a user can spend a note, they must prove that they own an incoming viewing key ivk which is strongly tied with the note to be spent.

What ties a nullifier to a note, is that the nullifier key nk and the incoming viewing key ivk are also strongly tied: the ivk is derived from the nk.

During the derivation of the ivk, the logic must convert a value from the circuit field (Fq) to a non-native field (Fr). This is because the ivk is a scalar value that is eventually used to perform a scalar multiplication. The problem arises in the implementation, which takes the value out of circuit to convert it to the other field:

impl IncomingViewingKeyVar {
    pub fn derive(nk: &NullifierKeyVar, ak: &AuthorizationKeyVar) -> Result<Self, SynthesisError> {
        // TRUNCATED...        
        let inner_ivk_mod_q: Fq = ivk_mod_q.value().unwrap_or_default();
        let ivk_mod_r = Fr::from_le_bytes_mod_order(&inner_ivk_mod_q.to_bytes());
        let ivk = NonNativeFieldVar::<Fr, Fq>::new_variable(
            cs,
            || Ok(ivk_mod_r),
            AllocationMode::Witness,
        )?;

In the above snippet, the circuit value of ivk_mod_q is extracted out of circuit, and then reinserted as a witness value under ivk. The problem is that doing that removes any constraint on ivk to the previous circuit value ivk_mod_q.

At this point, a malicious prover can decide to set anything as the output ivk of the derivation function. This is not very useful, as they must use a correct ivk later on to prove that they can spend the note.

This is not the end of it, a malicious prover can also go backward and decide not to derive the correct ivk_mod_q (but to use the correct ivk as the output of the function still). In this case, it allows the malicious prover to use an arbitrary nullifier key nk, and thus produce an incorrect nullifier.

This means that they can double spend (or spend as many times as they want) notes they own, simply by choosing a different nullifier every time.

Reproduction steps. The issue can be reproduced by modifying the test spend_proof_verification_success in crates/core/component/shielded-pool/src/spend/proof.rs to use a different nullifier key (and thus produce a different nullifier) based on the value of an environment variable:

        let note = Note::generate(&mut rng, &sender, value_to_send);
        let note_commitment = note.commit();
        let rsk = sk_sender.spend_auth_key().randomize(&spend_auth_randomizer);
        let mut nk = *sk_sender.nullifier_key();
+        if let Ok(s) = std::env::var("ZKSEC") {
+            let shift = Fq::from_str(&s).unwrap();
+            nk.0 += shift;
+        }

In order to derive the correct ivk, the crates/core/keys/src/keys/ivk.rs file needs to be modified as well to correct the nk when an attack is being performed:

pub fn derive(nk: &NullifierKeyVar, ak: &AuthorizationKeyVar) -> Result<Self, SynthesisError> {
        let cs = nk.inner.cs();
        let ivk_domain_sep = FqVar::new_constant(cs.clone(), *IVK_DOMAIN_SEP)?;
        let ivk_mod_q = poseidon377::r1cs::hash_2(
            cs.clone(),
            &ivk_domain_sep,
            (nk.inner.clone(), ak.inner.compress_to_field()?),
        )?;

        // Reduce `ivk_mod_q` modulo r
+        let inner_ivk_mod_q = match (std::env::var("ZKSEC"), cs.is_in_setup_mode()) {
+            (Ok(shift), false) => {
+                let shift = Fq::from_str(&shift).unwrap();
+                let real_nk = nk.inner.value().unwrap() - shift;
+                let ak: Element = ak.inner.value().unwrap();
+                let compressed_ak = ak.vartime_compress_to_field();
+                poseidon377::hash_2(
+                    &IVK_DOMAIN_SEP,
+                    (real_nk, compressed_ak),
+                )
+            }
+            _ => ivk_mod_q.value().unwrap_or_default()
+        };
+        let ivk_mod_r =
+            Fr::from_le_bytes_mod_order(&inner_ivk_mod_q.to_bytes());

You can then run the test using a shift of 1, for example:

$ ZKSEC=1 cargo test --color=always --lib spend::proof::tests::zksec_double_spend -- --nocapture

Recommendation. Add a constraint that verifies that the ivk value is a valid encoding (in Fr) of the previous ivk_mod_q value.

Client Response. Penumbra fixed the issue by computing the reduced value res out of circuit and proving that it correctly satisfies ivk_mod_q = quotient * r_modulus + res modulo the circuit field Fq (with quotient <= 4). This works because the modulus of the scalar field Fr is smaller than the circuit field Fq.

Fixed-point arithmetic

Description. Parts of Penumbra's logic relies on a U128x128Var type and associated subcircuits. The type implements checked_add, to add two 256-bit values without allowing overflow. The function is underconstrained, producing the wrong results in some cases.

Under the hood, a U128x128Var stores its value as 4 limbs of UInt64s, an Arkworks type which internally simply contains vectors of boolean circuit variables.

The checked_add function first converts the limbs to field values, then adds them pairwise, tracking the carry for each limb. In addition, it enforces that the most significant carry is zero, to prevent overflow. The carry is tracked since addition of two 64-bit values can produce a 65-bit value, which is then split into a 64-bit value and a carry bit (e.g. 0b11 + 0b11 = 0b110).

The following code shows the issue at play:

pub struct U128x128Var {
    pub limbs: [UInt64<Fq>; 4],
}

// TRUNCATED...

impl U128x128Var {
    pub fn checked_add(self, rhs: &Self) -> Result<U128x128Var, SynthesisError> {
        // x = [x0, x1, x2, x3]
        // x = x0 + x1 * 2^64 + x2 * 2^128 + x3 * 2^192
        // y = [y0, y1, y2, y3]
        // y = y0 + y1 * 2^64 + y2 * 2^128 + y3 * 2^192
        let x0 = Boolean::<Fq>::le_bits_to_fp_var(&self.limbs[0].to_bits_le())?;
        let x1 = Boolean::<Fq>::le_bits_to_fp_var(&self.limbs[1].to_bits_le())?;
        let x2 = Boolean::<Fq>::le_bits_to_fp_var(&self.limbs[2].to_bits_le())?;
        let x3 = Boolean::<Fq>::le_bits_to_fp_var(&self.limbs[3].to_bits_le())?;

        let y0 = Boolean::<Fq>::le_bits_to_fp_var(&rhs.limbs[0].to_bits_le())?;
        let y1 = Boolean::<Fq>::le_bits_to_fp_var(&rhs.limbs[1].to_bits_le())?;
        let y2 = Boolean::<Fq>::le_bits_to_fp_var(&rhs.limbs[2].to_bits_le())?;
        let y3 = Boolean::<Fq>::le_bits_to_fp_var(&rhs.limbs[3].to_bits_le())?;

        // z = x + y
        // z = [z0, z1, z2, z3]
        let z0_raw = &x0 + &y0; // 65-bit potentially
        let z1_raw = &x1 + &y1; // 65-bit potentially
        let z2_raw = &x2 + &y2; // 65-bit potentially
        let z3_raw = &x3 + &y3; // must be 64-bit, otherwise there is an overflow

        // z0 < 2^64 + 2^64 < 2^(65) => 65 bits
        let z0_bits = bit_constrain(z0_raw, 64)?; // no carry-in
        let z0 = UInt64::from_bits_le(&z0_bits[0..64]);
        let c1 = Boolean::<Fq>::le_bits_to_fp_var(&z0_bits[64..].to_bits_le()?)?;

        // z1 < 2^64 + 2^64 + 2^64 < 2^(66) => 66 bits
        let z1_bits = bit_constrain(z1_raw + c1, 66)?; // carry-in c1

The problem here comes from the wrong assumption on the contract of the bit_constrain function: the bit_constrain function returns an array of the size of its second argument (64), but the code assumes that the rest of the bits will trail the output of the function (if it was the case, the bit_constrain function would actually "throw", as it not only produces bit constraints for n bits of the given input, but also recombine them to enforce that they fully describe the given input).

So in practice, z0_bits[64..].to_bits_le() will return the empty vec in this code. Meaning that the carry c1 will always be zero during proving.

Reproduction steps. Running a test with u64::MAX as the two inputs will produce a z0 of size 64, and a c1 of size 0, and the test will fail (since the test additionally enforces the result). One can do this by modifying the tests in crates/core/num/src/fixpoint.rs to use the specific a and b values as follows:

let (lo, hi) = (u64::MAX, 0);
let a = U128x128(U256::from_words(hi, lo));
let b = U128x128(U256::from_words(hi, lo));

Note that the current proptests did not surface this issue because they do not generate U128x128 values in the full range of possibilities (they always set the low 128 bits to 0, and the high 128 bits are sampled from $[0, 2^{64})$).

Recommendations. Fix the property tests to generate values in the full range of possibilities, and fix the current logic in order to correctly enforce the carry.

Client Response. Penumbra released a fix that correctly computes each limb in the circuit.

Description. A similar error as with the Unsound fixed-point addition finding is present in the fixed-point multiplication U128x128Var::checked_mul. To see why the computation is erroneous, let's first see what the computation is trying to achieve.

Fixed-point multiplications handle scaled values $ax$ and $ay$ for some scalar $a$. Multiplying them directly gives out a result $(ax)(ay) = a(axy)$ that needs to be unscaled; we want $a(xy)$.

For $a = 2^{128}$, which is what Penumbra uses, we need to multiply by $2^{-128}$ and truncate any decimals.

Since U128x128Var handles values chunked in limbs of size 64-bit, we have the following values computed on the limbs of the operands $x$ and $y$:

• $z_0 = x_0 \cdot y_0$
• $z_1 = x_0 \cdot y_1 + x_1 \cdot y_0$
• $z_2 = x_0 \cdot y_2 + x_1 \cdot y_1 + x_2 \cdot y_0$
• $z_3 = x_0 \cdot y_3 + x_1 \cdot y_2 + x_2 \cdot y_1 + x_3 \cdot y_0$
• $z_4 = x_1 \cdot y_3 + x_2 \cdot y_2 + x_3 \cdot y_1$
• $z_5 = x_2 \cdot y_3 + x_3 \cdot y_2$
• $z_6 = x_3 \cdot y_3$

where

Since we need to divide by $2^{128}$, we need to compute $z \cdot 2^{-128}$:

and obtain $w = w_0 + w_1 \cdot 2^{64} + w_2 \cdot 2^{128} + w_3 \cdot 2^{192}$ such that:

• $w_0 = z_2 + c_0$
• $w_1 = z_3 + c_1$
• $w_2 = z_4 + c_2$
• $w_3 = z_5 + c_3$

Where the $c_i$ are the carries. For example, $c_0$ is essentially the bits left after truncating the first 128 bits of $z_0 + z_1 \cdot 2^{64}$. Note that $z_0 = x_0 * y_0$ is going to be of 128 bits, and thus you can discard it entirely. So $c_0 = bits(z_1)[64..]$

(In addition we want to check that $z_6 = 0$ because we do not allow overflow.)

We can see that the implementation is computing a wrong $w_0$ right at the start, as it does not use $z_2$:

pub fn checked_mul(self, rhs: &Self) -> Result<U128x128Var, SynthesisError> {
        // TRUNCATED...

        let z0 = &x0 * &y0;
        let z1 = &x0 * &y1 + &x1 * &y0;
        let z2 = &x0 * &y2 + &x1 * &y1 + &x2 * &y0;

        // TRUNCATED...

        let t0 = z0 + z1 * Fq::from(1u128 << 64);
        let t0_bits = bit_constrain(t0.clone(), 193)?;
        let t1 = z2 + Boolean::<Fq>::le_bits_to_fp_var(&t0_bits[128..193].to_bits_le()?)?;
        let t1_bits = bit_constrain(t1, 129)?;

        let w0 = UInt64::from_bits_le(&t0_bits[0..64]);

Reproduction steps. One can produce an erroring test by modifying the tests in crates/core/num/src/fixpoint.rs to use the specific a and b values as follows

let (hi, lo) = (0, 1);
        let a = U128x128(U256::from_words(hi, lo));
        let b = U128x128(U256::from_words(hi, lo));

Recommendations. As with the Unsound fixed-point addition finding, fix the property tests to use the full domain of possible U128x128 values. In addition, ensure that the limbs of the result are computed correctly according to the description of this finding.

Client Response. Penumbra fixed the issue by correctly constraining the limbs.

Description. The AmountVar type is used to represent amounts of tokens in all of Penumbra's circuits. Different operations can be performed on AmountVar types, including divisions via the AmountVar::quo_rem function. The gadget is currently underconstrained, allowing malicious provers to arbitrary choose the remainder part of the division. The reason why is that the quotient quo_var is not constrained at all:

pub fn quo_rem(
    &self,
    divisor_var: &AmountVar,
) -> Result<(AmountVar, AmountVar), SynthesisError> {
    let current_amount_bytes: [u8; 16] = self.amount.value().unwrap_or_default().to_bytes()
        [0..16]
        .try_into()
        .expect("amounts should fit in 16 bytes");
    let current_amount = u128::from_le_bytes(current_amount_bytes);
    let divisor_bytes: [u8; 16] = divisor_var.amount.value().unwrap_or_default().to_bytes()
        [0..16]
        .try_into()
        .expect("amounts should fit in 16 bytes");
    let divisor = u128::from_le_bytes(divisor_bytes);

    // Out of circuit
    let quo = current_amount.checked_div(divisor).unwrap_or(0);
    let rem = current_amount.checked_rem(divisor).unwrap_or(0);

    // Add corresponding in-circuit variables
    let quo_var = AmountVar {
        amount: FqVar::new_witness(self.cs(), || Ok(Fq::from(quo)))?,
    };

Notice that if the quotient $q$ is not constrained in a division $x = qy + r$ in the field, then you can set the remainder $r$ arbitrarily and compute the quotient as $q = (x - r)y^{-1}$.

Using sage, we can show that:

F = GF(8444461749428370424248824938781546531375899335154063827935233455917409239041)
F(7) == F(3 * 2 + 1) # True
F(7) == F(3 * 2 + 2) # False
new_q = F(7 - 2) / F(3)
F(7) == F(3 * new_q + 2) # True

Note that exploitation of the flawed gadget seems limited in practice, due to additional checks on the callers' sides. There's currently only one call site to AmountVar::quo_rem in the codebase, which is in PenaltyVar::apply_to, and which does not appear to make use of the resulting remainder (only the quotient).

Recommendations. Both $q$ and $d$ cannot be larger than 64 bits since $x$ is constrained to 128 bits. Thus, constraining that $q$ is 128-bit, and that either $q$ or $d$ is 64-bit, is enough to ensure that there are no overflows.

Client Response. Penumbra implemented the fix by constraining the quotient $q$ to 128-bits, and adding an extra constraint ensureing that either $q$ or $d$ has a size of 64 bits.

The arkworks R1CS library works by mixing compile-time (setup) with runtime (proving) logic. That is, users of the library must write code that will handle both pathways.

To do this, a user must first declare a structure associated with the circuit, and then write its circuit by implementing the ConstraintSynthesizer trait. For example, the proof associated with proving Merkle tree membership is defined with the following struct and trait implementation:

struct MerkleProofCircuit {
    state_commitment_proof: tct::Proof,
    pub anchor: tct::Root,
    pub epoch: Fq,
    pub block: Fq,
    pub commitment_index: Fq,
}

impl ConstraintSynthesizer<Fq> for MerkleProofCircuit {
    fn generate_constraints(
        self,
        cs: ConstraintSystemRef<Fq>,
    ) -> ark_relations::r1cs::Result<()> {
        // TRUNCATED...
    }
}

The struct can mix both compile-time values as well as runtime values. It would be much clearer if runtime values were encapsulated in Option types. This way, you wouldn't need to give them any value when compiling the circuit, and you would be forced to give them a non-default value when proving (as runtime code would need to unwrap these values).

Furthermore, logic in the circuit is also mixed between compile-time and runtime. For example, in the U128x128Var::checked_div function some values are computed out of circuit and then witnessed and constrained in the circuit:

let xbar_ooc = self.value().unwrap_or_default();
let ybar_ooc = rhs.value().unwrap_or(U128x128::from(1u64));
let Ok((quo_ooc, rem_ooc)) = stub_div_rem_u384_by_u256(xbar_ooc.0, ybar_ooc.0) else {
    return Err(SynthesisError::Unsatisfiable);
};

// TRUNCATED...

let q = U128x128Var::new_witness(cs.clone(), || Ok(U128x128(quo_ooc)))?;

Mixing out-of-circuit code with in-circuit code is error-prone, as was shown in Double spending due to incoming viewing key (ivk) derivation not constrained. While this pattern is inevitable, due to the nature of the library, it could be made safer by using Option types and by making the code more explicit.

That is, no default values should be used, and instead out-of-circuit code should happen in a monadic way as much as possible (using Options).

So, for example, the previous code could be rewritten as:

let (quo_val, rem_val) = (!cs.in_setup_mode())
    .then(|| {
        let x_bar = self.value().unwrap();
        let y_bar = rhs.value().unwrap();
        stub_div_rem_u384_by_u256(x_bar.0, y_bar.0)
            .map_err(|_| SynthesisError::Unsatisfiable)?
    )
    .unzip();
};

// TRUNCATED...

let q = U128x128Var::new_witness(cs.clone(), || Ok(U128x128(quo_val.unwrap())))?;

or even more concisely by using the closure passed to new_witness:

let q = U128x128Var::new_witness(cs.clone(), || {
    let x_bar = self.value().unwrap();
    let y_bar = rhs.value().unwrap();
    let (q_bar, r_bar) = stub_div_rem_u384_by_u256(x_bar.0, y_bar.0)
        .map_err(|_| SynthesisError::Unsatisfiable)?;
    Ok(q_bar)
})?;

In addition, new circuit values are allocated using the arkworks function AllocVar::new_variable. As such, custom user types must implement this function themselves. Its signature takes a closure f, which is supposed to contain a recipe on how to compute the witness value associated with the circuit variable at runtime.

pub trait AllocVar<V, F: Field>
where
    Self: Sized,
    V: ?Sized,
{
    fn new_variable<T: Borrow<V>>(
        cs: impl Into<Namespace<F>>,
        f: impl FnOnce() -> Result<T, SynthesisError>,
        mode: AllocationMode,
    ) -> Result<Self, SynthesisError>;

In many custom implementations of AllocVar::new_variable, it was observed that the closure f was called/executed even when running the setup phase (not just during witness generation/proving). This is an ill pattern as the closure can contain logic that is not supposed to be executed in setup mode. See the previous refactoring recommendation for an example.

For example, in the following code, the closure f is executed even in setup mode:

impl AllocVar<Note, Fq> for NoteVar {
    fn new_variable<T: std::borrow::Borrow<Note>>(
        cs: impl Into<ark_relations::r1cs::Namespace<Fq>>,
        f: impl FnOnce() -> Result<T, SynthesisError>,
        mode: ark_r1cs_std::prelude::AllocationMode,
    ) -> Result<Self, SynthesisError> {
        let ns = cs.into();
        let cs = ns.cs();
        let note1 = f()?; // <---- executed even in setup mode!
        let note: &Note = note1.borrow();
        let note_blinding =
            FqVar::new_variable(cs.clone(), || Ok(note.note_blinding().clone()), mode)?;

Description. In crates/core/asset/src/balance.rs, the BalanceVar::commit gadget conditionally computes a commitment to the balance, depending on the sign of the amount. The code is as follows:

// We scalar mul first with value (small), then negate [v]G_v if needed
let commitment_plus_contribution =
    commitment.clone() + G_v.scalar_mul_le(value_amount.to_bits_le()?.iter())?;
let commitment_minus_contribution =
    commitment - G_v.scalar_mul_le(value_amount.to_bits_le()?.iter())?;
commitment = ElementVar::conditionally_select(
    sign,
    &commitment_plus_contribution,
    &commitment_minus_contribution,
)?;

Here to_bits_le is called twice, which is going to increase the size of the witness twice instead of once. Not only calling it once should improve the number of constraints, but the second scalar multiplication should be avoidable altogether by computing $P = [v]G$ and then the negated point directly as $-P$.

Description. Gadgets are used in different places, sort of like subcircuits, to abstract parts of the logic. When gadgets return an output value, the value is automatically being allocated in the witness. It is thus redundant to reallocate it on the caller side and enforce that the two values match.

This pattern has been seen several times in the codebase, and increase the size of the circuit for no clear benefits. For example, in crates/core/component/stake/src/penalty.rs the result of the call to AmountVar::quo_rem is constrained to be equal to a free witness variable penalized_amount_var.

impl PenaltyVar {
    pub fn apply_to(&self, amount: AmountVar) -> Result<AmountVar, SynthesisError> {
        // TRUNCATED...

        // Out of circuit penalized amount computation:
        let amount_bytes = &amount.value().unwrap_or(Amount::from(0u64)).to_le_bytes()[0..16];
        let amount_128 =
            u128::from_le_bytes(amount_bytes.try_into().expect("should fit in 16 bytes"));
        let penalized_amount = amount_128 * (1_0000_0000 - penalty.0 as u128) / 1_0000_0000;

        // Witness the result in the circuit.
        let penalized_amount_var = AmountVar::new_witness(self.cs(), || {
            Ok(Amount::from(
                u64::try_from(penalized_amount).expect("can fit in u64"),
            ))
        })?;

        // TRUNCATED...

        let (penalized_amount_quo, _) = numerator.quo_rem(&hundred_mil)?;
        penalized_amount_quo.enforce_equal(&penalized_amount_var)?;

Note that this particular example is not necessarily a good one, as the final enforce_equal is actually not benign since the call to AmountVar::new_witness will constrain penalized_amount_var to be 128 bits, which will constrain the quotient computed by AmountVar::quo_rem to be 128-bit as well.

So in practice, while this specific check seems redundant, it helps mitigating the issue described in Unsound Division of AmountVar. But since the unsound division issue should be fixed, this check could be removed as well.

Description. In order to handle actions in user transactions, action handlers are implemented for each action. These action handlers are in charge of doing stateless checks as well as stateful checks, where the former checks usually verify zero-knowledge proofs when present, and the latter require reading the state of the blockchain.

One pattern was noticed during the audit: some values in the body of the action (provided by the user) can sometimes appear redundant.

For example, the body for a delegator vote action contains an unbounded amount value, which is provided by the user as the amount their delegated note would have unbounded to in the Penumbra token (if they had unbounded the note at the time). Importantly, the stateful check of the delegator vote action handler will recompute this value (based on the value of the note and historical information about the validator delegation rate at the time the note was delegated).

impl ActionHandler for DelegatorVote {
    // TRUNCATED...

    async fn check_stateful<S: StateRead + 'static>(&self, state: Arc<S>) -> Result<()> {
        let DelegatorVote {
            // TRUNCATED...
            body:
                DelegatorVoteBody {
                    // TRUNCATED...
                    value,
                    unbonded_amount,
                },
        } = self;

        // TRUNCATED...

        state
            .check_unbonded_amount_correct_exchange_for_proposal(*proposal, value, unbonded_amount)
            .await?;

In general this is a dangerous and error-prone pattern, as any user-controlled value is potentially malicious. Bugs can arise easily, when forgetting to verify such redundant values. When values can be computed by the validator themselves, it is better to do so.

Description. In the Amount::quo_rem function, the following checks are being enforced in the gadget:

zero_var  
    .amount  
    .enforce_cmp(&rem_var.amount, core::cmp::Ordering::Less, true)?;
rem_var  
    .amount  
    .enforce_cmp(&divisor_var.amount, core::cmp::Ordering::Less, false)?;
divisor_var.enforce_not_equal(&zero_var)?;

The first check is redundant, as it is merely checking that rem_var is not negative (that is is strictly less than $(p-1)/2$), but we're already doing this in the second line as enforce_cmp will check that both operand are non-negative.

In addition, the last check that $d \neq 0$ is also unnecessary, as it is already implied by the previous check that $0 \leq r < d$.