Upstream lemmas from Blockswap

runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License

51 stars 6 forks source link

Upstream lemmas from Blockswap #56

Open palinatolmach opened 1 year ago

palinatolmach commented 1 year ago

We should upstream lemmas used in the Blockswap engagement to KEVM/Kontrol (including the ones that helped with the issue inhttps://github.com/runtimeverification/kontrol/issues/19).

anvacaru commented 9 months ago

@PetarMax I remember upstreaming some lemmas from Blockswap. Can we close this issue?

PetarMax commented 9 months ago

Not quite yet, this is happening in stages. The current relevant PR is this one.