Make symbolic simulation for equiv checking infer output of loads

[aqjune-aws]

This patch updates symbolic simulation tactics for equivalence checking to infer the output of memory loads from assumptions if there is no directly matching equality.

For example, if there is an assumption read (memory :> bytes (ptr,8*n)) = a but nothing about read (memory :> bytes64 (word_add (ptr,8*k))), it tries to construct its output as bigdigit a k using SIMPLE_ARITH_TAC. This helps remove boilerplate codes in proofs that manually construct all equalities between 64-bit and 128-bit memory reads at known locations, which typically looked like:

REPEAT (FIRST_X_ASSUM BIGNUM_EXPAND_AND_DIGITIZE_TAC) THEN
ASM_PROPAGATE_DIGIT_EQS_FROM_EXPANDED_BIGNUM_TAC THEN
(* necessary to run ldr qs *)
COMBINE_READ_BYTES64_PAIRS_TAC THEN

This also reduces the sizes of assumptions, which may affect positive results to proof checking times, but in fact caused slowdown to larger equivalence checking tactics such as p256/p384's point operations. For these ops, a separate flag disabling this feature is set.

The main tactics are MK_MEMORY_READ_EQ_BIGDIGIT_CONV and DIGITIZE_MEMORY_READS_TAC.
They construct equations involving the unseen memory reads and bigdigit. They are passed to ARM_N_STEP_TAC (the ARM_STEP'_TAC in the past; this renaming will be explained below), which are called 'auxiliary memory read equations, and they are either ASSUME_TACed or passed to the caller separately from other normal equations describing the actual outputs of a simulated instruction.

On top of these updates, I also

• Renamed the tactics that are related to equivalence checking so that it does not have a punctuation mark but instead _N as a differentiating string from its original version. For example, the equivlaence checking version of ARM_STEP_TAC was ARM_STEP'_TAC, but now it is ARM_N_STEP_TAC. _N came from ensures_n. Some tactics are exception from this pattern, however.
• Added approximate_input_output_regs which gets the input and output register from a basic block. Input registers are registers that are read without written, and output registers are those written but not read later. This does not consider memory reads and writes. This will be used in my future patches.
• Extended ENSURES2_WHILE_PAUP_TAC so that its step counter needed to simulate the backedge is not just '1', but parameterically given in general.
• And many other minor changes and updates..!

Issue #, if available:

Description of changes:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[aqjune-aws]

I realized that MK_MEMORY_READ_EQ_BIGDIGIT_RULE was actually a conversion; renamed it to MK_MEMORY_READ_EQ_BIGDIGIT_CONV. :)