pow, even, odd, min, max

AGENTS.md

@@ -16,6 +16,26 @@ nix build .#
 
 > **Rule of thumb:** if it builds, links, or tests, it goes through `nix`.
 
+### Write and test, don't mentally trace
+
+`nix flake check` finishes quickly. Use it.
+
+tricu's minimalism makes it easy to build a confident-sounding but wrong
+mental model of evaluation order, branch selection (`matchBool` arg order),
+or number encoding. A quick test replaces many minutes of uncertain reasoning.
+
+Prefer:
+
+1. Write a candidate implementation.
+2. Run the tests or a probe.
+3. Fix what's wrong.
+
+Over:
+
+1. Reason about semantics across multiple files.
+2. Build up a chain of inference.
+3. Write code that assumes the chain was correct.
+
 ## Project Overview
 
 **tricu** (pronounced "tree-shoe") is a programming-language experiment written primarily in Haskell.

README.md

@@ -62,19 +62,14 @@ tricu eval --format decode program.tri
 tricu eval --output result.txt program.tri
 ```
 
-Annotated programs run normally under `eval`; annotations are metadata, not
+Unchecked eval parses annotation syntax, discards contract metadata, skips
-runtime types. If you want evaluation to ignore View Contracts completely while
+producer-side View Contract checks during workspace module auto-builds, and does
-loading workspace modules, use unchecked mode:
+not publish unchecked View refs. 
 
 ```sh
 tricu eval --unchecked 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. Executable module exports may still be cached in
-the content store.
-
 Check View Contract annotations explicitly:
 
 ```sh

docs/view-contracts.md

@@ -94,7 +94,37 @@ 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. Guards
+## 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.
 
@@ -123,7 +153,7 @@ 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.
 
-## 5. View Tree Artifact
+## 6. View Tree Artifact
 
 The primary checker-facing artifact is a view executable term graph.
 
@@ -156,7 +186,24 @@ 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.
 
-## 6. Checker Semantics
+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.
 
@@ -184,7 +231,7 @@ or, in self-hosted terms:
 checkViewTree viewTree = ... -- ok checkedExec / err diagnostic
 ```
 
-## 7. Compatibility and Guard Injection
+## 8. Compatibility and Guard Injection
 
 Structural compatibility is about Views. Guard injection is about producing the
 checked-execution tree.
@@ -200,7 +247,7 @@ code that applies `userIdGuard` at the appropriate checked boundary.
 
 The checker, not the runtime metadata system, owns this transformation.
 
-## 8. Source Annotations
+## 9. Source Annotations
 
 Source annotations are one frontend syntax for producing view-tree nodes.
 
@@ -222,7 +269,7 @@ 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.
 
-## 9. Contract Expressions
+## 10. Contract Expressions
 
 Contract-expression helpers remain useful as authoring/building tools, but they
 are not the fundamental artifact model.
@@ -240,7 +287,7 @@ mapBoolStringUse = cFn <|
 These helpers should be understood as convenient ways to build typed/checkable
 structure, not as a permanent replacement for view-tree artifacts.
 
-## 10. Artifact Direction
+## 11. Artifact Direction
 
 The target direction is to make the view tree the canonical checked-program
 artifact.
