Fix interaction tree demos and HTTP recv 4096

Contracts now live directly on definitions via @ / =@ annotations and
travel automatically with exported values.

- Remove !export from lexer/parser/AST/evaluator/manifest/resolver and CLI.
- Simplify workspace module export logic: export all top-level local
  definitions by default.
- Update Frontend.ContractDesugar:
  - Named binder annotations (x@nat?) expand to per-argument withContract.
  - Phantom annotations (@nat?) expand to a local raw helper plus a wrapper,
    keeping fixed points shared and only depending on withContract.
- Merge lib/guardedBase.tri into lib/base.tri and annotate partial/sensitive
  base functions: head, tail, last, add, sub, mul, div, mod, pow, min,
  max, length, sum, product.
- Add check contract helper to lib/base.tri.
- Update demos/contractBasics.tri and README to reflect @/=@-only design.
- Update test suite: remove guardedBase import, replace explicit !export
  test with a test verifying that contract annotations on an exported
  definition are enforced on import.
- Fix remaining base.tri definitions (div/mod/pow) to stay point-free.

README.md

@@ -8,7 +8,7 @@ tricu is the word for "tree" in Lojban: `(x1) is a tree of species/cultivar (x2)
 
 In the `ext/` directory there are implementations of TC evaluators and tooling in other languages. Here be dragons; beware.
 
-I have fully embraced the slopmachine (LLM-assisted development) for this project. Nothing is stable or sacred. We will discover sanity at the end of the journey but we won't strive for it until then.
+While my original implementation was hand-written, I have since fully embraced the slopmachine for this project. Nothing is stable or sacred. We will discover sanity at the end of the journey but we won't strive for it until then. The `main` branch will see my latest thoughts and experiments. Emphasis on "AUTHOR DISCLAIMS ALL WARRANTIES" from the LICENSE.
 
 This README.md is 100% human written. No other .md file will be until stabilization.
 
@@ -31,6 +31,7 @@ tricu < triage = (a b c : t (t a b) c)
 tricu < test = triage "Leaf" (z : "Stem") (a b : "Fork")
 tricu < test (t t)
 tricu > "Stem"
+
 tricu < -- We can even convert a term back to source code (/demos/toSource.tri)
 tricu < toSource not?
 tricu > "(t (t (t t) (t t t)) (t t (t t t)))"
@@ -62,21 +63,6 @@ tricu eval --format decode program.tri
 tricu eval --output result.txt program.tri
 ```
 
-Unchecked eval parses annotation syntax, discards contract metadata, skips
-producer-side View Contract checks during workspace module auto-builds, and does
-not publish unchecked View refs. 
-
-```sh
-tricu eval --unchecked program.tri
-```
-
-Check View Contract annotations explicitly:
-
-```sh
-tricu check program.tri
-tricu check --store ./.tricu-store program.tri
-```
-
 Compile/import/export Arboricx bundles:
 
 ```sh
@@ -85,13 +71,6 @@ tricu arboricx import --file program.arboricx --module program
 tricu arboricx export --module prelude --output prelude.arboricx
 ```
 
-Inspect store aliases:
-
-```sh
-tricu store alias list --kind modules
-tricu store alias get --kind modules prelude
-```
-
 ### REPL
 
 Running `tricu` with no subcommand starts the REPL. The REPL uses the same
@@ -101,13 +80,10 @@ Useful commands:
 
 ```text
 !load FILE          load/evaluate a .tri file without printing a result
-!check FILE         run View Contract checking for a file
 !store [PATH]       show or set the content-addressed store
-!unchecked on       evaluate loaded files without contract checking/publishing refs
-!unchecked off      return to normal producer-checked module loading
 !format decode      set output format by name
 !env                list current in-memory bindings
 ```
 
-`!load` and `!check` support filename tab completion. Normal REPL input also
+`!load` supports filename tab completion. Normal REPL input also supports tab
-supports tab completion for names currently in the REPL environment.
+completion for names currently in the REPL environment.

bench/Bench.hs

@@ -2,124 +2,63 @@
 module Main where
 
 import Criterion.Main
-import qualified Data.ByteString as BS
 import qualified Data.Map as Map
 
-import ApplyStats (runApplyCounted, runApplyGlobalCounted, printApplyStats)
 import Eval
 import FileEval
 import Parser
 import Research
 
--- | Pre-process a demo file and return its AST.
-loadDemo :: FilePath -> IO [TricuAST]
-loadDemo = preprocessFile
-
--- | Evaluate a pre-processed demo to its result term.
-runDemo :: [TricuAST] -> T
-runDemo ast = result (evalTricu Map.empty ast)
-
 -- | Build an environment from a library file.
 loadLib :: FilePath -> IO Env
 loadLib = evaluateFile
 
 main :: IO ()
 main = do
-  !equalityAst    <- loadDemo "demos/equality.tri"
+  !baseLib      <- loadLib "lib/base.tri"
-  !sizeAst        <- loadDemo "demos/size.tri"
-  !toSourceAst    <- loadDemo "demos/toSource.tri"
-  !levelOrderAst  <- loadDemo "demos/levelOrderTraversal.tri"
-  !patternAst     <- loadDemo "demos/patternMatching.tri"
   !listLib      <- loadLib "lib/list.tri"
-
+  !contractsLib <- loadLib "lib/contracts.tri"
-  -- Stress benchmark environment: Arboricx parser + size + toSource
+  !intLib       <- loadLib "lib/intensionalContracts.tri"
-  !arboricxLib    <- loadLib "lib/arboricx/dispatch.tri"
+  !guardedLib   <- loadLib "lib/guardedBase.tri"
-  !sizeEnv        <- evaluateFileWithContext arboricxLib "demos/size.tri"
+  let !env = Map.unions [baseLib, listLib, contractsLib, intLib, guardedLib]
-  !toSourceEnv    <- evaluateFileWithContext sizeEnv "demos/toSource.tri"
-
-  -- Print apply stats for toSource not?
-  let Just toSource = Map.lookup "toSource" toSourceEnv
-      Just notTerm  = Map.lookup "not?" toSourceEnv
-      (_result, stats) = runApplyCounted toSource notTerm
-  printApplyStats stats
-
-  -- Print apply stats for readArboricxContainer against id.arboricx
-  !idBundleBytes <- BS.readFile "test/fixtures/id.arboricx"
-  let Just readContainer = Map.lookup "readArboricxContainer" sizeEnv
-      bundleTree = ofBytes idBundleBytes
-  (_result2, stats2) <- runApplyGlobalCounted 100000 1000000 readContainer bundleTree
-  printApplyStats stats2
 
   defaultMain
-    [ bgroup "demos"
+    [ bgroup "contracts"
-        [ bench "equality"          $ whnf runDemo equalityAst
+        [ bench "raw head" $ whnf
-        , bench "size"              $ whnf runDemo sizeAst
+            (result . evalTricu env . parseTricu)
-        , bench "toSource"          $ whnf runDemo toSourceAst
+            "head [1 2 3 4 5]"
-        , bench "levelOrderTraversal" $ whnf runDemo levelOrderAst
+        , bench "safeHead (checked)" $ whnf
-        , bench "patternMatching"   $ whnf runDemo patternAst
+            (result . evalTricu env . parseTricu)
+            "safeHead [1 2 3 4 5]"
+        , bench "raw div" $ whnf
+            (result . evalTricu env . parseTricu)
+            "div 10 2"
+        , bench "safeDiv (checked)" $ whnf
+            (result . evalTricu env . parseTricu)
+            "safeDiv 10 2"
+        , bench "safeDiv failure (div by zero)" $ whnf
+            (result . evalTricu env . parseTricu)
+            "safeDiv 10 0"
+        , bench "sortedMax on sorted list" $ whnf
+            (result . evalTricu env . parseTricu)
+            "sortedMax [1 2 3 4 5]"
+        , bench "safeHalf (even check)" $ whnf
+            (result . evalTricu env . parseTricu)
+            "safeHalf 8"
+        , bench "sortedList? success" $ whnf
+            (result . evalTricu env . parseTricu)
+            "withContract (sortedList? nat?) [1 2 3 4 5] (xs : sum xs) (msg : 0)"
+        , bench "sortedList? failure" $ whnf
+            (result . evalTricu env . parseTricu)
+            "withContract (sortedList? nat?) [5 1 3] (xs : sum xs) (msg : 0)"
+        , bench "listOf nat? success" $ whnf
+            (result . evalTricu env . parseTricu)
+            "withContract (listOf nat?) [1 2 3 4 5] (xs : sum xs) (msg : 0)"
+        , bench "fn2 apply add" $ whnf
+            (result . evalTricu env . parseTricu)
+            "(fn2 nat? nat? nat? add) 3 5"
+        , bench "fnContract apply identity" $ whnf
+            (result . evalTricu env . parseTricu)
+            "(fnContract nat? nat? (x : x)) 7"
         ]
-
-    , bgroup "lib/list.tri"
-        [ bench "append strings" $ whnf
-            (result . evalTricu listLib . parseTricu)
-            "append \"Hello, \" \"world!\""
-        , bench "map over 3 elements" $ whnf
-            (result . evalTricu listLib . parseTricu)
-            "head (tail (map (a : (t t t)) [(t) (t) (t)]))"
-        , bench "equal? same" $ whnf
-            (result . evalTricu listLib . parseTricu)
-            "equal? (t t t) (t t t)"
-        , bench "equal? different" $ whnf
-            (result . evalTricu listLib . parseTricu)
-            "equal? (t t) (t t t)"
-        , bench "triage Leaf" $ whnf
-            (result . evalTricu listLib . parseTricu)
-            "test t"
-        , bench "triage Stem" $ whnf
-            (result . evalTricu listLib . parseTricu)
-            "test (t t)"
-        , bench "triage Fork" $ whnf
-            (result . evalTricu listLib . parseTricu)
-            "test (t t t)"
-        , bench "not? true" $ whnf
-            (result . evalTricu listLib . parseTricu)
-            "not? (t t)"
-        , bench "not? false" $ whnf
-            (result . evalTricu listLib . parseTricu)
-            "not? t"
-        ]
-
-    , bgroup "stress"
-        [ bench "size runArboricxTyped" $ whnf
-            (result . evalTricu sizeEnv . parseTricu)
-            "size runArboricxTyped"
-        , bench "equal? runArboricxTyped runArboricxTyped" $ whnf
-            (result . evalTricu sizeEnv . parseTricu)
-            "equal? runArboricxTyped runArboricxTyped"
-        , bench "size readArboricxBundle" $ whnf
-            (result . evalTricu sizeEnv . parseTricu)
-            "size readArboricxBundle"
-        , bench "equal? readArboricxBundle readArboricxBundle" $ whnf
-            (result . evalTricu sizeEnv . parseTricu)
-            "equal? readArboricxBundle readArboricxBundle"
-        ]
-
-    , bgroup "raw-apply"
-        [ bench "rule-1 (Fork Leaf a) b" $ whnf
-            (\n -> apply (Fork Leaf (ofNumber n)) (ofNumber 42))
-            1000
-        , bench "rule-2 (Fork (Stem a) b) c" $ whnf
-            (\n -> apply (Fork (Stem (ofNumber n)) (ofNumber n)) (ofNumber 42))
-            1000
-        , bench "rule-3a (Fork (Fork a b) c) Leaf" $ whnf
-            (\n -> apply (Fork (Fork (ofNumber n) (ofNumber n)) (ofNumber n)) Leaf)
-            1000
-        , bench "rule-3b (Fork (Fork a b) c) (Stem u)" $ whnf
-            (\n -> apply (Fork (Fork (ofNumber n) (ofNumber n)) (ofNumber n)) (Stem Leaf))
-            1000
-        , bench "rule-3c (Fork (Fork a b) c) (Fork u v)" $ whnf
-            (\n -> apply (Fork (Fork (ofNumber n) (ofNumber n)) (ofNumber n)) (Fork Leaf Leaf))
-            1000
-        ]
-
     ]

demos/contractBasics.tri

@@ -0,0 +1,25 @@
+!import "prelude" !Local
+
+-- Custom contract combinators built directly on matchResult.
+myAndC = (c1 c2 value rest :
+  matchResult
+    (msg _ : contractErr msg rest)
+    (v _ : c2 v rest)
+    (c1 value rest))
+
+-- Plain predicates lifted into contracts with a diagnostic message.
+natural? = guardC "natural" isNat?
+nonZero? = guardC "non-zero" (n : and? (isNat? n) (not? (isZero_? n)))
+
+-- Phantom annotations let point-free definitions carry their own contracts.
+-- The base library now uses the same syntax, so head/tail/div etc. are
+-- guarded by default.
+myHead @(nonEmptyListOf anyC) =@anyC head
+myTail @(listOf anyC) =@(listOf anyC) tail
+myDiv @natural? @(myAndC natural? nonZero?) =@natural? div
+
+-- The `check` helper applies a contract to any value and returns the
+-- checked value (or the diagnostic message on failure).
+checkedSuccessor = check natural? (add 1 2)
+
+main = pair checkedSuccessor (myDiv 10 2)

demos/contractEffects.tri

@@ -0,0 +1,64 @@
+!import "prelude" !Local
+
+-- ---------------------------------------------------------------------------
+-- Contracts + interaction trees with `do` notation
+--
+-- The `do` keyword takes a monadic bind operator. Here we use `bindM` from
+-- `lib/contracts.tri` to sequence pure, contract-checked computations.
+--
+--   checkM contract value     -- lift a contract failure into the tree
+--   exceptE tag value k       -- a resumable failure carrying a continuation
+--   handleM tag handler tree  -- rewrite matching exceptions
+--   runM tree                 -- interpret the tree into a Result
+--
+-- A handler receives the exception value and the resumption continuation `k`.
+-- It may resume by calling `k value`, or it may replace the failing action with
+-- a new tree of its own.
+-- ---------------------------------------------------------------------------
+
+positive? = guardC "expected positive integer" (n : gte? n 1)
+nonEmpty? = guardC "expected non-empty list" (xs : not? (emptyList? xs))
+
+-- Average a list. Fails with a contract exception if the list is empty.
+average = (xs :
+  do bindM
+    _ <- checkM nonEmpty? xs
+    n <- pureM (length xs)
+    _ <- checkM positive? n
+    total <- pureM (sum xs)
+    pureM (div total n))
+
+-- A resumable config lookup. When the key is missing, callers can supply a
+-- value by handling the "missing" exception.
+lookupConfig = (key defaultValue :
+  exceptE "missing" key (resume : pureM defaultValue))
+
+-- A pipeline that averages a list and divides by a configured divisor.
+pipeline = (xs :
+  do bindM
+    divisor <- lookupConfig "divisor" 1
+    avg <- average xs
+    scaled <- liftM (x : div x divisor) avg
+    pureM scaled)
+
+-- Without a handler the missing-key exception reaches runM.
+unhandled = runM (pipeline [10 20 30])
+-- < unhandled
+-- > [t, "divisor"]
+
+-- With a handler we replace the missing divisor with 2, so 20 / 2 = 10.
+withHandler = runM (handleM "missing" (key k : pureM 2) (pipeline [10 20 30]))
+-- < withHandler
+-- > [t t, 10]
+
+-- Handler can also use the original default by calling the resumption.
+withResume = runM (handleM "missing" (key k : k 2) (pipeline [10 20 30]))
+-- < withResume
+-- > [t t, 20]
+
+-- Contract failures still propagate through handlers for other tags.
+bothFail = runM (handleM "missing" (key k : pureM 2) (pipeline []))
+-- < bothFail
+-- > [t, "expected non-empty list"]
+
+main = withHandler

demos/interactionTrees/arboricxServer.tri

@@ -1,4 +1,4 @@
-!import "base"            !Local
+!import "prelude" !Local
 !import "io"              !Local
 !import "arboricx.server" !Local
 

demos/interactionTrees/environment.tri

@@ -1,5 +1,4 @@
-!import "base" !Local
+!import "prelude" !Local
-!import "list" !Local
 !import "io"   !Local
 
 -- Environment effects: ask and local.

demos/interactionTrees/forkAwait.tri

@@ -1,5 +1,4 @@
-!import "base" !Local
+!import "prelude" !Local
-!import "list" !Local
 !import "io"   !Local
 
 -- Basic fork and await.

demos/interactionTrees/greet.tri

@@ -1,5 +1,4 @@
-!import "base" !Local
+!import "prelude" !Local
-!import "list" !Local
 !import "io"   !Local
 
 -- Greet and return a pure value.

demos/interactionTrees/safeRead.tri

@@ -1,5 +1,4 @@
-!import "base" !Local
+!import "prelude" !Local
-!import "list" !Local
 !import "io"   !Local
 
 -- readFile returns a Result.  matchResult branches on ok / err.

demos/interactionTrees/shout.tri

@@ -1,5 +1,4 @@
-!import "base" !Local
+!import "prelude" !Local
-!import "list" !Local
 !import "io"   !Local
 
 -- Transform an IO result.

demos/interactionTrees/state.tri

@@ -1,5 +1,4 @@
-!import "base" !Local
+!import "prelude" !Local
-!import "list" !Local
 !import "io"   !Local
 
 -- Mutable state via get and put.

demos/interactionTrees/writeThenRead.tri

@@ -1,5 +1,4 @@
-!import "base" !Local
+!import "prelude" !Local
-!import "list" !Local
 !import "io"   !Local
 
 -- Write a file, then read it back.

demos/interactionTrees/yield.tri

@@ -1,5 +1,4 @@
-!import "base" !Local
+!import "prelude" !Local
-!import "list" !Local
 !import "io"   !Local
 
 -- Cooperative scheduling with yield.

demos/viewContracts.tri

@@ -1,190 +0,0 @@
-!import "prelude" !Local
-!import "view" !Local
-
--- ============================================================================
--- View Contracts in tricu
--- ============================================================================
---
--- Verify this guide passes checking with:
---
---   tricu check demos/viewContracts.tri
---
--- Expected output:
---
---   ok
---
--- This file uses tricu syntax sugar. The lower-level portable View Tree
--- form is shown in demos/viewContracts/complete.tri.
-
--- ============================================================================
--- 1. What's the problem?
--- ============================================================================
---
--- Programs grow by connecting definitions. A common mistake is connecting a
--- value with one shape to code that expects another shape:
---
---   a function expects Bool, but receives String
---   a function returns String, but its caller expects Bool
---   a list is expected to contain bytes, but contains strings
---
--- In a large program, those mistakes are often far away from where the bad value
--- was first introduced. View Contracts give tricu a portable way to check those
--- boundaries.
-
--- ============================================================================
--- 2. Views: useful built-in shapes
--- ============================================================================
---
--- A View is a description of the shape we expect at a boundary. tricu includes
--- built-in Views for common shapes such as:
---
---   Bool
---   String
---   Byte
---   Unit
---   List View
---   Maybe View
---   Pair View1 View2
---   Fn [View1] View2
---
--- tricu has unconventional but intuitive sugar for annotations:
---
---   name =@View value
---   function argument@View =@ResultView body
---
--- These examples are ordinary checked source definitions.
-
-message =@String "hello"
-
-names =@(List String) [("Ada") ("Grace")]
-
-chooseFirst left@String right@String =@String left
-
-stringIdentity =@(Fn [String] String) (x : x)
-
--- Uncommenting the below definition demonstrates a plain View mismatch:
---
---   bad =@Bool "not a Bool"
---
--- `tricu check` reports that the value is known as String where Bool was
--- required.
-
--- ============================================================================
--- 3. Why don't you just have Types?
--- ============================================================================
---
--- tricu is built on Tree Calculus. A defining feature of Tree Calculus is
--- intensionality: programs can inspect and construct program-shaped trees directly.
--- That intensional power is useful, but it makes ordinary sound static typing a
--- hard fit. A value can be both data and executable structure, and code can make
--- decisions based on tree shape in ways a conventional type checker may not be
--- able to predict soundly. This is an area of active research, not a settled 
--- claim that Tree Calculus languages cannot ever have useful typed variants.
---
--- View Contracts are not advertised as "the type system for tricu". They are
--- a practical contract layer: portable metadata plus checker/runtime boundaries
--- that catch many real mistakes while leaving the underlying language intact.
-
--- For more information about sound typing for Tree Calculus:
--- https://github.com/barry-jay-personal/typed_tree_calculus
-
--- ============================================================================
--- 4. What are the Contracts about, then?
--- ============================================================================
---
--- `List String` tells us that every element is a String. It does not tell us the
--- list has at least one element.
---
--- That matters for functions like `head`. Calling `head` on an empty list is a
--- bug. We want to express the stronger requirement:
---
---   this is a List String, and it is non-empty
---
--- That is what a guarded View is for.
-
--- A guard is ordinary tricu code. It receives the runtime value and returns:
---
---   guardOk value   -- accept the value
---   guardFail       -- reject the boundary
---
--- The guard does not write diagnostics. The checked runner reports where the
--- failing boundary came from.
-
-requireNonEmpty = (xs :
-  lazyBool
-    (_ : guardFail)
-    (_ : guardOk xs)
-    (emptyList? xs))
-
--- A user-defined View can be parameterized just like an ordinary function.
---
---   NonEmptyList String
---
--- means "a List String guarded by requireNonEmpty".
-
-NonEmptyList elem = viewGuarded (viewList elem) requireNonEmpty
-
--- ============================================================================
--- 5. Using a custom View in normal annotations
--- ============================================================================
---
--- This value satisfies the custom contract.
-
-contributors =@(NonEmptyList String) [("Ada") ("Grace")]
-
--- This function requires NonEmptyList String before its body can run. In a
--- library, this is the kind of contract you would put on an operation like
--- `head`: callers must prove the list is non-empty first.
-
-acceptNames xs@(NonEmptyList String) =@String "accepted non-empty names"
-
-primaryContributor =@String acceptNames contributors
-
--- Uncommenting this definition demonstrates a guarded View failure:
---
---   nobody =@(NonEmptyList String) []
---
--- The structure is fine (`[]` is a List String), but the runtime guard rejects
--- it because the list is empty.
-
--- ============================================================================
--- 6. Contracts protect callers too
--- ============================================================================
---
--- Contracts can describe function results as well as arguments. If a function
--- promises to return `NonEmptyList String`, checked execution guards that result
--- before callers depend on it.
-
-mkContributors name@String =@(NonEmptyList String) [(name)]
-
-fromSingleName =@String acceptNames (mkContributors "Evelyn")
-
--- Uncommenting this version would fail because the result contract is too
--- strong for the implementation:
---
---   badContributors name@String =@(NonEmptyList String) []
-
--- ============================================================================
--- 7. Writing your own Views and Contracts
--- ============================================================================
---
--- The pattern is:
---
---   1. Start with the closest structural View.
---   2. Write a guard for the runtime fact the structure cannot express.
---   3. Package them with viewGuarded.
---   4. Use the new View in normal annotations.
---
--- Examples of useful guarded Views:
---
---   NonEmptyList String
---   SortedList Byte
---   FixedLengthBytes 32
---   ValidUserId
---   NonEmptyString
---
--- Guards are intentionally runtime checks. Use plain Views for ordinary shape
--- checking, and guarded Views when a boundary really must enforce a stronger
--- invariant.
-
-main =@String primaryContributor

demos/viewContracts/README.md

@@ -1,137 +0,0 @@
-# View Contract Demos
-
-These demos exercise the finalized View Contract stack in `lib/view.tri`:
-portable View Trees/checkable typed-program nodes, structural View flow checks,
-runtime guarded Views, checked-exec, source annotations, and module-boundary
-View metadata.
-
-## End-user guide
-
-Start here. `demos/viewContracts.tri` is written with normal source annotation
-sugar and reads as a short guide to View Contracts: motivating structural
-mismatches, explaining plain Views, noting why this is not a full static type
-system, and building a custom `NonEmptyList` guarded View.
-
-```bash
-tricu check demos/viewContracts.tri
-```
-
-Expected output:
-
-```text
-ok
-```
-
-## Complete explicit demo
-
-`demos/viewContracts/complete.tri` shows the same layer from the portable
-View Tree/checkable-program side. It uses explicit builders such as
-`typedValue`, `typedRequire`, and `typedApply`, and demonstrates contextual guard
-diagnostics, observation composition, reachability, and malformed guard output.
-
-```bash
-tricu eval demos/viewContracts/complete.tri -f decode
-```
-
-## Portable checker self-tests
-
-Runs the checker self-test suite carried as ordinary `tricu` code.
-
-```bash
-tricu eval demos/viewContracts/selfTests.tri -f decode
-```
-
-Expected output is a list of `"ok"` strings.
-
-## Diagnostic rendering
-
-Shows a strict-mode structural View failure rendered for humans.
-
-```bash
-tricu eval demos/viewContracts/diagnostic.tri -f decode
-```
-
-Expected output:
-
-```text
-"symbol 162 expected List Bool but got List String"
-```
-
-## Stdlib-shaped contracts
-
-Checks successful higher-order contracts shaped like common stdlib APIs.
-
-```bash
-tricu eval demos/viewContracts/stdlibContracts.tri -f decode
-```
-
-Expected output:
-
-```text
-["ok", "ok", "ok", "ok", "ok"]
-```
-
-These examples are structural View checks, not runtime guarded checks.
-
-## Frontend emission layer
-
-`frontendEmission/` documents the portable artifact shape a frontend can emit
-after parsing/elaboration. The `*.source.txt` files are pseudo-source; the
-matching `*.emitted.tri` files are explicit typed-program builder output.
-
-This layer is still instructive because it shows the exact bridge between source
-syntax and portable View Tree/checkable metadata.
-
-## Source syntax sugar
-
-The `sourceSyntax/` demos use ergonomic annotations and the `tricu check`
-frontend. The frontend lowers annotations to the same typed-program nodes used by
-the explicit demos above, then executes checked-exec so guarded annotations fail
-through the portable runner.
-
-Successful check:
-
-```bash
-tricu check demos/viewContracts/sourceSyntax/success.tri
-```
-
-Expected output:
-
-```text
-ok
-```
-
-Labeled diagnostic check:
-
-```bash
-tricu check demos/viewContracts/sourceSyntax/failure.tri
-```
-
-Expected first failing diagnostic:
-
-```text
-symbol 4 (x) expected Bool but got String
-```
-
-If the first definition is fixed or removed, the later application-result
-failure demonstrates callee-aware labels:
-
-```text
-symbol 3 (g application result) expected String but got Bool
-```
-
-## Module boundary layer
-
-`modules/` shows producer-checked module export Views flowing into a consumer
-check as module-boundary evidence. During auto-build, annotated exports are
-checked before the module manifest alias is published. Consumers then use the
-manifest's View Contract metadata as assumptions, while compatibility is still
-judged by `lib/view.tri`.
-
-```bash
-tricu check demos/viewContracts/modules/success.tri
-# ok
-
-tricu check demos/viewContracts/modules/failure.tri
-# symbol 3 (Util.toString application result) expected Bool but got String
-```

demos/viewContracts/complete.tri

@@ -1,119 +0,0 @@
-!import "prelude" !Local
-!import "view" !Local
-
--- Complete explicit View Contract demo.
--- Run with: tricu eval demos/viewContracts/complete.tri -f decode
---
--- This file uses the low-level portable typed-program builders directly. It is
--- useful for understanding what source annotations lower to. For the end-user
--- guide, see demos/viewContracts.tri.
-
-requireNonEmpty = (xs :
-  lazyBool
-    (_ : guardFail)
-    (_ : guardOk xs)
-    (emptyList? xs))
-
-NonEmptyList = (elemView :
-  viewGuarded (viewList elemView) requireNonEmpty)
-
-checkedResult = (result :
-  matchResult
-    (diag env : renderDiagnostic diag)
-    (exec env :
-      matchResult
-        (runtimeDiag runtimeEnv : renderDiagnostic runtimeDiag)
-        (value runtimeEnv : value)
-        (runChecked exec))
-    result)
-
-checkedContract = (program :
-  checkedResult (checkTypedProgramWith policyStrict program))
-
-plainViewFailure =
-  matchResult
-    (diag env : renderDiagnostic diag)
-    (exec env : "unexpected-ok")
-    (checkTypedProgramWith
-      policyStrict
-      (typedProgram
-        0
-        [(typedValue 0 (viewList viewString) [("Ada")])
-         (typedRequire 0 (viewList viewBool) t)]))
-
-nonEmptyRootSuccess =
-  matchBool
-    "ok"
-    "unexpected-value"
-    (equal?
-      (checkedContract
-        (typedProgram
-          0
-          [(typedValue 0 (NonEmptyList viewString) [("Ada") ("Grace")])]))
-      [("Ada") ("Grace")])
-
-nonEmptyRootFailure =
-  checkedContract
-    (typedProgram
-      0
-      [(typedValue 0 (viewList viewString) [])
-       (typedRequire 0 (NonEmptyList viewString) [])])
-
-firstNameSuccess =
-  checkedContract
-    (typedProgram
-      2
-      [(typedValue 0 (viewFn [(NonEmptyList viewString)] viewString) (xs : head xs))
-       (typedValue 1 (viewList viewString) [("Ada") ("Grace")])
-       (typedApply 2 0 1 "Ada")
-       (typedRequire 2 viewString "Ada")])
-
-firstNameFailure =
-  checkedContract
-    (typedProgram
-      2
-      [(typedValue 0 (viewFn [(NonEmptyList viewString)] viewString) (xs : head xs))
-       (typedValue 1 (viewList viewString) [])
-       (typedApply 2 0 1 t)
-       (typedRequire 2 viewString t)])
-
-resultGuardFailure =
-  checkedContract
-    (typedProgram
-      2
-      [(typedValue 0 (viewFn [(viewString)] (NonEmptyList viewString)) (name : []))
-       (typedValue 1 viewString "Ada")
-       (typedApply 2 0 1 [])])
-
-observationComposition =
-  checkedContract
-    (typedProgram
-      0
-      [(typedValue 0 viewString "Ada")
-       (typedRequire 0 (viewGuarded viewString (x : guardOk (append x " Lovelace"))) "Ada")
-       (typedRequire 0 (viewGuarded viewString (x : guardOk (append x "!"))) "Ada")])
-
-unreachableGuard =
-  checkedContract
-    (typedProgram
-      0
-      [(typedValue 0 viewString "only the root is checked")
-       (typedValue 1 (viewList viewString) [])
-       (typedRequire 1 (NonEmptyList viewString) [])])
-
-malformedGuard =
-  checkedContract
-    (typedProgram
-      0
-      [(typedValue 0 (viewGuarded viewString (x : record 99 t)) "bad guard")])
-
-main = [
-  (append "plain View structural failure: " plainViewFailure)
-  (append "NonEmptyList root success: " nonEmptyRootSuccess)
-  (append "NonEmptyList root failure: " nonEmptyRootFailure)
-  (append "NonEmptyList function argument success: " firstNameSuccess)
-  (append "NonEmptyList function argument failure: " firstNameFailure)
-  (append "NonEmptyList function result failure: " resultGuardFailure)
-  (append "guard observations compose: " observationComposition)
-  (append "unreachable guard does not run: " unreachableGuard)
-  (append "malformed guard result: " malformedGuard)]

demos/viewContracts/diagnostic.tri

@@ -1,9 +0,0 @@
-!import "prelude" !Local
-!import "view" !Local
-!import "views.catalog" !Local
-
-main =
-  matchResult
-    (diag env : renderDiagnostic diag)
-    (env rest : "ok")
-    (checkTypedProgramWith policyStrict listMapWrongListArgContract)

demos/viewContracts/frontendEmission/README.md

@@ -1,116 +0,0 @@
-# Frontend Emission Demos
-
-These examples show the layer between source-level View annotations and the
-portable View Contract checker.
-
-Each `*.source.txt` file is pseudo-source: it is not parsed by `tricu`. It shows
-the information a frontend has after parsing/elaboration.
-
-Each matching `*.emitted.tri` file shows the lowered typed-program metadata that
-a frontend can emit today. A successful check returns checked-exec; these demos
-focus on structural Views, so they report `"ok"` as soon as metadata checking
-succeeds. Guarded programs should run the returned checked-exec with
-`runChecked`, as shown in `demos/viewContracts.tri` and by `tricu check`.
-
-## Successful map use
-
-Pseudo-source:
-
-```text
-map : Fn [Fn [Bool] String, List Bool] (List String)
-f   : Fn [Bool] String
-xs  : List Bool
-
-partial = map f
-out     = partial xs
-
-require out : List String
-```
-
-Run the emitted artifact:
-
-```bash
-tricu eval demos/viewContracts/frontendEmission/map-success.emitted.tri -f decode
-```
-
-Expected output:
-
-```text
-"ok"
-```
-
-## Wrong list argument
-
-Pseudo-source:
-
-```text
-map : Fn [Fn [Bool] String, List Bool] (List String)
-f   : Fn [Bool] String
-xs  : List String
-
-partial = map f
-out     = partial xs
-```
-
-Run:
-
-```bash
-tricu eval demos/viewContracts/frontendEmission/map-wrong-list.emitted.tri -f decode
-```
-
-Expected output:
-
-```text
-"symbol 162 expected List Bool but got List String"
-```
-
-## Wrong filter predicate
-
-Pseudo-source:
-
-```text
-filter : Fn [Fn [Bool] Bool, List Bool] (List Bool)
-pred   : Fn [Bool] String
-xs     : List Bool
-
-partial = filter pred
-out     = partial xs
-```
-
-Run:
-
-```bash
-tricu eval demos/viewContracts/frontendEmission/filter-wrong-predicate.emitted.tri -f decode
-```
-
-Expected output:
-
-```text
-"symbol 181 expected Fn [Bool] Bool but got Fn [Bool] String"
-```
-
-## Lowering shape
-
-A frontend does not need to expose `tricu` syntax internally. It only needs to
-emit portable typed-program nodes:
-
-```text
-typedValue symbol view term
-typedApply out callee arg term
-typedRequire symbol view term
-```
-
-The source-level flow:
-
-```text
-out = map f xs
-```
-
-lowers to curried Tree Calculus application nodes:
-
-```text
-typedApply partial map f partialTerm
-typedApply out partial xs outTerm
-```
-
-Function Views drive argument checking and result inference.

demos/viewContracts/frontendEmission/filter-wrong-predicate.emitted.tri

@@ -1,17 +0,0 @@
-!import "prelude" !Local
-!import "view" !Local
-!import "views.catalog" !Local
-
--- Lowering of filter-wrong-predicate.source.txt to portable typed-program metadata.
--- Symbols:
---   180 filter
---   181 pred
---   182 partial
-
-program = listFilterWrongPredicateContract
-
-main =
-  matchResult
-    (diag env : renderDiagnostic diag)
-    (env rest : "unexpected-ok")
-    (checkTypedProgramWith policyStrict program)

demos/viewContracts/frontendEmission/map-success.emitted.tri

@@ -1,20 +0,0 @@
-!import "prelude" !Local
-!import "view" !Local
-!import "views.catalog" !Local
-
--- Lowering of map-success.source.txt to portable typed-program metadata.
--- Symbols:
---   100 map
---   101 f
---   102 xs
---   103 partial
---   104 out
-
-program =
-  listMapUseContract viewBool viewString 100 101 102 103 104
-
-main =
-  matchResult
-    (diag env : renderDiagnostic diag)
-    (env rest : "ok")
-    (checkTypedProgramWith policyStrict program)

demos/viewContracts/frontendEmission/map-wrong-list.emitted.tri

@@ -1,19 +0,0 @@
-!import "prelude" !Local
-!import "view" !Local
-!import "views.catalog" !Local
-
--- Lowering of map-wrong-list.source.txt to portable typed-program metadata.
--- Symbols:
---   160 map
---   161 f
---   162 xs
---   163 partial
---   164 out
-
-program = listMapWrongListArgContract
-
-main =
-  matchResult
-    (diag env : renderDiagnostic diag)
-    (env rest : "unexpected-ok")
-    (checkTypedProgramWith policyStrict program)

demos/viewContracts/io-continuation.tri

@@ -1,30 +0,0 @@
-!import "prelude" !Local
-!import "io" !Local
-!import "view" !Local
-
--- View Contracts inside IO continuations
--- Run with:
---
---   tricu eval demos/viewContracts/io-continuation.tri --io -f decode
---
--- Checked IO evaluation instruments continuation bodies once from source
--- annotations. The IO runtime still executes ordinary interaction-tree actions;
--- the returned continuations already contain the checked-exec guard boundaries.
-
-requireNonEmpty = (xs :
-  lazyBool
-    (_ : guardFail)
-    (_ : guardOk xs)
-    (emptyList? xs))
-
-NonEmptyList elem = viewGuarded (viewList elem) requireNonEmpty
-
-acceptNames xs@(NonEmptyList String) =@String "accepted"
-
-useHandler handler@(Fn [(NonEmptyList String)] String) xs@(List String) =@String
-  handler xs
-
--- The IO action yields an empty list. The higher-order boundary requires a
--- handler that accepts NonEmptyList String, so the continuation-internal pure
--- call fails before returning the next IO value.
-main = io (bind (pure []) (xs : pure (useHandler acceptNames xs)))

demos/viewContracts/io.tri

@@ -1,51 +0,0 @@
-!import "prelude" !Local
-!import "io" !Local
-!import "view" !Local
-
--- View Contracts + IO interaction trees
--- Run with:
---
---   tricu eval demos/viewContracts/io.tri --io -f decode
---
--- The IO runtime expects the top-level value to be an interaction tree wrapped
--- by the `io` sentinel:
---
---   pair "tricuIO" (pair version action)
---
--- View Contracts can validate that boundary before the IO driver starts. The IO
--- value is still just an interaction tree; this demo only checks how it was
--- exposed.
-
-ioSentinel? = (value :
-  and?
-    (equal? (fst value) "tricuIO")
-    (equal? (fst (snd value)) 1))
-
-requireIO = (value :
-  lazyBool
-    (_ : guardOk value)
-    (_ : guardFail)
-    (ioSentinel? value))
-
--- A first useful IO View is intentionally shallow:
---
---   viewAny             -- accept any payload structurally
---   requireIO sentinel  -- require the top-level IO wrapper at runtime
---
--- This does not prove every future continuation step is well-formed. It proves
--- the checked program exposes an IO interaction tree to the host driver.
-viewIO = viewGuarded viewAny requireIO
-
-checkedIO = (action :
-  matchResult
-    (diag env : io (pure (renderDiagnostic diag)))
-    (exec env :
-      matchResult
-        (runtimeDiag runtimeEnv : io (pure (renderDiagnostic runtimeDiag)))
-        (value runtimeEnv : value)
-        (runChecked exec))
-    (checkTypedProgramWith
-      policyStrict
-      (typedProgram 0 [(typedValue 0 viewIO action)])))
-
-main = checkedIO (io (pure "checked interaction tree"))

demos/viewContracts/modules/README.md

@@ -1,17 +0,0 @@
-# Module View Contract demo
-
-This demo shows producer-checked module export Views flowing into a consumer
-check as trusted View Contract evidence.
-
-```sh
-tricu check demos/viewContracts/modules/success.tri
-# ok
-
-tricu check demos/viewContracts/modules/failure.tri
-# symbol 3 (Util.toString application result) expected Bool but got String
-```
-
-`util.tri` is a local workspace module. During auto-build, its annotated exports
-are checked before the module manifest alias is published. The consumer then
-uses the manifest's View Contract metadata and View Tree export artifacts as
-module-boundary assumptions; compatibility is still judged by `lib/view.tri`.

demos/viewContracts/modules/failure.tri

@@ -1,3 +0,0 @@
-!import "vc.demo.util" Util
-
-foo x@Bool =@Bool Util.toString x

demos/viewContracts/modules/success.tri

@@ -1,3 +0,0 @@
-!import "vc.demo.util" Util
-
-foo x@Bool =@Bool Util.id x

demos/viewContracts/modules/tricu.workspace

@@ -1 +0,0 @@
-module vc.demo.util = util.tri

demos/viewContracts/modules/util.tri

@@ -1,2 +0,0 @@
-id x@Bool =@Bool x
-toString x@Bool =@String "ok"

demos/viewContracts/selfTests.tri

@@ -1,3 +0,0 @@
-!import "views.catalog" !Local
-
-main = viewCatalogSelfTests

demos/viewContracts/sourceSyntax/failure.tri

@@ -1,9 +0,0 @@
--- Source-level View Contract diagnostic demo.
--- Run with: tricu check demos/viewContracts/sourceSyntax/failure.tri
-
-makeBool x@String =@Bool x
-
-xs =@(List String) [(g "hi")]
-g y@String =@Bool y
-
-main = "if you're seeing this instead of an error, you ran the file unchecked"

demos/viewContracts/sourceSyntax/success.tri

@@ -1,10 +0,0 @@
--- Source-level View Contract syntax sugar demo.
--- Run with: tricu check demos/viewContracts/sourceSyntax/success.tri
-
-message =@String "hello"
-
-boxedMessages =@(Maybe (List String)) just [(message) ("world")]
-
-chooseFirst x@String y@Byte =@String x
-
-fromLambda =@(Fn [String] String) (x : x)

demos/viewContracts/stdlibContracts.tri

@@ -1,10 +0,0 @@
-!import "prelude" !Local
-!import "view" !Local
-!import "views.catalog" !Local
-
-main = [
-  (typedContractCheck listMapBoolStringContract)
-  (typedContractCheck headMaybeBoolContract)
-  (typedContractCheck listFilterBoolContract)
-  (typedContractCheck listFoldStringBoolContract)
-  (typedContractCheck listMapMaybeBoolStringContract)]

docs/content-store-and-module-format.md

@@ -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
+      contract: optional
-        kind: <view artifact kind>
+        kind: arboricx.tree-term.v1
-        hash: <view artifact hash>
+        hash: <contract term hash>
-      catalog: optional
-        kind: <view catalog kind>
-        hash: <view catalog 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:
+contract:
-  kind: arboricx.view-contract.type.v1
+  kind: arboricx.tree-term.v1
-  hash: <view type hash>
+  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
+Contracts are ordinary `tricu` functions `Tree -> Result Tree Tree`. They are
-as content objects and referenced by module exports. `tricu` may emit these
+stored and referenced as ordinary `arboricx.tree-term.v1` objects. There is no
-objects, but the object kind is not tricu-specific.
+separate contract object kind.
 
-Current artifact kind:
+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
-```text
+result convention and the boundary helpers; it does not define a binary contract
-arboricx.view-contract.type.v1
+grammar.
-```
-
-`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>
-```
 
 ### 9.1 Export-level pairing
 
-The module manifest is the canonical pairing of an executable export and its
+The module manifest pairs each export with an optional contract object:
-advertised contract:
 
 ```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:
+This prevents the executable and its advertised contract from drifting apart.
-
-```text
-map -> tree A
-map.view -> contract B
-```
-
-where aliases might be retargeted independently.
 
 ### 9.2 Import checking
 
-When a source file imports a module, a frontend can resolve an imported export,
+When a source file imports a contracted export, the frontend loads the contract
-decode its direct `arboricx.view-contract.type.v1` ref, and emit typed program
+object and applies it at the boundary using the standard contract helpers. For
-evidence locally:
+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
+For locally built workspace modules, advertised export contracts may be checked
-before the module manifest alias is published, including imported view facts from
+before the manifest is published. For external or prebuilt manifests, the
-dependencies used by the producer source. External or prebuilt manifests are
+advertised contract is a trusted boundary declaration; the consumer may insert
-trusted boundary declarations for now; they are not accompanied by proof objects.
+guard wrappers as needed.
-The checker still consumes only local numeric symbols and typed-program evidence.
-Global content hashes do not become checker symbols.
 
-Correct split:
+The contract term itself is the authority. There is no separate checker binary
+format and no typed-program evidence graph.
 
-```text
+### 9.3 Execution hydration versus contract checking
-local checker symbol: 3
-presentation label:   "List.map"
-resolved object:      sha256:...
-exported view:        Fn [...]
-```
 
-### 9.3 Execution hydration versus contract evidence
+Execution imports use a narrow path:
-
-Execution imports should use a narrow, demand-driven path:
 
 ```text
 module import -> selected executable exports -> hydrate selected tree-term objects
 ```
 
-This path should not compute a dependency closure over other module exports.
+Contract-aware imports use a slightly broader path:
-Each selected executable export is already a complete Tree Calculus value.
-
-Contract-aware checking may use a 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
+Because contract objects are ordinary tree terms, they can be reused, composed,
-the Tree Calculus checker. typed programs and reusable catalogs do not need their
+and stored with the same tools as any other value.
-own binary object kinds today: they are ordinary Tree Calculus data and can be
-stored as `arboricx.tree-term.v1` when persistence is useful.
 
 ## 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
+  immutable manifests pairing export names with object refs and optional
-  Contract refs
+  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.

docs/contracts.md

@@ -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.

docs/guard-injection.md

@@ -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.

docs/module-system-design.md

@@ -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
+The store may integrate with Contracts because a contract is itself an ordinary
-format are pure Tree Calculus / portable tree data. View Contracts are not a
+Tree Calculus term. Contracts are not a Haskell-private or `tricu`-private
-Haskell-private or `tricu`-private semantic layer.
+semantic layer.
 
-The module resolver may emit typed-program evidence, but checker semantics remain
+A module manifest may reference a contract object, but the contract is evaluated
-unchanged:
+by ordinary Tree Calculus reduction, not by a special checker.
-
-```text
-Haskell emits evidence.
-tricu judges evidence.
-```
 
 ### 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
+Contract Term
-  portable evidence/checker data over tree artifacts
+  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
+Contracts are ordinary tree-valued functions; `tricu` produces and consumes those
-those formats.
+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
+Contract checking is a runtime boundary check. It may load exported contract term
-exported direct view types for the symbols that participate in a check. That
+objects for the symbols that participate in a boundary. That slower path remains
-slower path must remain behind the typed program boundary:
+separate from execution hydration:
 
 ```text
-Haskell emits evidence.
+Haskell loads contract terms.
-tricu judges evidence.
+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
+For locally built workspace modules, advertised direct export contracts may be
-producer-checked before the manifest alias is written. Producer checking includes
+checked before the manifest alias is written. Producer checking includes
-advertised views from any imported modules used by that source, so a module
+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
+Consumer checking then resolves selected module exports and loads their exported
-`arboricx.view-contract.type.v1` refs, and emits trusted `KnownView` evidence
+contract term objects. Those contracts are applied at the import boundary using
-for the local imported symbols. Those facts are module-boundary assumptions:
+the standard contract helpers. For external or prebuilt manifests, the advertised
-local workspace builds create them after producer-side checking, while external
+contract is a trusted boundary declaration; the consumer may still re-apply it at
-or prebuilt manifests are trusted inputs for now. In all cases, compatibility
+the boundary.
-with local requirements is still judged by the portable checker in `lib/view.tri`.
 
 ## 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
+A module manifest pairs each export name with its compiled tree term and an
-typed program. Its global identity remains a content hash or module export ref.
+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
+Local source name: "List.map"
-Debug label: "List.map"
 Resolved object:    sha256:...
-Exported view: Fn [...]
+Exported contract:  sha256:...
 ```
 
-De Bruijn-style integer symbols are still appropriate inside a typed program. They
+There is no typed-program evidence graph and no local numeric checker symbols.
-are local evidence identifiers, not global content identity.
+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 has no
-
+contract information, it simply performs no runtime check. We should not pretend
-Untyped code remains valid with no contract artifact. If a boundary needs to
+that untyped functions have an implicit `Any -> Any -> ...` contract.
-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.
 
 ## 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:
+Contracts:
-  portable evidence artifacts attached to exports and checked by pure Tree
+  ordinary tree-valued functions attached to exports and applied by pure Tree
-  Calculus code
+  Calculus reduction at boundaries
 ```
 
 The key architectural rule is that hashes provide stable identity, while names

docs/view-contract-syntax.md

@@ -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.

docs/view-contracts.md

@@ -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.

lib/base.tri

@@ -39,10 +39,10 @@ snd p = matchPair takeSecond p
   where takeSecond a b = b
 
 resultIsOk result =
-  matchResult (err rest : false) (val rest : true) result
+  matchResult (errR rest : false) (val rest : true) result
 
 resultIsErr result =
-  matchResult (err rest : true) (val rest : false) result
+  matchResult (errR rest : true) (val rest : false) result
 
 not? = matchBool false true
 and? = matchBool id (_ : false)
@@ -176,7 +176,7 @@ andLazy? = (a bK :
     bK
     (_ : false))
 
-pred = y (self : triage
+pred_ = y (self : triage
   0
   0
   (bit rest :
@@ -188,81 +188,90 @@ pred = y (self : triage
         rest)
       (_ : t (t t) (self rest))))
 
-isZero? = triage true (_ : false) (_ _ : false)
+pred @nat? =@nat? pred_
 
-add = y (self x y :
+isZero_? = triage true (_ : false) (_ _ : false)
+
+isZero? @nat? =@bool? isZero_?
+
+add @nat? @nat? =@nat? (y (self x y :
   triage
     y
     (_ : succ y)
-    (_ _ : succ (self (pred x) y))
+    (_ _ : succ (self (pred_ x) y))
-    x)
+    x))
 
-sub = y (self a b :
+sub @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : a)
-    (_ : self (pred a) (pred b)))
+    (_ : self (pred_ a) (pred_ b)))
 
-lte? = y (self a b :
+lte_? = y (self a b :
   ifLazy
-    (isZero? a)
+    (isZero_? a)
     (_ : true)
     (_ :
       ifLazy
-        (isZero? b)
+        (isZero_? b)
         (_ : false)
-        (_ : self (pred a) (pred b))))
+        (_ : self (pred_ a) (pred_ b))))
 
