Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
PetarMax opened this issue Sep 10, 2024 · 7 comments
Open

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

PetarMax opened this issue Sep 10, 2024 · 7 comments
Labels
bug Something isn't working

Comments

@PetarMax
Copy link
Contributor

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

@PetarMax PetarMax added the bug Something isn't working label Sep 10, 2024
@ehildenb
Copy link
Member

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
Copy link
Contributor Author

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

@PetarMax
Copy link
Contributor Author

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
Copy link
Contributor Author

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
Copy link
Contributor Author

@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
Copy link
Contributor

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

@PetarMax
Copy link
Contributor Author

PetarMax commented Oct 7, 2024

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

3 participants