Pi-Squared-Inc · dwightguth · Sep 18, 2024 · Sep 6, 2024 · Sep 13, 2024 · Sep 13, 2024
diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-.PHONY: build clean test test-tokens test-staking test-lending test-swap test-erc20 test-erc1155 test-liquid test-lido test-lendingpool test-aave test-regression
+.PHONY: build clean test test-clean test-tokens test-staking test-lending test-swap test-erc20 test-erc1155 test-liquid test-lido test-lendingpool test-aave test-regression
 
 SEMANTICS_DIR = src
 TEST_DIR = test
@@ -25,8 +25,10 @@ EXAMPLE_TESTS = $(patsubst %.txn, %.out, $(TRANSACTIONS))
 build: $(SEMANTICS_DIR)/$(SEMANTICS_FILE)
 	kompile $(SEMANTICS_DIR)/$(SEMANTICS_FILE) --main-module $(MAIN_MODULE) --gen-glr-bison-parser -O2 --heuristic pbaL
 
-clean:
+clean: test-clean
 	rm -Rf $(SEMANTICS_FILE_NAME)-kompiled
+
+test-clean:
 	rm -Rf $(OUTPUT_DIR)
 	rm -Rf $(TEST_DIR)/regression/*.out
 	rm -Rf $(EXAMPLE_TESTS)

diff --git a/bin/krun-sol b/bin/krun-sol
@@ -2,7 +2,7 @@
 contract="$1"
 txn="$2"
 
-if [ "$#" -lt 3 ]; then
+if [[ "$3" == -* ]]; then
     isuniswap=""
 else
     isuniswap="$3"

diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-7.1.130
+7.1.144
diff --git a/src/expression.md b/src/expression.md
@@ -13,7 +13,7 @@ module SOLIDITY-EXPRESSION
        <this> THIS => ADDR </this>
        <this-type> TYPE => X </this-type>
        <env> E => .Map </env>
-       <store> S => .Map </store>
+       <store> S => .List </store>
        <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> X </contract-id>
        <contract-init> INIT </contract-init>
@@ -38,7 +38,7 @@ module SOLIDITY-EXPRESSION
        <this> THIS => ADDR </this>
        <this-type> TYPE => X </this-type>
        <env> E => .Map </env>
-       <store> S => .Map </store>
+       <store> S => .List </store>
        <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> X </contract-id>
        <contract-init> INIT </contract-init>
@@ -53,10 +53,10 @@ module SOLIDITY-EXPRESSION
        <next-address> ADDR => ADDR +MInt 1p160 </next-address>
 
   // new array
-  rule <k> new T[](Len:Int) => lv(!I:Int, .List, T[]) ...</k>
-       <store> S => S [ !I:Int <- makeList(Len, default(T)) ] </store>
-  rule <k> new T[](v(Len:MInt{256}, _)) => lv(!I:Int, .List, T[]) ...</k>
-       <store> S => S [ !I:Int <- makeList(MInt2Unsigned(Len), default(T)) ] </store>
+  rule <k> new T[](Len:Int) => lv(size(S), .List, T[]) ...</k>
+       <store> S => S ListItem(makeList(Len, default(T))) </store>
+  rule <k> new T[](v(Len:MInt{256}, _)) => lv(size(S), .List, T[]) ...</k>
+       <store> S => S ListItem(makeList(MInt2Unsigned(Len), default(T))) </store>
 
   // literal assignment to state variable
   rule <k> X:Id = N:Int => X = v(convert(N, LT), LT) ...</k>
@@ -139,7 +139,7 @@ module SOLIDITY-EXPRESSION
   // local variable lookup
   rule <k> X:Id => v(V, T) ...</k>
        <env>... X |-> var(I, T) ...</env>
-       <store>... I |-> V ...</store>
+       <store> _ [ I <- V ] </store>
     requires notBool isAggregateType(T)
 
   rule <k> X:Id => lv(I, .List, T) ...</k>
@@ -150,10 +150,10 @@ module SOLIDITY-EXPRESSION
   context HOLE:Expression [ _:Expression ]
   context _:Expression [ HOLE:Expression ]
   rule <k> lv(I:Int, L, T []) [ Idx:Int ] => v(read(V, L ListItem(Idx), T[]), T) ...</k>
-       <store>... I |-> V ...</store>
+       <store> _ [ I <- V ] </store>
     requires notBool isAggregateType(T)
   rule <k> lv(I:Int, L, T []) [ v(Idx:MInt{256}, _) ] => v(read(V, L ListItem(MInt2Unsigned(Idx)), T[]), T) ...</k>
-       <store>... I |-> V ...</store>
+       <store> _ [ I <- V ] </store>
     requires notBool isAggregateType(T)
   rule <k> lv(X:Id, L, mapping(T1:ElementaryTypeName _ => T2)) [ v(Key, RT) ] => v(read({S [ X ] orDefault .Map}:>Value, L ListItem(convert(Key, RT, T1)), T), T2) ...</k>
        <this> THIS </this>
@@ -180,7 +180,7 @@ module SOLIDITY-EXPRESSION
   syntax Id ::= "length" [token]
   context HOLE . length
   rule <k> lv(I:Int, .List, T) . length => v(Int2MInt(size({read(V, .List, T)}:>List))::MInt{256}, uint) ...</k>
-       <store>... I |-> V ...</store>
+       <store> _ [ I <- V ] </store>
 
   // external call
   context HOLE . _ ( _:CallArgumentList )
@@ -191,7 +191,7 @@ module SOLIDITY-EXPRESSION
        <this> THIS => ADDR </this>
        <this-type> TYPE => TYPE' </this-type>
        <env> E => .Map </env>
-       <store> S => .Map </store>
+       <store> S => .List </store>
        <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> TYPE' </contract-id>
        <contract-fn-id> F </contract-fn-id>
@@ -216,7 +216,7 @@ module SOLIDITY-EXPRESSION
        <this> THIS => ADDR </this>
        <this-type> TYPE => TYPE' </this-type>
        <env> E => .Map </env>
-       <store> S => .Map </store>
+       <store> S => .List </store>
        <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> TYPE' </contract-id>
        <contract-fn-id> F </contract-fn-id>
@@ -310,10 +310,10 @@ module SOLIDITY-EXPRESSION
   // local increment and decrement
   rule <k> X:Id ++ => v(V, T) ...</k>
        <env>... X |-> var(I, T) ...</env>
-       <store>... I |-> (V => add(V, convert(1, T))) ...</store>
+       <store> _ [ I <- (V => add(V, convert(1, T))) ] </store>
   rule <k> X:Id -- => v(V, T) ...</k>
        <env>... X |-> var(I, T) ...</env>
-       <store>... I |-> (V => sub(V, convert(1, T))) ...</store>
+       <store> _ [ I <- (V => sub(V, convert(1, T))) ] </store>
 
   // equality and inequality
   rule v(V1:Value, T) == v(V2:Value, T) => v(eq(V1, V2), bool)
@@ -384,19 +384,19 @@ module SOLIDITY-EXPRESSION
 
   syntax KItem ::= var(Int, TypeName)
 
-  syntax KItem ::= bind(Map, List, List, CallArgumentList, List, List)
+  syntax KItem ::= bind(List, List, List, CallArgumentList, List, List)
   rule bind(_, .List, .List, .CallArgumentList, .List, .List) => .K
   rule bind(STORE, ListItem(noId) PARAMS, ListItem(_) TYPES, _, ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2)
   rule bind(STORE, .List, .List, .CallArgumentList, ListItem(_) TYPES, ListItem(noId) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES)
   rule <k> bind(STORE, ListItem(X:Id) PARAMS, ListItem(T:TypeName) TYPES, lv(I:Int, .List, T:TypeName), ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ...</k>
-       <env> E => E [ X <- var(!I:Int, T) ] </env>
-       <store> S => S [ !I <- STORE [ I ] ] </store>
+       <env> E => E [ X <- var(size(S), T) ] </env>
+       <store> S => S ListItem(STORE [ I ]) </store>
   rule <k> bind(STORE, ListItem(X:Id) PARAMS, ListItem(LT:TypeName) TYPES, v(V:Value, RT:TypeName), ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- convert(V, RT, LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(convert(V, RT, LT)) </store>
   rule <k> bind(STORE, .List, .List, .CallArgumentList, ListItem(LT:TypeName) TYPES, ListItem(X:Id) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES) ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- default(LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(default(LT)) </store>
 
   syntax Value ::= convert(Value, from: TypeName, to: TypeName) [function]
   rule convert(V, T, T) => V

diff --git a/src/solidity.md b/src/solidity.md
@@ -69,7 +69,7 @@ module SOLIDITY-CONFIGURATION
         <this> 0p160 </this>
         <this-type> Id </this-type>
         <env> .Map </env>
-        <store> .Map </store>
+        <store> .List </store>
         <call-stack> .List </call-stack>
         <live-contracts>
           <live-contract multiplicity="*" type="Map">
@@ -164,7 +164,7 @@ module SOLIDITY-DATA
   rule isAggregateType(_) => false [owise]
 
   // external frame
-  syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id, value: MInt{256})
+  syntax Frame ::= frame(continuation: K, env: Map, store: List, from: MInt{160}, type: Id, value: MInt{256})
   // internal frame
                  | frame(continuation: K, env: Map)
   syntax Event ::= event(name: Id, args: TypedVals)

diff --git a/src/statement.md b/src/statement.md
@@ -31,27 +31,27 @@ module SOLIDITY-STATEMENT
        <call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List </call-stack>
 
   rule <k> return lv(I:Int, .List, T) ; => return v(L, T) ; ...</k>
-       <store>... I |-> L ...</store>
+       <store> _ [ I <- L ] </store>
 
   rule <k> return V:TypedVal ; ~> _ => V ~> K </k>
        <env> _ => E </env>
        <call-stack>... ListItem(frame(K, E)) => .List </call-stack> [owise]
 
   // variable declaration
   rule <k> LT:TypeName X:Id = v(V, RT) ; => .K ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- convert(V, RT, LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(convert(V, RT, LT)) </store>
   rule <k> LT:TypeName X:Id = N:Int ; => .K ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- convert(N, LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(convert(N, LT)) </store>
   rule <k> LT:TypeName memory X:Id = v(V, RT) ; => .K ...</k>
-       <env> E => E [ X <- var(!I:Int, LT) ] </env>
-       <store> S => S [ !I <- convert(V, RT, LT) ] </store>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(convert(V, RT, LT)) </store>
   rule <k> T:TypeName memory X:Id = lv(I:Int, .List, T) ; => .K ...</k>
        <env> E => E [ X <- var(I, T) ] </env>
   rule <k> T:TypeName X:Id ;::VariableDeclarationStatement => .K ...</k>
-       <env> E => E [ X <- var(!I:Int, T) ] </env>
-       <store> S => S [ !I <- default(T) ] </store>
+       <env> E => E [ X <- var(size(S), T) ] </env>
+       <store> S => S ListItem(default(T)) </store>
 
   // emit statement
   rule <k> emit X:Id ( ARGS ) ; => discard(Event2String(ARGS, ((.StringBuffer +String Id2String(X)) +String "("))) ...</k>

diff --git a/src/transaction.md b/src/transaction.md
@@ -7,15 +7,15 @@ module SOLIDITY-TRANSACTION
   imports INT
   imports private SOLIDITY-EXPRESSION
 
-  rule <k> create(FROM, VALUE, NOW, CTOR, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
+  rule <k> create(FROM, VALUE, NOW, CTOR, ARGS) => bind(.List, PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
        <msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
        <msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
        <tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
        <block-timestamp> _ => Int2MInt(Number2Int(NOW)) </block-timestamp>
        <this> _ => ADDR </this>
        <this-type> _ => CTOR </this-type>
        <env> _ => .Map </env>
-       <store> _ => .Map </store>
+       <store> _ => .List </store>
        <contract-id> CTOR </contract-id>
        <contract-init> INIT </contract-init>
        <contract-fn-id> constructor </contract-fn-id>
@@ -41,7 +41,7 @@ module SOLIDITY-TRANSACTION
        <this> _ => ADDR </this>
        <this-type> _ => CTOR </this-type>
        <env> _ => .Map </env>
-       <store> _ => .Map </store>
+       <store> _ => .List </store>
        <contract-id> CTOR </contract-id>
        <contract-init> INIT </contract-init>
        <live-contracts>
@@ -58,15 +58,15 @@ module SOLIDITY-TRANSACTION
   syntax Transaction ::= txn(from: Decimal, to: MInt{160}, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) [strict(6)]
   rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => txn(FROM, Int2MInt(Number2Int(TO)), VALUE, NOW, FUNC, ARGS)
 
-  rule <k> txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.Map, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
+  rule <k> txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(.List, PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
        <msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
        <msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
        <tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
        <block-timestamp> _ => Int2MInt(Number2Int(NOW)) </block-timestamp>
        <this> _ => TO </this>
        <this-type> _ => TYPE </this-type>
        <env> _ => .Map </env>
-       <store> _ => .Map </store>
+       <store> _ => .List </store>
        <live-contracts>
          <contract-address> TO </contract-address>
          <contract-type> TYPE </contract-type>

diff --git a/test/regression/addliquidity.ref b/test/regression/addliquidity.ref
@@ -2350,11 +2350,11 @@
       testAmount |-> var ( 0 , uint256 )
     </env>
     <store>
-      0 |-> 131072p256
-      1 |-> 10000p256
-      2 |-> 10000p256
-      3 |-> 0p256
-      4 |-> 0p256
+      ListItem ( 131072p256 )
+      ListItem ( 10000p256 )
+      ListItem ( 10000p256 )
+      ListItem ( 0p256 )
+      ListItem ( 0p256 )
     </store>
     <call-stack>
       .List

diff --git a/test/regression/arithmetic.ref b/test/regression/arithmetic.ref
@@ -87,14 +87,14 @@
       i256_2 |-> var ( 7 , uint8 )
     </env>
     <store>
-      0 |-> 2p8
-      1 |-> 4p8
-      2 |-> 2p8
-      3 |-> 4p8
-      4 |-> 2p8
-      5 |-> 4p8
-      6 |-> 2p8
-      7 |-> 4p8
+      ListItem ( 2p8 )
+      ListItem ( 4p8 )
+      ListItem ( 2p8 )
+      ListItem ( 4p8 )
+      ListItem ( 2p8 )
+      ListItem ( 4p8 )
+      ListItem ( 2p8 )
+      ListItem ( 4p8 )
     </store>
     <call-stack>
       .List

diff --git a/test/regression/arraystestcontract.ref b/test/regression/arraystestcontract.ref
@@ -106,7 +106,7 @@
       .Map
     </env>
     <store>
-      .Map
+      .List
     </store>
     <call-stack>
       .List

diff --git a/test/regression/block.ref b/test/regression/block.ref
@@ -80,8 +80,8 @@
       x |-> var ( 0 , bool )
     </env>
     <store>
-      0 |-> false
-      1 |-> true
+      ListItem ( false )
+      ListItem ( true )
     </store>
     <call-stack>
       .List

diff --git a/test/regression/boolean.ref b/test/regression/boolean.ref
@@ -105,7 +105,7 @@
       x |-> var ( 0 , bool )
     </env>
     <store>
-      0 |-> false
+      ListItem ( false )
     </store>
     <call-stack>
       .List

diff --git a/test/regression/contract.ref b/test/regression/contract.ref
@@ -348,9 +348,9 @@
       _weth |-> var ( 0 , address )
     </env>
     <store>
-      0 |-> 2p160
-      1 |-> 3p160
-      2 |-> 4p160
+      ListItem ( 2p160 )
+      ListItem ( 3p160 )
+      ListItem ( 4p160 )
     </store>
     <call-stack>
       .List

diff --git a/test/regression/emit.ref b/test/regression/emit.ref
@@ -98,7 +98,7 @@
       .Map
     </env>
     <store>
-      .Map
+      .List
     </store>
     <call-stack>
       .List

diff --git a/test/regression/eventtestcontract.ref b/test/regression/eventtestcontract.ref
@@ -226,7 +226,7 @@
       .Map
     </env>
     <store>
-      .Map
+      .List
     </store>
     <call-stack>
       .List

diff --git a/test/regression/for.ref b/test/regression/for.ref
@@ -81,9 +81,9 @@
       y |-> var ( 1 , uint256 )
     </env>
     <store>
-      0 |-> 5p256
-      1 |-> 20p256
-      2 |-> 10p256
+      ListItem ( 5p256 )
+      ListItem ( 20p256 )
+      ListItem ( 10p256 )
     </store>
     <call-stack>
       .List

diff --git a/test/regression/function.ref b/test/regression/function.ref
@@ -2074,7 +2074,7 @@
       .Map
     </env>
     <store>
-      .Map
+      .List
     </store>
     <call-stack>
       .List

diff --git a/test/regression/if.ref b/test/regression/if.ref
@@ -81,8 +81,8 @@
       y |-> var ( 1 , bool )
     </env>
     <store>
-      0 |-> false
-      1 |-> true
+      ListItem ( false )
+      ListItem ( true )
     </store>
     <call-stack>
       .List

diff --git a/test/regression/increment.ref b/test/regression/increment.ref
@@ -80,7 +80,7 @@
       x |-> var ( 0 , uint256 )
     </env>
     <store>
-      0 |-> 0p256
+      ListItem ( 0p256 )
     </store>
     <call-stack>
       .List