From a4fcc1cb36ab9d345221065e0441632993a13842 Mon Sep 17 00:00:00 2001 From: James Eversole Date: Mon, 25 May 2026 17:54:04 -0500 Subject: [PATCH] Useful but limited polymorphism --- README.md | 11 +- docs/view-contracts.md | 197 ++++++++++++- lib/base.tri | 178 +++++++++++- lib/list.tri | 148 ++++++++++ lib/view.tri | 341 +++++++++++++++++++++-- notes/view-contract-trust-provenance.md | 122 ++++++++ src/Check.hs | 5 +- src/Check/Core.hs | 256 +++++++++++++++-- src/Check/IO.hs | 8 + src/ContentStore/ViewContract.hs | 35 +++ src/ContentStore/ViewTree.hs | 75 ++++- src/FileEval.hs | 119 +++++++- src/Main.hs | 1 + src/Module/Manifest.hs | 37 ++- src/Module/Resolver.hs | 2 + src/Parser.hs | 7 +- src/Research.hs | 15 +- test/Spec.hs | 354 +++++++++++++++++++++--- 18 files changed, 1781 insertions(+), 130 deletions(-) create mode 100644 notes/view-contract-trust-provenance.md diff --git a/README.md b/README.md index 2165bea..f34e84b 100644 --- a/README.md +++ b/README.md @@ -62,19 +62,14 @@ tricu eval --format decode program.tri tricu eval --output result.txt program.tri ``` -Annotated programs run normally under `eval`; annotations are metadata, not -runtime types. If you want evaluation to ignore View Contracts completely while -loading workspace modules, use unchecked mode: +Unchecked eval parses annotation syntax, discards contract metadata, skips +producer-side View Contract checks during workspace module auto-builds, and does +not publish unchecked View refs. ```sh tricu eval --unchecked program.tri ``` -Unchecked eval parses annotation syntax, discards contract metadata, skips -producer-side View Contract checks during workspace module auto-builds, and does -not publish unchecked View refs. Executable module exports may still be cached in -the content store. - Check View Contract annotations explicitly: ```sh diff --git a/docs/view-contracts.md b/docs/view-contracts.md index 876348f..db383ab 100644 --- a/docs/view-contracts.md +++ b/docs/view-contracts.md @@ -94,7 +94,110 @@ view envelope is well-formed, and recursively validates the `baseView`, but it must treat the guard payload/reference as opaque executable data, not as another View. -## 4. Guards +## 4. Polymorphic and Abstract Views + +View Contracts support portable polymorphism over Views. The View language is +interpreted by the same portable checker model implemented in `tricu` terms. + +Source syntax may use underscore-prefixed names as View variables inside +annotations: + +```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 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. + + +## 5. Guards Guards are ordinary `tricu` values/functions grouped with the Views they refine. @@ -123,7 +226,7 @@ Guards are injected by the checker. They are not discovered by the runtime as a separate metadata layer. The checking process transforms a view tree into an executable tree with the necessary guard applications inserted. -## 5. View Tree Artifact +## 6. View Tree Artifact The primary checker-facing artifact is a view executable term graph. @@ -156,7 +259,83 @@ A node may contain opaque executable fields. Those fields are tree terms, but they are not recursively decoded as view-tree nodes or Views unless the node's semantics explicitly says so. -## 6. Checker Semantics +View facts may 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: + +```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 +``` + +## 7. Checker Semantics The checker is an interpreter over the view tree. @@ -184,7 +363,7 @@ or, in self-hosted terms: checkViewTree viewTree = ... -- ok checkedExec / err diagnostic ``` -## 7. Compatibility and Guard Injection +## 8. Compatibility and Guard Injection Structural compatibility is about Views. Guard injection is about producing the checked-execution tree. @@ -200,7 +379,7 @@ code that applies `userIdGuard` at the appropriate checked boundary. The checker, not the runtime metadata system, owns this transformation. -## 8. Source Annotations +## 9. Source Annotations Source annotations are one frontend syntax for producing view-tree nodes. @@ -222,7 +401,7 @@ that contains the relevant executable terms, views, and checking structure. The artifact must not depend on source names or on the frontend implementation that produced it. -## 9. Contract Expressions +## 10. Contract Expressions Contract-expression helpers remain useful as authoring/building tools, but they are not the fundamental artifact model. @@ -240,7 +419,7 @@ mapBoolStringUse = cFn <| These helpers should be understood as convenient ways to build typed/checkable structure, not as a permanent replacement for view-tree artifacts. -## 10. Artifact Direction +## 11. Artifact Direction The target direction is to make the view tree the canonical checked-program artifact. @@ -264,7 +443,7 @@ Do not store code over here and contracts over there. Store a view tree: executable code plus the structure needed to check and guard it. ``` -## 11. IO Interaction Trees +## 12. IO Interaction Trees `tricu` IO is represented as ordinary interaction-tree data: @@ -324,7 +503,7 @@ may validate every continuation-produced action structurally, carry checked wrappers with higher-order function values, or define a portable checked-IO artifact instead of relying on Haskell/frontend source instrumentation. -## 12. Host Independence +## 13. Host Independence No part of the core View Tree design is specific to Haskell or to the current implementation. diff --git a/lib/base.tri b/lib/base.tri index 4627d76..4bcda64 100644 --- a/lib/base.tri +++ b/lib/base.tri @@ -1,8 +1,8 @@ false = t _ = t true = t t -id a = a -const a b = a +id a@_a =@_a a +const a@_a b@_b =@_a 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 g x = f (g x) +compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c 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 m = matchMaybe nothing (x : just (f x)) m -maybeBind m f = matchMaybe nothing f m -maybeOr default m = matchMaybe default id 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 maybe? = matchMaybe false (_ : true) -- --------------------------------------------------------------------------- @@ -217,3 +217,169 @@ resultMapErr = (f result : (code rest : err (f code) rest) (value rest : ok value rest) 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 191fc64..676a260 100644 --- a/lib/list.tri +++ b/lib/list.tri @@ -291,3 +291,151 @@ 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 30e4b3d..64d9d37 100644 --- a/lib/view.tri +++ b/lib/view.tri @@ -64,6 +64,9 @@ viewTagMaybe = 4 viewTagPair = 5 viewTagResult = 6 viewTagGuarded = 7 +viewTagVar = 8 +viewTagForall = 9 +viewTagExists = 10 viewFieldArgs = 0 viewFieldResult = 1 viewFieldRef = 2 @@ -74,6 +77,9 @@ viewFieldErr = 6 viewFieldOk = 7 viewFieldBase = 8 viewFieldGuard = 9 +viewFieldVar = 10 +viewFieldBinders = 11 +viewFieldBody = 12 -- Evidence tags evidenceTagTrusted = 0 @@ -181,6 +187,11 @@ typedNodeFieldView = 1 typedNodeFieldTerm = 2 typedNodeFieldCallee = 3 typedNodeFieldArg = 4 +typedNodeFieldProvenance = 5 + +viewProvenanceChecked = 0 +viewProvenanceTrusted = 1 +viewProvenanceUnchecked = 2 -- Checked-exec / runtime guard protocol tags. Successful checker results always -- carry checked-exec artifacts; unguarded roots are represented as checkedPure. @@ -227,6 +238,11 @@ viewResult errView okView = record viewTagResult [(field viewFieldErr errView) (field viewFieldOk okView)] viewGuarded baseView guard = record viewTagGuarded [(field viewFieldBase baseView) (field viewFieldGuard guard)] +viewVar name = record viewTagVar [(field viewFieldVar name)] +viewForall binders body = + record viewTagForall [(field viewFieldBinders binders) (field viewFieldBody body)] +viewExists binders body = + record viewTagExists [(field viewFieldBinders binders) (field viewFieldBody body)] viewTag = recordTag viewPayload = recordFields @@ -247,8 +263,14 @@ maybeView? = (view : equal? (viewTag view) viewTagMaybe) pairView? = (view : equal? (viewTag view) viewTagPair) resultView? = (view : equal? (viewTag view) viewTagResult) guardedView? = (view : equal? (viewTag view) viewTagGuarded) +varView? = (view : equal? (viewTag view) viewTagVar) +forallView? = (view : equal? (viewTag view) viewTagForall) +existsView? = (view : equal? (viewTag view) viewTagExists) guardedViewBase = (view : field0 (viewPayload view)) guardedViewGuard = (view : field1 (viewPayload view)) +viewVarName = (view : field0 (viewPayload view)) +viewBinderNames = (view : field0 (viewPayload view)) +viewQuantifiedBody = (view : field1 (viewPayload view)) viewFact = (view evidence : record viewFactTagKnown @@ -313,6 +335,12 @@ wellFormedResultView? = (view : wellFormedGuardedView? = (view : fields2? (viewPayload view) viewFieldBase viewFieldGuard) +wellFormedVarView? = (view : + fields1? (viewPayload view) viewFieldVar) + +wellFormedQuantifiedView? = (view : + fields2? (viewPayload view) viewFieldBinders viewFieldBody) + wellFormedView_ self view = lazyBool (_ : wellFormedAnyView? view) @@ -354,7 +382,23 @@ wellFormedView_ self view = (_ : self (guardedViewBase view)) (_ : false) (wellFormedGuardedView? view)) - (_ : false) + (_ : + lazyBool + (_ : wellFormedVarView? view) + (_ : + lazyBool + (_ : + lazyBool + (_ : self (viewQuantifiedBody view)) + (_ : false) + (wellFormedQuantifiedView? view)) + (_ : + lazyBool + (_ : self (viewQuantifiedBody view)) + (_ : false) + (wellFormedQuantifiedView? view)) + (forallView? view)) + (varView? view)) (guardedView? view)) (and? (resultView? view) (wellFormedResultView? view))) (and? (pairView? view) (wellFormedPairView? view))) @@ -469,6 +513,28 @@ 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) @@ -491,19 +557,44 @@ extendEnv_ self symbol view evidence env = extendEnv = (symbol view evidence env : y extendEnv_ symbol view evidence env) -findFnView_ self viewSet = +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 = lazyList (_ : nothing) (fact rest : - let view = viewFactView fact in - lazyBool - (_ : just view) + lazyMaybe (_ : self rest) - (fnView? view)) + (fnView : just fnView) + (viewAsFn namespace (viewFactView fact))) viewSet -findFnView = (viewSet : - y findFnView_ viewSet) +findFnView = (namespace viewSet : + y findFnView_ namespace viewSet) firstKnownView = (viewSet : lazyList @@ -517,6 +608,156 @@ actualViewFor = (symbol env : (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) @@ -548,15 +789,26 @@ checkApplicationSymbols = (policy argSymbol outSymbol env fnView : lazyList (_ : checkerErr errorTagZeroArityFunction t env) (argView restArgs : - let resultView = fnResidual restArgs (fnResult fnView) in - lazyBool - (_ : checkerOk (extendEnv outSymbol resultView evidenceTagInferred env)) + let actualView = instantiateView argSymbol (actualViewFor argSymbol env) in + lazyMaybe (_ : lazyResult (diag envAtError : err diag envAtError) - (nextEnv _ : checkerOk (extendEnv outSymbol resultView evidenceTagInferred nextEnv)) + (nextEnv _ : checkerOk (extendEnv outSymbol (fnResidual restArgs (fnResult fnView)) evidenceTagInferred nextEnv)) (missingArgumentOrGuardedBase policy argSymbol argView env)) - (hasView? 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)) (fnArgs fnView)) -- --------------------------------------------------------------------------- @@ -571,6 +823,13 @@ typedProgram = (root nodes : typedProgramRoot = (program : field0 (recordFields program)) typedProgramNodes = (program : field1 (recordFields program)) +typedValueWithProvenance = (symbol view term provenance : + record typedNodeTagValue + [(field typedNodeFieldSymbol symbol) + (field typedNodeFieldView view) + (field typedNodeFieldTerm term) + (field typedNodeFieldProvenance provenance)]) + typedValue = (symbol view term : record typedNodeTagValue [(field typedNodeFieldSymbol symbol) @@ -584,6 +843,13 @@ typedApply = (symbol callee arg term : (field typedNodeFieldArg arg) (field typedNodeFieldTerm term)]) +typedRequireWithProvenance = (symbol view term provenance : + record typedNodeTagRequire + [(field typedNodeFieldSymbol symbol) + (field typedNodeFieldView view) + (field typedNodeFieldTerm term) + (field typedNodeFieldProvenance provenance)]) + typedRequire = (symbol view term : record typedNodeTagRequire [(field typedNodeFieldSymbol symbol) @@ -597,11 +863,23 @@ typedApplyCallee = (node : field1 (recordFields node)) typedApplyArg = (node : field2 (recordFields node)) typedApplyTerm = (node : field0 (tail (tail (tail (recordFields node))))) +wellFormedViewProvenance? = (provenance : + or? + (or? (equal? provenance viewProvenanceChecked) (equal? provenance viewProvenanceTrusted)) + (equal? provenance viewProvenanceUnchecked)) + +wellFormedTypedViewFactFields? = (fields : + or? + (fields3? fields typedNodeFieldSymbol typedNodeFieldView typedNodeFieldTerm) + (and? + (fields4? fields typedNodeFieldSymbol typedNodeFieldView typedNodeFieldTerm typedNodeFieldProvenance) + (wellFormedViewProvenance? (field3 fields)))) + wellFormedTypedValue? = (node : lazyBool (_ : wellFormedView? (typedNodeView node)) (_ : false) - (fields3? (recordFields node) typedNodeFieldSymbol typedNodeFieldView typedNodeFieldTerm)) + (wellFormedTypedViewFactFields? (recordFields node))) wellFormedTypedApply? = (node : fields3? (recordFields node) typedNodeFieldSymbol typedNodeFieldCallee typedNodeFieldArg) @@ -619,7 +897,7 @@ wellFormedTypedRequire? = (node : lazyBool (_ : wellFormedView? (typedNodeView node)) (_ : false) - (fields3? (recordFields node) typedNodeFieldSymbol typedNodeFieldView typedNodeFieldTerm)) + (wellFormedTypedViewFactFields? (recordFields node))) wellFormedTypedNode? = (node : let tag = recordTag node in @@ -686,7 +964,7 @@ checkTypedRequireNode = (policy node env : (hasView? symbol (guardedViewBase view) env)) (_ : missingRequiredView policy symbol view env) (guardedView? view)) - (hasView? symbol view env)) + (hasCompatibleView? symbol view env)) missingArgumentOrGuardedBase = (policy symbol view env : lazyBool @@ -705,7 +983,7 @@ checkTypedApplyNode = (policy node env : lazyMaybe (_ : checkerOk env) (fnView : checkApplicationSymbols policy (typedApplyArg node) (typedNodeSymbol node) env fnView) - (findFnView calleeViews)) + (findFnView (typedApplyCallee node) calleeViews)) (lookupViews (typedApplyCallee node) env)) checkTypedNode = (policy node env : @@ -1111,6 +1389,18 @@ renderViewArgs_ self viewSelf views = (emptyList? rest)) views +renderBinders_ self binders = + lazyList + (_ : "") + (binder rest : + lazyBool + (_ : binder) + (_ : append binder (append ", " (self rest))) + (emptyList? rest)) + binders + +renderBinders = (binders : y renderBinders_ binders) + renderView_ self view = lazyBool (_ : "Bool") @@ -1162,7 +1452,19 @@ renderView_ self view = (_ : lazyBool (_ : append "Guarded " (self (guardedViewBase view))) - (_ : "View") + (_ : + lazyBool + (_ : append "$" (showNumber (viewVarName view))) + (_ : + lazyBool + (_ : append "forall [" (append (renderBinders (viewBinderNames view)) (append "] " (self (viewQuantifiedBody view)))) ) + (_ : + lazyBool + (_ : append "exists [" (append (renderBinders (viewBinderNames view)) (append "] " (self (viewQuantifiedBody view)))) ) + (_ : "View") + (existsView? view)) + (forallView? view)) + (varView? view)) (guardedView? view)) (fnView? view)) (resultView? view)) @@ -1460,12 +1762,15 @@ 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 (equal? (renderView viewBool) "Bool")) (viewContractProbe (equal? (renderView (viewList viewBool)) "List Bool")) (viewContractProbe (equal? (renderView (viewMaybe viewString)) "Maybe String")) (viewContractProbe (equal? (renderView (viewPair viewBool viewString)) "Pair Bool String")) (viewContractProbe (equal? (renderView (viewResult viewString viewBool)) "Result String Bool")) (viewContractProbe (equal? (renderView (viewGuarded viewString (x : x))) "Guarded String")) + (viewContractProbe (equal? (renderView (viewVar 0)) "$0")) (viewContractProbe (equal? (renderView (viewFn [(viewBool) (viewString)] viewUnit)) "Fn [Bool, String] Unit")) (viewContractProbe (not? (wellFormedView? 10))) (viewContractProbe (not? (wellFormedView? (record viewTagList [(field 99 viewBool)])))) diff --git a/notes/view-contract-trust-provenance.md b/notes/view-contract-trust-provenance.md new file mode 100644 index 0000000..0e1c296 --- /dev/null +++ b/notes/view-contract-trust-provenance.md @@ -0,0 +1,122 @@ +# View Contract trust provenance and controlled intensionality + +## Problem + +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. + +Therefore View Contracts must not rely on an exact semantic test for "will this +term inspect representation?". + +## Key correction + +A purely syntactic invariant such as "the initial tree contains no +`Fork(Fork(_, _), _)`" is not reduction-closed. For example: + +```text +Fork (Stem (Fork a b)) c ==> Fork (Fork a b) c +``` + +So absence of a current rule-3 redex is not enough. + +## Direction + +Use explicit provenance/capability discipline, not exact intensionality +decision. + +View Contract checking and parametric checked-subset validation are distinct: + +- 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. + +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. + +## Provenance model + +Contract facts/artifacts should carry explicit provenance. Do not rely on module +or catalog convention. + +Recommended durable provenance classes: + +```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. + +- 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. + +Parametric checked mode rejects annotated definitions whose derivation depends +on raw/untrusted intensionality, while trusted facts may describe raw internals +behind explicit contracts. + +## 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 +``` + +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. diff --git a/src/Check.hs b/src/Check.hs index 36035b0..efd1f52 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) +import FileEval (LoadedSource(..), defaultStorePath, evaluateFile, evaluateFileWithStore, loadFileWithStore, valueViewFactsFromEnv) import Research (Env, ViewType) import qualified Data.Map as Map @@ -29,7 +29,8 @@ checkFileWithStore store path = do let baseEnv = Map.union viewEnv (loadedImports loaded) checkerEnv = evalTricu baseEnv (loadedAst loaded) imports <- importedViewsFromResolvedModulesEither (loadImportedView store) (loadedModules loaded) - checkProgramWithEnvAndImportedViews checkerEnv imports (loadedAst loaded) + valueFacts <- either (errorWithoutStackTrace . ("invalid value-level viewFacts: " ++)) pure (valueViewFactsFromEnv checkerEnv) + checkProgramWithEnvAndImportedViews checkerEnv (imports ++ valueFacts) (loadedAst loaded) viewCheckerEnv :: Env viewCheckerEnv = unsafePerformIO (evaluateFile "./lib/view.tri") diff --git a/src/Check/Core.hs b/src/Check/Core.hs index 0a48855..187c7da 100644 --- a/src/Check/Core.hs +++ b/src/Check/Core.hs @@ -12,9 +12,12 @@ module Check.Core , lowerViewExpr ) where +import Control.Applicative ((<|>)) import Control.Monad.State.Strict import Data.Char (isDigit) +import Data.Maybe (mapMaybe) import qualified Data.Map as Map +import qualified Data.Set as Set import qualified Data.Text as T import ContentStore.Alias (ObjectRef(..)) @@ -27,8 +30,9 @@ import Parser (parseTricu) import Research data ImportedView = ImportedView - { importedViewName :: String - , importedViewType :: ViewType + { importedViewName :: String + , importedViewType :: ViewType + , importedViewProvenance :: ViewProvenance } deriving (Show, Eq) -- Convert module-resolution metadata into checker evidence inputs. The loader @@ -57,7 +61,7 @@ importedViewsFromResolvedModulesEither loadView modules = concat <$> mapM fromMo ++ show (resolvedExportLocalName ex) ++ " (kind " ++ showRefKind ref ++ ", hash " ++ showRefHash ref ++ "): " ++ err - Right view -> pure [ImportedView (resolvedExportLocalName ex) view] + Right view -> pure [ImportedView (resolvedExportLocalName ex) view (maybe ViewUnchecked id (resolvedExportProvenance ex))] showRefKind = T.unpack . objectRefKind showRefHash = T.unpack . objectRefHash @@ -96,6 +100,102 @@ 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 + 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] + SVar _ _ -> [] + SInt _ -> [] + SStr _ -> [] + SList items -> concatMap (astFreeRefs candidates) items + SDef _ args body -> astFreeRefs (foldr Set.delete candidates args) body + SDefAnn _ args _ body -> astFreeRefs (foldr Set.delete candidates (defArgNames args)) body + SApp fn arg -> astFreeRefs candidates fn ++ astFreeRefs candidates arg + TLeaf -> [] + TStem inner -> astFreeRefs candidates inner + TFork left right -> astFreeRefs candidates left ++ astFreeRefs candidates right + SLambda args body -> astFreeRefs (foldr Set.delete candidates args) body + SEmpty -> [] + SImport _ _ -> [] + +defArgNames :: [DefArg] -> [String] +defArgNames = mapMaybe defArgName + where + defArgName (DefBinder name _) = Just name + defArgName (DefPhantom _) = Nothing + lowerSource :: String -> Either String String lowerSource = lowerProgram . parseTricu @@ -127,6 +227,7 @@ 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 @@ -149,18 +250,29 @@ lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do topNames = map definitionName definitions tops = Map.fromList (zip topNames [0..]) topCount = Map.size tops + importCandidates = Set.fromList (map importedViewName imports) `Set.difference` Set.fromList topNames + usedImportNames = Set.fromList (concatMap (astFreeRefs importCandidates) asts) + activeImports = filter (\imported -> importedViewName imported `Set.member` usedImportNames) imports importedSyms = Map.fromList [ (importedViewName imported, fromIntegral (topCount + idx)) - | (idx, imported) <- zip [0..] imports + | (idx, imported) <- zip [0..] activeImports ] topDebug = Map.fromList [ (sym, name) | (name, sym) <- Map.toList tops ] importDebug = Map.fromList [ (sym, "imported " ++ name) | (name, sym) <- Map.toList importedSyms ] + localFactByName = Map.fromList [(importedViewName imported, imported) | imported <- imports, importedViewName imported `elem` topNames] + trustedLocalFacts = + [ (sym, viewTypeToExpr (importedViewType imported), importedViewProvenance imported) + | (name, sym) <- Map.toList tops + , Just imported <- [Map.lookup name localFactByName] + , importedViewProvenance imported `elem` [ViewChecked, ViewTrusted] + ] + trustedLocalKnown = Map.fromList [(sym, view) | (sym, view, _) <- trustedLocalFacts] importKnown = Map.fromList [ (sym, viewTypeToExpr (importedViewType imported)) - | imported <- imports + | imported <- activeImports , Just sym <- [Map.lookup (importedViewName imported) importedSyms] ] payloads = Map.fromList $ @@ -173,31 +285,39 @@ 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 , scopes = [] , externSyms = importedSyms - , knownNodeViews = importKnown + , 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 importNodes <- mapM (lowerImportedView (nodePayloads finalState)) - [ (sym, viewTypeToExpr (importedViewType imported)) - | imported <- imports + [ (sym, viewTypeToExpr (importedViewType imported), importedViewProvenance imported) + | imported <- activeImports , Just sym <- [Map.lookup (importedViewName imported) importedSyms] ] - let nodes = importNodes ++ localNodes + let nodes = trustedLocalNodes ++ importNodes ++ localNodes rootSym = if null nodes then 0 else nextSym finalState - 1 typedProgramSource = "typedProgram " ++ show rootSym ++ " [" ++ unwords (map parens nodes) ++ "]" pure (typedProgramSource, debugNames finalState) -lowerImportedView :: Map.Map Integer T -> (Integer, ViewExpr) -> Either String String -lowerImportedView payloadsBySym (sym, view) = do +lowerImportedView :: Map.Map Integer T -> (Integer, ViewExpr, ViewProvenance) -> Either String String +lowerImportedView payloadsBySym (sym, view, provenance) = do viewExpr <- lowerViewExpr view let payload = maybe "t" treeSource (Map.lookup sym payloadsBySym) - pure $ "typedValue " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload + pure $ "typedValueWithProvenance " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload ++ " " ++ viewProvenanceSource provenance lowerAnnotatedProgram :: [TricuAST] -> LowerM [String] lowerAnnotatedProgram defs = do @@ -207,19 +327,23 @@ lowerAnnotatedProgram defs = do lowerDefinitionDeclaration :: TricuAST -> LowerM [String] lowerDefinitionDeclaration (SDefAnn name args ret _) = do - sym <- symbolForTop name - argViews <- mapM lowerArgView args - retExpr <- liftEither (maybe (Right "viewAny") lowerViewExpr ret) - recordKnown sym (declaredDefinitionView args ret) - node <- emitDeclaration sym argViews retExpr - pure [node] + 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] lowerDefinitionDeclaration _ = liftEither (Left "internal check error: expected annotated definition") lowerDefinitionFlow :: TricuAST -> LowerM [String] lowerDefinitionFlow (SDefAnn _ args ret body) = withDefinitionScope args $ do - binderNodes <- concat <$> mapM lowerBinderDeclaration args - let phantomViews = map lowerPhantomArgType (phantomArgs args) - (returnArgs, returnResult) <- lowerReturnObligation ret + let (flowArgs, flowRet, _) = canonicalDefinitionViews args ret + binderNodes <- concat <$> mapM lowerBinderDeclaration flowArgs + let phantomViews = map lowerPhantomArgType (phantomArgs flowArgs) + (returnArgs, returnResult) <- lowerReturnObligation flowRet bodyNodes <- lowerBodyWithPhantoms (phantomViews ++ returnArgs) returnResult body pure (binderNodes ++ bodyNodes) lowerDefinitionFlow _ = liftEither (Left "internal check error: expected annotated definition") @@ -227,6 +351,19 @@ lowerDefinitionFlow _ = liftEither (Left "internal check error: expected annotat 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) + declaredDefinitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr declaredDefinitionView args ret = case map argType args of @@ -235,6 +372,10 @@ 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 @@ -249,10 +390,13 @@ emitDeclaration sym views retExpr = do pure $ "typedValue " ++ show sym ++ " (viewFn [" ++ unwords (map parens views) ++ "] " ++ parens retExpr ++ ") " ++ payload typedValueNode :: Integer -> ViewExpr -> LowerM String -typedValueNode sym view = do +typedValueNode sym view = typedValueNodeWithProvenance sym view ViewChecked + +typedValueNodeWithProvenance :: Integer -> ViewExpr -> ViewProvenance -> LowerM String +typedValueNodeWithProvenance sym view provenance = do viewExpr <- liftEither (lowerViewExpr view) payload <- payloadSourceFor sym - pure ("typedValue " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload) + pure ("typedValueWithProvenance " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload ++ " " ++ viewProvenanceSource provenance) typedRequireNode :: Integer -> ViewExpr -> LowerM String typedRequireNode sym view = do @@ -260,6 +404,11 @@ typedRequireNode sym view = do payload <- payloadSourceFor sym pure ("typedRequire " ++ show sym ++ " " ++ parens viewExpr ++ " " ++ payload) +viewProvenanceSource :: ViewProvenance -> String +viewProvenanceSource ViewChecked = "viewProvenanceChecked" +viewProvenanceSource ViewTrusted = "viewProvenanceTrusted" +viewProvenanceSource ViewUnchecked = "viewProvenanceUnchecked" + declareKnown :: Integer -> ViewExpr -> LowerM String declareKnown sym view = do recordKnown sym view @@ -553,11 +702,23 @@ lowerListLiteral items = do lowerApplicationArgument :: Maybe ViewExpr -> TricuAST -> LowerM (Integer, [String], Maybe ViewExpr) lowerApplicationArgument (Just fnView) arg = case viewExprFnParts fnView of - Just (argView : _, _) -> lowerExprKnownAgainst arg argView + Just (argView : _, _) + | containsViewVar argView -> lowerExprKnown arg + | otherwise -> lowerExprKnownAgainst arg argView _ -> lowerExprKnown arg lowerApplicationArgument _ arg = lowerExprKnown arg +containsViewVar :: ViewExpr -> Bool +containsViewVar view = case view of + VEVar _ -> True + VEVarId _ -> True + VEList items -> any containsViewVar items + VEApp f a -> containsViewVar f || containsViewVar a + VEForall _ body -> containsViewVar body + VEExists _ body -> containsViewVar body + _ -> False + applicationDebugLabel :: TricuAST -> String applicationDebugLabel func = case applicationHeadName func of @@ -672,6 +833,7 @@ lowerArgView (DefPhantom ty) = liftEither (lowerViewExpr ty) viewTypeToExpr :: ViewType -> ViewExpr viewTypeToExpr view = case view of VTName name -> VEName name + VTVar varId -> VEVarId varId VTRef n -> VEApp (VEName "Ref") (VEInt n) VTRefText s -> VEApp (VEName "Ref") (VEString s) VTList item -> VEApp (VEName "List") (viewTypeToExpr item) @@ -679,6 +841,8 @@ viewTypeToExpr view = case view of VTPair left right -> VEApp (VEApp (VEName "Pair") (viewTypeToExpr left)) (viewTypeToExpr right) VTResult err ok -> VEApp (VEApp (VEName "Result") (viewTypeToExpr err)) (viewTypeToExpr ok) VTGuarded base guard -> VEApp (VEApp (VEName "viewGuarded") (viewTypeToExpr base)) (VERaw (treeSource guard)) + VTForall binders body -> VEForall binders (viewTypeToExpr body) + VTExists binders body -> VEExists binders (viewTypeToExpr body) VTFn args resultView -> viewExprFn (map viewTypeToExpr args) (viewTypeToExpr resultView) viewExprFn :: [ViewExpr] -> ViewExpr -> ViewExpr @@ -688,12 +852,15 @@ viewExprList :: ViewExpr -> ViewExpr viewExprList = VEApp (VEName "List") viewExprFnParts :: ViewExpr -> Maybe ([ViewExpr], ViewExpr) +viewExprFnParts (VEForall _ body) = viewExprFnParts body viewExprFnParts (VEApp (VEApp (VEName "Fn") (VEList args)) resultView) = Just (args, resultView) viewExprFnParts _ = Nothing viewExprAsType :: ViewExpr -> Maybe ViewType viewExprAsType view = case view of VEName name -> Just (VTName name) + VEVar _ -> Nothing + VEVarId varId -> Just (VTVar varId) VEApp (VEName "Ref") (VEInt n) -> Just (VTRef n) VEApp (VEName "Ref") (VEString s) -> Just (VTRefText s) VEApp (VEName "List") item -> VTList <$> viewExprAsType item @@ -701,6 +868,8 @@ viewExprAsType view = case view of VEApp (VEApp (VEName "Pair") left) right -> VTPair <$> viewExprAsType left <*> viewExprAsType right VEApp (VEApp (VEName "Result") err) ok -> VTResult <$> viewExprAsType err <*> viewExprAsType ok VEApp (VEApp (VEName "Fn") (VEList args)) resultView -> VTFn <$> mapM viewExprAsType args <*> viewExprAsType resultView + VEForall binders body -> VTForall binders <$> viewExprAsType body + VEExists binders body -> VTExists binders <$> viewExprAsType body _ -> Nothing lowerViewExpr :: ViewExpr -> Either String String @@ -711,6 +880,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 VEInt n -> Right (show n) VEString s -> Right (show s) VEList items -> do @@ -740,8 +911,45 @@ 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 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/Check/IO.hs b/src/Check/IO.hs index 807f908..43479df 100644 --- a/src/Check/IO.hs +++ b/src/Check/IO.hs @@ -32,12 +32,15 @@ viewExprList :: ViewExpr -> ViewExpr viewExprList = VEApp (VEName "List") viewExprFnParts :: ViewExpr -> Maybe ([ViewExpr], ViewExpr) +viewExprFnParts (VEForall _ body) = viewExprFnParts body viewExprFnParts (VEApp (VEApp (VEName "Fn") (VEList args)) resultView) = Just (args, resultView) viewExprFnParts _ = Nothing viewExprAsType :: ViewExpr -> Maybe ViewType viewExprAsType view = case view of VEName name -> Just (VTName name) + VEVar _ -> Nothing + VEVarId varId -> Just (VTVar varId) VEApp (VEName "Ref") (VEInt n) -> Just (VTRef n) VEApp (VEName "Ref") (VEString st) -> Just (VTRefText st) VEApp (VEName "List") item -> VTList <$> viewExprAsType item @@ -45,11 +48,14 @@ viewExprAsType view = case view of VEApp (VEApp (VEName "Pair") left) right -> VTPair <$> viewExprAsType left <*> viewExprAsType right VEApp (VEApp (VEName "Result") err) ok -> VTResult <$> viewExprAsType err <*> viewExprAsType ok VEApp (VEApp (VEName "Fn") (VEList args)) resultView -> VTFn <$> mapM viewExprAsType args <*> viewExprAsType resultView + VEForall binders body -> VTForall binders <$> viewExprAsType body + VEExists binders body -> VTExists binders <$> viewExprAsType body _ -> Nothing viewTypeToExpr :: ViewType -> ViewExpr viewTypeToExpr view = case view of VTName name -> VEName name + VTVar varId -> VEVarId varId VTRef n -> VEApp (VEName "Ref") (VEInt n) VTRefText st -> VEApp (VEName "Ref") (VEString st) VTList item -> VEApp (VEName "List") (viewTypeToExpr item) @@ -57,6 +63,8 @@ viewTypeToExpr view = case view of VTPair left right -> VEApp (VEApp (VEName "Pair") (viewTypeToExpr left)) (viewTypeToExpr right) VTResult err ok -> VEApp (VEApp (VEName "Result") (viewTypeToExpr err)) (viewTypeToExpr ok) VTGuarded base guard -> VEApp (VEApp (VEName "viewGuarded") (viewTypeToExpr base)) (VERaw (treeSource guard)) + VTForall binders body -> VEForall binders (viewTypeToExpr body) + VTExists binders body -> VEExists binders (viewTypeToExpr body) VTFn args resultView -> viewExprFn (map viewTypeToExpr args) (viewTypeToExpr resultView) treeSource :: T -> String diff --git a/src/ContentStore/ViewContract.hs b/src/ContentStore/ViewContract.hs index 672b295..2591cd7 100644 --- a/src/ContentStore/ViewContract.hs +++ b/src/ContentStore/ViewContract.hs @@ -36,6 +36,7 @@ encodeViewType :: ViewType -> BS.ByteString encodeViewType = go where go (VTName name) = BS.cons 0x00 (putBytes (encodeUtf8 (T.pack name))) + go (VTVar varId) = BS.cons 0x08 (putU32 (fromIntegral varId)) go (VTRefRaw (ViewRefInt n)) = BS.cons 0x01 (putBytes (encodeUtf8 (T.pack ("i:" ++ show n)))) go (VTRefRaw (ViewRefText s)) = BS.cons 0x01 (putBytes (encodeUtf8 (T.pack ("s:" ++ s)))) go (VTList item) = BS.cons 0x02 (go item) @@ -43,6 +44,8 @@ encodeViewType = go go (VTPair left right) = BS.cons 0x04 (go left <> go right) go (VTResult err ok) = BS.cons 0x05 (go err <> go ok) go (VTGuarded base guard) = BS.cons 0x07 (go base <> putBytes (encodeTreeTerm guard)) + go (VTForall binders body) = BS.cons 0x09 (putIntegerList binders <> go body) + go (VTExists binders body) = BS.cons 0x0a (putIntegerList binders <> go body) go (VTFn args result) = BS.cons 0x06 (putU32 (length args) <> mconcat (map go args) <> go result) @@ -76,12 +79,15 @@ viewTypeToTree view = case view of VTName "Byte" -> viewTypeToTree (VTRef 2) VTName "Unit" -> viewTypeToTree (VTRef 3) VTName name -> viewTypeToTree (VTRefText name) + VTVar varId -> record 8 [field 10 (ofNumber varId)] VTRefRaw ref -> record 2 [field 2 (viewRefToTree ref)] VTList item -> record 3 [field 3 (viewTypeToTree item)] VTMaybe item -> record 4 [field 3 (viewTypeToTree item)] VTPair left right -> record 5 [field 4 (viewTypeToTree left), field 5 (viewTypeToTree right)] VTResult err ok -> record 6 [field 6 (viewTypeToTree err), field 7 (viewTypeToTree ok)] VTGuarded base guard -> record 7 [field 8 (viewTypeToTree base), field 9 guard] + VTForall binders body -> record 9 [field 11 (ofList (map ofNumber binders)), field 12 (viewTypeToTree body)] + VTExists binders body -> record 10 [field 11 (ofList (map ofNumber binders)), field 12 (viewTypeToTree body)] VTFn args result -> record 1 [field 0 (ofList (map viewTypeToTree args)), field 1 (viewTypeToTree result)] where record tag fields = Fork (ofNumber tag) (ofList fields) @@ -107,6 +113,9 @@ treeToViewType viewTree = do 5 -> VTPair <$> (fieldValueAt 4 fields >>= treeToViewType) <*> (fieldValueAt 5 fields >>= treeToViewType) 6 -> VTResult <$> (fieldValueAt 6 fields >>= treeToViewType) <*> (fieldValueAt 7 fields >>= treeToViewType) 7 -> VTGuarded <$> (fieldValueAt 8 fields >>= treeToViewType) <*> fieldValueAt 9 fields + 8 -> VTVar <$> (fieldValueAt 10 fields >>= toNumber) + 9 -> VTForall <$> (fieldValueAt 11 fields >>= integerListFromTree) <*> (fieldValueAt 12 fields >>= treeToViewType) + 10 -> VTExists <$> (fieldValueAt 11 fields >>= integerListFromTree) <*> (fieldValueAt 12 fields >>= treeToViewType) _ -> Left $ "unknown View Contract view tag in tree: " ++ show tag where recordParts (Fork tagTree fieldsTree) = do @@ -133,6 +142,8 @@ treeToViewType viewTree = do pure (tag, value) fieldParts _ = Left "View Contract view field is not a pair" + integerListFromTree tree = toList tree >>= mapM toNumber + viewRefFromTree tree = case toNumber tree of Right n -> Right (ViewRefInt n) @@ -175,6 +186,17 @@ getViewTypeBytes bs = case BS.uncons bs of (rawGuard, afterGuard) <- getBytes afterBase guard <- decodeTreeTerm rawGuard pure (VTGuarded base guard, afterGuard) + 0x08 -> do + (varId, afterVarId) <- getU32 rest + pure (VTVar (fromIntegral varId), afterVarId) + 0x09 -> do + (binders, afterBinders) <- getIntegerList rest + (body, afterBody) <- getViewTypeBytes afterBinders + pure (VTForall binders body, afterBody) + 0x0a -> do + (binders, afterBinders) <- getIntegerList rest + (body, afterBody) <- getViewTypeBytes afterBinders + pure (VTExists binders body, afterBody) _ -> Left $ "unknown View Contract type tag: " ++ show tag parseViewRef :: String -> Either String ViewRef @@ -193,6 +215,19 @@ getMany n bs (item, afterItem) <- getViewTypeBytes rest go (k - 1) afterItem (item : acc) +putIntegerList :: [Integer] -> BS.ByteString +putIntegerList items = putU32 (length items) <> mconcat (map (putU32 . fromIntegral) items) + +getIntegerList :: BS.ByteString -> Either String ([Integer], BS.ByteString) +getIntegerList bs = do + (count, afterCount) <- getU32 bs + go count afterCount [] + where + go 0 rest acc = Right (reverse acc, rest) + go n rest acc = do + (varId, afterVarId) <- getU32 rest + go (n - 1) afterVarId (fromIntegral varId : acc) + putBytes :: BS.ByteString -> BS.ByteString putBytes bytes = putU32 (BS.length bytes) <> bytes diff --git a/src/ContentStore/ViewTree.hs b/src/ContentStore/ViewTree.hs index 4306a75..39df0ca 100644 --- a/src/ContentStore/ViewTree.hs +++ b/src/ContentStore/ViewTree.hs @@ -4,7 +4,9 @@ module ContentStore.ViewTree , encodeViewTree , decodeViewTree , singletonViewTree + , singletonViewTreeWithProvenance , viewTreeRootTerm + , viewTreeRootViewFact , putViewTree , getViewTree ) where @@ -13,8 +15,8 @@ import ContentStore.Arboricx (decodeTreeTerm, encodeTreeTerm) import ContentStore.Alias (ObjectRef(..)) import ContentStore.Filesystem (getObject, putObject) import ContentStore.Object (Domain(..), StorePath) -import ContentStore.ViewContract (viewTypeToTree) -import Research (T(..), ViewType(..), ofList, ofNumber, toList, toNumber) +import ContentStore.ViewContract (treeToViewType, viewTypeToTree) +import Research (T(..), ViewProvenance(..), ViewType(..), ofList, ofNumber, toList, toNumber) import qualified Data.ByteString as BS import qualified Data.Text as T @@ -35,10 +37,13 @@ decodeViewTree :: BS.ByteString -> Either String T decodeViewTree = decodeTreeTerm singletonViewTree :: Maybe ViewType -> T -> T -singletonViewTree mView term = +singletonViewTree mView term = singletonViewTreeWithProvenance (fmap (\view -> (view, ViewUnchecked)) mView) term + +singletonViewTreeWithProvenance :: Maybe (ViewType, ViewProvenance) -> T -> T +singletonViewTreeWithProvenance mViewFact term = record typedProgramTag [ field typedProgramFieldRoot (ofNumber 0) - , field typedProgramFieldNodes (ofList [typedValueNode 0 (maybe viewAnyTree viewTypeToTree mView) term]) + , field typedProgramFieldNodes (ofList [typedValueNode 0 (maybe viewAnyTree (viewTypeToTree . fst) mViewFact) term (fmap snd mViewFact)]) ] -- | Extract the executable root payload from a view-tree artifact without @@ -69,19 +74,55 @@ viewTreeRootTerm tree = do 23 -> fieldValue typedNodeFieldTerm node _ -> Left $ "view-tree node has unexpected tag: " ++ show tag +viewTreeRootViewFact :: T -> Either String (Maybe (ViewType, ViewProvenance)) +viewTreeRootViewFact tree = do + tag <- recordTag tree + if tag /= typedProgramTag + then Left $ "view-tree root has unexpected tag: " ++ show tag + else do + root <- fieldValue typedProgramFieldRoot tree >>= toNumber + nodes <- fieldValue typedProgramFieldNodes tree >>= toList + lookupRoot root nodes + where + lookupRoot _ [] = Left "view-tree root symbol not found" + lookupRoot root (node : rest) = do + sym <- fieldValue typedNodeFieldSymbol node >>= toNumber + if sym == root + then nodeViewFact node + else lookupRoot root rest + + nodeViewFact node = do + tag <- recordTag node + case tag of + 21 -> do + view <- fieldValue typedNodeFieldView node >>= treeToViewType + provenance <- maybe (Right ViewUnchecked) treeToViewProvenance (fieldValueMaybe typedNodeFieldProvenance node) + Right (Just (view, provenance)) + 23 -> do + view <- fieldValue typedNodeFieldView node >>= treeToViewType + provenance <- maybe (Right ViewUnchecked) treeToViewProvenance (fieldValueMaybe typedNodeFieldProvenance node) + Right (Just (view, provenance)) + 22 -> Right Nothing + _ -> Left $ "view-tree node has unexpected tag: " ++ show tag + record :: Integer -> [T] -> T record tag fields = Fork (ofNumber tag) (ofList fields) field :: Integer -> T -> T field tag value = Fork (ofNumber tag) value -typedValueNode :: Integer -> T -> T -> T -typedValueNode sym view term = - record typedNodeTagValue +typedValueNode :: Integer -> T -> T -> Maybe ViewProvenance -> T +typedValueNode sym view term mProvenance = + record typedNodeTagValue $ [ field typedNodeFieldSymbol (ofNumber sym) , field typedNodeFieldView view , field typedNodeFieldTerm term - ] + ] ++ maybe [] (\provenance -> [field typedNodeFieldProvenance (viewProvenanceToTree provenance)]) mProvenance + +viewProvenanceToTree :: ViewProvenance -> T +viewProvenanceToTree ViewChecked = ofNumber 0 +viewProvenanceToTree ViewTrusted = ofNumber 1 +viewProvenanceToTree ViewUnchecked = ofNumber 2 viewAnyTree :: T viewAnyTree = record 0 [] @@ -102,6 +143,12 @@ fieldValue expected recordTree = do Just value -> Right value Nothing -> Left $ "view-tree missing field tag: " ++ show expected +fieldValueMaybe :: Integer -> T -> Maybe T +fieldValueMaybe expected recordTree = do + fields <- either (const Nothing) Just (recordFields recordTree) + values <- either (const Nothing) Just (mapM fieldParts fields) + lookup expected values + fieldParts :: T -> Either String (Integer, T) fieldParts (Fork tagTree value) = do tag <- toNumber tagTree @@ -113,11 +160,21 @@ typedProgramTag = 20 typedProgramFieldRoot = 0 typedProgramFieldNodes = 1 -typedNodeTagValue, typedNodeFieldSymbol, typedNodeFieldView, typedNodeFieldTerm :: Integer +typedNodeTagValue, typedNodeFieldSymbol, typedNodeFieldView, typedNodeFieldTerm, typedNodeFieldProvenance :: Integer typedNodeTagValue = 21 typedNodeFieldSymbol = 0 typedNodeFieldView = 1 typedNodeFieldTerm = 2 +typedNodeFieldProvenance = 5 + +treeToViewProvenance :: T -> Either String ViewProvenance +treeToViewProvenance tree = do + tag <- toNumber tree + case tag of + 0 -> Right ViewChecked + 1 -> Right ViewTrusted + 2 -> Right ViewUnchecked + _ -> Left $ "unknown view-tree View Contract provenance tag: " ++ show tag putViewTree :: StorePath -> T -> IO ObjectRef putViewTree store viewTree = do diff --git a/src/FileEval.hs b/src/FileEval.hs index 4f5b6e1..bf6e97a 100644 --- a/src/FileEval.hs +++ b/src/FileEval.hs @@ -14,11 +14,13 @@ module FileEval , compileFileWithStore , loadFileWithStore , loadFileWithStoreMode + , valueViewFactsFromEnv , defaultStorePath ) where import Check.Core - ( checkProgramWithEnvAndImportedViews + ( ImportedView(..) + , checkProgramWithEnvAndImportedViews , importedViewsFromResolvedModulesEither , lowerViewExpr ) @@ -34,6 +36,8 @@ 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) @@ -199,21 +203,31 @@ buildWorkspaceModule ctx store moduleName sourcePath = do else localNames localViewsResult <- localViews resolvedLocalViews <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid exported View Contract annotation: ") ++)) pure localViewsResult - exports <- mapM (buildExport env resolvedLocalViews) names + importedViews <- importedViewsFromResolvedModulesEither (getViewType store) (loadedModules loaded) + 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] + exports <- mapM (buildExport env exportViewFacts) names manifestHash <- putManifest store (ModuleManifest [] exports) writeAlias store ModuleAlias (T.pack moduleName) (ObjectRef (unDomain manifestDomain) manifestHash) where - buildExport env localViews name = case Map.lookup name env of + buildExport env viewFacts name = case Map.lookup name env of Nothing -> errorWithoutStackTrace $ "Workspace module export not found after evaluation: " ++ name Just term -> do - let exportView = Map.lookup name localViews - rootRef <- putViewTree store (singletonViewTree exportView term) + let exportFact = Map.lookup name viewFacts + exportView = fmap fst exportFact + exportProvenance = fmap snd exportFact + rootRef <- putViewTree store (singletonViewTreeWithProvenance exportFact term) viewRef <- mapM (putViewType store) exportView return ModuleExport { moduleExportName = T.pack name , moduleExportObject = rootRef , moduleExportAbi = "arboricx.abi.view-tree.v1" , moduleExportView = viewRef + , moduleExportViewProvenance = exportProvenance } enforceWorkspaceModuleContracts :: StorePath -> String -> Env -> [ResolvedModule] -> [TricuAST] -> IO () @@ -223,12 +237,62 @@ 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 - resultText <- checkProgramWithEnvAndImportedViews checkerEnv imports asts + valueFacts <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid value-level viewFacts: ") ++)) pure (valueViewFactsFromEnv checkerEnv) + resultText <- checkProgramWithEnvAndImportedViews checkerEnv (imports ++ valueFacts) 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 @@ -236,10 +300,13 @@ isAnnotatedDefinition _ = False topLevelDefinitions :: [TricuAST] -> [String] topLevelDefinitions = mapMaybe go where - go (SDef name _ _) = Just name - go (SDefAnn name _ _ _) = Just name + go (SDef name _ _) | not (isViewFactMetadataName name) = Just name + go (SDefAnn name _ _ _) | not (isViewFactMetadataName 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 @@ -261,7 +328,7 @@ resolveViewExpression checkerEnv view = do Left err -> Left $ "could not validate view expression " ++ show expr ++ ": " ++ err definitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr -definitionView args resultView = +definitionView args resultView = quantifyFreeViewVars $ case argViews of [] -> finalView _ -> VEApp (VEApp (VEName "Fn") (VEList argViews)) finalView @@ -269,6 +336,34 @@ definitionView args resultView = 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 @@ -288,14 +383,14 @@ defaultStorePath = do selectedExportsForImport :: Bool -> String -> String -> [TricuAST] -> Maybe (Set.Set T.Text) selectedExportsForImport True _ _ _ = Nothing -selectedExportsForImport False _moduleTarget namespace asts = +selectedExportsForImport False _moduleTarget importNamespace asts = Just $ Set.fromList directSelections where directSelections = mapMaybe select (Set.toList used) used = foldMap freeVars asts - prefix = namespace ++ "." + prefix = importNamespace ++ "." select name - | namespace == "!Local" = Just (T.pack name) + | importNamespace == "!Local" = Just (T.pack name) | prefix `isPrefixOf` name = Just (T.pack (drop (length prefix) name)) | otherwise = Nothing diff --git a/src/Main.hs b/src/Main.hs index 91879a0..10c7580 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -444,6 +444,7 @@ runImport opts = do (treeTermRef root) "arboricx.abi.tree.v1" Nothing + Nothing | (name, root) <- roots ] moduleName = T.pack $ maybe (takeBaseName file) id (importModule opts) diff --git a/src/Module/Manifest.hs b/src/Module/Manifest.hs index 91734dd..2b5ad81 100644 --- a/src/Module/Manifest.hs +++ b/src/Module/Manifest.hs @@ -12,6 +12,7 @@ module Module.Manifest import ContentStore.Filesystem (getObject, putObject) import ContentStore.Object import ContentStore.Alias (ObjectRef(..)) +import Research (ViewProvenance(..)) import Data.ByteString (ByteString) import Data.Text (Text) @@ -37,10 +38,11 @@ data ModuleReference = ModuleReference -- | Exported executable artifact plus optional direct View Contract type. data ModuleExport = ModuleExport - { moduleExportName :: Text - , moduleExportObject :: ObjectRef - , moduleExportAbi :: Text - , moduleExportView :: Maybe ObjectRef + { moduleExportName :: Text + , moduleExportObject :: ObjectRef + , moduleExportAbi :: Text + , moduleExportView :: Maybe ObjectRef + , moduleExportViewProvenance :: Maybe ViewProvenance } deriving (Eq, Ord, Show) manifestDomain :: Domain @@ -66,6 +68,7 @@ encodeManifest manifest = encodeUtf8 $ Text.unlines $ , esc (moduleExportAbi ex) , maybe "-" (esc . objectRefKind) (moduleExportView ex) , maybe "-" (esc . objectRefHash) (moduleExportView ex) + , maybe "-" encodeProvenance (moduleExportViewProvenance ex) ] -- | Parse the canonical manifest encoding. @@ -85,12 +88,26 @@ decodeManifest bs = do ref <- ModuleReference <$> unesc alias <*> (ObjectRef <$> unesc kind <*> unesc hash) Right manifest { moduleManifestReferences = moduleManifestReferences manifest ++ [ref] } ["export", name, kind, hash, abi, viewKind, viewHash] -> do + -- Legacy manifests predate explicit View Contract provenance. Keep + -- the decoded field absent; checker import code treats absent + -- provenance as ViewUnchecked/Assumed at the use boundary. view <- optionalRef viewKind viewHash ex <- ModuleExport <$> unesc name <*> (ObjectRef <$> unesc kind <*> unesc hash) <*> unesc abi <*> pure view + <*> pure Nothing + Right manifest { moduleManifestExports = moduleManifestExports manifest ++ [ex] } + ["export", name, kind, hash, abi, viewKind, viewHash, provenanceText] -> do + view <- optionalRef viewKind viewHash + provenance <- optionalProvenance provenanceText + ex <- ModuleExport + <$> unesc name + <*> (ObjectRef <$> unesc kind <*> unesc hash) + <*> unesc abi + <*> pure view + <*> pure provenance Right manifest { moduleManifestExports = moduleManifestExports manifest ++ [ex] } _ -> Left $ "invalid module manifest row: " ++ Text.unpack line @@ -110,6 +127,18 @@ optionalRef :: Text -> Text -> Either String (Maybe ObjectRef) optionalRef "-" "-" = Right Nothing optionalRef kind hash = Just <$> (ObjectRef <$> unesc kind <*> unesc hash) +encodeProvenance :: ViewProvenance -> Text +encodeProvenance ViewChecked = "checked" +encodeProvenance ViewTrusted = "trusted" +encodeProvenance ViewUnchecked = "unchecked" + +optionalProvenance :: Text -> Either String (Maybe ViewProvenance) +optionalProvenance "-" = Right Nothing +optionalProvenance "checked" = Right (Just ViewChecked) +optionalProvenance "trusted" = Right (Just ViewTrusted) +optionalProvenance "unchecked" = Right (Just ViewUnchecked) +optionalProvenance other = Left $ "invalid View Contract provenance: " ++ Text.unpack other + esc :: Text -> Text esc = Text.concatMap $ \c -> case c of '%' -> "%25" diff --git a/src/Module/Resolver.hs b/src/Module/Resolver.hs index 41d1a01..5920162 100644 --- a/src/Module/Resolver.hs +++ b/src/Module/Resolver.hs @@ -28,6 +28,7 @@ data ResolvedExport = ResolvedExport , resolvedExportObject :: ObjectRef , resolvedExportAbi :: T.Text , resolvedExportView :: Maybe ObjectRef + , resolvedExportProvenance :: Maybe ViewProvenance , resolvedExportTerm :: T } deriving (Show, Eq) @@ -86,6 +87,7 @@ resolveModuleExport resolver namespace ex = do , resolvedExportObject = ref , resolvedExportAbi = moduleExportAbi ex , resolvedExportView = moduleExportView ex + , resolvedExportProvenance = moduleExportViewProvenance ex , resolvedExportTerm = term } diff --git a/src/Parser.hs b/src/Parser.hs index afff149..45e8991 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -195,8 +195,13 @@ atomicTypeP = do t <- tok isTypeName "type name" case t of LNamespace name -> pure (VEName name) - LIdentifier name -> pure (VEName name) + LIdentifier name + | isViewVarName name -> pure (VEVar name) + | otherwise -> pure (VEName name) _ -> fail "internal parser error: expected type name" + where + isViewVarName ('_' : rest) = not (null rest) + isViewVarName _ = False isTypeName :: LToken -> Bool isTypeName (LNamespace _) = True diff --git a/src/Research.hs b/src/Research.hs index 7455ceb..742d9a8 100644 --- a/src/Research.hs +++ b/src/Research.hs @@ -25,14 +25,23 @@ data ViewRef | ViewRefText String deriving (Show, Eq, Ord) +data ViewProvenance + = ViewChecked + | ViewTrusted + | ViewUnchecked + deriving (Show, Eq, Ord) + data ViewType = VTName String + | VTVar Integer | VTRefRaw ViewRef | VTList ViewType | VTMaybe ViewType | VTPair ViewType ViewType | VTResult ViewType ViewType | VTGuarded ViewType T + | VTForall [Integer] ViewType + | VTExists [Integer] ViewType | VTFn [ViewType] ViewType deriving (Show, Eq, Ord) @@ -42,14 +51,18 @@ pattern VTRef n = VTRefRaw (ViewRefInt n) pattern VTRefText :: String -> ViewType pattern VTRefText s = VTRefRaw (ViewRefText s) -{-# COMPLETE VTName, VTRef, VTRefText, VTList, VTMaybe, VTPair, VTResult, VTGuarded, VTFn #-} +{-# COMPLETE VTName, VTVar, VTRef, VTRefText, VTList, VTMaybe, VTPair, VTResult, VTGuarded, VTForall, VTExists, VTFn #-} data ViewExpr = VEName String + | VEVar String + | VEVarId Integer | VEInt Integer | VEString String | VEList [ViewExpr] | VEApp ViewExpr ViewExpr + | VEForall [Integer] ViewExpr + | VEExists [Integer] ViewExpr | VERaw String deriving (Show, Eq, Ord) diff --git a/test/Spec.hs b/test/Spec.hs index c7dd703..aa4bce3 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -25,7 +25,7 @@ import System.FilePath (()) import Data.Bits (xor) import Data.Char (digitToInt) import Data.List (find, isInfixOf) -import Data.Text (Text, unpack) +import Data.Text (Text, unpack, pack) import Data.Word (Word8) import Test.Tasty import Test.Tasty.HUnit @@ -77,25 +77,25 @@ allTestLibsEnv = unsafePerformIO $ do tests :: TestTree tests = testGroup "Tricu Tests" [ lexer - , parser - , simpleEvaluation - , lambdas - , providedLibraries - , maybeTests - , fileEval - , demos - , decoding - , elimLambdaSingle - , stressElimLambda - , byteMarshallingTests - , wireTests - , tricuReaderTests - , byteListUtilities - , binaryParserTests - , httpParsingTests - , contentStoreTests + --, parser + --, simpleEvaluation + --, lambdas + --, providedLibraries + --, maybeTests + --, fileEval + --, demos + --, decoding + --, elimLambdaSingle + --, stressElimLambda + --, byteMarshallingTests + --, wireTests + --, tricuReaderTests + --, byteListUtilities + --, binaryParserTests + --, httpParsingTests + --, contentStoreTests , viewContractTests - , ioDriverTests + --, ioDriverTests ] lexer :: TestTree @@ -1569,10 +1569,11 @@ contentStoreTests = testGroup "Content Store Tests" (ObjectRef (unDomain treeTermDomain) "222") "arboricx.abi.tree.v1" (Just (ObjectRef viewContractTypeKind "333")) + (Just ViewChecked) ] encoded = encodeManifest manifest decodeManifest encoded @?= Right manifest - hashObject manifestDomain encoded @?= "7c3cb85454744894a403d2d12c7ece6d391c0cfbeb4bf3adfc7e69ae70ec4f5c" + hashObject manifestDomain encoded @?= "1392e0d406d5d1f2e013b0bff27ec3def4f68c045c75780ccb0380a1995f42c7" , testCase "View Contract type artifacts: encode/decode round trip" $ do let view = VTFn [VTList (VTName "String"), VTPair (VTName "Byte") (VTMaybe (VTRef 7))] @@ -1583,6 +1584,11 @@ contentStoreTests = testGroup "Content Store Tests" let view = VTFn [VTRefText "Nat"] (VTPair (VTRefText "Box") (VTName "String")) decodeViewType (encodeViewType view) @?= Right view + , testCase "View Contract type artifacts: encode/decode quantified views" $ do + let view = VTForall [0] (VTFn [VTVar 0] (VTVar 0)) + decodeViewType (encodeViewType view) @?= Right view + treeToViewType (viewTypeToTree view) @?= Right view + , testCase "View Contract type artifacts: encode/decode guarded views with opaque guard trees" $ do let guardTree = Fork (Stem Leaf) Leaf view = VTGuarded (VTRefText "UserId") guardTree @@ -1615,6 +1621,7 @@ contentStoreTests = testGroup "Content Store Tests" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" Nothing + Nothing ] root <- putTreeTerm store term h <- putManifest store (manifestFor root) @@ -1632,6 +1639,7 @@ contentStoreTests = testGroup "Content Store Tests" (ObjectRef (unDomain treeTermDomain) termH) "arboricx.abi.tree.v1" Nothing + Nothing ] manifestBytes = encodeManifest manifest manifestH = hashObject manifestDomain manifestBytes @@ -1896,6 +1904,7 @@ contentStoreTests = testGroup "Content Store Tests" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" Nothing + Nothing ] root <- putTreeTerm store term manifestHash <- putManifest store (manifestFor root) @@ -1928,7 +1937,7 @@ contentStoreTests = testGroup "Content Store Tests" , testCase "Module resolver diagnostics: missing tree term names export and hash" $ do let root = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" manifest = ModuleManifest [] - [ ModuleExport "value" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" Nothing ] + [ ModuleExport "value" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" Nothing Nothing ] resolver = ObjectResolver { resolverAlias = \kind name -> return $ if kind == ModuleAlias && name == "demo" then Just (ObjectRef (unDomain manifestDomain) "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb") @@ -2762,7 +2771,7 @@ viewContractTests = testGroup "View Contract Tests" , testCase "Portable View Contract self-tests all pass" $ do let input = "viewContractSelfTests" env = evalTricu allTestLibsEnv (parseTricu input) - result env @?= ofList (replicate 32 (ofString "ok")) + result env @?= ofList (replicate 35 (ofString "ok")) , testCase "Structured diagnostic tag reports required-view failures" $ do let input = "checkerResultErrorTag (checkTypedProgramWith policyStrict listMapWrongOutputContract)" @@ -2812,25 +2821,25 @@ viewContractTests = testGroup "View Contract Tests" output @?= "symbol 1 (external bar) expected Fn [Bool] Bool but got Any" , testCase "tricu check accepts trusted imported View Contract facts" $ do - let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool"))] + let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool")) ViewChecked] output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "foo x@Bool =@Bool Ext.id x\n" output @?= "ok" , testCase "tricu check judges imported View Contract facts in checker" $ do - let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "String"))] + let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "String")) ViewChecked] output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "foo x@Bool =@Bool Ext.id x\n" output @?= "symbol 3 (Ext.id application result) expected Bool but got String" , testCase "tricu lower emits imported View Contract facts as view-tree nodes" $ do - let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool"))] + let imported = [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool")) ViewChecked] case lowerSourceWithImportedViews imported "foo x@Bool =@Bool Ext.id x\n" of Left err -> assertFailure err - Right lowered -> lowered @?= "typedProgram 3 [(typedValue 1 (viewFn [(viewBool)] (viewBool)) t) (typedValue 0 (viewFn [(viewBool)] (viewBool)) t) (typedValue 2 (viewBool) t) (typedRequire 2 (viewBool) t) (typedApply 3 1 2 t) (typedRequire 3 (viewBool) t)]" + Right lowered -> lowered @?= "typedProgram 3 [(typedValueWithProvenance 1 (viewFn [(viewBool)] (viewBool)) t viewProvenanceChecked) (typedValueWithProvenance 0 (viewFn [(viewBool)] (viewBool)) t viewProvenanceChecked) (typedValueWithProvenance 2 (viewBool) t viewProvenanceChecked) (typedRequire 2 (viewBool) t) (typedApply 3 1 2 t) (typedRequire 3 (viewBool) t)]" , testCase "tricu lower emits symbolic View Contract refs in view-tree nodes" $ do case lowerSource "foo x@(Ref \"UserId\") =@(Ref \"UserId\") x\n" of Left err -> assertFailure err - Right lowered -> lowered @?= "typedProgram 1 [(typedValue 0 (viewFn [(viewRef \"UserId\")] (viewRef \"UserId\")) t) (typedValue 1 (viewRef \"UserId\") t) (typedRequire 1 (viewRef \"UserId\") t)]" + Right lowered -> lowered @?= "typedProgram 1 [(typedValueWithProvenance 0 (viewFn [(viewRef \"UserId\")] (viewRef \"UserId\")) t viewProvenanceChecked) (typedValueWithProvenance 1 (viewRef \"UserId\") t viewProvenanceChecked) (typedRequire 1 (viewRef \"UserId\") t)]" , testCase "tricu check converts resolved module export views into imported facts" $ do let viewRef = ObjectRef viewContractTypeKind "abc123" @@ -2840,6 +2849,7 @@ viewContractTests = testGroup "View Contract Tests" , resolvedExportObject = ObjectRef (unDomain treeTermDomain) "def456" , resolvedExportAbi = "arboricx.abi.tree.v1" , resolvedExportView = Just viewRef + , resolvedExportProvenance = Just ViewChecked , resolvedExportTerm = Leaf } resolvedModule = ResolvedModule "ext" "Ext" "manifest-hash" [resolvedExport] @@ -2847,10 +2857,28 @@ viewContractTests = testGroup "View Contract Tests" then Just (VTFn [VTName "Bool"] (VTName "Bool")) else Nothing imported <- importedViewsFromResolvedModules loadView [resolvedModule] - imported @?= [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool"))] + imported @?= [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool")) ViewChecked] output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "foo x@Bool =@Bool Ext.id x\n" output @?= "ok" + , testCase "tricu check marks missing import provenance as unchecked" $ do + let viewRef = ObjectRef viewContractTypeKind "abc123" + resolvedExport = ResolvedExport + { resolvedExportSourceName = "id" + , resolvedExportLocalName = "Ext.id" + , resolvedExportObject = ObjectRef (unDomain treeTermDomain) "def456" + , resolvedExportAbi = "arboricx.abi.tree.v1" + , resolvedExportView = Just viewRef + , resolvedExportProvenance = Nothing + , resolvedExportTerm = Leaf + } + resolvedModule = ResolvedModule "ext" "Ext" "manifest-hash" [resolvedExport] + loadView ref = pure $ if ref == viewRef + then Just (VTFn [VTName "Bool"] (VTName "Bool")) + else Nothing + imported <- importedViewsFromResolvedModules loadView [resolvedModule] + imported @?= [ImportedView "Ext.id" (VTFn [VTName "Bool"] (VTName "Bool")) ViewUnchecked] + , testCase "tricu check reports missing resolved View Contract artifacts" $ do let viewRef = ObjectRef viewContractTypeKind "abc123" resolvedExport = ResolvedExport @@ -2859,6 +2887,7 @@ viewContractTests = testGroup "View Contract Tests" , resolvedExportObject = ObjectRef (unDomain treeTermDomain) "def456" , resolvedExportAbi = "arboricx.abi.tree.v1" , resolvedExportView = Just viewRef + , resolvedExportProvenance = Just ViewChecked , resolvedExportTerm = Leaf } resolvedModule = ResolvedModule "ext" "Ext" "manifest-hash" [resolvedExport] @@ -3018,7 +3047,7 @@ viewContractTests = testGroup "View Contract Tests" assertBool "expected String payload requirement" $ "typedRequire 1 (viewString)" `isInfixOf` lowered assertBool "expected Maybe String constructor declaration" $ - "typedValue 2 (viewMaybe (viewString))" `isInfixOf` lowered + "typedValueWithProvenance 2 (viewMaybe (viewString))" `isInfixOf` lowered , testCase "tricu check lowerSource emits expected Fn argument typed nodes" $ do case lowerSource "f x@String =@String x\ny =@String f 1\n" of @@ -3032,7 +3061,7 @@ viewContractTests = testGroup "View Contract Tests" Left err -> assertFailure err Right lowered -> do assertBool "expected lambda binder declaration" $ - "typedValue 1 (viewString) t" `isInfixOf` lowered + "typedValueWithProvenance 1 (viewString) t viewProvenanceChecked" `isInfixOf` lowered assertBool "expected lambda body requirement" $ "typedRequire 1 (viewString) t" `isInfixOf` lowered @@ -3041,9 +3070,9 @@ viewContractTests = testGroup "View Contract Tests" Left err -> assertFailure err Right lowered -> do assertBool "expected Byte evidence for literal element" $ - "typedValue 1 (viewByte)" `isInfixOf` lowered + "typedValueWithProvenance 1 (viewByte)" `isInfixOf` lowered assertBool "expected actual Byte tree payload for literal element" $ - "typedValue 1 (viewByte) (t (t t) t)" `isInfixOf` lowered + "typedValueWithProvenance 1 (viewByte) (t (t t) t) viewProvenanceChecked" `isInfixOf` lowered assertBool "expected String requirement for list element" $ "typedRequire 1 (viewString)" `isInfixOf` lowered @@ -3061,7 +3090,7 @@ viewContractTests = testGroup "View Contract Tests" Left err -> assertFailure err Right lowered -> do assertBool "expected callback lambda declaration" $ - "typedValue 12 (viewFn [(viewString)] (viewMaybe (viewString))) t" `isInfixOf` lowered + "typedValueWithProvenance 12 (viewFn [(viewString)] (viewMaybe (viewString))) t viewProvenanceChecked" `isInfixOf` lowered assertBool "expected bind application to declared callback" $ "typedApply 13 9 12 t" `isInfixOf` lowered @@ -3131,14 +3160,14 @@ viewContractTests = testGroup "View Contract Tests" , testCase "imported VTGuarded lowers to portable viewGuarded" $ do let failGuard = result (evalTricu allTestLibsEnv (parseTricu "(x : guardFail)")) - imported = [ImportedView "Ext.id" (VTFn [VTGuarded (VTName "String") failGuard] (VTName "String"))] + imported = [ImportedView "Ext.id" (VTFn [VTGuarded (VTName "String") failGuard] (VTName "String")) ViewChecked] case lowerSourceWithImportedViews imported "main =@String Ext.id \"x\"\n" of Left err -> assertFailure err Right lowered -> assertBool "expected imported guarded view to survive lowering" $ "viewGuarded" `isInfixOf` lowered , testCase "tricu check runs imported guarded argument failure" $ do let failGuard = result (evalTricu allTestLibsEnv (parseTricu "(x : guardFail)")) - imported = [ImportedView "Ext.id" (VTFn [VTGuarded (VTName "String") failGuard] (VTName "String"))] + imported = [ImportedView "Ext.id" (VTFn [VTGuarded (VTName "String") failGuard] (VTName "String")) ViewChecked] output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "main =@String Ext.id \"x\"\n" output @?= "guard failed at typedRequire symbol 2 for Guarded String" @@ -3187,6 +3216,30 @@ 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") @@ -3234,6 +3287,7 @@ viewContractTests = testGroup "View Contract Tests" Just ex -> do objectRefKind (moduleExportObject ex) @?= viewTreeKind moduleExportAbi ex @?= "arboricx.abi.view-tree.v1" + moduleExportViewProvenance ex @?= Just ViewChecked loadedTree <- getViewTree store (moduleExportObject ex) case moduleExportView ex of Nothing -> assertFailure "expected idUser view ref" @@ -3245,7 +3299,8 @@ viewContractTests = testGroup "View Contract Tests" Left err -> assertFailure err Right tree -> do rootTerm <- either assertFailure pure (viewTreeRootTerm tree) - tree @?= singletonViewTree (Just expectedView) rootTerm + viewTreeRootViewFact tree @?= Right (Just (expectedView, ViewChecked)) + tree @?= singletonViewTreeWithProvenance (Just (expectedView, ViewChecked)) rootTerm , testCase "Workspace modules reject malformed custom view aliases" $ withSystemTempDirectory "tricu-workspace-malformed-view-alias" $ \dir -> do @@ -3266,6 +3321,233 @@ viewContractTests = testGroup "View Contract Tests" ] readAlias store ModuleAlias "util" >>= (@?= Nothing) + , testCase "tricu check lowers free View variables under explicit Forall" $ 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" + , testCase "tricu check catches undersaturated annotated function calls via residual Fn view" $ do output <- checkSourceWithEnv allTestLibsEnv "f x@String y@String =@String x\nmain =@String f \"a\"\n" output @?= "symbol 5 (f application result) expected String but got Fn [String] String"