-
Notifications
You must be signed in to change notification settings - Fork 143
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* 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 <devops@runtimeverification.com> * Remove `foundry.md` and the `foundry` target (#2142) * Remove `foundry.md` and the `foundry` target * Set Version: 1.0.329 --------- Co-authored-by: devops <devops@runtimeverification.com> * 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 <devops@runtimeverification.com> Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> * 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 <devops@runtimeverification.com> Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> Co-authored-by: Sam Balco <goodlyrottenapple@gmail.com> * 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 <16517508+anvacaru@users.noreply.github.com> * Fix formatting * Set Version: 1.0.330 * Set Version: 1.0.331 * Set Version: 1.0.332 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com> * 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 <devops@runtimeverification.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com> * 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 <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com> Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com> Co-authored-by: Sam Balco <goodlyrottenapple@gmail.com> Co-authored-by: Noah Watson <107630091+nwatson22@users.noreply.github.com> Co-authored-by: Freeman <105403280+F-WRunTime@users.noreply.github.com>
- Loading branch information
1 parent
630d136
commit 7b04335
Showing
11 changed files
with
297 additions
and
12 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -6,4 +6,4 @@ | |
from typing import Final | ||
|
||
|
||
VERSION: Final = '1.0.348' | ||
VERSION: Final = '1.0.349' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1 @@ | ||
1.0.348 | ||
1.0.349 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,128 @@ | ||
requires "verification.k" | ||
|
||
module DYNAMICARRAY00-SPEC | ||
imports VERIFICATION | ||
|
||
// fn-execute | ||
claim | ||
<k> (#execute => #halt) ~> _ </k> | ||
<exit-code> 1 </exit-code> | ||
<mode> NORMAL </mode> | ||
<schedule> ISTANBUL </schedule> | ||
<ethereum> | ||
<evm> | ||
<output> _ => #encodeArgs(#uint256(3)) </output> | ||
<statusCode> _ => EVMC_SUCCESS </statusCode> | ||
<callStack> _ </callStack> | ||
<interimStates> _ </interimStates> | ||
<touchedAccounts> _ => ?_ </touchedAccounts> | ||
<callState> | ||
<program> #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") </program> | ||
<jumpDests> #computeValidJumpDests(#parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029")) </jumpDests> | ||
<id> CONTRACT_ID </id> // this | ||
<caller> MSG_SENDER </caller> // msg.sender | ||
<callData> #abiCallData2("execute(uint256[])", #array(#uint256(1), 3, #uint256(A0), #uint256(A1), #uint256(A2), .TypedArgs)) </callData> // msg.data | ||
<callValue> 0 </callValue> // msg.value | ||
<wordStack> .WordStack => ?_ </wordStack> | ||
<localMem> .Bytes => ?_ </localMem> | ||
<pc> 0 => ?_ </pc> | ||
<gas> #gas(_VGAS) => ?_ </gas> | ||
<memoryUsed> 0 => ?_ </memoryUsed> | ||
<callGas> _ => ?_ </callGas> | ||
<static> false </static> // NOTE: non-static call | ||
<callDepth> CD </callDepth> | ||
</callState> | ||
<substate> | ||
<selfDestruct> _ </selfDestruct> | ||
<log> _ </log> | ||
<refund> _ </refund> | ||
<accessedAccounts> _ => ?_ </accessedAccounts> | ||
<accessedStorage> _ => ?_ </accessedStorage> | ||
</substate> | ||
<gasPrice> _ </gasPrice> | ||
<origin> _ </origin> // tx.origin | ||
<blockhashes> _BLOCK_HASHES </blockhashes> // block.blockhash | ||
<block> | ||
<previousHash> _ </previousHash> | ||
<ommersHash> _ </ommersHash> | ||
<coinbase> _ </coinbase> // block.coinbase | ||
<stateRoot> _ </stateRoot> | ||
<transactionsRoot> _ </transactionsRoot> | ||
<receiptsRoot> _ </receiptsRoot> | ||
<logsBloom> _ </logsBloom> | ||
<difficulty> _ </difficulty> | ||
<number> BLOCK_NUM </number> // block.number | ||
<gasLimit> _ </gasLimit> | ||
<gasUsed> _ </gasUsed> | ||
<timestamp> NOW </timestamp> // now = block.timestamp | ||
<extraData> _ </extraData> | ||
<mixHash> _ </mixHash> | ||
<blockNonce> _ </blockNonce> | ||
<baseFee> _ </baseFee> | ||
<ommerBlockHeaders> _ </ommerBlockHeaders> | ||
<withdrawalsRoot> _ </withdrawalsRoot> | ||
</block> | ||
</evm> | ||
<network> | ||
<chainID> _ </chainID> | ||
|
||
<accounts> | ||
<account> | ||
<acctID> CONTRACT_ID </acctID> | ||
<balance> CONTRACT_BAL </balance> | ||
<code> #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") </code> | ||
<storage> | ||
_ | ||
</storage> | ||
<origStorage> | ||
_ | ||
</origStorage> | ||
<nonce> CONTRACT_NONCE </nonce> | ||
</account> | ||
|
||
<account> | ||
<acctID> CALLEE_ID </acctID> | ||
<balance> CALLEE_BAL </balance> | ||
<code> _ </code> | ||
<storage> | ||
_ | ||
</storage> | ||
<origStorage> | ||
_ | ||
</origStorage> | ||
<nonce> CALLEE_NONCE </nonce> | ||
</account> | ||
|
||
<account> | ||
// precompiled account for ECCREC | ||
<acctID> 1 </acctID> | ||
<balance> 0 </balance> | ||
<code> .Bytes </code> | ||
<storage> .Map </storage> | ||
<origStorage> .Map </origStorage> | ||
<nonce> 0 </nonce> | ||
</account> | ||
|
||
|
||
... | ||
</accounts> | ||
<txOrder> _ </txOrder> | ||
<txPending> _ </txPending> | ||
<messages> _ </messages> | ||
</network> | ||
</ethereum> | ||
requires #rangeAddress(CONTRACT_ID) | ||
andBool #rangeAddress(CALLEE_ID) | ||
andBool #rangeUInt(256, NOW) | ||
andBool #rangeUInt(128, BLOCK_NUM) // Solidity | ||
andBool #rangeUInt(256, CONTRACT_BAL) | ||
andBool #rangeUInt(256, CALLEE_BAL) | ||
andBool #rangeNonce(CONTRACT_NONCE) | ||
andBool #rangeNonce(CALLEE_NONCE) | ||
andBool #range(0 <= CD < 1024) | ||
andBool #rangeAddress(MSG_SENDER) | ||
andBool #rangeUInt(256, A0) | ||
andBool #rangeUInt(256, A1) | ||
andBool #rangeUInt(256, A2) | ||
|
||
endmodule |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
pragma solidity 0.4.24; | ||
contract dynamicarray00 { | ||
function execute(uint[] a) public returns (uint) { | ||
return a.length; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,127 @@ | ||
requires "verification.k" | ||
|
||
module STRUCTARG00-SPEC | ||
imports VERIFICATION | ||
|
||
// fn-execute | ||
claim | ||
<k> (#execute => #halt) ~> _ </k> | ||
<exit-code> 1 </exit-code> | ||
<mode> NORMAL </mode> | ||
<schedule> ISTANBUL </schedule> | ||
<ethereum> | ||
<evm> | ||
<output> _ => #encodeArgs(#uint256(A0)) </output> | ||
<statusCode> _ => EVMC_SUCCESS </statusCode> | ||
<callStack> _ </callStack> | ||
<interimStates> _ </interimStates> | ||
<touchedAccounts> _ => ?_ </touchedAccounts> | ||
<callState> | ||
<program> #parseByteStack("0x6080604052600436106100245760003560e01c63ffffffff168063dd77d08e14610029575b600080fd5b34801561003557600080fd5b506100496100443660046100c9565b61005f565b60405161005691906100fe565b60405180910390f35b5190565b60006040828403121561007557600080fd5b61007f6040610112565b9050600061008d84846100aa565b825250602061009e848483016100bd565b60208301525092915050565b60006100b68235610139565b9392505050565b60006100b6823561013c565b6000604082840312156100db57600080fd5b60006100e78484610063565b949350505050565b6100f881610139565b82525050565b6020810161010c82846100ef565b92915050565b60405181810167ffffffffffffffff8111828210171561013157600080fd5b604052919050565b90565b60ff16905600a265627a7a723058206cff7fc5f1eee5a02118c03209b136de08c05265f52541d16a578e6ff695a84b6c6578706572696d656e74616cf50037") </program> | ||
<jumpDests> #computeValidJumpDests(#parseByteStack("0x6080604052600436106100245760003560e01c63ffffffff168063dd77d08e14610029575b600080fd5b34801561003557600080fd5b506100496100443660046100c9565b61005f565b60405161005691906100fe565b60405180910390f35b5190565b60006040828403121561007557600080fd5b61007f6040610112565b9050600061008d84846100aa565b825250602061009e848483016100bd565b60208301525092915050565b60006100b68235610139565b9392505050565b60006100b6823561013c565b6000604082840312156100db57600080fd5b60006100e78484610063565b949350505050565b6100f881610139565b82525050565b6020810161010c82846100ef565b92915050565b60405181810167ffffffffffffffff8111828210171561013157600080fd5b604052919050565b90565b60ff16905600a265627a7a723058206cff7fc5f1eee5a02118c03209b136de08c05265f52541d16a578e6ff695a84b6c6578706572696d656e74616cf50037")) </jumpDests> | ||
<id> CONTRACT_ID </id> // this | ||
<caller> MSG_SENDER </caller> // msg.sender | ||
<callData> #abiCallData2("execute((uint256,uint8))", #tuple(#uint256(A0), #uint8(A1), .TypedArgs)) </callData> // msg.data | ||
<callValue> 0 </callValue> // msg.value | ||
<wordStack> .WordStack => ?_ </wordStack> | ||
<localMem> .Bytes => ?_ </localMem> | ||
<pc> 0 => ?_ </pc> | ||
<gas> #gas(_VGAS) => ?_ </gas> | ||
<memoryUsed> 0 => ?_ </memoryUsed> | ||
<callGas> _ => ?_ </callGas> | ||
<static> false </static> // NOTE: non-static call | ||
<callDepth> CD </callDepth> | ||
</callState> | ||
<substate> | ||
<selfDestruct> _ </selfDestruct> | ||
<log> _ </log> | ||
<refund> _ </refund> | ||
<accessedAccounts> _ => ?_ </accessedAccounts> | ||
<accessedStorage> _ => ?_ </accessedStorage> | ||
</substate> | ||
<gasPrice> _ </gasPrice> | ||
<origin> _ </origin> // tx.origin | ||
<blockhashes> _BLOCK_HASHES </blockhashes> // block.blockhash | ||
<block> | ||
<previousHash> _ </previousHash> | ||
<ommersHash> _ </ommersHash> | ||
<coinbase> _ </coinbase> // block.coinbase | ||
<stateRoot> _ </stateRoot> | ||
<transactionsRoot> _ </transactionsRoot> | ||
<receiptsRoot> _ </receiptsRoot> | ||
<logsBloom> _ </logsBloom> | ||
<difficulty> _ </difficulty> | ||
<number> BLOCK_NUM </number> // block.number | ||
<gasLimit> _ </gasLimit> | ||
<gasUsed> _ </gasUsed> | ||
<timestamp> NOW </timestamp> // now = block.timestamp | ||
<extraData> _ </extraData> | ||
<mixHash> _ </mixHash> | ||
<blockNonce> _ </blockNonce> | ||
<baseFee> _ </baseFee> | ||
<ommerBlockHeaders> _ </ommerBlockHeaders> | ||
<withdrawalsRoot> _ </withdrawalsRoot> | ||
</block> | ||
</evm> | ||
<network> | ||
<chainID> _ </chainID> | ||
|
||
<accounts> | ||
<account> | ||
<acctID> CONTRACT_ID </acctID> | ||
<balance> CONTRACT_BAL </balance> | ||
<code> #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") </code> | ||
<storage> | ||
_ | ||
</storage> | ||
<origStorage> | ||
_ | ||
</origStorage> | ||
<nonce> CONTRACT_NONCE </nonce> | ||
</account> | ||
|
||
<account> | ||
<acctID> CALLEE_ID </acctID> | ||
<balance> CALLEE_BAL </balance> | ||
<code> _ </code> | ||
<storage> | ||
_ | ||
</storage> | ||
<origStorage> | ||
_ | ||
</origStorage> | ||
<nonce> CALLEE_NONCE </nonce> | ||
</account> | ||
|
||
<account> | ||
// precompiled account for ECCREC | ||
<acctID> 1 </acctID> | ||
<balance> 0 </balance> | ||
<code> .Bytes </code> | ||
<storage> .Map </storage> | ||
<origStorage> .Map </origStorage> | ||
<nonce> 0 </nonce> | ||
</account> | ||
|
||
|
||
... | ||
</accounts> | ||
<txOrder> _ </txOrder> | ||
<txPending> _ </txPending> | ||
<messages> _ </messages> | ||
</network> | ||
</ethereum> | ||
requires #rangeAddress(CONTRACT_ID) | ||
andBool #rangeAddress(CALLEE_ID) | ||
andBool #rangeUInt(256, NOW) | ||
andBool #rangeUInt(128, BLOCK_NUM) // Solidity | ||
andBool #rangeUInt(256, CONTRACT_BAL) | ||
andBool #rangeUInt(256, CALLEE_BAL) | ||
andBool #rangeNonce(CONTRACT_NONCE) | ||
andBool #rangeNonce(CALLEE_NONCE) | ||
andBool #range(0 <= CD < 1024) | ||
andBool #rangeAddress(MSG_SENDER) | ||
andBool #rangeUInt(256, A0) | ||
andBool #rangeUInt(8, A1) | ||
|
||
endmodule |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
pragma solidity 0.4.24; | ||
pragma experimental ABIEncoderV2; | ||
|
||
contract structarg00 { | ||
struct Var { | ||
uint a; | ||
uint8 b; | ||
} | ||
|
||
function execute(Var p) public returns (uint) { | ||
return p.a; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters