From 50a77a3ddb0738d52fe6f348b56366c28acc7b9f Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 13 Jun 2024 07:03:32 -0600 Subject: [PATCH] Factor out vat arithmetic in proof-reuse for MCD (#2467) * tests/specs/mcd/vat-arithmetic-spec: single spec file with all vat arithmetic specs * tests/specs/mcd/vat-spec.k: add single file incorporating all VAT proofs * tests/specs/mcd/vat-*: update vat specs with more dependencies * tests/specs/mcd/flopper-cage-pass: formatting * tests/specs/mcd/vat-*: update with more dependency proofs * tests/specs/mcd/vat-spec: add missing spec * tests/specs/mcd/vat-arithmetic-spec: update cell, remove unused cells * tests/specs/mcd: remove now-redundant vat arithmetic pass proofs * tests/failing: update failing lists * tests/specs/mcd/vat-flux-diff-pass-spec.k: add useGas cell * tests/specs/mcd: add useGas cell in several places * tests/specs/mcd/vat*: reuse specs from vat-arithmetic-spec file * tests/specs/mcd/vat-spec: update to list all Vat proofs * tests/specs/mcd: remove exit-code cell from specs * tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k: add other needed dependencies * kevm-pyk/kevm: add dummy merge-nodes heuristic * Makefile, kevm-pyk/: add test of DSS spec reuse * .github/test-pr: add job for spec-reuse proofs * tests/test_prove: tests/failing: remove tests/specs/mcd/vat-* from test-pyk-prove test-suite * kevm-pyk/{utils,cli,__main__,test_prove}: use new field direct_subproof_rules to run test-prove-dss * Set Version: 1.0.599 * Set Version: 1.0.602 * Revert "kevm-pyk/kevm: add dummy merge-nodes heuristic" This reverts commit 41a04998de570693675f66162a9f67b20b102b59. * kevm-pyk/{conftest,test_prove}: hardcode the number of workers for dss test --------- Co-authored-by: devops --- .github/workflows/test-pr.yml | 3 + Makefile | 7 +- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 1 + kevm-pyk/src/kevm_pyk/cli.py | 9 + kevm-pyk/src/kevm_pyk/utils.py | 5 + kevm-pyk/src/tests/integration/test_prove.py | 48 +- package/version | 2 +- tests/failing-symbolic.haskell | 14 - tests/failing-symbolic.haskell-booster | 3 - tests/failing-symbolic.haskell-booster-dev | 14 - tests/failing-symbolic.pyk | 6 - tests/specs/mcd/flopper-cage-pass-spec.k | 1 - tests/specs/mcd/vat-addui-pass-spec.k | 107 ---- tests/specs/mcd/vat-arithmetic-spec.k | 571 ++++++++++++++++++ ...-pass-rough-spec.k => vat-dai-pass-spec.k} | 38 +- .../specs/mcd/vat-flux-diff-pass-rough-spec.k | 201 +----- ...-pass-spec.k => vat-flux-diff-pass-spec.k} | 68 ++- tests/specs/mcd/vat-fold-pass-rough-spec.k | 210 +------ .../specs/mcd/vat-fork-diff-pass-rough-spec.k | 314 +--------- .../vat-frob-diff-zero-dart-pass-rough-spec.k | 104 +--- ...subui-pass-spec.k => vat-heal-pass-spec.k} | 70 ++- tests/specs/mcd/vat-move-diff-rough-spec.k | 207 +------ ...-muluu-pass-spec.k => vat-sin-pass-spec.k} | 43 +- tests/specs/mcd/vat-slip-pass-rough-spec.k | 106 +--- tests/specs/mcd/vat-spec.k | 33 + 27 files changed, 820 insertions(+), 1369 deletions(-) delete mode 100644 tests/specs/mcd/vat-addui-pass-spec.k create mode 100644 tests/specs/mcd/vat-arithmetic-spec.k rename tests/specs/mcd/{vat-subui-pass-rough-spec.k => vat-dai-pass-spec.k} (75%) rename tests/specs/mcd/{vat-mului-pass-spec.k => vat-flux-diff-pass-spec.k} (51%) rename tests/specs/mcd/{vat-subui-pass-spec.k => vat-heal-pass-spec.k} (51%) rename tests/specs/mcd/{vat-muluu-pass-spec.k => vat-sin-pass-spec.k} (74%) create mode 100644 tests/specs/mcd/vat-spec.k diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 8ff3078ab0..48afeac9e7 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -125,6 +125,9 @@ jobs: - test-suite: 'test-prove-optimizations' test-args: timeout: 45 + - test-suite: 'test-prove-dss' + test-args: + timeout: 45 timeout-minutes: ${{ matrix.timeout }} steps: - name: 'Check out code' diff --git a/Makefile b/Makefile index 6928f12d0e..1de3b69262 100644 --- a/Makefile +++ b/Makefile @@ -27,7 +27,7 @@ kevm-pyk: poetry-env # Tests # ----- -test: test-integration test-conformance test-prove test-prove-pyk test-prove-kprove test-interactive +test: test-integration test-conformance test-prove test-prove-pyk test-prove-kprove test-prove-dss test-interactive # Conformance Tests @@ -50,7 +50,7 @@ test-rest-bchain: poetry # Proof Tests -test-prove: test-prove-pyk test-prove-kprove test-prove-optimizations +test-prove: test-prove-pyk test-prove-kprove test-prove-optimizations test-prove-dss test-prove-pyk: poetry $(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_pyk_prove" @@ -61,6 +61,9 @@ test-prove-kprove: poetry test-prove-optimizations: poetry $(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_optimizations" +test-prove-dss: poetry + $(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_dss" + # Integration Tests diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index daa27e47a6..f3a851b650 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.601" +version = "1.0.602" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 9370cd640c..bc7e5b26f5 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '1.0.601' +VERSION: Final = '1.0.602' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 66402f680c..f3d1b72b3e 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -381,6 +381,7 @@ def create_kcfg_explore() -> KCFGExplore: fail_fast=options.fail_fast, always_check_subsumption=options.always_check_subsumption, fast_check_subsumption=options.fast_check_subsumption, + direct_subproof_rules=options.direct_subproof_rules, max_frontier_parallel=options.max_frontier_parallel, ) end_time = time.time() diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 792456cb98..dd4b4a28fb 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -416,6 +416,7 @@ class KProveOptions(Options): debug_equations: list[str] always_check_subsumption: bool fast_check_subsumption: bool + direct_subproof_rules: bool @staticmethod def default() -> dict[str, Any]: @@ -423,6 +424,7 @@ def default() -> dict[str, Any]: 'debug_equations': [], 'always_check_subsumption': True, 'fast_check_subsumption': False, + 'direct_subproof_rules': False, } @@ -907,6 +909,13 @@ def kprove_args(self) -> ArgumentParser: action='store_true', help='Use fast-check on k-cell to determine subsumption (experimental).', ) + args.add_argument( + '--direct-subproof-rules', + dest='direct_subproof_rules', + default=None, + action='store_true', + help='For passing subproofs, construct lemmas directly from initial to target state.', + ) return args @cached_property diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 2bae200f85..57e60f1b04 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -105,6 +105,7 @@ class RunProverParams: counterexample_info: bool always_check_subsumption: bool fast_check_subsumption: bool + direct_subproof_rules: bool class APRProofStrategy(ABC): @@ -141,6 +142,7 @@ def create_prover() -> APRProver: counterexample_info=self.params.counterexample_info, always_check_subsumption=self.params.always_check_subsumption, fast_check_subsumption=self.params.fast_check_subsumption, + direct_subproof_rules=self.params.direct_subproof_rules, ) parallel_advance_proof( @@ -168,6 +170,7 @@ def prove(self, proof: APRProof, max_iterations: int | None = None, fail_fast: b counterexample_info=self.params.counterexample_info, always_check_subsumption=self.params.always_check_subsumption, fast_check_subsumption=self.params.fast_check_subsumption, + direct_subproof_rules=self.params.direct_subproof_rules, ) prover.advance_proof(fail_fast=fail_fast, max_iterations=max_iterations, proof=proof) @@ -215,6 +218,7 @@ def run_prover( counterexample_info: bool = False, always_check_subsumption: bool = False, fast_check_subsumption: bool = False, + direct_subproof_rules: bool = False, max_frontier_parallel: int = 1, ) -> bool: prover: APRProver | ImpliesProver @@ -231,6 +235,7 @@ def run_prover( execute_depth=max_depth, fast_check_subsumption=fast_check_subsumption, terminal_rules=terminal_rules, + direct_subproof_rules=direct_subproof_rules, ), ) strategy.prove(fail_fast=fail_fast, max_iterations=max_iterations, proof=proof) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 7f16cec4e3..a2bc3993ad 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -2,6 +2,7 @@ import logging import sys +from pathlib import Path from typing import TYPE_CHECKING, NamedTuple import pytest @@ -24,7 +25,6 @@ if TYPE_CHECKING: from collections.abc import Callable - from pathlib import Path from typing import Any, Final from pyk.utils import BugReport @@ -57,6 +57,8 @@ def spec_files(dir_name: str, glob: str) -> tuple[Path, ...]: ERC20_TESTS: Final = spec_files('erc20', '*/*-spec.k') EXAMPLES_TESTS: Final = spec_files('examples', '*-spec.k') + spec_files('examples', '*-spec.md') MCD_TESTS: Final = spec_files('mcd', '*-spec.k') +VAT_TESTS: Final = spec_files('mcd', 'vat*-spec.k') +NON_VAT_MCD_TESTS: Final = tuple(test for test in MCD_TESTS if test not in VAT_TESTS) KONTROL_TESTS: Final = spec_files('kontrol', '*-spec.k') ALL_TESTS: Final = sum( @@ -65,7 +67,7 @@ def spec_files(dir_name: str, glob: str) -> tuple[Path, ...]: FUNCTIONAL_TESTS, ERC20_TESTS, EXAMPLES_TESTS, - MCD_TESTS, + NON_VAT_MCD_TESTS, KONTROL_TESTS, ], (), @@ -357,6 +359,48 @@ def _get_optimization_proofs() -> list[APRProof]: assert proof.passed +def test_prove_dss( + kompiled_target_for: Callable[[Path], Path], + tmp_path: Path, + caplog: LogCaptureFixture, + bug_report: BugReport | None, + spec_name: str | None, +) -> None: + spec_file = Path('../tests/specs/mcd/vat-spec.k') + caplog.set_level(logging.INFO) + + if spec_name is not None and str(spec_file).find(spec_name) < 0: + pytest.skip() + + # Given + log_file = tmp_path / 'log.txt' + use_directory = tmp_path / 'kprove' + use_directory.mkdir() + + # When + try: + definition_dir = kompiled_target_for(spec_file) + options = ProveOptions( + { + 'spec_file': spec_file, + 'definition_dir': definition_dir, + 'includes': [str(include_dir) for include_dir in config.INCLUDE_DIRS], + 'save_directory': use_directory, + 'md_selector': 'foo', # TODO Ignored flag, this is to avoid KeyError + 'use_booster': True, + 'bug_report': bug_report, + 'break_on_calls': False, + 'workers': 8, + 'direct_subproof_rules': True, + } + ) + exec_prove(options=options) + except BaseException: + raise + finally: + log_file.write_text(caplog.text) + + # ------------ # Legacy tests # ------------ diff --git a/package/version b/package/version index 18e1034084..2ef01da42b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.601 +1.0.602 diff --git a/tests/failing-symbolic.haskell b/tests/failing-symbolic.haskell index ba3fae6042..2347d6fa3b 100644 --- a/tests/failing-symbolic.haskell +++ b/tests/failing-symbolic.haskell @@ -114,19 +114,5 @@ tests/specs/mcd/flopper-kick-pass-rough-spec.k tests/specs/mcd/flopper-tick-pass-rough-spec.k tests/specs/mcd/functional-spec.k tests/specs/mcd/pot-join-pass-rough-spec.k -tests/specs/mcd/vat-addui-fail-rough-spec.k -tests/specs/mcd/vat-addui-pass-spec.k -tests/specs/mcd/vat-deny-diff-fail-rough-spec.k -tests/specs/mcd/vat-flux-diff-pass-rough-spec.k -tests/specs/mcd/vat-fold-pass-rough-spec.k -tests/specs/mcd/vat-fork-diff-pass-rough-spec.k -tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k -tests/specs/mcd/vat-move-diff-rough-spec.k -tests/specs/mcd/vat-mului-pass-spec.k -tests/specs/mcd/vat-muluu-pass-spec.k -tests/specs/mcd/vat-slip-pass-rough-spec.k -tests/specs/mcd/vat-subui-fail-rough-spec.k -tests/specs/mcd/vat-subui-pass-rough-spec.k -tests/specs/mcd/vat-subui-pass-spec.k tests/specs/mcd/vow-fess-fail-rough-spec.k tests/specs/mcd/vow-flog-fail-rough-spec.k diff --git a/tests/failing-symbolic.haskell-booster b/tests/failing-symbolic.haskell-booster index 8dbe55d6a9..660007fd61 100644 --- a/tests/failing-symbolic.haskell-booster +++ b/tests/failing-symbolic.haskell-booster @@ -3,6 +3,3 @@ tests/specs/examples/sum-to-n-foundry-spec.k tests/specs/examples/sum-to-n-spec.k tests/specs/functional/merkle-spec.k tests/specs/functional/storageRoot-spec.k -tests/specs/mcd/vat-fold-pass-rough-spec.k -tests/specs/mcd/vat-fork-diff-pass-rough-spec.k -tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k diff --git a/tests/failing-symbolic.haskell-booster-dev b/tests/failing-symbolic.haskell-booster-dev index 3bd1a6896f..d73d0b08dc 100644 --- a/tests/failing-symbolic.haskell-booster-dev +++ b/tests/failing-symbolic.haskell-booster-dev @@ -111,19 +111,5 @@ tests/specs/mcd/flopper-kick-pass-rough-spec.k tests/specs/mcd/flopper-tick-pass-rough-spec.k tests/specs/mcd/functional-spec.k tests/specs/mcd/pot-join-pass-rough-spec.k -tests/specs/mcd/vat-addui-fail-rough-spec.k -tests/specs/mcd/vat-addui-pass-spec.k -tests/specs/mcd/vat-deny-diff-fail-rough-spec.k -tests/specs/mcd/vat-flux-diff-pass-rough-spec.k -tests/specs/mcd/vat-fold-pass-rough-spec.k -tests/specs/mcd/vat-fork-diff-pass-rough-spec.k -tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k -tests/specs/mcd/vat-move-diff-rough-spec.k -tests/specs/mcd/vat-mului-pass-spec.k -tests/specs/mcd/vat-muluu-pass-spec.k -tests/specs/mcd/vat-slip-pass-rough-spec.k -tests/specs/mcd/vat-subui-fail-rough-spec.k -tests/specs/mcd/vat-subui-pass-rough-spec.k -tests/specs/mcd/vat-subui-pass-spec.k tests/specs/mcd/vow-fess-fail-rough-spec.k tests/specs/mcd/vow-flog-fail-rough-spec.k diff --git a/tests/failing-symbolic.pyk b/tests/failing-symbolic.pyk index 3072de9f6b..59242101ee 100644 --- a/tests/failing-symbolic.pyk +++ b/tests/failing-symbolic.pyk @@ -55,11 +55,5 @@ tests/specs/mcd/flopper-kick-pass-rough-spec.k tests/specs/mcd/flopper-tick-pass-rough-spec.k tests/specs/mcd/functional-spec.k tests/specs/mcd/pot-join-pass-rough-spec.k -tests/specs/mcd/vat-flux-diff-pass-rough-spec.k -tests/specs/mcd/vat-fold-pass-rough-spec.k -tests/specs/mcd/vat-fork-diff-pass-rough-spec.k -tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k -tests/specs/mcd/vat-move-diff-rough-spec.k -tests/specs/mcd/vat-slip-pass-rough-spec.k tests/specs/mcd/vow-fess-fail-rough-spec.k tests/specs/mcd/vow-flog-fail-rough-spec.k diff --git a/tests/specs/mcd/flopper-cage-pass-spec.k b/tests/specs/mcd/flopper-cage-pass-spec.k index d7d2c6d460..603a0f014d 100644 --- a/tests/specs/mcd/flopper-cage-pass-spec.k +++ b/tests/specs/mcd/flopper-cage-pass-spec.k @@ -3,7 +3,6 @@ requires "verification.k" module FLOPPER-CAGE-PASS-SPEC imports VERIFICATION - // Flopper_cage claim [Flopper.cage.pass]: #execute ~> CONTINUATION => #halt ~> CONTINUATION NORMAL diff --git a/tests/specs/mcd/vat-addui-pass-spec.k b/tests/specs/mcd/vat-addui-pass-spec.k deleted file mode 100644 index 12dc400f06..0000000000 --- a/tests/specs/mcd/vat-addui-pass-spec.k +++ /dev/null @@ -1,107 +0,0 @@ -requires "verification.k" - -module VAT-ADDUI-PASS-SPEC - imports VERIFICATION - - // Vat_addui - claim [Vat.addui.pass]: - #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => ABI_x +Int ABI_y : WS - _ - 13112 => 13174 - #gas(VGas) => #if ( ABI_y - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeSInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1015) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) - -endmodule diff --git a/tests/specs/mcd/vat-arithmetic-spec.k b/tests/specs/mcd/vat-arithmetic-spec.k new file mode 100644 index 0000000000..a8ff05f0e2 --- /dev/null +++ b/tests/specs/mcd/vat-arithmetic-spec.k @@ -0,0 +1,571 @@ +requires "verification.k" + +module VAT-ARITHMETIC-SPEC + imports VERIFICATION + + claim [Vat.adduu.pass]: + #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + NORMAL + ISTANBUL + true + + + VOutput => VOutput + _ => ?_ + _VCallStack + _ + _ => ?_ + + Vat_bin_runtime + #computeValidJumpDests(Vat_bin_runtime) + ACCT_ID + CALLER_ID + _ => ?_ + VCallValue + ABI_y : ABI_x : JMPTO : WS => ABI_x +Int ABI_y : WS + _ + 13086 => 13111 + #gas(VGas) => #gas ( ( VGas +Int -62 ) ) + VMemoryUsed + _ => ?_ + _ + VCallDepth + + + _VSelfDestruct + _ => ?_ + _Vrefund => ?_ + _ => ?_ + _ => ?_ + + _ + ORIGIN_ID + _ + + _ + _ + _ + _ + _ + _ + _ + _ + _BLOCK_NUMBER + _ + _ + TIME + _ + _ + _ + _ + _ + _ + + + + VChainId + + + ACCT_ID + ACCT_ID_balance + Vat_bin_runtime + ... + + ... + + _ + _ + _ + + + requires #rangeAddress(ACCT_ID) + andBool ACCT_ID =/=Int 0 + andBool #notPrecompileAddress(ACCT_ID) + andBool #rangeAddress(CALLER_ID) + andBool #rangeAddress(ORIGIN_ID) + andBool #rangeUInt(256, TIME) + andBool #rangeUInt(256, ACCT_ID_balance) + andBool VCallDepth <=Int 1024 + andBool #rangeUInt(256, VCallValue) + andBool #rangeUInt(256, VChainId) + andBool (#rangeUInt(256, ABI_x) + andBool (#rangeUInt(256, ABI_y) + andBool ((#sizeWordStack(WS) <=Int 100) + andBool (#rangeUInt(256, VMemoryUsed) + andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) + + claim [Vat.addui.pass]: + #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + NORMAL + ISTANBUL + true + + + VOutput => VOutput + _ => ?_ + _VCallStack + _ + _ => ?_ + + Vat_bin_runtime + #computeValidJumpDests(Vat_bin_runtime) + ACCT_ID + CALLER_ID + _ => ?_ + VCallValue + chop(ABI_y) : ABI_x : JMPTO : WS => ABI_x +Int ABI_y : WS + _ + 13112 => 13174 + #gas(VGas) => #if ( ABI_y + VMemoryUsed + _ => ?_ + _ + VCallDepth + + + _VSelfDestruct + _ => ?_ + _Vrefund => ?_ + _ => ?_ + _ => ?_ + + _ + ORIGIN_ID + _ + + _ + _ + _ + _ + _ + _ + _ + _ + _BLOCK_NUMBER + _ + _ + TIME + _ + _ + _ + _ + _ + _ + + + + VChainId + + + ACCT_ID + ACCT_ID_balance + Vat_bin_runtime + ... + + ... + + _ + _ + _ + + + requires #rangeAddress(ACCT_ID) + andBool ACCT_ID =/=Int 0 + andBool #notPrecompileAddress(ACCT_ID) + andBool #rangeAddress(CALLER_ID) + andBool #rangeAddress(ORIGIN_ID) + andBool #rangeUInt(256, TIME) + andBool #rangeUInt(256, ACCT_ID_balance) + andBool VCallDepth <=Int 1024 + andBool #rangeUInt(256, VCallValue) + andBool #rangeUInt(256, VChainId) + andBool (#rangeUInt(256, ABI_x) + andBool (#rangeSInt(256, ABI_y) + andBool ((#sizeWordStack(WS) <=Int 1015) + andBool (#rangeUInt(256, VMemoryUsed) + andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) + + claim [Vat.subuu.pass]: + #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + NORMAL + ISTANBUL + true + + + VOutput => VOutput + _ => ?_ + _VCallStack + _ + _ => ?_ + + Vat_bin_runtime + #computeValidJumpDests(Vat_bin_runtime) + ACCT_ID + CALLER_ID + _ => ?_ + VCallValue + ABI_y : ABI_x : JMPTO : WS => ABI_x -Int ABI_y : WS + _ + 13060 => 13085 + #gas(VGas) => #gas ( ( VGas +Int -62 ) ) + VMemoryUsed + _ => ?_ + _ + VCallDepth + + + _VSelfDestruct + _ => ?_ + _Vrefund => ?_ + _ => ?_ + _ => ?_ + + _ + ORIGIN_ID + _ + + _ + _ + _ + _ + _ + _ + _ + _ + _BLOCK_NUMBER + _ + _ + TIME + _ + _ + _ + _ + _ + _ + + + + VChainId + + + ACCT_ID + ACCT_ID_balance + Vat_bin_runtime + ... + + ... + + _ + _ + _ + + + requires #rangeAddress(ACCT_ID) + andBool ACCT_ID =/=Int 0 + andBool #notPrecompileAddress(ACCT_ID) + andBool #rangeAddress(CALLER_ID) + andBool #rangeAddress(ORIGIN_ID) + andBool #rangeUInt(256, TIME) + andBool #rangeUInt(256, ACCT_ID_balance) + andBool VCallDepth <=Int 1024 + andBool #rangeUInt(256, VCallValue) + andBool #rangeUInt(256, VChainId) + andBool (#rangeUInt(256, ABI_x) + andBool (#rangeUInt(256, ABI_y) + andBool ((#sizeWordStack(WS) <=Int 100) + andBool (#rangeUInt(256, VMemoryUsed) + andBool ((#rangeUInt(256, ABI_x -Int ABI_y))))))) + + claim [Vat.subui.pass]: + #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + NORMAL + ISTANBUL + true + + + VOutput => VOutput + _ => ?_ + _VCallStack + _ + _ => ?_ + + Vat_bin_runtime + #computeValidJumpDests(Vat_bin_runtime) + ACCT_ID + CALLER_ID + _ => ?_ + VCallValue + chop(ABI_y) : ABI_x : JMPTO : WS => ABI_x -Int ABI_y : WS + _ + 13304 => 13366 + #gas(VGas) => #if ( ABI_y =/=Int 0 andBool 0 <=Int ABI_y ) + #then #gas ( ( VGas +Int -136 ) ) + #else #if 0 <=Int ABI_y + #then #gas ( ( VGas +Int -122 ) ) + #else #gas ( ( VGas +Int -136 ) ) + #fi + #fi + VMemoryUsed + _ => ?_ + _ + VCallDepth + + + _VSelfDestruct + _ => ?_ + _Vrefund => ?_ + _ => ?_ + _ => ?_ + + _ + ORIGIN_ID + _ + + _ + _ + _ + _ + _ + _ + _ + _ + _BLOCK_NUMBER + _ + _ + TIME + _ + _ + _ + _ + _ + _ + + + + VChainId + + + ACCT_ID + ACCT_ID_balance + Vat_bin_runtime + ... + + ... + + _ + _ + _ + + + requires #rangeAddress(ACCT_ID) + andBool ACCT_ID =/=Int 0 + andBool #notPrecompileAddress(ACCT_ID) + andBool #rangeAddress(CALLER_ID) + andBool #rangeAddress(ORIGIN_ID) + andBool #rangeUInt(256, TIME) + andBool #rangeUInt(256, ACCT_ID_balance) + andBool VCallDepth <=Int 1024 + andBool #rangeUInt(256, VCallValue) + andBool #rangeUInt(256, VChainId) + andBool (#rangeUInt(256, ABI_x) + andBool (#rangeSInt(256, ABI_y) + andBool ((#sizeWordStack(WS) <=Int 1015) + andBool (#rangeUInt(256, VMemoryUsed) + andBool ((#rangeUInt(256, ABI_x -Int ABI_y))))))) + + claim [Vat.muluu.pass]: + #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + NORMAL + ISTANBUL + true + + + VOutput => VOutput + _ => ?_ + _VCallStack + _ + _ => ?_ + + Vat_bin_runtime + #computeValidJumpDests(Vat_bin_runtime) + ACCT_ID + CALLER_ID + _ => ?_ + VCallValue + ABI_y : ABI_x : JMPTO : WS => ABI_x *Int ABI_y : WS + _ + 13234 => 13277 + #gas(VGas) => #if ABI_y ==Int 0 + #then #gas ( ( VGas +Int -62 ) ) + #else #gas ( ( VGas +Int -114 ) ) + #fi + VMemoryUsed + _ => ?_ + _ + VCallDepth + + + _VSelfDestruct + _ => ?_ + _Vrefund => ?_ + _ => ?_ + _ => ?_ + + _ + ORIGIN_ID + _ + + _ + _ + _ + _ + _ + _ + _ + _ + _BLOCK_NUMBER + _ + _ + TIME + _ + _ + _ + _ + _ + _ + + + + VChainId + + + ACCT_ID + ACCT_ID_balance + Vat_bin_runtime + ... + + ... + + _ + _ + _ + + + requires #rangeAddress(ACCT_ID) + andBool ACCT_ID =/=Int 0 + andBool #notPrecompileAddress(ACCT_ID) + andBool #rangeAddress(CALLER_ID) + andBool #rangeAddress(ORIGIN_ID) + andBool #rangeUInt(256, TIME) + andBool #rangeUInt(256, ACCT_ID_balance) + andBool VCallDepth <=Int 1024 + andBool #rangeUInt(256, VCallValue) + andBool #rangeUInt(256, VChainId) + andBool (#rangeUInt(256, ABI_x) + andBool (#rangeUInt(256, ABI_y) + andBool ((#sizeWordStack(WS) <=Int 1000) + andBool (#rangeUInt(256, VMemoryUsed) + andBool ((#rangeUInt(256, ABI_x *Int ABI_y))))))) + + claim [Vat.mului.pass]: + #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + NORMAL + ISTANBUL + true + + + VOutput => VOutput + _ => ?_ + _VCallStack + _ + _ => ?_ + + Vat_bin_runtime + #computeValidJumpDests(Vat_bin_runtime) + ACCT_ID + CALLER_ID + _ => ?_ + VCallValue + chop(ABI_y) : ABI_x : JMPTO : WS => chop(ABI_x *Int ABI_y) : WS + _ + 13175 => 13233 + #gas(VGas) => #if ABI_y ==Int 0 + #then #gas ( ( VGas +Int -104 ) ) + #else #gas ( ( VGas +Int -140 ) ) + #fi + VMemoryUsed + _ => ?_ + _ + VCallDepth + + + _VSelfDestruct + _ => ?_ + _Vrefund => ?_ + _ => ?_ + _ => ?_ + + _ + ORIGIN_ID + _ + + _ + _ + _ + _ + _ + _ + _ + _ + _BLOCK_NUMBER + _ + _ + TIME + _ + _ + _ + _ + _ + _ + + + + VChainId + + + ACCT_ID + ACCT_ID_balance + Vat_bin_runtime + ... + + ... + + _ + _ + _ + + + requires #rangeAddress(ACCT_ID) + andBool ACCT_ID =/=Int 0 + andBool #notPrecompileAddress(ACCT_ID) + andBool #rangeAddress(CALLER_ID) + andBool #rangeAddress(ORIGIN_ID) + andBool #rangeUInt(256, TIME) + andBool #rangeUInt(256, ACCT_ID_balance) + andBool VCallDepth <=Int 1024 + andBool #rangeUInt(256, VCallValue) + andBool #rangeUInt(256, VChainId) + andBool (#rangeUInt(256, ABI_x) + andBool (#rangeSInt(256, ABI_y) + andBool ((#sizeWordStack(WS) <=Int 1000) + andBool (#rangeUInt(256, VMemoryUsed) + andBool ((#rangeSInt(256, ABI_x)) + andBool ((#rangeSInt(256, ABI_x *Int ABI_y)))))))) + +endmodule diff --git a/tests/specs/mcd/vat-subui-pass-rough-spec.k b/tests/specs/mcd/vat-dai-pass-spec.k similarity index 75% rename from tests/specs/mcd/vat-subui-pass-rough-spec.k rename to tests/specs/mcd/vat-dai-pass-spec.k index 9b94fb91fb..56df19fe79 100644 --- a/tests/specs/mcd/vat-subui-pass-rough-spec.k +++ b/tests/specs/mcd/vat-dai-pass-spec.k @@ -1,18 +1,17 @@ requires "verification.k" -module VAT-SUBUI-PASS-ROUGH-SPEC +module VAT-DAI-PASS-SPEC imports VERIFICATION - // Vat_subui - claim [Vat.subui.pass.rough]: - #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + claim [Vat.dai.pass]: + #execute ~> CONTINUATION => #halt ~> CONTINUATION NORMAL ISTANBUL true - VOutput => VOutput - _ => ?_ + _ => #buf(32, Rad) + _ => EVMC_SUCCESS _VCallStack _ _ => ?_ @@ -21,13 +20,13 @@ module VAT-SUBUI-PASS-ROUGH-SPEC #computeValidJumpDests(Vat_bin_runtime) ACCT_ID CALLER_ID - _ => ?_ + #abiCallData("dai", #address(ABI_usr)) +Bytes CD => ?_ VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => ABI_x -Int ABI_y : WS - _ - 13304 => 13366 - #gas(VGas) => ?_ - VMemoryUsed + .WordStack => ?_ + .Bytes => ?_ + 0 => ?_ + #gas(VGas) => #gas ( ( VGas +Int -1236 ) ) + 0 => ?_ _ => ?_ _ VCallDepth @@ -71,7 +70,7 @@ module VAT-SUBUI-PASS-ROUGH-SPEC ACCT_ID_balance Vat_bin_runtime ACCT_ID_STORAGE => ACCT_ID_STORAGE - _ACCT_ID_ORIG_STORAGE + ACCT_ID_ORIG_STORAGE Nonce_Vat ... @@ -93,12 +92,13 @@ module VAT-SUBUI-PASS-ROUGH-SPEC andBool #rangeUInt(256, VChainId) andBool #rangeNonce(Nonce_Vat) - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeSInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1015) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x -Int ABI_y))))))) - + andBool (#rangeAddress(ABI_usr) + andBool (#rangeUInt(256, Rad) + andBool (lengthBytes(CD) <=Int 1250000000 + andBool (#rangeUInt(256, Junk_0) + andBool ((VCallValue ==Int 0)))))) + andBool #lookup(ACCT_ID_STORAGE, #Vat.dai[ABI_usr]) ==Int Rad + andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.dai[ABI_usr]) ==Int Junk_0 endmodule diff --git a/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k b/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k index 35e06d02f2..a81ac7e203 100644 --- a/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k +++ b/tests/specs/mcd/vat-flux-diff-pass-rough-spec.k @@ -1,9 +1,10 @@ requires "verification.k" +requires "vat-arithmetic-spec.k" module VAT-FLUX-DIFF-PASS-ROUGH-SPEC imports VERIFICATION + imports VAT-ARITHMETIC-SPEC - // Vat_flux-diff claim [Vat.flux-diff.pass.rough]: #execute ~> CONTINUATION => #halt ~> CONTINUATION NORMAL @@ -119,202 +120,6 @@ module VAT-FLUX-DIFF-PASS-ROUGH-SPEC andBool #Vat.can[ABI_src][CALLER_ID] =/=Int #Vat.gem[ABI_ilk][ABI_dst] andBool #Vat.gem[ABI_ilk][ABI_src] =/=Int #Vat.gem[ABI_ilk][ABI_dst] - // Vat_subuu - claim [Vat.subuu.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - ABI_y : ABI_x : JMPTO : WS => JMPTO : ABI_x -Int ABI_y : WS - _ - 13060 => 13085 - #gas(VGas) => #gas ( ( VGas +Int -54 ) ) - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeUInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 100) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x -Int ABI_y))))))) - - - [trusted] - - - // Vat_adduu - claim [Vat.adduu.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - ABI_y : ABI_x : JMPTO : WS => JMPTO : ABI_x +Int ABI_y : WS - _ - 13086 => 13111 - #gas(VGas) => #gas ( ( VGas +Int -54 ) ) - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeUInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 100) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) - - - [trusted] - + [depends(VAT-ARITHMETIC-SPEC.Vat.subuu.pass,VAT-ARITHMETIC-SPEC.Vat.adduu.pass)] endmodule diff --git a/tests/specs/mcd/vat-mului-pass-spec.k b/tests/specs/mcd/vat-flux-diff-pass-spec.k similarity index 51% rename from tests/specs/mcd/vat-mului-pass-spec.k rename to tests/specs/mcd/vat-flux-diff-pass-spec.k index c6c8f8682a..c8306fbc63 100644 --- a/tests/specs/mcd/vat-mului-pass-spec.k +++ b/tests/specs/mcd/vat-flux-diff-pass-spec.k @@ -1,18 +1,17 @@ -requires "verification.k" +requires "vat-arithmetic-spec.k" -module VAT-MULUI-PASS-SPEC - imports VERIFICATION +module VAT-FLUX-DIFF-PASS-SPEC + imports VAT-ARITHMETIC-SPEC - // Vat_mului - claim [Vat.mului.pass]: - #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + claim [Vat.flux-diff.pass]: + #execute ~> CONTINUATION => #halt ~> CONTINUATION NORMAL ISTANBUL true - VOutput => VOutput - _ => ?_ + .Bytes + _ => EVMC_SUCCESS _VCallStack _ _ => ?_ @@ -21,18 +20,15 @@ module VAT-MULUI-PASS-SPEC #computeValidJumpDests(Vat_bin_runtime) ACCT_ID CALLER_ID - _ => ?_ + #abiCallData("flux", #bytes32(ABI_ilk), #address(ABI_src), #address(ABI_dst), #uint256(ABI_wad)) +Bytes CD => ?_ VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => chop(ABI_x *Int ABI_y) : WS - _ - 13175 => 13233 - #gas(VGas) => #if ABI_y ==Int 0 - #then #gas ( ( VGas +Int -104 ) ) - #else #gas ( ( VGas +Int -140 ) ) - #fi - VMemoryUsed + .WordStack => ?_ + .Bytes => ?_ + 0 => ?_ + #gas(VGas) => #gas ( ( ( ( VGas -Int Csstore( ISTANBUL , ( Gem_src -Int ABI_wad ) , Gem_src , Junk_1 ) ) -Int Csstore( ISTANBUL , ( Gem_dst +Int ABI_wad ) , Gem_dst , Junk_2 ) ) +Int -8307 ) ) + 0 => ?_ _ => ?_ - _ + false VCallDepth @@ -73,8 +69,8 @@ module VAT-MULUI-PASS-SPEC ACCT_ID ACCT_ID_balance Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - _ACCT_ID_ORIG_STORAGE + ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.gem[ABI_ilk][ABI_src] <- Gem_src -Int ABI_wad ] [ #Vat.gem[ABI_ilk][ABI_dst] <- Gem_dst +Int ABI_wad ] + ACCT_ID_ORIG_STORAGE Nonce_Vat ... @@ -96,13 +92,33 @@ module VAT-MULUI-PASS-SPEC andBool #rangeUInt(256, VChainId) andBool #rangeNonce(Nonce_Vat) - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeSInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1000) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeSInt(256, ABI_x)) - andBool ((#rangeSInt(256, ABI_x *Int ABI_y)))))))) + andBool (#rangeBytes(32, ABI_ilk) + andBool (#rangeAddress(ABI_src) + andBool (#rangeAddress(ABI_dst) + andBool (#rangeUInt(256, ABI_wad) + andBool (#rangeUInt(256, May) + andBool (#rangeUInt(256, Gem_src) + andBool (#rangeUInt(256, Gem_dst) + andBool ((lengthBytes(CD) <=Int 1250000000) + andBool ((ABI_src =/=Int ABI_dst) + andBool (#rangeUInt(256, Junk_0) + andBool (#rangeUInt(256, Junk_1) + andBool (#rangeUInt(256, Junk_2) + andBool ((((May ==Int 1 orBool ABI_src ==Int CALLER_ID))) + andBool (((VCallValue ==Int 0)) + andBool ((#rangeUInt(256, Gem_src -Int ABI_wad)) + andBool ((#rangeUInt(256, Gem_dst +Int ABI_wad)))))))))))))))))) + andBool #lookup(ACCT_ID_STORAGE, #Vat.can[ABI_src][CALLER_ID]) ==Int May + andBool #lookup(ACCT_ID_STORAGE, #Vat.gem[ABI_ilk][ABI_src]) ==Int Gem_src + andBool #lookup(ACCT_ID_STORAGE, #Vat.gem[ABI_ilk][ABI_dst]) ==Int Gem_dst + andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.can[ABI_src][CALLER_ID]) ==Int Junk_0 + andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.gem[ABI_ilk][ABI_src]) ==Int Junk_1 + andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.gem[ABI_ilk][ABI_dst]) ==Int Junk_2 + andBool #Vat.can[ABI_src][CALLER_ID] =/=Int #Vat.gem[ABI_ilk][ABI_src] + andBool #Vat.can[ABI_src][CALLER_ID] =/=Int #Vat.gem[ABI_ilk][ABI_dst] + andBool #Vat.gem[ABI_ilk][ABI_src] =/=Int #Vat.gem[ABI_ilk][ABI_dst] + [depends(VAT-ARITHMETIC-SPEC.Vat.adduu.pass,VAT-ARITHMETIC-SPEC.Vat.subuu.pass)] endmodule diff --git a/tests/specs/mcd/vat-fold-pass-rough-spec.k b/tests/specs/mcd/vat-fold-pass-rough-spec.k index a28afb297c..f55285dbdb 100644 --- a/tests/specs/mcd/vat-fold-pass-rough-spec.k +++ b/tests/specs/mcd/vat-fold-pass-rough-spec.k @@ -1,7 +1,9 @@ requires "verification.k" +requires "vat-arithmetic-spec.k" module VAT-FOLD-PASS-ROUGH-SPEC imports VERIFICATION + imports VAT-ARITHMETIC-SPEC // Vat_fold claim [Vat.fold.pass.rough]: @@ -144,212 +146,6 @@ module VAT-FOLD-PASS-ROUGH-SPEC andBool #Vat.ilks[ABI_i].rate =/=Int #Vat.debt andBool #Vat.dai[ABI_u] =/=Int #Vat.debt - // Vat_addui - claim [Vat.addui.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => JMPTO : ABI_x +Int ABI_y : WS - _ - 13112 => 13174 - #gas(VGas) => #if ( ABI_y - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeSInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1015) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) - - - [trusted] - - - // Vat_mului - claim [Vat.mului.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => JMPTO : chop(ABI_x *Int ABI_y) : WS - _ - 13175 => 13233 - #gas(VGas) => #if ABI_y ==Int 0 - #then #gas ( ( VGas +Int -96 ) ) - #else #gas ( ( VGas +Int -132 ) ) - #fi - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeSInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1000) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeSInt(256, ABI_x)) - andBool ((#rangeSInt(256, ABI_x *Int ABI_y)))))))) - - - [trusted] - + [depends(VAT-ARITHMETIC-SPEC.Vat.addui.pass,VAT-ARITHMETIC-SPEC.Vat.mului.pass)] endmodule diff --git a/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k b/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k index 0304fa78cc..1bb8113cf3 100644 --- a/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k +++ b/tests/specs/mcd/vat-fork-diff-pass-rough-spec.k @@ -1,7 +1,9 @@ requires "verification.k" +requires "vat-arithmetic-spec.k" module VAT-FORK-DIFF-PASS-ROUGH-SPEC imports VERIFICATION + imports VAT-ARITHMETIC-SPEC // Vat_fork-diff claim [Vat.fork-diff.pass.rough]: @@ -186,316 +188,6 @@ module VAT-FORK-DIFF-PASS-ROUGH-SPEC andBool #Vat.urns[ABI_ilk][ABI_src].art =/=Int #Vat.urns[ABI_ilk][ABI_dst].art andBool #Vat.urns[ABI_ilk][ABI_dst].ink =/=Int #Vat.urns[ABI_ilk][ABI_dst].art - // Vat_addui - claim [Vat.addui.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => JMPTO : ABI_x +Int ABI_y : WS - _ - 13112 => 13174 - #gas(VGas) => #if ( ABI_y - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeSInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1015) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) - - - [trusted] - - - // Vat_subui - claim [Vat.subui.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => JMPTO : ABI_x -Int ABI_y : WS - _ - 13304 => 13366 - #gas(VGas) => #if ( ABI_y =/=Int 0 andBool 0 <=Int ABI_y ) - #then #gas ( ( VGas +Int -128 ) ) - #else #if 0 <=Int ABI_y - #then #gas ( ( VGas +Int -114 ) ) - #else #gas ( ( VGas +Int -128 ) ) - #fi - #fi - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeSInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1015) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x -Int ABI_y))))))) - - - [trusted] - - - // Vat_muluu - claim [Vat.muluu.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - ABI_y : ABI_x : JMPTO : WS => JMPTO : ABI_x *Int ABI_y : WS - _ - 13234 => 13277 - #gas(VGas) => #if ABI_y ==Int 0 - #then #gas ( ( VGas +Int -54 ) ) - #else #gas ( ( VGas +Int -106 ) ) - #fi - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeUInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1000) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x *Int ABI_y))))))) - - - [trusted] - + [depends(VAT-ARITHMETIC-SPEC.Vat.addui.pass,VAT-ARITHMETIC-SPEC.Vat.subui.pass,VAT-ARITHMETIC-SPEC.Vat.muluu.pass)] endmodule diff --git a/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k b/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k index 2e2ca8f572..1bd0a7613a 100644 --- a/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k +++ b/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k @@ -1,7 +1,9 @@ requires "verification.k" +requires "vat-arithmetic-spec.k" module VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC imports VERIFICATION + imports VAT-ARITHMETIC-SPEC // Vat_frob-diff-zero-dart claim [Vat.frob-diff-zero-dart.pass.rough]: @@ -284,106 +286,6 @@ module VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC andBool #Vat.urns[ABI_i][ABI_u].art =/=Int #Vat.live andBool #Vat.ilks[ABI_i].Art =/=Int #Vat.live - // Vat_muluu - claim [Vat.muluu.pass]: - #execute ~> CONTINUATION => #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - ABI_y : ABI_x : JMPTO : WS => JMPTO : ABI_x *Int ABI_y : WS - _ - 13234 => 13277 - #gas(VGas) => #if ABI_y ==Int 0 - #then #gas ( ( VGas +Int -54 ) ) - #else #gas ( ( VGas +Int -106 ) ) - #fi - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeUInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1000) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x *Int ABI_y))))))) - - - [trusted] - + [depends(VAT-ARITHMETIC-SPEC.Vat.addui.pass,VAT-ARITHMETIC-SPEC.Vat.subui.pass,VAT-ARITHMETIC-SPEC.Vat.mului.pass,VAT-ARITHMETIC-SPEC.Vat.muluu.pass)] endmodule diff --git a/tests/specs/mcd/vat-subui-pass-spec.k b/tests/specs/mcd/vat-heal-pass-spec.k similarity index 51% rename from tests/specs/mcd/vat-subui-pass-spec.k rename to tests/specs/mcd/vat-heal-pass-spec.k index ad9f36dbce..53cdd66e19 100644 --- a/tests/specs/mcd/vat-subui-pass-spec.k +++ b/tests/specs/mcd/vat-heal-pass-spec.k @@ -1,18 +1,17 @@ requires "verification.k" -module VAT-SUBUI-PASS-SPEC +module VAT-HEAL-PASS-SPEC imports VERIFICATION - // Vat_subui - claim [Vat.subui.pass]: - #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + claim [Vat.heal.pass]: + #execute ~> CONTINUATION => #halt ~> CONTINUATION NORMAL ISTANBUL true - VOutput => VOutput - _ => ?_ + .Bytes + _ => EVMC_SUCCESS _VCallStack _ _ => ?_ @@ -21,21 +20,15 @@ module VAT-SUBUI-PASS-SPEC #computeValidJumpDests(Vat_bin_runtime) ACCT_ID CALLER_ID - _ => ?_ + #abiCallData("heal", #uint256(ABI_rad)) +Bytes CD => ?_ VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => ABI_x -Int ABI_y : WS - _ - 13304 => 13366 - #gas(VGas) => #if ( ABI_y =/=Int 0 andBool 0 <=Int ABI_y ) - #then #gas ( ( VGas +Int -136 ) ) - #else #if 0 <=Int ABI_y - #then #gas ( ( VGas +Int -122 ) ) - #else #gas ( ( VGas +Int -136 ) ) - #fi - #fi - VMemoryUsed + .WordStack => ?_ + .Bytes => ?_ + 0 => ?_ + #gas(VGas) => #gas ( ( ( ( ( ( VGas -Int Csstore( ISTANBUL , ( Sin -Int ABI_rad ) , Sin , Junk_0 ) ) -Int Csstore( ISTANBUL , ( Dai -Int ABI_rad ) , Dai , Junk_1 ) ) -Int Csstore( ISTANBUL , ( Vice -Int ABI_rad ) , Vice , Junk_2 ) ) -Int Csstore( ISTANBUL , ( Debt -Int ABI_rad ) , Debt , Junk_3 ) ) +Int -8616 ) ) + 0 => ?_ _ => ?_ - _ + false VCallDepth @@ -76,8 +69,8 @@ module VAT-SUBUI-PASS-SPEC ACCT_ID ACCT_ID_balance Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - _ACCT_ID_ORIG_STORAGE + ACCT_ID_STORAGE => ACCT_ID_STORAGE [ #Vat.sin[CALLER_ID] <- Sin -Int ABI_rad ] [ #Vat.dai[CALLER_ID] <- Dai -Int ABI_rad ] [ #Vat.vice <- Vice -Int ABI_rad ] [ #Vat.debt <- Debt -Int ABI_rad ] + ACCT_ID_ORIG_STORAGE Nonce_Vat ... @@ -99,12 +92,35 @@ module VAT-SUBUI-PASS-SPEC andBool #rangeUInt(256, VChainId) andBool #rangeNonce(Nonce_Vat) - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeSInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1015) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x -Int ABI_y))))))) - + andBool (#rangeUInt(256, ABI_rad) + andBool (#rangeUInt(256, Dai) + andBool (#rangeUInt(256, Sin) + andBool (#rangeUInt(256, Debt) + andBool (#rangeUInt(256, Vice) + andBool (lengthBytes(CD) <=Int 1250000000 + andBool (#rangeUInt(256, Junk_0) + andBool (#rangeUInt(256, Junk_1) + andBool (#rangeUInt(256, Junk_2) + andBool (#rangeUInt(256, Junk_3) + andBool (((VCallValue ==Int 0)) + andBool ((#rangeUInt(256, Dai -Int ABI_rad)) + andBool ((#rangeUInt(256, Sin -Int ABI_rad)) + andBool ((#rangeUInt(256, Debt -Int ABI_rad)) + andBool ((#rangeUInt(256, Vice -Int ABI_rad))))))))))))))))) + andBool #lookup(ACCT_ID_STORAGE, #Vat.sin[CALLER_ID]) ==Int Sin + andBool #lookup(ACCT_ID_STORAGE, #Vat.dai[CALLER_ID]) ==Int Dai + andBool #lookup(ACCT_ID_STORAGE, #Vat.vice) ==Int Vice + andBool #lookup(ACCT_ID_STORAGE, #Vat.debt) ==Int Debt + andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.sin[CALLER_ID]) ==Int Junk_0 + andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.dai[CALLER_ID]) ==Int Junk_1 + andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.vice) ==Int Junk_2 + andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.debt) ==Int Junk_3 + andBool #Vat.sin[CALLER_ID] =/=Int #Vat.dai[CALLER_ID] + andBool #Vat.sin[CALLER_ID] =/=Int #Vat.vice + andBool #Vat.sin[CALLER_ID] =/=Int #Vat.debt + andBool #Vat.dai[CALLER_ID] =/=Int #Vat.vice + andBool #Vat.dai[CALLER_ID] =/=Int #Vat.debt + andBool #Vat.vice =/=Int #Vat.debt endmodule diff --git a/tests/specs/mcd/vat-move-diff-rough-spec.k b/tests/specs/mcd/vat-move-diff-rough-spec.k index 823860bdc4..f8aa1d7025 100644 --- a/tests/specs/mcd/vat-move-diff-rough-spec.k +++ b/tests/specs/mcd/vat-move-diff-rough-spec.k @@ -1,8 +1,10 @@ requires "verification.k" +requires "vat-arithmetic-spec.k" module VAT-MOVE-DIFF-ROUGH-SPEC - imports VAT-MOVE-DIFF-ROUGH-ARITH-SPEC + imports VERIFICATION + imports VAT-ARITHMETIC-SPEC // Vat_move-diff claim [Vat.move-diff.pass.rough]: @@ -119,207 +121,6 @@ module VAT-MOVE-DIFF-ROUGH-SPEC andBool #Vat.can[ABI_src][CALLER_ID] =/=Int #Vat.dai[ABI_src] andBool #Vat.can[ABI_src][CALLER_ID] =/=Int #Vat.dai[ABI_dst] andBool #Vat.dai[ABI_src] =/=Int #Vat.dai[ABI_dst] - [depends(VAT-MOVE-DIFF-ROUGH-ARITH-SPEC.Vat.adduu.pass,VAT-MOVE-DIFF-ROUGH-ARITH-SPEC.Vat.subuu.pass)] + [depends(VAT-ARITHMETIC-SPEC.Vat.adduu.pass,VAT-ARITHMETIC-SPEC.Vat.subuu.pass)] endmodule - - -module VAT-MOVE-DIFF-ROUGH-ARITH-SPEC - imports VERIFICATION - - // Vat_adduu - claim [Vat.adduu.pass]: - #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - ABI_y : ABI_x : JMPTO : WS => ABI_x +Int ABI_y : WS - _ - 13086 => 13111 - #gas(VGas) => #gas ( ( VGas -Int 62 ) ) - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - _ACCT_ID_ORIG_STORAGE - Nonce_Vat - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - andBool #rangeNonce(Nonce_Vat) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeUInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 100) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) - [trusted] - - // Vat_subuu - claim [Vat.subuu.pass]: - #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - ABI_y : ABI_x : JMPTO : WS => ABI_x -Int ABI_y : WS - _ - 13060 => 13085 - #gas(VGas) => #gas ( ( VGas -Int 62 ) ) - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - _ACCT_ID_ORIG_STORAGE - Nonce_Vat - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - andBool #rangeNonce(Nonce_Vat) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeUInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 100) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x -Int ABI_y))))))) - [trusted] - -endmodule - diff --git a/tests/specs/mcd/vat-muluu-pass-spec.k b/tests/specs/mcd/vat-sin-pass-spec.k similarity index 74% rename from tests/specs/mcd/vat-muluu-pass-spec.k rename to tests/specs/mcd/vat-sin-pass-spec.k index 8bea0b55da..04203dac71 100644 --- a/tests/specs/mcd/vat-muluu-pass-spec.k +++ b/tests/specs/mcd/vat-sin-pass-spec.k @@ -1,19 +1,17 @@ - requires "verification.k" -module VAT-MULUU-PASS-SPEC +module VAT-SIN-PASS-SPEC imports VERIFICATION - // Vat_muluu - claim [Vat.muluu.pass]: - #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION + claim [Vat.sin.pass]: + #execute ~> CONTINUATION => #halt ~> CONTINUATION NORMAL ISTANBUL true - VOutput => VOutput - _ => ?_ + _ => #buf(32, Rad) + _ => EVMC_SUCCESS _VCallStack _ _ => ?_ @@ -22,16 +20,13 @@ module VAT-MULUU-PASS-SPEC #computeValidJumpDests(Vat_bin_runtime) ACCT_ID CALLER_ID - _ => ?_ + #abiCallData("sin", #address(ABI_usr)) +Bytes CD => ?_ VCallValue - ABI_y : ABI_x : JMPTO : WS => ABI_x *Int ABI_y : WS - _ - 13234 => 13277 - #gas(VGas) => #if ABI_y ==Int 0 - #then #gas ( ( VGas +Int -62 ) ) - #else #gas ( ( VGas +Int -114 ) ) - #fi - VMemoryUsed + .WordStack => ?_ + .Bytes => ?_ + 0 => ?_ + #gas(VGas) => #gas ( ( VGas +Int -1235 ) ) + 0 => ?_ _ => ?_ _ VCallDepth @@ -76,7 +71,7 @@ module VAT-MULUU-PASS-SPEC Vat_bin_runtime ACCT_ID_STORAGE => ACCT_ID_STORAGE ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ + Nonce_Vat ... @@ -95,11 +90,15 @@ module VAT-MULUU-PASS-SPEC andBool VCallDepth <=Int 1024 andBool #rangeUInt(256, VCallValue) andBool #rangeUInt(256, VChainId) + andBool #rangeNonce(Nonce_Vat) + + andBool (#rangeAddress(ABI_usr) + andBool (#rangeUInt(256, Rad) + andBool (lengthBytes(CD) <=Int 1250000000 + andBool (#rangeUInt(256, Junk_0) + andBool ((VCallValue ==Int 0)))))) - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeUInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1000) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x *Int ABI_y))))))) + andBool #lookup(ACCT_ID_STORAGE, #Vat.sin[ABI_usr]) ==Int Rad + andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.sin[ABI_usr]) ==Int Junk_0 endmodule diff --git a/tests/specs/mcd/vat-slip-pass-rough-spec.k b/tests/specs/mcd/vat-slip-pass-rough-spec.k index 89a7e60d77..42285572e7 100644 --- a/tests/specs/mcd/vat-slip-pass-rough-spec.k +++ b/tests/specs/mcd/vat-slip-pass-rough-spec.k @@ -1,7 +1,9 @@ requires "verification.k" +requires "vat-arithmetic-spec.k" module VAT-SLIP-PASS-ROUGH-SPEC imports VERIFICATION + imports VAT-ARITHMETIC-SPEC // Vat_slip claim [Vat.slip.pass.rough]: @@ -110,108 +112,6 @@ module VAT-SLIP-PASS-ROUGH-SPEC andBool #lookup(ACCT_ID_ORIG_STORAGE, #Vat.gem[ABI_ilk][ABI_usr]) ==Int Junk_1 andBool #Vat.wards[CALLER_ID] =/=Int #Vat.gem[ABI_ilk][ABI_usr] - [depends(Vat.addui.pass)] - - // Vat_addui - claim [Vat.addui.pass]: - #execute ~> CONTINUATION => JUMP JMPTO ~> #pc [ JUMP ] ~> #execute ~> CONTINUATION - NORMAL - ISTANBUL - true - - - VOutput => VOutput - _ => ?_ - _VCallStack - _ - _ => ?_ - - Vat_bin_runtime - #computeValidJumpDests(Vat_bin_runtime) - ACCT_ID - CALLER_ID - _ => ?_ - VCallValue - chop(ABI_y) : ABI_x : JMPTO : WS => ABI_x +Int ABI_y : WS - _ - 13112 => 13174 - #gas(VGas) => #if ( ABI_y - VMemoryUsed - _ => ?_ - _ - VCallDepth - - - _VSelfDestruct - _ => ?_ - _Vrefund => ?_ - _ => ?_ - _ => ?_ - - _ - ORIGIN_ID - _ - - _ - _ - _ - _ - _ - _ - _ - _ - _BLOCK_NUMBER - _ - _ - TIME - _ - _ - _ - _ - _ - _ - - - - VChainId - - - ACCT_ID - ACCT_ID_balance - Vat_bin_runtime - ACCT_ID_STORAGE => ACCT_ID_STORAGE - ACCT_ID_ORIG_STORAGE - _Nonce_Vat => ?_ - - ... - - _ - _ - _ - - - requires #rangeAddress(ACCT_ID) - andBool ACCT_ID =/=Int 0 - andBool #notPrecompileAddress(ACCT_ID) - andBool #rangeAddress(CALLER_ID) - andBool #rangeAddress(ORIGIN_ID) - andBool #rangeUInt(256, TIME) - andBool #rangeUInt(256, ACCT_ID_balance) - andBool VCallDepth <=Int 1024 - andBool #rangeUInt(256, VCallValue) - andBool #rangeUInt(256, VChainId) - - andBool (#rangeUInt(256, ABI_x) - andBool (#rangeSInt(256, ABI_y) - andBool ((#sizeWordStack(WS) <=Int 1015) - andBool (#rangeUInt(256, VMemoryUsed) - andBool ((#rangeUInt(256, ABI_x +Int ABI_y))))))) - [trusted] + [depends(VAT-ARITHMETIC-SPEC.Vat.addui.pass)] endmodule diff --git a/tests/specs/mcd/vat-spec.k b/tests/specs/mcd/vat-spec.k new file mode 100644 index 0000000000..a96c5f1de3 --- /dev/null +++ b/tests/specs/mcd/vat-spec.k @@ -0,0 +1,33 @@ +requires "vat-addui-fail-rough-spec.k" +requires "vat-arithmetic-spec.k" +requires "vat-dai-pass-spec.k" +requires "vat-deny-diff-fail-rough-spec.k" +requires "vat-flux-diff-pass-rough-spec.k" +requires "vat-flux-diff-pass-spec.k" +requires "vat-fold-pass-rough-spec.k" +requires "vat-fork-diff-pass-rough-spec.k" +requires "vat-frob-diff-zero-dart-pass-rough-spec.k" +requires "vat-heal-pass-spec.k" +requires "vat-move-diff-rough-spec.k" +requires "vat-sin-pass-spec.k" +requires "vat-slip-pass-rough-spec.k" +requires "vat-subui-fail-rough-spec.k" + +module VAT-SPEC + + imports VAT-ADDUI-FAIL-ROUGH-SPEC + imports VAT-ARITHMETIC-SPEC + imports VAT-DAI-PASS-SPEC + imports VAT-DENY-DIFF-FAIL-ROUGH-SPEC + imports VAT-FLUX-DIFF-PASS-ROUGH-SPEC + imports VAT-FLUX-DIFF-PASS-SPEC + imports VAT-FOLD-PASS-ROUGH-SPEC + imports VAT-FORK-DIFF-PASS-ROUGH-SPEC + imports VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC + imports VAT-HEAL-PASS-SPEC + imports VAT-MOVE-DIFF-ROUGH-SPEC + imports VAT-SIN-PASS-SPEC + imports VAT-SLIP-PASS-ROUGH-SPEC + imports VAT-SUBUI-FAIL-ROUGH-SPEC + +endmodule