Runtime contract guard kernel

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,9 +63,6 @@ tricu eval --format decode program.tri
 tricu eval --output result.txt program.tri
 ```
 
-Annotations are parsed but currently ignored at runtime; the contract layer
-is not yet wired into evaluation or workspace module auto-builds.
-
 Compile/import/export Arboricx bundles:
 
 ```sh
@@ -73,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

demos/contractBasics.tri

@@ -1,10 +1,6 @@
-!import "base" !Local
-!import "list" !Local
-!import "contracts" !Local
+!import "prelude" !Local
 
--- A custom 'and' combinator written directly against base.matchResult.
--- It succeeds only when *both* contracts succeed, threading the checked value
--- from the first into the second. This makes the Result pair structure explicit.
+-- Custom contract combinators built directly on matchResult.
 myAndC = (c1 c2 value rest :
   matchResult
     (msg _ : contractErr msg rest)
@@ -12,32 +8,18 @@ myAndC = (c1 c2 value rest :
     (c1 value rest))
 
 -- Plain predicates lifted into contracts with a diagnostic message.
-natural? = guardC "natural" (n : gte? n 0)
-nonZero? = guardC "non-zero" (n : not? (isZero? n))
+natural? = guardC "natural" isNat?
+nonZero? = guardC "non-zero" (n : and? (isNat? n) (not? (isZero_? n)))
 
--- Safe wrappers around partial base / list functions.
--- The frontend desugars @ and =@ into runtime withContract applications.
-safeDiv a@natural? b@(myAndC natural? nonZero?) =@natural? div a b
+-- 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
 
-safeHead xs@(nonEmptyListOf anyC) =@anyC head xs
-safeTail xs@(nonEmptyListOf anyC) =@(listOf anyC) tail xs
+-- 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)
 
--- A higher-order wrapper: the supplied function must satisfy a contract,
--- the input list must satisfy a contract, and the result list is guaranteed.
-checkedMap f@(fnContract anyC natural?) xs@(listOf anyC) =@(listOf natural?) map f xs
-
--- Advertise the safe wrappers in the module manifest with their own contracts.
-!export safeDiv : fn2 natural? nonZero? natural?
-!export safeHead : fnContract (nonEmptyListOf anyC) anyC
-!export checkedMap : fn2 (fnContract anyC natural?) (listOf anyC) (listOf natural?)
-
--- A small interaction-tree pipeline that uses contracts as recoverable effects.
-pipeline = (input :
-  do bindM
-    scaled <- checkM natural? (mul input 2)
-    half   <- handleM "contract"
-                  (_ : pureM 1)
-                  (checkM nonZero? (sub scaled 4))
-    pureM (div scaled half))
-
-main = runM (pipeline 5)
+main = pair checkedSuccessor (myDiv 10 2)

demos/contractEffects.tri

@@ -1,6 +1,4 @@
-!import "base" !Local
-!import "list" !Local
-!import "contracts" !Local
+!import "prelude" !Local
 
 -- ---------------------------------------------------------------------------
 -- Contracts + interaction trees with `do` notation

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 "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- Environment effects: ask and local.

demos/interactionTrees/forkAwait.tri

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

demos/interactionTrees/greet.tri

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

demos/interactionTrees/safeRead.tri

@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import prelude !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 "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- Transform an IO result.

demos/interactionTrees/state.tri

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

demos/interactionTrees/writeThenRead.tri

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

demos/interactionTrees/yield.tri

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

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))
-    x)
+    (_ _ : succ (self (pred_ x) y))
+    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? b a
+lte? @nat? @nat? =@bool? lte_?
 
-lt? = a b :
-  and? (lte? a b) (not? (equal? a b))
+gte_? = a b : lte_? b a
 
-gt? = a b :
-  lt? b a
+gte? @nat? @nat? =@bool? gte_?
 
-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/contracts.tri

