Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman: A verified algebraic representation of cairo program execution. CPP 2022: 153-165