tmp

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

@@ -1,6 +1,6 @@
 call :: bytes_hooks :: empty;
 return_value_to_arg;
-push "myEndpoint";
+push "myEndpoint(Uint64)";
 call :: bytes_hooks :: append_str;
 return_value_to_arg;
 push 123_u64;
@@ -9,6 +9,11 @@ return_value;
 mock CallData;
 
 call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 0;
 
 push_output;
 call :: endpoints :: decode_single_u64;

ukm-semantics/main/configuration.md

@@ -1,12 +1,15 @@
 ```k
 
 requires "hooks/bytes.md"
+requires "hooks/state.md"
 
 module UKM-CONFIGURATION
     imports UKM-HOOKS-BYTES-CONFIGURATION
+    imports UKM-HOOKS-STATE-CONFIGURATION
     configuration
         <ukm>
             <ukm-bytes/>
+            <ukm-state/>
         </ukm>
 endmodule
 

ukm-semantics/main/execution.md

@@ -3,10 +3,12 @@
 requires "execution/dispatch.md"
 requires "execution/syntax.md"
 requires "hooks.md"
+requires "representation.md"
 
 module UKM-EXECUTION
     imports private UKM-EXECUTION-DISPATCH
     imports private UKM-HOOKS
+    imports private UKM-REPRESENTATION
 endmodule
 
 ```

ukm-semantics/main/hooks/bytes.md

@@ -27,6 +27,8 @@ module UKM-HOOKS-BYTES
     imports private RUST-REPRESENTATION
     imports private UKM-HOOKS-BYTES-CONFIGURATION
     imports private UKM-HOOKS-BYTES-SYNTAX
+    imports private UKM-REPRESENTATION
+
 
     syntax Identifier ::= "bytes_hooks"  [token]
                         | "empty"  [token]
@@ -44,11 +46,6 @@ module UKM-HOOKS-BYTES
                         | "decode_u8"  [token]
                         | "decode_str"  [token]
 
-    syntax UkmBytesValue ::= ukmBytesValue(Bytes)
-    syntax UkmExpression  ::= ukmBytesId(MInt{64})
-                            | UkmBytesValue
-    syntax KResult ::= UkmBytesValue
-
     rule
         <k>
             normalizedFunctionCall

ukm-semantics/main/hooks/state.md