@@ -1,240 +0,0 @@
-!import "base" !Local
-!import "list" !Local
-
--- ---------------------------------------------------------------------------
--- 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.
--- ---------------------------------------------------------------------------
-
-contractOk = (value : (rest : ok value rest))
-contractErr = (msg : (rest : err msg rest))
-
--- Apply a contract with the conventional rest slot and return the raw Result.
-checkContract = (contract value : contract value t)
-
--- Apply a contract and continue with either the onOk or onFail branch.
-withContract = (contract value onOk onFail :
-  matchResult
-    (msg _ : onFail msg)
-    (checked _ : onOk checked)
-    (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))
-
--- Natural number contract.
-nat? = guardC "not a natural number" (n : gte? n 0)
-
--- Non-zero number contract.
-nonZero? = guardC "non-zero" (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 :
-      withContract argC x
-        (x' :
-          withContract resC (f x')
-            (y : contractOk y rest1)
-            (msg : contractErr msg rest1))
-        (msg : contractErr msg rest1)))
-    rest)
-
-fn2 = (arg1C arg2C resC f rest :
-  contractOk
-    (x : (rest1 :
-      withContract arg1C x
-        (x' :
-          contractOk
-            (y : (rest2 :
-              withContract arg2C y
-                (y' :
-                  withContract resC (f x' y')
-                    (z : contractOk z rest2)
-                    (msg : contractErr msg rest2))
-                (msg : contractErr msg rest2)))
-            rest1)
-        (msg : contractErr msg rest1)))
-    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/conversions.tri

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

lib/guardedBase.tri

@@ -1,24 +0,0 @@
-!import "base" !Local
-!import "list" !Local
-!import "contracts" !Local
-!import "intensional" !Local
-
--- Runtime-guarded wrappers around partial or structurally-sensitive base/list
--- functions. Each wrapper uses the frontend @ / =@ desugaring and is exported
--- with an advertised contract so manifests carry the contract terms.
-
-safeHead xs@(nonEmptyListOf anyC) =@anyC head xs
-safeTail xs@(nonEmptyListOf anyC) =@(listOf anyC) tail xs
-
-safeDiv a@nat? b@(andC nat? nonZero?) =@nat? div a b
-
-safeHalf n@(andC nat? evenC?) =@nat? div n 2
-
--- last is only guaranteed to return the maximum if the input list is sorted.
-sortedMax xs@(sortedList? nat?) =@nat? last xs
-
-!export safeHead : fnContract (nonEmptyListOf anyC) anyC
-!export safeTail : fnContract (nonEmptyListOf anyC) (listOf anyC)
-!export safeDiv : fn2 nat? nonZero? nat?
-!export safeHalf : fnContract (andC nat? evenC?) nat?
-!export sortedMax : fnContract (sortedList? nat?) nat?

lib/intensionalContracts.tri

@@ -1,6 +1,4 @@
-!import "base" !Local
-!import "list" !Local
-!import "contracts" !Local
+!import "prelude" !Local
 
 -- Structural contracts that exploit Tree Calculus's intensional nature.
 -- These are not simple type tags; they recursively inspect the tree shape.

lib/list.tri

@@ -1,342 +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
-
-sum = foldl (acc x : add x acc) 0
-product = 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.
---
--- 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

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.

src/Eval.hs

@@ -73,6 +73,19 @@ evalTricu env x = go env (reorderDefs env (map recoverParams (desugarContracts 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)
@@ -205,8 +218,6 @@ freeVars (SDefAnn _ args ret body) =
       , Set.singleton "withContract"
       ])
     (Set.fromList (annotatedBinders args))
-freeVars (SExport _ Nothing) = Set.empty
-freeVars (SExport _ (Just c)) = freeVarsViewExpr c
 freeVars (TStem t) = freeVars t
 freeVars (TFork t u) = Set.union (freeVars t) (freeVars u)
 freeVars (SList xs) = foldMap freeVars xs

src/FileEval.hs

@@ -16,8 +16,8 @@ module FileEval
   ) where
 
 import ContentStore
