Contracts

Contracts are portable runtime boundary checks, implemented as ordinary tricu functions in lib/base.tri. Additional structural predicates live in lib/intensionalContracts.tri (workspace alias intensional).

A contract checks an observed tree and returns a Result. Its success value may be transformed, so callers use the value returned by the check. Functions and contracts remain inspectable tree values.

1. The contract convention

A contract takes a value and a conventional remainder slot:

contract : Tree -> Tree -> Result Tree Tree

The library's Result constructors are:

ok value rest = pair true (pair value rest)
err msg rest = pair false (pair msg rest)
contractOk = (value : (rest : ok value rest))
contractErr = (msg : (rest : err msg rest))

Contract callers normally supply t as rest. Success contains the checked value, which may have been transformed; failure contains an arbitrary diagnostic tree, often a string. Library callers enforce this protocol by inspecting the returned Result. A user-written contract that returns another shape violates the protocol.

2. Checking and handling Results

2.1 Direct check

checkContract applies the contract without consulting the contract kernel:

checkContract = (contract value : contract value t)

For example, checkContract nat? 5 returns ok 5 t.

2.2 Kernel-mediated check

withContract also returns a Result. It takes two arguments:

withContract = (contract value :
  kernel contract value (contract value t))

The kernel receives the contract, original value, and check Result. The default kernel = defaultKernel preserves that Result. skipKernel preserves successes and replaces failures with ok originalValue rest.

These are ordinary library bindings. Apply a custom policy explicitly to a check Result; already-compiled trees retain their original bindings.

2.3 Continue or recover explicitly

Use bindResult to propagate failure and continue on success, or matchResult to select both handlers. matchResult takes the failure handler first:

checkedSum = (xs : bindResult (withContract (listOf nat?) xs)
  (checked _ : ok (sum checked) t))

fiveOrZero = (matchResult
  (msg _ : 0)
  (checked _ : checked)
  (withContract nat? 5))

checkedSum [1 2 3] returns ok 6 t; fiveOrZero is 5. The caller chooses how to handle a failed check.

The convenience function check contract value extracts either the checked value or the diagnostic from withContract. It discards the success/failure tag, so use the Result-returning APIs when that distinction matters.

3. Contract combinators

guardC message predicate turns a Boolean predicate into a contract:

positive? = guardC "expected positive integer" (n : gte? n 1)

Adapt Boolean predicates with guardC before passing them to checkContract or checkM. For example, even? returns a Boolean; evenC? from intensional returns a Result.

The current library includes:

Combinator	Behavior
andC c1 c2	Applies c2 to the value accepted/transformed by c1.
orC c1 c2	Uses c1's success, otherwise tries c2 on the original value.
notC c	Accepts the original value when c fails.
mapC f c	Applies f to the accepted value.
listOf c	Checks a proper list and returns its accepted/transformed elements in order, preserving higher-order proxies.
nonEmptyListOf c	Checks nonemptiness, then listOf c.
pairOf c1 c2	Checks both components and returns their accepted/transformed pair.

Examples of contracts include nat?, nonZero?, bool?, and anyC in base, and evenC? and sortedList? in intensional. Natural-number contracts use tricu's canonical compact-number encoding: bits must be exactly Leaf or Stem Leaf, and redundant high zero bits are rejected rather than normalized. This agrees with zero tests and native_math's input domain.

listOf and nonEmptyListOf reject improper tails with err "not a list" rest; the latter rejects an empty list with err "empty list" rest. pairOf rejects non-Forks with err "not a pair" rest. Element failures short-circuit without inspecting subsequent elements. Composition requires each supplied contract to obey the Result protocol.

List checking retains transformed values. In particular, listOf (fnContract argC resC) retains the checked proxies; callers still use each proxy's explicit Result/remainder calling protocol. Building a checked list incurs allocation even for anyC.

andC calls its second contract with the original remainder, orC retries the original value/remainder, and bindC supplies its continuation the checked value, original value and original remainder. Those delegated final Results are returned as supplied; wrapping combinators such as mapC and collection/proxy checks restore their caller's remainder. Custom contracts should preserve the conventional remainder unless the caller deliberately relies on a different protocol.

Structural contracts in intensional distinguish arbitrary trees from numbers: nonEmptyTree? accepts any non-Leaf, and fullTree? permits only Leaves/Forks. Parity, power-of-two, and ASCII checks first validate natural-number shape. sortedList? c checks/transforms elements with c, then checks natural-valued ascending order on that resulting list using exact successful comparisons. These checks require the demanded tree structure to terminate.

Arithmetic and decimal boundaries

