commit d0c6aa315f3b10310d5440966361dc1d92dab342
parent e19c70422f54b9a29ccc00d533b02400238637de
Author: James Eversole <james@eversole.co>
Date: Fri, 10 Jul 2026 18:26:38 -0500
Back out the worst of the unsound nonsense
Diffstat:
| M | docs/view-contracts.md | | | 198 | ++++++++++++++------------------------------------------------------------------ |
| M | lib/base.tri | | | 174 | +++---------------------------------------------------------------------------- |
| M | lib/list.tri | | | 148 | ------------------------------------------------------------------------------- |
| M | lib/view.tri | | | 251 | +++++++------------------------------------------------------------------------ |
| M | notes/view-contract-trust-provenance.md | | | 163 | +++++++++++++++++++++++++++++++++---------------------------------------------- |
| M | src/Check.hs | | | 5 | ++--- |
| M | src/Check/Core.hs | | | 161 | +++++++------------------------------------------------------------------------ |
| M | src/FileEval.hs | | | 97 | +++++-------------------------------------------------------------------------- |
| M | test/Spec.hs | | | 252 | +------------------------------------------------------------------------------ |
9 files changed, 152 insertions(+), 1297 deletions(-)
diff --git a/docs/view-contracts.md b/docs/view-contracts.md
@@ -94,108 +94,35 @@ 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. Polymorphic and Abstract Views
+## 4. Soundness Boundary
-View Contracts support portable polymorphism over Views. The View language is
-interpreted by the same portable checker model implemented in `tricu` terms.
+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.
-Source syntax may use underscore-prefixed names as View variables inside
-annotations:
+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.
-```tri
-id x@_a =@_a x
-const x@_a y@_b =@_a x
-compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
-```
-
-In the portable artifact, these lower to scoped View binders rather than
-unscoped source-name conventions. This fits the existing View encoding style:
-Views are tagged records with numeric tags and tagged fields. Polymorphic forms
-are View records such as:
-
-```text
-Var localId
-Forall binders body
-Exists binders body
-```
-
-The current durable encoding uses stable local binder IDs. For example,
-`id x@_a =@_a x` exports a shape equivalent to:
-
-```text
-Forall [0] (Fn [Var 0] (Var 0))
-```
-
-Source names like `_a` are for authoring; the artifact carries binder scope and
-local IDs rather than relying on source-name identity.
-
-`Forall` supports generic contracts:
-
-```tri
-map f@(Fn [_a] _b) xs@(List _a) =@(List _b) ...
-head xs@(NonEmptyList _a) =@_a ...
-```
-
-At each checked use, the checker instantiates quantified variables into
-use-local internal variables and solves View compatibility constraints. The
-portable checker uses structural use-local IDs rather than expensive numeric
-freshening, and treats unconstrained variable-variable matches as constraints
-that do not create substitution cycles. Concrete observations still bind these
-variables when enough information is available. This is what lets explicitly
-annotated higher-order boundaries accept polymorphic values, for example
-`compose id id "x"`, and lets quantified values satisfy concrete requirements
-such as `Fn [String] String`. It gives useful polymorphic contracts for
-explicitly declared/imported View facts.
-
-`Exists` supports checked abstraction boundaries. A module can expose a value as
-"some representation `_repr` plus capabilities over `_repr`":
-
-```text
-Exists _repr.
- Pair
- (Fn [String] _repr) -- constructor
- (Fn [_repr] String) -- renderer / eliminator
-```
-
-This does not make raw Tree Calculus inspection impossible. Unchecked code can
-always inspect trees. It means checked clients cannot justify
-representation-specific operations through the View system unless the package
-exports an appropriate capability or eliminator.
-
-This leads to an important distinction for future checked subsets:
-
-```text
-controlled observation: Bool/List/Maybe/Result/etc. eliminators with Views
-raw observation: direct tree-shape inspection through triage-like power
-```
-
-Useful application code can live mostly in the controlled fragment and receive
-explicit View validation over lambdas, application, let, and typed eliminators.
-Low-level library code may still use raw intensionality, but should expose
-disciplined Views and capabilities above it. Scott-encoded constructors and
-eliminators are a natural tricu-native representation for these APIs.
-
-Tree Calculus terms do not carry intrinsic principal Views, and raw intensional
-code can invalidate parametric claims. View Contracts are an explicit evidence
-and contract layer over tricu programs; limited polymorphic Views are supported
-when they are declared or imported as facts with provenance.
+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 first stdlib annotation island starts with parametric functions that do not
-inspect representation:
-
-```tri
-id x@_a =@_a x
-const x@_a y@_b =@_a x
-compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
-```
+The guarantees retained here are narrower:
-Re-export-only modules preserve imported View metadata, so these contracts flow
-through `prelude` rather than only through direct `base` imports.
+- 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.
-Functions built on raw `t`/`triage` should enter the checked world through
-trusted, controlled eliminator contracts rather than by treating arbitrary raw
-inspection as parametric.
+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
@@ -259,81 +186,22 @@ A node may contain opaque executable fields. Those fields are tree terms, but
they are not recursively decoded as view-tree nodes or Views unless the node's
semantics explicitly says so.
-View facts may also carry explicit per-fact trust provenance:
-
-```text
-Checked -- derived by checked lowering / checker validation
-Trusted -- asserted by a trusted boundary, e.g. a primitive eliminator API
-Unchecked -- raw or assumed; no parametricity/abstraction guarantee
-```
-
-In the portable view-tree envelope this provenance is represented as an optional
-field on `typedValue` / `typedRequire` facts. In module manifests the same
-provenance is carried beside the exported View Contract object reference so that
-imports and re-exports preserve it without relying on module-level convention.
-Absent provenance is interpreted conservatively as `Unchecked` at use sites.
-
-For parametric checked definitions, the frontend now performs a conservative
-raw-intensionality dependency pass over local definitions. If a definition with
-scoped View variables depends directly or indirectly on raw `triage` / raw `t`
-construction, or on an imported `Unchecked` fact, lowering fails and asks the
-author to route observation through a trusted eliminator boundary. This is
-intentionally provenance/dependency based; it is not an attempt to decide
-whether arbitrary Tree Calculus reduction will ever reach rule 3.
-
-View facts can be authored as ordinary value-level Tree Calculus metadata under
-one conventional top-level name:
+View facts may carry per-fact provenance:
```text
-viewFacts = [fact ...]
-fact = pair exportName (pair provenance view)
+Checked
+Trusted
+Unchecked
```
-where `exportName` is a string naming a value exported by the module,
-`provenance` is `0 = Checked`, `1 = Trusted`, or `2 = Unchecked`, and `view` is
-the same portable View record used by `view-tree` artifacts. The host evaluates
-this value and decodes the data schema; it does not infer trust from source
-syntax, AST shape, module name, or a Haskell-side catalog.
+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 initial trusted eliminator facts are authored this way in clearly separated
-stdlib `viewFacts` sections:
-
-```text
-matchBool : forall r. r -> r -> Bool -> r
-matchMaybe : forall a r. r -> (a -> r) -> Maybe a -> r
-matchList : forall a r. r -> (a -> List a -> r) -> List a -> r
-```
-
-The `base` module provides small `facts*` authoring helpers for this advanced
-metadata, e.g. `factsFact`, `factsChecked`, `factsTrusted`, `factsUnchecked`,
-`factsForall`, `factsFn`, `factsVar`, `factsBool`, `factsString`, `factsByte`,
-`factsUnit`, `factsMaybe`, and `factsList`. These helpers construct ordinary
-Tree data; authority comes from the exported `viewFacts` value and its explicit
-provenance tags. Loader validation rejects duplicate fact names and facts for
-names the module does not export.
-
-Initial derived stdlib annotations using this trusted kernel include:
-
-```text
-maybeMap : forall a b. (a -> b) -> Maybe a -> Maybe b
-maybeBind : forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
-maybeOr : forall a. a -> Maybe a -> a
-```
-
-Recursive list combinators are currently published as explicit `Trusted`
-value-level facts rather than `Checked` source annotations, because their bodies
-pass through raw fixed-point machinery that the conservative parametric taint
-pass intentionally does not prove safe. This is the stabilized boundary: raw
-stdlib kernels establish conventions with explicit authority; ordinary checked
-clients consume those facts rather than re-proving the internals.
-
-```text
-headMaybe / lastMaybe / nthMaybe
-append / map / filter / foldl / foldr
-length / reverse / snoc / count / all? / any? / intersect
-take / drop / splitAt / concatMap / find / partition / zipWith
-string/list-byte helpers such as strLength, startsWith?, lines, words
-```
+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
diff --git a/lib/base.tri b/lib/base.tri
@@ -1,8 +1,8 @@
false = t
_ = t
true = t t
-id a@_a =@_a a
-const a@_a b@_b =@_a a
+id a = a
+const a b = a
pair = t
if cond then else = t (t else (t t then)) t cond
@@ -10,7 +10,7 @@ y = ((mut wait fun : wait mut (x : fun (wait mut x)))
(x : x x)
(a0 a1 a2 : t (t a0) (t t a2) a1))
-compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
+compose f g x = f (g x)
triage leaf stem fork = t (t leaf stem) fork
test = triage "Leaf" (_ : "Stem") (_ _ : "Fork")
@@ -114,9 +114,9 @@ matchMaybe nothingCase justCase maybe =
maybe
maybe default f m = matchMaybe default f m
-maybeMap f@(Fn [_a] _b) m@(Maybe _a) =@(Maybe _b) matchMaybe nothing (compose just f) m
-maybeBind m@(Maybe _a) f@(Fn [_a] (Maybe _b)) =@(Maybe _b) matchMaybe nothing f m
-maybeOr default@_a m@(Maybe _a) =@_a matchMaybe default id m
+maybeMap f m = matchMaybe nothing (x : just (f x)) m
+maybeBind m f = matchMaybe nothing f m
+maybeOr default m = matchMaybe default id m
maybe? = matchMaybe false (_ : true)
-- ---------------------------------------------------------------------------
@@ -221,165 +221,3 @@ resultMapErr = (f result :
-- ---------------------------------------------------------------------------
-- View facts
-- ---------------------------------------------------------------------------
-
-factsFact name provenance view = pair name (pair provenance view)
-factsChecked = 0
-factsTrusted = 1
-factsUnchecked = 2
-factsField tag value = pair tag value
-factsRecord tag fields = pair tag fields
-factsVar id = factsRecord 8 [(factsField 10 id)]
-factsForall binders body =
- factsRecord 9 [(factsField 11 binders) (factsField 12 body)]
-factsFn args result =
- factsRecord 1 [(factsField 0 args) (factsField 1 result)]
-factsAny = factsRecord 0 []
-factsRef symbol = factsRecord 2 [(factsField 2 symbol)]
-factsBool = factsRef 0
-factsString = factsRef 1
-factsByte = factsRef 2
-factsUnit = factsRef 3
-factsMaybe elem = factsRecord 4 [(factsField 3 elem)]
-factsList elem = factsRecord 3 [(factsField 3 elem)]
-factsPair left right = factsRecord 5 [(factsField 4 left) (factsField 5 right)]
-factsResult err ok = factsRecord 6 [(factsField 6 err) (factsField 7 ok)]
-
-viewFacts =
- [ (factsFact "pair" factsTrusted
- (factsForall [0]
- (factsFn
- [(factsVar 0) (factsList (factsVar 0))]
- (factsList (factsVar 0)))))
- (factsFact "nothing" factsTrusted
- (factsForall [0]
- (factsMaybe (factsVar 0))))
- (factsFact "just" factsTrusted
- (factsForall [0]
- (factsFn [(factsVar 0)] (factsMaybe (factsVar 0)))))
- (factsFact "false" factsTrusted factsBool)
- (factsFact "true" factsTrusted factsBool)
- (factsFact "if" factsTrusted
- (factsForall [0]
- (factsFn [factsBool (factsVar 0) (factsVar 0)] (factsVar 0))))
- (factsFact "triage" factsTrusted
- (factsForall [0]
- (factsFn [factsAny factsAny factsAny factsAny] (factsVar 0))))
- (factsFact "test" factsTrusted factsString)
- (factsFact "matchBool" factsTrusted
- (factsForall [0]
- (factsFn
- [(factsVar 0) (factsVar 0) factsBool]
- (factsVar 0))))
- (factsFact "lAnd" factsTrusted
- (factsFn [factsBool factsBool] factsBool))
- (factsFact "lOr" factsTrusted
- (factsFn [factsBool factsBool] factsBool))
- (factsFact "matchPair" factsTrusted
- (factsForall [0 1 2]
- (factsFn
- [(factsFn [(factsVar 0) (factsVar 1)] (factsVar 2))
- (factsPair (factsVar 0) (factsVar 1))]
- (factsVar 2))))
- (factsFact "fst" factsTrusted
- (factsForall [0 1]
- (factsFn [(factsPair (factsVar 0) (factsVar 1))] (factsVar 0))))
- (factsFact "snd" factsTrusted
- (factsForall [0 1]
- (factsFn [(factsPair (factsVar 0) (factsVar 1))] (factsVar 1))))
- (factsFact "not?" factsTrusted
- (factsFn [factsBool] factsBool))
- (factsFact "and?" factsTrusted
- (factsFn [factsBool factsBool] factsBool))
- (factsFact "or?" factsTrusted
- (factsFn [factsBool factsBool] factsBool))
- (factsFact "xor?" factsTrusted
- (factsFn [factsBool factsBool] factsBool))
- (factsFact "equal?" factsTrusted
- (factsForall [0]
- (factsFn [(factsVar 0) (factsVar 0)] factsBool)))
- (factsFact "succ" factsTrusted
- (factsFn [factsByte] factsByte))
- (factsFact "pred" factsTrusted
- (factsFn [factsByte] factsByte))
- (factsFact "isZero?" factsTrusted
- (factsFn [factsByte] factsBool))
- (factsFact "add" factsTrusted
- (factsFn [factsByte factsByte] factsByte))
- (factsFact "sub" factsTrusted
- (factsFn [factsByte factsByte] factsByte))
- (factsFact "lte?" factsTrusted
- (factsFn [factsByte factsByte] factsBool))
- (factsFact "gte?" factsTrusted
- (factsFn [factsByte factsByte] factsBool))
- (factsFact "lt?" factsTrusted
- (factsFn [factsByte factsByte] factsBool))
- (factsFact "gt?" factsTrusted
- (factsFn [factsByte factsByte] factsBool))
- (factsFact "mul" factsTrusted
- (factsFn [factsByte factsByte] factsByte))
- (factsFact "matchMaybe" factsTrusted
- (factsForall [0 1]
- (factsFn
- [(factsVar 1)
- (factsFn [(factsVar 0)] (factsVar 1))
- (factsMaybe (factsVar 0))]
- (factsVar 1))))
- (factsFact "maybe" factsTrusted
- (factsForall [0 1]
- (factsFn
- [(factsVar 1)
- (factsFn [(factsVar 0)] (factsVar 1))
- (factsMaybe (factsVar 0))]
- (factsVar 1))))
- (factsFact "maybe?" factsTrusted
- (factsForall [0]
- (factsFn [(factsMaybe (factsVar 0))] factsBool)))
- (factsFact "ifLazy" factsTrusted
- (factsForall [0]
- (factsFn
- [factsBool
- (factsFn [factsUnit] (factsVar 0))
- (factsFn [factsUnit] (factsVar 0))]
- (factsVar 0))))
- (factsFact "andLazy?" factsTrusted
- (factsFn [factsBool (factsFn [factsUnit] factsBool)] factsBool))
- (factsFact "ok" factsTrusted
- (factsForall [0 1]
- (factsFn [(factsVar 1) factsAny] (factsResult (factsVar 0) (factsVar 1)))))
- (factsFact "err" factsTrusted
- (factsForall [0 1]
- (factsFn [(factsVar 0) factsAny] (factsResult (factsVar 0) (factsVar 1)))))
- (factsFact "matchResult" factsTrusted
- (factsForall [0 1 2]
- (factsFn
- [(factsFn [(factsVar 0) factsAny] (factsVar 2))
- (factsFn [(factsVar 1) factsAny] (factsVar 2))
- (factsResult (factsVar 0) (factsVar 1))]
- (factsVar 2))))
- (factsFact "resultIsOk" factsTrusted
- (factsForall [0 1]
- (factsFn [(factsResult (factsVar 0) (factsVar 1))] factsBool)))
- (factsFact "resultIsErr" factsTrusted
- (factsForall [0 1]
- (factsFn [(factsResult (factsVar 0) (factsVar 1))] factsBool)))
- (factsFact "mapResult" factsTrusted
- (factsForall [0 1 2]
- (factsFn
- [(factsFn [(factsVar 1)] (factsVar 2))
- (factsResult (factsVar 0) (factsVar 1))]
- (factsResult (factsVar 0) (factsVar 2)))))
- (factsFact "bindResult" factsTrusted
- (factsForall [0 1 2]
- (factsFn
- [(factsResult (factsVar 0) (factsVar 1))
- (factsFn [(factsVar 1)] (factsResult (factsVar 0) (factsVar 2)))]
- (factsResult (factsVar 0) (factsVar 2)))))
- (factsFact "resultOr" factsTrusted
- (factsForall [0 1]
- (factsFn [(factsVar 1) (factsResult (factsVar 0) (factsVar 1))] (factsVar 1))))
- (factsFact "resultMapErr" factsTrusted
- (factsForall [0 1 2]
- (factsFn
- [(factsFn [(factsVar 0)] (factsVar 2))
- (factsResult (factsVar 0) (factsVar 1))]
- (factsResult (factsVar 2) (factsVar 1)))))]
diff --git a/lib/list.tri b/lib/list.tri
@@ -291,151 +291,3 @@ zipWith_ self f xs ys =
ys)
xs
zipWith = f xs ys : y zipWith_ f xs ys
-
--- ---------------------------------------------------------------------------
--- View facts
---
--- Value-level metadata consumed by View tooling. These facts are ordinary Tree
--- Calculus data, not host-side assumptions and not part of the public stdlib
--- API exported by module manifests.
--- ---------------------------------------------------------------------------
-
-viewFacts =
- [(factsFact "matchList" factsTrusted
- (factsForall [0 1]
- (factsFn
- [(factsVar 1)
- (factsFn
- [(factsVar 0) (factsList (factsVar 0))]
- (factsVar 1))
- (factsList (factsVar 0))]
- (factsVar 1))))
- (factsFact "emptyList?" factsTrusted
- (factsForall [0]
- (factsFn [(factsList (factsVar 0))] factsBool)))
- (factsFact "tail" factsTrusted
- (factsForall [0]
- (factsFn [(factsList (factsVar 0))] (factsList (factsVar 0)))))
- (factsFact "append" factsTrusted
- (factsForall [0]
- (factsFn
- [(factsList (factsVar 0))
- (factsList (factsVar 0))]
- (factsList (factsVar 0)))))
- (factsFact "lExist?" factsTrusted
- (factsForall [0]
- (factsFn [(factsVar 0) (factsList (factsVar 0))] factsBool)))
- (factsFact "map" factsTrusted
- (factsForall [0 1]
- (factsFn
- [(factsFn [(factsVar 0)] (factsVar 1))
- (factsList (factsVar 0))]
- (factsList (factsVar 1)))))
- (factsFact "filter" factsTrusted
- (factsForall [0]
- (factsFn
- [(factsFn [(factsVar 0)] factsBool)
- (factsList (factsVar 0))]
- (factsList (factsVar 0)))))
- (factsFact "foldl" factsTrusted
- (factsForall [0 1]
- (factsFn
- [(factsFn [(factsVar 1) (factsVar 0)] (factsVar 1))
- (factsVar 1)
- (factsList (factsVar 0))]
- (factsVar 1))))
- (factsFact "foldr" factsTrusted
- (factsForall [0 1]
- (factsFn
- [(factsFn [(factsVar 1) (factsVar 0)] (factsVar 1))
- (factsVar 1)
- (factsList (factsVar 0))]
- (factsVar 1))))
- (factsFact "length" factsTrusted
- (factsForall [0]
- (factsFn [(factsList (factsVar 0))] factsByte)))
- (factsFact "reverse" factsTrusted
- (factsForall [0]
- (factsFn [(factsList (factsVar 0))] (factsList (factsVar 0)))))
- (factsFact "snoc" factsTrusted
- (factsForall [0]
- (factsFn [(factsVar 0) (factsList (factsVar 0))] (factsList (factsVar 0)))))
- (factsFact "count" factsTrusted
- (factsForall [0]
- (factsFn [(factsVar 0) (factsList (factsVar 0))] factsByte)))
- (factsFact "all?" factsTrusted
- (factsForall [0]
- (factsFn [(factsFn [(factsVar 0)] factsBool) (factsList (factsVar 0))] factsBool)))
- (factsFact "any?" factsTrusted
- (factsForall [0]
- (factsFn [(factsFn [(factsVar 0)] factsBool) (factsList (factsVar 0))] factsBool)))
- (factsFact "intersect" factsTrusted
- (factsForall [0]
- (factsFn [(factsList (factsVar 0)) (factsList (factsVar 0))] (factsList (factsVar 0)))))
- (factsFact "headMaybe" factsTrusted
- (factsForall [0]
- (factsFn [(factsList (factsVar 0))] (factsMaybe (factsVar 0)))))
- (factsFact "lastMaybe" factsTrusted
- (factsForall [0]
- (factsFn [(factsList (factsVar 0))] (factsMaybe (factsVar 0)))))
- (factsFact "nthMaybe" factsTrusted
- (factsForall [0]
- (factsFn [factsByte (factsList (factsVar 0))] (factsMaybe (factsVar 0)))))
- (factsFact "take" factsTrusted
- (factsForall [0]
- (factsFn [factsByte (factsList (factsVar 0))] (factsList (factsVar 0)))))
- (factsFact "drop" factsTrusted
- (factsForall [0]
- (factsFn [factsByte (factsList (factsVar 0))] (factsList (factsVar 0)))))
- (factsFact "splitAt" factsTrusted
- (factsForall [0]
- (factsFn
- [factsByte (factsList (factsVar 0))]
- (factsPair (factsList (factsVar 0)) (factsList (factsVar 0))))))
- (factsFact "concatMap" factsTrusted
- (factsForall [0 1]
- (factsFn
- [(factsFn [(factsVar 0)] (factsList (factsVar 1)))
- (factsList (factsVar 0))]
- (factsList (factsVar 1)))))
- (factsFact "find" factsTrusted
- (factsForall [0]
- (factsFn
- [(factsFn [(factsVar 0)] factsBool)
- (factsList (factsVar 0))]
- (factsMaybe (factsVar 0)))))
- (factsFact "partition" factsTrusted
- (factsForall [0]
- (factsFn
- [(factsFn [(factsVar 0)] factsBool)
- (factsList (factsVar 0))]
- (factsPair (factsList (factsVar 0)) (factsList (factsVar 0))))))
- (factsFact "strLength" factsTrusted
- (factsFn [factsString] factsByte))
- (factsFact "strAppend" factsTrusted
- (factsFn [factsString factsString] factsString))
- (factsFact "strEq?" factsTrusted
- (factsFn [factsString factsString] factsBool))
- (factsFact "strEmpty?" factsTrusted
- (factsFn [factsString] factsBool))
- (factsFact "startsWith?" factsTrusted
- (factsFn [factsString factsString] factsBool))
- (factsFact "endsWith?" factsTrusted
- (factsFn [factsString factsString] factsBool))
- (factsFact "contains?" factsTrusted
- (factsFn [factsString factsString] factsBool))
- (factsFact "lines" factsTrusted
- (factsFn [factsString] (factsList factsString)))
- (factsFact "unlines" factsTrusted
- (factsFn [(factsList factsString)] factsString))
- (factsFact "words" factsTrusted
- (factsFn [factsString] (factsList factsString)))
- (factsFact "unwords" factsTrusted
- (factsFn [(factsList factsString)] factsString))
- (factsFact "zipWith" factsTrusted
- (factsForall [0 1 2]
- (factsFn
- [(factsFn [(factsVar 0) (factsVar 1)] (factsVar 2))
- (factsList (factsVar 0))
- (factsList (factsVar 1))]
- (factsList (factsVar 2)))))]
diff --git a/lib/view.tri b/lib/view.tri
@@ -335,11 +335,12 @@ wellFormedResultView? = (view :
wellFormedGuardedView? = (view :
fields2? (viewPayload view) viewFieldBase viewFieldGuard)
-wellFormedVarView? = (view :
- fields1? (viewPayload view) viewFieldVar)
+-- 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? = (view :
- fields2? (viewPayload view) viewFieldBinders viewFieldBody)
+wellFormedQuantifiedView? = (_ : false)
wellFormedView_ self view =
lazyBool
@@ -513,28 +514,6 @@ hasView? = (symbol view env :
(viewSet : viewSetHas? view viewSet)
(lookupViews symbol env))
-viewSetHasCompatible_ self namespace expected viewSet =
- lazyList
- (_ : false)
- (fact rest :
- lazyMaybe
- (_ : self namespace expected rest)
- (_ : true)
- (matchView expected (instantiateView namespace (viewFactView fact)) t))
- viewSet
-
-viewSetHasCompatible? = (namespace expected viewSet :
- lazyBool
- (_ : true)
- (_ : y viewSetHasCompatible_ namespace expected viewSet)
- (anyView? expected))
-
-hasCompatibleView? = (symbol view env :
- lazyMaybe
- (_ : anyView? view)
- (viewSet : viewSetHasCompatible? symbol view viewSet)
- (lookupViews symbol env))
-
addViewToSet = (view evidence viewSet :
lazyBool
(_ : viewSet)
@@ -557,44 +536,19 @@ extendEnv_ self symbol view evidence env =
extendEnv = (symbol view evidence env :
y extendEnv_ symbol view evidence env)
-instantiateVarId = (namespace localId :
- pair namespace localId)
-
-instantiateBinders_ self namespace binders subst =
- lazyList
- (_ : subst)
- (binder rest :
- self namespace rest (pair (pair binder (viewVar (instantiateVarId namespace binder))) subst))
- binders
-
-instantiateBinders = (namespace binders subst :
- y instantiateBinders_ namespace binders subst)
-
-instantiateView = (namespace view :
- lazyBool
- (_ : substituteView (instantiateBinders namespace (viewBinderNames view) t) (viewQuantifiedBody view))
- (_ : view)
- (forallView? view))
-
-viewAsFn = (namespace view :
- let instantiated = instantiateView namespace view in
- lazyBool
- (_ : just instantiated)
- (_ : nothing)
- (fnView? instantiated))
-
-findFnView_ self namespace viewSet =
+findFnView_ self viewSet =
lazyList
(_ : nothing)
(fact rest :
- lazyMaybe
+ let view = viewFactView fact in
+ lazyBool
+ (_ : just view)
(_ : self rest)
- (fnView : just fnView)
- (viewAsFn namespace (viewFactView fact)))
+ (fnView? view))
viewSet
-findFnView = (namespace viewSet :
- y findFnView_ namespace viewSet)
+findFnView = (viewSet :
+ y findFnView_ viewSet)
firstKnownView = (viewSet :
lazyList
@@ -607,157 +561,6 @@ actualViewFor = (symbol env :
(_ : viewAny)
(viewSet : firstKnownView viewSet)
(lookupViews symbol env))
-
-substLookup_ self name subst =
- lazyList
- (_ : nothing)
- (entry rest :
- lazyBool
- (_ : just (snd entry))
- (_ : self name rest)
- (equal? name (fst entry)))
- subst
-
-substLookup = (name subst : y substLookup_ name subst)
-
-substBind = (name actual subst :
- lazyBool
- (_ : just subst)
- (_ :
- lazyBool
- (_ : just subst)
- (_ :
- lazyMaybe
- (_ : just (pair (pair name actual) subst))
- (existing :
- lazyBool
- (_ : just subst)
- (_ : nothing)
- (equal? existing actual))
- (substLookup name subst))
- (varView? actual))
- (equal? actual (viewVar name)))
-
-substituteView_ self subst view =
- lazyBool
- (_ :
- lazyMaybe
- (_ : view)
- (bound : self subst bound)
- (substLookup (viewVarName view) subst))
- (_ :
- lazyBool
- (_ : viewFn (y substituteViews_ self subst (fnArgs view)) (self subst (fnResult view)))
- (_ :
- lazyBool
- (_ : viewList (self subst (field0 (viewPayload view))))
- (_ :
- lazyBool
- (_ : viewMaybe (self subst (field0 (viewPayload view))))
- (_ :
- lazyBool
- (_ : viewPair (self subst (field0 (viewPayload view))) (self subst (field1 (viewPayload view))))
- (_ :
- lazyBool
- (_ : viewResult (self subst (field0 (viewPayload view))) (self subst (field1 (viewPayload view))))
- (_ :
- lazyBool
- (_ : viewGuarded (self subst (guardedViewBase view)) (guardedViewGuard view))
- (_ : view)
- (guardedView? view))
- (resultView? view))
- (pairView? view))
- (maybeView? view))
- (listView? view))
- (fnView? view))
- (varView? view)
-
-substituteViews_ self viewSelf subst views =
- lazyList
- (_ : t)
- (view rest : pair (viewSelf subst view) (self viewSelf subst rest))
- views
-
-substituteView = (subst view : y substituteView_ subst view)
-
-matchViewList_ self matchSelf expected actual subst =
- lazyList
- (_ :
- lazyList
- (_ : just subst)
- (_ _ : nothing)
- actual)
- (expectedHead expectedRest :
- lazyList
- (_ : nothing)
- (actualHead actualRest :
- lazyMaybe
- (_ : nothing)
- (nextSubst : self matchSelf expectedRest actualRest nextSubst)
- (matchSelf expectedHead actualHead subst))
- actual)
- expected
-
-matchView_ self expected actual subst =
- lazyBool
- (_ : just subst)
- (_ :
- lazyBool
- (_ : substBind (viewVarName expected) actual subst)
- (_ :
- lazyBool
- (_ : substBind (viewVarName actual) expected subst)
- (_ :
- lazyBool
- (_ : just subst)
- (_ :
- lazyBool
- (_ :
- lazyMaybe
- (_ : nothing)
- (argSubst : self (fnResult expected) (fnResult actual) argSubst)
- (y matchViewList_ self (fnArgs expected) (fnArgs actual) subst))
- (_ :
- lazyBool
- (_ : self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst)
- (_ :
- lazyBool
- (_ : self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst)
- (_ :
- lazyBool
- (_ :
- lazyMaybe
- (_ : nothing)
- (leftSubst : self (field1 (viewPayload expected)) (field1 (viewPayload actual)) leftSubst)
- (self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst))
- (_ :
- lazyBool
- (_ :
- lazyMaybe
- (_ : nothing)
- (errSubst : self (field1 (viewPayload expected)) (field1 (viewPayload actual)) errSubst)
- (self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst))
- (_ :
- lazyBool
- (_ : self (guardedViewBase expected) actual subst)
- (_ :
- lazyBool
- (_ : self expected (guardedViewBase actual) subst)
- (_ : nothing)
- (guardedView? actual))
- (guardedView? expected))
- (and? (resultView? expected) (resultView? actual)))
- (and? (pairView? expected) (pairView? actual)))
- (and? (maybeView? expected) (maybeView? actual)))
- (and? (listView? expected) (listView? actual)))
- (and? (fnView? expected) (fnView? actual)))
- (equal? expected actual))
- (varView? actual))
- (varView? expected))
- (anyView? expected)
-
-matchView = (expected actual subst : y matchView_ expected actual subst)
-
checkerErr = (tag fields env : err (diagnostic tag fields) env)
checkerOk = (env : ok env t)
@@ -789,28 +592,16 @@ checkApplicationSymbols = (policy argSymbol outSymbol env fnView :
lazyList
(_ : checkerErr errorTagZeroArityFunction t env)
(argView restArgs :
- let actualView = instantiateView argSymbol (actualViewFor argSymbol env) in
- lazyMaybe
+ let resultView = fnResidual restArgs (fnResult fnView) in
+ lazyBool
+ (_ : checkerOk (extendEnv outSymbol resultView evidenceTagInferred env))
(_ :
lazyResult
(diag envAtError : err diag envAtError)
- (nextEnv _ : checkerOk (extendEnv outSymbol (fnResidual restArgs (fnResult fnView)) evidenceTagInferred nextEnv))
+ (nextEnv _ : checkerOk (extendEnv outSymbol resultView evidenceTagInferred nextEnv))
(missingArgumentOrGuardedBase policy argSymbol argView env))
- (subst :
- let nextEnv =
- lazyBool
- (_ : extendEnv argSymbol argView evidenceTagRequired env)
- (_ : env)
- (guardedView? argView) in
- checkerOk
- (extendEnv
- outSymbol
- (substituteView subst (fnResidual restArgs (fnResult fnView)))
- evidenceTagInferred
- nextEnv))
- (matchView argView actualView t))
+ (hasView? argSymbol argView env))
(fnArgs fnView))
-
-- ---------------------------------------------------------------------------
-- View-tree checker artifact
-- ---------------------------------------------------------------------------
@@ -964,7 +755,7 @@ checkTypedRequireNode = (policy node env :
(hasView? symbol (guardedViewBase view) env))
(_ : missingRequiredView policy symbol view env)
(guardedView? view))
- (hasCompatibleView? symbol view env))
+ (hasView? symbol view env))
missingArgumentOrGuardedBase = (policy symbol view env :
lazyBool
@@ -983,7 +774,7 @@ checkTypedApplyNode = (policy node env :
lazyMaybe
(_ : checkerOk env)
(fnView : checkApplicationSymbols policy (typedApplyArg node) (typedNodeSymbol node) env fnView)
- (findFnView (typedApplyCallee node) calleeViews))
+ (findFnView calleeViews))
(lookupViews (typedApplyCallee node) env))
checkTypedNode = (policy node env :
@@ -1762,8 +1553,8 @@ viewContractSelfTests = [
(viewContractProbe (wellFormedView? (viewPair viewBool viewString)))
(viewContractProbe (wellFormedView? (viewResult viewString viewBool)))
(viewContractProbe (wellFormedView? (viewGuarded viewString (x : x))))
- (viewContractProbe (wellFormedView? (viewVar 0)))
- (viewContractProbe (wellFormedView? (viewForall [(0)] (viewFn [(viewVar 0)] (viewVar 0)))))
+ (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"))
diff --git a/notes/view-contract-trust-provenance.md b/notes/view-contract-trust-provenance.md
@@ -1,122 +1,95 @@
-# View Contract trust provenance and controlled intensionality
+# View Contracts at the intensionality boundary
-## Problem
+## Conclusion
-Tree Calculus / tricu code can perform raw intensional observation through `t` /
-`triage`-like power. Exact detection of whether an arbitrary term ever reaches
-rule 3 is undecidable: the SK fragment is already Turing-complete, and a program
-can construct/apply an intensional observer iff an encoded machine halts.
+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.
-Therefore View Contracts must not rely on an exact semantic test for "will this
-term inspect representation?".
+## Fundamental conflicts
-## Key correction
+### Raw observation defeats representation independence
-A purely syntactic invariant such as "the initial tree contains no
-`Fork(Fork(_, _), _)`" is not reduction-closed. For example:
+A parametric contract such as:
```text
-Fork (Stem (Fork a b)) c ==> Fork (Fork a b) c
+forall a. a -> a
```
-So absence of a current rule-3 redex is not enough.
+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.
-## Direction
+The same breaks existential abstraction. Advertising a payload as
+`exists repr. ...` changes no operational capability: a client can still
+inspect the representation directly.
-Use explicit provenance/capability discipline, not exact intensionality
-decision.
+### Opaque payloads are asserted, not checked
-View Contract checking and parametric checked-subset validation are distinct:
+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.
-- View Contract checking: verifies executable tree artifacts against declared
- boundary Views.
-- Parametric checked-subset validation: verifies that abstraction/parametricity
- claims do not depend on raw untrusted intensional observation.
+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.
-Unchecked/raw Tree Calculus can always inspect trees. Existential/abstract Views
-are checker-level opacity: checked clients cannot justify representation-specific
-operations unless an exported trusted capability/eliminator provides them.
+### Syntactic taint is not a semantic parametricity proof
-## Provenance model
+Rejecting direct uses of `t` or `triage` is neither complete nor a stable
+soundness boundary:
-Contract facts/artifacts should carry explicit provenance. Do not rely on module
-or catalog convention.
+- 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.
-Recommended durable provenance classes:
+A conservative taint pass can define a programming convention, but it cannot
+justify the parametric or abstraction guarantees previously attached to Views.
-```text
-Checked -- derived by checked lowering / checker validation
-Trusted -- asserted by a trusted boundary, e.g. a primitive eliminator API
-Unchecked -- no abstraction/parametricity guarantee; raw/assumed fact if exposed
-```
-
-The correct granularity is per exported View fact, not per module. A single
-module may contain checked definitions, trusted eliminators, and unchecked raw
-helpers.
-
-## Controlled intensionality
-
-Raw intensionality should be tracked by dependency/provenance, not syntax-only.
+### Flow checking only checks represented flow
-- Direct `triage` / arbitrary `t` eliminator use is raw intensional capability.
-- Trusted eliminators expose controlled observation and do not taint clients.
-- Calling unchecked/untrusted code taints the caller for parametricity purposes.
-- Constructors/literals are not automatically tainting unless they expose raw
- inspection power.
+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.
-Parametric checked mode rejects annotated definitions whose derivation depends
-on raw/untrusted intensionality, while trusted facts may describe raw internals
-behind explicit contracts.
+## Retained contract
-## Trusted eliminator kernel
-
-First trusted observation capabilities should be the smallest useful kernels:
-
-```text
-matchBool : forall r. r -> r -> Bool -> r
-matchMaybe : forall a r. r -> (a -> r) -> Maybe a -> r
-matchList : forall a r. r -> (a -> List a -> r) -> List a -> r
-```
+The reduced checker may soundly claim only:
-Derived functions should be checked against these trusted capabilities where
-possible. Raw recursive kernels and other code
-that passes through fixed-point/intensional machinery should publish explicit
-`Trusted` facts rather than being treated as checked.
-
-Current stdlib shape:
-
-```text
-Checked annotations where the body checks through trusted capabilities:
- maybeMap : forall a b. (a -> b) -> Maybe a -> Maybe b
- maybeBind : forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
- maybeOr : forall a. a -> Maybe a -> a
-
-Trusted value-level facts for raw/recursive stdlib boundaries:
- headMaybe / lastMaybe / nthMaybe
- append / map / filter / foldl / foldr
- length / reverse / snoc / count / all? / any? / intersect
- take / drop / splitAt / concatMap / find / partition / zipWith
- string/list-byte helpers such as strLength, startsWith?, lines, words
-```
-
-Do not assign total contracts to partial APIs such as:
-
-```text
-head : List a -> a
-```
+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.
-Prefer `headMaybe : List a -> Maybe a`, or later introduce `NonEmptyList a`.
+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.
-## Implementation order
+## Code direction
-Most-correct tractable path:
+The initial rollback therefore:
-1. Add contract provenance to the Haskell View model and portable artifacts. ✅
-2. Preserve provenance through module exports/imports/re-exports. ✅
-3. Teach checker environments to distinguish checked vs trusted facts. ✅
-4. Add trusted stdlib eliminator facts. ◐ initial value-level `viewFacts` landed for `matchBool`, `matchMaybe`, `matchList`; Haskell trusted catalog removed
-5. Add parametric-mode dependency/effect checking. ◐ local raw-dependency and unchecked-import rejection landed
-6. Annotate/publish derived stdlib Views at the right provenance. ◐ checked `maybeMap`/`maybeBind`/`maybeOr`; trusted value-level facts for recursive list combinators
+- 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.
-Avoid introducing implicit trusted catalogs before provenance exists; that would
-create semantics that later need to be unwound.
+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.
diff --git a/src/Check.hs b/src/Check.hs
@@ -10,7 +10,7 @@ import Check.Core
import Check.IO
import ContentStore (ObjectRef, StorePath, getViewType)
import Eval (evalTricu)
-import FileEval (LoadedSource(..), defaultStorePath, evaluateFile, evaluateFileWithStore, loadFileWithStore, valueViewFactsFromEnv)
+import FileEval (LoadedSource(..), defaultStorePath, evaluateFile, evaluateFileWithStore, loadFileWithStore)
import Research (Env, ViewType)
import qualified Data.Map as Map
@@ -29,8 +29,7 @@ checkFileWithStore store path = do
let baseEnv = Map.union viewEnv (loadedImports loaded)
checkerEnv = evalTricu baseEnv (loadedAst loaded)
imports <- importedViewsFromResolvedModulesEither (loadImportedView store) (loadedModules loaded)
- valueFacts <- either (errorWithoutStackTrace . ("invalid value-level viewFacts: " ++)) pure (valueViewFactsFromEnv checkerEnv)
- checkProgramWithEnvAndImportedViews checkerEnv (imports ++ valueFacts) (loadedAst loaded)
+ checkProgramWithEnvAndImportedViews checkerEnv imports (loadedAst loaded)
viewCheckerEnv :: Env
viewCheckerEnv = unsafePerformIO (evaluateFile "./lib/view.tri")
diff --git a/src/Check/Core.hs b/src/Check/Core.hs
@@ -12,7 +12,6 @@ module Check.Core
, lowerViewExpr
) where
-import Control.Applicative ((<|>))
import Control.Monad.State.Strict
import Data.Char (isDigit)
import Data.Maybe (mapMaybe)
@@ -74,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
@@ -100,82 +104,6 @@ annotateDiagnostic debugNames message =
"symbol " ++ symText ++ " (" ++ label ++ ") " ++ unwords rest
_ -> message
-viewExprHasParametricBinder :: ViewExpr -> Bool
-viewExprHasParametricBinder expr = case expr of
- VEVar _ -> True
- VEVarId _ -> True
- VEList items -> any viewExprHasParametricBinder items
- VEApp fn arg -> viewExprHasParametricBinder fn || viewExprHasParametricBinder arg
- VEForall binders body -> not (null binders) || viewExprHasParametricBinder body
- VEExists binders body -> not (null binders) || viewExprHasParametricBinder body
- VEName _ -> False
- VEInt _ -> False
- VEString _ -> False
- VERaw _ -> False
-
-rawTaintedDefinitions :: Set.Set String -> [TricuAST] -> Map.Map String String
-rawTaintedDefinitions allowedExternalFacts asts = fixedPoint initiallyRaw
- where
- allowedFacts = allowedExternalFacts
- definitions = Map.fromList
- [ (name, (args, body))
- | ast <- asts
- , Just (name, args, body) <- [definitionBody ast]
- ]
- localNames = Map.keysSet definitions
- initiallyRaw = Map.mapMaybeWithKey
- (\name (args, body) ->
- if name `Set.member` allowedFacts
- then Nothing
- else definitionUnsafeBaseReason localNames allowedFacts (Set.fromList args) body)
- definitions
-
- fixedPoint tainted =
- let tainted' = Map.mapMaybeWithKey (transitiveReason tainted) definitions
- combined = Map.union tainted tainted'
- in if combined == tainted then tainted else fixedPoint combined
-
- transitiveReason tainted name (args, body)
- | name `Map.member` tainted = Nothing
- | name `Set.member` allowedFacts = Nothing
- | otherwise = case filter (`Map.member` tainted) (astFreeRefs (foldr Set.delete localNames args) body) of
- helper : _ -> Just $ "depends on raw-tainted local helper " ++ show helper ++ " (" ++ tainted Map.! helper ++ ")"
- [] -> Nothing
-
- definitionBody ast = case ast of
- SDef name args body -> Just (name, args, body)
- SDefAnn name args _ body -> Just (name, defArgNames args, body)
- _ -> Nothing
-
-definitionUnsafeBaseReason :: Set.Set String -> Set.Set String -> Set.Set String -> TricuAST -> Maybe String
-definitionUnsafeBaseReason localNames allowedExternalFacts bound ast = case ast of
- SVar name _
- | name `Set.member` bound -> Nothing
- | name `Set.member` localNames -> Nothing
- | name `Set.member` allowedExternalFacts -> Nothing
- | name == "triage" -> Just "uses raw triage directly"
- | otherwise -> Just $ "depends on unchecked or unknown external name " ++ show name
- SInt _ -> Nothing
- SStr _ -> Nothing
- SList items -> firstJust (map (definitionUnsafeBaseReason localNames allowedExternalFacts bound) items)
- SDef _ args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body
- SDefAnn _ args _ body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound (defArgNames args)) body
- SApp fn arg -> definitionUnsafeBaseReason localNames allowedExternalFacts bound fn <|> definitionUnsafeBaseReason localNames allowedExternalFacts bound arg
- TLeaf -> Just "uses raw t directly"
- TStem _ -> Just "uses raw t directly"
- TFork _ _ -> Just "uses raw t directly"
- SLambda args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body
- SLet name val body ->
- definitionUnsafeBaseReason localNames allowedExternalFacts bound val
- <|> definitionUnsafeBaseReason localNames allowedExternalFacts (Set.insert name bound) body
- SEmpty -> Nothing
- SImport _ _ -> Nothing
-
-firstJust :: [Maybe a] -> Maybe a
-firstJust [] = Nothing
-firstJust (Just x : _) = Just x
-firstJust (Nothing : xs) = firstJust xs
-
astFreeRefs :: Set.Set String -> TricuAST -> [String]
astFreeRefs candidates ast = case ast of
SVar name _ | name `Set.member` candidates -> [name]
@@ -231,7 +159,6 @@ data LowerState = LowerState
, knownNodeViews :: Map.Map Integer ViewExpr
, nodePayloads :: Map.Map Integer T
, debugNames :: Map.Map Integer String
- , rawTaintedDefs :: Map.Map String String
}
type LowerM a = StateT LowerState (Either String) a
@@ -289,12 +216,6 @@ lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
, Just term <- [Map.lookup name checkerEnvForLowering]
]
annotated = [ def | def@SDefAnn {} <- asts ]
- allowedExternalFacts = Set.fromList
- [ importedViewName imported
- | imported <- imports
- , importedViewProvenance imported `elem` [ViewChecked, ViewTrusted]
- ]
- taintedDefs = rawTaintedDefinitions allowedExternalFacts asts
initialState = LowerState
{ nextSym = fromIntegral (Map.size tops + Map.size importedSyms)
, topSyms = tops
@@ -303,7 +224,6 @@ lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
, knownNodeViews = Map.union trustedLocalKnown importKnown
, nodePayloads = payloads
, debugNames = Map.union topDebug importDebug
- , rawTaintedDefs = taintedDefs
}
(localNodes, finalState) <- runStateT (lowerAnnotatedProgram annotated) initialState
trustedLocalNodes <- mapM (lowerImportedView (nodePayloads finalState)) trustedLocalFacts
@@ -332,14 +252,10 @@ lowerAnnotatedProgram defs = do
lowerDefinitionDeclaration :: TricuAST -> LowerM [String]
lowerDefinitionDeclaration (SDefAnn name args ret _) = do
let (_, _, declaredView) = canonicalDefinitionViews args ret
- tainted <- gets rawTaintedDefs
- if viewExprHasParametricBinder declaredView && name `Map.member` tainted
- then liftEither (Left $ "parametric View definition " ++ show name ++ " depends on raw intensional Tree Calculus machinery (" ++ tainted Map.! name ++ "); use a trusted eliminator boundary instead")
- else do
- sym <- symbolForTop name
- recordKnown sym declaredView
- node <- typedValueNode sym declaredView
- pure [node]
+ sym <- symbolForTop name
+ recordKnown sym declaredView
+ node <- typedValueNode sym declaredView
+ pure [node]
lowerDefinitionDeclaration _ = liftEither (Left "internal check error: expected annotated definition")
lowerDefinitionFlow :: TricuAST -> LowerM [String]
@@ -356,17 +272,7 @@ viewAnyType :: ViewExpr
viewAnyType = VEName "Any"
canonicalDefinitionViews :: [DefArg] -> Maybe ViewExpr -> ([DefArg], Maybe ViewExpr, ViewExpr)
-canonicalDefinitionViews args ret =
- let rawView = declaredDefinitionView args ret
- vars = Set.toList (freeViewVars rawView)
- binderIds = zip vars [0..]
- binderMap = Map.fromList binderIds
- mappedArgs = map (mapDefArgView (rewriteViewVars binderMap)) args
- mappedRet = fmap (rewriteViewVars binderMap) ret
- mappedView = declaredDefinitionView mappedArgs mappedRet
- binders = map snd binderIds
- declaredView = if null vars then mappedView else VEForall binders mappedView
- in (mappedArgs, mappedRet, declaredView)
+canonicalDefinitionViews args ret = (args, ret, declaredDefinitionView args ret)
declaredDefinitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
declaredDefinitionView args ret =
@@ -376,10 +282,6 @@ declaredDefinitionView args ret =
where
resultType = maybe viewAnyType id ret
-mapDefArgView :: (ViewExpr -> ViewExpr) -> DefArg -> DefArg
-mapDefArgView f (DefBinder name mTy) = DefBinder name (fmap f mTy)
-mapDefArgView f (DefPhantom ty) = DefPhantom (f ty)
-
argType :: DefArg -> ViewExpr
argType (DefBinder _ Nothing) = viewAnyType
argType (DefBinder _ (Just ty)) = ty
@@ -900,8 +802,8 @@ lowerViewExpr ty = case ty of
VEName "Byte" -> Right "viewByte"
VEName "Unit" -> Right "viewUnit"
VEName name -> Right name
- VEVar name -> Right $ "viewVar " ++ show name
- VEVarId varId -> Right $ "viewVar " ++ show varId
+ 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
@@ -931,45 +833,10 @@ lowerViewExpr ty = case ty of
f <- lowerViewExpr func
a <- lowerViewExpr arg
Right $ parens f ++ " " ++ parens a
- VEForall binders body -> do
- bodyExpr <- lowerViewExpr body
- Right $ "viewForall " ++ lowerStringList binders ++ " " ++ parens bodyExpr
- VEExists binders body -> do
- bodyExpr <- lowerViewExpr body
- Right $ "viewExists " ++ lowerStringList binders ++ " " ++ parens bodyExpr
+ VEForall _ _ -> Left "quantified View contracts are unsupported"
+ VEExists _ _ -> Left "existential View contracts are unsupported"
VERaw raw -> Right raw
-lowerStringList :: [Integer] -> String
-lowerStringList items = "[" ++ unwords (map (parens . show) items) ++ "]"
-
-quantifyFreeViewVars :: ViewExpr -> ViewExpr
-quantifyFreeViewVars view =
- let vars = Set.toList (freeViewVars view)
- binderIds = zip vars [0..]
- binderMap = Map.fromList binderIds
- body = rewriteViewVars binderMap view
- binders = map snd binderIds
- in if null vars then view else VEForall binders body
-
-rewriteViewVars :: Map.Map String Integer -> ViewExpr -> ViewExpr
-rewriteViewVars binderMap view = case view of
- VEVar name -> maybe (VEVar name) VEVarId (Map.lookup name binderMap)
- VEList items -> VEList (map (rewriteViewVars binderMap) items)
- VEApp f a -> VEApp (rewriteViewVars binderMap f) (rewriteViewVars binderMap a)
- VEForall binders body -> VEForall binders (rewriteViewVars binderMap body)
- VEExists binders body -> VEExists binders (rewriteViewVars binderMap body)
- _ -> view
-
-freeViewVars :: ViewExpr -> Set.Set String
-freeViewVars view = case view of
- VEVar name -> Set.singleton name
- VEVarId _ -> Set.empty
- VEList items -> Set.unions (map freeViewVars items)
- VEApp f a -> Set.union (freeViewVars f) (freeViewVars a)
- VEForall _ body -> freeViewVars body
- VEExists _ body -> freeViewVars body
- _ -> Set.empty
-
treeSource :: T -> String
treeSource Leaf = "t"
treeSource (Stem x) = "(t " ++ treeSource x ++ ")"
diff --git a/src/FileEval.hs b/src/FileEval.hs
@@ -14,7 +14,6 @@ module FileEval
, compileFileWithStore
, loadFileWithStore
, loadFileWithStoreMode
- , valueViewFactsFromEnv
, defaultStorePath
) where
@@ -36,8 +35,6 @@ import Wire (buildBundle, encodeBundle, decodeBundle, verifyBundle, Bundle(..))
import Data.List (partition, isPrefixOf)
import Data.Maybe (mapMaybe)
-import Control.Monad (forM)
-import qualified Data.Set as Set
import System.Directory (getHomeDirectory, getTemporaryDirectory)
import System.FilePath ((</>))
import System.Exit (die)
@@ -204,12 +201,9 @@ buildWorkspaceModule ctx store moduleName sourcePath = do
localViewsResult <- localViews
resolvedLocalViews <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid exported View Contract annotation: ") ++)) pure localViewsResult
importedViews <- importedViewsFromResolvedModulesEither (getViewType store) (loadedModules loaded)
- valueFacts <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid value-level viewFacts: ") ++)) pure (valueViewFactsFromEnv env)
- validateValueViewFactExports moduleName names valueFacts
let localViewFacts = Map.map (\view -> (view, ViewChecked)) resolvedLocalViews
importedViewFacts = Map.fromList [(importedViewName iv, (importedViewType iv, importedViewProvenance iv)) | iv <- importedViews]
- valueViewFacts = Map.fromList [(importedViewName iv, (importedViewType iv, importedViewProvenance iv)) | iv <- valueFacts]
- exportViewFacts = Map.unions [localViewFacts, valueViewFacts, importedViewFacts]
+ 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)
@@ -237,62 +231,12 @@ enforceWorkspaceModuleContracts store moduleName importEnv modules asts
viewEnv <- evaluateFileWithContextWithStoreAndMode IgnoreContracts (Just store) Map.empty "./lib/view.tri"
let checkerEnv = evalTricu (Map.union viewEnv importEnv) asts
imports <- importedViewsFromResolvedModulesEither (getViewType store) modules
- valueFacts <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid value-level viewFacts: ") ++)) pure (valueViewFactsFromEnv checkerEnv)
- resultText <- checkProgramWithEnvAndImportedViews checkerEnv (imports ++ valueFacts) asts
+ resultText <- checkProgramWithEnvAndImportedViews checkerEnv imports asts
case resultText of
"ok" -> pure ()
diagnostic -> errorWithoutStackTrace $
"Workspace module " ++ show moduleName ++ " failed View Contract check: " ++ diagnostic
-valueViewFactsFromEnv :: Env -> Either String [ImportedView]
-valueViewFactsFromEnv env = case Map.lookup "viewFacts" env of
- Nothing -> Right []
- Just factsTree -> do
- facts <- context "viewFacts is not a list" (toList factsTree)
- decoded <- forM (zip [0 :: Int ..] facts) (uncurry decodeFactAt)
- rejectDuplicateFacts decoded
- pure decoded
- where
- decodeFactAt index factTree = do
- (nameTree, rest) <- context prefix (pairParts factTree)
- name <- context (prefix ++ ": export name is not a string") (toString nameTree)
- (provenanceTree, viewTree) <- context (prefixFor name ++ ": payload is not a pair") (pairParts rest)
- provenance <- context (prefixFor name ++ ": invalid provenance") (decodeProvenance provenanceTree)
- view <- context (prefixFor name ++ ": malformed View") (treeToViewType viewTree)
- pure (ImportedView name view provenance)
- where
- prefix = "viewFacts[" ++ show index ++ "]"
- prefixFor name = prefix ++ " for " ++ show name
-
- pairParts (Fork left right) = Right (left, right)
- pairParts _ = Left "expected pair"
-
- decodeProvenance tree = do
- n <- toNumber tree
- case n of
- 0 -> Right ViewChecked
- 1 -> Right ViewTrusted
- 2 -> Right ViewUnchecked
- _ -> Left $ "unknown provenance tag " ++ show n
-
- rejectDuplicateFacts facts = go Set.empty facts
- where
- go _ [] = Right ()
- go seen (fact : rest)
- | importedViewName fact `Set.member` seen = Left $ "duplicate viewFacts entry for " ++ show (importedViewName fact)
- | otherwise = go (Set.insert (importedViewName fact) seen) rest
-
- context label = either (Left . ((label ++ ": ") ++)) Right
-
-validateValueViewFactExports :: String -> [String] -> [ImportedView] -> IO ()
-validateValueViewFactExports moduleName exportedNames facts = do
- let exported = Set.fromList exportedNames
- missing = [importedViewName fact | fact <- facts, importedViewName fact `Set.notMember` exported]
- case missing of
- [] -> pure ()
- name : _ -> errorWithoutStackTrace $
- "Workspace module " ++ show moduleName ++ " has value-level viewFacts for non-exported name " ++ show name
-
isAnnotatedDefinition :: TricuAST -> Bool
isAnnotatedDefinition SDefAnn {} = True
isAnnotatedDefinition _ = False
@@ -300,13 +244,10 @@ isAnnotatedDefinition _ = False
topLevelDefinitions :: [TricuAST] -> [String]
topLevelDefinitions = mapMaybe go
where
- go (SDef name _ _) | not (isViewFactMetadataName name) = Just name
- go (SDefAnn name _ _ _) | not (isViewFactMetadataName name) = Just name
+ go (SDef name _ _) = Just name
+ go (SDefAnn name _ _ _) = Just name
go _ = Nothing
-isViewFactMetadataName :: String -> Bool
-isViewFactMetadataName name = name == "viewFacts"
-
topLevelDefinitionViews :: [TricuAST] -> Map.Map String ViewExpr
topLevelDefinitionViews asts = Map.fromList (mapMaybe go asts)
where
@@ -328,7 +269,7 @@ resolveViewExpression checkerEnv view = do
Left err -> Left $ "could not validate view expression " ++ show expr ++ ": " ++ err
definitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
-definitionView args resultView = quantifyFreeViewVars $
+definitionView args resultView =
case argViews of
[] -> finalView
_ -> VEApp (VEApp (VEName "Fn") (VEList argViews)) finalView
@@ -336,34 +277,6 @@ definitionView args resultView = quantifyFreeViewVars $
argViews = map defArgView args
finalView = maybe exportedViewAny id resultView
-quantifyFreeViewVars :: ViewExpr -> ViewExpr
-quantifyFreeViewVars view =
- let vars = Set.toList (freeViewVars view)
- binderIds = zip vars [0..]
- binderMap = Map.fromList binderIds
- body = rewriteViewVars binderMap view
- binders = map snd binderIds
- in if null vars then view else VEForall binders body
-
-rewriteViewVars :: Map.Map String Integer -> ViewExpr -> ViewExpr
-rewriteViewVars binderMap view = case view of
- VEVar name -> maybe (VEVar name) VEVarId (Map.lookup name binderMap)
- VEList items -> VEList (map (rewriteViewVars binderMap) items)
- VEApp f a -> VEApp (rewriteViewVars binderMap f) (rewriteViewVars binderMap a)
- VEForall binders body -> VEForall binders (rewriteViewVars binderMap body)
- VEExists binders body -> VEExists binders (rewriteViewVars binderMap body)
- _ -> view
-
-freeViewVars :: ViewExpr -> Set.Set String
-freeViewVars view = case view of
- VEVar name -> Set.singleton name
- VEVarId _ -> Set.empty
- VEList items -> Set.unions (map freeViewVars items)
- VEApp f a -> Set.union (freeViewVars f) (freeViewVars a)
- VEForall _ body -> freeViewVars body
- VEExists _ body -> freeViewVars body
- _ -> Set.empty
-
defArgView :: DefArg -> ViewExpr
defArgView (DefBinder _ Nothing) = exportedViewAny
defArgView (DefBinder _ (Just ty)) = ty
diff --git a/test/Spec.hs b/test/Spec.hs
@@ -3234,30 +3234,6 @@ viewContractTests = testGroup "View Contract Tests"
view <- getViewType store viewRef
view @?= Right (VTFn [VTRef 10] (VTRef 10))
- , testCase "Workspace modules publish explicitly quantified polymorphic views" $
- withSystemTempDirectory "tricu-workspace-polymorphic-view" $ \dir -> do
- let store = StorePath (dir </> "store")
- utilPath = dir </> "util.tri"
- mainPath = dir </> "main.tri"
- writeFile (dir </> "tricu.workspace") "module util = util.tri\n"
- writeFile utilPath "idP x@_a =@_a x\n"
- writeFile mainPath "!import \"util\" Util\n\nmain =@String Util.idP \"hi\"\n"
- _ <- evaluateFileWithStore (Just store) mainPath
- mAlias <- readAlias store ModuleAlias "util"
- case mAlias of
- Nothing -> assertFailure "expected util module alias"
- Just ref -> do
- mManifest <- getManifest store (objectRefHash ref)
- case mManifest of
- Nothing -> assertFailure "expected util module manifest"
- Just manifest -> case find ((== "idP") . unpack . moduleExportName) (moduleManifestExports manifest) of
- Nothing -> assertFailure "expected idP export"
- Just ex -> case moduleExportView ex of
- Nothing -> assertFailure "expected idP view ref"
- Just viewRef -> do
- view <- getViewType store viewRef
- view @?= Right (VTForall [0] (VTFn [VTVar 0] (VTVar 0)))
-
, testCase "Workspace modules publish string custom view aliases" $
withSystemTempDirectory "tricu-workspace-string-view-alias" $ \dir -> do
let store = StorePath (dir </> "store")
@@ -3339,232 +3315,10 @@ viewContractTests = testGroup "View Contract Tests"
]
readAlias store ModuleAlias "util" >>= (@?= Nothing)
- , testCase "tricu check lowers free View variables under explicit Forall" $ do
+ , testCase "tricu check rejects polymorphic View variables" $ do
case lowerSource "idP x@_a =@_a x\n" of
- Left err -> assertFailure err
- Right lowered -> do
- assertBool "expected polymorphic declaration to be explicitly quantified" $ "viewForall [(0)]" `isInfixOf` lowered
- assertBool "expected quantified identity function body" $ "viewFn [(viewVar 0)] (viewVar 0)" `isInfixOf` lowered
-
- , testCase "tricu check supports first-order polymorphic identity View variables" $ do
- output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\nmain =@String idP \"hi\"\n"
- output @?= "ok"
-
- , testCase "tricu check propagates first-order polymorphic result relationships" $ do
- output <- checkSourceWithEnv allTestLibsEnv "constP x@_a y@_b =@_a x\nmain =@String constP \"hi\" 1\n"
- output @?= "ok"
-
- , testCase "tricu check instantiates quantified Views at higher-order boundaries" $ do
- output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\ncomposeP f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)\nmain =@String composeP idP idP \"hi\"\n"
- output @?= "ok"
-
- , testCase "tricu check matches quantified values against concrete Fn requirements" $ do
- output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\nacceptSS f@(Fn [String] String) =@String f \"hi\"\nmain =@String acceptSS idP\n"
- output @?= "ok"
-
- , testCase "tricu check propagates nested polymorphic List relationships" $ do
- output <- checkSourceWithEnv allTestLibsEnv "idList xs@(List _a) =@(List _a) xs\nmain =@(List String) idList [(\"hi\")]\n"
- output @?= "ok"
-
- , testCase "tricu check keeps polymorphic instantiation acyclic for reciprocal higher-order constraints" $ do
- output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\nrel f@(Fn [_a] _b) g@(Fn [_b] _a) =@String \"ok\"\nmain =@String rel idP idP\n"
- output @?= "ok"
-
- , testCase "tricu check supports first-principles parametric stdlib island shapes" $ do
- output <- checkSourceWithEnv allTestLibsEnv "idV x@_a =@_a x\nconstV x@_a y@_b =@_a x\ncomposeV f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)\nmain =@String composeV idV (constV \"hi\") 1\n"
- output @?= "ok"
-
- , testCase "tricu check rejects raw triage in parametric annotated definitions" $ do
- output <- checkSourceWithEnv allTestLibsEnv "bad x@_a =@String triage \"leaf\" (_ : \"stem\") (_ _ : \"fork\") x\n"
- output `containsAll` ["parametric View definition \"bad\"", "uses raw triage directly", "trusted eliminator boundary"]
-
- , testCase "tricu check rejects raw t in parametric annotated definitions" $ do
- output <- checkSourceWithEnv allTestLibsEnv "bad x@_a =@_a t\n"
- output `containsAll` ["parametric View definition \"bad\"", "uses raw t directly", "trusted eliminator boundary"]
-
- , testCase "tricu check rejects parametric definitions depending on local raw helpers" $ do
- output <- checkSourceWithEnv allTestLibsEnv "raw x = triage \"leaf\" (_ : \"stem\") (_ _ : \"fork\") x\nbad x@_a =@String raw x\n"
- output `containsAll` ["parametric View definition \"bad\"", "raw-tainted local helper \"raw\"", "uses raw triage directly"]
-
- , testCase "tricu check rejects parametric definitions depending on unchecked imported facts" $ do
- let imported = [ImportedView "Ext.raw" (VTFn [VTVar 0] (VTName "String")) ViewUnchecked]
- output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "bad x@_a =@String Ext.raw x\n"
- output `containsAll` ["parametric View definition \"bad\"", "unchecked or unknown external name \"Ext.raw\""]
-
- , testCase "tricu check accepts parametric code through value-level trusted stdlib facts" $ do
- facts <- either assertFailure pure (valueViewFactsFromEnv allTestLibsEnv)
- let source = "idP x@_a =@_a x\nmaybeOrV default@_a m@(Maybe _a) =@_a matchMaybe default idP m\n"
- output <- checkSourceWithEnvAndImportedViews allTestLibsEnv facts source
- output @?= "ok"
-
- , testCase "unused value-level trusted facts do not perturb root selection" $ do
- facts <- either assertFailure pure (valueViewFactsFromEnv allTestLibsEnv)
- output <- checkSourceWithEnvAndImportedViews allTestLibsEnv facts "idP x@_a =@_a x\n"
- output @?= "ok"
-
- , testCase "value-level trusted stdlib facts lower with Trusted provenance" $ do
- facts <- either assertFailure pure (valueViewFactsFromEnv allTestLibsEnv)
- case lowerSourceWithImportedViews facts "notV x@Bool =@Bool matchBool false true x\n" of
- Left err -> assertFailure err
- Right lowered -> assertBool "expected trusted provenance in lowered view tree" $ "typedValueWithProvenance" `isInfixOf` lowered && "viewProvenanceTrusted" `isInfixOf` lowered
-
- , testCase "tricu check uses annotated id const compose through re-export modules" $
- withSystemTempDirectory "tricu-stdlib-prelude-views" $ \dir -> do
- let store = StorePath (dir </> "store")
- basePath = dir </> "mybase.tri"
- preludePath = dir </> "myprelude.tri"
- mainPath = dir </> "main.tri"
- writeFile (dir </> "tricu.workspace") "module mybase = mybase.tri\nmodule myprelude = myprelude.tri\n"
- writeFile basePath "id a@_a =@_a a\nconst a@_a b@_b =@_a a\ncompose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)\n"
- writeFile preludePath "!import \"mybase\" !Local\n"
- writeFile mainPath "!import \"myprelude\" !Local\nmain =@String compose id (const \"hi\") 1\n"
- output <- checkFileWithStore store mainPath
- output @?= "ok"
-
- , testCase "Workspace value-level viewFacts export and re-export Trusted provenance" $
- withSystemTempDirectory "tricu-workspace-value-view-facts" $ \dir -> do
- let store = StorePath (dir </> "store")
- depPath = dir </> "dep.tri"
- shimPath = dir </> "shim.tri"
- mainPath = dir </> "main.tri"
- factBlock = unlines
- [ "factsPair = t"
- , "factsFact name provenance view = factsPair name (factsPair provenance view)"
- , "factsTrusted = 1"
- , "factsField tag value = factsPair tag value"
- , "factsRecord tag fields = factsPair tag fields"
- , "factsVar id = factsRecord 8 [(factsField 10 id)]"
- , "factsForall binders body = factsRecord 9 [(factsField 11 binders) (factsField 12 body)]"
- , "factsFn args result = factsRecord 1 [(factsField 0 args) (factsField 1 result)]"
- , "viewFacts = [(factsFact \"rawId\" factsTrusted (factsForall [0] (factsFn [(factsVar 0)] (factsVar 0))))]"
- ]
- expected = VTForall [0] (VTFn [VTVar 0] (VTVar 0))
- writeFile (dir </> "tricu.workspace") "module dep = dep.tri\nmodule shim = shim.tri\n"
- writeFile depPath ("rawId x = x\n" ++ factBlock)
- writeFile shimPath "!import \"dep\" !Local\n"
- writeFile mainPath "!import \"shim\" Shim\nmain x@_a =@_a Shim.rawId x\n"
- output <- checkFileWithStore store mainPath
- output @?= "ok"
- forM_ [("dep", "rawId"), ("shim", "rawId")] $ \(moduleName, exportName) -> do
- mAlias <- readAlias store ModuleAlias (pack moduleName)
- case mAlias of
- Nothing -> assertFailure ("expected " ++ moduleName ++ " module alias")
- Just ref -> do
- mManifest <- getManifest store (objectRefHash ref)
- case mManifest of
- Nothing -> assertFailure ("expected " ++ moduleName ++ " module manifest")
- Just manifest -> do
- assertBool ("viewFacts should not be exported from " ++ moduleName) $
- all ((/= "viewFacts") . unpack . moduleExportName) (moduleManifestExports manifest)
- case find ((== exportName) . unpack . moduleExportName) (moduleManifestExports manifest) of
- Nothing -> assertFailure ("expected " ++ exportName ++ " export from " ++ moduleName)
- Just ex -> do
- moduleExportViewProvenance ex @?= Just ViewTrusted
- case moduleExportView ex of
- Nothing -> assertFailure "expected trusted value-level view ref"
- Just viewRef -> do
- view <- getViewType store viewRef
- view @?= Right expected
-
- , testCase "value-level viewFacts decoder reports malformed fact context" $ do
- let env = evalTricu Map.empty (parseTricu "viewFacts = [(t \"bad\" (t 9 t))]\n")
- case valueViewFactsFromEnv env of
- Right _ -> assertFailure "expected malformed provenance error"
- Left err -> err `containsAll` ["viewFacts[0]", "bad", "invalid provenance", "unknown provenance tag 9"]
-
- , testCase "value-level viewFacts decoder reports malformed View context" $ do
- let env = evalTricu Map.empty (parseTricu "viewFacts = [(t \"bad\" (t 1 (t 9 [])))]\n")
- case valueViewFactsFromEnv env of
- Right _ -> assertFailure "expected malformed View error"
- Left err -> err `containsAll` ["viewFacts[0]", "bad", "malformed View"]
-
- , testCase "value-level viewFacts decoder rejects duplicate fact names" $ do
- let env = evalTricu Map.empty (parseTricu "v = t 9 [(t 11 []) (t 12 (t 0 []))]\nviewFacts = [(t \"dup\" (t 1 v)) (t \"dup\" (t 1 v))]\n")
- case valueViewFactsFromEnv env of
- Right _ -> assertFailure "expected duplicate viewFacts error"
- Left err -> err `containsAll` ["duplicate viewFacts entry", "dup"]
-
- , testCase "Workspace modules reject viewFacts for non-exported names" $
- withSystemTempDirectory "tricu-workspace-view-facts-nonexport" $ \dir -> do
- let store = StorePath (dir </> "store")
- depPath = dir </> "dep.tri"
- mainPath = dir </> "main.tri"
- writeFile (dir </> "tricu.workspace") "module dep = dep.tri\n"
- writeFile depPath "rawId x = x\nv = t 9 [(t 11 []) (t 12 (t 0 []))]\nviewFacts = [(t \"missing\" (t 1 v))]\n"
- writeFile mainPath "!import \"dep\" Dep\nmain = Dep.rawId t\n"
- outcome <- try (evaluateFileWithStore (Just store) mainPath) :: IO (Either SomeException Env)
- case outcome of
- Right _ -> assertFailure "expected non-exported viewFacts rejection"
- Left err -> show err `containsAll` ["viewFacts for non-exported name", "missing"]
-
- , testCase "stdlib list value-level facts publish Trusted contracts" $
- withSystemTempDirectory "tricu-stdlib-list-view-facts" $ \dir -> do
- let store = StorePath (dir </> "store")
- basePath = dir </> "base.tri"
- listPath = dir </> "list.tri"
- mainPath = dir </> "main.tri"
- baseSource <- readFile "./lib/base.tri"
- listSource <- readFile "./lib/list.tri"
- writeFile (dir </> "tricu.workspace") "module base = base.tri\nmodule list = list.tri\n"
- writeFile basePath baseSource
- writeFile listPath listSource
- writeFile mainPath "!import \"list\" L\ninc x@Byte =@Byte x\nmain xs@(List Byte) =@(List Byte) L.map inc xs\n"
- output <- checkFileWithStore store mainPath
- output @?= "ok"
- mAlias <- readAlias store ModuleAlias (pack "list")
- case mAlias of
- Nothing -> assertFailure "expected list module alias"
- Just ref -> do
- mManifest <- getManifest store (objectRefHash ref)
- case mManifest of
- Nothing -> assertFailure "expected list module manifest"
- Just manifest -> do
- let trustedNames =
- [ "emptyList?", "tail", "append", "lExist?", "map", "filter"
- , "foldl", "foldr", "length", "reverse", "snoc", "count"
- , "all?", "any?", "intersect", "headMaybe", "lastMaybe"
- , "nthMaybe", "take", "drop", "splitAt", "concatMap", "find"
- , "partition", "strLength", "strAppend", "strEq?", "strEmpty?"
- , "startsWith?", "endsWith?", "contains?", "lines", "unlines"
- , "words", "unwords", "zipWith"
- ]
- forM_ trustedNames $ \exportName ->
- case find ((== exportName) . unpack . moduleExportName) (moduleManifestExports manifest) of
- Nothing -> assertFailure ("expected " ++ exportName ++ " export")
- Just ex -> moduleExportViewProvenance ex @?= Just ViewTrusted
-
- , testCase "Workspace re-export-only modules preserve imported View Contracts" $
- withSystemTempDirectory "tricu-workspace-reexport-views" $ \dir -> do
- let store = StorePath (dir </> "store")
- depPath = dir </> "dep.tri"
- shimPath = dir </> "shim.tri"
- mainPath = dir </> "main.tri"
- writeFile (dir </> "tricu.workspace") "module dep = dep.tri\nmodule shim = shim.tri\n"
- writeFile depPath "idP x@_a =@_a x\n"
- writeFile shimPath "!import \"dep\" !Local\n"
- writeFile mainPath "!import \"shim\" Shim\nmain =@String Shim.idP \"hi\"\n"
- output <- checkFileWithStore store mainPath
- output @?= "ok"
- mAlias <- readAlias store ModuleAlias "shim"
- case mAlias of
- Nothing -> assertFailure "expected shim module alias"
- Just ref -> do
- mManifest <- getManifest store (objectRefHash ref)
- case mManifest of
- Nothing -> assertFailure "expected shim module manifest"
- Just manifest -> case find ((== "idP") . unpack . moduleExportName) (moduleManifestExports manifest) of
- Nothing -> assertFailure "expected idP re-export"
- Just ex -> do
- moduleExportViewProvenance ex @?= Just ViewChecked
- case moduleExportView ex of
- Nothing -> assertFailure "expected idP re-export view ref"
- Just viewRef -> do
- view <- getViewType store viewRef
- view @?= Right (VTForall [0] (VTFn [VTVar 0] (VTVar 0)))
-
- , testCase "tricu check rejects inconsistent first-order polymorphic View bindings" $ do
- output <- checkSourceWithEnv allTestLibsEnv "same x@_a y@_a =@_a x\nmain =@String same \"hi\" 1\n"
- output @?= "symbol 6 (byte literal) expected String but got Byte"
+ 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"
