October 2026 main drop: mirror from GitHub

.gitattributes

@@ -1,3 +1,13 @@
+# 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.
+
+* text=auto
+*.sh text eol=lf
+*.idr text eol=lf
+*.sats text eol=lf
+*.dats text eol=lf
+
 *.7z filter=lfs diff=lfs merge=lfs -text
 *.arrow filter=lfs diff=lfs merge=lfs -text
 *.bin filter=lfs diff=lfs merge=lfs -text
@@ -33,3 +43,5 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
 *.zip filter=lfs diff=lfs merge=lfs -text
 *.zst filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text
+docs/assets/bounded-memory.png filter=lfs diff=lfs merge=lfs -text
+docs/assets/proof-workbench.png filter=lfs diff=lfs merge=lfs -text

.github/workflows/ats-spark.yml

@@ -0,0 +1,134 @@
+# 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.
+
+name: ATS and SPARK validation
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  ats:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+      - name: Install ATS compiler
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y ats2-lang=0.4.2-1.1 build-essential
+      - name: Typecheck supplied ATS interfaces
+        run: |
+          mkdir -p build/reports/ats
+          set -o pipefail
+          patsopt --version | tee build/reports/ats/version.txt
+          patsopt -tc -s ats/heap.sats 2>&1 | tee build/reports/ats/heap-typecheck.txt
+          patsopt -tc -s ats/state.sats 2>&1 | tee build/reports/ats/state-typecheck.txt
+      - name: Preserve ATS evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: ats-validation-evidence
+          path: build/reports/ats/
+  spark:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+      - name: Install native Ada compiler
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y gnat gprbuild
+      - name: Restore pinned SPARK toolchain
+        id: spark-cache
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830
+        with:
+          path: ~/.local/gnatprove-15.1.0
+          key: gnatprove-linux-aad9a73f600d3008-v1
+      - name: Install checksum-verified GNATprove
+        if: steps.spark-cache.outputs.cache-hit != 'true'
+        run: |
+          curl --fail --location --retry 3 \
+            https://github.com/alire-project/GNAT-FSF-builds/releases/download/gnatprove-15.1.0-1/gnatprove-x86_64-linux-15.1.0-1.tar.gz \
+            -o "$RUNNER_TEMP/gnatprove.tar.gz"
+          echo "aad9a73f600d3008f33141a6cd4c5314d4c210e8928edc172c23c76104ddf7b2  $RUNNER_TEMP/gnatprove.tar.gz" | sha256sum --check
+          mkdir -p "$HOME/.local/gnatprove-15.1.0"
+          tar -xzf "$RUNNER_TEMP/gnatprove.tar.gz" --strip-components=1 -C "$HOME/.local/gnatprove-15.1.0"
+      - name: Save prover before running project checks
+        if: steps.spark-cache.outputs.cache-hit != 'true'
+        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830
+        with:
+          path: ~/.local/gnatprove-15.1.0
+          key: gnatprove-linux-aad9a73f600d3008-v1
+      - name: Build and run heap smoke test
+        run: |
+          mkdir -p build/reports/spark
+          set -o pipefail
+          gnat --version | tee build/reports/spark/compiler-version.txt
+          gprbuild -p -P ada/heap_model.gpr 2>&1 | tee build/reports/spark/build.txt
+          build/heap_demo | tee build/reports/spark/smoke.txt
+          test "$(cat build/reports/spark/smoke.txt)" = 'heap contract smoke test: PASS'
+      - name: Prove all heap obligations and fail on unproved checks
+        run: |
+          export PATH="$HOME/.local/gnatprove-15.1.0/bin:$PATH"
+          mkdir -p build/reports/spark
+          set -o pipefail
+          gnatprove --version | tee build/reports/spark/prover-version.txt
+          gnatprove -P ada/heap_model.gpr -u heap_model.adb --mode=all \
+            --checks-as-errors=on --warnings=error --report=all --level=2 \
+            2>&1 | tee build/reports/spark/proof.txt
+      - name: Preserve SPARK evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: spark-validation-evidence
+          path: |
+            build/reports/spark/
+            build/ada_obj/gnatprove/
+  combined:
+    needs: [ats, spark]
+    runs-on: ubuntu-24.04
+    timeout-minutes: 35
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+      - name: Install combined compiler dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y ats2-lang=0.4.2-1.1 gnat gprbuild chezscheme build-essential libgmp-dev
+      - name: Restore pinned Idris compiler
+        id: combined-idris
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830
+        with:
+          path: ~/.idris2
+          key: idris2-ubuntu24-15a3e4e70843f7a34100f6470c04b791330788df-v1
+      - name: Bootstrap Idris if cache was evicted
+        if: steps.combined-idris.outputs.cache-hit != 'true'
+        run: |
+          git clone https://github.com/idris-lang/Idris2.git "$RUNNER_TEMP/Idris2"
+          cd "$RUNNER_TEMP/Idris2"
+          git checkout 15a3e4e70843f7a34100f6470c04b791330788df
+          make bootstrap SCHEME=chezscheme
+          make install
+      - name: Restore SPARK toolchain validated by prerequisite job
+        uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830
+        with:
+          path: ~/.local/gnatprove-15.1.0
+          key: gnatprove-linux-aad9a73f600d3008-v1
+          fail-on-cache-miss: true
+      - name: Run the complete checked-component entry point
+        run: |
+          export PATH="$HOME/.idris2/bin:$HOME/.local/gnatprove-15.1.0/bin:$PATH"
+          mkdir -p build/reports
+          set -o pipefail
+          bash verify.sh 2>&1 | tee build/reports/combined.txt
+      - name: Preserve combined evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: combined-validation-evidence
+          path: build/reports/combined.txt

.github/workflows/idris-proofs.yml

@@ -0,0 +1,72 @@
+# 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.
+
+name: Idris proof typecheck
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  typecheck:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 35
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+      - name: Install bootstrap dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme build-essential libgmp-dev
+      - name: Cache pinned Idris installation
+        id: idris-cache
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830
+        with:
+          path: ~/.idris2
+          key: idris2-ubuntu24-15a3e4e70843f7a34100f6470c04b791330788df-v1
+      - name: Bootstrap pinned Idris 2
+        if: steps.idris-cache.outputs.cache-hit != 'true'
+        run: |
+          git clone https://github.com/idris-lang/Idris2.git "$RUNNER_TEMP/Idris2"
+          cd "$RUNNER_TEMP/Idris2"
+          git checkout 15a3e4e70843f7a34100f6470c04b791330788df
+          make bootstrap SCHEME=chezscheme
+          make install
+      - name: Save compiler before checking project proofs
+        if: steps.idris-cache.outputs.cache-hit != 'true'
+        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830
+        with:
+          path: ~/.idris2
+          key: idris2-ubuntu24-15a3e4e70843f7a34100f6470c04b791330788df-v1
+      - name: Check handwritten proof terms and model
+        run: |
+          export PATH="$HOME/.idris2/bin:$PATH"
+          mkdir -p build/reports
+          idris2 --version | tee build/reports/idris-version.txt
+          set -o pipefail
+          cd idris
+          idris2 --total --check LambdaProofs.idr 2>&1 | tee ../build/reports/lambda-typecheck.txt
+          idris2 --total --check Main.idr 2>&1 | tee ../build/reports/model-typecheck.txt
+      - name: Compile and smoke-test the current control model
+        run: |
+          export PATH="$HOME/.idris2/bin:$PATH"
+          set -o pipefail
+          cd idris
+          idris2 --total -o control-model Main.idr 2>&1 | tee ../build/reports/model-build.txt
+          build/exec/control-model | tee ../build/reports/model-smoke.txt
+          test "$(cat ../build/reports/model-smoke.txt)" = 'step: advanced'
+      - name: Preserve typechecker evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: idris-typecheck-evidence
+          path: build/reports/
+      - name: Preserve the prototype control-model executable
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: idris-control-model-ubuntu24
+          path: idris/build/exec/

