argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel
MIT License
114 stars 8 forks source link

[RFC] Generating Lurk proofs of typechecking #242

Closed winston-h-zhang closed 1 year ago

winston-h-zhang commented 1 year ago

Closes #236 Closes #232 because we use anon hashes all over the pipeline instead of names/namespaces Closes #205 because we're abandoning IPLD and we're using Lurk as data where it's needed Closes #201 because CLI API has changed Closes #200 Closes #136 because an invalid recursor will entail some weird hash, namely one that nobody's interested in Closes #133 because that's implemented as a CLI command (gentc) Closes #71 because IPLD encoding no longer applies Closes #30 (similar to #136)