| (* | |
| 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. | |
| *) | |
| (* Typed contract for the planned machine. Implementations are pending. *) | |
| staload H = "./heap.sats" | |
| abstype term_ref = ptr | |
| datatype status = | |
| | Running of () | |
| | Halted of () | |
| | Failed of () | |
| | OutOfFuel of () | |
| | OutOfMemory of () | |
| datatype control = | |
| | Ctrl_Term of term_ref | |
| | Ctrl_Value of $H.node_ref | |
| datatype frame = | |
| | F_EvalArg of term_ref | |
| | F_ApplyFun of $H.node_ref | |
| typedef input_state = @{ | |
| buffer=List0(uchar), cursor=size_t, current=Option(uchar) | |
| } | |
| typedef machine_state = @{ | |
| control=control, | |
| kont=List0(frame), | |
| heap=$H.heap, | |
| input=input_state, | |
| output=List0(uchar), | |
| fuel=intGte(0), | |
| status=status | |
| } | |
| fun state_invariant_holds (state: machine_state): bool | |
| fun state_step (state: machine_state): machine_state | |