Handling optional stuff in a proof

[mimoo]

I've noticed that we handle optional things in a proof not super safely. For example, in verify for lookups we do:

let joint_combiner = if let Some(l) = &index.lookup_index {
  // ...
  self.commitments.lookup.iter().for_each(|l| {
                l.sorted
                    .iter()
                    .for_each(|c| fq_sponge.absorb_g(&c.unshifted));
            });

The first line is fine, we will enter the lookup flow if lookup is present in the index. What happens next is most likely not fine: it absorbs some lookup commitments only if they are present in the proof. This is because we use Option::iter() on an Option. Better is to do something like:

let lookup_comms = self.commitments.lookup.ok_or(VerifyError::MissingLookupCommitments)?;
for com in lookup_comms.sorted {
  fq_sponge.absorb_g(&com.unshifted);
}

[github-actions[bot]]

Stale issue message

[github-actions[bot]]

Stale issue message

[mimoo]

perhaps there is a way to enforce this using types or something

[github-actions[bot]]

Stale issue message

[duguorong009]

@mimoo I think the current code is working as expected. I think the example code you are showing is this one. In fact, the Option::iter().for_each() is applied only when there are values.(I mean Some(value)). So, if there is no value(LookupCommitment is None), the code just do NOTHING, and keep going. From my understanding, there are the cases of NO LookupCommitments. right?

[duguorong009]

@mimoo I also see that the codes are different between current master branch and your example. Can you check & let me know why? One is absorbing the sorted values, while another is absorbing the aggreg values. :man_shrugging: Your example

let joint_combiner = if let Some(l) = &index.lookup_index {
  // ...
  self.commitments.lookup.iter().for_each(|l| {
                l.sorted
                    .iter()
                    .for_each(|c| fq_sponge.absorb_g(&c.unshifted));
            });

Current code

//~ 1. If using lookup, absorb the commitment to the aggregation lookup polynomial.
        self.commitments.lookup.iter().for_each(|l| {
            fq_sponge.absorb_g(&l.aggreg.unshifted);
        });

[mimoo]

the code is different because it must have been updated since I wrote this issue :) I still see the sorted commitments absorbed here:

• prover
• verifier

my issue was really about: we should not just take the proof and do things based on what's in the proof. The proof is expected to be constructed a certain way (to have some of its fields set or not) based on the VerifierIndex struct.

(I think I have another issue that says we should make sure that the proof is well-formatted based on the index, first thing in the verification.)

For example here, we check if lookup commitments exist, and absorb them if they do. We're doing things based on what the prover gives us, which is untrusted input at this point. Instead, we should check what the index says, if the index says that we're using lookup, then we should absorb these things, if the index says we're not using lookup, then we should make sure that there's nothing to absorb in the proof (i.e. fields set to None)

[duguorong009]

the code is different because it must have been updated since I wrote this issue :) I still see the sorted commitments absorbed here:

• prover
• verifier

my issue was really about: we should not just take the proof and do things based on what's in the proof. The proof is expected to be constructed a certain way (to have some of its fields set or not) based on the VerifierIndex struct.

(I think I have another issue that says we should make sure that the proof is well-formatted based on the index, first thing in the verification.)

For example here, we check if lookup commitments exist, and absorb them if they do. We're doing things based on what the prover gives us, which is untrusted input at this point. Instead, we should check what the index says, if the index says that we're using lookup, then we should absorb these things, if the index says we're not using lookup, then we should make sure that there's nothing to absorb in the proof (i.e. fields set to None)

Thanks for the detail! @mimoo So, it means that the verification SHOULD error when fields set to None.

[mimoo]

I guess there are 4 cases, maybe a match statement would make sense:

match (index_has_lookup, lookup_commitment_field_set) {
  (x, y) if x == y => ()
  (x, y) => error
}

[duguorong009]

Thx again! @mimoo I hope I take this one first. The reason is that it looks like simpler than ChunkedEvaluations issue. (Tbh, ChunkedEvaluations issue is literally MEDIUM DIFFICULTY for myself :dizzy_face: )

[duguorong009]

BTW, @mimoo It looks like the Lookup Index check has been already done. (at least in verifier) https://github.com/o1-labs/proof-systems/blob/f353a04848363374b8318cb96224370b1105e085/kimchi/src/verifier.rs#L85-L89

[mimoo]

yeah no worries! If you ever think of a list of things that were hard to grasp to tackle the first one I can try to make these clearer for you or for other people in the future :)

the checks on the lookup index are done but they're not really exhaustive, and I'm scared that we might do it the wrong way sometimes. IMO we should still validate that the proof is correctly constructed based on the verifier index first thing in the verifier

[duguorong009]

Thanks! @mimoo Then, you will list the possible issues for validating the verifier index in verifier.rs? or Should I go for finding myself & add improvement commits?

[mimoo]

if you can find them yourself it's good, otherwise I can list more when you have a PR : )

[github-actions[bot]]

Stale issue message

[github-actions[bot]]

Stale issue message