PR to test CI

.github/workflows/certora-access.yml

@@ -0,0 +1,48 @@
+name: Certora verification - Access
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    access_control_integrity.conf
+    access_control_invariants.conf
+    access_control_non_panics.conf
+    access_control_panics.conf
+    access_control_revoke_role_non_panic.conf
+    ownable_integrity.conf
+    ownable_invariants.conf
+    ownable_non_panics.conf
+    ownable_panics.conf
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install rust
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Install just
+        uses: extractions/setup-just@v3
+      - name: Install soroban
+        run: |
+          cargo update -p cvlr-soroban
+          rustup target add wasm32-unknown-unknown
+      - name: run configs
+        uses: Certora/certora-run-action@v2
+        with:
+          ecosystem: soroban
+          configurations: ${{ env.CONFIGS }}
+          job-name: "Verified Soroban Rules"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          working-directory: packages/access/confs
+          cli-release: stable
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/certora-contract-utils.yml

@@ -0,0 +1,46 @@
+name: Certora verification - Contract Utils
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    math_rounding.conf
+    merkle_distributor_integrity.conf
+    merkle_distributor_panics.conf
+    pausable_integrity.conf
+    pausable_non_panics.conf
+    pausable_panics.conf
+    upgradeable_panics.conf
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install rust
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Install just
+        uses: extractions/setup-just@v3
+      - name: Install soroban
+        run: |
+          cargo update -p cvlr-soroban
+          rustup target add wasm32-unknown-unknown
+      - name: run configs
+        uses: Certora/certora-run-action@v2
+        with:
+          ecosystem: soroban
+          configurations: ${{ env.CONFIGS }}
+          job-name: "Verified Soroban Rules"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          working-directory: packages/contract-utils/confs
+          cli-release: stable
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/certora-smart-accounts.yml

@@ -0,0 +1,51 @@
+name: Certora verification - Smart Accounts
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    simple_threshold_integrity.conf
+    simple_threshold_invariants.conf
+    simple_threshold_non_panics.conf
+    simple_threshold_panics.conf
+    smart_account_integrity.conf
+    smart_account_invariants.conf
+    spending_limit_integrity.conf
+    spending_limit_invariants.conf
+    spending_limit_panics.conf
+    weighted_threshold_integrity.conf
+    weighted_threshold_invariants.conf
+    weighted_threshold_panics.conf
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install rust
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Install just
+        uses: extractions/setup-just@v3
+      - name: Install soroban
+        run: |
+          cargo update -p cvlr-soroban
+          rustup target add wasm32-unknown-unknown
+      - name: run configs
+        uses: Certora/certora-run-action@v2
+        with:
+          ecosystem: soroban
+          configurations: ${{ env.CONFIGS }}
+          job-name: "Verified Soroban Rules"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          working-directory: packages/accounts/confs
+          cli-release: stable
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/certora-token-fungible.yml

@@ -0,0 +1,46 @@
+name: Certora verification - Token - Fungible
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    allowlist.conf
+    blocklist.conf
+    burnable.conf
+    capped.conf
+    fungible_integrity.conf
+    fungible_invariants.conf
+    fungible_panics.conf
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install rust
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Install just
+        uses: extractions/setup-just@v3
+      - name: Install soroban
+        run: |
+          cargo update -p cvlr-soroban
+          rustup target add wasm32-unknown-unknown
+      - name: run configs
+        uses: Certora/certora-run-action@v2
+        with:
+          ecosystem: soroban
+          configurations: ${{ env.CONFIGS }}
+          job-name: "Verified Soroban Rules - Fungible"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          working-directory: packages/tokens/confs
+          cli-release: stable
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/certora-token-non-fungible.yml

@@ -0,0 +1,48 @@
+name: Certora verification - Token - Non-Fungible
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    consecutive.conf
+    enumerable_mint_burn_integrity.conf
+    enumerable_transfer_integrity.conf
+    non_fungible_burnable.conf
+    non_fungible_integrity.conf
+    non_fungible_invariants.conf
+    non_fungible_non_panics.conf
+    non_fungible_panics.conf
+    royalties.conf
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install rust
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Install just
+        uses: extractions/setup-just@v3
+      - name: Install soroban
+        run: |
+          cargo update -p cvlr-soroban
+          rustup target add wasm32-unknown-unknown
+      - name: run configs
+        uses: Certora/certora-run-action@v2
+        with:
+          ecosystem: soroban
+          configurations: ${{ env.CONFIGS }}
+          job-name: "Verified Soroban Rules - Non-Fungible"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          working-directory: packages/tokens/confs
+          cli-release: stable
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/certora-token-rwa.yml

