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. This is a programming convention, not a host-enforced type: 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. A failed check does not inherently abort the host or raise an interaction-tree exception.

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)

Do not pass a Boolean predicate directly 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, not a host integer type: 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. Well-formed supplied contracts are still required; these helpers cannot make an arbitrary contract 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.

Remainders are not parser state threaded between checks: 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; it does not treat comparison failures as truthy success. These are finite-tree checks, not termination guarantees.

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; not host exceptions.

Raw native_math does not validate inputs. Its divMod a 0 is explicitly the degenerate pair (0,a) (quotient 0, remainder a), not valid Euclidean division; the checked facade rejects that case before calling it. Do not use the raw kernel's total zero convention as a boundary check. 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. Constructing the proxy does not prove anything about unobserved calls or the internals of f.

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; its tag and continuation are not retained in that Result. It is not a general IO interpreter and does not return residual host effects. 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, not names in a separate type language.

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, not an outer ok. Failure returns err diagnostic t.
• Unannotated binders and a missing result annotation add no check. They do not insert an implicit anyC application.
• 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; there is no Haskell source desugarer. 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; an oversized suffix is not traversed. This validates a path component, not the integrity or format of the stored bundle, and does not replace filesystem permissions.

getBundleByHash applies checkContract before constructing its file-read action. It explicitly translates contract failures into the HTTP convention: err 400 diagnostic, rather than propagating a contract remainder as an HTTP message. Read failures remain err 404 message; success is ok bytes t. serveBundleHash handles those statuses, so both download routes share the same guard. Direct callers of getBundleByHash also receive the guard.

The host/unit tests record requested effects with a small interpreter: rejected identifiers must request zero reads, not merely return an error after a failed read. They also check byte membership, malformed trees, oversized suffix non-evaluation, accepted-value/remainder preservation, missing objects, and unchanged health/landing routes. This is a boundary convention, not a private capability: code can still deliberately call readFile or path helpers itself.

putBundle computes the digest itself, checks the same hash contract before filesystem IO, then publishes with atomicWriteBytes. There is no public unchecked hash-taking writer. It preserves the existing replace-on-upload policy; the hash contract does not validate bundle contents or supply general symlink containment. Root is trusted configuration, and host permissions remain necessary.

See registry pipeline validation for current artifact checks and their limits.