Use arecibo::supernova::NonUniformCircuit

[porcuquine]

See lurk-supernova (#631).

Arecibo introduced a NonUniformCircuit trait in lurk-lang/arecibo#23. Use this to support NIVC from Lurk, using Coprocessors.

• Implement a trivial NIVC code path that uses NonUniformCircuit but only provides a single sub-circuit, just to surface or rule out trivial problems with the interface and establish lurk-rs' ability to use it.
• Add Coprocessor support.
  • The main trait method to implement is NonUniformCircuit::primary_circuit — which takes a circuit_index parameter and returns the appropriate circuit. Note that all return values must have the same type — so this type will need to be an enum implementing StepCircuit. Each variant of the enum will specify a different circuit. By convention, we will specify that primary_circuit(0) returns an enum variant corresponding to a universal Lurk reduction. Other variants represent the coprocessors supported by the Lang.
  • Eventually, we will need a way of deriving these NonUniformCircuit enums from a Lang (derive proc macro?). Initially (this work), we can require that these be constructed by hand.

In order for coprocessor semantics to be implemented using NIVC, we will need some small extensions to how the circuit is generated. That means this work depends on lem-coprocessors.

The circuit extensions required are as follows:

• coprocessor circuits must check their inputs (CEK) and only generate correct proofs if the input is indeed computable by the coprocessor in question. This maintains the invariant that all circuits provided as variants of NonUniformCircuit guarantee to correctly prove evaluation of some reduction step of a Lurk Lang.

  • The following naive description captures the spirit of the requirement:

    When that Lang includes coprocessors, expressions of the form (<coprocessor-name> <arg-1> <arg-2> ... <arg-n>) are considered primitive reduction steps which can be implemented by a coprocessor circuit. This means the coprocessor circuit must include a Lurk-aware wrapper, checking the symbol in the function (head) position of the call is the one to which this coprocessor has been bound in the Lang.

    Note, however, that the above simplified description does not respect the coprocessor calling semantics (as-yet not fully defined, see Coprocessor args must be evaluated #398, aka coprocessor-eval). The most likely candidate is that the evaluated arguments will in fact be on the top of the env (binding stack), in reverse order (last arg on top). The expr (C(ontrol) register of the CEK) may be a Thunk or other object representing a zero-arg call to the coprocessor. The important point is that this control value must be checked by the coprocessor.

  • SuperNova defines the function $\phi$, which must specify the index of the next circuit to be used. This is implemented in arecibo by adding an IO value to each NonUniformCircuit. This means each circuit is responsible for computing and returning the result of $\phi$ computed on that circuit's input+witness, and is also responsible for checking that the index received as input is correct.

  • That means each coprocessor circuit must check that the index input is the one statically assigned for the enum variant. This is trivial but must be performed — even for the universal circuit, which must ensure the incoming index is 0.

  • Because Lurk defines coprocessors to be interchangeable (a coprocessor is incapable of proving an invalid Lurk reduction step — see above), there is no constraint on selection of 'next circuit'. That is, each circuit may provide any next-circuit index as the result of its $\phi$ computation. The correct value must be chosen non-deterministically, by the prover, depending on which sub-circuit will be capable of proving the next step. If a coprocessor is required for the next reduction, that coprocessor's index must be provided as the final output of the circuit. If a general Lurk reduction (for example) is required, then 0 must be returned. Again, note that the circuit need not constrain this final output.

  • In order to accommodate reduction-count > 1 (i.e. multiple reduction circuits representing multiple Frames unrolled into a single MultiFrame circuit, we need to handle 'padding' in the likely case that a coprocessor invocation does not fall exactly the end (in the last Frame) of a MultiFrame. In that case, we define a simple reduction rule when using a universal Lurk reduction circuit to evaluate an expression which invokes a coprocessor during its evaluation. Specifically, since a univeral Lurk circuit cannot reduce a coprocessor invocation, then when such an invocation is detected in the control position, the deterministic reduction rule is to copy all inputs to outputs — making the frame a no-op. (The $\phi$ value need not be copied or otherwise constrained.)

  • In the future, we will likely want to implement circuits such that the prover can non-deterministically choose to make any reduction a no-op. This will allow an important class of optimizations involving heterogenous MultiFrames. For now, we ignore this and mention it only for situational awareness to inform implementation and design decisions.

[porcuquine]

#677 addresses the spirit of this issue. Some details landed slightly differently, and some gaps remain due to dependent work not yet being completed.