James/tricu
1
1
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Begin removing view related code and docs

Browse Source
This commit is contained in:
James Eversole
2026-08-31 15:24:19 -05:00
parent c6e4a43178
commit d9a69513d7
59 changed files with 1739 additions and 7700 deletions
Download Patch File Download Diff File Expand all files Collapse all files

147
docs/content-store-and-module-format.md
View File

@@ -17,7 +17,7 @@ This document specifies the first target shape for:
- indexed Arboricx bundle import/export as transport;
- module manifests as immutable export maps;
- workspace aliases as mutable human-facing references;
- View Contract artifact attachment to module exports.
- Contract artifact attachment to module exports.
It does not specify:
@@ -37,7 +37,7 @@ Arboricx tooling, or future frontends. The store core only knows object bytes,
object kinds, hashes, aliases, and optionally structural references for known
portable formats.
View Contracts may be first-class artifact references because they are portable
Contracts may be first-class artifact references because they are portable
Tree Calculus data checked by pure Tree Calculus code. They are not
Haskell-private semantics.
@@ -280,7 +280,7 @@ It exists to support:
- reproducible import resolution;
- executable export discovery;
- View Contract lookup for imported symbols;
- Contract lookup for imported symbols;
- module-to-module reference tracking;
- transport/store interop.
@@ -301,12 +301,9 @@ moduleManifestV1:
kind: <object kind>
hash: <object hash>
abi: <abi identifier>
view: optional
kind: <view artifact kind>
hash: <view artifact hash>
catalog: optional
kind: <view catalog kind>
hash: <view catalog hash>
contract: optional
kind: arboricx.tree-term.v1
hash: <contract term hash>
metadata: optional human-facing fields
```
@@ -343,7 +340,7 @@ object:
abi: arboricx.abi.tree.v1
```
Export with View Contract:
Export with Contract:
```text
name: "map"
@@ -351,15 +348,15 @@ object:
kind: arboricx.tree-term.v1
hash: <whole-term hash>
abi: arboricx.abi.tree.v1
view:
kind: arboricx.view-contract.type.v1
hash: <view type hash>
contract:
kind: arboricx.tree-term.v1
hash: <contract term hash>
```
The manifest preserves the pairing between exported executable and exported
contract. For workspace modules built from local source, annotated exports are
checked before the manifest is published; only exports that pass producer-side
View Contract checking receive direct `arboricx.view-contract.type.v1` refs.
checking receive direct contract term refs.
### 8.6 Metadata
@@ -375,112 +372,68 @@ createdBy
Metadata is not source provenance and is not required for execution or checking.
## 9. View Contract Artifacts
## 9. Contract Artifacts
View Contract artifacts are portable Arboricx-layer data. They may be stored
as content objects and referenced by module exports. `tricu` may emit these
objects, but the object kind is not tricu-specific.
Contracts are ordinary `tricu` functions `Tree -> Result Tree Tree`. They are
stored and referenced as ordinary `arboricx.tree-term.v1` objects. There is no
separate contract object kind.
Current artifact kind:
```text
arboricx.view-contract.type.v1
```
`arboricx.view-contract.type.v1` is the direct export-view artifact. Its
payload is a canonical prefix binary encoding of the syntactic ViewType:
```text
Name = 0x00 u32be(byte-length) utf8-name
Ref = 0x01 u32be(byte-length) utf8-ref
List = 0x02 ViewType
Maybe = 0x03 ViewType
Pair = 0x04 ViewType ViewType
Result = 0x05 ViewType ViewType
Fn = 0x06 u32be(argument-count) ViewType* ViewType
```
`utf8-ref` is tagged text:
```text
i:<decimal-integer> numeric/legacy ref
s:<text> symbolic user ref
```
Symbolic refs are the preferred user-authored form; numeric refs remain useful
for generated code, fixtures, and old low-level examples.
The object hash domain is the object kind:
```text
arboricx.view-contract.type.v1 \0 <payload>
```
A contract object is a complete Tree Calculus term. Any implementation that can
evaluate Tree Calculus terms can apply it. The contract standard defines only the
result convention and the boundary helpers; it does not define a binary contract
grammar.
### 9.1 Export-level pairing
The module manifest is the canonical pairing of an executable export and its
advertised contract:
The module manifest pairs each export with an optional contract object:
```text
export name -> tree-term hash + optional view artifact hash
name: "map"
object:
kind: arboricx.tree-term.v1
hash: <whole-term hash>
abi: arboricx.abi.tree.v1
contract:
kind: arboricx.tree-term.v1
hash: <contract term hash>
```
This avoids drift such as:
```text
map -> tree A
map.view -> contract B
```
where aliases might be retargeted independently.
This prevents the executable and its advertised contract from drifting apart.
### 9.2 Import checking
When a source file imports a module, a frontend can resolve an imported export,
decode its direct `arboricx.view-contract.type.v1` ref, and emit typed program
evidence locally:
When a source file imports a contracted export, the frontend loads the contract
object and applies it at the boundary using the standard contract helpers. For
example:
```text
imported List.map has view Fn [...]
imported List.map has contract <tree-term hash>
```
For locally built workspace modules this is backed by producer-side checking
before the module manifest alias is published, including imported view facts from
dependencies used by the producer source. External or prebuilt manifests are
trusted boundary declarations for now; they are not accompanied by proof objects.
The checker still consumes only local numeric symbols and typed-program evidence.
Global content hashes do not become checker symbols.
For locally built workspace modules, advertised export contracts may be checked
before the manifest is published. For external or prebuilt manifests, the
advertised contract is a trusted boundary declaration; the consumer may insert
guard wrappers as needed.
Correct split:
The contract term itself is the authority. There is no separate checker binary
format and no typed-program evidence graph.
```text
local checker symbol: 3
presentation label: "List.map"
resolved object: sha256:...
exported view: Fn [...]
```
### 9.3 Execution hydration versus contract checking
### 9.3 Execution hydration versus contract evidence
Execution imports should use a narrow, demand-driven path:
Execution imports use a narrow path:
```text
module import -> selected executable exports -> hydrate selected tree-term objects
```
This path should not compute a dependency closure over other module exports.
Each selected executable export is already a complete Tree Calculus value.
Contract-aware checking may use a broader path:
Contract-aware imports use a slightly broader path:
```text
module import -> selected exports -> exported view type refs -> typed-program evidence
module import -> selected exports -> exported contract term refs -> apply at boundary
```
That path emits portable evidence and leaves compatibility policy decisions to
the Tree Calculus checker. typed programs and reusable catalogs do not need their
own binary object kinds today: they are ordinary Tree Calculus data and can be
stored as `arboricx.tree-term.v1` when persistence is useful.
Because contract objects are ordinary tree terms, they can be reused, composed,
and stored with the same tools as any other value.
## 10. Workspace Aliases
@@ -528,7 +481,7 @@ This design intentionally preserves existing conventions where they already fit:
- three-character object sharding from `lib/arboricx/server.tri`;
- indexed Arboricx bundles as compact transport objects;
- optional human-facing export names in manifests;
- View Contract checker evidence as portable Tree Calculus data.
- Contract terms as portable Tree Calculus data.
It replaces or demotes conventions that do not fit:
@@ -550,7 +503,7 @@ A staged implementation can proceed as follows:
7. Store/load module manifests as content-addressed objects.
8. Add workspace alias read/write helpers.
9. Teach import resolution to target module manifests/exports.
10. Attach exported View Contract artifacts to module exports.
10. Attach exported contract terms to module exports.
11. Gradually migrate existing `!import` users.
## 13. Deferred Decisions
@@ -584,13 +537,13 @@ Transport:
indexed .arboricx bundles, packable from and unpackable to CAS roots
Modules:
immutable manifests pairing export names with object refs and optional View
Contract refs
immutable manifests pairing export names with object refs and optional
contract term refs
Workspace:
mutable aliases from human names to immutable content hashes
```
This keeps the store portable, preserves Arboricx's compact transport role,
restores Merkle DAGs as the persistence model, and gives View Contracts a stable
restores Merkle DAGs as the persistence model, and gives contracts a stable
module/export attachment point without making the store `tricu`-specific.

326
docs/contracts.md Normal file
View File

@@ -0,0 +1,326 @@
# Contracts
Contracts are the portable runtime boundary-checking layer for `tricu`. A
contract is an ordinary `tricu` function that inspects a value and returns a
standard `Result`.
Contracts are not a type system. Tree Calculus is intensional: every value is a
tree and can be inspected by any function. A contract can only observe a value
and fail when it does not satisfy the advertised predicate. It cannot hide a
value's representation or prove that an opaque function behaves correctly for
all inputs.
Static typing for Tree Calculus is an area of active research. This document
describes the dynamic-contract layer that exists today and the guarantees it
can honestly claim.
## 1. The contract type
A contract is a function:
```tri
contract : Tree -> Tree -> Result Tree Tree
```
The second argument is the conventional `rest` slot. It takes a value and a rest
and returns one of the standard `Result` shapes from `lib/base.tri`:
```tri
ok value rest = pair true (pair value rest)
err msg rest = pair false (pair msg rest)
```
In contract contexts the `rest` slot is conventionally `t`. Two helpers make
this explicit:
```tri
contractOk = (value : (rest : ok value rest))
contractErr = (msg : (rest : err msg rest))
```
- On success, a contract returns the checked value. This may be the original
value or a transformed/normalized value.
- On failure, it returns a reason. The reason is an arbitrary tree, often a
string or a structured diagnostic.
Because a contract is just a tree-valued function, any Tree Calculus
implementation can apply it. No special contract object format is required.
## 2. Core boundary wrappers
### 2.1 Explicit check
`checkContract` applies a contract with the conventional `t` rest slot and
returns the raw `Result`:
```tri
checkContract = (contract value : contract value t)
```
This is the most flexible form. The caller decides what to do with failure.
### 2.2 Direct boundary abort
`withContract` applies a contract with the conventional `t` rest slot and
continues on success, or calls a failure continuation on failure:
```tri
withContract = (contract value onOk onFail :
matchResult
(msg _ : onFail msg)
(checked _ : onOk checked)
(contract value t))
```
The failure continuation is supplied by the host or by the surrounding program.
It may abort, log, return a default, or raise an effect. The core contract
standard does not prescribe the failure behavior.
### 2.3 Example: a simple contract
```tri
isZero? = n :
equal? n 0
nat? = guardC "not a natural number" (n : gte? n 0)
-- explicit check
result = checkContract nat? 5
-- boundary abort
five = withContract nat? 5 (x : x) (msg : 0)
```
Real contract predicates are usually more interesting than `isZero?`; this
illustrates only the shape.
## 3. Contract combinators
Contracts compose using ordinary `tricu` functions. A few common patterns:
```tri
andC = (c1 c2 value rest :
matchResult
(msg _ : contractErr msg rest)
(v _ : c2 v rest)
(c1 value rest))
mapC = (f c value rest :
matchResult
(msg _ : contractErr msg rest)
(v _ : contractOk (f v) rest)
(c value rest))
listOf = (c xs rest : ...) -- checks spine and element contract
pairOf = (c1 c2 p rest : ...)
```
These are library code, not core standard. A contract library can provide
`listOf`, `pairOf`, `fnContract`, and similar helpers.
## 4. Higher-order contracts
A contract for a function value returns a wrapped proxy. The proxy itself is a
contract: it checks arguments on the way in and results on the way out.
```tri
fnContract = (argC resC f rest :
contractOk
(x : (rest1 :
withContract argC x
(x' :
withContract resC (f x')
(y : contractOk y rest1)
(msg : contractErr msg rest1))
(msg : contractErr msg rest1)))
rest)
```
This does not prove that `f` is well-behaved internally; it only catches
violations at observed calls.
## 5. Interaction-tree contract effects
The core contract layer returns `Result`. For code that wants catchable,
composable contract failures without threading `Result` through every function,
contracts can be lifted into an interaction tree.
### 5.1 Interaction-tree constructors
These reuse the same `pure`/`bind` tags already used for `tricu` IO:
```tri
pureE value = pair 0 value
bindE action k = pair 1 (pair action k)
exceptE tag value k = pair 2 (pair tag (pair value k))
```
`exceptE` is resumable: `k` is the continuation. A handler may resume with
`k replacement` or abort by ignoring `k`. Contract failures usually abort; the
resumable shape is provided for generality and for richer effect handlers.
### 5.2 Lifting a contract
```tri
checkM contract value =
matchResult
(msg _ : exceptE "contract" msg (\_ : pureE t))
(checked _ : pureE checked)
(contract value t)
```
`pureM` and `bindM` are aliases for `pureE` and `bindE`:
```tri
pureM = pureE
bindM = bindE
```
### 5.3 Lifting pure functions
```tri
liftM f = (x : pureE (f x))
```
### 5.4 Example
```tri
halfM n =
bindM (checkM even? n)
(\n' : pureM (div n' 2))
use =
handleM "contract"
(\msg k : pureM 0)
(halfM 5)
```
`handleM` is a pure tree-to-tree function that interprets `exceptE` nodes,
either resuming with a replacement value or returning a failure tree.
### 5.5 Running a pure interaction tree
```tri
runM tree =
-- interprets pureE, bindE, and exceptE nodes
-- returns a Result or a residual effect tree
...
```
If the tree contains no IO or other host effects, `runM` can be written
entirely in `tricu`.
## 6. Source syntax
Source annotations are frontend sugar for inserting contract boundaries. They do
not change the runtime semantics of ordinary code; they tell the frontend where
to emit contract checks.
### 6.1 Argument and result assertions
```tri
idNat x@Nat =@Nat x
```
`x@Nat` inserts a `Nat` contract check on the argument. `=@Nat` inserts a check
on the result.
### 6.2 Compound contracts
```tri
sum xs@(List Nat) =@Nat ...
useHandler f@(Fn [(NonEmptyList String)] String) =@String ...
```
Compound annotations must be parenthesized when they contain application.
### 6.3 Phantom arguments
```tri
map @A @B =@(Fn [(Fn [A] B) (List A)] (List B)) ...
```
A phantom argument contributes a contract to the function boundary without
introducing a term binder.
### 6.4 Missing annotations
Unannotated binders in a contract-bearing head default to `Any`. A missing
return annotation defaults to `Any`.
```tri
foo x y@Bool = body -- foo : Fn [Any Bool] Any, y : Bool
```
### 6.5 Export contracts
A module export may advertise a contract:
```tri
!export factorial : Fn [Nat] Nat
```
The advertised contract travels with the export in the module manifest.
## 7. Module and content-store integration
Contracts attach to module exports as ordinary content-addressed tree terms.
There is no special contract object kind. The manifest references the contract
with the same object kind as any other tree term:
```text
name: "factorial"
object:
kind: arboricx.tree-term.v1
hash: <tree-term hash>
contract:
kind: arboricx.tree-term.v1
hash: <contract term hash>
```
The earlier `arboricx.view-contract.type.v1` object kind is removed. A
contract is just a tree term.
For locally built modules, advertised export contracts may be checked before the
manifest is published. For imported modules, the advertised contract is a
boundary assumption. The local checker may insert guard wrappers when a
contracted import is used.
See `docs/module-system-design.md` and
`docs/content-store-and-module-format.md` for the full store, manifest, and
bundle conventions.
## 8. Guarantees
The contract layer honestly claims only:
1. A contract applied to a value returns a standard `Result` shape.
2. `withContract` and `checkM` invoke the contract at the represented boundary.
3. A failed contract invokes the supplied failure continuation or `exceptE`
node.
4. Content-addressed references prevent an attached contract from silently
drifting to a different stored object.
5. Provenance labels record where a contract assertion came from.
Only the contract function itself observes the runtime value. The rest is
metadata plumbing.
## 9. Limitations
- Contracts do not establish parametricity or representation independence.
- They do not prove that opaque recursive or primitive code satisfies its
contract for every input.
- They do not remove the need for tests, careful API design, or future static
analysis.
- Higher-order contract wrapping has the usual costs and proxy-like behavior
of dynamic contract systems.
## 10. Summary
- A contract is an ordinary `tricu` function: `Tree -> Result Tree Tree`.
- `withContract` aborts at a boundary; `checkContract` returns the raw
`Result`.
- The interaction-tree layer (`checkM`, `bindM`, `handleM`) adds catchable,
composable failures on top of the same core contracts.
- Contracts attach to module exports as ordinary tree-term objects.
- Provenance labels record source and blame, but do not prove truth.

371
docs/guard-injection.md
View File

@@ -1,371 +0,0 @@
# Guard Injection Semantics
This document describes the runtime guard model for View Contracts.
Views describe portable structural contracts. Guarded views refine those
contracts with executable predicates while keeping ordinary value-level code free
of `Maybe`, `Result`, sentinel, or host-language abort handling.
```tri
viewGuarded baseView guard
```
A guarded view means: when this guarded view is observed along the reachable
checked-execution path, run `guard` against the runtime value.
## Goals
- Preserve ordinary value-level program shapes.
- Keep guard failure out of user code.
- Avoid Haskell-specific checker/runtime semantics.
- Represent guard boundaries explicitly in portable tree data.
- Make successful guarded execution transparent: guarded values are unwrapped
before ordinary code receives them.
- Prefer correctness-by-default over avoiding repeated predicate cost.
## Non-goals
- Preventing user-written guards from diverging.
- Letting guards author their own diagnostics.
- Solving IO interaction-tree composition.
- Finalizing long-term artifact identity policy.
- Deduplicating or hoisting repeated guard checks.
## Plain Views vs Guards
Plain Views still provide concrete benefits without guards:
- structural flow checking;
- portable API metadata;
- module/export contract metadata;
- content-store view-tree metadata;
- cross-frontend agreement on contract structure;
- diagnostics for wrong-view flows.
Guards are for invariants that require runtime value inspection, such as:
- non-empty list;
- sorted list;
- byte string of exactly 32 bytes;
- protocol payload with a valid checksum;
- domain-specific runtime predicate.
Guards are deliberately more expensive than ordinary Views. Use them when the
runtime contract must be enforced.
## Guard Result Protocol
Guards return one of two standardized shapes:
```tri
guardOk value
guardFail
```
Guards do not provide diagnostics. The checked-exec runner owns diagnostics.
Malformed guard output is treated as a checked-runtime failure.
## Checked Execution Protocol
A successful typed-program check returns a checked-execution artifact, not a raw
payload.
Current constructors:
```tri
checkedPure value
checkedFail diagnostic
checkedGuard view guard value continuation
checkedGuardWithContext context view guard value continuation
checkedBind exec continuation
```
`checkedGuard` is the compatibility/default constructor. It lowers to
`checkedGuardWithContext` with an unknown context. Checker-injected guard
boundaries use `checkedGuardWithContext` so failures can identify where the
boundary came from.
Runner:
```tri
runChecked checkedExec
```
Semantics:
```text
runChecked (checkedPure value)
= checkedRuntimeOk value
runChecked (checkedFail diagnostic)
= checkedRuntimeFail diagnostic
runChecked (checkedGuardWithContext context view guard value continuation)
= case guard value of
guardOk checkedValue -> runChecked (continuation checkedValue)
guardFail -> checkedRuntimeFail (guardFailed context view)
malformed -> checkedRuntimeFail (malformedGuardResult context view malformed)
runChecked (checkedGuard view guard value continuation)
= runChecked (checkedGuardWithContext unknownContext view guard value continuation)
runChecked (checkedBind exec continuation)
= case runChecked exec of
checkedRuntimeOk value -> runChecked (continuation value)
checkedRuntimeFail diag -> checkedRuntimeFail diag
```
Important invariant:
> Guard failure is consumed by `runChecked`. It is never passed into ordinary
> user code.
## Checker Result Shape
`checkTypedProgramWith` returns checked-exec on success:
```tri
ok checkedExec env
```
Even unguarded programs return:
```tri
checkedPure rootPayload
```
Compatibility helper:
```tri
checkedProgramTree result
```
`checkedProgramTree` runs/unwraps checked-exec to preserve older raw-tree helper
behavior.
The Haskell `tricu check` path now evaluates successful checker output through
`runChecked`, so source-level guarded annotations fail through the same portable
checked-exec protocol.
## Boundary Semantics
Guard insertion follows correctness-first semantics:
> Every guarded View observation on the reachable checked-execution path runs
> its guard.
Important boundary kinds:
### Guarded typed value
```tri
typedValue sym (viewGuarded base guard) payload
```
This observes `sym` as a guarded value. It also supplies base-view evidence for
flow checking.
### Guarded requirement
```tri
typedRequire sym (viewGuarded base guard) payload
```
The symbol must satisfy `base`; the guarded observation is attached to `sym` and
is enforced when `sym` is used or exposed along the reachable root path.
### Guarded function argument
For:
```tri
viewFn [(viewGuarded base guard)] result
```
application checking guards the argument before the callee receives it.
### Guarded function result
For:
```tri
viewFn [arg] (viewGuarded base guard)
```
application checking guards the application result before exposing it as the
result value.
### Guarded callee symbol
If a function symbol itself has a guarded observation, that guard runs before the
function value is applied. A successful guard may transform the function value;
the application uses the guarded value.
## Global Symbol Observations
Guarded `typedValue` and `typedRequire` nodes are **global per-symbol
observations**, not position-sensitive flow events.
All guarded observations for a symbol compose in typed-node order whenever that
symbol is used or exposed on the reachable checked-execution path.
This means a later requirement still applies to an earlier syntactic use:
```tri
typedValue 1 viewString "x"
typedApply 2 f 1 "x"
typedRequire 1 (viewGuarded viewString guard) "x"
```
The guarded requirement is attached to symbol `1`; compiling the reachable root
path that uses symbol `1` runs that guard.
Rationale:
- typed programs are declarative symbol graphs, not imperative event traces;
- global observations are simpler and more correct-by-default;
- producers cannot accidentally bypass a guard by ordering a requirement too
late;
- staged raw/checked phases should use distinct symbols.
## Reachability and Repetition
Guards are not run eagerly for every guarded node in a program.
Execution is root-reachable:
```tri
compileSymbol (typedProgramRoot program)
```
Only guarded observations reachable from the root checked-execution path run.
Unreachable guarded symbols do not pay guard cost and do not fail execution.
Repeated reachable uses rerun guards. There is currently no deduplication or
hoisting. This is intentional: each guarded observation/use is a runtime contract
boundary.
Future optimization policies may add explicit deduplication or hoisting, but the
baseline semantics are repeated, deterministic guard execution.
## Function and Application Compilation
Checked execution is built compositionally from typed-node dependencies:
1. compile the callee symbol;
2. compile the argument symbol;
3. run any guarded observations attached to the argument symbol;
4. run the guarded function-argument boundary, if present;
5. apply the callee to the checked argument;
6. run the guarded function-result boundary, if present;
7. run guarded observations attached to the application result symbol.
This handles nested and curried application chains because each `typedApply`
consumes one function argument and produces a symbol whose inferred view is the
function residual/result view.
## Diagnostics
Guards do not author diagnostics. The checked-exec runner renders diagnostics
from checker-owned boundary context plus the guarded View.
Checker-injected guard nodes carry portable structural context. Current context
kinds are:
- root `typedValue` exposure;
- root `typedRequire` exposure;
- non-root `typedValue` symbol observation;
- non-root `typedRequire` symbol observation;
- function argument boundary;
- function result boundary;
- unknown/default context for manually constructed `checkedGuard` values.
Examples:
```text
guard failed at root typedValue symbol 0 for Guarded String
guard failed at root typedRequire symbol 3 for Guarded String
guard failed at typedRequire symbol 6 for Guarded String
guard failed at argument 0 of application symbol 2 (callee symbol 0, arg symbol 1) for Guarded String
guard failed at result of application symbol 2 (callee symbol 0, arg symbol 1) for Guarded String
malformed guard result at argument 0 of application symbol 2 (callee symbol 0, arg symbol 1) for Guarded String
```
Manually constructed `checkedGuard` values use unknown context and therefore
render without a boundary suffix:
```text
guard failed for String
malformed guard result for String
```
The context is diagnostic-only. It does not affect guard execution, View
compatibility, success/failure semantics, or continuation values.
The context deliberately contains raw portable data such as symbols and
application edges. It does not preserve source aliases such as `NonEmptyString`,
and it does not rely on Haskell-side post-processing or source-name annotation.
Named View rendering is a separate future design topic.
## Why Not Abort in Haskell?
A host-level abort primitive would move guard semantics into Haskell. The design
instead encodes guard failure in portable checked-exec artifacts and interprets
it with portable `tricu` code.
Haskell may evaluate the runner, but Haskell is not the semantic source of guard
validity or failure behavior.
## Why Not Maybe / Result Everywhere?
Returning `Maybe` or `Result` from every guarded boundary would infect ordinary
APIs. A function expecting a `List Byte` would have to accept
`Maybe (List Byte)` or `Result Error (List Byte)`, and every downstream caller
would need defensive handling.
The checked-exec runner avoids this. It unwraps successful guard results before
continuing and stops checked execution on failure.
## Known Sharp Edges
### Guard divergence
A user-written guard may diverge. This design handles intentional failure via
`guardFail`; it does not solve arbitrary nontermination. Fuel or timeouts are
separate runtime concerns.
### Payload trust
Typed nodes carry executable payloads. Guard injection must not expose an
unchecked precomputed payload at a guarded boundary. Boundaries are mediated by
checked-exec nodes.
This does not make malicious producer forgery impossible; it gives honest
frontends a portable, checkable protocol that avoids accidental bypasses.
### Cyclic typed-apply graphs
The current symbol compiler assumes typed programs are well-founded dependency
graphs as emitted by the frontend/lowering path. Cyclic typed-apply graphs are a
malformed-program validation concern, not a guard-specific semantic feature.
## Current Implementation Status
Implemented in `lib/view.tri` and exercised by tests:
- `guardOk` / `guardFail`;
- `checkedPure`, `checkedFail`, `checkedGuard`, `checkedGuardWithContext`, `checkedBind`;
- `runChecked`;
- success from `checkTypedProgramWith` returns checked-exec;
- `checkedProgramTree` compatibility helper;
- guarded root exposure;
- guarded `typedValue` and `typedRequire`;
- guarded function arguments and results;
- guarded callee observations;
- nested/curried application guard composition;
- global per-symbol observations;
- root-reachability behavior;
- repeated reachable uses rerun guards;
- source/Haskell `tricu check` integration;
- imported/module `VTGuarded` lowering to portable `viewGuarded`;
- portable guard boundary diagnostics with symbol/application context.

115
docs/module-system-design.md
View File

@@ -50,26 +50,21 @@ content identity from ergonomic naming and namespace organization.
The content store must not be married to `tricu` or Haskell.
It stores a small set of portable Arboricx artifacts: module manifests,
complete tree terms, and direct View Contract types. Lower-level Merkle/bundle
complete tree terms, and direct Contract terms. Lower-level Merkle/bundle
formats exist for transport and DAG tooling, but the store core should treat all
objects as content-addressed bytes with formats/media types.
`tricu` and Haskell are clients/tooling. They are not the semantic owners of the
store.
### 2.3 View Contracts are portable enough to integrate
### 2.3 Contracts are portable enough to integrate
The store may integrate with View Contracts because the checker and evidence
format are pure Tree Calculus / portable tree data. View Contracts are not a
Haskell-private or `tricu`-private semantic layer.
The store may integrate with Contracts because a contract is itself an ordinary
Tree Calculus term. Contracts are not a Haskell-private or `tricu`-private
semantic layer.
The module resolver may emit typed-program evidence, but checker semantics remain
unchanged:
```text
Haskell emits evidence.
tricu judges evidence.
```
A module manifest may reference a contract object, but the contract is evaluated
by ordinary Tree Calculus reduction, not by a special checker.
### 2.4 Modules should reflect definitions as they actually exist
@@ -95,11 +90,11 @@ Arboricx CAS / Merkle Store
Arboricx Bundle
compact indexed transport/execution format
View Contract Artifact
portable evidence/checker data over tree artifacts
Contract Term
ordinary tree-valued contract function, applied by reduction
Module Manifest
immutable export map from names to content objects and optional contracts
immutable export map from names to content objects and optional contract terms
Workspace
mutable aliases, selected versions, package pins, and user-facing names
@@ -109,8 +104,8 @@ tricu
```
The content store stores objects. Arboricx defines important object formats.
View Contracts define portable checking artifacts. `tricu` produces and consumes
those formats.
Contracts are ordinary tree-valued functions; `tricu` produces and consumes those
formats.
### 3.1 Execution imports versus contract checking
@@ -122,30 +117,29 @@ Calculus values are complete normal forms: importing `foo` does not require
hydrating separate `bar` or `baz` exports that may have helped build it. This is
the fast path for `!import`, including `!Local` imports.
View Contract checking is a separate evidence-gathering path. It may load
exported direct view types for the symbols that participate in a check. That
slower path must remain behind the typed program boundary:
Contract checking is a runtime boundary check. It may load exported contract term
objects for the symbols that participate in a boundary. That slower path remains
separate from execution hydration:
```text
Haskell emits evidence.
tricu judges evidence.
Haskell loads contract terms.
tricu applies them by reduction.
```
Reusable view catalogs are ordinary tricu libraries/tree terms, not a separate
Reusable contract catalogs are ordinary `tricu` libraries/tree terms, not a separate
core CAS artifact kind.
For locally built workspace modules, advertised direct export views are
producer-checked before the manifest alias is written. Producer checking includes
advertised views from any imported modules used by that source, so a module
For locally built workspace modules, advertised direct export contracts may be
checked before the manifest alias is written. Producer checking includes
advertised contracts from any imported modules used by that source, so a module
cannot publish a local annotated export that contradicts a dependency's exported
view. If producer checking fails, the module alias is not written.
contract. If producer checking fails, the module alias is not written.
Consumer checking then resolves selected module exports, decodes their
`arboricx.view-contract.type.v1` refs, and emits trusted `KnownView` evidence
for the local imported symbols. Those facts are module-boundary assumptions:
local workspace builds create them after producer-side checking, while external
or prebuilt manifests are trusted inputs for now. In all cases, compatibility
with local requirements is still judged by the portable checker in `lib/view.tri`.
Consumer checking then resolves selected module exports and loads their exported
contract term objects. Those contracts are applied at the import boundary using
the standard contract helpers. For external or prebuilt manifests, the advertised
contract is a trusted boundary declaration; the consumer may still re-apply it at
the boundary.
## 4. Content Store Direction
@@ -167,11 +161,11 @@ Current module/check object kinds:
```text
arboricx.module-manifest.v1
arboricx.tree-term.v1
arboricx.view-contract.type.v1
arboricx.tree-term.v1
```
Merkle nodes and indexed bundles remain lower-level Arboricx transport/DAG
formats, but they are not the module/eval storage model. typed programs and view
formats, but they are not the module/eval storage model. typed programs and contract
catalogs are ordinary tree terms unless a future external tooling use case proves
that they need their own object kind.
@@ -295,7 +289,7 @@ metadata:
license
createdBy
optional:
view contract artifact refs
contract artifact refs
ABI/media type info
source/provenance refs
```
@@ -312,7 +306,7 @@ name: "map"
object: sha256:...
kind: arboricx.tree-term.v1
abi: arboricx.abi.tree.v1
view: sha256:... -- optional View Contract artifact
contract: sha256:... -- optional contract term
source: sha256:... -- optional source/provenance object
```
@@ -343,7 +337,7 @@ The future pipeline should be:
parse source
resolve imports/names to module exports and content refs
lower source using resolved refs
emit a view-tree artifact
emit a contract artifact
check evidence when requested
store/export artifacts
```
@@ -392,36 +386,37 @@ This is the right identity for:
### 8.2 Module/export identity
The module manifest is the higher-level artifact boundary. It pairs each export
name with its compiled tree term and optional direct View Contract type.
name with its compiled tree term and an optional contract term reference.
The content store should not require extra definition/source/provenance objects,
and fully untyped Tree Calculus code must remain valid.
## 9. View Contract Integration
## 9. Contract Integration
View Contracts should attach to modules/exports as portable artifacts.
Contracts attach to modules/exports as ordinary tree-term objects. A contract is
a `tricu` function `Tree -> Result Tree Tree`; it is not a special artifact
kind and it does not require a separate checker binary.
An imported definition can be assigned a local numeric symbol while lowering a
typed program. Its global identity remains a content hash or module export ref.
A module manifest pairs each export name with its compiled tree term and an
optional contract term reference. The importer loads the contract object and
applies it at the boundary.
This is the intended split:
An imported definition can be assigned a local name while lowering source. Its
global identity remains a content hash or module export ref. The intended split
is:
```text
typed program local symbol: 3
Debug label: "List.map"
Resolved object: sha256:...
Exported view: Fn [...]
Local source name: "List.map"
Resolved object: sha256:...
Exported contract: sha256:...
```
De Bruijn-style integer symbols are still appropriate inside a typed program. They
are local evidence identifiers, not global content identity.
There is no typed-program evidence graph and no local numeric checker symbols.
The contract term itself is the authority.
We should not make global objects depend on numeric checker symbols.
Untyped code remains valid with no contract artifact. If a boundary needs to
participate in checking but has no information, it may use `Any` or rely on
policy. We should not pretend all untyped functions have an infinite
`Any -> Any -> ...` contract.
Untyped code remains valid with no contract artifact. If a boundary has no
contract information, it simply performs no runtime check. We should not pretend
that untyped functions have an implicit `Any -> Any -> ...` contract.
## 10. Import Syntax Direction
@@ -457,7 +452,7 @@ A plausible migration path:
index layer.
5. Define module manifest objects.
6. Teach source imports to resolve manifests/exports instead of rewriting ASTs.
7. Attach View Contract artifacts to module exports.
7. Attach contract terms to module exports.
8. Gradually migrate existing `lib/` and `demos/` imports.
Compatibility shims may keep existing `!import` working during migration.
@@ -496,9 +491,9 @@ Modules:
Workspace:
mutable human aliases, version selections, and package/module pins
View Contracts:
portable evidence artifacts attached to exports and checked by pure Tree
Calculus code
Contracts:
ordinary tree-valued functions attached to exports and applied by pure Tree
Calculus reduction at boundaries
```
The key architectural rule is that hashes provide stable identity, while names

