The equivalence checker has a number of assumptions that are caveats to a successful equivalence check result. Each assumption can be roughly categorized as "meta", "provable" or "cheating".

Meta Assumptions

These relate to the soundness of the verification tools themselves, as well as the execution environment of the binary under analysis

We assume:

1. Correctness of our architecture semantics, code discovery, binary disassembler, etc.
2. Soundness of the specific SAT solver used and the correctness of our encoding of the equivalence problems into SAT.
3. Memory-mapped IO is not used in the given binaries. Later this can be weakened to assuming that memory-mapped IO regions have been accurately identified.

Provable Assumptions

These are assumptions that should be provable, but are unlikely to be false and therefore low priority to verify.

We assume:

1. Functions correctly restore non-volatile registers after returning.
2. Volatile registers are not read after a function call.
3. Functions correctly return to their call site (i.e. the pointer on the stack/link register before the call is the one that is jumped to afterwards).

"Cheating" Assumptions

These are assumptions that are certainly too strong, and need to be weakened before they are provable. For well-behaved programs, these assumptions are unlikely to invalidate the equivalence result, but a pathological program could exploit them to incorrectly prove equivalence.

We assume:

1. Stack pointers are initially equal. This can be invalidated if each block pair is reached via a different call path, or one program allocates a different number of stack variables.
2. Exact memory equivalence in the initial state for each block pair, including the stack. This needs to be weakened to account for unobservable differences in memory, but this requires a dependency analysis and a more precise model of the stack.
3. Equivalence of all non-volatile registers at intermediate function points. These can certainly be modified in the middle of a function, as long as they are properly restored, so we can't rely on their equivalence.