| <!-- |
| Copyright (c) 2026 Ahmad Ali Parr. All rights reserved. |
| SPDX-License-Identifier: LicenseRef-Proprietary |
| Public source visibility does not grant an open-source license. See LICENSE. |
| --> |
|
|
| # Contributing |
|
|
| This public, proprietary source-visible repository develops a combined Unlambda/ATS/Idris/SPARK |
| verification scaffold. Review [LICENSE](LICENSE) before proposing contributions. Start with the |
| [workflow](docs/WORKFLOW.md), [current evidence](docs/verification/ats-spark-af40c4e.md), |
| and [delivery gates](docs/DELIVERY.md). |
|
|
| ## Work on a reviewable increment |
|
|
| Open an issue describing the behavior or proof obligation, then use a focused |
| branch. An implementation change should include a test of observable behavior |
| or a constructive proof of the changed invariant. Documentation-only changes |
| should have working links and accurate scope statements. |
|
|
| ```sh |
| git switch -c change/describe-the-increment |
| # Edit source, specifications, and relevant tests or proofs. |
| bash verify.sh |
| git add <changed-files> |
| git commit -m "Describe the resulting behavior" |
| git push -u origin change/describe-the-increment |
| ``` |
|
|
| Create a pull request with the concrete problem, resulting behavior, checked |
| commands/CI runs, and any remaining proof obligations. Reference the gate it |
| advances. Do not mark a runtime gate complete from interface checks alone. |
|
|
| ## Proof and safety rules |
|
|
| - Keep handwritten derivations and Idris witnesses consistent. State the |
| quantified operand class and every required substitution lemma. |
| - Keep Idris proof-bearing definitions total. Do not use `believe_me`, |
| `assert_total`, `assert_smaller`, missing proof holes, or equivalent bypasses. |
| - Do not introduce `pragma Assume` or suppress required SPARK checks. Strengthen |
| contracts and supply loop invariants when needed; retain unproved-check failures. |
| - Preserve distinct `OutOfFuel`, `OutOfMemory`, failure, and successful statuses. |
| - Do not dereference a future node handle without generation-checked lookup. |
| - Preserve input/output ordering and record effects in explicit machine state. |
| - Add runtime code only with its actual compiler and behavioral checks. Abstract |
| ATS declarations do not establish implementation or FFI correctness. |
| - Never source unreviewed agent hooks. `agent_hooks.example.sh` is an example, |
| not an active proof-generation agent or a release gate. |
|
|
| The source scanner is a guardrail. Compiler/prover evidence and review are still |
| required. Do not invent coverage percentages, certification seals, or claims |
| that one language's tool verifies the other language's implementation. |
|
|
| ## Review checklist |
|
|
| - The change explains its observable behavior and proof boundary. |
| - Specs and implementation agree; provenance and dependency versions are recorded. |
| - Relevant CI passes on the proposed source snapshot. |
| - Required checks are not skipped, assumed, or downgraded. |
| - Reports and release notes distinguish checked scope from future work. |
| - Contributions identify their authorship and any third-party license obligations. |
|
|
| Original project code is proprietary and source-visible, not open source; |
| see [LICENSING.md](LICENSING.md). Do not assume a copyright transfer or commercial |
| relicensing grant. Discuss the applicable contribution terms with the maintainer |
| before contributing third-party material. Report sensitive issues through |
| [SECURITY.md](SECURITY.md), rather than a normal issue or pull request. |
|
|
