For and While Loops

rust-semantics/expression.md

@@ -6,6 +6,7 @@ requires "expression/calls.md"
 requires "expression/constants.md"
 requires "expression/casts.md"
 requires "expression/conditionals.md"
+requires "expression/loops.md"
 requires "expression/expression-list.md"
 requires "expression/integer-operations.md"
 requires "expression/literals.md"
@@ -18,6 +19,7 @@ module RUST-EXPRESSION
     imports private RUST-CASTS
     imports private RUST-BLOCK-EXPRESSIONS
     imports private RUST-CONDITIONAL-EXPRESSIONS
+    imports private RUST-LOOP-EXPRESSIONS
     imports private RUST-EXPRESSION-ASSIGNMENTS
     imports private RUST-EXPRESSION-CALLS
     imports private RUST-EXPRESSION-CONSTANTS

rust-semantics/expression/integer-operations.md

@@ -3,6 +3,7 @@
 module RUST-INTEGER-OPERATIONS
     imports private RUST-INTEGER-ARITHMETIC-OPERATIONS
     imports private RUST-INTEGER-RELATIONAL-OPERATIONS
+    imports private RUST-INTEGER-RANGE-OPERATIONS
 endmodule
 
 module RUST-INTEGER-ARITHMETIC-OPERATIONS
@@ -50,40 +51,53 @@ module RUST-INTEGER-RELATIONAL-OPERATIONS
     imports RUST-SHARED-SYNTAX
     imports private RUST-REPRESENTATION
 
