docs/DELIVERY.md

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