Hugging Face's logo

Snapkitty
/
unlambda-idris-spark

snapkitty
october-2026-drop
unlambda
idris
ats
ada
spark
lambda-calculus
formal-verification
Model card Files
xet
 Community
unlambda-idris-spark / docs /releases /v1.0.0.md
SNAPKITTYWEST's picture
SNAPKITTYWEST
October 2026 main drop: mirror from GitHub
d8df231 verified
preview code
|
Raw History Blame Contribute Delete
2.52 kB

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.

This release does not claim full interpreter correctness, cross-language correspondence, Windows runtime support, or production certification. The delivery backlog 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. Published v1.0.0 archives remain unchanged. Commercial permissions require a separate written agreement; the donation destination remains pending.