anoma / vamp-ir

Vamp-IR is a proof-system-agnostic language for writing arithmetic circuits
https://anoma.github.io/VampIR-Book/
Apache License 2.0
156 stars 44 forks source link

Separate circuit specification from evaluation #63

Open lopeetall opened 1 year ago

lopeetall commented 1 year ago

Currently we use fresh in the .pir document to instruct the evaluator to use the expression inside the fresh command to properly evaluate the witness during the proving process, meaning the .pir document contains both circuit specification and evaluation instructions. Ideally, instructions for evaluation would be completely separate from circuit specification.

A few reasons for this:

  1. Separation of concerns is usually a good idea.
  2. Evaluation/proving can be done outside of vamp-ir completely. For instance a front-end language targeting vamp-ir may want to handle this step, or even the backend proving library, and we should encourage this by default.
  3. The fresh command causes confusion, because the expression contained inside fresh does not add any constraints at all. If the user does not know this they can easily write under-constrained circuits with major exploits. It is best to hide this footgun as much as possible, or at least separate it from the constraints to better indicate that it is conceptually different.