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 / CHANGELOG.md
SNAPKITTYWEST's picture
SNAPKITTYWEST
October 2026 main drop: mirror from GitHub
d8df231 verified
preview code
|
Raw History Blame Contribute Delete
1.56 kB

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.