Trellis: Design Document

Trellis is the project, the specification layer, and the IDE. Soil is the target language it lowers to. The name reflects what the tool does: vibes grow, the trellis shapes them.

Status: design phase. This document records every decision made so far, the reasoning behind each, the items explicitly deferred, and the planned build order. It is intended to be the single reference for the project until the .tr grammar and lock schema documents supersede the relevant sections.

1. Vision

1.1 The core thesis

If an AI agent writes the implementations, the human-authored layer of a program should consist of specifications, types, tests, and structural constraints rather than code. The target language those implementations are written in should be designed to be easy for a machine to write and easy for a checker to verify, rather than pleasant for a human to type. Soil is that target language; Trellis is the specification layer and the tooling that lowers specifications into Soil.

Soil is, in effect, the assembly language of vibe-coding: a small, strict, verifiable language that humans read but rarely write.

1.2 The shape of a project

Both intended users write a slice. An individual writes a small program that calls foreign libraries. A team writes a small module inside a large foreign codebase. In both cases Trellis owns a bounded region of the program and treats everything outside that region as untrusted foreign code with a tested boundary. The scope pitch is: Trellis owns the region you care about being right; the rest of your stack is FFI.

Trellis remains a vibe-coding language, with two tiers:

• Unchecked vibing: an agent writes the .tr files and an agent lowers them. The human reads nothing. This is still strictly better than vibe-coding as commonly practiced, because every function has a type that checks and tests that pass, even if no human looked at them.
• Disciplined vibing: the human writes the .tr files and an agent lowers them. The human’s attention goes entirely to specifying and judging; they never write a loop, a match, or a signature. They are forced to think about correctness, not about code.

Both tiers produce identical artifacts, so a project can move from unchecked to disciplined one function at a time: a human takes over a .tr file, reviews or rewrites the tests, and marks the definition accepted. This is the migration path from “prototype I vibed” to “thing I trust” without a rewrite. The “humans write tests” rule concerns what gates lowering in the disciplined tier, not what workflows are permitted.

1.3 Users

• First user: the author, building small projects that use Python libraries.
• Target users: both individuals writing small projects against libraries, and large teams migrating small slices of code within a larger codebase.
• First users beyond the author: other individuals on their own small projects. This keeps team tooling deferred but pulls installation and the first-hour experience forward, since each user cannot be hand-held.

The rule adopted for resolving the tension between these two: decisions that affect format or semantics must be made now to accommodate both users; decisions that are tooling only are made in the simplest form for the first user and grown later.

1.4 Design tenet

Nothing that affects correctness exists only in an agent’s context. Signatures, human answers to agent questions, export pins, style examples, and every other input to a lowering lives in a hashed file. An agent’s “memory” of a function is its lock entry and its last lowering, nothing more.

2. The three components

2.1 Soil: the target language

A small, strict, refinement-typed ML with effect tracking, designed as an agent target and a glue language for tying other languages together.

2.2 Trellis: the specification layer

A file format and toolchain in which humans write prose, types (optionally), and tests, and an agent lowers each definition to Soil under the supervision of a type checker, a refinement checker, and the tests.

2.3 Trellis IDE and build system

A graph-oriented IDE over the definition graph, with an interactive lowering interface, and a build system that compiles a TOML declaration of dependencies down to Nix.

3. Soil language design

3.1 Surface language

3.2 Refinement types, not full dependent types

Full dependent types (Agda/Idris style) were considered and rejected for v1. They are hard to infer, would discard ML inference, and agents write proofs poorly. Refinement types (Liquid Haskell / F* style) keep inference, let the agent write specifications rather than proofs, and discharge obligations through an SMT solver. Full dependent types remain a possible future escape hatch for the small fraction of functions where SMT cannot help.

Where inference stops: types may mention terms only if those terms are total and fall in a decidable fragment (linear arithmetic, uninterpreted functions, lengths of lists and sets). Beyond that, the refinement is unproven and the function is demoted (see §6.4).

Refinements are erased at runtime in release builds only if they were proven (see §3.9).

Refinements may eliminate error cases. A function returning Result may carry a postcondition such as {r | is_ok r} under a precondition, allowing callers that can discharge the precondition to skip the match. This pushes obligations up the call chain, which is the intended ratchet behaviour: a caller that cannot prove the precondition simply matches on the Result as normal. The Err arm must still exist at runtime in unrefined/debug builds, because the refinement is erased.

3.3 Effects

Effects are tracked as effect rows on types, not as monads. Rows compose without the transformer-stacking problem, and row-polymorphic higher-order functions inherit the effects of their arguments automatically (so map over a total function is total).

The effect system is purely a tracking mechanism. There are no first-class algebraic effect handlers and no effect runtime. This keeps backends simple. The consequence accepted: no mock handlers for testing, which is addressed instead by the capability model (§3.5).

Effect lattice:

• total: the empty row; the function provably terminates and has no effects.
• div: may diverge.
• panic: may crash at runtime (indexing, division, unproven refinements, FFI).
• io: touches the world.
• ffi: calls foreign code; implies panic.
• User-declared algebraic effects are a possible future extension but not part of v1.

There is no exn effect and no exceptions. Result a e is the error channel — success type first, as in OCaml and Rust. Haskell’s error-first Either e a order exists so the partially applied constructor can be the Functor/Monad instance, a motivation that cannot arise in Soil (no type classes, no higher-kinded abstraction), so the more widely known order wins. Cases that cannot be expressed as Result and cannot be proven safe by refinement carry panic.

Function application annotations (the Trellis feature of declaring what a function may call) fall out of the effect system: f may call g iff g’s row is a subset of f’s row. The graph view of the IDE is therefore also an effect-flow diagram.

3.4 Totality

Totality is tracked as the absence of div in the effect row. Termination is established by an Idris/Agda-style termination checker: structural decrease on an argument, or a user-supplied measure (decreases n). This is preferred over Koka’s syntactic approach because an agent can usually supply the decreasing argument, and the annotation is cheap for both the agent to write and the checker to verify. If the checker fails, the function acquires div and the manifest may refuse it.

Only total functions may appear in type indices (refinements), because the type checker must normalize them. Totality is thus an effect at the term level and a gate at the type level.

Policy: total by default, div opt-in (the Idris policy), which is the right default for an agent-written language.

3.5 Capabilities

io is not ambient. A function that performs I/O receives an opaque capability value representing the permission, and the io effect in its row indicates that it uses it.

type Fs = opaque
type Net = opaque
type Clock = opaque

read_file : Fs -> Path -> io (Result String FsError)
now       : Clock -> io Time

World is the root capability, handed to main by the runtime (or by the host in embedded mode). Sub-capabilities are derived from it and cannot be constructed any other way because the types are opaque.

main : World -> io Unit
main w =
  let fs = world_fs w in
  ...

Testing: the prelude provides fake capabilities of the same type (fake_fs [("config.toml", "...")]), so a function under test cannot distinguish a real capability from a fake. The capability is the handler, passed by hand; no effect handlers are needed.

Capability set (confirmed): Fs, Net, Clock, Env, Proc, Rand, Py.

Effect row stays a bare io. Naming capabilities in the row (<io:fs,net>) was considered and rejected for v1 as the capability arguments already carry the same information.

FFI needs a capability too. A Python call takes Py. This makes FFI-calling functions visible, allows stubbed fakes for tests, and makes a prelude fork without a Py constructor into a Python-free sandbox.

Boilerplate accepted: the individual user writes read_file fs path rather than read_file path. A with fs sugar for implicit passing was considered and rejected, since implicit parameters are a form of type classes.

Rationale for deciding this now: the capability style must be present in every io signature in the prelude from the start. Retrofitting it would invalidate the corpus. A default “real world” capability keeps the individual user’s CLI experience unchanged.

3.6 Polymorphism

Parametric polymorphism only. No type classes, no functors, no overloading of any kind. This is accepted as painful for humans and acceptable for an agent target, and it fits “one way to do things.” Global coherence constraints of a class system would also conflict with the per-file incremental model.

Consequences accepted:

• No overloaded numeric literals. There is no general-purpose Int or String type; see §3.12. Literals have a default type (1 is I64, 1.0 is F64, "..." is Utf8) unless annotated, as in Rust.
• Maps take an explicit comparator (OCaml Map.Make as a plain higher-order function). This is the confirmed idiom and the prelude will show it.
• Sort takes a key function (sort_by : (a -> k) -> List a -> List a), with structural compare on k. The Python idiom; agents know it.

3.7 Derived functions: eq, show, compare, hash

With no ad-hoc polymorphism there is exactly one possible eq per type, so all four are auto-derived for every type rather than opted into as in Rust.

Implementation: derived per type as new definitions (Foo::eq, etc. — :: is the namespace separator, . being reserved for field access), rather than as polymorphic primitives. The user’s reasoning was the ability to statically exclude closures and to give float types a specific treatment. (Both approaches are semantically equivalent given a kind restriction; per-type derivation was the chosen spelling.)

• Functions: deriving eq on a type containing an arrow is a type error.
• Floats: total order. NaN is equal to itself and sorts last (Rust’s total_cmp). Float therefore derives all four functions and can be a map key. Decided.
• FFI handles and abstract types: pointer identity via the opaque strategy.
• show is the JSON encoder and read/parse is the decoder. Expect tests compare on JSON. One value format for everything.
• Refinements: erased at runtime; eq on {v:Int | v > 0} is eq on Int.
• hash is FNV-1a 64-bit over the value’s canonical JSON encoding (the opaque strategy hashes the address instead). Fixed and documented because hash is language-observable and must be deterministic across platforms, runs, and toolchains; hashing the canonical bytes means “equal ⇒ same hash” follows from canonical encoding for free, and there is only one byte-form of a value in the system. Soil maps are comparator-ordered, not hash tables, so keyed/DoS-resistant hashing buys nothing. (Resolved 2026-08-22 with the soil-rt implementation plan.)
• Large structures: structural eq is O(n); accepted.

No user override for now. A first-class override mechanism was discussed and recognized as type classes returning through the side door (coherence, hash/eq agreement, equivalence-relation guarantees). Instead, types may declare one of a small fixed menu of derivation strategies:

ignored is a per-field marker, not a per-type strategy, and must carry a default expression — total calls only, with the record’s other fields in scope — which refills the field wherever a value is materialized without it (JSON decode, py_to_soil, host stubs): cached_word_count : U64 ignored = word_count(text). Because there is no mutation (§3.13), the default always reproduces the value the constructor stored, so omission from show is lossless. ignored thus means “excluded from derivation, reconstructible on demand.”

The cases a user override would have served are handled without it: case-insensitive strings via a newtype with normalization in the constructor; ignored cache fields via the ignored strategy; FFI handles via opaque. Real overrides, if ever needed, are understood to be the addition of a class system and are deferred indefinitely.

3.8 Recursion

Mutual recursion across Trellis definitions is forbidden. Content addressing becomes a tree, incremental checking is a topological walk, and every lowering has a well-defined “everything below me is already checked.”

What is lost: mutual algorithms (even/odd, recursive-descent parsers with expr/term, traversals of mutually recursive data). The workaround is the standard one: one function with sum-typed dispatch, or mutually recursive locals. Nothing is inexpressible; only decomposition into separately specified units is constrained. Parsers are expected to be the most painful case, and to hurt the agent more than the human because the mutual shape is the idiom it has seen most.

Within a single .soil file, let rec ... and ... is allowed freely. Mutual recursion among locals and module-private helpers is a Soil-level detail invisible to Trellis. This covers most parser cases: parse is one Trellis definition whose lowering contains mutually recursive locals.

Not a stdlib-only feature. The stdlib must be written in the same dialect it teaches, or the corpus shows idioms users cannot use.

Recursive types across definitions remain allowed. Types are definitions but are not lowered, so cycles among them do not break the lowering walk. They need a combined cycle hash in the lock; this is the one cycle the lock must represent.

3.9 Debug and release modes

First-class in Soil, not two separate lowerings. Two lowerings would mean two artifacts that can diverge and two hashes. Instead, one lowering carries refinements, invariant checks, panic guards, and test hooks as erasable annotations.

Release mode only erases what was proven. A demoted (unproven) refinement still runs its check in release, because tests are the trust root and an unproven claim must not become an unchecked one. Unverified code carries runtime checks forever, which is the correct incentive.

3.10 Runtime and embedding

The Soil runtime is a Rust crate exposing a C ABI, with a trivial main wrapper. Writing the runtime in Rust makes three things one codebase: embeddability as a C library, shared ownership with Rust batteries (Rust values are runtime-owned, so no FFI and no conversion), and the memory model (reference counting, Perceus-style reuse, cycle handling). The compiler may still emit C, native code, or JVM bytecode; this decision is about the runtime only.

Soil is embeddable as a C library. This is committed to from the first commit: no global state, explicit init/teardown, callable from C. It serves both users from the same compiled artifact:

• Individual user: Soil is main, Python is a library it calls.
• Migrating team: Python (or another host) is main and imports the Soil module.

Writing the runtime as a program and libraryizing it later would be a rewrite.

3.11 Backends and FFI

• v1 backend: Cranelift. The backend proper is a pure pass emitting CLIF text (golden-testable like every compiler pass); a small Rust driver feeds Cranelift for instruction selection, register allocation, and object emission — x86-64 and arm64 from one backend, no C toolchain dependency. C emission, JVM, and direct x86 were considered and deferred: direct emission means writing the two largest, least-testable compiler phases first, and C is a semantically messy target that drags in an external toolchain. See docs/bootstrap-plan.md §4.
• v1 FFI: both SysV/C ABI and Python. They are different kinds of work and share no duplicated code. The C ABI is a layout and calling-convention problem in the compiler backend and is close to free once the runtime is Rust (Rust extern "C" functions are the native case). Python is a marshalling and lifecycle problem: CPython embedded from the Rust runtime (via pyo3), GIL held around calls, PyObject* wrapped as an opaque refcounted handle, py_to_soil/soil_to_py defined over the same JSON-shaped value model as show, tests, and host stubs (one value model, never two). Sequencing: C ABI → Rust batteries → Python embedding → Python batteries, each usable before the next. Rust is for the stdlib; Python is for libraries. Node comes later.
• Hand-written bindings only in v1 for both FFIs. “Hand-written” means a specific binding exists because someone asked for it, one at a time, with a spec; it does not mean a human types it. A binding is three artifacts: a .tr spec (prose, Soil signature with effects and capabilities, auto-generated contract tests per §4.5); a shim (a Rust extern "C" function, or a pyo3 function across the GIL); and a lock entry with trust level declared-only, contract, or harvested. The corpus includes one worked example of each shim kind so the agent writes them inside a normal lowering.
• The whole-package binding generator is deferred, likely permanently. Reading a crate or package and emitting its full surface is a separate project with an unbounded difficulty profile: every foreign type system is a new translator (Rust lifetimes, traits, generics; Python’s effectively untyped .pyi stubs; C pointers and ownership); effects and capabilities are invisible in foreign signatures, so the generator either assigns everything io + ffi + panic with World (defeating the capability system) or guesses; refinements are entirely absent, so the valuable annotation is still manual; the surface is unbounded and most of it is never called, flooding the lock with untrusted entries (the same trust hole closed by rejecting helpers.tr); and subtly wrong generated bindings are memory-safety bugs surfacing far from their cause. Hand-written bindings grow the batteries layers by demand, are mostly agent-written anyway, and surface which foreign types are actually hard to map one at a time. The thing that is built, in v1, is a per-symbol binding assistant: trellis bind requests.get or trellis bind regex::Regex::new. This is vital to the first project, which is the kind of program that would otherwise have been vibed in pure Python and will call a dozen functions from a few packages; each needs a binding before any lowering that uses it can proceed, and a dozen hand-written bindings is a week of friction at the exact moment the tool’s pleasantness is being tested. The assistant is not the bulk generator and has none of its problems, because it is a lowering job with a different context bundle: the daemon fetches that one symbol’s metadata (.pyi stub, inspect.signature, docstring for Python; cargo doc JSON for Rust) into symbol.json and docstring.md, adds one corpus shim example, and runs the normal lowering loop with the normal MCP tools. The output is a .tr with prose summarized from the docstring, an agent-proposed signature with effects and capabilities, the shim, and auto-generated contract tests; the human reviews and accepts it like any other lowering. At single-symbol scale the type-mapping, effect-guessing, and refinement problems each have a human in the loop who corrects in one click, which is fine for twelve symbols and not for twelve thousand. No new agent loop, trust path, or file format. The bulk importer (trellis bind regex) is never built.
• Embedding direction in v1 is Soil-hosts-Python. The py_module build target and generated .pyi (Python-hosts-Soil) are small but post-v1.
• Generated bindings (reading documentation and types to produce FFI interfaces) will be constrained to sources with machine-readable types: C headers, .pyi, .d.ts. This feature is expected to be the largest bug source.
• Primitive types: strings, integers, floats in all the variants the FFI targets need, with the stdlib providing interop. Defining these with the FFI in mind from day one is a known requirement; the specific technical decisions are deferred (§10).
• Host stub erasure rule (confirmed): an exported Soil function with effects io, panic becomes a host-language function that may raise SoilError; capabilities become host-side objects passed in. The generated .pyi/.d.ts stub documents the effect row. Decided once, applied to every host language. In debug mode SoilError is structured and carries the trace, the demoted refinement if any, and the JSON inputs, so host test suites can locate Soil bugs.
• Foreign values are opaque handles and carry no refinements. A Py handle stays a handle; refinements could be invalidated by foreign mutation, so they attach only to Soil values. Converting a handle to a Soil value is an explicit, visible call (py_to_soil) whose cost the caller chooses to pay. Big structures stay in Python and are manipulated by handle-in, handle-out batteries functions; small results cross the boundary and may be refined after conversion. Rust-backed batteries differ: Rust structures are owned by Soil’s runtime and are therefore ordinary Soil values, refinable and potentially total, with no conversion and no capability (capabilities are about the world, not the implementing language; a Rust function that does no io takes none).

3.12 Primitive types

There is no blessed general-purpose integer or string type. The types that exist are those with unambiguous semantics, so that backends, FFI, and refinements all agree:

• Fixed-width integers: I64, U64, I32, U32, etc. Overflow is panic, or is refinement-checked away. Integer / and % are floor division and floor modulus (Python’s semantics, matching the reference-implementation language so differential tests agree without adjustment), not C/Rust truncation; a zero divisor is panic or refinement-checked away like overflow.
• BigInt: arbitrary precision, implemented in the pure core prelude (not foreign-backed, so it remains total). SMT reasons about unbounded integers natively.
• F64: total-ordered (§3.7).
• Utf8: validated UTF-8 bytes, no O(1) indexing. Bytes for raw data.

