Use an llvm backend library in exec_prove with --use-booster

[jberthold]

Set llvm_definition_dir in exec_prove when use_booster == True.
Otherwise we might run with booster but will fall back to kore-rpc on every concrete term that needs hooks.

With this change, test address00-spec.k runs in 76 sec with --use-booster, while it takes 110 sec without (This includes the compilation time for the verification module, the actual speedup for running the proof is higher).

[jberthold]

The activated LLVM backend causes issues in proof mcd/dai-symbol-pass-spec.k, the function #asByteStackInWidthaux is missing from the LLVM library because of the [symbolic] tag here.
Probably one needs to add a [symbolic] attribute to every lemma that introduces this function? not sure

[ehildenb]

Wow, good find!

[jberthold]

I tried to remove the [symbolic] attributes from the verification modules in tests/specs/erc20 and tests/specs/mcd but that causes compilation issues because include/kframework/lemmas/lemmas.k is [symbolic], too, and its definitions are missing when compiling the now-not-symbolic mcd/verification.k.
Not sure about the best way forward here, probably we need to refactor more module headers, or craft a dedicated syntax module for llvm-targeted compilation.

[ehildenb]

There are some more changes on this PR, which may help this one to pass. In particular:

• ec44f50
• b7466e5
• 928afb5
• 83ecad6
• ee6dad0

[ehildenb]

This looks ready to merge to me, any other blockers? The last require check is removed here: #2076