Upstream simplified Optimism test (#369)

* Upstream `PortalTest.test_withdrawal_paused` with lemmas, update expected output * Set Version: 0.1.160 * Set Version: 0.1.161 * Simplify `test_withdrawal_paused` to speed it up * Experimental: temp increase CI timeout * Set Version: 0.1.165 * Set Version: 0.1.172 * Set Version: 0.1.177 * Set Version: 0.1.179 * Optimism lemmas cleanup * Update simplified OptimismTest corresponding to the copying loop lemma * Set Version: 0.1.180 * Set Version: 0.1.185 * Upstreamed simplified `PortalTest` * Cleanup updated `contracts.k` and `foundry.k` * Update output for `testFail_assume_true` w/simplifications, cosmetic changes in `foundry.k` * Set Version: 0.1.188 * Update output for `test_assume_false` * Update revert message in `Portal` Co-authored-by: Andrei Văcaru <[email protected]> * Set Version: 0.1.189 * Set Version: 0.1.190 * Set Version: 0.1.192 * Remove reflexivity lemma * Update bytecode for `Portal` * Set Version: 0.1.205 * Revert `lemmas.k` renaming * Formatting in tests * Set Version: 0.1.210 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]>
runtimeverification · Mar 18, 2024 · 0d997ea · 0d997ea
1 parent d614f9a
commit 0d997ea
Show file tree

Hide file tree

Showing 13 changed files with 595 additions and 31 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.209
+0.1.210
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.209"
+version = "0.1.210"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.209'
+VERSION: Final = '0.1.210'
diff --git a/src/tests/integration/conftest.py b/src/tests/integration/conftest.py
@@ -70,8 +70,17 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo
             foundry_kompile(
                 foundry=Foundry(foundry_root),
                 includes=(),
-                requires=[str(TEST_DATA_DIR / 'lemmas.k'), str(TEST_DATA_DIR / 'cse-lemmas.k')],
-                imports=['LoopsTest:SUM-TO-N-INVARIANT', 'ArithmeticCallTest:CSE-LEMMAS', 'CSETest:CSE-LEMMAS'],
+                requires=[
+                    str(TEST_DATA_DIR / 'lemmas.k'),
+                    str(TEST_DATA_DIR / 'cse-lemmas.k'),
+                    str(TEST_DATA_DIR / 'pausability-lemmas.k'),
+                ],
+                imports=[
+                    'LoopsTest:SUM-TO-N-INVARIANT',
+                    'ArithmeticCallTest:CSE-LEMMAS',
+                    'CSETest:CSE-LEMMAS',
+                    'PortalTest:PAUSABILITY-LEMMAS',
+                ],
             )
 
     session_foundry_root = tmp_path_factory.mktemp('foundry')

diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all
@@ -185,6 +185,7 @@ PlainPrankTest.test_startPrankWithOrigin_true()
 PlainPrankTest.test_startPrank_zeroAddress_true()
 PlainPrankTest.test_stopPrank_notExistent()
 PlainPrankTest.test_prank_expectRevert()
+PortalTest.test_withdrawal_paused((uint256,address,address,uint256,uint256,bytes),uint256,(bytes32,bytes32,bytes32,bytes32),bytes[])
 PrankTest.testAddAsOwner(uint256)
 PrankTest.testAddStartPrank(uint256)
 PrankTest.testFailAddPrank(uint256)

diff --git a/src/tests/integration/test-data/foundry-prove-skip-legacy b/src/tests/integration/test-data/foundry-prove-skip-legacy
@@ -182,6 +182,7 @@ PlainPrankTest.test_prank_zeroAddress_true()
 PlainPrankTest.test_startPrank_true()
 PlainPrankTest.test_startPrankWithOrigin_true()
 PlainPrankTest.test_startPrank_zeroAddress_true()
+PortalTest.test_withdrawal_paused((uint256,address,address,uint256,uint256,bytes),uint256,(bytes32,bytes32,bytes32,bytes32),bytes[])
 PrankTestMsgSender.test_msgsender_setup()
 PrankTestOrigin.test_origin_setup()
 PrankTest.testAddAsOwner(uint256)

