Back out the worst of the unsound nonsense
This commit is contained in:
@@ -1,122 +1,95 @@
|
||||
# View Contract trust provenance and controlled intensionality
|
||||
# View Contracts at the intensionality boundary
|
||||
|
||||
## Problem
|
||||
## Conclusion
|
||||
|
||||
Tree Calculus / tricu code can perform raw intensional observation through `t` /
|
||||
`triage`-like power. Exact detection of whether an arbitrary term ever reaches
|
||||
rule 3 is undecidable: the SK fragment is already Turing-complete, and a program
|
||||
can construct/apply an intensional observer iff an encoded machine halts.
|
||||
Tree Calculus does not support the abstraction theorem that the former
|
||||
parametric View design assumed. Views can remain useful as boundary metadata and
|
||||
as instructions for runtime guard placement, but they must not be presented as
|
||||
types, proofs of parametricity, or representation-hiding abstraction.
|
||||
|
||||
Therefore View Contracts must not rely on an exact semantic test for "will this
|
||||
term inspect representation?".
|
||||
## Fundamental conflicts
|
||||
|
||||
## Key correction
|
||||
### Raw observation defeats representation independence
|
||||
|
||||
A purely syntactic invariant such as "the initial tree contains no
|
||||
`Fork(Fork(_, _), _)`" is not reduction-closed. For example:
|
||||
A parametric contract such as:
|
||||
|
||||
```text
|
||||
Fork (Stem (Fork a b)) c ==> Fork (Fork a b) c
|
||||
forall a. a -> a
|
||||
```
|
||||
|
||||
So absence of a current rule-3 redex is not enough.
|
||||
normally relies on code being unable to learn anything about `a`. A Tree
|
||||
Calculus term can inspect the tree supplied at `a`, distinguish
|
||||
representations, and return a representation-dependent value. The View variable
|
||||
does not hide or seal that tree.
|
||||
|
||||
## Direction
|
||||
The same breaks existential abstraction. Advertising a payload as
|
||||
`exists repr. ...` changes no operational capability: a client can still
|
||||
inspect the representation directly.
|
||||
|
||||
Use explicit provenance/capability discipline, not exact intensionality
|
||||
decision.
|
||||
### Opaque payloads are asserted, not checked
|
||||
|
||||
View Contract checking and parametric checked-subset validation are distinct:
|
||||
A typed-value node carries an executable tree beside a View. Metadata validation
|
||||
deliberately treats that executable field as opaque. Consequently, accepting a
|
||||
node proves that the envelope and View are well formed; it does not prove that
|
||||
the tree denotes the advertised `Fn`, `List`, `Maybe`, or other structural
|
||||
View.
|
||||
|
||||
- View Contract checking: verifies executable tree artifacts against declared
|
||||
boundary Views.
|
||||
- Parametric checked-subset validation: verifies that abstraction/parametricity
|
||||
claims do not depend on raw untrusted intensional observation.
|
||||
Provenance labels do not change this. `Checked` and `Trusted` record where an
|
||||
assertion came from, but neither is a derivation that another implementation can
|
||||
replay to establish the assertion.
|
||||
|
||||
Unchecked/raw Tree Calculus can always inspect trees. Existential/abstract Views
|
||||
are checker-level opacity: checked clients cannot justify representation-specific
|
||||
operations unless an exported trusted capability/eliminator provides them.
|
||||
### Syntactic taint is not a semantic parametricity proof
|
||||
|
||||
## Provenance model
|
||||
Rejecting direct uses of `t` or `triage` is neither complete nor a stable
|
||||
soundness boundary:
|
||||
|
||||
Contract facts/artifacts should carry explicit provenance. Do not rely on module
|
||||
or catalog convention.
|
||||
- an observer can be assembled after reduction;
|
||||
- observation can arrive through higher-order or dynamically selected code;
|
||||
- unknown external code can hide observation;
|
||||
- absence of a rule-3 redex is not reduction-closed;
|
||||
- exact detection would subsume non-trivial termination/reachability questions.
|
||||
|
||||
Recommended durable provenance classes:
|
||||
A conservative taint pass can define a programming convention, but it cannot
|
||||
justify the parametric or abstraction guarantees previously attached to Views.
|
||||
|
||||
```text
|
||||
Checked -- derived by checked lowering / checker validation
|
||||
Trusted -- asserted by a trusted boundary, e.g. a primitive eliminator API
|
||||
Unchecked -- no abstraction/parametricity guarantee; raw/assumed fact if exposed
|
||||
```
|
||||
### Flow checking only checks represented flow
|
||||
|
||||
The correct granularity is per exported View fact, not per module. A single
|
||||
module may contain checked definitions, trusted eliminators, and unchecked raw
|
||||
helpers.
|
||||
The checker sees frontend-emitted value, application, and requirement nodes. It
|
||||
can check consistency among those nodes, but it cannot establish that the graph
|
||||
faithfully represents every use performed by the opaque executable payload.
|
||||
This is useful artifact validation, not whole-program typing.
|
||||
|
||||
## Controlled intensionality
|
||||
## Retained contract
|
||||
|
||||
Raw intensionality should be tracked by dependency/provenance, not syntax-only.
|
||||
The reduced checker may soundly claim only:
|
||||
|
||||
- Direct `triage` / arbitrary `t` eliminator use is raw intensional capability.
|
||||
- Trusted eliminators expose controlled observation and do not taint clients.
|
||||
- Calling unchecked/untrusted code taints the caller for parametricity purposes.
|
||||
- Constructors/literals are not automatically tainting unless they expose raw
|
||||
inspection power.
|
||||
1. View, node, and program envelopes satisfy their declared data schemas.
|
||||
2. Explicit monomorphic View facts are propagated consistently through the
|
||||
represented application graph.
|
||||
3. A `Guarded` View causes its executable predicate to run at represented
|
||||
boundaries, and guard failure prevents checked execution.
|
||||
4. Content-addressed references prevent an attached View artifact from silently
|
||||
drifting to a different stored object.
|
||||
|
||||
Parametric checked mode rejects annotated definitions whose derivation depends
|
||||
on raw/untrusted intensionality, while trusted facts may describe raw internals
|
||||
behind explicit contracts.
|
||||
Items 1, 2, and 4 establish metadata integrity, not semantic membership in an
|
||||
unguarded View. Item 3 is the only retained mechanism that observes an ordinary
|
||||
runtime value.
|
||||
|
||||
## Trusted eliminator kernel
|
||||
## Code direction
|
||||
|
||||
First trusted observation capabilities should be the smallest useful kernels:
|
||||
The initial rollback therefore:
|
||||
|
||||
```text
|
||||
matchBool : forall r. r -> r -> Bool -> r
|
||||
matchMaybe : forall a r. r -> (a -> r) -> Maybe a -> r
|
||||
matchList : forall a r. r -> (a -> List a -> r) -> List a -> r
|
||||
```
|
||||
- removes View-variable instantiation, substitution, and unification from the
|
||||
portable checker;
|
||||
- rejects `Var`, `Forall`, and `Exists` as checker inputs while reserving
|
||||
their legacy tags for deterministic decoding;
|
||||
- removes the frontend raw-intensionality taint pass;
|
||||
- removes polymorphic stdlib annotations and value-level View facts;
|
||||
- retains monomorphic View flow, artifact plumbing, diagnostics, and executable
|
||||
guards.
|
||||
|
||||
Derived functions should be checked against these trusted capabilities where
|
||||
possible. Raw recursive kernels and other code
|
||||
that passes through fixed-point/intensional machinery should publish explicit
|
||||
`Trusted` facts rather than being treated as checked.
|
||||
|
||||
Current stdlib shape:
|
||||
|
||||
```text
|
||||
Checked annotations where the body checks through trusted capabilities:
|
||||
maybeMap : forall a b. (a -> b) -> Maybe a -> Maybe b
|
||||
maybeBind : forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
|
||||
maybeOr : forall a. a -> Maybe a -> a
|
||||
|
||||
Trusted value-level facts for raw/recursive stdlib boundaries:
|
||||
headMaybe / lastMaybe / nthMaybe
|
||||
append / map / filter / foldl / foldr
|
||||
length / reverse / snoc / count / all? / any? / intersect
|
||||
take / drop / splitAt / concatMap / find / partition / zipWith
|
||||
string/list-byte helpers such as strLength, startsWith?, lines, words
|
||||
```
|
||||
|
||||
Do not assign total contracts to partial APIs such as:
|
||||
|
||||
```text
|
||||
head : List a -> a
|
||||
```
|
||||
|
||||
Prefer `headMaybe : List a -> Maybe a`, or later introduce `NonEmptyList a`.
|
||||
|
||||
## Implementation order
|
||||
|
||||
Most-correct tractable path:
|
||||
|
||||
1. Add contract provenance to the Haskell View model and portable artifacts. ✅
|
||||
2. Preserve provenance through module exports/imports/re-exports. ✅
|
||||
3. Teach checker environments to distinguish checked vs trusted facts. ✅
|
||||
4. Add trusted stdlib eliminator facts. ◐ initial value-level `viewFacts` landed for `matchBool`, `matchMaybe`, `matchList`; Haskell trusted catalog removed
|
||||
5. Add parametric-mode dependency/effect checking. ◐ local raw-dependency and unchecked-import rejection landed
|
||||
6. Annotate/publish derived stdlib Views at the right provenance. ◐ checked `maybeMap`/`maybeBind`/`maybeOr`; trusted value-level facts for recursive list combinators
|
||||
|
||||
Avoid introducing implicit trusted catalogs before provenance exists; that would
|
||||
create semantics that later need to be unwound.
|
||||
Further simplification should treat unguarded structural Views as descriptive
|
||||
labels. If stronger guarantees are desired later, they require an operational
|
||||
mechanism such as runtime recognizers/seals or a genuinely restricted language
|
||||
whose evaluator enforces the restriction. Metadata provenance alone is
|
||||
insufficient.
|
||||
|
||||
Reference in New Issue
Block a user