.gitignore

@@ -0,0 +1,9 @@
+# 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.
+
+/build/
+/idris/build/
+__pycache__/
+*.pyc
+/agent_hooks.sh

CHANGELOG.md

@@ -0,0 +1,29 @@
+<!--
+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.
+-->
+
+# Changelog
+
+## Unreleased
+
+- Declare original project material proprietary and publicly source-visible, not open source; add license headers and the root LICENSE notice.
+- Update public repository and commercial permission documentation; preserve third-party archives and published v1.0.0 assets.
+
+## v1.0.0 — Verification scaffold
+
+- Converted supplied heap/state sketches into ATS/Postiats-checked interfaces.
+- Added handwritten I/K/S lambda derivations and explicit Idris beta witnesses.
+- Added capture-avoidance examples, corrected fuel proofs, and explicit exhaustion status.
+- Compiled the Idris control-model program and checked its output in CI.
+- Strengthened Ada allocation contracts and tested capacity, exhaustion, and reset.
+- Discharged all six SPARK checks for the allocation-counter model.
+- Added pinned compiler/prover workflows and combined `verify.sh` validation.
+- Recorded source-pinned verification reports and original sketch provenance.
+- Added workflow diagrams, conceptual photographs, contribution/security policies,
+  licensing-inquiry and support pages, repository description, topics, and badges.
+
+The ATS evaluator, generation-checked slot-map heap, FFI adapter, full effectful
+semantics, differential tests, and cross-language correspondence remain open.
+Commercial license terms and a payment destination remain owner decisions.

COMMERCIAL-LICENSING.md

