Merge pull request #702 from molecula451/smt-checker

packages/contracts/foundry.toml

@@ -18,3 +18,20 @@ force = false
 
 [rpc_endpoints]
 mainnet = "https://eth.ubq.fi/v1/mainnet"
+
+[profile.SMT.model_checker]
+contracts = { }
+engine = 'chc'
+solvers = ['z3']
+show_unproved = true
+timeout = 0
+targets = [
+  'assert',
+  'constantCondition',
+  'divByZero',
+  'outOfBounds',
+  'overflow',
+  'popEmptyArray',
+  'underflow',
+  'balance',
+]

packages/contracts/package.json

@@ -67,6 +67,7 @@
     "@types/node": "^18.11.18",
     "@types/react-transition-group": "^4",
     "cspell": "latest",
+    "glob": "^10.3.0",
     "prettier-plugin-solidity": "^1.1.2",
     "typescript": "^4.9.4"
   }

packages/contracts/run-smt-setup.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+# Define paths
+foundryTomlPath="foundry.toml"
+backupFoundryTomlPath="foundry.toml.backup"
+smtScriptPath="scripts/smt-checker/smt/smt.ts"
+
+# Copy foundry.toml to backup file
+cp -p "$foundryTomlPath" "$backupFoundryTomlPath"
+
+# Run smt.ts script
+npx tsx "$smtScriptPath"

packages/contracts/scripts/smt-checker/README.md