@@ -264,7 +311,7 @@ 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.
 ```
 
-## 11. IO Interaction Trees
+## 12. IO Interaction Trees
 
 `tricu` IO is represented as ordinary interaction-tree data:
 
@@ -324,7 +371,7 @@ 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.
 
-## 12. Host Independence
+## 13. Host Independence
 
 No part of the core View Tree design is specific to Haskell or to the current implementation.
 

lib/base.tri

@@ -119,6 +119,47 @@ maybeBind m f = matchMaybe nothing f m
 maybeOr default m = matchMaybe default id m
 maybe? = matchMaybe false (_ : true)
 
+-- ---------------------------------------------------------------------------
+-- Lazy eliminators
+--
+-- A strict eliminator evaluates both branches because they are ordinary
+-- arguments. Give a branch that recurses, looks something up, or builds
+-- structure to one of these instead: it becomes a thunk and only the selected
+-- branch is ever applied.
+-- ---------------------------------------------------------------------------
+
+lazyBool = (thenK elseK cond :
+  ((chosen : chosen t)
+   (matchBool
+     thenK
+     elseK
+     cond)))
+
+-- This module has no list matcher, so `triage` is used directly: a cons is a
+-- Fork, which is why the cons case sits in the fork slot, exactly as in
+-- `matchList` in lib/list.tri.
+lazyList = (nilK consK xs :
+  ((chosen : chosen t)
+   (triage
+     nilK
+     _
+     (h r : (_ : consK h r))
+     xs)))
+
+lazyMaybe = (noneK someK m :
+  ((chosen : chosen t)
+   (matchMaybe
+     noneK
+     (x : (_ : someK x))
+     m)))
+
+lazyResult = (errK okK result :
+  ((chosen : chosen t)
+   (matchResult
+     (code rest : (_ : errK code rest))
+     (value rest : (_ : okK value rest))
+     result)))
+
 -- ---------------------------------------------------------------------------
 -- Basic arithmetic
 -- ---------------------------------------------------------------------------
@@ -137,18 +178,15 @@ andLazy? = (a bK :
 
 pred = y (self : triage
   0
-  (_ : 0)
+  0
   (bit rest :
-    matchBool
+    ifLazy
-      (matchBool
+      bit
+      (_ : matchBool
+        (t t rest)
         0
-        (pair 0 rest)
+        rest)
-        (equal? rest 0))
+      (_ : t (t t) (self rest))))
-      (matchBool
-        0
-        (pair 1 (self rest))
-        (equal? rest 0))
-      bit))
 
 isZero? = triage true (_ : false) (_ _ : false)
 
@@ -190,6 +228,42 @@ mul = y (self a b :
     (_ : 0)
     (_ : add a (self a (pred b))))
 
+div = y (self a b :
+  ifLazy
+    (isZero? b)
+    (_ : 0)
+    (_ : ifLazy
+      (lt? a b)
+      (_ : 0)
+      (_ : succ (self (sub a b) b))))
+
+mod = y (self a b :
+  ifLazy
+    (isZero? b)
+    (_ : 0)
+    (_ : ifLazy
+      (lt? a b)
+      (_ : a)
+      (_ : self (sub a b) b)))
+
+pow = y (self a b :
+  ifLazy
+    (isZero? b)
+    (_ : 1)
+    (_ : mul a (self a (pred b))))
+
+even? n = (triage
+  true
+  (_ : false)
+  (bit _ : isZero? bit)
+  n)
+
+odd? = (n : not? (even? n))
+
+min = (a b : ifLazy (lte? a b) (_ : a) (_ : b))
+
+max = (a b : ifLazy (lte? a b) (_ : b) (_ : a))
+
 -- ---------------------------------------------------------------------------
 -- Result combinators
 -- ---------------------------------------------------------------------------

lib/lazy.tri

@@ -1,30 +0,0 @@
-!import "base" !Local
-!import "list" !Local
-
-lazyBool = (thenK elseK cond :
-  ((chosen : chosen t)
-   (matchBool
-     thenK
-     elseK
-     cond)))
-
-lazyList = (nilK consK xs :
-  ((chosen : chosen t)
-   (matchList
-     nilK
-     (h r : (_ : consK h r))
-     xs)))
-
-lazyMaybe = (noneK someK m :
-  ((chosen : chosen t)
-   (matchMaybe
-     noneK
-     (x : (_ : someK x))
-     m)))
-
-lazyResult = (errK okK result :
-  ((chosen : chosen t)
-   (matchResult
-     (code rest : (_ : errK code rest))
-     (value rest : (_ : okK value rest))
-     result)))

lib/list.tri

@@ -232,54 +232,100 @@ contains?_ self needle haystack =
     (startsWith? needle haystack)
 contains? = needle haystack : y contains?_ needle haystack
 
-linesFinish current accRev =
+-- ---------------------------------------------------------------------------
-  reverse (pair (reverse current) accRev)
+-- 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.
+-- ---------------------------------------------------------------------------
 
-lines_ self str accRev current =
+takeWhile_ self xs f =
-  matchList
+  lazyList
-    (linesFinish current accRev)
+    (_ : t)
     (h r :
-      matchBool
+      lazyBool
-        (self r (pair (reverse current) accRev) t)
+        (_ : pair h (self r f))
-        (self r accRev (pair h current))
+        (_ : t)
-        (equal? h 10))
+        (f h))
-    str
+    xs
-lines = str : y lines_ str t t
+takeWhile = f xs : y takeWhile_ xs f
 
-unlines_ self lines =
+dropWhile_ self xs f =
-  matchList
+  lazyList
-    ""
+    (_ : t)
-    (h r : append h (append "\n" (self r)))
-    lines
-unlines = lines : y unlines_ lines
-
-wordsAdd current accRev =
-  matchBool
-    accRev
-    (pair (reverse current) accRev)
-    (emptyList? current)
-
-words_ self str accRev current =
-  matchList
-    (reverse (wordsAdd current accRev))
     (h r :
-      matchBool
+      lazyBool
-        (self r (wordsAdd current accRev) t)
+        (_ : self r f)
-        (self r accRev (pair h current))
+        (_ : pair h r)
-        (equal? h 32))
+        (f h))
-    str
+    xs
-words = str : y words_ str t t
+dropWhile = f xs : y dropWhile_ xs f
 
-unwords_ self words =
+-- Byte-level whitespace only: space and horizontal tab (HTTP OWS).
-  matchList
+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 :
-      matchBool
+      lazyBool
-        h
+        (_ : h)
-        (append h (append " " (self r)))
+        (_ : append h (append sep (self r sep)))
         (emptyList? r))
-    words
+    xs
-unwords = words : y unwords_ words
+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

lib/prelude.tri

@@ -3,5 +3,4 @@
 !import "base"        !Local
 !import "list"        !Local
 !import "bytes"       !Local
-!import "lazy"        !Local
 !import "conversions" !Local

lib/view.tri

@@ -64,6 +64,9 @@ viewTagMaybe = 4
 viewTagPair = 5
 viewTagResult = 6
 viewTagGuarded = 7
+viewTagVar = 8
+viewTagForall = 9
+viewTagExists = 10
 viewFieldArgs = 0
 viewFieldResult = 1
 viewFieldRef = 2
@@ -74,6 +77,9 @@ viewFieldErr = 6
 viewFieldOk = 7
 viewFieldBase = 8
 viewFieldGuard = 9
+viewFieldVar = 10
+viewFieldBinders = 11
+viewFieldBody = 12
 
 -- Evidence tags
 evidenceTagTrusted = 0
@@ -181,6 +187,11 @@ typedNodeFieldView = 1
 typedNodeFieldTerm = 2
 typedNodeFieldCallee = 3
 typedNodeFieldArg = 4
+typedNodeFieldProvenance = 5
+
+viewProvenanceChecked = 0
+viewProvenanceTrusted = 1
+viewProvenanceUnchecked = 2
 
 -- Checked-exec / runtime guard protocol tags. Successful checker results always
 -- carry checked-exec artifacts; unguarded roots are represented as checkedPure.
@@ -227,6 +238,11 @@ viewResult errView okView =
   record viewTagResult [(field viewFieldErr errView) (field viewFieldOk okView)]
 viewGuarded baseView guard =
   record viewTagGuarded [(field viewFieldBase baseView) (field viewFieldGuard guard)]
+viewVar name = record viewTagVar [(field viewFieldVar name)]
+viewForall binders body =
+  record viewTagForall [(field viewFieldBinders binders) (field viewFieldBody body)]
+viewExists binders body =
+  record viewTagExists [(field viewFieldBinders binders) (field viewFieldBody body)]
 
 viewTag = recordTag
 viewPayload = recordFields
@@ -247,8 +263,14 @@ maybeView? = (view : equal? (viewTag view) viewTagMaybe)
 pairView? = (view : equal? (viewTag view) viewTagPair)
 resultView? = (view : equal? (viewTag view) viewTagResult)
 guardedView? = (view : equal? (viewTag view) viewTagGuarded)
+varView? = (view : equal? (viewTag view) viewTagVar)
+forallView? = (view : equal? (viewTag view) viewTagForall)
+existsView? = (view : equal? (viewTag view) viewTagExists)
 guardedViewBase = (view : field0 (viewPayload view))
 guardedViewGuard = (view : field1 (viewPayload view))
+viewVarName = (view : field0 (viewPayload view))
+viewBinderNames = (view : field0 (viewPayload view))
+viewQuantifiedBody = (view : field1 (viewPayload view))
 
 viewFact = (view evidence :
   record viewFactTagKnown
@@ -313,6 +335,13 @@ wellFormedResultView? = (view :
 wellFormedGuardedView? = (view :
   fields2? (viewPayload view) viewFieldBase viewFieldGuard)
 
+-- Tags 8-10 remain reserved so old artifacts decode deterministically, but
+-- quantified/variable Views are no longer accepted by the checker. They
+-- implied abstraction and parametricity that raw Tree Calculus cannot enforce.
+wellFormedVarView? = (_ : false)
+
+wellFormedQuantifiedView? = (_ : false)
+
 wellFormedView_ self view =
   lazyBool
     (_ : wellFormedAnyView? view)
@@ -354,7 +383,23 @@ wellFormedView_ self view =
                                 (_ : self (guardedViewBase view))
                                 (_ : false)
                                 (wellFormedGuardedView? view))
-                            (_ : false)
+                            (_ :
+                              lazyBool
+                                (_ : wellFormedVarView? view)
+                                (_ :
+                                  lazyBool
+                                    (_ :
+                                      lazyBool
+                                        (_ : self (viewQuantifiedBody view))
+                                        (_ : false)
+                                        (wellFormedQuantifiedView? view))
+                                    (_ :
+                                      lazyBool
+                                        (_ : self (viewQuantifiedBody view))
+                                        (_ : false)
+                                        (wellFormedQuantifiedView? view))
+                                    (forallView? view))
+                                (varView? view))
                             (guardedView? view))
                         (and? (resultView? view) (wellFormedResultView? view)))
                     (and? (pairView? view) (wellFormedPairView? view)))
@@ -516,7 +561,6 @@ actualViewFor = (symbol env :
     (_ : viewAny)
     (viewSet : firstKnownView viewSet)
     (lookupViews symbol env))
-
 checkerErr = (tag fields env : err (diagnostic tag fields) env)
 checkerOk = (env : ok env t)
 
@@ -558,7 +602,6 @@ checkApplicationSymbols = (policy argSymbol outSymbol env fnView :
             (missingArgumentOrGuardedBase policy argSymbol argView env))
         (hasView? argSymbol argView env))
     (fnArgs fnView))
-
 -- ---------------------------------------------------------------------------
 -- View-tree checker artifact
 -- ---------------------------------------------------------------------------
@@ -571,6 +614,13 @@ typedProgram = (root nodes :
 typedProgramRoot = (program : field0 (recordFields program))
 typedProgramNodes = (program : field1 (recordFields program))
 
+typedValueWithProvenance = (symbol view term provenance :
+  record typedNodeTagValue
+    [(field typedNodeFieldSymbol symbol)
+     (field typedNodeFieldView view)
+     (field typedNodeFieldTerm term)
+     (field typedNodeFieldProvenance provenance)])
+
 typedValue = (symbol view term :
   record typedNodeTagValue
     [(field typedNodeFieldSymbol symbol)
@@ -584,6 +634,13 @@ typedApply = (symbol callee arg term :
      (field typedNodeFieldArg arg)
      (field typedNodeFieldTerm term)])
 
+typedRequireWithProvenance = (symbol view term provenance :
+  record typedNodeTagRequire
+    [(field typedNodeFieldSymbol symbol)
+     (field typedNodeFieldView view)
+     (field typedNodeFieldTerm term)
+     (field typedNodeFieldProvenance provenance)])
+
 typedRequire = (symbol view term :
   record typedNodeTagRequire
     [(field typedNodeFieldSymbol symbol)
@@ -597,11 +654,23 @@ typedApplyCallee = (node : field1 (recordFields node))
 typedApplyArg = (node : field2 (recordFields node))
 typedApplyTerm = (node : field0 (tail (tail (tail (recordFields node)))))
 
+wellFormedViewProvenance? = (provenance :
+  or?
+    (or? (equal? provenance viewProvenanceChecked) (equal? provenance viewProvenanceTrusted))
+    (equal? provenance viewProvenanceUnchecked))
+
+wellFormedTypedViewFactFields? = (fields :
+  or?
+    (fields3? fields typedNodeFieldSymbol typedNodeFieldView typedNodeFieldTerm)
+    (and?
+      (fields4? fields typedNodeFieldSymbol typedNodeFieldView typedNodeFieldTerm typedNodeFieldProvenance)
+      (wellFormedViewProvenance? (field3 fields))))
+
 wellFormedTypedValue? = (node :
   lazyBool
     (_ : wellFormedView? (typedNodeView node))
     (_ : false)
-    (fields3? (recordFields node) typedNodeFieldSymbol typedNodeFieldView typedNodeFieldTerm))
+    (wellFormedTypedViewFactFields? (recordFields node)))
 
 wellFormedTypedApply? = (node :
   fields3? (recordFields node) typedNodeFieldSymbol typedNodeFieldCallee typedNodeFieldArg)
@@ -619,7 +688,7 @@ wellFormedTypedRequire? = (node :
   lazyBool
     (_ : wellFormedView? (typedNodeView node))
     (_ : false)
-    (fields3? (recordFields node) typedNodeFieldSymbol typedNodeFieldView typedNodeFieldTerm))
+    (wellFormedTypedViewFactFields? (recordFields node)))
 
 wellFormedTypedNode? = (node :
   let tag = recordTag node in
@@ -1111,6 +1180,18 @@ renderViewArgs_ self viewSelf views =
         (emptyList? rest))
     views
 
+renderBinders_ self binders =
+  lazyList
+    (_ : "")
+    (binder rest :
+      lazyBool
+        (_ : binder)
+        (_ : append binder (append ", " (self rest)))
+        (emptyList? rest))
+    binders
+
+renderBinders = (binders : y renderBinders_ binders)
+
 renderView_ self view =
   lazyBool
     (_ : "Bool")
@@ -1162,7 +1243,19 @@ renderView_ self view =
                                             (_ :
                                               lazyBool
                                                 (_ : append "Guarded " (self (guardedViewBase view)))
-                                                (_ : "View")
+                                                (_ :
+                                                  lazyBool
+                                                    (_ : append "$" (showNumber (viewVarName view)))
+                                                    (_ :
+                                                      lazyBool
+                                                        (_ : append "forall [" (append (renderBinders (viewBinderNames view)) (append "] " (self (viewQuantifiedBody view)))) )
+                                                        (_ :
+                                                          lazyBool
+                                                            (_ : append "exists [" (append (renderBinders (viewBinderNames view)) (append "] " (self (viewQuantifiedBody view)))) )
+                                                            (_ : "View")
+                                                            (existsView? view))
+                                                        (forallView? view))
+                                                    (varView? view))
                                                 (guardedView? view))
                                             (fnView? view))
                                         (resultView? view))
@@ -1460,12 +1553,15 @@ viewContractSelfTests = [
   (viewContractProbe (wellFormedView? (viewPair viewBool viewString)))
   (viewContractProbe (wellFormedView? (viewResult viewString viewBool)))
   (viewContractProbe (wellFormedView? (viewGuarded viewString (x : x))))
+  (viewContractProbe (not? (wellFormedView? (viewVar 0))))
+  (viewContractProbe (not? (wellFormedView? (viewForall [(0)] (viewFn [(viewVar 0)] (viewVar 0))))))
   (viewContractProbe (equal? (renderView viewBool) "Bool"))
   (viewContractProbe (equal? (renderView (viewList viewBool)) "List Bool"))
   (viewContractProbe (equal? (renderView (viewMaybe viewString)) "Maybe String"))
   (viewContractProbe (equal? (renderView (viewPair viewBool viewString)) "Pair Bool String"))
   (viewContractProbe (equal? (renderView (viewResult viewString viewBool)) "Result String Bool"))
   (viewContractProbe (equal? (renderView (viewGuarded viewString (x : x))) "Guarded String"))
+  (viewContractProbe (equal? (renderView (viewVar 0)) "$0"))
   (viewContractProbe (equal? (renderView (viewFn [(viewBool) (viewString)] viewUnit)) "Fn [Bool, String] Unit"))
   (viewContractProbe (not? (wellFormedView? 10)))
   (viewContractProbe (not? (wellFormedView? (record viewTagList [(field 99 viewBool)]))))

notes/view-contract-trust-provenance.md

@@ -0,0 +1,95 @@
+# 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/Core.hs

@@ -14,7 +14,9 @@ module Check.Core
 
 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(..))
@@ -27,8 +29,9 @@ import Parser (parseTricu)
 import Research
 
 data ImportedView = ImportedView
-  { importedViewName :: String
+  { importedViewName       :: String
-  , importedViewType :: ViewType
+  , importedViewType       :: ViewType
+  , importedViewProvenance :: ViewProvenance
   } deriving (Show, Eq)
 
 -- Convert module-resolution metadata into checker evidence inputs. The loader
@@ -57,7 +60,7 @@ importedViewsFromResolvedModulesEither loadView modules = concat <$> mapM fromMo
             ++ show (resolvedExportLocalName ex)
             ++ " (kind " ++ showRefKind ref ++ ", hash " ++ showRefHash ref ++ "): "
             ++ err
-          Right view -> pure [ImportedView (resolvedExportLocalName ex) view]
+          Right view -> pure [ImportedView (resolvedExportLocalName ex) view (maybe ViewUnchecked id (resolvedExportProvenance ex))]
 
     showRefKind = T.unpack . objectRefKind
     showRefHash = T.unpack . objectRefHash
@@ -70,6 +73,11 @@ 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
@@ -96,6 +104,30 @@ annotateDiagnostic debugNames message =
           "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
 
@@ -149,18 +181,29 @@ lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
       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..] imports
+        | (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 <- imports
+        | imported <- activeImports
         , Just sym <- [Map.lookup (importedViewName imported) importedSyms]
         ]
       payloads = Map.fromList $
@@ -178,26 +221,27 @@ lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
         , topSyms = tops
         , scopes = []
         , externSyms = importedSyms
-        , knownNodeViews = importKnown
+        , 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))
+    [ (sym, viewTypeToExpr (importedViewType imported), importedViewProvenance imported)
-    | imported <- imports
+    | imported <- activeImports
     , Just sym <- [Map.lookup (importedViewName imported) importedSyms]
     ]
-  let nodes = importNodes ++ localNodes
+  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) -> Either String String
+lowerImportedView :: Map.Map Integer T -> (Integer, ViewExpr, ViewProvenance) -> Either String String
-lowerImportedView payloadsBySym (sym, view) = do
+lowerImportedView payloadsBySym (sym, view, provenance) = do
   viewExpr <- lowerViewExpr view
   let payload = maybe "t" treeSource (Map.lookup sym payloadsBySym)
-  pure $ "typedValue " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload
+  pure $ "typedValueWithProvenance " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload ++ " " ++ viewProvenanceSource provenance
 
 lowerAnnotatedProgram :: [TricuAST] -> LowerM [String]
 lowerAnnotatedProgram defs = do
@@ -207,19 +251,19 @@ lowerAnnotatedProgram defs = do
 
 lowerDefinitionDeclaration :: TricuAST -> LowerM [String]
 lowerDefinitionDeclaration (SDefAnn name args ret _) = do
+  let (_, _, declaredView) = canonicalDefinitionViews args ret
   sym <- symbolForTop name
-  argViews <- mapM lowerArgView args
+  recordKnown sym declaredView
-  retExpr <- liftEither (maybe (Right "viewAny") lowerViewExpr ret)
+  node <- typedValueNode sym declaredView
-  recordKnown sym (declaredDefinitionView args ret)
-  node <- emitDeclaration sym argViews retExpr
   pure [node]
 lowerDefinitionDeclaration _ = liftEither (Left "internal check error: expected annotated definition")
 
 lowerDefinitionFlow :: TricuAST -> LowerM [String]
 lowerDefinitionFlow (SDefAnn _ args ret body) = withDefinitionScope args $ do
-  binderNodes <- concat <$> mapM lowerBinderDeclaration args
+  let (flowArgs, flowRet, _) = canonicalDefinitionViews args ret
-  let phantomViews = map lowerPhantomArgType (phantomArgs args)
+  binderNodes <- concat <$> mapM lowerBinderDeclaration flowArgs
-  (returnArgs, returnResult) <- lowerReturnObligation ret
+  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")
@@ -227,6 +271,9 @@ lowerDefinitionFlow _ = liftEither (Left "internal check error: expected annotat
 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
@@ -249,10 +296,13 @@ emitDeclaration sym views retExpr = do
   pure $ "typedValue " ++ show sym ++ " (viewFn [" ++ unwords (map parens views) ++ "] " ++ parens retExpr ++ ") " ++ payload
 
 typedValueNode :: Integer -> ViewExpr -> LowerM String
-typedValueNode sym view = do
+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 ("typedValue " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload)
+  pure ("typedValueWithProvenance " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload ++ " " ++ viewProvenanceSource provenance)
 
 typedRequireNode :: Integer -> ViewExpr -> LowerM String
 typedRequireNode sym view = do
@@ -260,6 +310,11 @@ typedRequireNode sym view = do
   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
@@ -435,6 +490,14 @@ lowerExprKnownAgainst expr expected = case (expr, viewExprAsType expected) of
   (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)
@@ -509,6 +572,14 @@ lowerExprKnown TLeaf = do
 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)
@@ -553,11 +624,23 @@ lowerListLiteral items = do
 lowerApplicationArgument :: Maybe ViewExpr -> TricuAST -> LowerM (Integer, [String], Maybe ViewExpr)
 lowerApplicationArgument (Just fnView) arg =
   case viewExprFnParts fnView of
-    Just (argView : _, _) -> lowerExprKnownAgainst arg argView
+    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
@@ -672,6 +755,7 @@ 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)
@@ -679,6 +763,8 @@ viewTypeToExpr view = case view of
   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
@@ -688,12 +774,15 @@ 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
@@ -701,6 +790,8 @@ viewExprAsType view = case view of
   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
@@ -711,6 +802,8 @@ lowerViewExpr ty = case ty of
   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
@@ -740,6 +833,8 @@ lowerViewExpr ty = case ty of
     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

src/Check/IO.hs

@@ -32,12 +32,15 @@ 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
@@ -45,11 +48,14 @@ viewExprAsType view = case view of
   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)
@@ -57,6 +63,8 @@ viewTypeToExpr view = case view of
   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
@@ -97,6 +105,7 @@ instrumentIOContinuations asts = mapM transformTop asts
       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
@@ -110,6 +119,7 @@ instrumentIOContinuations asts = mapM transformTop asts
         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 =
@@ -175,6 +185,7 @@ 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
@@ -364,6 +375,7 @@ 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)
@@ -389,6 +401,7 @@ astSource expr = case expr of
   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 ++ ")"

src/ContentStore/ViewContract.hs

@@ -36,6 +36,7 @@ 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)
@@ -43,6 +44,8 @@ encodeViewType = go
     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)
 
@@ -76,12 +79,15 @@ viewTypeToTree view = case view of
   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)
@@ -107,6 +113,9 @@ treeToViewType viewTree = do
     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
@@ -133,6 +142,8 @@ treeToViewType viewTree = do
       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)
@@ -175,6 +186,17 @@ getViewTypeBytes bs = case BS.uncons bs of
       (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
@@ -193,6 +215,19 @@ getMany n bs
       (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
 

src/ContentStore/ViewTree.hs

@@ -4,7 +4,9 @@ module ContentStore.ViewTree
   , encodeViewTree
   , decodeViewTree
   , singletonViewTree
+  , singletonViewTreeWithProvenance
   , viewTreeRootTerm
+  , viewTreeRootViewFact
   , putViewTree
   , getViewTree
   ) where
@@ -13,8 +15,8 @@ import ContentStore.Arboricx (decodeTreeTerm, encodeTreeTerm)
 import ContentStore.Alias (ObjectRef(..))
 import ContentStore.Filesystem (getObject, putObject)
 import ContentStore.Object (Domain(..), StorePath)
-import ContentStore.ViewContract (viewTypeToTree)
+import ContentStore.ViewContract (treeToViewType, viewTypeToTree)
-import Research (T(..), ViewType(..), ofList, ofNumber, toList, toNumber)
+import Research (T(..), ViewProvenance(..), ViewType(..), ofList, ofNumber, toList, toNumber)
 
 import qualified Data.ByteString as BS
 import qualified Data.Text as T
@@ -35,10 +37,13 @@ decodeViewTree :: BS.ByteString -> Either String T
 decodeViewTree = decodeTreeTerm
 
 singletonViewTree :: Maybe ViewType -> T -> T
-singletonViewTree mView term =
+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 mView) term])
+    , 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
@@ -69,19 +74,55 @@ viewTreeRootTerm tree = do
         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 -> T
+typedValueNode :: Integer -> T -> T -> Maybe ViewProvenance -> T
-typedValueNode sym view term =
+typedValueNode sym view term mProvenance =
-  record typedNodeTagValue
+  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 []
@@ -102,6 +143,12 @@ fieldValue expected recordTree = do
     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
@@ -113,11 +160,21 @@ typedProgramTag = 20
 typedProgramFieldRoot = 0
 typedProgramFieldNodes = 1
 
-typedNodeTagValue, typedNodeFieldSymbol, typedNodeFieldView, typedNodeFieldTerm :: Integer
+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

src/Eval.hs

@@ -75,6 +75,7 @@ evalTricu env x = go env (reorderDefs env (map recoverParams x))
 evalASTSync :: Env -> TricuAST -> T
 evalASTSync env term = case term of
   SLambda _ _ -> evalASTSync env (elimLambda term)
+  SLet name val body -> evalASTSync env (SApp (SLambda [name] body) val)
   SVar name Nothing -> case Map.lookup name env of
     Just v -> v
     Nothing -> errorWithoutStackTrace $ "Variable " ++ name ++ " not defined"
@@ -108,6 +109,7 @@ annotatedBinders (DefPhantom _ : rest) = annotatedBinders rest
 elimLambda :: TricuAST -> TricuAST
 elimLambda = go
   where
+    go (SLet name val body) = go (SApp (SLambda [name] body) val)
     go term
       | etaReduction term   = go (etaReduceResult term)
       | triagePattern term  = _TRI
@@ -190,6 +192,8 @@ freeVars (SVar v Nothing) = Set.singleton v
 freeVars (SVar v (Just _)) = Set.singleton v
 freeVars (SApp t u) = Set.union (freeVars t) (freeVars u)
 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 (TStem t) = freeVars t
@@ -297,6 +301,7 @@ findVarNames ast = case ast of
   SVar name _ -> [name]
   SApp a b -> findVarNames a ++ findVarNames b
   SLambda args body -> findVarNames body \\ args
+  SLet name val body -> findVarNames val ++ (findVarNames body \\ [name])
   SDef name args body -> name : (findVarNames body \\ args)
   SDefAnn name args _ body -> name : (findVarNames body \\ annotatedBinders args)
   _ -> []
@@ -317,6 +322,7 @@ toDB env = \case
   SInt n       -> BInt n
   SList xs     -> BList (map (toDB env) xs)
   SEmpty       -> BEmpty
+  SLet name val body -> toDB env (SApp (SLambda [name] body) val)
   SDef{}       -> error "toDB: unexpected SDef at this stage"
   SDefAnn{}    -> error "toDB: unexpected SDefAnn at this stage"
   SImport _ _  -> BEmpty

src/FileEval.hs

@@ -18,7 +18,8 @@ module FileEval
   ) where
 
 import Check.Core
-  ( checkProgramWithEnvAndImportedViews
+  ( ImportedView(..)
+  , checkProgramWithEnvAndImportedViews
   , importedViewsFromResolvedModulesEither
   , lowerViewExpr
   )
@@ -199,21 +200,28 @@ buildWorkspaceModule ctx store moduleName sourcePath = do
         else localNames
   localViewsResult <- localViews
   resolvedLocalViews <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid exported View Contract annotation: ") ++)) pure localViewsResult
-  exports <- mapM (buildExport env resolvedLocalViews) names
+  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 localViews name = case Map.lookup name env of
+    buildExport env viewFacts name = case Map.lookup name env of
       Nothing -> errorWithoutStackTrace $ "Workspace module export not found after evaluation: " ++ name
       Just term -> do
-        let exportView = Map.lookup name localViews
+        let exportFact = Map.lookup name viewFacts
-        rootRef <- putViewTree store (singletonViewTree exportView 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
           , moduleExportAbi = "arboricx.abi.view-tree.v1"
           , moduleExportView = viewRef
+          , moduleExportViewProvenance = exportProvenance
           }
 
 enforceWorkspaceModuleContracts :: StorePath -> String -> Env -> [ResolvedModule] -> [TricuAST] -> IO ()
@@ -288,14 +296,14 @@ defaultStorePath = do
 
 selectedExportsForImport :: Bool -> String -> String -> [TricuAST] -> Maybe (Set.Set T.Text)
 selectedExportsForImport True _ _ _ = Nothing
-selectedExportsForImport False _moduleTarget namespace asts =
+selectedExportsForImport False _moduleTarget importNamespace asts =
   Just $ Set.fromList directSelections
   where
     directSelections = mapMaybe select (Set.toList used)
     used = foldMap freeVars asts
-    prefix = namespace ++ "."
+    prefix = importNamespace ++ "."
     select name
-      | namespace == "!Local" = Just (T.pack name)
+      | importNamespace == "!Local" = Just (T.pack name)
       | prefix `isPrefixOf` name = Just (T.pack (drop (length prefix) name))
       | otherwise = Nothing
 

src/Main.hs

@@ -17,11 +17,13 @@ import FileEval
   )
 import IODriver (IOPermissions(..), runIO)
 import Parser (parseTricu)
-import REPL (repl)
+import REPL (repl, replWithStore)
 import Research (T, EvaluatedForm(..), Env, formatT, exportDag)
 import Wire (encodeBundle, defaultExportNames, Bundle(..))
 
-import Control.Monad (foldM, unless, when)
+import Control.Monad (foldM, forM, unless, when)
+import Data.Char (isAlphaNum)
+import Data.List (sortOn)
 import qualified Data.Text as T
 import Data.Version (showVersion)
 import Paths_tricu (version)
@@ -31,13 +33,18 @@ import qualified Data.ByteString as BS
 import qualified Data.ByteString.Lazy as BL
 import qualified Data.Sequence as Seq
 import qualified Data.Map as Map
-import System.Directory (getHomeDirectory)
+import System.Directory (createDirectoryIfMissing, getHomeDirectory)
 import System.FilePath (takeBaseName, (</>))
 
 -- ---------------------------------------------------------------------------
 -- CLI argument types
 -- ---------------------------------------------------------------------------
 
+data AppArgs = AppArgs
+  { globalStore :: Maybe FilePath
+  , appCommand   :: TricuArgs
+  } deriving (Show)
+
 data TricuArgs
   = Repl
   | Check
@@ -74,6 +81,8 @@ data TricuArgs
       , exportOutput  :: FilePath
       , exportNames   :: [String]
       , exportStore   :: Maybe FilePath
+      , exportAll     :: Bool
+      , exportSplit   :: Bool
       , dag           :: Bool
       }
   | StoreAliasList
@@ -251,6 +260,14 @@ exportParser = ArboricxExport
      <> metavar "PATH"
      <> help "Content-addressed store path"
       ))
+  <*> switch
+      ( long "all"
+     <> help "Export all name aliases that point at tree-term objects"
+      )
+  <*> switch
+      ( long "split"
+     <> help "Write one single-export bundle per export; --output is treated as a directory"
+      )
   <*> switch
       ( long "dag"
      <> help "Export as a topologically-sorted DAG node table instead of a bundle"
@@ -297,9 +314,15 @@ storeAliasGetParser = StoreAliasGet
 versionStr :: String
 versionStr = "tricu " ++ showVersion version
 
-tricuParser :: Parser TricuArgs
+tricuParser :: Parser AppArgs
-tricuParser = (subparser topCommands <|> pure Repl)
+tricuParser = AppArgs
-  <**> infoOption versionStr (long "version" <> help "Show version")
+  <$> optional (option str
+      ( long "store"
+     <> metavar "PATH"
+     <> help "Global content-addressed store path used by commands and the REPL unless a subcommand overrides it"
+      ))
+  <*> ((subparser topCommands <|> pure Repl)
+      <**> infoOption versionStr (long "version" <> help "Show version"))
   where
     topCommands = mconcat
       [ command "check" (info (checkParser <**> helper)
@@ -342,13 +365,15 @@ storeAliasParser = subparser $ mconcat
 
 main :: IO ()
 main = do
-  args <- execParser $ info (tricuParser <**> helper)
+  appArgs <- execParser $ info (tricuParser <**> helper)
     ( fullDesc
    <> progDesc "Exploring Tree Calculus"
    <> header versionStr
     )
+  let mGlobalStore = globalStore appArgs
+      args = applyGlobalStore mGlobalStore (appCommand appArgs)
   case args of
-    Repl               -> runRepl
+    Repl               -> runReplWithStore mGlobalStore
     Check {}           -> runCheck args
     Eval {}            -> runEval args
     ArboricxCompile {} -> runCompile args
@@ -362,11 +387,31 @@ main = do
 -- Command runners
 -- ---------------------------------------------------------------------------
 
+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) }
+  ArboricxExport {} -> args { exportStore = preferLocal (exportStore args) }
+  StoreAliasList {} -> args { storePathOpt = preferLocal (storePathOpt args) }
+  StoreAliasGet {} -> args { storePathOpt = preferLocal (storePathOpt args) }
+  where
+    preferLocal local = case local of
+      Just _  -> local
+      Nothing -> mGlobal
+
 runRepl :: IO ()
-runRepl = do
+runRepl = runReplWithStore Nothing
+
+runReplWithStore :: Maybe FilePath -> IO ()
+runReplWithStore mStore = do
   putStrLn "Welcome to the tricu REPL"
   putStrLn "You may exit with `CTRL+D` or the `!exit` command."
-  repl
+  case mStore of
+    Nothing -> repl
+    Just store -> replWithStore (StorePath store)
 
 runCheck :: TricuArgs -> IO ()
 runCheck opts = do
@@ -444,6 +489,7 @@ runImport opts = do
             (treeTermRef root)
             "arboricx.abi.tree.v1"
             Nothing
+            Nothing
         | (name, root) <- roots
         ]
       moduleName = T.pack $ maybe (takeBaseName file) id (importModule opts)
@@ -465,23 +511,46 @@ runExportBundle opts = do
       modules = exportModules opts
       out     = exportOutput opts
       names   = exportNames opts
+      allFlag = exportAll opts
+      splitFlag = exportSplit opts
   when (null out) $ die "tricu arboricx export: --output is required"
-  when (null targets && null modules) $
+  when (null targets && null modules && not allFlag) $
-    die "tricu arboricx export: at least one --target or --module is required"
+    die "tricu arboricx export: at least one --target, --module, or --all is required"
+  when (splitFlag && not (null names)) $
+    die "tricu arboricx export --split: --name is not supported; split bundles use their export names"
   store <- resolveStorePath (exportStore opts)
+  allEntries <- if allFlag then resolveAllNameExports store else pure []
   targetRoots <- mapM (resolveStoreTarget store) targets
   moduleRoots <- concat <$> mapM (resolveModuleExports store) modules
   let targetEntries = zip (defaultExportNames (length targetRoots)) targetRoots
-      entries = targetEntries ++ moduleRoots
+      entries = allEntries ++ targetEntries ++ moduleRoots
       expNames = if null names then map fst entries else map T.pack names
+  when (null entries) $
+    die "tricu arboricx export: no tree-term exports found"
   when (length expNames /= length entries) $
     die "tricu arboricx export: number of --name values must match number of exported roots"
-  bundle <- packBundleFromStore store (zip expNames (map snd entries))
+  if splitFlag
-  let bundleData = encodeBundle bundle
+    then runExportBundleSplit store out (zip expNames (map snd entries))
-  BL.writeFile out (BL.fromStrict bundleData)
+    else do
-  putStrLn $ "Exported bundle with " ++ show (length entries) ++ " export(s) to " ++ out
+      bundle <- packBundleFromStore store (zip expNames (map snd entries))
-  putStrLn $ "  nodes: " ++ show (Seq.length (bundleNodes bundle))
+      let bundleData = encodeBundle bundle
-  putStrLn $ "  size: " ++ show (BS.length bundleData) ++ " bytes"
+      BL.writeFile out (BL.fromStrict bundleData)
+      putStrLn $ "Exported bundle with " ++ show (length entries) ++ " export(s) to " ++ out
+      putStrLn $ "  nodes: " ++ show (Seq.length (bundleNodes bundle))
+      putStrLn $ "  size: " ++ show (BS.length bundleData) ++ " bytes"
+
+runExportBundleSplit :: StorePath -> FilePath -> [(T.Text, ObjectHash)] -> IO ()
+runExportBundleSplit store outDir entries = do
+  createDirectoryIfMissing True outDir
+  written <- forM (zip [0 :: Int ..] entries) $ \(i, (name, root)) -> do
+    bundle <- packBundleFromStore store [(name, root)]
+    let bundleData = encodeBundle bundle
+        path = outDir </> splitBundleFileName i name
+    BL.writeFile path (BL.fromStrict bundleData)
+    pure (path, Seq.length (bundleNodes bundle), BS.length bundleData)
+  putStrLn $ "Exported " ++ show (length written) ++ " split bundle(s) to " ++ outDir
+  mapM_ (\(path, nodeCount, byteCount) ->
+    putStrLn $ "  " ++ path ++ " (nodes: " ++ show nodeCount ++ ", size: " ++ show byteCount ++ " bytes)") written
 
 runStoreAliasList :: TricuArgs -> IO ()
 runStoreAliasList opts = do
@@ -542,6 +611,19 @@ resolveStoreTarget store target = do
     Just _ -> return root
     Nothing -> die $ "Term not found in store: " ++ target
 
+resolveAllNameExports :: StorePath -> IO [(T.Text, ObjectHash)]
+resolveAllNameExports store = do
+  aliases <- sortOn fst <$> listAliases store NameAlias
+  fmap concat $ mapM exportAlias aliases
+  where
+    exportAlias (name, ref)
+      | objectRefKind ref /= unDomain treeTermDomain = pure []
+      | otherwise = do
+          mTree <- getTreeTerm store (objectRefHash ref)
+          case mTree of
+            Nothing -> die $ "Name alias tree term not found: " ++ T.unpack name
+            Just _  -> pure [(name, objectRefHash ref)]
+
 resolveModuleExports :: StorePath -> String -> IO [(T.Text, ObjectHash)]
 resolveModuleExports store moduleTarget = do
   manifestHash <- resolveModuleManifestHash store moduleTarget
@@ -573,6 +655,17 @@ resolveModuleManifestHash store moduleTarget = do
 formatObjectRef :: ObjectRef -> String
 formatObjectRef ref = T.unpack (objectRefKind ref) ++ " " ++ T.unpack (objectRefHash ref)
 
+splitBundleFileName :: Int -> T.Text -> FilePath
+splitBundleFileName i name = show i ++ "-" ++ sanitize (T.unpack name) ++ ".arboricx"
+  where
+    sanitize [] = "export"
+    sanitize xs = case map safeChar xs of
+      [] -> "export"
+      ys -> ys
+    safeChar c
+      | isAlphaNum c || c == '-' || c == '_' || c == '.' = c
+      | otherwise = '_'
+
 writeOutput :: FilePath -> String -> IO ()
 writeOutput path content
   | null path = putStr content

src/Module/Manifest.hs

@@ -12,6 +12,7 @@ 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)
@@ -37,10 +38,11 @@ data ModuleReference = ModuleReference
 
 -- | Exported executable artifact plus optional direct View Contract type.
 data ModuleExport = ModuleExport
-  { moduleExportName    :: Text
+  { moduleExportName           :: Text
-  , moduleExportObject  :: ObjectRef
+  , moduleExportObject         :: ObjectRef
-  , moduleExportAbi     :: Text
+  , moduleExportAbi            :: Text
-  , moduleExportView    :: Maybe ObjectRef
+  , moduleExportView           :: Maybe ObjectRef
+  , moduleExportViewProvenance :: Maybe ViewProvenance
   } deriving (Eq, Ord, Show)
 
 manifestDomain :: Domain
@@ -66,6 +68,7 @@ encodeManifest manifest = encodeUtf8 $ Text.unlines $
       , esc (moduleExportAbi ex)
       , maybe "-" (esc . objectRefKind) (moduleExportView ex)
       , maybe "-" (esc . objectRefHash) (moduleExportView ex)
+      , maybe "-" encodeProvenance (moduleExportViewProvenance ex)
       ]
 
 -- | Parse the canonical manifest encoding.
@@ -85,12 +88,26 @@ decodeManifest bs = do
           ref <- ModuleReference <$> unesc alias <*> (ObjectRef <$> unesc kind <*> unesc hash)
           Right manifest { moduleManifestReferences = moduleManifestReferences manifest ++ [ref] }
         ["export", name, kind, hash, abi, viewKind, viewHash] -> 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
 
@@ -110,6 +127,18 @@ 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

@@ -28,6 +28,7 @@ data ResolvedExport = ResolvedExport
   , resolvedExportObject     :: ObjectRef
   , resolvedExportAbi        :: T.Text
   , resolvedExportView       :: Maybe ObjectRef
+  , resolvedExportProvenance :: Maybe ViewProvenance
   , resolvedExportTerm       :: T
   } deriving (Show, Eq)
 
@@ -86,6 +87,7 @@ resolveModuleExport resolver namespace ex = do
         , resolvedExportObject = ref
         , resolvedExportAbi = moduleExportAbi ex
         , resolvedExportView = moduleExportView ex
+        , resolvedExportProvenance = moduleExportViewProvenance ex
         , resolvedExportTerm = term
         }
 

src/Parser.hs

@@ -195,8 +195,13 @@ atomicTypeP = do
   t <- tok isTypeName "type name"
   case t of
     LNamespace name -> pure (VEName name)
-    LIdentifier name -> pure (VEName name)
+    LIdentifier name
+      | isViewVarName name -> pure (VEVar name)
+      | otherwise -> pure (VEName name)
     _ -> fail "internal parser error: expected type name"
+  where
+    isViewVarName ('_' : rest) = not (null rest)
+    isViewVarName _ = False
 
 isTypeName :: LToken -> Bool
 isTypeName (LNamespace _) = True
@@ -491,7 +496,7 @@ whereChainP parseBody = do
     Nothing -> pure body
     Just (name, args, value) ->
       let boundValue = foldr (\p acc -> SLambda [p] acc) value args
-      in pure (SApp (SLambda [name] body) boundValue)
+      in pure (SLet name boundValue body)
 
 whereBindingP :: TokParser (String, [String], TricuAST)
 whereBindingP = do
@@ -519,7 +524,7 @@ letP = do
   bodyIndent <- skipNestedNewlinesGetIndent
   body <- exprAtIndentP bodyIndent
   let boundValue = foldr (\p acc -> SLambda [p] acc) value args
-  pure (SApp (SLambda [name] body) boundValue)
+  pure (SLet name boundValue body)
 
 data DoStmt
   = DoBind String TricuAST

src/REPL.hs

@@ -10,7 +10,17 @@ import FileEval
   )
 import Parser (parseTricu)
 import Research (EvaluatedForm(..), Env, formatT)
-import ContentStore (StorePath(..))
+import ContentStore
+  ( AliasKind(..)
+  , ObjectRef(..)
+  , StorePath(..)
+  , cachedFilesystemResolver
+  , getTreeTerm
+  , readAlias
+  , treeTermDomain
+  , unDomain
+  )
+import Module.Resolver (resolveModuleImport, resolvedModulesEnv)
 
 import Control.Exception (SomeException, catch, displayException)
 import Control.Monad.IO.Class (liftIO)
@@ -22,6 +32,7 @@ import System.Console.Haskeline
 import System.Directory (doesFileExist)
 
 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
@@ -35,8 +46,10 @@ data REPLState = REPLState
   }
 
 repl :: IO ()
-repl = do
+repl = defaultStorePath >>= replWithStore
-  store <- defaultStorePath
+
+replWithStore :: StorePath -> IO ()
+replWithStore store = do
   envRef <- newIORef Map.empty
   let settings = Settings
         { complete = completeRepl envRef
@@ -66,6 +79,8 @@ repl = do
             "!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)
@@ -85,6 +100,8 @@ repl = do
       outputStrLn "  !output                - Change output format interactively"
       outputStrLn "  !format FORM           - Set output format: tree, fsl, ast, ternary, ascii, decode, number, string"
       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"
@@ -136,6 +153,49 @@ repl = do
               outputStrLn output
               loop state
 
+    handleUse :: REPLState -> String -> InputT IO ()
+    handleUse state arg = case words arg of
+      [] -> outputStrLn "Usage: !use MODULE [NAMESPACE]" >> loop state
+      [moduleTarget] -> loadModule moduleTarget "!Local"
+      [moduleTarget, namespace] -> loadModule moduleTarget namespace
+      _ -> outputStrLn "Usage: !use MODULE [NAMESPACE]" >> loop state
+      where
+        loadModule moduleTarget namespace = do
+          resolver <- liftIO $ cachedFilesystemResolver (replStore state)
+          resolved <- liftIO $ resolveModuleImport resolver moduleTarget namespace
+          let importedEnv = resolvedModulesEnv [resolved]
+              env' = Map.union importedEnv (replEnv state)
+          liftIO $ writeIORef (replEnvRef state) env'
+          outputStrLn $ "Loaded " ++ show (Map.size importedEnv) ++ " export(s) from store module " ++ moduleTarget
+          loop state { replEnv = env' }
+
+    handleName :: REPLState -> String -> InputT IO ()
+    handleName state arg = case words arg of
+      [] -> outputStrLn "Usage: !name NAME [LOCAL]" >> loop state
+      [name] -> loadName name name
+      [name, localName] -> loadName name localName
+      _ -> outputStrLn "Usage: !name NAME [LOCAL]" >> loop state
+      where
+        loadName name localName = do
+          let store = replStore state
+              nameText = T.pack name
+          mAlias <- liftIO $ readAlias store NameAlias nameText
+          let root = maybe nameText objectRefHash mAlias
+              badKind = case mAlias of
+                Just ref -> objectRefKind ref /= unDomain treeTermDomain
+                Nothing -> False
+          if badKind
+            then outputStrLn ("Name alias does not point at a tree term: " ++ name) >> loop state
+            else do
+              mTerm <- liftIO $ getTreeTerm store root
+              case mTerm of
+                Nothing -> outputStrLn ("Tree term not found in store: " ++ name) >> loop state
+                Just term -> do
+                  let env' = Map.insert localName term (replEnv state)
+                  liftIO $ writeIORef (replEnvRef state) env'
+                  outputStrLn $ "Loaded " ++ name ++ " as " ++ localName
+                  loop state { replEnv = env' }
+
     handleStore :: REPLState -> String -> InputT IO ()
     handleStore state path
       | null path = do
@@ -201,6 +261,8 @@ completeRepl envRef input@(left, _right)
       , "!reset"
       , "!help"
       , "!load"
+      , "!use"
+      , "!name"
       , "!check"
       , "!store"
       , "!unchecked"

src/Research.hs

@@ -25,14 +25,23 @@ data ViewRef
   | 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)
 
@@ -42,14 +51,18 @@ pattern VTRef n = VTRefRaw (ViewRefInt n)
 pattern VTRefText :: String -> ViewType
 pattern VTRefText s = VTRefRaw (ViewRefText s)
 
-{-# COMPLETE VTName, VTRef, VTRefText, VTList, VTMaybe, VTPair, VTResult, VTGuarded, VTFn #-}
+{-# COMPLETE VTName, VTVar, VTRef, VTRefText, VTList, VTMaybe, VTPair, VTResult, VTGuarded, VTForall, VTExists, VTFn #-}
 
 data ViewExpr
   = VEName String
+  | VEVar String
+  | VEVarId Integer
   | VEInt Integer
   | VEString String
   | VEList [ViewExpr]
   | VEApp ViewExpr ViewExpr
+  | VEForall [Integer] ViewExpr
+  | VEExists [Integer] ViewExpr
   | VERaw String
   deriving (Show, Eq, Ord)
 
@@ -71,6 +84,11 @@ data TricuAST
   | TStem TricuAST
   | TFork TricuAST TricuAST
   | SLambda [String] TricuAST
+  -- Non-recursive local binding: `name = boundValue` scoped over `body`.
+  -- Produced by let/where desugaring. `boundValue` already folds any binding
+  -- arguments into nested SLambda. Semantically equal to
+  --   SApp (SLambda [name] body) boundValue
+  | SLet String TricuAST TricuAST
   | SEmpty
   | SImport String String
   deriving (Show, Eq, Ord)

test/Spec.hs

@@ -25,7 +25,7 @@ import System.FilePath       ((</>))
 import Data.Bits              (xor)
 import Data.Char              (digitToInt)
 import Data.List              (find, isInfixOf)
-import Data.Text              (Text, unpack)
+import Data.Text              (Text, unpack, pack)
 import Data.Word              (Word8)
 import Test.Tasty
 import Test.Tasty.HUnit
@@ -77,25 +77,26 @@ allTestLibsEnv = unsafePerformIO $ do
 tests :: TestTree
 tests = testGroup "Tricu Tests"
   [ lexer
-  , parser
+  --, parser
-  , simpleEvaluation
+  --, simpleEvaluation
-  , lambdas
+  --, lambdas
+  , arithmetic
   , providedLibraries
-  , maybeTests
+  --, maybeTests
-  , fileEval
+  --, fileEval
-  , demos
+  --, demos
-  , decoding
+  --, decoding
-  , elimLambdaSingle
+  --, elimLambdaSingle
-  , stressElimLambda
+  --, stressElimLambda
-  , byteMarshallingTests
+  --, byteMarshallingTests
-  , wireTests
+  --, wireTests
-  , tricuReaderTests
+  --, tricuReaderTests
-  , byteListUtilities
+  --, byteListUtilities
-  , binaryParserTests
+  --, binaryParserTests
-  , httpParsingTests
+  --, httpParsingTests
-  , contentStoreTests
+  --, contentStoreTests
-  , viewContractTests
+  --, viewContractTests
-  , ioDriverTests
+  --, ioDriverTests
   ]
 
 lexer :: TestTree
@@ -336,7 +337,7 @@ parser = testGroup "Parser Tests"
 
   , testCase "Parse let expression" $ do
       let input  = "let x = t t in x"
-          expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf)
+          expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing)
       parseSingle input @?= expect
 
   , testCase "Evaluate let expression" $ do
@@ -344,18 +345,36 @@ parser = testGroup "Parser Tests"
 
   , testCase "Parse let function binding" $ do
       let input  = "let f x = x in f t"
-          expect = SApp (SLambda ["f"] (SApp (SVar "f" Nothing) TLeaf))
+          expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing))
-                        (SLambda ["x"] (SVar "x" Nothing))
+                        (SApp (SVar "f" Nothing) TLeaf)
       parseSingle input @?= expect
 
   , testCase "Parse where expression" $ do
       let input  = "x where x = t t"
-          expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf)
+          expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing)
       parseSingle input @?= expect
 
   , testCase "Evaluate where expression" $ do
       tricuTestString "x where x = 1" @?= "Fork (Stem Leaf) Leaf"
 
+  , testCase "Parse where binding with arguments (SLet)" $ do
+      let input  = "f 3 where f x = x"
+          expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing))
+                        (SApp (SVar "f" Nothing) (SInt 3))
+      parseSingle input @?= expect
+
+  , testCase "Evaluate where binding with arguments matches applied lambda" $ do
+      tricuTestString "f (t t) where f x = t x x"
+        @?= tricuTestString "(f : f (t t)) (x : t x x)"
+
+  , testCase "Evaluate nested let bindings" $ do
+      tricuTestString "let a = t t in let b = t in t a b"
+        @?= tricuTestString "t (t t) t"
+
+  , testCase "Inner let binding shadows outer binding" $ do
+      tricuTestString "let x = t in let x = t t in x"
+        @?= tricuTestString "t t"
+
   , testCase "Parse indented multiline definition body" $ do
       let input  = "x =\n  t\n    t"
           expect = SDef "x" [] (SApp TLeaf TLeaf)
@@ -1088,10 +1107,95 @@ providedLibraries = testGroup "Library Tests"
       let input = "unwords []"
           env = evalTricu allTestLibsEnv (parseTricu input)
       result env @?= ofString ""
+
+  , testCase "intercalate joins fields" $ do
+      let input = "intercalate \", \" [(\"a\") (\"b\") (\"c\")]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "a, b, c"
+
+  , testCase "intercalate leaves a lone field alone" $ do
+      let input = "intercalate \", \" [(\"a\")]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "a"
+
+  , testCase "intercalate empty list" $ do
+      let input = "intercalate \", \" []"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString ""
+
+  , testCase "joinSuffix terminates every field" $ do
+      let input = "joinSuffix \"-\" [(\"a\") (\"b\")]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "a-b-"
+
+  , testCase "splitOnByte splits on a byte" $ do
+      let input = "splitOnByte 58 \"a:b:c\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString "a", ofString "b", ofString "c"]
+
+  , testCase "splitOnByte keeps empty fields" $ do
+      let input = "splitOnByte 58 \"a::b\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString "a", ofString "", ofString "b"]
+
+  , testCase "splitOnByte trailing separator leaves an empty field" $ do
+      let input = "splitOnByte 58 \"a:\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString "a", ofString ""]
+
+  , testCase "splitOnByte without a match" $ do
+      let input = "splitOnByte 58 \"abc\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString "abc"]
+
+  , testCase "splitOnByte empty input" $ do
+      let input = "splitOnByte 58 \"\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString ""]
+
+  , testCase "intercalate round trips splitOnByte" $ do
+      let input = "equal? (intercalate \":\" (splitOnByte 58 \"a:b:c\")) \"a:b:c\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "takeWhile keeps the matching prefix" $ do
+      let input = "takeWhile (n : lt? n 3) [(1) (2) (3) (1)]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofNumber 1, ofNumber 2]
+
+  , testCase "takeWhile stops at the first mismatch" $ do
+      let input = "takeWhile (n : lt? n 3) [(3) (1)]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList []
+
+  , testCase "dropWhile drops the matching prefix" $ do
+      let input = "dropWhile (n : lt? n 3) [(1) (2) (3) (1)]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofNumber 3, ofNumber 1]
+
+  , testCase "dropWhile on an all matching list" $ do
+      let input = "dropWhile (n : lt? n 3) [(1) (2)]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList []
+
+  , testCase "trim strips surrounding spaces and tabs" $ do
+      let input = "trim \"  \\ttrimmed  \\t\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "trimmed"
+
+  , testCase "trim leaves interior bytes alone" $ do
+      let input = "trim \" a b \""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "a b"
+
+  , testCase "trim all whitespace is empty" $ do
+      let input = "trim \" \\t \""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString ""
   ]
 
-arithmeticTests :: TestTree
+arithmetic :: TestTree
-arithmeticTests = testGroup "Arithmetic Tests"
+arithmetic = testGroup "Arithmetic Tests"
   [ testCase "isZero? on 0" $ do
       let input = "isZero? 0"
           env = evalTricu allTestLibsEnv (parseTricu input)
@@ -1271,6 +1375,181 @@ arithmeticTests = testGroup "Arithmetic Tests"
       let input = "isZero? (add 0 0)"
           env = evalTricu allTestLibsEnv (parseTricu input)
       result env @?= trueT
+
+  , testCase "div 10 3 = 3" $ do
+      let input = "div 10 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "div 12 4 = 3 (exact)" $ do
+      let input = "div 12 4"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "div 3 5 = 0 (divisor larger)" $ do
+      let input = "div 3 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "div 7 1 = 7 (identity)" $ do
+      let input = "div 7 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 7
+
+  , testCase "div 0 5 = 0" $ do
+      let input = "div 0 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "div 5 0 = 0 (div by zero)" $ do
+      let input = "div 5 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "mod 10 3 = 1" $ do
+      let input = "mod 10 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 1
+
+  , testCase "mod 12 4 = 0 (exact)" $ do
+      let input = "mod 12 4"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "mod 3 5 = 3 (divisor larger)" $ do
+      let input = "mod 3 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "mod 7 1 = 0" $ do
+      let input = "mod 7 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "mod 5 0 = 0 (mod by zero)" $ do
+      let input = "mod 5 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "div mod consistency" $ do
+      let input = "equal? (add (mul 3 7) 4) 25"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "pow 2 0 = 1" $ do
+      let input = "pow 2 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 1
+
+  , testCase "pow 2 3 = 8" $ do
+      let input = "pow 2 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 8
+
+  , testCase "pow 3 2 = 9" $ do
+      let input = "pow 3 2"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 9
+
+  , testCase "pow 0 0 = 1" $ do
+      let input = "pow 0 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 1
+
+  , testCase "pow 0 5 = 0" $ do
+      let input = "pow 0 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "pow 1 10 = 1" $ do
+      let input = "pow 1 10"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 1
+
+  , testCase "pow 5 1 = 5" $ do
+      let input = "pow 5 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 5
+
+  , testCase "min 3 7 = 3" $ do
+      let input = "min 3 7"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "min 7 3 = 3" $ do
+      let input = "min 7 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "min 5 5 = 5" $ do
+      let input = "min 5 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 5
+
+  , testCase "min 0 5 = 0" $ do
+      let input = "min 0 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "max 3 7 = 7" $ do
+      let input = "max 3 7"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 7
+
+  , testCase "max 7 3 = 7" $ do
+      let input = "max 7 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 7
+
+  , testCase "max 5 5 = 5" $ do
+      let input = "max 5 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 5
+
+  , testCase "max 0 5 = 5" $ do
+      let input = "max 0 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 5
+
+  , testCase "even? 0 = true" $ do
+      let input = "even? 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "even? 1 = false" $ do
+      let input = "even? 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= falseT
+
+  , testCase "even? 2 = true" $ do
+      let input = "even? 2"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "even? 7 = false" $ do
+      let input = "even? 7"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= falseT
+
+  , testCase "odd? 0 = false" $ do
+      let input = "odd? 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= falseT
+
+  , testCase "odd? 1 = true" $ do
+      let input = "odd? 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "odd? 2 = false" $ do
+      let input = "odd? 2"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= falseT
+
+  , testCase "odd? 7 = true" $ do
+      let input = "odd? 7"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
   ]
 
 fileEval :: TestTree
@@ -1569,10 +1848,11 @@ contentStoreTests = testGroup "Content Store Tests"
                 (ObjectRef (unDomain treeTermDomain) "222")
                 "arboricx.abi.tree.v1"
                 (Just (ObjectRef viewContractTypeKind "333"))
+                (Just ViewChecked)
             ]
           encoded = encodeManifest manifest
       decodeManifest encoded @?= Right manifest
-      hashObject manifestDomain encoded @?= "7c3cb85454744894a403d2d12c7ece6d391c0cfbeb4bf3adfc7e69ae70ec4f5c"
+      hashObject manifestDomain encoded @?= "1392e0d406d5d1f2e013b0bff27ec3def4f68c045c75780ccb0380a1995f42c7"
 
   , testCase "View Contract type artifacts: encode/decode round trip" $ do
       let view = VTFn [VTList (VTName "String"), VTPair (VTName "Byte") (VTMaybe (VTRef 7))]
@@ -1583,6 +1863,11 @@ contentStoreTests = testGroup "Content Store Tests"
       let view = VTFn [VTRefText "Nat"] (VTPair (VTRefText "Box") (VTName "String"))
       decodeViewType (encodeViewType view) @?= Right view
 
+  , testCase "View Contract type artifacts: encode/decode quantified views" $ do
+      let view = VTForall [0] (VTFn [VTVar 0] (VTVar 0))
+      decodeViewType (encodeViewType view) @?= Right view
+      treeToViewType (viewTypeToTree view) @?= Right view
+
   , testCase "View Contract type artifacts: encode/decode guarded views with opaque guard trees" $ do
       let guardTree = Fork (Stem Leaf) Leaf
           view = VTGuarded (VTRefText "UserId") guardTree
@@ -1615,6 +1900,7 @@ contentStoreTests = testGroup "Content Store Tests"
                   (ObjectRef (unDomain treeTermDomain) root)
                   "arboricx.abi.tree.v1"
                   Nothing
+                  Nothing
               ]
         root <- putTreeTerm store term
         h <- putManifest store (manifestFor root)
@@ -1632,6 +1918,7 @@ contentStoreTests = testGroup "Content Store Tests"
                 (ObjectRef (unDomain treeTermDomain) termH)
                 "arboricx.abi.tree.v1"
                 Nothing
+                Nothing
               ]
           manifestBytes = encodeManifest manifest
           manifestH = hashObject manifestDomain manifestBytes
@@ -1896,6 +2183,7 @@ contentStoreTests = testGroup "Content Store Tests"
                   (ObjectRef (unDomain treeTermDomain) root)
                   "arboricx.abi.tree.v1"
                   Nothing
+                  Nothing
               ]
         root <- putTreeTerm store term
         manifestHash <- putManifest store (manifestFor root)
@@ -1928,7 +2216,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" Nothing Nothing ]
           resolver = ObjectResolver
             { resolverAlias = \kind name -> return $ if kind == ModuleAlias && name == "demo"
                 then Just (ObjectRef (unDomain manifestDomain) "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb")
@@ -2762,7 +3050,7 @@ viewContractTests = testGroup "View Contract Tests"
   , testCase "Portable View Contract self-tests all pass" $ do
       let input = "viewContractSelfTests"
           env = evalTricu allTestLibsEnv (parseTricu input)
-      result env @?= ofList (replicate 32 (ofString "ok"))
+      result env @?= ofList (replicate 35 (ofString "ok"))
 
   , testCase "Structured diagnostic tag reports required-view failures" $ do
       let input = "checkerResultErrorTag (checkTypedProgramWith policyStrict listMapWrongOutputContract)"
@@ -2812,25 +3100,25 @@ viewContractTests = testGroup "View Contract Tests"
       output @?= "symbol 1 (external bar) expected Fn [Bool] Bool but got Any"
 
   , testCase "tricu check accepts trusted imported View Contract facts" $ do
-      let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool"))]
+      let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool")) ViewChecked]
       output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "foo x@Bool =@Bool Ext.id x\n"
       output @?= "ok"
 
   , testCase "tricu check judges imported View Contract facts in checker" $ do
-      let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "String"))]
+      let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "String")) ViewChecked]
       output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "foo x@Bool =@Bool Ext.id x\n"
       output @?= "symbol 3 (Ext.id application result) expected Bool but got String"
 
   , testCase "tricu lower emits imported View Contract facts as view-tree nodes" $ do
-      let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool"))]
+      let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool")) ViewChecked]
       case lowerSourceWithImportedViews imported "foo x@Bool =@Bool Ext.id x\n" of
         Left err -> assertFailure err
-        Right lowered -> lowered @?= "typedProgram 3 [(typedValue 1 (viewFn [(viewBool)] (viewBool)) t) (typedValue 0 (viewFn [(viewBool)] (viewBool)) t) (typedValue 2 (viewBool) t) (typedRequire 2 (viewBool) t) (typedApply 3 1 2 t) (typedRequire 3 (viewBool) t)]"
+        Right lowered -> lowered @?= "typedProgram 3 [(typedValueWithProvenance 1 (viewFn [(viewBool)] (viewBool)) t viewProvenanceChecked) (typedValueWithProvenance 0 (viewFn [(viewBool)] (viewBool)) t viewProvenanceChecked) (typedValueWithProvenance 2 (viewBool) t viewProvenanceChecked) (typedRequire 2 (viewBool) t) (typedApply 3 1 2 t) (typedRequire 3 (viewBool) t)]"
 
   , testCase "tricu lower emits symbolic View Contract refs in view-tree nodes" $ do
       case lowerSource "foo x@(Ref \"UserId\") =@(Ref \"UserId\") x\n" of
         Left err -> assertFailure err
-        Right lowered -> lowered @?= "typedProgram 1 [(typedValue 0 (viewFn [(viewRef \"UserId\")] (viewRef \"UserId\")) t) (typedValue 1 (viewRef \"UserId\") t) (typedRequire 1 (viewRef \"UserId\") t)]"
+        Right lowered -> lowered @?= "typedProgram 1 [(typedValueWithProvenance 0 (viewFn [(viewRef \"UserId\")] (viewRef \"UserId\")) t viewProvenanceChecked) (typedValueWithProvenance 1 (viewRef \"UserId\") t viewProvenanceChecked) (typedRequire 1 (viewRef \"UserId\") t)]"
 
   , testCase "tricu check converts resolved module export views into imported facts" $ do
       let viewRef = ObjectRef viewContractTypeKind "abc123"
@@ -2840,6 +3128,7 @@ viewContractTests = testGroup "View Contract Tests"
             , resolvedExportObject = ObjectRef (unDomain treeTermDomain) "def456"
             , resolvedExportAbi = "arboricx.abi.tree.v1"
             , resolvedExportView = Just viewRef
+            , resolvedExportProvenance = Just ViewChecked
             , resolvedExportTerm = Leaf
             }
           resolvedModule = ResolvedModule "ext" "Ext" "manifest-hash" [resolvedExport]
@@ -2847,10 +3136,28 @@ viewContractTests = testGroup "View Contract Tests"
             then Just (VTFn [VTName "Bool"] (VTName "Bool"))
             else Nothing
       imported <- importedViewsFromResolvedModules loadView [resolvedModule]
-      imported @?= [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool"))]
+      imported @?= [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool")) ViewChecked]
       output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "foo x@Bool =@Bool Ext.id x\n"
       output @?= "ok"
 
+  , testCase "tricu check marks missing import provenance as unchecked" $ do
+      let viewRef = ObjectRef viewContractTypeKind "abc123"
+          resolvedExport = ResolvedExport
+            { resolvedExportSourceName = "id"
+            , resolvedExportLocalName = "Ext.id"
+            , resolvedExportObject = ObjectRef (unDomain treeTermDomain) "def456"
+            , resolvedExportAbi = "arboricx.abi.tree.v1"
+            , resolvedExportView = Just viewRef
+            , resolvedExportProvenance = Nothing
+            , resolvedExportTerm = Leaf
+            }
+          resolvedModule = ResolvedModule "ext" "Ext" "manifest-hash" [resolvedExport]
+          loadView ref = pure $ if ref == viewRef
+            then Just (VTFn [VTName "Bool"] (VTName "Bool"))
+            else Nothing
+      imported <- importedViewsFromResolvedModules loadView [resolvedModule]
+      imported @?= [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool")) ViewUnchecked]
+
   , testCase "tricu check reports missing resolved View Contract artifacts" $ do
       let viewRef = ObjectRef viewContractTypeKind "abc123"
           resolvedExport = ResolvedExport
@@ -2859,6 +3166,7 @@ viewContractTests = testGroup "View Contract Tests"
             , resolvedExportObject = ObjectRef (unDomain treeTermDomain) "def456"
             , resolvedExportAbi = "arboricx.abi.tree.v1"
             , resolvedExportView = Just viewRef
+            , resolvedExportProvenance = Just ViewChecked
             , resolvedExportTerm = Leaf
             }
           resolvedModule = ResolvedModule "ext" "Ext" "manifest-hash" [resolvedExport]
@@ -3018,7 +3326,7 @@ viewContractTests = testGroup "View Contract Tests"
           assertBool "expected String payload requirement" $
             "typedRequire 1 (viewString)" `isInfixOf` lowered
           assertBool "expected Maybe String constructor declaration" $
-            "typedValue 2 (viewMaybe (viewString))" `isInfixOf` lowered
+            "typedValueWithProvenance 2 (viewMaybe (viewString))" `isInfixOf` lowered
 
   , testCase "tricu check lowerSource emits expected Fn argument typed nodes" $ do
       case lowerSource "f x@String =@String x\ny =@String f 1\n" of
@@ -3032,7 +3340,7 @@ viewContractTests = testGroup "View Contract Tests"
         Left err -> assertFailure err
         Right lowered -> do
           assertBool "expected lambda binder declaration" $
-            "typedValue 1 (viewString) t" `isInfixOf` lowered
+            "typedValueWithProvenance 1 (viewString) t viewProvenanceChecked" `isInfixOf` lowered
           assertBool "expected lambda body requirement" $
             "typedRequire 1 (viewString) t" `isInfixOf` lowered
 
@@ -3041,9 +3349,9 @@ viewContractTests = testGroup "View Contract Tests"
         Left err -> assertFailure err
         Right lowered -> do
           assertBool "expected Byte evidence for literal element" $
-            "typedValue 1 (viewByte)" `isInfixOf` lowered
+            "typedValueWithProvenance 1 (viewByte)" `isInfixOf` lowered
           assertBool "expected actual Byte tree payload for literal element" $
-            "typedValue 1 (viewByte) (t (t t) t)" `isInfixOf` lowered
+            "typedValueWithProvenance 1 (viewByte) (t (t t) t) viewProvenanceChecked" `isInfixOf` lowered
           assertBool "expected String requirement for list element" $
             "typedRequire 1 (viewString)" `isInfixOf` lowered
 
@@ -3061,7 +3369,7 @@ viewContractTests = testGroup "View Contract Tests"
         Left err -> assertFailure err
         Right lowered -> do
           assertBool "expected callback lambda declaration" $
-            "typedValue 12 (viewFn [(viewString)] (viewMaybe (viewString))) t" `isInfixOf` lowered
+            "typedValueWithProvenance 12 (viewFn [(viewString)] (viewMaybe (viewString))) t viewProvenanceChecked" `isInfixOf` lowered
           assertBool "expected bind application to declared callback" $
             "typedApply 13 9 12 t" `isInfixOf` lowered
 
@@ -3131,14 +3439,14 @@ viewContractTests = testGroup "View Contract Tests"
 
   , testCase "imported VTGuarded lowers to portable viewGuarded" $ do
       let failGuard = result (evalTricu allTestLibsEnv (parseTricu "(x : guardFail)"))
-          imported = [ImportedView "Ext.id" (VTFn [VTGuarded (VTName "String") failGuard] (VTName "String"))]
+          imported = [ImportedView "Ext.id" (VTFn [VTGuarded (VTName "String") failGuard] (VTName "String")) ViewChecked]
       case lowerSourceWithImportedViews imported "main =@String Ext.id \"x\"\n" of
         Left err -> assertFailure err
         Right lowered -> assertBool "expected imported guarded view to survive lowering" $ "viewGuarded" `isInfixOf` lowered
 
   , testCase "tricu check runs imported guarded argument failure" $ do
       let failGuard = result (evalTricu allTestLibsEnv (parseTricu "(x : guardFail)"))
-          imported = [ImportedView "Ext.id" (VTFn [VTGuarded (VTName "String") failGuard] (VTName "String"))]
+          imported = [ImportedView "Ext.id" (VTFn [VTGuarded (VTName "String") failGuard] (VTName "String")) ViewChecked]
       output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "main =@String Ext.id \"x\"\n"
       output @?= "guard failed at typedRequire symbol 2 for Guarded String"
 
@@ -3234,6 +3542,7 @@ viewContractTests = testGroup "View Contract Tests"
                 Just ex -> do
                   objectRefKind (moduleExportObject ex) @?= viewTreeKind
                   moduleExportAbi ex @?= "arboricx.abi.view-tree.v1"
+                  moduleExportViewProvenance ex @?= Just ViewChecked
                   loadedTree <- getViewTree store (moduleExportObject ex)
                   case moduleExportView ex of
                     Nothing -> assertFailure "expected idUser view ref"
@@ -3245,7 +3554,8 @@ viewContractTests = testGroup "View Contract Tests"
                         Left err -> assertFailure err
                         Right tree -> do
                           rootTerm <- either assertFailure pure (viewTreeRootTerm tree)
-                          tree @?= singletonViewTree (Just expectedView) rootTerm
+                          viewTreeRootViewFact tree @?= Right (Just (expectedView, ViewChecked))
+                          tree @?= singletonViewTreeWithProvenance (Just (expectedView, ViewChecked)) rootTerm
 
   , testCase "Workspace modules reject malformed custom view aliases" $
       withSystemTempDirectory "tricu-workspace-malformed-view-alias" $ \dir -> do
@@ -3266,6 +3576,11 @@ viewContractTests = testGroup "View Contract Tests"
             ]
         readAlias store ModuleAlias "util" >>= (@?= Nothing)
 
+  , testCase "tricu check rejects polymorphic View variables" $ do
+      case lowerSource "idP x@_a =@_a x\n" of
+        Left err -> assertBool "expected unsupported polymorphism diagnostic" $ "polymorphic View variables are unsupported" `isInfixOf` err
+        Right _ -> assertFailure "expected polymorphic View rejection"
+
   , testCase "tricu check catches undersaturated annotated function calls via residual Fn view" $ do
       output <- checkSourceWithEnv allTestLibsEnv "f x@String y@String =@String x\nmain =@String f \"a\"\n"
       output @?= "symbol 5 (f application result) expected String but got Fn [String] String"

tricu.workspace

@@ -3,7 +3,6 @@ module base = lib/base.tri
 module list = lib/list.tri
 module bytes = lib/bytes.tri
 module conversions = lib/conversions.tri
-module lazy = lib/lazy.tri
 module prelude = lib/prelude.tri
 module binary = lib/binary.tri
 module patterns = lib/patterns.tri