582
docs/view-contract-syntax.md
View File

@@ -1,582 +0,0 @@
# View Contract Syntax Design
## 1. Purpose
This document specifies source-level syntax sugar for emitting View Contract
metadata from annotated `tricu` definitions.
The syntax is frontend sugar. It lowers to ordinary typed-program nodes consumed
by the portable checker in `lib/view.tri` and catalog helpers in
`lib/views/catalog.tri`.
The checker remains independent of source syntax.
## 2. Definition Annotations
A definition may carry argument and return view annotations directly in its head.
```tri
name arg1@Type1 arg2@Type2 =@ReturnType body
```
This declares:
```text
name : Fn [Type1 Type2] ReturnType
arg1 : Type1
arg2 : Type2
```
and lowers to View Contract metadata:
```tri
typedDeclareFn nameSym [(Type1) (Type2)] ReturnType t
typedValue arg1Sym Type1 t
typedValue arg2Sym Type2 t
```
If body flow metadata is emitted, the body result is required to satisfy the
appropriate residual view.
## 3. Syntax Forms
### 3.1 Binder annotation
```tri
x@Bool
xs@(List Bool)
f@(Fn [Bool] String)
```
A binder annotation introduces a normal term binder and contributes an argument
view to the function contract.
### 3.2 Phantom argument annotation
```tri
name @A @B =@C body
```
A phantom argument annotation contributes an argument view to the function
contract but introduces no term binder.
This is useful for point-free and combinator-heavy definitions.
```tri
name @A @B =@C body
```
declares:
```text
name : Fn [A B] C
```
The body itself must satisfy the residual function view:
```text
Fn [A B] C
```
### 3.3 Binder prefix with phantom tail
Phantom annotations may appear after binder annotations:
```tri
name x@A @B =@C body
```
This declares:
```text
name : Fn [A B] C
x : A
```
The body must satisfy:
```text
Fn [B] C
```
This allows a named binder prefix with a point-free tail.
### 3.4 Return annotation
```tri
name x@A =@B body
name =@B body
```
`=@B` contributes the result view.
A definition with no arguments and a return annotation is a value contract, not a
zero-arity function contract:
```tri
name =@Bool body
```
lowers to:
```tri
typedValue nameSym viewBool t
```
not:
```tri
typedDeclareFn nameSym [] viewBool t
```
## 4. Ordering Rule
Phantom argument annotations may only appear at the end of the argument list.
Valid:
```tri
foo x@A y@B =@C body
foo @A @B =@C body
foo x@A @B =@C body
foo x y@B @C =@D body
```
Invalid:
```tri
foo x@A @B z@C =@D body
foo @A x@B =@C body
```
Once a phantom `@Type` item appears, no later named binder may appear.
## 5. Contract-Bearing Definitions
A definition is contract-bearing if its head contains any of:
```text
binder@Type
@Type
=@Type
```
Ordinary unannotated definitions do not emit View Contract metadata.
```tri
foo x y = body
```
emits no contract metadata.
## 6. Unannotated Binders in Contract-Bearing Heads
In a contract-bearing definition, an unannotated binder contributes `Any`.
```tri
foo x y@Bool =@String body
```
means:
```text
foo : Fn [Any Bool] String
x : Any
y : Bool
```
This keeps mixed annotation lightweight without emitting contracts for fully
unannotated definitions.
## 7. Missing Return Annotation
If a contract-bearing definition has argument annotations but no return
annotation, the return view defaults to `Any`.
```tri
foo x@Bool = body
```
means:
```text
foo : Fn [Bool] Any
x : Bool
```
## 8. Type Annotation Grammar
Annotations are intentionally small at the attachment site.
After `@` or `=@`, the parser accepts either a single atomic view expression or
a parenthesized compound view expression.
Valid:
```tri
x@Bool
x@(List Bool)
f@(Fn [Bool] String)
r@(Result String Bool)
name =@Bool body
name =@(List Bool) body
```
These are not structural annotations:
```tri
x@List Bool
f@Fn [Bool] String
name =@List Bool body
```
They are parsed according to normal definition-head rules. For example,
`x@List Bool` means binder `x` has the atomic view expression `List`, followed by
an unannotated binder named `Bool`. Use parentheses when the annotation itself is
an application.
## 9. Type Grammar
View expressions are ordinary value-level expressions in a restricted annotation
grammar:
```text
ViewExpr
= name
| integer
| [ViewExpr...]
| ViewExpr ViewExpr
| (ViewExpr)
```
Built-in names lower to standard view values:
```text
Any -> viewAny
Bool -> viewBool
String -> viewString
Byte -> viewByte
Unit -> viewUnit
```
Atomic refs lower explicitly. String refs are the preferred user-facing form;
numeric refs remain available for low-level/generated code:
```text
Ref "Nat" -> viewRef "Nat"
Ref 10 -> viewRef 10
```
Additional named views and view constructors are ordinary `tricu` values:
```tri
Nat = viewRef "Nat"
Box a = viewPair (viewRef "Box") a
idNat x@Nat =@Nat x
idBox x@(Box String) =@(Box String) x
```
The frontend resolves names and evaluates view expressions, but well-formedness
is judged by the self-hosted checker (`wellFormedView?` in `lib/view.tri`).
Malformed view values are rejected when checked or published.
## 10. List Syntax in Types
Function argument lists use the source type grammar:
```tri
Fn [Bool String] Unit
Fn [(List Bool) (Maybe String)] Unit
```
The lowered typed program must still respect ordinary `tricu` list syntax, where
each list element is parenthesized when needed:
```tri
viewFn [(viewBool) (viewString)] viewUnit
```
## 11. Residual Body View
For a contract-bearing definition, the full definition view is always:
```text
Fn [allArgumentViews...] returnView
```
except for nullary value annotations, which use the return view directly.
The body obligation depends on how many argument views are represented by named
binders in the definition head.
Let:
```text
argViews = [A B C]
returnView = R
binderCount = number of named binders before the phantom tail
remaining = drop binderCount argViews
```
Then:
```text
bodyRequiredView = residual(remaining, returnView)
```
where:
```text
residual([], R) = R
residual([A ...], R) = Fn [A ...] R
```
Examples:
```tri
foo x@A y@B =@C body
```
Body required view:
```text
C
```
```tri
foo @A @B =@C body
```
Body required view:
```text
Fn [A B] C
```
```tri
foo x@A @B =@C body
```
Body required view:
```text
Fn [B] C
```
## 12. Lowering Examples
### 12.1 Fully annotated binders
Source:
```tri
foo x@Bool xs@(List Bool) =@String body
```
Definition contract:
```tri
typedDeclareFn fooSym [(viewBool) (viewList viewBool)] viewString t
typedValue xSym viewBool t
typedValue xsSym (viewList viewBool) t
```
Body obligation:
```tri
typedRequire bodySym viewString t
```
### 12.2 Pure phantom signature
Source:
```tri
foo @Bool @(List Bool) =@String body
```
Definition contract:
```tri
typedDeclareFn fooSym [(viewBool) (viewList viewBool)] viewString t
```
Body obligation:
```tri
typedRequire bodySym (viewFn [(viewBool) (viewList viewBool)] viewString) t
```
### 12.3 Binder prefix with phantom tail
Source:
```tri
foo x@Bool @(List Bool) =@String body
```
Definition contract:
```tri
typedDeclareFn fooSym [(viewBool) (viewList viewBool)] viewString t
typedValue xSym viewBool t
```
Body obligation:
```tri
typedRequire bodySym (viewFn [(viewList viewBool)] viewString) t
```
### 12.4 Value annotation
Source:
```tri
message =@String "hello"
```
Definition contract:
```tri
typedValue messageSym viewString t
```
Body obligation:
```tri
typedRequire bodySym viewString t
```
## 13. `tricu check`
`tricu check` consumes an annotated program, lowers annotations to typed program
metadata, runs the checker, and reports either `ok` or rendered diagnostics.
Initial behavior:
```bash
tricu check path/to/program.tri
```
outputs checker success or errors. Diagnostics are rendered by the portable
checker, then annotated by the frontend with source/debug labels when available:
```tri
id x@String =@Bool x
```
reports:
```text
symbol 1 (x) expected Bool but got String
```
Application result labels include the application head when known:
```tri
xs =@(List String) [(g "hi")]
g y@String =@Bool y
```
reports:
```text
symbol 3 (g application result) expected String but got Bool
```
These labels are presentation-only metadata. The checker still judges only the
emitted typed-program evidence.
Future behavior may include:
```bash
tricu check --out path/to/executable.arboricx path/to/program.tri
```
which checks an annotated source program and emits an executable Arboricx bundle.
The checker library remains available independently of the CLI workflow.
## 14. Frontend Lowering Boundaries
The annotation syntax is frontend sugar. The canonical checker input remains a
plain typed program: ordinary `typedValue`, `typedDeclareFn`,
`typedRequire`, and `typedApply` nodes represented as portable `tricu`
data.
The frontend may emit richer evidence from source forms, but it does not decide
semantic compatibility. In short:
```text
Haskell emits evidence.
tricu judges evidence.
```
Current source-driven evidence includes:
- literal views for strings, bytes, unit, and homogeneous list literals;
- expected element requirements for `List T` bodies;
- expected `Fn` requirements for lambda literals and curried application spines;
- application argument requirements when the callee has a known `Fn` view;
- expected constructor flow for unshadowed stdlib constructors:
- `pair` with expected `Pair A B`;
- `just` and `nothing` with expected `Maybe A`;
- `ok` and `err` with expected `Result E A`.
Constructor lowering only applies when the constructor name is not shadowed by a
local binder or top-level definition in the checked source. If a program defines
its own `pair`, `just`, `nothing`, `ok`, or `err`, checking falls back to normal
application evidence.
For tooling and regression tests, the frontend exposes a lowering-only API that
returns emitted typed program text without invoking the checker:
```hs
lowerSource :: String -> Either String String
```
It also exposes debug labels for symbols:
```hs
lowerSourceWithDebug :: String -> Either String (String, Map Integer String)
```
Debug labels are presentation metadata only. They are not part of checker
semantics and are not consumed by `lib/view.tri`.
`do` blocks have no separate View Contract semantics. The parser lowers them
through their explicit bind operator:
```tri
do bind
x <- action
next x
```
becomes ordinary application/lambda structure. Checking then follows the known
`Fn` view of the bind operator, including the callback argument view when it is
available.
## 15. Summary
The annotation syntax is:
```tri
name arg@A arg2@B =@C body
name @A @B =@C body
name arg@A @B =@C body
name =@C body
```
Core rules:
1. Binder annotations introduce binders and argument views.
2. Phantom annotations introduce argument views only.
3. Phantom annotations may only appear after all binders.
4. Unannotated binders in contract-bearing heads contribute `Any`.
5. Missing return annotations in contract-bearing heads default to `Any`.
6. Nullary `=@T` definitions are value contracts, not zero-arity functions.
7. Compound annotation types must be parenthesized.
8. Lowering emits ordinary typed-program nodes for the existing checker.

