`kprove` with fresh variables

[Baltoli]

A user on Discord reports the following:

test.k:

module TEST-SYNTAX
    syntax Pgm ::= "quux"
endmodule

module TEST
    imports TEST-SYNTAX
    imports INT

    configuration <k> $PGM:Pgm </k>
        <c1> . </c1>
        <c2> . </c2>

    rule <k> quux => . </k>
        <c1> . => !C:Int </c1>
        <c2> . => !C:Int </c2>
endmodule

test-spec.k

requires "test.k"

module TEST-SPEC-SYNTAX
    imports TEST-SYNTAX

endmodule

module VERIFICATION
    imports K-EQUAL
    imports TEST-SPEC-SYNTAX
    imports TEST

endmodule

module TEST-SPEC
    imports VERIFICATION

    claim <k> quux => . </k>
        <c1> . => ?C </c1>
        <c2> . => ?C </c2>
endmodule

kprove output:

kore-exec: [384063] Warning (WarnStuckClaimState):
    The configuration's term unifies with the destination's term, but the implication check between the conditions has failed. Location: /mnt/c/Users/brown/Code/ktest/test-spec.k:18:11-20:27
Context:
    (InfoReachability) while checking the implication
  #Not ( {
    _DotVar1
  #Equals
    _DotVar1 +Int 1
  } )
#And
  <generatedTop>
    <k>
      .
    </k>
    <c1>
      _DotVar1:Int ~> .
    </c1>
    <c2>
      _DotVar1:Int ~> .
    </c2>
  </generatedTop>
[Error] Prover: backend terminated because the configuration cannot be
rewritten further. See output for more details

Should this proof go through? Can you write proofs over fresh variables like this?

[ehildenb]

It seems that what's happening is that for each occurrence of the fresh integer variable !C, we are incrementing the <generatedCounter> cell (which has contents _DotVar1 at the beginning of the proof.

So perhaps, in the code which handles fresh counters, we should inspect if the variables used have the same name, and if so, give it the same incremented value (rather than incrementing twice).

Currently, the rule:

    rule <k> quux => . </k>
        <c1> . => !C:Int </c1>
        <c2> . => !C:Int </c2>

Is probably getting compiled to:

    rule <k> quux => . </k>
        <c1> . => _DotVar1 </c1>
        <c2> . => _DotVar1 +Int 1 </c2>
        <generatedCounter> _DotVar1 => _DotVar1 +Int 1 +Int 1 </generatedCounter>

And it should be something more like:

    rule <k> quux => . </k>
        <c1> . => _DotVar1 </c1>
        <c2> . => _DotVar1 </c2>
        <generatedCounter> _DotVar1 => _DotVar1 +Int 1 </generatedCounter>

Because we see that !C is the same variable name used twice.

[ehildenb]

A workaround, ofr the moment, is something like this:

module TEST-SYNTAX
    imports INT-SYNTAX
    syntax Pgm ::= "quux" | quux ( Int )
endmodule

module TEST
    imports TEST-SYNTAX
    imports INT

    configuration <k> $PGM:Pgm </k>
        <c1> . </c1>
        <c2> . </c2>

    rule <k> quux => quux(!C:Int) </k>

    rule <k> quux(X) => . </k>
        <c1> . => X </c1>
        <c2> . => X </c2>
endmodule

[Baltoli]

• We should look at the compiled.txt and definition.kore to see where the issue is in the compilation pipeline.
  • The relevant part of the pipeline is ResolveFreshConstants

[radumereuta]

Here is the compiled.txt rule

rule `<generatedTop>`(
`<k>`(`quux_TEST-SYNTAX_Pgm`(.KList)=>.K),
`<c1>`(.K=>`freshInt(_)_INT_Int_Int`(`_+Int_`(#Fresh,#token("0","Int")))),
`<c2>`(.K=>`freshInt(_)_INT_Int_Int`(`_+Int_`(#Fresh,#token("0","Int")))),
`<generatedCounter>`(#Fresh=>`_+Int_`(#Fresh,#token("1","Int")))) requires #token("true","Bool") ensures #token("true","Bool") 
[UNIQUE_ID(d987aa50e1b11231a4df88ffd6e2823e221b1beb0ff844c724f798210cdf8ee7), org.kframework.attributes.Location(Location(13,10,15,31)), org.kframework.attributes.Source(Source(/home/radu/work/test/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]

[Baltoli]

Based on this, it appears that the rule is being compiled correctly. Need to also confirm what the final value of the generated counter cell is.

The question is then why the backend can't discharge { _DotVar #Equal _DotVar +Int 1 } as being #Bottom.

[Baltoli]

What is the value of the <generatedCounter> cell in the final configuration? @dwightguth reckons that this might be because the prover is trying to assert that the value of that cell does not change from start to end in the claim. It is not actually possible to mention that cell in a claim.

[Baltoli]

@ehildenb queries whether we can just change configuration completion for generatedCounter such that it implicitly contains _ => ?_. Perhaps better to explicitly state the effect on that cell - @dwightguth may have worked on this at some point but has not reached a solution.

[Baltoli]

In fact, that code may have landed - try writing the generated counter cell in the claim.

[Baltoli]

Confirmed that the the following spec goes through:

test.k:

module TEST-SYNTAX
    syntax Pgm ::= "quux"
endmodule

module TEST
    imports TEST-SYNTAX
    imports INT

    configuration <k> $PGM:Pgm </k>
        <c1> . </c1>
        <c2> . </c2>

    rule <k> quux => . </k>
        <c1> . => !C:Int </c1>
        <c2> . => !C:Int </c2>
endmodule

test-spec.k:

require "test.k"

module TEST-SPEC
    imports TEST

    claim <k> quux => . </k>
        <c1> . => ?C </c1>
        <c2> . => ?C </c2>
        <generatedCounter> _ => ?_ </generatedCounter>
endmodule

This confirms our suspicion that the problem is the prover trying to assert that the generated counter cell doesn't change, and that the suggested solution where we implicitly add:

<generatedCounter> _ => ?_ </generatedCounter>

to claims (where the user hasn't explicitly mentioned the cell already?) is probably correct.

This cell is compiler-generated so we probably want this to be handled by the compiler rather than a warning / error, but for our own purposes re. writing tests we want to keep the option open to mention the cell explicitly.