Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

docs/proof-trace.md

@@ -1,13 +1,16 @@
 # 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. In order for the trace
-to be emitted, an appropriate instrumentation flag should have been passed to `llvm-kompile`.
+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 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.
+`--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
 
@@ -74,3 +77,76 @@ uint64            ::= <64-bit unsigned little endian integer>
   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 either `hook`, `function`, `rule`, `side_cond_entry`, `side_cond_exit`, or `kore_term`.
+
+
+## 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](./binary-kore-2.md) file.
+
+## Example
+### Definition
+
+```K
+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
+
+```Bash
+kompile add-rewrite.k --llvm-proof-hint-instrumentation
+krun input.add-rewrite --proof-hint > input.add-rewrite.hints
+```
+
+### Commands to print the Proof Trace in human-readable format
+
+```Bash
+kore-rich-header add-rewrite-kompiled/definition.kore > add-rewrite.header
+kore-proof-trace add-rewrite.header input.add-rewrite.hints --expand-terms --verbose
+```