# 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.