Skip to content

Commit

Permalink
Drop . in favour of .K (#2309)
Browse files Browse the repository at this point in the history 
* Drop . in favour of .K

* Set Version: 1.0.459

---------

Co-authored-by: devops <[email protected]>
  • Loading branch information
@Baltoli
Baltoli and devops authored Feb 21, 2024
1 parent fbacafc commit bdcfe1c
Show file tree
Hide file tree
Showing 7 changed files with 150 additions and 150 deletions.
2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
View file
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.458"
version = "1.0.459"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@
from typing import Final


VERSION: Final = '1.0.458'
VERSION: Final = '1.0.459'
120 changes: 60 additions & 60 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
View file

Large diffs are not rendered by default.

122 changes: 61 additions & 61 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file

Large diffs are not rendered by default.

18 changes: 9 additions & 9 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ module EVM-OPTIMIZATIONS
rule
<kevm>
<k>
( #next[ PUSHZERO ] => . ) ...
( #next[ PUSHZERO ] => .K ) ...
</k>
<schedule>
SCHED
Expand Down Expand Up @@ -60,7 +60,7 @@ module EVM-OPTIMIZATIONS
rule
<kevm>
<k>
( #next[ PUSH(N) ] => . ) ...
( #next[ PUSH(N) ] => .K ) ...
</k>
<schedule>
SCHED
Expand Down Expand Up @@ -98,7 +98,7 @@ module EVM-OPTIMIZATIONS
rule
<kevm>
<k>
( #next[ DUP(N) ] => . ) ...
( #next[ DUP(N) ] => .K ) ...
</k>
<schedule>
SCHED
Expand Down Expand Up @@ -134,7 +134,7 @@ module EVM-OPTIMIZATIONS
rule
<kevm>
<k>
( #next[ SWAP(N) ] => . ) ...
( #next[ SWAP(N) ] => .K ) ...
</k>
<schedule>
SCHED
Expand Down Expand Up @@ -170,7 +170,7 @@ module EVM-OPTIMIZATIONS
rule
<kevm>
<k>
( #next[ ADD ] => . ) ...
( #next[ ADD ] => .K ) ...
</k>
<schedule>
SCHED
Expand Down Expand Up @@ -205,7 +205,7 @@ module EVM-OPTIMIZATIONS
rule
<kevm>
<k>
( #next[ SUB ] => . ) ...
( #next[ SUB ] => .K ) ...
</k>
<schedule>
SCHED
Expand Down Expand Up @@ -240,7 +240,7 @@ module EVM-OPTIMIZATIONS
rule
<kevm>
<k>
( #next[ AND ] => . ) ...
( #next[ AND ] => .K ) ...
</k>
<schedule>
SCHED
Expand Down Expand Up @@ -275,7 +275,7 @@ module EVM-OPTIMIZATIONS
rule
<kevm>
<k>
( #next[ LT ] => . ) ...
( #next[ LT ] => .K ) ...
</k>
<schedule>
SCHED
Expand Down Expand Up @@ -310,7 +310,7 @@ module EVM-OPTIMIZATIONS
rule
<kevm>
<k>
( #next[ GT ] => . ) ...
( #next[ GT ] => .K ) ...
</k>
<schedule>
SCHED
Expand Down
34 changes: 17 additions & 17 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ module STATE-UTILS
syntax EthereumCommand ::= "clearTX"
// ------------------------------------
rule <k> clearTX => . ... </k>
rule <k> clearTX => .K ... </k>
<output> _ => .Bytes </output>
<memoryUsed> _ => 0 </memoryUsed>
<callDepth> _ => 0 </callDepth>
Expand All @@ -52,7 +52,7 @@ module STATE-UTILS
syntax EthereumCommand ::= "clearBLOCK"
// ---------------------------------------
rule <k> clearBLOCK => . ... </k>
rule <k> clearBLOCK => .K ... </k>
<previousHash> _ => 0 </previousHash>
<ommersHash> _ => 0 </ommersHash>
<coinbase> _ => 0 </coinbase>
Expand All @@ -75,7 +75,7 @@ module STATE-UTILS
syntax EthereumCommand ::= "clearNETWORK"
// -----------------------------------------
rule <k> clearNETWORK => . ... </k>
rule <k> clearNETWORK => .K ... </k>
<statusCode> _ => .StatusCode </statusCode>
<accounts> _ => .Bag </accounts>
<messages> _ => .Bag </messages>
Expand All @@ -98,11 +98,11 @@ module STATE-UTILS
```k
syntax EthereumCommand ::= "load" JSON
// --------------------------------------
rule <k> load _DATA : { .JSONs } => . ... </k>
rule <k> load _DATA : { .JSONs } => .K ... </k>
rule <k> load DATA : { KEY : VALUE , REST } => load DATA : { KEY : VALUE } ~> load DATA : { REST } ... </k>
requires REST =/=K .JSONs andBool DATA =/=String "transaction"
rule <k> load _DATA : [ .JSONs ] => . ... </k>
rule <k> load _DATA : [ .JSONs ] => .K ... </k>
rule <k> load DATA : [ { TEST } , REST ] => load DATA : { TEST } ~> load DATA : [ REST ] ... </k>
```

Expand All @@ -113,7 +113,7 @@ Here we perform pre-proccesing on account data which allows "pretty" specificati
syntax EthereumCommand ::= "loadAccount" Int JSON
// -------------------------------------------------
rule <k> loadAccount _ { .JSONs } => . ... </k>
rule <k> loadAccount _ { .JSONs } => .K ... </k>
rule <k> loadAccount ACCT { "balance" : (BAL:Int), REST => REST } ... </k>
<account> <acctID> ACCT </acctID> <balance> _ => BAL </balance> ... </account>
Expand All @@ -136,13 +136,13 @@ Here we load the environmental information.
rule <k> load "env" : { KEY : ((VAL:String) => #parseHexWord(VAL)) } ... </k>
requires KEY in (SetItem("currentCoinbase") SetItem("previousHash"))
// ----------------------------------------------------------------------
rule <k> load "env" : { "currentCoinbase" : (CB:Int) } => . ... </k> <coinbase> _ => CB </coinbase>
rule <k> load "env" : { "currentDifficulty" : (DIFF:Int) } => . ... </k> <difficulty> _ => DIFF </difficulty>
rule <k> load "env" : { "currentGasLimit" : (GLIMIT:Int) } => . ... </k> <gasLimit> _ => GLIMIT </gasLimit>
rule <k> load "env" : { "currentNumber" : (NUM:Int) } => . ... </k> <number> _ => NUM </number>
rule <k> load "env" : { "previousHash" : (HASH:Int) } => . ... </k> <previousHash> _ => HASH </previousHash>
rule <k> load "env" : { "currentTimestamp" : (TS:Int) } => . ... </k> <timestamp> _ => TS </timestamp>
rule <k> load "env" : { "currentBaseFee" : (BF:Int) } => . ... </k> <baseFee> _ => BF </baseFee>
rule <k> load "env" : { "currentCoinbase" : (CB:Int) } => .K ... </k> <coinbase> _ => CB </coinbase>
rule <k> load "env" : { "currentDifficulty" : (DIFF:Int) } => .K ... </k> <difficulty> _ => DIFF </difficulty>
rule <k> load "env" : { "currentGasLimit" : (GLIMIT:Int) } => .K ... </k> <gasLimit> _ => GLIMIT </gasLimit>
rule <k> load "env" : { "currentNumber" : (NUM:Int) } => .K ... </k> <number> _ => NUM </number>
rule <k> load "env" : { "previousHash" : (HASH:Int) } => .K ... </k> <previousHash> _ => HASH </previousHash>
rule <k> load "env" : { "currentTimestamp" : (TS:Int) } => .K ... </k> <timestamp> _ => TS </timestamp>
rule <k> load "env" : { "currentBaseFee" : (BF:Int) } => .K ... </k> <baseFee> _ => BF </baseFee>
syntax KItem ::= "loadCallState" JSON
// -------------------------------------
Expand All @@ -157,13 +157,13 @@ Here we load the environmental information.
rule <k> loadCallState { "value" : VALUE:Int , REST => REST } ... </k> <callValue> _ => VALUE </callValue>
rule <k> loadCallState { "data" : DATA:Bytes, REST => REST } ... </k> <callData> _ => DATA </callData>
rule <k> loadCallState { .JSONs } => . ... </k>
rule <k> loadCallState { .JSONs } => .K ... </k>
```

The `"network"` key allows setting the fee schedule inside the test.

```k
rule <k> load "network" : SCHEDSTRING => . ... </k>
rule <k> load "network" : SCHEDSTRING => .K ... </k>
<schedule> _ => #asScheduleString(SCHEDSTRING) </schedule>
syntax Schedule ::= #asScheduleString ( String ) [function]
Expand Down Expand Up @@ -233,7 +233,7 @@ The `"rlp"` key loads the block information.
syntax EthereumCommand ::= "mkTX" Int
// -------------------------------------
rule <k> mkTX TXID => . ... </k>
rule <k> mkTX TXID => .K ... </k>
<chainID> CID </chainID>
<txOrder> ... (.List => ListItem(TXID)) </txOrder>
<txPending> ... (.List => ListItem(TXID)) </txPending>
Expand Down Expand Up @@ -294,7 +294,7 @@ The `"rlp"` key loads the block information.
syntax EthereumCommand ::= "loadTransaction" Int JSON
// -----------------------------------------------------
rule <k> loadTransaction _ { .JSONs } => . ... </k>
rule <k> loadTransaction _ { .JSONs } => .K ... </k>
rule <k> loadTransaction TXID { GLIMIT : TG:Int, REST => REST } ... </k>
<message> <msgID> TXID </msgID> <txGasLimit> _ => TG </txGasLimit> ... </message>
Expand Down
2 changes: 1 addition & 1 deletion package/version
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.0.458
1.0.459

0 comments on commit bdcfe1c

Please sign in to comment.