-    rule ptrValue(null, i32(A):Value)  == ptrValue(null, i32(B):Value)  => ptrValue(null, A ==MInt  B)
-    rule ptrValue(null, i32(A):Value)  != ptrValue(null, i32(B):Value)  => ptrValue(null, A =/=MInt B)
-    rule ptrValue(null, i32(A):Value)  >  ptrValue(null, i32(B):Value)  => ptrValue(null, A >sMInt  B)
-    rule ptrValue(null, i32(A):Value)  <  ptrValue(null, i32(B):Value)  => ptrValue(null, A <sMInt  B)
-    rule ptrValue(null, i32(A):Value)  >= ptrValue(null, i32(B):Value)  => ptrValue(null, A >=sMInt B)
-    rule ptrValue(null, i32(A):Value)  <= ptrValue(null, i32(B):Value)  => ptrValue(null, A <=sMInt B)
-
-    rule ptrValue(null, u32(A):Value) == ptrValue(null, u32(B):Value)  => ptrValue(null, A ==MInt B)
-    rule ptrValue(null, u32(A):Value) != ptrValue(null, u32(B):Value)  => ptrValue(null, A =/=MInt B)
-    rule ptrValue(null, u32(A):Value) > ptrValue(null, u32(B):Value)  => ptrValue(null, A >uMInt B)
-    rule ptrValue(null, u32(A):Value) < ptrValue(null, u32(B):Value)  => ptrValue(null, A <uMInt B)
-    rule ptrValue(null, u32(A):Value) >= ptrValue(null, u32(B):Value)  => ptrValue(null, A >=uMInt B)
-    rule ptrValue(null, u32(A):Value) <= ptrValue(null, u32(B):Value)  => ptrValue(null, A <=uMInt B)
-
-    rule ptrValue(null, i64(A):Value)  == ptrValue(null, i64(B):Value)  => ptrValue(null, A ==MInt  B)
-    rule ptrValue(null, i64(A):Value)  != ptrValue(null, i64(B):Value)  => ptrValue(null, A =/=MInt B)
-    rule ptrValue(null, i64(A):Value)  >  ptrValue(null, i64(B):Value)  => ptrValue(null, A >sMInt  B)
-    rule ptrValue(null, i64(A):Value)  <  ptrValue(null, i64(B):Value)  => ptrValue(null, A <sMInt  B)
-    rule ptrValue(null, i64(A):Value)  >= ptrValue(null, i64(B):Value)  => ptrValue(null, A >=sMInt B)
-    rule ptrValue(null, i64(A):Value)  <= ptrValue(null, i64(B):Value)  => ptrValue(null, A <=sMInt B)
-
-    rule ptrValue(null, u64(A):Value)  == ptrValue(null, u64(B):Value)  => ptrValue(null, A ==MInt  B)
-    rule ptrValue(null, u64(A):Value)  != ptrValue(null, u64(B):Value)  => ptrValue(null, A =/=MInt B)
-    rule ptrValue(null, u64(A):Value)  >  ptrValue(null, u64(B):Value)  => ptrValue(null, A >uMInt  B)
-    rule ptrValue(null, u64(A):Value)  <  ptrValue(null, u64(B):Value)  => ptrValue(null, A <uMInt  B)
-    rule ptrValue(null, u64(A):Value)  >= ptrValue(null, u64(B):Value)  => ptrValue(null, A >=uMInt B)
-    rule ptrValue(null, u64(A):Value)  <= ptrValue(null, u64(B):Value)  => ptrValue(null, A <=uMInt B)
-
-    rule ptrValue(null, u128(A):Value) == ptrValue(null, u128(B):Value) => ptrValue(null, A ==MInt  B)
-    rule ptrValue(null, u128(A):Value) != ptrValue(null, u128(B):Value) => ptrValue(null, A =/=MInt B)
-    rule ptrValue(null, u128(A):Value) >  ptrValue(null, u128(B):Value) => ptrValue(null, A >uMInt  B)
-    rule ptrValue(null, u128(A):Value) <  ptrValue(null, u128(B):Value) => ptrValue(null, A <uMInt  B)
-    rule ptrValue(null, u128(A):Value) >= ptrValue(null, u128(B):Value) => ptrValue(null, A >=uMInt B)
-    rule ptrValue(null, u128(A):Value) <= ptrValue(null, u128(B):Value) => ptrValue(null, A <=uMInt B)
+    rule ptrValue(_, i32(A):Value)  == ptrValue(_, i32(B):Value)  => ptrValue(null, A ==MInt  B)
+    rule ptrValue(_, i32(A):Value)  != ptrValue(_, i32(B):Value)  => ptrValue(null, A =/=MInt B)
+    rule ptrValue(_, i32(A):Value)  >  ptrValue(_, i32(B):Value)  => ptrValue(null, A >sMInt  B)
+    rule ptrValue(_, i32(A):Value)  <  ptrValue(_, i32(B):Value)  => ptrValue(null, A <sMInt  B)
+    rule ptrValue(_, i32(A):Value)  >= ptrValue(_, i32(B):Value)  => ptrValue(null, A >=sMInt B)
+    rule ptrValue(_, i32(A):Value)  <= ptrValue(_, i32(B):Value)  => ptrValue(null, A <=sMInt B)
+
+    rule ptrValue(_, u32(A):Value) == ptrValue(_, u32(B):Value)  => ptrValue(null, A ==MInt B)
+    rule ptrValue(_, u32(A):Value) != ptrValue(_, u32(B):Value)  => ptrValue(null, A =/=MInt B)
+    rule ptrValue(_, u32(A):Value) > ptrValue(_, u32(B):Value)  => ptrValue(null, A >uMInt B)
+    rule ptrValue(_, u32(A):Value) < ptrValue(_, u32(B):Value)  => ptrValue(null, A <uMInt B)
+    rule ptrValue(_, u32(A):Value) >= ptrValue(_, u32(B):Value)  => ptrValue(null, A >=uMInt B)
+    rule ptrValue(_, u32(A):Value) <= ptrValue(_, u32(B):Value)  => ptrValue(null, A <=uMInt B)
+
+    rule ptrValue(_, i64(A):Value)  == ptrValue(_, i64(B):Value)  => ptrValue(null, A ==MInt  B)
+    rule ptrValue(_, i64(A):Value)  != ptrValue(_, i64(B):Value)  => ptrValue(null, A =/=MInt B)
+    rule ptrValue(_, i64(A):Value)  >  ptrValue(_, i64(B):Value)  => ptrValue(null, A >sMInt  B)
+    rule ptrValue(_, i64(A):Value)  <  ptrValue(_, i64(B):Value)  => ptrValue(null, A <sMInt  B)
+    rule ptrValue(_, i64(A):Value)  >= ptrValue(_, i64(B):Value)  => ptrValue(null, A >=sMInt B)
+    rule ptrValue(_, i64(A):Value)  <= ptrValue(_, i64(B):Value)  => ptrValue(null, A <=sMInt B)
+
+    rule ptrValue(_, u64(A):Value)  == ptrValue(_, u64(B):Value)  => ptrValue(null, A ==MInt  B)
+    rule ptrValue(_, u64(A):Value)  != ptrValue(_, u64(B):Value)  => ptrValue(null, A =/=MInt B)
+    rule ptrValue(_, u64(A):Value)  >  ptrValue(_, u64(B):Value)  => ptrValue(null, A >uMInt  B)
+    rule ptrValue(_, u64(A):Value)  <  ptrValue(_, u64(B):Value)  => ptrValue(null, A <uMInt  B)
+    rule ptrValue(_, u64(A):Value)  >= ptrValue(_, u64(B):Value)  => ptrValue(null, A >=uMInt B)
+    rule ptrValue(_, u64(A):Value)  <= ptrValue(_, u64(B):Value)  => ptrValue(null, A <=uMInt B)
+
+    rule ptrValue(_, u128(A):Value) == ptrValue(_, u128(B):Value) => ptrValue(null, A ==MInt  B)
+    rule ptrValue(_, u128(A):Value) != ptrValue(_, u128(B):Value) => ptrValue(null, A =/=MInt B)
+    rule ptrValue(_, u128(A):Value) >  ptrValue(_, u128(B):Value) => ptrValue(null, A >uMInt  B)
+    rule ptrValue(_, u128(A):Value) <  ptrValue(_, u128(B):Value) => ptrValue(null, A <uMInt  B)
+    rule ptrValue(_, u128(A):Value) >= ptrValue(_, u128(B):Value) => ptrValue(null, A >=uMInt B)
+    rule ptrValue(_, u128(A):Value) <= ptrValue(_, u128(B):Value) => ptrValue(null, A <=uMInt B)
+
+endmodule
+
+
+module RUST-INTEGER-RANGE-OPERATIONS
+    imports RUST-SHARED-SYNTAX
+    imports private RUST-REPRESENTATION
+
+    rule (ptrValue(_, i32(A):Value) .. ptrValue(_, i32(B):Value)):Expression => ptrValue(null, intRange(i32(A), i32(B)))
+    rule (ptrValue(_, u32(A):Value) .. ptrValue(_, u32(B):Value)):Expression => ptrValue(null, intRange(u32(A), u32(B)))
+    rule (ptrValue(_, i64(A):Value) .. ptrValue(_, i64(B):Value)):Expression => ptrValue(null, intRange(i64(A), i64(B)))
+    rule (ptrValue(_, u64(A):Value) .. ptrValue(_, u64(B):Value)):Expression => ptrValue(null, intRange(u64(A), u64(B)))
+    rule (ptrValue(_, u128(A):Value) .. ptrValue(_, u128(B):Value)):Expression => ptrValue(null, intRange(u128(A), u128(B)))
 
 endmodule
 

