Modular definition of small-step semantics (sInsn)

[jeehoonkang]

• Currently sInsn (in /src/Vellvm/opsem.v) comprises some 20 cases.
• In my experience, many proofs are common to many of 20 cases. for many cases memory is intact, and it is the only property that is required for those cases.
• In that case I had to prove a trivial lemma that [sInsn means memory intact or 5 more cases], or [inverse sInsn and have 20 cases, which means slow interpretation of proof terms].
• I would like sInsn to be organised in such a way that not too much cases arise in proof. For example:

Inductive arithmetic_step : ...
| bop | fbop | ...

Inductive intact_stack_step : ...
| arithmetic_step | load | ... | branch

Inductive step : ... // sInsn
intact_stack_step | call | return | ...

It would require a complete adjustment of metatheories, so I would like to discuss in detail.

[dgarbuzov]

I think this is clearly a good idea, but it's hard to estimate how much effort it would require. Personally, before undertaking a change this size, I would prefer to

1. Complete Remove all obvious dead code and unused lemmas #5 so that we don't waste time updating dead code
2. Have a parser and test suite that works with current versions of LLVM, so we know we aren't introducing additional bugs

[jeehoonkang]

@dmitrig totally agree with you :-)