Inconsistency between --concrete-rules and [concrete] attribute

[Baltoli]

@jberthold reports on Slack that a KEVM rule is getting the concrete attribute applied during compilation.

We narrowed this down to the set of concrete rules passed by the kompile Python code: https://github.com/runtimeverification/evm-semantics/blob/d893b31867b1b73941dc7091bfa13e520841a94e/kevm-pyk/src/kevm_pyk/kompile.py#L50

Jost also identifies that the kompile pipeline may complain if you add the concrete attribute by hand to this rule, which suggests we might consider looking at the ordering of passes here.

There is also a question of why the old Haskell backend handles this case OK.

Things to investigate:

• Haskell backend old behaviour
• Warning if attribute specified by hand
• Correct solution - apply to owise branch for same production automatically? Not clear what we want to do here

[jberthold]

Definitely a discrepancy between manual insertion of concrete and using the flag:

test.k with concrete attribute:

module TEST
  imports K-EQUAL
  syntax Thing ::= "a" [token]
                 | "b" [token]
                 | "c" [token]
  syntax Thing ::= f ( Thing ) [ function, total ]

  rule [f-of-a-is-b] :  f(A) => b requires A ==K a [concrete]
  rule [f-otherwise] : f(_) => c                   [owise]
endmodule

jost@freshcode-1:~/work/RV/code/scratch/concrete-bug$ kompile test.k
[Error] Compiler: Found concrete attribute without simplification attribute on
function with one or more non-concrete rules.
	Source(/home/jost/work/RV/code/scratch/concrete-bug/test.k)
	Location(10,25,10,51)
	10 |	  rule [f-of-a-is-b] :  f(A) => b requires A ==K a [concrete]
	   .	                        ^~~~~~~~~~~~~~~~~~~~~~~~~~
[Error] Compiler: Had 1 structural errors.
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition.  Use --syntax-module to specify one. Using TEST as default.

test.k without concrete attribute, compiled with --concrete-rules flag

module TEST
  imports K-EQUAL
  syntax Thing ::= "a" [token]
                 | "b" [token]
                 | "c" [token]
  syntax Thing ::= f ( Thing ) [ function, total ]

  rule [f-of-a-is-b] :  f(A) => b requires A ==K a // [concrete]
  rule [f-otherwise] : f(_) => c                   [owise]
endmodule

jost@freshcode-1:~/work/RV/code/scratch/concrete-bug$ kompile test.k --concrete-rules TEST.f-of-a-is-b
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition.  Use --syntax-module to specify one. Using TEST as default.
jost@freshcode-1:~/work/RV/code/scratch/concrete-bug$ grep f-of-a-is-b test-kompiled/definition.kore  | grep -o -e " concrete.........................."
 concrete, label(TEST.f-of-a-is-b),
 concrete{}(), org'Stop'kframework'

[jberthold]

The kore backend does not apply the owise rule (in the example where this was found) because it considers an antiLeft predicate generated from the other rule's requirement. The new backend skips the antiLeft check and therefore erroneously proceeds to applying the owise rule.

[Baltoli]

This is a phase-ordering problem in the frontend; either we:

1. Modify the order / run the concrete attribute check after the concrete-rules check (not preferred)
2. Extract the --concrete-rules information in the attribute checker (preferred)

[Scott-Guest]

Closed by #3467