A default literal type exists for ergonomics (1 is I64, "..." is Utf8), which is the only concession. The pressure to make I64 and Utf8 feel general-purpose falls on the prelude, not the language. The Python batteries layer (§5) uses BigInt at its boundary because that is what Python numbers are.

3.13 Mutation and records

No mutation. Every function body is a term; there is no st effect and refinements are sound without an aliasing story. In-place update is recovered by the backend where possible (Perceus-style reuse analysis, as in Koka) without the language being aware.

Records only. Product types are records with named fields; there are no positional tuples and no named arguments. This is what JSON wants and what agents read best.

3.14 Module exports and types

Export lists name functions and types explicitly. If an exported function’s signature references a type that is not exported, it is an error the agent must repair, with two permitted repairs: export the type, or mark it as intentionally abstract (callers may hold values of it but not inspect them). Abstract types are therefore a deliberate feature rather than an accident.

main is an ordinary definition with effect io and a World argument; it has a .tr, tests (cram only), and a lock. soil.toml names it as the entrypoint and it receives no other special treatment.

4. Trellis: the specification layer

4.1 Trust model

Key consequences:

• A passing refinement check proves the body satisfies the agent’s claim, not the human’s intent. The IDE shows “typed” and “tested” as separate badges; only “tested” means correct.
• Tests are written by humans. If someone wants to truly vibe-code, they use their agent to generate Trellis files; the Trellis layer itself does not generate the gating tests. Agent-generated tests may exist as a clearly labelled differential tier run against the reference implementation, but they do not gate lowering.
• A cheap tightening: auto-generate property tests from refinements ({v | v > 0} becomes a QuickCheck property), so refinements are cross-checked against the trust root.
• Escape hatches (unsafe, partial, raw FFI) are written only by the human, in the spec, and every escape hatch in the project is listed in the manifest so the audit view shows where trust is concentrated.

4.2 The unit: one file per definition

A definition is a function, a type, or a module header. Each lives in its own file.

Reasoning: the unit of lowering, checking, testing, and locking is the function; file = definition aligns every per-function artifact, makes git diffs map to semantic changes, eliminates merge conflicts between people editing different definitions, makes content addressing trivial (hash the file), and naturally bounds the agent’s context.

Costs accepted: external tooling (grep, git log, GitHub review) degrades with many small files, mitigated by a “module view” in the IDE that renders a directory as one virtual file.

Helpers are not Trellis definitions. A helpers.tr magic file with reduced requirements was considered and rejected: it would be a hole in the trust model that grows until all real logic lives there. The friction of requiring a spec and tests for anything named at the Trellis level is the correct friction; if a helper is not worth specifying, it is not Trellis’s business.

Helpers live at the Soil layer in two forms:

1. Local let bindings inside a lowering, hashed as part of the parent, invisible to Trellis. Covers most cases.
2. Module-private Soil definitions (_private.soil) when the same helper is needed across several lowerings in a module. Rules:
   • Cannot be called from outside the module; cannot appear in any Trellis signature or refinement.
   • Owned by the lowerings that use them; garbage-collected when no caller references them. The agent does not accumulate a private standard library.
   • The lowering skill prefers local lets and promotes to a private helper only to avoid duplication.
   • Their hashes feed into their callers’ soil_hash.
   • The global manifest lists them as nodes flagged soil-private with no spec hash; the IDE greys them out. A module with many private helpers and few definitions is a smell the IDE flags.

Promotion path: the IDE offers “promote to Trellis definition,” which stubs a spec file with the inferred signature and existing Soil as the initial lowering, and requires prose and tests before the lock entry is valid. A helper crosses the boundary only by acquiring a spec, never by exemption.

4.3 File format

• Markdown with fenced code blocks. Prose is freeform Markdown; formal parts (signature, tests, calls) are fenced blocks with designated languages.
• Signature: a combination of English prose and Soil types, as the human prefers. Since the agent owns types, the human may write no formal signature at all.
• Minimal valid definition: frontmatter naming the definition, one sentence of prose, and one expect test. This is the onboarding story.
• Filename is identity. Filenames are static; renaming a file without updating every reference is an error, and the IDE provides refactor-rename. The lock stores the filename; hashes are for invalidation, not identity. No separate name table is needed. Filenames are lowercase snake_case for every file kind, and every file carries YAML frontmatter with a required name: a function’s equals the filename stem, a type’s is PascalCase with the filename its snake_case form (the one formal record of casing, so identity survives case-insensitive filesystems), a module’s equals its directory. File kind itself stays inferred, never declared. Frontmatter also admits optional tags, drawn from a vocabulary declared in soil.toml: non-semantic, user-extensible metadata for IDE graph filtering and CI policy, hashed under prose_hash and never an input to lowering.
• Tests are named blocks, and a file may contain any number. Names are used by the lock to report failures, by the IDE for click-to-run, and by REPL-to-test promotion to know where to append. Expect tests are call-arrow lines (("1,2") => {"tag": "Ok", "value": [1, 2]}): the function under test is implicit (file = definition), with lines bind fake capabilities with pinned seeds, panic is a legal outcome only under a panic row, and xfail is an info-string modifier.
• Refinements are written in a prose-friendly, human-readable form that is still machine-readable. Decided: separate requires/ensures blocks of label: predicate clauses; the signature block stays plain Soil types. Labels are what the lock and checker errors pin; the shared predicate language (also used by type invariants and property tests) is restricted to total calls in the decidable fragment. ensures on a Result uses result is Ok(v) implies ….
• There is no calls annotation. The original “function application annotation” idea is fully subsumed by effect rows and capabilities: a function without a Net argument cannot reach the network regardless of what it calls. Call edges are tracked by the lock for the graph view but are not human-written.
• Values: JSON, with a block drag-and-drop UI in the IDE for constructing them. Every Trellis type is round-trippable through JSON; this is also the derivation mechanism for show/eq (§3.7). Sum types are internally tagged ({"tag": "Ok", "value": …}; nullary variants {"tag": "None"}): one uniform shape for every variant, self-describing for hosts and generic tooling. The verbosity is accepted because the IDE’s widgets, not humans, write and read these values. Decoding is always type-directed; show output is canonical (declaration-order fields, comparator-order maps, shortest round-trip floats) so expect tests compare on the string. Full encoding table in the grammar prototype.
• Type definitions are definitions: prose plus a shape (or agent-inferred shape) plus optional invariants expressed as refinements on aliases, which are checked as properties every constructor must preserve. Confirmed; whether invariants are checked on every constructor call or only proven at definition sites is an open detail (§9).
• The .tr grammar is prototyped in docs/tr-grammar.md with worked examples in examples/. The reserved block languages are soil-sig, requires, ensures, test, property, cram, reference, allow, soil-type, invariant, exports; fenced blocks in any other language are prose. Finalization into docs/ is pending (§11).

4.4 Module structure

• Folder = module. _module.tr holds module-level prose and the export list.
• Export list is an explicit list of Trellis files (functions), exactly. Easy to hash. The export list is the FFI surface; host stubs are generated from it.
• Export pinning (proposed, unenforced in v1): because exported signatures are agent-authored, the public API of a module is agent-authored. The proposal is that exported signatures require human approval via a pinned flag in the lock, after which the agent cannot change them without a Trellis error. Same principle as “humans write the tests.” Enforcement is tooling and is deferred; the flag exists in the lock format from the start.

4.5 Tests

Tiers, expressed as a lattice the manifest can describe:

expect (cheap, always run) → property/quickcheck/fuzz → differential against reference → proof.

• The user declares which tier each function must reach; the lowering agent escalates automatically when a cheaper tier is green.
• Test budget is inferred from the effect row: pure functions are fuzzed hard; io functions get expect/cram tests only. Per-function override available.
• Not every tier is equally English-describable: expect tests and properties translate well from prose; fuzz harness configuration is just code.
• Reference implementation / validator in Python, or a CLI oracle: a JSON-in/JSON-out executable invoked as a black box and hashed like any oracle (amended for the compiler bootstrap, where soil0’s passes are the oracles — see docs/bootstrap-plan.md). Always attached explicitly by the human, never auto-detected. Differential tests call it through the Python FFI with a Py capability in the test harness. serves as a differential-testing oracle, an executable spec the agent reads when prose is ambiguous, and a migration path (an existing Python codebase is the reference spec, and Trellis becomes a verified port tool).
• Test dependencies: tests may reference the prelude, the reference implementation, the function under test, and other user definitions only if those definitions are accepted. Acceptance is the human’s trust signal, so accepted definitions are legitimate oracles, and this creates test-level edges only to frozen work. The lock tracks the edge; if the oracle’s spec changes, dependent tests re-run. Unaccepted definitions cannot be oracles, which prevents oracle cycles among unfinished work.
• xfail marker: a test may be marked expected-to-fail to document a known limitation. It stays in the spec, is shown in the lock, and blocks accepted until resolved, so the disciplined alternative to deleting a test exists.
• Non-deterministic functions: Rand and Clock fakes take seeds and timestamps; the IDE’s test widgets expose these as fields so every such test is pinned by construction.
• Contradiction pre-flight: before spending any tokens, the daemon checks tests against each other and against the prose for mechanical contradictions (same input, different expected output). This is a distinguished check; subtler contradictions become a distinguished class of ask_human question.
• The kind of test a definition needs depends on what it is. Every definition has tests, but not the same tests: pure functions get expect and property tests; io functions get fake-capability tests; FFI bindings get contract tests (below). The invariant “nothing in the lock is untested” holds throughout.
• FFI bindings get auto-generated contract tests, not human-written behavioural tests. A binding’s spec is “faithfully cross the boundary,” and that is checkable without understanding the library. The daemon derives contract tests from the signature and effect row: a call with an obvious valid input yields Ok; an invalid input yields Err, not panic; returned handles are accepted by the sibling bindings for that type; a loop of calls under the debug runtime’s leak checker shows no growth; Soil values survive soil_to_py/py_to_soil unchanged. The human supplies prose and at most one example input. The lock records tests as contract rather than expect, so the trust level stays visible. Behavioural correctness of foreign code is not the binding’s job; it is caught one level up by the user’s own tested functions, which is the same place a hand-written wrapper around a C library would fail.
• Harvested tests remain optional and strictly better when the foreign library has examples or a test suite worth translating. Trust level harvested vs contract is recorded in the lock.
• Refined bindings need one real test per refinement. A refinement on a binding (e.g. {p | valid_regex p} -> total Regex) does work for downstream proofs that contract tests do not exercise, so each refinement requires one human-written counterexample. Most bindings carry no refinements.
• io testing: fake capabilities (§3.5) are the primary mode. Cram tests against real side effects are the fallback for the individual user and for the FFI boundary, where fakes stop being possible. A cram transcript runs in a fresh temp dir with with file fixtures and may invoke built binary targets or trellis call <def> <json-args> (any io definition, real World-derived capabilities, canonical JSON out) — the real-mode escape for non-main functions. Cram never runs inside the lowering sandbox (§4.6). The lock tags a function’s io tests with their mode so additional modes can be added later without a format change.

4.6 Lowering

Input context per lowering is a fixed directory layout (the context bundle): spec.md, callees/ (signatures only, never bodies), tests.json, examples/ (prelude), reference.py, and previous.soil if re-lowering. The agent reads it through a tool; humans can inspect it. Unverified callees are shown as their base type plus a note that the refinement is demoted, so the agent cannot rely on an unproven claim.

Lowerings run strictly serially and in disciplined order: a definition cannot lower until all its callees have. There is no separate signature-inference step; a definition with no lowering has no checkable signature, and callers wait. The dependency tree provides the queue order, the IDE shows what is blocking what, and the IDE supports queuing lowerings while other definitions are still being written. If a human edits a definition that a queued or running lowering depends on, the daemon invalidates that job.

Fresh context per lowering. Every lowering is its own session receiving a fresh context built from the current (human-edited) files. More expensive in tokens; guaranteed to be correct and free of stale memory. A separate “memory cache” of agent observations was considered and rejected under the design tenet: anything the lowerer learns that would help next time either belongs in the prose, the tests, the module header, or the prelude fork, or it is not an input. The one exception allowed: a per-lowering log (f.log, gitignored) of what was tried and why it failed, for the human to read only; never an input to the next session.

Lowerer implementation. Each lowering is one headless agent invocation, which implements the fresh-context rule via the process boundary. The daemon (§4.9) assembles the context bundle and invokes the agent with a prompt to lower it. The daemon is an MCP server, and the agent is allow-listed to exactly its tools: read_context, check_types, check_refinements, run_tests, write_soil, ask_human. No raw shell, no filesystem outside the scratch directory. Consequences:

• The sandbox is the tool allow-list. run_tests runs in the daemon’s sandbox with fake capabilities; real-world tests are not a tool the lowerer has.
• The check loop lives inside one invocation. The agent writes Soil, checks, reads structured errors, revises, tests. The daemon caps turns, time, and cost rather than implementing retries.
• Every tool call is logged by the daemon, which is f.log and the cost telemetry with no instrumentation of the agent.

The question channel ends the invocation. ask_human writes a structured question and exits. The daemon surfaces it in the IDE, the human answers, the daemon writes the answer into the .tr prose, and re-invokes the lowerer fresh. The agent never sees an answer that is not already in the spec, and every question/answer pair is a visible diff. A blocking in-context variant may be added later as a cost optimization.

Provider abstraction. One interface, lower(bundle, tools, budget) -> outcome, with two provider kinds: agent-CLI providers (Claude Code headless / Agent SDK, and other headless agent CLIs; nearly free to build; runs on subscription quotas) and a raw-API provider (own loop against a model API; full control; pay-as-you-go). The IDE supports multiple agents with user-supplied credentials. Agent-CLI is v1; raw-API is v2. Running the lowerer through Claude Code is a high-priority feature because it is how subscription users avoid paying twice, though subscription quota policy for headless use has shifted recently and should be re-verified. Daemon responsibilities from day one: per-invocation timeouts, turn caps, cost caps, and isolated agent home directories.

Per-function granularity, manifest/type/lint checked at each step. Failures are local and retryable.

No widening. If lowering f reveals that g’s signature is wrong, the agent does not widen g; it is a Trellis error for the human.

Agent write-back: the agent writes its inferred signature back into the .tr file. How agent-authored parts are marked, and what happens when a human edits them (presumably: they become pinned), is an open format question (§9).

Agent questions before lowering: the agent may raise an ambiguity as a blocking state (“should parse accept trailing whitespace?”). The human’s answer is written back into the prose. Ambiguity becomes spec improvement rather than silent guessing. Implied by the interactive UI decision; not separately confirmed.

Errors for the agent as a first-class audience: the LSP has two output modes, human and agent; the agent mode is structured (JSON) with concrete counterexample, violated spec clause, failing test, and a suggested repair class.

Interactive lowering UI: the user interacts with lowering errors and reports through a prompt or UI. Rule: anything the human says to the lowerer that changes the outcome must be persisted to the .tr file, or the lowerer refuses to act on it.

Model selection: user-customizable, with “auto” functionality that chooses when no model is selected. Auto keys on spec size, effect row, presence of refinements, and number of past lowering attempts; escalates on retry. A per-project cost ceiling is planned because auto-with-escalation is exactly the setting where one pathological function burns a budget. All of this is tooling and ships minimal for v1 (one model, fixed retry count).

Style and the prelude corpus: see §5.

4.7 “Done”

Done is the user’s decision. The lowering’s current status (tests, proofs, demotions) is presented transparently and the user decides when they are happy. The lock status vocabulary is typed, tested, verified, accepted; only accepted is set by a human. CI policy (“every exported definition must be accepted”) is a line in soil.toml, not a semantic rule.

4.8 Generated Soil

• Checked in. Agent output is not reproducible, so the Soil is the artifact and the agent is a code generator like protoc; regeneration is a deliberate step.
• Editable by humans. People will do it anyway. The lock records hand-edited and skips re-lowering until the spec changes.
• Round-trip check: handled by the spec rather than by diffing prose summaries. The checked type of the generated function must entail the spec type from the manifest (a mechanical subtyping/entailment check). Prose drift is handled separately via hashing (§6.2).

4.9 The daemon

Because the IDE is the primary product (§7.1), the lowerer, checker, REPL, and runtime are services rather than batch commands. A long-running trellis daemon holds incremental compiler state, exposes the LSP, runs lowerings as jobs with the question channel, serves the REPL, and exposes the MCP tool surface used by the lowering agent. The CLI and the IDE are both thin clients; CI support later is “run the daemon headless.”

REPL: nearly free given incremental compilation, since the daemon already holds every definition compiled. It works at the Trellis level (call a definition with JSON) as well as the Soil level; the former feeds REPL-to-expect-test promotion.

Debug mode: debug builds instrument every Trellis definition boundary (not every Soil function) with entry/exit, JSON arguments and return, timing, and which refinement checks fired. One run yields a trace convertible to expect tests by clicking a call, a flame graph at definition granularity, and a repro for any panic with exact inputs. Slowness is treated as a bug; the spec-granularity flame graph lets the human see it without reading Soil. Run logs are labelled sandboxed (from lowering) or real (from the human), and the IDE shows which one a proposed test came from.

5. The prelude as a trusted corpus

The standard library is a Trellis project whose lock file is trusted. Each entry is a spec plus a blessed, human-verified lowering. This serves simultaneously as:

• The stdlib.
• The few-shot example corpus that defines the style of Soil the agent writes. Examples are real checked code and cannot drift from the language.
• The mechanism for forks with different capabilities: a no-io fork is a sandboxed profile; a fork without Py is Python-free. Forking the stdlib is forking a repo; no new mechanism.
• The governance mechanism: users contribute by promoting their own definitions; style is a PR-review question rather than a prompt-engineering one.
• The home for shared oracles (§4.5).

Structure: a pure core plus a foreign-backed batteries layer. The core prelude is written in Soil and is pure and total where possible: Option, Result, List, Map (with comparator), BigInt, Utf8, Bytes, JSON encode/decode, the derived-function primitives, the capabilities and their fakes, and Py. This is small (a few thousand lines) and is what teaches the agent what Soil looks like. A separate batteries layer provides refinement-typed Soil signatures over foreign stdlib functions. soil-rs-std is built first: Rust-backed functions are runtime-owned, can be total, and are refinable, so the batteries layer teaches the agent sound idioms. soil-py-std follows in v1 as the library layer, with handle-in/handle-out style, ffi/panic, and the Py capability. Python-backed functions must not be the core or the first batteries, or nothing would be total and the corpus would teach “call out” as the idiom. BigInt may be Rust-backed (num-bigint) and still count as core, since runtime-owned values are ordinary.