base delegates numeric computation to the self-contained native_math binary engine. The annotated pred, add, sub, comparisons, mul, min, max and pow check canonical-natural inputs/results. Subtraction and predecessor saturate at zero; pow 0 0 is 1. succ, parity helpers, and underscore-suffixed raw comparison/predecessor bindings remain unchecked canonical-natural operations. Structural/compiler consumers use these raw bindings.

div, mod, and divMod require a positive divisor. Zero or malformed divisors produce err "non-zero" t; malformed dividends produce the natural-number error first. Successful divMod a b is the pair t quotient remainder, with a = quotient*b + remainder and 0 <= remainder < b. Use it instead of doing the same division twice. Annotations return plain success values and in-band failure Results, as elsewhere.

Raw native_math requires canonical-natural inputs from its caller. Its divMod a 0 convention returns (0,a) (quotient 0, remainder a). Euclidean division requires a positive divisor, which the checked facade enforces before calling the kernel. decimal value digit means 10*value + digit, with a caller precondition of 0 <= digit <= 9.

conversions.showNumber validates its natural input and emits canonical ASCII decimal: zero is "0", with no sign or leading zeros. Formatting divides once per output digit, and division scans bits rather than subtracting once per quotient unit. Exponentiation squares factors while scanning exponent bits; enormous powers still require enormous output and can exhaust resources.

4. Higher-order contracts

fnContract argC resC f rest returns a Result containing a proxy. The proxy takes an argument and its own remainder slot, then returns a Result. It checks the argument and result using withContract.

identityResult = (bindResult (fnContract nat? nat? (x : x) t)
  (proxy _ : proxy 7 t))

identityResult is ok 7 t. The proxy checks each observed call at its argument and result boundaries; the implementation of f remains opaque.

fn2 returns a curried proxy through the same Result protocol. Each stage must be unwrapped before applying the next argument:

additionResult = (bindResult (fn2 nat? nat? nat? add t)
  (first _ : bindResult (first 3 t)
    (second _ : second 5 t)))

additionResult is ok 8 t. Neither (fnContract nat? nat? f) x nor (fn2 nat? nat? nat? add) x y follows this protocol.

5. Interaction-tree contract effects

For catchable, composable failures, lift a check into the library's pure interaction-tree layer:

pureE value = pair 0 value
bindE action k = pair 1 (pair action k)
exceptE tag value k = pair 2 (pair tag (pair value k))
pureM = pureE
bindM = bindE

checkM contract value calls contract value t directly, bypassing the kernel. Success becomes pureE checked; failure becomes exceptE "contract" diagnostic (_ : pureE t). That failure continuation ignores its resumption argument: resuming this particular node does not replace the failed value. General exceptE computations can provide a continuation that uses a replacement.

handleM tag handler tree rewrites matching exceptions. The handler receives the diagnostic/value and original continuation; it can call that continuation or replace the action with a new tree. Other exception tags are left intact. liftM f x constructs pureE (f x).

evenContract = guardC "not even" even?
halfM n = (bindM (checkM evenContract n)
  (checked : pureM (div checked 2)))

recoveredHalf = (runM (handleM "contract"
  (msg k : pureM 0)
  (halfM 5)))

runM (halfM 8) returns ok 4 t; recoveredHalf returns ok 0 t.

runM interprets this pure pureE/bindE/exceptE representation and returns a Result. An unhandled exception becomes err value t, retaining its diagnostic value. This runner handles the pure effects protocol. See demos/contractEffects.tri for do bindM, handler replacement and resumption examples.

6. Source annotations

.tri annotations are frontend sugar for inserting calls to withContract and handling their Results. Contract expressions are ordinary source expressions.

idNat x@nat? =@nat? x
sumChecked xs@(listOf nat?) =@nat? sum xs
addChecked @nat? @nat? =@nat? add

• x@contract checks an argument before entering the body.
• =@contract checks the returned value.
• A successful annotated call returns the accepted plain value. Failure returns err diagnostic t.
• Checks are inserted only for explicitly annotated arguments/results.
• Phantom annotations supply contracts without term binders, wrapping a local raw implementation. Mixing phantom and named binders is unsupported.
• Compound annotations containing application must be parenthesized.

For example, idNat 5 is 5; idNat "bad" is err "not a natural number" t. In a curried definition, an argument failure before the final binder produces an absorbing function for the next argument before returning the failure Result.

Annotation lowering belongs to the portable source compiler in lib/source/program.tri. The accepted profile is described in the source profile.

7. Modules and content-addressed storage

A contract can be exported and stored as an ordinary tree. Source annotations travel with compiled definitions because their guard code is part of the executable. Importing the tree preserves those checks. Consumers invoke separately exported contracts explicitly.

