From e8f4ab7e836a33dfac14e3b02749c04c89f96195 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 12:54:30 +0700
Subject: [PATCH] Update expected output, remove `Accounts` test

---
 .../test-data/foundry-dependency-all          |   2 -
 .../test-data/foundry/src/cse/Accounts.sol    |  34 --
 .../AddConst.applyOp(uint256).cse.expected    |  18 +-
 ...ctFieldTest.testEscrowToken().cse.expected | 309 ++++++++++++++++++
 ...ImportedContract.add(uint256).cse.expected |  22 +-
 .../ImportedContract.count().cse.expected     |   6 +-
 .../show/ImportedContract.init.cse.expected   |   2 +-
 ...ImportedContract.set(uint256).cse.expected |  18 +-
 .../test-data/show/contracts.k.expected       |  26 +-
 .../test-data/show/foundry.k.expected         |  14 +-
 10 files changed, 362 insertions(+), 89 deletions(-)
 delete mode 100644 src/tests/integration/test-data/foundry/src/cse/Accounts.sol
 create mode 100644 src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected

diff --git a/src/tests/integration/test-data/foundry-dependency-all b/src/tests/integration/test-data/foundry-dependency-all
index c6ecf9343..5880aa6c5 100644
--- a/src/tests/integration/test-data/foundry-dependency-all
+++ b/src/tests/integration/test-data/foundry-dependency-all
@@ -7,8 +7,6 @@ ArithmeticContract.add_sub_external(uint256,uint256,uint256)
 CSETest.test_add_const(uint256,uint256)
 CSETest.test_identity(uint256,uint256)
 ConstructorTest.test_contract_call()
-ContractFieldTest.testEscrowToken()
-CompositionalAccounts.getEscrowToken()
 Identity.applyOp(uint256)
 Identity.identity(uint256)
 ImportedContract.set(uint256)
diff --git a/src/tests/integration/test-data/foundry/src/cse/Accounts.sol b/src/tests/integration/test-data/foundry/src/cse/Accounts.sol
deleted file mode 100644
index a36409ede..000000000
--- a/src/tests/integration/test-data/foundry/src/cse/Accounts.sol
+++ /dev/null
@@ -1,34 +0,0 @@
-// SPDX-License-Identifier: UNLICENSED
-pragma solidity =0.8.13;
-import {Test} from "forge-std/Test.sol";
-
-contract CompositionalToken {
-    uint256 public totalSupply;
-
-    constructor(uint256 _totalSupply) {
-        totalSupply = _totalSupply;
-    }
-}
-
-contract CompositionalEscrow {
-    CompositionalToken cseToken;
-
-    constructor(uint256 _totalSupply) {
-        cseToken = new CompositionalToken(_totalSupply);
-    }
-
-    function getTokenTotalSupply() public returns (uint256) {
-        return cseToken.totalSupply() + 15;
-    }
-}
-
-contract CompositionalAccounts {
-    CompositionalEscrow cseEscrow;
-
-    /* Calling `getTokenTotalSupply` will summarize `totalSupply` and
-       include `CompositionalEscrow escrow`and `CompositionalToken token` into the list of accounts in `getEscrowToken`'s summary
-    */
-    function getEscrowToken() public {
-        assert(cseEscrow.getTokenTotalSupply() == 12345);
-    }
-}
\ No newline at end of file
diff --git a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
index 953b2b42c..703d0b69d 100644
--- a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
@@ -6,7 +6,7 @@
 │   statusCode: STATUSCODE:StatusCode
 ┃
 ┃ (branch)
-┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) )
+┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
 ┃  │
 ┃  ├─ 8
 ┃  │   k: #execute ~> CONTINUATION:K
@@ -29,7 +29,7 @@
 ┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
-┗━━┓ constraint: ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) <Int VV0_x_114b9705:Int
+┗━━┓ constraint: ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) <Int VV0_x_114b9705:Int
    │
    ├─ 9
    │   k: #execute ~> CONTINUATION:K
@@ -76,7 +76,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
              <ethereum>
                <evm>
                  <output>
-                   ( _OUTPUT_CELL => #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) ) )
+                   ( _OUTPUT_CELL => #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
                  </output>
                  <statusCode>
                    ( _STATUSCODE => EVMC_SUCCESS )
@@ -98,7 +98,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                      ( .WordStack => ( selector ( "applyOp(uint256)" ) : .WordStack ) )
                    </wordStack>
                    <localMem>
-                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) ) )
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
                    </localMem>
                    <memoryUsed>
                      0