@@ -0,0 +1,46 @@
+name: Certora verification - Token - RWA
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    claim_topics_and_issuers.conf
+    identity_claims.conf
+    identity_registry_storage.conf
+    identity_verifier_integrity.conf
+    rwa_integrity.conf
+    rwa_panics.conf
+    token_binder_integrity.conf
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install rust
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Install just
+        uses: extractions/setup-just@v3
+      - name: Install soroban
+        run: |
+          cargo update -p cvlr-soroban
+          rustup target add wasm32-unknown-unknown
+      - name: run configs
+        uses: Certora/certora-run-action@v2
+        with:
+          ecosystem: soroban
+          configurations: ${{ env.CONFIGS }}
+          job-name: "Verified Soroban Rules - RWA"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          working-directory: packages/tokens/confs
+          cli-release: stable
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/certora-token-vault.yml

@@ -0,0 +1,43 @@
+name: Certora verification - Token - Vault
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    vault_64_conversions.conf
+    vault_64_integrity.conf
+    vault_64_panics.conf
+    vault_64_invariants.conf
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install rust
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Install just
+        uses: extractions/setup-just@v3
+      - name: Install soroban
+        run: |
+          cargo update -p cvlr-soroban
+          rustup target add wasm32-unknown-unknown
+      - name: run configs
+        uses: Certora/certora-run-action@v2
+        with:
+          ecosystem: soroban
+          configurations: ${{ env.CONFIGS }}
+          job-name: "Verified Soroban Rules - Vault"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          working-directory: packages/tokens/confs
+          cli-release: stable
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.gitignore

@@ -1,8 +1,15 @@
+# certora
+.certora_internal
+emv-*
+local.conf
+*.wat
+
 **/target/
 /.idea
 .DS_Store
 .thumbs.db
 .vscode
+.cursorrules
 
 # These are backup files generated by rustfmt
 **/*.rs.bk

CERTORA.md

@@ -0,0 +1,23 @@
+# Formal Verification Using Certora's Sunbeam Prover for Stellar Smart Contracts
+
+We used Certora's Sunbeam prover to formally verify various parts of the code in this library. This document
+explains how we have organized the work and how to run the prover, including helpful links. For a detailed summary of the work, please refer to the formal verification report.
+
+## Installation
+
+To install Certora's Sunbeam prover, see the documentation [here](https://docs.certora.com/en/latest/docs/sunbeam/installation.html). You can find a tutorial and troubleshooting details in our [documentation page](https://docs.certora.com/en/latest/docs/sunbeam/index.html).
+
+## Project layout
+
+- Within each package, we have included a new `confs` directory that
+  has the configuration files needed to run the verification jobs.
+- For each component, we have also included a designated `specs` directory
+  that has the formal properties we wrote, any helpers, and mocks we used for verification.
+- In the case of `vault`, we have created a 64 bit version (`vault_64`) to help scale formal verification. We also have introduced a 64 bit version of `math` which can be found here: `math/math_64`.
+- For each package, we also have a `justfile` for compiling the code with the right version of the rust compiler and required feature flags. You can run `just build` to compile and generate the wasm bytecode.
+- For each package, we also have a `certora_build.py` file that we use for running the verification jobs. You should rarely need to run this script manually.
+
+## Looking at results and running the prover
+
+- In each spec file, we have included a link to the verification job above each formal specification `#[rule]`. You can click on this link and see the results. Specifically, you can look at the `run.conf` file available in the link to see how exactly we ran the prover and what flags we used.
+- We also have provided various `.conf` files to run the jobs. You can try them by running `certoraSorobanProver name.conf`. Note however that we sometimes run the rules individually and we do not include conf files for each individual rule separately. We recommend referring to the run links in the source code or the report for exact reproducibility.