vyper-lll: updated semantics to work with K5. Scripts not updated yet.

common/evm-syntax.k

@@ -1,4 +1,5 @@
 module EVM-SYNTAX
+    imports DOMAINS
     imports EVM-CORE-SYNTAX
     syntax EVM ::= EVMCORE
                   | Int

common/lll-abstract-syntax.k

@@ -1,4 +1,5 @@
 module LLL-ABSTRACT-SYNTAX
+  imports DOMAINS
 
     syntax LLLExp ::= LLLEVM
                     | Int

lll-evm/xevm-evm.k

@@ -4,6 +4,7 @@ require "../common/evm-syntax.k"
 require "lll-evm-config.k"
 
 module XEVM-EVM
+    imports DOMAINS
     imports XEVM-EVM-INTERFACE
 
     imports LLL-EVM-CONFIG
@@ -18,6 +19,7 @@ module XEVM-EVM
     rule xevm2evm(Code) => genLabelTbl(Code) ~> decode(Code)
 
 ////
+    syntax KItem ::= genLabelTbl ( List /* XEVM* */ )
 
     rule genLabelTbl(.List) => .
 
@@ -62,9 +64,9 @@ module XEVM-EVM
     rule     decode(ListItem(PUSH(N, B))      Code) => decode(ListItem(decode1(PUSH(N,B)))) ~> decodeBytes(B) ~> decode(Code)
 
     rule <k> decode(ListItem(CODELEN)         Code) => decodeInt(POS) ~>       decode(                   Code) ... </k> <pos> POS </pos>
-    rule <k> decode(ListItem(PUSH (label(L))) Code) => decodeInt(M[L]:>Int) ~> decode(                   Code) ... </k> <labelTbl> M </labelTbl> when L in keys(M)
-    rule <k> decode(ListItem(JUMP (label(L))) Code) => decodeInt(M[L]:>Int) ~> decode(ListItem(JUMP)     Code) ... </k> <labelTbl> M </labelTbl> when L in keys(M)
-    rule <k> decode(ListItem(JUMPI(label(L))) Code) => decodeInt(M[L]:>Int) ~> decode(ListItem(JUMPI)    Code) ... </k> <labelTbl> M </labelTbl> when L in keys(M)
+    rule <k> decode(ListItem(PUSH (label(L))) Code) => decodeInt(POS) ~>       decode(                   Code) ... </k> <labelTbl>... L |-> POS ...</labelTbl>
+    rule <k> decode(ListItem(JUMP (label(L))) Code) => decodeInt(POS) ~>       decode(ListItem(JUMP)     Code) ... </k> <labelTbl>... L |-> POS ...</labelTbl>
+    rule <k> decode(ListItem(JUMPI(label(L))) Code) => decodeInt(POS) ~>       decode(ListItem(JUMPI)    Code) ... </k> <labelTbl>... L |-> POS ...</labelTbl>
     rule     decode(ListItem(JUMPI(pc))       Code) =>            decode(ListItem(PC) ListItem(JUMPI)    Code)
     rule     decode(ListItem(JUMPDEST(_))     Code) =>                         decode(ListItem(JUMPDEST) Code)
     rule     decode(ListItem(BLANK(_))        Code) =>                         decode(                   Code)

lll-evm/xevm-syntax.k

@@ -1,6 +1,7 @@
 require "../common/evm-syntax.k"
 
 module XEVM-SYNTAX
+    imports DOMAINS
     imports EVM-CORE-SYNTAX
 
     syntax XEVM ::= EVMCORE

tests/vyper/tests/parser/features/test_comments/251ec168-d509-4680-b521-07451cc357b2.v.py → tests/vyper/tests/parser/features/test_comments/test_comment_test.v.py

@@ -1,6 +1,6 @@
 
 @public
-def foo() -> num:
+def foo() -> int128:
     # Returns 3
     return 3
 

vyper-lll/vyper-lll-post.k

@@ -7,5 +7,9 @@ module VYPER-LLL-POST
  // -----------------------------------------------------------------
     rule $%seq(EXPR, .LLLExps) => EXPR
     rule $%seq(EXPR1, (EXPR2, EXPRS)) => $seq(EXPR1, $%seq(EXPR2, EXPRS))
