Skip to content

Pull requests: opencompl/veir

New pull request New
39 Open 1,159 Closed
39 Open 1,159 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
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat: for eligible operations, fold the result to poison when any input is poison
#1276 opened Aug 19, 2026 by regehr Collaborator Loading…
@regehr
chore: Remove generic functions about region kind out of Verifier.lean
#1275 opened Aug 19, 2026 by math-fehr Collaborator Loading…
@math-fehr
1
feat: (WIP) Basic tactic to solve bounded parametric bitvector formulas automatically
#1274 opened Aug 19, 2026 by luigirinaldi Contributor • Draft
chore: fail CI when there exist lean files disconnected from the build
#1272 opened Aug 19, 2026 by regehr Collaborator • Draft
@regehr
4
feat: implement MLIR's isolatedFromAbove trait
#1265 opened Aug 18, 2026 by regehr Collaborator Loading…
@regehr
7
feat: Expand PBV examples to cover sign and zero extensions
#1263 opened Aug 18, 2026 by luigirinaldi Contributor • Draft
1
update lean to 4.33.0
#1255 opened Aug 17, 2026 by tobiasgrosser Collaborator Loading…
@tobiasgrosser
19
feat(printer): registerable custom printing hooks
#1236 opened Aug 14, 2026 by GZGavinZhao Collaborator • Draft
@GZGavinZhao
5
feat(legalizer): add GlobalISel-like legalization framework
#1234 opened Aug 12, 2026 by naveen-seth Contributor • Draft
Add a basic CTree data structure
#1228 opened Aug 7, 2026 by nchappe Contributor Loading…
@nchappe
feat(match): add the value-producing match operations
#1218 opened Aug 6, 2026 by tobiasgrosser Collaborator Loading…
@tobiasgrosser
3
ci: drop the no-op source .envrc step
#1193 opened Aug 4, 2026 by tobiasgrosser Collaborator Loading…
@tobiasgrosser
4
[WIP] Work in progress propositional dominance definition
#1089 opened Jul 16, 2026 by math-fehr Collaborator • Draft
1
feat(LLVM): prove monotonicity of the LLVM.Byte operations LLVM The LLVM Dialect
#1070 opened Jul 12, 2026 by tobiasgrosser Collaborator • Draft
@tobiasgrosser
feat(interpret): prove interpretOp' monotone for the riscv dialect RISCV The RISCV Dialect
#1069 opened Jul 12, 2026 by tobiasgrosser Collaborator Loading…
@tobiasgrosser
13
Combine proofs
#1055 opened Jul 10, 2026 by tobiasgrosser Collaborator Loading…
feat: proof for same_val_zero_0
#1044 opened Jul 9, 2026 by osmanyasar05 Contributor Loading…
feat: prove correctness of the LLVM-dialect RISC-V combines
#1043 opened Jul 9, 2026 by tobiasgrosser Collaborator Loading…
1
feat(Rewriter): introduce eraseOp!/replaceValue! and clear remaining pass sorries
#968 opened Jul 1, 2026 by tobiasgrosser Collaborator Loading…
3
feat(printer): declarative assembly-format DSL + custom (pretty) printing parser
#946 opened Jun 29, 2026 by GZGavinZhao Collaborator Loading…
@GZGavinZhao
10
feat(verifier): check dominance
#944 opened Jun 28, 2026 by regehr Collaborator • Draft
@regehr
23
Feat: cse for gep incl. incomplete testing
#887 opened Jun 16, 2026 by salinhkuhn Contributor • Draft
1 task
3
feat(cse): use dominance to make CSE work across blocks
#867 opened Jun 13, 2026 by regehr Collaborator • Draft
3
[WIP] progress on rewrite lifting
#866 opened Jun 13, 2026 by math-fehr Collaborator • Draft
1
feat(dataflow): sparse forward dataflow analysis api
#854 opened Jun 11, 2026 by axelcool1234 Collaborator Loading…
24
ProTip! What’s not been updated in a month: updated:<2026-07-19.