384
docs/view-contracts.md
View File

@@ -1,384 +0,0 @@
# View Contracts and View Trees
## 1. Purpose
View Contracts are the portable checking layer for Tree Calculus programs.
The checker does not consume detached metadata about a separate executable. Its
canonical input is a typed, checkable tree artifact: ordinary tree data that
contains both the executable program payloads and the view/contract structure
needed to validate and transform them.
The checker consumes this artifact and returns either:
```text
checked-execution artifact
```
or:
```text
structured diagnostic
```
A checked-execution artifact is interpreted by `runChecked`. Unguarded programs
are represented as `checkedPure rootPayload`; guarded programs contain explicit
checked guard/bind nodes.
This keeps checking independent of any particular host implementation. A typed
artifact may be produced by any frontend, compiler, hand-written generator, or
future self-hosted `tricu` toolchain.
## 2. Design Principle
The model follows the same discipline as interaction trees.
Interaction trees use tagged structural envelopes with explicit executable
payloads:
```tri
io action = pair "tricuIO" (pair version action)
pure x = pair 0 x
bind action k = pair 1 (pair action k)
```
The interpreter understands the outer structure, but it does not recursively
mistake every subtree for interpreter metadata. A continuation `k` is an opaque
executable tree until the interpreter reaches the `bind` step that applies it.
View trees use the same rule:
```text
structure says how to check;
opaque executable fields are only executed/applied by the checker at the
appropriate step.
```
This is the key distinction that allows Views to carry guards without confusing
ordinary program trees with View metadata.
## 3. Views
A View is an extrinsic contract over an ordinary Tree Calculus value. Tree
Calculus values do not carry native runtime types; a View describes how a value
may be treated by the checker or by a checked boundary.
Core View forms:
```text
Any
Ref ref
Fn [argView...] resultView
List elemView
Maybe elemView
Pair leftView rightView
Result errView okView
Guarded baseView guard
```
`Ref` supports both generated/numeric and symbolic references. Symbolic refs are
preferred for user-authored views:
```tri
UserId = viewRef "UserId"
```
A guarded view refines a base view with an executable guard:
```tri
UserId = viewGuarded (viewRef "UserId") userIdGuard
```
The guard is ordinary program code. The View validator checks that the guarded
view envelope is well-formed, and recursively validates the `baseView`, but it
must treat the guard payload/reference as opaque executable data, not as another
View.
## 4. Soundness Boundary
Views are descriptive boundary metadata, not types and not proofs about opaque
Tree Calculus terms. In particular, the checker does not claim parametricity,
representation independence, or existential abstraction.
Raw Tree Calculus observation can distinguish values by their tree
representation. A term advertised as `Fn [A] A` can inspect its argument and
choose a representation-dependent result; a metadata-only checker cannot rule
that out. The same issue applies transitively through higher-order arguments and
dynamically constructed observers.
The checker therefore accepts only monomorphic Views. Legacy `Var`, `Forall`,
and `Exists` tags remain reserved so old artifacts fail deterministically, but
they are not well-formed checker inputs.
The guarantees retained here are narrower:
- View and typed-program envelopes are structurally well formed.
- Declared monomorphic Views flow consistently across explicit typed nodes.
- Guarded Views execute their predicates at represented boundaries.
- Artifact references bind metadata to particular stored objects.
These guarantees do not establish that an opaque payload has an unguarded
structural View such as `List` or `Fn`. Such Views are conventions/assertions
used to place and compose checks. Only an executed guard observes the value.
See [the intensionality analysis](../notes/view-contract-trust-provenance.md) for
the rationale and remaining limitations.
## 5. Guards
Guards are ordinary `tricu` values/functions grouped with the Views they refine.
Example:
```tri
userIdGuard = value :
-- ordinary program that validates value
UserId = viewGuarded (viewRef "UserId") userIdGuard
loadUser id@UserId = ...
```
Guards return the standard checked-runtime protocol:
```tri
guardOk value
guardFail
```
Guards do not author diagnostics. The checked-exec runner owns guard failure and
malformed-guard diagnostics using boundary context from the checked artifact.
Guards are injected by the checker. They are not discovered by the runtime as a
separate metadata layer. The checking process transforms a view tree into an
executable tree with the necessary guard applications inserted.
## 6. View Tree Artifact
The primary checker-facing artifact is a view executable term graph.
Conceptually:
```text
ViewTree
version
root node id
nodes
```
Each node is tagged tree data. Nodes combine executable payloads, view claims,
and structural relationships in one graph.
Representative node forms:
```text
Value node view executableTree
Apply node calleeNode argNode expectedOrInferredView
Require node requiredView sourceNode
External node name view
```
This is not a mandatory final encoding; it is the semantic target. The important
property is that executable trees and checking structure are carried together in
a single portable artifact.
A node may contain opaque executable fields. Those fields are tree terms, but
they are not recursively decoded as view-tree nodes or Views unless the node's
semantics explicitly says so.
View facts may carry per-fact provenance:
```text
Checked
Trusted
Unchecked
```
These labels are retained for artifact compatibility and auditing. They identify
the source of an assertion; they do not prove semantic membership, parametricity,
or abstraction. An absent label is interpreted conservatively as `Unchecked`.
The former value-level polymorphic `viewFacts` catalogs and frontend
raw-intensionality taint pass have been removed. Monomorphic imported facts may
still be attached to exports, but consumers must treat them as assertions unless
an executable guard enforces the relevant property.
## 7. Checker Semantics
The checker is an interpreter over the view tree.
For each node it may:
1. validate the node envelope;
2. validate Views referenced by the node;
3. check compatibility between expected and actual Views;
4. recursively check child nodes;
5. inject guards required by guarded Views;
6. produce the executable tree for that node;
7. memoize node results by node id.
The root node result is a checked-execution program.
In abstract form:
```text
checkViewTree : ViewTree -> Result CheckedExec Diagnostic
```
or, in self-hosted terms:
```tri
checkViewTree viewTree = ... -- ok checkedExec / err diagnostic
```
## 8. Compatibility and Guard Injection
Structural compatibility is about Views. Guard injection is about producing the
checked-execution tree.
For example, if a node is required to satisfy:
```tri
viewGuarded (viewRef "UserId") userIdGuard
```
then the checker verifies the underlying View relationship and emits executable
code that applies `userIdGuard` at the appropriate checked boundary.
The checker, not the runtime metadata system, owns this transformation.
## 9. Source Annotations
Source annotations are one frontend syntax for producing view-tree nodes.
Examples:
```tri
Nat = viewRef "Nat"
Box a = viewPair (viewRef "Box") a
idNat x@Nat =@Nat x
idBox x@(Box String) =@(Box String) x
```
Annotations are value-level View expressions. Names such as `Nat` and `Box` are
ordinary program values/functions that evaluate to Views.
A frontend that supports this syntax should lower the source into a view tree
that contains the relevant executable terms, views, and checking structure. The
artifact must not depend on source names or on the frontend implementation that
produced it.
## 10. Contract Expressions
Contract-expression helpers remain useful as authoring/building tools, but they
are not the fundamental artifact model.
Preferred style for expression-oriented authoring is pipeline-first:
```tri
mapBoolStringUse = cFn <|
[(viewFn [(viewBool)] viewString) (viewList viewBool)] (viewList viewString)
|> cApply (cFn [(viewBool)] viewString)
|> cApply (cValue (viewList viewBool))
|> cRequire (viewList viewString)
```
These helpers should be understood as convenient ways to build typed/checkable
structure, not as a permanent replacement for view-tree artifacts.
## 11. Artifact Direction
The target direction is to make the view tree the canonical checked-program
artifact.
Older split concepts remain useful internally or during development:
```text
tree term
view value
typed-program node
module/export manifest
```
But the durable design should avoid treating contracts as detached facts about a
separate program. The portable checker input is the checkable program itself.
In short:
```text
Do not store code over here and contracts over there.
Store a view tree: executable code plus the structure needed to check and guard it.
```
## 12. IO Interaction Trees
`tricu` IO is represented as ordinary interaction-tree data:
```tri
io action = pair "tricuIO" (pair version action)
pure value = pair 0 value
bind action k = pair 1 (pair action k)
```
View Contracts do not change that representation. A checked program may produce
an ordinary IO interaction tree, and the existing IO driver can execute it
unchanged.
For source evaluation with contracts enabled, `tricu eval --io` performs an
additional frontend instrumentation pass over visible IO continuations. When a
continuation returns a `pure (...)` value that mentions source-annotated
functions, the frontend lowers that pure expression into the existing portable
checked-exec protocol before returning the next IO action.
This means source sugar works for practical checked IO paths such as:
```tri
acceptNames xs@(NonEmptyList String) =@String "accepted"
main = io (bind (pure []) (xs : pure (acceptNames xs)))
```
and for explicit higher-order boundaries:
```tri
useHandler handler@(Fn [(NonEmptyList String)] String) xs@(List String) =@String
handler xs
main = io (bind (pure []) (xs : pure (useHandler acceptNames xs)))
```
The IO runtime does not perform View inference or guard injection at every step.
The source/frontend pass constructs checked-exec boundaries once; the runtime
only evaluates the resulting interaction tree.
Current limitations:
- This is source-visible instrumentation, not whole-program function-flow
tracking.
- Higher-order guarantees require explicit annotated boundaries.
- Raw prebuilt interaction trees, imported executable artifacts, and content-store
terms are not automatically re-instrumented unless they pass through this
source-lowering path.
- The IO action shape itself is only shallowly checkable unless users provide
guarded Views for the relevant boundaries.
- Continuation result Views are not inferred from external effects; dynamic IO
values should cross annotated/guarded boundaries when runtime enforcement is
required.
Making IO checking more complete is future work. In particular, a future design
may validate every continuation-produced action structurally, carry checked
wrappers with higher-order function values, or define a portable checked-IO
artifact instead of relying on Haskell/frontend source instrumentation.
## 13. Host Independence
No part of the core View Tree design is specific to Haskell or to the current implementation.
Any producer may emit a view-tree artifact if it follows the portable tree-data
encoding. Any checker implementation may consume it if it implements the typed
node semantics.
The current implementation can produce and consume these artifacts, but it is
not the semantic authority. The artifact format and the self-hosted checker
semantics are the authority.