runtimeverification / kasmer-multiversx

Wasm semantics for the Elrond/MultiversX blockchain network
BSD 3-Clause "New" or "Revised" License
0 stars 0 forks source link

Set custom indexing when running proofs with booster #148

Closed jberthold closed 3 months ago

jberthold commented 3 months ago

By default, booster will index rewrite rules by the head of the K cell (i.e., the first cell named <k> that is found in the configuration).

For MX-Backend, we should also, and more importantly, index the <instrs> and <commands> cells, this PR adds the option to do so. In the long term, the index cells should be indicated in a definition attribute by the compiler, but it is easier to adjust them explicitly for the time being.