-import Eval (evalASTSync, evalTricu, freeVars, result)
-import Frontend.ContractDesugar (viewExprToAst)
+import Eval (evalTricu, freeVars, result, injectKernel)
+import Frontend.ContractDesugar (desugarContracts)
 import Lexer
 import Module.Manifest
 import Module.Resolver
@@ -81,7 +81,7 @@ 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
@@ -91,7 +91,7 @@ evaluateFileWithContextWithStore mStore env filePath = do
   loaded <- case mStore of
     Nothing    -> loadFile 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
@@ -127,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
           }
 
@@ -159,37 +160,25 @@ buildWorkspaceModule ctx store moduleName sourcePath = do
   loaded <- loadFile' ctx sourcePath
   let asts = loadedAst loaded
       env = evalTricu (loadedImports loaded) asts
-      explicitExports = topLevelExports asts
       localNames = topLevelDefinitions asts
-      names = if not (null explicitExports)
-                then explicitExports
-                else if null localNames
-                       then map (\n -> (n, Nothing)) (filter (/= "!result") (Map.keys env))
-                       else map (\n -> (n, Nothing)) localNames
+      names = if null localNames
+                then filter (/= "!result") (Map.keys env)
+                else localNames
   exports <- mapM (buildExport env) names
   manifestHash <- putManifest store (ModuleManifest [] exports)
   writeAlias store ModuleAlias (T.pack moduleName) (ObjectRef (unDomain manifestDomain) manifestHash)
   where
-    buildExport env (name, mContract) = 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
       Just term -> do
         rootRef <- putTreeTerm store term
-        mContractRef <- case mContract of
-          Nothing -> return Nothing
-          Just c  -> do
-            cterm <- evaluateContract env c
-            chash <- putTreeTerm store cterm
-            return (Just (ObjectRef (unDomain treeTermDomain) chash))
         return ModuleExport
           { moduleExportName = T.pack name
           , moduleExportObject = ObjectRef (unDomain treeTermDomain) rootRef
           , moduleExportAbi = "arboricx.abi.tree.v1"
-          , moduleExportContract = mContractRef
           }
 
-    evaluateContract env c = return $ evalASTSync env (viewExprToAst c)
-
 topLevelDefinitions :: [TricuAST] -> [String]
 topLevelDefinitions = mapMaybe go
   where
@@ -197,12 +186,6 @@ topLevelDefinitions = mapMaybe go
     go (SDefAnn name _ _ _) = Just name
     go _ = Nothing
 
-topLevelExports :: [TricuAST] -> [(String, Maybe ViewExpr)]
-topLevelExports = mapMaybe go
-  where
-    go (SExport name mContract) = Just (name, mContract)
-    go _ = Nothing
-
 defaultStorePath :: IO StorePath
 defaultStorePath = do
   home <- getHomeDirectory

src/Frontend/ContractDesugar.hs

@@ -3,59 +3,90 @@
 module Frontend.ContractDesugar
   ( desugarContracts
   , viewExprToAst
-  , withContractE
   ) where
 
 import Research
 
 -- | Convert source-level contract annotations into runtime boundary checks.
 --
--- A definition such as
+-- Named binder annotations (e.g. @x@nat?) wrap each argument as it is
+-- received and the result before it is returned.
 --
---     addPos x@positive? y@positive? =@positive? (add x y)
---
--- is desugared to a plain definition whose body wraps every annotated
--- argument and the result with 'withContract' from the contract library:
---
---     addPos = \x -> withContract positive? x
---       (\x -> \y -> withContract positive? y
---         (\y -> withContract positive? (add x y)
---           (\r -> r)
---           (\msg _ -> msg))
---         (\msg _ -> msg))
---       (\msg _ -> msg)
---
--- This makes annotated source depend on the existing 'withContract' helper,
--- which is an ordinary 'tricu' function from 'lib/contracts.tri'. Files that
--- use annotations should import the contract library (or another library that
--- re-exports 'withContract').
+-- 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 = map desugarTopItem asts
+desugarContracts asts = concatMap desugarTopItem asts
   where
     desugarTopItem (SDefAnn name args ret body) = desugarDefAnn name args ret body
