Formally defining X86 semactics in K

Ideas (To be Implemented)

First deal with stratum 0 cases because that will expose all the K rules used for based instrcutions. That will also ensure that verification lemma are to be written for all the base rules. The higher stratum rules will just use the base rules for which we already have the verifications lemmas defined.
The write set is something that is always be touched by the target instruction or stratifies seq of instruction.
strata formulas agreee on target instruction write set ==> even the read set can get clobbered.
addpd_xmm_xmm: shows that the existing rules can save the upper 128 bits of 256 registers, if the operation demands cloberring just the 128 bits.
Why simplification lemmas are useful
- Opt help in testing individual instructions as the instructions only dependencies are the base K operations NOT any other instr, not even the pseudo instr
- Small formulas prevent slow down of the k tool
- Help to check consistency with strata BV formula
Stata's gives uninterpreted formulas whereas K gives executation seantics for those cases.
The K rule representation is much more legible than a sequesnce of x86 instructions.
Strata gives the semantics for a concrete instructions whereas K gives symantics for generic instructions