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

Select the next unmet gate and record its concrete acceptance criteria.
Implement a reviewable increment with tests of observable behavior.
Compile and run the tests; collect proof reports where applicable.
Commit the increment and update this ledger with evidence and blockers.
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 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 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. Negotiated commercial terms and a donation destination remain owner decisions.