Contributing
This public, proprietary source-visible repository develops a combined Unlambda/ATS/Idris/SPARK verification scaffold. Review LICENSE before proposing contributions. Start with the workflow, current evidence, and delivery gates.
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.
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 Assumeor 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.shis 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. 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, rather than a normal issue or pull request.