@@ -138,7 +138,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -247,7 +247,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) )
+       andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
                ))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-8-TO-6)]
     
@@ -288,7 +288,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( 0 : ( VV0_x_114b9705:Int : ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) : ( 118 : ( 0 : ( VV0_x_114b9705:Int : ( 70 : ( selector ( "applyOp(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
+                     ( .WordStack => ( 0 : ( VV0_x_114b9705:Int : ( #lookup ( CONTRACT_STORAGE:Map , 0 ) : ( 118 : ( 0 : ( VV0_x_114b9705:Int : ( 70 : ( selector ( "applyOp(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
@@ -331,7 +331,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -440,7 +440,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) <Int VV0_x_114b9705:Int
+       andBool ( ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) <Int VV0_x_114b9705:Int
                ))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-9-TO-7)]
 
diff --git a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
new file mode 100644
index 000000000..a9e417af4
--- /dev/null
+++ b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
@@ -0,0 +1,309 @@
+
+┌─ 1 (root, init)
+│   k: #execute ~> CONTINUATION:K
+│   pc: 0
+│   callDepth: 0
+│   statusCode: STATUSCODE:StatusCode
+│
+│  (2219 steps)
+├─ 14 (terminal)
+│   k: #halt ~> CONTINUATION:K
+│   pc: 194
+│   callDepth: 0
+│   statusCode: EVMC_SUCCESS
+│
+┊  constraint: true
+┊  subst: OMITTED SUBST
+└─ 11 (leaf, target, terminal)
+    k: #halt ~> CONTINUATION:K
+    pc: PC_CELL_5d410f2a:Int
+    callDepth: CALLDEPTH_CELL_5d410f2a:Int
+    statusCode: STATUSCODE_FINAL:StatusCode
+
+
+
+
+module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0
+    
+    
+    rule [BASIC-BLOCK-1-TO-14]: <foundry>
+           <kevm>
+             <k>
+               ( #execute => #halt )
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               SHANGHAI
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   b""
+                 </output>
+                 <statusCode>
+                   ( _STATUSCODE => EVMC_SUCCESS )
+                 </statusCode>
+                 <callStack>
+                   .List
+                 </callStack>
+                 <interimStates>
+                   .List
+                 </interimStates>
+                 <touchedAccounts>
+                   ( .Set => ( SetItem ( 263400868551549723330807389252719309078400616203 ) ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) )
+                 </touchedAccounts>
+                 <callState>
+                   <id>
+                     728815563385977040452943777879061427756277306518
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     ( b"\n\x92T\xe4" => b"51X\xa0" )
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( .WordStack => ( selector ( "testEscrowToken()" ) : .WordStack ) )
+                   </wordStack>
+                   <localMem>
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0009" )
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <static>
+                     false
+                   </static>
+                   <callDepth>
+                     0
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <log>
+                     .List
+                   </log>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     ( .Set => ( SetItem ( 263400868551549723330807389252719309078400616203 ) ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) )
+                   </accessedAccounts>
+                   <accessedStorage>
+                     .Map
+                   </accessedStorage>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       ( 645326474426547203313410069153905908525362434349 => 263400868551549723330807389252719309078400616203 )
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       ( .Map => ( 0 |-> 491460923342184218035706888008750043977755113263 ) )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       ( 0 => 1 )
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       ( ( 11 |-> 1 )
+                       ( 7 |-> 1 ) )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                     ...
+                   </account> => ( <account>
+                     <acctID>
+                       491460923342184218035706888008750043977755113263
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       ( 0 |-> 12300 )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       645326474426547203313410069153905908525362434349
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       0
+                     </nonce>
+                     ...
+                   </account>
+                   <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       ( ( 11 |-> 1 )
+                       ( ( 27 |-> 491460923342184218035706888008750043977755113263 )
+                       ( ( 28 |-> 263400868551549723330807389252719309078400616203 )
+                       ( 7 |-> 1 ) ) ) )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       3
+                     </nonce>
+                     ...
+                   </account> ) ) ) )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressSet>
+                 .Set
+               </addressSet>
+               <storageSlotSet>
+                 .Set
+               </storageSlotSet>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( 0 <=Int NUMBER_CELL:Int
+       andBool ( 0 <=Int TIMESTAMP_CELL:Int
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( NUMBER_CELL:Int <=Int maxSInt256
+       andBool ( TIMESTAMP_CELL:Int <Int pow256
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+               ))))))))))))
+      [priority(20), label(BASIC-BLOCK-1-TO-14)]
+
+endmodule
\ No newline at end of file
diff --git a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected
index 12a63c233..34e532a29 100644
--- a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected
@@ -6,7 +6,7 @@
 │   statusCode: STATUSCODE:StatusCode
 ┃
 ┃ (branch)