+      requires EXPR1 =/=K $pass
+
+    rule $%seq($pass, (EXPR2, EXPRS)) => $%seq(EXPR2, EXPRS)
+    rule $%seq(.LLLExps) => $pass
 
 endmodule 

vyper-lll/vyper-lll.k

@@ -4,6 +4,7 @@
 
 require "../common/vyper-abstract-syntax.k"
 require "../common/lll-abstract-syntax.k"
+require "../vyper/krypto.k"
 require "vyper-lll-utils.k"
 require "domains.k"
 
@@ -528,7 +529,7 @@ module VYPER-LLL
 
     syntax CLLLExps  ::= "#copyArg" "(" Params "," Bool /*init?*/ ")"
  // -----------------------------------------------------------------
-    rule #copyArg(.Params, _) => $pass,.LLLExps
+    rule #copyArg(.Params, _) => .LLLExps
 
     rule <k> #copyArg(PARAMS, true) => $codecopy(@reservedMemPos,
                                                  $codelen,
@@ -628,17 +629,17 @@ module VYPER-LLL
            #mkClamperListT(N -Int 1, T, DPOS +Int #sizeOfType(T), MPOS +Int #sizeOfType(T), ISINIT)
       requires N >Int 1
 
-    rule #mkClamper(%decimal, _, _, _) => $pass,.LLLExps
+    rule #mkClamper(%decimal, _, _, _) => .LLLExps
 
-    rule #mkClamper(%unitT(%decimal, _:Map, _), _, _, _) => $pass,.LLLExps
+    rule #mkClamper(%unitT(%decimal, _:Map, _), _, _, _) => .LLLExps
 
-    rule #mkClamper(%num256, _, _, _) => $pass,.LLLExps
+    rule #mkClamper(%num256, _, _, _) => .LLLExps
 
-    rule #mkClamper(%bytes32, _, _, _) => $pass,.LLLExps
+    rule #mkClamper(%bytes32, _, _, _) => .LLLExps
 
-    rule #mkClamper(%mapT(_, _), _, _, _) => $pass,.LLLExps
+    rule #mkClamper(%mapT(_, _), _, _, _) => .LLLExps
 
-    rule #mkClamper(%structT(_), _, _, _) => $pass,.LLLExps
+    rule #mkClamper(%structT(_), _, _, _) => .LLLExps
 
     rule #mkCopier(MPOS, POS, SIZE, true) => $codecopy(MPOS, $add($codelen, POS), SIZE)
 
@@ -686,7 +687,7 @@ module VYPER-LLL
 // ====================
 
 
-    rule #compileStmt(%annvar(NAME, T)) => #newVar(NAME, #parseType(T, true)) ~> #deletePrev ~> $pass,.LLLExps
+    rule #compileStmt(%annvar(NAME, T)) => #newVar(NAME, #parseType(T, true)) ~> #deletePrev ~> .LLLExps
 
     rule #compileStmt(%annvar(NAME, T, EXPR))
          => #newVar(NAME, #parseType(T, true)) ~> #deletePrev ~> #compileStmt(%assign(%var(NAME), EXPR))
@@ -4652,16 +4653,16 @@ module VYPER-LLL
       requires lengthString(STR) ==Int 0
 
     rule #string2BytesAux(STR, RESULT)
-        => #nonEmptystring2Bytes(STR, RESULT)
+        => #nonEmptyString2Bytes(STR, RESULT)
       requires lengthString(STR) >Int 0
 
-    rule #nonEmptystring2Bytes(STR, RESULT)
+    rule #nonEmptyString2Bytes(STR, RESULT)
         => #string2BytesAux(substrString(STR, 1, lengthString(STR)),
                             RESULT ++Byte (ordChar(substrString(STR, 0, 1)) : .Bytes))
       requires ordChar(substrString(STR, 0, 1)) <Int 256
 
     rule (. => #exception("Cannot insert special character into byte array"))
-         ~> #nonEmptystring2Bytes(STR, RESULT)
+         ~> #nonEmptyString2Bytes(STR, RESULT)
       requires ordChar(substrString(STR, 0, 1)) >=Int 256