@@ -1,22 +1,72 @@
 ```k
 
+module UKM-HOOKS-STATE-CONFIGURATION
+    imports BYTES-SYNTAX
+    imports INT-SYNTAX
+
+    configuration
+        <ukm-state>
+            <ukm-status> 0 </ukm-status>
+            <ukm-output> b"" </ukm-output>
+            <ukm-gas> 0 </ukm-gas>
+        </ukm-state>
+endmodule
+
 module UKM-HOOKS-STATE
+    imports private COMMON-K-CELL
+    imports private RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+    imports private UKM-HOOKS-STATE-CONFIGURATION
+    imports private UKM-REPRESENTATION
+
     syntax UKMInstruction ::= ukmSetStatus(Expression)  [strict(1)]
-                            | ukmSetStatus(UkmExpression)  [strict(1)]
+                            | ukmSetGasLeft(Expression)  [strict(1)]
+                            | ukmSetOutput(Expression)  [strict(1)]
+                            | ukmSetOutput(UkmExpression)  [strict(1)]
 
     syntax Identifier ::= "state_hooks"  [token]
                         | "setStatus"  [token]
+                        | "setGasLeft"  [token]
 
     rule normalizedFunctionCall
             ( :: state_hooks :: setStatus :: .PathExprSegments
             , StatusId:Ptr , .PtrList
             )
         => ukmSetStatus(StatusId)
 
-    rule ukmSetStatus(ptrValue(_, u64(BytesId))) => ukmSetStatus(ukmBytesId(BytesId))
-    rule ukmBytesLength(ukmBytesValue(Value:Bytes))
-        => ptrValue(null, u32(Int2MInt(lengthBytes(Value))))
-        requires notBool uoverflowMInt(32, lengthBytes(Value))
+    rule normalizedFunctionCall
+            ( :: state_hooks :: setGasLeft :: .PathExprSegments
+            , GasId:Ptr , .PtrList
+            )
+        => ukmSetGasLeft(GasId)
+
+    rule normalizedFunctionCall
+            ( :: state_hooks :: setOutput :: .PathExprSegments
+            , OutputId:Ptr , .PtrList
+            )
+        => ukmSetOutput(OutputId)
+
+    rule
+        <k>
+            ukmSetStatus(ptrValue(_, u64(Value))) => ptrValue(null, tuple(.ValueList))
+            ...
+        </k>
+        <ukm-status> _ => MInt2Unsigned(Value) </ukm-status>
+
+    rule
+        <k>
+            ukmSetGasLeft(ptrValue(_, u64(Value))) => ptrValue(null, tuple(.ValueList))
+            ...
+        </k>
+        <ukm-gas> _ => MInt2Unsigned(Value) </ukm-gas>
+
+    rule ukmSetOutput(ptrValue(_, u64(BytesId))) => ukmSetOutput(ukmBytesId(BytesId))
+    rule
+        <k>
+            ukmSetOutput(ukmBytesValue(Value:Bytes)) => ptrValue(null, tuple(.ValueList))
+            ...
+        </k>
+        <ukm-output> _ => Value </ukm-output>
 
 endmodule
 

ukm-semantics/main/preprocessing/endpoints.md

@@ -70,11 +70,11 @@ module UKM-PREPROCESSING-ENDPOINTS
                     <method-implementation>
                         block({
                             .InnerAttributes
-                            :: state_hooks :: setGasLeft(gas);
+                            :: state_hooks :: setGasLeft(gas , .CallParamsList);
                             concatNonEmptyStatements
                                 ( Decode
                                 , let return_value = callMethod(ImplementationMethod, Params);
-                                  let buffer_id = :: bytes_hooks :: empty();
+                                  let buffer_id = :: bytes_hooks :: empty(.CallParamsList);
                                   let buffer_id = Append;
                                   :: state_hooks :: setOutput(buffer_id , .CallParamsList);
                                   :: state_hooks :: setStatus(:: ukm :: EVMC_SUCCESS , .CallParamsList);
@@ -118,14 +118,14 @@ module UKM-PREPROCESSING-ENDPOINTS
                         block({
                             .InnerAttributes
                             concatNonEmptyStatements
-                                ( let buffer_id = ukm :: CallData();
-                                    let
-                                        ( buffer_id | .PatternNoTopAlts
+                                (   let buffer_id = ukm :: CallData();
+                                    let ( buffer_id | .PatternNoTopAlts
                                         , signature | .PatternNoTopAlts
                                         , .Patterns
                                         ) = decodeSignature(buffer_id);
-                                , signatureToCall(signature, keys_list(Signatures), Signatures, buffer_id, gas);
-                                  .NonEmptyStatements
+                                    .NonEmptyStatements
+                                ,   signatureToCall(signature, keys_list(Signatures), Signatures, buffer_id, gas)
+                                    .NonEmptyStatements
                                 )
                         })
                     </method-implementation>
@@ -212,9 +212,11 @@ module UKM-PREPROCESSING-ENDPOINTS
         =>  if signature == CurrentSignature {
                 .InnerAttributes
                 self . Method ( BufferId , Gas , .CallParamsList );
+                .NonEmptyStatements
             } else {
                 .InnerAttributes
-                signatureToCall(Signature, Signatures, SignatureToMethod, BufferId, Gas);
+                signatureToCall(Signature, Signatures, SignatureToMethod, BufferId, Gas)
+                .NonEmptyStatements
             };
 
     syntax Expression ::= decodeSignature(Identifier)  [function, total]
@@ -245,21 +247,18 @@ module UKM-PREPROCESSING-ENDPOINTS
     rule decodeParam(I:Int, T:Type) => decodeParam(I, decodeForType(T))
     rule decodeParam(_:Int, e(E:SemanticsError)) => E
     rule decodeParam(Index:Int, v(E:Expression))
-        =>  let
-                (   ( buffer_id
-                    , StringToIdentifier("v" +String Int2String(Index))
-                    , .Patterns
-                    )
-                | .PatternNoTopAlts
+        =>  let ( buffer_id | .PatternNoTopAlts
+                , StringToIdentifier("v" +String Int2String(Index)) | .PatternNoTopAlts
+                , .Patterns
                 ) = E;
             .NonEmptyStatements
 
     rule decodeForType(T:Type) => e(error("decodeForType: unrecognized type", ListItem(T)))
         [owise]
     rule decodeForType(u8) => v(:: bytes_hooks :: decode_u8 ( buffer_id , .CallParamsList ))
     rule decodeForType(u16) => v(:: bytes_hooks :: decode_u16 ( buffer_id , .CallParamsList ))
-    rule decodeForType(u32) => v(:: bytes_hooks :: decode_u64 ( buffer_id , .CallParamsList ))
-    rule decodeForType(u64) => v(:: bytes_hooks :: decode_u32 ( buffer_id , .CallParamsList ))
+    rule decodeForType(u32) => v(:: bytes_hooks :: decode_u32 ( buffer_id , .CallParamsList ))
+    rule decodeForType(u64) => v(:: bytes_hooks :: decode_u64 ( buffer_id , .CallParamsList ))
 
     syntax Expression ::= callMethod(Identifier, NormalizedFunctionParameterList)  [function, total]
     syntax Expression ::= callMethod(Identifier, CallParamsList)  [function, total]

ukm-semantics/main/representation.md

@@ -0,0 +1,17 @@
+```k
+
+module UKM-REPRESENTATION
+    imports private BYTES-SYNTAX
+    imports private INT-SYNTAX
+    imports private MINT
+
+    syntax UkmValue ::= ukmBytesValue(Bytes)
+                      | ukmIntValue(Int)
+    syntax UkmExpression  ::= ukmBytesId(MInt{64})
+                            | ukmInt(MInt{64})
+                            | UkmValue
+    syntax KResult ::= UkmValue
+
+endmodule
+
+```

ukm-semantics/test/execution.md

@@ -7,6 +7,8 @@ module UKM-TEST-SYNTAX
     syntax ExecutionItem  ::= "mock" "CallData"
                             | "call_contract" Int
                             | "push_output"
+                            | "push_status"
+                            | "check_eq" Int
 endmodule
 
 module UKM-TEST-EXECUTION
@@ -15,6 +17,7 @@ module UKM-TEST-EXECUTION
     imports private UKM-EXECUTION-SYNTAX
     imports private UKM-HOOKS-BYTES-CONFIGURATION
     imports private UKM-HOOKS-BYTES-SYNTAX
+    imports private UKM-HOOKS-STATE-CONFIGURATION
     imports private UKM-HOOKS-UKM-SYNTAX
     imports private UKM-TEST-SYNTAX
 
@@ -27,6 +30,31 @@ module UKM-TEST-EXECUTION
 
     rule call_contract Account => ukmExecute(Account, 100)
 
+    rule
+        <k>
+            push_output => ukmBytesNew(Output) ~> return_value
+            ...
+        </k>
+        <ukm-output>
+            Output:Bytes
+        </ukm-output>
+
+    rule
+        <k>
+            push_status => .K
+            ...
+        </k>
+        <ukm-status>
+            Status:Int
+        </ukm-status>
+        <test-stack>
+            .List => ListItem(Status)
+            ...
+        </test-stack>
+
+    rule
+        <k> check_eq I:Int => .K ... </k>
+        <test-stack> ListItem(I) => .List ... </test-stack>
 endmodule
 
 ```