search

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 6 forks source link

Dexter build harness #198

Closed hjorthjort closed 3 years ago

hjorthjort commented 3 years ago

Closes #197

Build on #195 which should be merged first

To include the Michelson semantics, we include the <michelsonTop/> cell through compostion.

Just using the existing .build/defn/prove build causes a NullPointerException. I suspect it's because the new configuration symbols are not included in that compiled definition, and there is an error trying to parse or unparse them. It happens even if I set --output KORE, so I suspect it an parsing error rather than an unparsing error.

❯ ./kmich prove --backend prove tests/proofs/dexter/dexter.md DEXTER-VERIFICATION --spec-module DEXTER-SPEC --debug --output KORE                                      ─╯ 
+ kprove --directory /home/hjort/michelson-semantics/dev/.build/defn/prove tests/proofs/dexter/dexter.md --def-module DEXTER-VERIFICATION --debug --debug --spec-module DE
XTER-SPEC --output KORE                                                                                                                                                   
[Error] Internal: Uncaught exception thrown of type NullPointerException.                                                                                                 
Please rerun your program with the --debug flag to generate a stack trace, and                                                                                            
file a bug report at https://github.com/kframework/k/issues                                                                                                               
(NullPointerException: null)

To solve this we use a separate build for Dexter. Since we will likely add new syntax as well for loading and unloading the state, I made a DEXTER-VERIFICATION-SYNTAX submodule.

ehildenb commented 3 years ago

Let's run this proof on CI and fix the merge conflicts.