Add Wonderland demo tests

.gitmodules

@@ -1,8 +1,8 @@
-[submodule "lib/forge-std"]
-	path = lib/forge-std
+[submodule "oz_erc20/lib/forge-std"]
+	path = oz_erc20/lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
-[submodule "lib/kontrol-cheatcodes"]
-	path = lib/kontrol-cheatcodes
+[submodule "oz_erc20/lib/kontrol-cheatcodes"]
+	path = oz_erc20/lib/kontrol-cheatcodes
 	url = https://github.com/runtimeverification/kontrol-cheatcodes.git
 [submodule "oz_erc20/lib/forge-std"]
 	path = oz_erc20/lib/forge-std
@@ -13,3 +13,9 @@
 [submodule "oz_erc20/lib/openzeppelin-contracts"]
 	path = oz_erc20/lib/openzeppelin-contracts
 	url = https://github.com/OpenZeppelin/openzeppelin-contracts
+[submodule "wonderland/lib/forge-std"]
+	path = wonderland/lib/forge-std
+	url = https://github.com/foundry-rs/forge-std
+[submodule "wonderland/lib/kontrol-cheatcodes"]
+	path = wonderland/lib/kontrol-cheatcodes
+	url = https://github.com/runtimeverification/kontrol-cheatcodes

oz_erc20/test/RebasingToken.t.sol

@@ -0,0 +1,23 @@
+pragma solidity ^0.8.13;
+
+import {Test, console} from "forge-std/Test.sol";
+
+contract RebasingTokenTest is Test {
+    function check_balanceToRebasingCredits(uint256 rebasingCreditsPerToken, uint256 balance) public {
+        vm.assume(rebasingCreditsPerToken <= 1e27 && rebasingCreditsPerToken >= 1e18);
+        vm.assume(balance <= 1e25);
+
+        uint256 rebasingCredits = ((balance) * rebasingCreditsPerToken + 1e18 - 1) / 1e18;
+        uint256 actualBalance = (rebasingCredits * 1e18) / rebasingCreditsPerToken;
+        assert(actualBalance == balance);
+    }
+
+    function testFail_balanceToRebasingCredits(uint256 rebasingCreditsPerToken, uint256 balance) public {
+        vm.assume(rebasingCreditsPerToken <= 1e27); // && rebasingCreditsPerToken >= 1e18);
+        vm.assume(balance <= 1e25);
+
+        uint256 rebasingCredits = ((balance) * rebasingCreditsPerToken + 1e18 - 1) / 1e18;
+        uint256 actualBalance = (rebasingCredits * 1e18) / rebasingCreditsPerToken;
+        assert(actualBalance == balance);
+    }
+}

wonderland/.gitignore

@@ -0,0 +1,14 @@
+# Compiler files
+cache/
+out/
+
+# Ignores development broadcast logs
+!/broadcast
+/broadcast/*/31337/
+/broadcast/**/dry-run/
+
+# Docs
+docs/
+
+# Dotenv file
+.env

wonderland/KONTROL.md

@@ -0,0 +1,54 @@
+
+## Kontrol
+
+**Kontrol grants developers the ability to perform formal verification without learning a new language or tool.**
+
+## Documentation
+
+https://docs.runtimeverification.com/kontrol/cheatsheets/kontrol-cheatsheet
+
+## Usage
+
+### Build
+
+```shell
+$ kontrol build
+```
+
+### Test
+
+```shell
+$ kontrol prove --match-test 'ContractName.TestName()'
+```
+
+### List
+
+```shell
+$ kontrol list
+```
+
+### Show
+
+```shell
+$ kontrol show --match-test 'ContractName.TestName()'
+```
+
+### Explore KCFG
+
+```shell
+$ kontrol view-kcfg 'ContractName.TestName()'
+```
+
+### Clean
+
+```shell
+$ kontrol clean
+```
+
+
+### Help
+
+```shell
+$ kontrol --help
+$ kontrol command --help
+```

wonderland/README.md

