The Rewrites type definition generated for evm-semantics.llvm compiles in about 20 mins (after imports, patching ite and setting set_option maxHeartbeats 10000000).

Rewrite.txt

Where do the names of rewrite rules such as _43a65b8 come from?

Where do the names of rewrite rules such as _43a65b8 come from?

I guess from unnamed rules. But maybe it's better to have something like ruleN where N is the counter of how many rules there are. Otherwise proving things with this can get more convoluted.

A related question: Even if we named all rules in K definitions, will there be generated rules by the compiler that we cannot name?

Where do the names of rewrite rules such as _43a65b8 come from?

It's a prefix of the UNIQUE-ID generated by the frontend for each rule.

But maybe it's better to have something like ruleN where N is the counter of how many rules there are.

I can make that change, but that'll make it significantly harder to manually trace back and forth between K and Lean source. Right now you can look up the source and UNIQUE-ID attributes from compiled.txt or definition.kore, which provides the mapping. And it's easier to search for a unique string in those files then to navigate to the n-th match of a regex identifying rule axioms.

A related question: Even if we named all rules in K definitions, will there be generated rules by the compiler that we cannot name?

The only frontend-generated rules I can think of are heating-cooling rules, but they seem to have a label. Still, it's possible there are unlabeled generated rules.