From 0fd8ca7441ce063a9ea7c421a6878d6e6ef688ca Mon Sep 17 00:00:00 2001 From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com> Date: Thu, 17 Oct 2024 15:03:37 +0300 Subject: [PATCH] Implement storage (#157) * Implement storage * Remove comment * Remove redundant priority --- Makefile | 6 + rust-semantics/expression/casts.md | 1 + tests/ukm-contracts/bytes_hooks.rs | 2 + tests/ukm-contracts/single_value_mapper.rs | 7 ++ tests/ukm-with-contract/storage.key.run | 47 ++++++++ tests/ukm-with-contract/storage.rs | 36 ++++++ tests/ukm-with-contract/storage.simple.run | 41 +++++++ ukm-semantics/main/execution.md | 4 + ukm-semantics/main/execution/casts.md | 16 +++ ukm-semantics/main/execution/storage.md | 38 +++++++ ukm-semantics/main/hooks/bytes.md | 24 ++++ ukm-semantics/main/hooks/ukm.md | 37 +++++++ ukm-semantics/main/preprocessing.md | 2 + ukm-semantics/main/preprocessing/methods.md | 29 ++++- ukm-semantics/main/preprocessing/storage.md | 115 ++++++++++++++++++++ ukm-semantics/main/preprocessing/syntax.md | 10 ++ ukm-semantics/main/representation.md | 3 + ukm-semantics/test/execution.md | 4 + 18 files changed, 421 insertions(+), 1 deletion(-) create mode 100644 tests/ukm-contracts/single_value_mapper.rs create mode 100644 tests/ukm-with-contract/storage.key.run create mode 100644 tests/ukm-with-contract/storage.rs create mode 100644 tests/ukm-with-contract/storage.simple.run create mode 100644 ukm-semantics/main/execution/casts.md create mode 100644 ukm-semantics/main/execution/storage.md create mode 100644 ukm-semantics/main/preprocessing/storage.md diff --git a/Makefile b/Makefile index 28e672a..50a8b69 100644 --- 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 index cba7bb1..d0a9fe1 100644 --- 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 index ae8e34a..aa1a786 100644 --- 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 new file mode 100644 index 0000000..26be625 --- /dev/null +++ b/tests/ukm-contracts/single_value_mapper.rs @@ -0,0 +1,7 @@ +#![no_std] + +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 new file mode 100644 index 0000000..129a218 --- /dev/null +++ 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 new file mode 100644 index 0000000..6667714 --- /dev/null +++ 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; + + #[storage_mapper("myDataKey")] + fn my_data_key(&self, key: u64) -> ::single_value_mapper::SingleValueMapper; + + #[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 new file mode 100644 index 0000000..72b139a --- /dev/null +++ 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 index 0b926d0..eb608d0 100644 --- 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 new file mode 100644 index 0000000..e4ac3d0 --- /dev/null +++ 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 new file mode 100644 index 0000000..94a168f --- /dev/null +++ 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 index 9b25d37..ee69b79 100644 --- 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 @@ -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 @@ -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 I requires 0 <=Int I andBool I #ukmBytesHash + ( (I &Int ((1 <>Int 64) + ) endmodule ``` diff --git a/ukm-semantics/main/hooks/ukm.md b/ukm-semantics/main/hooks/ukm.md index b6343f8..94f5151 100644 --- 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 index 46645bc..f28192a 100644 --- 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 diff --git a/ukm-semantics/main/preprocessing/methods.md b/ukm-semantics/main/preprocessing/methods.md index 4a27f90..c09ecf3 100644 --- a/ukm-semantics/main/preprocessing/methods.md +++ b/ukm-semantics/main/preprocessing/methods.md @@ -26,7 +26,20 @@ module UKM-PREPROCESSING-METHODS Method Atts:OuterAttributes requires getEndpointName(Atts, MethodIdentifier) =/=K "" - [priority(50)] + andBool getStorageName(Atts) ==K "" + rule + + ukmPreprocessMethod(_Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression) + => ukmPreprocessStorage + (... fullMethodPath: Method + , storageName: getStorageName(Atts) + ) + ... + + Method + Atts:OuterAttributes + requires getStorageName(Atts) =/=K "" + andBool getEndpointName(Atts, MethodIdentifier) ==K "" rule ukmPreprocessMethod(_:TypePath, _:Identifier, _:PathInExpression) => .K [owise] @@ -64,6 +77,20 @@ module UKM-PREPROCESSING-METHODS => getEndpointName(Atts, Default) [owise] + // This is identical to the function in the mx-rust semantics. + syntax String ::= getStorageName(atts:OuterAttributes) [function, total] + rule getStorageName() => "" + rule getStorageName(.NonEmptyOuterAttributes) => "" + rule getStorageName + ( (#[ #token("storage_mapper", "Identifier") :: .SimplePathList + ( Name:String, .CallParamsList ) + ]) + _:NonEmptyOuterAttributes + ) => Name + rule getStorageName(_:OuterAttribute Atts:NonEmptyOuterAttributes) + => getStorageName(Atts) + [owise] + endmodule ``` diff --git a/ukm-semantics/main/preprocessing/storage.md b/ukm-semantics/main/preprocessing/storage.md new file mode 100644 index 0000000..3391c73 --- /dev/null +++ b/ukm-semantics/main/preprocessing/storage.md @@ -0,0 +1,115 @@ +```k + +module UKM-PREPROCESSING-STORAGE + imports private COMMON-K-CELL + imports private RUST-ERROR-SYNTAX + imports private RUST-PREPROCESSING-CONFIGURATION + imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + imports private UKM-REPRESENTATION + + rule + + ukmPreprocessStorage + (... fullMethodPath: Method:PathInExpression + , storageName: StorageName:String + ) + => ukmAddStorageMethodBody + (... methodName: Method + , storageName: StorageName + , mapperValueType: MapperValue + , appendParamsInstructions: encodeParams(Params) + ) + ... + + Method + empty + (self : $selftype , Params:NormalizedFunctionParameterList) + + :: single_value_mapper :: SingleValueMapper + < MapperValue:Type , .GenericArgList > + + + rule + + ukmAddStorageMethodBody + (... methodName: Method:PathInExpression + , storageName: StorageName:String + , mapperValueType: MapperValueType:Type + , appendParamsInstructions: Append:NonEmptyStatements + ) => .K + ... + + Method + + empty => block({ .InnerAttributes + concatNonEmptyStatements + ( concatNonEmptyStatements + ( let buffer_id = :: bytes_hooks :: empty(.CallParamsList); + let buffer_id = :: bytes_hooks :: append_str + ( buffer_id + , ptrValue(null, StorageName) + , .CallParamsList + ); + .NonEmptyStatements + , Append + ) + , let hash = :: bytes_hooks :: hash(buffer_id , .CallParamsList); + let storage = :: single_value_mapper :: new(hash , .CallParamsList); + storage . value_type = ptrValue(null, rustType(MapperValueType)); + .NonEmptyStatements + ) + storage + }) + + + syntax Identifier ::= "buffer_id" [token] + | "bytes_hooks" [token] + | "append_str" [token] + | "append_u8" [token] + | "append_u16" [token] + | "append_u32" [token] + | "append_u64" [token] + | "empty" [token] + | "hash" [token] + | "new" [token] + | "single_value_mapper" [token] + | "SingleValueMapper" [token] + | "storage" [token] + | "value_type" [token] + + syntax NonEmptyStatementsOrError ::= encodeParams(NormalizedFunctionParameterList) + [function, total] + rule encodeParams(.NormalizedFunctionParameterList) => .NonEmptyStatements + rule encodeParams(Name:Identifier : T:Type , Ps:NormalizedFunctionParameterList) + => concat(encodeParam(Name, T), encodeParams(Ps)) + rule encodeParams(P:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList) + => error("encodeParams: unexpected", ListItem(P) ListItem(Ps)) + [owise] + + syntax NonEmptyStatementsOrError ::= encodeParam(Identifier, Type) [function, total] + syntax NonEmptyStatementsOrError ::= encodeParam(ExpressionOrError) [function, total] + syntax ExpressionOrError ::= encodeForType(Identifier, Type) [function, total] + + rule encodeParam(Name:Identifier, T:Type) + => encodeParam(encodeForType(Name, T)) + + rule encodeParam(e(E:SemanticsError)) => E + rule encodeParam(v(E:Expression)) + => let buffer_id = E; + .NonEmptyStatements + + rule encodeForType(Name:Identifier, T:Type) + => e(error("decodeForType: unrecognized type", ListItem(Name) ListItem(T))) + [owise] + rule encodeForType(Name:Identifier, u8) + => v(:: bytes_hooks :: append_u8 ( buffer_id , Name , .CallParamsList )) + rule encodeForType(Name:Identifier, u16) + => v(:: bytes_hooks :: append_u16 ( buffer_id , Name , .CallParamsList )) + rule encodeForType(Name:Identifier, u32) + => v(:: bytes_hooks :: append_u32 ( buffer_id , Name , .CallParamsList )) + rule encodeForType(Name:Identifier, u64) + => v(:: bytes_hooks :: append_u64 ( buffer_id , Name , .CallParamsList )) + +endmodule + +``` diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ukm-semantics/main/preprocessing/syntax.md index eeb8a62..a4a4dcc 100644 --- a/ukm-semantics/main/preprocessing/syntax.md +++ b/ukm-semantics/main/preprocessing/syntax.md @@ -36,6 +36,16 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE ) | ukmAddEndpointSignature(signature: StringOrError, method: Identifier) | ukmAddDispatcher(TypePath) + | ukmPreprocessStorage + ( fullMethodPath: PathInExpression + , storageName: String + ) + | ukmAddStorageMethodBody + ( methodName: PathInExpression + , storageName: String + , mapperValueType: Type + , appendParamsInstructions: NonEmptyStatementsOrError + ) endmodule diff --git a/ukm-semantics/main/representation.md b/ukm-semantics/main/representation.md index 7de5054..50af36f 100644 --- a/ukm-semantics/main/representation.md +++ b/ukm-semantics/main/representation.md @@ -13,6 +13,9 @@ module UKM-REPRESENTATION | UkmValue syntax KResult ::= UkmValue + syntax Expression ::= ukmCast(Expression, Expression) [seqstrict] + syntax Value ::= rustType(Type) + endmodule ``` diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index de0d56c..c9d764f 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -3,9 +3,11 @@ module UKM-TEST-SYNTAX imports INT-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX + imports UKM-HOOKS-UKM-SYNTAX syntax ExecutionItem ::= "mock" "CallData" | "mock" "Caller" + | "mock" UkmHook UkmHookResult | "call_contract" Int | "output_to_arg" | "push_status" @@ -38,6 +40,8 @@ module UKM-TEST-EXECUTION ... + rule mock Hook:UkmHook Result:UkmHookResult => mock(Hook, Result) + rule call_contract Account => ukmExecute(Account, 100) rule