rust-semantics/expression/loops.md

@@ -0,0 +1,52 @@
+```k
+
+module RUST-LOOP-EXPRESSIONS
+    imports RUST-REPRESENTATION
+
+    syntax IteratorLoopExpression ::=  "for1" Pattern "limit" PtrValue BlockExpression
+                                    | "for2" Pattern "limit" PtrValue BlockExpression
+
+    rule for Patt:Identifier:PatternNoTopAlt | R:PatternNoTopAlts in ptrValue(_, intRange(First, Last)) B:BlockExpression => 
+            {
+                .InnerAttributes
+                let Patt = ptrValue(null, First);
+                (for1 Patt | R limit ptrValue(null, Last) B):IteratorLoopExpression; 
+                .NonEmptyStatements
+            };
+        requires checkIntOfSameType(First, Last)
+
+    rule for1 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit Last B:BlockExpression => 
+        if (Patt :: .PathExprSegments):PathExprSegments < Last 
+        { 
+            .InnerAttributes B; 
+            (for2 Patt | .PatternNoTopAlts limit Last B):IteratorLoopExpression;  
+            .NonEmptyStatements
+        };
+
+    rule for2 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit ptrValue(_, LastValue) #as Last B:BlockExpression => 
+            incrementPatt(Patt, LastValue) ~> for1 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit Last B
+
+    rule while (E:ExpressionExceptStructExpression) S:BlockExpression => if E { .InnerAttributes S; while(E)S; .NonEmptyStatements};
+
+    // Necessary for handling all possible integer types provided in the range expression of for loops
+    syntax LetStatement ::= incrementPatt(Identifier, Value) [function]
+
+    rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => 
+            let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i32(Int2MInt(1:Int)));
+        requires checkIntOfType(ComparisonValue, i32)
+    rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => 
+            let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u32(Int2MInt(1:Int)));
+        requires checkIntOfType(ComparisonValue, u32)
+    rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => 
+            let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u64(Int2MInt(1:Int)));
+        requires checkIntOfType(ComparisonValue, u64)
+    rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => 
+            let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i64(Int2MInt(1:Int)));
+        requires checkIntOfType(ComparisonValue, i64)
+    rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => 
+            let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u128(Int2MInt(1:Int))); 
+        requires checkIntOfType(ComparisonValue, u128)
+
+endmodule
+
+```

rust-semantics/representation.md

@@ -23,9 +23,13 @@ module RUST-VALUE-SYNTAX
                     | u128(MInt{128})
                     | tuple(ValueList)
                     | struct(TypePath, Map)  // Map from field name (Identifier) to value ID (Int)
+                    | Range
                     | Bool
                     | String
 