The module manifest records names, object kinds, hashes, and ABIs. Content verification authenticates the stored checking code; whether a program invokes that code follows its implementation. See Modules and Storage for publication and identity.

8. Handling failures

Failures are values. Inspect or propagate the Result, or use the interaction-tree layer for catchable failures. Higher-order proxies check observed calls and change the calling protocol. Arbitrary supplied contracts must themselves follow the Result convention. Runtime checks complement tests and execution budgets.

9. A registry boundary in use

lib/arboricx/server.tri exports bundleHashC: exactly 64 lowercase ASCII hexadecimal characters, preserving the checked value and remainder. Its predicate rejects malformed list/numeral trees as well as malformed strings. It examines at most 64 characters and one final list constructor, leaving an oversized suffix opaque. This validates the spelling of a path component.

handler_artifacts.loadFrom applies the contract before issuing a storage request. Its filesystem adapter also checks raw requests before constructing paths. Rejected digests return err ["invalid-digest" message] t; the HTTP consumer maps this to status 400 and other load failures to a redacted 404. Successful loads authenticate the bytes against the requested SHA-256 name.

Publication validates canonical octets, computes the digest, stages the bytes, and verifies/synchronizes immutable winners before acknowledging success. Existing corrupt winners remain intact for diagnosis. Stored bytes are opaque; applications supply executable-bundle validation when required. Roots are trusted configuration and path access follows OS process authority.

Independent handler and storage tests check zero requested reads for invalid digests, canonical character/numeral shapes, oversized suffix laziness, accepted-value/remainder preservation, byte authentication, corrupt winners, publication races and ordinary failures. See handler validation and the IO storage controls.

10. Scoped request handlers

The native workspace modules handlers, handler_log, handler_artifacts, and handler_testing provide request/response services. They implement a source-owned interaction-tree protocol, with explicit bridges to host IO. Browser use requires publication of the selected source cohort.

Checked continuations

H.checkWith contract value rejected malformed next applies checkContract once and selects a continuation:

Contract reply	Continuation argument
ok checked t	next checked
err diagnostic remainder	rejected diagnostic
Any other shape	malformed value, using the original value

The selected continuation determines the returned computation or value. The checked value can be a transformation or higher-order proxy. Rejection preserves existing callers' treatment of the diagnostic independently of its remainder. Unselected continuations and unused payloads remain lazy.

H.checkRequest service operation contract argument next supplies the standard request policy: rejection produces invalid-request, and a malformed contract reply produces invalid-request-contract. Both carry the service and operation; interpretation supplies the surrounding diagnostic labels. Logging's sink adapter uses this helper to pass the checked event directly to its sink.

H.checkedRequest service operation inputC outputC argument checks the argument, issues the request with the checked value, then checks the delivered reply in its continuation. Reply failures use invalid-response and invalid-response-contract. Successful service Results remain ordinary values inside the handler computation.

Artifact loading uses checkWith to select its domain-specific policy: rejected digests produce an ordinary invalid-digest Result, while malformed contract replies produce a handler failure. Artifact publishing retains its own diagnostic categories. These helpers share checking and continuation selection while keeping those policies explicit at each boundary.

Application code and composition

!import handlers as H
!import handler_log as Log
!export main

application = do H.bind
  Log.info "starting"
  Log.info "finished"
  H.pure 42

main = Log.withContext [["request" 7]] application
  |> Log.capture
  |> H.runPure

The result is ok [42 events] t, with two events. A log event is [level contextFields payload]: fields and payload are trees, with formatting chosen by the sink. withContext prepends outer context fields, preserving order and duplicate keys. It checks that its fields form a proper list. Log.info and Log.warn are conveniences over Log.emit level payload.

Log.withSink sink computation installs a function receiving the event and returning a handler computation whose value is an ordinary Result: ok t t or err diagnostic t. Log.discard installs a successful no-op sink. Log operations return those Results for applications to inspect or deliberately ignore.

Log.capture computation is a composable boundary transformer returning [value events] on normal completion, including when value is an ordinary failure Result. It forwards other operations to outer handlers. A terminal interpreter failure propagates, discarding the accumulated events. Persist events through a sink when they must survive a failed computation. Capture belongs outside context decoration if it should observe the decorated events. An inner sink consumes requests before an outer capture can see them, and an inner capture similarly hides events from an outer sink or capture.

See the runnable logging example and the artifact GET consumer.

Requests, scopes, and forwarding

H.request service operation argument constructs a request. Names are ordinary trees; use readable service/operation strings for diagnostics. H.handle service handler computation installs a handler whose callback receives operation and argument and returns a computation yielding one reply.

