Add angelic encoding for division/remainder

[lsrcz]

I tried to use this to help proving division/remainder but it does not help much. But still good to keep it there.

---

Stack:

• Add angelic encoding for division/remainder #478 ⬅
• Add declare_fresh #477

⚠️ Part of a stack created by spr. Do not merge manually using the UI - doing so may have unexpected results.

[cdleary]

Can you add to this a good definition of what "angelic" means / where it comes from as a term of art? Looks like it's a library implementation for some known operation that we expect might make things easier for the solver, but I'm not 100% sure (or why we'd pick this particular structure) -- documentation would be good. You can make a markdown with some design thoughts in xlsynth-g8r/docs/solver.md or something if it's an involved explanation. Thanks for explaining!

[lsrcz]

Can you add to this a good definition of what "angelic" means / where it comes from as a term of art? Looks like it's a library implementation for some known operation that we expect might make things easier for the solver, but I'm not 100% sure (or why we'd pick this particular structure) -- documentation would be good. You can make a markdown with some design thoughts in xlsynth-g8r/docs/solver.md or something if it's an involved explanation. Thanks for explaining!

Ah this is not something I invented. The paper Programming with angelic nondeterminism could provide more context. I will add an explanation in the code tomorrow.

tl;dr in verification, we can consider the inputs as demonic nondeterminism such that it will be chosen to falsify our claim. Angelic nondeterminism, in contrast, works in favor for us and is chosen to provide a value to meet our specification, here, the division.

We try to reduce the division to multiplication with angelic nondeterminism by the relation such that for $(q, r) = \mathrm{divMod}(a, b)$, $q * b + r = a$. Divisions are in general the hardest operator for an SMT solver to reason about as after bitblasting the division circuit may require an iterative process that is far more complex than other arithmetic operations, including multiplication.

But for very large bit-width, multiplications are very hard too...so this may help, but we cannot expect too much.

[cdleary]

Thanks for explaining angelic to me on the whiteboard -- now looking at the code I'm wondering, how do we usually know/determine if the angelic encoded properties are correct? e.g. if it was off somehow would we have an indicator or we just need to review it very carefully?