Trust is by full hash per package, pinned in soil.toml: the core prelude and each batteries package are separate hashes, and the lock holds the list of trusted packages. A fork is a different hash; partial trust of a package is not possible. Batteries functions come in two visible flavours: handle-in/handle-out (cheap, unrefined) and handle-in/Soil-out (converts, refinable on the result).

Corpus retrieval: for v1 the whole prelude fits in context. At scale, retrieval by signature similarity and effect row is the obvious mechanism, and the lock file is already most of the index. Deferred.

The prelude must be written in the same dialect users are permitted to use (no stdlib-only features), and must use capability-style io signatures from the start.

First prelude definition to write: read_file, since it exercises capabilities, effects, Result, and the FFI boundary at once.

6. Hashing, locking, and incrementality

6.1 Content addressing (Unison-style)

Every definition is identified by the hash of its syntax tree with free variables replaced by the hashes of what they refer to. Names are a lookup table on the side. Consequences:

• A function’s identity includes the identities of everything it calls. Change g and f gets a new hash automatically; unchanged functions do not.
• No name-based conflicts; renames are free.
• Check results, test results, and lowering results are cached by hash.
• Composes with Nix, which is also content-addressed.

Because cross-definition mutual recursion is forbidden (§3.8), the definition graph is a tree for functions. Recursive types need a combined cycle hash.

6.2 Three-part hashing per definition

A prose-stale state may be auto-cleared when an agent re-reads the prose and confirms the existing Soil still matches. This gives a cheap round-trip check without forced regeneration. Prose is thus “somewhere between hashed exactly and allowed to drift.”

6.3 Lock file

• One lock file per definition: f.tr → f.lock. Sidecar.
• Global manifest is derived, gitignored, regenerated from the sidecars. It is what Nix consumes. It must be a merge of the sidecars, never separately maintained.
• Merge conflicts can only arise when two people edit the same definition, which is a real conflict anyway.
• Verbosity is fine. Fields expected per entry: formal_hash, test_hash, prose_hash, soil_hash (covering the Soil body plus transitively referenced private helpers), check status, test status and test mode tags, provenance (agent, human-verified, hand-edited, prelude-fork), trust level for FFI bindings (harvested, generated, declared-only), language/format version, pinned flag, accepted flag, escape hatch list, cycle hash for recursive types, and for FFI bindings the symbol hash plus the Nix store path of the package.
• Language versioning: the lock records which Soil and Trellis versions a lowering targeted, so upgrades do not invalidate silently.
• The lock schema is prototyped in docs/lock-schema.md with example sidecars in examples/. Decisions: JSON in the canonical value form (one format, one parser, diff-stable key order); component statuses (checks facts plus per-test results) with the typed/tested/verified/accepted ladder derived by the IDE, never stored; the lowering record carries provider and model for audit while costs, retries, and timings stay in the gitignored f.log; per-block provenance under spec.blocks implements the @agent write-back scheme; oracles records test-level edges by hash; accepted requires no xfail/xpass results.

6.4 Incremental refinement checking and demotion

Refinement types are modular: each function is checked against its own signature plus the signatures of callees. Checking is per-function; changing a body without changing its signature invalidates nothing downstream. Changing a signature invalidates callers via content addressing.

Fallback on proof failure: the function is demoted to its base ML type (refinements erased from the checker’s view), marked unverified, and tests remain required. Callers relying on the refinement are checked against the weaker type. Demotion is explicit and local; the agent never silently widens a signature. The IDE shows the unproven chain. This is effectively gradual refinement typing (Lehmann & Tanter).

Blast radius is kept small by design: the checker is for extra safety; tests are what correctness is based on.

7. Product and IDE

7.1 IDE-first

The IDE experience is the primary goal; the first milestone is a tool the author wants to use. Industry adoption within larger teams is the secondary goal (such teams will want a trellis derive command that stubs .tr files from an existing codebase). CI and headless operation are later concerns, served by running the daemon headless.

• Platform: a web app served by Electron, for portability and simplicity, and so the same UI can later be served remotely. The Electron tax is accepted.
• Editing model: a text editor with widgets. Widgets are the JSON test blocks (drag-and-drop), REPL-to-test promotion, and the question/answer panel. Everything else is Markdown.
• Lowering UX: clicking “lower” starts an interactive session in which the agent can prompt back with questions and error reports. The human answers in the IDE; answers are persisted to the .tr.
• Fix mode: a debug-mode run produces a trace, flame graph, and proposed test cases; the IDE supports turning any of these into tests.
• Git: the IDE never commits on its own. At accept, pin, and rename it suggests a commit with a message; one click to commit, one to decline.
• Lints: definition-size and split-suggestion lints (e.g. a 400-line lowering for a one-paragraph spec) come from the Soil checker and surface in the IDE as suggestions, never blocking.
• Status: the lock is ugly and never read directly; the IDE renders it. Code review is supported by the IDE rendering “specs changed, tests changed, N re-lowered, M newly accepted.”
• Telemetry: the lowerer tracks tokens, cost, retries, and provider per lowering from day one; this is what later makes automatic model selection possible.
• Build targets: trellis build builds whatever soil.toml specifies: binary, py_module, shared_lib, jvm_jar, etc. One tool, one flag surface.
• Upgrades: lowerings record the language version they targeted and are left alone on upgrade until their spec changes; the Soil compiler therefore needs a compatibility policy.
• Licensing (resolved 2026-08-22): the open parts are GPL-3.0-or-later, with the GCC Runtime Library Exception 3.1 additionally applied to everything that ends up inside compiled user programs (soil-rt, the prelude, later batteries) — the GCC model, so forks of the toolchain must stay open while user binaries carry no obligations. Docs, specs, and examples are CC BY-SA 4.0 (copyleft for prose without GPL’s ill-fitting source-form mechanics). Contributions are DCO-only, no CLA; consequently the closed-source IDE shares no code with the open repo and talks to the daemon only over its API — which is already the architecture (§4.9). AGPL for the daemon was considered (hosted-lowering loophole) and rejected in favor of one uniform license; MPL was rejected as too weak (closed files around the open core); a CLA was rejected as the wrong asymmetry for a copyleft project. License texts: LICENSE, LICENSE.exception, LICENSE.docs at the repo root.
• Hosted lowering: eventually possible by design (the daemon is a service), but not a v1 or v2 concern.
• Naming: the project, the specification layer, and the IDE are Trellis; the target language is Soil. The CLI is trellis (e.g. trellis lower, trellis bind). “Trellis” was the placeholder (declarative vibe-coding).

7.2 On-disk layout

Soil lives in its own directory, any directory with a soil.toml at its root. Zip files were rejected as opaque to git; inline embedding in foreign source was rejected as worse. A repo may contain multiple independent Soil roots with no cross-root imports; slices that need to share are one root.

Spec, generated Soil, and lock sit side by side per definition. A split into spec/ and gen/ was rejected as losing the locality that justified one-file-per-definition.

soil/
  soil.toml            -- deps, prelude fork, build targets, CI policy, tag vocabulary
  soil.lock            -- derived global manifest, gitignored
  parser/
    _module.tr         -- module prose, export list
    parse.tr
    parse.soil
    parse.lock
    parse.log          -- gitignored, human-readable lowering log
    tokenize.tr
    tokenize.soil
    tokenize.lock
    _private.soil      -- module-private helpers
  soil/__init__.pyi    -- generated host stub

Every definition is three files; the module header and private helpers are the two exceptions; the only non-derived global file is soil.toml.

8. Build system

• Declare dependencies in TOML; Trellis compiles it to a Nix build script. Nix is the right model (hermetic, content-addressed) but adopting it wholesale couples users to its ecosystem. The approach mirrors dream2nix, crate2nix, poetry2nix; Trellis is the polyglot roof over them.
• Generate flake.lock-style pinned inputs.
• No “escape to raw Nix” field in the TOML, or every project will use it and the tool becomes Nix with extra steps.
• A dev mode that shells out to native toolchains without Nix is planned for contributor onboarding.
• Foreign file locking: Nix hashes lock provenance (which bytes); Trellis’s lock records interface (which shape) via symbol hashes of .pyi, .d.ts, or C header declarations. v1 accepts Nix’s coarse invalidation (any upstream commit invalidates all bindings); the lock format is designed so finer symbol-level invalidation slots in later.
• Buck2 was noted as an alternative if Nix proves too heavy. Deferred.
• FFI boundary tests: harvesting tests from the dependency’s own suite is the default; generated boundary property tests from declared types are the fallback; each binding records its trust level. A foreign call has effect ffi (implying panic) and “tests are the only guarantee here”; no attempt to shrink effect rows for foreign code.

9. Open questions

1. .tr grammar — prototyped in docs/tr-grammar.md (§4.3) with its follow-up questions resolved: type files carry YAML frontmatter declaring the type’s cased name (filenames are snake_case everywhere); property where filters use constrained generation, not rejection sampling; the cram block is a minimal cram subset (with file fixtures, fresh temp dir, literal output, [n] exit codes, trellis call for real-capability invocation); property-only and cram-only files are valid (main and other toplevel functions are typically of that shape); every file carries frontmatter with a required name and optional non-semantic tags whose vocabulary is declared in soil.toml, while file kind stays inferred. Finalization into docs/ pending.
2. JSON encoding of Soil values — resolved: internally tagged sums, type-directed decode, canonical show output, opaque one-way "<handle>", functions a hard error (grammar prototype §7). BigInt is hybrid by range: a JSON number within ±(2^53−1), a string beyond, and decode accepts either — small values stay readable while big ones survive float-only host JSON parsers.
3. Lock entry schema — prototyped in docs/lock-schema.md (§6.3), including .tr provenance for the vibing tiers and per-block provenance for the write-back scheme (5). Newly open from the prototype: whether module entries participate in accepted; a fixed naming scheme for derived tests; whether entries pin the prelude-fork hash or leave it global in soil.toml.
4. Prose-friendly refinement syntax — resolved: labelled requires/ensures clauses over a shared predicate language (§4.3; grammar prototype §2.3).
5. Agent write-back markers — tentative proposal (grammar prototype §8): agent-authored blocks carry @agent in the info string; a human edit removes the marker, and an unmarked formal block is pinned — the agent may not change it, only ask_human.
6. Type invariants: checked on every constructor call, or only proven at definition sites.
7. Naming conventions for agent-created private helpers.

10. Deferred decisions and their triggers

11. Build order

The build order follows the bootstrap plan (docs/bootstrap-plan.md): the compiler itself is the first Trellis project, self-hosted on a minimal Rust implementation that is kept forever as a differential oracle. Each milestone has an implementation guide in docs/plans/.

1. soil0 + soil-rt. A Rust workspace: the runtime crate (values, reference counting, JSON bridge, C ABI with a trivial main wrapper from the first commit) and a minimal Soil implementation — parser, ML + effect-row inference, exhaustiveness, tree-walking interpreter, test runner. No refinements, no termination checker, no codegen, no FFI yet. Every pass is exposed as a JSON-in/JSON-out CLI command (soil0 parse, soil0 infer, soil0 run) — the future differential oracles. Deliberately small; interpreted execution is the engine for the whole bootstrap, and slow is accepted.
2. The daemon. Incremental compiler state, LSP, context-bundle assembler, MCP tool surface, lowering jobs with the exit-and-reinvoke question channel, serial queue, agent-CLI provider (Claude Code headless first), REPL endpoint, debug-mode instrumentation, cost telemetry, per-definition locks and the derived manifest. This is where the effort goes; it is smaller than it sounds because the agent CLI supplies the loop.
3. The pure-core prelude as the first Trellis code, interpreted on soil0.
4. soilc: the compiler as the first Trellis project. Passes in oracle-ready order — lexer, parser (the mutual-recursion stress test, deliberately early), renamer, type + effect inference, exhaustiveness/patterns, ANF, termination checker, refinement checker (SMT-LIB out, Z3 behind a Solver capability), CLIF backend — each differentially tested against the matching soil0 command and swapped into the daemon at accepted (strangler pattern). Refinements and demotion therefore arrive here, as compiler passes, not as a later milestone. Closure: soilc interpreted compiles the prelude and itself via the Cranelift driver → soilc₁; soilc₁ compiles the same sources → soilc₂; the build requires soilc₁ ≡ soilc₂ byte-identical. soil0 is retained permanently as oracle and debug-mode engine.
5. FFI, trellis bind, minimal IDE. C-ABI FFI to Rust and Python FFI via embedded CPython, hand-written bindings, sequenced C ABI → Rust batteries → Python embedding → Python batteries; one corpus shim example per FFI; the per-symbol bind assistant; the Electron-served IDE over the daemon (Markdown editor with test-block widgets, graph view, lower button with streaming output and the question panel, REPL, lock rendering), as thin as possible.
6. The Python-glue project as the second Trellis project. A program the author would otherwise have had an agent write in pure Python: Rust crates through soil-rs-std, a dozen Python functions through trellis bind, real work in Soil. The compiler validates the pure core; this validates the FFI/capability/bind half of the pitch and the pleasantness test — writing .tr files and reading generated Soil.
7. Then trace-to-test fix mode, profiling, build targets, TOML→Nix, raw-API provider, trellis derive, headless CI mode.

Immediate next artifacts:

• The .tr grammar specification — prototyped (docs/tr-grammar.md plus examples/, including the JSON value encoding and the refinement prose syntax); to be finalized into docs/ once the prototype has been exercised.
• The lock entry schema — prototyped (docs/lock-schema.md plus example .lock sidecars); to be finalized into docs/ with the grammar.
• The prelude’s read_file as the first real definition (drafted as examples/read_file.tr with read_file.lock and read_file.soil).
• A high-level Soil surface syntax: prototyped in docs/soil-syntax.md (Haskell-style signatures and inline refinements, OCaml-style terms, decreases lines, comparison operators as derived-function notation, no imports; guards/;/let? deliberately absent or deferred), elaborated into a lexical spec, EBNF, and static rules in docs/soil-syntax-spec.md (OCaml-style match with parenthesized nesting; one connective spelling and/or/not shared by terms and predicates, implies predicate-only; shadowing forbidden; :: namespacing; .. required in partial record patterns; parameterless let bindings with explicit lambdas; a fixed scalar-value-only string escape set; arithmetic operators as notation with overflow/zero-divisor as refinement obligations; Bool encoding as JSON booleans). Result a e is success-first (§3.3). Full semantics arrive with the Soil core milestone.

12. Prior art to consult

• Idris 2 / Agda / Lean: type-as-spec, hole-driven workflow (Trellis without the LLM); termination checking; total-by-default policy.
• Hazel: live holes, typed structure editing, for the IDE.
• Unison: content-addressed definitions, incremental typechecking, codebase-as-database; cycle hashing; closest existing thing to the manifest idea.
• Dafny / Verus: spec-then-implementation with a checker in the loop.
• Liquid Haskell / F*: refinement types with SMT discharge.
• Lehmann & Tanter: gradual refinement types, for the demotion model.
• Koka: direct-style surface with effect rows, div as an effect, Perceus reference counting; its effect types subsume function-application annotations.
• OCaml: polymorphic compare, Map.Make comparator idiom.
• Rust: derive, total_cmp for floats, debug/release split.
• dream2nix / crate2nix / poetry2nix: per-ecosystem TOML-to-Nix precedent.
• Buck2: polyglot build alternative.
• Inform 7, AppleScript, COBOL, Wolfram: history of natural-language programming. The consistent lesson: prose as syntax fails; prose as spec alongside formal structure works. Trellis is on the right side of that line.

The .tr File Format — Prototype Grammar

Status: prototype. Tentatively resolves §9.1 (grammar), §9.2 (JSON value encoding), and §9.4 (refinement prose syntax) of docs/design.md, and proposes an answer to §9.5 (write-back markers). Worked examples live in examples/.

1. Container format

A .tr file is CommonMark. Formal content lives in fenced code blocks whose info string begins with a reserved word. Everything else — including fenced blocks in unreserved languages such as python or text — is prose: it is hashed under prose_hash and never parsed.

There are three file kinds, distinguished by content, with filename as identity (design §4.3):

Filenames are lowercase snake_case for every kind, so identity survives case-insensitive filesystems.

Every .tr file begins with YAML frontmatter. name is required and is the definition’s canonical name: a function’s equals the filename stem; a type’s is PascalCase and the filename is its snake_case form; a module’s equals its directory name. There is no kind field — kind is inferred (_module.tr by filename; a soil-type block makes a type file; otherwise the file is a function).

tags is optional: a list drawn from a per-project vocabulary declared in a [tags] table in soil.toml; an undeclared tag is an error. Tags are non-semantic metadata — IDE graph filtering and colouring, CI policy in soil.toml (e.g. “every definition tagged api must be accepted”) — and are never part of the lowering context bundle. Unknown frontmatter keys are errors.

---
name: ParseError
tags: [parser]
---

Reserved block languages

Mapping to the three-part hash (design §6.2)

• formal_hash: the frontmatter name, soil-sig, requires, ensures, soil-type, invariant, exports, allow.
• test_hash: test, property, cram, reference (the reference is an oracle; changing it re-runs differential tests, not the lowering).
• prose_hash: everything else in the file, including tags.

2. Shared mini-languages

2.1 JSON values

json below means an RFC 8259 JSON value, interpreted type-directedly under the encoding of §7.

2.2 Identifiers

ident is lowercase snake_case (functions, parameters, fields). Ctor and TypeName are PascalCase.

2.3 The predicate language

Shared by requires, ensures, invariant, and property. It is a restricted Soil boolean expression: calls may target only total definitions, and predicates outside the decidable fragment (linear arithmetic, uninterpreted functions, lengths — design §3.2) still parse but demote the function to unverified.

predicate  ::= disj [ "implies" predicate ]            (right-assoc)
disj       ::= conj { "or" conj }
conj       ::= neg { "and" neg }
neg        ::= [ "not" ] atom
atom       ::= comparison | is-test | call | "(" predicate ")"
comparison ::= expr relop expr
relop      ::= "==" | "!=" | "<" | "<=" | ">" | ">="
is-test    ::= expr "is" Ctor [ "(" ident ")" ]        (binds the payload)
expr       ::= literal | path | call
             | expr ("+" | "-" | "*") expr | "(" expr ")"
path       ::= ident { "." ident }                     (record field access)
call       ::= ident "(" [ expr { "," expr } ] ")"
literal    ::= JSON literal

Names in scope: the signature’s named parameters; result (in ensures only); self (in invariant only); forall binders (in property only); and total definitions visible to the file.

3. Function-definition blocks

3.1 soil-sig

sig    ::= defname ":" arrow
arrow  ::= param "->" arrow | ret
param  ::= "(" ident ":" type ")" | type
ret    ::= [ row ] type
row    ::= effect { effect }
effect ::= "div" | "panic" | "io" | "ffi"

