Finch VM Contract

Canonical source: vocabulary/language/FINCH_VM.md. This page is refreshed from the Finch repository when the website builds.

Contract version: FINCH-VM-TYPED/1

Finch is a conversational runtime in which ordinary human input starts an agent turn and the provider may return a Lisp or Co-Forth program through the direct response-wire boundary or a provider-native program tool. Lisp and Co-Forth compile to one internal typed stack IR, are verified, and execute in the recipient’s local VM. A text-only provider response is source, not display prose: use say for human-visible language. Shell stdout remains display content and is never executable VM input. Never emit internal IR or CLIF.

Every executable IR operation has a canonical Co-Forth spelling. Lisp may provide tree-oriented syntax and bounded macro expansion, but its expanded forms lower directly to that same IR; it does not gain Lisp-only execution semantics or serialize through reparsed Forth text. This preserves source origins while allowing an inspected Lisp program to be represented by canonical Co-Forth.

The submission envelope may identify the source language explicitly (language: "lisp" or language: "forth"). For compact tool calls that omit it, Finch infers Lisp only when the first non-whitespace character is ( and otherwise treats the source as Forth; the resolved language is recorded before execution. Co-Forth can be incrementally buffered because words are read left-to-right, but executes only at an explicit program boundary. Lisp is buffered until its delimiters balance. Source framing is independent of output streaming: each say emits a chunk as it executes.

The receiving host, not the model, attaches a stable source identity to every submission (for example a script path, provider response ID, scheduled callback, or editor buffer). Diagnostics and effect origins preserve that identity through lowering and suspension/resume; a program cannot forge its own provenance by placing a string in source text.

The normal visible response is a Lisp program:

(say "Your response to the human")

Prefer Lisp for model-authored programs with branching, bindings, closures, or more than a tiny stack pipeline. Co-Forth is the compact, incrementally bufferable alternative:

"Your response to the human" say

Use a larger program only when computation, memory, automation, scheduling, or child agents are needed. Do not wrap programs in Markdown when submitting through submit_program.

Before composing positional stack operations, call get_vm_state. Submit the observed manifest generation and VM revision. The stack is reported bottom-to-top; the last value is the top.

Every callable word/function has input types -> output types ! {capability requirements}. An empty requirement set is pure. Requirements are inferred transitively; declaring a program pure cannot hide a capability-bearing call. The receiver independently verifies types, stack shape, effects, grants, resource selectors, revisions, and budgets.

Closed tagged sums use the shared compact type spelling variant{none|some(int)|metadata(record{name:string})}. Each tag carries either no payload or one typed payload. This spelling is accepted identically in Lisp annotations and Co-Forth signatures; values and exhaustive matching use verified vocabulary/IR operations rather than an untyped tag string convention. Lisp constructs them with (variant variant{none|some(int)} :some 42); Co-Forth uses 42 variant<variant{none|some(int)},some>. Both lower to MakeVariant, whose verified IR carries the full closed type, selected tag, and optional payload type. Safe projection also shares one IR operation: Lisp (variant-get value :some) and Co-Forth value variant-get<some> return option<int>. A matching payload-free tag returns some(unit); a different tag returns none. Lisp’s exhaustive closed-variant match is syntax over VariantGet, ordinary option branches, locals, and verified merge edges; Co-Forth can compose those same public operations directly.

Structured option branches are part of the common semantics: Co-Forth if-some ... else ... then and Lisp (match-option option (some name ...) (none ...)) both lower to typed branch edges. The some edge receives T, the none edge consumes the option, and the two edges must merge with the same verified stack/value type; no dynamic type test or thrown unwrap is needed for ordinary option control flow.

Structured result branches use the same typed control-flow rule: Co-Forth if-ok ... else ... then gives the ok payload to its then edge and the err payload to its else edge; Lisp (match-result result (ok name ...) (err name ...)) binds the corresponding payload lexically. Both arms are required and must merge with the same verified stack/value type. Lisp may use the type-directed (match value arms...) spelling for these two exhaustive tagged forms. It also accepts (match bool (true ...) (false ...)) and integer literal arms ending in a required (_ ...) default; all variants select the same verified branch IR and never fall back to dynamic pattern dispatch.

For a statically typed record, Lisp also accepts one total (record ((field binding) ...) body...) arm. It lowers only to ordinary typed record-get, unwrap, and local instructions; Co-Forth uses those same operations directly, so record destructuring introduces no frontend-specific runtime behavior.

Co-Forth also supports an integer case with of ... endof arms and an optional otherwise. It lowers to the same verified branch edges, has no fallthrough, and requires every reachable arm to leave the same stack row. It is not a dynamic dictionary dispatch or C-style switch.

Capabilities are positive, scoped grants such as:

fs.read(${workspace}/src/**)
fs.write(${workspace}/generated/**)
memory.read(tree=session,path=**)
agent.spawn(max_depth=2,max_children=4)
schedule.create(policy=daily-report)
session.emit

Capability parameters compose through calls. Argument-dependent filesystem requirements use a restricted template AST over immutable refined path values, never string replacement. Each template has a conservative upper bound (for example ${workspace}/reports/**); Finch substitutes the actual argument at a call site and checks the canonical resolved path again at the host boundary. If it cannot prove the result remains within the bound, verification fails.

Response/UI effects are stack-neutral in the shared IR. say and output-* consume their arguments and leave no synthetic unit on the persistent stack; consecutive calls compose without drop. The Lisp frontend represents effect-only forms as unit internally so they remain valid expressions, then removes that implementation detail at its top-level boundary.

Capabilities do not appear as forgeable data-stack tokens. Pure means the inferred requirement set is empty. session.emit is granted by the active response session; memory, scheduling, agents, tools, files, processes, network, and automation require their own availability and grants.

Static requirements are inferred and exposed before execution for declaration checks and permission preview. Every structured execution outcome retains this complete set as inferred_capabilities; required_capabilities is only the currently missing, concretely instantiated subset (for example, a static path-argument template versus the actual requested path). A missing grant pauses only when execution reaches the concrete capability boundary, so earlier pure work and streamed say output are not discarded because an unreachable branch has an effect. Dynamic resources are checked again at that boundary. Grants may be once, task, session, project, or global and may be revoked. Child agents receive only an explicitly attenuated subset.

Errors are structured by phase and stable code. Correct the program using expected/found types, source origin, and VM/manifest revisions; never scrape a formatted error string. Failed or cancelled executions do not commit VM-local stack/dictionary changes. External effects are separately audited and cannot be undone by rolling back the VM.

Use get_language_definition for complete grammar, get_vm_state for the current stack/revision, and search_word followed by inspect_word for a core word, persisted definition, or source syntax such as while/define. Source syntax is deliberately reported without a pretend runtime signature. Inspect definitions instead of inventing words.

When desktop automation is enabled, the typed vocabulary exposes automation-availability, automation-displays, automation-windows, automation-click, and automation-type. These return serialized operation results as strings and remain capability- and availability-checked at the host boundary.

Child-agent handles are opaque, persistent task<agent-result> values: they carry a daemon task ID and their declared terminal type, not a process-local future. A handle may remain on the VM stack across later program turns. agent-spawn starts bounded work. agent-poll returns a nonblocking typed snapshot record with task-id, agent-id, status, task, role, provider-model, depth, and complete. agent-await joins and returns a typed result record with task-id, agent-id, status, final-message, diagnostics, turns, elapsed-ms, provider-model, and depth; programs never need to parse scheduler JSON or scrape a final-message string. agent-cancel requests cancellation. agent-spawn-with accepts one exact typed record with task, role, background, provider, model, context-refs, capabilities, max-turns, timeout-ms, and max-output-bytes fields. Each context reference is {kind:string,id:string,sha256:string}; the list is bounded to 64 entries and each digest must be 64 hexadecimal digits. Empty background/provider/model strings mean no override; all budgets are positive and host-bounded. Provider/model names go through the scheduler’s configured-profile resolver rather than capturing the frontend’s current provider. Poll and await expose starting-context-hash, a deterministic digest bound to the task, role, background, budgets, parent ancestry, selected provider/model, VM revision/manifest generation, declared references, and inherited grant ceiling. A reference digest identifies expected content. Hosts register immutable bounded UTF-8 artifacts and receive the computed {kind,id,sha256} reference; child creation resolves and verifies every byte before a task is allocated, and includes the verified contents in the child’s explicit data context. capability-list returns the reusable grants visible within the current ProgramRun ceiling as typed metadata paired with opaque resource<capability-grant> values. Put only the desired resource values in capabilities; an empty list delegates no non-intrinsic authority. The compact agent-spawn word intentionally inherits the caller’s whole creation-time ceiling. Grant resources are revalidated for policy, scope, expiry/revocation, and parent containment when the child is created; printed UUIDs and JSON requirement metadata are never authority. Scheduler ancestry and ownership are checked for every operation. Child providers receive submit_program plus read-only language/VM discovery tools. Filesystem and nested-agent work must use verified tree-list/file-*/agent-* words through that submission; the scheduler does not expose direct Read/Glob/Grep or direct agent-control tools that bypass the child’s typed grant ceiling.

Pure zero-argument closures may use (defer :cpu (lambda () ...)) to run on Finch’s bounded local worker pool. It returns task<T> with an explicit cpu_fiber owner kind; captured values are immutable snapshots and the worker has a private stack/frame set. task-poll has type task<T> -> record{task:task<T>,value:option<T>} and never blocks. Returning the handle makes a later poll, join, or cancellation explicit without a hidden borrow or a privileged multiple return. task-join has type task<T> -> T; if the worker is still running it preserves the parent continuation as a scheduler suspension instead of blocking the UI/event loop. task-cancel consumes a CPU task handle and requests cooperative cancellation at the worker’s next VM boundary. CPU task operations reject agent-task handles; agent coordination remains agent-* and is a separate protocol.

yield consumes and publishes one typed value and returns the VM’s remaining frames to the Finch event-loop trampoline as a saved ProgramRun suspension. unit yield / (yield) is the plain cooperative-timeslice case; the interactive provider-wire runner automatically resumes only that unit form. Other hosts choose their own scheduling policy and may inspect the payload. It may occur more than once in one program and does not expose an LLM-authored continuation value. A callable that can publish values advertises yields<Y,unit> after its ordinary stack/effect signature. That metadata is serialized with function and closure types, composes through calls, and is checked again against IR; it describes control flow, not authority. fiber<Y,R> is a first-class, checkpointable handle over this same typed control effect, with a declared resume type (currently unit). fiber-next returns an ordinary result<Y,variant{end(R)}>; fiber-join discards yielded values to obtain R, and fiber-cancel leaves a deterministic cancelled state. Producer registry changes are part of the ProgramRun transaction, so a failed outer program cannot consume a yield. Finch does not add a second generator-only yield or hidden multi-return protocol. Known finite values use typed lists, host-backed iteration uses explicit cursor resources, and user-defined lazy producers use fibers.

vm-vocabulary is a pure VM inspection operation that returns the current serialized typed vocabulary. Use it (or the external get_vm_state tool) instead of guessing callable names.

mcp-call is the explicit managed-JSON fallback for a host-configured MCP tool. It consumes a server string, tool string, and json, then returns json. The runtime derives the concrete mcp.call(server,tool) requirement from those first two arguments before dispatch; installing an MCP transport does not grant it. Schema-derived namespaced words may provide narrower static types, but unsupported schemas stay at this boundary rather than becoming dynamic. A discovered tool with an admissible object schema is published as mcp.<server>.<tool> with one typed-record input; unsupported but well-formed property shapes use one managed json input instead. Each discovered binding carries a schema hash and changes the manifest generation when installed.

Structured values are part of the shared ABI. some and none construct option<T> values; is-some tests one and unwrap extracts its payload (returning a structured E-OPTION-001 diagnostic for none). ok and err construct result<T,E> values, is-ok inspects which branch was produced, and result-unwrap/result-error project the corresponding payload with a structured diagnostic on the wrong branch. These values remain typed when crossing the VM/runtime boundary and are rendered to legacy Lisp callers as (some value), (none), (ok value), or (err value).

Inside a typed function whose sole declared return value is result<R,E>, Lisp try and Co-Forth ? inspect one result<T,E> once. An ok(T) continues with T; an err(E) returns that error directly from the current function, discarding intermediate stack values. This lowers to a verified cold error edge, not a mutable error accumulator or a catchable exception. Use match-result / if-ok at the caller’s boundary to recover. Top-level forms and closures cannot use propagation because they have no declared result return target.

json-parse is pure and returns result<json,string> rather than throwing on untrusted input. json-get takes a managed json value and a string field name, returning option<json>; it only looks up object fields and never treats a supplied string as code, a path, or authority. Convert a known scalar through json-as-string, json-as-int, json-as-float, or json-as-bool, each of which returns an option rather than coercing or guessing. json-index similarly returns an option for an array element, and json-keys returns a typed list<string> (empty for a non-object). json-stringify explicitly returns compact JSON text.

json-as-map explicitly normalizes a JSON object to option<map<string,json>>, preserving its field strings (including spaces) as map keys. It returns none for non-object JSON and never silently converts an object into a typed record.

Co-Forth also accepts a pasted JSON object literal directly when its first key is quoted (for example {"first name":"Ada"}). It pushes managed json, not a record or map. { name: "Ada" } continues to be the typed-record grammar. Commas are optional separators in Co-Forth list source, so [1, 2, 3] and [ 1 2 3 ] are equivalent.

Typed maps and records are also shared source values, distinct from arbitrary json. Maps accept typed keys and values: Lisp spells construction (map key value ...), while Co-Forth spells map{ key value ... }map. map-get returns option<V>, map-set returns a replacement map, and map-entries returns an insertion-ordered list<record{key:K,value:V}>. String-keyed maps are the appropriate normalized representation for external keys such as "first name".

Typed records are immutable heterogeneous products with statically known identifier-like field names: Lisp { :name value ... }; Co-Forth { name: value ... }. (record-get record "name") and record "name" record-get return option<T>. (record-set record "name" value) and record value "name" record-set return a replacement record after verifying the literal field name and replacement type. A record may hold a typed closure; method invocation remains explicit and never grants ambient mutable self access. Arbitrary JSON object keys—including keys with spaces—remain at the json-get or string-keyed-map boundary rather than being silently coerced into typed record fields.

Typed lists are homogeneous immutable values: Lisp spells construction (list value ...) and Co-Forth spells [ value ... ]. list-append consumes a list and matching element and returns a replacement list; list-get and list-length inspect it. ['] word remains the distinct Co-Forth quotation syntax. Empty list literals require an explicit element type and are therefore intentionally not inferred by either source form: use (empty-list type) in Lisp or empty-list<type> in Co-Forth. list{ value ... }list remains a compatibility spelling. list-uncons consumes list<A> and returns option<record{head:A,tail:list<A>}>, giving both frontends a safe ordinary-word basis for list patterns and range-style traversal without compiler-only multiple returns. Lisp (match items (empty ...) (cons head tail ...)) is an exhaustive surface spelling over that word, the shared option branch, record projection, and typed locals. Co-Forth composes those same public words with if-some ... else ... then.

Lisp symbols are identifiers, not strings: 'name is quoted data (equivalent to (quote name)), whereas (say "name") contains text. Co-Forth uses bare tokens for executable dictionary words; 'name produces a typed symbol value and ['] word execute passes an execution token as data. These remain distinct from both a dictionary word reference and a string.

process-run accepts a command path and a list of argument strings. It invokes the executable directly, never through a shell, and requires an explicit process.run capability and approval.

say is stream-capable: each invocation yields an output chunk to the active session sink while the complete buffered response remains available in the execution result. It appends its text exactly: it adds neither a space nor a newline. Use multiple say operations for progressive UI updates only, and include separators in the text yourself (for example, "result: " say 2 3 + int-to-string say "\n" say). s"..." remains an equivalent Forth-compatible spelling. There is no separate streaming language.

At the execution boundary, chunks are represented as ordered typed side-effect events. A session may render, buffer, inspect, test, or reject those events; the VM does not require the UI to mutate state synchronously during interpretation.

The portable event envelope contains the VM protocol version, monotonically increasing sequence, capability requirement, typed event payload, expected typed result row (empty for terminal emits), and source origin. A harness pairs the sequence with its execution ID as an idempotency key, records the result in its effect journal, validates the typed result against the awaited output row, then resumes the serialized VM continuation. A VmResume { execution_id, sequence, response } acknowledges that exact event and does not dispatch the host operation a second time. Its response is exactly one of result { values }, denied { reason }, or cancelled { reason? }; a stale sequence is rejected without consuming a newer continuation. The terminal effect-journal state records the same choice as acknowledged, denied, or cancelled. Per-run effect observers receive an awaited request before authorization or local dispatch, so a host can persist or route that boundary without waiting for a synchronous adapter. An embedder may choose the portable deferred-host mode, in which every approved awaited request (file, process, network, proposal, and so on) suspends and must receive this correlated VmResume; Finch’s compatibility submission mode still dispatches its installed host bindings synchronously except for editor proposals. Finch projects these events onto its reactive WorkUnit/shadow-buffer UI; another harness may instead use a browser, IDE, voice interface, or audit log. say is only a durable response-append event, never a direct terminal write. Rich replaceable/progress output will use host-issued opaque output handles rather than guessed string or symbol IDs.

Editor-backed proposals are language-neutral host operations, not a property of Forth. An explicit Lisp/control-plane proposal may carry Bash, Python, Lisp, Forth, or another supported script:

The outer event loop owns the editor and returns execute, chat, or cancel. execute submits the edited payload through that language’s normal validator and capability boundary; chat returns the edited buffer as context without running it; cancel discards it. Ordinary Forth execution never opens an editor implicitly.

The current typed surface spells this as three strings so it remains equally available in both frontends: (proposal-open "bash" "Regenerate local indexes" "#!/usr/bin/env bash\\n...") or s"bash" s"Regenerate local indexes" s"#!/usr/bin/env bash\\n..." proposal-open. It requires program.invoke and returns option<result<string,string>>: none means cancel, some(ok source) means accepted artifact source, and some(err context) means chat. Acceptance returns data only; it never executes the proposal. A Finch payload must be submitted again through the typed verifier, while an external script follows the separately authorized script workflow. The requirement is concrete at the call boundary (program.invoke(language="python"), for example), so granting one artifact language does not confer authority to open another.

Workspace file access uses refined paths rather than raw strings. (path "relative/name") constructs a path constrained to the workspace selector; (file-read path) returns bytes, and (file-write path bytes) returns unit. The host canonicalizes and rechecks the path, so .., absolute paths, and wildcard-bearing runtime arguments cannot escape the declared selector. A submission that needs file access produces an approval prompt when the corresponding scoped grant is absent; after approval, Finch resumes the saved execution ID and its verified frame. Do not resubmit source: doing so would repeat any prior say output or completed host effects.

Whole-machine scope is explicit rather than an absolute-string escape hatch. A host may install root<host-machine> (normally a narrower directory; / only after an intentional full-machine decision). (host-path "relative/name") produces the distinct path<host-machine> type, which only host-file-read and host-file-write accept. Installing the root is availability, not a grant: the concrete file.read(${host-machine}/...) or file.write(${host-machine}/...) capability must still be approved, and the host canonicalizes containment again on every call. Ordinary path / file-read never widen to this root.

Hosts may also install root<project> and root<task.output> independently of the process workspace. project-path is accepted only by project-file-read / project-file-write, while task-output-path is accepted only by task-output-file-read / task-output-file-write. This lets a task receive, for example, project-read plus task-output-write without receiving workspace write or whole-machine authority. Root installation still grants nothing; every concrete file operation is checked against its own selector.

file-size(path) and file-slice(path, offset, length) share the same refined file.read(path) requirement. A slice is bounded (currently 8 MiB maximum per call) and may be shorter at EOF, so large CSV/text/binary processing can keep only a bounded window in VM memory. tree-list(path, max_entries) returns a deterministic record containing a bounded list of {path:string, kind:string, size:int} metadata records and a truncated:bool field. It scans and returns at most 100,000 entries, rejects symlinks and unsupported file kinds, and grants no authority to returned path strings; refine a selected string through path before another file call. file-lines-open(path) mints a ProgramRun-owned opaque stream<string>; stream-next returns bounded UTF-8 option<string> records (1 MiB maximum line) and stream-close releases the stream. The initial path grant covers later stream operations only because the stream is unforgeable and host-validated on each call. file-lines-next and file-lines-close remain compatibility aliases. csv-open(path) mints a distinct stream<list<string>>; stream-next returns bounded option<list<string>> CSV records and stream-close releases it. It parses quoted, comma-containing, and multiline fields rather than treating physical lines as records; malformed quote boundaries fail with a host diagnostic. Both stream kinds use the same opaque-handle pattern; workbook-open(path) and workbook-sheet-open(path, sheet) use it for XLSX/XLS/ODS rows too and must not smuggle an ambient filesystem path back into VM values. The current workbook adapter caps the decoded host sheet at 10 million cells; only one row crosses through stream-next, but this is not yet a true streaming ZIP/XML decoder. csv-summary(path, max_rows) is the bounded aggregate path for model inspection. It consumes no stream handle and returns managed json describing the header and per-column empty/non-empty and numeric min/max/mean statistics for at most 100,000 data records. The concrete path still determines the file.read request; the row bound is work policy, not authority. workbook-range(path, sheet, start_row, start_column, row_count, column_count) returns at most 10,000 selected cells as list<list<string>>, using zero-based offsets. workbook-summary(path, sheet, max_rows) treats the first row as headers and returns the same bounded column facts plus the sheet name. Use workbook-sheets(path) to discover valid names without reading cell contents.