diff --git a/src/tests/integration/test-data/foundry/src/Portal.sol b/src/tests/integration/test-data/foundry/src/Portal.sol
@@ -0,0 +1,50 @@
+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;
+    }
+}
+
+contract Portal  {
+    bool paused;
+
+    /// @notice Emitted when a withdrawal transaction is proven.
+    event WithdrawalProven(address indexed from, address indexed to);
+
+    /// @notice Reverts when paused.
+    modifier whenNotPaused() {
+        require(paused == false, "Portal: paused");
+        _;
+    }
+
+    constructor() {
+        paused = true;
+    }
+
+    /// @notice Proves a withdrawal transaction.
+    function proveWithdrawalTransaction(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+        whenNotPaused
+    {
+        // Emit a `WithdrawalProven` event.
+        emit WithdrawalProven(_tx.sender, _tx.target);
+    }
+}
diff --git a/src/tests/integration/test-data/foundry/test/PortalTest.sol b/src/tests/integration/test-data/foundry/test/PortalTest.sol
@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import "forge-std/Test.sol";
+import "../src/Portal.sol";
+
+contract PortalTest is Test {
+    Portal portalContract;
+
+    function setUp() public {
+        portalContract = new Portal();
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 1,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 32,
+    function test_withdrawal_paused(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        vm.expectRevert();
+        portalContract.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+}
diff --git a/src/tests/integration/test-data/pausability-lemmas.k b/src/tests/integration/test-data/pausability-lemmas.k
@@ -0,0 +1,182 @@
+requires "evm.md"
+requires "foundry.md"
+
+module PAUSABILITY-LEMMAS [symbolic]
+    imports BOOL
+    imports FOUNDRY
+    imports INT-SYMBOLIC
+
+    syntax StepSort ::= Int
+                      | Bool
+                      | Bytes
+                      | Set
+ // ------------------------
+
+    syntax KItem ::= runLemma ( StepSort )
+                   | doneLemma( StepSort )
+ // --------------------------------------
+    rule <k> runLemma(T) => doneLemma(T) ... </k>
+
+    // We need to enforce some limit on the length of bytearrays
+    // and indices into bytearrays in order to avoid chop-reasoning
+    syntax Int ::= "maxBytesLength" [alias]
+    rule maxBytesLength => 9223372036854775808
+
+
+    // Deconstruction of <<Int into #buf
+    rule X <<Int Y => #asWord ( #buf ( 32 -Int (Y /Int 8) , X ) +Bytes #buf ( Y /Int 8 , 0 ) )
+      requires 0 <=Int X andBool X <Int 2 ^Int (256 -Int Y)
+       andBool 0 <=Int Y andBool Y <=Int 256 andBool Y modInt 8 ==Int 0
+      [simplification, concrete(Y)]
+
+    //
+    // Arithmetic
+    //
+
+    // Cancellativity #1
+    rule A +Int B -Int B +Int C => A +Int C [simplification]
+
+    // Cancellativity #2
+    rule A -Int B +Int C -Int D +Int B +Int E => A -Int D +Int C +Int E [simplification]
+
+    // Cancellativity #3
+    rule ( A +Int B ) +Int C <=Int ( D +Int B ) +Int E => A +Int C <=Int D +Int E [simplification]
+
+    // Cancellativity #4
+    rule A +Int B <=Int ( A +Int C ) +Int D => B <=Int C +Int D [simplification]
+
+    // Cancellativity #5
+    rule A +Int ( (B -Int A) +Int C ) => B +Int C [simplification]
+
+    // Cancellativity #6
+    rule (A -Int B) -Int (C -Int B) => A -Int C [simplification]
+
+    // Upper bound on (pow256 - 32) &Int lengthBytes(X)
+    rule notMaxUInt5 &Int Y <=Int Y => true
+      requires 0 <=Int Y
+      [simplification]
+
+    // Bounds on notMaxUInt5 &Int ( X +Int 31 )
+    // Note: upstream in the next round
+    rule X <=Int   notMaxUInt5 &Int ( X +Int 31 )          => true requires 0 <=Int X                   [simplification]
+    rule X <=Int   notMaxUInt5 &Int ( Y +Int 31 )          => true requires X <=Int 0 andBool 0 <=Int Y [simplification, concrete(X)]
+    rule X <=Int ( notMaxUInt5 &Int ( X +Int 31 ) ) +Int Y => true requires 0 <=Int X andBool 0 <=Int Y [simplification, concrete(Y)]
+
+    rule notMaxUInt5 &Int X +Int 31 <Int Y => true requires 0 <=Int X andBool X +Int 32 <=Int Y [simplification, concrete(Y)]
+
+    rule notMaxUInt5 &Int X +Int 31 <Int X +Int 32 => true requires 0 <=Int X [simplification]
+
+    //
+    // #asWord
+    //
+
+    // Move to function parameters
+    rule { #asWord ( X ) #Equals #asWord ( Y ) } => #Top
+      requires X ==K Y
+      [simplification]
+
+    // #asWord ignores leading zeros
+    rule #asWord ( BA1 +Bytes BA2 ) => #asWord ( BA2 )
+      requires #asInteger(BA1) ==Int 0
+      [simplification, concrete(BA1)]
+
+
+    // Equality and #range
+    rule #asWord ( #range ( #buf ( 32 , _X:Int ) , S:Int , W:Int ) ) ==Int Y:Int => false
+        requires S +Int W <=Int 32
+         andBool (2 ^Int (8 *Int W)) <=Int Y
+        [concrete(S, W, Y), simplification]
+
+    // Conversion from bytes always yields a non-negative integer
+    rule 0 <=Int #asInteger ( _ ) => true [simplification]
+
+    //
+    // #padRightToWidth
+    //
+
+    rule #padRightToWidth (W, X) => X +Bytes #buf(W -Int lengthBytes(X), 0)
+      [concrete(W), simplification]
+
+    //
+    // #range(M, START, WIDTH)
+    //
+
+    // Parameter equality
+    rule { #range (A, B, C) #Equals #range (A, B, D) } => #Top
+      requires C ==Int D
+      [simplification]
+
+    //
+    // Bytes indexing and update
+    //
+
+    rule B:Bytes [ X:Int ] => #asWord ( #range (B, X, 1) )
+      requires X <=Int lengthBytes(B)
+      [simplification(40)]
+
+    // Empty update has no effect
+    rule B:Bytes [ START:Int := b"" ] => B
+      requires 0 <=Int START andBool START <=Int lengthBytes(B)
+      [simplification]
+
+    // Consecutive quasi-contiguous byte-array update
+    rule B [ S1 := B1 ] [ S2 := B2 ] => B [ S1 := #range(B1, 0, S2 -Int S1) +Bytes B2 ]
+      requires 0 <=Int S1 andBool S1 <=Int S2 andBool S2 <=Int S1 +Int lengthBytes(B1)
+      [simplification]
+
+    // Parameter equality: byte-array update
+    rule { B1:Bytes [ S1:Int := B2:Bytes ] #Equals B3:Bytes [ S2:Int := B4:Bytes ] } => #Top
+      requires B1 ==K B3 andBool S1 ==Int S2 andBool B2 ==K B4
+      [simplification]
+
+    //
+    // SUMMARIES
+    //
+
+    // This rule cannot be used without the [symbolic] tag because it uses
+    // "existentials", which is not correct, it uses variables that are learnt
+    // from the requires and not from the structure
+
+    // copy-memory-to-memory
+    rule [test-copy-memory-to-memory-summary]:
+      <k> #execute ... </k>
+      <useGas> false </useGas>
+      <schedule> SHANGHAI </schedule>
+      <jumpDests> JUMPDESTS </jumpDests>
+      // The program and program counter are symbolic, focusing on the part we will be executing (CP)
+      <program> PROGRAM </program>
+      <pc> PCOUNT => PCOUNT +Int 44 </pc>
+      // The word stack has the appropriate form, as per the compiled code
+      <wordStack> SRC : DEST : LENGTH : WS </wordStack>
+      // The program copies LENGTH bytes of memory from SRC +Int 32 to DEST +Int OFFSET,
+      // padded with 32 zeros in case LENGTH is not divisible by 32
+      <localMem>
+        LM => LM [ DEST := #range ( LM, SRC, LENGTH ) +Bytes
+                                   #buf ( ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) , 0 ) +Bytes
+                                   #buf ( ( ( ( 32 -Int ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) ) ) modInt 32 ), 0 ) ]
+      </localMem>
+      requires
+       // The current program we are executing differs from the original one only in the hardcoded jump addresses,
+       // which are now relative to PCOUNT, and the hardcoded offset, which is now symbolic.
+               #range(PROGRAM, PCOUNT, 44) ==K b"[`\x00[\x83\x81\x10\x15a\n\x9fW\x81\x81\x01Q\x83\x82\x01R` \x01a\n\x87V[\x83\x81\x11\x15a\n\xaeW`\x00\x84\x84\x01R[P"
+                                               [ 09 := #buf(2, PCOUNT +Int 27) ]
+                                               [ 24 := #buf(2, PCOUNT +Int  3) ]
+                                               [ 33 := #buf(2, PCOUNT +Int 42) ]
+
+       // Various well-formedness constraints. In particular, the maxBytesLength-related ones are present to
+       // remove various chops that would otherwise creep into the execution, and are reasonable since byte
+       // arrays in actual programs would never reach that size.
+       andBool 0 <=Int PCOUNT
+       andBool 0 <=Int LENGTH andBool LENGTH <Int maxBytesLength
+       andBool 0 <=Int SRC    andBool SRC    <Int maxBytesLength
+       andBool 0 <=Int DEST   andBool DEST   <Int maxBytesLength
+       andBool #sizeWordStack(WS) <=Int 1015
+
+       andBool SRC +Int LENGTH <=Int DEST // No overlap between source and destination
+       andBool DEST <=Int lengthBytes(LM) // Destination starts within current memory
+       // All JUMPDESTs in the program are valid
+       andBool (PCOUNT +Int 3) in JUMPDESTS andBool (PCOUNT +Int 27) in JUMPDESTS andBool (PCOUNT +Int 42) in JUMPDESTS
+       andBool PCOUNT +Int 42 <Int 2 ^Int 16  // and fit into two bytes
+      [priority(30), concrete(JUMPDESTS, PROGRAM, PCOUNT), preserves-definedness]
+
+endmodule