Skip to content

Commit

Permalink
Mx-rust framework and storage implementation (#80) (#81)
Browse files Browse the repository at this point in the history 
* Arrange the cells for easier debugging

* Create a list of traits to help with mx preprocessing

* Static method calls

* Integer - value conversions

* Ignore generic args when casting structs

* Framework for executing Mx+Rust

* Framework for testing Mx+Rust

* Implement storage functions

* Implement storage accessors

* Implement BigUint::from

* Default storage values

* Storage set_if_empty

* Storage tests

---------

Co-authored-by: Virgil <[email protected]>
  • Loading branch information
@ACassimiro @virgil-serbanuta
ACassimiro and virgil-serbanuta authored Sep 11, 2024
1 parent ba6decd commit b62f09a
Show file tree
Hide file tree
Showing 39 changed files with 929 additions and 46 deletions.
65 changes: 61 additions & 4 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,14 +27,30 @@ MX_TESTING_OUTPUT_DIR ::= .build/mx/output
MX_TESTING_INPUTS ::= $(wildcard $(MX_TESTING_INPUT_DIR)/**/*.mx)
MX_TESTING_OUTPUTS ::= $(patsubst $(MX_TESTING_INPUT_DIR)/%,$(MX_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_TESTING_INPUTS))

.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test
MX_RUST_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
MX_RUST_KOMPILED ::= .build/mx-rust-kompiled
MX_RUST_TIMESTAMP ::= $(MX_RUST_KOMPILED)/timestamp

MX_RUST_TESTING_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
MX_RUST_TESTING_KOMPILED ::= .build/mx-rust-testing-kompiled
MX_RUST_TESTING_TIMESTAMP ::= $(MX_RUST_TESTING_KOMPILED)/timestamp
MX_RUST_TESTING_INPUT_DIR ::= tests/mx-rust
MX_RUST_TESTING_OUTPUT_DIR ::= .build/mx-rust/output
MX_RUST_TESTING_INPUTS ::= $(wildcard $(MX_RUST_TESTING_INPUT_DIR)/*.run)
MX_RUST_TESTING_OUTPUTS ::= $(patsubst $(MX_RUST_TESTING_INPUT_DIR)/%,$(MX_RUST_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_RUST_TESTING_INPUTS))

.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test mx-rust-test

clean:
rm -r .build

build: $(RUST_PREPROCESSING_TIMESTAMP) $(RUST_EXECUTION_TIMESTAMP) $(MX_TESTING_TIMESTAMP)
build: $(RUST_PREPROCESSING_TIMESTAMP) \
$(RUST_EXECUTION_TIMESTAMP) \
$(MX_TESTING_TIMESTAMP) \
$(MX_RUST_TIMESTAMP) \
$(MX_RUST_TESTING_TIMESTAMP)

test: syntax-test preprocessing-test execution-test mx-test
test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test

syntax-test: $(SYNTAX_OUTPUTS)

Expand All @@ -44,6 +60,8 @@ execution-test: $(EXECUTION_OUTPUTS)

mx-test: $(MX_TESTING_OUTPUTS)

mx-rust-test: $(MX_RUST_TESTING_OUTPUTS)

$(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
# Workaround for https://github.com/runtimeverification/k/issues/4141
-rm -r $(RUST_PREPROCESSING_KOMPILED)
Expand All @@ -59,6 +77,22 @@ $(MX_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES)
-rm -r $(MX_TESTING_KOMPILED)
$$(which kompile) mx-semantics/targets/testing/mx.md -o $(MX_TESTING_KOMPILED) --debug

$(MX_RUST_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES)
# Workaround for https://github.com/runtimeverification/k/issues/4141
-rm -r $(MX_RUST_KOMPILED)
$$(which kompile) mx-rust-semantics/targets/blockchain/mx-rust.md \
-o $(MX_RUST_KOMPILED) \
-I . \
--debug

$(MX_RUST_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES)
# Workaround for https://github.com/runtimeverification/k/issues/4141
-rm -r $(MX_RUST_TESTING_KOMPILED)
$$(which kompile) mx-rust-semantics/targets/testing/mx-rust.md \
-o $(MX_RUST_TESTING_KOMPILED) \
-I . \
--debug

$(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
mkdir -p $(RUST_SYNTAX_OUTPUT_DIR)
kast --definition $(RUST_PREPROCESSING_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@
Expand All @@ -75,7 +109,11 @@ $(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%

# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
# as a dependency
$(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: $(EXECUTION_INPUT_DIR)/%.run $(RUST_EXECUTION_TIMESTAMP)
$(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: \
$(EXECUTION_INPUT_DIR)/%.run \
$(RUST_EXECUTION_TIMESTAMP) \
parse-rust.sh \
parse-test.sh
mkdir -p $(EXECUTION_OUTPUT_DIR)
krun \
"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
Expand All @@ -97,3 +135,22 @@ $(MX_TESTING_OUTPUT_DIR)/%.mx.executed.kore: $(MX_TESTING_INPUT_DIR)/%.mx $(MX_T
--output-file $@.tmp
cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
mv -f $@.tmp $@

# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
# as a dependency
$(MX_RUST_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
$(MX_RUST_TESTING_INPUT_DIR)/%.run \
$(MX_RUST_TESTING_TIMESTAMP) \
parse-mx-rust.sh \
parse-mx-rust-test.sh
mkdir -p $(MX_RUST_TESTING_OUTPUT_DIR)
krun \
"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
--definition $(MX_RUST_TESTING_KOMPILED) \
--parser $(CURDIR)/parse-mx-rust.sh \
--output kore \
--output-file $@.tmp \
-cTEST='$(shell cat $<)' \
-pTEST=$(CURDIR)/parse-mx-rust-test.sh
cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
mv -f $@.tmp $@
17 changes: 17 additions & 0 deletions mx-rust-semantics/main/configuration.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
```k
requires "mx-semantics/main/configuration.md"
requires "rust-semantics/config.md"
module MX-RUST-COMMON-CONFIGURATION
imports MX-COMMON-CONFIGURATION
imports RUST-CONFIGURATION
configuration
<mx-rust>
<mx-common/>
<rust/>
</mx-rust>
endmodule
```
9 changes: 9 additions & 0 deletions mx-rust-semantics/main/expression.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
```k
requires "expression/strings.md"
module MX-RUST-EXPRESSION
imports private MX-RUST-EXPRESSION-STRINGS
endmodule
```
34 changes: 34 additions & 0 deletions mx-rust-semantics/main/expression/strings.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
```k
module MX-RUST-EXPRESSION-STRINGS
imports private BOOL
imports private INT
imports private MX-RUST-REPRESENTATION
imports private RUST-VALUE-SYNTAX
imports private STRING
rule concatString(ptrValue(_, S1:String), ptrValue(_, S2:String))
=> ptrValue(null, S1 +String S2)
rule toString(ptrValue(_, i32(Value:MInt{32})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 32 divInt 4))
rule toString(ptrValue(_, u32(Value:MInt{32})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 32 divInt 4))
rule toString(ptrValue(_, i64(Value:MInt{64})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 64 divInt 4))
rule toString(ptrValue(_, u64(Value:MInt{64})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 64 divInt 4))
rule toString(ptrValue(_, u128(Value:MInt{128})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 128 divInt 4))
rule toString(ptrValue(null, Value:String)) => ptrValue(null, Value)
// TODO: convert all Value entries to string
syntax String ::= padLeftString(value:String, padding:String, count:Int) [function, total]
rule padLeftString(...value:S, padding:P, count:C) => S
requires C <=Int lengthString(S) orBool lengthString(P) =/=Int 1
rule padLeftString(S:String => P +String S, P:String, _Count:Int)
[owise]
endmodule
```
50 changes: 50 additions & 0 deletions mx-rust-semantics/main/glue.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
```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>
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)
=> mxRustNewValue(integerToValue(I, T))
endmodule
```
11 changes: 11 additions & 0 deletions mx-rust-semantics/main/modules.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
```k
requires "modules/biguint.md"
requires "modules/storage.md"
module MX-RUST-MODULES
imports private MX-RUST-MODULES-BIGUINT
imports private MX-RUST-MODULES-STORAGE
endmodule
```
48 changes: 48 additions & 0 deletions mx-rust-semantics/main/modules/biguint.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
```k
module MX-RUST-MODULES-BIGUINT
imports private COMMON-K-CELL
imports private MX-COMMON-SYNTAX
imports private MX-RUST-REPRESENTATION
imports private RUST-EXECUTION-CONFIGURATION
imports private RUST-REPRESENTATION
imports private RUST-SHARED-SYNTAX
rule
<k>
normalizedMethodCall
( #token("BigUint", "Identifier"):Identifier
, #token("from", "Identifier"):Identifier
, ( ptr(ValueId:Int)
, .NormalizedCallParams
)
)
// TODO: Should check that V >= 0
=> mxRustBigIntNew(valueToInteger(V))
...
</k>
<values> ValueId |-> V:Value ... </values>
// --------------------------------------
syntax MxRustInstruction ::= mxRustBigIntNew(IntOrError)
| "mxRustCreateBigUint"
rule mxRustBigIntNew(V:Int)
=> MX#bigIntNew(mxIntValue(V))
~> mxValueToRust(i32)
~> mxRustCreateBigUint
rule ptrValue(ptr(BigUintId:Int), _) ~> mxRustCreateBigUint
=> mxRustNewValue
( struct
( #token("BigUint", "Identifier"):Identifier
, #token("mx_biguint_id", "Identifier"):Identifier |-> BigUintId
)
)
rule mxRustEmptyValue(BigUint) => mxRustBigIntNew(0)
endmodule
```
113 changes: 113 additions & 0 deletions mx-rust-semantics/main/modules/storage.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,113 @@
```k
module MX-RUST-MODULES-STORAGE
imports private COMMON-K-CELL
imports private MX-COMMON-SYNTAX
imports private MX-RUST-REPRESENTATION
imports private RUST-EXECUTION-CONFIGURATION
imports private RUST-REPRESENTATION
imports private RUST-SHARED-SYNTAX
rule
normalizedMethodCall
( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
, #token("new", "Identifier"):Identifier
, ( ptr(KeyId:Int)
, ptr(ResultTypeId:Int)
, .NormalizedCallParams
)
)
=> mxRustNewValue
( struct
( Type
, #token("storage_key", "Identifier"):Identifier |-> KeyId
#token("result_type", "Identifier"):Identifier |-> ResultTypeId
)
)
rule
<k>
normalizedMethodCall
( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
, #token("set", "Identifier"):Identifier
, ( ptr(SelfId:Int)
, ptr(ValueId:Int)
, .NormalizedCallParams
)
)
=> MX#storageStore(mxStringValue(StorageKey), wrappedRust(V))
...
</k>
<values>
SelfId |-> struct
( Type
, #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int
_:Map
)
StorageKeyId |-> StorageKey:String
ValueId |-> V:Value
...
</values>
rule
<k>
normalizedMethodCall
( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
, #token("set_if_empty", "Identifier"):Identifier
, ( ptr(SelfId:Int)
, ptr(ValueId:Int)
, .NormalizedCallParams
)
)
=> MX#storageLoad(mxStringValue(StorageKey), rustDestination(-1, noType))
~> setIfEmpty
~> MX#storageStore(mxStringValue(StorageKey), wrappedRust(V))
...
</k>
<values>
SelfId |-> struct
( Type
, #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int
_:Map
)
StorageKeyId |-> StorageKey:String
ValueId |-> V:Value
...
</values>
rule mxRustEmptyValue(noType) ~> storeHostValue(...) ~> setIfEmpty
=> .K
rule storeHostValue(... value: wrappedRust(_))
~> setIfEmpty ~> MX#storageStore(_)
=> .K
rule
<k>
normalizedMethodCall
( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
, #token("get", "Identifier"):Identifier
, ( ptr(SelfId:Int)
, .NormalizedCallParams
)
)
=> MX#storageLoad(mxStringValue(StorageKey), rustDestination(NextId, ResultType))
~> mxRustLoadPtr(NextId)
...
</k>
<values>
SelfId |-> struct
( Type
, #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int
#token("result_type", "Identifier"):Identifier |-> ResultTypeId:Int
_:Map
)
StorageKeyId |-> StorageKey:String
ResultTypeId |-> ResultType:MxRustType
...
</values>
<next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
syntax MxRustInstruction ::= "setIfEmpty"
endmodule
```
Loading

0 comments on commit b62f09a

Please sign in to comment.