runtimeverification / avm-semantics

BSD 3-Clause "New" or "Revised" License
15 stars 4 forks source link

Implement RPC based prover #283

Closed geo2a closed 1 year ago

geo2a commented 1 year ago

KAVM should take advantage of the emerging KCFG (K Control-flow graph) infrastructure to facilitate interactive exploration of proofs.

The kavm command-line executable should support two new commands:

View a KCFG: kavm kcfg-view

View a KCFG using the terminal UI provided by pyk.kcfg.tui.

This command should not do any execution and should just allow interactive viewing of an already generated KCFG.

kavm kcfg-view --definition-dir <path/to/kompiled/definition> <kcfg>.json

Generate a KCFG by attempting to prove a K claim: kavm kcfg-prove

This command should attempt to prove a K claim using kore-rpc --- the JSON RPC server of the Haskell backend. The command should leverage the pyk.kcfg.explore module. Whether the claim is proven or not, the kavm kcfg-prove command must generate a KCFG JSON file that can be viewed post factum with kavm kcfg-view.

kavm kcfg-prove --definition-dir <path/to/kompiled/definition>  --claim-id <claim-id-from-spec-file> <spec-file>(.k|.md)