Skip to content

Latest commit

 

History

History
195 lines (153 loc) · 9.18 KB

File metadata and controls

195 lines (153 loc) · 9.18 KB

Contribute to RAES

RAES SDL is a research-oriented engineering project. Contributions are useful when they make the language, reference implementation, contracts, examples, or documentation more precise and easier to validate.

Choose the right route

  • For a small docs fix, typo fix, or narrow test improvement, a pull request is enough. Use No issue: <brief reason> in its Related Issues section.
  • For SDL language changes, contract changes, processor behavior changes, or backend conformance changes, open an issue first and reference it with a standalone Refs #N line when the issue's Requirements section declares requirement UIDs, or Closes #N otherwise. Those changes can affect authored scenario meaning and generated artifacts.
  • Keep unrelated work in separate pull requests.
  • Base pull requests on dev, not main. main is the stable release line; dev is the integration branch.

Requirement-backed issues stay open at merge. The delivery workflow verifies the merged requirement status and traceability, records its final report, and then closes the issue. The body guard checks scope from the linked issue, not from a self-declaration in the PR.

Pull request bodies use the section structure that the Ground Control delivery workflow renders, so a rendered body passes the body guard unmodified. The pull request template lists the sections: Summary, Requirement UIDs, Related Issues, ADR Impact, Changes, Test Plan, Ground Control Checks, Traceability, and Checklist, plus an optional Documentation section. Each required section appears exactly once and has content. The guard also enforces the following rules:

  • The Summary describes the change in non-placeholder prose.
  • Related Issues declares exactly one tracking route: standalone Refs #N or Closes #N lines, or one substantive No issue: declaration.
  • The Test Plan records the commands run and their outcomes, or a reason a check was not run. Checklist items alone are not evidence.
  • No other part of the body uses a GitHub closing reference: a closing keyword such as fixes or closes, directly followed by a reference to an issue in this repository. GitHub reads that as a closing route, so reword the mention, for example as "the issue 1219 migration". Other issue mentions are accepted.

The body guard normally executes the validator from the PR's base revision. A policy migration admits exactly one prior validator digest and a pinned two-file validator bundle, with an independent SHA-256 check of each Git blob before execution. This lets the introducing PR be validated without executing PR-head code or bypassing policy. Once the replacement lands on dev, the prior digest no longer matches and the normal base-validator path applies. Changing these migration pins is an explicit, reviewable workflow trust change.

Set up the repository

An optional development container provides automated setup for the reviewed x86_64 image. The guide labels each start route verified or unverified, and records the evidence behind those labels. The container cannot run the Isabelle proof lane; CI runs that gate.

To set up natively instead:

Prerequisites:

  • a standard CPython 3.11, 3.12, 3.13, or 3.14 payload admitted by the development profile; 3.14t is preview-only
  • the exact uv payload selected by the development artifact lock

The host profile also requires Git, trusted CA roots, SHA-256 tooling, GH CLI when GitHub operations are used, and curl 8.4.0 or newer with verified unknown-length size enforcement. An older client is a hard failure for generic artifact acquisition. Provision native prerequisites from the reviewed host image or signed package repositories. Connected setup acquires exact Python, uv and generic-tool inputs against their reviewed identities. Do not pipe a remote installer into a shell.

Install the separate locked project and verification-tool environments:

git clone https://github.com/OpenRAE/rae.git
cd rae
uv sync --project implementations/python --all-extras --frozen
uv sync --project implementations/tooling/python --frozen --no-default-groups

Specialized TLS acquisition fixtures use the tooling acquisition-tests dependency group; ordinary tooling sync does not need it. The existing Intel Mac restriction is not lifted by that separation: patched runtime dependencies and actual target smoke evidence are still required. No vulnerable dependency downgrade or untested support is implied.

The developer documentation index links to architecture, research, migration, release, and workflow records that are not part of the hosted reader guide.

Make a change

  1. Fork the repository and create a branch from dev.
  2. Make the smallest coherent change that solves the issue.
  3. Add or update tests when behavior changes.
  4. Update examples, schemas, contracts, or documentation when the public surface changes.
  5. For public docs changes, follow docs/explain/reference/documentation-style-guide.md.
  6. Use a Conventional Commit PR title, such as feat: or fix:. Release Please reads that title.
  7. Run the relevant checks locally.
  8. Open a pull request against dev with a concrete description of what changed and why.

Run the checks

Commit hooks run file-scoped hygiene and secrets checks: whitespace, final newlines, YAML/JSON syntax, file size, conflict markers, private keys, and Gitleaks. No pre-push check is configured. Full tests, policy, contracts, lint, proof, and documentation validation remain required in CI/CD.

The full repository gate is available locally when needed:

uv run --project implementations/tooling/python --frozen --no-default-groups nox -f noxfile.py -s verify

That gate includes a participant-opacity-proof lane, which replays the pinned Isabelle proof offline. The lane runs on Linux x86_64 only. It needs bubblewrap to enforce the offline replay, and a fontconfig setup with at least one installed font, because Isabelle starts a JVM that will not run without one:

sudo apt-get install bubblewrap fontconfig fonts-dejavu-core

Acquire the pinned Isabelle distribution once before running the lane. The tool admits the exact reviewed archive with a qualified curl (8.4.0 or newer) and verifies the complete installed tree on every use:

uv run --project implementations/tooling/python --frozen --no-default-groups python -m tools.isabelle_tool acquire

On a host whose curl is older, such as Ubuntu 22.04, pass an archive you already have with --local-input PATH. The tool admits it only when its size and SHA-256 match the lock. An approved mirror is selected explicitly with --locator-ref official-isabelle-cambridge-mirror. To list every missing proof prerequisite without network access or execution, run python -m tools.isabelle_tool preflight.

The proof tool checks the fontconfig runtime and the C.UTF-8 locale before entering the sandbox, and it reports a missing prerequisite separately from a kernel rejection. Run the gate on Linux, or rely on continuous integration, when your workstation is another platform.

Some Linux security policies also deny unprivileged user or network namespaces. The proof tool reports that condition as unavailable bubblewrap isolation and does not retry without the network sandbox. Use an administrator-approved host policy for bubblewrap or rely on continuous integration; do not disable the offline boundary to make the lane pass.

Run the change-aware local gate while iterating:

uv run --project implementations/tooling/python --frozen --no-default-groups nox -f noxfile.py -s verify-changed

It runs changed-file checks and directly changed test modules against the branch's upstream ref. Uncertain classification never triggers a full local suite. Select relevant test modules or cases explicitly for source-only changes. Full test, integration, fuzz and completion suites run in CI/CD only. The unconditional verify graph remains a CI/CD entry point.

Useful narrower sessions:

uv run --project implementations/python --frozen pytest implementations/python/tests/test_runtime_models.py -q
uv run --project implementations/tooling/python --frozen --no-default-groups nox -f noxfile.py -s docs
uv run --project implementations/tooling/python --frozen --no-default-groups nox -f noxfile.py -l

Run targeted checks for the changes you make. CI/CD runs the full gate before merge, including language, contract, generated-artifact, and shared-runtime checks.

Let Release Please write the changelog

CHANGELOG.md is generated by release-please from the Conventional Commit history on main; do not hand-edit it or add changelog fragments. The Conventional Commit PR title is the entry release-please reads. See docs/explain/releasing.md.

Report security issues privately

Do not open public issues for suspected security vulnerabilities. See SECURITY.md.

Follow the community rules

Participation in this project is covered by CODE_OF_CONDUCT.md.