Unexpected behaviour in proving sum-to-n-foundry-spec.k

[PetarMax]

The sum-to-n-foundry-spec.k file contains a circular proof of the usual sum of the first n integers. Currently, at the critical point, the branching that happens is unexpected to me and appears to require a lemma that I don't think should be required. I believe that Kore incorrectly returns a result that can then be interpreted as a split instead of a non-deterministic branch. The lemma in question is:

rule [rangeBool-not-zero-l]: notBool (X ==Int 0) => X ==Int 1 requires #rangeBool(X) [simplification]

The most important parts of the claim are the K cell and the word stack, and they are as expected:

<k>
  (JUMPI 1569 bool2Word(N:Int ==Int 0) ~> #pc [ JUMPI ] => .K)
  ~> #execute
  ...
</k>

<wordStack>
    (S => (S +Int ((N *Int (N +Int 1)) divInt 2)))
  : 0
  : (N => 0)
  : 334
  : 2123244496
  : .WordStack
</wordStack>

and the path condition is

{ true #Equals 0 <Int N:Int }
{ true #Equals 0 <=Int N:Int }
{ true #Equals 0 <=Int S:Int }
{ true #Equals N:Int <Int pow256 }
{ true #Equals S:Int <Int pow256 }
{ true #Equals ( 178 *Int N:Int ) <=Int GAS_AMT:Int }
{ true #Equals ( S:Int +Int ( ( ( N:Int *Int ( N:Int +Int 1 ) ) -Int ( ( N:Int *Int ( N:Int +Int 1 ) ) modInt 2 ) ) /Int 2 ) ) <Int pow256 } ) ) ) ) ) ) )

Now, the critical node in the proof is node 18, whose K cell and word stack are

<k>
  JUMPI 1569 bool2Word ( N:Int ==Int 1 )
  ~> #pc [ JUMPI ]
  ~> #execute
  ~> K_CELL_de090c3b:K
</k>

<wordStack>
  ( ( S:Int +Int N:Int ) : ( 0 : ( ( N:Int +Int -1 ) : ( 334 : ( 2123244496 : .WordStack ) ) ) ) )
</wordStack>

and whose path condition is the same as above. Without the lemma above, the execution branches into the following split:

┃ (branch)
┣━━┓ subst: .Subst
┃  ┃ constraint:
┃  ┃     ( ( S:Int +Int N:Int ) +Int ( ( ( ( N:Int +Int -1 ) *Int N:Int ) -Int ( ( ...
┃  ┃     ( S:Int +Int N:Int ) <Int pow256
┃  ┃     1 <Int N:Int
┃  ┃     N:Int <Int 115792089237316195423570985008687907853269984665640564039457584...
┃  ┃     ( 178 *Int ( N:Int +Int -1 ) ) <=Int ( GAS_AMT:Int +Int -178 )
┃  ┃     1 <=Int N:Int
┃  │
┃  └─ 19 (leaf, pending)
┃      k: JUMPI 1569 bool2Word ( N:Int ==Int 1 ) ~> #pc [ JUMPI ] ~> #execute ~> K_CELL_de ...
┃      pc: 1539
┃      callDepth: CALLDEPTH_CELL:Int
┃      statusCode: STATUSCODE_CELL:StatusCode
┃
┗━━┓ subst: .Subst
   ┃ constraint:
   ┃     notBool ( N:Int ==Int 0 )
   │
   └─ 20 (leaf, pending)
       k: JUMPI 1569 bool2Word ( N:Int ==Int 1 ) ~> #pc [ JUMPI ] ~> #execute ~> K_CELL_de ...
       pc: 1539
       callDepth: CALLDEPTH_CELL:Int
       statusCode: STATUSCODE_CELL:StatusCode

and since the second branch carries no additional information, the execution keeps branching infinitely. This appears to be a remainder branch of some kind, but the backend returns a non-empty rule predicate for every next state.

With the lemma above in place, Kore somehow uses it to make the split condition of node 20 become N ==Int 1. I have looked at all possible logs and I do not understand how.

As part of one of the latest PRs, I have added that lemma locally to that file so that it could pass, but I think that we should not have that lemma anywhere and that have a bug either in the backend reasoning or in the results returned by the backend or in how we interpret these results.

I am attaching the failing (without the lemma) and successful (with the lemma) bug reports for inspection by the backend team (@geo2a @goodlyrottenapple @jberthold).

succ.tar.gz
fail.tar.gz

[ehildenb]

So, notBool (N ==Int 0) is already implied by the prior path condition 0 <Int N, and so the first branch on N ==Int 0 is incorrect basically, it sohuld be vacuous?

[PetarMax]

I think that there is a remainder branch that gets incorrectly characterised with that notBool (N ==Int 0). I will explore further.

[PetarMax]

It is possible that it is vacuous, yes, because I think at that point the circularity should just apply for N mapped to N -Int 1.

[PetarMax]

In this branch

┃ (branch)
┣━━┓ subst: .Subst
┃  ┃ constraint:
┃  ┃     ( ( S:Int +Int N:Int ) +Int ( ( ( ( N:Int +Int -1 ) *Int N:Int ) -Int ( ( ...
┃  ┃     ( S:Int +Int N:Int ) <Int pow256
┃  ┃     1 <Int N:Int
┃  ┃     N:Int <Int 115792089237316195423570985008687907853269984665640564039457584...
┃  ┃     ( 178 *Int ( N:Int +Int -1 ) ) <=Int ( GAS_AMT:Int +Int -178 )
┃  ┃     1 <=Int N:Int
┃  │
┃  └─ 19 (leaf, pending)
┃      k: JUMPI 1569 bool2Word ( N:Int ==Int 1 ) ~> #pc [ JUMPI ] ~> #execute ~> K_CELL_de ...
┃      pc: 1539
┃      callDepth: CALLDEPTH_CELL:Int
┃      statusCode: STATUSCODE_CELL:StatusCode

the circularity gets applied.

[PetarMax]

@goodlyrottenapple and I have understood what's happening. There's an additional constraint in the path condition, N <=Int 1***, which is the negation of the requires of the circularity, and which both:

• Does not get propagated to the rule_predicate part of the response, which I think it should, and I would argue that the meaning of rule_predicate should be 'what must hold for this rule to be applied in this configuration' rather than 'requires clause of the rule'.
• Allows the simplification to fire, creating N ==Int 1 from notBool ( 0 ==Int N ) correctly.

***Technically, a disjunction of a bunch of negations, but in which the only disjunct to possibly hold is N <=Int 1.

[palinatolmach]

@PetarMax can we close it now that #2618 has been merged?

[PetarMax]

Well, the problem has not been fixed, but the test has.