Skip to content

Kore REPL

Jump to bottom
David Cox edited this page Aug 18, 2021 · 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.

Available commands in the Kore REPL

command behaviour
help shows the help message
claim [n | <name>] shows the nth claim, the claim with <name> or if used without args shows the currently focused claim in the form:
LHS ⇒ (modality) RHS
axiom <n | name> shows the nth axiom or the axiom with <name>
prove <n | name> initializes proof mode for the nth claim or for the claim with <name>
graph [view] [file] [format] shows the current proof graph (*)(**); optional view argument can be either expanded or collapsed; default is collapsed
(saves image in [format] if file argument is given; default is .svg in order to support large graphs; file extension is added automatically);
accepted formats: svg, jpeg, png, pdf;
step [n] attempts to run n proof steps at the current node (n=1 by default)
stepf [n] attempts to run n proof steps at the current node, stepping through branchings (n=1 by default); current node is advanced to the first interesting branching node (***)
select <n> select node id n from the graph
config [n] shows the config for node n (defaults to current node)
dest [n] shows the destination for node n (defaults to current node)
omit [cell] adds or removes cell to omit list (defaults to showing the omit list)
leafs shows unevaluated or stuck leafs
rule [n] shows the rule for node n (defaults to current node)
rules <n1> <n2> shows the rules applied on the path between nodes n1 and n2
prec-branch [n] shows first preceding branch (defaults to current node)
children [n] shows direct children of node (defaults to current node)
label shows all node labels
label <l> jump to a label
label <+l> [n] add a new label for a node (defaults to current node)
label <-l> remove a label
try (<a|c><num>)|<name> attempts <a>xiom or <c>laim at index <num> or rule with <name>
tryf (<a|c><num>)|<name> attempts <a>xiom or <c>laim at index <num> or rule with <name>, and if successful, it will apply it.
clear [n] removes all the node's children from the proof graph (****) (defaults to current node)
save-session file saves the current session to file
save-partial-proof [n] file creates a file, <file>.kore, containing a kore module with the name uppercase (<file>)-SPEC, a new claim with the current config (or config <n>) as its LHS and all other claims (including the original claim) marked as trusted
alias <name> = <command> adds as an alias for <command>
<alias> runs an existing alias
load file loads the file as a repl script
proof-status shows status for each claim
log <severity> "["<entry>"]" <type> <switch-timestamp> configures the logging output
<severity> can be debug, info, warning, error, or critical; is optional and defaults to warning
[<entry>] is the list of entries separated by white spaces or commas, e.g. [entry1, entry2];
these entries are used for filtering the logged information, for example, [] will log all entries with <severity>;
[entry1, entry2] will only log entries of types entry1 or entry2 as well as entries of severity .
See available entry types below.
<type> can be stderr or file filename
<switch-timestamp> can be enable-log-timestamps or disable-log-timestamps
debug-[type]-equation [eqId1] [eqId2] .. show debugging information for multiple specific equations; [type] can be attempt or apply, or nothing meaning both, as follows (debug-equation);
example usage: debug-attempt-equation eqId, debug-equation eqId1 eqId2; without arguments it will will disable showing the info, for example: debug-apply-equation;
exit exits the repl

Available modifiers:

usage behaviour
<command> > file prints the output of 'command' to file
<command> >> file appends the output of 'command' to file
<command> | external script pipes command to external script and prints the result in the repl
<command> | external script > file pipes and then redirects the output of the piped command to a file
<command> | external script >> file pipes and then appends the output of the piped command to a file

Explanations:

(*) If an edge is labeled as Simpl/RD it means that either the target node was reached using the SMT solver or it was reached through the Remove Destination step.

(**) A green node represents the proof has completed on that respective branch. A red node represents a stuck configuration.

(***) An interesting branching node has at least two children which contain non-bottom leaves in their subtrees. If no such node exists, the current node is advanced to the (only) non-bottom leaf. If no such leaf exists (i.e the proof is complete), the current node remains the same and a message is emitted.

(****) The clear command doesn't allow the removal of nodes which are direct descendants of branchings. The steps which create branchings cannot be partially redone. Therefore, if this were allowed it would result in invalid proofs.

Rule names can be added in two ways:
a) rule <k> ... </k> [label(myName)]
b) rule [myName] : <k> ... </k>

Names added via a) can be used as-is. Note that names which match indexing syntax for the try and tryf commands shouldn't be added (e.g. a5 as a rule name).

Names added via b) need to be prefixed with the module name followed by dot, e.g. IMP.myName

Available log entry types

Run kore-repl --help and refer to the --log-entries option for an up-to-date list of available log entry types and descriptions.

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