Make MemoSet provable with Lurk

[porcuquine]

Once #1004 merges, the next step is to allow making proofs of calls to a query from Lurk. This issues tries to itemize the tasks needed to accomplish this. The first version to tackle will simply support factorial as implemented by DemoQuery.

• [ ] Make MemoSet proving configurable — so this work doesn't prevent the status quo from continuing to function exactly as-is.
• [ ] Add two new registers alongside existing CEK: transcript and memoset (the latter is the multiset acc associated with the deferred proofs).
• [ ] Add constraints to the primary reduction circuit so that the transition from Outermost to Terminal continuations can only be performed if the MemoSet conditions are met. This is very important. The conditions are:
  • [ ] memoset must be empty, which in this case means equal to zero.
  • [ ] transcript must equal the global r value that has been dynamically allocated for this proof.
  • NOTE: Both of the above are accomplished by CircuitScope::finalize().
• [ ] Create coprocessor that can prove blocks (of some rc) of factorial queries, by calling DemoCircuitQuery::synthesize_eval() on a query known to be factorial. This will need to handle padding when fewer than rc queries must be proved.
• [ ] Enhance evaluation to create a Scope and thread through reduction.
• [ ] Enhance reduction to support factorial with calls to DemoQuery::eval().
• [ ] Enhance proving to include the logic in CircuitScope::synthesize()
  • [ ] Create a CircuitScope from Scope
  • [ ] Prove insertion of toplevel queries as part of normal reduction proving (i.e. inline the call to synthesize_toplevel_query as the circuit equivalent of Query::eval().
  • [ ] Prove the queries themselves, by sequencing as many repetitions of the (in this case) factorial circuit as are required (depending on that circuit's rc and the total number of such queries used).
  • [ ] Prove the final transition to Terminal continuation.