CONTRIBUTING.md

Contributing to Security Envelopes

Thank you for your interest in contributing. This document describes setup, expectations, and how to run the same checks as CI.

Table of Contents

• Code of Conduct
• Getting Started
• Development Setup
• Contributing Guidelines
• Pull Request Process
• Code Standards
• Testing
• Documentation
• Security
• Questions and Support

Code of Conduct

This project and everyone participating in it is governed by our Code of Conduct. By participating, you are expected to uphold this code.

Getting Started

Prerequisites

• Lean — lean-toolchain; install via elan
• Rust — rust-toolchain.toml (currently 1.88)
• Python 3.12+ — bundle tooling via pyproject.toml
• Node.js 18+ — only if you work on bindings/node; CI validates the crate with cargo check
• Go 1.21+ — only if you work on bindings/go
• Docker — optional; see docker-compose.jepsen.yml and Dockerfiles in the repo root

Development Setup

1. Fork and clone

   git clone https://github.com/your-username/security-envelopes.git
   cd security-envelopes

2. Install dependencies

   # Lean (elan)
   curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
   
   # Rust (rustup)
   curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
   
   # Python (editable install for the bundle package)
   pip install -e ".[dev]"
   
   # Node bindings (optional): align Neon/npm with the crate before `npm install`

3. Build

   lake build
   cargo fmt --check
   cargo clippy --workspace --all-targets -- -D warnings
   cargo build

4. Run checks

   lake exe test_rbac && lake exe test_tenant && lake exe test_attest
   cargo test --workspace
   ruff check bundle scripts tests
   pytest tests/ -v

Pre-commit (recommended)

Install pre-commit and enable hooks once per clone:

pip install pre-commit
pre-commit install
pre-commit run --all-files

Architecture overview

See docs/ARCHITECTURE.md and the doc index docs/README.md.

Contributing Guidelines

Types of contributions

• Formal specifications (Lean)
• Policy engine (Rust / WASM)
• Language bindings (Go, Node, Python)
• Compliance bundle and tooling (Python)
• Documentation and tests
• CI and developer experience

Before you start

1. Search existing issues and PRs
2. For larger changes, open an issue to agree on direction
3. Match existing style and abstractions in the area you touch

Pull Request Process

Creating a pull request

1. Branch

   git checkout -b feature/your-feature-name

2. Change, test, document — see Testing and Documentation.

3. Verify locally (same categories as CI)

   lake build
   lake exe test_rbac && lake exe test_tenant && lake exe test_attest
   cargo fmt --check
   cargo clippy --workspace --all-targets -- -D warnings
   cargo test --workspace
   ruff check bundle scripts tests
   pytest tests/

   Optional, when relevant:

   cargo deny check
   cargo audit

4. Commit — Conventional commits are preferred.

5. Push and open a PR against the default branch.

Pull request expectations

• Clear title and description
• Tests or specs updated when behavior changes
• Docs updated when user-facing behavior or workflows change
• Security-sensitive changes: describe threat model and review needs in the PR

Review process

1. Automated workflows must pass (see docs/ARCHITECTURE.md)
2. Maintainer review as needed for the area

Code Standards

General principles

• Prefer small, reviewable changes
• Security-sensitive paths deserve explicit review and tests
• Document public APIs and non-obvious invariants
• Avoid committing secrets, tokens, or large generated artifacts unless the repo already tracks them intentionally

Language-specific notes

Lean

Use clear names and module structure consistent with Spec/. Prefer Mathlib idioms already used in the tree.

Rust

The main crate is policyengine (engine/). Use cargo clippy with -D warnings before pushing.

Python

Type hints and ruff/pytest as configured in pyproject.toml.

Commit message format

Conventional style:

type(scope): description

[optional body]

Common types: feat, fix, docs, style, refactor, test, chore.

Testing

What to run

Area	Command
Lean smoke	lake exe test_rbac, lake exe test_tenant, lake exe test_attest
Rust	cargo test --workspace (narrow with cargo test -p policyengine)
Python	pytest tests/
Policy YAML	python scripts/policy_lint.py examples/*/policy.yaml

Chaos / Jepsen helpers under chaos-scripts/ are optional and environment-specific.

Documentation

Keep these aligned when you change workflows, layout, or formal specs:

File	Purpose
README.md	Overview and quick start
docs/README.md	Documentation index
docs/ARCHITECTURE.md	Components and CI
TRACEABILITY.md	Lean ↔ Rust / automation
SECURITY.md	Reporting and supply chain
scripts/README.md	Policy linter

Security

• Do not open public issues for undisclosed vulnerabilities; see SECURITY.md.
• Follow secure dependency practices; Cargo.lock is tracked for reproducible Rust builds.

Questions and support

Use GitHub issues for bugs and feature requests. For broader design discussion, use GitHub Discussions if enabled on the repository.

Recognition

Contributors are credited via GitHub and release notes when applicable.

Thank you for contributing.