-┣━━┓ constraint: ( maxUInt256 -Int VV0_x_114b9705:Int ) <Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+┣━━┓ constraint: ( maxUInt256 -Int VV0_x_114b9705:Int ) <Int #lookup ( CONTRACT_STORAGE:Map , 0 )
 ┃  │
 ┃  ├─ 13
 ┃  │   k: #execute ~> CONTINUATION:K
@@ -30,7 +30,7 @@
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
 ┣━━┓ constraints:
-┃  ┃     #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
+┃  ┃     #lookup ( CONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
 ┃  ┃     ( notBool STATIC_CELL:Bool )
 ┃  │
 ┃  ├─ 16
@@ -55,7 +55,7 @@
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
 ┗━━┓ constraints:
-   ┃     #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
+   ┃     #lookup ( CONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
    ┃     STATIC_CELL:Bool
    │
    ├─ 17
@@ -122,7 +122,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                      CALLVALUE_79cb2bc6:Int
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( 0 : ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) : ( VV0_x_114b9705:Int : ( 147 : ( VV0_x_114b9705:Int : ( 106 : ( selector ( "add(uint256)" ) : .WordStack ) ) ) ) ) ) ) )
+                     ( .WordStack => ( 0 : ( #lookup ( CONTRACT_STORAGE:Map , 0 ) : ( VV0_x_114b9705:Int : ( 147 : ( VV0_x_114b9705:Int : ( 106 : ( selector ( "add(uint256)" ) : .WordStack ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
@@ -165,7 +165,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -276,7 +276,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( ( maxUInt256 -Int VV0_x_114b9705:Int ) <Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+       andBool ( ( maxUInt256 -Int VV0_x_114b9705:Int ) <Int #lookup ( CONTRACT_STORAGE:Map , 0 )
                ))))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-13-TO-7)]
     
@@ -363,7 +363,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       ( STORAGE_CONTRACT_ID:Map => STORAGE_CONTRACT_ID:Map [ 0 <- ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) +Int VV0_x_114b9705:Int ) ] )
+                       ( CONTRACT_STORAGE:Map => CONTRACT_STORAGE:Map [ 0 <- ( #lookup ( CONTRACT_STORAGE:Map , 0 ) +Int VV0_x_114b9705:Int ) ] )
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -475,7 +475,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
+       andBool ( #lookup ( CONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
                )))))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-16-TO-10)]
     
@@ -513,7 +513,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                      CALLVALUE_79cb2bc6:Int
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( 0 : ( ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) +Int VV0_x_114b9705:Int ) : ( VV0_x_114b9705:Int : ( 106 : ( selector ( "add(uint256)" ) : .WordStack ) ) ) ) ) )
+                     ( .WordStack => ( 0 : ( ( #lookup ( CONTRACT_STORAGE:Map , 0 ) +Int VV0_x_114b9705:Int ) : ( VV0_x_114b9705:Int : ( 106 : ( selector ( "add(uint256)" ) : .WordStack ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
@@ -559,7 +559,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -671,7 +671,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
+       andBool ( #lookup ( CONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
                )))))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-17-TO-11)]
 
diff --git a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected
index 9b2f99e2d..8cc5321cb 100644
--- a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected
@@ -44,7 +44,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0
              <ethereum>
                <evm>
                  <output>
