Func claims translation to KORE

[radumereuta]

Translate functional claims into kore in a similar way we do for simplification rules

[radumereuta]

module TEST
    imports INT
    syntax Int ::= f ( Int ) [function, functional]
    rule f(1) => 2
endmodule

module SPEC
  imports TEST
  claim f(1) => 2
  rule  f(1) => 2 [simplification]
endmodule

[org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/radu/work/test/spec.k)")]
module SPEC

// imports
import TEST []


// claims
// claim `f(_)_TEST_Int_Int`(#token("1","Int"))=>#token("2","Int") requires #token("true","Bool") ensures #token("true","Bool") [org.kframework.attributes.Location(Location(3,9,3,18)), org.kframework.attributes.Source(Source(/home/radu/work/test/spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
  claim{R} \implies{R} (
    \top{R}(),
    \equals{SortInt{},R} (
      Lblf'LParUndsRParUnds'TEST'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1")),
     \and{SortInt{}} (
       \dv{SortInt{}}("2"),
        \top{SortInt{}}())))
  [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3,9,3,18)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/radu/work/test/spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}()]

// rule `f(_)_TEST_Int_Int`(#token("1","Int"))=>#token("2","Int") requires #token("true","Bool") ensures #token("true","Bool") [org.kframework.attributes.Location(Location(4,9,4,18)), org.kframework.attributes.Source(Source(/home/radu/work/test/spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification]
  axiom{R} \implies{R} (
    \top{R}(),
    \equals{SortInt{},R} (
      Lblf'LParUndsRParUnds'TEST'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1")),
     \and{SortInt{}} (
       \dv{SortInt{}}("2"),
        \top{SortInt{}}())))
  [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(4,9,4,18)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/radu/work/test/spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}(), simplification{}()]

endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1,1,5,10)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/radu/work/test/spec.k)")]

Calling kprove though crashes the haskell backend:

Executing [kore-exec, /home/radu/work/test/./test-kompiled/definition.kore, --module, TEST, --prove, /home/radu/work/test/./.kprove-2022-07-18-20-46-05-227-6ebedd82-dc71-4e0c-a35c-84fdfa7bd0f6/spec.kore, --spec-module, SPEC, --output, /home/radu/work/test/./.kprove-2022-07-18-20-46-05-227-6ebedd82-dc71-4e0c-a35c-84fdfa7bd0f6/result.kore]
Executing command: kore-exec /home/radu/work/test/./test-kompiled/definition.kore --module TEST --prove /home/radu/work/test/./.kprove-2022-07-18-20-46-05-227-6ebedd82-dc71-4e0c-a35c-84fdfa7bd0f6/spec.kore --spec-module SPEC --output /home/radu/work/test/./.kprove-2022-07-18-20-46-05-227-6ebedd82-dc71-4e0c-a35c-84fdfa7bd0f6/result.kore
kore-exec: [83394] Error (ErrorException):
    Prelude.undefined
    CallStack (from HasCallStack):
      error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err
      undefined, called at src/Kore/Claim/SomeClaim.hs:184:17 in kore-0.60.0.0-AfDbhwdKwsp4a4wsGSYVve:Kore.Claim.SomeClaim
Created bug report: kore-exec.tar.gz

[ana-pantilie]

Please add a warning for these kinds of claims that they're currently unsupported in the backend.

[radumereuta]

Warning message looks something like this. The haskell backend still fails though.
You should be able to test it more easily now.

kore-exec: [164228] Error (ErrorException):
    Unexpected empty set of claims.
    Possible explanation: the frontend and the backend don't agree on the representation of claims.
    CallStack (from HasCallStack):
      error, called at src/Kore/Exec.hs:800:26 in kore-0.60.0.0-32qEnrm4hFr1HXNMYza0uf:Kore.Exec
Created bug report: kore-exec.tar.gz
[Warning] Compiler: Functional claims not yet supported.
https://github.com/runtimeverification/haskell-backend/issues/3010
	Source(/home/radu/work/test/spec.k)
	Location(3,9,3,18)
	3 |	  claim f(1) => 2
	  .	        ^~~~~~~~~

[ana-pantilie]

Great, thank you!