-    desugarTopItem other = other
+    desugarTopItem other = [other]
 
-desugarDefAnn :: String -> [DefArg] -> Maybe ViewExpr -> TricuAST -> TricuAST
-desugarDefAnn name args ret body = SDef name [] (wrapArgs args body')
+-- | 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 =
-      withContractE (viewExprToAst c) b (SLambda ["r"] (SVar "r" Nothing)) errCont
+    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 =
-      SLambda [nm] $
-        withContractE (viewExprToAst c) (SVar nm Nothing)
-          (SLambda [nm] (wrapArgs rest b))
-          errCont
+      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"
 
-    errCont = SLambda ["msg"] (SVar "msg" Nothing)
-
 -- | 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.
@@ -73,12 +104,15 @@ viewExprToAst = \case
   VEExists _ _ -> error "exists annotations are not supported by the frontend"
 
 -- | Build an application of 'withContract' from the contract library.
-withContractE :: TricuAST -> TricuAST -> TricuAST -> TricuAST -> TricuAST
-withContractE contract value onOk onFail =
+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
-        (SApp (SVar "withContract" Nothing) contract)
-        value)
-      onOk)
-    onFail
+      (SApp (SVar "matchResult" Nothing) errCase)
+      okCase)
+    result

src/Lexer.hs

@@ -36,7 +36,6 @@ tricuLexer = do
       , try dot
       , try identifierWithHash
       , try keywordT
-      , try lExport
       , try identifier
       , try namespace
       , try integerLiteral
@@ -131,9 +130,6 @@ lImport = do
   name <- importAlias
   return (LImport path name)
 
-lExport :: Lexer LToken
-lExport = string "!export" *> notFollowedBy alphaNumChar $> LExport
-
 importAlias :: Lexer String
 importAlias = string "!Local" <|> do
   first <- letterChar <|> char '_'

src/Main.hs

@@ -442,7 +442,6 @@ runImport opts = do
             name
             (treeTermRef root)
             "arboricx.abi.tree.v1"
-            Nothing
         | (name, root) <- roots
         ]
       moduleName = T.pack $ maybe (takeBaseName file) id (importModule opts)

src/Module/Manifest.hs

@@ -41,7 +41,6 @@ data ModuleExport = ModuleExport
   { moduleExportName   :: Text
   , moduleExportObject :: ObjectRef
   , moduleExportAbi    :: Text
-  , moduleExportContract :: Maybe ObjectRef
   } deriving (Eq, Ord, Show)
 
 manifestDomain :: Domain
@@ -59,17 +58,13 @@ encodeManifest manifest = encodeUtf8 $ Text.unlines $
       , esc (objectRefKind $ moduleReferenceRef ref)
       , esc (objectRefHash $ moduleReferenceRef ref)
       ]
-    encodeExport ex =
-      let base = Text.intercalate "\t"
-            [ "export"
-            , esc (moduleExportName ex)
-            , esc (objectRefKind $ moduleExportObject ex)
-            , esc (objectRefHash $ moduleExportObject ex)
-            , esc (moduleExportAbi ex)
-            ]
-      in case moduleExportContract ex of
-           Nothing -> base
-           Just ref -> base <> "\t" <> esc (objectRefKind ref) <> "\t" <> esc (objectRefHash ref)
+    encodeExport ex = Text.intercalate "\t"
+      [ "export"
+      , esc (moduleExportName ex)
+      , esc (objectRefKind $ moduleExportObject ex)
+      , esc (objectRefHash $ moduleExportObject ex)
+      , esc (moduleExportAbi ex)
+      ]
 
 -- | Parse the canonical manifest encoding.
 decodeManifest :: ByteString -> Either String ModuleManifest
