+
Skip to content

Conversation

clararod9
Copy link

The Decoder template misses a check, generating a R1CS constraint system that admits multiple outputs for the same input. For example, in case it is instantiated with w = 2 then the generated constraint system

out[0] * inp === 0
out[1] * (inp - 1) === 0
out[0] + out[1] === success
success * (success - 1) === 0

admits multiple solutions for the input inp = 1:

  • out[0] === 0, out[1] === 1, success = 1
  • out[0] === 0, out[1] === 0, success = 0

The proposed solution adds the missing check satisfying the same specification for the template.

  • Success := w < inp
  • for i in 0..w: out[i] = 1 if i = inp, else out[i]

However, as adding the check increments the number of non-linear constraints, the proposed solution also defines a new template (Decoder_strict) that can be used to optimize the number of non-linear constraints when the only solutions that are valid are the ones where success == 1. This condition appears in the template Multiplexer that represents the main use of Decoder in the circomlib.

The template Decoder_strict satisfies the following specification:

  • In case inp < w:
    for i in 0..w: out[i] = 1 if i = inp, else out[i] = 0
  • If w >= inp => the sysetm of constraints does not have any solution

The number of constraints after compiling using --O2 of each one of the templates is:

  • Decoder(w): 2 * w + 1
  • Decoder_strict(w): w + 1
  • Multiplexer(wIn, nIn): (wIn + 1) * nIn (same as previous version of Multiplexer)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

点击 这是indexloc提供的php浏览器服务,不要输入任何密码和下载