Implement storage

Pi-Squared-Inc · Oct 16, 2024 · 19d7889 · 19d7889
1 parent efc4633
commit 19d7889
Show file tree

Hide file tree

Showing 18 changed files with 423 additions and 0 deletions.
diff --git a/Makefile b/Makefile
@@ -463,6 +463,12 @@ $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/state_hooks.rs >> $@.in.tmp
 	echo ">)>" >> $@.in.tmp
 
+	echo "<(<" >> $@.in.tmp
+	echo "::single_value_mapper" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/single_value_mapper.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+
 	echo "<(<" >> $@.in.tmp
 	echo "::ukm" >> $@.in.tmp
 	echo "<|>" >> $@.in.tmp

diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md
@@ -100,6 +100,7 @@ module RUST-CASTS
 
     rule implicitCast(struct(T, _) #as V, T) => V
     rule implicitCast(struct(T, _) #as V, T < _ >) => V
+    rule implicitCast(struct(:: A :: T, _) #as V, :: A :: T < _ >) => V
 
     // Rewrites
 

diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ukm-contracts/bytes_hooks.rs
@@ -16,4 +16,6 @@ extern "C" {
   fn decode_u16(bytes_id: u64) -> (u64, u16);
   fn decode_u8(bytes_id: u64) -> (u64, u8);
   fn decode_str(bytes_id: u64) -> (u64, str);
+
+  fn hash(bytes_id: u64) -> u64;
 }
diff --git a/tests/ukm-contracts/single_value_mapper.rs b/tests/ukm-contracts/single_value_mapper.rs
@@ -0,0 +1,8 @@
+#![no_std]
+
+// TODO: Support structs and figure out the content of MessageResult
+struct SingleValueMapper { key: u64, value_type: () }
+
+fn new(key:u64) -> :: single_value_mapper :: SingleValueMapper {
+    :: single_value_mapper :: SingleValueMapper { key: key, value_type: () }
+}
diff --git a/tests/ukm-with-contract/storage.key.run b/tests/ukm-with-contract/storage.key.run
@@ -0,0 +1,47 @@
+mock SetAccountStorageHook ( 7010817630605304703 , 123 ) ukmNoResult();
+mock GetAccountStorageHook ( 7010817630605304703 ) ukmInt64Result(123);
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "setMyDataKey(Uint64,Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 555_u64;
+call :: bytes_hooks :: append_u64;
+return_value_to_arg;
+push 123_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "getMyDataKey(Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 555_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 123_u64
+
diff --git a/tests/ukm-with-contract/storage.rs b/tests/ukm-with-contract/storage.rs
@@ -0,0 +1,36 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use ukm::*;
+
+#[ukm::contract]
+pub trait Storage {
+  #[storage_mapper("myData")]
+  fn my_data(&self) -> ::single_value_mapper::SingleValueMapper<u64>;
+
+  #[storage_mapper("myDataKey")]
+  fn my_data_key(&self, key: u64) -> ::single_value_mapper::SingleValueMapper<u64>;
+
+  #[init]
+  fn init(&self) {}
+
+  #[endpoint(setMyData)]
+  fn set(&self, value: u64) {
+      self.my_data().set(value)
+  }
+
+  #[endpoint(getMyData)]
+  fn get(&self) -> u64 {
+      self.my_data().get()
+  }
+
+  #[endpoint(setMyDataKey)]
+  fn set_key(&self, key: u64, value: u64) {
+      self.my_data_key(key).set(value)
+  }
+
+  #[endpoint(getMyDataKey)]
+  fn get_key(&self, key: u64) -> u64 {
+      self.my_data_key(key).get()
+  }
+}
diff --git a/tests/ukm-with-contract/storage.simple.run b/tests/ukm-with-contract/storage.simple.run
@@ -0,0 +1,41 @@
+mock SetAccountStorageHook ( 1809217465971809 , 123 ) ukmNoResult();
+mock GetAccountStorageHook ( 1809217465971809 ) ukmInt64Result(123);
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "setMyData(Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 123_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "getMyData()";
+call :: bytes_hooks :: append_str;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 123_u64
+
diff --git a/ukm-semantics/main/execution.md b/ukm-semantics/main/execution.md
@@ -1,14 +1,18 @@
 ```k
 
 requires "common-tools.md"
+requires "execution/casts.md"
 requires "execution/dispatch.md"
+requires "execution/storage.md"
 requires "execution/syntax.md"
 requires "hooks.md"
 requires "representation.md"
 
 module UKM-EXECUTION
     imports private UKM-COMMON-TOOLS
+    imports private UKM-EXECUTION-CASTS
     imports private UKM-EXECUTION-DISPATCH
+    imports private UKM-EXECUTION-STORAGE
     imports private UKM-HOOKS
     imports private UKM-REPRESENTATION
 endmodule

diff --git a/ukm-semantics/main/execution/casts.md b/ukm-semantics/main/execution/casts.md
@@ -0,0 +1,16 @@
+```k
+
+module UKM-EXECUTION-CASTS
+    imports private RUST-REPRESENTATION
+    imports private RUST-VALUE-SYNTAX
+    imports private UKM-REPRESENTATION
+
+    syntax Expression ::= ukmCastResult(ValueOrError)
+
+    rule ukmCast(ptrValue(_, V), ptrValue(_, rustType(T))) => ukmCastResult(implicitCast(V, T))
+    rule ukmCastResult(V:Value) => ptrValue(null, V)
+
+
+endmodule
+
+```
diff --git a/ukm-semantics/main/execution/storage.md b/ukm-semantics/main/execution/storage.md
@@ -0,0 +1,38 @@
+```k
+
+module UKM-EXECUTION-STORAGE
+    imports private RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+    imports private UKM-REPRESENTATION
+
+    syntax Identifier ::= "get"  [token]
+                        | "GetAccountStorage"  [token]
+                        | "key"  [token]
+                        | "set"  [token]
+                        | "SetAccountStorage"  [token]
+                        | "single_value_mapper"  [token]
+                        | "SingleValueMapper"  [token]
+                        | "ukm"  [token]
+
+    rule normalizedFunctionCall
+            ( :: single_value_mapper :: SingleValueMapper :: set :: .PathExprSegments
+            , (SelfPtr:Ptr , ValuePtr:Ptr , .PtrList)
+            )
+        =>  :: ukm :: SetAccountStorage :: .PathExprSegments
+            ( SelfPtr . key
+            , ukmCast(ValuePtr, ptrValue(null, rustType(u64)))
+            , .CallParamsList
+            )
+
+    rule normalizedFunctionCall
+            ( :: single_value_mapper :: SingleValueMapper :: get :: .PathExprSegments
+            , (SelfPtr:Ptr , .PtrList)
+            )
+        =>  :: ukm :: GetAccountStorage :: .PathExprSegments
+            ( SelfPtr . key
+            , .CallParamsList
+            )
+
+endmodule
+
+```
diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md
@@ -46,6 +46,7 @@ module UKM-HOOKS-BYTES
                         | "decode_u16"  [token]
                         | "decode_u8"  [token]
                         | "decode_str"  [token]
+                        | "hash"  [token]
 
     rule
         <k>
@@ -162,6 +163,13 @@ module UKM-HOOKS-BYTES
             )
         => ukmBytesDecode(BufferIdId, str)
 
+    rule
+        normalizedFunctionCall
+            ( :: bytes_hooks :: hash :: .PathExprSegments
+            , BufferIdId:Ptr, .PtrList
+            )
+        => ukmBytesHash(BufferIdId)
+
     // ---------------------------------------
 
     rule
@@ -187,6 +195,8 @@ module UKM-HOOKS-BYTES
                             | ukmBytesDecode(Int, Bytes, Type)
                             | ukmBytesDecodeInt(Int, Bytes, Type)
                             | ukmBytesDecode(ValueOrError, Bytes)
+                            | ukmBytesHash(Expression)  [strict(1)]
+                            | ukmBytesHash(UkmExpression)  [strict(1)]
 
     rule
         <k>
@@ -269,6 +279,20 @@ module UKM-HOOKS-BYTES
         => ukmBytesDecode(integerToValue(Value, T), B)
     rule ukmBytesDecode(Value:Value, B:Bytes)
         => tupleExpression(ukmBytesNew(B) , ptrValue(null, Value) , .TupleElementsNoEndComma)
+
+    rule ukmBytesHash(ptrValue(_, u64(BytesId)))
+        => ukmBytesHash(ukmBytesId(BytesId))
+    rule ukmBytesHash(ukmBytesValue(B:Bytes))
+        => ptrValue(null, u64(Int2MInt(#ukmBytesHash(Bytes2Int(B, BE, Unsigned)))))
+
+    syntax Int ::= #ukmBytesHash(Int)  [function, total]
+    rule #ukmBytesHash(I:Int) => #ukmBytesHash(0 -Int I)  requires I <Int 0
+    rule #ukmBytesHash(I:Int) => I requires 0 <=Int I andBool I <Int (1 <<Int 64)
+    rule #ukmBytesHash(I:Int)
+        => #ukmBytesHash
+            ( (I &Int ((1 <<Int 64) -Int 1))
+            |Int #ukmBytesHash(I >>Int 64)
+            )
 endmodule
 
 ```
diff --git a/ukm-semantics/main/hooks/ukm.md b/ukm-semantics/main/hooks/ukm.md
@@ -1,8 +1,15 @@
 ```k
 
 module UKM-HOOKS-UKM-SYNTAX
+    imports INT-SYNTAX
+
     syntax UkmHook  ::= CallDataHook()
                       | CallerHook()
+                      | SetAccountStorageHook(Int, Int)
+                      | GetAccountStorageHook(Int)
+
+    syntax UkmHookResult  ::= ukmNoResult()
+                            | ukmInt64Result(Int)
 endmodule
 
 
@@ -14,11 +21,41 @@ module UKM-HOOKS-UKM
     syntax Identifier ::= "ukm"  [token]
                         | "CallData"  [token]
                         | "Caller"  [token]
+                        | "SetAccountStorage"  [token]
+                        | "GetAccountStorage"  [token]
 
     rule normalizedFunctionCall ( :: ukm :: CallData :: .PathExprSegments , .PtrList )
         => CallDataHook()
     rule normalizedFunctionCall ( :: ukm :: Caller :: .PathExprSegments , .PtrList )
         => CallerHook()
+
+    rule normalizedFunctionCall
+            ( :: ukm :: SetAccountStorage :: .PathExprSegments
+            , (KeyPtr:Ptr , ValuePtr:Ptr , .PtrList)
+            )
+        => #SetAccountStorageHook(KeyPtr, ValuePtr)
+
+    syntax UkmHook ::= #SetAccountStorageHook(Expression, Expression)  [seqstrict]
+
+    rule #SetAccountStorageHook(ptrValue(_, u64(Key)), ptrValue(_, u64(Value)))
+        => SetAccountStorageHook(MInt2Unsigned(Key), MInt2Unsigned(Value))
+
+    rule normalizedFunctionCall
+            ( :: ukm :: GetAccountStorage :: .PathExprSegments
+            , (KeyPtr:Ptr , .PtrList)
+            )
+        => #GetAccountStorageHook(KeyPtr)
+
+    syntax UkmHook ::= #GetAccountStorageHook(Expression)  [strict]
+
+    rule #GetAccountStorageHook(ptrValue(_, u64(Key)))
+        => GetAccountStorageHook(MInt2Unsigned(Key))
+
+    rule ukmNoResult() => ptrValue(null, tuple(.ValueList))
+    syntax UkmHook ::= #ukmInt64Result(ValueOrError)
+    rule ukmInt64Result(Value:Int) => #ukmInt64Result(integerToValue(Value, u64))
+    rule #ukmInt64Result(V:Value) => ptrValue(null, V)
+
 endmodule
 
 ```
diff --git a/ukm-semantics/main/preprocessing.md b/ukm-semantics/main/preprocessing.md
@@ -3,6 +3,7 @@
 requires "preprocessing/crates.md"
 requires "preprocessing/endpoints.md"
 requires "preprocessing/methods.md"
+requires "preprocessing/storage.md"
 requires "preprocessing/syntax.md"
 requires "preprocessing/traits.md"
 requires "common-tools.md"
@@ -13,6 +14,7 @@ module UKM-PREPROCESSING
     imports private UKM-PREPROCESSING-CRATES
     imports private UKM-PREPROCESSING-ENDPOINTS
     imports private UKM-PREPROCESSING-METHODS
+    imports private UKM-PREPROCESSING-STORAGE
     imports private UKM-PREPROCESSING-TRAITS
 endmodule