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.

Sign up for GitHub

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

Annotating rules that preserve definedness #2260

Merged
merged 21 commits into from
Feb 28, 2024
Merged

Annotating rules that preserve definedness #2260

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
93ecbeb
refactoring new account generation to ensure definedness preservation
PetarMax Jan 17, 2024
87fcb45
Set Version: 1.0.420
Jan 17, 2024
1ab9a57
Merge branch 'master' into preserving-definedness
PetarMax Jan 17, 2024
dda3a83
Set Version: 1.0.420
Jan 17, 2024
96d2d84
Merge branch 'master' into preserving-definedness
PetarMax Jan 18, 2024
b687d23
Set Version: 1.0.421
Jan 18, 2024
87346bc
Merge branch 'master' into preserving-definedness
PetarMax Jan 25, 2024
c00dd37
Set Version: 1.0.432
Jan 25, 2024
a10aeb8
Merge branch 'master' into preserving-definedness
anvacaru Jan 30, 2024
65d729d
Set Version: 1.0.433
Jan 30, 2024
1b0d819
Merge branch 'master' into preserving-definedness
PetarMax Feb 5, 2024
a80e62e
Set Version: 1.0.443
Feb 5, 2024
a0f0382
Merge branch 'master' into preserving-definedness
PetarMax Feb 15, 2024
04da00e
Set Version: 1.0.457
Feb 15, 2024
0e12056
Merge branch 'master' into preserving-definedness
PetarMax Feb 24, 2024
253c6fa
Set Version: 1.0.465
Feb 24, 2024
2e7a770
further annotations
PetarMax Feb 25, 2024
36f8e92
Bump SMT timeout to 500 in `test_pyk_prove`
palinatolmach Feb 26, 2024
be5f59e
Increased the SMT timeout to 1800 in `test_pyk_prove` to make `kontro…
palinatolmach Feb 26, 2024
b25d528
Change SMT timeout in `test_pyk_prove` to 1600
palinatolmach Feb 26, 2024
5784c19
Revert SMT timeout to 300 in tests, skip `test-arithmetictest-test_wm…
palinatolmach Feb 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kevm-pyk"
version = "1.0.464"
version = "1.0.465"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@
from typing import Final


VERSION: Final = '1.0.464'
VERSION: Final = '1.0.465'
30 changes: 17 additions & 13 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -749,10 +749,23 @@ These are just used by the other operators for shuffling local execution state a
```k
syntax InternalOp ::= "#newAccount" Int
| "#newExistingAccount" Int
| "#newFreshAccount" Int
// --------------------------------------------
rule <k> #newAccount ACCT => #newExistingAccount ACCT ... </k> <account> <acctID> ACCT </acctID> ... </account>
rule <k> #newAccount ACCT => #newFreshAccount ACCT ... </k> [owise]
rule <k> #newAccount ACCT => . ... </k>
<accounts>
( .Bag
=>
<account>
<acctID> ACCT </acctID>
<balance> 0 </balance>
<code> .Bytes:AccountCode </code>
<storage> .Map </storage>
<origStorage> .Map </origStorage>
<nonce> 0 </nonce>
</account>
)
...
</accounts> [owise, preserves-definedness]
Comment on lines +754 to +768
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

By moving this account creation here, the [owise] guarantees that ACCT is not in the <accounts> map, and the rule preserves definedness. Previosly, with the account creation isolated inside #newFreshAccount, which could be in principle called from anywhere, this would not hold.


rule <k> #newExistingAccount ACCT => #end EVMC_ACCOUNT_ALREADY_EXISTS ... </k>
<account>
Expand All @@ -773,17 +786,6 @@ These are just used by the other operators for shuffling local execution state a
...
</account>
requires lengthBytes(CODE) ==Int 0

rule <k> #newFreshAccount ACCT => .K ... </k>
<accounts>
( .Bag
=> <account>
<acctID> ACCT </acctID>
...
</account>
)
...
</accounts>
```

- `#transferFunds` moves money from one account into another, creating the destination account if it doesn't exist.
Expand Down Expand Up @@ -812,6 +814,7 @@ These are just used by the other operators for shuffling local execution state a
...
</account>
requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM
[preserves-definedness]

rule <k> #transferFunds ACCTFROM _ACCTTO VALUE => #end EVMC_BALANCE_UNDERFLOW ... </k>
<account>
Expand Down Expand Up @@ -1365,6 +1368,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
<accessedStorage> ... ACCT |-> (TS:Set => TS |Set SetItem(INDEX)) ... </accessedStorage>
<schedule> SCHED </schedule>
requires Ghasaccesslist << SCHED >>
[preserves-definedness]

rule <k> #accessStorage ACCT INDEX => .K ... </k>
<accessedStorage> TS => TS[ACCT <- SetItem(INDEX)] </accessedStorage>
Expand Down
2 changes: 1 addition & 1 deletion package/version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.0.464
1.0.465
1 change: 1 addition & 0 deletions tests/failing-symbolic.haskell-booster
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ tests/specs/functional/lemmas-no-smt-spec.k
tests/specs/functional/lemmas-spec.k
tests/specs/functional/merkle-spec.k
tests/specs/functional/storageRoot-spec.k
tests/specs/kontrol/test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k
tests/specs/mcd/dstoken-burn-self-fail-rough-spec.k
tests/specs/mcd/dstoken-transferfrom-fail-rough-spec.k
tests/specs/mcd/end-cash-pass-rough-spec.k
Expand Down
Loading