@@ -0,0 +1,54 @@
+# SMT-Checker Support for Smart Contract Testing
+
+This repository provides SMT-Checker support for testing smart contracts. Follow these steps to get started:
+
+
+## Make Sure Your System Has Z3 Installed >= "4.8.11"
+
+Ensure that your system has Z3 installed with a version number greater than or equal to the required version.
+
+## Step 1: Download and Install Z3
+
+Before proceeding, ensure that you have `g++` and `python3` installed on your system. To download and install Z3, enter the following commands in your terminal:
+
+### Run script:
+```
+sh ./update-dependencies.sh
+```
+
+Once installed, you can verify that Z3 is correctly installed by checking the version number.
+
+## Step 3: Use Forge to Test Contracts Using SMT
+
+Check that you do not have a profile ready at foundry.toml you might skip this step, else run
+```
+npx tsx smt-checker/smt/update.ts
+```
+
+This will add a new pre-defined profile to foundry.toml for testing & compiling contracts using SMTChecker
+
+### Export a foundry env variable to make use of the profile
+
+```
+export FOUNDRY_PROFILE=SMT
+```
+
+
+https://github.com/molecula451/ubiquity-dollar/assets/41552663/cdcf3982-94a4-4cf5-8962-c49982b7c83a
+
+
+
+Ensure that your repository is up-to-date with the latest npm/yarn packages, then run the following command:
+
+```
+sh ./run-smt-setup.sh
+```
+
+
+https://github.com/molecula451/ubiquity-dollar/assets/41552663/a4cad18e-0686-4637-bd0e-e229159543fe
+
+
+
+This will prompt you to select a contract. Once selected, check that the contract was updated in Foundry, then build it using forge build. Wait for the SMT-Checker results to appear after compiling.
+
+![checker](https://github.com/molecula451/ubiquity-dollar/assets/41552663/a8e6a3de-2ccf-40bd-8d19-c1b4203c466f)

packages/contracts/scripts/smt-checker/check-deps.sh

@@ -0,0 +1,27 @@
+#!/bin/bash
+
+missing_dependencies=()
+
+# Check if wget is installed
+if ! command -v wget &>/dev/null; then
+    missing_dependencies+=("wget")
+fi
+
+# Check if g++ is installed
+if ! command -v g++ &>/dev/null; then
+    missing_dependencies+=("g++")
+fi
+
+if [ ${#missing_dependencies[@]} -ne 0 ]; then
+    echo "The following dependencies are missing: ${missing_dependencies[*]}"
+    echo "Please install them to continue."
+    echo "On Ubuntu/Debian, use the command:"
+    echo "sudo apt-get install ${missing_dependencies[*]}"
+    echo "On Arch Linux, use the command:"
+    echo "sudo pacman -S ${missing_dependencies[*]}"
+    echo "On macOS, you can install ${missing_dependencies[*]} by installing Xcode Command Line Tools:"
+    echo "xcode-select --install"
+    exit 1
+fi
+
+echo "All required programs are installed on your system."

packages/contracts/scripts/smt-checker/smt/smt.ts

@@ -0,0 +1,124 @@
+import { globSync } from "glob";
+import fs from "fs";
+import path from "path";
+import readline from "readline";
+
+const searchContracts = async (directory) => {
+  const contracts = await globSync(`${directory}/**/*.{sol,t.sol}`);
+  return contracts.map((contract) => ({
+    path: contract.replace(directory, ""),
+    name: contract.replace(/^.*[\\/]/, "").replace(/\.[^.]+$/, ""),
+  }));
+};
+
+const updateFoundryToml = async () => {
+  const currentDirectory = process.cwd();
+  const foundryTomlPath = path.join(currentDirectory, "foundry.toml");
+  const contractsDirectoryPath = path.join(currentDirectory, "src", "dollar");
+
+  try {
+    // Read the contents of foundry.toml
+    let foundryTomlContent = fs.readFileSync(foundryTomlPath, "utf-8");
+
+    // List all the contracts
+    const contractsArray = await searchContracts(contractsDirectoryPath);
+
+    // Choose contracts to add
+    const selectedContracts = [];
+    let shouldContinue = true;
+    while (shouldContinue) {
+      const contractIndex = await promptContractSelection(contractsArray);
+      if (contractIndex !== -1) {
+        const selectedContract = contractsArray[contractIndex];
+        selectedContracts.push(selectedContract);
+        console.log(`Contract '${selectedContract.name}' selected to be added to foundry.toml.`);
+      } else {
+        shouldContinue = false;
+      }
+    }
+
+    // Generate the contracts section content
+    const contractsSectionContent = generateContractsSectionContent(selectedContracts);
+
+    // Update the contracts section in foundry.toml
+    foundryTomlContent = updateContractsSection(foundryTomlContent, contractsSectionContent);
+
+    // Write the updated content back to foundry.toml
+    fs.writeFileSync(foundryTomlPath, foundryTomlContent);
+
+    console.log("foundry.toml updated successfully.");
+  } catch (error) {
+    console.error("Error updating foundry.toml:", error);
+  }
+};
+
+const promptContractSelection = (contractsArray) => {
+  return new Promise((resolve) => {
+    const rd = readline.createInterface({
+      input: process.stdin,
+      output: process.stdout,
+    });
+
+    const printContractsList = () => {
+      console.log("Contracts:");
+      contractsArray.forEach((contract, index) => {
+        console.log(`${index + 1}. ${contract.name}`);
+      });
+    };
+
+    let selectedContract;
+
+    const handleAnswer = (answer) => {
+      rd.close();
+      const selectedContractIndex = parseInt(answer) - 1;
+
+      if (!isNaN(selectedContractIndex) && selectedContractIndex >= 0 && selectedContractIndex < contractsArray.length) {
+        selectedContract = contractsArray[selectedContractIndex];
+        resolve(selectedContractIndex);
+      } else {
+        resolve(-1);
+      }
+    };
+    printContractsList();
+    rd.question("Enter the number of the contract to add or press Enter to finish: ", (answer) => {
+      handleAnswer(answer);
+
+      if (selectedContract) {
+        console.log(`Contract '${selectedContract.name}' added to the selection.`);
+      }
+    });
+  });
+};
+
+const generateContractsSectionContent = (selectedContracts) => {
+  const contractsEntries = selectedContracts.map((contract) => `"${path.join("src", "dollar", contract.path)}" = ["${contract.name}"]`);
+  return `contracts = { ${contractsEntries.join(", ")} }`;
+};
+
+const updateContractsSection = (foundryTomlContent, contractsSectionContent) => {
+  const regex = /contracts\s*=\s*\{([^}]+)\}/;
+  const match = regex.exec(foundryTomlContent);
+
+  if (match) {
+    const updatedContent = foundryTomlContent.replace(match[0], contractsSectionContent);
+    const modifiedContent = removeExtraSpace(updatedContent);
+    return modifiedContent;
+  } else {
+    const modelCheckerSectionRegex = /\[profile\.default\.model_checker\]/;
+    const modelCheckerMatch = modelCheckerSectionRegex.exec(foundryTomlContent);
+
+    if (modelCheckerMatch) {
+      const modelCheckerSectionStartIndex = modelCheckerMatch.index;
+      const insertionIndex = foundryTomlContent.indexOf("\n", modelCheckerSectionStartIndex);
+      return foundryTomlContent.slice(0, insertionIndex) + `\n\n${contractsSectionContent}\n` + foundryTomlContent.slice(insertionIndex);
+    } else {
+      return foundryTomlContent + `\n\n${contractsSectionContent}\n`;
+    }
+  }
+};
+
+const removeExtraSpace = (content) => {
+  return content.replace(/\n\n+/g, "\n\n").trim() + "\n";
+};
+
+updateFoundryToml();

packages/contracts/scripts/smt-checker/smt/update.ts

@@ -0,0 +1,70 @@
+import fs from "fs";
+import path from "path";
+
+const updateFoundryToml = async () => {
+  const currentDirectory = process.cwd();
+  const foundryTomlPath = path.join(currentDirectory, "foundry.toml");
+
+  try {
+    // Read the contents of foundry.toml
+    let foundryTomlContent = fs.readFileSync(foundryTomlPath, "utf-8");
+
+    // Check if the model_checker section exists in foundry.toml
+    const regex = /\[profile\.default\.model_checker\]/;
+    const match = regex.exec(foundryTomlContent);
+
+    if (match) {
+      console.log("model_checker section already exists in foundry.toml.");
+      return;
+    }
+
+    // Generate the model_checker section content
+    const modelCheckerSectionContent = generateModelCheckerSectionContent();
+
+    // Update foundry.toml with the model_checker section
+    foundryTomlContent = updateFoundryTomlContent(foundryTomlContent, modelCheckerSectionContent);
+
+    // Write the updated content back to foundry.toml
+    fs.writeFileSync(foundryTomlPath, foundryTomlContent);
+
+    console.log("foundry.toml updated successfully.");
+  } catch (error) {
+    console.error("Error updating foundry.toml:", error);
+  }
+};
+
+const generateModelCheckerSectionContent = (): string => {
+  const modelCheckerSectionContent = `
+[profile.SMT.model_checker]
+contracts = { }
+engine = 'chc'
+solvers = ['z3']
+show_unproved = true
+timeout = 0
+targets = [
+  'assert',
+  'constantCondition',
+  'divByZero',
+  'outOfBounds',
+  'overflow',
+  'popEmptyArray',
+  'underflow',
+  'balance',
+]
+`;
+  return modelCheckerSectionContent.trim() + "\n";
+};
+
+const updateFoundryTomlContent = (foundryTomlContent: string, modelCheckerSectionContent: string): string => {
+  const lastTwoLinesRegex = /.*\n.*\n.*$/s;
+  const match = lastTwoLinesRegex.exec(foundryTomlContent);
+
+  if (match) {
+    const insertionIndex = match.index + match[0].length;
+    return foundryTomlContent.slice(0, insertionIndex) + `\n${modelCheckerSectionContent}\n` + foundryTomlContent.slice(insertionIndex);
+  } else {
+    return foundryTomlContent + `\n\n${modelCheckerSectionContent}\n`;
+  }
+};
+
+updateFoundryToml();

packages/contracts/scripts/smt-checker/update-deps-ubuntu.sh

@@ -0,0 +1,22 @@
+#!/bin/bash
+
+# Install dependencies
+sudo apt-get update && sudo apt-get install -y g++ && \
+sudo apt-get install -y wget
+sudo apt-get install -y z3 && \
+sudo apt-get install -y libz3-dev && \
+
+# Download and install Z3
+sudo wget https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.11.0.tar.gz && \
+sudo tar -zxvf z3-4.11.0.tar.gz && \
+cd z3-z3-4.11.0 && \
+sudo python3 scripts/mk_make.py && \
+cd build && \
+sudo make -j$(nproc) && \
+sudo make install && \
+sudo cp libz3.so libz3.so.4.11 && \
+sudo mv libz3.so.4.11 /usr/lib/x86_64-linux-gnu && \
+echo "Successfully copied Z3 to the system" && \
+
+# Print success message
+echo "Z3 installation completed successfully!"