Implement instruction sequences; let; var expressions

rust-semantics/execution.md

@@ -3,12 +3,16 @@
 requires "execution/configuration.md"
 requires "execution/block.md"
 requires "execution/calls.md"
+requires "execution/let.md"
 requires "execution/stack.md"
+requires "execution/statements.md"
 
 module RUST-EXECUTION
     imports RUST-BLOCK
     imports RUST-CALLS
+    imports RUST-LET
     imports RUST-STACK
+    imports RUST-STATEMENTS
 endmodule
 
 ```

rust-semantics/execution/let.md

@@ -0,0 +1,30 @@
+```k
+
+module RUST-LET
+    imports COMMON-K-CELL
+    imports RUST-CASTS
+    imports RUST-EXECUTION-CONFIGURATION
+    imports RUST-VALUE-SYNTAX
+    imports RUST-SHARED-SYNTAX
+
+    // Not all cases are implemented
+    rule
+        <k>
+            let Variable:Identifier : T:Type = V:Value ; => .K
+            ...
+        </k>
+        <next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
+        <locals> Locals:Map => Locals[Variable <- NextId] </locals>
+        <values> Values:Map => Values[NextId <- implicitCast(V, T)] </values>
+    rule
+        <k>
+            let Variable:Identifier = V:Value ; => .K
+            ...
+        </k>
+        <next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
+        <locals> Locals:Map => Locals[Variable <- NextId] </locals>
+        <values> Values:Map => Values[NextId <- V] </values>
+    requires notBool mayBeDefaultTypedInt(V)
+endmodule
+
+```

rust-semantics/execution/statements.md

@@ -0,0 +1,11 @@
+```k
+
+module RUST-STATEMENTS
+    imports RUST-SHARED-SYNTAX
+
+    rule Nes:NonEmptyStatements E:Expression => Nes ~> E
+    rule S:Statement Ss:NonEmptyStatements => S ~> Ss
+    rule .NonEmptyStatements => .K
+endmodule
+
+```

rust-semantics/expression.md

@@ -1,9 +1,11 @@
 ```k
 requires "expression/casts.md"
 requires "expression/literals.md"
+requires "expression/variables.md"
 
 module RUST-EXPRESSION
     imports private RUST-CASTS
     imports private RUST-EXPRESSION-LITERALS
+    imports private RUST-EXPRESSION-VARIABLES
 endmodule
 ```

rust-semantics/expression/variables.md

@@ -0,0 +1,18 @@
+```k
+
+module RUST-EXPRESSION-VARIABLES
+    imports COMMON-K-CELL
+    imports RUST-EXECUTION-CONFIGURATION
+    imports RUST-VALUE-SYNTAX
+    imports RUST-SHARED-SYNTAX
+
+    rule
+        <k>
+            Variable:Identifier :: .PathExprSegments => V
+            ...
+        </k>
+        <locals> Variable |-> VarId:Int ... </locals>
+        <values> VarId |-> V:Value ... </values>
+endmodule
+
+```

rust-semantics/representation.md

@@ -1,6 +1,7 @@
 ```k
 
 module RUST-VALUE-SYNTAX
+    imports BOOL
     imports LIST  // for filling the second argument of `error`.
     imports MAP
     imports MINT
@@ -28,6 +29,10 @@ module RUST-VALUE-SYNTAX
     syntax KResult ::= Value
 
     syntax ValueOrError ::= Value | SemanticsError
+
+    syntax Bool ::= mayBeDefaultTypedInt(Value)  [function, total]
+    rule mayBeDefaultTypedInt(_V) => false  [owise]
+    rule mayBeDefaultTypedInt(u128(_)) => true
 endmodule
 
 module RUST-REPRESENTATION

rust-semantics/rust-common-syntax.md

@@ -736,9 +736,9 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
 
 ```k
 
-  syntax LetStatement ::= OuterAttributes "let" PatternNoTopAlt MaybeColonType MaybeEqualsExpressionMaybeElseBlockExpression ";"
+  syntax LetStatement ::= OuterAttributes "let" PatternNoTopAlt MaybeColonType ";"
+                        | OuterAttributes "let" PatternNoTopAlt MaybeColonType "=" Expression MaybeElseBlockExpression ";"  [strict(4)]
   syntax MaybeColonType ::= "" | ":" Type
-  syntax MaybeEqualsExpressionMaybeElseBlockExpression ::= "" | "=" Expression MaybeElseBlockExpression
   // TODO: Not implemented properly to remove ambiguities
   syntax MaybeElseBlockExpression ::= "" // | "else" BlockExpression
 

rust-semantics/targets/preprocessing/rust.md

@@ -3,15 +3,16 @@
 requires "configuration.md"
 requires "../../preprocessing.md"
 requires "../../representation.md"
-requires "../../expression.md"
+requires "../../expression/casts.md"
+requires "../../expression/literals.md"
 requires "../../rust-common-syntax.md"
 
 module RUST-SYNTAX
     imports RUST-COMMON-SYNTAX
 endmodule
 
 module RUST
-    imports private RUST-EXPRESSION
+    imports private RUST-EXPRESSION-LITERALS
     imports private RUST-PREPROCESSING
     imports private RUST-RUNNING-CONFIGURATION
 endmodule

tests/execution/let-final-expression.1.run

@@ -0,0 +1,4 @@
+new LetFinal;
+call LetFinal.let_final;
+return_value;
+check_eq 100_u64

tests/execution/let-final-expression.rs

@@ -0,0 +1,19 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use multiversx_sc::imports::*;
+
+#[multiversx_sc::contract]
+pub trait LetFinal {
+    #[init]
+    fn init(&self) {
+    }
+
+    #[upgrade]
+    fn upgrade(&self) {}
+
+    fn let_final(&self) -> u64 {
+        let x = 100_u64;
+        x
+    }
+}