diff --git a/docs/view-contracts.md b/docs/view-contracts.md index db383ab..b5aea41 100644 --- 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) -``` +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. -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: +The guarantees retained here are narrower: -```text -Var localId -Forall binders body -Exists binders body -``` +- 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. -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 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) -``` - -Re-export-only modules preserve imported View metadata, so these contracts flow -through `prelude` rather than only through direct `base` imports. - -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: +View facts may carry per-fact 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 +Checked +Trusted +Unchecked ``` -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. +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`. -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: - -```text -viewFacts = [fact ...] -fact = pair exportName (pair provenance view) -``` - -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. - -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 index 4bcda64..f138f56 100644 --- 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 index 676a260..191fc64 100644 --- 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 index 64d9d37..9ba1df5 100644 --- 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 index 0e1c296..ff6bc87 100644 --- 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 -``` +### Flow checking only checks represented flow -The correct granularity is per exported View fact, not per module. A single -module may contain checked definitions, trusted eliminators, and unchecked raw -helpers. +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. -## Controlled intensionality +## Retained contract -Raw intensionality should be tracked by dependency/provenance, not syntax-only. +The reduced checker may soundly claim only: -- 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. +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. -Parametric checked mode rejects annotated definitions whose derivation depends -on raw/untrusted intensionality, while trusted facts may describe raw internals -behind explicit contracts. +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. -## Trusted eliminator kernel +## Code direction -First trusted observation capabilities should be the smallest useful kernels: +The initial rollback therefore: -```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 -``` +- 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. -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 -``` - -Prefer `headMaybe : List a -> Maybe a`, or later introduce `NonEmptyList a`. - -## Implementation order - -Most-correct tractable path: - -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 - -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 index efd1f52..36035b0 100644 --- 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 index c452976..37570dc 100644 --- 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 index bf6e97a..e1a2d57 100644 --- 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 index b6b6ec2..ccfa5c1 100644 --- 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"