Merge branch 'master' into _update-deps/runtimeverification/pyk

.github/workflows/master-push.yml

@@ -23,6 +23,7 @@ jobs:
         uses: actions/checkout@v3
         with:
           ref: ${{ github.event.push.head.sha }}
+          fetch-depth: 0
       - name: 'Upgrade bash'
         if: ${{ contains(matrix.os, 'macos') }}
         run: brew install bash
@@ -61,6 +62,7 @@ jobs:
         with:
           submodules: recursive
           ref: ${{ github.event.push.head.sha }}
+          fetch-depth: 0
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
@@ -119,6 +121,7 @@ jobs:
         uses: actions/checkout@v3
         with:
           ref: ${{ github.event.push.head.sha }}
+          fetch-depth: 0
       - name: 'Make Release'
         env:
          GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}

.github/workflows/test-pr.yml

@@ -56,6 +56,7 @@ jobs:
         uses: actions/checkout@v3
         with:
           submodules: true
+          fetch-depth: 0
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
       - name: 'Build kevm'
@@ -136,6 +137,7 @@ jobs:
         uses: actions/checkout@v3
         with:
           submodules: recursive
+          fetch-depth: 0
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
@@ -157,6 +159,7 @@ jobs:
         uses: actions/checkout@v3
         with:
           submodules: recursive
+          fetch-depth: 0
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
@@ -182,6 +185,7 @@ jobs:
         uses: actions/checkout@v3
         with:
           submodules: recursive
+          fetch-depth: 0
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:

.github/workflows/update-foundry-prove.yml

@@ -16,6 +16,7 @@ jobs:
           submodules: recursive
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
           ref: ${{ github.events.inputs.branch }}
+          fetch-depth: 0
       - name: 'Configure GitHub user'
         run: |
           git config user.name devops

.github/workflows/update-version.yml

@@ -21,6 +21,7 @@ jobs:
         with:
           submodules: recursive
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
+          fetch-depth: 0
       - name: 'Configure GitHub user'
         run: |
           git config user.name devops

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.274"
+version = "1.0.275"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kevm-pyk/src/kevm_pyk/utils.py

@@ -21,7 +21,6 @@
 from pyk.kore.rpc import KoreClient, KoreExecLogFormat, kore_server
 from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver
 from pyk.proof.equality import EqualityProof, EqualityProver
-from pyk.proof.proof import ProofStatus
 from pyk.utils import single
 
 if TYPE_CHECKING:
@@ -125,38 +124,30 @@ def kevm_prove(
                 cut_point_rules=cut_point_rules,
             )
             assert isinstance(proof, APRProof)
-            failure_nodes = proof.failing
-            if len(failure_nodes) == 0:
+            if proof.passed:
                 _LOGGER.info(f'Proof passed: {proof.id}')
                 return True
             else:
                 _LOGGER.error(f'Proof failed: {proof.id}')
                 return False
         elif type(prover) is EqualityProver:
             prover.advance_proof()
-            if prover.proof.status == ProofStatus.PASSED:
+            if prover.proof.passed:
                 _LOGGER.info(f'Proof passed: {prover.proof.id}')
                 return True
-            if prover.proof.status == ProofStatus.FAILED:
+            elif prover.proof.failed:
                 _LOGGER.error(f'Proof failed: {prover.proof.id}')
                 if type(proof) is EqualityProof:
                     _LOGGER.info(proof.pretty(kprove))
                 return False
-            if prover.proof.status == ProofStatus.PENDING:
+            else:
                 _LOGGER.info(f'Proof pending: {prover.proof.id}')
                 return False
         return False
 
     except Exception as e:
         _LOGGER.error(f'Proof crashed: {proof.id}\n{e}', exc_info=True)
         return False
-    failure_nodes = proof.pending + proof.failing
-    if len(failure_nodes) == 0:
-        _LOGGER.info(f'Proof passed: {proof.id}')
-        return True
-    else:
-        _LOGGER.error(f'Proof failed: {proof.id}')
-        return False
 
 
 def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> list[str]:

kevm-pyk/src/tests/integration/test_foundry_prove.py

@@ -328,7 +328,9 @@ def assert_or_update_show_output(show_res: str, expected_file: Path, *, update:
 
 
 def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool) -> None:
+    foundry = Foundry(foundry_root)
     test_id = 'AssumeTest.test_assume_false(uint256,uint256)'
+
     prove_res = foundry_prove(
         foundry_root,
         tests=[test_id],
@@ -338,7 +340,10 @@ def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool)
         max_iterations=4,
         reinit=True,
     )
-    assert_pass(test_id, prove_res)
+
+    proof = foundry.get_apr_proof(test_id)
+    assert proof.pending
+
     prove_res = foundry_prove(
         foundry_root,
         tests=[test_id],

package/debian/changelog

@@ -1,5 +1,6 @@
-kevm (1.0.274) unstable; urgency=medium
+kevm (1.0.275) unstable; urgency=medium
 
   * Initial Release.
 
  -- Everett Hildenbrandt <everett.hildenbrandt@runtimeverification.com> Tue, 16 Jul 2019 00:14:12 -0700
+

package/version

@@ -1 +1 @@
-1.0.274
+1.0.275