@@ -0,0 +1,66 @@
+## Foundry
+
+**Foundry is a blazing fast, portable and modular toolkit for Ethereum application development written in Rust.**
+
+Foundry consists of:
+
+-   **Forge**: Ethereum testing framework (like Truffle, Hardhat and DappTools).
+-   **Cast**: Swiss army knife for interacting with EVM smart contracts, sending transactions and getting chain data.
+-   **Anvil**: Local Ethereum node, akin to Ganache, Hardhat Network.
+-   **Chisel**: Fast, utilitarian, and verbose solidity REPL.
+
+## Documentation
+
+https://book.getfoundry.sh/
+
+## Usage
+
+### Build
+
+```shell
+$ forge build
+```
+
+### Test
+
+```shell
+$ forge test
+```
+
+### Format
+
+```shell
+$ forge fmt
+```
+
+### Gas Snapshots
+
+```shell
+$ forge snapshot
+```
+
+### Anvil
+
+```shell
+$ anvil
+```
+
+### Deploy
+
+```shell
+$ forge script script/Counter.s.sol:CounterScript --rpc-url <your_rpc_url> --private-key <your_private_key>
+```
+
+### Cast
+
+```shell
+$ cast <subcommand>
+```
+
+### Help
+
+```shell
+$ forge --help
+$ anvil --help
+$ cast --help
+```

wonderland/foundry.toml

@@ -0,0 +1,8 @@
+[profile.default]
+src = "src"
+out = "out"
+libs = ["lib"]
+
+# See more config options https://github.com/foundry-rs/foundry/blob/master/crates/config/README.md#all-options
+
+extra_output = ['storageLayout']

wonderland/kontrol.toml

@@ -0,0 +1,41 @@
+[build.default]
+foundry-project-root       = '.'
+regen                      = false
+rekompile                  = false
+verbose                    = false
+debug                      = false
+require                    = 'lemmas.k'
+module-import              = 'TestBase:KONTROL-LEMMAS'
+auxiliary-lemmas           = true
+
+[prove.default]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 25000
+reinit                     = false
+cse                        = false
+workers                    = 4
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 1000
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+run-constructor            = false
+symbolic-immutables        = true
+
+[show.default]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+use-hex-encoding           = false
+
+[view-kcfg.default]
+foundry-project-root       = '.'
+use-hex-encoding           = false

wonderland/lemmas.k

@@ -0,0 +1,14 @@
+requires "foundry.md"
+
+module KONTROL-LEMMAS
+
+// Your lemmas go here
+// Not sure what to do next? Try checking the documentation for writing lemmas: https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/kevm-lemmas
+
+    imports FOUNDRY
+
+    /*
+    rule bool2Word ( X ) => 1 requires X         [simplification]
+    rule bool2Word ( X ) => 0 requires notBool X [simplification]
+    */
+endmodule

wonderland/src/Portal.sol

@@ -0,0 +1,98 @@
+// SPDX-License-Identifier: MIT
+// (The MIT License)
+
+// Copyright 2020-2024 Optimism
+
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+// IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+// CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+// TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+// SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+pragma solidity ^0.8.13;
+
+library Types {
+    struct OutputRootProof {
+        bytes32 version;
+        bytes32 stateRoot;
+        bytes32 messagePasserStorageRoot;
+        bytes32 latestBlockhash;
+    }
+
+    struct WithdrawalTransaction {
+        uint256 nonce;
+        address sender;
+        address target;
+        uint256 value;
+        uint256 gasLimit;
+        bytes data;
+    }
+}
+
+// Adapted from https://github.com/ethereum-optimism/optimism
+contract Portal  {
+    bool public paused;
+    address public guardian;
+
+    /// @notice Emitted when a withdrawal transaction is proven.
+    event WithdrawalProven(address indexed from, address indexed to);
+
+    /// @notice Emitted when the conract is paused.
+    event Paused();
+
+    /// @notice Reverts when paused.
+    modifier whenNotPaused() {
+        require(paused == false, "Portal: paused");
+        _;
+    }
+
+    constructor() {
+        guardian = msg.sender;
+    }
+
+    /// @notice Pauses this contract.
+    function pause()
+        external
+        whenNotPaused
+    {
+        require(msg.sender == guardian, "Portal: not a guardian");
+        paused = true;
+        // Emit a `Paused` event.
+        emit Paused();
+    }
+
+    /// @notice Accepts ETH value without triggering a deposit to L2.
+    ///         This function mainly exists for the sake of the migration between the legacy
+    ///         Optimism system and Bedrock.
+    function donateETH() external payable {
+        // Intentionally empty.
+    }
+
+   /// @notice Proves a withdrawal transaction.
+    function proveWithdrawalTransaction(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+        whenNotPaused
+    {
+        // Implementation omitted
+        // Emit a `WithdrawalProven` event.
+        emit WithdrawalProven(_tx.sender, _tx.target);
+    }
+}