-                   ( _OUTPUT_CELL => #buf ( 32 , #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) )
+                   ( _OUTPUT_CELL => #buf ( 32 , #lookup ( CONTRACT_STORAGE:Map , 0 ) ) )
                  </output>
                  <statusCode>
                    ( _STATUSCODE => EVMC_SUCCESS )
@@ -66,7 +66,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0
                      ( .WordStack => ( 73 : ( selector ( "count()" ) : .WordStack ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) )
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , #lookup ( CONTRACT_STORAGE:Map , 0 ) ) )
                    </localMem>
                    <memoryUsed>
                      0
@@ -106,7 +106,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
diff --git a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
index 74c99048d..92a7e19af 100644
--- a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
@@ -109,7 +109,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.INIT:0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       ( CONTRACT_STORAGE:Map => CONTRACT_STORAGE:Map [ 0 <- 5 ] )
+                       ( CONTRACT_STORAGE_ID:Map => CONTRACT_STORAGE_ID:Map [ 0 <- 5 ] )
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
diff --git a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected
index 5921a35c8..c7beff05c 100644
--- a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected
@@ -6,7 +6,7 @@
 │   statusCode: STATUSCODE:StatusCode
 ┃
 ┃ (branch)
-┣━━┓ constraint: #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <Int 3
+┣━━┓ constraint: #lookup ( CONTRACT_STORAGE:Map , 0 ) <Int 3
 ┃  │
 ┃  ├─ 13
 ┃  │   k: #execute ~> CONTINUATION:K
@@ -30,7 +30,7 @@
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
 ┣━━┓ constraints:
-┃  ┃     3 <=Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+┃  ┃     3 <=Int #lookup ( CONTRACT_STORAGE:Map , 0 )
 ┃  ┃     ( notBool STATIC_CELL:Bool )
 ┃  │
 ┃  ├─ 16
@@ -55,7 +55,7 @@
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
 ┗━━┓ constraints:
-   ┃     3 <=Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+   ┃     3 <=Int #lookup ( CONTRACT_STORAGE:Map , 0 )
    ┃     STATIC_CELL:Bool
    │
    ├─ 17
@@ -165,7 +165,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -271,7 +271,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
        andBool ( ( notBool <acctID>
           CONTRACT_ID:Int
         </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
-       andBool ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <Int 3
+       andBool ( #lookup ( CONTRACT_STORAGE:Map , 0 ) <Int 3
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
@@ -361,7 +361,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       ( STORAGE_CONTRACT_ID:Map => STORAGE_CONTRACT_ID:Map [ 0 <- VV0_x_114b9705:Int ] )
+                       ( CONTRACT_STORAGE:Map => CONTRACT_STORAGE:Map [ 0 <- VV0_x_114b9705:Int ] )
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -468,7 +468,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
        andBool ( ( notBool <acctID>
           CONTRACT_ID:Int
         </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
-       andBool ( 3 <=Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+       andBool ( 3 <=Int #lookup ( CONTRACT_STORAGE:Map , 0 )
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
@@ -555,7 +555,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -662,7 +662,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
        andBool ( ( notBool <acctID>
           CONTRACT_ID:Int
         </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
-       andBool ( 3 <=Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+       andBool ( 3 <=Int #lookup ( CONTRACT_STORAGE:Map , 0 )
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
index f39630875..24256b486 100644
--- a/src/tests/integration/test-data/show/contracts.k.expected
+++ b/src/tests/integration/test-data/show/contracts.k.expected
@@ -3017,18 +3017,18 @@ module S2KtestZModContractFieldTest-CONTRACT
 
 endmodule
 
-module S2KtestZModEscrow-CONTRACT
+module S2KtestZModTEscrow-CONTRACT
     imports public FOUNDRY
     
-    syntax Contract ::= S2KtestZModEscrowContract
+    syntax Contract ::= S2KtestZModTEscrowContract
     
-    syntax S2KtestZModEscrowContract ::= "S2KtestZModEscrow" [symbol(""), klabel(contract_test%Escrow)]
+    syntax S2KtestZModTEscrowContract ::= "S2KtestZModTEscrow" [symbol(""), klabel(contract_test%TEscrow)]
     
-    syntax Bytes ::= S2KtestZModEscrowContract "." S2KtestZModEscrowMethod [function, symbol(""), klabel(method_test%Escrow)]
+    syntax Bytes ::= S2KtestZModTEscrowContract "." S2KtestZModTEscrowMethod [function, symbol(""), klabel(method_test%TEscrow)]
     
-    syntax S2KtestZModEscrowMethod ::= "S2KgetTokenTotalSupply" "(" ")" [symbol(""), klabel(method_test%Escrow_S2KgetTokenTotalSupply_)]
+    syntax S2KtestZModTEscrowMethod ::= "S2KgetTokenTotalSupply" "(" ")" [symbol(""), klabel(method_test%TEscrow_S2KgetTokenTotalSupply_)]
     
-    rule  ( S2KtestZModEscrow . S2KgetTokenTotalSupply ( ) => #abiCallData ( "getTokenTotalSupply" , .TypedArgs ) )
+    rule  ( S2KtestZModTEscrow . S2KgetTokenTotalSupply ( ) => #abiCallData ( "getTokenTotalSupply" , .TypedArgs ) )
       
     
     rule  ( selector ( "getTokenTotalSupply()" ) => 1474266187 )
@@ -3036,21 +3036,21 @@ module S2KtestZModEscrow-CONTRACT
 
 endmodule
 
-module S2KtestZModTestToken-CONTRACT
+module S2KtestZModTToken-CONTRACT
     imports public FOUNDRY
     
-    syntax Contract ::= S2KtestZModTestTokenContract
+    syntax Contract ::= S2KtestZModTTokenContract
     
-    syntax S2KtestZModTestTokenContract ::= "S2KtestZModTestToken" [symbol(""), klabel(contract_test%TestToken)]
+    syntax S2KtestZModTTokenContract ::= "S2KtestZModTToken" [symbol(""), klabel(contract_test%TToken)]
     
-    syntax Bytes ::= S2KtestZModTestTokenContract "." S2KtestZModTestTokenMethod [function, symbol(""), klabel(method_test%TestToken)]
+    syntax Bytes ::= S2KtestZModTTokenContract "." S2KtestZModTTokenMethod [function, symbol(""), klabel(method_test%TToken)]
     
-    syntax S2KtestZModTestTokenMethod ::= "S2KtotalSupply" "(" ")" [symbol(""), klabel(method_test%TestToken_S2KtotalSupply_)]
+    syntax S2KtestZModTTokenMethod ::= "S2KgetTotalSupply" "(" ")" [symbol(""), klabel(method_test%TToken_S2KgetTotalSupply_)]
     
-    rule  ( S2KtestZModTestToken . S2KtotalSupply ( ) => #abiCallData ( "totalSupply" , .TypedArgs ) )
+    rule  ( S2KtestZModTToken . S2KgetTotalSupply ( ) => #abiCallData ( "getTotalSupply" , .TypedArgs ) )
       
     
-    rule  ( selector ( "totalSupply()" ) => 404098525 )
+    rule  ( selector ( "getTotalSupply()" ) => 3303283490 )
       
 
 endmodule
diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
index 5b61734a2..ec930ba13 100644
--- a/src/tests/integration/test-data/show/foundry.k.expected
+++ b/src/tests/integration/test-data/show/foundry.k.expected
@@ -40,8 +40,8 @@ module FOUNDRY-MAIN
     imports public S2KtestZModContractTest-VERIFICATION
     imports public S2KtestZModContractBTest-VERIFICATION
     imports public S2KtestZModContractFieldTest-VERIFICATION
-    imports public S2KtestZModEscrow-VERIFICATION
-    imports public S2KtestZModTestToken-VERIFICATION
+    imports public S2KtestZModTEscrow-VERIFICATION
+    imports public S2KtestZModTToken-VERIFICATION
     imports public S2KtestZModCounter-VERIFICATION
     imports public S2KtestZModCounterTest-VERIFICATION
     imports public S2KsrcZModDeploymentState-VERIFICATION
@@ -143,7 +143,7 @@ module FOUNDRY-MAIN
     imports public S2KlibZModforgeZSubstdZModsrcZModconsole-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModsrcZModconsole2-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModsrcZModsafeconsole-VERIFICATION
-    imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION    
+    imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION
 
 
 
@@ -396,15 +396,15 @@ module S2KtestZModContractFieldTest-VERIFICATION
 
 endmodule
 
-module S2KtestZModEscrow-VERIFICATION
-    imports public S2KtestZModEscrow-CONTRACT
+module S2KtestZModTEscrow-VERIFICATION
+    imports public S2KtestZModTEscrow-CONTRACT
     
     
 
 endmodule
 
-module S2KtestZModTestToken-VERIFICATION
-    imports public S2KtestZModTestToken-CONTRACT
+module S2KtestZModTToken-VERIFICATION
+    imports public S2KtestZModTToken-CONTRACT