Prepare for erc20

Makefile

@@ -446,6 +446,12 @@ $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 	mkdir -p $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)
 
 	echo "<(<" > $@.in.tmp
+	echo "::address" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/address.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+
+	echo "<(<" >> $@.in.tmp
 	echo "::bytes_hooks" >> $@.in.tmp
 	echo "<|>" >> $@.in.tmp
 	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp

rust-semantics/helpers.md

@@ -35,11 +35,10 @@ module RUST-HELPERS
 
     syntax Bool ::= isSignedInt(Type)  [function, total]
     rule isSignedInt(_) => false [owise]
-    rule isSignedInt(u8) => true
-    rule isSignedInt(u16) => true
-    rule isSignedInt(u32) => true
-    rule isSignedInt(u64) => true
-    rule isSignedInt(u128) => true
+    rule isSignedInt(i8) => true
+    rule isSignedInt(i16) => true
+    rule isSignedInt(i32) => true
+    rule isSignedInt(i64) => true
     rule isSignedInt(&T => T)
 
     rule concatNonEmptyStatements(.NonEmptyStatements, S:NonEmptyStatements) => S

rust-semantics/test/configuration.md

@@ -7,6 +7,7 @@ module RUST-EXECUTION-TEST-CONFIGURATION
         <rust-test>
             <test-stack> .List </test-stack>
             <mocks> .Map </mocks>
+            <mock-list> .List </mock-list>
         </rust-test>
 endmodule
 

rust-semantics/test/execution.md

@@ -14,7 +14,9 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
                             | "check_eq" Expression  [strict]
                             | "push" Expression [strict]
                             | "push_value" Expression [strict]
-    syntax KItem ::= mock(KItem, K)
+    syntax Mockable
+    syntax KItem  ::= mock(Mockable, K)
+                    | listMock(Mockable, K)
 endmodule
 
 module RUST-EXECUTION-TEST
@@ -101,7 +103,6 @@ module RUST-EXECUTION-TEST
         <next-value-id> NVI:Int => NVI +Int 1 </next-value-id>
 
     syntax KItem ::= wrappedK(K)
-    syntax Mockable
 
     rule
         <k> mock(Mocked:Mockable, Result:K) => .K ... </k>
@@ -111,6 +112,18 @@ module RUST-EXECUTION-TEST
         <k> (Mocked:Mockable => Result) ...</k>
         <mocks> Mocked |-> wrappedK(Result:K) ...</mocks>
         [priority(10)]
+
+    rule
+        <k> listMock(Mocked:Mockable, Result:K) => .K ... </k>
+        <mock-list> L:List => L ListItem(listMock(Mocked, Result)) </mock-list>
+
+    rule
+        <k> (Mocked:Mockable => Result) ...</k>
+        <mock-list>
+            (ListItem(listMock(Mocked:Mockable, Result:K)) => .List)
+            ...
+        </mock-list>
+        [priority(9)]
 endmodule
 
 ```

ukm-semantics/test/execution.md

@@ -8,6 +8,7 @@ module UKM-TEST-SYNTAX
     syntax ExecutionItem  ::= "mock" "CallData"
                             | "mock" "Caller"
                             | "mock" UkmHook UkmHookResult
+                            | "list_mock" UkmHook UkmHookResult
                             | "call_contract" Int
                             | "output_to_arg"
                             | "push_status"
@@ -41,6 +42,7 @@ module UKM-TEST-EXECUTION
         </test-stack>
 
     rule mock Hook:UkmHook Result:UkmHookResult => mock(Hook, Result)
+    rule list_mock Hook:UkmHook Result:UkmHookResult => listMock(Hook, Result)
 
     rule call_contract Account => ukmExecute(Account, 100)