| <!-- |
| 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. |
| --> |
|
|
| # Delivery workflow |
|
|
| Lead: Codex, during active working sessions. Product owner: repository owner. |
| Status: v1.0.0 verification-scaffold packaging; implementation continues and no |
| production interpreter release is certified. |
|
|
| ## Working cycle |
|
|
| 1. Select the next unmet gate and record its concrete acceptance criteria. |
| 2. Implement a reviewable increment with tests of observable behavior. |
| 3. Compile and run the tests; collect proof reports where applicable. |
| 4. Commit the increment and update this ledger with evidence and blockers. |
| 5. Release only after all required gates pass on the release commit. |
|
|
| ## Backlog and acceptance gates |
|
|
| | Gate | Work | Required evidence | State | |
| | --- | --- | --- | --- | |
| | 0 | Combined ATS runtime, Idris semantic proofs, SPARK heap; freeze platform, dialect and licensing | Product decisions; authoritative semantics; license provenance | Architecture confirmed; remaining decisions open | |
| | A | Bounded slot-map heap with generations | Allocation exhaustion, reuse, stale lookup/update, invariant tests | Open | |
| | B | Parser and core machine: s,k,i,v,d,output,newline | Compiler success; strictness, delay, output order, fuel tests | Open | |
| | C | Continuations, exit and input primitives | Capture/restore, EOF, current-character, input order tests | Open | |
| | D | Independent reference comparisons | Pinned reference; byte-for-byte output and termination corpus | Open | |
| | E | GC, if required for release | Root tracing, continuation retention, stale-reference safety | Open | |
| | R | Packaging and production release | Clean builds; CI; installation smoke test; version/checksums; rollback instructions | Open | |
|
|
| ## Current assessment |
|
|
| - Idris `stepControl` consumes fuel but does not evaluate terms. |
| - Ada heap is an allocation counter; it has no node slots or generation handles. |
| The counter implementation compiles, passes exhaustion/reset tests, and has |
| all six GNATprove checks discharged. |
| - ATS files are now typed, compiler-validated interfaces. There are no ATS |
| runtime implementations or heap adapter yet. |
| - No executable Unlambda interpreter exists yet. The Idris control-model |
| executable now builds and passes a smoke test in CI. |
| - Private GitHub repository and `origin` configured: |
| https://github.com/AHMADALIPARR/unlambda-idris-spark. |
| The owner explicitly approved the push; the Idris workflow is active. |
| - ATS, Idris 2, and GNATprove are absent from the current PATH. Git's bundled |
| Bash is available at `C:/Program Files/Git/bin/bash.exe`. |
| - WSL has no usable installed distribution in the current environment. |
|
|
| ## Definition of done |
|
|
| A runtime increment must compile and pass behavior and resource-boundary tests. |
| A proof increment must produce checked proof evidence; a source scan is insufficient. |
| A release must include a documented supported platform, CLI contract, resource |
| limits, tested installation, reproducible build instructions, license/provenance, |
| and a recorded passing release-gate result. Design documents alone do not pass a gate. |
|
|
| ## Next increment |
|
|
| Architecture confirmed by the owner: ATS runtime, handwritten lambda-calculus |
| derivations formalized in Idris 2, and SPARK-verified heap contracts. The Idris |
| program/models must typecheck. Begin with the explicit SKI proof terms and |
| compiler workflow, then implement gate A before connecting the core machine. |
| Production platform and packaging remain to be decided. |
|
|
| ## Proof increment |
|
|
| - Handwritten I/K/S beta derivations recorded in `spec/lambda-proofs.md`. |
| - Explicit indexed reduction witnesses written in `idris/LambdaProofs.idr`. |
| - Capture-avoidance boundary cases expressed as equality proofs. |
| - Corrected the original fuel theorem's successor inequality; added explicit |
| `OutOfMemory` and exact fuel-consumption obligations. |
| - CI definition bootstraps pinned Idris 2 and retains typechecker logs. |
| - Local whitespace and Bash syntax checks pass; source scan finds no prohibited |
| proof escape hatches in Idris, Ada, or ATS files. |
| - GitHub upload completed after the owner's explicit approval. |
| - Idris 2 0.8.0 typechecked the lambda proofs and control model, compiled the |
| model program, and passed its smoke test at commit `bb9abcc`. |
| [Recorded evidence](verification/idris-bb9abcc.md) links the successful run. |
| - SPARK proves the allocation-counter heap's current contracts. The generation |
| slot-map required by gate A is still open. |
| - ATS interface validation passes; the ATS runtime, correspondence, and |
| production packaging remain open. |
|
|
| ## ATS/SPARK validation increment |
|
|
| - Replaced invalid ATS shorthand with typed interfaces; preserved originals. |
| - Strengthened allocation's contract to require success whenever capacity remains. |
| - Added assertion-enabled tests for all 64 allocations, exhaustion, reset, and reuse. |
| - Ran GNAT 13.3.0 and checksum-pinned GNATprove distribution 15.1.0. |
| - Proved all six checks; no unproved or justified checks, warnings, or assumptions. |
| - [Verification report](verification/ats-spark-af40c4e.md) records source commit, |
| source hashes, toolchains, CI runs, proof scope, and remaining certification work. |
| - `verify.sh` now checks ATS interfaces, Idris proofs/executable, Ada tests, and |
| GNATprove with unproved checks and warnings treated as errors. |
|
|
| ## v1.0.0 release scope |
|
|
| The owner requested a v1 release of the current repository. It packages the |
| validated scaffold, with documentation, evidence, and checksums. It does not |
| mark runtime or production gates A–R complete. Repository description/topics, |
| CI/evidence badges, Mermaid flowcharts, conceptual images, contributing and |
| security policies, licensing-inquiry information, and support documentation |
| are included. Current original source is proprietary and source-visible under |
| [LICENSE](../LICENSE). Negotiated commercial terms and a donation destination |
| remain owner decisions. |
|
|
