Stable coprocessor order #665
Conversation
arthurpaulino
force-pushed
the
ap/stable-coprocs-order
branch
from
44d1f40
to
987b2f5
Compare
| // TODO: eliminate this unecessary piece of data | ||
| let z_ptr = lurk::z_ptr::ZPtr(ExprTag::Nil, F::ZERO); |
There was a problem hiding this comment.
It's a little worse than this comment suggests. As far as I can see, this is adding the wrong data. Now, maybe in the LEM case, this wrong data is unnecessary. But a Lang is not specific to LEM or not-LEM. And consequently, it cannot be correct to construct one this way. This 'scalar ptr' must correspond to the symbol to which the coprocessor is bound. If LEM requires its own variant of Lang, then that would need to be formalized somehow.
This is not just academic. A Lang created as above could lead a non-LEM circuit to producing incorrect proofs. Such a Lang would be toxic and require very special handling. It shouldn't be possible to create such dangerous substances with the Lurk API.
There was a problem hiding this comment.
The LEM pipeline indeed doesn't need the cached ZPtr for this.
Would it be okay to have an add_coprocessor_with_zptr and allow the caller to provide the ZPtr? Then LEM would be able to feed it with whatever.
|
As noted elsewhere, this will likely need to change to be consistent with the (not-quite-complete) parallel work to allow creation of NIVC proofs from |
|
#670 makes this PR obsolete |
Use an
IndexMapto stabilize the order of coprocessors in a Lang.This stable order is needed in order to make LEM code generation for a Lang consistent, regardless of the internal algorithm that
HashMapwould use.The
IndexMapalso comes in handy when we want to efficiently retrieve the index of a coprocessor. This will be useful for the implementation of NIVC.