| <!-- |
| 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. |
| --> |
|
|
| # Development and verification workflow |
|
|
| The project combines three verification layers around the Unlambda language. |
| Each tool checks a different artifact. Their results become a shared evidence |
| record; they do not automatically prove one another's implementations. |
|
|
| ## From mathematics to checked source |
|
|
| 1. Define the dialect, reductions, observable I/O order, resource statuses, and |
| heap invariants in `spec/`. The intended dialect is Unlambda 2.0.0. |
| 2. Write the mathematical derivation, including substitutions and intermediate |
| terms. Current I/K/S derivations are in `spec/lambda-proofs.md`. |
| 3. Encode the derivation as explicit Idris proof terms. `LambdaProofs.idr` uses |
| locally nameless terms, capture-avoiding substitution, and indexed reduction |
| witnesses. Current witnesses quantify over symbolic free atoms. |
| 4. Typecheck the proofs with totality checking. Compile and run the current |
| fuel/control model. Its output is `step: advanced`; it is not an evaluator. |
| 5. Typecheck the ATS declarations. They describe abstract handles, error results, |
| stack frames, control, I/O, fuel, and status. Implementations remain pending. |
| 6. Compile the Ada heap, run assertion-enabled boundary tests, and prove its |
| contracts with SPARK. The current heap is a capacity-64 allocation counter. |
| 7. Run the combined validation command and retain the logs for the same source |
| snapshot. Reject unproved checks and warnings in the SPARK job. |
| 8. Release the checked component scaffold with versioned source, checksums, |
| evidence, and a precise statement of what remains unimplemented. |
|
|
| ## Target architecture and current boundary |
|
|
| ```mermaid |
| flowchart LR |
| U["Unlambda program"] -. "planned parser" .-> A["ATS evaluator: planned"] |
| A -. "planned adapter" .-> H["Ada generational slot-map: planned"] |
| A -. "simulation obligation" .-> M["Idris semantic model: partial"] |
| H -. "correspondence obligation" .-> M |
| I["ATS interface declarations: checked"] --> T["ATS typechecker"] |
| C["Ada allocation counter: implemented"] --> P["GNATprove"] |
| L["Handwritten SKI derivations"] --> D["Idris proof terms: checked"] |
| T --> E["Verification evidence"] |
| P --> E |
| D --> E |
| ``` |
|
|
| Solid arrows show existing checked paths. Dotted arrows show planned runtime |
| paths or outstanding correspondence obligations. There is no AST parser, |
| continuation evaluator, generation-checked slot-map, or ATS/Ada adapter in v1. |
|
|
|  |
|
|
| ## Continuous integration |
|
|
| `idris-proofs.yml` bootstraps or restores Idris 2 from pinned upstream commit |
| `15a3e4e70843f7a34100f6470c04b791330788df`. It typechecks `LambdaProofs.idr` and |
| `Main.idr`, compiles the model, and checks its output. |
|
|
| `ats-spark.yml` has three jobs: |
|
|
| | Job | Checks | Evidence | |
| | --- | --- | --- | |
| | `ats` | ATS compiler version and both interface typechecks | `ats-validation-evidence` | |
| | `spark` | Native compilation, heap boundary tests, strict GNATprove checks | `spark-validation-evidence` | |
| | `combined` | All toolchains run the repository's `verify.sh` after the first two jobs pass | `combined-validation-evidence` | |
|
|
| The prover distribution is pinned by SHA-256 and cached before project checks. |
| The proof command uses `--mode=all --checks-as-errors=on --warnings=error |
| --report=all --level=2`, targeting `heap_model.adb`. The I/O test driver is outside |
| the SPARK proof boundary. Failures preserve the available reports for diagnosis. |
| |
| ```mermaid |
| flowchart TD |
| Push["Push or pull request"] --> ATS["ATS job"] |
| Push --> SPARK["SPARK job"] |
| Push --> Idris["Idris workflow"] |
| ATS --> Combined["Combined validation"] |
| SPARK --> Combined |
| Idris --> Review["Review source and evidence"] |
| Combined --> Review |
| Review --> Tag["Version tag on checked commit"] |
| Tag --> Package["Source and evidence archives"] |
| Package --> Hash["SHA-256 checksums"] |
| Hash --> Publish["Private GitHub release"] |
| ``` |
| |
| ## Toolchain setup |
| |
| CI's supported host is Ubuntu 24.04, Linux x86-64. The ATS package is |
| `ats2-lang=0.4.2-1.1`, Idris is 0.8.0, the native compiler is GNAT 13.3.0, and |
| the checksum-pinned GNATprove distribution is Alire 15.1.0 (reports FSF 15.0). |
| |
| For a local Linux environment, install ATS, the Ada compiler/build tool, and the |
| Idris bootstrap dependencies: |
| |
| ```sh |
| sudo apt-get update |
| sudo apt-get install -y ats2-lang=0.4.2-1.1 gnat gprbuild chezscheme build-essential libgmp-dev |
| ``` |
| |
| Follow the [official Idris installation instructions](https://github.com/idris-lang/Idris2/blob/15a3e4e70843f7a34100f6470c04b791330788df/INSTALL.md) |
| for that source commit. GNATprove can be obtained through |
| [Alire](https://alire.ada.dev/crates/gnatprove); the exact verified archive and |
| hash are in [the evidence report](verification/ats-spark-af40c4e.md). The workflow |
| files record the commands used by CI. Ensure `idris2`, `patsopt`, `gprbuild`, and |
| `gnatprove` are on PATH before running `bash verify.sh`. |
| |
| The local Windows workspace does not currently have those compiler toolchains; |
| the passing reports were produced by Linux CI. Native Windows runtime support |
| has not been established. |
| |
| ## Release and rollback |
| |
| v1 is a verification-scaffold release. Release assets include source, recorded |
| evidence, and `SHA256SUMS.txt`. Compare the hash before unpacking an asset and |
| rerun validation when changing compilers or source. |
| |
| To reproduce or return to the release source: |
| |
| ```sh |
| git fetch --tags |
| git switch --detach v1.0.0 |
| bash verify.sh |
| ``` |
| |
| A future interpreter release must pass the open gates in `DELIVERY.md`: actual |
| heap safety, all primitives and effects, differential tests, and correspondence. |
| The v1 tag does not mark those gates complete. |
| |
