Rerun claims when the claim body or those of dependent claims changes #2099

nwatson22 · 2023-09-30T01:55:27Z

Part of #2088

Adds KClaimJob class, which wraps KClaim and computes a digest associated with each claim (to change whenever the claim changes on disk). Digest also depends on the digest of all dependent claims.
Adds init_claim_jobs to set up the KClaimJobs so they can easily access the digests of their dependencies to compute their own digest.

…aims

kevm-pyk/src/kevm_pyk/__main__.py

nwatson22 · 2023-10-02T22:58:47Z

I've realized there is an awkwardness when using this functionality. When a claim doesn't have an explicit label, we use the UNIQUE_ID attribute, which I'm assuming is some sort of hash of the claim body, and I don't have a better way to track claim identity. So if the claim is not labeled and changes, it will simply be treated as a new claim, and the system I implemented here will not kick in.

…rification/evm-semantics into noah/claims-invalidate

nwatson22 · 2023-10-04T16:08:14Z

Change this to not use digests, but just always use the unique id and store under directory that has the same name as the user-provided label

Edit: this wouldn't work to get dependencies between labeled claims because the UNIQUE_ID doesn't depend on the dependencies, so I guess the current approach is still what I'm leaning towards.

kevm-pyk/src/kevm_pyk/__main__.py

anvacaru

Looks good to me! 👍 Left a single comment, but feel free to ignore it.

Co-authored-by: Andrei Văcaru <[email protected]>

…#2099) * Rerun claims based on digest, computed from claim body + dependent claims * Set Version: 1.0.309 * Make KClaimJob a frozen class and cache digest * Set Version: 1.0.310 * Change to using frozenset * Raise exception when label is not found * Set Version: 1.0.310 * Set Version: 1.0.312 * Set Version: 1.0.314 * Set Version: 1.0.329 * Update kevm-pyk/src/kevm_pyk/__main__.py Co-authored-by: Andrei Văcaru <[email protected]> * Fix formatting * Set Version: 1.0.330 * Set Version: 1.0.331 * Set Version: 1.0.332 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]> Co-authored-by: rv-jenkins <[email protected]>

