Preparing to run the Erc20 test

Makefile

@@ -108,7 +108,7 @@ build-legacy: \
 		$(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP)
 
 
-test: build syntax-test preprocessing-test execution-test crates-test ukm-no-contracts-test
+test: build syntax-test preprocessing-test execution-test crates-test ukm-no-contracts-test ukm-with-contracts-test
 
 test-legacy: mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
 
@@ -451,6 +451,12 @@ $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp
 	echo ">)>" >> $@.in.tmp
 
+	echo "<(<" >> $@.in.tmp
+	echo "::test_helpers" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/test_helpers.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+
 	echo "<(<" >> $@.in.tmp
 	echo "::state_hooks" >> $@.in.tmp
 	echo "<|>" >> $@.in.tmp

rust-semantics/test/execution.md

@@ -13,6 +13,7 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
                             | "return_value_to_arg"
                             | "check_eq" Expression  [strict]
                             | "push" Expression [strict]
+                            | "push_value" Expression [strict]
     syntax KItem ::= mock(KItem, K)
 endmodule
 
@@ -93,6 +94,12 @@ module RUST-EXECUTION-TEST
         <values> VALUES:Map => VALUES[NVI <- V] </values>
         <next-value-id> NVI:Int => NVI +Int 1 </next-value-id>
 
+    rule
+        <k> push_value ptrValue(_, V:Value) => .K ... </k>
+        <test-stack> .List => ListItem(ptrValue(ptr(NVI), V)) ... </test-stack>
+        <values> VALUES:Map => VALUES[NVI <- V] </values>
+        <next-value-id> NVI:Int => NVI +Int 1 </next-value-id>
+
     syntax KItem ::= wrappedK(K)
     syntax Mockable
 
@@ -106,4 +113,4 @@ module RUST-EXECUTION-TEST
         [priority(10)]
 endmodule
 
-```
+```

tests/ukm-contracts/bytes_hooks.rs

@@ -7,6 +7,7 @@ extern "C" {
   fn append_u32(bytes_id: u64, value: u32) -> u64;
   fn append_u16(bytes_id: u64, value: u16) -> u64;
   fn append_u8(bytes_id: u64, value: u8) -> u64;
+  fn append_bool(bytes_id: u64, value: bool) -> u64;
   fn append_str(bytes_id: u64, value: &str) -> u64;
 
   fn decode_u128(bytes_id: u64) -> (u64, u128);

tests/ukm-contracts/test_helpers.rs

@@ -0,0 +1,8 @@
+
+fn decode_single_u64(bytes_id: u64) -> u64 {
+  let (remaining_id, value) = :: bytes_hooks :: decode_u64(bytes_id);
+  if :: bytes_hooks :: length(remaining_id) > 0_u32 {
+      fail();
+  };
+  value
+}

tests/ukm-with-contract/endpoints.1.run

@@ -16,7 +16,7 @@ push_status;
 check_eq 2;
 
 output_to_arg;
-call :: endpoints :: decode_single_u64;
+call :: test_helpers :: decode_single_u64;
 return_value;
 
 check_eq 126_u64

tests/ukm-with-contract/endpoints.rs

@@ -13,11 +13,3 @@ pub trait Endpoints {
         value + 3_u64
     }
 }
-
-fn decode_single_u64(bytes_id: u64) -> u64 {
-    let (remaining_id, value) = :: bytes_hooks :: decode_u64(bytes_id);
-    if :: bytes_hooks :: length(remaining_id) > 0_u32 {
-        fail();
-    };
-    value
-}

ukm-semantics/main/hooks/bytes.md

@@ -38,6 +38,7 @@ module UKM-HOOKS-BYTES
                         | "append_u32"  [token]
                         | "append_u16"  [token]
                         | "append_u8"  [token]
+                        | "append_bool"  [token]
                         | "append_str"  [token]
                         | "decode_u128"  [token]
                         | "decode_u64"  [token]
@@ -105,6 +106,13 @@ module UKM-HOOKS-BYTES
             )
         => ukmBytesAppendInt(BufferIdId, IntId)
 