@@ -92,14 +87,6 @@ decodeManifest bs = do
             <$> unesc name
             <*> (ObjectRef <$> unesc kind <*> unesc hash)
             <*> unesc abi
-            <*> pure Nothing
-          Right manifest { moduleManifestExports = moduleManifestExports manifest ++ [ex] }
-        ["export", name, kind, hash, abi, ckind, chash] -> do
-          ex <- ModuleExport
-            <$> unesc name
-            <*> (ObjectRef <$> unesc kind <*> unesc hash)
-            <*> unesc abi
-            <*> (Just <$> (ObjectRef <$> unesc ckind <*> unesc chash))
           Right manifest { moduleManifestExports = moduleManifestExports manifest ++ [ex] }
         _ -> Left $ "invalid module manifest row: " ++ Text.unpack line
 

src/Module/Resolver.hs

@@ -84,7 +84,6 @@ resolveModuleExport resolver namespace ex = do
         , resolvedExportLocalName = nsVariable namespace (T.unpack sourceName)
         , resolvedExportObject = ref
         , resolvedExportAbi = moduleExportAbi ex
-        , resolvedExportContract = moduleExportContract ex
         , resolvedExportTerm = term
         }
 

src/Parser.hs

@@ -69,12 +69,9 @@ manyItemsP = do
 topItemP :: TokParser TricuAST
 topItemP = do
   toks <- getInput
-  case toks of
-    LExport : _ -> exportP
-    _ ->
-      case definitionHeadTop toks of
-        Just _  -> definitionP
-        Nothing -> exprTopP
+  case definitionHeadTop toks of
+    Just _  -> definitionP
+    Nothing -> exprTopP
 
 definitionHeadTop :: [LToken] -> Maybe (String, [String])
 definitionHeadTop toks =
@@ -221,13 +218,6 @@ importP = do
     isImport (LImport _ _) = True
     isImport _             = False
 
-exportP :: TokParser TricuAST
-exportP = do
-  void (tok (== LExport) "export")
-  name <- identifierNameP
-  mContract <- optional (tok (== LColon) ":" *> annotationTypeP)
-  pure (SExport name mContract)
-
 exprTopP :: TokParser TricuAST
 exprTopP = do
   toks <- getInput

src/Research.hs

@@ -19,10 +19,9 @@ import qualified Data.Text       as T
 data T = Leaf | Stem T | Fork T T
   deriving (Show, Eq, Ord)
 
--- Contract source annotations
--- ViewType, ViewRef, and ViewProvenance were removed with the old View Contract
--- checker. Source annotations are still parsed into ViewExpr but are not
--- interpreted by a separate static checker.
+-- Contract source annotations for @ and =@ syntax. ViewExpr carries the
+-- surface syntax of a contract until Frontend.ContractDesugar turns it into a
+-- runtime contract application.
 data ViewExpr
   = VEName String
   | VEVar String
@@ -61,7 +60,6 @@ data TricuAST
   | SLet String TricuAST TricuAST
   | SEmpty
   | SImport String String
-  | SExport String (Maybe ViewExpr)
   deriving (Show, Eq, Ord)
 
 -- Lexer Tokens
@@ -71,7 +69,6 @@ data LToken
   | LKeywordT
   | LNamespace String
   | LImport String String
-  | LExport
   | LAssign
   | LAssignAt
   | LAt

test/Spec.hs

@@ -19,7 +19,7 @@ import qualified Network.Socket as NS
 import Control.Monad         (forM, forM_)
 import Control.Monad.IO.Class (liftIO)
 import System.IO.Temp         (withSystemTempDirectory)