An empty row means total. type is Soil type syntax, specified separately; this grammar treats it as opaque. The signature may be absent — the agent infers it and writes it back (§8). If requires/ensures refer to a parameter by name, the signature must exist and use the named-parameter form.

3.2 requires / ensures

block  ::= clause { clause }
clause ::= label ":" predicate                          (one per line)
label  ::= free text not containing ":"

Labels are the pinnable names: the lock, the IDE, and checker errors refer to clauses by label. In ensures, result is bound to the return value; for Result-typed functions the idiom is result is Ok(v) implies … (design §3.2: refinements may eliminate error cases).

3.3 test

The function under test is implicit — it is the file’s definition. A block holds any number of cases; case k of block name is reported as name#k.

block     ::= { with-line } case-line { case-line }
with-line ::= "with" ident "=" fake-call
fake-call ::= ident { json }
case-line ::= "(" [ arg { "," arg } ] ")" "=>" outcome
arg       ::= json | ident                              (a with-binding)
outcome   ::= json | "panic"

• with lines construct fake capabilities from the prelude (design §3.5); their arguments are JSON, so seeds and timestamps are pinned by construction (with clock = fake_clock 1700000000).
• panic as an outcome is only legal if the signature’s row carries panic.
• xfail in the info string marks the whole block expected-to-fail; it blocks accepted until resolved (design §4.5).

3.4 property

block       ::= forall-line { forall-line } predicate
forall-line ::= "forall" ident ":" type [ "where" predicate ]

Generators are derived from the binder’s type; a where filter is a generator constraint, satisfied by constrained generation rather than rejection sampling. Properties may call the function under test, the prelude, the reference implementation, and accepted definitions (design §4.5).

3.5 cram

For io functions where fakes stop being possible, for FFI bindings, and for main. The dialect is a minimal subset of classic cram: unindented, no (re)/(glob) matchers (extensible later).

block       ::= { with-line } step { step }
with-line   ::= "with" "file" string "=" string      (JSON strings)
step        ::= command { output-line } [ exit ]
command     ::= "$ " rest-of-line                    (a shell command)
output-line ::= any line not beginning "$ " or "["
exit        ::= "[" integer "]"

• Each block runs in a fresh temp dir. with file lines materialize fixtures before the transcript runs — path and contents are JSON strings, so escapes are pinned.
• Commands run sequentially in one shell session in that dir. Expected output is combined stdout+stderr, matched literally. An omitted exit line means 0.
• The transcript may invoke built binary targets from soil.toml (placed on PATH), and trellis call <def> <json-arg>…, which runs an io definition with real World-derived capabilities and prints its result as canonical JSON — the real-mode escape for non-main io functions and FFI bindings. Capability parameters are injected from World; the JSON arguments fill the remaining parameters in order.
• The lock tags these tests mode real (design §4.5). Cram never runs inside the lowering sandbox: the lowerer’s run_tests tool exposes only fake-capability tests (design §4.6).

3.6 reference

One line, in one of two forms:

line ::= relpath "::" symbol          (Python reference)
       | "cli" command-line          (CLI oracle)

ref/stats.py::median attaches a Python reference implementation. cli soil0 parse attaches a JSON-in/JSON-out executable as a black-box oracle: the daemon passes the test’s JSON arguments on stdin and expects canonical JSON on stdout (added for the compiler bootstrap; design §4.5). Attached explicitly by the human, never auto-detected.

3.7 allow

One escape hatch per line, from the fixed set partial, unsafe, ffi-raw. Written only by the human; every allow block in the project is surfaced in the manifest’s audit view (design §4.1).

4. Type-definition blocks

4.1 soil-type

typedef ::= "type" TypeName { tyvar } "=" body
body    ::= "opaque" | record | sum | type              (last = alias)
record  ::= "{" field { "," field } "}"
field   ::= ident ":" type [ "ignored" "=" expr ]
sum     ::= [ "|" ] ctor { "|" ctor }
ctor    ::= Ctor [ type ]

A variant carries at most one payload of any type; multi-field payloads are inline records, since there are no positional products (design §3.13) — Ok a, but BadCell { index : U64, text : Utf8 }. Derivation strategies (design §3.7): structural is the default; an opaque body selects the opaque strategy; the ignored field marker selects the ignored strategy for that field.

An ignored field must carry a default: an expr from the predicate language (§2.3) — so calls target only total definitions — with the record’s non-ignored fields in scope. The default materializes the field wherever a value is built without it: JSON decode, py_to_soil, host stubs. ignored thus means “excluded from derivation, reconstructible on demand”:

type Doc = { text : Utf8, cached_word_count : U64 ignored = word_count(text) }

4.2 invariant

Same clause grammar as ensures, with self bound to a value of the type. Invariants are properties every constructor must preserve (whether checked at every construction or proven at definition sites remains open, design §9.6). Each invariant clause auto-generates a property test (design §4.1), which is why type files carry no hand-written test blocks.

5. Module headers

5.1 exports

line ::= ident
       | "type" TypeName
       | "abstract" "type" TypeName

An exact list of definitions (design §4.4). If an exported signature references an unexported type, the two permitted repairs are exporting it or marking it abstract here (design §3.14).

6. Validity rules

1. Every file begins with frontmatter carrying a name. Unknown frontmatter keys, and tags not declared in soil.toml, are errors.
2. Function file: name equals the filename stem; at least one prose paragraph and at least one test, property, or cram block. The minimal valid definition is the frontmatter, one sentence of prose, and one expect test (design §4.3); property-only and cram-only files are valid — main and other toplevel functions are typically of that shape.
3. Type file: the snake_case form of name equals the filename stem; at least one prose paragraph and exactly one soil-type block. No test blocks.
4. Module header: name equals the containing directory’s name; exactly one exports block.
5. Block multiplicities per the table in §1; test/property/cram names unique within a file.
6. The names declared in soil-sig and soil-type, when present, must equal the frontmatter name. Renaming is refactor-rename (design §4.3).
7. Predicates may reference parameters only via a named-parameter soil-sig.

7. JSON value encoding (resolves design §9.2)

One encoding serves show/parse, tests, the REPL, and host stubs. Encoding and decoding are always type-directed. Sum types are internally tagged: one uniform shape for every variant, self-describing for hosts and generic tooling. The verbosity is accepted because JSON values are primarily written and read through the IDE’s block widgets (design §4.3), not typed by hand.

Canonical output: show emits record fields in declaration order, map entries in comparator order, and floats in shortest round-trip form, so equal values produce byte-equal JSON and expect tests can compare on the string (design §3.7).

The keys "tag" and "value" are produced only by the sum encoding; since decoding is type-directed, a record field named tag is not ambiguous, but the linter warns on it.

8. Provenance and write-back (tentative, design §9.5)

Agent-authored formal blocks carry an @agent marker at the end of the info string:

```soil-sig @agent
mean : (xs : List F64) -> F64
```

The agent may freely rewrite blocks marked @agent. When a human edits such a block they remove the marker; an unmarked formal block is human-authored and therefore pinned — the agent may not change it, only raise ask_human. The lock records provenance per block alongside the hashes.

9. Open questions raised by this prototype

All questions raised by the first draft — type-name casing (frontmatter, §1), ignored-field decoding (defaults, §4.1), BigInt interop (hybrid by range, §7), generator strategy (constrained, §3.4), the cram grammar (§3.5), and property-only files (valid, §6) — have been resolved and folded into the sections above.

The Lock Entry Schema — Prototype

Status: prototype. Tentatively resolves §9.3 of docs/design.md. Example sidecars live next to the .tr examples in examples/. Hashes in examples are abbreviated.

1. Shape

One lock file per definition, sidecar: f.tr → f.lock (design §6.3). A lock file is a single JSON object in the canonical form of the value encoding (grammar prototype §7): sorted-stable key order, so diffs are minimal and semantic. The global soil.lock manifest is derived by merging sidecars (§7 below) and is gitignored.

Top-level keys, in order:

2. spec

"spec": {
  "provenance": "human",
  "hashes": {
    "formal": "sha256:9f2c41aa",
    "test": "sha256:41aa73c0",
    "prose": "sha256:c8172d99"
  },
  "prose_state": "fresh",
  "blocks": [
    { "block": "soil-sig", "author": "agent" },
    { "block": "test odd-length", "author": "human" }
  ],
  "pinned": false,
  "escape_hatches": []
}

• provenance: human | agent — who authored the .tr overall, distinguishing the two vibing tiers (design §1.2, §9.3).
• hashes: the three-part hash (design §6.2). The block-to-hash mapping is grammar prototype §1. test is null for type and module files.
• prose_state: fresh | review-suggested. Set to review-suggested when prose changes under an unchanged lowering; auto-cleared when an agent re-reads the prose and confirms the Soil still matches (design §6.2).
• blocks: per-block provenance for the write-back scheme (grammar prototype §8). block is the info string minus modifiers (xfail is not identity). author: human means unmarked, therefore pinned — the agent may not edit it. Frontmatter is implicitly human.
• pinned: the export-pin flag (design §4.4) — human approval of the public signature. Present from the start, unenforced in v1.
• escape_hatches: the contents of the allow block, aggregated by the manifest into the audit view (design §4.1).

3. lowering

"lowering": {
  "soil_hash": "sha256:77b04e12",
  "provenance": "agent",
  "provider": "claude-code",
  "model": "claude-opus-4-7",
  "private_helpers": [ { "name": "_parse_cell", "hash": "sha256:3fe210bb" } ],
  "calls": [ { "name": "sort_by", "hash": "sha256:aa90b1f3" } ]
}

• soil_hash: content-address of the Soil body plus transitively referenced private helpers (design §6.3), free variables replaced by callee hashes (design §6.1).
• provenance: agent | human-verified | hand-edited | prelude-fork. hand-edited skips re-lowering until the spec changes (design §4.8).
• provider / model: which agent produced the current Soil, for audit and future model routing. Costs, retries, and timings live in the gitignored f.log, not here (design §4.6).
• private_helpers: the _private.soil definitions this lowering owns (design §4.2); the manifest derives its soil-private nodes from these, and a helper with no remaining owner is garbage-collected.
• calls: callee edges with the hashes they were checked against — the graph view and the invalidation record (design §4.3, §6.1).

4. checks

"checks": {
  "types": "ok",
  "refinements": "demoted",
  "demoted": ["upper bound"]
}

• types: ok | error.
• termination: verified | unverified | n/a — whether the claimed row’s absence of div is established. Until the termination checker exists (plans 04–05), recursive definitions claiming totality carry unverified: the demotion philosophy applied to div — unproven, visible, tests still gate.
• refinements: proven | demoted | none. Demotion is per design §6.4: the function drops to its base ML type for callers, tests remain required, and the runtime check stays in release builds (design §3.9).
• demoted: the clause labels (grammar prototype §3.2) that failed to prove — what the IDE renders as the unproven chain.
• Type entries use invariants in place of refinements.

5. tests and oracles