+    rule
+        normalizedFunctionCall
+            ( :: bytes_hooks :: append_bool :: .PathExprSegments
+            , BufferIdId:Ptr, IntId:Ptr, .PtrList
+            )
+        => ukmBytesAppendBool(BufferIdId, IntId)
+
     rule
         normalizedFunctionCall
             ( :: bytes_hooks :: append_str :: .PathExprSegments
@@ -170,6 +178,7 @@ module UKM-HOOKS-BYTES
                             | ukmBytesLength(UkmExpression)  [strict(1)]
                             | ukmBytesAppendInt(Expression, Expression)  [seqstrict]
                             | ukmBytesAppendInt(UkmExpression, Int)  [strict(1)]
+                            | ukmBytesAppendBool(Expression, Expression)  [seqstrict]
                             | ukmBytesAppendStr(Expression, Expression)  [seqstrict]
                             | ukmBytesAppendBytes(UkmExpression, Bytes)  [strict(1)]
                             | ukmBytesAppendLenAndBytes(Bytes, Bytes)
@@ -212,6 +221,11 @@ module UKM-HOOKS-BYTES
     rule ukmBytesAppendInt(ukmBytesValue(B:Bytes), Value:Int)
         => ukmBytesAppendLenAndBytes(B, Int2Bytes(Value, BE, Unsigned))
 
+    rule ukmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, false))
+        => ukmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(0p8)))
+    rule ukmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, true))
+        => ukmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(1p8)))
+
     rule ukmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String))
         => ukmBytesAppendBytes(ukmBytesId(BytesId), String2Bytes(Value))
 

ukm-semantics/main/hooks/ukm.md

@@ -1,7 +1,8 @@
 ```k
 
 module UKM-HOOKS-UKM-SYNTAX
-    syntax UkmHook ::= CallDataHook()
+    syntax UkmHook  ::= CallDataHook()
+                      | CallerHook()
 endmodule
 
 
@@ -12,9 +13,12 @@ module UKM-HOOKS-UKM
 
     syntax Identifier ::= "ukm"  [token]
                         | "CallData"  [token]
+                        | "Caller"  [token]
 
-    rule normalizedFunctionCall ( ukm :: CallData :: .PathExprSegments , .PtrList )
+    rule normalizedFunctionCall ( :: ukm :: CallData :: .PathExprSegments , .PtrList )
         => CallDataHook()
+    rule normalizedFunctionCall ( :: ukm :: Caller :: .PathExprSegments , .PtrList )
+        => CallerHook()
 endmodule
 
 ```

ukm-semantics/main/preprocessing/endpoints.md

@@ -121,7 +121,7 @@ module UKM-PREPROCESSING-ENDPOINTS
                         block({
                             .InnerAttributes
                             concatNonEmptyStatements
-                                (   let buffer_id = ukm :: CallData();
+                                (   let buffer_id = :: ukm :: CallData();
                                     let ( buffer_id | .PatternNoTopAlts
                                         , signature | .PatternNoTopAlts
                                         , .Patterns
@@ -151,6 +151,7 @@ module UKM-PREPROCESSING-ENDPOINTS
                         | "append_u16"  [token]
                         | "append_u32"  [token]
                         | "append_u64"  [token]
+                        | "append_bool"  [token]
                         | "decode_u8"  [token]
                         | "decode_u16"  [token]
                         | "decode_u32"  [token]
@@ -232,6 +233,8 @@ module UKM-PREPROCESSING-ENDPOINTS
         => v(:: bytes_hooks :: append_u32 ( BufferId , Value , .CallParamsList ))
     rule appendValue(BufferId:Identifier, Value:Identifier, u64)
         => v(:: bytes_hooks :: append_u64 ( BufferId , Value , .CallParamsList ))
+    rule appendValue(BufferId:Identifier, Value:Identifier, bool)
+        => v(:: bytes_hooks :: append_bool ( BufferId , Value , .CallParamsList ))
     rule appendValue(BufferId:Identifier, _Value:Identifier, ()) => v(BufferId)
     rule appendValue(BufferId:Identifier, Value:Identifier, T:Type)
         => e(error("appendValue: unrecognized type", ListItem(BufferId) ListItem(Value) ListItem(T)))

ukm-semantics/test/execution.md

@@ -5,6 +5,7 @@ module UKM-TEST-SYNTAX
     imports RUST-EXECUTION-TEST-PARSING-SYNTAX
 
     syntax ExecutionItem  ::= "mock" "CallData"
+                            | "mock" "Caller"
                             | "call_contract" Int
                             | "output_to_arg"
                             | "push_status"
@@ -30,6 +31,13 @@ module UKM-TEST-EXECUTION
             ...
         </test-stack>
 
+    rule
+        <k> mock Caller => mock(CallerHook(), V) ... </k>
+        <test-stack>
+            (ListItem(ptrValue(_, u64(_BytesId)) #as V:PtrValue) => .List)
+            ...
+        </test-stack>
+
     rule call_contract Account => ukmExecute(Account, 100)
 
     rule