-gte? = a b :
+lte? @nat? @nat? =@bool? lte_?
-  lte? b a
 
-lt? = a b :
+gte_? = a b : lte_? b a
-  and? (lte? a b) (not? (equal? a b))
 
-gt? = a b :
+gte? @nat? @nat? =@bool? gte_?
-  lt? b a
 
-mul = y (self a b :
+lt_? = a b : and? (lte_? a b) (not? (equal? a b))
+
+lt? @nat? @nat? =@bool? lt_?
+
+gt_? = a b : lt_? b a
+
+gt? @nat? @nat? =@bool? gt_?
+
+mul @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : 0)
-    (_ : add a (self a (pred b))))
+    (_ : add a (self a (pred_ b))))
 
-div = y (self a b :
+div @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : 0)
     (_ : ifLazy
-      (lt? a b)
+      (lt_? a b)
       (_ : 0)
       (_ : succ (self (sub a b) b))))
 
-mod = y (self a b :
+mod @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : 0)
     (_ : ifLazy
-      (lt? a b)
+      (lt_? a b)
       (_ : a)
       (_ : self (sub a b) b)))
 
-pow = y (self a b :
+pow @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : 1)
-    (_ : mul a (self a (pred b))))
+    (_ : mul a (self a (pred_ b))))
 
 even? n = (triage
   true
   (_ : false)
-  (bit _ : isZero? bit)
+  (bit _ : isZero_? bit)
   n)
 
 odd? = (n : not? (even? n))
 
-min = (a b : ifLazy (lte? a b) (_ : a) (_ : b))
+min @nat? @nat? =@nat? (a b : ifLazy (lte_? a b) (_ : a) (_ : b))
 
-max = (a b : ifLazy (lte? a b) (_ : b) (_ : a))
+max @nat? @nat? =@nat? (a b : ifLazy (lte_? a b) (_ : b) (_ : a))
 
 -- ---------------------------------------------------------------------------
 -- Result combinators
@@ -291,3 +300,623 @@ resultMapErr = (f result :
     (code rest : err (f code) rest)
     (value rest : ok value rest)
     result)
