-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Contract initialization without args and simple calls
- Loading branch information
1 parent
4eac1c1
commit 5783250
Showing
47 changed files
with
762 additions
and
140 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,9 @@ | ||
| ```k | ||
| requires "calls/implementation.md" | ||
| module MX-RUST-CALLS | ||
| imports private MX-RUST-CALLS-IMPLEMENTATION | ||
| endmodule | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,17 @@ | ||
| ```k | ||
| module MX-RUST-CALLS-CONFIGURATION | ||
| imports LIST | ||
| imports RUST-SHARED-SYNTAX | ||
| configuration | ||
| <mx-rust-calls> | ||
| <rust-execution-state-stack> .List </rust-execution-state-stack> | ||
| <mx-rust-endpoint-to-function> .Map </mx-rust-endpoint-to-function> // String to Identifier | ||
| // Valid only while a contract call is being prepared | ||
| <mx-rust-last-trait-name> (#token("no#path", "Identifier"):Identifier):TypePath </mx-rust-last-trait-name> | ||
| </mx-rust-calls> | ||
| endmodule | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,92 @@ | ||
| ```k | ||
| module MX-RUST-CALLS-IMPLEMENTATION | ||
| imports private COMMON-K-CELL | ||
| imports private MX-CALL-CONFIGURATION | ||
| imports private MX-COMMON-SYNTAX | ||
| imports private MX-RUST-CALLS-CONFIGURATION | ||
| imports private MX-RUST-REPRESENTATION | ||
| imports private RUST-EXECUTION-CONFIGURATION | ||
| imports private RUST-PREPROCESSING-CONFIGURATION | ||
| imports private RUST-REPRESENTATION | ||
| imports private RUST-SHARED-SYNTAX | ||
| rule (.K => rustValueToMx(V)) | ||
| ~> rustValuesToMx((V:Value , L:ValueList => L), _:MxValueList) | ||
| rule (V:MxValue => .K) | ||
| ~> rustValuesToMx(_:ValueList, (L:MxValueList => V , L)) | ||
| rule rustValuesToMx(.ValueList, ReversedArgs:MxValueList) ~> Hook:MxHookName | ||
| => Hook(reverse(ReversedArgs, .MxValueList)) | ||
| rule | ||
| <k> | ||
| host.pushCallState => .K | ||
| ... | ||
| </k> | ||
| Execution:ExecutionCell | ||
| <rust-execution-state-stack> .List => ListItem(Execution) ... </rust-execution-state-stack> | ||
| rule | ||
| <k> | ||
| host.popCallState => .K | ||
| ... | ||
| </k> | ||
| (_:ExecutionCell => Execution) | ||
| <rust-execution-state-stack> ListItem(Execution:ExecutionCell) => .List ... </rust-execution-state-stack> | ||
| rule | ||
| <k> | ||
| host.resetCallState => .K | ||
| ... | ||
| </k> | ||
| (_:ExecutionCell => <execution>... <values> .Map </values> </execution>) | ||
| rule | ||
| <k> | ||
| host.newEnvironment | ||
| ( rustCode | ||
| ( EndpointToFunction:Map | ||
| , TraitName:TypePath | ||
| , Preprocessed:PreprocessedCell | ||
| ) | ||
| ) | ||
| => .K | ||
| ... | ||
| </k> | ||
| <mx-rust-last-trait-name> _ => TraitName </mx-rust-last-trait-name> | ||
| <mx-rust-endpoint-to-function> _ => EndpointToFunction </mx-rust-endpoint-to-function> | ||
| (_:PreprocessedCell => Preprocessed) | ||
| rule | ||
| <k> | ||
| host.mkCall(FunctionName:String) | ||
| => MxRust#newContractObject(TraitName) | ||
| ~> MxRust#partialMethodCall(Endpoint, mxArgsToRustArgs(Args)) | ||
| ... | ||
| </k> | ||
| <mx-rust-endpoint-to-function> | ||
| FunctionName |-> Endpoint:Identifier ... | ||
| </mx-rust-endpoint-to-function> | ||
| <mx-rust-last-trait-name> | ||
| TraitName:TypePath | ||
| => (#token("no#path", "Identifier"):Identifier):TypePath | ||
| </mx-rust-last-trait-name> | ||
| <mx-call-args> Args:MxValueList </mx-call-args> | ||
| rule ptrValue(...) #as SelfValue:Expression | ||
| ~> MxRust#partialMethodCall(Method:Identifier, Params:CallParamsList) | ||
| => methodCall(... self: SelfValue, method: Method, params: Params) | ||
| syntax MxRustInstruction ::= "MxRust#newContractObject" "(" TypePath ")" | ||
| rule MxRust#newContractObject(P:TypePath) => Rust#newStruct(P, .Map) | ||
| syntax MxRustInstruction ::= "MxRust#partialMethodCall" "(" Identifier "," CallParamsList ")" | ||
| syntax CallParamsList ::= mxArgsToRustArgs(MxValueList) [function, total] | ||
| rule mxArgsToRustArgs(.MxValueList) => .CallParamsList | ||
| rule (ptrValue(_, V:Value) => rustValueToMx(V)) ~> endCall | ||
| endmodule | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,50 +1,60 @@ | ||
| ```k | ||
| module MX-RUST-GLUE | ||
| imports private COMMON-K-CELL | ||
| imports private MX-COMMON-SYNTAX | ||
| imports private RUST-EXECUTION-CONFIGURATION | ||
| imports private RUST-VALUE-SYNTAX | ||
| imports private MX-RUST-REPRESENTATION | ||
| rule | ||
| <k> | ||
| storeHostValue | ||
| (... destination: rustDestination(ValueId, _:MxRustType) | ||
| , value: wrappedRust(V:Value) | ||
| ) | ||
| => .K | ||
| ... | ||
| </k> | ||
| <values> Values:Map => Values[ValueId <- V] </values> | ||
| requires ValueId >=Int 0 | ||
| rule | ||
| (.K => mxRustEmptyValue(T)) | ||
| ~> storeHostValue | ||
| (... destination: rustDestination(_, T:MxRustType) | ||
| , value: mxWrappedEmpty | ||
| ) | ||
| rule | ||
| (ptrValue(_, V:Value) => .K) | ||
| ~> storeHostValue | ||
| (... value: mxWrappedEmpty => wrappedRust(V) | ||
| ) | ||
| rule | ||
| <k> | ||
| mxRustLoadPtr(P:Int) => ptrValue(ptr(P), V) | ||
| ... | ||
| </k> | ||
| <values> P |-> V:Value ... </values> | ||
| imports private COMMON-K-CELL | ||
| imports private K-EQUAL-SYNTAX | ||
| imports private MX-COMMON-SYNTAX | ||
| imports private MX-RUST-REPRESENTATION | ||
| imports private RUST-EXECUTION-CONFIGURATION | ||
| imports private RUST-VALUE-SYNTAX | ||
| rule (.K => mxValueToRust(T, V)) | ||
| ~> storeHostValue | ||
| (... destination: rustDestination(_ValueId, rustType(T):MxRustType) | ||
| , value: V:MxValue | ||
| ) | ||
| requires notBool isMxEmptyValue(V) | ||
| rule | ||
| <k> | ||
| ptrValue(_, V:Value) | ||
| ~> storeHostValue | ||
| (... destination: rustDestination(ValueId, _:MxRustType) | ||
| , value: _:MxValue | ||
| ) | ||
| => .K | ||
| ... | ||
| </k> | ||
| <values> Values:Map => Values[ValueId <- V] </values> | ||
| requires ValueId >=Int 0 | ||
| rule | ||
| (.K => mxRustEmptyValue(T)) | ||
| ~> storeHostValue | ||
| (... destination: rustDestination(_, T:MxRustType) | ||
| , value: mxEmptyValue | ||
| ) | ||
| rule | ||
| <k> | ||
| mxRustLoadPtr(P:Int) => ptrValue(ptr(P), V) | ||
| ... | ||
| </k> | ||
| <values> P |-> V:Value ... </values> | ||
| rule | ||
| <k> mxRustNewValue(V:Value) => ptrValue(ptr(NextId), V) ... </k> | ||
| <next-value-id> NextId:Int => NextId +Int 1 </next-value-id> | ||
| <values> Values:Map => Values[NextId <- V] </values> | ||
| rule mxIntValue(I:Int) ~> mxValueToRust(T:Type) | ||
| rule V:MxValue ~> mxValueToRust(T:Type) | ||
| => mxValueToRust(T, V) | ||
| rule mxValueToRust(T:Type, mxIntValue(I:Int)) | ||
| => mxRustNewValue(integerToValue(I, T)) | ||
| requires | ||
| (T ==K i32 orBool T ==K u32) | ||
| orBool (T ==K i64 orBool T ==K u64) | ||
| endmodule | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.