-import System.Directory      (createDirectory, doesFileExist, doesDirectoryExist, listDirectory)
+import System.Directory      (createDirectory, doesFileExist, doesDirectoryExist, listDirectory, getCurrentDirectory)
 import System.FilePath       ((</>))
 import Data.Bits              (xor)
 import Data.Char              (digitToInt)
@@ -51,17 +51,14 @@ testStore = StorePath "/tmp/tricu-test-store"
 allTestLibsEnv :: Env
 allTestLibsEnv = unsafePerformIO $ do
   base    <- evaluateFile "./lib/base.tri"
-  list    <- evaluateFile "./lib/list.tri"
   bytes   <- evaluateFile "./lib/bytes.tri"
   bin     <- evaluateFile "./lib/binary.tri"
   http    <- evaluateFile "./lib/http.tri"
   arbor   <- evaluateFile "./lib/arboricx/arboricx.tri"
   io      <- evaluateFile "./lib/io.tri"
   sock    <- evaluateFile "./lib/socket.tri"
-  contracts     <- evaluateFile "./lib/contracts.tri"
   intensional   <- evaluateFile "./lib/intensionalContracts.tri"
-  guarded       <- evaluateFile "./lib/guardedBase.tri"
-  pure (Map.unions [base, list, bytes, bin, http, arbor, io, sock, contracts, intensional, guarded])
+  pure (injectKernel (Map.unions [base, bytes, bin, http, arbor, io, sock, intensional]))
 {-# NOINLINE allTestLibsEnv #-}
 
 tests :: TestTree
@@ -1264,7 +1261,7 @@ contractsTests = testGroup "Contracts library tests"
             , "main = boom"
             ]
           env = evalTricu allTestLibsEnv (parseTricu input)
-      result env @?= ofString "boom"
+      decodeResult (result env) @?= "[t, \"boom\"]"
 
   , testCase "@ argument annotation passes" $ do
       let input = unlines
@@ -1280,7 +1277,7 @@ contractsTests = testGroup "Contracts library tests"
             , "main = idNat 5"
             ]
           env = evalTricu allTestLibsEnv (parseTricu input)
-      result env @?= ofString "bad"
+      decodeResult (result env) @?= "[t, \"bad\"]"
   ]
 
 arithmetic :: TestTree
@@ -1679,8 +1676,8 @@ demos = testGroup "Test provided demo functionality"
       res     <- liftIO $ evaluateFileResult "./demos/contractEffects.tri"
       decodeResult res @?= "[t t, 10]"
   , testCase "Safe base wrappers demo" $ do
-      res     <- liftIO $ evaluateFileResult "./demos/safeBaseWrappers.tri"
-      decodeResult res @?= "[t t, 1]"
+      res     <- liftIO $ evaluateFileResult "./demos/contractBasics.tri"
+      decodeResult res @?= "[3, t t, t, t t]"
   ]
 
 decoding :: TestTree
@@ -1944,7 +1941,6 @@ contentStoreTests = testGroup "Content Store Tests"
                   "main"
                   (ObjectRef (unDomain treeTermDomain) root)
                   "arboricx.abi.tree.v1"
-                  Nothing
               ]
         root <- putTreeTerm store term
         h <- putManifest store (manifestFor root)
@@ -1961,7 +1957,6 @@ contentStoreTests = testGroup "Content Store Tests"
                 "value"
                 (ObjectRef (unDomain treeTermDomain) termH)
                 "arboricx.abi.tree.v1"
-                Nothing
               ]
           manifestBytes = encodeManifest manifest
           manifestH = hashObject manifestDomain manifestBytes
@@ -2015,32 +2010,20 @@ contentStoreTests = testGroup "Content Store Tests"
               Nothing -> assertFailure "expected workspace module manifest"
               Just manifest -> map moduleExportName (moduleManifestExports manifest) @?= ["value"]
 
