Skip to content

Pull requests: Verified-zkEVM/evm-asm

New pull request New
44 Open 696 Closed
44 Open 696 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

refactor(SailEquiv): flip runSail_rX_bits_x{1,2,5,6,7,10,11,12} (s v) to implicit
#851 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(ControlFlow): flip signExtend13/21_ofNat_small n to implicit
#850 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
feat(evm-word-arith): div128Quot_phase1b_check_implies_q1c_pos (#61)
#849 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SepLogic): flip PartialState trivial-family args to implicit
#848 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SailEquiv): flip runSail_{get_arch_pc,readReg_PC,get_next_pc} (s v) to implicit
#847 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SailEquiv): flip runSail_rX_bits_of_stateRel (sRv sSail) to implicit
#846 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
feat(evm-word-arith): div128Quot_rhatc_lt_2dHi — Phase 1b overflow bound (#61)
#845 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor: inline single-use isLt renames (#694)
#844 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SepLogic): flip CompatibleWith_singleton{PublicValues,PrivateInput} args to implicit
#843 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SepLogic): flip CompatibleWith_singleton{Reg,Mem,PC,Code} args to implicit
#842 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
feat(evm-word-arith): div128Quot_q1c_lt_pow33 — Phase 1b prerequisite (#61)
#841 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SepLogic): flip holdsFor_{memIs,pcIs,emp,regOwn,memOwn,pure,publicValuesIs,privateInputIs,stateIs} simp-lemma args to implicit
#840 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SepLogic): flip CodeReq.Disjoint.singleton (i1 i2) to implicit
#839 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(Stack): flip signExtend12_ofNat_small m to implicit
#838 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
feat(evm-word-arith): div128Quot_first_round_post — combined first round (#61)
#837 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(MulCorrect): flip div_mod_eq {x q r} to implicit, keep W explicit
#836 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(EvmWordArith): flip borrow_or_iff (c1 c2) props to implicit
#835 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
feat(evm-word-arith): div128Quot_first_round_correction (#61)
#834 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SailEquiv): flip runSail_jump_to (target s) to implicit
#833 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SailEquiv): flip stateRel_nextPC (sRv sSail) to implicit
#832 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(EvmWordArith): flip EvmWord.ult_iff (x y) to implicit
#831 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
feat(evm-word-arith): div128Quot_first_round_euclidean (#61)
#830 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SepLogic): flip CodeReq.union_satisfiedBy (cr1 cr2 s) to implicit
#829 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(DivMod/LoopDefs): flip loopIterPost{Max,Call}_{addback,skip} word args to implicit
#828 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
refactor(SepLogic): flip sepConj_pure_right (P Q) to implicit
#827 opened Apr 21, 2026 by pirapira Collaborator Loading…
1 task done
2
ProTip! no:milestone will show everything without a milestone.