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