@@ -0,0 +1,27 @@
+<!--
+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.
+-->
+
+# Commercial licensing inquiries
+
+[![Commercial licensing](https://img.shields.io/badge/commercial-licensing_inquiries-7c3aed)](https://github.com/AHMADALIPARR)
+
+Contact the [repository maintainer](https://github.com/AHMADALIPARR) to discuss
+commercial licensing or support. An inquiry is not a license grant. Pricing,
+license scope, support commitments, warranties, and permitted distribution must
+be agreed in writing; no standard commercial agreement is published in v1.
+
+Describe your intended use, deployment/distribution model, required components,
+organization, and support needs. The agreement would need to identify the
+covered source version, ownership/provenance, applicable third-party terms,
+license duration, redistribution rights, and any support or maintenance terms.
+
+Original project code is proprietary and source-visible, not open source. See [LICENSING.md](LICENSING.md). Commercial arrangements can cover
+only rights the licensor can grant; they do not remove third-party obligations.
+
+v1 is a verification scaffold, with an unimplemented ATS runtime and slot-map
+heap. Its commercial availability must not be described as a certified
+production interpreter. The [verification report](docs/verification/ats-spark-af40c4e.md)
+defines the checked component scope.

CONTRIBUTING.md

@@ -0,0 +1,67 @@
+<!--
+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.
+-->
+
+# Contributing
+
+This public, proprietary source-visible repository develops a combined Unlambda/ATS/Idris/SPARK
+verification scaffold. Review [LICENSE](LICENSE) before proposing contributions. Start with the
+[workflow](docs/WORKFLOW.md), [current evidence](docs/verification/ats-spark-af40c4e.md),
+and [delivery gates](docs/DELIVERY.md).
+
+## Work on a reviewable increment
+
+Open an issue describing the behavior or proof obligation, then use a focused
+branch. An implementation change should include a test of observable behavior
+or a constructive proof of the changed invariant. Documentation-only changes
+should have working links and accurate scope statements.
+
+```sh
+git switch -c change/describe-the-increment
+# Edit source, specifications, and relevant tests or proofs.
+bash verify.sh
+git add <changed-files>
+git commit -m "Describe the resulting behavior"
+git push -u origin change/describe-the-increment
+```
+
+Create a pull request with the concrete problem, resulting behavior, checked
+commands/CI runs, and any remaining proof obligations. Reference the gate it
+advances. Do not mark a runtime gate complete from interface checks alone.
+
+## Proof and safety rules
+
+- Keep handwritten derivations and Idris witnesses consistent. State the
+  quantified operand class and every required substitution lemma.
+- Keep Idris proof-bearing definitions total. Do not use `believe_me`,
+  `assert_total`, `assert_smaller`, missing proof holes, or equivalent bypasses.
+- Do not introduce `pragma Assume` or suppress required SPARK checks. Strengthen
+  contracts and supply loop invariants when needed; retain unproved-check failures.
+- Preserve distinct `OutOfFuel`, `OutOfMemory`, failure, and successful statuses.
+- Do not dereference a future node handle without generation-checked lookup.
+- Preserve input/output ordering and record effects in explicit machine state.
+- Add runtime code only with its actual compiler and behavioral checks. Abstract
+  ATS declarations do not establish implementation or FFI correctness.
+- Never source unreviewed agent hooks. `agent_hooks.example.sh` is an example,
+  not an active proof-generation agent or a release gate.
+
+The source scanner is a guardrail. Compiler/prover evidence and review are still
+required. Do not invent coverage percentages, certification seals, or claims
+that one language's tool verifies the other language's implementation.
+
+## Review checklist
+
+- The change explains its observable behavior and proof boundary.
+- Specs and implementation agree; provenance and dependency versions are recorded.
+- Relevant CI passes on the proposed source snapshot.
+- Required checks are not skipped, assumed, or downgraded.
+- Reports and release notes distinguish checked scope from future work.
+- Contributions identify their authorship and any third-party license obligations.
+
+Original project code is proprietary and source-visible, not open source;
+see [LICENSING.md](LICENSING.md). Do not assume a copyright transfer or commercial
+relicensing grant. Discuss the applicable contribution terms with the maintainer
+before contributing third-party material. Report sensitive issues through
+[SECURITY.md](SECURITY.md), rather than a normal issue or pull request.

LICENSE

@@ -0,0 +1,21 @@
+Proprietary source-visible notice
+
+Copyright (c) 2026 Ahmad Ali Parr. All rights reserved.
+SPDX-License-Identifier: LicenseRef-Proprietary
+
+This repository is publicly visible source, not open-source software.
+Except for rights provided by applicable law or the hosting platform's terms,
+no permission is granted to use, copy, modify, distribute, sublicense, or sell
+original project material without separate written permission from the owner.
+Public access does not grant a general software license. GitHub platform rights
+to view and fork a public repository under its terms are not revoked by this notice.
+
+Commercial permissions must be agreed separately in writing. Contact:
+https://github.com/AHMADALIPARR or ahmedparr93@gmail.com.
+
+This notice applies only to original project material for which the owner holds
+applicable rights. Third-party material retains its own notices and terms;
+this notice does not replace them. Archived supplied material in
+docs/source-sketches/ and docs/unlambda_x5f_ats_x5f_runtime_x5f_architecture.html
+is preserved for provenance and is not assigned new ownership by this notice.
+See LICENSING.md for scope and provenance details.

LICENSING.md

@@ -0,0 +1,29 @@
+# Licensing and provenance
+
+This is a **proprietary, publicly source-visible project, not open source**.
+Original project material is covered by [LICENSE](LICENSE). Copyright (c) 2026
+Ahmad Ali Parr. All rights reserved. Public visibility does not grant a general
+license to use, modify, redistribute, or commercialize that material. Separate
+written permission is required except for rights provided by applicable law or
+GitHub's platform terms, including its public-repository viewing and forking rights.
+See [GitHub's licensing guidance](https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/licensing-a-repository).
+
+Source headers use `SPDX-License-Identifier: LicenseRef-Proprietary`, a custom
+identifier referring to the root notice rather than an open-source license.
+The root notice also covers original documentation and applicable rights in
+project assets; PNG files and the machine-readable VERSION file remain intact.
+
+The supplied architecture notes mention Unlambda 2.0.0 and GPL-2.0-or-later
+for upstream material from madore.org. Any actual third-party material retains
+its own applicable notices and rights; this proprietary notice cannot override
+those terms. Compiler and prover licenses are separate from project licensing.
+
+Original supplied sketches in `docs/source-sketches/` and the archived
+`docs/unlambda_x5f_ats_x5f_runtime_x5f_architecture.html` are preserved without
+new ownership headers. Their provenance must be established before incorporating
+third-party implementations or redistributing third-party material.
+
+For separately negotiated permissions, see
+[COMMERCIAL-LICENSING.md](COMMERCIAL-LICENSING.md). No standard commercial grant,
+price, warranty, or support commitment is implied. Published v1.0.0 source and
+evidence archives remain unchanged; current headers do not rewrite that snapshot.

README.md

@@ -0,0 +1,18 @@
+---
+license: other
+license_name: proprietary-source-visible
+license_link: https://huggingface.co/Snapkitty/unlambda-idris-spark/blob/main/LICENSE
+tags:
+- snapkitty
+- october-2026-drop
+- unlambda
+- idris
+- ats
+- ada
+- spark
+- lambda-calculus
+- formal-verification
+---
+
+> Mirrored from [https://github.com/SNAPKITTYWEST/unlambda-idris-spark](https://github.com/SNAPKITTYWEST/unlambda-idris-spark) at commit `a42eccc`. Part of the **SnapKitty October 2026 main drop**.
+

SECURITY.md

@@ -0,0 +1,52 @@
+<!--
+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.
+-->
+
+# Security policy
+
+## Supported scope
+
+| Version | Scope |
+| --- | --- |
+| v1.0.x | Maintainer triage for the verification scaffold and build/proof workflow |
+| Unreleased runtime designs | Design review; no supported deployed interpreter |
+
+The repository is public and source-visible. v1 contains interfaces, a proof/control model, and an
+allocation counter. It is not a sandbox for executing untrusted Unlambda code.
+Passing typechecks and the counter's SPARK proofs do not establish security of
+an interpreter, an FFI adapter, or a production deployment.
+
+## Report privately
+
+Email the repository owner at **ahmedparr93@gmail.com** with subject
+`[unlambda-idris-spark] Security report`. This is the contact published on the
+[maintainer's GitHub profile](https://github.com/AHMADALIPARR). If GitHub private
+vulnerability reporting is enabled later, the repository's Security tab may
+also provide a private report form. Do not assume that form is currently enabled.
+
+Include the affected commit/version, relevant toolchain versions, a minimal
+reproduction, expected impact, and suggested remediation if available. Do not
+include credentials, personal data, or live customer input. Avoid publishing
+an exploit or opening an ordinary issue containing sensitive details while
+the report is being investigated.
+
+The maintainer reviews reports and coordinates fixes and disclosure. No fixed
+response SLA or paid bounty program is currently promised.
+
+## What to report
+
+- Build or agent-hook execution that can expose secrets or run unintended commands.
+- A proof gate that reports success despite missing, suppressed, or unproved checks.
+- Unsafe future handle lookup, generation reuse, or incorrect memory exhaustion.
+- Release asset/source mismatch, compromised dependencies, or false evidence claims.
+- A defect in the checked model or contracts that invalidates a documented result.
+
+## Build and proof boundaries
+
+CI actions and compiler sources are pinned; the GNATprove archive is checksum
+verified. Evidence is tied to source commits. Credentials and local
+`agent_hooks.sh` must not be committed. Generated proof modules require the same
+review and typechecking as handwritten modules. Third-party compilers, provers,
+and runtime libraries remain part of the trusted toolchain.

SUPPORT.md

@@ -0,0 +1,23 @@
+<!--
+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.
+-->
+
+# Support and donations
+
+[![Donate](https://img.shields.io/badge/donate-details_pending-d97706)](https://github.com/AHMADALIPARR)
+
+The maintainer has not provided a verified donation destination yet. The badge
+links to support information and the maintainer profile; it does not initiate
+a payment. No payment account, donation URL, or GitHub Sponsors enrollment is
+assumed. A funding link and `.github/FUNDING.yml` can be added when the owner
+confirms the destination.
+
+You can help now by reviewing the handwritten derivations, reproducing CI,
+improving specifications, or contributing tests and the open runtime/heap
+implementation work. Start with [CONTRIBUTING.md](CONTRIBUTING.md).
+
+Future donations would support project work; they would not purchase a commercial
+license, security SLA, or proof of production readiness. Commercial inquiries
+belong in [COMMERCIAL-LICENSING.md](COMMERCIAL-LICENSING.md).

VERSION

@@ -0,0 +1 @@
+1.0.0

ada/heap_demo.adb

@@ -0,0 +1,28 @@
+-- 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.
+
+with Ada.Text_IO; use Ada.Text_IO;
+with Heap_Model;
+
+--  Test driver: I/O is outside the proof boundary of Heap_Model.
+procedure Heap_Demo is
+   H : Heap_Model.Heap;
+   Success : Boolean;
+begin
+   Heap_Model.Reset (H);
+   pragma Assert (Heap_Model.Used (H) = 0);
+   for Expected in 1 .. Heap_Model.Capacity loop
+      Heap_Model.Allocate (H, Success);
+      pragma Assert (Success);
+      pragma Assert (Heap_Model.Used (H) = Expected);
+   end loop;
+   Heap_Model.Allocate (H, Success);
+   pragma Assert (not Success);
+   pragma Assert (Heap_Model.Used (H) = Heap_Model.Capacity);
+   Heap_Model.Reset (H);
+   pragma Assert (Heap_Model.Used (H) = 0);
+   Heap_Model.Allocate (H, Success);
+   pragma Assert (Success and then Heap_Model.Used (H) = 1);
+   Put_Line ("heap contract smoke test: PASS");
+end Heap_Demo;

ada/heap_model.adb

@@ -0,0 +1,24 @@
+-- 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.
+
+package body Heap_Model with SPARK_Mode is
+
+   function Used (H : Heap) return Count is (H.Allocated);
+
+   procedure Reset (H : out Heap) is
+   begin
+      H := (Allocated => 0);
+   end Reset;
+
+   procedure Allocate (H : in out Heap; Success : out Boolean) is
+   begin
+      if H.Allocated < Capacity then
+         H.Allocated := H.Allocated + 1;
+         Success := True;
+      else
+         Success := False;
+      end if;
+   end Allocate;
+
+end Heap_Model;

ada/heap_model.ads

@@ -0,0 +1,29 @@
+-- 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.
+
+package Heap_Model with SPARK_Mode is
+   Capacity : constant := 64;
+   subtype Index is Natural range 0 .. Capacity - 1;
+   subtype Count is Natural range 0 .. Capacity;
+
+   type Heap is private;
+
+   function Used (H : Heap) return Count;
+
+   procedure Reset (H : out Heap)
+     with Post => Used (H) = 0;
+
+   procedure Allocate (H : in out Heap; Success : out Boolean)
+     with
+       Pre  => Used (H) <= Capacity,
+       Post =>
+         Success = (Used (H'Old) < Capacity) and then
+         (if Success then Used (H) = Used (H'Old) + 1
+          else Used (H) = Used (H'Old));
+
+private
+   type Heap is record
+      Allocated : Count := 0;
+   end record;
+end Heap_Model;

ada/heap_model.gpr

@@ -0,0 +1,13 @@
+-- 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.
+
+project Heap_Model is
+   for Source_Dirs use (".");
+   for Main use ("heap_demo.adb");
+   for Object_Dir use "../build/ada_obj";
+   for Exec_Dir use "../build";
+   package Compiler is
+      for Switches ("Ada") use ("-gnat2022", "-gnata");
+   end Compiler;
+end Heap_Model;

agent_hooks.example.sh

@@ -0,0 +1,21 @@
+# 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.
+
+# Copy to agent_hooks.sh and replace the bodies with your local agent integration.
+# Do not source unreviewed hook scripts: they execute with your user permissions.
+
+generate_proof_tactic() {
+  # Print a COMPLETE Idris 2 module to stdout, not a tactic fragment.
+  # Example: invoke your local agent CLI here.
+  echo 'module GeneratedProofs'
+  echo '%default total'
+  echo 'example : 1 = 1'
+  echo 'example = Refl'
+}
+
+update_agent_context() {
+  # Persist feedback to your agent's context/session using your integration.
+  # This sample only writes feedback to stderr.
+  printf '%s\n' "$1" >&2
+}

ats/heap.sats

@@ -0,0 +1,27 @@
+(*
+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.
+*)
+
+(* Typed contract for the planned heap adapter. Implementations are pending. *)
+abstype heap = ptr
+abstype node_ref = ptr
+abstype node = ptr
+
+datatype heap_err =
+  | StaleRef of ()
+  | InvalidSlot of ()
+  | OutOfMemory of ()
+
+datatype heap_result (a:t@ype) =
+  | HeapOK of a
+  | HeapError of heap_err
+
+fun heap_create (capacity: intGte(0)): heap_result(heap)
+fun heap_alloc (h: heap, n: node): heap_result(node_ref)
+fun heap_lookup (h: heap, r: node_ref): heap_result(node)
+fun heap_update (h: heap, r: node_ref, n: node): heap_result(bool)
+fun heap_free (h: heap, r: node_ref): heap_result(bool)
+fun heap_live (h: heap): intGte(0)
+fun heap_is_valid (h: heap): bool

ats/state.sats

@@ -0,0 +1,42 @@
+(*
+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.
+*)
+
+(* Typed contract for the planned machine. Implementations are pending. *)
+staload H = "./heap.sats"
+
+abstype term_ref = ptr
+
+datatype status =
+  | Running of ()
+  | Halted of ()
+  | Failed of ()
+  | OutOfFuel of ()
+  | OutOfMemory of ()
+
+datatype control =
+  | Ctrl_Term of term_ref
+  | Ctrl_Value of $H.node_ref
+
+datatype frame =
+  | F_EvalArg of term_ref
+  | F_ApplyFun of $H.node_ref
+
+typedef input_state = @{
+  buffer=List0(uchar), cursor=size_t, current=Option(uchar)
+}
+
+typedef machine_state = @{
+  control=control,
+  kont=List0(frame),
+  heap=$H.heap,
+  input=input_state,
+  output=List0(uchar),
+  fuel=intGte(0),
+  status=status
+}
+
+fun state_invariant_holds (state: machine_state): bool
+fun state_step (state: machine_state): machine_state

docs/DELIVERY.md

@@ -0,0 +1,106 @@
+<!--
+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.

docs/WORKFLOW.md

@@ -0,0 +1,130 @@
+<!--
+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.
+
+![Conceptual bounded-memory tabletop model, used as an illustration rather than proof evidence](assets/bounded-memory.png)
+
+## 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.

docs/assets/README.md

@@ -0,0 +1,29 @@
+<!--
+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.
+-->
+
+# Visual assets
+
+These AI-generated conceptual photographs illustrate the project. They are
+not screenshots, hardware products, or formal verification evidence. Read
+`spec/lambda-proofs.md` for the actual derivations; notebook marks in artwork
+are decorative.
+
+Generated with the built-in imagegen tool. The selected PNG outputs are stored
+in this repository; no external image-generation account or file URL is required
+to render the README. Applicable rights in project artwork are reserved under
+[LICENSE](../../LICENSE); see [LICENSING.md](../../LICENSING.md).
+
+## `proof-workbench.png`
+
+Exact prompt:
+
+> Use case: photorealistic-natural. Asset type: wide GitHub README cover photo for the Unlambda + ATS + Idris 2 + SPARK proof scaffold. Primary request: a polished editorial photograph of a dark desk with a notebook of handwritten lambda calculus, a pen, and three translucent geometric blocks suggesting typed interfaces, checked proofs, and bounded memory. Wide landscape composition, restrained navy background, soft cyan and amber studio lighting, realistic paper and glass textures, plenty of clean visual space. No people. No logos, no fabricated software screenshot, no certification seals, no checkmarks, no readable claims of production readiness. Notebook symbols may include a simple lambda and S K I. No title text, no watermark.
+
+## `bounded-memory.png`
+
+Exact prompt:
+
+> Use case: photorealistic-natural. Asset type: supporting editorial photograph for a README's bounded-memory verification section. An abstract desktop memory model made from a compact orderly array of small translucent square glass tiles, some softly illuminated amber and others clear, with a notebook and pen out of focus in the background. This is a conceptual tabletop scene, not a real hardware product or screenshot. Realistic glass textures, navy and teal studio lighting, wide landscape composition, visually cohesive with a dark lambda-calculus proof workbench photo. No people, no readable text, no logos, no certification seals, no checkmarks, no watermark.

docs/releases/v1.0.0.md

@@ -0,0 +1,49 @@
+<!--
+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.
+-->
+
+# v1.0.0 — Verification scaffold
+
+This first version packages the checked proof/model/interface components and
+their evidence. It is a development foundation for the combined Unlambda,
+ATS, Idris 2, and SPARK architecture.
+
+## Included
+
+- ATS/Postiats 0.4.2-checked heap and state interface declarations.
+- Handwritten SKI derivations with Idris 2 0.8.0-checked proof terms.
+- A compiled fuel/control model with an executable smoke test.
+- An assertion-tested Ada allocation counter with all six SPARK checks discharged.
+- Combined compiler/prover validation, documented toolchains, and source-pinned reports.
+- Contributor/security policies, licensing/support information, diagrams, and artwork.
+
+## Release assets
+
+- `unlambda-idris-spark-v1.0.0-source.zip`: source snapshot and documentation.
+- `unlambda-idris-spark-v1.0.0-evidence.zip`: release-commit CI reports, plus a
+  manifest identifying the source commit and workflow runs.
+- `SHA256SUMS.txt`: SHA-256 hashes of those two archives.
+
+The release record and evidence manifest identify the exact source commit.
+Validate asset checksums, install the documented toolchains, and run
+`bash verify.sh` to reproduce the component checks.
+
+## Verification scope
+
+The runtime `.sats` declarations have no `.dats` implementation or ATS/Ada
+adapter. The Ada heap counts allocations and does not store nodes or generation
+handles. The Idris control model does not evaluate Unlambda programs. These
+components and their proof boundaries are documented in
+[the verification report](https://github.com/AHMADALIPARR/unlambda-idris-spark/blob/v1.0.0/docs/verification/ats-spark-af40c4e.md).
+
+This release does not claim full interpreter correctness, cross-language
+correspondence, Windows runtime support, or production certification. The
+[delivery backlog](https://github.com/AHMADALIPARR/unlambda-idris-spark/blob/v1.0.0/docs/DELIVERY.md) retains those open gates.
+
+At initial publication, the repository was private and no original-code license
+grant was selected. The repository is now public and proprietary source-visible;
+see [current licensing policy](https://github.com/AHMADALIPARR/unlambda-idris-spark/blob/main/LICENSE).
+Published v1.0.0 archives remain unchanged. Commercial permissions require a
+separate written agreement; the donation destination remains pending.

docs/source-sketches/heap.sats.txt

@@ -0,0 +1,3 @@
+abstype heap, node_ref, node
+heap_err StaleRef InvalidSlot OutOfMemory
+heap_create, heap_alloc, heap_lookup, heap_update, heap_live, heap_is_valid

docs/source-sketches/state.sats.txt

@@ -0,0 +1,4 @@
+status Running Halted Failed OutOfFuel OutOfMemory
+control Ctrl_Term Ctrl_Value
+machine_state {control,kont,heap,input,output,fuel,status}
+state_invariant_holds, state_step

docs/verification/ats-spark-af40c4e.md

@@ -0,0 +1,86 @@
+<!--
+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.
+-->
+
+# ATS/SPARK verification report
+
+Checked source commit: `af40c4e75c51c4dfc636b3eaa53f2362ffae0c4a`.
+
+[ATS and SPARK validation run](https://github.com/AHMADALIPARR/unlambda-idris-spark/actions/runs/38026024273)
+and [Idris validation on the same source commit](https://github.com/AHMADALIPARR/unlambda-idris-spark/actions/runs/38026024320)
+both passed.
+
+## Checked scope
+
+| Component | Result | Scope |
+| --- | --- | --- |
+| `ats/heap.sats` | ATS typecheck passed | Interface declarations |
+| `ats/state.sats` | ATS typecheck passed | Interface declarations |
+| Ada `Heap_Model` | Compiled and tests passed | Fixed-capacity allocation counter |
+| Ada `Heap_Model` | All six GNATprove checks discharged | Initialization, range safety, postconditions, termination |
+| Idris proofs/model | Typechecked; model built and smoke-tested | Previously documented proof/model slice |
+| ATS runtime | Not certified | No `.dats` implementation exists |
+| Generational slot-map heap | Not certified | Not yet implemented |
+| Cross-language correspondence | Not certified | No checked adapter/simulation argument yet |
+
+This report certifies only the observed compiler/prover results for the stated
+source snapshot and scope. It is not a third-party certification, a full
+interpreter correctness proof, or a production release certificate.
+
+## Tools and reproducibility
+
+- Runner: Ubuntu 24.04, x86-64.
+- ATS/Postiats: 0.4.2; Ubuntu package `ats2-lang=0.4.2-1.1`.
+- Native Ada compiler: GNAT 13.3.0; assertion checking enabled with `-gnata`.
+- GNATprove distribution: Alire `gnatprove` 15.1.0 (reports `FSF 15.0`).
+- GNATprove archive SHA-256:
+  `aad9a73f600d3008f33141a6cd4c5314d4c210e8928edc172c23c76104ddf7b2`.
+- Prover checks use `--mode=all --checks-as-errors=on --warnings=error
+  --report=all --level=2`, targeting `heap_model.adb`.
+- Machine evidence is retained in the run's `ats-validation-evidence` and
+  `spark-validation-evidence` artifacts, subject to GitHub retention.
+
+The compiler/prover installation follows the official
+[Ubuntu ATS package](https://packages.ubuntu.com/noble/ats2-lang),
+[Alire GNATprove manifest](https://github.com/alire-project/alire-index/blob/9ecbbfb0f9442fa6e53f5492258837c430154a3e/index/gn/gnatprove/gnatprove-15.1.0.toml),
+and [GNATprove command documentation](https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_run_gnatprove.html).
+
+## Discharged SPARK checks
+
+The prover summary reports six checks: two initialization checks, one run-time
+range check, two functional-contract checks, and one termination check. Three
+are discharged by flow analysis and three by CVC5. There are zero unproved or
+justified checks. The detailed report records no warnings or `pragma Assume`.
+
+The functional contracts establish:
+
+- Reset sets the used count to zero.
+- Allocation succeeds exactly when the old count is below capacity.
+- Successful allocation increments the count by one.
+- Rejected allocation preserves the count.
+
+The test driver fills all 64 slots counted by the model, checks exhaustion,
+resets the count, and allocates again. It uses runtime assertions; its I/O
+driver is outside the SPARK proof boundary.
+
+## Checked source hashes
+
+SHA-256 hashes are for the Git blob bytes in the checked commit, with LF endings.
+
+| File | SHA-256 |
+| --- | --- |
+| `ats/heap.sats` | `31f057dca9fc21f88bda99f071904fb781cc02650d005b3aa098204f48a1d550` |
+| `ats/state.sats` | `ce64db05252470b0dd1eb3ec930477f02aa22c812c3857eceab43466527836e4` |
+| `ada/heap_model.ads` | `a98bd4dc755c03807b1ea84cc158fcd94f325503facfe5021443d60df33317ab` |
+| `ada/heap_model.adb` | `8bb9c934b080efe8ff9d9e7e042c1fa3a95c92497f1f6511ce1cdd7409ded9cc` |
+
+## Required before full runtime certification
+
+Implement the ATS parser and evaluator, the Ada slot-map with generation-checked
+references, and the ATS/Ada adapter. Compile/link the real runtime; test every
+Unlambda primitive, strictness/delay, I/O ordering, continuation restoration,
+fuel exhaustion, and heap exhaustion. Prove the extended heap contracts and
+establish correspondence to the Idris semantics. Passing interface checks and
+counter proofs alone cannot establish these properties.

docs/verification/idris-bb9abcc.md

@@ -0,0 +1,41 @@
+<!--
+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.
+-->
+
+# Idris compiler evidence
+
+Source commit: `bb9abccd3eec626ce1aeac0894a75a6385ed898b`.
+
+[Successful GitHub Actions run](https://github.com/AHMADALIPARR/unlambda-idris-spark/actions/runs/38025027084).
+
+Runner: Ubuntu 24.04. Compiler: Idris 2 0.8.0, bootstrapped from upstream commit
+`15a3e4e70843f7a34100f6470c04b791330788df`.
+
+## Passed checks
+
+- `idris2 --total --check LambdaProofs.idr`
+- `idris2 --total --check Main.idr`
+- `idris2 --total -o control-model Main.idr`
+- Run `build/exec/control-model`; require exact output `step: advanced`.
+
+The run retains the `idris-typecheck-evidence` artifact with version,
+typechecker, build, and smoke-test logs. It also retains the prototype executable
+as `idris-control-model-ubuntu24`. Artifact availability follows GitHub retention.
+
+## What the checked proofs establish
+
+- Explicit I/K/S beta-reduction witnesses for symbolic free atoms.
+- Concrete substitution/capture-avoidance boundary cases.
+- Fuel never increases in the current control model.
+- A positive-fuel running transition consumes exactly one unit.
+- Zero fuel reports `OutOfFuel`.
+- `OutOfMemory` remains preserved through fuel handling.
+
+## Remaining verification
+
+The control model is still a stub; the smoke test is not an Unlambda semantic
+test. ATS runtime compilation, SPARK heap verification, general substitution
+lemmas, effectful semantics, and cross-language correspondence remain open.
+No production release is certified by this run.

idris/LambdaProofs.idr

@@ -0,0 +1,121 @@
+-- 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.
+
+module LambdaProofs
+
+%default total
+
+||| Locally nameless syntax: free atoms cannot be captured by a binder.
+public export
+data Lambda = Free Nat | Bound Nat | Lam Lambda | App Lambda Lambda
+
+predecessor : Nat -> Nat
+predecessor Z = Z
+predecessor (S n) = n
+
+||| Shift bound indices at or above a cutoff when entering binders.
+public export
+shift : Nat -> Nat -> Lambda -> Lambda
+shift amount cutoff (Free atom) = Free atom
+shift amount cutoff (Bound index) =
+  case compare index cutoff of
+    LT => Bound index
+    EQ => Bound (amount + index)
+    GT => Bound (amount + index)
+shift amount cutoff (Lam body) = Lam (shift amount (S cutoff) body)
+shift amount cutoff (App fun arg) =
+  App (shift amount cutoff fun) (shift amount cutoff arg)
+
+||| Remove one binder, substituting its argument without variable capture.
+public export
+substitute : Nat -> Lambda -> Lambda -> Lambda
+substitute depth argument (Free atom) = Free atom
+substitute depth argument (Bound index) =
+  case compare index depth of
+    LT => Bound index
+    EQ => shift depth Z argument
+    GT => Bound (predecessor index)
+substitute depth argument (Lam body) =
+  Lam (substitute (S depth) argument body)
+substitute depth argument (App fun arg) =
+  App (substitute depth argument fun) (substitute depth argument arg)
+
+public export
+identity : Lambda
+identity = Lam (Bound 0)
+
+public export
+constant : Lambda
+constant = Lam (Lam (Bound 1))
+
+public export
+substitutionBody : Lambda
+substitutionBody = Lam (Lam (App (App (Bound 2) (Bound 0))
+                               (App (Bound 1) (Bound 0))))
+
+public export
+substitutionCombinator : Lambda
+substitutionCombinator = Lam substitutionBody
+
+||| One beta reduction, possibly in the function side of an application.
+||| This relation describes the pure SKI fragment, not effectful evaluation.
+public export
+data BetaStep : Lambda -> Lambda -> Type where
+  Contract : (body : Lambda) -> (argument : Lambda) ->
+             BetaStep (App (Lam body) argument)
+                      (substitute Z argument body)
+  InFunction : BetaStep before after -> (argument : Lambda) ->
+               BetaStep (App before argument) (App after argument)
+
+public export
+data BetaSteps : Lambda -> Lambda -> Type where
+  Done : BetaSteps term term
+  Then : BetaStep before middle -> BetaSteps middle after ->
+         BetaSteps before after
+
+||| I x -> x for every symbolic free atom x.
+public export
+iBeta : (x : Nat) -> BetaStep (App LambdaProofs.identity (Free x)) (Free x)
+iBeta x = Contract (Bound 0) (Free x)
+
+||| Substitution under a binder must lift a bound argument to avoid capture.
+public export
+captureAvoidance : substitute Z (Bound 0) (Lam (Bound 1)) = Lam (Bound 1)
+captureAvoidance = Refl
+
+||| The inner binder's variable remains untouched by outer substitution.
+public export
+innerBinderPreserved : substitute Z (Free 7) (Lam (Bound 0)) = Lam (Bound 0)
+innerBinderPreserved = Refl
+
+||| Removing a binder decrements references to enclosing binders.
+public export
+outerIndexDecremented : substitute Z (Free 7) (Bound 2) = Bound 1
+outerIndexDecremented = Refl
+
+||| K x y -> x, with two explicit contractions.
+public export
+kBeta : (x, y : Nat) ->
+        BetaSteps (App (App LambdaProofs.constant (Free x)) (Free y)) (Free x)
+kBeta x y =
+  Then (InFunction (Contract (Lam (Bound 1)) (Free x)) (Free y))
+       (Then (Contract (Free x) (Free y)) Done)
+
+||| S x y z -> (x z) (y z), with three explicit contractions.
+public export
+sBeta : (x, y, z : Nat) ->
+        BetaSteps (App (App (App LambdaProofs.substitutionCombinator (Free x))
+                           (Free y)) (Free z))
+                  (App (App (Free x) (Free z)) (App (Free y) (Free z)))
+sBeta x y z =
+  Then (InFunction (InFunction (Contract substitutionBody (Free x))
+                              (Free y)) (Free z))
+       (Then (InFunction
+               (Contract (Lam (App (App (Free x) (Bound 0))
+                                   (App (Bound 1) (Bound 0))))
+                         (Free y))
+               (Free z))
+             (Then (Contract (App (App (Free x) (Bound 0))
+                                  (App (Free y) (Bound 0)))
+                             (Free z)) Done))

idris/Main.idr

@@ -0,0 +1,82 @@
+-- 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.
+
+module Main
+
+import Data.Nat
+
+%default total
+
+||| Abstract execution status. Resource exhaustion is not successful termination.
+data Status = Running | Halted | OutOfFuel | OutOfMemory | Failed
+
+||| Minimal control term for the first machine milestone.
+||| Extend only after the selected Unlambda dialect is specified.
+data Term = PrimI | PrimK | PrimS | Apply Term Term | DelayedTerm Term
+
+record Machine where
+  constructor MkMachine
+  control : Term
+  fuel : Nat
+  status : Status
+
+||| A transition outcome always records the next explicit machine status.
+data Transition = Advanced Machine | Finished Machine
+
+||| Fuel is consumed exactly once for an ordinary transition.
+consumeRunning : Term -> Nat -> Machine
+consumeRunning t Z = MkMachine t Z OutOfFuel
+consumeRunning t (S k) = MkMachine t k Running
+
+consumeFuel : Machine -> Machine
+consumeFuel (MkMachine t n Running) = consumeRunning t n
+consumeFuel (MkMachine t n Halted) = MkMachine t n Halted
+consumeFuel (MkMachine t n OutOfFuel) = MkMachine t n OutOfFuel
+consumeFuel (MkMachine t n OutOfMemory) = MkMachine t n OutOfMemory
+consumeFuel (MkMachine t n Failed) = MkMachine t n Failed
+
+||| The transition function is intentionally a control-model stub until
+||| the full Unlambda operational semantics are fixed in spec/.
+stepControl : Machine -> Transition
+stepControl m@(MkMachine _ Z Running) = Finished (consumeFuel m)
+stepControl m@(MkMachine _ (S _) Running) = Advanced (consumeFuel m)
+stepControl m = Finished m
+
+||| A structural fact: consuming fuel never increases the fuel counter.
+natLteRefl : (n : Nat) -> LTE n n
+natLteRefl Z = LTEZero
+natLteRefl (S n) = LTESucc (natLteRefl n)
+
+natLteNext : (n : Nat) -> LTE n (S n)
+natLteNext Z = LTEZero
+natLteNext (S n) = LTESucc (natLteNext n)
+
+fuelDoesNotIncrease : (m : Machine) -> fuel (consumeFuel m) `LTE` fuel m
+fuelDoesNotIncrease (MkMachine t Z Running) = LTEZero
+fuelDoesNotIncrease (MkMachine t (S k) Running) = natLteNext k
+fuelDoesNotIncrease (MkMachine t n Halted) = natLteRefl n
+fuelDoesNotIncrease (MkMachine t n OutOfFuel) = natLteRefl n
+fuelDoesNotIncrease (MkMachine t n OutOfMemory) = natLteRefl n
+fuelDoesNotIncrease (MkMachine t n Failed) = natLteRefl n
+
+||| One running transition consumes exactly one unit, not two or zero.
+positiveFuelConsumesOne : (t : Term) -> (n : Nat) ->
+  fuel (consumeFuel (MkMachine t (S n) Running)) = n
+positiveFuelConsumesOne t n = Refl
+
+||| Heap exhaustion remains distinct from generic failure and termination.
+memoryExhaustionIsPreserved : (t : Term) -> (n : Nat) ->
+  status (consumeFuel (MkMachine t n OutOfMemory)) = OutOfMemory
+memoryExhaustionIsPreserved t n = Refl
+
+||| Resource exhaustion is explicit when a running machine has zero fuel.
+zeroFuelIsNotHalted : (t : Term) -> status (consumeFuel (MkMachine t Z Running)) = OutOfFuel
+zeroFuelIsNotHalted t = Refl
+
+main : IO ()
+main = do
+  let initial = MkMachine PrimI 1 Running
+  case stepControl initial of
+    Advanced next => putStrLn "step: advanced"
+    Finished next => putStrLn "step: finished"

iterate-proof.sh

@@ -0,0 +1,57 @@
+#!/usr/bin/env bash
+# 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.
+
+set -euo pipefail
+
+ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+HOOKS="${AGENT_HOOKS:-$ROOT/agent_hooks.sh}"
+MAX_RETRIES="${MAX_RETRIES:-5}"
+ATTEMPT=1
+TARGET="$ROOT/idris/GeneratedProofs.idr"
+
+if [[ ! -f "$HOOKS" ]]; then
+  echo "Missing agent hook file: $HOOKS" >&2
+  echo "Create it with generate_proof_tactic and update_agent_context functions." >&2
+  exit 2
+fi
+# The hook file is executable project configuration and must be reviewed before sourcing.
+# shellcheck source=/dev/null
+source "$HOOKS"
+command -v generate_proof_tactic >/dev/null || { echo "generate_proof_tactic hook missing" >&2; exit 2; }
+command -v update_agent_context >/dev/null || { echo "update_agent_context hook missing" >&2; exit 2; }
+command -v idris2 >/dev/null || { echo "idris2 not installed" >&2; exit 2; }
+
+while (( ATTEMPT <= MAX_RETRIES )); do
+  echo "Proof iteration $ATTEMPT/$MAX_RETRIES"
+  if ! generate_proof_tactic > "$TARGET"; then
+    FEEDBACK="Agent generation command failed. Return a complete Idris 2 module with explicit theorem statements and constructive proof terms."
+    update_agent_context "$FEEDBACK"
+    ((ATTEMPT+=1))
+    continue
+  fi
+
+  if grep -nE '\b(believe_me|sorry|admit|assert_total|assert_smaller)\b' "$TARGET"; then
+    FEEDBACK="Rejected: prohibited Idris proof escape hatch detected. Remove the escape hatch and construct a proof term that typechecks."
+    update_agent_context "$FEEDBACK"
+    ((ATTEMPT+=1))
+    continue
+  fi
+
+  set +e
+  COMPILER_OUT="$(cd "$ROOT/idris" && idris2 --total --check GeneratedProofs.idr 2>&1)"
+  COMPILER_STATUS=$?
+  set -e
+
+  if (( COMPILER_STATUS == 0 )); then
+    echo "Idris typecheck passed. This validates the generated module only; it does not by itself establish the cross-language SPARK correspondence."
+    exit 0
+  fi
+
+  update_agent_context "Idris 2 typechecker output (attempt $ATTEMPT):\n$COMPILER_OUT"
+  ((ATTEMPT+=1))
+done
+
+echo "FAIL: proof generation did not produce a typechecking module after $MAX_RETRIES attempts." >&2
+exit 1

spec/ats-runtime-architecture.md

@@ -0,0 +1,113 @@
+<!--
+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.
+-->
+
+# Unlambda ATS runtime specification
+
+Supplied design notes. These describe intended behavior and proof obligations;
+they do not claim that the current starter implements or verifies them.
+The `ats/heap.sats` and `ats/state.sats` files now contain compiler-validated
+typed interfaces derived from the supplied sketches. Original shorthand files
+are preserved in `docs/source-sketches/`. No ATS runtime implementation exists
+yet. [Validation evidence](../docs/verification/ats-spark-af40c4e.md) defines the
+checked scope.
+
+## Language semantics — Unlambda 2.0.0
+
+Dialect: 2.0.0 GPL2+ from madore.org (as specified by the supplied notes).
+
+Syntax: application, primitives `s k i v c d e r @ | .x ?x`.
+
+Evaluation is strict except for `d`: `d x => Delayed(x)` without evaluating
+`x`; `Delayed(x) y => Eval(x)` applied to `y`.
+
+Reductions:
+
+- `i x => x`
+- `k x => K1(x)`; `K1(x) y => x`
+- `s x => S1`; `s x y => S2`; `s x y z => x z y z`
+- `v x => v`
+- `.c x => print c, return x`; `r => newline`
+- `e x => halt`
+- `c x => capture K as Cont(K), eval x, apply x to Cont`
+- `Cont(k) y => K=k, result y`
+- `@ x => read byte, cur_char set, x i if byte else x v`
+- `?c x => if cur_char==c then x i else x v`
+- `| x => if cur_char Some(b) then x .b else x v`
+
+Observables: output `O` is ordered; input cursor `I` is monotonic.
+
+## Abstract machine
+
+`Sigma=<C,K,H,I,O,F,Q>`
+
+- `C=Ctrl_Term|Ctrl_Value`
+- `K=list Frame`: `F_EvalArg(arg_term)`, `F_ApplyFun(fun_ref)`
+- `H=slot-map NodeRef {slot,gen}`
+- `I={buf,cursor,cur_char}`
+- `O=vec OutChar`
+- `F=fuel`
+- `Q=Running|Halted|Failed|OutOfFuel|OutOfMemory`
+
+Step: at most one transition, consumes one fuel. If `F==0`, set `OutOfFuel`.
+Apply logic handles `d` specially in `EvalArg`: if `fun==D`, produce
+`Delayed(arg_term)`; otherwise evaluate strictly.
+Capture the continuation on `c`; restore it on `Cont` application.
+
+## Memory model
+
+Slot-map: slots contain generation plus state `Free|Occupied(Node)`;
+maintain a free list, capacity, and live count.
+
+`NodeRef` contains slot and generation. Allocation pops the free list and
+checks generation. Lookup checks `gen==slot.gen` and `Occupied`, otherwise
+returns `StaleRef`. Update performs the same checks. Free increments generation.
+
+- H1: stored references valid at store time.
+- H2: free list exact.
+- H3: live count equals occupied count.
+- H4: generation monotonic.
+- H5: no dereference without lookup.
+
+Capacity is fixed initially; `OutOfMemory` is explicit and leaves the heap valid.
+Future GC roots: `C`, `K`, and continuation nodes.
+
+## Invariants
+
+- I1: stack references valid.
+- I2: control valid.
+- I3: heap satisfies H1–H5.
+- I4: fuel decreases monotonically by one per transition.
+- I5: output extends monotonically.
+- I6: input cursor monotonic.
+- I7: no hidden state.
+- I8: status consistent.
+- R1: `OutOfFuel != Halted`.
+- R2: `OutOfMemory != Failed`.
+- R3: `StaleRef` never dereferenced.
+
+Intended ATS enforcement: abstract `term_ref` constructible only via parser,
+abstract `NodeRef`, typed stack, abstract heap.
+Runtime assertions: lookup before use, depth limit, spans.
+Future proofs: `s,k,i` match SKI; `d` delays side effects; `c` captures/restores;
+I/O preserves order.
+
+## Gates
+
+- A: heap safety.
+- B: core machine `s,k,i,v,d,.,r`.
+- C: all primitives.
+- D: differential testing.
+- E: garbage collection.
+
+## Source materials
+
+- [Architecture HTML](../docs/unlambda_x5f_ats_x5f_runtime_x5f_architecture.html)
+- [Heap interface sketch](../ats/heap.sats)
+- [State interface sketch](../ats/state.sats)
+
+The supplied syntax sentence omits its application symbol, and the newline
+rule does not specify an argument or return value. These details remain to be
+resolved against the dialect before implementing the evaluator.

spec/invariants.md

@@ -0,0 +1,29 @@
+<!--
+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.
+-->
+
+# Unlambda / Idris 2 / SPARK verification contract
+
+## Scope of this executable slice
+
+This starter project verifies a bounded heap model and a small abstract-machine control model. It is not yet a complete Unlambda implementation. Before adding the remaining language primitives, freeze the chosen Unlambda dialect and its operational semantics.
+
+## Shared invariants
+
+- H1: heap capacity is fixed and every valid index is in `0 .. Capacity - 1`.
+- H2: `Used <= Capacity`.
+- H3: allocation succeeds only when capacity remains; failure does not change `Used`.
+- H4: a successful allocation increases `Used` by exactly one.
+- M1: machine fuel never increases during a transition.
+- M2: an exhausted machine reports `OutOfFuel`, never `Halted`.
+- M3: the Idris model's state constructors make the terminal status explicit.
+
+## Proof boundary
+
+Idris 2 checks the model and its proof terms. SPARK/GNATprove checks Ada contracts and runtime-safety/functional verification conditions. Neither tool proves the other language's implementation. Agreement is established through the shared invariants, tests, and (later) a translation/correspondence proof.
+
+## Escape-hatch policy
+
+Reject `believe_me`, `assert_total`, `assert_smaller`, `sorry`, `admit`, `pragma Assume`, and unchecked imported proof claims in proof-bearing files unless a specific reviewed exception is documented. The scanner is a guardrail, not a sound proof of absence of unsoundness.

spec/lambda-proofs.md

@@ -0,0 +1,54 @@
+<!--
+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.
+-->
+
+# Handwritten lambda-calculus proofs: pure SKI fragment
+
+Application associates to the left. Bound variables are alpha-renamed to avoid
+capture. The implementation uses de Bruijn indices for bound variables and
+separate free atoms; see `idris/LambdaProofs.idr`.
+
+## Identity
+
+`I = λa.a`
+
+`I x = (λa.a) x →β x`.
+
+Idris witness: `iBeta`, one `Contract`.
+
+## Constant
+
+`K = λa.λb.a`
+
+`K x y = ((λa.λb.a) x) y →β (λb.x) y →β x`.
+
+Idris witness: `kBeta`, two contractions, the first inside the function position.
+
+## Substitution
+
+`S = λa.λb.λc.(a c) (b c)`
+
+`S x y z = (((λa.λb.λc.(a c) (b c)) x) y) z`
+
+`→β ((λb.λc.(x c) (b c)) y) z`
+
+`→β (λc.(x c) (y c)) z`
+
+`→β (x z) (y z)`.
+
+Idris witness: `sBeta`, three explicit contractions.
+
+## Scope and remaining obligations
+
+The Idris witnesses quantify over symbolic free atoms. They do not yet establish
+substitution lemmas for arbitrary compound operands, confluence, or operational
+equivalence of the ATS evaluator. Unlambda is strict and effectful: beta equality
+of pure SKI terms alone cannot justify reordering output, input, delay, or
+continuation operations.
+
+SPARK verifies Ada heap safety and contracts. It does not check these lambda
+proof terms or the Idris compiler. The production argument additionally needs
+ATS-to-model simulation, a checked FFI contract, and correspondence evidence for
+the Idris heap abstraction and the concrete Ada implementation.

verify.sh

@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+# 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.
+
+set -euo pipefail
+
+ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+IDRIS_DIR="$ROOT/idris"
+ADA_DIR="$ROOT/ada"
+ATS_DIR="$ROOT/ats"
+
+# Guardrail only: semantic review and compiler checks remain necessary.
+if grep -RniE '\b(believe_me|sorry|admit|assert_total|assert_smaller)\b|pragma[[:space:]]+Assume' \
+    "$IDRIS_DIR" "$ADA_DIR" "$ATS_DIR"; then
+  echo "FAIL: prohibited proof escape hatch detected" >&2
+  exit 20
+fi
+
+for tool in idris2 patsopt gprbuild gnatprove; do
+  if ! command -v "$tool" >/dev/null 2>&1; then
+    echo "FAIL: $tool not installed" >&2
+    exit 2
+  fi
+done
+
+mkdir -p "$ROOT/build"
+patsopt -tc -s "$ATS_DIR/heap.sats"
+patsopt -tc -s "$ATS_DIR/state.sats"
+cd "$IDRIS_DIR"
+idris2 --total --check Main.idr
+idris2 --total --check LambdaProofs.idr
+idris2 --total -o unlambda_model Main.idr
+test "$(build/exec/unlambda_model)" = 'step: advanced'
+
+cd "$ADA_DIR"
+gprbuild -p -P heap_model.gpr
+test "$("$ROOT/build/heap_demo")" = 'heap contract smoke test: PASS'
+# All required checks must be proved; ordinary successful invocation is insufficient.
+gnatprove -P heap_model.gpr -u heap_model.adb --mode=all \
+  --checks-as-errors=on --warnings=error --report=all --level=2
+echo "PASS: ATS interfaces, Idris model, and allocation-counter heap."