Skip to content

Latest commit

 

History

History
152 lines (111 loc) · 5.58 KB

proof-trace.md

File metadata and controls

152 lines (111 loc) · 5.58 KB
Raw

Proof Trace Format

This document describes the format for the binary proof trace that gets emitted when the --proof-output flag gets passed to the interpreter or --proof-hint is passed to krun. In order for the trace to be emitted, an appropriate instrumentation flag should have been passed to kompile or directly to llvm-kompile.

We currently offer two modes of instrumentation: the default one is enabled with the flag --proof-hint-instrumentation, while a slower one that generates a longer trace with all intermediate configurations is enabled with the flag --proof-hint-instrumentation-slow. Note that this trace format is in its early stages and will probably change quite a bit as development on it continues. Watch for the version of the trace format in the header of the trace.

Overview

The information presented by the trace starts with the initial configuration of the execution, followed by a sequence of rewrite steps consisting of which rule applied and the variable substitutions for that rule, and finally the configuration at the end of the execution. If slow instrumentation has been enabled, the trace additionally contains the intermediate configurations after each rewrite event, as well as the KORE terms that are passed as arguments in function events.

The format of the KORE terms themselves are in binary format, and in the proof trace, we delimit them with 64-bit sentinel values of 0xffffffffffffffff at the beginning.

Grammar

Here is a BNF styled description of the format:

proof_trace ::= header event* // only starting and final config events in normal mode

header            ::= "HINT" <4-byte version number>

event             ::= hook
                    | function
                    | rule
                    | side_cond_entry
                    | side_cond_exit
                    | config
                    | pattern_matching_failure
                    | function_exit

arg               ::= kore_term

name              ::= string
location          ::= string
function          ::= WORD(0xDD) name location arg* WORD(0x11) // the arg list is ommited in normal mode

function_name     ::= string
pattern_matching_failure ::= WORD(0x44) function_name

symbol_name       ::= string
hook              ::= WORD(0xAA) name symbol_name location arg* WORD(0xBB) kore_term

ordinal           ::= uint64
arity             ::= uint64
boolean_result    ::= uint8
variable          ::= name kore_term
rule              ::= WORD(0x22) ordinal arity variable*

side_cond_entry   ::= WORD(0xEE) ordinal arity variable*
side_cond_exit    ::= WORD(0x33) ordinal boolean_result

function_exit     ::= WORD(0x55) ordinal boolean_result

config            ::= WORD(0xFF) kore_term

string            ::= <c-style null terminated string>
uint64            ::= <64-bit unsigned little endian integer>

Notes

  • The rule_arity should be used to determine how many variable substitutions to read.
  • Events at the beginning of the trace (i.e. before the first config event) are related to configuration initialization.
  • The relative_position is a null terminated string of positive integers separated by : (ie. 0:1:1)
  • The arg* in the function and hook event is a list of arguments that are kore_terms passed to the function or hook.

Tools

As mentioned above, the proof trace is in binary format and can be generated using the appropriated flags to kompile and krun or directly to llvm-kompile and llvm-krun. We provide a tool to deserialize the binary trace to a human-readable format. The kore-proof-trace is located in the tools directory of the LLVM Backend repository and it takes two arguments: the path to the binary header and to the binary trace file. It can take 3 flags:

  • --verbose for verbose output,
  • --expand-terms for printing the KORE terms in the trace instead of their sizes and
  • --streaming-parser to use the streaming parser instead of the default one.

The tool will output the trace in a human-readable format to the standard output.

The binary header mentioned above is a file that contains data about the terms that might be serialized and the version of the binary KORE format used to serialize/deserialize the terms in the trace. The header is generated by the kore-rich-header tool located in the tools directory of the LLVM Backend repository. This tool takes a single argument, the path to the KORE definition file, and outputs the header to the standard output. The complete documentation for the header format and the new binary KORE format can be found in the docs/binary-kore-2.md file.

Example

Definition

module ADD-REWRITE-SYNTAX

  syntax Nat ::= z()
               | s(Nat)
  syntax Nat ::= add(Nat, Nat)

  syntax State ::= state(Nat, Nat)

endmodule

module ADD-REWRITE

  imports ADD-REWRITE-SYNTAX

  rule [add-zero] : add(z(), N:Nat) => N
  rule [add-succ] : add(s(N:Nat), M:Nat) => add(N, s(M))

  rule [state-next] : state(s(N:Nat), M:Nat) => add(s(N), M) ~> state(N, M)

  rule [state-succ] : s(M:Nat) ~> state(N:Nat, _:Nat) => state(N, s(M))
  rule [state-zero] : z() ~> state(N:Nat, _:Nat) => state(N, z())

endmodule

Input

state(s(s(z())), z())

Commands to generate the Proof Trace in binary format

kompile add-rewrite.k --llvm-proof-hint-instrumentation
krun input.add-rewrite --proof-hint --output-file input.add-rewrite.hints

Commands to print the Proof Trace in human-readable format

kore-rich-header add-rewrite-kompiled/definition.kore -o add-rewrite.header
kore-proof-trace add-rewrite.header input.add-rewrite.hints --expand-terms --verbose