| -- 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. |
|
|
| module Main |
|
|
| import Data.Nat |
|
|
| %default total |
|
|
| ||| Abstract execution status. Resource exhaustion is not successful termination. |
| data Status = Running | Halted | OutOfFuel | OutOfMemory | Failed |
|
|
| ||| Minimal control term for the first machine milestone. |
| ||| Extend only after the selected Unlambda dialect is specified. |
| data Term = PrimI | PrimK | PrimS | Apply Term Term | DelayedTerm Term |
|
|
| record Machine where |
| constructor MkMachine |
| control : Term |
| fuel : Nat |
| status : Status |
|
|
| ||| A transition outcome always records the next explicit machine status. |
| data Transition = Advanced Machine | Finished Machine |
|
|
| ||| Fuel is consumed exactly once for an ordinary transition. |
| consumeRunning : Term -> Nat -> Machine |
| consumeRunning t Z = MkMachine t Z OutOfFuel |
| consumeRunning t (S k) = MkMachine t k Running |
|
|
| consumeFuel : Machine -> Machine |
| consumeFuel (MkMachine t n Running) = consumeRunning t n |
| consumeFuel (MkMachine t n Halted) = MkMachine t n Halted |
| consumeFuel (MkMachine t n OutOfFuel) = MkMachine t n OutOfFuel |
| consumeFuel (MkMachine t n OutOfMemory) = MkMachine t n OutOfMemory |
| consumeFuel (MkMachine t n Failed) = MkMachine t n Failed |
|
|
| ||| The transition function is intentionally a control-model stub until |
| ||| the full Unlambda operational semantics are fixed in spec/. |
| stepControl : Machine -> Transition |
| stepControl m@(MkMachine _ Z Running) = Finished (consumeFuel m) |
| stepControl m@(MkMachine _ (S _) Running) = Advanced (consumeFuel m) |
| stepControl m = Finished m |
|
|
| ||| A structural fact: consuming fuel never increases the fuel counter. |
| natLteRefl : (n : Nat) -> LTE n n |
| natLteRefl Z = LTEZero |
| natLteRefl (S n) = LTESucc (natLteRefl n) |
|
|
| natLteNext : (n : Nat) -> LTE n (S n) |
| natLteNext Z = LTEZero |
| natLteNext (S n) = LTESucc (natLteNext n) |
|
|
| fuelDoesNotIncrease : (m : Machine) -> fuel (consumeFuel m) `LTE` fuel m |
| fuelDoesNotIncrease (MkMachine t Z Running) = LTEZero |
| fuelDoesNotIncrease (MkMachine t (S k) Running) = natLteNext k |
| fuelDoesNotIncrease (MkMachine t n Halted) = natLteRefl n |
| fuelDoesNotIncrease (MkMachine t n OutOfFuel) = natLteRefl n |
| fuelDoesNotIncrease (MkMachine t n OutOfMemory) = natLteRefl n |
| fuelDoesNotIncrease (MkMachine t n Failed) = natLteRefl n |
|
|
| ||| One running transition consumes exactly one unit, not two or zero. |
| positiveFuelConsumesOne : (t : Term) -> (n : Nat) -> |
| fuel (consumeFuel (MkMachine t (S n) Running)) = n |
| positiveFuelConsumesOne t n = Refl |
|
|
| ||| Heap exhaustion remains distinct from generic failure and termination. |
| memoryExhaustionIsPreserved : (t : Term) -> (n : Nat) -> |
| status (consumeFuel (MkMachine t n OutOfMemory)) = OutOfMemory |
| memoryExhaustionIsPreserved t n = Refl |
|
|
| ||| Resource exhaustion is explicit when a running machine has zero fuel. |
| zeroFuelIsNotHalted : (t : Term) -> status (consumeFuel (MkMachine t Z Running)) = OutOfFuel |
| zeroFuelIsNotHalted t = Refl |
|
|
| main : IO () |
| main = do |
| let initial = MkMachine PrimI 1 Running |
| case stepControl initial of |
| Advanced next => putStrLn "step: advanced" |
| Finished next => putStrLn "step: finished" |
|
|