+
+-- ---------------------------------------------------------------------------
+-- List
+-- ---------------------------------------------------------------------------
+
+matchList = a b : triage a _ b
+
+emptyList? = matchList true (_ _ : false)
+head xs@(nonEmptyListOf anyC) =@anyC matchList t (h _ : h) xs
+tail xs@(nonEmptyListOf anyC) =@(listOf anyC) matchList t (_ r : r) xs
+
+append_ self xs ys =
+  matchList
+    ys
+    (h r : pair h (self r ys))
+    xs
+append = xs ys : y append_ xs ys
+
+lExist?_ self x xs =
+  matchList
+    false
+    (h r : or? (equal? x h) (self x r))
+    xs
+lExist? = x xs : y lExist?_ x xs
+
+map_ self l f =
+  matchList
+    t
+    (h r : pair (f h) (self r f))
+    l
+map = f l : y map_ l f
+
+filter_ self l f =
+  matchList
+    t
+    (h r :
+      matchBool
+        (pair h (self r f))
+        (self r f)
+        (f h))
+    l
+filter = f l : y filter_ l f
+
+foldl_ self l f acc =
+  matchList
+    acc
+    (h r : self r f (f acc h))
+    l
+foldl = f x l : y foldl_ l f x
+
+foldr_ self l f x =
+  matchList
+    x
+    (h r : f (self r f x) h)
+    l
+foldr = f x l : y foldr_ l f x
+
+length_ self xs =
+  matchList
+    0
+    (_ r : succ (self r))
+    xs
+length @(listOf anyC) =@nat? y length_
+
+reverse_ self xs acc =
+  matchList
+    acc
+    (h r : self r (pair h acc))
+    xs
+reverse = xs : y reverse_ xs t
+
+snoc_ self x xs =
+  matchList
+    (pair x t)
+    (h r : pair h (self x r))
+    xs
+snoc = x xs : y snoc_ x xs
+
+count_ self x xs =
+  matchList
+    0
+    (h r :
+      matchBool
+        (succ (self x r))
+        (self x r)
+        (equal? x h))
+    xs
+count = x xs : y count_ x xs
+
+last_ self xs =
+  matchList
+    t
+    (h r :
+      matchBool
+        h
+        (self r)
+        (emptyList? r))
+    xs
+last @(nonEmptyListOf anyC) =@anyC y last_
+
+all?_ self pred xs =
+  matchList
+    true
+    (h r : and? (pred h) (self pred r))
+    xs
+all? = pred xs : y all?_ pred xs
+
+any?_ self pred xs =
+  matchList
+    false
+    (h r : or? (pred h) (self pred r))
+    xs
+any? = pred xs : y any?_ pred xs
+
+intersect = xs ys : filter (x : lExist? x ys) xs
+
+nth_ self xs n i =
+  matchList
+    t
+    (h r :
+      matchBool
+        h
+        (self r n (succ i))
+        (equal? i n))
+    xs
+nth = n xs : y nth_ xs n 0
+
+headMaybe = matchList nothing (h _ : just h)
+
+lastMaybe_ self xs =
+  matchList
+    nothing
+    (h r :
+      matchBool
+        (just h)
+        (self r)
+        (emptyList? r))
+    xs
+lastMaybe = xs : y lastMaybe_ xs
+
+nthMaybe_ self xs n i =
+  matchList
+    nothing
+    (h r :
+      matchBool
+        (just h)
+        (self r n (succ i))
+        (equal? i n))
+    xs
+nthMaybe = n xs : y nthMaybe_ xs n 0
+
+take_ self xs n i =
+  matchList
+    t
+    (h r :
+      matchBool
+        t
+        (pair h (self r n (succ i)))
+        (equal? i n))
+    xs
+take = n xs : y take_ xs n 0
+
+drop_ self xs n i =
+  matchBool
+    xs
+    (matchList
+      t
+      (_ r : self r n (succ i))
+      xs)
+    (equal? i n)
+drop = n xs : y drop_ xs n 0
+
+splitAt = n xs : pair (take n xs) (drop n xs)
+
+concatMap_ self f xs =
+  matchList
+    t
+    (h r : append (f h) (self f r))
+    xs
+concatMap = f xs : y concatMap_ f xs
+
+find_ self pred xs =
+  matchList
+    nothing
+    (h r :
+      matchBool
+        (just h)
+        (self pred r)
+        (pred h))
+    xs
+find = pred xs : y find_ pred xs
+
+partition_ self pred xs trues falses =
+  matchList
+    (pair (reverse trues) (reverse falses))
+    (h r :
+      matchBool
+        (self pred r (pair h trues) falses)
+        (self pred r trues (pair h falses))
+        (pred h))
+    xs
+partition = pred xs : y partition_ pred xs t t
+
+strLength = length
+strAppend = append
+strEq? = equal?
+strEmpty? = emptyList?
+
+startsWith?_ self prefix input =
+  matchList
+    true
+    (ph pr :
+      matchList
+        false
+        (sh sr :
+          matchBool
+            (self pr sr)
+            false
+            (equal? ph sh))
+        input)
+    prefix
+startsWith? = prefix input : y startsWith?_ prefix input
+
+endsWith? = prefix str : startsWith? (reverse prefix) (reverse str)
+
+contains?_ self needle haystack =
+  matchBool
+    true
+    (matchList
+      false
+      (_ r : self needle r)
+      haystack)
+    (startsWith? needle haystack)
+contains? = needle haystack : y contains?_ needle haystack
+
+sum @(listOf nat?) =@nat? foldl (acc x : add x acc) 0
+product @(listOf nat?) =@nat? foldl (acc x : mul x acc) 1
+
+-- ---------------------------------------------------------------------------
+-- Generic separators
+--
+-- `lines`, `unlines`, `words` and `unwords` at the bottom of this section are
+-- the byte-valued special cases of these primitives.
+--
+-- Joining takes any separator; splitting takes one byte. Separators are removed
+-- rather than kept, and empty fields are preserved.
+-- ---------------------------------------------------------------------------
+
+takeWhile_ self xs f =
+  lazyList
+    (_ : t)
+    (h r :
+      lazyBool
+        (_ : pair h (self r f))
+        (_ : t)
+        (f h))
+    xs
+takeWhile = f xs : y takeWhile_ xs f
+
+dropWhile_ self xs f =
+  lazyList
+    (_ : t)
+    (h r :
+      lazyBool
+        (_ : self r f)
+        (_ : pair h r)
+        (f h))
+    xs
+dropWhile = f xs : y dropWhile_ xs f
+
+-- Byte-level whitespace only: space and horizontal tab (HTTP OWS).
+spaceByte? = b : equal? b 32
+tabByte?   = b : equal? b 9
+trimByte?  = b : or? (spaceByte? b) (tabByte? b)
+
+trim = xs : dropWhile trimByte? (reverse (dropWhile trimByte? (reverse xs)))
+
+intercalate_ self xs sep =
+  lazyList
+    (_ : t)
+    (h r :
+      lazyBool
+        (_ : h)
+        (_ : append h (append sep (self r sep)))
+        (emptyList? r))
+    xs
+intercalate = sep xs : y intercalate_ xs sep
+
+-- Separator after every field, including the last one. Line-oriented formats
+-- want this: `joinSuffix "\n" xs` terminates the final line while
+-- `intercalate "\n" xs` does not.
+joinSuffix_ self xs sep =
+  lazyList
+    (_ : t)
+    (h r : append (append h sep) (self r sep))
+    xs
+joinSuffix = sep xs : y joinSuffix_ xs sep
+
+-- Split on a single byte. 
+-- Empty fields are preserved: `splitOnByte 58 "a::b"` is ["a" "" "b"].
+splitByte_ self str byte acc current =
+  lazyList
+    (_ : map reverse (reverse (pair current acc)))
+    (h r :
+      lazyBool
+        (_ : self r byte (pair current acc) t)
+        (_ : self r byte acc (pair h current))
+        (equal? h byte))
+    str
+splitOnByte = byte str : y splitByte_ str byte t t
+
+-- Every one of these keeps its arguments bound: partially applying a
+-- multi-argument function at the top level leaves a fixed point exposed.
+lines   = str : splitOnByte 10 str
+unlines = xs : joinSuffix "\n" xs
+
+-- Runs of separators collapse: empty fields are dropped.
+words   = str : filter (w : not? (emptyList? w)) (splitOnByte 32 str)
+unwords = xs : intercalate " " xs
+
+zipWith_ self f xs ys =
+  matchList
+    t
+    (xh xt :
+      matchList
+        t
+        (yh yt : pair (f xh yh) (self f xt yt))
+        ys)
+    xs
+zipWith = f xs ys : y zipWith_ f xs ys
+
+-- ---------------------------------------------------------------------------
+-- Core contract type
+--
+-- A contract is an ordinary tricu function: Tree -> Tree -> Result Tree Tree.
+-- The second argument is the conventional "rest" slot. On success a contract
+-- returns the checked value wrapped in the standard ok shape; on failure it
+-- returns a diagnostic wrapped in the standard err shape.
+--
+-- The contract kernel is a globally configurable function selected by the
+-- runner. It decides whether to accept the contract result, replace it, log
+-- it, or transform the diagnostic. The default kernel is the identity on the
+-- contract Result.
+--
+-- The runner may rebind 'kernel' to a different kernel before evaluating
+-- user code (e.g. via --contract-kernel).
+-- ---------------------------------------------------------------------------
+
+contractOk = (value : (rest : ok value rest))
+contractErr = (msg : (rest : err msg rest))
+
+-- Default contract kernel. Return the contract Result unchanged.
+defaultKernel = (contract value result :
+  matchResult
+    (msg rest : err msg rest)
+    (v rest : ok v rest)
+    result)
+
+-- The active kernel. The runner may rebind this name to a different kernel
+-- before evaluating user code (e.g. via --contract-kernel). Internally,
+-- withContract dispatches through this binding, so rebinding 'kernel' changes
+-- the behaviour of every contract boundary in the program.
+kernel = defaultKernel
+
+-- Skip-everything kernel. Resume with the original value on failure.
+skipKernel = (contract value result :
+  matchResult
+    (msg rest : ok value rest)
+    (v rest : ok v rest)
+    result)
+
+-- Apply a contract and pass the raw Result to the kernel.
+withContract = (contract value :
+  kernel contract value (contract value t))
+
+-- Apply a contract and return the checked value or the diagnostic message.
+check contract value =
+  matchResult
+    (msg _ : msg)
+    (v _ : v)
+    (withContract contract value)
+
+-- Apply a contract and return the raw Result (kernel is bypassed).
+checkContract = (contract value : contract value t)
+
+-- ---------------------------------------------------------------------------
+-- Basic contracts
+-- ---------------------------------------------------------------------------
+
+-- Any value passes.
+anyC = (value : contractOk value)
+
+-- Always fails with the supplied message.
+neverC = (msg : (value : contractErr msg))
+
+-- Build a contract from a predicate that inspects only the value.
+guardC = (msg predicate value rest :
+  lazyBool
+    (_ : contractOk value rest)
+    (_ : contractErr msg rest)
+    (predicate value))
+
+-- Structural natural-number predicate.
+-- A natural is either Leaf (0) or Fork bit rest where bit is Leaf (even)
+-- or Stem Leaf (odd) and rest is itself a natural.
+isNat? = y (self n :
+  triage
+    true
+    (_ : false)
+    (bit r :
+      triage
+        (self r)
+        (_ : self r)
+        (_ _ : false)
+        bit)
+    n)
+
+-- Natural number contract.
+nat? = guardC "not a natural number" isNat?
+
+-- Non-zero natural number contract.
+nonZero? = guardC "non-zero" (n : and? (isNat? n) (not? (isZero_? n)))
+
+-- Boolean contract.
+bool? = guardC "not a boolean" (b : or? (equal? b true) (equal? b false))
+
+-- ---------------------------------------------------------------------------
+-- Contract combinators
+-- ---------------------------------------------------------------------------
+
+andC = (c1 c2 value rest :
+  matchResult
+    (msg _ : contractErr msg rest)
+    (v _ : c2 v rest)
+    (c1 value rest))
+
+orC = (c1 c2 value rest :
+  matchResult
+    (msg _ : c2 value rest)
+    (v _ : contractOk v rest)
+    (c1 value rest))
+
+notC = (c value rest :
+  matchResult
+    (msg _ : contractOk value rest)
+    (_ _ : contractErr "notC: predicate succeeded" rest)
+    (c value rest))
+
+mapC = (f c value rest :
+  matchResult
+    (msg _ : contractErr msg rest)
+    (v _ : contractOk (f v) rest)
+    (c value rest))
+
+bindC = (c f value rest :
+  matchResult
+    (msg _ : contractErr msg rest)
+    (v _ : f v value rest)
+    (c value rest))
+
+-- ---------------------------------------------------------------------------
+-- Collection contracts
+-- ---------------------------------------------------------------------------
+
+listOf = (c value rest :
+  y (self orig xs :
+    matchList
+      (contractOk orig rest)
+      (h r :
+        matchResult
+          (msg _ : contractErr msg rest)
+          (_ _ : self orig r)
+          (c h rest))
+      xs) value value)
+
+nonEmptyListOf = (c :
+  andC (guardC "empty list" (xs : not? (emptyList? xs))) (listOf c))
+
+pairOf = (c1 c2 p rest :
+  matchPair
+    (a b :
+      matchResult
+        (msg _ : contractErr msg rest)
+        (a' _ :
+          matchResult
+            (msg _ : contractErr msg rest)
+            (b' _ : contractOk (pair a' b') rest)
+            (c2 b rest))
+        (c1 a rest))
+    p)
+
+-- ---------------------------------------------------------------------------
+-- Higher-order function contracts
+--
+-- These return a Result-wrapped proxy. The proxy itself is a contract: it
+-- checks arguments on the way in and results on the way out.
+-- ---------------------------------------------------------------------------
+
+fnContract = (argC resC f rest :
+  contractOk
+    (x : (rest1 :
+      matchResult
+        (msg _ : contractErr msg rest1)
+        (x' _ :
+          matchResult
+            (msg _ : contractErr msg rest1)
+            (y _ : contractOk y rest1)
+            (withContract resC (f x')))
+        (withContract argC x)))
+    rest)
+
+fn2 = (arg1C arg2C resC f rest :
+  contractOk
+    (x : (rest1 :
+      matchResult
+        (msg _ : contractErr msg rest1)
+        (x' _ :
+          contractOk
+            (y : (rest2 :
+              matchResult
+                (msg _ : contractErr msg rest2)
+                (y' _ :
+                  matchResult
+                    (msg _ : contractErr msg rest2)
+                    (z _ : contractOk z rest2)
+                    (withContract resC (f x' y')))
+                (withContract arg2C y)))
+            rest1)
+        (withContract arg1C x)))
+    rest)
+
+-- ---------------------------------------------------------------------------
+-- Interaction-tree effect layer
+--
+-- These constructors and combinators layer catchable, composable failures on
+-- top of the core Result contracts. They reuse the same tags as tricu IO:
+--   0 = pureE
+--   1 = bindE
+--   2 = exceptE
+-- ---------------------------------------------------------------------------
+
+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
+
+-- Lift a contract failure into an interaction tree.
+checkM = (contract value :
+  matchResult
+    (msg _ : exceptE "contract" msg (_ : pureE t))
+    (checked _ : pureE checked)
+    (contract value t))
+
+-- Lift a pure function into the interaction tree.
+liftM = (f : (x : pureE (f x)))
+
+-- Interpret a pure interaction tree into a Result.
+runM = (tree :
+  run tree
+  where run =
+          y (self tree :
+            matchPair
+              (op payload :
+                matchBool
+                  -- pureE
+                  (contractOk (snd tree) t)
+                  (matchBool
+                    -- bindE
+                    (matchPair
+                      (action k :
+                        matchResult
+                          (msg _ : contractErr msg t)
+                          (v _ : self (k v))
+                          (self action))
+                      payload)
+                    -- exceptE
+                    (matchPair
+                      (tag pair :
+                        matchPair
+                          (value k :
+                            contractErr value t)
+                          pair)
+                      payload)
+                    (equal? op 1))
+                  (equal? op 0))
+              tree))
+
+-- Handle matching exceptE nodes by applying the handler to the value and the
+-- resumption continuation. Non-matching exceptions are left in place.
+handleM = (tag handler tree :
+  handle tree
+  where handle =
+          y (self tree :
+            matchPair
+              (op payload :
+                matchBool
+                  -- pureE
+                  tree
+                  (matchBool
+                    -- bindE
+                    (matchPair
+                      (action k :
+                        bindE (self action) (v : self (k v)))
+                      payload)
+                    -- exceptE
+                    (matchPair
+                      (et pair :
+                        matchPair
+                          (value k :
+                            matchBool
+                              (self (handler value k))
+                              tree
+                              (equal? et tag))
+                          pair)
+                      payload)
+                    (equal? op 1))
+                  (equal? op 0))
+              tree))

lib/bytes.tri

@@ -1,5 +1,4 @@
 !import "base" !Local
-!import "list" !Local
 
 bytesNil? = emptyList?
 

lib/conversions.tri

@@ -1,5 +1,4 @@
 !import "base" !Local
-!import "list" !Local
 
 incDecRev = y (self : matchList
   "1"

lib/http.tri

@@ -152,7 +152,7 @@ responseForMethod = (method resp :
 -- ---------------------------------------------------------------------------
 
 recvUntilMax_ = (y (self sock pattern maxBytes acc accLen :
-  onResult_ (recv sock 1)
+  onResult_ (recv sock 4096)
     (err :
       pure (err 400 acc))
     (chunk :

lib/intensionalContracts.tri

@@ -0,0 +1,53 @@
+!import "prelude" !Local
+
+-- Structural contracts that exploit Tree Calculus's intensional nature.
+-- These are not simple type tags; they recursively inspect the tree shape.
+
+-- Any value that is not Leaf.
+nonEmptyTree? = guardC "empty tree" (x : not? (isZero? x))
+
+-- Every internal node is a Fork with two children; Stems are not allowed.
+fullTree? = guardC "not a full binary tree"
+  (y (self x :
+    triage
+      true
+      (_ : false)
+      (l r : and? (self l) (self r))
+      x))
+
+-- Even and odd number contracts that inspect the LSB bit tree.
+evenC? = guardC "not even" even?
+oddC?  = guardC "not odd" odd?
+
+-- A power of two has exactly one '1' bit in its LSB encoding.
+powerOfTwo? = guardC "not a power of two"
+  (y (self n :
+    triage
+      false
+      true
+      (bit rest :
+        matchBool
+          (self rest)
+          false
+          (isZero? bit))
+      n))
+
+-- A string (list of numbers) where every code point is in the ASCII range.
+asciiString? = listOf
+  (guardC "non-ascii byte" (n : and? (gte? n 0) (lte? n 127)))
+
+-- Check that a list of numbers is sorted in ascending order.
+-- The element contract parameter is applied separately by listOf.
+isSorted_ = (self xs :
+  matchList
+    true
+    (h r :
+      matchBool
+        (self r)
+        false
+        (matchList true (h2 _ : lte? h h2) r))
+    xs)
+
+isSorted = y isSorted_
+
+sortedList? = (c : andC (listOf c) (guardC "not sorted" isSorted))

lib/list.tri

@@ -1,339 +0,0 @@
-!import "base" !Local
-
-_ = t
-
-matchList = a b : triage a _ b
-
-emptyList? = matchList true (_ _ : false)
-head = matchList t (head _ : head)
-tail = matchList t (_ tail : tail)
-
-append_ self xs ys =
-  matchList
-    ys
-    (h r : pair h (self r ys))
-    xs
-append = xs ys : y append_ xs ys
-
-lExist?_ self x xs =
-  matchList
-    false
-    (h r : or? (equal? x h) (self x r))
-    xs
-lExist? = x xs : y lExist?_ x xs
-
-map_ self l f =
-  matchList
-    t
-    (h r : pair (f h) (self r f))
-    l
-map = f l : y map_ l f
-
-filter_ self l f =
-  matchList
-    t
-    (h r :
-      matchBool
-        (pair h (self r f))
-        (self r f)
-        (f h))
-    l
-filter = f l : y filter_ l f
-
-foldl_ self l f acc =
-  matchList
-    acc
-    (h r : self r f (f acc h))
-    l
-foldl = f x l : y foldl_ l f x
-
-foldr_ self l f x =
-  matchList
-    x
-    (h r : f (self r f x) h)
-    l
-foldr = f x l : y foldr_ l f x
-
-length_ self xs =
-  matchList
-    0
-    (_ r : succ (self r))
-    xs
-length = xs : y length_ xs
-
-reverse_ self xs acc =
-  matchList
-    acc
-    (h r : self r (pair h acc))
-    xs
-reverse = xs : y reverse_ xs t
-
-snoc_ self x xs =
-  matchList
-    (pair x t)
-    (h r : pair h (self x r))
-    xs
-snoc = x xs : y snoc_ x xs
-
-count_ self x xs =
-  matchList
-    0
-    (h r :
-      matchBool
-        (succ (self x r))
-        (self x r)
-        (equal? x h))
-    xs
-count = x xs : y count_ x xs
-
-last_ self xs =
-  matchList
-    t
-    (h r :
-      matchBool
-        h
-        (self r)
-        (emptyList? r))
-    xs
-last = xs : y last_ xs
-
-all?_ self pred xs =
-  matchList
-    true
-    (h r : and? (pred h) (self pred r))
-    xs
-all? = pred xs : y all?_ pred xs
-
-any?_ self pred xs =
-  matchList
-    false
-    (h r : or? (pred h) (self pred r))
-    xs
-any? = pred xs : y any?_ pred xs
-
-intersect = xs ys : filter (x : lExist? x ys) xs
-
-nth_ self xs n i =
-  matchList
-    t
-    (h r :
-      matchBool
-        h
-        (self r n (succ i))
-        (equal? i n))
-    xs
-nth = n xs : y nth_ xs n 0
-
-headMaybe = matchList nothing (h _ : just h)
-
-lastMaybe_ self xs =
-  matchList
-    nothing
-    (h r :
-      matchBool
-        (just h)
-        (self r)
-        (emptyList? r))
-    xs
-lastMaybe = xs : y lastMaybe_ xs
-
-nthMaybe_ self xs n i =
-  matchList
-    nothing
-    (h r :
-      matchBool
-        (just h)
-        (self r n (succ i))
-        (equal? i n))
-    xs
-nthMaybe = n xs : y nthMaybe_ xs n 0
-
-take_ self xs n i =
-  matchList
-    t
-    (h r :
-      matchBool
-        t
-        (pair h (self r n (succ i)))
-        (equal? i n))
-    xs
-take = n xs : y take_ xs n 0
-
-drop_ self xs n i =
-  matchBool
-    xs
-    (matchList
-      t
-      (_ r : self r n (succ i))
-      xs)
-    (equal? i n)
-drop = n xs : y drop_ xs n 0
-
-splitAt = n xs : pair (take n xs) (drop n xs)
-
-concatMap_ self f xs =
-  matchList
-    t
-    (h r : append (f h) (self f r))
-    xs
-concatMap = f xs : y concatMap_ f xs
-
-find_ self pred xs =
-  matchList
-    nothing
-    (h r :
-      matchBool
-        (just h)
-        (self pred r)
-        (pred h))
-    xs
-find = pred xs : y find_ pred xs
-
-partition_ self pred xs trues falses =
-  matchList
-    (pair (reverse trues) (reverse falses))
-    (h r :
-      matchBool
-        (self pred r (pair h trues) falses)
-        (self pred r trues (pair h falses))
-        (pred h))
-    xs
-partition = pred xs : y partition_ pred xs t t
-
-strLength = length
-strAppend = append
-strEq? = equal?
-strEmpty? = emptyList?
-
-startsWith?_ self prefix input =
-  matchList
-    true
-    (ph pr :
-      matchList
-        false
-        (sh sr :
-          matchBool
-            (self pr sr)
-            false
-            (equal? ph sh))
-        input)
-    prefix
-startsWith? = prefix input : y startsWith?_ prefix input
-
-endsWith? = prefix str : startsWith? (reverse prefix) (reverse str)
-
-contains?_ self needle haystack =
-  matchBool
-    true
-    (matchList
-      false
-      (_ r : self needle r)
-      haystack)
-    (startsWith? needle haystack)
-contains? = needle haystack : y contains?_ needle haystack
-
--- ---------------------------------------------------------------------------
--- Generic separators
---
--- `lines`, `unlines`, `words` and `unwords` at the bottom of this section are
--- the byte-valued special cases of these primitives.
---
--- Joining takes any separator; splitting takes one byte. Separators are removed
--- rather than kept, and empty fields are preserved.
---
--- The workers below follow notes/tricu-normalization-rules.md: consumed data
--- first, lazy eliminators around every recursive branch, `y` only inside the
--- public wrapper, and `pair`-only state updates.
--- ---------------------------------------------------------------------------
-
-takeWhile_ self xs f =
-  lazyList
-    (_ : t)
-    (h r :
-      lazyBool
-        (_ : pair h (self r f))
-        (_ : t)
-        (f h))
-    xs
-takeWhile = f xs : y takeWhile_ xs f
-
-dropWhile_ self xs f =
-  lazyList
-    (_ : t)
-    (h r :
-      lazyBool
-        (_ : self r f)
-        (_ : pair h r)
-        (f h))
-    xs
-dropWhile = f xs : y dropWhile_ xs f
-
--- Byte-level whitespace only: space and horizontal tab (HTTP OWS).
-spaceByte? = b : equal? b 32
-tabByte?   = b : equal? b 9
-trimByte?  = b : or? (spaceByte? b) (tabByte? b)
-
-trim = xs : dropWhile trimByte? (reverse (dropWhile trimByte? (reverse xs)))
-
-intercalate_ self xs sep =
-  lazyList
-    (_ : t)
-    (h r :
-      lazyBool
-        (_ : h)
-        (_ : append h (append sep (self r sep)))
-        (emptyList? r))
-    xs
-intercalate = sep xs : y intercalate_ xs sep
-
--- Separator after every field, including the last one. Line-oriented formats
--- want this: `joinSuffix "\n" xs` terminates the final line while
--- `intercalate "\n" xs` does not.
-joinSuffix_ self xs sep =
-  lazyList
-    (_ : t)
-    (h r : append (append h sep) (self r sep))
-    xs
-joinSuffix = sep xs : y joinSuffix_ xs sep
-
--- Split on a single byte. A separator byte is never stored, so the state
--- updates stay `pair`s and every recursive argument is a variable: the input is
--- walked exactly once and the fields are reversed back once, when it ends.
---
--- Splitting on a multi-byte separator is deliberately not here. Detecting a
--- separator longer than a byte means re-walking the remaining input at every
--- split point (or splicing the field), which is quadratic in the best case and
--- blew up when tried. `http.tri` wants CRLF and `:` splits; that wants a shape
--- where the separator drives the recursion instead of the input.
---
--- Empty fields are preserved: `splitOnByte 58 "a::b"` is ["a" "" "b"].
-splitByte_ self str byte acc current =
-  lazyList
-    (_ : map reverse (reverse (pair current acc)))
-    (h r :
-      lazyBool
-        (_ : self r byte (pair current acc) t)
-        (_ : self r byte acc (pair h current))
-        (equal? h byte))
-    str
-splitOnByte = byte str : y splitByte_ str byte t t
-
--- Every one of these keeps its arguments bound: partially applying a
--- multi-argument function at the top level leaves a fixed point exposed.
-lines   = str : splitOnByte 10 str
-unlines = xs : joinSuffix "\n" xs
-
--- Runs of separators collapse: empty fields are dropped.
-words   = str : filter (w : not? (emptyList? w)) (splitOnByte 32 str)
-unwords = xs : intercalate " " xs
-
-zipWith_ self f xs ys =
-  matchList
-    t
-    (xh xt :
-      matchList
-        t
-        (yh yt : pair (f xh yh) (self f xt yt))
-        ys)
-    xs
-zipWith = f xs ys : y zipWith_ f xs ys

lib/prelude.tri

@@ -1,6 +1,3 @@
--- Standard tricu prelude.
-
 !import "base"        !Local
-!import "list"        !Local
 !import "bytes"       !Local
 !import "conversions" !Local

lib/views/catalog.tri

@@ -1,267 +0,0 @@
-!import "prelude" !Local
-!import "view" !Local
-
--- Stdlib-shaped typed-program catalog. These helpers are stable lowering
--- targets for frontend-emitted API contracts. They are monomorphic
--- instantiations of familiar polymorphic shapes.
-listMapUseContract = (elemIn elemOut mapSym fnSym xsSym partialSym outSym :
-  typedProgram
-    outSym
-    [(typedDeclareFn
-       mapSym
-       [(viewFn [(elemIn)] elemOut) (viewList elemIn)]
-       (viewList elemOut)
-       t)
-     (typedDeclareFn fnSym [(elemIn)] elemOut t)
-     (typedValue xsSym (viewList elemIn) t)
-     (typedApply partialSym mapSym fnSym t)
-     (typedApply outSym partialSym xsSym t)
-     (typedRequire outSym (viewList elemOut) t)])
-
-headMaybeUseContract = (elem headSym xsSym outSym :
-  typedProgram
-    outSym
-    [(typedDeclareFn headSym [(viewList elem)] (viewMaybe elem) t)
-     (typedValue xsSym (viewList elem) t)
-     (typedApply outSym headSym xsSym t)
-     (typedRequire outSym (viewMaybe elem) t)])
-
-listFilterUseContract = (elem filterSym predSym xsSym partialSym outSym :
-  typedProgram
-    outSym
-    [(typedDeclareFn
-       filterSym
-       [(viewFn [(elem)] viewBool) (viewList elem)]
-       (viewList elem)
-       t)
-     (typedDeclareFn predSym [(elem)] viewBool t)
-     (typedValue xsSym (viewList elem) t)
-     (typedApply partialSym filterSym predSym t)
-     (typedApply outSym partialSym xsSym t)
-     (typedRequire outSym (viewList elem) t)])
-
-listFoldUseContract = (acc elem foldSym fnSym initSym xsSym partialFnSym partialInitSym outSym :
-  typedProgram
-    outSym
-    [(typedDeclareFn
-       foldSym
-       [(viewFn [(acc) (elem)] acc) acc (viewList elem)]
-       acc
-       t)
-     (typedDeclareFn fnSym [(acc) (elem)] acc t)
-     (typedValue initSym acc t)
-     (typedValue xsSym (viewList elem) t)
-     (typedApply partialFnSym foldSym fnSym t)
-     (typedApply partialInitSym partialFnSym initSym t)
-     (typedApply outSym partialInitSym xsSym t)
-     (typedRequire outSym acc t)])
-
-listMapMaybeUseContract = (elemIn elemOut mapMaybeSym fnSym xsSym partialSym outSym :
-  typedProgram
-    outSym
-    [(typedDeclareFn
-       mapMaybeSym
-       [(viewFn [(elemIn)] (viewMaybe elemOut)) (viewList elemIn)]
-       (viewList elemOut)
-       t)
-     (typedDeclareFn fnSym [(elemIn)] (viewMaybe elemOut) t)
-     (typedValue xsSym (viewList elemIn) t)
-     (typedApply partialSym mapMaybeSym fnSym t)
-     (typedApply outSym partialSym xsSym t)
-     (typedRequire outSym (viewList elemOut) t)])
-
--- Concrete stdlib-shaped typed programs. These are deliberately monomorphic
--- examples of the shapes a frontend can emit for polymorphic library functions.
-listMapBoolStringExpr = cFn <|
-    [(viewFn [(viewBool)] viewString) (viewList viewBool)] (viewList viewString)
-    |> cApply (cFn [(viewBool)] viewString)
-    |> cApply (cValue (viewList viewBool))
-    |> cRequire (viewList viewString)
-
-headMaybeBoolExpr = cFn <|
-    [(viewList viewBool)] (viewMaybe viewBool)
-    |> cApply (cValue (viewList viewBool))
-    |> cRequire (viewMaybe viewBool)
-
-listFilterBoolExpr = cFn <|
-    [(viewFn [(viewBool)] viewBool) (viewList viewBool)] (viewList viewBool)
-    |> cApply (cFn [(viewBool)] viewBool)
-    |> cApply (cValue (viewList viewBool))
-    |> cRequire (viewList viewBool)
-
-listFoldStringBoolExpr = cFn <|
-    [(viewFn [(viewString) (viewBool)] viewString) viewString (viewList viewBool)] viewString
-    |> cApply (cFn [(viewString) (viewBool)] viewString)
-    |> cApply (cValue viewString)
-    |> cApply (cValue (viewList viewBool))
-    |> cRequire viewString
-
-listMapMaybeBoolStringExpr = cFn <|
-    [(viewFn [(viewBool)] (viewMaybe viewString)) (viewList viewBool)] (viewList viewString)
-    |> cApply (cFn [(viewBool)] (viewMaybe viewString))
-    |> cApply (cValue (viewList viewBool))
-    |> cRequire (viewList viewString)
-
--- Keep catalog exports as explicit finite typed-programs. `cCompileAt` is useful
--- as a frontend-emission helper, but forcing generated node lists at module
--- import time can violate top-level normalization discipline.
-listMapBoolStringContract =
-  listMapUseContract viewBool viewString 100 101 102 103 104
-headMaybeBoolContract =
-  headMaybeUseContract viewBool 110 111 112
-listFilterBoolContract =
-  listFilterUseContract viewBool 120 121 122 123 124
-listFoldStringBoolContract =
-  listFoldUseContract viewString viewBool 130 131 132 133 134 135 136
-listMapMaybeBoolStringContract =
-  listMapMaybeUseContract viewBool viewString 140 141 142 143 144
-
-listMapWrongFunctionArgContract =
-  typedProgram
-    152
-    [(typedDeclareFn
-       150
-       [(viewFn [(viewBool)] viewString) (viewList viewBool)]
-       (viewList viewString)
-       t)
-     (typedDeclareFn 151 [(viewString)] viewString t)
-     (typedApply 152 150 151 t)]
-
-listMapWrongListArgContract =
-  typedProgram
-    164
-    [(typedDeclareFn
-       160
-       [(viewFn [(viewBool)] viewString) (viewList viewBool)]
-       (viewList viewString)
-       t)
-     (typedDeclareFn 161 [(viewBool)] viewString t)
-     (typedValue 162 (viewList viewString) t)
-     (typedApply 163 160 161 t)
-     (typedApply 164 163 162 t)]
-
-listMapWrongOutputContract =
-  typedProgram
-    174
-    [(typedDeclareFn
-       170
-       [(viewFn [(viewBool)] viewString) (viewList viewBool)]
-       (viewList viewString)
-       t)
-     (typedDeclareFn 171 [(viewBool)] viewString t)
-     (typedValue 172 (viewList viewBool) t)
-     (typedApply 173 170 171 t)
-     (typedApply 174 173 172 t)
-     (typedRequire 174 (viewList viewBool) t)]
-
-listFilterWrongPredicateContract =
-  typedProgram
-    182
-    [(typedDeclareFn
-       180
-       [(viewFn [(viewBool)] viewBool) (viewList viewBool)]
-       (viewList viewBool)
-       t)
-     (typedDeclareFn 181 [(viewBool)] viewString t)
-     (typedApply 182 180 181 t)]
-
-listMapWrongListArgExpr = cFn <|
-    [(viewFn [(viewBool)] viewString) (viewList viewBool)] (viewList viewString)
-    |> cApply (cFn [(viewBool)] viewString)
-    |> cApply (cValue (viewList viewString))
-    |> cRequire (viewList viewString)
-
-listMapWrongListArgExprContract =
-  typedProgram
-    194
-    [(typedDeclareFn
-       190
-       [(viewFn [(viewBool)] viewString) (viewList viewBool)]
-       (viewList viewString)
-       t)
-     (typedDeclareFn 191 [(viewBool)] viewString t)
-     (typedValue 193 (viewList viewString) t)
-     (typedApply 192 190 191 t)
-     (typedApply 194 192 193 t)
-     (typedRequire 194 (viewList viewString) t)]
-
-viewCatalogSelfTests =
-  append
-    viewContractSelfTests
-    [ (typedContractCheck listMapBoolStringContract)
-      (typedContractCheck headMaybeBoolContract)
-      (typedContractCheck listFilterBoolContract)
-      (typedContractCheck listFoldStringBoolContract)
-      (typedContractCheck listMapMaybeBoolStringContract)
-      (viewContractExpectResult
-        "function argument view is not known"
-        (checkTypedProgramWith policyStrict listMapWrongFunctionArgContract))
-      (viewContractExpectResult
-        "function argument view is not known"
-        (checkTypedProgramWith policyStrict listMapWrongListArgContract))
-      (viewContractExpectResult
-        "required view is not known"
-        (checkTypedProgramWith policyStrict listMapWrongOutputContract))
-      (viewContractExpectResult
-        "function argument view is not known"
-        (checkTypedProgramWith policyStrict listFilterWrongPredicateContract))
-      (viewContractExpectResult
-        "function argument view is not known"
-        (checkTypedProgramWith policyStrict listMapWrongListArgExprContract))
-      (viewContractExpectErrorTag
-        errorTagOk
-        (checkTypedProgram listMapBoolStringContract))
-      (viewContractExpectErrorTag
-        errorTagMissingFunctionArgumentView
-        (checkTypedProgramWith policyStrict listMapWrongFunctionArgContract))
-      (viewContractExpectErrorTag
-        errorTagMissingFunctionArgumentView
-        (checkTypedProgramWith policyStrict listMapWrongListArgContract))
-      (viewContractExpectErrorTag
-        errorTagMissingFunctionArgumentView
-        (checkTypedProgramWith policyStrict listMapWrongListArgExprContract))
-      (viewContractExpectErrorTag
-        errorTagMissingRequiredView
-        (checkTypedProgramWith policyStrict listMapWrongOutputContract))
-      (viewContractExpectDiagnostic
-        errorTagMissingFunctionArgumentView
-        162
-        (viewList viewBool)
-        (checkTypedProgramWith policyStrict listMapWrongListArgContract))
-      (viewContractExpectDiagnostic
-        errorTagMissingRequiredView
-        174
-        (viewList viewBool)
-        (checkTypedProgramWith policyStrict listMapWrongOutputContract))
-      (viewContractExpectDiagnosticActual
-        errorTagMissingFunctionArgumentView
-        162
-        (viewList viewBool)
-        (viewList viewString)
-        (checkTypedProgramWith policyStrict listMapWrongListArgContract))
-      (viewContractExpectDiagnosticActual
-        errorTagMissingFunctionArgumentView
-        193
-        (viewList viewBool)
-        (viewList viewString)
-        (checkTypedProgramWith policyStrict listMapWrongListArgExprContract))
-      (viewContractExpectDiagnosticActual
-        errorTagMissingRequiredView
-        174
-        (viewList viewBool)
-        (viewList viewString)
-        (checkTypedProgramWith policyStrict listMapWrongOutputContract))
-      (viewContractExpectDiagnosticActual
-        errorTagMissingFunctionArgumentView
-        181
-        (viewFn [(viewBool)] viewBool)
-        (viewFn [(viewBool)] viewString)
-        (checkTypedProgramWith policyStrict listFilterWrongPredicateContract))
-      (matchResult
-        (diag env :
-          viewContractProbe
-            (equal?
-              (renderDiagnostic diag)
-              "symbol 162 expected List Bool but got List String"))
-        (env rest : "fail")
-        (checkTypedProgramWith policyStrict listMapWrongListArgContract))]

notes/contract-design.md

@@ -0,0 +1,328 @@
+# Contract Kernel Design
+
+## Status
+
+Implemented. The contract system uses a configurable kernel defined in
+`lib/base.tri`. All contract logic lives in pure tree calculus.
+
+## Goals
+
+1. **User code stays ergonomic.** `@`/`=@` syntax remains. Calling a guarded
+   function looks the same as calling an unguarded one.
+2. **No stringly-dynamic failures.** A contract boundary returns a structured
+   `Result`. The kernel decides whether to abort, resume with a replacement,
+   log, or otherwise transform the result.
+3. **All evaluation logic in pure tree calculus.** The evaluator does not treat
+   contracts specially; contracts are ordinary functions and the desugarer
+   emits ordinary tricu code.
+4. **Optional contract enforcement.** A CLI/REPL flag can disable contract
+   syntax entirely by stripping annotations at desugar time.
+5. **Configurable failure semantics.** A global kernel, supplied by the user
+   via CLI/REPL, determines how contract failures are handled for the
+   session.
+
+## Core idea
+
+A contract annotation on a definition desugars into a runtime guard. The
+runtime guard applies a contract predicate to a value and passes the resulting
+`Result` to the current `kernel`. The `kernel` returns another `Result`, which
+the wrapper inspects:
+
+- `ok value` means the guard succeeded; continue with `value`.
+- `err msg` means the guard failed; abort and propagate the error.
+
+The default kernel is the identity on the contract `Result`. A custom kernel
+can transform failures into successes, wrap diagnostics, or log failures before
+aborting.
+
+## Kernel
+
+### Signature
+
+```tricu
+kernel contract value result -> Result
+```
+
+- `contract`: the contract predicate being checked.
+- `value`: the unevaluated original value passed to the contract.
+- `result`: the `Result` produced by evaluating `contract value t`.
+
+### Default kernel
+
+`lib/base.tri` defines both `defaultKernel` and the active `kernel`:
+
+```tricu
+defaultKernel = (contract value result :
+  matchResult
+    (msg rest : err msg rest)
+    (v rest : ok v rest)
+    result)
+
+kernel = defaultKernel
+```
+
+The runner may rebind `kernel` to a different value before evaluating user
+code (e.g. via `--contract-kernel`). Because `withContract` looks up `kernel`
+dynamically at application time, rebinding it changes the behaviour of every
+contract boundary.
+
+### Skip kernel
+
+Resume with the original value whenever a contract fails:
+
+```tricu
+skipKernel = (contract value result :
+  matchResult
+    (msg rest : ok value rest)
+    (v rest : ok v rest)
+    result)
+```
+
+### Logging kernel
+
+Abort but also emit a log entry:
+
+```tricu
+loggingKernel = (contract value result :
+  matchResult
+    (msg rest : pair (logMsg msg) (err msg rest))
+    (v rest : ok v rest)
+    result)
+```
+
+### Resume-with-default kernel
+
+```tricu
+resumeWithZero = (contract value result :
+  matchResult
+    (msg rest : ok 0 rest)
+    (v rest : ok v rest)
+    result)
+```
+
+## Runtime guard primitive
+
+`withContract` is the primitive emitted by the desugarer:
+
+```tricu
+withContract = (contract value :
+  kernel contract value (contract value t))
+```
+
+`check` is a convenience wrapper that extracts the value or the diagnostic
+message:
+
+```tricu
+check contract value =
+  matchResult
+    (msg _ : msg)
+    (v _ : v)
+    (withContract contract value)
+```
+
+## Desugaring
+
+Desugaring runs **before** import selection so that names introduced by the
+desugarer (`withContract`, `matchResult`, `err`, `ok`, etc.) are included in
+the selected exports of imported modules. This ensures that a module using
+contract annotations imports everything it needs from `base`/`prelude`.
+
+### Phantom annotations
+
+```tricu
+add @nat? @nat? =@nat? addRaw
+```
+
+desugars to:
+
+```tricu
+add = (x y :
+  matchResult
+    (msg _ : \_ : err msg t)
+    (x' _ :
+      matchResult
+        (msg _ : err msg t)
+        (y' _ :
+          matchResult
+            (msg _ : err msg t)
+            (r _ : r)
+            (withContract nat? (addRaw x' y')))
+        (withContract nat? y))
+    (withContract nat? x))
+```
+
+The first failure continuation is absorbing (`\_ : err msg t`) because `add`
+is curried and a failure on the first argument should consume the second
+argument without producing garbage.
+
+`addRaw` is the locally-let-bound raw helper, as in the current phantom
+implementation.
+
+### Named-binder annotations
+
+```tricu
+safeDiv a@nat? b@(andC nat? nonZero?) =@nat? div a b
+```
+
+desugars to:
+
+```tricu
+safeDiv = (a b :
+  matchResult
+    (msg _ : \_ : err msg t)
+    (a' _ :
+      matchResult
+        (msg _ : err msg t)
+        (b' _ :
+          matchResult
+            (msg _ : err msg t)
+            (r _ : r)
+            (withContract nat? (div a' b')))
+        (withContract (andC nat? nonZero?) b))
+    (withContract nat? a))
+```
+
+### No return contract
+
+```tricu
+head xs@(nonEmptyListOf anyC) =@anyC headRaw
+```
+
+desugars to:
+
+```tricu
+head = (xs :
+  matchResult
+    (msg _ : err msg t)
+    (xs' _ :
+      matchResult
+        (msg _ : err msg t)
+        (r _ : r)
+        (withContract anyC (headRaw xs')))
+    (withContract (nonEmptyListOf anyC) xs))
+```
+
+### No annotations
+
+Definitions without `@`/`=@` are emitted unchanged.
+
+## Failure propagation
+
+When a non-final argument contract fails, the wrapper returns a function that
+absorbs the next argument and then returns the failed `Result`. This prevents
+partial-application accidents like `gt? "the" 3` reducing to a garbage number.
+
+When the final argument or result contract fails, the wrapper returns
+`\msg -> err msg t`, which is the failure constructor awaiting its `rest`
+slot.
+
+## Skip-contracts flag
+
+When the `--skip-contracts` flag is set, the desugarer strips all `@`/`=@`
+annotations and emits the raw function body. This is faster than running the
+skip kernel because no contract code is generated at all.
+
+### CLI
+
+```bash
+tricu eval --skip-contracts program.tri
+tricu repl --skip-contracts
+```
+
+### REPL
+
+```tricu
+> :set skip-contracts
+> add 1 2
+3
+> :unset skip-contracts
+> add "bad" 2
+[t, "not a natural number"]
+```
+
+## Kernel selection
+
+### CLI
+
+```bash
+tricu eval --contract-kernel resumeWithZero program.tri
+```
+
+### REPL
+
+```tricu
+> :set contract-kernel resumeWithZero
+> add "bad" 2
+2
+```
+
+### Resolution
+
+The kernel name is resolved like any other top-level binding in the program or
+its imports. The runner prepends `kernel = <name>` to the program AST (or
+inserts it into the environment) after imports are resolved. If the name is
+not found, evaluation fails with an undefined-variable error.
+
+## Base library changes
+
+1. `withContract` becomes the runtime guard primitive shown above.
+2. `check` extracts the checked value or diagnostic message from the kernel
+   `Result`.
+3. Contract predicates (`nat?`, `nonZero?`, `bool?`, etc.) remain pure
+   functions returning `Result`.
+4. Guarded base functions (`add`, `sub`, `head`, `div`, etc.) use the new
+   desugaring.
+5. Raw helpers (`addRaw`, `subRaw`, etc.) remain for internal use and recursion.
+
+## Custom contracts
+
+Users write ordinary predicates returning `Result`:
+
+```tricu
+positive? = (n rest :
+  ifThenElse (gte? n 1)
+    (ok n rest)
+    (err "expected positive integer" rest))
+```
+
+and use them with the same syntax:
+
+```tricu
+fact n@positive? =@nat? y (self n : ...)
+```
+
+Contract combinators (`andC`, `orC`, `guardC`) compose in the obvious way.
+
+## Limitations
+
+1. **Global kernel only.** There is no local kernel override. A module or
+   function cannot install a different kernel for part of the program.
+   Workarounds: split into separate evaluation sessions, or use explicit
+   `withContract` calls with a local handler function.
+2. **Kernel must return `Result`.** A kernel that returns a plain value is a
+   bug. The `defaultKernel`/`skipKernel` templates show the required shape.
+3. **Failures are first-class `Result` values.** A caller that ignores a
+   returned `err msg` and treats it as data will operate on the `Result` tree.
+   This is inherent to any value-level error mechanism.
+4. **Function contracts are advanced.** Contracts on function arguments
+   (e.g. `f @ (nat? -> nat?)`) require intensional/quantified contracts. The
+   simple predicate model covers most use cases.
+
+## Implementation notes
+
+- `Frontend.ContractDesugar` emits `matchResult`/`withContract`/`err`/`ok`
+  instead of continuation-passing `withContract`.
+- `FileEval.loadFile'` desugars before computing selected exports, so
+  imported modules bring in the runtime helpers needed by annotations.
+- `Eval.injectKernel` is a fallback that binds `kernel` to `defaultKernel`
+  when `kernel` is missing from the environment.
+
+## Open questions
+
+1. **Should `--skip-contracts` strip annotations or just bind the skip
+   kernel?** Currently stripping is the intended design; not yet implemented.
+2. **Should we provide a small set of built-in kernel names?** `default`,
+   `skip`, `strict`, `log` would cover common cases without requiring the user
+   to define them.
+3. **How do we expose the current kernel to introspection?** A top-level
+   `currentContractKernel` binding might be useful for debugging.

notes/view-contract-trust-provenance.md

@@ -1,95 +0,0 @@
-# View Contracts at the intensionality boundary
-
-## Conclusion
-
-Tree Calculus does not support the abstraction theorem that the former
-parametric View design assumed. Views can remain useful as boundary metadata and
-as instructions for runtime guard placement, but they must not be presented as
-types, proofs of parametricity, or representation-hiding abstraction.
-
-## Fundamental conflicts
-
-### Raw observation defeats representation independence
-
-A parametric contract such as:
-
-```text
-forall a. a -> a
-```
-
-normally relies on code being unable to learn anything about `a`. A Tree
-Calculus term can inspect the tree supplied at `a`, distinguish
-representations, and return a representation-dependent value. The View variable
-does not hide or seal that tree.
-
-The same breaks existential abstraction. Advertising a payload as
-`exists repr. ...` changes no operational capability: a client can still
-inspect the representation directly.
-
-### Opaque payloads are asserted, not checked
-
-A typed-value node carries an executable tree beside a View. Metadata validation
-deliberately treats that executable field as opaque. Consequently, accepting a
-node proves that the envelope and View are well formed; it does not prove that
-the tree denotes the advertised `Fn`, `List`, `Maybe`, or other structural
-View.
-
-Provenance labels do not change this. `Checked` and `Trusted` record where an
-assertion came from, but neither is a derivation that another implementation can
-replay to establish the assertion.
-
-### Syntactic taint is not a semantic parametricity proof
-
-Rejecting direct uses of `t` or `triage` is neither complete nor a stable
-soundness boundary:
-
-- an observer can be assembled after reduction;
-- observation can arrive through higher-order or dynamically selected code;
-- unknown external code can hide observation;
-- absence of a rule-3 redex is not reduction-closed;
-- exact detection would subsume non-trivial termination/reachability questions.
-
-A conservative taint pass can define a programming convention, but it cannot
-justify the parametric or abstraction guarantees previously attached to Views.
-
-### Flow checking only checks represented flow
-
-The checker sees frontend-emitted value, application, and requirement nodes. It
-can check consistency among those nodes, but it cannot establish that the graph
-faithfully represents every use performed by the opaque executable payload.
-This is useful artifact validation, not whole-program typing.
-
-## Retained contract
-
-The reduced checker may soundly claim only:
-
-1. View, node, and program envelopes satisfy their declared data schemas.
-2. Explicit monomorphic View facts are propagated consistently through the
-   represented application graph.
-3. A `Guarded` View causes its executable predicate to run at represented
-   boundaries, and guard failure prevents checked execution.
-4. Content-addressed references prevent an attached View artifact from silently
-   drifting to a different stored object.
-
-Items 1, 2, and 4 establish metadata integrity, not semantic membership in an
-unguarded View. Item 3 is the only retained mechanism that observes an ordinary
-runtime value.
-
-## Code direction
-
-The initial rollback therefore:
-
-- removes View-variable instantiation, substitution, and unification from the
-  portable checker;
-- rejects `Var`, `Forall`, and `Exists` as checker inputs while reserving
-  their legacy tags for deterministic decoding;
-- removes the frontend raw-intensionality taint pass;
-- removes polymorphic stdlib annotations and value-level View facts;
-- retains monomorphic View flow, artifact plumbing, diagnostics, and executable
-  guards.
-
-Further simplification should treat unguarded structural Views as descriptive
-labels. If stronger guarantees are desired later, they require an operational
-mechanism such as runtime recognizers/seals or a genuinely restricted language
-whose evaluator enforces the restriction. Metadata provenance alone is
-insufficient.

src/Check.hs

@@ -1,42 +0,0 @@
-module Check
-  ( module Check.Core
-  , module Check.IO
-  , checkFile
-  , checkFileWithStore
-  , checkSource
-  ) where
-
-import Check.Core
-import Check.IO
-import ContentStore (ObjectRef, StorePath, getViewType)
-import Eval (evalTricu)
-import FileEval (LoadedSource(..), defaultStorePath, evaluateFile, evaluateFileWithStore, loadFileWithStore)
-import Research (Env, ViewType)
-
-import qualified Data.Map as Map
-
-import System.IO.Unsafe (unsafePerformIO)
-
-checkFile :: FilePath -> IO String
-checkFile path = do
-  store <- defaultStorePath
-  checkFileWithStore store path
-
-checkFileWithStore :: StorePath -> FilePath -> IO String
-checkFileWithStore store path = do
-  loaded <- loadFileWithStore store path
-  viewEnv <- evaluateFileWithStore (Just store) "./lib/view.tri"
-  let baseEnv = Map.union viewEnv (loadedImports loaded)
-      checkerEnv = evalTricu baseEnv (loadedAst loaded)
-  imports <- importedViewsFromResolvedModulesEither (loadImportedView store) (loadedModules loaded)
-  checkProgramWithEnvAndImportedViews checkerEnv imports (loadedAst loaded)
-
-viewCheckerEnv :: Env
-viewCheckerEnv = unsafePerformIO (evaluateFile "./lib/view.tri")
-{-# NOINLINE viewCheckerEnv #-}
-
-checkSource :: String -> IO String
-checkSource = checkSourceWithEnv viewCheckerEnv
-
-loadImportedView :: StorePath -> ObjectRef -> IO (Either String ViewType)
-loadImportedView = getViewType

src/Check/Core.hs

@@ -1,846 +0,0 @@
-module Check.Core
-  ( ImportedView(..)
-  , importedViewsFromResolvedModules
-  , importedViewsFromResolvedModulesEither
-  , checkProgramWithEnvAndImportedViews
-  , checkSourceWithEnv
-  , checkSourceWithEnvAndImportedViews
-  , lowerSource
-  , lowerSourceWithDebug
-  , lowerSourceWithImportedViews
-  , lowerSourceWithImportedViewsDebug
-  , lowerViewExpr
-  ) where
-
-import Control.Monad.State.Strict
-import Data.Char (isDigit)
-import Data.Maybe (mapMaybe)
-import qualified Data.Map as Map
-import qualified Data.Set as Set
-import qualified Data.Text as T
-
-import ContentStore.Alias (ObjectRef(..))
-import Eval (evalTricu, result)
-import Module.Resolver
-  ( ResolvedExport(..)
-  , ResolvedModule(..)
-  )
-import Parser (parseTricu)
-import Research
-
-data ImportedView = ImportedView
-  { importedViewName       :: String
-  , importedViewType       :: ViewType
-  , importedViewProvenance :: ViewProvenance
-  } deriving (Show, Eq)
-
--- Convert module-resolution metadata into checker evidence inputs. The loader
--- decodes a portable view artifact into a syntactic ViewType, but this function
--- does not judge compatibility or policy. It only says: this resolved imported
--- name has an advertised view fact that should be emitted into the typed program.
-importedViewsFromResolvedModules :: (ObjectRef -> IO (Maybe ViewType)) -> [ResolvedModule] -> IO [ImportedView]
-importedViewsFromResolvedModules loadView = importedViewsFromResolvedModulesEither loadViewEither
-  where
-    loadViewEither ref = do
-      mView <- loadView ref
-      pure $ maybe (Left "artifact not found or could not be decoded") Right mView
-
-importedViewsFromResolvedModulesEither :: (ObjectRef -> IO (Either String ViewType)) -> [ResolvedModule] -> IO [ImportedView]
-importedViewsFromResolvedModulesEither loadView modules = concat <$> mapM fromModule modules
-  where
-    fromModule m = concat <$> mapM fromExport (resolvedModuleExports m)
-
-    fromExport ex = case resolvedExportView ex of
-      Nothing -> pure []
-      Just ref -> do
-        eView <- loadView ref
-        case eView of
-          Left err -> errorWithoutStackTrace $
-            "View Contract artifact invalid for imported export "
-            ++ show (resolvedExportLocalName ex)
-            ++ " (kind " ++ showRefKind ref ++ ", hash " ++ showRefHash ref ++ "): "
-            ++ err
-          Right view -> pure [ImportedView (resolvedExportLocalName ex) view (maybe ViewUnchecked id (resolvedExportProvenance ex))]
-
-    showRefKind = T.unpack . objectRefKind
-    showRefHash = T.unpack . objectRefHash
-
-checkSourceWithEnv :: Env -> String -> IO String
-checkSourceWithEnv checkerEnv = checkSourceWithEnvAndImportedViews checkerEnv []
-
-checkSourceWithEnvAndImportedViews :: Env -> [ImportedView] -> String -> IO String
-checkSourceWithEnvAndImportedViews checkerEnv imports source =
-  checkProgramWithEnvAndImportedViews checkerEnv imports (parseTricu source)
-
-checkProgramWithEnvAndImportedViews :: Env -> [ImportedView] -> [TricuAST] -> IO String
-checkProgramWithEnvAndImportedViews _ _ asts
-  | not (any isAnnotatedDefinition asts) = pure "ok"
-  where
-    isAnnotatedDefinition SDefAnn {} = True
-    isAnnotatedDefinition _ = False
-checkProgramWithEnvAndImportedViews checkerEnv imports asts = do
-  case lowerProgramWithImportedViewsDebugInEnv checkerEnv imports asts of
-    Left err -> pure err
-    Right (typedProgramSource, debugNames) -> do
-      let input =
-            "matchResult " ++
-            "(diag env : renderDiagnostic diag) " ++
-            "(exec env : matchResult (runtimeDiag runtimeEnv : renderDiagnostic runtimeDiag) (_ runtimeEnv : \"ok\") (runChecked exec)) " ++
-            "(checkTypedProgramWith policyStrict " ++ parens typedProgramSource ++ ")"
-      let env = evalTricu checkerEnv (parseTricu input)
-      pure $ case toString (result env) of
-        Right s -> annotateDiagnostic debugNames s
-        Left _  -> formatT Decode (result env)
-
--- Debug names are a frontend-only side table. The portable checker renders
--- canonical numeric-symbol diagnostics; the CLI annotates that presentation
--- afterward without feeding labels back into checker semantics.
-annotateDiagnostic :: Map.Map Integer String -> String -> String
-annotateDiagnostic debugNames message =
-  case words message of
-    ("symbol" : symText : rest)
-      | all isDigit symText
-      , Just label <- Map.lookup (read symText) debugNames ->
-          "symbol " ++ symText ++ " (" ++ label ++ ") " ++ unwords rest
-    _ -> message
-
-astFreeRefs :: Set.Set String -> TricuAST -> [String]
-astFreeRefs candidates ast = case ast of
-  SVar name _ | name `Set.member` candidates -> [name]
-  SVar _ _ -> []
-  SInt _ -> []
-  SStr _ -> []
-  SList items -> concatMap (astFreeRefs candidates) items
-  SDef _ args body -> astFreeRefs (foldr Set.delete candidates args) body
-  SDefAnn _ args _ body -> astFreeRefs (foldr Set.delete candidates (defArgNames args)) body
-  SApp fn arg -> astFreeRefs candidates fn ++ astFreeRefs candidates arg
-  TLeaf -> []
-  TStem inner -> astFreeRefs candidates inner
-  TFork left right -> astFreeRefs candidates left ++ astFreeRefs candidates right
-  SLambda args body -> astFreeRefs (foldr Set.delete candidates args) body
-  SLet name val body -> astFreeRefs candidates val ++ astFreeRefs (Set.delete name candidates) body
-  SEmpty -> []
-  SImport _ _ -> []
-
-defArgNames :: [DefArg] -> [String]
-defArgNames = mapMaybe defArgName
-  where
-    defArgName (DefBinder name _) = Just name
-    defArgName (DefPhantom _) = Nothing
-
-lowerSource :: String -> Either String String
-lowerSource = lowerProgram . parseTricu
-
-lowerSourceWithDebug :: String -> Either String (String, Map.Map Integer String)
-lowerSourceWithDebug = lowerProgramWithDebug . parseTricu
-
-lowerSourceWithImportedViews :: [ImportedView] -> String -> Either String String
-lowerSourceWithImportedViews imports = lowerProgramWithImportedViews imports . parseTricu
-
-lowerSourceWithImportedViewsDebug :: [ImportedView] -> String -> Either String (String, Map.Map Integer String)
-lowerSourceWithImportedViewsDebug imports = lowerProgramWithImportedViewsDebug imports . parseTricu
-
--- Symbol allocation is intentionally deterministic so emitted view-tree
--- nodes are stable and lower-only tests can inspect them directly:
---
--- * top-level definitions receive symbols 0..n-1 in source order;
--- * local binders, literals, application results, and synthetic typed nodes
---   are allocated monotonically from nextSym;
--- * external names are allocated on first reference and then reused.
---
--- Symbols are view-tree node identifiers only. Checker semantics remain in
--- lib/view.tri; the frontend only emits typed/checkable structure about these
--- symbols.
-data LowerState = LowerState
-  { nextSym :: Integer
-  , topSyms :: Map.Map String Integer
-  , scopes :: [Map.Map String Integer]
-  , externSyms :: Map.Map String Integer
-  , knownNodeViews :: Map.Map Integer ViewExpr
-  , nodePayloads :: Map.Map Integer T
-  , debugNames :: Map.Map Integer String
-  }
-
-type LowerM a = StateT LowerState (Either String) a
-
-lowerProgram :: [TricuAST] -> Either String String
-lowerProgram asts = fst <$> lowerProgramWithDebug asts
-
-lowerProgramWithDebug :: [TricuAST] -> Either String (String, Map.Map Integer String)
-lowerProgramWithDebug = lowerProgramWithImportedViewsDebug []
-
-lowerProgramWithImportedViews :: [ImportedView] -> [TricuAST] -> Either String String
-lowerProgramWithImportedViews imports asts = fst <$> lowerProgramWithImportedViewsDebug imports asts
-
-lowerProgramWithImportedViewsDebug :: [ImportedView] -> [TricuAST] -> Either String (String, Map.Map Integer String)
-lowerProgramWithImportedViewsDebug = lowerProgramWithImportedViewsDebugInEnv Map.empty
-
-lowerProgramWithImportedViewsDebugInEnv :: Env -> [ImportedView] -> [TricuAST] -> Either String (String, Map.Map Integer String)
-lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
-  let definitions = [ def | def <- asts, isDefinition def ]
-      topNames = map definitionName definitions
-      tops = Map.fromList (zip topNames [0..])
-      topCount = Map.size tops
-      importCandidates = Set.fromList (map importedViewName imports) `Set.difference` Set.fromList topNames
-      usedImportNames = Set.fromList (concatMap (astFreeRefs importCandidates) asts)
-      activeImports = filter (\imported -> importedViewName imported `Set.member` usedImportNames) imports
-      importedSyms = Map.fromList
-        [ (importedViewName imported, fromIntegral (topCount + idx))
-        | (idx, imported) <- zip [0..] activeImports
-        ]
-      topDebug = Map.fromList [ (sym, name) | (name, sym) <- Map.toList tops ]
-      importDebug = Map.fromList
-        [ (sym, "imported " ++ name)
-        | (name, sym) <- Map.toList importedSyms
-        ]
-      localFactByName = Map.fromList [(importedViewName imported, imported) | imported <- imports, importedViewName imported `elem` topNames]
-      trustedLocalFacts =
-        [ (sym, viewTypeToExpr (importedViewType imported), importedViewProvenance imported)
-        | (name, sym) <- Map.toList tops
-        , Just imported <- [Map.lookup name localFactByName]
-        , importedViewProvenance imported `elem` [ViewChecked, ViewTrusted]
-        ]
-      trustedLocalKnown = Map.fromList [(sym, view) | (sym, view, _) <- trustedLocalFacts]
-      importKnown = Map.fromList
-        [ (sym, viewTypeToExpr (importedViewType imported))
-        | imported <- activeImports
-        , Just sym <- [Map.lookup (importedViewName imported) importedSyms]
-        ]
-      payloads = Map.fromList $
-        [ (sym, term)
-        | (name, sym) <- Map.toList tops
-        , Just term <- [Map.lookup name checkerEnvForLowering]
-        ] ++
-        [ (sym, term)
-        | (name, sym) <- Map.toList importedSyms
-        , Just term <- [Map.lookup name checkerEnvForLowering]
-        ]
-      annotated = [ def | def@SDefAnn {} <- asts ]
-      initialState = LowerState
-        { nextSym = fromIntegral (Map.size tops + Map.size importedSyms)
-        , topSyms = tops
-        , scopes = []
-        , externSyms = importedSyms
-        , knownNodeViews = Map.union trustedLocalKnown importKnown
-        , nodePayloads = payloads
-        , debugNames = Map.union topDebug importDebug
-        }
-  (localNodes, finalState) <- runStateT (lowerAnnotatedProgram annotated) initialState
-  trustedLocalNodes <- mapM (lowerImportedView (nodePayloads finalState)) trustedLocalFacts
-  importNodes <- mapM (lowerImportedView (nodePayloads finalState))
-    [ (sym, viewTypeToExpr (importedViewType imported), importedViewProvenance imported)
-    | imported <- activeImports
-    , Just sym <- [Map.lookup (importedViewName imported) importedSyms]
-    ]
-  let nodes = trustedLocalNodes ++ importNodes ++ localNodes
-      rootSym = if null nodes then 0 else nextSym finalState - 1
-      typedProgramSource =
-        "typedProgram " ++ show rootSym ++ " [" ++ unwords (map parens nodes) ++ "]"
-  pure (typedProgramSource, debugNames finalState)
-lowerImportedView :: Map.Map Integer T -> (Integer, ViewExpr, ViewProvenance) -> Either String String
-lowerImportedView payloadsBySym (sym, view, provenance) = do
-  viewExpr <- lowerViewExpr view
-  let payload = maybe "t" treeSource (Map.lookup sym payloadsBySym)
-  pure $ "typedValueWithProvenance " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload ++ " " ++ viewProvenanceSource provenance
-
-lowerAnnotatedProgram :: [TricuAST] -> LowerM [String]
-lowerAnnotatedProgram defs = do
-  declarations <- concat <$> mapM lowerDefinitionDeclaration defs
-  flows <- concat <$> mapM lowerDefinitionFlow defs
-  pure (declarations ++ flows)
-
-lowerDefinitionDeclaration :: TricuAST -> LowerM [String]
-lowerDefinitionDeclaration (SDefAnn name args ret _) = do
-  let (_, _, declaredView) = canonicalDefinitionViews args ret
-  sym <- symbolForTop name
-  recordKnown sym declaredView
-  node <- typedValueNode sym declaredView
-  pure [node]
-lowerDefinitionDeclaration _ = liftEither (Left "internal check error: expected annotated definition")
-
-lowerDefinitionFlow :: TricuAST -> LowerM [String]
-lowerDefinitionFlow (SDefAnn _ args ret body) = withDefinitionScope args $ do
-  let (flowArgs, flowRet, _) = canonicalDefinitionViews args ret
-  binderNodes <- concat <$> mapM lowerBinderDeclaration flowArgs
-  let phantomViews = map lowerPhantomArgType (phantomArgs flowArgs)
-  (returnArgs, returnResult) <- lowerReturnObligation flowRet
-  bodyNodes <- lowerBodyWithPhantoms (phantomViews ++ returnArgs) returnResult body
-  pure (binderNodes ++ bodyNodes)
-lowerDefinitionFlow _ = liftEither (Left "internal check error: expected annotated definition")
-
-viewAnyType :: ViewExpr
-viewAnyType = VEName "Any"
-
-canonicalDefinitionViews :: [DefArg] -> Maybe ViewExpr -> ([DefArg], Maybe ViewExpr, ViewExpr)
-canonicalDefinitionViews args ret = (args, ret, declaredDefinitionView args ret)
-
-declaredDefinitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
-declaredDefinitionView args ret =
-  case map argType args of
-    [] -> resultType
-    views -> viewExprFn views resultType
-  where
-    resultType = maybe viewAnyType id ret
-
-argType :: DefArg -> ViewExpr
-argType (DefBinder _ Nothing) = viewAnyType
-argType (DefBinder _ (Just ty)) = ty
-argType (DefPhantom ty) = ty
-
-emitDeclaration :: Integer -> [String] -> String -> LowerM String
-emitDeclaration sym [] retExpr = do
-  payload <- payloadSourceFor sym
-  pure $ "typedValue " ++ show sym ++ " " ++ parens retExpr ++ " " ++ payload
-emitDeclaration sym views retExpr = do
-  payload <- payloadSourceFor sym
-  pure $ "typedValue " ++ show sym ++ " (viewFn [" ++ unwords (map parens views) ++ "] " ++ parens retExpr ++ ") " ++ payload
-
-typedValueNode :: Integer -> ViewExpr -> LowerM String
-typedValueNode sym view = typedValueNodeWithProvenance sym view ViewChecked
-
-typedValueNodeWithProvenance :: Integer -> ViewExpr -> ViewProvenance -> LowerM String
-typedValueNodeWithProvenance sym view provenance = do
-  viewExpr <- liftEither (lowerViewExpr view)
-  payload <- payloadSourceFor sym
-  pure ("typedValueWithProvenance " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload ++ " " ++ viewProvenanceSource provenance)
-
-typedRequireNode :: Integer -> ViewExpr -> LowerM String
-typedRequireNode sym view = do
-  viewExpr <- liftEither (lowerViewExpr view)
-  payload <- payloadSourceFor sym
-  pure ("typedRequire " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload)
-
-viewProvenanceSource :: ViewProvenance -> String
-viewProvenanceSource ViewChecked = "viewProvenanceChecked"
-viewProvenanceSource ViewTrusted = "viewProvenanceTrusted"
-viewProvenanceSource ViewUnchecked = "viewProvenanceUnchecked"
-
-declareKnown :: Integer -> ViewExpr -> LowerM String
-declareKnown sym view = do
-  recordKnown sym view
-  typedValueNode sym view
-
-declareKnownWithPayload :: Integer -> ViewExpr -> T -> LowerM String
-declareKnownWithPayload sym view payload = do
-  recordPayload sym payload
-  declareKnown sym view
-
-declareKnownFresh :: ViewExpr -> LowerM (Integer, [String])
-declareKnownFresh view = do
-  sym <- freshSym
-  node <- declareKnown sym view
-  pure (sym, [node])
-
-declareKnownFreshWithPayload :: ViewExpr -> T -> LowerM (Integer, [String])
-declareKnownFreshWithPayload view payload = do
-  sym <- freshSym
-  node <- declareKnownWithPayload sym view payload
-  pure (sym, [node])
-
-declareAndRequireFresh :: ViewExpr -> LowerM (Integer, [String])
-declareAndRequireFresh view = do
-  sym <- freshSym
-  declareNode <- declareKnown sym view
-  requireNode <- typedRequireNode sym view
-  pure (sym, [declareNode, requireNode])
-
-declareAndRequireFreshWithPayload :: ViewExpr -> T -> LowerM (Integer, [String])
-declareAndRequireFreshWithPayload view payload = do
-  sym <- freshSym
-  declareNode <- declareKnownWithPayload sym view payload
-  requireNode <- typedRequireNode sym view
-  pure (sym, [declareNode, requireNode])
-
-lowerBinderDeclaration :: DefArg -> LowerM [String]
-lowerBinderDeclaration (DefBinder name mTy) = do
-  sym <- symbolForLocal name
-  node <- declareKnown sym (maybe viewAnyType id mTy)
-  pure [node]
-lowerBinderDeclaration (DefPhantom _) = pure []
-
-lowerBodyWithPhantoms :: [ViewExpr] -> ViewExpr -> TricuAST -> LowerM [String]
-lowerBodyWithPhantoms [] _ SLambda {} = pure []
-lowerBodyWithPhantoms [] expected body =
-  lowerExprAgainst body expected
-lowerBodyWithPhantoms phantomViews expected (SLambda params body) =
-  lowerLambdaSpine phantomViews expected params body
-lowerBodyWithPhantoms phantomViews expected body =
-  lowerExprAgainst body (residualViewExpr phantomViews expected)
-
-lowerLambdaSpine :: [ViewExpr] -> ViewExpr -> [String] -> TricuAST -> LowerM [String]
-lowerLambdaSpine phantomViews expected [] body = lowerBodyWithPhantoms phantomViews expected body
-lowerLambdaSpine [] _ _ _ = pure []
-lowerLambdaSpine (view : views) expected (param : params) body =
-  withLocalBinder param $ \paramSym -> do
-    declareParam <- declareKnown paramSym view
-    restNodes <- lowerLambdaSpine views expected params body
-    pure (declareParam : restNodes)
-
-residualViewExpr :: [ViewExpr] -> ViewExpr -> ViewExpr
-residualViewExpr [] resultView = resultView
-residualViewExpr args resultView = viewExprFn args resultView
-
-phantomArgs :: [DefArg] -> [DefArg]
-phantomArgs [] = []
-phantomArgs (DefPhantom ty : rest) = DefPhantom ty : phantomArgs rest
-phantomArgs (_ : rest) = phantomArgs rest
-
-lowerPhantomArgType :: DefArg -> ViewExpr
-lowerPhantomArgType (DefPhantom ty) = ty
-lowerPhantomArgType _ = error "internal check error: expected phantom arg"
-
-lowerReturnObligation :: Maybe ViewExpr -> LowerM ([ViewExpr], ViewExpr)
-lowerReturnObligation Nothing = pure ([], viewAnyType)
-lowerReturnObligation (Just ty) = pure (peelFnObligation ty)
-
-peelFnObligation :: ViewExpr -> ([ViewExpr], ViewExpr)
-peelFnObligation ty = case viewExprFnParts ty of
-  Just (args, resultView) ->
-    let (restArgs, finalResult) = peelFnObligation resultView
-    in (args ++ restArgs, finalResult)
-  Nothing -> ([], ty)
-
-withDefinitionScope :: [DefArg] -> LowerM a -> LowerM a
-withDefinitionScope args action = do
-  binderEntries <- mapM allocateBinder [ name | DefBinder name _ <- args ]
-  modify $ \st -> st { scopes = Map.fromList binderEntries : scopes st }
-  resultValue <- action
-  modify $ \st -> st { scopes = drop 1 (scopes st) }
-  pure resultValue
-
-allocateBinder :: String -> LowerM (String, Integer)
-allocateBinder name = do
-  sym <- freshSym
-  recordDebugName sym name
-  pure (name, sym)
-
-withLocalBinder :: String -> (Integer -> LowerM a) -> LowerM a
-withLocalBinder name action = do
-  sym <- freshSym
-  recordDebugName sym name
-  withLocalAlias name sym (action sym)
-
-withLocalAlias :: String -> Integer -> LowerM a -> LowerM a
-withLocalAlias name sym action = do
-  modify $ \st -> st { scopes = Map.singleton name sym : scopes st }
-  resultValue <- action
-  modify $ \st -> st { scopes = drop 1 (scopes st) }
-  pure resultValue
-
-recordKnown :: Integer -> ViewExpr -> LowerM ()
-recordKnown sym view =
-  modify $ \st -> st { knownNodeViews = Map.insert sym view (knownNodeViews st) }
-
-recordPayload :: Integer -> T -> LowerM ()
-recordPayload sym payload =
-  modify $ \st -> st { nodePayloads = Map.insert sym payload (nodePayloads st) }
-
-payloadFor :: Integer -> LowerM (Maybe T)
-payloadFor sym = do
-  st <- get
-  pure (Map.lookup sym (nodePayloads st))
-
-payloadSourceFor :: Integer -> LowerM String
-payloadSourceFor sym = maybe "t" treeSource <$> payloadFor sym
-
-knownNodeViewFor :: Integer -> LowerM (Maybe ViewExpr)
-knownNodeViewFor sym = do
-  st <- get
-  pure (Map.lookup sym (knownNodeViews st))
-
-recordDebugName :: Integer -> String -> LowerM ()
-recordDebugName sym label =
-  modify $ \st -> st { debugNames = Map.insertWith keepExisting sym label (debugNames st) }
-  where
-    keepExisting _ old = old
-
-lowerExpr :: TricuAST -> LowerM (Integer, [String])
-lowerExpr expr = do
-  (sym, nodes, _) <- lowerExprKnown expr
-  pure (sym, nodes)
-
-lowerExprAgainst :: TricuAST -> ViewExpr -> LowerM [String]
-lowerExprAgainst body expected = do
-  (_, nodes, _) <- lowerExprKnownAgainst body expected
-  pure nodes
-
-lowerExprKnownAgainst :: TricuAST -> ViewExpr -> LowerM (Integer, [String], Maybe ViewExpr)
-lowerExprKnownAgainst expr expected = case (expr, viewExprAsType expected) of
-  (SApp (SApp (SVar "pair" _) left) right, Just (VTPair leftView rightView)) ->
-    let leftExpr = viewTypeToExpr leftView
-        rightExpr = viewTypeToExpr rightView
-    in lowerUnshadowedConstructor "pair" expr expected $ do
-      (_, leftNodes, _) <- lowerExprKnownAgainst left leftExpr
-      (_, rightNodes, _) <- lowerExprKnownAgainst right rightExpr
-      (sym, nodes) <- declareAndRequireFresh expected
-      pure (sym, leftNodes ++ rightNodes ++ nodes, Just expected)
-  (SApp (SVar "just" _) value, Just (VTMaybe elemView)) ->
-    let elemExpr = viewTypeToExpr elemView
-    in lowerUnshadowedConstructor "just" expr expected $ do
-      (_, valueNodes, _) <- lowerExprKnownAgainst value elemExpr
-      (sym, nodes) <- declareAndRequireFresh expected
-      pure (sym, valueNodes ++ nodes, Just expected)
-  (SVar "nothing" _, Just (VTMaybe _)) ->
-    lowerUnshadowedConstructor "nothing" expr expected $ do
-      (sym, nodes) <- declareAndRequireFresh expected
-      pure (sym, nodes, Just expected)
-  (SApp (SApp (SVar "ok" _) value) rest, Just (VTResult _ okView)) ->
-    lowerUnshadowedConstructor "ok" expr expected $
-      lowerResultConstructor expected (viewTypeToExpr okView) value rest
-  (SApp (SApp (SVar "err" _) value) rest, Just (VTResult errView _)) ->
-    lowerUnshadowedConstructor "err" expr expected $
-      lowerResultConstructor expected (viewTypeToExpr errView) value rest
-  (SLet name value body, _) -> do
-    (valueSym, valueNodes, _) <- lowerExprKnown value
-    recordDebugName valueSym name
-    bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected)
-    let (bodySym, bodyNodes, bodyKnown) = bodyResult
-    pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
-  -- Hand-written immediately-applied lambda (not compiler output; let/where
-  -- now emit SLet). Kept for source that relies on alias semantics.
-  (SApp (SLambda [name] body) value, _) -> do
-    (valueSym, valueNodes, _) <- lowerExprKnown value
-    bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected)
-    let (bodySym, bodyNodes, bodyKnown) = bodyResult
-    pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
-  (SList items, Just (VTList elemView)) -> do
-    let elemExpr = viewTypeToExpr elemView
-    lowered <- mapM (`lowerExprKnownAgainst` elemExpr) items
-    let itemNodes = concat [ nodes | (_, nodes, _) <- lowered ]
-    (sym, nodes) <- declareAndRequireFresh expected
-    pure (sym, itemNodes ++ nodes, Just expected)
-  (SLambda _ _, _) ->
-    case peelFnObligation expected of
-      ([], _) -> lowerExprKnownAndRequire expr expected
-      (argViews, resultView) -> lowerLambdaAgainst argViews resultView expr
-  _ -> lowerExprKnownAndRequire expr expected
-
-lowerUnshadowedConstructor :: String -> TricuAST -> ViewExpr -> LowerM (Integer, [String], Maybe ViewExpr) -> LowerM (Integer, [String], Maybe ViewExpr)
-lowerUnshadowedConstructor name fallback expected lowerCtor = do
-  ctorIsUnbound <- nameIsUnbound name
-  if ctorIsUnbound
-    then lowerCtor
-    else lowerExprKnownAndRequire fallback expected
-
-lowerResultConstructor :: ViewExpr -> ViewExpr -> TricuAST -> TricuAST -> LowerM (Integer, [String], Maybe ViewExpr)
-lowerResultConstructor expected valueView value rest = do
-  (_, valueNodes, _) <- lowerExprKnownAgainst value valueView
-  (_, restNodes, _) <- lowerExprKnown rest
-  (sym, nodes) <- declareAndRequireFresh expected
-  pure (sym, valueNodes ++ restNodes ++ nodes, Just expected)
-
-lowerExprKnownAndRequire :: TricuAST -> ViewExpr -> LowerM (Integer, [String], Maybe ViewExpr)
-lowerExprKnownAndRequire body expected = do
-  (bodySym, bodyNodes, known) <- lowerExprKnown body
-  requireNode <- typedRequireNode bodySym expected
-  pure (bodySym, bodyNodes ++ [requireNode], known)
-
-lowerLambdaAgainst :: [ViewExpr] -> ViewExpr -> TricuAST -> LowerM (Integer, [String], Maybe ViewExpr)
-lowerLambdaAgainst argViews resultView (SLambda params body) = do
-  nodes <- lowerLambdaSpine argViews resultView params body
-  sym <- freshSym
-  let fnView = residualViewExpr argViews resultView
-  declareNode <- declareKnown sym fnView
-  pure (sym, nodes ++ [declareNode], Just fnView)
-lowerLambdaAgainst argViews resultView body =
-  lowerExprKnownAndRequire body (residualViewExpr argViews resultView)
-
-lowerExprKnown :: TricuAST -> LowerM (Integer, [String], Maybe ViewExpr)
-lowerExprKnown (SVar name _) = do
-  sym <- symbolForName name
-  known <- knownNodeViewFor sym
-  pure (sym, [], known)
-lowerExprKnown (SStr s) = do
-  let view = VEName "String"
-  (sym, nodes) <- declareKnownFreshWithPayload view (ofString s)
-  recordDebugName sym "string literal"
-  pure (sym, nodes, Just view)
-lowerExprKnown (SInt n)
-  | n >= 0 && n <= 255 = do
-      let view = VEName "Byte"
-      (sym, nodes) <- declareKnownFreshWithPayload view (ofNumber n)
-      recordDebugName sym "byte literal"
-      pure (sym, nodes, Just view)
-  | otherwise = do
-      sym <- freshSym
-      pure (sym, [], Nothing)
-lowerExprKnown TLeaf = do
-  let view = VEName "Unit"
-  (sym, nodes) <- declareKnownFreshWithPayload view Leaf
-  recordDebugName sym "unit literal"
-  pure (sym, nodes, Just view)
-lowerExprKnown (SList items) = do
-  (sym, nodes, view, _) <- lowerListLiteral items
-  pure (sym, nodes, Just view)
-lowerExprKnown (SLet name value body) = do
-  (valueSym, valueNodes, _) <- lowerExprKnown value
-  recordDebugName valueSym name
-  bodyResult <- withLocalAlias name valueSym (lowerExprKnown body)
-  let (bodySym, bodyNodes, bodyKnown) = bodyResult
-  pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
--- Hand-written immediately-applied lambda (not compiler output; let/where
--- now emit SLet). Kept for source that relies on alias semantics.
-lowerExprKnown (SApp (SLambda [name] body) value) = do
-  (valueSym, valueNodes, known) <- lowerExprKnown value
-  bodyResult <- withLocalAlias name valueSym (lowerExprKnown body)
-  let (bodySym, bodyNodes, bodyKnown) = bodyResult
-  pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
-lowerExprKnown (SApp func arg) = do
-  (funcSym, funcNodes, funcKnown) <- lowerExprKnown func
-  (argSym, argNodes, _) <- lowerApplicationArgument funcKnown arg
-  outSym <- freshSym
-  recordDebugName outSym (applicationDebugLabel func)
-  funcPayload <- payloadFor funcSym
-  argPayload <- payloadFor argSym
-  case (funcPayload, argPayload) of
-    (Just f, Just a) -> recordPayload outSym (apply f a)
-    _ -> pure ()
-  applyPayload <- payloadSourceFor outSym
-  let applyNode = "typedApply " ++ show outSym ++ " " ++ show funcSym ++ " " ++ show argSym ++ " " ++ applyPayload
-      outKnown = applicationResultView funcKnown
-  mapM_ (recordKnown outSym) outKnown
-  pure (outSym, funcNodes ++ argNodes ++ [applyNode], outKnown)
-lowerExprKnown (SLambda params body) = do
-  nodes <- lowerUnannotatedLambda params body
-  sym <- freshSym
-  pure (sym, nodes, Nothing)
-lowerExprKnown _ = do
-  sym <- freshSym
-  pure (sym, [], Nothing)
-
-lowerListLiteral :: [TricuAST] -> LowerM (Integer, [String], ViewExpr, [Integer])
-lowerListLiteral items = do
-  lowered <- mapM lowerExprKnown items
-  let itemSyms = [ itemSym | (itemSym, _, _) <- lowered ]
-      itemNodes = concat [ nodes | (_, nodes, _) <- lowered ]
-      view = listLiteralView [ known | (_, _, known) <- lowered ]
-  itemPayloads <- mapM payloadFor itemSyms
-  let mPayload = ofList <$> sequence itemPayloads
-  (sym, declareNodes) <- case mPayload of
-    Just payload -> declareKnownFreshWithPayload view payload
-    Nothing -> declareKnownFresh view
-  pure (sym, itemNodes ++ declareNodes, view, itemSyms)
-
-lowerApplicationArgument :: Maybe ViewExpr -> TricuAST -> LowerM (Integer, [String], Maybe ViewExpr)
-lowerApplicationArgument (Just fnView) arg =
-  case viewExprFnParts fnView of
-    Just (argView : _, _)
-      | containsViewVar argView -> lowerExprKnown arg
-      | otherwise -> lowerExprKnownAgainst arg argView
-    _ -> lowerExprKnown arg
-lowerApplicationArgument _ arg =
-  lowerExprKnown arg
-
-containsViewVar :: ViewExpr -> Bool
-containsViewVar view = case view of
-  VEVar _ -> True
-  VEVarId _ -> True
-  VEList items -> any containsViewVar items
-  VEApp f a -> containsViewVar f || containsViewVar a
-  VEForall _ body -> containsViewVar body
-  VEExists _ body -> containsViewVar body
-  _ -> False
-
-applicationDebugLabel :: TricuAST -> String
-applicationDebugLabel func =
-  case applicationHeadName func of
-    Just name -> name ++ " application result"
-    Nothing   -> "application result"
-
-applicationHeadName :: TricuAST -> Maybe String
-applicationHeadName (SVar name _) = Just name
-applicationHeadName (SApp func _) = applicationHeadName func
-applicationHeadName _ = Nothing
-
-applicationResultView :: Maybe ViewExpr -> Maybe ViewExpr
-applicationResultView (Just fnView) = case viewExprFnParts fnView of
-  Just (_ : restArgs, resultView) ->
-    Just $ case restArgs of
-      [] -> resultView
-      _  -> viewExprFn restArgs resultView
-  _ -> Nothing
-applicationResultView _ = Nothing
-
-listLiteralView :: [Maybe ViewExpr] -> ViewExpr
-listLiteralView [] = viewExprList viewAnyType
-listLiteralView (Just firstView : rest)
-  | all (== Just firstView) rest = viewExprList firstView
-listLiteralView _ = viewExprList viewAnyType
-
-lowerUnannotatedLambda :: [String] -> TricuAST -> LowerM [String]
-lowerUnannotatedLambda [] body = do
-  (_, nodes) <- lowerExpr body
-  pure nodes
-lowerUnannotatedLambda (param : params) body =
-  withLocalBinder param $ \paramSym -> do
-    declareParam <- declareKnown paramSym viewAnyType
-    restNodes <- lowerUnannotatedLambda params body
-    pure (declareParam : restNodes)
-
-symbolForTop :: String -> LowerM Integer
-symbolForTop name = do
-  st <- get
-  case Map.lookup name (topSyms st) of
-    Just sym -> pure sym
-    Nothing -> liftEither (Left $ "internal check error: missing top-level symbol: " ++ name)
-
-symbolForLocal :: String -> LowerM Integer
-symbolForLocal name = do
-  st <- get
-  case lookupInScopes name (scopes st) of
-    Just sym -> pure sym
-    Nothing -> liftEither (Left $ "internal check error: missing local symbol: " ++ name)
-
-symbolForName :: String -> LowerM Integer
-symbolForName name = do
-  st <- get
-  case lookupInScopes name (scopes st) of
-    Just sym -> pure sym
-    Nothing -> case Map.lookup name (topSyms st) of
-      Just sym -> pure sym
-      Nothing -> symbolForExternal name
-
-symbolForExternal :: String -> LowerM Integer
-symbolForExternal name = do
-  st <- get
-  case Map.lookup name (externSyms st) of
-    Just sym -> pure sym
-    Nothing -> do
-      sym <- freshSym
-      recordDebugName sym ("external " ++ name)
-      modify $ \st' -> st' { externSyms = Map.insert name sym (externSyms st') }
-      pure sym
-
-nameIsUnbound :: String -> LowerM Bool
-nameIsUnbound name = do
-  st <- get
-  pure $ case lookupInScopes name (scopes st) of
-    Just _ -> False
-    Nothing -> Map.notMember name (topSyms st)
-
-lookupInScopes :: String -> [Map.Map String Integer] -> Maybe Integer
-lookupInScopes _ [] = Nothing
-lookupInScopes name (scope : rest) =
-  case Map.lookup name scope of
-    Just sym -> Just sym
-    Nothing -> lookupInScopes name rest
-
-freshSym :: LowerM Integer
-freshSym = do
-  st <- get
-  let sym = nextSym st
-  put st { nextSym = sym + 1 }
-  pure sym
-
-isDefinition :: TricuAST -> Bool
-isDefinition SDef {} = True
-isDefinition SDefAnn {} = True
-isDefinition _ = False
-
-definitionName :: TricuAST -> String
-definitionName (SDef name _ _) = name
-definitionName (SDefAnn name _ _ _) = name
-definitionName _ = error "definitionName: expected top-level definition"
-
-liftEither :: Either String a -> LowerM a
-liftEither value = StateT $ \st -> case value of
-  Left err -> Left err
-  Right resultValue -> Right (resultValue, st)
-
-lowerArgView :: DefArg -> LowerM String
-lowerArgView (DefBinder _ Nothing) = pure "viewAny"
-lowerArgView (DefBinder _ (Just ty)) = liftEither (lowerViewExpr ty)
-lowerArgView (DefPhantom ty) = liftEither (lowerViewExpr ty)
-
-viewTypeToExpr :: ViewType -> ViewExpr
-viewTypeToExpr view = case view of
-  VTName name -> VEName name
-  VTVar varId -> VEVarId varId
-  VTRef n -> VEApp (VEName "Ref") (VEInt n)
-  VTRefText s -> VEApp (VEName "Ref") (VEString s)
-  VTList item -> VEApp (VEName "List") (viewTypeToExpr item)
-  VTMaybe item -> VEApp (VEName "Maybe") (viewTypeToExpr item)
-  VTPair left right -> VEApp (VEApp (VEName "Pair") (viewTypeToExpr left)) (viewTypeToExpr right)
-  VTResult err ok -> VEApp (VEApp (VEName "Result") (viewTypeToExpr err)) (viewTypeToExpr ok)
-  VTGuarded base guard -> VEApp (VEApp (VEName "viewGuarded") (viewTypeToExpr base)) (VERaw (treeSource guard))
-  VTForall binders body -> VEForall binders (viewTypeToExpr body)
-  VTExists binders body -> VEExists binders (viewTypeToExpr body)
-  VTFn args resultView -> viewExprFn (map viewTypeToExpr args) (viewTypeToExpr resultView)
-
-viewExprFn :: [ViewExpr] -> ViewExpr -> ViewExpr
-viewExprFn args resultView = VEApp (VEApp (VEName "Fn") (VEList args)) resultView
-
-viewExprList :: ViewExpr -> ViewExpr
-viewExprList = VEApp (VEName "List")
-
-viewExprFnParts :: ViewExpr -> Maybe ([ViewExpr], ViewExpr)
-viewExprFnParts (VEForall _ body) = viewExprFnParts body
-viewExprFnParts (VEApp (VEApp (VEName "Fn") (VEList args)) resultView) = Just (args, resultView)
-viewExprFnParts _ = Nothing
-
-viewExprAsType :: ViewExpr -> Maybe ViewType
-viewExprAsType view = case view of
-  VEName name -> Just (VTName name)
-  VEVar _ -> Nothing
-  VEVarId varId -> Just (VTVar varId)
-  VEApp (VEName "Ref") (VEInt n) -> Just (VTRef n)
-  VEApp (VEName "Ref") (VEString s) -> Just (VTRefText s)
-  VEApp (VEName "List") item -> VTList <$> viewExprAsType item
-  VEApp (VEName "Maybe") item -> VTMaybe <$> viewExprAsType item
-  VEApp (VEApp (VEName "Pair") left) right -> VTPair <$> viewExprAsType left <*> viewExprAsType right
-  VEApp (VEApp (VEName "Result") err) ok -> VTResult <$> viewExprAsType err <*> viewExprAsType ok
-  VEApp (VEApp (VEName "Fn") (VEList args)) resultView -> VTFn <$> mapM viewExprAsType args <*> viewExprAsType resultView
-  VEForall binders body -> VTForall binders <$> viewExprAsType body
-  VEExists binders body -> VTExists binders <$> viewExprAsType body
-  _ -> Nothing
-
-lowerViewExpr :: ViewExpr -> Either String String
-lowerViewExpr ty = case ty of
-  VEName "Any" -> Right "viewAny"
-  VEName "Bool" -> Right "viewBool"
-  VEName "String" -> Right "viewString"
-  VEName "Byte" -> Right "viewByte"
-  VEName "Unit" -> Right "viewUnit"
-  VEName name -> Right name
-  VEVar name -> Left $ "polymorphic View variables are unsupported: " ++ show name
-  VEVarId varId -> Left $ "polymorphic View variables are unsupported: " ++ show varId
-  VEInt n -> Right (show n)
-  VEString s -> Right (show s)
-  VEList items -> do
-    itemExprs <- mapM lowerViewExpr items
-    Right $ "[" ++ unwords (map parens itemExprs) ++ "]"
-  VEApp (VEName "Ref") (VEInt n) -> Right $ "viewRef " ++ show n
-  VEApp (VEName "Ref") (VEString s) -> Right $ "viewRef " ++ show s
-  VEApp (VEName "List") elemView -> do
-    elemExpr <- lowerViewExpr elemView
-    Right $ "viewList " ++ parens elemExpr
-  VEApp (VEName "Maybe") elemView -> do
-    elemExpr <- lowerViewExpr elemView
-    Right $ "viewMaybe " ++ parens elemExpr
-  VEApp (VEApp (VEName "Pair") left) right -> do
-    l <- lowerViewExpr left
-    r <- lowerViewExpr right
-    Right $ "viewPair " ++ parens l ++ " " ++ parens r
-  VEApp (VEApp (VEName "Result") err) ok -> do
-    e <- lowerViewExpr err
-    a <- lowerViewExpr ok
-    Right $ "viewResult " ++ parens e ++ " " ++ parens a
-  VEApp (VEApp (VEName "Fn") (VEList args)) resultView -> do
-    as <- mapM lowerViewExpr args
-    r <- lowerViewExpr resultView
-    Right $ "viewFn [" ++ unwords (map parens as) ++ "] " ++ parens r
-  VEApp func arg -> do
-    f <- lowerViewExpr func
-    a <- lowerViewExpr arg
-    Right $ parens f ++ " " ++ parens a
-  VEForall _ _ -> Left "quantified View contracts are unsupported"
-  VEExists _ _ -> Left "existential View contracts are unsupported"
-  VERaw raw -> Right raw
-
-treeSource :: T -> String
-treeSource Leaf = "t"
-treeSource (Stem x) = "(t " ++ treeSource x ++ ")"
-treeSource (Fork x y) = "(t " ++ treeSource x ++ " " ++ treeSource y ++ ")"
-
-parens :: String -> String
-parens s = "(" ++ s ++ ")"

src/Check/IO.hs

@@ -1,422 +0,0 @@
-module Check.IO
-  ( instrumentIOContinuations
-  ) where
-
-import Control.Monad.State.Strict
-import qualified Data.Map as Map
-
-import Check.Core (lowerViewExpr)
-import Parser (parseTricu)
-import Research
-
-viewAnyType :: ViewExpr
-viewAnyType = VEName "Any"
-
-argType :: DefArg -> ViewExpr
-argType (DefBinder _ Nothing) = viewAnyType
-argType (DefBinder _ (Just ty)) = ty
-argType (DefPhantom ty) = ty
-
-declaredDefinitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
-declaredDefinitionView args ret =
-  case map argType args of
-    [] -> resultType
-    views -> viewExprFn views resultType
-  where
-    resultType = maybe viewAnyType id ret
-
-viewExprFn :: [ViewExpr] -> ViewExpr -> ViewExpr
-viewExprFn args resultView = VEApp (VEApp (VEName "Fn") (VEList args)) resultView
-
-viewExprList :: ViewExpr -> ViewExpr
-viewExprList = VEApp (VEName "List")
-
-viewExprFnParts :: ViewExpr -> Maybe ([ViewExpr], ViewExpr)
-viewExprFnParts (VEForall _ body) = viewExprFnParts body
-viewExprFnParts (VEApp (VEApp (VEName "Fn") (VEList args)) resultView) = Just (args, resultView)
-viewExprFnParts _ = Nothing
-
-viewExprAsType :: ViewExpr -> Maybe ViewType
-viewExprAsType view = case view of
-  VEName name -> Just (VTName name)
-  VEVar _ -> Nothing
-  VEVarId varId -> Just (VTVar varId)
-  VEApp (VEName "Ref") (VEInt n) -> Just (VTRef n)
-  VEApp (VEName "Ref") (VEString st) -> Just (VTRefText st)
-  VEApp (VEName "List") item -> VTList <$> viewExprAsType item
-  VEApp (VEName "Maybe") item -> VTMaybe <$> viewExprAsType item
-  VEApp (VEApp (VEName "Pair") left) right -> VTPair <$> viewExprAsType left <*> viewExprAsType right
-  VEApp (VEApp (VEName "Result") err) ok -> VTResult <$> viewExprAsType err <*> viewExprAsType ok
-  VEApp (VEApp (VEName "Fn") (VEList args)) resultView -> VTFn <$> mapM viewExprAsType args <*> viewExprAsType resultView
-  VEForall binders body -> VTForall binders <$> viewExprAsType body
-  VEExists binders body -> VTExists binders <$> viewExprAsType body
-  _ -> Nothing
-
-viewTypeToExpr :: ViewType -> ViewExpr
-viewTypeToExpr view = case view of
-  VTName name -> VEName name
-  VTVar varId -> VEVarId varId
-  VTRef n -> VEApp (VEName "Ref") (VEInt n)
-  VTRefText st -> VEApp (VEName "Ref") (VEString st)
-  VTList item -> VEApp (VEName "List") (viewTypeToExpr item)
-  VTMaybe item -> VEApp (VEName "Maybe") (viewTypeToExpr item)
-  VTPair left right -> VEApp (VEApp (VEName "Pair") (viewTypeToExpr left)) (viewTypeToExpr right)
-  VTResult err ok -> VEApp (VEApp (VEName "Result") (viewTypeToExpr err)) (viewTypeToExpr ok)
-  VTGuarded base guard -> VEApp (VEApp (VEName "viewGuarded") (viewTypeToExpr base)) (VERaw (treeSource guard))
-  VTForall binders body -> VEForall binders (viewTypeToExpr body)
-  VTExists binders body -> VEExists binders (viewTypeToExpr body)
-  VTFn args resultView -> viewExprFn (map viewTypeToExpr args) (viewTypeToExpr resultView)
-
-treeSource :: T -> String
-treeSource Leaf = "t"
-treeSource (Stem x) = "(t " ++ treeSource x ++ ")"
-treeSource (Fork x y) = "(t " ++ treeSource x ++ " " ++ treeSource y ++ ")"
-
-applicationResultView :: Maybe ViewExpr -> Maybe ViewExpr
-applicationResultView (Just fnView) = case viewExprFnParts fnView of
-  Just (_ : restArgs, resultView) ->
-    Just $ case restArgs of
-      [] -> resultView
-      _  -> viewExprFn restArgs resultView
-  _ -> Nothing
-applicationResultView _ = Nothing
-
--- Instrument source-level IO continuations so pure calls to annotated
--- functions can run the already-portable checked-exec protocol at runtime.
--- This is deliberately a lowering pass: it builds checked boundaries once from
--- source annotations, then ordinary IO execution only evaluates runChecked.
-instrumentIOContinuations :: [TricuAST] -> Either String [TricuAST]
-instrumentIOContinuations asts = mapM transformTop asts
-  where
-    contracts = Map.fromList
-      [ (name, (args, ret, body))
-      | SDefAnn name args ret body <- asts
-      , all isRuntimeBinder args
-      ]
-
-    isRuntimeBinder DefBinder {} = True
-    isRuntimeBinder DefPhantom {} = False
-
-    transformTop (SDef name params body) = SDef name params <$> transformExpr body
-    transformTop (SDefAnn name args ret body) = SDefAnn name args ret <$> transformExpr body
-    transformTop other = transformExpr other
-
-    transformExpr expr = case expr of
-      SApp (SVar "io" h) action -> SApp (SVar "io" h) <$> transformIOAction action
-      SApp f a -> SApp <$> transformExpr f <*> transformExpr a
-      SLambda params body -> SLambda params <$> transformExpr body
-      SLet name val body -> SLet name <$> transformExpr val <*> transformExpr body
-      TStem x -> TStem <$> transformExpr x
-      TFork x y -> TFork <$> transformExpr x <*> transformExpr y
-      _ -> pure expr
-
-    transformIOAction action = case action of
-      SApp (SVar "pure" _) value ->
-        case checkedPureActionFor value of
-          Just checked -> parseOne checked
-          Nothing -> SApp (SVar "pure" Nothing) <$> transformExpr value
-      SApp (SApp (SVar "bind" h) left) (SLambda params body) ->
-        SApp <$> (SApp (SVar "bind" h) <$> transformIOAction left) <*> (SLambda params <$> transformIOAction body)
-      SApp f a -> SApp <$> transformIOAction f <*> transformIOAction a
-      SLambda params body -> SLambda params <$> transformIOAction body
-      SLet name val body -> SLet name <$> transformIOAction val <*> transformIOAction body
-      _ -> transformExpr action
-
-    checkedPureActionFor value =
-      case contractedApplication value of
-        Just (name, defArgs, ret, body, callArgs) ->
-          Just (checkedPureApplicationActionSource contracts name defArgs ret body callArgs)
-        Nothing ->
-          if mentionsContractedName contracts value
-            then Just (checkedPureValueActionSource contracts value)
-            else Nothing
-      where
-        contractedApplication valueExpr = do
-          (headExpr, callArgs) <- applicationSpine valueExpr
-          name <- case headExpr of
-            SVar n _ -> Just n
-            _ -> Nothing
-          (defArgs, ret, body) <- Map.lookup name contracts
-          if length callArgs == length defArgs
-            then Just (name, defArgs, ret, body, callArgs)
-            else Nothing
-
-    parseOne source = case parseTricu source of
-      [expr] -> Right expr
-      _ -> Left $ "internal check error: could not parse generated checked IO action: " ++ source
-
-applicationSpine :: TricuAST -> Maybe (TricuAST, [TricuAST])
-applicationSpine expr = Just (go expr [])
-  where
-    go (SApp f a) args = go f (a : args)
-    go headExpr args = (headExpr, args)
-
-checkedPureApplicationActionSource :: RuntimeContracts -> String -> [DefArg] -> Maybe ViewExpr -> TricuAST -> [TricuAST] -> String
-checkedPureApplicationActionSource contracts name defArgs ret body callArgs =
-  checkedProgramAction boundaryProgram ("(_ runtimeEnv : " ++ bodyAction ++ ")")
-  where
-    argViews = map argType defArgs
-    retView = maybe viewAnyType id ret
-    fnView = "viewFn [" ++ unwords (map (parens . unsafeLowerViewExpr) argViews) ++ "] " ++ parens (unsafeLowerViewExpr retView)
-    boundaryRoot = fromIntegral (length callArgs * 2) :: Integer
-    boundaryProgram = "typedProgram " ++ show boundaryRoot ++ " [" ++ unwords (map parens boundaryNodes) ++ "]"
-    boundaryNodes = functionNode : concat argApplyNodes
-    functionNode = "typedValue 0 " ++ parens fnView ++ " " ++ parens (astSource (SVar name Nothing))
-    argApplyNodes =
-      [ let argSym = fromIntegral (idx * 2 - 1) :: Integer
-            outSym = fromIntegral (idx * 2) :: Integer
-            calleeSym = if idx == 1 then 0 else fromIntegral ((idx - 1) * 2)
-            argView = argRuntimeViewSource view
-            prefixArgs = take idx callArgs
-            payload = astSource (foldl SApp (SVar name Nothing) prefixArgs)
-        in [ "typedValue " ++ show argSym ++ " " ++ parens argView ++ " " ++ parens (astSource arg)
-           , "typedApply " ++ show outSym ++ " " ++ show calleeSym ++ " " ++ show argSym ++ " " ++ parens payload
-           ]
-      | (idx, (view, arg)) <- zip [1 :: Int ..] (zip argViews callArgs)
-      ]
-    (bodyRoot, bodyNodes) = runtimeBodyProgramNodes contracts defArgs retView body callArgs
-    bodyProgram = "typedProgram " ++ show bodyRoot ++ " [" ++ unwords (map parens bodyNodes) ++ "]"
-    bodyAction = checkedProgramAction bodyProgram "(value runtimeEnv : pure value)"
-
-type RuntimeContracts = Map.Map String ([DefArg], Maybe ViewExpr, TricuAST)
-
-mentionsContractedName :: RuntimeContracts -> TricuAST -> Bool
-mentionsContractedName contracts expr = case expr of
-  SVar name _ -> Map.member name contracts
-  SApp f a -> mentionsContractedName contracts f || mentionsContractedName contracts a
-  SLambda _ body -> mentionsContractedName contracts body
-  SLet _ val body -> mentionsContractedName contracts val || mentionsContractedName contracts body
-  SList items -> any (mentionsContractedName contracts) items
-  TStem x -> mentionsContractedName contracts x
-  TFork x y -> mentionsContractedName contracts x || mentionsContractedName contracts y
-  SDef _ _ body -> mentionsContractedName contracts body
-  SDefAnn _ _ _ body -> mentionsContractedName contracts body
-  _ -> False
-
-checkedPureValueActionSource :: RuntimeContracts -> TricuAST -> String
-checkedPureValueActionSource contracts value =
-  checkedProgramAction program "(value runtimeEnv : pure value)"
-  where
-    (rootSym, nodes) = runtimeExpressionProgramNodes contracts value viewAnyType
-    program = "typedProgram " ++ show rootSym ++ " [" ++ unwords (map parens nodes) ++ "]"
-
-checkedProgramAction :: String -> String -> String
-checkedProgramAction program okCase =
-  "matchResult " ++
-  "(diag env : pure (renderDiagnostic diag)) " ++
-  "(exec env : matchResult " ++
-    "(runtimeDiag runtimeEnv : pure (renderDiagnostic runtimeDiag)) " ++
-    okCase ++ " " ++
-    "(runChecked exec)) " ++
-  "(checkTypedProgramWith policyStrict " ++ parens program ++ ")"
-
-runtimeExpressionProgramNodes :: RuntimeContracts -> TricuAST -> ViewExpr -> (Integer, [String])
-runtimeExpressionProgramNodes contracts expr expected =
-  let (rootSym, nodes, _) = runRuntimeLower 0 Map.empty Map.empty Map.empty contracts (lowerRuntimeExprAgainst expr expected)
-  in (rootSym, nodes)
-
-runtimeBodyProgramNodes :: RuntimeContracts -> [DefArg] -> ViewExpr -> TricuAST -> [TricuAST] -> (Integer, [String])
-runtimeBodyProgramNodes contracts defArgs retView body callArgs =
-  let binders = [ (idx, name, maybe viewAnyType id mView, arg)
-                | (idx, (DefBinder name mView, arg)) <- zip [0 :: Integer ..] (zip defArgs callArgs)
-                ]
-      initialNext = fromIntegral (length binders)
-      initialKnown = Map.fromList [ (idx, view) | (idx, _, view, _) <- binders ]
-      subst = Map.fromList [ (name, arg) | (_, name, _, arg) <- binders ]
-      symbols = Map.fromList [ (name, idx) | (idx, name, _, _) <- binders ]
-      argNodes = concatMap argBoundaryNodes binders
-      (rootSym, bodyNodes, _) = runRuntimeLower initialNext initialKnown subst symbols contracts (lowerRuntimeExpr body)
-      resultRequire = "typedRequire " ++ show rootSym ++ " " ++ parens (unsafeLowerViewExpr retView) ++ " " ++ parens (astSource (substAst subst body))
-  in (rootSym, argNodes ++ bodyNodes ++ [resultRequire])
-  where
-    argBoundaryNodes (idx, _name, view, arg) =
-      [ "typedValue " ++ show idx ++ " " ++ parens (argRuntimeViewSource view) ++ " " ++ parens (astSource arg)
-      , "typedRequire " ++ show idx ++ " " ++ parens (unsafeLowerViewExpr view) ++ " " ++ parens (astSource arg)
-      ]
-
-data RuntimeLower = RuntimeLower
-  { runtimeNext :: Integer
-  , runtimeKnown :: Map.Map Integer ViewExpr
-  , runtimeSubst :: Map.Map String TricuAST
-  , runtimeSymbols :: Map.Map String Integer
-  , runtimeContracts :: RuntimeContracts
-  }
-
-type RuntimeM a = State RuntimeLower a
-
-runRuntimeLower :: Integer -> Map.Map Integer ViewExpr -> Map.Map String TricuAST -> Map.Map String Integer -> RuntimeContracts -> RuntimeM (Integer, [String], Maybe ViewExpr) -> (Integer, [String], Maybe ViewExpr)
-runRuntimeLower next known subst symbols contracts action = evalState action RuntimeLower
-  { runtimeNext = next
-  , runtimeKnown = known
-  , runtimeSubst = subst
-  , runtimeSymbols = symbols
-  , runtimeContracts = contracts
-  }
-
-freshRuntimeSym :: RuntimeM Integer
-freshRuntimeSym = do
-  st <- get
-  let sym = runtimeNext st
-  put st { runtimeNext = sym + 1 }
-  pure sym
-
-runtimeKnownFor :: Integer -> RuntimeM (Maybe ViewExpr)
-runtimeKnownFor sym = gets (Map.lookup sym . runtimeKnown)
-
-recordRuntimeKnown :: Integer -> ViewExpr -> RuntimeM ()
-recordRuntimeKnown sym view = modify $ \st -> st { runtimeKnown = Map.insert sym view (runtimeKnown st) }
-
-lowerRuntimeExpr :: TricuAST -> RuntimeM (Integer, [String], Maybe ViewExpr)
-lowerRuntimeExpr expr = case expr of
-  SVar name _ -> do
-    symbols <- gets runtimeSymbols
-    case Map.lookup name symbols of
-      Just sym -> do
-        known <- runtimeKnownFor sym
-        pure (sym, [], known)
-      Nothing -> do
-        contracts <- gets runtimeContracts
-        sym <- freshRuntimeSym
-        case Map.lookup name contracts of
-          Just (defArgs, ret, _) -> do
-            let view = declaredDefinitionView defArgs ret
-                viewSource = unsafeLowerViewExpr view
-            recordRuntimeKnown sym view
-            pure (sym, ["typedValue " ++ show sym ++ " " ++ parens viewSource ++ " " ++ parens (astSource expr)], Just view)
-          Nothing ->
-            pure (sym, ["typedValue " ++ show sym ++ " viewAny " ++ parens (astSource expr)], Just viewAnyType)
-  SStr s -> do
-    sym <- freshRuntimeSym
-    let view = VEName "String"
-    recordRuntimeKnown sym view
-    pure (sym, ["typedValue " ++ show sym ++ " viewString " ++ parens (astSource (SStr s))], Just view)
-  SInt n | n >= 0 && n <= 255 -> do
-    sym <- freshRuntimeSym
-    let view = VEName "Byte"
-    recordRuntimeKnown sym view
-    pure (sym, ["typedValue " ++ show sym ++ " viewByte " ++ show n], Just view)
-  TLeaf -> do
-    sym <- freshRuntimeSym
-    let view = VEName "Unit"
-    recordRuntimeKnown sym view
-    pure (sym, ["typedValue " ++ show sym ++ " viewUnit t"], Just view)
-  SList items -> do
-    lowered <- mapM lowerRuntimeExpr items
-    sym <- freshRuntimeSym
-    let view = viewExprList viewAnyType
-    recordRuntimeKnown sym view
-    subst <- gets runtimeSubst
-    let payload = astSource (substAst subst expr)
-    pure (sym, concat [ ns | (_, ns, _) <- lowered ] ++ ["typedValue " ++ show sym ++ " " ++ parens (unsafeLowerViewExpr view) ++ " " ++ parens payload], Just view)
-  SApp f a -> lowerRuntimeApplication f a expr
-  _ -> do
-    sym <- freshRuntimeSym
-    subst <- gets runtimeSubst
-    pure (sym, ["typedValue " ++ show sym ++ " viewAny " ++ parens (astSource (substAst subst expr))], Just viewAnyType)
-
-lowerRuntimeApplication :: TricuAST -> TricuAST -> TricuAST -> RuntimeM (Integer, [String], Maybe ViewExpr)
-lowerRuntimeApplication f a expr = do
-    (fSym, fNodes, fKnown) <- lowerRuntimeExpr f
-    let expectedArg = case fKnown >>= viewExprFnParts of
-          Just (argView : _, _) -> Just argView
-          _ -> Nothing
-    (aSym, aNodes, _) <- case expectedArg of
-      Just view -> lowerRuntimeExprAgainst a view
-      Nothing -> lowerRuntimeExpr a
-    outSym <- freshRuntimeSym
-    let outKnown = applicationResultView fKnown
-    mapM_ (recordRuntimeKnown outSym) outKnown
-    subst <- gets runtimeSubst
-    let payload = astSource (substAst subst expr)
-        applyNode = "typedApply " ++ show outSym ++ " " ++ show fSym ++ " " ++ show aSym ++ " " ++ parens payload
-    pure (outSym, fNodes ++ aNodes ++ [applyNode], outKnown)
-
-lowerRuntimeExprAgainst :: TricuAST -> ViewExpr -> RuntimeM (Integer, [String], Maybe ViewExpr)
-lowerRuntimeExprAgainst expr expected = do
-  mBoundary <- dynamicBoundaryValue expr expected
-  case mBoundary of
-    Just resultValue -> pure resultValue
-    Nothing -> do
-      (sym, nodes, known) <- lowerRuntimeExpr expr
-      subst <- gets runtimeSubst
-      let requireNode = "typedRequire " ++ show sym ++ " " ++ parens (unsafeLowerViewExpr expected) ++ " " ++ parens (astSource (substAst subst expr))
-      pure (sym, nodes ++ [requireNode], known)
-
--- IO continuations receive host-produced values whose structural View may not be
--- statically known to the source lowerer. At an explicit annotated boundary we
--- may introduce the requested base observation and let guarded Views perform the
--- runtime assertion. This keeps guard failures in checked-exec instead of
--- rejecting dynamic IO values as frontend-unknown Any.
-dynamicBoundaryValue :: TricuAST -> ViewExpr -> RuntimeM (Maybe (Integer, [String], Maybe ViewExpr))
-dynamicBoundaryValue expr expected = case expr of
-  SVar name _ -> do
-    symbols <- gets runtimeSymbols
-    contracts <- gets runtimeContracts
-    case (Map.lookup name symbols, Map.lookup name contracts) of
-      (Nothing, Nothing) -> do
-        subst <- gets runtimeSubst
-        sym <- freshRuntimeSym
-        let payload = astSource (substAst subst expr)
-            knownView = dynamicBoundaryKnownView expected
-            valueNode = "typedValue " ++ show sym ++ " " ++ parens (unsafeLowerViewExpr knownView) ++ " " ++ parens payload
-            requireNode = "typedRequire " ++ show sym ++ " " ++ parens (unsafeLowerViewExpr expected) ++ " " ++ parens payload
-        recordRuntimeKnown sym knownView
-        pure (Just (sym, [valueNode, requireNode], Just knownView))
-      _ -> pure Nothing
-  _ -> pure Nothing
-
-dynamicBoundaryKnownView :: ViewExpr -> ViewExpr
-dynamicBoundaryKnownView view = case viewExprAsType view of
-  Just (VTGuarded base _) -> viewTypeToExpr base
-  _ -> view
-
-substAst :: Map.Map String TricuAST -> TricuAST -> TricuAST
-substAst subst expr = case expr of
-  SVar name Nothing -> Map.findWithDefault expr name subst
-  SApp f a -> SApp (substAst subst f) (substAst subst a)
-  SLambda params body -> SLambda params (substAst (foldr Map.delete subst params) body)
-  SLet name val body -> SLet name (substAst subst val) (substAst (Map.delete name subst) body)
-  SList items -> SList (map (substAst subst) items)
-  TStem x -> TStem (substAst subst x)
-  TFork x y -> TFork (substAst subst x) (substAst subst y)
-  _ -> expr
-
-argRuntimeViewSource :: ViewExpr -> String
-argRuntimeViewSource view =
-  "lazyBool (_ : guardedViewBase " ++ v ++ ") (_ : " ++ v ++ ") (guardedView? " ++ v ++ ")"
-  where
-    v = parens (unsafeLowerViewExpr view)
-
-unsafeLowerViewExpr :: ViewExpr -> String
-unsafeLowerViewExpr view = case lowerViewExpr view of
-  Right source -> source
-  Left err -> errorWithoutStackTrace err
-
-astSource :: TricuAST -> String
-astSource expr = case expr of
-  SVar name Nothing -> name
-  SVar name (Just hash) -> name ++ "#" ++ hash
-  SInt n -> show n
-  SStr s -> show s
-  SList items -> "[" ++ unwords (map (parens . astSource) items) ++ "]"
-  SApp f a -> parens (astSource f) ++ " " ++ parens (astSource a)
-  SLambda params body -> parens (unwords params ++ " : " ++ astSource body)
-  SLet name val body -> parens ("let " ++ name ++ " = " ++ astSource val ++ " in " ++ astSource body)
-  TLeaf -> "t"
-  TStem x -> "(t " ++ astSource x ++ ")"
-  TFork x y -> "(t " ++ astSource x ++ " " ++ astSource y ++ ")"
-  SEmpty -> "[]"
-  SDef name params body -> name ++ " " ++ unwords params ++ " = " ++ astSource body
-  SDefAnn name args ret body -> name ++ " " ++ unwords (map defArgSource args) ++ maybe "" ((" =@" ++) . viewAnnSource) ret ++ " " ++ astSource body
-  SImport path ns -> "!import " ++ show path ++ " " ++ ns
-
-viewAnnSource :: ViewExpr -> String
-viewAnnSource = unsafeLowerViewExpr
-
-defArgSource :: DefArg -> String
-defArgSource (DefBinder name Nothing) = name
-defArgSource (DefBinder name (Just view)) = name ++ "@" ++ viewAnnSource view
-defArgSource (DefPhantom view) = "@" ++ viewAnnSource view
-
-parens :: String -> String
-parens s = "(" ++ s ++ ")"

src/ContentStore.hs

@@ -4,8 +4,6 @@ module ContentStore
   , module ContentStore.Arboricx
   , module ContentStore.Alias
   , module ContentStore.Resolver
-  , module ContentStore.ViewTree
-  , module ContentStore.ViewContract
   ) where
 
 import ContentStore.Arboricx
@@ -13,5 +11,3 @@ import ContentStore.Alias
 import ContentStore.Filesystem
 import ContentStore.Object
 import ContentStore.Resolver
-import ContentStore.ViewTree
-import ContentStore.ViewContract

src/ContentStore/ViewContract.hs

@@ -1,265 +0,0 @@
-{-# LANGUAGE PatternSynonyms #-}
-
-module ContentStore.ViewContract
-  ( viewContractTypeKind
-  , viewContractTypeDomain
-  , encodeViewType
-  , decodeViewType
-  , treeToViewType
-  , viewTypeToTree
-  , putViewType
-  , getViewType
-  ) where
-
-import ContentStore.Alias (ObjectRef(..))
-import ContentStore.Arboricx (decodeTreeTerm, encodeTreeTerm)
-import ContentStore.Filesystem (getObject, putObject)
-import ContentStore.Object (Domain(..), StorePath, ObjectHash)
-import Research (T(..), ViewRef(..), ViewType(..), pattern VTRef, pattern VTRefText, ofList, ofNumber, ofString, toList, toNumber, toString)
-
-import Data.Bits (shiftL, shiftR, (.&.))
-import Data.Text (Text)
-import Data.Text.Encoding (decodeUtf8', encodeUtf8)
-import Data.Word (Word8)
-import Text.Read (readMaybe)
-
-import qualified Data.ByteString as BS
-import qualified Data.Text as T
-
-viewContractTypeKind :: Text
-viewContractTypeKind = "arboricx.view-contract.type.v1"
-
-viewContractTypeDomain :: Domain
-viewContractTypeDomain = Domain viewContractTypeKind
-
-encodeViewType :: ViewType -> BS.ByteString
-encodeViewType = go
-  where
-    go (VTName name) = BS.cons 0x00 (putBytes (encodeUtf8 (T.pack name)))
-    go (VTVar varId) = BS.cons 0x08 (putU32 (fromIntegral varId))
-    go (VTRefRaw (ViewRefInt n)) = BS.cons 0x01 (putBytes (encodeUtf8 (T.pack ("i:" ++ show n))))
-    go (VTRefRaw (ViewRefText s)) = BS.cons 0x01 (putBytes (encodeUtf8 (T.pack ("s:" ++ s))))
-    go (VTList item) = BS.cons 0x02 (go item)
-    go (VTMaybe item) = BS.cons 0x03 (go item)
-    go (VTPair left right) = BS.cons 0x04 (go left <> go right)
-    go (VTResult err ok) = BS.cons 0x05 (go err <> go ok)
-    go (VTGuarded base guard) = BS.cons 0x07 (go base <> putBytes (encodeTreeTerm guard))
-    go (VTForall binders body) = BS.cons 0x09 (putIntegerList binders <> go body)
-    go (VTExists binders body) = BS.cons 0x0a (putIntegerList binders <> go body)
-    go (VTFn args result) =
-      BS.cons 0x06 (putU32 (length args) <> mconcat (map go args) <> go result)
-
-putViewType :: StorePath -> ViewType -> IO ObjectRef
-putViewType store view = do
-  h <- putObject store viewContractTypeDomain (encodeViewType view)
-  pure ObjectRef { objectRefKind = viewContractTypeKind, objectRefHash = h }
-
-getViewType :: StorePath -> ObjectRef -> IO (Either String ViewType)
-getViewType store ref
-  | objectRefKind ref /= viewContractTypeKind =
-      pure $ Left $ "unsupported View Contract type object kind: " ++ T.unpack (objectRefKind ref)
-  | otherwise = do
-      mPayload <- getObject store (objectRefHash ref)
-      pure $ case mPayload of
-        Nothing -> Left $ "missing View Contract type object: " ++ T.unpack (objectRefHash ref)
-        Just payload -> decodeViewType payload
-
-decodeViewType :: BS.ByteString -> Either String ViewType
-decodeViewType payload = do
-  (view, rest) <- getViewTypeBytes payload
-  if BS.null rest
-    then Right view
-    else Left "trailing bytes after View Contract type"
-
-viewTypeToTree :: ViewType -> T
-viewTypeToTree view = case view of
-  VTName "Any" -> record 0 []
-  VTName "Bool" -> viewTypeToTree (VTRef 0)
-  VTName "String" -> viewTypeToTree (VTRef 1)
-  VTName "Byte" -> viewTypeToTree (VTRef 2)
-  VTName "Unit" -> viewTypeToTree (VTRef 3)
-  VTName name -> viewTypeToTree (VTRefText name)
-  VTVar varId -> record 8 [field 10 (ofNumber varId)]
-  VTRefRaw ref -> record 2 [field 2 (viewRefToTree ref)]
-  VTList item -> record 3 [field 3 (viewTypeToTree item)]
-  VTMaybe item -> record 4 [field 3 (viewTypeToTree item)]
-  VTPair left right -> record 5 [field 4 (viewTypeToTree left), field 5 (viewTypeToTree right)]
-  VTResult err ok -> record 6 [field 6 (viewTypeToTree err), field 7 (viewTypeToTree ok)]
-  VTGuarded base guard -> record 7 [field 8 (viewTypeToTree base), field 9 guard]
-  VTForall binders body -> record 9 [field 11 (ofList (map ofNumber binders)), field 12 (viewTypeToTree body)]
-  VTExists binders body -> record 10 [field 11 (ofList (map ofNumber binders)), field 12 (viewTypeToTree body)]
-  VTFn args result -> record 1 [field 0 (ofList (map viewTypeToTree args)), field 1 (viewTypeToTree result)]
-  where
-    record tag fields = Fork (ofNumber tag) (ofList fields)
-    field tag value = Fork (ofNumber tag) value
-    viewRefToTree (ViewRefInt n) = ofNumber n
-    viewRefToTree (ViewRefText s) = ofString s
-
-treeToViewType :: T -> Either String ViewType
-treeToViewType viewTree = do
-  (tag, fields) <- recordParts viewTree
-  case tag of
-    0 -> do
-      expectNoFields fields "Any"
-      Right (VTName "Any")
-    1 -> do
-      argsTree <- fieldValueAt 0 fields
-      resultTree <- fieldValueAt 1 fields
-      args <- toList argsTree
-      VTFn <$> mapM treeToViewType args <*> treeToViewType resultTree
-    2 -> VTRefRaw <$> (fieldValueAt 2 fields >>= viewRefFromTree)
-    3 -> VTList <$> (fieldValueAt 3 fields >>= treeToViewType)
-    4 -> VTMaybe <$> (fieldValueAt 3 fields >>= treeToViewType)
-    5 -> VTPair <$> (fieldValueAt 4 fields >>= treeToViewType) <*> (fieldValueAt 5 fields >>= treeToViewType)
-    6 -> VTResult <$> (fieldValueAt 6 fields >>= treeToViewType) <*> (fieldValueAt 7 fields >>= treeToViewType)
-    7 -> VTGuarded <$> (fieldValueAt 8 fields >>= treeToViewType) <*> fieldValueAt 9 fields
-    8 -> VTVar <$> (fieldValueAt 10 fields >>= toNumber)
-    9 -> VTForall <$> (fieldValueAt 11 fields >>= integerListFromTree) <*> (fieldValueAt 12 fields >>= treeToViewType)
-    10 -> VTExists <$> (fieldValueAt 11 fields >>= integerListFromTree) <*> (fieldValueAt 12 fields >>= treeToViewType)
-    _ -> Left $ "unknown View Contract view tag in tree: " ++ show tag
-  where
-    recordParts (Fork tagTree fieldsTree) = do
-      tag <- toNumber tagTree
-      fields <- toList fieldsTree
-      pure (tag, fields)
-    recordParts _ = Left "View Contract view tree is not a record"
-
-    expectNoFields fields label =
-      if null fields
-        then Right ()
-        else Left $ "View Contract " ++ label ++ " view has unexpected fields"
-
-    fieldValueAt expectedTag fields = do
-      values <- mapM fieldParts fields
-      case values of
-        [(actualTag, value)] | actualTag == expectedTag -> Right value
-        _ -> case lookup expectedTag values of
-          Just value -> Right value
-          Nothing -> Left $ "View Contract view tree missing field tag: " ++ show expectedTag
-
-    fieldParts (Fork tagTree value) = do
-      tag <- toNumber tagTree
-      pure (tag, value)
-    fieldParts _ = Left "View Contract view field is not a pair"
-
-    integerListFromTree tree = toList tree >>= mapM toNumber
-
-    viewRefFromTree tree =
-      case toNumber tree of
-        Right n -> Right (ViewRefInt n)
-        Left _ -> ViewRefText <$> toString tree
-
-getViewTypeBytes :: BS.ByteString -> Either String (ViewType, BS.ByteString)
-getViewTypeBytes bs = case BS.uncons bs of
-  Nothing -> Left "unexpected end of View Contract type"
-  Just (tag, rest) -> case tag of
-    0x00 -> do
-      (rawName, afterName) <- getBytes rest
-      name <- either (const (Left "View Contract type name is not valid UTF-8")) Right (decodeUtf8' rawName)
-      pure (VTName (T.unpack name), afterName)
-    0x01 -> do
-      (rawRef, afterRef) <- getBytes rest
-      refText <- either (const (Left "View Contract ref is not valid UTF-8")) Right (decodeUtf8' rawRef)
-      ref <- parseViewRef (T.unpack refText)
-      pure (VTRefRaw ref, afterRef)
-    0x02 -> do
-      (item, afterItem) <- getViewTypeBytes rest
-      pure (VTList item, afterItem)
-    0x03 -> do
-      (item, afterItem) <- getViewTypeBytes rest
-      pure (VTMaybe item, afterItem)
-    0x04 -> do
-      (left, afterLeft) <- getViewTypeBytes rest
-      (right, afterRight) <- getViewTypeBytes afterLeft
-      pure (VTPair left right, afterRight)
-    0x05 -> do
-      (err, afterErr) <- getViewTypeBytes rest
-      (ok, afterOk) <- getViewTypeBytes afterErr
-      pure (VTResult err ok, afterOk)
-    0x06 -> do
-      (argc, afterArgc) <- getU32 rest
-      (args, afterArgs) <- getMany argc afterArgc
-      (result, afterResult) <- getViewTypeBytes afterArgs
-      pure (VTFn args result, afterResult)
-    0x07 -> do
-      (base, afterBase) <- getViewTypeBytes rest
-      (rawGuard, afterGuard) <- getBytes afterBase
-      guard <- decodeTreeTerm rawGuard
-      pure (VTGuarded base guard, afterGuard)
-    0x08 -> do
-      (varId, afterVarId) <- getU32 rest
-      pure (VTVar (fromIntegral varId), afterVarId)
-    0x09 -> do
-      (binders, afterBinders) <- getIntegerList rest
-      (body, afterBody) <- getViewTypeBytes afterBinders
-      pure (VTForall binders body, afterBody)
-    0x0a -> do
-      (binders, afterBinders) <- getIntegerList rest
-      (body, afterBody) <- getViewTypeBytes afterBinders
-      pure (VTExists binders body, afterBody)
-    _ -> Left $ "unknown View Contract type tag: " ++ show tag
-
-parseViewRef :: String -> Either String ViewRef
-parseViewRef raw = case raw of
-  'i' : ':' : rest -> ViewRefInt <$> maybe (Left "View Contract integer ref is not an integer") Right (readMaybe rest)
-  's' : ':' : rest -> Right (ViewRefText rest)
-  legacy -> ViewRefInt <$> maybe (Left "View Contract ref is neither tagged nor a legacy integer") Right (readMaybe legacy)
-
-getMany :: Int -> BS.ByteString -> Either String ([ViewType], BS.ByteString)
-getMany n bs
-  | n < 0 = Left "negative View Contract argument count"
-  | otherwise = go n bs []
-  where
-    go 0 rest acc = Right (reverse acc, rest)
-    go k rest acc = do
-      (item, afterItem) <- getViewTypeBytes rest
-      go (k - 1) afterItem (item : acc)
-
-putIntegerList :: [Integer] -> BS.ByteString
-putIntegerList items = putU32 (length items) <> mconcat (map (putU32 . fromIntegral) items)
-
-getIntegerList :: BS.ByteString -> Either String ([Integer], BS.ByteString)
-getIntegerList bs = do
-  (count, afterCount) <- getU32 bs
-  go count afterCount []
-  where
-    go 0 rest acc = Right (reverse acc, rest)
-    go n rest acc = do
-      (varId, afterVarId) <- getU32 rest
-      go (n - 1) afterVarId (fromIntegral varId : acc)
-
-putBytes :: BS.ByteString -> BS.ByteString
-putBytes bytes = putU32 (BS.length bytes) <> bytes
-
-getBytes :: BS.ByteString -> Either String (BS.ByteString, BS.ByteString)
-getBytes bs = do
-  (len, afterLen) <- getU32 bs
-  let (payload, rest) = BS.splitAt len afterLen
-  if BS.length payload == len
-    then Right (payload, rest)
-    else Left "truncated length-prefixed View Contract field"
-
-putU32 :: Int -> BS.ByteString
-putU32 n
-  | n < 0 = error "putU32: negative length"
-  | n > 0xffffffff = error "putU32: length too large"
-  | otherwise = BS.pack
-      [ fromIntegral ((n `shiftR` 24) .&. 0xff)
-      , fromIntegral ((n `shiftR` 16) .&. 0xff)
-      , fromIntegral ((n `shiftR` 8) .&. 0xff)
-      , fromIntegral (n .&. 0xff)
-      ]
-
-getU32 :: BS.ByteString -> Either String (Int, BS.ByteString)
-getU32 bs
-  | BS.length bs < 4 = Left "truncated View Contract u32"
-  | otherwise =
-      let [b0, b1, b2, b3] = BS.unpack (BS.take 4 bs)
-          n = word8ToInt b0 `shiftL` 24
-            + word8ToInt b1 `shiftL` 16
-            + word8ToInt b2 `shiftL` 8
-            + word8ToInt b3
-      in Right (n, BS.drop 4 bs)
-
-word8ToInt :: Word8 -> Int
-word8ToInt = fromIntegral

src/ContentStore/ViewTree.hs

@@ -1,192 +0,0 @@
-module ContentStore.ViewTree
-  ( viewTreeKind
-  , viewTreeDomain
-  , encodeViewTree
-  , decodeViewTree
-  , singletonViewTree
-  , singletonViewTreeWithProvenance
-  , viewTreeRootTerm
-  , viewTreeRootViewFact
-  , putViewTree
-  , getViewTree
-  ) where
-
-import ContentStore.Arboricx (decodeTreeTerm, encodeTreeTerm)
-import ContentStore.Alias (ObjectRef(..))
-import ContentStore.Filesystem (getObject, putObject)
-import ContentStore.Object (Domain(..), StorePath)
-import ContentStore.ViewContract (treeToViewType, viewTypeToTree)
-import Research (T(..), ViewProvenance(..), ViewType(..), ofList, ofNumber, toList, toNumber)
-
-import qualified Data.ByteString as BS
-import qualified Data.Text as T
-
-viewTreeKind :: T.Text
-viewTreeKind = "arboricx.view-tree.v1"
-
-viewTreeDomain :: Domain
-viewTreeDomain = Domain viewTreeKind
-
--- View-tree artifacts are ordinary tree data. Their node envelope semantics
--- live in lib/view.tri; this module only provides CAS persistence for the
--- portable tree payload.
-encodeViewTree :: T -> BS.ByteString
-encodeViewTree = encodeTreeTerm
-
-decodeViewTree :: BS.ByteString -> Either String T
-decodeViewTree = decodeTreeTerm
-
-singletonViewTree :: Maybe ViewType -> T -> T
-singletonViewTree mView term = singletonViewTreeWithProvenance (fmap (\view -> (view, ViewUnchecked)) mView) term
-
-singletonViewTreeWithProvenance :: Maybe (ViewType, ViewProvenance) -> T -> T
-singletonViewTreeWithProvenance mViewFact term =
-  record typedProgramTag
-    [ field typedProgramFieldRoot (ofNumber 0)
-    , field typedProgramFieldNodes (ofList [typedValueNode 0 (maybe viewAnyTree (viewTypeToTree . fst) mViewFact) term (fmap snd mViewFact)])
-    ]
-
--- | Extract the executable root payload from a view-tree artifact without
--- judging view validity. Checker semantics remain in lib/view.tri; this is only
--- the module loader's payload projection for imports.
-viewTreeRootTerm :: T -> Either String T
-viewTreeRootTerm tree = do
-  tag <- recordTag tree
-  if tag /= typedProgramTag
-    then Left $ "view-tree root has unexpected tag: " ++ show tag
-    else do
-      root <- fieldValue typedProgramFieldRoot tree >>= toNumber
-      nodes <- fieldValue typedProgramFieldNodes tree >>= toList
-      lookupRoot root nodes
-  where
-    lookupRoot _ [] = Left "view-tree root symbol not found"
-    lookupRoot root (node : rest) = do
-      sym <- fieldValue typedNodeFieldSymbol node >>= toNumber
-      if sym == root
-        then nodeTerm node
-        else lookupRoot root rest
-
-    nodeTerm node = do
-      tag <- recordTag node
-      case tag of
-        21 -> fieldValue typedNodeFieldTerm node
-        22 -> fieldValue typedNodeFieldTerm node
-        23 -> fieldValue typedNodeFieldTerm node
-        _  -> Left $ "view-tree node has unexpected tag: " ++ show tag
-
-viewTreeRootViewFact :: T -> Either String (Maybe (ViewType, ViewProvenance))
-viewTreeRootViewFact tree = do
-  tag <- recordTag tree
-  if tag /= typedProgramTag
-    then Left $ "view-tree root has unexpected tag: " ++ show tag
-    else do
-      root <- fieldValue typedProgramFieldRoot tree >>= toNumber
-      nodes <- fieldValue typedProgramFieldNodes tree >>= toList
-      lookupRoot root nodes
-  where
-    lookupRoot _ [] = Left "view-tree root symbol not found"
-    lookupRoot root (node : rest) = do
-      sym <- fieldValue typedNodeFieldSymbol node >>= toNumber
-      if sym == root
-        then nodeViewFact node
-        else lookupRoot root rest
-
-    nodeViewFact node = do
-      tag <- recordTag node
-      case tag of
-        21 -> do
-          view <- fieldValue typedNodeFieldView node >>= treeToViewType
-          provenance <- maybe (Right ViewUnchecked) treeToViewProvenance (fieldValueMaybe typedNodeFieldProvenance node)
-          Right (Just (view, provenance))
-        23 -> do
-          view <- fieldValue typedNodeFieldView node >>= treeToViewType
-          provenance <- maybe (Right ViewUnchecked) treeToViewProvenance (fieldValueMaybe typedNodeFieldProvenance node)
-          Right (Just (view, provenance))
-        22 -> Right Nothing
-        _  -> Left $ "view-tree node has unexpected tag: " ++ show tag
-
-record :: Integer -> [T] -> T
-record tag fields = Fork (ofNumber tag) (ofList fields)
-
-field :: Integer -> T -> T
-field tag value = Fork (ofNumber tag) value
-
-typedValueNode :: Integer -> T -> T -> Maybe ViewProvenance -> T
-typedValueNode sym view term mProvenance =
-  record typedNodeTagValue $
-    [ field typedNodeFieldSymbol (ofNumber sym)
-    , field typedNodeFieldView view
-    , field typedNodeFieldTerm term
-    ] ++ maybe [] (\provenance -> [field typedNodeFieldProvenance (viewProvenanceToTree provenance)]) mProvenance
-
-viewProvenanceToTree :: ViewProvenance -> T
-viewProvenanceToTree ViewChecked = ofNumber 0
-viewProvenanceToTree ViewTrusted = ofNumber 1
-viewProvenanceToTree ViewUnchecked = ofNumber 2
-
-viewAnyTree :: T
-viewAnyTree = record 0 []
-
-recordTag :: T -> Either String Integer
-recordTag (Fork tagTree _) = toNumber tagTree
-recordTag _ = Left "view-tree value is not a record"
-
-recordFields :: T -> Either String [T]
-recordFields (Fork _ fieldsTree) = toList fieldsTree
-recordFields _ = Left "view-tree value is not a record"
-
-fieldValue :: Integer -> T -> Either String T
-fieldValue expected recordTree = do
-  fields <- recordFields recordTree
-  values <- mapM fieldParts fields
-  case lookup expected values of
-    Just value -> Right value
-    Nothing -> Left $ "view-tree missing field tag: " ++ show expected
-
-fieldValueMaybe :: Integer -> T -> Maybe T
-fieldValueMaybe expected recordTree = do
-  fields <- either (const Nothing) Just (recordFields recordTree)
-  values <- either (const Nothing) Just (mapM fieldParts fields)
-  lookup expected values
-
-fieldParts :: T -> Either String (Integer, T)
-fieldParts (Fork tagTree value) = do
-  tag <- toNumber tagTree
-  Right (tag, value)
-fieldParts _ = Left "view-tree field is not a pair"
-
-typedProgramTag, typedProgramFieldRoot, typedProgramFieldNodes :: Integer
-typedProgramTag = 20
-typedProgramFieldRoot = 0
-typedProgramFieldNodes = 1
-
-typedNodeTagValue, typedNodeFieldSymbol, typedNodeFieldView, typedNodeFieldTerm, typedNodeFieldProvenance :: Integer
-typedNodeTagValue = 21
-typedNodeFieldSymbol = 0
-typedNodeFieldView = 1
-typedNodeFieldTerm = 2
-typedNodeFieldProvenance = 5
-
-treeToViewProvenance :: T -> Either String ViewProvenance
-treeToViewProvenance tree = do
-  tag <- toNumber tree
-  case tag of
-    0 -> Right ViewChecked
-    1 -> Right ViewTrusted
-    2 -> Right ViewUnchecked
-    _ -> Left $ "unknown view-tree View Contract provenance tag: " ++ show tag
-
-putViewTree :: StorePath -> T -> IO ObjectRef
-putViewTree store viewTree = do
-  h <- putObject store viewTreeDomain (encodeViewTree viewTree)
-  pure ObjectRef { objectRefKind = viewTreeKind, objectRefHash = h }
-
-getViewTree :: StorePath -> ObjectRef -> IO (Either String T)
-getViewTree store ref
-  | objectRefKind ref /= viewTreeKind =
-      pure $ Left $ "unsupported view-tree object kind: " ++ T.unpack (objectRefKind ref)
-  | otherwise = do
-      mPayload <- getObject store (objectRefHash ref)
-      pure $ case mPayload of
-        Nothing -> Left $ "missing view-tree object: " ++ T.unpack (objectRefHash ref)
-        Just payload -> decodeViewTree payload

src/Eval.hs

@@ -1,5 +1,6 @@
 module Eval where
 
+import Frontend.ContractDesugar
 import Parser
 import Research
 
@@ -63,7 +64,7 @@ evalSingle env term
     in Map.insert "!result" res env
 
 evalTricu :: Env -> [TricuAST] -> Env
-evalTricu env x = go env (reorderDefs env (map recoverParams x))
+evalTricu env x = go env (reorderDefs env (map recoverParams (desugarContracts x)))
   where
     go env' []     = env'
     go env' [def]    =
@@ -72,6 +73,19 @@ evalTricu env x = go env (reorderDefs env (map recoverParams x))
     go env' (def:xs) =
       evalTricu (evalSingle env' def) xs
 
+-- | Ensure the contract kernel is bound. If the environment already defines
+-- 'kernel', leave it alone. Otherwise, bind 'kernel' to 'defaultKernel' if
+-- that is available. This lets the default kernel live in a .tri file while
+-- still providing a fallback for code that imports the base library.
+injectKernel :: Env -> Env
+injectKernel env =
+  case Map.lookup "kernel" env of
+    Just _  -> env
+    Nothing ->
+      case Map.lookup "defaultKernel" env of
+        Just k  -> Map.insert "kernel" k env
+        Nothing -> env
+
 evalASTSync :: Env -> TricuAST -> T
 evalASTSync env term = case term of
   SLambda _ _ -> evalASTSync env (elimLambda term)
@@ -195,12 +209,35 @@ freeVars (SLambda vs body) = Set.difference (freeVars body) (Set.fromList vs)
 freeVars (SLet name val body) =
   Set.union (freeVars val) (Set.delete name (freeVars body))
 freeVars (SDef _ params body) = Set.difference (freeVars body) (Set.fromList params)
-freeVars (SDefAnn _ args _ body) = Set.difference (freeVars body) (Set.fromList (annotatedBinders args))
+freeVars (SDefAnn _ args ret body) =
+  Set.difference
+    (Set.unions
+      [ freeVars body
+      , freeVarsDefArgs args
+      , maybe Set.empty freeVarsViewExpr ret
+      , Set.singleton "withContract"
+      ])
+    (Set.fromList (annotatedBinders args))
 freeVars (TStem t) = freeVars t
 freeVars (TFork t u) = Set.union (freeVars t) (freeVars u)
 freeVars (SList xs) = foldMap freeVars xs
 freeVars _ = Set.empty
 
+freeVarsViewExpr :: ViewExpr -> Set String
+freeVarsViewExpr (VEName s) = Set.singleton s
+freeVarsViewExpr (VEVar s) = Set.singleton s
+freeVarsViewExpr (VEApp f a) = Set.union (freeVarsViewExpr f) (freeVarsViewExpr a)
+freeVarsViewExpr (VEList es) = Set.unions (map freeVarsViewExpr es)
+freeVarsViewExpr (VEForall _ e) = freeVarsViewExpr e
+freeVarsViewExpr (VEExists _ e) = freeVarsViewExpr e
+freeVarsViewExpr _ = Set.empty
+
+freeVarsDefArgs :: [DefArg] -> Set String
+freeVarsDefArgs = Set.unions . map go
+  where
+    go (DefBinder _ mAnn) = maybe Set.empty freeVarsViewExpr mAnn
+    go (DefPhantom ann) = freeVarsViewExpr ann
+
 reorderDefs :: Env -> [TricuAST] -> [TricuAST]
 reorderDefs env defs
   | not (null missingDeps) =

src/FileEval.hs

@@ -1,6 +1,5 @@
 module FileEval
-  ( ContractMode(..)
+  ( LoadedSource(..)
-  , LoadedSource(..)
   , preprocessFile
   , preprocessFileWithStore
   , preprocessFileWithResolver
@@ -8,23 +7,17 @@ module FileEval
   , evaluateFileWithStore
   , evaluateFileWithContext
   , evaluateFileWithContextWithStore
-  , evaluateFileWithContextWithStoreAndMode
   , evaluateFileResult
   , compileFile
   , compileFileWithStore
   , loadFileWithStore
-  , loadFileWithStoreMode
+  , loadFileWithResolver
   , defaultStorePath
   ) where
 
-import Check.Core
-  ( ImportedView(..)
-  , checkProgramWithEnvAndImportedViews
-  , importedViewsFromResolvedModulesEither
-  , lowerViewExpr
-  )
 import ContentStore
-import Eval (evalASTSync, evalTricu, freeVars, result)
+import Eval (evalTricu, freeVars, result, injectKernel)
+import Frontend.ContractDesugar (desugarContracts)
 import Lexer
 import Module.Manifest
 import Module.Resolver
@@ -52,11 +45,6 @@ extractMain env =
     Just evalResult -> Right evalResult
     Nothing -> Left "No `main` function detected"
 
-data ContractMode
-  = EnforceContracts
-  | IgnoreContracts
-  deriving (Eq, Show)
-
 data LoadedSource = LoadedSource
   { loadedImports :: Env
   , loadedAst     :: [TricuAST]
@@ -67,7 +55,6 @@ data LoadContext = LoadContext
   { loadResolver  :: ObjectResolver
   , loadStore     :: Maybe StorePath
   , loadWorkspace :: Workspace
-  , loadContracts :: ContractMode
   }
 
 processImports :: [TricuAST] -> ([TricuAST], [(String, String)])
@@ -94,21 +81,17 @@ evaluateFile = evaluateFileWithStore Nothing
 evaluateFileWithStore :: Maybe StorePath -> FilePath -> IO Env
 evaluateFileWithStore mStore filePath = do
   loaded <- maybe loadFile loadFileWithStore mStore filePath
-  pure $ evalTricu (loadedImports loaded) (loadedAst loaded)
+  pure $ evalTricu (injectKernel (loadedImports loaded)) (loadedAst loaded)
 
 evaluateFileWithContext :: Env -> FilePath -> IO Env
 evaluateFileWithContext = evaluateFileWithContextWithStore Nothing
 
 evaluateFileWithContextWithStore :: Maybe StorePath -> Env -> FilePath -> IO Env
-evaluateFileWithContextWithStore mStore =
+evaluateFileWithContextWithStore mStore env filePath = do
-  evaluateFileWithContextWithStoreAndMode EnforceContracts mStore
-
-evaluateFileWithContextWithStoreAndMode :: ContractMode -> Maybe StorePath -> Env -> FilePath -> IO Env
-evaluateFileWithContextWithStoreAndMode mode mStore env filePath = do
   loaded <- case mStore of
-    Nothing    -> loadFileMode mode filePath
+    Nothing    -> loadFile filePath
-    Just store -> loadFileWithStoreMode mode store filePath
+    Just store -> loadFileWithStore store filePath
-  pure $ evalTricu (Map.union (loadedImports loaded) env) (loadedAst loaded)
+  pure $ evalTricu (injectKernel (Map.union (loadedImports loaded) env)) (loadedAst loaded)
 
 preprocessFile :: FilePath -> IO [TricuAST]
 preprocessFile p = loadedAst <$> loadFile p
@@ -120,26 +103,20 @@ preprocessFileWithResolver :: ObjectResolver -> FilePath -> IO [TricuAST]
 preprocessFileWithResolver resolver p = loadedAst <$> loadFileWithResolver resolver p
 
 loadFile :: FilePath -> IO LoadedSource
-loadFile = loadFileMode EnforceContracts
+loadFile p = do
-
-loadFileMode :: ContractMode -> FilePath -> IO LoadedSource
-loadFileMode mode p = do
   store <- defaultStorePath
-  loadFileWithStoreMode mode store p
+  loadFileWithStore store p
 
 loadFileWithStore :: StorePath -> FilePath -> IO LoadedSource
-loadFileWithStore = loadFileWithStoreMode EnforceContracts
+loadFileWithStore store p = do
-
-loadFileWithStoreMode :: ContractMode -> StorePath -> FilePath -> IO LoadedSource
-loadFileWithStoreMode mode store p = do
   workspace <- findWorkspaceFor p
   resolver <- cachedFilesystemResolver store
-  let ctx = LoadContext resolver (Just store) workspace mode
+  let ctx = LoadContext resolver (Just store) workspace
   loadFile' ctx p
 
 loadFileWithResolver :: ObjectResolver -> FilePath -> IO LoadedSource
 loadFileWithResolver resolver p = do
-  let ctx = LoadContext resolver Nothing emptyWorkspace EnforceContracts
+  let ctx = LoadContext resolver Nothing emptyWorkspace
   loadFile' ctx p
 
 loadFile' :: LoadContext -> FilePath -> IO LoadedSource
@@ -150,15 +127,16 @@ loadFile' ctx currentPath = do
     Left err -> errorWithoutStackTrace (handleParseError tokens err)
     Right ast ->
       let (nonImports, importTargets) = processImports ast
+          desugaredNonImports = desugarContracts nonImports
       in do
-        let reexportOnlyModule = null (topLevelDefinitions nonImports) && not (null importTargets)
+        let reexportOnlyModule = null desugaredNonImports && not (null importTargets)
         resolvedModules <- mapM (\(target, name) -> do
             ensureWorkspaceModule ctx target
-            resolveModuleImportSelecting (loadResolver ctx) (selectedExportsForImport reexportOnlyModule target name nonImports) target name) importTargets
+            resolveModuleImportSelecting (loadResolver ctx) (selectedExportsForImport reexportOnlyModule target name desugaredNonImports) target name) importTargets
         let moduleEnv = resolvedModulesEnv resolvedModules
         pure LoadedSource
           { loadedImports = moduleEnv
-          , loadedAst = nonImports
+          , loadedAst = desugaredNonImports
           , loadedModules = resolvedModules
           }
 
@@ -181,66 +159,26 @@ buildWorkspaceModule :: LoadContext -> StorePath -> String -> FilePath -> IO ()
 buildWorkspaceModule ctx store moduleName sourcePath = do
   loaded <- loadFile' ctx sourcePath
   let asts = loadedAst loaded
-  case loadContracts ctx of
+      env = evalTricu (loadedImports loaded) asts
-    EnforceContracts -> enforceWorkspaceModuleContracts store moduleName (loadedImports loaded) (loadedModules loaded) asts
-    IgnoreContracts  -> pure ()
-  let env = evalTricu (loadedImports loaded) asts
       localNames = topLevelDefinitions asts
-      localViewExprs = topLevelDefinitionViews asts
-      localViews = case loadContracts ctx of
-        EnforceContracts
-          | Map.null localViewExprs -> pure (Right Map.empty)
-          | otherwise -> do
-              viewEnv <- evaluateFileWithContextWithStoreAndMode IgnoreContracts (Just store) Map.empty "./lib/view.tri"
-              let checkerEnv = evalTricu (Map.union viewEnv (loadedImports loaded)) asts
-              pure (resolveDefinitionViews checkerEnv localViewExprs)
-        IgnoreContracts -> pure (Right Map.empty)
       names = if null localNames
                 then filter (/= "!result") (Map.keys env)
                 else localNames
-  localViewsResult <- localViews
+  exports <- mapM (buildExport env) names
-  resolvedLocalViews <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid exported View Contract annotation: ") ++)) pure localViewsResult
-  importedViews <- importedViewsFromResolvedModulesEither (getViewType store) (loadedModules loaded)
-  let localViewFacts = Map.map (\view -> (view, ViewChecked)) resolvedLocalViews
-      importedViewFacts = Map.fromList [(importedViewName iv, (importedViewType iv, importedViewProvenance iv)) | iv <- importedViews]
-      exportViewFacts = Map.union localViewFacts importedViewFacts
-  exports <- mapM (buildExport env exportViewFacts) names
   manifestHash <- putManifest store (ModuleManifest [] exports)
   writeAlias store ModuleAlias (T.pack moduleName) (ObjectRef (unDomain manifestDomain) manifestHash)
   where
-    buildExport env viewFacts name = case Map.lookup name env of
+    buildExport env name = case Map.lookup name env of
-      Nothing -> errorWithoutStackTrace $ "Workspace module export not found after evaluation: " ++ name
+      Nothing -> errorWithoutStackTrace $
+        "Workspace module export not found after evaluation: " ++ name
       Just term -> do
-        let exportFact = Map.lookup name viewFacts
+        rootRef <- putTreeTerm store term
-            exportView = fmap fst exportFact
-            exportProvenance = fmap snd exportFact
-        rootRef <- putViewTree store (singletonViewTreeWithProvenance exportFact term)
-        viewRef <- mapM (putViewType store) exportView
         return ModuleExport
           { moduleExportName = T.pack name
-          , moduleExportObject = rootRef
+          , moduleExportObject = ObjectRef (unDomain treeTermDomain) rootRef
-          , moduleExportAbi = "arboricx.abi.view-tree.v1"
+          , moduleExportAbi = "arboricx.abi.tree.v1"
-          , moduleExportView = viewRef
-          , moduleExportViewProvenance = exportProvenance
           }
 
-enforceWorkspaceModuleContracts :: StorePath -> String -> Env -> [ResolvedModule] -> [TricuAST] -> IO ()
-enforceWorkspaceModuleContracts store moduleName importEnv modules asts
-  | not (any isAnnotatedDefinition asts) = pure ()
-  | otherwise = do
-      viewEnv <- evaluateFileWithContextWithStoreAndMode IgnoreContracts (Just store) Map.empty "./lib/view.tri"
-      let checkerEnv = evalTricu (Map.union viewEnv importEnv) asts
-      imports <- importedViewsFromResolvedModulesEither (getViewType store) modules
-      resultText <- checkProgramWithEnvAndImportedViews checkerEnv imports asts
-      case resultText of
-        "ok" -> pure ()
-        diagnostic -> errorWithoutStackTrace $
-          "Workspace module " ++ show moduleName ++ " failed View Contract check: " ++ diagnostic
-
-isAnnotatedDefinition :: TricuAST -> Bool
-isAnnotatedDefinition SDefAnn {} = True
-isAnnotatedDefinition _ = False
-
 topLevelDefinitions :: [TricuAST] -> [String]
 topLevelDefinitions = mapMaybe go
   where
@@ -248,43 +186,6 @@ topLevelDefinitions = mapMaybe go
     go (SDefAnn name _ _ _) = Just name
     go _ = Nothing
 
-topLevelDefinitionViews :: [TricuAST] -> Map.Map String ViewExpr
-topLevelDefinitionViews asts = Map.fromList (mapMaybe go asts)
-  where
-    go (SDefAnn name args resultView _) = Just (name, definitionView args resultView)
-    go _ = Nothing
-
-resolveDefinitionViews :: Env -> Map.Map String ViewExpr -> Either String (Map.Map String ViewType)
-resolveDefinitionViews env = mapM (resolveViewExpression env)
-
-resolveViewExpression :: Env -> ViewExpr -> Either String ViewType
-resolveViewExpression checkerEnv view = do
-  expr <- lowerViewExpr view
-  let term = evalASTSync checkerEnv (head (parseTricu expr))
-      probeEnv = Map.insert "__candidateView" term checkerEnv
-      probe = evalTricu probeEnv (parseTricu "viewContractProbe (wellFormedView? __candidateView)")
-  case toString (result probe) of
-    Right "ok" -> treeToViewType term
-    Right other -> Left $ "malformed view expression " ++ show expr ++ ": " ++ other
-    Left err -> Left $ "could not validate view expression " ++ show expr ++ ": " ++ err
-
-definitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
-definitionView args resultView =
-  case argViews of
-    [] -> finalView
-    _  -> VEApp (VEApp (VEName "Fn") (VEList argViews)) finalView
-  where
-    argViews = map defArgView args
-    finalView = maybe exportedViewAny id resultView
-
-defArgView :: DefArg -> ViewExpr
-defArgView (DefBinder _ Nothing) = exportedViewAny
-defArgView (DefBinder _ (Just ty)) = ty
-defArgView (DefPhantom ty) = ty
-
-exportedViewAny :: ViewExpr
-exportedViewAny = VEName "Any"
-
 defaultStorePath :: IO StorePath
 defaultStorePath = do
   home <- getHomeDirectory

src/Frontend/ContractDesugar.hs

@@ -0,0 +1,118 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Frontend.ContractDesugar
+  ( desugarContracts
+  , viewExprToAst
+  ) where
+
+import Research
+
+-- | Convert source-level contract annotations into runtime boundary checks.
+--
+-- Named binder annotations (e.g. @x@nat?) wrap each argument as it is
+-- received and the result before it is returned.
+--
+-- Phantom annotations (e.g. @nat? on a point-free definition) are turned
+-- into a fresh local raw value plus a wrapper definition that uses named
+-- binder annotations.  The raw value is bound with a local 'let' so that
+-- fixed points (such as definitions built with 'y') are shared rather than
+-- recreated on every call.  The wrapper only needs 'withContract' and
+-- 'matchResult' from the contract library.
+desugarContracts :: [TricuAST] -> [TricuAST]
+desugarContracts asts = concatMap desugarTopItem asts
+  where
+    desugarTopItem (SDefAnn name args ret body) = desugarDefAnn name args ret body
+    desugarTopItem other = [other]
+
+-- | Fresh internal name for the raw, contract-free helper introduced by
+-- phantom annotations.  It is bound locally with 'SLet' so it never escapes
+-- into the final environment.
+rawNameFor :: String -> String
+rawNameFor name = "_" ++ name ++ "_raw"
+
+desugarDefAnn :: String -> [DefArg] -> Maybe ViewExpr -> TricuAST -> [TricuAST]
+desugarDefAnn name args ret body
+  | all isPhantom args =
+      let argContracts = map getPhantom args
+          rawNm = rawNameFor name
+          rawVar = SVar rawNm Nothing
+          argNames = take (length args) ["x","y","z"]
+          newArgs = zipWith DefBinder argNames (map Just argContracts)
+          wrappedBody = foldl SApp rawVar (map (\n -> SVar n Nothing) argNames)
+          wrapper = wrapArgs newArgs (wrapReturn ret wrappedBody)
+      in [ SDef name [] (SLet rawNm body wrapper) ]
+  | otherwise = [ SDef name [] (wrapArgs args body') ]
+  where
+    body' = wrapReturn ret body
+
+    isPhantom (DefPhantom _) = True
+    isPhantom _              = False
+
+    getPhantom (DefPhantom c) = c
+    getPhantom _                = error "expected phantom annotation"
+
+    -- | Build:  matchResult onFail (\value _ -> body) result
+    bindResult result valueName body onFail =
+      matchResultE
+        onFail
+        (SLambda [valueName, "_"] body)
+        result
+
+    -- | Build:  matchResult (\msg _ -> err msg t) (\r _ -> r) result
+    returnResult result =
+      matchResultE
+        (SLambda ["msg", "_"] errResult)
+        (SLambda ["r", "_"] (SVar "r" Nothing))
+        result
+
+    -- | Build:  \msg _ -> \_ -> err msg t
+    absorbErr =
+      SLambda ["msg", "_"] (SLambda ["_"] errResult)
+
+    errResult = SApp (SApp (SVar "err" Nothing) (SVar "msg" Nothing)) TLeaf
+
+    wrapReturn Nothing b = b
+    wrapReturn (Just c) b = returnResult (withContractE (viewExprToAst c) b)
+
+    wrapArgs [] b = b
+    wrapArgs (DefBinder nm Nothing : rest) b = SLambda [nm] (wrapArgs rest b)
+    wrapArgs (DefBinder nm (Just c) : rest) b =
+      let onFail = if null rest then SLambda ["msg", "_"] errResult else absorbErr
+      in SLambda [nm] $
+           bindResult
+             (withContractE (viewExprToAst c) (SVar nm Nothing))
+             nm
+             (wrapArgs rest b)
+             onFail
+    wrapArgs (DefPhantom _ : _) _ =
+      error "phantom contract arguments are not yet supported by the frontend"
+
+-- | Turn a source annotation expression into an ordinary AST expression.
+-- Contract annotations are written with the same surface syntax as terms,
+-- so the mapping is mostly structural.
+viewExprToAst :: ViewExpr -> TricuAST
+viewExprToAst = \case
+  VEName s -> SVar s Nothing
+  VEVar s  -> SVar s Nothing
+  VEInt i  -> SInt i
+  VEString s -> SStr s
+  VEList es -> SList (map viewExprToAst es)
+  VEApp f a -> SApp (viewExprToAst f) (viewExprToAst a)
+  VERaw s -> SStr s
+  VEVarId _ -> error "view variable ids are not supported by the frontend"
+  VEForall _ _ -> error "forall annotations are not supported by the frontend"
+  VEExists _ _ -> error "exists annotations are not supported by the frontend"
+
+-- | Build an application of 'withContract' from the contract library.
+withContractE :: TricuAST -> TricuAST -> TricuAST
+withContractE contract value =
+  SApp (SApp (SVar "withContract" Nothing) contract) value
+
+-- | Build an application of 'matchResult' from the contract library.
+matchResultE :: TricuAST -> TricuAST -> TricuAST -> TricuAST
+matchResultE errCase okCase result =
+  SApp
+    (SApp
+      (SApp (SVar "matchResult" Nothing) errCase)
+      okCase)
+    result

src/Main.hs

@@ -1,18 +1,16 @@
 module Main where
 
-import Check (checkFile, checkFileWithStore, instrumentIOContinuations)
 import ContentStore
 import ContentStore.Bundle
 import Module.Manifest
 import System.Exit (die)
 import Eval (evalTricu, mainResult, result)
 import FileEval
-  ( ContractMode(..)
+  ( LoadedSource(..)
-  , LoadedSource(..)
   , defaultStorePath
-  , evaluateFileWithContextWithStoreAndMode
+  , evaluateFileWithContextWithStore
   , evaluateFileWithStore
-  , loadFileWithStoreMode
+  , loadFileWithStore
   , compileFileWithStore
   )
 import IODriver (IOPermissions(..), runIO)
@@ -47,16 +45,11 @@ data AppArgs = AppArgs
 
 data TricuArgs
   = Repl
-  | Check
-      { checkInput :: FilePath
-      , checkStore :: Maybe FilePath
-      }
   | Eval
       { evalFiles         :: [FilePath]
       , evalStore         :: Maybe FilePath
       , evalFormat        :: EvaluatedForm
       , evalOutput        :: FilePath
-      , evalUnchecked     :: Bool
       , evalIo            :: Bool
       , evalAllowRead     :: [FilePath]
       , evalAllowWrite    :: [FilePath]
@@ -112,16 +105,6 @@ readEvaluatedForm = eitherReader $ \s -> case s of
   "string"  -> Right StringLit
   _         -> Left $ "Unknown format: " ++ s ++ ". Expected: tree, fsl, ast, ternary, ascii, decode, number, string"
 
-checkParser :: Parser TricuArgs
-checkParser = Check
-  <$> argument str (metavar "FILE")
-  <*> optional (option str
-      ( long "store"
-     <> short 's'
-     <> metavar "PATH"
-     <> help "Content-addressed store path for module import resolution"
-      ))
-
 evalParser :: Parser TricuArgs
 evalParser = Eval
   <$> many (argument str (metavar "FILE..."))
@@ -145,10 +128,6 @@ evalParser = Eval
      <> value ""
      <> help "Write output to file instead of stdout"
       )
-  <*> switch
-      ( long "unchecked"
-     <> help "Evaluate as untyped code: ignore View Contract annotations and do not publish unchecked view refs"
-      )
   <*> switch
       ( long "io"
      <> help "Interpret the result as an IO action tree and execute it"
@@ -325,9 +304,7 @@ tricuParser = AppArgs
       <**> infoOption versionStr (long "version" <> help "Show version"))
   where
     topCommands = mconcat
-      [ command "check" (info (checkParser <**> helper)
+      [ command "eval" (info (evalParser <**> helper)
-          (progDesc "Check View Contract annotations and report ok or diagnostics"))
-      , command "eval" (info (evalParser <**> helper)
           (progDesc "Evaluate tricu source and print the result of the final expression"))
       , command "arboricx" (info (arboricxParser <**> helper)
           (progDesc "Arboricx bundle operations"))
@@ -374,7 +351,6 @@ main = do
       args = applyGlobalStore mGlobalStore (appCommand appArgs)
   case args of
     Repl               -> runReplWithStore mGlobalStore
-    Check {}           -> runCheck args
     Eval {}            -> runEval args
     ArboricxCompile {} -> runCompile args
     ArboricxImport {}  -> runImport args
@@ -390,7 +366,6 @@ main = do
 applyGlobalStore :: Maybe FilePath -> TricuArgs -> TricuArgs
 applyGlobalStore mGlobal args = case args of
   Repl -> Repl
-  Check {} -> args { checkStore = preferLocal (checkStore args) }
   Eval {} -> args { evalStore = preferLocal (evalStore args) }
   ArboricxCompile {} -> args { compileStore = preferLocal (compileStore args) }
   ArboricxImport {} -> args { importStore = preferLocal (importStore args) }
@@ -413,22 +388,6 @@ runReplWithStore mStore = do
     Nothing -> repl
     Just store -> replWithStore (StorePath store)
 
-runCheck :: TricuArgs -> IO ()
-runCheck opts = do
-  output <- case checkStore opts of
-    Nothing -> checkFile (checkInput opts)
-    Just storePath -> checkFileWithStore (StorePath storePath) (checkInput opts)
-  putStrLn output
-
-evaluateCheckedIOFile :: StorePath -> ContractMode -> Env -> FilePath -> IO Env
-evaluateCheckedIOFile store mode env filePath = do
-  loaded <- loadFileWithStoreMode mode store filePath
-  checkedAst <- case instrumentIOContinuations (loadedAst loaded) of
-    Left err -> die err
-    Right asts -> pure asts
-  viewEnv <- evaluateFileWithStore (Just store) "./lib/view.tri"
-  pure $ evalTricu (Map.unions [viewEnv, loadedImports loaded, env]) checkedAst
-
 runEval :: TricuArgs -> IO ()
 runEval opts = do
   let files = evalFiles opts
@@ -441,12 +400,7 @@ runEval opts = do
       return $ result env
     _  -> do
       mStoreOpt <- traverse (pure . StorePath) (evalStore opts)
-      let contractMode = if evalUnchecked opts then IgnoreContracts else EnforceContracts
+      finalEnv <- foldM (evaluateFileWithContextWithStore mStoreOpt) Map.empty files
-      finalEnv <- if evalIo opts && contractMode == EnforceContracts
-        then do
-          store <- maybe defaultStorePath pure mStoreOpt
-          foldM (evaluateCheckedIOFile store contractMode) Map.empty files
-        else foldM (evaluateFileWithContextWithStoreAndMode contractMode mStoreOpt) Map.empty files
       return $ mainResult finalEnv
   finalT <- if evalIo opts
     then do
@@ -488,8 +442,6 @@ runImport opts = do
             name
             (treeTermRef root)
             "arboricx.abi.tree.v1"
-            Nothing
-            Nothing
         | (name, root) <- roots
         ]
       moduleName = T.pack $ maybe (takeBaseName file) id (importModule opts)

src/Module/Manifest.hs

@@ -12,7 +12,6 @@ module Module.Manifest
 import ContentStore.Filesystem (getObject, putObject)
 import ContentStore.Object
 import ContentStore.Alias (ObjectRef(..))
-import Research (ViewProvenance(..))
 
 import Data.ByteString (ByteString)
 import Data.Text (Text)
@@ -36,13 +35,12 @@ data ModuleReference = ModuleReference
   , moduleReferenceRef   :: ObjectRef
   } deriving (Eq, Ord, Show)
 
--- | Exported executable artifact plus optional direct View Contract type.
+-- | Exported executable artifact. Optional contract terms are ordinary tree
+-- terms referenced from elsewhere in the store, not a special artifact kind.
 data ModuleExport = ModuleExport
   { moduleExportName   :: Text
   , moduleExportObject :: ObjectRef
   , moduleExportAbi    :: Text
-  , moduleExportView           :: Maybe ObjectRef
-  , moduleExportViewProvenance :: Maybe ViewProvenance
   } deriving (Eq, Ord, Show)
 
 manifestDomain :: Domain
@@ -66,9 +64,6 @@ encodeManifest manifest = encodeUtf8 $ Text.unlines $
       , esc (objectRefKind $ moduleExportObject ex)
       , esc (objectRefHash $ moduleExportObject ex)
       , esc (moduleExportAbi ex)
-      , maybe "-" (esc . objectRefKind) (moduleExportView ex)
-      , maybe "-" (esc . objectRefHash) (moduleExportView ex)
-      , maybe "-" encodeProvenance (moduleExportViewProvenance ex)
       ]
 
 -- | Parse the canonical manifest encoding.
@@ -87,27 +82,11 @@ decodeManifest bs = do
         ["reference", alias, kind, hash] -> do
           ref <- ModuleReference <$> unesc alias <*> (ObjectRef <$> unesc kind <*> unesc hash)
           Right manifest { moduleManifestReferences = moduleManifestReferences manifest ++ [ref] }
-        ["export", name, kind, hash, abi, viewKind, viewHash] -> do
+        ["export", name, kind, hash, abi] -> do
-          -- Legacy manifests predate explicit View Contract provenance. Keep
-          -- the decoded field absent; checker import code treats absent
-          -- provenance as ViewUnchecked/Assumed at the use boundary.
-          view <- optionalRef viewKind viewHash
           ex <- ModuleExport
             <$> unesc name
             <*> (ObjectRef <$> unesc kind <*> unesc hash)
             <*> unesc abi
-            <*> pure view
-            <*> pure Nothing
-          Right manifest { moduleManifestExports = moduleManifestExports manifest ++ [ex] }
-        ["export", name, kind, hash, abi, viewKind, viewHash, provenanceText] -> do
-          view <- optionalRef viewKind viewHash
-          provenance <- optionalProvenance provenanceText
-          ex <- ModuleExport
-            <$> unesc name
-            <*> (ObjectRef <$> unesc kind <*> unesc hash)
-            <*> unesc abi
-            <*> pure view
-            <*> pure provenance
           Right manifest { moduleManifestExports = moduleManifestExports manifest ++ [ex] }
         _ -> Left $ "invalid module manifest row: " ++ Text.unpack line
 
@@ -123,22 +102,6 @@ getManifest store h = do
       Left err -> fail $ "invalid module manifest " ++ Text.unpack h ++ ": " ++ err
       Right manifest -> return (Just manifest)
 
-optionalRef :: Text -> Text -> Either String (Maybe ObjectRef)
-optionalRef "-" "-" = Right Nothing
-optionalRef kind hash = Just <$> (ObjectRef <$> unesc kind <*> unesc hash)
-
-encodeProvenance :: ViewProvenance -> Text
-encodeProvenance ViewChecked = "checked"
-encodeProvenance ViewTrusted = "trusted"
-encodeProvenance ViewUnchecked = "unchecked"
-
-optionalProvenance :: Text -> Either String (Maybe ViewProvenance)
-optionalProvenance "-" = Right Nothing
-optionalProvenance "checked" = Right (Just ViewChecked)
-optionalProvenance "trusted" = Right (Just ViewTrusted)
-optionalProvenance "unchecked" = Right (Just ViewUnchecked)
-optionalProvenance other = Left $ "invalid View Contract provenance: " ++ Text.unpack other
-
 esc :: Text -> Text
 esc = Text.concatMap $ \c -> case c of
   '%'  -> "%25"

src/Module/Resolver.hs

@@ -9,7 +9,6 @@ module Module.Resolver
 
 import ContentStore.Alias
 import ContentStore.Arboricx (decodeTreeTerm, treeTermDomain)
-import ContentStore.ViewTree (decodeViewTree, viewTreeKind, viewTreeRootTerm)
 import ContentStore.Object
 import ContentStore.Resolver
 import Module.Manifest
@@ -20,15 +19,14 @@ import qualified Data.Set as Set
 import qualified Data.Text as T
 
 -- | A manifest export resolved into the importing source's local lexical scope.
--- The executable term is loaded, while object/view refs remain available for
+-- The executable term is loaded directly; contract terms are not interpreted by
--- later checker and diagnostics phases.
+-- the resolver.
 data ResolvedExport = ResolvedExport
   { resolvedExportSourceName :: T.Text
   , resolvedExportLocalName  :: String
   , resolvedExportObject     :: ObjectRef
   , resolvedExportAbi        :: T.Text
-  , resolvedExportView       :: Maybe ObjectRef
+  , resolvedExportContract   :: Maybe ObjectRef
-  , resolvedExportProvenance :: Maybe ViewProvenance
   , resolvedExportTerm       :: T
   } deriving (Show, Eq)
 
@@ -86,23 +84,13 @@ resolveModuleExport resolver namespace ex = do
         , resolvedExportLocalName = nsVariable namespace (T.unpack sourceName)
         , resolvedExportObject = ref
         , resolvedExportAbi = moduleExportAbi ex
-        , resolvedExportView = moduleExportView ex
-        , resolvedExportProvenance = moduleExportViewProvenance ex
         , resolvedExportTerm = term
         }
 
 resolveExportTerm :: ObjectResolver -> T.Text -> ObjectRef -> IO T
 resolveExportTerm resolver sourceName ref
-  | objectRefKind ref == viewTreeKind = do
-      bytes <- requireObject "view tree"
-      case decodeViewTree bytes >>= viewTreeRootTerm of
-        Left err -> errorWithoutStackTrace $
-          "Module export " ++ show (T.unpack sourceName)
-          ++ " references invalid view tree " ++ T.unpack (objectRefHash ref)
-          ++ ": " ++ err
-        Right term -> return term
   | objectRefKind ref == unDomain treeTermDomain = do
-      bytes <- requireObject "tree term"
+      bytes <- requireObject
       case decodeTreeTerm bytes of
         Left err -> errorWithoutStackTrace $
           "Module export " ++ show (T.unpack sourceName)
@@ -112,16 +100,15 @@ resolveExportTerm resolver sourceName ref
   | otherwise = errorWithoutStackTrace $
       "Module export " ++ show (T.unpack sourceName)
       ++ " has unsupported object kind " ++ show (T.unpack (objectRefKind ref))
-      ++ "; expected " ++ show (T.unpack viewTreeKind)
+      ++ "; expected " ++ show (T.unpack (unDomain treeTermDomain))
-      ++ " or " ++ show (T.unpack (unDomain treeTermDomain))
   where
-    requireObject label = do
+    requireObject = do
       mBytes <- resolverObject resolver ref
       case mBytes of
         Just bytes -> return bytes
         Nothing -> errorWithoutStackTrace $
           "Module export " ++ show (T.unpack sourceName)
-          ++ " references missing " ++ label ++ " " ++ T.unpack (objectRefHash ref)
+          ++ " references missing tree term " ++ T.unpack (objectRefHash ref)
           ++ " (kind " ++ T.unpack (objectRefKind ref) ++ ")"
 
 resolvedModulesEnv :: [ResolvedModule] -> Env

src/REPL.hs

@@ -1,12 +1,10 @@
 module REPL where
 
-import Check (checkFileWithStore)
 import Eval (evalTricu, result)
 import FileEval
-  ( ContractMode(..)
+  ( LoadedSource(..)
-  , LoadedSource(..)
   , defaultStorePath
-  , loadFileWithStoreMode
+  , loadFileWithStore
   )
 import Parser (parseTricu)
 import Research (EvaluatedForm(..), Env, formatT)
@@ -35,13 +33,11 @@ import qualified Data.Map as Map
 import qualified Data.Text as T
 
 -- | Source-local REPL with the same filesystem CAS/module loader used by the
--- CLI. View Contract checking is explicit (`!check`); evaluation can run in
+-- CLI.
--- normal publishing mode or unchecked mode.
 data REPLState = REPLState
   { replForm   :: EvaluatedForm
   , replEnv    :: Env
   , replStore  :: StorePath
-  , replContracts :: ContractMode
   , replEnvRef :: IORef Env
   }
 
@@ -56,7 +52,7 @@ replWithStore store = do
         , historyFile = Just "~/.local/state/tricu/history"
         , autoAddHistory = True
         }
-  runInputT settings (loop (REPLState Decode Map.empty store EnforceContracts envRef))
+  runInputT settings (loop (REPLState Decode Map.empty store envRef))
   where
 
     loop :: REPLState -> InputT IO ()
@@ -78,12 +74,10 @@ replWithStore store = do
             "!output" -> handleOutput state
             "!env" -> handleEnv state >> loop state
             _ | "!load" `isPrefixOf` s -> handleLoad state (strip $ drop 5 s)
-              | "!check" `isPrefixOf` s -> handleCheck state (strip $ drop 6 s)
               | "!use" `isPrefixOf` s -> handleUse state (strip $ drop 4 s)
               | "!name" `isPrefixOf` s -> handleName state (strip $ drop 5 s)
               | "!store" `isPrefixOf` s -> handleStore state (strip $ drop 6 s)
               | "!format" `isPrefixOf` s -> handleFormat state (strip $ drop 7 s)
-              | "!unchecked" `isPrefixOf` s -> handleUnchecked state (strip $ drop 10 s)
               | take 2 s == "--" -> loop state
               | otherwise -> do
                   next <- liftIO $ catch (processInput state raw) (errorHandler state)
@@ -102,9 +96,7 @@ replWithStore store = do
       outputStrLn "  !load FILE             - Load and evaluate a .tri file into the environment"
       outputStrLn "  !use MODULE [NS]       - Load a module alias/manifest from the store (NS defaults to !Local)"
       outputStrLn "  !name NAME [LOCAL]     - Load a name alias/tree-term hash from the store"
-      outputStrLn "  !check FILE            - Check View Contract annotations in a .tri file"
       outputStrLn "  !store [PATH]          - Show or set the content-addressed store path"
-      outputStrLn "  !unchecked [on|off]    - Show or set unchecked eval mode"
       outputStrLn "  !env                   - List names currently in the REPL environment"
 
     handleOutput :: REPLState -> InputT IO ()
@@ -135,24 +127,12 @@ replWithStore store = do
           if not exists
             then outputStrLn ("File not found: " ++ path) >> loop state
             else do
-              loaded <- liftIO $ loadFileWithStoreMode (replContracts state) (replStore state) path
+              loaded <- liftIO $ loadFileWithStore (replStore state) path
               let env' = evalTricu (Map.union (loadedImports loaded) (replEnv state)) (loadedAst loaded)
               liftIO $ writeIORef (replEnvRef state) env'
               outputStrLn $ "Loaded " ++ path
               loop state { replEnv = env' }
 
-    handleCheck :: REPLState -> String -> InputT IO ()
-    handleCheck state path
-      | null path = outputStrLn "Usage: !check FILE" >> loop state
-      | otherwise = do
-          exists <- liftIO $ doesFileExist path
-          if not exists
-            then outputStrLn ("File not found: " ++ path) >> loop state
-            else do
-              output <- liftIO $ checkFileWithStore (replStore state) path
-              outputStrLn output
-              loop state
-
     handleUse :: REPLState -> String -> InputT IO ()
     handleUse state arg = case words arg of
       [] -> outputStrLn "Usage: !use MODULE [NAMESPACE]" >> loop state
@@ -205,23 +185,6 @@ replWithStore store = do
           outputStrLn $ "Store changed to: " ++ path
           loop state { replStore = StorePath path }
 
-    handleUnchecked :: REPLState -> String -> InputT IO ()
-    handleUnchecked state arg = setUnchecked state arg
-
-    setUnchecked :: REPLState -> String -> InputT IO ()
-    setUnchecked state arg = case arg of
-      ""    -> reportContracts state >> loop state
-      "on"  -> setMode IgnoreContracts
-      "off" -> setMode EnforceContracts
-      _     -> outputStrLn "Usage: !unchecked [on|off]" >> loop state
-      where
-        setMode mode = do
-          outputStrLn $ contractModeMessage mode
-          loop state { replContracts = mode }
-
-    reportContracts :: REPLState -> InputT IO ()
-    reportContracts state = outputStrLn $ contractModeMessage (replContracts state)
-
     handleEnv :: REPLState -> InputT IO ()
     handleEnv state =
       case sort (Map.keys (replEnv state)) of
@@ -263,12 +226,10 @@ completeRepl envRef input@(left, _right)
       , "!load"
       , "!use"
       , "!name"
-      , "!check"
       , "!store"
-      , "!unchecked"
       , "!env"
       ]
-    commandWantsFile inputLine = any (`isPrefixOf` inputLine) ["!load ", "!check "]
+    commandWantsFile inputLine = "!load " `isPrefixOf` inputLine
     termBreakChars = " \t\n\r()[]{}\"'"
 
 outputFormats :: [EvaluatedForm]
@@ -286,10 +247,6 @@ readEvaluatedForm s = case s of
   "string"  -> Just StringLit
   _         -> Nothing
 
-contractModeMessage :: ContractMode -> String
-contractModeMessage EnforceContracts = "Contracts: on"
-contractModeMessage IgnoreContracts  = "Contracts: off (unchecked eval)"
-
 storePathString :: StorePath -> FilePath
 storePathString (StorePath path) = path
 

src/Research.hs

@@ -19,40 +19,9 @@ import qualified Data.Text       as T
 data T = Leaf | Stem T | Fork T T
   deriving (Show, Eq, Ord)
 
--- View Contract source annotations
+-- Contract source annotations for @ and =@ syntax. ViewExpr carries the
-data ViewRef
+-- surface syntax of a contract until Frontend.ContractDesugar turns it into a
-  = ViewRefInt Integer
+-- runtime contract application.
-  | ViewRefText String
-  deriving (Show, Eq, Ord)
-
-data ViewProvenance
-  = ViewChecked
-  | ViewTrusted
-  | ViewUnchecked
-  deriving (Show, Eq, Ord)
-
-data ViewType
-  = VTName String
-  | VTVar Integer
-  | VTRefRaw ViewRef
-  | VTList ViewType
-  | VTMaybe ViewType
-  | VTPair ViewType ViewType
-  | VTResult ViewType ViewType
-  | VTGuarded ViewType T
-  | VTForall [Integer] ViewType
-  | VTExists [Integer] ViewType
-  | VTFn [ViewType] ViewType
-  deriving (Show, Eq, Ord)
-
-pattern VTRef :: Integer -> ViewType
-pattern VTRef n = VTRefRaw (ViewRefInt n)
-
-pattern VTRefText :: String -> ViewType
-pattern VTRefText s = VTRefRaw (ViewRefText s)
-
-{-# COMPLETE VTName, VTVar, VTRef, VTRefText, VTList, VTMaybe, VTPair, VTResult, VTGuarded, VTForall, VTExists, VTFn #-}
-
 data ViewExpr
   = VEName String
   | VEVar String

tricu.cabal

@@ -62,9 +62,6 @@ executable tricu
     , vector
     , zlib
   other-modules:
-    Check
-    Check.Core
-    Check.IO
     ContentStore
     ContentStore.Alias
     ContentStore.Arboricx
@@ -72,10 +69,9 @@ executable tricu
     ContentStore.Filesystem
     ContentStore.Object
     ContentStore.Resolver
-    ContentStore.ViewTree
-    ContentStore.ViewContract
     Eval
     FileEval
+    Frontend.ContractDesugar
     IODriver
     Lexer
     Module.Manifest
@@ -113,6 +109,7 @@ benchmark tricu-bench
     , memory
     , mtl
     , network
+    , stm
     , text
     , time
     , transformers
@@ -128,10 +125,9 @@ benchmark tricu-bench
     ContentStore.Filesystem
     ContentStore.Object
     ContentStore.Resolver
-    ContentStore.ViewTree
-    ContentStore.ViewContract
     Eval
     FileEval
+    Frontend.ContractDesugar
     IODriver
     Lexer
     Module.Manifest
@@ -181,9 +177,6 @@ test-suite tricu-tests
     , zlib
   default-language:    Haskell2010
   other-modules:
-    Check
-    Check.Core
-    Check.IO
     ContentStore
     ContentStore.Alias
     ContentStore.Arboricx
@@ -191,10 +184,9 @@ test-suite tricu-tests
     ContentStore.Filesystem
     ContentStore.Object
     ContentStore.Resolver
-    ContentStore.ViewTree
-    ContentStore.ViewContract
     Eval
     FileEval
+    Frontend.ContractDesugar
     IODriver
     Lexer
     Module.Manifest

tricu.workspace

@@ -1,6 +1,5 @@
 # tricu workspace module source map
 module base = lib/base.tri
-module list = lib/list.tri
 module bytes = lib/bytes.tri
 module conversions = lib/conversions.tri
 module prelude = lib/prelude.tri
@@ -9,8 +8,8 @@ module patterns = lib/patterns.tri
 module io = lib/io.tri
 module socket = lib/socket.tri
 module http = lib/http.tri
-module view = lib/view.tri
+module intensional = lib/intensionalContracts.tri
-module views.catalog = lib/views/catalog.tri
+module guarded = lib/guardedBase.tri
 module arboricx.common = lib/arboricx/common.tri
 module arboricx.nodes = lib/arboricx/nodes.tri
 module arboricx.manifest = lib/arboricx/manifest.tri