Skip to content
This repository has been archived by the owner on Feb 15, 2024. It is now read-only.

Issues: runtimeverification/proof-generation

34 Open 15 Closed
34 Open 15 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Remove redundancies such as well-formedness checks, positivity, etc.
#82 opened Jul 4, 2023 by fiedlr
Statement compression
#81 opened Jul 4, 2023 by fiedlr
Compact representation for proofs
#80 opened Jul 4, 2023 by fiedlr
1
Merge proof_generation.ast with pyk.kore.syntax
#68 opened Jun 12, 2023 by nishantjr
4 tasks
CI: Use python integration tests when generating/verifying metamath code
#63 opened Jun 1, 2023 by nishantjr
1
Look for benchmarks for IMP, python-esque language, Solidity, EVM.
#62 opened Jun 1, 2023 by nishantjr
@fiedlr @xc93
3
Prepare a short seminar about zkLLVM [optional]
#57 opened May 26, 2023 by fiedlr
Try the Metamath circuit on one of our benchmark proofs
#56 opened May 26, 2023 by fiedlr
2
Compile the Metamath verifier into LLVM bytecode compatible with zkLLVM
#55 opened May 26, 2023 by fiedlr
@Robertorosmaninho
8
Figure out how to verify a certificate
#54 opened May 26, 2023 by fiedlr
@mariaKt
4
LLVM Backend stores information needed for proof hints
#51 opened May 25, 2023 by gtrepta
ITP Compression algorithm is incorrect bug Something isn't working
#50 opened May 25, 2023 by nishantjr
Write python program to split metamath database into one file per lemma for testing ZK implementations. large-task 5 Days
#46 opened May 24, 2023 by nishantjr
@nishantjr
LLVM Backend generates proof hints xl-task 2 weeks
#45 opened May 23, 2023 by nishantjr
1
Proof generation for Blockchain tests.
#44 opened May 23, 2023 by nishantjr PoC-Phase-2
Proof generation for VM tests
#43 opened May 23, 2023 by nishantjr PoC-Phase-2
Test that kompile-generated kore for KEVM can be verified by MM large-task 5 Days
#42 opened May 23, 2023 by nishantjr PoC-Phase-2
Add tests for kompile-generated kore files for IMP medium-task Estimated 3 days
#40 opened May 23, 2023 by nishantjr PoC-Track-1
@nishantjr
Python parser for LLVM proof hints.
#39 opened May 23, 2023 by nishantjr PoC-Track-2
1
Update to latest K large-task 5 Days
#38 opened May 23, 2023 by nishantjr PoC-Track-1
1
Update hand-proved metamath files to work with the official metamath small-task
#37 opened May 23, 2023 by nishantjr PoC-Track-1
@nishantjr
CI for proof generation
#36 opened May 17, 2023 by nishantjr
5 tasks
<notation>-is-pattern should be proven, rather than assumed.
#33 opened May 3, 2023 by nishantjr
The Kore symbol named ceil
#32 opened Jul 11, 2022 by amelieled
1
Modeling the notion of fresh variable into Metamath
#30 opened Jan 27, 2022 by amelieled
2
ProTip! Add no:assignee to see everything that’s not assigned.