* add abi_array function * Set Version: 1.0.327 * use build_cons to concatenate list of types for array elements and struct fields * Set Version: 1.0.328 * Revert type of various functions back to KInner * add tests for dynamic array and struct function arguments * use build_cons to concatenate list of types for array elements and struct fields * Set Version: 1.0.328 * Revert type of various functions back to KInner * add the two argument type tests into the smoke test suite * Set Version: 1.0.334 * add the two argument type tests into the smoke test suite * Remove testing infrastructure related to kontrolx (#2135) * .gitignore, tests/specs/examples: commit bin-runtime files * kevm-pyk/test_prove: simplify compilation process now that we dont need to generate K code * .gitmodules: remove forge-std * kevm-pyk/: remove more references to foundry tests * kevm-pyk/src/tests/integration/test-data: remove references to foundry tests * kevm-pyk/src/tests/integration/test_{foundry_prove,solc_to_k}: remove unused files * Set Version: 1.0.326 * tests/foundry/lib/forge-std: remove submodule * Set Version: 1.0.328 --------- Co-authored-by: devops <[email protected]> * Remove `foundry.md` and the `foundry` target (#2142) * Remove `foundry.md` and the `foundry` target * Set Version: 1.0.329 --------- Co-authored-by: devops <[email protected]> * Bump Solidity version in README links. (#2139) * bump soliditylang docs version in readme * Set Version: 1.0.328 * Set Version: 1.0.329 * Set Version: 1.0.330 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> * Update dependency: deps/pyk_release (#2141) * deps/pyk_release: Set Version v0.1.480 * Set Version: 1.0.329 * kevm-pyk/: sync poetry files pyk version v0.1.480 * deps/k_release: sync release file version 6.0.164 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.481 * kevm-pyk/: sync poetry files pyk version v0.1.481 * deps/k_release: sync release file version 6.0.174 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.330 * kevm-pyk/: sync poetry files pyk version v0.1.481 * deps/pyk_release: Set Version v0.1.482 * kevm-pyk/: sync poetry files pyk version v0.1.482 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.483 * kevm-pyk/: sync poetry files pyk version v0.1.483 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.484 * kevm-pyk/: sync poetry files pyk version v0.1.484 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.485 * kevm-pyk/: sync poetry files pyk version v0.1.485 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.331 * deps/pyk_release: Set Version v0.1.486 * fix poetry2nix * kevm-pyk/: sync poetry files pyk version v0.1.486 * flake.{nix,lock}: update Nix derivations * minor tweak --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> Co-authored-by: Sam Balco <[email protected]> * Rerun claims when the claim body or those of dependent claims changes (#2099) * Rerun claims based on digest, computed from claim body + dependent claims * Set Version: 1.0.309 * Make KClaimJob a frozen class and cache digest * Set Version: 1.0.310 * Change to using frozenset * Raise exception when label is not found * Set Version: 1.0.310 * Set Version: 1.0.312 * Set Version: 1.0.314 * Set Version: 1.0.329 * Update kevm-pyk/src/kevm_pyk/__main__.py Co-authored-by: Andrei Văcaru <[email protected]> * Fix formatting * Set Version: 1.0.330 * Set Version: 1.0.331 * Set Version: 1.0.332 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]> Co-authored-by: rv-jenkins <[email protected]> * Remove option to skip simplifing init nodes (#2138) * kevm-pyk/{cli,__main__}: remove options --[no-]simplify-init * kevm-pyk/__main__: setup temporary directory for saving proofs if needed * Set Version: 1.0.328 * Set Version: 1.0.329 * Set Version: 1.0.331 * Set Version: 1.0.332 * Set Version: 1.0.333 * kevm-pyk/test_prove: remove kserver --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]> * Set Version: 1.0.334 * increase test suite time limit by 30 minutes * Set Version: 1.0.336 * increase ci timeout * add abi_array function * add tests for dynamic array and struct function arguments * use build_cons to concatenate list of types for array elements and struct fields * Revert type of various functions back to KInner * add the two argument type tests into the smoke test suite * increase ci timeout * Set Version: 1.0.341 * Set Version: 1.0.348 * Set Version: 1.0.349 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> Co-authored-by: Tamás Tóth <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: Sam Balco <[email protected]> Co-authored-by: Noah Watson <[email protected]> Co-authored-by: Freeman <[email protected]>

Rerun claims based on digest, computed from claim body + dependent cl…

14f2ff4

…aims

nwatson22 self-assigned this Sep 30, 2023

nwatson22 and others added 2 commits September 29, 2023 20:55

Merge branch 'master' into noah/claims-invalidate

c0a6147

Set Version: 1.0.309

382420d

nwatson22 requested review from h0nzZik, ehildenb, tothtamas28 and palinatolmach September 30, 2023 02:23

nwatson22 marked this pull request as ready for review September 30, 2023 02:23

anvacaru reviewed Oct 2, 2023

View reviewed changes

kevm-pyk/src/kevm_pyk/__main__.py Outdated Show resolved Hide resolved

anvacaru reviewed Oct 2, 2023

View reviewed changes

kevm-pyk/src/kevm_pyk/__main__.py Show resolved Hide resolved

nwatson22 and others added 5 commits October 2, 2023 18:34

Make KClaimJob a frozen class and cache digest

b1c5c74

Set Version: 1.0.310

f64639e

Change to using frozenset

f7c9df1

Merge branch 'noah/claims-invalidate' of https://github.com/runtimeve…

8b228ce

…rification/evm-semantics into noah/claims-invalidate

Raise exception when label is not found

fb6cc81

nwatson22 requested a review from anvacaru October 3, 2023 01:14

nwatson22 and others added 4 commits October 2, 2023 20:14

Merge branch 'master' into noah/claims-invalidate

89f2c06

Set Version: 1.0.310

6392d20

Merge branch 'master' into noah/claims-invalidate

569160c

Set Version: 1.0.312

7446c6a

nwatson22 and others added 4 commits October 6, 2023 19:26

Merge branch 'master' into noah/claims-invalidate

f8362ba

Set Version: 1.0.314

80fd6b8

Merge branch 'master' into noah/claims-invalidate

d1ffb8b

Set Version: 1.0.329

f4ba050

anvacaru reviewed Oct 27, 2023

View reviewed changes

kevm-pyk/src/kevm_pyk/__main__.py Outdated Show resolved Hide resolved

anvacaru approved these changes Oct 27, 2023

View reviewed changes

Update kevm-pyk/src/kevm_pyk/__main__.py

4c5bb31

Co-authored-by: Andrei Văcaru <[email protected]>

Fix formatting

d007502

nwatson22 added the automerge label Oct 27, 2023

rv-jenkins and others added 4 commits October 27, 2023 16:42

Merge branch 'master' into noah/claims-invalidate

0a1af44

Set Version: 1.0.330

faff6b4

Merge branch 'master' into noah/claims-invalidate

97991a1

Set Version: 1.0.331

0703fe2

yale-vinson mentioned this pull request Oct 30, 2023

Issues running kclaim style proofs #2088

Open

3 tasks

nwatson22 and others added 2 commits October 30, 2023 16:16

Merge branch 'master' into noah/claims-invalidate

c610bb2

Set Version: 1.0.332

dded76e

rv-jenkins merged commit f8051d5 into master Oct 31, 2023
11 checks passed

rv-jenkins deleted the noah/claims-invalidate branch October 31, 2023 00:31

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rerun claims when the claim body or those of dependent claims changes #2099

Rerun claims when the claim body or those of dependent claims changes #2099

nwatson22 commented Sep 30, 2023 •

edited

Loading

nwatson22 commented Oct 2, 2023

nwatson22 commented Oct 4, 2023 •

edited

Loading

anvacaru left a comment

Rerun claims when the claim body or those of dependent claims changes #2099

Rerun claims when the claim body or those of dependent claims changes #2099

Conversation

nwatson22 commented Sep 30, 2023 • edited Loading

nwatson22 commented Oct 2, 2023

nwatson22 commented Oct 4, 2023 • edited Loading

anvacaru left a comment

Choose a reason for hiding this comment

nwatson22 commented Sep 30, 2023 •

edited

Loading

nwatson22 commented Oct 4, 2023 •

edited

Loading