If we extend the bitc category which exposes VampIR APIs to Geb, then Geb's upcoming equalizers could either be erased by compile-time proofs or compiled to constraints which would alleviate the programmer's need to prove that constraints were satisfied. See https://github.com/anoma/geb/pull/105#issuecomment-1527714854 for some details.
If we extend the
bitc
category which exposes VampIR APIs to Geb, then Geb's upcoming equalizers could either be erased by compile-time proofs or compiled to constraints which would alleviate the programmer's need to prove that constraints were satisfied. See https://github.com/anoma/geb/pull/105#issuecomment-1527714854 for some details.