Skip to content

Commit

Permalink
Introducing proof hints feature to be used directly through kevm
Browse files Browse the repository at this point in the history
…binary or poetry. (#14)

Previously, we couldn't parse the `--proof-hints` flag to `krun` through
the poetry/`kevm` binary. As pyk now has support for calling `krun` with
this flag and returning `bytes` as expected, we can now call this new
function `run_proof_hint` and write the bytes to the stdout buffer.
  • Loading branch information
Robertorosmaninho committed Sep 12, 2024
1 parent 8ebf027 commit 1feffe4
Showing 1 changed file with 22 additions and 17 deletions.
39 changes: 22 additions & 17 deletions kevm-pyk/src/kevm_pyk/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -599,24 +599,29 @@ def exec_run(options: RunOptions) -> None:
)

if options.proof_hint:
kore_input = options.input_file.name.split('.')[0] + '.kore'
logging.warning('Proof hints are not supported in the pyk krun at the momment.')
logging.info('Saving the input file as %s', kore_input)
logging.info(
'If you want to emit hints take the krun command shown below and run it replacing the temp file by the kore file generated and append the `--proof-hint` flag to your command.'
logging.warning(
'Running KEVM with proof hint options enabled, remember to not use this with any `--verbose` mode if you are redirecting its output.'
)
output_bytes = kevm.run_proof_hint(
kore_pattern,
depth=options.depth,
parser='cat',
term=True,
expand_macros=options.expand_macros,
debugger=options.debugger,
proof_hint=True,
)
sys.stdout.buffer.write(output_bytes)
else:
kevm.run(
kore_pattern,
depth=options.depth,
term=True,
expand_macros=options.expand_macros,
output=options.output,
check=True,
debugger=options.debugger,
)
with open(kore_input, 'w') as f:
kore_pattern.write(f)

kevm.run(
kore_pattern,
depth=options.depth,
term=True,
expand_macros=options.expand_macros,
output=options.output,
check=True,
debugger=options.debugger,
)


def exec_kast(options: KastOptions) -> None:
Expand Down

0 comments on commit 1feffe4

Please sign in to comment.