Mirrored from https://github.com/SNAPKITTYWEST/unlambda-idris-spark at commit
a42eccc. Part of the SnapKitty October 2026 main drop.
Unlambda + ATS + Idris 2 + SPARK
Handwritten lambda-calculus derivations, checked proof terms, and explicit verification boundaries.
v1.0.0 packages a verification scaffold for a combined Unlambda/ATS/Idris/SPARK architecture. It includes compiler-checked ATS interfaces, handwritten SKI derivations formalized in Idris 2, and a SPARK-proved bounded allocation counter. The full ATS interpreter, generational heap, and cross-language correspondence are future work. This release makes the existing evidence easy to reproduce.
What is checked
| Layer | Current result | Boundary |
|---|---|---|
| ATS/Postiats 0.4.2 | Both .sats interfaces typecheck |
Runtime implementations and adapter are pending |
| Idris 2 0.8.0 | SKI proof terms and fuel model typecheck | SKI witnesses cover symbolic free atoms; control model is a stub |
| GNAT/Ada | Heap compiles and passes capacity/exhaustion/reset tests | Heap counts allocations; it does not yet store nodes |
| SPARK/GNATprove | Six checks discharged, zero unproved | Current allocation-counter contracts only |
| Combined CI | verify.sh passes with all toolchains |
Full runtime certification remains open |
The counter badge links a recorded source snapshot. CI badges show the current branch. Verification evidence records the source hashes, versions, proof results, and limitations.
How the workflow fits together
flowchart TD
Spec["Unlambda semantics and invariants"] --> Hand["Handwritten SKI beta derivations"]
Hand --> Idris["Idris proof terms and control model"]
Spec --> ATS["Typed ATS interfaces"]
Spec --> Ada["Ada allocation-counter contracts"]
Idris --> IC["Idris typecheck, build, smoke test"]
ATS --> AC["ATS interface typecheck"]
Ada --> SC["Ada tests and SPARK proof checks"]
IC --> Evidence["Source-pinned verification evidence"]
AC --> Evidence
SC --> Evidence
Evidence --> Combined["Combined verify.sh validation"]
Combined --> Release["v1 verification-scaffold release"]
Evidence -. "future work" .-> Runtime["ATS runtime, slot-map heap, correspondence"]
SPARK verifies the Ada contracts; Idris checks its own proof terms. Agreement between an ATS runtime, Ada implementation, and Idris semantics will require a checked adapter and a separate simulation/correspondence argument. See the full workflow and delivery backlog.
Reproduce the checks
Use Linux x86-64 with Bash, GNU grep, ATS/Postiats, Idris 2, GNAT, GPRbuild, and GNATprove installed. Toolchain versions and setup match the CI configuration.
gh repo clone AHMADALIPARR/unlambda-idris-spark
cd unlambda-idris-spark
bash verify.sh
The repository is public and source-visible; it is proprietary, not open source. A passing run checks the ATS declarations, typechecks and compiles the Idris model, runs the Ada tests, and requires GNATprove to discharge the heap checks. The success message names that component scope explicitly.
Repository map
| Path | Purpose |
|---|---|
ats/ |
Typed heap and machine interfaces |
idris/LambdaProofs.idr |
Explicit beta-reduction witnesses and substitution cases |
idris/Main.idr |
Fuel/control model and resource-status proof terms |
ada/ |
Bounded allocation counter, contracts, assertion-enabled test driver |
spec/ |
Semantics, invariants, handwritten derivations |
docs/verification/ |
Recorded compiler and prover evidence |
docs/source-sketches/ |
Original supplied shorthand interfaces |
.github/workflows/ |
Idris and ATS/SPARK/combined validation jobs |
Contribute, report, and support
- Contributing: meaningful changes, proof obligations, and review criteria.
- Security: private reporting and supported scope.
- Licensing: current licensing status and provenance boundaries.
- Commercial licensing: inquiries and required agreement details.
- Support and donations: ways to help; payment destination is awaiting confirmation.
- v1.0.0 release notes and changelog.
The cover and supporting photographs are AI-generated conceptual illustrations, not proof evidence or screenshots of an implemented interpreter. Image provenance and the exact generation prompts are in the asset notes.
💼 Commercial License
This repository is published under a proprietary source-visible license. Building a commercial product or service? A proprietary commercial license from Snapkitty Collective LLC lets you ship this code on terms other than a proprietary source-visible license.