Porting the benchmarks proofs to the haskell backend

[daejunpark]

List of the proofs to be ported:

• [x] tests/specs/benchmarks/address00-spec.k: https://github.com/kframework/evm-semantics/pull/839
• [ ] tests/specs/benchmarks/bytes00-spec.k
• [ ] tests/specs/benchmarks/ecrecover00-siginvalid-spec.k
• [ ] tests/specs/benchmarks/ecrecover00-sigvalid-spec.k
• [ ] tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k
• [ ] tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k
• [ ] tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k
• [ ] tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k
• [ ] tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k
• [ ] tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k
• [ ] tests/specs/benchmarks/encode_keccak00-spec.k
• [ ] tests/specs/benchmarks/encodepacked_keccak01-spec.k
• [ ] tests/specs/benchmarks/keccak00-spec.k
• [x] tests/specs/benchmarks/overflow00-nooverflow-spec.k: https://github.com/kframework/evm-semantics/pull/851
• [x] tests/specs/benchmarks/overflow00-overflow-spec.k: https://github.com/kframework/evm-semantics/pull/851
• [ ] tests/specs/benchmarks/requires01-a0gt0-spec.k
• [ ] tests/specs/benchmarks/requires01-a0le0-spec.k
• [ ] tests/specs/benchmarks/staticarray00-spec.k
• [ ] tests/specs/benchmarks/staticloop00-a0lt10-spec.k
• [x] tests/specs/benchmarks/storagevar00-spec.k: https://github.com/kframework/evm-semantics/pull/857
• [x] tests/specs/benchmarks/storagevar01-spec.k: #882
• [ ] tests/specs/benchmarks/storagevar02-nooverflow-spec.k
• [x] tests/specs/benchmarks/storagevar02-overflow-spec.k: #882
• [x] tests/specs/benchmarks/storagevar03-spec.k: #882

[daejunpark]

Haskell backend issues:

Completeness:

• Blocking:
  • https://github.com/kframework/kore/issues/1962: Failed to evaluate trivial unsat constraints to #Bottom
    • This blocks all storagevar0[123]* specs.
  • https://github.com/kframework/kore/issues/2032: Failed to evaluate transitive equalities through #lookup.
    • This blocks storagevar02-nooverflow
• Non-blocking:
  • https://github.com/kframework/kore/issues/1945: Evaluate the right-hand side of claims

Usability of kore-repl:

• Major:
  • https://github.com/kframework/kore/issues/1955: Make step N to stop only at a "real" branch
  • https://github.com/kframework/kore/issues/1960: Redirection doesn't work with alias
• Minor:
  • https://github.com/kframework/kore/issues/1826: Support command sequencing
  • ~https://github.com/kframework/kore/issues/1917~: omit doesn't work with kast (known limitation)
  • https://github.com/kframework/kore/issues/1946: List rules applied between two nodes
  • https://github.com/kframework/kore/issues/1957: Abbreviate help command