TODOs
Opened this issue · 0 comments
BoltonBailey commented
- Flesh out the
structure, and make it a complete implementation of "SNARK protocol".- General over field and pairing implementation.
- Module to say TypeI/TypeIII (every SRS element has an associated group, if it's TypeI copy the elements into the other group). Maybe make an
LinearPCPSNARKScheme.isTypeIdef to check this - subclass/typeclass for the special decidable snarks
- Is there a way to specify that a particular tactic should be used by default to close the soundness proposition goal?
- Port to lean 4
- Skip this and port by hand
- If I don't skip, get the mathlib3 working latest version
- Run mathport
- Reach out to Helger again/bring that email thread to a close