-  , testCase "Workspace modules: explicit !export with contract" $
-      withSystemTempDirectory "tricu-workspace-explicit-export" $ \dir -> do
+  , testCase "Workspace modules: contract annotations travel with exported definitions" $
+      withSystemTempDirectory "tricu-workspace-contract-export" $ \dir -> do
         let store = StorePath (dir </> "store")
             libPath = dir </> "util.tri"
             mainPath = dir </> "main.tri"
-        writeFile (dir </> "tricu.workspace") "module util = util.tri\n"
-        writeFile libPath "alwaysOk = (x : x)\n\naddOne x = x\n!export addOne : alwaysOk\n"
-        writeFile mainPath "!import \"util\" Util\n\nmain = Util.addOne 5\n"
+        cwd <- getCurrentDirectory
+        writeFile (dir </> "tricu.workspace") ("module base = \"" ++ cwd </> "lib/base.tri\"\nmodule util = \"" ++ dir </> "util.tri\"\n")
+        writeFile libPath "!import \"base\" !Local\n\nalwaysOk = (value rest : ok value rest)\n\nneverOk = (value rest : err \"nope\" rest)\n\nsafeId n@alwaysOk =@alwaysOk n\n\nbadId n@neverOk =@neverOk n\n"
+        writeFile mainPath "!import \"util\" Util\n\nmain = Util.safeId 5\n"
         env <- evaluateFileWithStore (Just store) mainPath
         result env @?= ofNumber 5
-        mAlias <- readAlias store ModuleAlias "util"
-        case mAlias of
-          Nothing -> assertFailure "expected workspace build to write util module alias"
-          Just ref -> do
-            mManifest <- getManifest store (objectRefHash ref)
-            case mManifest of
-              Nothing -> assertFailure "expected workspace module manifest"
-              Just manifest -> do
-                map moduleExportName (moduleManifestExports manifest) @?= ["addOne"]
-                case moduleManifestExports manifest of
-                  [ex] -> do
-                    assertBool "expected contract ref" (moduleExportContract ex /= Nothing)
-                    case moduleExportContract ex of
-                      Just cref -> objectRefKind cref @?= unDomain treeTermDomain
-                      Nothing -> assertFailure "expected contract ref"
-                  _ -> assertFailure "expected exactly one export"
+        writeFile mainPath "!import \"util\" Util\n\nmain = Util.badId 5\n"
+        envFail <- evaluateFileWithStore (Just store) mainPath
+        decodeResult (result envFail) @?= "[t, \"nope\"]"
 
   , testCase "Module imports: resolve manifest exports from store" $
       withSystemTempDirectory "tricu-module-import" $ \dir -> do
@@ -2052,7 +2035,6 @@ contentStoreTests = testGroup "Content Store Tests"
                   "value"
                   (ObjectRef (unDomain treeTermDomain) root)
                   "arboricx.abi.tree.v1"
-                  Nothing
               ]
         root <- putTreeTerm store term
         manifestHash <- putManifest store (manifestFor root)
@@ -2085,7 +2067,7 @@ contentStoreTests = testGroup "Content Store Tests"
   , testCase "Module resolver diagnostics: missing tree term names export and hash" $ do
       let root = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"
           manifest = ModuleManifest []
-            [ ModuleExport "value" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" Nothing ]
+            [ ModuleExport "value" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" ]
           resolver = ObjectResolver
             { resolverAlias = \kind name -> return $ if kind == ModuleAlias && name == "demo"
                 then Just (ObjectRef (unDomain manifestDomain) "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb")

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,7 +8,6 @@ module patterns = lib/patterns.tri
 module io = lib/io.tri
 module socket = lib/socket.tri
 module http = lib/http.tri
-module contracts = lib/contracts.tri
 module intensional = lib/intensionalContracts.tri
 module guarded = lib/guardedBase.tri
 module arboricx.common = lib/arboricx/common.tri