Claim infer cell2

[radumereuta]

Fixes: #3656
Changes:

• add the <generatedCounter> cell only when a fresh variable is found or it has cells.
• don't do configuration concretization on claims unless it has cells.
• added an option to disable the check for functional claims. --allow-func-claims. I thought about disabling the check when --dry-run but I think that would be confusing. This option makes it explicit and obvious.

[dwightguth]

I'm not actually sure it's correct to only add the generatedCounter cell if you see a fresh variable. It's possible that the rules that are applied as part of rewriting the claim's lhs might mention the fresh counter. I believe this is why the change was made.

I think what you probably want to do instead is only add the cell if the claim already mentions at least one cell.

[ehildenb]

The generated JSON is what's needed, but in general functional claims should be translated th esame as functional simplification rules. So a claim like this (which has a function on LHS):

claim foo(X) => 3

Should be translated the same as a simplification rule like this:

rule foo(X) => 3 [simplification]

Can we use the same transformation steps for the claim as we do for this rule?

[radumereuta]

@ehildenb I've modified ModuleToKore to print the proper sorts in the generated kore format.
Now, there is only one proof that fails in regression-new/issue-2287-simpl-rules-in-kprovex

// rule n +Int n => #Top [simplification, comm]
// rule `_+Int_`(`n_TEST_Int`(.KList),`n_TEST_Int`(.KList))=>#Top{Int}(.KList) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f9026946c3cd15136d4049ac2b99ca58c6ac06b23fb9a56ae61b27374ee585fd), org.kframework.attributes.Location(Location(10,8,10,24)), org.kframework.attributes.Source(Source(/home/radu/work/k/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification]
  axiom{R} \implies{R} (
    \top{R}(),
    \equals{SortInt{},R} (
      Lbl'UndsPlus'Int'Unds'{}(Lbln'Unds'TEST'Unds'Int{}(),Lbln'Unds'TEST'Unds'Int{}()),
     \and{SortInt{}} (
       \top{SortInt{}}(),
        \top{SortInt{}}())))
  [UNIQUE'Unds'ID{}("f9026946c3cd15136d4049ac2b99ca58c6ac06b23fb9a56ae61b27374ee585fd"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(10,8,10,24)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/radu/work/k/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}(), simplification{}()]

// claim c => 2 #And n +Int n
// claim `c_TEST_S`(.KList)=>inj{Int,S}(#And{Int}(#token("2","Int"),`_+Int_`(`n_TEST_Int`(.KList),`n_TEST_Int`(.KList)))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(7743d42dfb5ef280532311b58b99a654f35553980b4795cec24172c95ac7490f), org.kframework.attributes.Location(Location(9,9,9,29)), org.kframework.attributes.Source(Source(/home/radu/work/k/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
  claim{} \implies{SortS{}} (
      \and{SortS{}} (
      \top{SortS{}}(), Lblc'Unds'TEST'Unds'S{}()), weakAlwaysFinally{SortS{}} (
      \and{SortS{}} (
      inj{SortInt{}, SortS{}}(\and{SortInt{}}(\dv{SortInt{}}("2"),Lbl'UndsPlus'Int'Unds'{}(Lbln'Unds'TEST'Unds'Int{}(),Lbln'Unds'TEST'Unds'Int{}()))), \top{SortS{}}())))
  [UNIQUE'Unds'ID{}("7743d42dfb5ef280532311b58b99a654f35553980b4795cec24172c95ac7490f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(9,9,9,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/radu/work/k/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}()]

This fails with:

/home/radu/work/k/k-distribution/bin/kprove a5-spec.k --no-exc-wrap  --definition ./test-kompiled 2>&1 | sed 's!'`pwd`'/\(\./\)\{0,2\}!!g' | diff - a5-spec.k.out
1,6c1
< kore-exec: [623813] Warning (WarnStuckClaimState):
<     The configuration's term doesn't unify with the destination's term and the configuration cannot be rewritten further. Location: a5-spec.k:9:9-9:29
< Context:
<     (InfoReachability) while checking the implication
< c
< [Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
---
> #Top
make: *** [../../../include/kframework/ktest.mak:117: a5-spec.k] Error 1

I also found this error message saying "Functional claims not yet supported." with a link to this haskell-backend issue.

[ehildenb]

Can you link to the test? Which is it? https://github.com/runtimeverification/k/tree/master/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex

It looks to me like that test (a5-spec.k) does not have a function symbol on the top of the LHS, but a constructor, and so it should be modified to have <k> c => ... </k> tags put around it. Maybe @dwightguth (original author of the test) can chime in.

[radumereuta]

@ehildenb there are a few inconsistencies that got me blocked on this one:

• you say that if I have a functional symbol on top of a claim, then I should not add the <k> cell. But functional claims are not supported. We have a check in ModuleToKore with this error message saying "Functional claims not yet supported." with a link to this Haskell backend supports functional claims directly haskell-backend#3010. @goodlyrottenapple @jberthold @geo2a is this still the case?
• you say this claim [claim1]: true => false should not be wrapped with the <k> cell, but that's not a function on the LHS; it's a token.

If you want this functionality sooner, I can implement it under an option. Otherwise, we need to clarify the expected kore output to ensure we don't break the tests.

[ehildenb]

• A claim like claim true => false, if it doesn't have the <k> cell, should probably not have it added. That's because the user didn't write it explicitely. Basically, we should turn off default explicit inference of the cell presence.
• Yes, the pyk prover now supports functional claims directly. I would just generate the appropriate functional claim, and let the backend crash if needed. If it's run with the pyk prover, it will be fine (because it discharges it via RPC comands rather than feeding the kclaim to the backend directly). I don't think we need the textual prover to support it. We could also have it be that if --dry-run is supplied, then it's allowed, and if --dry-run is not supplied (so it will actually try to call the backend), it crashes with that error.

[radumereuta]

@ehildenb I think these last changes should work for you.

We could also have it be that if --dry-run is supplied, then it's allowed

I've added a special option to enable this. --allow-func-claims. The user should be aware the behavior will be different.

This has the potential to break things. What would you like me to test it with? For now, I've only tested the integration tests.

[radumereuta]

Tested the EVM semantics with make test-prove-kprove and all tests passed.

[Baltoli]

LGTM now that my comments have been addressed

[dwightguth]

looks fine.