The current transpiler is highly reliant on names to perform optimizations. At some point we will need to figure out how to make the transpiler work without names, generating anonymized proofs of execution.
As of writing this I see two options:
Allow the user to tell whether the transpiler should do optimizations which are limited to the content present on the official Lean Init. Then, after a Lurk AST is created, subject it to a post process step of anonymization
Do anonymized Lurk AST generation from the beginning, with optimizations based on anon CIDs. This option requires the maintenance of some CID-to-identifier map, very much like the map we currently have with PrimCids (or maybe an expansion of it?)
Option 1 seems easier and is in fact more aligned with what we have on main. But option 2 seems more correct.
The current transpiler is highly reliant on names to perform optimizations. At some point we will need to figure out how to make the transpiler work without names, generating anonymized proofs of execution.
As of writing this I see two options:
PrimCids(or maybe an expansion of it?)Option 1 seems easier and is in fact more aligned with what we have on
main. But option 2 seems more correct.