Int relational operators

rust-semantics/expression.md

@@ -1,4 +1,5 @@
 ```k
+requires "expression/integer-operations.md"
 requires "expression/constants.md"
 requires "expression/casts.md"
 requires "expression/literals.md"
@@ -9,5 +10,6 @@ module RUST-EXPRESSION
     imports private RUST-EXPRESSION-LITERALS
     imports private RUST-EXPRESSION-VARIABLES
     imports private RUST-EXPRESSION-CONSTANTS
+    imports private RUST-INTEGER-OPERATIONS
 endmodule
 ```

rust-semantics/expression/casts.md

@@ -36,6 +36,8 @@ module RUST-CASTS
     rule implicitCast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
     rule implicitCast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
 
+    rule implicitCast(V:Bool, bool) => V
+
     // Rewrites
 
     rule V:Value ~> implicitCastTo(T:Type) => implicitCast(V, T)

rust-semantics/expression/integer-operations.md

@@ -0,0 +1,91 @@
+```k
+
+module RUST-INTEGER-OPERATIONS
+    imports private RUST-INTEGER-ARITHMETIC-OPERATIONS
+    imports private RUST-INTEGER-RELATIONAL-OPERATIONS
+endmodule
+
+module RUST-INTEGER-ARITHMETIC-OPERATIONS
+    imports RUST-SHARED-SYNTAX
+    imports private RUST-REPRESENTATION
+
+    // Operations are implemented only for the same types, 
+    // as implicit type casting (coercion) is not available
+    // in Rust.
+
+    rule i32(A):Value * i32(B):Value => i32(A *MInt B)
+    rule i32(A):Value + i32(B):Value => i32(A +MInt B)
+    rule i32(A):Value - i32(B):Value => i32(A -MInt B)
+    rule i32(A):Value / i32(B):Value => i32(A /sMInt B)
+    rule i32(A):Value % i32(B):Value => i32(A %sMInt B)
+
+    rule u32(A):Value * u32(B):Value => u32(A *MInt B)
+    rule u32(A):Value + u32(B):Value => u32(A +MInt B)
+    rule u32(A):Value - u32(B):Value => u32(A -MInt B)
+    rule u32(A):Value / u32(B):Value => u32(A /uMInt B)
+    rule u32(A):Value % u32(B):Value => u32(A %uMInt B)
+
+    rule i64(A):Value * i64(B):Value => i64(A *MInt B)
+    rule i64(A):Value + i64(B):Value => i64(A +MInt B)
+    rule i64(A):Value - i64(B):Value => i64(A -MInt B)
+    rule i64(A):Value / i64(B):Value => i64(A /sMInt B)
+    rule i64(A):Value % i64(B):Value => i64(A %sMInt B)
+
+    rule u64(A):Value * u64(B):Value => u64(A *MInt B)
+    rule u64(A):Value + u64(B):Value => u64(A +MInt B)
+    rule u64(A):Value - u64(B):Value => u64(A -MInt B)
+    rule u64(A):Value / u64(B):Value => u64(A /uMInt B)
+    rule u64(A):Value % u64(B):Value => u64(A %uMInt B)
+
+    rule u128(A):Value * u128(B):Value => u128(A *MInt B)
+    rule u128(A):Value + u128(B):Value => u128(A +MInt B)
+    rule u128(A):Value - u128(B):Value => u128(A -MInt B)
+    rule u128(A):Value / u128(B):Value => u128(A /uMInt B)
+    rule u128(A):Value % u128(B):Value => u128(A %uMInt B)
+
+
+endmodule
+
+
+module RUST-INTEGER-RELATIONAL-OPERATIONS
+    imports RUST-SHARED-SYNTAX
+    imports private RUST-REPRESENTATION
+
+    rule i32(A):Value == i32(B):Value => A ==MInt B
+    rule i32(A):Value != i32(B):Value => A =/=MInt B
+    rule i32(A):Value > i32(B):Value  => A >sMInt B
+    rule i32(A):Value < i32(B):Value  => A <sMInt B
+    rule i32(A):Value >= i32(B):Value => A >=sMInt B
+    rule i32(A):Value <= i32(B):Value => A <=sMInt B
+
+    rule u32(A):Value == u32(B):Value => A ==MInt B
+    rule u32(A):Value != u32(B):Value => A =/=MInt B
+    rule u32(A):Value > u32(B):Value  => A >uMInt B
+    rule u32(A):Value < u32(B):Value  => A <uMInt B
+    rule u32(A):Value >= u32(B):Value => A >=uMInt B
+    rule u32(A):Value <= u32(B):Value => A <=uMInt B
+
+    rule i64(A):Value == i64(B):Value => A ==MInt B
+    rule i64(A):Value != i64(B):Value => A =/=MInt B
+    rule i64(A):Value > i64(B):Value  => A >sMInt B
+    rule i64(A):Value < i64(B):Value  => A <sMInt B
+    rule i64(A):Value >= i64(B):Value => A >=sMInt B
+    rule i64(A):Value <= i64(B):Value => A <=sMInt B
+
+    rule u64(A):Value == u64(B):Value => A ==MInt B
+    rule u64(A):Value != u64(B):Value => A =/=MInt B
+    rule u64(A):Value > u64(B):Value  => A >uMInt B
+    rule u64(A):Value < u64(B):Value  => A <uMInt B
+    rule u64(A):Value >= u64(B):Value => A >=uMInt B
+    rule u64(A):Value <= u64(B):Value => A <=uMInt B
+
+    rule u128(A):Value == u128(B):Value => A ==MInt B
+    rule u128(A):Value != u128(B):Value => A =/=MInt B
+    rule u128(A):Value > u128(B):Value  => A >uMInt B
+    rule u128(A):Value < u128(B):Value  => A <uMInt B
+    rule u128(A):Value >= u128(B):Value => A >=uMInt B
+    rule u128(A):Value <= u128(B):Value => A <=uMInt B
+
+endmodule
+
+```

