First attempt at PR & CI

.github/workflows/certora-access.yml

@@ -0,0 +1,50 @@
+name: Certora verification
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    access_control_integrity.conf
+    access_control_invariants.conf
+    access_control_non_panics.conf
+    access_control_revoke_role_non_panic.conf
+    access_control_panics.conf
+    access_control_sanity.conf
+    ownable_integrity.conf
+    ownable_invariants.conf
+    ownable_non_panics.conf
+    ownable_panics.conf
+    ownable_sanity.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,49 @@
+name: Certora verification
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    math_integrity.conf
+    math_non_panics.conf
+    math_panics.conf
+    math_sanity.conf
+    merkle_distributor_contract_sanity.conf
+    merkle_distributor_integrity.conf
+    pausable_integrity.conf
+    pausable_non_panics.conf
+    pausable_panics.conf
+    pausable_sanity.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,47 @@
+name: Certora verification
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    simple_threshold_integrity.conf
+    simple_threshold_non_panics.conf
+    simple_threshold_panics.conf
+    simple_threshold_contract_sanity.conf
+    weighted_threshold_integrity.conf
+    weighted_threshold_contract_sanity.conf
+    spending_limit_integrity.conf
+    spending_limit_contract_sanity.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.yml

@@ -0,0 +1,53 @@
+name: Certora verification
+
+on: pull_request
+
+env:
+  CONFIGS: |
+    fungible_integrity.conf
+    fungible_invariants.conf
+    fungible_non_panics.conf
+    fungible_panics.conf
+    fungible_sanity.conf
+    allowlist.conf
+    blocklist.conf
+    burnable.conf
+    burnable_nft_sanity.conf
+    capped.conf
+    consecutive_nft_sanity.conf
+    enumerable_nft_sanity.conf
+    royalties_nft_sanity.conf
+    vault_sanity.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@9596198c77a3f33d22c59226ff7757185a504f8f
+        with:
+          ecosystem: soroban
+          configurations: ${{ env.CONFIGS }}
+          job-name: "Verified Soroban Rules"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          working-directory: packages/tokens/confs
+          cli-release: stable
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.gitignore

@@ -1,11 +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
@@ -19,10 +23,6 @@ ENV/
 env.bak/
 venv.bak/
 
-# Documentation
-docs/node_modules
-docs/build
-
 # Code Coverage
 htmlcov/
 lcov.info

Architecture.md

@@ -26,7 +26,6 @@ stellar-contracts/
 │       │   └── non_fungible/    # Non-fungible token implementation
 │       └── lib.rs
 ├── examples/                    # Example contract implementations
-├── docs/                        # Documentation
 └── audits/                      # Security audit reports
 ```
 

CONTRIBUTING.md

@@ -47,11 +47,14 @@ As a contributor, you are expected to fork this repository, work on your own for
     # run tests
     cargo test
 
+    # build
+    cargo build --target wasm32v1-none --release
+
     # run linter
     cargo clippy --all-targets --all-features -- -D warnings
 
     # run formatter
-    cargo fmt --all -- --check
+    cargo +nightly fmt --all -- --check
 
     # run documentation checks
     cargo doc --all --no-deps