From 556a2f993188ca161797dc99e0660c778b055490 Mon Sep 17 00:00:00 2001
From: Maria Kotsifakou <kotsifakou.maria@gmail.com>
Date: Wed, 6 Nov 2024 17:09:53 -0600
Subject: [PATCH] Basic string support.

---
 byol_solidity.py                 | 64 ++++++++++++++++++++++++++++++++
 src/solidity.md                  |  3 ++
 test/demo-contracts/USDCMock.sol |  8 ++++
 3 files changed, 75 insertions(+)

diff --git a/byol_solidity.py b/byol_solidity.py
index 5ec5c58..aeed9f3 100755
--- a/byol_solidity.py
+++ b/byol_solidity.py
@@ -26,6 +26,9 @@
   'maxPriorityFeePerGas': 1000000000,
 }
 
+# deploy USDC
+print("Deploying USDC...")
+
 tx_hash = w3.eth.send_transaction(deploy_usdc_tx)
 print(tx_hash)
 receipt = w3.eth.wait_for_transaction_receipt(tx_hash)
@@ -44,10 +47,14 @@
   'maxPriorityFeePerGas': 1000000000,
 }
 
+# mint USDC
+print("Minting USDC...")
+
 tx_hash = w3.eth.send_transaction(mint_usdc_tx)
 print(tx_hash)
 receipt = w3.eth.wait_for_transaction_receipt(tx_hash)
 print(receipt)
+print("USDC Address:", usdc_address)
 
 balanceOf_usdc_data = '70a08231000000000000000000000000' + sender.address[2:]
 
@@ -61,6 +68,9 @@
   'maxPriorityFeePerGas': 1000000000,
 }
 
+# balanceOf USDC
+print("balanceOf USDC...")
+
 balance = w3.eth.call(balanceOf_usdc_tx)
 print(balance)
 
@@ -76,11 +86,17 @@
   'maxPriorityFeePerGas': 1000000000,
 }
 
+# transfer USDC
+print("transfer USDC...")
+
 tx_hash = w3.eth.send_transaction(transfer_usdc_tx)
 print(tx_hash)
 receipt = w3.eth.wait_for_transaction_receipt(tx_hash)
 print(receipt)
 
+# balanceOf USDC
+print("balanceOf USDC...")
+
 balance = w3.eth.call(balanceOf_usdc_tx)
 print(balance)
 
@@ -89,3 +105,51 @@
 
 balance = w3.eth.call(balanceOf_usdc_tx)
 print(balance)
+
+# decimals USDC
+decimals_usdc_data = '313ce567'
+decimals_usdc_tx = {
+  'from': sender.address,
+  'data': decimals_usdc_data,
+  'to': usdc_address,
+  'value': 0,
+  'gas': 11000000,
+  'maxFeePerGas': 2000000000,
+  'maxPriorityFeePerGas': 1000000000,
+}
+
+decimals = w3.eth.call(decimals_usdc_tx)
+print("Decimals:", int(decimals.hex(), 16))
+
+# name
+name_usdc_data = '06fdde03'
+name_usdc_tx = {
+  'from': sender.address,
+  'data': name_usdc_data,
+  'to': usdc_address,
+  'value': 0,
+  'gas': 11000000,
+  'maxFeePerGas': 2000000000,
+  'maxPriorityFeePerGas': 1000000000,
+}
+
+name = w3.eth.call(name_usdc_tx)
+name = w3.to_text(name)
+print("Name:", name)
+
+# symbol
+symbol_usdc_data = '95d89b41'
+symbol_usdc_tx = {
+  'from': sender.address,
+  'data': symbol_usdc_data,
+  'to': usdc_address,
+  'value': 0,
+  'gas': 11000000,
+  'maxFeePerGas': 2000000000,
+  'maxPriorityFeePerGas': 1000000000,
+}
+
+symbol = w3.eth.call(symbol_usdc_tx)
+symbol = w3.to_text(symbol)
+print("Symbol:", symbol)
+
diff --git a/src/solidity.md b/src/solidity.md
index ccbb924..9011fb3 100644
--- a/src/solidity.md
+++ b/src/solidity.md
@@ -202,6 +202,9 @@ module SOLIDITY-ULM-SIGNATURE-IMPLEMENTATION
   rule getOutput(<generatedTop>...
                    <k> v(false, bool) ...</k>
                  ...</generatedTop>) => Int2Bytes(32, 0, BE)
+  rule getOutput(<generatedTop>...
+                   <k> S:String ...</k>
+                 ...</generatedTop>) => Int2Bytes(32, 32, BE) +Bytes Int2Bytes(32, lengthString(S), BE) +Bytes padRightBytes(String2Bytes(S), 32, 0) // TODO: All strings in the EVM ABI must be UTF-8 encoded to bytes
 
   // getGasLeft returns the amount of gas left by reading it from the cell <gas>.
   // The semantics currently initialize the gas by reading the appropriate ULM
diff --git a/test/demo-contracts/USDCMock.sol b/test/demo-contracts/USDCMock.sol
index 109b1fe..cada8c8 100644
--- a/test/demo-contracts/USDCMock.sol
+++ b/test/demo-contracts/USDCMock.sol
@@ -21,6 +21,14 @@ contract USDCMock {
         return dec;
     }
 
+    string name() {
+        return "USD Coin";
+    }
+
+    string symbol() {
+        return "USDC";
+    }
+
     function mint(address account, uint256 value) public {
         require(account != address(0), "USDC: invalid receiver");
         _update(address(0), account, value);