From 34368e7bfaef96b8eb69b708b80307158b64beda Mon Sep 17 00:00:00 2001
From: Dwight Guth <dwight.guth@pi2.network>
Date: Thu, 22 Aug 2024 14:33:26 -0500
Subject: [PATCH 1/4] bool literals

---
 src/expression.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/expression.md b/src/expression.md
index b8165da..9213505 100644
--- a/src/expression.md
+++ b/src/expression.md
@@ -131,6 +131,9 @@ module SOLIDITY-EXPRESSION
        <contract-fn-body> BODY </contract-fn-body>
     requires isKResult(ARGS)
 
+  // boolean literal
+  rule B:Bool => v(B, bool)
+
   // equality and inequality
   rule v(V1:MInt{160}, _) == v(V2, _) => v(V1 ==MInt V2, bool)
   rule v(V1:MInt{160}, _) != v(V2, _) => v(V1 =/=MInt V2, bool)

From 5aa48b4dc5eb3047c2d895b220b392e9d5931301 Mon Sep 17 00:00:00 2001
From: Dwight Guth <dwight.guth@pi2.network>
Date: Thu, 22 Aug 2024 14:33:40 -0500
Subject: [PATCH 2/4] fix state variable lookup

---
 src/expression.md | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/expression.md b/src/expression.md
index 9213505..9c705c6 100644
--- a/src/expression.md
+++ b/src/expression.md
@@ -81,13 +81,13 @@ module SOLIDITY-EXPRESSION
        <iface-id> TYPE </iface-id>
 
   // state variable lookup
-  rule <k> X:Id => v(V, T) ...</k>
+  rule <k> X:Id => v({S[X] orDefault default(T)}:>Value, T) ...</k>
        <this> THIS </this>
        <this-type> TYPE </this-type>
        <contract-id> TYPE </contract-id>
-       <contract-state>... X |-> T </contract-state>
+       <contract-state>... X |-> T ...</contract-state>
        <contract-address> THIS </contract-address>
-       <contract-storage>... X |-> V ...</contract-storage>
+       <contract-storage> S </contract-storage>
 
   // local variable lookup
   rule <k> X:Id => v(V, T) ...</k>
@@ -190,7 +190,15 @@ module SOLIDITY-EXPRESSION
   rule convert(I:Int, uint256) => Int2MInt(I)::MInt{256}
 
   syntax Value ::= default(TypeName) [function]
+  rule default(uint8)   => 0p8
+  rule default(uint32)  => 0p32
+  rule default(uint112) => 0p112
   rule default(address) => 0p160
+  rule [[ default(X:Id) => 0p160 ]]
+       <contract-id> X </contract-id>
+  rule [[ default(X:Id) => 0p160 ]]
+       <iface-id> X </iface-id>
+  rule default(uint256) => 0p256
 
   syntax Expression ::= retval(List) [function] 
   rule retval(.List) => void

From f0ca2245ada2faa87b404127dabe3e17a7f86801 Mon Sep 17 00:00:00 2001
From: Dwight Guth <dwight.guth@pi2.network>
Date: Thu, 22 Aug 2024 14:33:51 -0500
Subject: [PATCH 3/4] fix return values with no name

---
 src/expression.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/expression.md b/src/expression.md
index 9c705c6..e4ba232 100644
--- a/src/expression.md
+++ b/src/expression.md
@@ -175,6 +175,7 @@ module SOLIDITY-EXPRESSION
   syntax KItem ::= bind(List, List, CallArgumentList, List, List)
   rule bind(.List, .List, .CallArgumentList, .List, .List) => .K
   rule bind(ListItem(noId) PARAMS, ListItem(_) TYPES, _, ARGS, L1:List, L2:List) => bind(PARAMS, TYPES, ARGS, L1, L2)
+  rule bind(.List, .List, .CallArgumentList, ListItem(_) TYPES, ListItem(noId) NAMES) => bind(.List, .List, .CallArgumentList, TYPES, NAMES)
   rule <k> bind(ListItem(X:Id) PARAMS, ListItem(LT:TypeName) TYPES, v(V:Value, RT:TypeName), ARGS, L1:List, L2:List) => bind(PARAMS, TYPES, ARGS, L1, L2) ...</k>
        <env> E => E [ X <- var(!I:Int, LT) ] </env>
        <store> S => S [ !I <- convert(V, RT, LT) ] </store>
@@ -202,5 +203,6 @@ module SOLIDITY-EXPRESSION
 
   syntax Expression ::= retval(List) [function] 
   rule retval(.List) => void
+  rule retval(ListItem(noId)) => void
   rule retval(ListItem(X:Id)) => X
 endmodule

From 4c4b17872333827f82cb2132e23e8386b1b734ef Mon Sep 17 00:00:00 2001
From: Dwight Guth <dwight.guth@pi2.network>
Date: Mon, 26 Aug 2024 10:48:44 -0500
Subject: [PATCH 4/4] add missing integer types

---
 src/solidity-syntax.md | 2 +-
 src/solidity.md        | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/solidity-syntax.md b/src/solidity-syntax.md
index a105bcc..c4eaf5d 100644
--- a/src/solidity-syntax.md
+++ b/src/solidity-syntax.md
@@ -25,7 +25,7 @@ We use tokens for the `pragma` definition in the header, hexadecimal numbers use
     syntax HexNumber ::= r"0x[A-Fa-f0-9]+"                                                          [token]
     syntax Decimal ::= r"(([0-9][_]?)+|([0-9][_]?)*[\\.]([0-9][_]?)+)([eE][\\-]?([0-9][_]?)+)?"     [token]
 
-    syntax ElementaryTypeName ::= "uint" [function] | "uint112" | "uint256" | "address" | "bool"
+    syntax ElementaryTypeName ::= "uint" [function] | "uint8" | "uint32" | "uint112" | "uint256" | "address" | "bool"
     syntax DataLocation ::= "memory" | "storage" | "calldata"
     syntax SubDenom ::= "wei" | "gwei" | "ether" | "seconds" | "minutes" | "hours" | "days" | "weeks" | "years"
     rule uint => uint256
diff --git a/src/solidity.md b/src/solidity.md
index e4b316e..8e9bf02 100644
--- a/src/solidity.md
+++ b/src/solidity.md
@@ -85,6 +85,8 @@ module SOLIDITY-DATA-SYNTAX
   imports STRING-SYNTAX
   imports SOLIDITY-SYNTAX
 
+  syntax MInt{8}
+  syntax MInt{32}
   syntax MInt{112}
   syntax MInt{160}
   syntax MInt{256}
@@ -113,7 +115,7 @@ module SOLIDITY-DATA
   syntax Expression ::= TypedVal
   syntax CallArgumentList ::= TypedVals
   syntax KResult ::= TypedVal
-  syntax Value ::= MInt{112} | MInt{160} | MInt{256} | Bool | String
+  syntax Value ::= MInt{8} | MInt{32} | MInt{112} | MInt{160} | MInt{256} | Bool | String
 
   syntax List ::= getTypes(ParameterList) [function]
   rule getTypes(.ParameterList) => .List