Split proof hint trace into multiple files #1147
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds support for generating multiple hint trace files containing parts of the total trace. To this end, we add an optional
--proof-chunk-size N
flag to theinterpreter
binary. When the flag is passed andN
is greater than0
, then the trace is separated into multiple files as follows:<output filename>.pre_trace
file with the pre-trace events and the initial configuration.<output filename>.<idx>
files that each containN
top-level rewrite rule events along with their corresponding side condition events and simplification events. If theinterpreter
binary has been generated with the slow option, then each of these files also contains configuration events after each rewrite event. Note that the last file may contain less thanN
events.By default
N
equals to0
and in this case, the trace is generated exactly as before.This PR also adds support to the
kore_proof_trace
tool to be able to parse partial trace files. To achieve this, we introduce two more special headers (one for the pre-trace file and one for the chunk files) that allow the parser to recognize what kind of file it should expect.