Formal verification related fixes

[OlivierBBB]

Main point

There is an issue with the padding in the ADD module spotted by @ericsson49 : a malicious prover can use the padding to insert a single wrong instruction into the ADD module. This is a serious security issue, thankfully with a trivial fix.

Other modules of that era may also be affected.

List of fixes

• ADD module: constrain INST to be zero in the padding (+ optional vanishing of arguments in padding)
  • fix spec https://github.com/Consensys/zkevm-spec/commit/16139fb240c01ec62d322317774602cf04c79dbc
  • fix corset ADD module padding fix #30
• check if affected and fix if necessary
  • MUL
  • MOD
    • currently requires instruction decoding, but could be done with out with 4 binary columns
    • missing constraint killing INST in the padding (spotted by @ericsson49)
  • EXT
  • SHF
    • instruction isn't constrained in padding
    • instruction isn't constrained outside of padding either, though the point is recognized
      
    • again 3 binary columns would suffice
  • BIN
    • spec update
    • lisp update
    • java update
  • WCP
    • spec update
    • lisp update
    • java update
      instruction + simplifying OLI etc ...