Contributing to Soteria #

Thank you for your interest in contributing to Soteria! This document provides guidelines and instructions for contributing to the project.

Soteria is developed and maintained by Soteria Tools Ltd. The core team makes final decisions on project direction, but we value community input and aim to be transparent about our decision-making process.

Table of Contents #

• Getting Started
• Development Setup
• Code Style and Formatting
• Testing
• Submitting Changes
• Coding Guidelines
• Contributor License Agreement

Getting Started #

1. Fork the repository on GitHub
2. Clone your fork locally:

   git clone https://github.com/<your-username>/soteria.git
   cd soteria
   

3. Set up the development environment (see Development Setup)
4. Create a branch for your changes:

   git checkout -b my-feature-branch
   

Development Setup #

Prerequisites #

• OCaml >= 5.4.0 with opam
• Z3 (SMT solver)
• For Soteria Rust: Rust nightly and Obol or Charon

Setting Up the Environment #

1. Install OCaml dependencies:

   Create a local opam switch with all development dependencies:

   make switch
   

   This installs:

   • All project dependencies
   • ocamlformat (code formatter)
   • ocaml-lsp-server (IDE support)
   • odig (documentation tools)

   If you already have a switch, install dependencies with:

   make ocaml-deps
   

2. Install Rust frontends (for Soteria Rust development):

   Use the versionsync script to automatically install both Obol and Charon at the correct commits:

   ./scripts/versionsync.py pull all --init
   

   This will:

   • Clone the repositories in ../obol and ../charon
   • Check out the correct commit hashes from scripts/versions.json
   • Build both frontends

   To update the frontends to the latest configured versions:

   ./scripts/versionsync.py pull all
   

   See the README for manual installation instructions.

Building #

dune build         # Build the project
dune test          # Run all tests (requires both Rust frontends)
dune build @doc    # Build documentation

To run tests without Rust frontends installed:

dune test soteria      # Core library tests only
dune test soteria-c    # Soteria-C tests only

Code Style and Formatting #

OCaml Formatting #

We use ocamlformat to ensure consistent code style, please make sure you have the correct version installed (see .ocamlformat).

Formatting Your Code #

Before committing, format your code:

dune fmt

To check if your code is properly formatted (without modifying files):

dune build @fmt

The CI will reject PRs with improperly formatted code.

Testing #

Running Tests #

To run all tests (requires both Rust frontends to be installed):

dune test

To run tests for specific packages without Rust frontends:

dune test soteria      # Core library tests only
dune test soteria-c    # Soteria-C tests only

Writing Tests #

• Place tests alongside the code they test or in a dedicated test/ directory
• Use Alcotest for unit test
• Use cram testing for end-to-end tests.
• Ensure new features have corresponding tests
• Ensure bug fixes include a regression test

Testing Soteria Rust #

For Soteria Rust specific testing:

# Run against the Kani test suite
soteria-rust/scripts/test.py kani

# Run against the Miri test suite
soteria-rust/scripts/test.py miri

Upgrading versions #

If you want to upgrade a version, say of OCaml, see ./scripts/versionsync.py list to see current versions and ./scripts/versionsync.py set OCAML_VERSION X.Y.Z to update it accross all its references in the repo.

Submitting Changes #

Before Submitting #

1. Format your code: Run dune fmt
2. Run tests: Ensure all tests pass with dune test (or dune test soteria soteria-c if you don't have Rust frontends)
3. Check formatting: Run dune build @fmt

Pull Request Process #

1. Push your branch to your fork
2. Open a Pull Request against main
3. Fill out the PR description explaining your changes. Explain what and why, not just how.
4. Wait for CI to pass
5. Address any review feedback

Coding Guidelines #

Exception Handling #

The library and executables should never raise uncaught exceptions unless they correspond to an internal error that should be fixed in the tool.

Acceptable exceptions:

• Patterns that are believed to be unreachable (assertions for invariants)
• Internal errors that indicate bugs in Soteria itself

Unacceptable exceptions:

• User input errors (use Result types instead)
• Expected edge cases in analyzed code

Error Handling Best Practices #

• Use Result types for operations that can fail due to user input
• Use Option for values that may or may not be present
• Reserve exceptions for truly exceptional circumstances (bugs)

Contributor License Agreement #

Before we can accept your contribution, you must agree to our Contributor License Agreement.

By opening a pull request, you confirm that:

• You have read and accepted the terms of the CLA
• You have the right to submit the contribution
• Your contribution is compatible with the Apache-2.0 license

This ensures that we can safely incorporate your contribution into the project.

Questions? #

• Visit our website for more information
• Join our Zulip chat for questions and discussions
• Open an issue on GitHub for bug reports or feature requests