"tests": [
  { "name": "odd-length#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
  { "name": "ensures lower bound", "tier": "property", "mode": "sandboxed", "origin": "derived", "result": "pass" },
  { "name": "real-read#1", "tier": "cram", "mode": "real", "origin": "spec", "result": "pass" }
],
"oracles": [
  { "kind": "reference", "path": "ref/stats.py::median", "hash": "sha256:5e8f0b2a" },
  { "kind": "definition", "name": "sort_by", "formal_hash": "sha256:aa90b1f3" }
]

• name: block-name#k for multi-case blocks; the bare block name for single-case blocks; a clause label for derived tests.
• tier: the test lattice (design §4.5): expect | property | cram | contract | differential | proof.
• mode: sandboxed (fakes, runnable by the lowerer’s run_tests) | real (cram; never available inside the lowering sandbox). New modes can be added without a format change (design §4.5).
• origin: spec (a block in the .tr) | derived (auto-generated: properties from refinement clauses per design §4.1, contract tests for bindings per design §4.5, invariant properties for types).
• result: pass | fail | xfail (expected failure, failed) | xpass (expected failure, passed — needs spec attention). Failure details (counterexample, diff) are not stored here; they live in f.log and the IDE. Results are cache entries keyed by the hashes (design §6.1), so they churn only when inputs do.
• oracles: what the tests depend on beyond the definition itself — the reference implementation (by file hash), accepted definitions used as oracles (by formal_hash), and CLI oracles (by executable hash): { "kind": "cli", "command": "soil0 parse", "hash": "sha256:…" }. A changed oracle re-runs dependent tests (design §4.5).

6. FFI bindings

A binding is an ordinary function entry plus an ffi section (design §3.11, §6.3, §8):

"ffi": {
  "trust": "contract",
  "symbol": "requests.get",
  "symbol_hash": "sha256:be77a0c1",
  "package": "/nix/store/a1b2…-python3.12-requests-2.32.3"
}

• trust: declared-only | contract | harvested.
• symbol_hash: hash of the symbol’s machine-readable declaration (.pyi stub, cargo doc JSON, C header decl) — the interface record, designed so symbol-level invalidation can slot in later (design §8).
• package: Nix store path — the provenance record.

7. The derived manifest (soil.lock)

A pure merge of the sidecars — never separately maintained (design §6.3) — plus nodes and aggregates that only exist globally:

{
  "lock_format": 1,
  "definitions": { "csvstats/median": { …sidecar contents… } },
  "soil_private": [
    { "name": "csvstats/_parse_cell", "hash": "sha256:3fe210bb", "owners": ["csvstats/parse_row"] }
  ],
  "escape_hatches": {},
  "trusted_packages": { "prelude": "sha256:e0a1b2c3", "soil-rs-std": "sha256:f1b2c3d4" }
}

soil_private nodes are derived from every lowering.private_helpers list (greyed out in the IDE; many helpers + few definitions is a flagged smell, design §4.2). escape_hatches is the audit view. trusted_packages pins the prelude and batteries by full package hash (design §5).

8. Derived status and invariants

The typed / tested / verified / accepted ladder (design §4.7) is derived, never stored:

• typed — checks.types == "ok".
• tested — typed, and every test result is pass or xfail.
• verified — tested, and checks.refinements == "proven" (unreachable when refinements is none; only tested means correct, design §4.1).
• accepted — the stored flag.

Invariants the daemon enforces:

1. accepted may be true only if tested holds and no result is xfail or xpass (design §4.5) — resolving an xfail is a spec change, which clears accepted via the hash rules below.
2. A human-authored block may not be rewritten by the agent; the lowerer can only ask_human.
3. Only accepted definitions may appear in another entry’s oracles.

Invalidation on change:

9. Open questions raised by this prototype

• Whether module entries participate in accepted (CI policy currently keys on exported function definitions) or carry only hashes.
• Naming scheme for derived tests is ad hoc (clause labels, contract names); needs fixing before the daemon exists.
• Whether versions should pin the prelude fork hash per entry or leave it global in soil.toml.

Soil Surface Syntax — Prototype Highlights

Status: prototype, highlights only — the full grammar comes with the Soil core (design §11, milestone 1). Haskell for the type-level look, OCaml for the term-level look, minimal everywhere the design tenets demand it. First sample: examples/read_file.soil.

1. Definitions

Haskell-style signature line, then one equation. Curried, strict. The signature is mandatory in .soil — the file must check standalone, and the daemon verifies it entails the .tr spec type (design §4.8).

read_file : (fs : Fs) -> (path : Path) -> io (Result Utf8 FsError)
read_file fs path = ...

Named parameters (x : T) are optional except where refinements refer to them.

2. Effect rows

Space-separated, before the return type; the empty row is total.

io (Result Utf8 FsError)
ffi panic io PyObject

3. Terms

OCaml: let … in, let rec … and … (free within a file, design §3.8), match … with, fun x -> e, if/then/else. No ; — sequencing an effect is let _ = log clock msg in …. Let bindings are parameterless: a let-bound function is an explicit lambda (let go = fun x -> … in). Boolean connectives are the words and/or/not, the same spelling as the predicate language. One way to do things.

4. Pattern matching

Variant patterns bind the payload; record payloads destructure by name with punning. Exhaustiveness is enforced. _ is the wildcard. No guards — nested if/match instead.

match parse_cell text with
| Ok row                  -> ...
| Err { index, text = t } -> ...

5. Records

Construct with =, access with ., functional (non-mutating) update with with:

let r = { cells = xs } in
let r2 = { r with cells = ys } in
r2.cells

6. Sums

Nullary variants are bare; a variant carries at most one payload of any type, and multi-field payloads are inline records (no tuples): None, Ok bytes, BadCell { index = 1, text = "x" }.

Result a e puts the success type first (OCaml/Rust order). Haskell’s error-first Either e a exists so the partially applied constructor can be a Functor instance — impossible in Soil (no type classes, no higher-kinded abstraction), so the widely known order wins.

7. Refinements

Inline in .soil signatures, Liquid-style — the agent-facing spelling that the .tr’s requires/ensures clauses desugar into:

median : (xs : {v : List F64 | len v > 0}) -> {r : F64 | min xs <= r and r <= max xs}

8. Termination

A decreases line between signature and equation when structural decrease is not inferable (Idris-style measure, design §3.4):

gcd : U64 -> U64 -> U64
decreases b
gcd a b = if b == 0 then a else gcd b (a % b)

9. Comparison operators are notation, not overloading

Every type has exactly one derived eq/compare (design §3.7), so the elaborator rewrites x == y to T::eq x y at the inferred monomorphic type. In polymorphic code the operators are unavailable — take the function as a parameter (sort_by, map comparators), the confirmed idiom (design §3.6).

10. Names and modules

No import statements; the daemon resolves names through the manifest, and the lock’s import set is computed, never written. Same-module definitions and the prelude are bare; cross-module exports are qualified (csvstats::median); derived functions are Row::eq; private helpers are underscore-prefixed and live only in _private.soil. :: is the namespace separator, keeping . exclusively for record field access.

11. Literals and comments

1 is I64, 1.0 is F64, "…" is Utf8; other widths by annotation (42 : U32), no suffixes. Comments are --.

12. Deliberately absent

Tuples, guards, ;, do-notation, exceptions, mutation, type classes, operator sections, user-defined operators, parameterized let bindings.

Deferred, not rejected: a let? x = e in … sugar for Result propagation. v1 writes the match explicitly; if the corpus shows it is the dominant noise, the sugar is one desugaring rule later.

Soil Surface Syntax — Elaborated Specification

Status: prototype. Elaborates soil-syntax.md into a lexical spec, EBNF, and static rules. Decisions folded in from review: OCaml-style match (no terminator, parenthesize non-tail nested matches), word connectives (and/or/not) shared with the predicate language, shadowing forbidden, :: for namespaces with . reserved for field access, .. required in partial record patterns, parameterless let bindings (functions are explicit lambdas). Semantics (typing, effect, and refinement rules) arrive with the Soil core milestone (design §11); this document is the parser’s contract.

1. Lexical structure

• Source is UTF-8. Whitespace separates tokens and is otherwise insignificant — there is no layout rule.
• Comments run from -- to end of line. No block comments.

Identifiers

Keywords

let  rec  and  or  not  in  fun  match  with  if  then  else  decreases

Effect names are reserved in type position only: div, panic, io, ffi. The boolean connectives are the keywords and/or/not — the same spelling as the predicate language, so specs and code read identically (implies remains predicate-exclusive). There are no boolean literals: Bool is the prelude sum True | False (see §6 for its JSON special case).

and serves both as the mutual-binding connector and the boolean connective; see §3.3 for the disambiguation rule.

Operators and punctuation

->  =  |  :  ::  .  ,  ..  ( )  { }
==  !=  <  <=  >  >=  +  -  *  /  %  _

Literals

• Integer: [0-9][0-9_]*, default type I64. Other widths by annotation: (42 : U32). No suffixes.
• Float: digits . digits, optional exponent (1.5e3), default F64.
• String: "…", default Utf8. The escape set is exactly \", \\, \n, \r, \t, and \u{hex} with one to six hex digits denoting a Unicode scalar value (surrogates U+D800–U+DFFF and values above U+10FFFF are errors — a Utf8 value can never hold them). Any other character after \ is an error; there are no octal/hex byte escapes (Bytes are built by prelude functions, not literals) and no line-continuation escapes.
• No character literals; no Bytes literals (construct via prelude functions).
• Negation is the unary operator, not part of the literal.

2. Files

• <name>.soil holds exactly one definition; its name equals the filename stem and the .tr frontmatter name.
• _private.soil holds any number of private-ident definitions (design §4.2).
• .soil files contain no type declarations — type shapes live in the .tr soil-type blocks and the compiler materializes them — and no imports: names resolve through the manifest (design §6.1), and the lock’s import set is computed.

3. Grammar

Notation: { x } is zero-or-more, [ x ] optional, | alternation, terminals quoted.

3.1 Definitions

soil-file      ::= definition
private-file   ::= { definition }

definition     ::= signature [ decreases-line ] equation
signature      ::= defname ":" type
decreases-line ::= "decreases" expr
equation       ::= defname { ident } "=" expr
defname        ::= ident | private-ident

Equation parameters are bare identifiers — destructuring happens in the body. The defname of the signature and equation must agree.

3.2 Types

type       ::= [ dom "->" ] cod                      (right-assoc arrows)
dom        ::= "(" ident ":" type ")" | app-type | refinement
cod        ::= [ row ] type
row        ::= effect { effect } [ ident ]           (trailing ident = row variable)
             | ident                                  (row variable alone — only before a type)
effect     ::= "div" | "panic" | "io" | "ffi"
app-type   ::= TypeName { atype } | atype
atype      ::= TypeName | ident | refinement | "(" type ")"
refinement ::= "{" ident ":" type "|" predicate "}"

• Quantification is implicit and prenex: free lowercase type variables are universally quantified. There is no forall.
• Row parsing is unambiguous without HKT: type variables have kind * and are never applied, so in a -> e b and a -> e (List b) the leading lowercase ident followed by another type can only be a row variable. A lone ident after -> is the return type. An absent row is the empty row (total).
• predicate is the shared predicate language of the .tr grammar (tr-grammar §2.3): refinements are the spec language embedded in Soil, desugaring one-to-one from requires/ensures clauses. Its connectives (and/or/not) are the same words the term layer uses, so there is exactly one spelling everywhere; implies exists only in predicates.

3.3 Expressions

expr      ::= "let" [ "rec" ] binding { "and" binding } "in" expr
            | "fun" ident { ident } "->" expr
            | "if" expr "then" expr "else" expr
            | "match" expr "with" arms
            | or-expr

binding   ::= ( defname | "_" ) "=" expr
arms      ::= "|" arm { "|" arm }
arm       ::= pattern "->" expr

or-expr   ::= and-expr { "or" and-expr }
and-expr  ::= not-expr { "and" not-expr }
not-expr  ::= "not" not-expr | cmp-expr
cmp-expr  ::= add-expr [ cmpop add-expr ]            (non-associative)
cmpop     ::= "==" | "!=" | "<" | "<=" | ">" | ">="
add-expr  ::= mul-expr { ("+" | "-") mul-expr }
mul-expr  ::= unary { ("*" | "/" | "%") unary }
unary     ::= "-" unary | app
app       ::= atom { atom }                          (left-assoc application)

atom      ::= literal
            | path
            | qualified
            | TypeName                               (constructor)
            | record
            | "(" expr [ ":" type ] ")"

path      ::= (ident | private-ident) { "." ident }  (variable + field projections)
qualified ::= (ident | TypeName) "::" ident          (module::def or Type::derived)
record    ::= "{" [ path "with" ] field { "," field } "}"
field     ::= ident "=" expr

• Bindings carry no parameters — a let-bound function is an explicit lambda: let go = fun x -> … in …. One way to write a function.
• let _ = e in … discards the result — the sequencing idiom for effects. _ binds nothing and is exempt from the no-shadowing rule; it is not permitted in let rec.
• The and disambiguation: after and, the two-token sequence defname "=" begins a new binding of the enclosing let rec; anything else makes and the boolean connective. This is unambiguous because = never occurs in expressions (equality is ==) and bindings are parameterless.
• An arm’s body extends as far as possible; a subsequent | belongs to the innermost open match. A nested match in non-tail position must be parenthesized (the OCaml rule, chosen deliberately).
• Constructor application is ordinary application with a TypeName head: Ok bytes, BadCell { index = 1, text = "x" }, nullary None.
• Record update bases are paths, not arbitrary expressions: { r with cells = ys }.
• (e : type) is a local annotation, the only way to give a literal a non-default type.

3.4 Patterns

pattern    ::= "_" | ident | literal
             | TypeName [ pat-atom ]
             | record-pat
             | "(" pattern ")"
pat-atom   ::= "_" | ident | literal | TypeName | record-pat | "(" pattern ")"
record-pat ::= "{" fieldpat { "," fieldpat } [ "," ".." ] "}"
fieldpat   ::= ident [ "=" pattern ]                 (bare ident = punning)

A record pattern must name every field of the record type unless it ends with .. — omitting fields silently is an error, so adding a field to a type breaks exactly the patterns that need reviewing.

Patterns nest arbitrarily. There are no or-patterns, no guards, and no as bindings (nested match and fresh lets instead).

4. Precedence

Tightest to loosest:

1. field access .
2. application (juxtaposition), ::
3. unary -
4. * / %
5. + -
6. == != < <= > >= (non-associative — a < b < c is a parse error)
7. not
8. and
9. or
10. if / fun / let / match bodies

This ladder is the predicate language’s ladder (tr-grammar §2.3) with the arithmetic tiers inserted below the comparisons and implies absent.

5. Static rules

1. No shadowing. Binding a name already in scope — by let, fun, an equation parameter, or a pattern — is an error. Fresh names only.

2. Exhaustive matches, and redundant arms are errors.

3. Effect subsumption: f may call g iff g’s row ⊆ f’s row; ffi implies panic (design §3.3).

4. Operators are notation, not overloading (design §3.6, §3.7). The elaborator rewrites at the inferred monomorphic type; in polymorphic position the operators are unavailable and the function is taken as a parameter.

   Surface	Elaborates to
   == !=	T::eq (negated for !=)
   < <= > >=	T::compare
   + - * / %, unary -	per-type numeric primitives (I64::add, F64::div, …)
   and or	short-circuit builtins on Bool
   not	builtin on Bool

5. Arithmetic obligations: overflow, and a zero divisor for / and % on integers, are refinement obligations (design §3.2, §3.12). If SMT discharges the obligation the operation is total; otherwise the enclosing function’s row acquires panic. There is no panic syntax; explicit panics are a prelude function.

6. Integer division is floor division. On integer types / rounds toward negative infinity and % is the matching floor modulus (the result carries the divisor’s sign), preserving (a / b) * b + a % b == a. These are Python’s semantics — the reference-implementation language — not C/Rust truncation, so differential tests agree without adjustment. I64::MIN / -1 is an overflow obligation like any other. On F64 the operators are IEEE 754.

7. Termination: a recursive definition needs structural decrease or a decreases measure; failing both, its row acquires div (design §3.4).

8. Derived functions are reached by qualification: Row::eq, Row::show, Row::compare, Row::hash (design §3.7).

6. Interaction with the value encoding

Bool is a prelude sum type but encodes as JSON true/false, not {"tag": "True"} — the one special case in the sum encoding, matching what every host expects (recorded in tr-grammar §7).

7. Worked examples

The checked-in sample (examples/read_file.soil):

read_file : (fs : Fs) -> (path : Path) -> io (Result Utf8 FsError)
read_file fs path =
  match fs_read_bytes fs path with
  | Err e -> Err e
  | Ok bytes ->
    match utf8_decode bytes with
    | Ok text -> Ok text
    | Err _ -> Err (NotUtf8 { path = path })

A measure, symbolic operators, and notation elaboration:

gcd : U64 -> U64 -> U64
decreases b
gcd a b = if b == 0 then a else gcd b (a % b)

Row polymorphism, a lambda, and qualification:

sum_lengths : (rows : List Row) -> I64
sum_lengths rows =
  fold (fun acc r -> acc + len r.cells) 0 rows

8. Open questions raised by this spec

All questions raised by the first draft have been resolved and folded in: partial record patterns require .. (§3.4); the term layer uses the word connectives, unifying with the predicate language (§1, §3.3); the string escape set is fixed and scalar-value-only (§1); let bindings are parameterless and functions are explicit lambdas (§3.3).

Bootstrapping Plan: Rust Interpreter → Self-Hosted Compiler

Status: prototype plan. The Soil compiler (soilc) is written as a Trellis project — the first Trellis project — bootstrapped on a minimal Rust implementation (soil0) that is never thrown away. Decisions folded in from review: slow interpreted bootstrapping is accepted; the reference-oracle rule is amended to allow CLI oracles (design §4.5); the compiler is the first project with the Python-glue project second; the backend emits Cranelift CLIF, not C and not direct x86.

0. Premise

A compiler is the ideal Trellis dogfood: every pass is a pure, total function over trees, which is exactly what the JSON value model, expect tables, property tests, and differential testing handle best. The AST is a family of Trellis type definitions, so serialization (show/parse) and golden tests come for free. And the stage-0 implementation is not scaffold but permanent infrastructure: an independent implementation to differentially test the real compiler against, forever.

The bias to keep in view: compiler code is the easiest kind of Trellis code (pure, total, no FFI, no capabilities). It validates the language core and the lowering workflow; it validates nothing about bindings, capabilities, or trellis bind. Hence the Python-glue project stays as the second project.

1. Stage 0 — soil0 + soil-rt (hand-written Rust)

One workspace, two crates:

• soil-rt — the runtime, never bootstrapped away (design §3.10): values, reference counting, the JSON bridge, C ABI from the first commit, later pyo3.
• soil0 — parser, ML type + effect-row inference, exhaustiveness, tree-walking interpreter, test runner. No refinements, no termination checker, no codegen. Deliberately the size of a class project.

The load-bearing requirement: every pass is a JSON-in/JSON-out CLI command — soil0 lex, soil0 parse, soil0 infer, soil0 run. These are the future differential oracles. Slowness is explicitly fine; the whole bootstrap runs interpreted.

2. Stage 1 — Trellis toolchain on the interpreter

Design §11 milestones 2–3 unchanged in substance: daemon (incremental state, hashing/locks, context bundles, MCP tool surface, lowering jobs, agent-CLI provider), then the pure-core prelude as the first Trellis code. Soil execution is soil0 interpretation throughout. At the end of stage 1, Trellis is a working language whose execution engine happens to be an interpreter.

3. Stage 2 — soilc: the compiler as the first Trellis project

Each pass is a module of .tr specs, agent-lowered, running interpreted. Pass order, chosen so each has its oracle before it is written:

1. Lexer — warm-up; calibrates the spec-and-lower workflow.
2. Parser — deliberately early: the predicted worst case for the mutual-recursion ban (design §3.8), written as one definition with let rec … and … locals. Stress-tests the language design while it is still cheap to change.
3. Renamer / scope checker — no-shadowing, :: qualification.
4. Type + effect inference.
5. Exhaustiveness + pattern compilation.
6. ANF lowering (the mid-end, design §3.1).
7. Termination checker — new functionality, no soil0 counterpart; tested by spec only.
8. Refinement checker — emits SMT-LIB text as a pure function; Z3 runs behind a new Solver capability (the Py pattern). Refinements and demotion therefore arrive as compiler passes, not a separate milestone.
9. CLIF backend — see stage 3.

Strangler pattern: as each pass reaches accepted, the daemon swaps its soil0 pass for the Trellis one (shelling to soil0 run while interpreted). The soil0 passes are demoted to oracles, never deleted.

Testing: every pass gets JSON→JSON expect tables, properties (e.g. parse after print is identity), and differential tests against the matching soil0 command via CLI oracle. Passes 7–8 are spec-only.

4. Stage 3 — closing the loop

The backend is a pure Trellis pass ANF → CLIF text (golden-testable like every other pass), plus a small Rust driver in the workspace that feeds Cranelift for isel/regalloc/object emission — x86-64 and arm64, no C toolchain.

Why not direct x86: instruction selection, register allocation, and ELF emission are the largest and least testable chunk of a native backend, platform-locked, with zero free optimization. ANF is already shaped like portable three-address code; emitting a textual SSA IR outsources exactly the bad part. Direct emission remains a deferred independence move, not a foreclosed one.

Closure:

1. soilc (interpreted on soil0) compiles the prelude and itself → native soilc₁.
2. soilc₁ compiles the same sources → soilc₂.
3. Fixed point: soilc₁ and soilc₂ are byte-identical. Soil is unusually well-positioned for this — no mutation, canonical JSON, comparator-ordered maps, content addressing — so determinism is the default, but the fixed-point test is what enforces it.

5. Permanent division of labor

6. Mapping to the build order

Design §11 is reordered (recorded there): soil0+soil-rt, daemon, prelude, soilc as first project (through self-hosting closure), then trellis bind + FFI batteries + minimal IDE, then the Python-glue project as second project — it validates the FFI/capability/bind half of the pitch that the compiler cannot touch.

7. Remaining risks

• Biased dogfood: the compiler proves the pure core, not the FFI story; mitigated only by actually doing the second project.
• Fixed-point determinism: any iteration-order or fresh-name nondeterminism in lowered passes breaks stage 3; the renamer must allocate names canonically.
• Type-inference pass size: the hardest single lowering target in the plan; if agent lowering strains anywhere, it is there — split the module aggressively.

Milestone Plans — Overview

These plans are implementation guides for future agents. Each corresponds to a milestone of the build order (design §11, bootstrap plan) and states its goal, scope, work breakdown, testing strategy, exit criteria, and open decision points.

How to use these plans

• Read CLAUDE.md, then docs/design.md for the decisions and reasoning, then the plan for your milestone. The plan tells you what to build and in what order; the specs (docs/tr-grammar.md, docs/lock-schema.md, docs/soil-syntax-spec.md) tell you what the artifacts must look like.
• Decision points listed in a plan are not yours to make. The initial sets were all resolved with the user on 2026-08-22 and are recorded in each plan; if implementation surfaces a new open choice, present options to the user and record the outcome in the plan and in docs/design.md the same way.
• Exit criteria are the definition of done. Do not start the next milestone’s work early; the ordering is load-bearing (each stage is the oracle or substrate for the next).
• When implementation reveals a spec contradiction or gap, stop and raise it — spec fixes propagate to docs/ and examples/ before code works around them.

Sequence

Rust code accumulates in one workspace (soil-rt, soil0, later the daemon and the Cranelift driver). Trellis code (prelude, soilc) lives in Soil roots with soil.toml. Nothing in these plans exists yet; the repo is design-only until plan 01 begins.

Plan 01 — soil-rt: the runtime crate

References: design §3.7 (derived functions), §3.10 (runtime and embedding), §3.12 (primitives), tr-grammar §7 (JSON value encoding).

Goal

A Rust crate owning the Soil value model, memory management, derived operations, the canonical JSON bridge, and a C ABI for embedding. This crate is permanent — it is never bootstrapped away — and everything else (interpreter, compiled code, hosts) manipulates values only through it.

Scope

1. Workspace skeleton. Cargo workspace at the repo root (or a rust/ subdirectory — decision point) containing soil-rt; later crates (soil0, daemon, Cranelift driver) join the same workspace.
2. Value model. A Value representation covering: fixed-width integers (I64, U64, I32, U32, I16, U16, I8, U8), BigInt, F64 with total order (total_cmp; NaN equal to itself, sorts last), Utf8 (immutable, validated), Bytes, Unit, records (fields in declaration order), sums (tag + at most one payload), List, Map (stored in comparator order — the comparator is a Soil closure carried by the map), closures, and opaque handles. Bool is the prelude sum True | False; the runtime may represent it natively as an optimization but must present it as a sum.
3. Type descriptors. Runtime-registered metadata per type: field names and order, variant names, derivation strategy (structural / opaque / per-field ignored with default thunks). Descriptors drive derived ops and type-directed JSON decode. Registration API used by the interpreter now and compiled code later.
4. Memory. Reference counting. No Perceus reuse yet (that is compiler-side, stage 3+); no cycle collector (strategy explicitly deferred, design §10 — document that cycles leak for now).
5. Derived operations. One implementation each of structural eq/compare/hash/show over Value + descriptor, honoring strategies: opaque → identity/"<handle>"/address; ignored → skipped. Deriving eq over a closure is rejected at descriptor registration.
6. Canonical JSON. Encode and type-directed decode per tr-grammar §7, exactly: internally tagged sums, Bool as JSON booleans, BigInt hybrid by range (±(2^53−1)), F64 "NaN"/"Inf"/"-Inf" strings, Bytes base64, Unit null, maps as comparator-ordered {"key","value"} arrays, ignored fields omitted on encode and refilled from default thunks on decode, opaque decode error, closures a hard error both ways. Encoding is canonical: declaration-order fields, shortest round-trip floats — byte-equal output for equal values.
7. Errors. A structured SoilError (panic kind, message, trace hook, offending JSON inputs when available) — the debug-mode payload of design §3.11’s host-stub rule.
8. C ABI. No global state; explicit soil_init/soil_teardown; opaque SoilValue* handles with constructors/accessors/refcount ops; error out-parameters; a trivial main wrapper entry. Header via cbindgen. A minimal C demo program proves embeddability.

Non-goals

Execution (plan 02), Perceus reuse, cycle collection, pyo3 (plan 06), refinements (checker-side only, and later).

Testing

• Rust unit tests per module; property tests (proptest) for: JSON round-trip identity on random well-typed values, eq/compare/hash agreement (equal ⇒ same hash; compare total order laws incl. NaN), canonical encoding determinism (encode twice, byte-equal).
• A fixtures/ corpus of (type descriptor, value, canonical JSON) triples, checked in — these become shared goldens for soilc’s passes later.
• The C demo compiled and run in CI fashion (a script for now).

Exit criteria

• The C demo constructs values through the ABI, round-trips them through canonical JSON, and tears down cleanly (no leaks under a debug counter).
• All tr-grammar §7 rows demonstrably implemented, including the Bool, BigInt-range, and ignored-field-default cases, backed by fixtures.
• Descriptor API documented well enough that plan 02 needs no runtime changes to interpret the prelude.

Decision points — resolved 2026-08-22

• Workspace location: rust/ subdirectory holding the Cargo workspace (soil-rt, later soil0, the daemon, the Cranelift driver); the repo root stays docs/examples/Trellis-roots.
• Integer widths: all eight (I64…U8) from the start — adding widths later ripples through JSON, the C ABI, and descriptors, and together they are mostly a macro.
• BigInt: num-bigint.
• Map representation: sorted vec of pairs with the carried comparator closure — trivially correct and canonically ordered for show/JSON; swap for a tree behind the same API only if profiling demands it.

Implementation plan

A detailed implementation guide exists at impls/01-soil-rt-impl.md. It records a second round of decisions resolved 2026-08-22 — Value as a Rust enum with nonatomic refcounted boxes, closures as boxed Rust callables, hand-rolled canonical encoder with serde_json decode, interned per-instance TypeIds, and hash as FNV-1a 64 over canonical JSON bytes (also recorded in design §3.7, being language-observable) — plus the module map, build order, fixture format, C ABI surface, and a set of micro-pins (its §8, approved 2026-08-22, including: all dev dependencies managed through a repo-root shell.nix, which is also the single pin for the Rust toolchain).

Implementation Plan 01 — soil-rt

Detailed implementation guide for ../01-soil-rt.md. That plan states the scope and exit criteria; this one states how the crate is actually structured and built, records the implementation decisions resolved with the user on 2026-08-22, and proposes the remaining micro-details (§8) for review before code is written. References: design §3.7, §3.10, §3.12, tr-grammar §7, soil-syntax-spec §1 (string escapes), plan 02 (the first consumer).

1. Resolved implementation decisions (2026-08-22)

The one language-observable item (the hash definition) is recorded in design §3.7; the rest are runtime-internal and live here.

2. Workspace and crate skeleton

Per plan 01’s resolved decision points: the Cargo workspace lives in rust/; the repo root stays docs/examples/Trellis-roots.

shell.nix              -- repo root; the dev environment, single source of truth (§8.12)
rust/
  Cargo.toml           -- workspace; members = ["soil-rt"] (later soil0, daemon, clif driver)
  check.sh             -- runs inside nix-shell: fmt --check, clippy -D warnings, test, C demo build+run
  soil-rt/
    Cargo.toml
    cbindgen.toml
    src/               -- module map in §3
    fixtures/          -- (descriptor, value, canonical JSON) triples, §6
    cdemo/
      main.c
      build.sh         -- cc against the staticlib + generated header

All dev dependencies are managed through a repo-root shell.nix: the Rust toolchain (rustc/cargo — no rust-toolchain.toml; the nixpkgs pin in shell.nix is the single source of the compiler version), cbindgen, the C compiler for the demo, and whatever later milestones add (Z3, Python). Building outside nix-shell is off the supported path. Rust crate dependencies remain in Cargo.toml/Cargo.lock as usual — shell.nix manages tools, Cargo manages crates.

Crate dependencies, kept deliberately short:

soil-rt builds as both rlib (for soil0 and the daemon) and staticlib (for the C demo and embedding).

3. Module map

src/
  lib.rs         -- Runtime (owns Registry + debug counters), re-exports, crate docs
  error.rs       -- SoilError, PanicKind, TraceFrame
  value.rs       -- Value, Ref<T>, heap payloads (Record, SumVal, MapVal, Closure, OpaqueVal)
  descriptor.rs  -- TypeShape, TypeDesc, FieldDesc, Registry, TypeId; descriptor JSON (§5)
  ops.rs         -- derived eq / compare / hash over Value + descriptor
  json/
    mod.rs
    encode.rs    -- the canonical encoder; owns every canonicality guarantee
    decode.rs    -- type-directed decode over the serde_json tree
  capi.rs        -- the C ABI surface (§7), the only module containing `extern "C"`

Dependency direction is strictly downward: capi → {json, ops} → {descriptor, value} → error. No module reaches back up; no global state anywhere (Runtime is a value the embedder holds).

4. Build order

Each step names its deliverable, the API it stabilizes, and its tests. Steps are sequential; a step is done when its tests pass and check.sh is green.

Step 1 — skeleton and SoilError

Workspace files, empty modules, check.sh, toolchain pin.

#![allow(unused)]
fn main() {
pub struct SoilError {
    pub kind: PanicKind,       // Overflow, DivideByZero, DecodeError,
                               // TypeError, DerivationError, CapiMisuse, …
    pub message: String,
    pub trace: Vec<TraceFrame>, // hook only; filled by soil0/daemon later
    pub inputs: Option<String>, // offending canonical-JSON inputs when available
}
}

This is the debug-mode payload of design §3.11’s host-stub rule; plan 02 raises interpreter panics as SoilError, so the shape is API from day one. Tests: construction and Display formatting only.

Step 2 — Value and Ref<T>

#![allow(unused)]
fn main() {
pub enum Value {
    I64(i64), U64(u64), I32(i32), U32(u32),
    I16(i16), U16(u16), I8(i8), U8(u8),
    F64(f64),
    BigInt(Ref<BigInt>),
    Utf8(Ref<str>),
    Bytes(Ref<[u8]>),
    Unit,
    Record(Ref<Record>),     // TypeId + field values in declaration order
    Sum(Ref<SumVal>),        // TypeId + variant index + optional payload
    List(Ref<Vec<Value>>),
    Map(Ref<MapVal>),        // sorted Vec<(Value, Value)> + comparator Closure
    Closure(Ref<Closure>),   // Box<dyn Fn(&[Value]) -> Result<Value, SoilError>>
    Opaque(Ref<OpaqueVal>),  // TypeId + Box<dyn Any>; identity = address
}
}

• Value is small and passed by value; clone is a refcount bump on heap variants.
• Ref<T> wraps Rc<T>; in debug builds every allocation increments and every final drop decrements a thread-local live counter (consistent with instances being single-threaded), exposed as soil_debug_live_values() for the leak-check exit criterion. Release builds compile the counter out.
• Bool is not a Value variant: it is the prelude sum True | False (plan 01 scope item 2). The registry pre-registers it (step 3) and the JSON layer special-cases its TypeId.
• Cycles leak; documented on Ref (design §10 defers the strategy).
• MapVal maintains the sorted-vec invariant internally: insertion is binary search via the carried comparator (a Closure — fallible, so every map operation is fallible). Plan 01’s resolved decision: swap for a tree behind the same API only if profiling demands it.

Tests: refcount behavior (clone/drop, counter returns to zero), map insert/lookup/remove with a native comparator closure, closure invocation, Value size assertion (fits two words + discriminant).

Step 3 — descriptors and the registry

#![allow(unused)]
fn main() {
pub enum TypeShape {
    I64, U64, I32, U32, I16, U16, I8, U8,
    BigInt, F64, Utf8, Bytes, Unit,
    List(Box<TypeShape>),
    Map(Box<TypeShape>, Box<TypeShape>),
    Closure,                  // may appear in shapes; poisons derivation
    Named(TypeId),            // records, sums, opaques — including recursion
}

pub struct TypeDesc {
    pub name: String,               // cased name, e.g. "SummaryRow"
    pub strategy: Strategy,         // Structural | Opaque
    pub body: TypeBody,             // Record(Vec<FieldDesc>) | Sum(Vec<VariantDesc>) | Opaque
}
pub struct FieldDesc {
    pub name: String,
    pub shape: TypeShape,
    pub ignored: Option<Closure>,   // default thunk; presence marks the field ignored
}

impl Registry {
    pub fn declare(&mut self, name: &str) -> Result<TypeId, SoilError>;
    pub fn define(&mut self, id: TypeId, desc: TypeDesc) -> Result<(), SoilError>;
    pub fn register(&mut self, desc: TypeDesc) -> Result<TypeId, SoilError>; // declare+define
    pub fn get(&self, id: TypeId) -> &TypeDesc;
    pub fn lookup(&self, name: &str) -> Option<TypeId>;
}
}

• Two-phase registration (declare then define) exists because recursive types across definitions are legal (design §3.8); a self-referential shape names its own declared id. Using an undefined id in any runtime operation is CapiMisuse.
• Derivability is computed at define time: a type whose shape transitively contains Closure (through fields, payloads, list/map elements — map comparators excluded, they are structure, not content) is marked non-derivable, per “deriving eq on a type containing an arrow is a type error” (design §3.7). Derived ops on such a type return DerivationError; the static rejection happens in soil0’s checker.
• The registry pre-registers Bool (sum True | False, in that declaration order) at construction and exposes Registry::BOOL.
• Strategies per design §3.7: Structural (default), Opaque (identity/"<handle>"/address); ignored is per-field with a mandatory default thunk.

Tests: registration round-trips, recursive type via declare/define, closure-poisoning marks non-derivable, duplicate names rejected, Bool present.

Step 4 — derived operations (ops.rs)

One implementation each of eq, compare, hash over (&Runtime, &Value); show is the canonical encoder (step 5), per “show is the JSON encoder” (design §3.7).

• compare is a total order per type. Numeric types compare numerically within their own type; comparing values of different types is TypeError (the checker prevents it; the runtime is defensive).
• F64: all NaN bit patterns are one logical value — equal to each other, sorting after +Inf (design §3.7: “NaN is equal to itself and sorts last”). This is total_cmp semantics with the NaN payload/sign distinctions collapsed, because canonical JSON has a single "NaN" and round-tripping must preserve eq. -0.0 < 0.0 stays distinct (canonical JSON distinguishes -0.0 from 0.0). Pinned in §8.
• Structural equality: records field-wise in declaration order; sums by variant index then payload; lists element-wise then by length; maps by sorted entry sequence (the comparator closure is excluded from eq — it is structure, not content); Utf8/Bytes byte-wise; BigInt numerically.
• opaque strategy: eq/compare/hash on the payload address.
• ignored fields: skipped by eq/compare; constant hash contribution by construction (omitted from the canonical encoding).
• hash: fnv1a64(canonical_json_bytes(v)) with the standard FNV-1a offset basis and prime, documented in the module; opaque hashes the address bytes instead.
• eq/compare/hash reaching a Closure value is DerivationError (defense in depth behind the descriptor-level rejection).

Tests: unit tests per type; property tests deferred to step 6 where generators exist.

Step 5 — the canonical encoder (json/encode.rs)

Implements tr-grammar §7 exactly, writing into a Vec<u8>. This module owns every canonicality guarantee; nothing else in the system may produce value JSON.

No whitespace anywhere (element separators are , and : alone — §8). Encoding is value-directed: scalars self-describe via their variant, records/sums carry their TypeId, and the registry supplies field and variant names.

Tests: golden strings per row of the table, including BigInt at ±(2^53−1)±1, negative zero, integral floats (1.0 not 1), and the determinism test (encode twice, byte-equal).

Step 6 — type-directed decode (json/decode.rs) and fixtures

decode(&Runtime, &TypeShape, &str) -> Result<Value, SoilError>: parse with serde_json into serde_json::Value, then walk the shape. Strict: every deviation is a DecodeError naming the JSON path.

• Numbers must be integral and in range for the target width; BigInt accepts number-or-string (hybrid); F64 accepts numbers and the three strings.
• Records: missing non-ignored field, unknown field, or a present ignored field are errors (§8); after the other fields decode, each ignored field is refilled by invoking its default thunk with the non-ignored fields as arguments in declaration order (§8).
• Sums: exactly the keys tag (+ value iff the variant has a payload); unknown tag is an error. Bool accepts only true/false.
• Opaque shapes and closure shapes are errors (tr-grammar §7).
• Recursion depth is bounded by serde_json’s parser limit; the walk itself is iterative or depth-checked to keep panic out of the crate.

Fixtures (fixtures/*.json, the shared goldens plan 01 requires, reused later by soilc’s passes):

{
  "types": [ …descriptor JSON, §5-encoded… ],
  "type": "SummaryRow",
  "canonical": "{\"count\":3,\"mean\":1.5}",
  "accepts": ["{\"mean\":1.5,\"count\":3}"],
  "rejects": ["{\"count\":3}", "{\"count\":3,\"mean\":1.5,\"x\":0}"]
}

The harness decodes canonical, re-encodes, requires byte equality; decodes each accepts entry and requires eq with the canonical value; requires each rejects entry to fail. Fixture files cover every row of the tr-grammar §7 table, including the Bool, BigInt-range, and ignored-field-default cases named in the exit criteria. Default thunks in fixtures are limited to a tiny built-in vocabulary the harness provides (e.g. a constant, a field copy), since fixtures are data, not code.

Property tests (proptest), closing plan 01’s testing section:

• generator of random well-formed descriptors + well-typed values;
• decode(encode(v)) eq v; encode determinism (byte-equal);
• eq ⇒ same hash; compare total-order laws (reflexive, antisymmetric, transitive, total) including NaN and -0.0;
• compare == Equal ⇔ eq.

Step 7 — descriptor JSON (descriptor.rs, serialization half)

The fixtures and the C ABI both need descriptors as data. The encoding follows tr-grammar §7’s own conventions, as if descriptors were Soil values (internally tagged sums, records):

{ "name": "SummaryRow",
  "strategy": {"tag": "Structural"},
  "body": {"tag": "Record", "value": [
    {"name": "count", "shape": {"tag": "U64"}, "ignored": null},
    {"name": "mean",  "shape": {"tag": "F64"}, "ignored": null} ] } }

TypeShape::Named serializes by name, not id (ids are per-instance); loading a descriptor list resolves names in two passes (declare all, then define all), which handles recursion for free.

This format is the seed of plan 02’s --types env.json contract; plan 02 freezes it in docs/soil0-cli.md, so it should be reviewed with that in mind, but it is not frozen by this plan.

Step 8 — the C ABI (capi.rs) and the demo

Surface (prefix soil_, verbatim rules: no global state, explicit init/teardown, no unwinding across the boundary):

SoilRuntime *soil_init(void);
void         soil_teardown(SoilRuntime *);

/* types: registered as descriptor JSON — one format everywhere */
int  soil_register_types(SoilRuntime *, const char *desc_json, SoilError **err);

/* values: opaque handles; constructors, accessors, refcounting */
SoilValue *soil_i64_new(int64_t);                 /* …one per scalar kind */
SoilValue *soil_record_new(SoilRuntime *, uint32_t type_id,
                           SoilValue *const *fields, size_t n, SoilError **err);
/* …sum_new, list_new, accessors (checked, error out-param)… */
SoilValue *soil_value_clone(const SoilValue *);
void       soil_value_free(SoilValue *);

/* derived ops and the JSON bridge */
bool   soil_eq(SoilRuntime *, const SoilValue *, const SoilValue *, SoilError **);
char  *soil_show(SoilRuntime *, const SoilValue *, SoilError **);   /* canonical JSON */
SoilValue *soil_decode(SoilRuntime *, const char *shape_json,
                       const char *value_json, SoilError **);

/* errors */
const char *soil_error_message(const SoilError *);
int         soil_error_kind(const SoilError *);
void        soil_error_free(SoilError *);

/* debug builds only */
size_t soil_debug_live_values(void);

int soil_main(int argc, char **argv, SoilMainFn);   /* trivial main wrapper */

• SoilValue* is a leaked Box<Value>; clone/free manage it. Handles and the runtime are single-threaded (decision §1); documented in the header.
• Every entry point wraps its body in catch_unwind; a caught panic becomes a SoilError of kind Internal — Rust panics never cross the boundary.
• Registration goes through descriptor JSON rather than a C struct surface: one format for fixtures, plan 02’s env.json, and embedding, and the C API stays five functions instead of thirty (§8).
• Header generated by cbindgen into soil_rt.h; cdemo/main.c registers a record type, constructs a value through the ABI, shows it, decodes it back, checks eq, frees everything, and asserts soil_debug_live_values() == 0. check.sh builds and runs it — the embeddability exit criterion.

Closures are not constructible over the C ABI in this plan (soil_closure_new arrives with compiled code, plan 05); the demo therefore uses map-free, ignored-free types, and Rust tests cover the rest.

Step 9 — docs pass

Rustdoc on Runtime, Value, Ref, Registry, TypeShape, the JSON modules (stating the canonicality guarantees and the FNV-1a definition), and capi (threading rule, error contract). Exit criterion: plan 02 can interpret the prelude against this API without runtime changes, judged by walking plan 02’s scope list against the rustdoc.

5. Exit-criteria traceability

6. Non-goals (restated from plan 01)

Execution of any kind, Perceus reuse, cycle collection, pyo3, refinements. Additionally out of scope here: C-ABI closure construction (plan 05), stable TypeIds across runs (names are the stable identity), and any performance work beyond the size assertion on Value.

7. Risks and checks

• Canonicality regressions are spec violations, not bugs of degree; the determinism property test and fixture byte-comparisons run in every check.sh.
• ryu output drift (crate update changing formatting) would break canonical bytes: the fixtures pin the expected strings, so an update that changes output fails loudly; the lockfile pins the version.
• serde_json float parsing is imprecise without the float_roundtrip feature — found by the property tests during implementation (§8.15). The feature is on; the round-trip property guards against regression.
• Map comparator misbehavior (a comparator that is not a total order) silently corrupts the sorted-vec invariant. The runtime does not detect it (that is the refinement checker’s future job); documented on MapVal.
• Descriptor/value mismatch through the C ABI (wrong field count, wrong scalar kind) must be a checked SoilError, never UB: record_new and friends validate against the descriptor.

8. Micro-pins — approved 2026-08-22

Per the overview’s rule that new choices go to the user, these were presented as proposals and approved by the user on 2026-08-22 (item 12 added at approval time). They are pinned; reopening one is a new decision point.

1. String escape set (canonical JSON): escape exactly " , \, and control characters U+0000–U+001F; use the short forms \n \r \t \b \f where they exist and lowercase \u00xx otherwise; all other characters (including non-ASCII) are raw UTF-8; no \/. (RFC 8785’s choices; deliberately not Soil’s source escape set, which is a different layer — soil-syntax-spec §1.)
2. Whitespace: none. Separators are , and : only.
3. NaN and zero: all NaN bit patterns are one logical value (equal, sorts after +Inf); -0.0 and 0.0 are distinct with -0.0 < 0.0, and ryu renders them -0.0 / 0.0, which round-trip. NaN collapses because canonical JSON has a single "NaN"; zeroes stay distinct because the encoding distinguishes them.
4. Base64 for Bytes: standard alphabet, with padding, no line wrapping; decode rejects non-canonical padding/alphabet.
5. Strict decode: unknown record fields, missing non-ignored fields, and present ignored fields are all DecodeErrors. Rationale for the last: encode omits them, so accepting them would admit a second, unverifiable source for a field whose value is defined to be reconstructed (design §3.7); one canonical form in both directions.
6. Default-thunk arity: an ignored field’s default closure receives the record’s non-ignored fields, in declaration order, as its arguments (“the record’s other fields in scope”, design §3.7, restricted to non-ignored to avoid ordering dependencies among ignored fields).
7. Duplicate keys in decoded JSON: rejected (DecodeError), not last-wins. Requires walking with a duplicate check since serde_json’s default map is last-wins — use its preserve_order/raw-value facilities or a custom visitor; whichever is chosen, the observable rule is “duplicates reject”.
8. Debug leak counter: thread-local (instances are single-threaded), debug builds only, exposed as soil_debug_live_values().
9. Panic policy: the crate itself never panics on valid API use; catch_unwind at the C ABI converts bugs to SoilError::Internal. Rust-side consumers (soil0) get Result everywhere.
10. C-ABI type registration via descriptor JSON (not a C struct builder API): one descriptor format across fixtures, env.json, and embedding.
11. Descriptor JSON is reviewable but not frozen here; plan 02 freezes it inside docs/soil0-cli.md as the --types contract.
12. All dev dependencies are managed through a repo-root shell.nix (§2): it is the single pin for the Rust toolchain (no rust-toolchain.toml) and provides every tool (cbindgen, the C compiler, later Z3/Python); building outside nix-shell is unsupported. Cargo continues to manage Rust crate dependencies. Location and single-pin choice resolved with the user 2026-08-22.

Items 13–15 were added during implementation (2026-08-22, autonomous session) — recorded here and flagged for user review:

13. Decoded maps carry the derived structural order. A map arriving through JSON has no program-supplied comparator closure to carry, so MapVal orders are Structural (the derived compare) or Custom(closure); decode always builds Structural, map operations take the runtime (structural order consults the registry), and the order is structure, not content — eq/compare see only the entries. Map decode accepts entries in any order (re-sorted) but rejects duplicate keys.
14. Ignored-default vocabulary. FieldDesc.ignored holds an IgnoredDefault: Const (a constant of the field’s own shape, scalar-only), CopyField (a non-ignored, same-shaped field), or Native (an arbitrary embedder thunk — what a Soil default expression eventually compiles to). Const/CopyField are the serializable subset used by descriptor JSON and fixtures; Native does not serialize. The C ABI’s soil_record_new takes non-ignored fields and refills ignored ones, mirroring decode.
15. serde_json needs its float_roundtrip feature. The default float parse is not correctly rounded (1.8821735589659427e48 re-parses to different bits), which breaks canonical round-trips; the round-trip property test caught it. The feature is enabled and pinned in Cargo.toml with a comment.

9. Open questions

• None currently. §8 was approved 2026-08-22; reopening any of its items is a new decision point for the user.

Plan 02 — soil0: the minimal Soil implementation

References: docs/soil-syntax-spec.md (the parser’s contract), design §3 (language), bootstrap plan §1.

Goal

A deliberately small Rust implementation of Soil — parser, static checks, tree-walking interpreter over soil-rt values — whose every pass is a JSON-in/JSON-out CLI command. It is the execution engine for the entire bootstrap and the permanent differential oracle for soilc. Resist every temptation to make it good; make it correct and small.

Scope

1. The AST JSON schema — a spec artifact, written first. The exact JSON encoding of the surface AST and of check results. This is the CLI oracle contract that soilc’s Trellis type definitions must later reproduce, so it follows the tr-grammar §7 value-encoding conventions (internally tagged sums, records) as if the AST were already Soil data. Deliverable: docs/soil0-cli.md, reviewed before code.
2. Lexer + parser. Hand-written recursive descent implementing docs/soil-syntax-spec.md exactly: the and binding/connective disambiguation, non-associative comparisons, parenthesized non-tail match, .. record patterns, the fixed escape set, decreases lines. Errors carry source spans.
3. Renamer. Scope resolution, the no-shadowing rule, :: qualification, _private visibility.
4. Type + effect inference. ML inference (HM with records and sums from registered type shapes — no row-polymorphic records needed), effect rows as sets with row variables, subsumption at calls, operator-notation elaboration (== → T::eq, arithmetic → per-type primitives at monomorphic types only). No refinements (parsed, retained in the AST, otherwise ignored). No termination checking: every self-recursive or let rec definition conservatively acquires div (consequence handled in plan 04).
5. Exhaustiveness + redundancy checking for matches.
6. Interpreter. Strict tree-walk over soil-rt values; closures; capability primitives implemented natively (fs_read_bytes, clock, rand, env, proc) plus the prelude’s fake capability constructors (fake_fs, seeded fake_rand, fake_clock); arithmetic follows floor division/modulus and panics (as SoilError) on overflow and zero divisors — obligations don’t exist yet, so these are always-on runtime checks, matching debug-mode semantics.
7. CLI. soil0 lex|parse|rename|infer|check|run|test, each reading source (or AST JSON) and emitting schema-conformant JSON on stdout, errors as structured JSON on stderr, nonzero exit. run takes --entry name --args <json-array> and prints the canonical JSON result; test executes a JSON test bundle (assembled by the daemon) and reports per-case results in the lock’s result vocabulary.

Non-goals

Refinement checking, termination checking, codegen, optimization of any kind, .tr parsing (daemon’s job, plan 03), Python FFI.

Testing

• Golden tests: a corpus of .soil fragments → expected AST/type/effect JSON, including every syntax-spec static rule as a rejection test (one test per rule: shadowing, redundant arm, a < b < c, missing .., parameterless let violation, bad escape…).
• examples/read_file.soil and examples/csvstats/median.soil must parse, check, and (with stub callees) run.
• Interpreter: expect-style tests mirroring the .tr examples’ test blocks, run through soil0 test.
• Fuzz the parser (cargo-fuzz or a simple generator) for panic-freedom.

Exit criteria

• docs/soil0-cli.md exists and every command conforms to it.
• Both checked-in .soil examples check and run with correct results.
• The rejection-test corpus covers every static rule in docs/soil-syntax-spec.md §5.
• A downstream consumer (plan 03) can drive lex→check→test entirely through the CLI without linking soil0 as a library.

Decision points — resolved 2026-08-22

• Library + CLI: the daemon links soil0 as a crate for in-process checking, but the CLI is the frozen compatibility contract — oracle and conformance tests always go through the CLI, never the library API.
• Spans: UTF-8 byte offsets are canonical (start/end), with derived line/col included alongside for display.
• Type environment: commands take --types env.json — type descriptors in the schema’s own encoding. Early tests hand-write it; the daemon generates it from .tr files later. soil0 never parses .tr.

Plan 03 — the Trellis daemon

References: design §4 (the specification layer, lowering, the daemon), §6 (hashing and locks), docs/tr-grammar.md, docs/lock-schema.md.

Goal

The long-running service that makes Trellis a language: parses .tr files, computes the hashes, maintains locks and the derived manifest, assembles context bundles, runs lowering jobs against an agent CLI with the MCP tool surface, and serves the CLI (and later the IDE and LSP). Execution is delegated to soil0 throughout.

Scope

1. .tr parsing. Frontmatter, reserved fenced blocks, block mini-languages (signature, requires/ensures/invariant predicates, test call-arrow lines with with bindings, property, cram, reference, exports, allow), validity rules — all per docs/tr-grammar.md. Unknown blocks pass through as prose.
2. Hashing. The three-part hash (formal/test/prose per tr-grammar §1), soil_hash with content addressing (free variables replaced by callee hashes, private helpers folded in), the recursive-type cycle hash. Canonicalization rules documented; hashes must be reproducible across machines.
3. Locks and manifest. Read/write .lock sidecars per docs/lock-schema.md in canonical JSON; derive soil.lock by merge (definitions, soil_private nodes, escape-hatch audit, trusted packages); enforce the schema invariants (accepted gating, oracle acceptance rule, block-author pinning).
4. Incremental state. Watch the Soil root; on change, recompute hashes, apply the invalidation table (lock-schema §8), update statuses.
5. Context bundles. The fixed directory layout per design §4.6: spec.md, callees/ (signatures only; demoted refinements shown as base type + note), tests.json, examples/ (prelude corpus), reference.py or CLI-oracle stanza, previous.soil.
6. MCP server + lowering jobs. The six tools (read_context, check_types, check_refinements — a stub returning none until soilc, run_tests (sandboxed, fakes only), write_soil, ask_human); one headless agent invocation per lowering (Claude Code provider first) with turn/time/cost caps, isolated agent home, every tool call logged to f.log; ask_human ends the invocation, the answer is written into the .tr prose, and the job re-runs fresh; serial queue with invalidation when a dependency is edited mid-flight.
7. Test running. Expect/property via soil0 test with fakes; contradiction pre-flight (mechanical same-input/different-output check before any tokens are spent); cram runner (temp dir, with file fixtures, literal output, [n] exit codes) and trellis call (real capabilities) — real mode never exposed to the lowering sandbox.
8. Thin CLI. trellis check|status|lower|test|call|repl speaking to the daemon. REPL: call any definition with JSON args (Trellis level), feeding later REPL-to-test promotion.
9. Telemetry. Tokens, cost, retries, provider, model per lowering, to f.log; provider/model into the lock’s lowering record.

Non-goals

The IDE (plan 06), LSP beyond bare diagnostics, refinement checking, concurrent lowerings, raw-API provider, hosted anything.

Testing

• Hash stability: golden hashes over examples/; mutation tests (edit prose → only prose_hash moves, etc. — one test per invalidation row).
• Lock round-trip: examples/*.lock re-emitted byte-identical.
• A scripted fake agent provider (plays back canned tool-call sequences) to test the job loop, question channel, caps, and log without spending tokens; one live smoke test against real Claude Code headless.
• End-to-end: a fixture project lowers mean.tr-sized definitions to green through the fake provider.

Exit criteria

• examples/ fully round-trips: parse → hash → lock regeneration matches the checked-in sidecars (update examples if the daemon exposes spec drift — spec first, then code).
• One real headless lowering of a trivial definition completes: bundle → agent → write_soil → checks → tests → lock, with f.log populated.
• A question round-trip works: ask_human → IDEless CLI answer → prose diff → re-invoke → green.

Decision points — resolved 2026-08-22

• IPC: JSON-RPC over a Unix socket ($XDG_RUNTIME_DIR/trellis/<root-hash>.sock); LSP speaks its own stdio transport; TCP is the future remote-serving path.
• Language: Rust, in the rust/ workspace as trellis-daemon, linking soil0 and soil-rt (the soil0 CLI remains the oracle contract regardless).
• Sandboxing: all three layers. Tool allow-list (the six MCP tools, no shell) + the agent CLI’s own sandbox and isolated home + a chroot-style OS jail around the agent process (unprivileged via user namespaces / bubblewrap in practice). Defense in depth from v1.
• Incremental state: explicit refresh — hashes re-checked at request boundaries plus trellis refresh; the watcher arrives with the IDE milestone on the same invalidation code path.

Plan 04 — the pure-core prelude

References: design §5 (the prelude as a trusted corpus), §3.5 (capabilities), examples/read_file.tr.

Goal

The first Trellis code: the pure core prelude, written as .tr specs and agent-lowered through the real daemon pipeline, human-reviewed to accepted. It is simultaneously the stdlib, the few-shot corpus that defines the agent’s Soil style, and the first honest test of the whole loop. Interpreted on soil0; small (a few thousand lines of Soil).

Scope

1. read_file first (design §5): capabilities, effects, Result, and the runtime boundary in one definition. Promote examples/read_file.tr into the real prelude root and lower it for real; reconcile any drift back into examples/.
2. Core types and functions, roughly in dependency order: Bool (with its JSON special case), Option, Result, List (map, filter, fold, len, nth, append, reverse, sort_by…), Utf8 (split, trim, parse-number…), Bytes, BigInt, Map with explicit comparator (the Map.Make-as-function idiom, design §3.6), JSON encode/decode surface (thin wrappers over the runtime).
3. Capabilities and fakes. The capability types (Fs, Net, Clock, Env, Proc, Rand) as opaque types with their World derivations, and the fake constructors with pinned seeds/timestamps — signatures in Trellis, backed by soil0/soil-rt native primitives.
4. Corpus duty. Every lowering is reviewed as a style exemplar, not just for correctness: idiomatic match shapes, naming, use of local lets vs private helpers. Style disagreements are settled by PR-style review with the user and become the corpus.
5. Trust and packaging. The prelude is a Soil root with soil.toml; on completion, pin its package hash as trusted (design §5); all exported definitions accepted and pinned.

The totality problem (known, planned for)

soil0 has no termination checker, so every recursive prelude function conservatively carries div — but the prelude’s signatures claim total, and those claims matter for the corpus and for callers. Interim policy (confirm with user at kickoff): the .tr signatures state the intended row; the daemon records a per-definition div-unverified flag in the lock (like a demoted refinement) rather than widening signatures; the stage-2 termination checker (plan 05) later discharges them in bulk. This mirrors the demotion philosophy: unproven, visible, tests still gate.

Non-goals

Batteries layers (soil-rs-std, soil-py-std — plan 06), Py capability, retrieval (whole prelude fits in context), performance.

Testing

• Every definition: expect tests + properties per the effect-row budget (pure functions fuzzed hard); capability functions get fake-capability tests; read_file keeps its real-mode cram test.
• Cross-cutting properties: sort_by stability and order laws, parse ∘ show identity on prelude types, Map comparator-order invariants.
• Differential where cheap: CLI oracles against Python equivalents (statistics, str methods) for the numeric/string corners.

Exit criteria

• Every exported definition accepted, pinned, tests green, package hash pinned in soil.toml.
• The corpus test: a fresh lowering of a new small function, given the prelude as examples, produces Soil the user judges idiomatic without style corrections.
• examples/ and the real prelude agree wherever they overlap.

Decision points — resolved 2026-08-22

• Totality gap: signatures claim the intended row; the lock records checks.termination: "unverified" (mirroring refinement demotion — unproven, visible, tests still gate); soilc’s termination checker (plan 05) discharges the flags in bulk. Recorded in docs/lock-schema.md §4.
• Location: in this repo, as a prelude/ Soil root; extraction into its own forkable repo waits for a second user.
• Inventory: a concrete reviewed list before lowering begins (read_file + the §5 core types with ~6–12 functions each), then additions strictly by consumer need — the corpus stays curated.

Plan 05 — soilc: the compiler as the first Trellis project

References: docs/bootstrap-plan.md §3–4, design §3.1 (ANF), §3.4 (termination), §6.4 (demotion), §3.11 (Cranelift backend).

Goal

The Soil compiler written as a Trellis project — specs, agent lowerings, locks — running interpreted on soil0, differentially tested against it, and finally compiling itself to native code through Cranelift with a byte-identical fixed point. Refinement checking and termination checking enter the system here, as passes.

Scope

Passes in order; each is a Trellis module of pure functions with the AST as Trellis type definitions (the JSON schema from docs/soil0-cli.md is the conformance target — soilc’s AST types must round-trip it).

1. Lexer. Warm-up; oracle soil0 lex.
2. Parser. One definition with let rec … and … locals — the mutual-recursion-ban stress test, taken early on purpose. Oracle soil0 parse. If the ban genuinely fails here, that is a design finding to raise, not to code around.
3. Renamer. No-shadowing, ::, _private visibility. Canonical fresh-name allocation (deterministic counters, no iteration-order dependence) — this is where fixed-point determinism is won or lost.
4. Type + effect inference. The hardest lowering target in the whole plan; split the module aggressively (unify, generalize, rows, operator elaboration as separate definitions). Oracle soil0 infer.
5. Exhaustiveness + pattern compilation (to decision trees). Oracle soil0 check for the boolean verdicts; pattern compilation is new but testable by semantics (compiled and source matches agree — property tests through the interpreter).
6. ANF transformation. New; tested by properties (well-formedness of the output IR; evaluation equivalence via soil0 run on both forms).
7. Termination checker. New functionality: structural decrease + decreases measures. Tested by spec (accept/reject corpus). On completion, run over the prelude to discharge the interim div flags from plan 04.
8. Refinement checker. Desugars requires/ensures/inline refinements to SMT-LIB text (a pure function, golden-testable); Z3 runs behind a new Solver capability added to the prelude (the Py pattern: opaque type, fake for tests). Implements demotion (design §6.4) and arithmetic obligations (syntax spec §5). The daemon’s check_refinements stub goes live here.
9. CLIF backend. Pure pass ANF → CLIF text, plus a small Rust Cranelift driver crate in the workspace (CLIF in, object files out, links soil-rt, x86-64 + arm64). Golden CLIF tests plus execution equivalence: compiled output vs soil0 run on the test corpus.

Strangler integration: as each pass reaches accepted, the daemon swaps its soil0 counterpart for the Trellis pass (invoked via soil0 run while interpreted). soil0 passes are demoted to oracles, never deleted.

Self-hosting closure: interpreted soilc compiles the prelude and itself → soilc₁; soilc₁ compiles the same sources → soilc₂; the build fails unless soilc₁ ≡ soilc₂ byte-identical. Then the daemon uses soilc₁ for execution, keeping soil0 for differential runs.

Non-goals

Optimization (beyond what Cranelift gives), Perceus reuse analysis, FFI codegen (plan 06 extends the backend), JVM/C/direct-x86 backends, concurrent lowering.

Testing

• Per pass: differential against the soil0 CLI oracle over (a) the golden corpus from plan 02, (b) the prelude, (c) soilc’s own sources — the compiler is its own largest test input.
• Property tests per pass (round-trips, well-formedness, evaluation equivalence through the interpreter).
• Determinism harness: compile the corpus twice from clean state, byte-compare all outputs — run continuously from pass 3 onward, not discovered at stage 3.

Exit criteria

• All passes accepted; daemon runs with soilc passes strangled in.
• Prelude totality flags discharged by the termination checker; refinement demotion live end-to-end (a deliberately unprovable example demotes, is visible in the lock, and still runs its check).
• The fixed point holds: soilc₁ ≡ soilc₂.
• examples/csvstats/median.soil’s refinements actually prove.

Decision points — resolved 2026-08-22

• Solver surface: one-shot — solve : (s : Solver) -> (script : SmtScript) -> io SolveResult with SolveResult = Sat CounterModel | Unsat | Unknown { reason }. Each obligation is an independent script: trivially fakeable, cacheable by script hash. Incremental sessions only if solve time ever hurts.
• Decision trees are internal. The public schema covers surface AST and ANF; pattern-compilation output is free to change and is tested by semantic equivalence against soil0, not by goldens.
• Fixed-point scope: all emitted artifacts — per-definition CLIF text, object files, and the linked binary must be byte-identical, so nondeterminism is caught at the layer that caused it. Artifacts may contain no timestamps or logs by construction.

Plan 06 — FFI, trellis bind, and the minimal IDE

References: design §3.11 (backends and FFI), §5 (batteries), §7.1 (IDE), tr-grammar §3.5–3.6 (cram, contract tests via design §4.5).

Goal

Open the foreign world in the committed sequence — C ABI → Rust batteries → Python embedding → Python batteries — with hand-written (agent-written, per-symbol) bindings, the trellis bind assistant, and the thinnest IDE that makes the lowering loop pleasant.

Scope

FFI (sequenced; each step usable before the next)

1. C ABI codegen. The Cranelift backend learns extern calls against soil-rt’s C ABI; a worked shim example (a Rust extern "C" function wrapped as a Soil binding) joins the corpus.
2. soil-rs-std batteries. Refinement-typed Soil signatures over Rust-backed functions — runtime-owned values, so ordinary, refinable, capability-free when pure (design §3.11). Start from demand: what the compiler and prelude wished they had.
3. Python embedding. CPython via pyo3 inside soil-rt: GIL held around calls, PyObject* as opaque refcounted handles, py_to_soil / soil_to_py over the same JSON-shaped value model (one value model, never two), the Py capability + fake in the prelude. One worked pyo3 shim example joins the corpus.
4. soil-py-std batteries. Handle-in/handle-out style, ffi panic io rows, Py capability; the visible two flavours (cheap handles vs converting/refinable).
5. Binding trust plumbing. Contract tests auto-generated from signature + effect row (design §4.5: valid input → Ok, invalid → Err not panic, handle compatibility, leak-check loop, round-trip); lock ffi records (trust level, symbol hash, Nix store path — store path may be a plain path until the Nix milestone).

trellis bind <symbol>

6. Symbol metadata fetch (Python: .pyi/inspect/docstring; Rust: cargo doc JSON) into symbol.json + docstring.md; the binding context bundle (one shim corpus example included); the normal lowering loop producing .tr + shim + contract tests + lock entry for human review. No bulk importer — ever (design §3.11).

Minimal IDE

7. Electron-served web app over the daemon, as thin as possible: Markdown editor with test-block widgets (JSON drag-and-drop can start as guided JSON editing), lower button with streaming agent output, the question/answer panel (persisting answers to prose), graph view over the manifest (effect-flow coloring, soil-private greying), lock rendering as status badges (typed/tested/verified/accepted derived), REPL pane with REPL-to-expect-test promotion, accept/pin buttons with suggested git commits (never auto-commit).

Non-goals

py_module/Python-hosts-Soil, .pyi stub generation, Node, TOML→Nix (later milestone), whole-package binding generation (never), IDE polish.

Testing

• FFI: contract-test generator exercised against deliberately broken shims (each failure mode caught); leak checks under the debug runtime; py_to_soil/soil_to_py round-trip properties.
• trellis bind: end-to-end against a fixed known symbol set (e.g. json.dumps, re.compile, one Rust crate fn) with recorded metadata so tests don’t depend on the network.
• IDE: the golden path exercised in-browser against a fixture project — open, edit a test, lower, answer a question, accept — before calling any feature done.

Exit criteria

• Both shim kinds exist as accepted corpus examples; a Soil program calls one Rust and one Python function through real bindings with contract tests green.
• trellis bind requests.get (offline-recorded metadata) produces a reviewable binding end-to-end.
• The IDE golden path works against the real daemon; question round-trip and accept flow usable without touching the CLI.

Decision points — resolved 2026-08-22

• IDE delivery: browser first. The daemon grows an HTTP/WebSocket facade (trellis daemon --serve) and the web app is developed in a normal browser; Electron becomes a thin packaging wrapper later (design §7.1 unchanged — this sequences the wrapper last).
• IDE stack: Svelte + CodeMirror 6 (widget decorations for test blocks and the question panel); graph view via SVG or cytoscape.js.
• soil-rs-std starts with the Rust standard library only — a curated set drawn from std (math on floats, hashing, path/string utilities, whatever plans 04–05 wished for), no external crates initially. External crates (regex, chrono, …) arrive by demand through trellis bind, one symbol at a time.
• Contract-test generation lives in the daemon (Rust), next to the test runner it feeds; rewriting it in Trellis is possible dogfood later, not v1.

Plan 07 — the Python-glue project: the second Trellis project

References: design §11 step 6, §1.2–1.3 (users and the pitch), bootstrap plan §0 (the bias this milestone exists to correct).

Goal

Write a real program the author would otherwise have vibed in pure Python: Rust crates through soil-rs-std, a dozen Python functions through trellis bind, real work done in Soil. The compiler validated the pure core; this validates FFI, capabilities, bindings, and — the actual product question — whether writing .tr files and reading generated Soil is pleasant. This milestone’s deliverable is as much a verdict as a program.

Scope

1. Pick the program with the user. Criteria: genuinely wanted (not a demo), touches files/network/clock (exercises three capabilities), needs ~a dozen foreign symbols across 2–3 Python packages plus at least one Rust crate, small enough to finish (order of 30–60 definitions).
2. Work disciplined-tier by the book. Human-written .tr prose and tests, agent lowerings, accepted gates, export pins, no hand-edited Soil unless the escape is genuinely needed (and then noted). The point is to feel the friction a real user feels; do not use insider shortcuts.
3. Bind on demand. Every foreign symbol through trellis bind as encountered, never batched up front — this tests the assistant’s real cadence (design §3.11’s “a dozen bindings is a week of friction” claim, now measured).
4. Keep a friction log. A running document (not memory, not code): every point where the format, the tooling, the corpus, or the agent made the wrong thing easy or the right thing hard, with enough context to act on. This log is the primary input to the next round of design changes.
5. Ship it. The program builds via trellis build to a native binary, runs cram-tested against the real world, and gets used.

Non-goals

New toolchain features mid-flight (log them instead — resist fixing the tool from inside the project except for outright blockers); team features; trellis derive; performance work beyond what debug-mode flame graphs reveal for free.

Testing

The project’s own tests are the milestone’s tests: expect/property on pure logic, fake-capability tests on io, contract tests on every binding, cram on the entry point. CI policy line in soil.toml: every exported definition accepted.

Exit criteria

• The program works and is actually used by the author.
• Every binding came through trellis bind; every definition is accepted; the lock audit view shows exactly which trust levels and escape hatches exist.
• The friction log is reviewed with the user and triaged into design changes, tooling issues, and corpus fixes — closing the loop that the compiler-first ordering deliberately left open.

Decision points — resolved 2026-08-22

• The program is chosen at milestone kickoff, not now — the right project is whatever the author genuinely wants built when the tooling is real. The criteria in §1 are the filter; a stale pre-commitment would defeat the “genuinely wanted” requirement.
• Friction cadence: fix after shipping, except outright blockers. The project is a measurement of real-user friction; mid-flight fixes with insider knowledge would contaminate it. Log and work around during; review and triage (design changes / tooling issues / corpus fixes) after.

read_file

The prelude’s read_file, slated to be the first real definition: a .tr spec (prose, capability-style signature, fake-capability test, real-mode cram test), its .soil lowering, and its .lock entry. The canonical files live in examples/; these are included verbatim.

read_file.tr

---
name: read_file
---

# read_file

Reads an entire file into a UTF-8 string. Returns `Err` if the file does not
exist, cannot be read, or is not valid UTF-8. Never panics.

```soil-sig
read_file : (fs : Fs) -> (path : Path) -> io (Result Utf8 FsError)
```

```test found-and-missing
with fs = fake_fs {"config.toml": "port = 8080"}
(fs, "config.toml") => {"tag": "Ok", "value": "port = 8080"}
(fs, "missing.toml") => {"tag": "Err", "value": {"tag": "NotFound", "value": {"path": "missing.toml"}}}
```

One real-mode test against the actual filesystem:

```cram real-read
with file "config.toml" = "port = 8080"
$ trellis call read_file '"config.toml"'
{"tag": "Ok", "value": "port = 8080"}
```

read_file.soil

read_file : (fs : Fs) -> (path : Path) -> io (Result Utf8 FsError)
read_file fs path =
  match fs_read_bytes fs path with
  | Err e -> Err e
  | Ok bytes ->
    match utf8_decode bytes with
    | Ok text -> Ok text
    | Err _ -> Err (NotUtf8 { path = path })

read_file.lock

{
  "lock_format": 1,
  "name": "read_file",
  "kind": "function",
  "versions": { "trellis": "0.1", "soil": "0.1" },
  "spec": {
    "provenance": "human",
    "hashes": {
      "formal": "sha256:0be4d1c7",
      "test": "sha256:9a31e0f8",
      "prose": "sha256:5cc2071d"
    },
    "prose_state": "fresh",
    "blocks": [
      { "block": "soil-sig", "author": "human" },
      { "block": "test found-and-missing", "author": "human" },
      { "block": "cram real-read", "author": "human" }
    ],
    "pinned": true,
    "escape_hatches": []
  },
  "lowering": {
    "soil_hash": "sha256:ce8842a0",
    "provenance": "human-verified",
    "provider": "claude-code",
    "model": "claude-opus-4-7",
    "private_helpers": [],
    "calls": [
      { "name": "fs_read_bytes", "hash": "sha256:44f7b2e9" },
      { "name": "utf8_decode", "hash": "sha256:d10a93c5" }
    ]
  },
  "checks": {
    "types": "ok",
    "refinements": "none",
    "demoted": []
  },
  "tests": [
    { "name": "found-and-missing#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "found-and-missing#2", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "real-read#1", "tier": "cram", "mode": "real", "origin": "spec", "result": "pass" }
  ],
  "oracles": [],
  "accepted": true
}

csvstats

A hand-written module exercising the formats: a module header, two types (Row, ParseError), and three functions (parse_row, mean, median). Not every definition has every layer — median is the only one carried through all three (.tr → .soil → .lock); _module, row, and parse_row have .tr + .lock; parse_error and mean are spec-only. The canonical files live in examples/csvstats/; these are included verbatim.

_module (module header: .tr + .lock)

_module.tr

---
name: csvstats
---

# csvstats

Reads rows of decimal numbers from CSV lines and computes summary
statistics. The parsing functions own input validation; the statistics
functions assume validated `Row` values and stay total.

```exports
parse_row
median
mean
type Row
type ParseError
```

_module.lock

{
  "lock_format": 1,
  "name": "csvstats",
  "kind": "module",
  "versions": { "trellis": "0.1", "soil": "0.1" },
  "spec": {
    "provenance": "human",
    "hashes": {
      "formal": "sha256:1c9be044",
      "test": null,
      "prose": "sha256:73a0d5f2"
    },
    "prose_state": "fresh",
    "blocks": [
      { "block": "exports", "author": "human" }
    ],
    "pinned": false,
    "escape_hatches": []
  },
  "checks": {
    "exports": "ok"
  },
  "accepted": false
}

row (type: .tr + .lock)

row.tr

---
name: Row
---

# Row

One parsed CSV row. Construction goes through `parse_row` or row literals;
every row has at least one cell.

```soil-type
type Row = { cells : List F64 }
```

```invariant
non-empty: len(self.cells) > 0
```

row.lock

{
  "lock_format": 1,
  "name": "Row",
  "kind": "type",
  "versions": { "trellis": "0.1", "soil": "0.1" },
  "spec": {
    "provenance": "human",
    "hashes": {
      "formal": "sha256:4d7e02c9",
      "test": null,
      "prose": "sha256:88b1f6a3"
    },
    "prose_state": "fresh",
    "blocks": [
      { "block": "soil-type", "author": "human" },
      { "block": "invariant", "author": "human" }
    ],
    "pinned": false,
    "escape_hatches": []
  },
  "cycle_hash": null,
  "checks": {
    "types": "ok",
    "invariants": "proven",
    "demoted": []
  },
  "tests": [
    { "name": "invariant non-empty", "tier": "property", "mode": "sandboxed", "origin": "derived", "result": "pass" }
  ],
  "accepted": true
}

parse_error (type: .tr only)

parse_error.tr

---
name: ParseError
---

# ParseError

Why a CSV line failed to parse. `BadCell` carries the zero-based index of
the offending cell and its raw text.

```soil-type
type ParseError =
  | EmptyLine
  | BadCell { index : U64, text : Utf8 }
```

parse_row (function: .tr + .lock)

parse_row.tr

---
name: parse_row
tags: [parser]
---

# parse_row

Parses one CSV line of decimal numbers into a `Row`. Cells are separated by
commas; surrounding whitespace in a cell is ignored. An empty line, or any
cell that is not a decimal number, is an error.

```soil-sig
parse_row : (line : Utf8) -> Result Row ParseError
```

```test happy-path
("1.0,2.5,3.0") => {"tag": "Ok", "value": {"cells": [1.0, 2.5, 3.0]}}
("  4.0 , 5.0") => {"tag": "Ok", "value": {"cells": [4.0, 5.0]}}
```

```test errors
("") => {"tag": "Err", "value": {"tag": "EmptyLine"}}
("1.0,x,3.0") => {"tag": "Err", "value": {"tag": "BadCell", "value": {"index": 1, "text": "x"}}}
```

Scientific notation is a known gap, blocked on deciding the cell grammar:

```test scientific-notation xfail
("1e3") => {"tag": "Ok", "value": {"cells": [1000.0]}}
```

parse_row.lock

{
  "lock_format": 1,
  "name": "parse_row",
  "kind": "function",
  "versions": { "trellis": "0.1", "soil": "0.1" },
  "spec": {
    "provenance": "human",
    "hashes": {
      "formal": "sha256:b3e91c07",
      "test": "sha256:6a2f88d1",
      "prose": "sha256:12c4a9ee"
    },
    "prose_state": "fresh",
    "blocks": [
      { "block": "soil-sig", "author": "agent" },
      { "block": "test happy-path", "author": "human" },
      { "block": "test errors", "author": "human" },
      { "block": "test scientific-notation", "author": "human" }
    ],
    "pinned": false,
    "escape_hatches": []
  },
  "lowering": {
    "soil_hash": "sha256:f00d3c21",
    "provenance": "agent",
    "provider": "claude-code",
    "model": "claude-opus-4-7",
    "private_helpers": [
      { "name": "_parse_cell", "hash": "sha256:3fe210bb" }
    ],
    "calls": [
      { "name": "utf8_split", "hash": "sha256:91d0aa47" },
      { "name": "utf8_trim", "hash": "sha256:207cbe55" }
    ]
  },
  "checks": {
    "types": "ok",
    "refinements": "none",
    "demoted": []
  },
  "tests": [
    { "name": "happy-path#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "happy-path#2", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "errors#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "errors#2", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "scientific-notation#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "xfail" }
  ],
  "oracles": [],
  "accepted": false
}

mean (function: .tr only)

mean.tr

---
name: mean
---

The arithmetic mean of a non-empty list of floats.

```test simple
([1.0, 2.0, 3.0]) => 2.0
```

median (function: .tr + .soil + .lock)

median.tr

---
name: median
---

# median

Returns the median of a non-empty list of floats. For an even number of
elements, returns the mean of the two middle elements.

```soil-sig
median : (xs : List F64) -> F64
```

```requires
non-empty: len(xs) > 0
```

```ensures
lower bound: min(xs) <= result
upper bound: result <= max(xs)
```

The reference implementation wraps `statistics.median` from the Python
standard library.

```reference
ref/stats.py::median
```

```test odd-length
([1.0, 3.0, 2.0]) => 2.0
```

```test even-length
([1.0, 2.0, 3.0, 4.0]) => 2.5
```

```test single
([42.0]) => 42.0
```

```property order-independent
forall xs : List F64 where len(xs) > 0
median(xs) == median(reverse(xs))
```

median.soil

median : (xs : {v : List F64 | len v > 0}) -> {r : F64 | min xs <= r and r <= max xs}
median xs =
  let sorted = sort_by (fun x -> x) xs in
  let n = len sorted in
  let mid = n / 2 in
  if n % 2 == 1
  then nth sorted mid
  else (nth sorted (mid - 1) + nth sorted mid) / 2.0

median.lock

{
  "lock_format": 1,
  "name": "median",
  "kind": "function",
  "versions": { "trellis": "0.1", "soil": "0.1" },
  "spec": {
    "provenance": "human",
    "hashes": {
      "formal": "sha256:9f2c41aa",
      "test": "sha256:41aa73c0",
      "prose": "sha256:c8172d99"
    },
    "prose_state": "fresh",
    "blocks": [
      { "block": "soil-sig", "author": "human" },
      { "block": "requires", "author": "human" },
      { "block": "ensures", "author": "human" },
      { "block": "reference", "author": "human" },
      { "block": "test odd-length", "author": "human" },
      { "block": "test even-length", "author": "human" },
      { "block": "test single", "author": "human" },
      { "block": "property order-independent", "author": "human" }
    ],
    "pinned": true,
    "escape_hatches": []
  },
  "lowering": {
    "soil_hash": "sha256:77b04e12",
    "provenance": "agent",
    "provider": "claude-code",
    "model": "claude-opus-4-7",
    "private_helpers": [],
    "calls": [
      { "name": "sort_by", "hash": "sha256:aa90b1f3" },
      { "name": "len", "hash": "sha256:0d33c2e8" },
      { "name": "nth", "hash": "sha256:6b1e94d7" }
    ]
  },
  "checks": {
    "types": "ok",
    "refinements": "proven",
    "demoted": []
  },
  "tests": [
    { "name": "odd-length#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "even-length#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "single#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "order-independent", "tier": "property", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "ensures lower bound", "tier": "property", "mode": "sandboxed", "origin": "derived", "result": "pass" },
    { "name": "ensures upper bound", "tier": "property", "mode": "sandboxed", "origin": "derived", "result": "pass" },
    { "name": "differential ref/stats.py::median", "tier": "differential", "mode": "sandboxed", "origin": "derived", "result": "pass" }
  ],
  "oracles": [
    { "kind": "reference", "path": "ref/stats.py::median", "hash": "sha256:5e8f0b2a" }
  ],
  "accepted": true
}