Adding indirect jump resolution

[didriklundberg]

This PR should put @adrwes work on indirect jump resolution into the main HolBA repository.

@adrwes, anything we should know before reviewing this?

[adrwes]

The work mainly consists of two proof-producing procedures:

• resolve_indirect_jumps which "removes" indirect jumps in the input program based on a proposal of indirect jump targets. It basically just evaluates resolve_fully_n. resolve_indirect_jumps is not very efficient since resolve_fully_n transforms the input program in multiple passes.
• transfer_contract which transfers a contract from the transformed program to the original one. It checks some conditions and instantiates the main correctness theorem of resolve_fully_n (resolve_fully_n_contract_transfer). (prove_and_transfer_contract also tries to prove the contract using existing infrastructure and logs some things)

The file examplesScript.sml contains examples of how the proof-producing procedures can be used.

[adrwes]

Also there is definitely some repitition in the proofs.