File size: 1,647 Bytes
d8df231 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 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.
-->
# 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.
|