Merge pull request #339 from Certora/jorge/solana-installation-and-usage

solana installation and usage

docs/solana/installation.md

@@ -0,0 +1,49 @@
+# How to get started with the Solana Certora Prover
+
+
+## Installing Solana Certora Prover 
+
+1. First, we will need to install the Solana Certora Prover.
+   For that, please visit [Certora.com](https://www.certora.com/) and sign up for a
+   free account at [Certora sign-up page](https://www.certora.com/signup).
+
+2. You will receive an email with a temporary password and a *Certora Key*.
+   Use the password to login to Certora following the link in the email.
+
+3. Next, install Python3.8.16 or newer on your machine.
+   If you already have Python3 installed, you can check the version: ``python3 --version``.
+   If you need to upgrade, follow these instructions in the
+   [Python Beginners Guide](https://wiki.python.org/moin/BeginnersGuide/Download).
+
+4. Next, install Java. Check your Java version: ``java -version``.
+   If the version is < 11, download and install Java version 11 or later from
+   [Oracle](https://www.oracle.com/java/technologies/downloads/).
+
+5. Then, install the Certora Prover: ``pip3 install certora-cli-beta``.
+
+   Tip: Always use a Python virtual environment when installing packages.
+
+6. Recall that you received a *Certora Key* in your email (Step 2).
+   Use the key to set a temporary environment variable like so
+   ``export CERTORAKEY=<personal_access_key>``.
+
+
+## Rust and Solana Setup
+
+1. We recommend installing Rust as on the
+   official [Rust website](https://www.rust-lang.org/tools/install): 
+
+   ``curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh``
+
+2. Next, install the Solana CLI:
+
+   ``sh -c "$(curl -sSfL https://release.solana.com/v1.18.16/install)``
+
+	Currently, the Solana Prover only supports version `1.18.16` so make sure that you install that specific version.
+
+3. Install Certora version of platform-tools 1.41 as shown [here](https://github.com/Certora/certora-solana-platform-tools?tab=readme-ov-file#installation-of-executables)
+
+4. Finally, install ``rustfilt`` like so: ``cargo install rustfilt``.
+
+
+

docs/solana/scripts/certora_build.py

@@ -0,0 +1,119 @@
+#!/usr/bin/env python3
+import argparse
+import json
+import subprocess
+import tempfile
+import sys
+import os
+from pathlib import Path
+
+SCRIPT_DIR = Path(__file__).resolve().parent
+
+# Command to run for compiling the rust project.
+COMMAND = "just build-sbf"
+
+# JSON FIELDS
+PROJECT_DIR = (SCRIPT_DIR / ".." / "..").resolve()
+SOURCES = ["lib/**/*.rs", 
+           "programs/manifest/**/*.rs", 
+           "programs/manifest/justfile",
+           "programs/manifest/Cargo.toml"
+           ]
+EXECUTABLES = "target/sbf-solana-solana/release/manifest.so"
+
+VERBOSE = False
+
+def log(msg):
+    if VERBOSE:
+        print(msg, file=sys.stderr)
+
+def run_command(command, to_stdout=False, env=None):
+    """Runs the build command and dumps output to temporary files."""
+    log(f"Running '{command}'")
+    try:
+        if to_stdout:
+            result = subprocess.run(
+                command,
+                shell=True,
+                text=True,
+                cwd=SCRIPT_DIR,
+                env=env
+            )
+            return None, None, result.returncode
+        else:
+            with tempfile.NamedTemporaryFile(delete=False, mode='w', prefix="certora_build_", suffix='.stdout') as stdout_file, \
+                tempfile.NamedTemporaryFile(delete=False, mode='w', prefix="certora_build_", suffix='.stderr') as stderr_file:
+                # Compile rust project and redirect stdout and stderr to a temp file
+                result = subprocess.run(
+                    command,
+                    shell=True,
+                    stdout=stdout_file,
+                    stderr=stderr_file,
+                    text=True,
+                    cwd=SCRIPT_DIR,
+                    env=env
+                )
+                return stdout_file.name, stderr_file.name, result.returncode
+    except Exception as e:
+        log(f"Error running command '{command}': {e}")
+        return None, None -1
+
+def write_output(output_data, output_file=None):
+    """Writes the JSON output either to a file or dumps it to the console."""
+    if output_file:
+        with open(output_file, 'w') as f:
+            json.dump(output_data, f, indent=4)
+        log(f"Output written to {output_file}")
+    else:
+        print(json.dumps(output_data, indent=4), file=sys.stdout)
+
+def main():
+    parser = argparse.ArgumentParser(description="Compile rust projects and generate JSON output to be used by Certora Prover.")
+    parser.add_argument("-o", "--output", metavar="FILE", help="Path to output JSON to a file.")
+    parser.add_argument("--json", action="store_true", help="Dump JSON output to the console.")
+    parser.add_argument("-l", "--log", action="store_true", help="Show log outputs from cargo build on standard out.")
+    parser.add_argument("-v", "--verbose", action="store_true", help="Be verbose.")
+    parser.add_argument("--cargo-features", nargs="+", help="Additional features to pass to cargo")
+
+
+    args = parser.parse_args()
+    global VERBOSE
+    VERBOSE = args.verbose
+
+    to_stdout = args.log
+
+    # pass extra features via env 
+    if args.cargo_features is not None:
+        env = os.environ.copy()
+        env['CARGO_FEATURES'] = ' '.join(args.cargo_features)
+    else:
+        env = None
+
+    # Compile rust project and dump the logs to tmp files
+    stdout_log, stderr_log, return_code = run_command(COMMAND, to_stdout, env)
+
+    if stdout_log is not None:
+        log(f"Temporary log file located at:\n\t{stdout_log}\nand\n\t{stderr_log}")
+
+    # JSON template
+    output_data = {
+        "project_directory": str(PROJECT_DIR),
+        "sources": SOURCES,
+        "executables": EXECUTABLES,
+        "success": True if return_code == 0 else False,
+        "return_code": return_code,
+        "log" : {"stdout": stdout_log, "stderr": stderr_log}
+    }
+
+    # Handle output based on the provided argument
+    if args.output:
+        write_output(output_data, args.output)
+
+    if args.json:
+        write_output(output_data)
+
+    # Needed for mutations: if you run _this_ script inside another script, you can check this returncode and decide what to do
+    sys.exit(0 if return_code == 0 else 1)
+
+if __name__ == "__main__":
+    main()

docs/solana/scripts/justfile

@@ -0,0 +1,14 @@
+# used by OSX, ignore otherwise
+export CPATH := env_var_or_default("CPATH", "/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include")
+
+# magic llvm flags
+export RUSTFLAGS := "-C llvm-args=--sbf-expand-memcpy-in-order -C llvm-args=--combiner-store-merging=false -C llvm-args=--combiner-load-merging=false -C llvm-args=--aggressive-instcombine-max-scan-instrs=0 -C llvm-args=--combiner-reduce-load-op-store-width=false -C llvm-args=--combiner-shrink-load-replace-store-with-store=false -C strip=none -C debuginfo=2 " + env("EXTRA_RUSTFLAGS", "") 
+
+# features used when compiling target Rust code
+export CARGO_FEATURES := env_var_or_default("CARGO_FEATURES", "")
+
+build-sbf extra_features="":
+       echo "env RUSTFLAGS=$RUSTFLAGS"
+       echo "env CARGO_FEATURES=$CARGO_FEATURES"
+       cargo +solana build-sbf --features certora {{ extra_features }} ${CARGO_FEATURES}
+

docs/solana/usage.md

@@ -0,0 +1,150 @@
+# Using the Solana Certora Prover 
+
+## Overview
+
+This document provides a guide on how to use the Solana Certora
+Prover. It details configuration formats, the build process, and how
+to execute verification locally and remotely.
+
+
+## Project Structure
+
+A typical Solana project integrated with the Solana Certora Prover includes:
+
+- A Solana smart contract written in Rust.
+
+- Configurations for running the Certora Prover in modes: running from
+  sources and verifying pre-built contracts.
+
+- An executable build script or command for compiling the project and
+  preparing it for verification.
+
+## Configuration Formats
+
+### Verifying Pre-Built Contracts
+
+This configuration mode explicitly specifies the pre-built files required for verification:
+
+```json
+{
+    "files": [
+        "solana_contract.so"
+    ],
+    "process": "sbf",
+    "optimistic_loop": false,
+    "rule": "rule_solvency"
+}
+```
+
+### Running from Sources
+
+This configuration mode uses a `build_script` or executable command for dynamic project building and eliminates hardcoded file paths:
+
+```json
+{
+    "build_script": "./certora_build.py",
+    "solana_inlining": "../../cvt_inlining.txt",
+    "solana_summaries": "../../cvt_summaries.txt",
+    "cargo_features": "<feature1> <feature2> <feature3>",
+    "process": "sbf",
+    "optimistic_loop": false,
+    "rule": "rule_solvency"
+}
+```
+
+**Key Differences:**
+
+- **Verifying Pre-Built Contracts**: Uses pre-compiled `.so` files for verification.
+
+- **Running from Sources**: Automates the build process through the
+  `certora_build.py` script or another executable
+  command. See [here](scripts/certora_build.py) for an example of such a script. 
+
+## Execution Examples
+
+### Running from Sources
+
+To run the Certora Prover using the "running from sources" configuration:
+
+```bash
+certoraSolanaProver sources_config.conf
+```
+
+**Expected Output:**
+
+```
+INFO: Building from script ./certora_build.py
+Connecting to server...
+Job submitted to server.
+Manage your jobs at <https://prover.certora.com>.
+Follow your job and see verification results at <https://prover.certora.com/output/{job_id}/{unique_key}>.
+```
+
+### Verifying Pre-Built Contracts
+
+To run the Certora Prover using the "verifying pre-built contracts" configuration:
+
+```bash
+certoraSolanaProver prebuilt_config.conf
+```
+
+**Expected Output:**
+
+```
+Connecting to server...
+Job submitted to server.
+Manage your jobs at <https://prover.certora.com>.
+Follow your job and see verification results at <https://prover.certora.com/output/{job_id}/{unique_key}>.
+```
+
+## Building the Project
+
+### Using the Build Script or Command
+
+The `certora_build.py` script or an equivalent executable command handles project compilation and prepares it for verification. Execute it as follows:
+
+```bash
+python3 certora_build.py
+```
+
+This ensures the `.so` file is up-to-date and ready for verification.
+
+### Build Script or Command Inputs and Outputs
+
+The script or command connects the project to the Certora Prover by:
+1. Compiling the project.
+2. Returning a JSON object with project details.
+3. Handling build failures appropriately.
+
+#### Inputs
+
+- `-o/--output`: Specifies the output JSON file path.
+- `--json`: Dumps JSON to the console.
+- `-l/--log`: Displays build logs.
+- `-v/--verbose`: Enables verbose mode.
+
+#### Outputs
+
+**Using `--json`**
+Prints a JSON structure to `stdout`:
+
+```json
+{
+    "project_directory": "<path>",
+    "sources": ["src/**/*.rs", "Cargo.toml"],
+    "executables": "target/release/solana_contract.so",
+    "success": true,
+    "return_code": 0,
+    "log": {
+        "stdout": "path/to/stdout",
+        "stderr": "path/to/stderr"
+    }
+}
+```
+
+**Using `--output`**
+Saves the JSON structure to the file specified by the `--output` flag.
+
+**Without `--json` or `--output`**
+Returns `0` if the build is successful and `1` otherwise.
+