Skip to content
This repository has been archived by the owner on Apr 25, 2024. It is now read-only.

Update dependency: deps/k_release #649

Merged
merged 44 commits into from
Sep 27, 2023

Conversation

rv-jenkins
Copy link
Contributor

@rv-jenkins rv-jenkins commented Sep 13, 2023

pyproject.toml Outdated Show resolved Hide resolved
@tothtamas28
Copy link
Collaborator

tothtamas28 commented Sep 21, 2023

Regression analysis

CI failure: https://github.com/runtimeverification/pyk/actions/runs/6254778017/job/16982998891

Caused by: runtimeverification/haskell-backend#3650

Bug reports:

Proofs in pretty format:


The pretty-printed proofs are the same up until node 8 (inclusive):

   │  (1 step)
   ├─ 8
   │     <generatedTop>
   │       <T>
   │         <k>
   │           if ( 0 <= $n ) { { $s = $s + $n ; $n = $n + -1 ; } while ( 0 <= $n ) { $s = $s + $n ; $n = $n + -1 ; } } else { }
   │           ~> K_CELL_de090c3b:K
   │         </k>
   │         <state>
   │           $n |-> N:Int +Int -1 $s |-> S:Int +Int N:Int
   │         </state>
   │       </T>
   │       <generatedCounter>
   │         GENERATEDCOUNTER_CELL_c84b0b5f:Int
   │       </generatedCounter>
   │     </generatedTop>
   │     #And { true #Equals 0 <=Int N:Int }
   │     #And #Not ( { true #Equals 0 <=Int N:Int +Int -1 } )
   │

From there, the old version proceeds 7 steps:

   │  (7 steps)
   ├─ 9
   │     <generatedTop>
   │       <T>
   │         <k>
   │           { }
   │           ~> K_CELL_de090c3b:K
   │         </k>
   │         <state>
   │           $n |-> N:Int +Int -1 $s |-> S:Int +Int N:Int
   │         </state>
   │       </T>
   │       <generatedCounter>
   │         GENERATEDCOUNTER_CELL_c84b0b5f:Int
   │       </generatedCounter>
   │     </generatedTop>
   │     #And { true #Equals 0 <=Int N:Int }
   │     #And { false #Equals 0 <=Int N:Int +Int -1 }
   │

and eventually reaches the target.

The new version on the other hand gets stuck after 6 steps:

   │  (6 steps)
   └─ 9 (stuck, leaf)
         <generatedTop>
           <T>
             <k>
               if ( 0 <=Int N:Int +Int -1 ) { { $s = $s + $n ; $n = $n + -1 ; } while ( 0 <= $n ) { $s = $s + $n ; $n = $n + -1 ; } } else { }
               ~> K_CELL_de090c3b:K
             </k>
             <state>
               $n |-> N:Int +Int -1 $s |-> S:Int +Int N:Int
             </state>
           </T>
           <generatedCounter>
             GENERATEDCOUNTER_CELL_c84b0b5f:Int
           </generatedCounter>
         </generatedTop>
         #And { true #Equals 0 <=Int N:Int }
         #And #Not ( { true #Equals 0 <=Int N:Int +Int -1 } )

@tothtamas28 tothtamas28 merged commit 5fbb725 into master Sep 27, 2023
@tothtamas28 tothtamas28 deleted the _update-deps/runtimeverification/k branch September 27, 2023 12:01
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
Closes
runtimeverification/haskell-backend#3662

~Blocked by: #3646

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Regression in pyk integration tests
3 participants