+
+    syntax Range ::= intRange(Value, Value) //[seqstrict]
+
     syntax ValueList ::= List{Value, ","}
     syntax ValueOrError ::= Value | SemanticsError
 
@@ -92,6 +96,7 @@ module RUST-REPRESENTATION
                         | "u32"  [token]
                         | "i64"  [token]
                         | "u64"  [token]
+                        | "u128"  [token]
                         | "bool" [token]
                         | "str"  [token]
 
@@ -111,6 +116,23 @@ module RUST-REPRESENTATION
 
     syntax CallParamsList ::= reverse(CallParamsList, CallParamsList)  [function, total]
 
+    syntax Bool ::= checkIntOfType(Value, Type)  [function, total]
+                  | checkIntOfSameType(Value, Value) [function, total]
+
+    rule checkIntOfType(u32(_),  u32) => true
+    rule checkIntOfType(i32(_),  i32) => true
+    rule checkIntOfType(u64(_),  u64) => true
+    rule checkIntOfType(i64(_),  i64) => true
+    rule checkIntOfType(i64(_),  u128) => true
+    rule checkIntOfType(_, _) => false [owise]
+
+    rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A,  u32) requires checkIntOfType(B,  u32) 
+    rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A,  i32) requires checkIntOfType(B,  i32)
+    rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A,  u64) requires checkIntOfType(B,  u64)
+    rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A,  i64) requires checkIntOfType(B,  i64)
+    rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A,  u128) requires checkIntOfType(B,  u128)
+    rule checkIntOfSameType(_, _) => false [owise]
+
     syntax TypePathOrError ::= TypePath | SemanticsError
     syntax TypePathOrError ::= parentTypePath(TypePath)  [function, total]
 

rust-semantics/rust-common-syntax.md

@@ -391,7 +391,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
                         Expression "&&" Expression [seqstrict]
                       | Expression "||" Expression [seqstrict]
 
-                      > Expression ".." Expression
+                      > Expression ".." Expression [seqstrict]
 
                       > right:
                         Expression "=" Expression
@@ -663,7 +663,8 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
 
 ```k
 
-  syntax IteratorLoopExpression ::= "for" Pattern "in" ExpressionExceptStructExpression BlockExpression
+  syntax IteratorLoopExpression ::= "for" Pattern "in" ExpressionExceptStructExpression BlockExpression [seqstrict(2)]
+                                  | "while" ExpressionExceptStructExpression BlockExpression
 
 ```
 
@@ -680,6 +681,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
 ```k
 
   syntax IfExpression ::= "if" ExpressionExceptStructExpression BlockExpression  MaybeIfElseExpression [strict(1)] 
+
   syntax MaybeIfElseExpression ::= "" 
                                  | "else" IfElseExpression
   syntax IfElseExpression ::= BlockExpression 
@@ -769,7 +771,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
 
 ```k
 
-  syntax RangePattern ::= "TODO: not needed yet, not implementing"
+  syntax RangePattern ::= Expression ".." Expression 
 
 ```
 

tests/execution/loops.1.run

@@ -0,0 +1,4 @@
+new LoopExpressions;
+call LoopExpressions.iterator_evaluation;
+return_value;
+check_eq ()

tests/execution/loops.2.run

@@ -0,0 +1,4 @@
+new LoopExpressions;
+call LoopExpressions.while_evaluation;
+return_value;
+check_eq ()

tests/execution/loops.3.run

@@ -0,0 +1,4 @@
+new LoopExpressions;
+call LoopExpressions.iterator_with_variables;
+return_value;
+check_eq ()

tests/execution/loops.4.run

@@ -0,0 +1,4 @@
+new LoopExpressions;
+call LoopExpressions.iterator_with_same_pattern;
+return_value;
+check_eq ()

tests/execution/loops.rs

@@ -0,0 +1,43 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use multiversx_sc::imports::*;
+
+#[multiversx_sc::contract]
+pub trait LoopExpressions {
+    #[init]
+    fn init(&self) {
+    }
+
+    #[upgrade]
+    fn upgrade(&self) {}
+
+    fn iterator_evaluation(&self){ 
+      for i in 1_u64..10_u64 {
+        let x = i * 2_u64;
+      };
+    }
+
+    fn while_evaluation(&self){ 
+      while 1_u64 < 1_u64 {
+        let x: u64 = 2_u64; 
+      };
+    }
+
+    fn iterator_with_variables(&self) { 
+      let y = 20_u64;
+      let z = 10_u64; 
+
+      for i in z..y {
+        let x = i * 2_u64;
+      };
+    }
+
+    fn iterator_with_same_pattern(&self) { 
+      let i = 1_u64;
+      for i in i..i+3_u64 {
+        let x = i * 2_u64;
+      };
+    }
+
+}