Erc20 demo (#114)

* Run the erc20 contract * More int types
Pi-Squared-Inc · Oct 2, 2024 · ec9ef92 · ec9ef92
1 parent a0c040b
commit ec9ef92
Show file tree

Hide file tree

Showing 22 changed files with 599 additions and 52 deletions.
diff --git a/Makefile b/Makefile
@@ -52,7 +52,16 @@ MX_RUST_TWO_CONTRACTS_TESTING_OUTPUT_DIR ::= .build/mx-rust-two-contracts/output
 MX_RUST_TWO_CONTRACTS_TESTING_INPUTS ::= $(wildcard $(MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR)/*.run)
 MX_RUST_TWO_CONTRACTS_TESTING_OUTPUTS ::= $(patsubst $(MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR)/%,$(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_RUST_TWO_CONTRACTS_TESTING_INPUTS))
 
-.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test
+DEMOS_TESTING_KOMPILED ::= $(MX_RUST_CONTRACT_TESTING_KOMPILED)
+DEMOS_TESTING_TIMESTAMP ::= $(DEMOS_TESTING_KOMPILED)/timestamp
+DEMOS_TESTING_INPUT_DIR ::= tests/demos
+DEMOS_TESTING_OUTPUT_DIR ::= .build/demos/output
+DEMOS_TESTING_INPUTS ::= $(wildcard $(DEMOS_TESTING_INPUT_DIR)/*.run)
+DEMOS_TESTING_OUTPUTS ::= $(patsubst $(DEMOS_TESTING_INPUT_DIR)/%,$(DEMOS_TESTING_OUTPUT_DIR)/%.executed.kore,$(DEMOS_TESTING_INPUTS))
+
+.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
+
+all: build test
 
 clean:
 	rm -r .build
@@ -65,7 +74,7 @@ build: $(RUST_PREPROCESSING_TIMESTAMP) \
 				$(MX_RUST_CONTRACT_TESTING_TIMESTAMP) \
 				$(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP)
 
-test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test
+test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
 
 syntax-test: $(SYNTAX_OUTPUTS)
 
@@ -81,6 +90,8 @@ mx-rust-contract-test: $(MX_RUST_CONTRACT_TESTING_OUTPUTS)
 
 mx-rust-two-contracts-test: $(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUTS)
 
+demos-test: $(DEMOS_TESTING_OUTPUTS)
+
 $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(RUST_PREPROCESSING_KOMPILED)
@@ -242,3 +253,27 @@ $(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 		-pARGS2=$(CURDIR)/parsers/args-mx-rust-two-contracts.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
+
+
+# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
+# as a dependency
+$(DEMOS_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
+			$(DEMOS_TESTING_INPUT_DIR)/%.run \
+			$(DEMOS_TESTING_TIMESTAMP) \
+			$(wildcard parsers/inc-*.sh) \
+			parsers/args-mx-rust-contract.sh \
+			parsers/contract-mx-rust-contract.sh \
+			parsers/test-mx-rust-contract.sh
+	mkdir -p $(DEMOS_TESTING_OUTPUT_DIR)
+	krun \
+		"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
+		--definition $(DEMOS_TESTING_KOMPILED) \
+		--parser $(CURDIR)/parsers/contract-mx-rust-contract.sh \
+		--output kore \
+		--output-file $@.tmp \
+		-cTEST='$(shell cat $<)' \
+		-pTEST=$(CURDIR)/parsers/test-mx-rust-contract.sh \
+		-cARGS='$(shell cat $(patsubst %.run,%.args,$<))' \
+		-pARGS=$(CURDIR)/parsers/args-mx-rust-contract.sh
+	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f $@.tmp $@
diff --git a/mx-rust-semantics/main/expression/mx-to-rust.md b/mx-rust-semantics/main/expression/mx-to-rust.md
@@ -33,7 +33,9 @@ module MX-RUST-EXPRESSION-MX-TO-RUST
 
     rule mxToRustTyped(T:Type, mxIntValue(I:Int)) => mxRustNewValue(integerToValue(I, T))
         requires
-            (T ==K i32 orBool T ==K u32)
+            (T ==K i8 orBool T ==K u8)
+            orBool (T ==K i16 orBool T ==K u16)
+            orBool (T ==K i32 orBool T ==K u32)
             orBool (T ==K i64 orBool T ==K u64)
     rule mxToRustTyped(str, mxStringValue(S:String)) => mxRustNewValue(S)
     rule mxToRustTyped

diff --git a/mx-rust-semantics/main/expression/strings.md b/mx-rust-semantics/main/expression/strings.md
@@ -10,6 +10,14 @@ module MX-RUST-EXPRESSION-STRINGS
     rule concatString(ptrValue(_, S1:String), ptrValue(_, S2:String))
           => ptrValue(null, S1 +String S2)
 
+    rule toString(ptrValue(_, i8(Value:MInt{8})))
+        => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 8 divInt 4))
+    rule toString(ptrValue(_, u8(Value:MInt{8})))
+        => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 8 divInt 4))
+    rule toString(ptrValue(_, i16(Value:MInt{16})))
+        => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 16 divInt 4))
+    rule toString(ptrValue(_, u16(Value:MInt{16})))
+        => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 16 divInt 4))
     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})))
@@ -20,7 +28,7 @@ module MX-RUST-EXPRESSION-STRINGS
         => 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)
+    rule toString(ptrValue(_, Value:String)) => ptrValue(null, Value)
     // TODO: convert all Value entries to string
 
     syntax String ::= padLeftString(value:String, padding:String, count:Int)  [function, total]

diff --git a/mx-rust-semantics/main/glue.md b/mx-rust-semantics/main/glue.md
@@ -55,7 +55,9 @@ module MX-RUST-GLUE
     rule mxValueToRust(T:Type, mxIntValue(I:Int))
         => mxRustNewValue(integerToValue(I, T))
         requires
-            (T ==K i32 orBool T ==K u32)
+            (T ==K i8 orBool T ==K u8)
+            orBool (T ==K i16 orBool T ==K u16)
+            orBool (T ==K i32 orBool T ==K u32)
             orBool (T ==K i64 orBool T ==K u64)
 
     rule ptrValue(_, V) ~> rustValueToMx => rustValueToMx(V)
@@ -97,6 +99,10 @@ module MX-RUST-GLUE
     syntax MxRustInstruction ::= cloneValue(Expression)  [strict]
     // TODO: Figure out if we need to do a deeper clone for, e.g., structs
     rule cloneValue(ptrValue(_, V:Value)) => mxRustNewValue(V)
+
+    rule mxRustGetBuffer(ptrValue(_, i32(BufferId:MInt{32})))
+        => mxGetBuffer(MInt2Unsigned(BufferId))
+
 endmodule
 
 ```
diff --git a/mx-rust-semantics/main/modules.md b/mx-rust-semantics/main/modules.md
@@ -5,6 +5,7 @@ requires "modules/biguint.md"
 requires "modules/blockchain.md"
 requires "modules/call-value.md"
 requires "modules/hooks.md"
+requires "modules/managed-buffer.md"
 requires "modules/managed-vec.md"
 requires "modules/multi-value-encoded.md"
 requires "modules/proxy.md"
@@ -18,6 +19,7 @@ module MX-RUST-MODULES
     imports private MX-RUST-MODULES-BLOCKCHAIN
     imports private MX-RUST-MODULES-CALL-VALUE
     imports private MX-RUST-MODULES-HOOKS
+    imports private MX-RUST-MODULES-MANAGED-BUFFER
     imports private MX-RUST-MODULES-MANAGED-VEC
     imports private MX-RUST-MODULES-MULTI-VALUE-ENCODED
     imports private MX-RUST-MODULES-PROXY

diff --git a/mx-rust-semantics/main/modules/address.md b/mx-rust-semantics/main/modules/address.md
@@ -6,33 +6,58 @@ module MX-RUST-MODULES-ADDRESS
     imports private MX-RUST-REPRESENTATION-CONVERSIONS
     imports private RUST-SHARED-SYNTAX
 
+    syntax Identifier ::= "ManagedAddress"  [token]
+                        | "mx_address_value"  [token]
+
+    rule
+        normalizedMethodCall
+            ( ManagedAddress
+            , #token("zero", "Identifier"):Identifier
+            , ( .PtrList)
+            )
+        => mxRustEmptyValue(rustType(ManagedAddress))
+
+    rule
+        normalizedMethodCall
+            ( ManagedAddress
+            , #token("is_zero", "Identifier"):Identifier
+            , ( ptr(SelfId) , .PtrList)
+            )
+        => ptr(SelfId) . mx_address_value == ""
+
+  // --------------------------------------
+
     syntax MxRustType ::= "addressType"  [function, total]
     rule addressType
         => rustStructType
-            ( #token("ManagedAddress", "Identifier"):Identifier
+            ( ManagedAddress
             ,   ( mxRustStructField
-                    ( #token("mx_address_value", "Identifier"):Identifier
+                    ( mx_address_value
                     , str
                     )
                 , .MxRustStructFields
                 )
             )
 
-    rule mxRustEmptyValue(rustType(#token("ManagedAddress", "Identifier")))
+    rule mxRustEmptyValue(rustType(ManagedAddress))
         => mxToRustTyped(addressType, mxListValue(mxStringValue("")))
 
-    rule mxValueToRust(#token("ManagedAddress", "Identifier"), V:MxValue)
+    rule mxValueToRust(ManagedAddress, V:MxValue)
         => mxToRustTyped(addressType, mxListValue(V))
 
     rule rustValueToMx
             ( struct
-                ( #token("ManagedAddress", "Identifier"):Identifier
-                , #token("mx_address_value", "Identifier"):Identifier |-> AddressValueId:Int
+                ( ManagedAddress
+                , mx_address_value |-> AddressValueId:Int
                   .Map
                 )
             )
         => ptr(AddressValueId) ~> rustValueToMx
 
+  // --------------------------------------
+
+    rule toString(ptrValue(P:Ptr, struct(ManagedAddress, _:Map)))
+        => toString(P .  #token("mx_address_value", "Identifier"))
 endmodule
 
 ```
diff --git a/mx-rust-semantics/main/modules/managed-buffer.md b/mx-rust-semantics/main/modules/managed-buffer.md
@@ -0,0 +1,40 @@
+```k
+
+module MX-RUST-MODULES-MANAGED-BUFFER
+    imports private MX-RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+
+  // --------------------------------------
+
+    syntax MxRustType ::= "managedBufferType"  [function, total]
+    rule managedBufferType
+        => rustStructType
+            ( #token("ManagedBuffer", "Identifier"):Identifier
+            ,   ( mxRustStructField
+                    ( #token("mx_buffer_id", "Identifier"):Identifier
+                    , MxRust#buffer
+                    )
+                , .MxRustStructFields
+                )
+            )
+
+    rule mxValueToRust
+            ( #token("ManagedBuffer", "Identifier")
+            , V:MxValue
+            )
+        => mxToRustTyped(managedBufferType, mxListValue(V , .MxValueList))
+
+    rule rustValueToMx
+            ( struct
+                ( #token("ManagedBuffer", "Identifier"):Identifier
+                , #token("mx_buffer_id", "Identifier"):Identifier |-> VecValueId:Int
+                  .Map
+                )
+            )
+        => mxRustGetBuffer(ptr(VecValueId))
+
+  // --------------------------------------
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/modules/multi-value-encoded.md b/mx-rust-semantics/main/modules/multi-value-encoded.md
@@ -62,10 +62,6 @@ module MX-RUST-MODULES-MULTI-VALUE-ENCODED
             )
         => mxRustGetBuffer(ptr(VecValueId))
 
-    syntax MxRustInstruction ::= mxRustGetBuffer(Expression)  [strict]
-    rule mxRustGetBuffer(ptrValue(_, i32(BufferId:MInt{32})))
-        => mxGetBuffer(MInt2Unsigned(BufferId))
-
   // --------------------------------------
 
 endmodule

diff --git a/mx-rust-semantics/main/preprocessing/methods.md b/mx-rust-semantics/main/preprocessing/methods.md
@@ -244,6 +244,13 @@ module MX-RUST-PREPROCESSING-METHODS
                 _: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]
@@ -336,6 +343,8 @@ module MX-RUST-PREPROCESSING-METHODS
         [owise]
     rule getMapperValueType(#token("BigUint", "Identifier") #as T:Type)
         => rustType(T)
+    rule getMapperValueType(#token("ManagedBuffer", "Identifier") #as T:Type)
+        => rustType(T)
 
     syntax BlockExpression ::= buildProxyMethodBody
                                   ( selfName: SelfSort

diff --git a/mx-rust-semantics/main/representation.md b/mx-rust-semantics/main/representation.md
@@ -28,6 +28,7 @@ module MX-RUST-REPRESENTATION
                                 | mxRustLoadPtr(Int)
                                 | mxRustGetBigIntFromStruct(Value)
                                 | mxRustGetStringFromId(Int)
+                                | mxRustGetBuffer(Expression)  [strict]
                                 | mxRustNewStruct(MxRustStructType, CallParamsList)
                                   [strict(2), result(ValueWithPtr)]
                                 | "mxRustCheckMxStatus"

diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md
@@ -9,27 +9,83 @@ module RUST-CASTS
 
     // https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-implicitCast
 
+    rule implicitCast(i8(Value), i8 ) => i8 (Value)
+    rule implicitCast(i8(Value), u8 ) => u8 (Value)
+    rule implicitCast(i8(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i8(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i8(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(i8(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(i8(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(i8(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
+
+    rule implicitCast(u8(Value), i8 ) => i8 (Value)
+    rule implicitCast(u8(Value), u8 ) => u8 (Value)
+    rule implicitCast(u8(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u8(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u8(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u8(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u8(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u8(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
+
+    rule implicitCast(i16(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i16(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i16(Value), i16) => i16(Value)
+    rule implicitCast(i16(Value), u16) => u16(Value)
+    rule implicitCast(i16(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(i16(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(i16(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(i16(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
+
+    rule implicitCast(u16(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u16(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u16(Value), i16) => i16(Value)
+    rule implicitCast(u16(Value), u16) => u16(Value)
+    rule implicitCast(u16(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u16(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u16(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u16(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
+
+    rule implicitCast(i32(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i32(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i32(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i32(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
     rule implicitCast(i32(Value), i32) => i32(Value)
     rule implicitCast(i32(Value), u32) => u32(Value)
     rule implicitCast(i32(Value), i64) => i64(Int2MInt(MInt2Signed(Value)))
     rule implicitCast(i32(Value), u64) => u64(Int2MInt(MInt2Signed(Value)))
 
+    rule implicitCast(u32(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u32(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u32(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u32(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
     rule implicitCast(u32(Value), i32) => i32(Value)
     rule implicitCast(u32(Value), u32) => u32(Value)
     rule implicitCast(u32(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
     rule implicitCast(u32(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
 
 
+    rule implicitCast(i64(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i64(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i64(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i64(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
     rule implicitCast(i64(Value), i32) => i32(Int2MInt(MInt2Signed(Value)))
     rule implicitCast(i64(Value), u32) => u32(Int2MInt(MInt2Signed(Value)))
     rule implicitCast(i64(Value), i64) => i64(Value)
     rule implicitCast(i64(Value), u64) => u64(Value)
 
+    rule implicitCast(u64(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u64(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u64(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u64(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
     rule implicitCast(u64(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
     rule implicitCast(u64(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
     rule implicitCast(u64(Value), i64) => i64(Value)
     rule implicitCast(u64(Value), u64) => u64(Value)
 
+    rule implicitCast(u128(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u128(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u128(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(u128(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
     rule implicitCast(u128(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
     rule implicitCast(u128(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
     rule implicitCast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))