rust-semantics/expression/literals.md

@@ -94,4 +94,5 @@ module RUST-EXPRESSION-INTEGER-LITERALS
     rule startsWith(_, _) => false [owise]
 
 endmodule
+
 ```

rust-semantics/preprocessing.md

@@ -1,6 +1,5 @@
 ```k
 
-requires "preprocessing/arithmetic-operations.md"
 requires "preprocessing/constants.md"
 requires "preprocessing/crate.md"
 requires "preprocessing/configuration.md"
@@ -16,7 +15,6 @@ module RUST-PREPROCESSING
     imports private INITIALIZATION
     imports private TRAIT
     imports private TRAIT-METHODS
-    imports private RUST-INTEGER-ARITHMETIC-OPERATIONS
 endmodule
 
 ```

rust-semantics/preprocessing/constants.md

@@ -10,7 +10,11 @@ module RUST-CONSTANTS
 
     rule
         (const Name:Identifier : T:Type = V:Value;):ConstantItem:KItem
-        => setConstant(Name, implicitCast(V, T))
+        => setConstant(Name, implicitCast(V, T)) 
+
+    // rule
+    //     (const Name:Identifier : _:Type = V:Bool;):ConstantItem:KItem
+    //     => setConstant(Name, V) [priority(50)]
 
     rule
         <k>
@@ -23,6 +27,8 @@ module RUST-CONSTANTS
                 <constant-value> V </constant-value>
             </constant>
             ...
-        </constants>
+        </constants> 
+
+
 endmodule
 ```

rust-semantics/representation.md

@@ -23,6 +23,7 @@ module RUST-VALUE-SYNTAX
                     | u128(MInt{128})
                     | tuple(ValueList)
                     | struct(TypePath, Map)  // Map from field name (Identifier) to value ID (Int)
+                    | Bool
 
     syntax ValueList ::= List{Value, ","}
     syntax Expression ::= Value
@@ -58,6 +59,8 @@ module RUST-REPRESENTATION
                         | "u32"  [token]
                         | "i64"  [token]
                         | "u64"  [token]
+                        | "bool" [token]
+
     syntax MaybeIdentifier ::= ".Identifier" | Identifier
 
 endmodule

rust-semantics/rust-common-syntax.md

