Test harness for lemmas

[bbyalcinkaya]

This PR adds a test harness for testing lemmas. Tests are written in .k or .md files containing claims that target specific lemmas, with comments above the claims indicating which lemmas are being tested.

Additionally, the spec file proving functionality is now exposed as a CLI command: komet prove-raw. This command enables proving of K claims from a file and includes options for generating bug reports and saving proofs to specified directories.

usage: komet prove-raw [-h] [--proof-dir PROOF_DIR] [--bug-report BUG_REPORT] [--label LABEL] CLAIM_FILE

positional arguments:
  CLAIM_FILE            path to claim file

options:
  -h, --help            show this help message and exit
  --proof-dir PROOF_DIR
                        Output directory for proofs
  --bug-report BUG_REPORT
                        Bug report directory for proofs
  --label LABEL         Label of the K claim in the file

[ehildenb]

I think we can actually avoid using the runLemma => doneLemma functionality altogether. Does parse_modules, when called on modules that have claims like this:

claim ( (I <<Int 32) |Int 4) modInt 256 => ( (I <<Int 32) |Int 4) &Int 255

Produce this directly, or automatically wrap it in <k> cell and configuration? If it doesn't aoutomatically include the k cell, we probably can use the logic here (https://github.com/runtimeverification/evm-semantics/blob/43fce3055f5f94606fb3952028e37bf01e409169/kevm-pyk/src/kevm_pyk/__main__.py#L283), and the EqualityProof.from_claim to build a proof that will be discharged just by calling the simplifier, rather than the reachability prover. Does that work?

[bbyalcinkaya]

I think we can actually avoid using the runLemma => doneLemma functionality altogether. Does parse_modules, when called on modules that have claims like this:

claim ( (I <<Int 32) |Int 4) modInt 256 => ( (I <<Int 32) |Int 4) &Int 255

Produce this directly, or automatically wrap it in <k> cell and configuration? If it doesn't aoutomatically include the k cell, we probably can use the logic here (https://github.com/runtimeverification/evm-semantics/blob/43fce3055f5f94606fb3952028e37bf01e409169/kevm-pyk/src/kevm_pyk/__main__.py#L283), and the EqualityProof.from_claim to build a proof that will be discharged just by calling the simplifier, rather than the reachability prover. Does that work?

@ehildenb

Attempting to prove this directly with the APRProver gives a sort error (something like "Int is not a subsort of GeneratedTopCell") . So I implemented the logic in the link you provided. My only concern is this warning:

Building an EqualityProof that has known soundness issues: See https://github.com/runtimeverification/haskell-backend/issues/3605.

Is it something we should worry about?

[ehildenb]

I think, given that we're using universal binding for the equality proof now (https://github.com/runtimeverification/k/blob/master/pyk/src/pyk/proof/implies.py#L173), we should be OK w.r.t. that warning. Can you test it by breaking one of the proofs manually, and make sure it fails appropriately?