Skip to content

Kore REPL

Jump to bottom
Andrei Burdușa edited this page Mar 18, 2020 · 18 revisions

Kore REPL

The Kore REPL is currently under early active development. Breaking changes may occur at any time.

Prerequisites

In order to see the execution graph (the graph command), you will need graphviz installed (and dot available in your path). This option currently only works on Linux.

In the root of the repository:

$ make k-frontend
$ stack build

Running the REPL

The REPL is currently setup to work with the imp proofs under the repository:

$ cd src/main/k/working/imp
$ make prove/max-spec.krepl

Running with other definitions/proofs

The kore-repl executable can be ran with any other languages/definitions.

You can run it with kprove, for example:

$ kprove --haskell-backend-command "/path/to/kore-repl " -d . -m VERIFICATION spec.k

In order to get the path to kore-repl, you can run stack exec -- which kore-repl.

Alternatively, you can run kore-repl directly:

$ /path/to/kore-repl path/to/vdefinition.kore --module VERIFICATION --prove /path/to/spec.kore --spec-module SPEC-NAME

Note you will have to manually compile to kore to obtain vdefinition.kore and spec.kore if you chose to run kore-repl yourself.

Interrupting

You can interrupt the repl while it is evaluating steps in order to stop long-running/infinite loops by pressing Ctrl-C. Please note that this not work if you run the repl through kprove. See above for how to run kore-repl directly.

REPL scripts

The repl can execute commands from a file. When supplying a repl script file as a command line argument, the repl can be run in two modes: interactive (default) or run-mode. After a script is executed in interactive mode you will be taken to the repl prompt. Running a script in run-mode will output the status of the proof after executing the script and exit. You can also load scripts while inside the repl by using the load command.

Command line arguments for when running kore-repl directly (as above):

  • --run-mode or -r: flag to run in run-mode; if you omit this argument you will run the repl in interactive mode
  • --repl-script: path to the script

So, in order to run in run-mode using script.kscript found in the current directory:

$ /path/to/kore-repl path/to/vdefinition.kore --module VERIFICATION --prove /path/to/spec.kore --spec-module SPEC-NAME --repl-script script.kscript --run-mode

Exit codes for run-mode:

  • exit code 0: successful execution and proof was completed
  • exit code 1: error during execution
  • exit code 2: successful execution but proof was not finished

K output

The repl has some commands which output patterns. By default, these patterns are written in KORE, but can be transformed to K by using the commands defined in kore/dist/kast.kscript. You can manually load the script using load after starting the repl, or execute the script at the beginning by supplying it as a command line argument (see the section above for further details).

The commands which output K have similar names to their KORE outputting counterparts, e.g. konfig instead of config or ktry instead of try. Some can be suffixed with -n, -d or -nd for specifying the argument, the directory or both, respectively.

  • kcliam, konfig and krule don't require the argument for their counterparts; can be suffixed with -n, -d or -nd
  • kaxiom, ktry and ktryf require the argument for their counterparts; can be suffixed with -d See the kast.kscript for the full list of K commands.
Clone this wiki locally