@@ -257,8 +257,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
                               | ByteLiteral | ByteStringLiteral | RawByteStringLiteral
                               | CStringLiteral | RawCStringLiteral
                               | IntegerLiteral | FloatLiteral
-                              | "true" | "false"
-
+
   syntax CharLiteral ::= "TODO: not needed yet, not implementing"
   // TODO: Not implemented properly
   syntax StringLiteral ::= String
@@ -372,12 +371,12 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
                       | Expression "^" Expression
                       | Expression "|" Expression
 
-                      > Expression "==" Expression
-                      | Expression "!=" Expression
-                      | Expression ">" Expression
-                      | Expression "<" Expression
-                      | Expression ">=" Expression
-                      | Expression "<=" Expression
+                      > Expression "==" Expression [seqstrict]
+                      | Expression "!=" Expression [seqstrict]
+                      | Expression ">" Expression [seqstrict]
+                      | Expression "<" Expression [seqstrict]
+                      | Expression ">=" Expression [seqstrict]
+                      | Expression "<=" Expression [seqstrict]
 
                       > left:
                         Expression "&&" Expression

rust-semantics/targets/preprocessing/rust.md

@@ -7,13 +7,15 @@ requires "../../expression/casts.md"
 requires "../../expression/constants.md"
 requires "../../expression/literals.md"
 requires "../../rust-common-syntax.md"
+requires "../../expression/integer-operations.md"
 
 module RUST-SYNTAX
     imports RUST-COMMON-SYNTAX
 endmodule
 
 module RUST
     imports private RUST-EXPRESSION-LITERALS
+    imports private RUST-INTEGER-OPERATIONS
     imports private RUST-EXPRESSION-CONSTANTS
     imports private RUST-PREPROCESSING
     imports private RUST-RUNNING-CONFIGURATION

tests/execution/integer-operations.1.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.arithmetic_expression_mult_constant;
+return_value;
+check_eq 86400_u64

tests/execution/integer-operations.10.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.relational_expression_smaller;
+return_value;
+check_eq true

tests/execution/integer-operations.11.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.relational_expression_greater;
+return_value;
+check_eq false

tests/execution/integer-operations.2.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.arithmetic_expression_div_constant;
+return_value;
+check_eq 2_u64

tests/execution/integer-operations.3.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.arithmetic_expression_sum_constant;
+return_value;
+check_eq 101_u64

tests/execution/integer-operations.4.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.arithmetic_expression_sub_constant;
+return_value;
+check_eq 99_u64

tests/execution/integer-operations.5.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.arithmetic_expression_mod_constant;
+return_value;
+check_eq 2_u64

tests/execution/integer-operations.6.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.relational_expression_equals;
+return_value;
+check_eq true

tests/execution/integer-operations.7.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.relational_expression_diff;
+return_value;
+check_eq false

tests/execution/integer-operations.8.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.relational_expression_smaller_or_equal;
+return_value;
+check_eq true

tests/execution/integer-operations.9.run

@@ -0,0 +1,4 @@
+new IntegerOperations;
+call IntegerOperations.relational_expression_greater_or_equal;
+return_value;
+check_eq true

tests/execution/arithmetic-expression.rs → tests/execution/integer-operations.rs

@@ -4,7 +4,7 @@
 use multiversx_sc::imports::*;
 
 #[multiversx_sc::contract]
-pub trait ArithmeticExpression {
+pub trait IntegerOperations {
     #[init]
     fn init(&self) {
     }
@@ -22,4 +22,16 @@ pub trait ArithmeticExpression {
 
     fn arithmetic_expression_mod_constant(&self) -> u64 { 5_u64 % 3_u64 }
 
+    fn relational_expression_equals(&self) -> bool { 5_u64 == 5_u64 }
+
+    fn relational_expression_diff(&self) -> bool { 5_i64 != 5_i64 }
+
+    fn relational_expression_smaller_or_equal(&self) -> bool { 5 >= 5 }
+
+    fn relational_expression_greater_or_equal(&self) -> bool { 70 >= 7 }
+
+    fn relational_expression_smaller(&self) -> bool { 5_u32 < 7_u32 }
+
+    fn relational_expression_greater(&self) -> bool { 5_i32 > 7_i32 }
+
 }