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