diff --git a/Makefile b/Makefile index 3a1416b..e052e85 100644 --- a/Makefile +++ b/Makefile @@ -82,6 +82,11 @@ UKM_NO_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ukm-no-contract/output UKM_NO_CONTRACT_TESTING_INPUTS ::= $(wildcard $(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/*.run) UKM_NO_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/%,$(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(UKM_NO_CONTRACT_TESTING_INPUTS)) +UKM_WITH_CONTRACT_TESTING_INPUT_DIR ::= tests/ukm-with-contract +UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ukm-with-contract/output +UKM_WITH_CONTRACT_TESTING_INPUTS ::= $(wildcard $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/*.run) +UKM_WITH_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/%,$(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(UKM_WITH_CONTRACT_TESTING_INPUTS)) + .PHONY: clean build build-legacy test test-legacy syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test ukm-no-contracts-test all: build test @@ -127,6 +132,8 @@ demos-test: $(DEMOS_TESTING_OUTPUTS) ukm-no-contracts-test: $(UKM_NO_CONTRACT_TESTING_OUTPUTS) +ukm-with-contracts-test: $(UKM_WITH_CONTRACT_TESTING_OUTPUTS) + $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES) # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(RUST_PREPROCESSING_KOMPILED) @@ -424,3 +431,51 @@ $(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ -pTEST=$(CURDIR)/parsers/test-ukm-testing-execution.sh cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" mv -f $@.tmp $@ + + +# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs +# as a dependency +$(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ + $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/%.run \ + $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs \ + $(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs \ + $(UKM_TESTING_TIMESTAMP) \ + $(wildcard parsers/inc-*.sh) \ + parsers/crates-ukm-testing-execution.sh \ + parsers/test-ukm-testing-execution.sh + mkdir -p $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR) + + echo "<(<" > $@.in.tmp + echo "::bytes_hooks" >> $@.in.tmp + echo "<|>" >> $@.in.tmp + cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp + echo ">)>" >> $@.in.tmp + + echo "<(<" >> $@.in.tmp + echo "::state_hooks" >> $@.in.tmp + echo "<|>" >> $@.in.tmp + cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/state_hooks.rs >> $@.in.tmp + echo ">)>" >> $@.in.tmp + + echo "<(<" >> $@.in.tmp + echo "::ukm" >> $@.in.tmp + echo "<|>" >> $@.in.tmp + cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs >> $@.in.tmp + echo ">)>" >> $@.in.tmp + + echo "<(<" >> $@.in.tmp + echo "$<" | sed 's%^.*/%%' | sed 's/\..*//' | sed 's/^/::/' >> $@.in.tmp + echo "<|>" >> $@.in.tmp + cat "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" >> $@.in.tmp + echo ">)>" >> $@.in.tmp + + krun \ + $@.in.tmp \ + --parser $(CURDIR)/parsers/crates-ukm-testing-execution.sh \ + --definition $(UKM_TESTING_KOMPILED) \ + --output kore \ + --output-file $@.tmp \ + -cTEST='$(shell cat $<)' \ + -pTEST=$(CURDIR)/parsers/test-ukm-testing-execution.sh + cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" + mv -f $@.tmp $@ diff --git a/mx-rust-semantics/main/preprocessing/configuration.md b/mx-rust-semantics/main/preprocessing/configuration.md index 23fa448..6f724c5 100644 --- a/mx-rust-semantics/main/preprocessing/configuration.md +++ b/mx-rust-semantics/main/preprocessing/configuration.md @@ -17,7 +17,7 @@ module MX-RUST-PREPROCESSED-CONTRACT-TRAIT-CONFIGURATION imports RUST-SHARED-SYNTAX configuration - (#token("no#path", "Identifier"):Identifier):TypePath // String to Identifier + (#token("no#path", "Identifier"):Identifier):TypePath endmodule module MX-RUST-PREPROCESSED-PROXIES-CONFIGURATION diff --git a/rust-semantics/error.md b/rust-semantics/error.md index 0f3f045..96ae836 100644 --- a/rust-semantics/error.md +++ b/rust-semantics/error.md @@ -5,6 +5,8 @@ module RUST-ERROR-SYNTAX syntax ValueListOrError ::= concat(ValueOrError, ValueListOrError) [function, total] syntax PtrListOrError ::= concat(Ptr, PtrListOrError) [function, total] + syntax StringOrError ::= concat(StringOrError, StringOrError) [function, total] + syntax NonEmptyStatementsOrError ::= concat(NonEmptyStatementsOrError, NonEmptyStatementsOrError) [function, total] syntax PtrValueOrError ::= wrapPtrValueOrError(Ptr, ValueOrError) [function, total] syntax TypePathOrError ::= doubleColonOrError(TypePathSegmentsOrError) [function, total] syntax TypePathOrError ::= injectOrError(TypePathSegmentsOrError) [function, total] @@ -22,10 +24,18 @@ module RUST-ERROR rule concat(V:Value, L:ValueList) => V , L rule concat(_:Value, E:SemanticsError) => E rule concat(E:SemanticsError, _:ValueListOrError) => E - rule concat(E:ValueOrError, L:ValueListOrError) - => error("unexpected branch (concat(ValueOrError, ValueListOrError))", ListItem(E) ListItem(L)) + + rule concat(S1:String:StringOrError, S2:String:StringOrError) => S1 +String S2 + rule concat(_:String:StringOrError, E:SemanticsError:StringOrError) => E + rule concat(E:SemanticsError:StringOrError, _:StringOrError) => E + rule concat(S1:StringOrError, S2:StringOrError) + => error("concat(StringOrError, StringOrError): Unknown error", ListItem(S1) ListItem(S2)) [owise] + rule concat(S1:NonEmptyStatements, S2:NonEmptyStatements) => concatNonEmptyStatements(S1, S2) + rule concat(_:NonEmptyStatements, E:SemanticsError) => E + rule concat(E:SemanticsError, _:NonEmptyStatementsOrError) => E + rule wrapPtrValueOrError(P:Ptr, V:Value) => ptrValue(P, V) rule wrapPtrValueOrError(_:Ptr, E:SemanticsError) => E @@ -38,9 +48,9 @@ module RUST-ERROR rule concat(_:TypePathSegment, E) => E rule concat(S:TypePathSegment, Ss:TypePathSegments) => S :: Ss - rule andOrError(_:ExpressionOrError, E:SemanticsError) => E - rule andOrError(E:SemanticsError, _:Expression) => E - rule andOrError(E1:Expression, E2:Expression) => E1 && E2 + rule andOrError(_:ExpressionOrError, e(E:SemanticsError)) => e(E) + rule andOrError(e(E:SemanticsError), v(_:Expression)) => e(E) + rule andOrError(v(E1:Expression), v(E2:Expression)) => v(E1 && E2) rule tupleOrError(L:ValueList) => tuple(L) rule tupleOrError(E:SemanticsError) => E diff --git a/rust-semantics/expression/comparisons.md b/rust-semantics/expression/comparisons.md index 4dc9e16..1c75f95 100644 --- a/rust-semantics/expression/comparisons.md +++ b/rust-semantics/expression/comparisons.md @@ -23,26 +23,28 @@ module RUST-EXPRESSION-STRUCT-COMPARISONS rule (ptrValue(_, struct(StructName:TypePath, FirstFields:Map)) == ptrValue(_, struct(StructName, SecondFields:Map)) ):Expression - => allPtrEquality - ( listToPtrList(values(FirstFields)) - , listToPtrList(values(SecondFields)) + => unwrap + ( allPtrEquality + ( listToPtrList(values(FirstFields)) + , listToPtrList(values(SecondFields)) + ) ) [owise] syntax ExpressionOrError ::= allPtrEquality(PtrListOrError, PtrListOrError) [function, total] - rule allPtrEquality(E:SemanticsError, _:PtrListOrError) => E - rule allPtrEquality(_:PtrList, E:SemanticsError) => E + rule allPtrEquality(E:SemanticsError, _:PtrListOrError) => e(E) + rule allPtrEquality(_:PtrList, E:SemanticsError) => e(E) - rule allPtrEquality(.PtrList, .PtrList) => true + rule allPtrEquality(.PtrList, .PtrList) => v(true) rule allPtrEquality((P:Ptr , Ps:PtrList), (Q:Ptr , Qs:PtrList)) - => andOrError(P == Q , allPtrEquality(Ps, Qs)) + => andOrError(v(P == Q) , allPtrEquality(Ps, Qs)) rule allPtrEquality(.PtrList, (_:Ptr , _:PtrList) #as Ps:PtrList) - => error("allPtrEquality: Second list too long", ListItem(Ps)) + => e(error("allPtrEquality: Second list too long", ListItem(Ps))) rule allPtrEquality((_:Ptr , _:PtrList) #as Ps:PtrList, .PtrList) - => error("zip(PtrList): First list too long", ListItem(Ps)) + => e(error("zip(PtrList): First list too long", ListItem(Ps))) endmodule diff --git a/rust-semantics/expression/struct.md b/rust-semantics/expression/struct.md index 7ac3b30..48242ec 100644 --- a/rust-semantics/expression/struct.md +++ b/rust-semantics/expression/struct.md @@ -57,9 +57,9 @@ module RUST-EXPRESSION-STRUCT rule fromStructExpressionWithAssignmentsBuildFieldsMap( Name:TypePath, - ((FieldName:Identifier : LE:Expression):StructExprField, RS):StructExprFields, + ((FieldName:Identifier : Le:Expression):StructExprField, RS):StructExprFields, FieldsMap:Map) - => LE ~> FieldName ~> fromStructExpressionWithAssignmentsBuildFieldsMap(Name, RS, FieldsMap) + => Le ~> FieldName ~> fromStructExpressionWithAssignmentsBuildFieldsMap(Name, RS, FieldsMap) ... diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md index 884de7d..26a056f 100644 --- a/rust-semantics/helpers.md +++ b/rust-semantics/helpers.md @@ -42,5 +42,8 @@ module RUST-HELPERS rule isSignedInt(u128) => true rule isSignedInt(&T => T) + rule concatNonEmptyStatements(.NonEmptyStatements, S:NonEmptyStatements) => S + rule concatNonEmptyStatements(S:Statement Ss1:NonEmptyStatements, Ss2:NonEmptyStatements) + => S concatNonEmptyStatements(Ss1, Ss2) endmodule ``` diff --git a/rust-semantics/preprocessing/configuration.md b/rust-semantics/preprocessing/configuration.md index b82430a..78aeb23 100644 --- a/rust-semantics/preprocessing/configuration.md +++ b/rust-semantics/preprocessing/configuration.md @@ -4,8 +4,6 @@ module RUST-PREPROCESSING-CONFIGURATION imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX - syntax Identifier ::= "my_identifier" [token] - configuration @@ -17,7 +15,7 @@ module RUST-PREPROCESSING-CONFIGURATION .List - my_identifier:TypePath + #token("not#initialized", "Identifier"):Identifier:TypePath .List // List of Identifier @@ -30,14 +28,14 @@ module RUST-PREPROCESSING-CONFIGURATION .List // List of TypePath - my_identifier:TypePath + #token("not#initialized", "Identifier"):Identifier:TypePath `emptyOuterAttributes`(.KList):OuterAttributes .List // List of Identifier - my_identifier:PathInExpression + #token("not#initialized", "Identifier"):Identifier:PathInExpression .NormalizedFunctionParameterList ():Type empty:FunctionBodyRepresentation diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index f4489b1..a4fe88d 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -98,7 +98,10 @@ module RUST-REPRESENTATION syntax MapOrError ::= Map | SemanticsError syntax Expression ::= Ptr - syntax ExpressionOrError ::= Expression | SemanticsError + syntax ExpressionOrError ::= v(Expression) | e(SemanticsError) + syntax KItem ::= unwrap(ExpressionOrError) [function, total] + rule unwrap(v(E:Expression)) => E + rule unwrap(e(E:SemanticsError)) => E syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError @@ -129,7 +132,10 @@ module RUST-REPRESENTATION syntax IntOrError ::= valueToInteger(Value) [function, total] syntax ValueOrError ::= integerToValue(Int, Type) [function, total] + syntax StringOrError ::= String | SemanticsError + syntax String ::= IdentifierToString(Identifier) [function, total, hook(STRING.token2string)] + syntax Identifier ::= StringToIdentifier(String) [function, total, hook(STRING.string2token)] syntax CallParamsList ::= reverse(CallParamsList, CallParamsList) [function, total] @@ -175,6 +181,9 @@ module RUST-REPRESENTATION syntax TypePath ::= append(MaybeTypePath, Identifier) [function, total] + syntax NonEmptyStatementsOrError ::= NonEmptyStatements | SemanticsError + syntax NonEmptyStatements ::= concatNonEmptyStatements(NonEmptyStatements, NonEmptyStatements) [function, total] + endmodule ``` diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md index 7f86fb6..4f53038 100644 --- a/rust-semantics/rust-common-syntax.md +++ b/rust-semantics/rust-common-syntax.md @@ -197,8 +197,8 @@ https://doc.rust-lang.org/reference/items/extern-crates.html syntax Struct ::= StructStruct | TupleStruct syntax TupleStruct ::= "TODO: not needed yet, not implementing" syntax StructStruct ::= "struct" Identifier MaybeGenericParams MaybeWhereClause "{" MaybeStructFields "}" - syntax MaybeStructFields ::= "" | StructFields - syntax StructFields ::= List{StructField, ","} + syntax MaybeStructFields ::= "" | StructFields | StructFields "," + syntax StructFields ::= NeList{StructField, ","} syntax StructField ::= OuterAttributes MaybeVisibility Identifier ":" Type //TODO: Outerfields and visibility for //struct fields is not yet supported. diff --git a/rust-semantics/test/configuration.md b/rust-semantics/test/configuration.md index 4126e0e..8c469cb 100644 --- a/rust-semantics/test/configuration.md +++ b/rust-semantics/test/configuration.md @@ -6,6 +6,7 @@ module RUST-EXECUTION-TEST-CONFIGURATION configuration .List + .Map endmodule diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md index e81ab94..5e71ed2 100644 --- a/rust-semantics/test/execution.md +++ b/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] + syntax KItem ::= mock(KItem, K) endmodule module RUST-EXECUTION-TEST @@ -92,6 +93,17 @@ module RUST-EXECUTION-TEST VALUES:Map => VALUES[NVI <- V] NVI:Int => NVI +Int 1 + syntax KItem ::= wrappedK(K) + syntax Mockable + + rule + mock(Mocked:Mockable, Result:K) => .K ... + M:Map => M[Mocked <- wrappedK(Result)] + + rule + (Mocked:Mockable => Result) ... + Mocked |-> wrappedK(Result:K) ... + [priority(10)] endmodule ``` \ No newline at end of file diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ukm-contracts/bytes_hooks.rs index 34d7fff..25d1ee1 100644 --- a/tests/ukm-contracts/bytes_hooks.rs +++ b/tests/ukm-contracts/bytes_hooks.rs @@ -6,7 +6,7 @@ extern "C" { fn append_u64(bytes_id: u64, value: u64) -> u64; fn append_u32(bytes_id: u64, value: u32) -> u64; fn append_u16(bytes_id: u64, value: u16) -> u64; - fn append_u7(bytes_id: u64, value: u8) -> u64; + fn append_u8(bytes_id: u64, value: u8) -> u64; fn append_str(bytes_id: u64, value: &str) -> u64; fn decode_u128(bytes_id: u64) -> (u64, u128); diff --git a/tests/ukm-contracts/state_hooks.rs b/tests/ukm-contracts/state_hooks.rs new file mode 100644 index 0000000..a563c28 --- /dev/null +++ b/tests/ukm-contracts/state_hooks.rs @@ -0,0 +1,4 @@ +extern "C" { + fn setStatus(status: u64); + fn setOutput(bytes_id: u64); +} diff --git a/tests/ukm-contracts/ukm.rs b/tests/ukm-contracts/ukm.rs index ab78967..42ace10 100644 --- a/tests/ukm-contracts/ukm.rs +++ b/tests/ukm-contracts/ukm.rs @@ -1,7 +1,7 @@ #![no_std] // TODO: Support structs and figure out the content of MessageResult -struct MessageResult { } +struct MessageResult { gas: u64 } pub const EVMC_REJECTED: u64 = 0_u64; pub const EVMC_INTERNAL_ERROR: u64 = 1_u64; diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ukm-with-contract/endpoints.1.run new file mode 100644 index 0000000..7ed3553 --- /dev/null +++ b/tests/ukm-with-contract/endpoints.1.run @@ -0,0 +1,23 @@ +call :: bytes_hooks :: empty; +return_value_to_arg; +push "myEndpoint(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; + +output_to_arg; +call :: endpoints :: decode_single_u64; +return_value; + +check_eq 126_u64 + diff --git a/tests/ukm-with-contract/endpoints.rs b/tests/ukm-with-contract/endpoints.rs new file mode 100644 index 0000000..9fc6650 --- /dev/null +++ b/tests/ukm-with-contract/endpoints.rs @@ -0,0 +1,23 @@ +#![no_std] + +#[allow(unused_imports)] +use ukm::*; + +#[ukm::contract] +pub trait Endpoints { + #[init] + fn init(&self) {} + + #[endpoint(myEndpoint)] + fn endpoint(&self, value: u64) -> u64 { + 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 +} diff --git a/ukm-semantics/main/common-tools.md b/ukm-semantics/main/common-tools.md new file mode 100644 index 0000000..35cf524 --- /dev/null +++ b/ukm-semantics/main/common-tools.md @@ -0,0 +1,13 @@ +```k + +module UKM-COMMON-TOOLS-SYNTAX + syntax Identifier ::= "dispatcherMethodIdentifier" [function, total] +endmodule + +module UKM-COMMON-TOOLS + imports private UKM-COMMON-TOOLS-SYNTAX + + rule dispatcherMethodIdentifier => #token("ukm#dispatch#method", "Identifier") +endmodule + +``` \ No newline at end of file diff --git a/ukm-semantics/main/configuration.md b/ukm-semantics/main/configuration.md index 73fefae..a065f34 100644 --- a/ukm-semantics/main/configuration.md +++ b/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 + endmodule diff --git a/ukm-semantics/main/execution.md b/ukm-semantics/main/execution.md index 057de65..0b926d0 100644 --- a/ukm-semantics/main/execution.md +++ b/ukm-semantics/main/execution.md @@ -1,10 +1,16 @@ ```k +requires "common-tools.md" +requires "execution/dispatch.md" requires "execution/syntax.md" requires "hooks.md" +requires "representation.md" module UKM-EXECUTION + imports private UKM-COMMON-TOOLS + imports private UKM-EXECUTION-DISPATCH imports private UKM-HOOKS + imports private UKM-REPRESENTATION endmodule ``` diff --git a/ukm-semantics/main/execution/dispatch.md b/ukm-semantics/main/execution/dispatch.md new file mode 100644 index 0000000..f7e5743 --- /dev/null +++ b/ukm-semantics/main/execution/dispatch.md @@ -0,0 +1,34 @@ +```k + +module UKM-EXECUTION-DISPATCH + imports private COMMON-K-CELL + imports private RUST-REPRESENTATION + imports private RUST-VALUE-SYNTAX + imports private RUST-EXECUTION-CONFIGURATION + imports private UKM-COMMON-TOOLS-SYNTAX + imports private UKM-EXECUTION-SYNTAX + imports private UKM-PREPROCESSING-CONFIGURATION + + syntax UkmInstruction ::= ukmExecute(contract:Value, gas: ValueOrError) + + rule + + ukmExecute(_AccountId:Int, Gas:Int) + => ukmExecute(struct(ContractTrait, .Map), integerToValue(Gas, u64)) + ... + + + ContractTrait:TypePath + + rule + + ukmExecute(... contract: Contract:Value, gas: Gas:Value) + => ptr(NVI) . dispatcherMethodIdentifier ( ptrValue(null, Gas), .CallParamsList ) + ... + + Values:Map => Values[NVI <- Contract] + NVI:Int => NVI +Int 1 + requires notBool NVI in_keys(Values) +endmodule + +``` diff --git a/ukm-semantics/main/execution/syntax.md b/ukm-semantics/main/execution/syntax.md index 54c919c..52b1158 100644 --- a/ukm-semantics/main/execution/syntax.md +++ b/ukm-semantics/main/execution/syntax.md @@ -3,7 +3,7 @@ module UKM-EXECUTION-SYNTAX imports INT-SYNTAX - syntax UKMInstruction ::= ukmExecute(accountId : Int) + syntax UKMInstruction ::= ukmExecute(accountId: Int, gas: Int) endmodule diff --git a/ukm-semantics/main/hooks.md b/ukm-semantics/main/hooks.md index 3c55c44..95a0efd 100644 --- a/ukm-semantics/main/hooks.md +++ b/ukm-semantics/main/hooks.md @@ -1,9 +1,13 @@ ```k requires "hooks/bytes.md" +requires "hooks/state.md" +requires "hooks/ukm.md" module UKM-HOOKS imports private UKM-HOOKS-BYTES + imports private UKM-HOOKS-STATE + imports private UKM-HOOKS-UKM endmodule ``` diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md index bd202c8..bf6acd3 100644 --- a/ukm-semantics/main/hooks/bytes.md +++ b/ukm-semantics/main/hooks/bytes.md @@ -15,12 +15,20 @@ module UKM-HOOKS-BYTES-CONFIGURATION endmodule +module UKM-HOOKS-BYTES-SYNTAX + imports BYTES-SYNTAX + syntax Expression ::= ukmBytesNew(Bytes) +endmodule + module UKM-HOOKS-BYTES imports private BYTES imports private COMMON-K-CELL imports private RUST-HELPERS 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] @@ -38,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 normalizedFunctionCall @@ -175,7 +178,6 @@ module UKM-HOOKS-BYTES | ukmBytesDecode(Int, Bytes, Type) | ukmBytesDecodeInt(Int, Bytes, Type) | ukmBytesDecode(ValueOrError, Bytes) - syntax Expression ::= ukmBytesNew(Bytes) rule diff --git a/ukm-semantics/main/hooks/state.md b/ukm-semantics/main/hooks/state.md new file mode 100644 index 0000000..ef50a11 --- /dev/null +++ b/ukm-semantics/main/hooks/state.md @@ -0,0 +1,74 @@ +```k + +module UKM-HOOKS-STATE-CONFIGURATION + imports BYTES-SYNTAX + imports INT-SYNTAX + + configuration + + 0 + b"" + 0 + +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)] + | ukmSetGasLeft(Expression) [strict(1)] + | ukmSetOutput(Expression) [strict(1)] + | ukmSetOutput(UkmExpression) [strict(1)] + + syntax Identifier ::= "state_hooks" [token] + | "setStatus" [token] + | "setGasLeft" [token] + | "setOutput" [token] + + rule normalizedFunctionCall + ( :: state_hooks :: setStatus :: .PathExprSegments + , StatusId:Ptr , .PtrList + ) + => ukmSetStatus(StatusId) + + rule normalizedFunctionCall + ( :: state_hooks :: setGasLeft :: .PathExprSegments + , GasId:Ptr , .PtrList + ) + => ukmSetGasLeft(GasId) + + rule normalizedFunctionCall + ( :: state_hooks :: setOutput :: .PathExprSegments + , OutputId:Ptr , .PtrList + ) + => ukmSetOutput(OutputId) + + rule + + ukmSetStatus(ptrValue(_, u64(Value))) => ptrValue(null, tuple(.ValueList)) + ... + + _ => MInt2Unsigned(Value) + + rule + + ukmSetGasLeft(ptrValue(_, u64(Value))) => ptrValue(null, tuple(.ValueList)) + ... + + _ => MInt2Unsigned(Value) + + rule ukmSetOutput(ptrValue(_, u64(BytesId))) => ukmSetOutput(ukmBytesId(BytesId)) + rule + + ukmSetOutput(ukmBytesValue(Value:Bytes)) => ptrValue(null, tuple(.ValueList)) + ... + + _ => Value + +endmodule + +``` diff --git a/ukm-semantics/main/hooks/ukm.md b/ukm-semantics/main/hooks/ukm.md new file mode 100644 index 0000000..b6d2a41 --- /dev/null +++ b/ukm-semantics/main/hooks/ukm.md @@ -0,0 +1,20 @@ +```k + +module UKM-HOOKS-UKM-SYNTAX + syntax UkmHook ::= CallDataHook() +endmodule + + +module UKM-HOOKS-UKM + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + imports private UKM-HOOKS-UKM-SYNTAX + + syntax Identifier ::= "ukm" [token] + | "CallData" [token] + + rule normalizedFunctionCall ( ukm :: CallData :: .PathExprSegments , .PtrList ) + => CallDataHook() +endmodule + +``` diff --git a/ukm-semantics/main/preprocessed-configuration.md b/ukm-semantics/main/preprocessed-configuration.md index 6b12cb0..a9e2d93 100644 --- a/ukm-semantics/main/preprocessed-configuration.md +++ b/ukm-semantics/main/preprocessed-configuration.md @@ -1,13 +1,10 @@ ```k -module UKM-PREPROCESSED-CONFIGURATION - configuration - .K -endmodule +requires "preprocessing/configuration.md" module UKM-FULL-PREPROCESSED-CONFIGURATION imports RUST-PREPROCESSING-CONFIGURATION - imports UKM-PREPROCESSED-CONFIGURATION + imports UKM-PREPROCESSING-CONFIGURATION configuration diff --git a/ukm-semantics/main/preprocessing.md b/ukm-semantics/main/preprocessing.md index ebcd71d..46645bc 100644 --- a/ukm-semantics/main/preprocessing.md +++ b/ukm-semantics/main/preprocessing.md @@ -1,8 +1,19 @@ ```k +requires "preprocessing/crates.md" +requires "preprocessing/endpoints.md" +requires "preprocessing/methods.md" requires "preprocessing/syntax.md" +requires "preprocessing/traits.md" +requires "common-tools.md" +requires "representation.md" module UKM-PREPROCESSING + imports private UKM-COMMON-TOOLS + imports private UKM-PREPROCESSING-CRATES + imports private UKM-PREPROCESSING-ENDPOINTS + imports private UKM-PREPROCESSING-METHODS + imports private UKM-PREPROCESSING-TRAITS endmodule ``` diff --git a/ukm-semantics/main/preprocessing/configuration.md b/ukm-semantics/main/preprocessing/configuration.md new file mode 100644 index 0000000..9302083 --- /dev/null +++ b/ukm-semantics/main/preprocessing/configuration.md @@ -0,0 +1,21 @@ +```k + +module UKM-PREPROCESSING-CONFIGURATION + imports RUST-SHARED-SYNTAX + + configuration + + + (#token("not#initialized", "Identifier"):Identifier):TypePath + + +endmodule + +module UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION + configuration + + .Map + +endmodule + +``` diff --git a/ukm-semantics/main/preprocessing/crates.md b/ukm-semantics/main/preprocessing/crates.md new file mode 100644 index 0000000..1f8e44d --- /dev/null +++ b/ukm-semantics/main/preprocessing/crates.md @@ -0,0 +1,14 @@ +```k + +module UKM-PREPROCESSING-CRATES + imports private COMMON-K-CELL + imports private RUST-PREPROCESSING-CONFIGURATION + imports private UKM-PREPROCESSING-SYNTAX + imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + + rule + ukmPreprocessCrates => ukmPreprocessTraits(Traits) ... + Traits:List +endmodule + +``` diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md new file mode 100644 index 0000000..b97b986 --- /dev/null +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -0,0 +1,282 @@ +```k + +module UKM-PREPROCESSING-ENDPOINTS + imports private COMMON-K-CELL + imports private RUST-CONVERSIONS-SYNTAX + imports private RUST-ERROR-SYNTAX + imports private RUST-PREPROCESSING-CONFIGURATION + imports private RUST-SHARED-SYNTAX + imports private UKM-COMMON-TOOLS-SYNTAX + imports private UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION + imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + + rule + + ukmPreprocessEndpoint + ( Trait:TypePath + , Method:Identifier + , FullMethodPath:PathInExpression + , Name:String + ) + => ukmAddEndpointWrapper + ( typePathToPathInExpression(append(Trait, StringToIdentifier("ukmWrap#" +String Name))) + , Params + , ReturnType + , Method + ) + ~> ukmAddEndpointSignature + ( methodSignature(Name, Params) + , StringToIdentifier("ukmWrap#" +String Name) + ) + ... + + FullMethodPath + (self : $selftype , Params:NormalizedFunctionParameterList) + ReturnType:Type + + + rule ukmAddEndpointWrapper + (... wrapperMethod: WrapperMethod:PathInExpression + , params: Params:NormalizedFunctionParameterList + , returnType: ReturnType:Type + , method: ImplementationMethod:Identifier + ) + => #ukmAddEndpointWrapper + (... wrapperMethod: WrapperMethod + , params: Params + , method: ImplementationMethod + , appendReturn: appendValue(buffer_id, return_value, ReturnType) + , decodeStatements: decodeParams(0, Params) + ) + + rule + + #ukmAddEndpointWrapper + (... wrapperMethod: WrapperMethod:PathInExpression + , params: Params:NormalizedFunctionParameterList + , method: ImplementationMethod:Identifier + , appendReturn: v(Append:Expression) + , decodeStatements: Decode:NonEmptyStatements + ) => .K + ... + + + (.Bag => + + WrapperMethod + + self : $selftype , buffer_id : u64 , gas : u64 , .NormalizedFunctionParameterList + + ():Type + + block({ + .InnerAttributes + :: state_hooks :: setGasLeft(gas , .CallParamsList); + concatNonEmptyStatements + ( Decode + , let return_value = callMethod(ImplementationMethod, Params); + let buffer_id = :: bytes_hooks :: empty(.CallParamsList); + let buffer_id = Append; + :: state_hooks :: setOutput(buffer_id , .CallParamsList); + :: state_hooks :: setStatus(:: ukm :: EVMC_SUCCESS , .CallParamsList); + ) + }) + + `emptyOuterAttributes`(.KList) + + ) + ... + + + rule + + ukmAddEndpointSignature(Signature:String, Method:Identifier) => .K + ... + + + Signatures:Map => Signatures[Signature <- Method] + + requires notBool (Signature in_keys(Signatures)) + + + rule + + ukmAddDispatcher(TypePath) => .K + ... + + + Signatures:Map + + + (.Bag => + + + typePathToPathInExpression(append(TypePath, dispatcherMethodIdentifier)) + + + self : $selftype , gas : u64, .NormalizedFunctionParameterList + + ():Type + + block({ + .InnerAttributes + concatNonEmptyStatements + ( let buffer_id = ukm :: CallData(); + let ( buffer_id | .PatternNoTopAlts + , signature | .PatternNoTopAlts + , .Patterns + ) = decodeSignature(buffer_id); + .NonEmptyStatements + , signatureToCall(signature, keys_list(Signatures), Signatures, buffer_id, gas) + .NonEmptyStatements + ) + }) + + `emptyOuterAttributes`(.KList) + + ) + ... + + + syntax Identifier ::= "buffer_id" [token] + | "signature" [token] + | "gas" [token] + | "state_hooks" [token] + | "setGasLeft" [token] + | "setOutput" [token] + | "setStatus" [token] + | "return_value" [token] + | "bytes_hooks" [token] + | "append_u8" [token] + | "append_u16" [token] + | "append_u32" [token] + | "append_u64" [token] + | "decode_u8" [token] + | "decode_u16" [token] + | "decode_u32" [token] + | "decode_u64" [token] + | "decode_str" [token] + | "empty" [token] + | "ukm" [token] + | "CallData" [token] + | "EVMC_BAD_JUMP_DESTINATION" [token] + | "EVMC_SUCCESS" [token] + + syntax StringOrError ::= methodSignature(String, NormalizedFunctionParameterList) [function, total] + | signatureTypes(NormalizedFunctionParameterList) [function, total] + | signatureType(Type) [function, total] + + rule methodSignature(S:String, Ps:NormalizedFunctionParameterList) + => concat(concat(S +String "(", signatureTypes(Ps)), ")") + + rule signatureTypes(.NormalizedFunctionParameterList) => "" + rule signatureTypes(_ : T:Type , .NormalizedFunctionParameterList) + => signatureType(T) + rule signatureTypes + ( _ : T:Type + , ((_:NormalizedFunctionParameter , _:NormalizedFunctionParameterList) + #as Ps:NormalizedFunctionParameterList) + ) + => concat(signatureType(T), concat(",", signatureTypes(Ps))) + + rule signatureType(u8) => "Uint8" + rule signatureType(u16) => "Uint16" + rule signatureType(u32) => "Uint32" + rule signatureType(u64) => "Uint64" + rule signatureType(T) => error("Unknown type in signatureType:", ListItem(T)) + [owise] + + syntax Statement ::= signatureToCall + ( signature: Identifier + , signatures: List + , signatureToMethod: Map + , bufferId: Identifier + , gas: Identifier + ) [function, total] + rule signatureToCall + (... signature: _:Identifier + , signatures: .List + , signatureToMethod: _:Map + , bufferId: _:Identifier + , gas: _:Identifier + ) + // TODO: Is this the right kind of error? + => :: state_hooks :: setStatus(:: ukm :: EVMC_BAD_JUMP_DESTINATION , .CallParamsList); + + rule signatureToCall + (... signature: Signature:Identifier + , signatures: ListItem(CurrentSignature:String) Signatures:List + , signatureToMethod: (CurrentSignature |-> Method:Identifier _:Map) #as SignatureToMethod:Map + , bufferId: BufferId:Identifier + , gas: Gas:Identifier + ) + => if signature == CurrentSignature { + .InnerAttributes + self . Method ( BufferId , Gas , .CallParamsList ); + .NonEmptyStatements + } else { + .InnerAttributes + signatureToCall(Signature, Signatures, SignatureToMethod, BufferId, Gas) + .NonEmptyStatements + }; + + syntax Expression ::= decodeSignature(Identifier) [function, total] + rule decodeSignature(BufferId) => :: bytes_hooks :: decode_str ( BufferId , .CallParamsList ) + + syntax ExpressionOrError ::= appendValue(bufferId: Identifier, value: Identifier, Type) [function, total] + rule appendValue(BufferId:Identifier, Value:Identifier, u8) + => v(:: bytes_hooks :: append_u8 ( BufferId , Value , .CallParamsList )) + rule appendValue(BufferId:Identifier, Value:Identifier, u16) + => v(:: bytes_hooks :: append_u16 ( BufferId , Value , .CallParamsList )) + rule appendValue(BufferId:Identifier, Value:Identifier, u32) + => 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, ()) => v(BufferId) + rule appendValue(BufferId:Identifier, Value:Identifier, T:Type) + => e(error("appendValue: unrecognized type", ListItem(BufferId) ListItem(Value) ListItem(T))) + [owise] + + syntax NonEmptyStatementsOrError ::= decodeParams(Int, NormalizedFunctionParameterList) [function, total] + rule decodeParams(_:Int, .NormalizedFunctionParameterList) => .NonEmptyStatements + rule decodeParams(Index:Int, _ : T:Type , Ps:NormalizedFunctionParameterList) + => concat(decodeParam(Index, T), decodeParams(Index +Int 1, Ps)) + + syntax NonEmptyStatementsOrError ::= decodeParam(Int, Type) [function, total] + syntax NonEmptyStatementsOrError ::= decodeParam(Int, ExpressionOrError) [function, total] + syntax ExpressionOrError ::= decodeForType(Type) [function, total] + 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 | .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_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] + syntax CallParamsList ::= buildArgs(Int, NormalizedFunctionParameterList) [function, total] + + rule callMethod(Method:Identifier, Ps:NormalizedFunctionParameterList) + => callMethod(Method, buildArgs(0, Ps)) + + rule callMethod(Method:Identifier, .CallParamsList) + => self . Method ( ) + rule callMethod(Method:Identifier, (_ , _:CallParamsList) #as Ps:CallParamsList) + => self . Method ( Ps ) + + rule buildArgs(_:Int, .NormalizedFunctionParameterList) => .CallParamsList + rule buildArgs(Index:Int, _:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList) + => StringToIdentifier("v" +String Int2String(Index)) , buildArgs(Index +Int 1, Ps) + +endmodule + +``` diff --git a/ukm-semantics/main/preprocessing/methods.md b/ukm-semantics/main/preprocessing/methods.md new file mode 100644 index 0000000..4a27f90 --- /dev/null +++ b/ukm-semantics/main/preprocessing/methods.md @@ -0,0 +1,69 @@ +```k + +module UKM-PREPROCESSING-METHODS + imports private COMMON-K-CELL + imports private K-EQUAL-SYNTAX + imports private RUST-CONVERSIONS-SYNTAX + imports private RUST-PREPROCESSING-CONFIGURATION + imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + + rule ukmPreprocessMethods(_:TypePath, .List) => .K + rule ukmPreprocessMethods(Trait:TypePath, ListItem(Name:Identifier) Methods:List) + => ukmPreprocessMethod(Trait, Name, typePathToPathInExpression(append(Trait, Name))) + ~> ukmPreprocessMethods(Trait, Methods:List) + + rule + + ukmPreprocessMethod(Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression) + => ukmPreprocessEndpoint + (... trait: Trait + , method: MethodIdentifier + , fullMethodPath: Method + , endpointName: getEndpointName(Atts, MethodIdentifier) + ) + ... + + Method + Atts:OuterAttributes + requires getEndpointName(Atts, MethodIdentifier) =/=K "" + [priority(50)] + rule ukmPreprocessMethod(_:TypePath, _:Identifier, _:PathInExpression) => .K + [owise] + + // This is identical to the function in the mx-rust semantics. + syntax String ::= getEndpointName(atts:OuterAttributes, default:Identifier) [function, total] + rule getEndpointName(, _:Identifier) => "" + rule getEndpointName(.NonEmptyOuterAttributes, _:Identifier) => "" + rule getEndpointName + ( (#[ #token("init", "Identifier") :: .SimplePathList + ]) + _:NonEmptyOuterAttributes + , _:Identifier + ) => "#init" + rule getEndpointName + ( (#[ #token("upgrade", "Identifier") :: .SimplePathList + ]) + _:NonEmptyOuterAttributes + , _:Identifier + ) => "#upgrade" + rule getEndpointName + ( (#[ #token("endpoint", "Identifier") :: .SimplePathList + ( Name:Identifier :: .PathExprSegments, .CallParamsList ) + ]) + _:NonEmptyOuterAttributes + , _:Identifier + ) => IdentifierToString(Name) + rule getEndpointName + ( (#[ #token("view", "Identifier") :: .SimplePathList + ( Name:Identifier :: .PathExprSegments, .CallParamsList ) + ]) + _:NonEmptyOuterAttributes + , _:Identifier + ) => IdentifierToString(Name) + rule getEndpointName(_:OuterAttribute Atts:NonEmptyOuterAttributes, Default:Identifier) + => getEndpointName(Atts, Default) + [owise] + +endmodule + +``` diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ukm-semantics/main/preprocessing/syntax.md index 1f2e8c9..eeb8a62 100644 --- a/ukm-semantics/main/preprocessing/syntax.md +++ b/ukm-semantics/main/preprocessing/syntax.md @@ -1,7 +1,42 @@ ```k module UKM-PREPROCESSING-SYNTAX + imports INT-SYNTAX + syntax UKMInstruction ::= "ukmPreprocessCrates" endmodule +module UKM-PREPROCESSING-SYNTAX-PRIVATE + imports LIST + imports RUST-REPRESENTATION + imports RUST-SHARED-SYNTAX + + syntax UKMInstruction ::= ukmPreprocessTraits(List) + | ukmPreprocessTrait(TypePath) + | ukmPreprocessMethods(trait: TypePath, List) + | ukmPreprocessMethod(trait: TypePath, methodId: Identifier, fullMethodPath: PathInExpression) + | ukmPreprocessEndpoint + ( trait: TypePath + , method: Identifier + , fullMethodPath: PathInExpression + , endpointName: String + ) + | ukmAddEndpointWrapper + ( wrapperMethod: PathInExpression + , params: NormalizedFunctionParameterList + , returnType: Type + , method: Identifier + ) + | #ukmAddEndpointWrapper + ( wrapperMethod: PathInExpression + , params: NormalizedFunctionParameterList + , method: Identifier + , appendReturn: ExpressionOrError + , decodeStatements: NonEmptyStatementsOrError + ) + | ukmAddEndpointSignature(signature: StringOrError, method: Identifier) + | ukmAddDispatcher(TypePath) + +endmodule + ``` diff --git a/ukm-semantics/main/preprocessing/traits.md b/ukm-semantics/main/preprocessing/traits.md new file mode 100644 index 0000000..2f1bcd0 --- /dev/null +++ b/ukm-semantics/main/preprocessing/traits.md @@ -0,0 +1,35 @@ +```k + +module UKM-PREPROCESSING-TRAITS + imports private COMMON-K-CELL + imports private RUST-PREPROCESSING-CONFIGURATION + imports private UKM-PREPROCESSING-CONFIGURATION + imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + + rule ukmPreprocessTraits(.List) => .K + rule ukmPreprocessTraits(ListItem(T:TypePath) Traits:List) + => ukmPreprocessTrait(T) ~> ukmPreprocessTraits(Traits) + + rule + + ukmPreprocessTrait(Trait:TypePath) + => ukmPreprocessMethods(Trait, Methods) ~> ukmAddDispatcher(Trait) + ... + + Trait + + #[ #token("ukm", "Identifier") + :: #token("contract", "Identifier") + :: .SimplePathList + ] + .NonEmptyOuterAttributes + + Methods:List + _ => Trait + + // There should be an owise rule rewriting ukmPreprocessTrait(_) to .K + // For now, it is probably more useful to stop execution when encountering + // an unknown trait than skipping it. +endmodule + +``` diff --git a/ukm-semantics/main/representation.md b/ukm-semantics/main/representation.md new file mode 100644 index 0000000..7de5054 --- /dev/null +++ b/ukm-semantics/main/representation.md @@ -0,0 +1,18 @@ +```k + +module UKM-REPRESENTATION + imports private BYTES-SYNTAX + imports private INT-SYNTAX + imports private MINT + imports private RUST-VALUE-SYNTAX + + syntax UkmValue ::= ukmBytesValue(Bytes) + | ukmIntValue(Int) + syntax UkmExpression ::= ukmBytesId(MInt{64}) + | ukmInt(MInt{64}) + | UkmValue + syntax KResult ::= UkmValue + +endmodule + +``` diff --git a/ukm-semantics/targets/execution/configuration.md b/ukm-semantics/targets/execution/configuration.md index d81dc0b..c5d7b08 100644 --- a/ukm-semantics/targets/execution/configuration.md +++ b/ukm-semantics/targets/execution/configuration.md @@ -13,7 +13,7 @@ module COMMON-K-CELL configuration ukmDecodePreprocessedCell($PGM:Bytes) - ~> ukmExecute($ACCTCODE:Int) + ~> ukmExecute($ACCTCODE:Int, $GAS:Int) endmodule diff --git a/ukm-semantics/targets/preprocessing/configuration.md b/ukm-semantics/targets/preprocessing/configuration.md index 020fe21..117bd71 100644 --- a/ukm-semantics/targets/preprocessing/configuration.md +++ b/ukm-semantics/targets/preprocessing/configuration.md @@ -22,10 +22,12 @@ endmodule module UKM-TARGET-CONFIGURATION imports COMMON-K-CELL imports UKM-FULL-PREPROCESSED-CONFIGURATION + imports UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION configuration + endmodule diff --git a/ukm-semantics/targets/testing/configuration.md b/ukm-semantics/targets/testing/configuration.md index 84c1fc9..7d3a7c8 100644 --- a/ukm-semantics/targets/testing/configuration.md +++ b/ukm-semantics/targets/testing/configuration.md @@ -9,10 +9,12 @@ requires "rust-semantics/test/configuration.md" module COMMON-K-CELL imports private RUST-EXECUTION-TEST-PARSING-SYNTAX imports private RUST-PREPROCESSING-SYNTAX + imports private UKM-PREPROCESSING-SYNTAX configuration cratesParser($PGM:WrappedCrateList) + ~> ukmPreprocessCrates ~> $TEST:ExecutionTest endmodule @@ -23,11 +25,13 @@ module UKM-TARGET-CONFIGURATION imports RUST-EXECUTION-TEST-CONFIGURATION imports UKM-CONFIGURATION imports UKM-FULL-PREPROCESSED-CONFIGURATION + imports UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION imports UKM-TEST-CONFIGURATION configuration + diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index e3bc92e..b407c07 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -1,10 +1,62 @@ ```k module UKM-TEST-SYNTAX + imports INT-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX + + syntax ExecutionItem ::= "mock" "CallData" + | "call_contract" Int + | "output_to_arg" + | "push_status" + | "check_eq" Int endmodule module UKM-TEST-EXECUTION + imports private COMMON-K-CELL + imports private RUST-EXECUTION-TEST-CONFIGURATION + 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 + + syntax Mockable ::= UkmHook + + rule + mock CallData => mock(CallDataHook(), V) ... + + (ListItem(ptrValue(_, u64(_BytesId)) #as V:PtrValue) => .List) + ... + + + rule call_contract Account => ukmExecute(Account, 100) + + rule + + output_to_arg => ukmBytesNew(Output) ~> return_value_to_arg + ... + + + Output:Bytes + + + rule + + push_status => .K + ... + + + Status:Int + + + .List => ListItem(Status) + ... + + + rule + check_eq I:Int => .K ... + ListItem(I) => .List ... endmodule ```