The nearest matching service handler owns the request. Its own computation runs in the environment outside its installation scope, excluding itself and any intervening inner handlers. The caller resumes in its original environment. H.forward service operation argument is an explicit spelling of another request from that outer environment. Outside a handler callback, forward uses the current request environment. Forward unknown operations to outer handlers.

This permits contextual overrides and stable service identity together. Wrapping a callback's body in its original service handler pins that service while leaving other services contextual. Merely returning a function or inert action from a scope leaves it to use the environment at its eventual execution. Handler order is significant: changing wrapper order can change routing. If service-handler work should inherit a logging context, install that context outside the service handler.

H.label name computation adds an execution label for diagnostics. Labels are outer-to-inner and are restored on scope exit. Handler-generated work retains the request's execution labels even though its service environment is the handler's outer environment. Labels supply diagnostic context.

Results, contracts, and execution

H.checkedRequest service operation inputContract outputContract argument checks the argument before requesting and the reply before returning. Checks use checkContract directly; transformed success values are retained. Successful contracts must return an empty remainder. Rejected or malformed contracts terminate with a named protocol diagnostic.

H.runPure computation returns an execution Result. ok value t says that interpretation completed. A service can return err message t as its ordinary value; the outer result is then ok (err message t) t. Unhandled requests, invalid protocol responses, and H.fail kind service operation detail terminate with:

err [kind service operation detail labels] t

A missing handler uses kind "unhandled-request". An invalid response uses "invalid-response". fail terminates the computation with its diagnostic.

H.liftIO hostAction requests the named "host.io" / "run" bridge. runPure rejects it like any other unhandled request. H.runIO computation is an alias for H.runIO: it returns a host IO action yielding the successful computation value. Handler failures become terminal v2 failures. Wrap the action with IO.io at an executable entrypoint. Install handlers for other named services. The host enforces resource ownership under OS process authority.

H.scope body and H.spawn supervised keep handles body preserve the lexical handler environment and labels in their callbacks. Each callback starts with an empty continuation stack. Their execution uses the host scope/task lifecycle; pure interpretation reports an invalid view for these boundaries.

Artifact storage

Artifacts.load digest and Artifacts.publish bytes address the default "artifacts" service. loadFrom service digest and publishTo service bytes select explicit roles, useful for source/destination stores.

Artifacts.withFilesystem root limit computation installs the default service; withFilesystemFor service root limit computation installs a named one. The byte limit applies to storage operations. Paths and publication use the artifact store's hash/shard layout, staging and authenticated winner checks. Artifacts.prepareFilesystem root prepares and synchronizes the directory layout at application startup and returns an ordinary Result. Run it explicitly before serving requests; path access follows OS process authority.

Loads return ok bytes t or err diagnostic t. Invalid digests return err ["invalid-digest" message] t before requesting storage. The filesystem adapter rechecks raw load requests before constructing paths. Publication checks canonical octets and returns ok digest t or an ordinary failure Result. Replies are checked, including byte-list contents and canonical digest spelling. These checks traverse their data, with costs depending on the demanded contents.

Domain Results use an empty remainder. HTTP mapping belongs to the consumer. The example GET consumer maps invalid digests to 400 and other load failures to a redacted 404, records a completion event, and explicitly treats logger failure as an application error. The default source registry composes these adapters. Publication stores opaque bytes; callers validate executable-bundle formats when required. A later failure can leave a published object visible.

Scripted services and low-level interpretation

Test.expect service operation argument reply constructs one script row. Test.run script computation interprets residual requests using exact matching and returns [executionResult chronologicalTrace unusedScript]. The trace includes attempted requests that exhaust or mismatch the script. Unused rows on successful completion are an error. Early failures retain their trace and unused rows. Reply contracts run after each scripted reply, preserving the service's response checks.

H.view computation exposes the normalized prefix for alternative interpreters: (100, value), (103, completeDiagnostic), or (106, [event labels replyContinuation]), where event is [service operation argument]. The continuation returns another normalized view. Scope and spawn views additionally use (107, [labels body next]) and (108, [supervised keep handles labels body next]). Bodies and continuations remain opaque until explicitly applied. H.collect service operation argumentContract reply computation is the lower- level boundary transformer used by log capture. It validates and collects matching arguments, replies with the supplied value, and relays other requests outward. Install collection inside each scoped or child body; crossing those boundaries produces a state-boundary diagnostic.

The implementation uses linear handler lookup and a two-stage interpreter. Service names and closures are inspectable routing values. Host authority and resource lifetimes come from the IO runtime; applications choose retry and persistence policies. Explicit value-based services remain useful where stable identity is the primary requirement.

Run the independent source and filesystem checks described in Testing.