diff --git a/README.md b/README.md index 682d671..cf5105e 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ The subset is the part of TypeScript whose value is fixed by its source: literal ## Status -Every part of the mechanism has a normative draft under `spec/`. One identifier vocabulary covers them (`S-*` for shape rules, `F-*` for fold rules). A decision-point inventory of 112 rows cites those rules and is gated in CI. A reference implementation covers J1 to J3 and revival; `packages/reference/CAVEATS.md` says what it does not. chant is cross-checked against it from the published package, on the fixtures and on chant's whole example corpus. Fixture coverage is 136 of 139 rules; `spec/fixtures/UNCOVERED.md` lists the rest with a reason each and may only shrink. +Every part of the mechanism has a normative draft under `spec/`. One identifier vocabulary covers them (`S-*` for shape rules, `F-*` for fold rules). A decision-point inventory of 112 rows cites those rules and is gated in CI. A reference implementation covers J1 to J3 and revival; `packages/reference/CAVEATS.md` says what it does not. The published chant package is cross-checked against it over the fixtures and chant's whole example corpus. Fixture coverage is 136 of 139 rules; `spec/fixtures/UNCOVERED.md` lists the rest with a reason each and may only shrink. ## Layout diff --git a/paper/discussion.md b/paper/discussion.md index 0d86e84..1b9c601 100644 --- a/paper/discussion.md +++ b/paper/discussion.md @@ -16,7 +16,7 @@ Nothing answers "will this produce the same output tomorrow" short of declining to run the source. A run returns a value and says nothing about where the value came from, so no inspection of the artifact recovers the difference. The security consequence is real and downstream. A build that -reproduces from source alone is one that never executed the source. Pitching +reproduces from source alone is one whose source never ran. Pitching it the other way round invites a substitution that does not hold. ## What is unresolved @@ -35,7 +35,7 @@ A specification that presented these as designed would be easier to read and les The identity theorem is the paper's center, so here is what would break it. Three things would. -**A single fold/run disagreement on a mixed build.** The differential requires identical errors and byte-identical output for every corpus entry, including the twelve with at least one file that falls back. One disagreement there is either a bug in the fixpoint or a gap in the argument, and the entry would name itself. +**A single fold/run disagreement on a mixed build**. The differential requires identical errors and byte-identical output for every corpus entry, including the twelve with at least one file that falls back. One disagreement there is either a bug in the fixpoint or a gap in the argument, and the entry would name itself. **An entity reachable by two paths with different verdicts.** The theorem's case analysis rules this out given `F-Memo` and `F-Count`. Two implementation choices would produce it anyway: memoising per referrer instead of per build, or invoking a composite once per member access. The corpus would not necessarily catch either. diff --git a/paper/draft.md b/paper/draft.md index 686e7ff..65d1043 100644 --- a/paper/draft.md +++ b/paper/draft.md @@ -6,19 +6,19 @@ date: "Draft for comment, September 2026" ## Abstract -Infrastructure and build configuration is increasingly written in a general-purpose language, and then must not be run, because a build that executes its own configuration has output nobody can reproduce or audit line by line. The usual answer is a configuration language, total by construction, in which unsupported source is a syntax error. This paper specifies and implements a different answer. A fragment of TypeScript is carved out whose value is fixed by its source; source inside the fragment is reduced to data without executing it; source outside it falls back to real execution; and the two paths are required to agree. This is offline partial evaluation with a binding-time analysis, the shape classifier being the analysis and the reducer the specializer. The operation is called folding, after constant folding: the one classical technique that produces a build-time value without executing the program, expression-local where this reduces a whole file. Fallback from static evaluation to execution is known, per call site in compile-time function execution and per page in static site rendering. What is new is per-file granularity with object identity shared across the boundary, and the bidirectional fixpoint that keeps a shared entity from becoming two objects. We give the specification as a grammar and four judgments with named rules, a reference implementation written from the text, a second evaluator in Rust for the profile that needs no JavaScript runtime, and a conformance suite that a production system passes beside both. Over the 467 files of that system's corpus the reference and the production system agree on every comparable file, and again over a project nobody on the team maintains. +Infrastructure and build configuration is increasingly written in a general-purpose language, and then must not be run, because a build that executes its own configuration has output nobody can reproduce or audit line by line. The usual answer is a configuration language, total by construction, in which unsupported source is a syntax error. This paper specifies and implements a different answer. A fragment of TypeScript is carved out whose value is fixed by its source. Source inside the fragment is reduced to data without executing it, and outside it falls back to real execution; the two paths are required to agree. This is offline partial evaluation with a binding-time analysis, the shape classifier being the analysis and the reducer the specializer. The operation is called folding, after constant folding: the one classical technique that produces a build-time value without executing the program, expression-local where this reduces a whole file. Fallback from static evaluation to execution is known already, with compile-time function execution deciding per call site and static site rendering per page. What is new is per-file granularity with object identity shared across the boundary, and the bidirectional fixpoint that keeps a shared entity from becoming two objects. We give the specification as a grammar and four judgments with named rules, a reference implementation written from the text, a second evaluator in Rust for the profile that needs no JavaScript runtime, and a conformance suite that a production system passes beside both. Over the 467 files of that system's corpus the reference and the production system agree on every comparable file, and again over a project nobody on the team maintains. ## 1. Introduction -Configuration as data is auditable: every value traces to a line of source and the same file gives the same artifact anywhere. Configuration as code is expressive, with types and refactoring in a language people already know. Existing designs pick one. A configuration language gives up the general-purpose language's libraries and tools, and a program that emits configuration gives up auditability, because the graph exists only as the output of a run. +Configuration as data is auditable: every value traces to a line of source and the same file gives the same artifact anywhere. As code, configuration is expressive: types and refactoring come with a language people already know. Existing designs pick one. Choosing a configuration language gives up the general-purpose language's libraries and tools, and a program that emits configuration gives up auditability, because the graph exists only as the output of a run. -A fragment of an existing language promises both. Defining the fragment is routine; defining its edge is the work. A total language never has to say what happens to source it cannot evaluate, because that source does not compile. A system with a fallback must say it, and three obligations follow. +A fragment of an existing language promises both. Defining the fragment is routine; its edge is the work. A total language never has to say what happens to source it cannot evaluate, because that source does not compile. A system with a fallback must say it, and three obligations follow. The two paths must agree. Folding a file and running it must be observationally equivalent at a fixed binding of build parameters, which means stating what still executes when a file folds: none of its own statements, but the constructor a name resolves to. The decision must be total per unit. A file folds entirely or runs entirely, since a partly folded namespace is a half-built object graph. -Identity must survive the boundary. If one file folds and another runs, and both refer to an entity the first produced, the build holds two objects for one entity. Compile-time function execution copies values across its boundary and a whole-program partial evaluator has a single heap; only a per-unit decision over a shared object graph has the problem. The answer is a fixpoint over the module graph closed under two edges, a running file tainting what it imports and a file whose objects were captured tainting the capturer, with a third edge through calls. We found no precedent for it. +Identity must survive the boundary. If one file folds and another runs, and both refer to an entity the first produced, the build holds two objects for one entity. Compile-time function execution copies values across its boundary and a whole-program partial evaluator has a single heap; only a per-unit decision over a shared object graph has the problem. The answer is a fixpoint over the module graph closed under two edges, a running file tainting what it imports and a file whose objects were captured tainting the capturer, with a third edge through calls. No precedent for it was found. We provide the specification, versioned and tagged. A reference implementation is written from its text, covering the expression layer through the fixpoint, and a second evaluator in Rust serves the profile without a runtime and compiles to a WebAssembly module with no imports. A conformance suite holds every rule to a fixture and every fixture to a real rule. The measurements come from chant, the production system the subset was extracted from. Rule identifiers such as `F-Total` name rules of the specification; appendix A lists the ones used here, and appendix B the artifacts every number was taken from. @@ -51,9 +51,9 @@ Two statement-level grammars govern what may appear inside a function the reduce The subset has one definition and two consumers. A lint pass reads it without a binding resolver or a registry; an evaluator reads it with both. They will disagree, and the specification constrains how. -If evaluation succeeds, classification accepts, with two exceptions. The classifier is flow-insensitive, so it requires every branch of a short-circuiting operator to be admissible where the evaluator reduces only the taken one, and `false && f()` is a lint error on source that reduces cleanly. And the classifier takes the intrinsic registry as an optional parameter, so without one a call form the registry would admit is refused. +If evaluation succeeds, classification accepts, with two exceptions. The classifier is flow-insensitive, so it requires every branch of a short-circuiting operator to be admissible where the evaluator reduces only the taken one, and `false && f()` is a lint error on source that reduces cleanly. The other exception comes from the intrinsic registry being an optional parameter of the classifier, so without one a call form the registry would admit is refused. -The direction is chosen for its cost. A classifier that accepts too much produces a fallback the author learns about from a per-file decision line. A classifier that rejects too much produces an error on correct source, and a lint that cries wolf gets disabled. The classifier is also how a downstream tool asks whether a file will reduce without reducing it, and that answer must be safe to act on. +The direction is chosen for its cost. Accepting too much produces a fallback the author learns about from a per-file decision line. Rejecting too much produces an error on correct source, and a lint that cries wolf gets disabled. A downstream tool also asks the classifier whether a file will reduce without reducing it, and that answer must be safe to act on. Twelve divergences run the permitted way, and the specification enumerates them, because a claim that two analyses disagree in one direction is only checkable against the list. @@ -76,9 +76,9 @@ In every row the classifier decides from syntax while the evaluator consults som ### 2.4 The per-file verdict -Evaluating a single file yields either a reduction with a complete export namespace, or a fallback with a located reason. The verdict is total per file. Every fallback is reported, since an unreported one is indistinguishable from a reduction and the no-execution guarantee becomes unauditable; the reason names the construct and its position, and a failure inside a called function is re-anchored at the call site. +Evaluating a single file yields either a reduction with a complete export namespace, or a fallback with a located reason. It is total per file. Every fallback is reported, since an unreported one is indistinguishable from a reduction and the no-execution guarantee becomes unauditable; the reason names the construct and its position, and a failure inside a called function is re-anchored at the call site. -The verdict is parameterized by an isolation mode with three values. The default, `open`, executes no project code. Under `isolated`, a reduction that would have to invoke project-owned code falls back. Under `executing`, the one opt-in, a project function whose body cannot be reduced is invoked; the fold then carries what a run would have computed in the folding process. Section 6.4 records how this mode came to exist. The verdict is therefore not a pure function of the source. +The verdict is parameterized by an isolation mode with three values. The default, `open`, executes no project code. Under `isolated`, a reduction that would have to invoke project-owned code falls back. The one opt-in, `executing`, invokes a project function whose body cannot be reduced; the fold then carries what a run would have computed in the folding process. Section 6.4 records how this mode came to exist. The verdict is therefore not a pure function of the source. All of this is a proposal. The fixpoint makes it final. @@ -88,7 +88,7 @@ Per-file partial evaluation is unsound when values have identity. Suppose file A The fixpoint closes the tentative verdicts under two edges. The forward edge runs along imports; a running file taints what it imports, because its real import would construct what a folded copy already holds. Along captures runs the backward edge; a file whose objects were captured taints the capturer, because the instance the capturer holds is no longer the one the build collects. Calls carry a third, since a project-local function whose call returns a live object records the same capture. Seeded with every file that would not fold alone, the closure is a least fixpoint over a finite set. Two supporting rules make it sound: each file is evaluated at most once per build, and within a file a call reached through several member accesses is invoked once; without them a capture would record an edge to a copy. -Two consequences look like defects. A leaf fix buys nothing while an importer still falls back, and this was first observed as coverage falling after a widely imported file was made reducible. And a file's verdict is not a property of its own source, because through the backward edge a file that reduces cleanly can be forced back by something that captured one of its objects and then fell back. The second places an obligation on reporting: the reason must be able to say that a file fell back because another did and captured from it. +Two consequences look like defects. A leaf fix buys nothing while an importer still falls back, and this was first observed as coverage falling after a widely imported file was made reducible. A file's verdict is also not a property of its own source, because through the backward edge a file that reduces cleanly can be forced back by something that captured one of its objects and then fell back. The second places an obligation on reporting: the reason must be able to say that a file fell back because another did and captured from it. ### 2.6 A worked example @@ -117,9 +117,19 @@ The fixpoint seeds with the one failed file. The forward edge taints `shared-con ### 2.7 What a host supplies -A host provides seven things: the classes whose instances are entities and how they expose attributes; an intrinsic registry; an allowlist of authoring helpers; a trust set of packages; a registration form that makes a project-defined factory interpretable; and rules over the folded values, under a contract of their own. A registered call is admitted only if it is a pure function of its arguments and invoking it at fold time is indistinguishable from invoking it during a run, and revival always invokes the function the file imported. +A host provides seven things. -Into a package, reduction goes only through a closed allowlist checked by name and by the provenance of the binding. Into a project file, reduction proceeds whenever the callee's body is itself in the subset, with no allowlist. The asymmetry follows the trust boundary. Package code is already loaded and executed by the build before reduction begins, to obtain the serializers and lint rules the build cannot run without, so admitting a call into it costs no execution the process was not already performing. Project code is the untrusted input and is admitted only when it can be evaluated without being executed, which a syntactic check of the callee's body decides and an allowlist could not. +- the classes whose instances are entities +- how those classes expose attributes +- an intrinsic registry +- an allowlist of authoring helpers +- a trust set of packages +- a registration form that makes a project-defined factory interpretable +- rules over the folded values, under a contract of their own + +A registered call is admitted only if it is a pure function of its arguments and invoking it at fold time is indistinguishable from invoking it during a run, and revival always invokes the function the file imported. + +Into a package, reduction goes only through a closed allowlist checked by name and by the provenance of the binding. For a callee in a project file, reduction proceeds whenever the callee's body is itself in the subset, with no allowlist. The asymmetry follows the trust boundary. Package code is already loaded and executed by the build before reduction begins, to obtain the serializers and lint rules the build cannot run without, so admitting a call into it costs no execution the process was not already performing. The untrusted input is project code. It is admitted only when it can be evaluated without being executed, and a syntactic check of the callee's body decides that where an allowlist could not. The generality is over host vocabularies and not over languages. The syntax is TypeScript's and the operator semantics are ECMAScript's, with two departures the specification names. @@ -148,11 +158,11 @@ Reduction yields a value from a closed domain. Six cases are ordinary JSON: scal An envelope is a finished value. An attribute reference is the shape the runtime object serializes to, and the value it denotes does not exist at build time on either path. Revival replaces five of the six, resolving each name through the folding file's own imports and invoking the real function or constructor, and only the attribute reference reaches a serializer; an implementation that emitted a resource envelope has produced wrong output, which a differential across a real corpus caught before the rule was written. -Validity is position-dependent. Inside the arguments of an intrinsic or a helper an attribute reference is refused, because the receiving function inspects what it is given and a look-alike plain object makes it produce wrong output. One position out, in a construction's props, the same value passes, because there the serializer resolves it by name. So the rule is part of the domain. +Validity is position-dependent. Inside the arguments of an intrinsic or a helper an attribute reference is refused, because the receiving function inspects what it is given and a look-alike plain object makes it produce wrong output. One position out, in a construction's props, the same value passes, because there the serializer resolves it by name. The rule therefore belongs to the domain's definition. Liveness is what makes the identity rules statable. A value carries a live object when it or anything reachable through plain objects and arrays has a prototype other than the plain ones, is a function, or carries a host's marker. Live objects reached through cross-file resolution pass through revival untouched, because a generic walk would rebuild them as plain copies and destroy the identity the fixpoint preserves. -Three smaller rules complete the domain. A callable is in the domain and is never a value: `f(x)` reduces where `{ resolver: f }` does not, because nothing can serialize a function. Constructor arity is contractual, so when the argument list is not a props object optionally followed by attributes, the positional list is authoritative. And absence has two forms, `undefined` in a property position being dropped at emission and in an array position becoming `null`, which platforms act on. +Three smaller rules complete the domain. A callable is in the domain and is never a value: `f(x)` reduces where `{ resolver: f }` does not, because nothing can serialize a function. Constructor arity is contractual, so when the argument list is not a props object optionally followed by attributes, the positional list is authoritative. Absence has two forms as well, since `undefined` is dropped at emission in a property position and becomes `null` in an array position, and platforms act on the difference. ### 3.2 Three evaluation modes @@ -168,9 +178,9 @@ Three capabilities follow, and neither a syntax linter nor a configuration langu Synthesis with no execution. A file in the subset becomes its artifact by being read, so the artifact is a function of the source and the build-parameter binding, and the same file yields the same artifact in any evaluator in any language. The user meets the fold as a lint that says while they type whether the file is data and which line makes it not data; that lint is the shape classifier, and it needs no evaluator. -Rules over values. A type can say a port is out of range. It cannot say that two fields of one resource contradict each other, or that a resource in one file makes a resource in another incoherent, because it lacks the values of every file in the build before anything is emitted. The fold has them. The specification defines no rule, only the contract a rule runs under: what it sees and when it runs, and what a finding carries. Rules over the emitted artifact need no fold; rules over the declared values do, and there references are still references and an entity is one entity wherever it is used, with nothing executed. The contract states as a property that findings are the same whether the build folded the file or ran it, and a finding is data carrying its rule and subject with a path into the value, which is what lets a person or an agent act on it. +Rules over values. A type can say a port is out of range. It cannot say that two fields of one resource contradict each other, or that a resource in one file makes a resource in another incoherent, because it lacks the values of every file in the build before anything is emitted. The fold has them. The specification defines no rule, only the contract a rule runs under: what it sees and when it runs, and what a finding carries. The emitted artifact can be checked without a fold, while rules over the declared values need one; there references are still references and an entity is one entity wherever it is used, with nothing executed. The contract states as a property that findings are the same whether the build folded the file or ran it, and a finding is data carrying its rule and subject with a path into the value, which is what lets a person or an agent act on it. -Round-trip generation. A generator turns data into source, and composed with the fold it turns an existing artifact or a live system into source that folds back to what it came from. A generator decides what each value is, and each decision needs a source form the subset can express and the fold can reverse: a value that is another resource's attribute is `bucket.Arn`, and a repetition across forty resources is one `const` spread where it is used. YAML cannot express either, and a configuration language can only by leaving the artifact's own shape. The specification states the completeness half as a rule, one source form per case of the domain, and holds a generator to the fidelity half through a fixture kind whose input is a namespace as data. +Round-trip generation. A generator turns data into source, and composed with the fold it turns an existing artifact or a live system into source that folds back to what it came from. Deciding what each value is falls to the generator, and each decision needs a source form the subset can express and the fold can reverse: a value that is another resource's attribute is `bucket.Arn`, and a repetition across forty resources is one `const` spread where it is used. YAML cannot express either, and a configuration language can only by leaving the artifact's own shape. The specification states the completeness half as a rule, one source form per case of the domain, and holds a generator to the fidelity half through a fixture kind whose input is a namespace as data. The first two need only `data-host`. None of the three needs the fallback or the fixpoint; those exist so that source outside the subset can still be built by an implementation that has a runtime, and they are what this paper is about. @@ -186,7 +196,7 @@ Proof sketch. If `g ∉ T(B)`, then `g` folded and `e` is the object in its name The sketch assumes memoisation and the once-per-call-site rule hold in the implementation, that the run path yields one module instance per file, and that `T(B)` exists and is finite. The first prose statement of the forward edge had its direction reversed; writing the successor relation as an operator caught it. -The reference computes `T(B)` by a worklist from the seed, and whole-build fixtures hold it to each edge: a file that seeds with no edge; the forward edge into an import; the backward edge two hops out through a capture; and a control, the file nothing reaches, which must still fold. Falling back on everything satisfies the claim, so the control is the assertion that discriminates. chant answers the same fixtures, and the two agree on every file's final verdict and its verdict before taint, and for each casualty on the file the edge came from and the rule. +The reference computes `T(B)` by a worklist from the seed, and whole-build fixtures hold it to each edge. One seeds with no edge, and two take the forward edge into an import and the backward edge two hops out through a capture. The fourth is a control that nothing reaches and that must still fold. Falling back on everything satisfies the claim, so the control is the assertion that discriminates. chant answers the same fixtures, and the two agree on every file's final verdict and its verdict before taint, and for each casualty on the file the edge came from and the rule. ### 5.2 The permitted direction of divergence @@ -202,7 +212,7 @@ Corollary. Every disagreement outside the two exceptions costs coverage and neve For every value `v` the domain admits, `fold(generate(v)) = v` in `data-host`, and equals the revived value in `full`. Completeness is a rule, a table with one source form per case of the closed domain, each folding to its value by the rule the table cites. Fidelity is an obligation on each generator, that its output is in the subset and folds to its input, tested through a fixture kind whose input is a namespace as data. The reference and the Rust evaluator each carry the smallest generator that makes the property testable, and the four round-trip fixtures pass on both. -Mechanisation is declined for the submission. The first property has the argument above and three executed artifacts: the differential over every corpus entry including the mixed ones; an adversarial build that fires both taint edges; and a second implementation held to whole-build fixtures. The second has the shared-classifier construction and the enumerated table with a fixture per row. +Mechanisation is declined for the submission. The first property has the argument above and three executed artifacts. They are the differential over every corpus entry including the mixed ones, an adversarial build that fires both taint edges and a second implementation held to whole-build fixtures. The second has the shared-classifier construction and the enumerated table with a fixture per row. ## 6. Evaluation @@ -216,7 +226,7 @@ chant builds every corpus entry twice, folded and run, and requires identical er |---|---|---|---|---| | first mixed-entry run, chant 0.65.0 | 107 | 95 | 12 | 0 | -One entry is nine files, each named for a resolution-time decision point and citing the inventory row that governs it. Four make the fixpoint fire on purpose, and section 2.6 walked through them; the entry asserts each verdict by name and the differential holds across it. +One entry is nine files, each named for a resolution-time decision point and citing the inventory row that governs it. Four make the fixpoint fire on purpose, and section 2.6 walked through them; each verdict is asserted by name and the differential holds across it. ### 6.2 The execution boundary @@ -263,7 +273,7 @@ The last row crosses a major. Specification 2.0 narrowed the call rule so that a A file is comparable when nothing disarmed either implementation before the comparison. Four things did at the first pin and one remains, the single file that imports a package the reference's host cannot load. Two were limits of chant's entry point, 52 files reading a host export that needed a lexicon list and 19 in entries with build parameters the entry could not be given, until chant `0.71.0` took both; one held 290 files reaching a host factory until the reference implemented the call rule; the last held 68 files calling a package export outside a declarator, until specification `1.6` wrote chant's behavior into the declarator and call rules. -On 466 files nobody wrote for the purpose the two implementations agree on every verdict, and on the 310 that fold on both sides the namespaces are structurally identical, entity class and properties included. A limit is an over-approximation, so the one file outside the set may hide a disagreement. And chant is the implementation the text was extracted from, so this is agreement between chant and a rewrite written from the text rather than between two independent readings. +On 466 files nobody wrote for the purpose the two implementations agree on every verdict, and on the 310 that fold on both sides the namespaces are structurally identical, entity class and properties included. A limit is an over-approximation, so the one file outside the set may hide a disagreement. chant is also the implementation the text was extracted from, so this is agreement between chant and a rewrite written from the text rather than between two independent readings. Every entry above was written by the people who wrote the folder. A public project that depends on chant and is not maintained by us runs beside it at a pinned revision, each directory with a configuration file an entry. A second project is private and outside the record; run once locally the same way, it agreed on all 12 of its comparable files. @@ -271,9 +281,9 @@ Every entry above was written by the people who wrote the folder. A public proje |---|---|---|---|---|---| | an Infisical deployment | 6 | 31 | 13 | 13 | 5 | -The host limit is large there because the project was written against an older chant, so a package export the pinned release no longer has disarms every file that imports it. The first run found one disagreement: a file whose only declarator called a project function that reads the process environment. chant folded it by invoking the function at fold time, and the fold's output carried whatever the folding shell held. The specification routes a declared function to the project-local call rule, whose ambient read is a pointed rejection, so the file runs. chant `0.72.3` does the same, and specification `1.8` made the old behavior the opt-in mode of section 2.4. +The host limit is large there because the project was written against an older chant, so a package export the pinned release no longer has disarms every file that imports it. The first run found one disagreement: a file whose only declarator called a project function that reads the process environment. chant folded it by invoking the function at fold time, and the fold's output carried whatever the folding shell held. The specification routes a declared function to the project-local call rule, whose ambient read is a pointed rejection, so the file runs. Since `0.72.3` chant does the same, and specification `1.8` made the old behavior the opt-in mode of section 2.4. -The runs found things on the way. The first run had no host and compared seven files, none of which folded on either side. With a host it found a reference bug, the capture walk stopping at an entity's boundary; a specification defect, a rule that read an instance as pre-built that no rule built; and 21 files on which the harness had asked the two implementations different questions. The second exposed 79 more files and 10 disagreed, all in the harness or the reference. The third implemented the call rule and exposed 290, among the fallout a liveness test that was prototype-only where the host's marker was the rule. The fourth settled the last 68 with a rule written to what chant does, after a first draft folded five shapes chant refuses and the fixture cross-check caught it before the corpus could. +The runs found things on the way. The first run had no host and compared seven files, none of which folded on either side. With a host it found a reference bug (the capture walk stopping at an entity's boundary), a specification defect (a rule that read an instance as pre-built that no rule built) and 21 files on which the harness had asked the two implementations different questions. The second exposed 79 more files and 10 disagreed, all in the harness or the reference. The third implemented the call rule and exposed 290, among the fallout a liveness test that was prototype-only where the host's marker was the rule. The fourth settled the last 68 with a rule written to what chant does, after a first draft folded five shapes chant refuses and the fixture cross-check caught it before the corpus could. ### 6.5 What the specification found @@ -304,7 +314,7 @@ Separate partial evaluation. Heldal and Hughes treat a program as modules that c Partial evaluation and binding-time analysis. The shape classifier is a binding-time analysis and the fold is the specializer in the sense of Jones, Gomard and Sestoft. The per-file verdict with taint is closer to an online decision over a coarse unit, and forcing a folded file back to run is a coarse lift. Multi-stage programming makes staging explicit instead of inferring it. -Partial evaluation of JavaScript. Prepack evaluates a bundle's global code, captures the heap, and emits a residual program that rebuilds it, with abstract values for what it cannot evaluate and always one program. Its residual-heap visitor emits a shared object once, which is identity within one heap, the case a per-file split gives up. +JavaScript partial evaluation. Prepack evaluates a bundle's global code, captures the heap, and emits a residual program that rebuilds it, with abstract values for what it cannot evaluate and always one program. Its residual-heap visitor emits a shared object once, which is identity within one heap, the case a per-file split gives up. Per-unit static or executed. Next.js decides per page whether to prerender or render on request, from a marker the author writes, and Astro's hybrid mode is the same shape. Prerendered and served pages share no runtime objects, and no agreement obligation is stated. @@ -321,7 +331,7 @@ Total configuration languages. | Nickel | yes | constrained to commutative | error | | Pkl | yes | no | error | -Every row answers unsupported source with an error and so has neither an agreement problem nor an identity problem; the fallback is what removes that simplification. Pkl and CUE give a platform typed, deterministic configuration that emits YAML or JSON, and Pkl puts value constraints in the type where this work puts them in a pass over folded values. Neither makes the authoring surface the artifact's own shape: a Pkl or CUE file is a second grammar pointed at the spec, where a typed object literal is the spec with its keys unquoted. Pkl's bindings for other languages shell out to an evaluator binary; `data-host` is what lets an evaluator for this subset be a library in the platform's own language, or a WebAssembly module inside it. +Every row answers unsupported source with an error and so has neither an agreement problem nor an identity problem; the fallback is what removes that simplification. Pkl and CUE give a platform typed, deterministic configuration that emits YAML or JSON, and Pkl puts value constraints in the type where this work puts them in a pass over folded values. Neither makes the authoring surface the artifact's own shape: a file in either language is a second grammar pointed at the spec, where a typed object literal is the spec with its keys unquoted. For other languages Pkl's bindings shell out to an evaluator binary; `data-host` is what lets an evaluator for this subset be a library in the platform's own language, or a WebAssembly module inside it. Infrastructure tools. CDK, Pulumi and Alchemy execute the program that builds the resource graph. Terraform evaluates HCL with functions against state. Formae compiles Pkl to data. @@ -331,7 +341,7 @@ Claimed as new. Per-file partial evaluation with a fallback is precedented in sh Costs. Section 2.5 named two. A third is that coverage is not the security-relevant number: a file that folds executes none of its own code either way, so partial coverage does nothing for the files that matter, and isolating the fallback is what bounds the remainder, which is why isolation is a mode of the verdict rather than a deployment detail. A fourth is that security is the cheaper property and the claim is not pitched there. A sandbox answers it well. Nothing but declining to run the source answers whether the output repeats, since a run returns a value and says nothing about where the value came from. -Unresolved. Three places where the implementation settled a question by accident, recorded as such. The classifier is flow-insensitive, and making it flow-sensitive means writing an evaluator inside a lint rule. One member name, `.step`, is admitted after a call because one idiom uses it, and no boundary stated in the rule admits it and excludes the next member somebody needs. And one class of registered call is evaluated at fold time because its usual use coerces the result to a string. +Unresolved. Three places where the implementation settled a question by accident, recorded as such. The classifier is flow-insensitive, and making it flow-sensitive means writing an evaluator inside a lint rule. One member name, `.step`, is admitted after a call because one idiom uses it, and no boundary stated in the rule admits it and excludes the next member somebody needs. Last, one class of registered call is evaluated at fold time because its usual use coerces the result to a string. What would falsify the identity property. A fold-run disagreement on a mixed build. An entity reachable by two paths with different verdicts, which memoising per referrer or invoking a composite once per member access would produce and the corpus would not necessarily catch. A sharing relationship the capture set does not record; nothing currently searches for a third route into another file's objects. diff --git a/paper/enables.md b/paper/enables.md index 5b7135c..7553733 100644 --- a/paper/enables.md +++ b/paper/enables.md @@ -4,7 +4,7 @@ Draft for #87. The other sections say what the fold is. This one says what it is ## Synthesis with no execution -A file in the subset becomes its artifact by being read. Nothing runs, so the artifact is a function of the source and the build-parameter binding and nothing else. The same file yields the same artifact on any machine and in any evaluator, whatever language the evaluator is written in. A reviewer reading a diff sees exactly what will ship. The user never meets the fold as a mechanism; they meet it as a lint that says at the keystroke whether the file is data and points at the line that makes it not data. That lint is the shape classifier of `grammar.md`, and it needs no evaluator to run. `F-NoOwnExecution` is the rule, and chant's execution-boundary profile (`measurements.md`) is the measurement. +A file in the subset becomes its artifact by being read. Nothing runs, so the artifact is a function of the source and the build-parameter binding and nothing else. Any machine and any evaluator get the same artifact from the same file, whatever language the evaluator is written in. A reviewer reading a diff sees exactly what will ship. The user never meets the fold as a mechanism; they meet it as a lint that says at the keystroke whether the file is data and points at the line that makes it not data. That lint is the shape classifier of `grammar.md`, and it needs no evaluator to run. `F-NoOwnExecution` is the rule, and chant's execution-boundary profile (`measurements.md`) is the measurement. ## Semantic rules over values @@ -12,7 +12,7 @@ A syntax linter sees tokens and can say a key is misspelt. A configuration langu ## Round-trip generation -The fold goes from source to data. A generator goes from data to source. Composed, an existing artifact or a live system becomes source that folds back to exactly what it came from, `fold(generate(v)) = v`. This is where the choice of a general-purpose language stops being taste and becomes correctness. A generator decides what each value is, and each decision needs a source form the subset can express and the fold can reverse. A literal is a literal. A value that is another resource's attribute is `bucket.Arn`, which `F-Eval-Member` step 1 turns back into an attribute reference. A repetition across forty resources is one `const`, spread where it is used, which `F-Eval-Object` folds back to the same forty objects. YAML cannot express the second or the third; a configuration language can, but then the source is no longer the artifact's own shape. chant has three generators through one pipeline and a round-trip suite for one target. The property itself is stated as a forward reference (typescript-as-data#80): every value in the domain has a source form that folds to it, and a generator's output is held to folding to its input. +The fold goes from source to data and a generator goes the other way. Composed, an existing artifact or a live system becomes source that folds back to exactly what it came from, `fold(generate(v)) = v`. This is where the choice of a general-purpose language stops being taste and becomes correctness. A generator decides what each value is, and each decision needs a source form the subset can express and the fold can reverse. A literal is a literal. A value that is another resource's attribute is `bucket.Arn`, which `F-Eval-Member` step 1 turns back into an attribute reference. A repetition across forty resources is one `const`, spread where it is used, which `F-Eval-Object` folds back to the same forty objects. YAML cannot express the second or the third; a configuration language can, but then the source is no longer the artifact's own shape. chant has three generators through one pipeline and a round-trip suite for one target. The property itself is stated as a forward reference (typescript-as-data#80): every value in the domain has a source form that folds to it, and a generator's output is held to folding to its input. ## Which profile each needs diff --git a/paper/introduction.md b/paper/introduction.md index 57299e9..a266645 100644 --- a/paper/introduction.md +++ b/paper/introduction.md @@ -14,7 +14,7 @@ Graceful fallback from static evaluation to execution is not itself new; compile ## The problem -Configuration as data is auditable: every value traces to a line of source, and the build makes no network call and holds no credential. Configuration as code is expressive: types, imports, refactoring, a language people already know. Existing designs pick one. A configuration language gives up the general-purpose ecosystem; a program that emits configuration gives up the property that made data auditable, because the graph exists only as the output of a run. +Configuration as data is auditable: every value traces to a line of source, and the build makes no network call and holds no credential. As code, configuration is expressive: types, imports and refactoring come with a language people already know. Existing designs pick one. Choosing a configuration language gives up the general-purpose ecosystem; a program that emits configuration gives up the property that made data auditable, because the graph exists only as the output of a run. The fragment approach promises both. Its difficulty is not defining the fragment, which is routine, but defining the edge. @@ -22,17 +22,17 @@ The fragment approach promises both. Its difficulty is not defining the fragment A total language never has to answer what happens to source it cannot evaluate, because that source does not compile. A system with a fallback must answer it, and three obligations follow. -**The two paths must agree.** Folding a file and running it must be observationally equivalent, at a fixed build-parameter binding. Stating this precisely means stating what still executes when a file folds: the file's own statements do not, but resolving a name to its real constructor and invoking it does. +**The two paths must agree**. Folding a file and running it must be observationally equivalent, at a fixed build-parameter binding. Stating this precisely means stating what still executes when a file folds: the file's own statements do not, but resolving a name to its real constructor and invoking it does. -**The decision must be total per unit.** A file folds entirely or runs entirely. Partial folding would mean holding a half-built namespace. +**The decision must be total per unit**. A file folds entirely or runs entirely. Partial folding would mean holding a half-built namespace. -**Identity must survive the boundary.** This is the obligation with no precedent we found. If one file folds and another runs, and both refer to an entity the first produced, the build holds two objects for one entity. Attribute references cannot both receive a logical name; a reference to one silently inlines rather than referring. Every comparable system avoids this by construction: compile-time function execution copies values across its boundary, per-page rendering shares no runtime objects, and a whole-program partial evaluator has a single heap. Only a per-unit decision over a shared object graph has the problem at all. +**Identity must survive the boundary**. This is the obligation with no precedent we found. If one file folds and another runs, and both refer to an entity the first produced, the build holds two objects for one entity. Attribute references cannot both receive a logical name; a reference to one silently inlines rather than referring. Every comparable system avoids this by construction: compile-time function execution copies values across its boundary, per-page rendering shares no runtime objects, and a whole-program partial evaluator has a single heap. Only a per-unit decision over a shared object graph has the problem at all. The answer is a fixpoint over the module graph, closed under two edges: a running file taints what it imports, and a file whose objects were captured taints the capturer. A third edge runs through calls rather than imports. ## What we provide -A specification of the subset and its edge, as a grammar and four judgments with identified rules. A reference implementation of the expression layer, written from the specification text. A conformance suite in which every rule is cited by the fixtures that exercise it, and a ledger in which every decision point of a production implementation cites the rule that governs it. And measurements from that production implementation: a differential over 116 corpus entries requiring identical errors and byte-identical output, an execution-boundary measurement, and a build designed to make the fixpoint fire in both directions. +A specification of the subset and its edge, as a grammar and four judgments with identified rules. A reference implementation of the expression layer, written from the specification text. A conformance suite in which every rule is cited by the fixtures that exercise it, and a ledger in which every decision point of a production implementation cites the rule that governs it. We also report measurements from that production implementation: a differential over 116 corpus entries requiring identical errors and byte-identical output, an execution-boundary measurement, and a build designed to make the fixpoint fire in both directions. ## What we do not claim diff --git a/paper/measurements.md b/paper/measurements.md index d3a008a..e63aa72 100644 --- a/paper/measurements.md +++ b/paper/measurements.md @@ -54,11 +54,11 @@ The chant side's `false` is also an unsampled invariant: the run fails unless ev |---|---|---|---| | chant `0.72.5` | 127, of which 65 are whole-build | 135 of 139 | all, on the 120 the pin answers; three wait on the adapter (the counters fixture and the executing pair, both halves in the release), and the four round-trip fixtures skip, chant having no generator | -The 3 rules without a fixture are listed in `spec/fixtures/UNCOVERED.md` with a reason each. All are properties no adapter can observe from verdicts: the host's own module tree, and what a host may vary or must not execute. Provenance has fixtures now. The capability is optional, so they are judged for an adapter that claims it and reported skipped for one that does not. chant claims it since `0.109.0` and passes all five. One disagreement existed between the reference and chant, on an envelope inside a template span. The spec recorded the recommendation, chant-v0.68.0 implemented it, and a fixture now pins it (chant#2349). +The 3 rules without a fixture are listed in `spec/fixtures/UNCOVERED.md` with a reason each. All are properties no adapter can observe from verdicts: the host's own module tree, and what a host may vary or must not execute. Provenance has fixtures now. The capability is optional, so they are judged for an adapter that claims it and reported skipped for one that does not. chant claims it since `0.109.0` and passes all five. One disagreement existed between the reference and chant, on an envelope inside a template span. The recommendation went into the spec, chant-v0.68.0 implemented it, and a fixture now pins it (chant#2349). -**Two profiles.** Spec `1.1` names `full` and `data-host` (F-Profile, F-Profile-DataHost); the second is the specification for an evaluator with no JavaScript runtime, and it is what a platform in another language implements. Fixtures carry profile tags, and 77 of the 134 belong to `data-host`, and the reference judged in that profile passes every one of them. That is a JavaScript implementation passing a profile defined by the absence of JavaScript, so it establishes that the profile is consistent. Whether it is implementable without an engine is what `evaluators/rust` establishes (#86): `tsad-eval`, written from the text in Rust on oxc, passes every fixture tagged for the profile, the four round-trip fixtures among them since it generates as well as folds (F-Val-Source), and agrees with the reference on each; compiled to WebAssembly, with no imports, the same crate passes the same fixtures and agrees with its own binary answer for answer (`rust-wasm-agreement.test.ts`), so the embedded form is the evaluator measured here and not a second one; and over chant's corpus it sits as a third column, both evaluators judged in `data-host` on the same host description: at `chant-v0.109.0` the two agree on all 467 files, and 149 fold on both sides to the same namespace, envelopes included. Writing it found the reference reviving and tainting in a profile that does neither, both fixed in the reference; the corpus report records the column's numbers. +**Two profiles.** Spec `1.1` names `full` and `data-host` (F-Profile, F-Profile-DataHost); the second is the specification for an evaluator with no JavaScript runtime, and it is what a platform in another language implements. Fixtures carry profile tags, and 77 of the 134 belong to `data-host`, and the reference judged in that profile passes every one of them. That is a JavaScript implementation passing a profile defined by the absence of JavaScript, so it establishes that the profile is consistent. Whether it is implementable without an engine is what `evaluators/rust` establishes (#86): `tsad-eval`, written from the text in Rust on oxc, passes every fixture tagged for the profile, the four round-trip fixtures among them since it generates as well as folds (F-Val-Source), and agrees with the reference on each; compiled to WebAssembly, with no imports, the same crate passes the same fixtures and agrees with its own binary answer for answer (`rust-wasm-agreement.test.ts`), so the embedded form is the evaluator measured here and not a second one. Over chant's corpus it sits as a third column, both evaluators judged in `data-host` on the same host description: at `chant-v0.109.0` the two agree on all 467 files, and 149 fold on both sides to the same namespace, envelopes included. Writing it found the reference reviving and tainting in a profile that does neither, both fixed in the reference; the corpus report records the column's numbers. -**Coercion, stated as fixtures.** Thirteen expression fixtures pin the parts of ECMAScript an evaluator in another language has to reproduce bit for bit. Number formatting in template literals is the largest of them (shortest round-trip digits; `1e+21`; `-0` as `0`; a literal beyond 2^53 rounded before it is printed). The others are `+`'s string-or-number dispatch and relational comparison on strings; the logical operators returning an operand; unary coercion and IEEE division; and the one deliberate departure, array spread refusing a string (R10.6). The same family pins that an `undefined`-valued property is present in the folded namespace and travels through a spread, which is what a selective-by-omission consumer reads (#82). Both implementations agree on all thirteen. Their sufficiency is not established by that: the reference is JavaScript and passes them for free, so whether they are enough is known only once an evaluator with no JavaScript engine runs them (#86). +**Coercion, stated as fixtures.** Thirteen expression fixtures pin the parts of ECMAScript an evaluator in another language has to reproduce bit for bit. Number formatting in template literals is the largest of them (shortest round-trip digits; `1e+21`; `-0` as `0`; a literal beyond 2^53 rounded before it is printed). The others are `+`'s string-or-number dispatch and relational comparison on strings; the logical operators returning an operand; unary coercion and IEEE division. The one deliberate departure, array spread refusing a string (R10.6), is pinned as well. The same family pins that an `undefined`-valued property is present in the folded namespace and travels through a spread, which is what a selective-by-omission consumer reads (#82). Both implementations agree on all thirteen. Their sufficiency is not established by that: the reference is JavaScript and passes them for free, so whether they are enough is known only once an evaluator with no JavaScript engine runs them (#86). **What this agreement establishes.** Until #50 the reference implementation's evaluation layer was a *port* of chant's, so agreement on expression-level fixtures was guaranteed by construction rather than observed. It is now written from `grammar.md` §2 and `judgments.md` J1 without consulting chant's source, and the two implementations agree on every fixture, so the comparison is between two codebases rather than one code base with itself. @@ -84,12 +84,12 @@ The 3 rules without a fixture are listed in `spec/fixtures/UNCOVERED.md` with a The `chant-v0.73.0` row crosses a major. Spec `2.0` narrowed F-Call step 5 so that a project-file callee is refused outside `ι = executing`, and spec `2.1` bounded what an entity constructor may do. Neither moved the comparable set or -the agreement. The last row is spec `2.2`, which widened F-Call to a binding +the agreement. In the last row the spec is at `2.2`, which widened F-Call to a binding exported by name and to a same-file call's result read inside an argument. Every file the corpus gained between the two releases is comparable, and every comparable file agrees. -A file is comparable when nothing disarmed either implementation before the comparison started. Four things did so under `chant-v0.70.1`, two under `chant-v0.71.0`, and one remains under spec `1.6`, the single file that imports a package the host cannot load, which is the reference's limit. Each of the others retired for its own reason. Two were limits of chant's entry point rather than of chant, 52 files reading a host data export that `foldProject` could not resolve without a lexicon list and 19 in entries with build parameters it could not be given, until chant#2422 gave it both (#96). Another held 290 files reaching a host factory until the reference implemented F-Call (#109). The final one held 68 files calling a package export outside a declarator; it went when spec `1.6` wrote chant's behavior into F-Declarator and F-Call (#110). +A file is comparable when nothing disarmed either implementation before the comparison started. Four things did so under `chant-v0.70.1`, two under `chant-v0.71.0`, and one remains under spec `1.6`, the single file that imports a package the host cannot load, which is the reference's limit. Each of the others retired for its own reason. Two were limits of chant's entry point rather than of chant, 52 files reading a host data export that `foldProject` could not resolve without a lexicon list and 19 in entries with build parameters it could not be given, until chant#2422 gave it both (#96). Another held 290 files reaching a host factory until F-Call was implemented in the reference (#109). The final one held 68 files calling a package export outside a declarator; the limit went when spec `1.6` wrote chant's behavior into F-Declarator and F-Call (#110). **What this establishes.** On 466 files nobody wrote for the purpose, the two implementations agree on every verdict, and on the 310 that fold on both sides the export namespaces are structurally identical, entity class and properties included. It is agreement between the two that was observed rather than designed; each run since the first has widened the set it is observed on without adding a disagreement, and the fourth, at spec `1.6`, covers every file but one. @@ -107,12 +107,12 @@ The host limit is large there because the project was written against an older c **Found on the way, third run (#109).** Implementing F-Call exposed 290 files, and three things fell out before the comparable set was clean. L6.1 lists a Declarable and a CompositeInstance among live objects and the reference's liveness test was prototype-only, so chant's composite instances, plain objects with a marker, failed step 7; the test now reads the marker the way F-Host-Interface item 1 describes it. The registration declarator `export const N = Composite(fn, "N")` is a function used as a value; the defining module therefore runs while callers interpret the body from source, which is what chant does and what one lexicon example pinned. F-Bind's destructured locals from a composite call had never been bound. What was left over, 68 files, is the fourth run's. -**Found on the way, second run.** Retiring the two limits exposed 79 more files, and 10 of them disagreed before any of it was a disagreement about the mechanism. Five were the harness binding `params` to the module's live export instead of the build's values, which F-Import's first arm forbids. Two were the reference never joining a `../` specifier to the importer's directory, so an import edge went unrecorded and with it a forward taint, and a file chant ran folded; the fix is in `project.ts`. Three were the reference deciding F-Capture only over the produced namespace, where F-Import's text records a capture at the import for any value with identity: a file that reads one string out of an imported object holds no object in its namespace and chant taints it anyway. The reference now does both, and every one of the ten agrees. +**The second run.** Retiring the two limits exposed 79 more files, and 10 of them disagreed before any of it was a disagreement about the mechanism. Five were the harness binding `params` to the module's live export instead of the build's values, which F-Import's first arm forbids. Two were the reference never joining a `../` specifier to the importer's directory, so an import edge went unrecorded and with it a forward taint, and a file chant ran folded; the fix is in `project.ts`. Three were the reference deciding F-Capture only over the produced namespace, where F-Import's text records a capture at the import for any value with identity: a file that reads one string out of an imported object holds no object in its namespace and chant taints it anyway. The reference now does both, and every one of the ten agrees. **The first run.** With no host, the first run compared 7 files and none of them folded on either side, which is agreement by vacuity. With a host it turned up a reference bug, a specification defect and a harness artifact. The bug was F-Capture's walk stopping at an entity's boundary, invisible without a host because an unrevived entity is a plain object; fixed, the reference reproduces `fold-adversarial`'s backward capture edge against a real host for the first time. The defect, #68, was that F-Eval-Ident step 1 read an instance "J2 pre-built" that no rule of J2 built, so the reference refused 22 files chant folds, and F-Prebuild now states the rule. The artifact was 21 files on which the harness had asked the two implementations different questions, now counted under the lexicon-list limit. -Two limits on that. The rewrite's author had read chant's implementation closely while writing the specification from it, so this establishes that the specification is complete enough to implement from, not that a reader who had never seen chant would arrive at the same place. And the agreement covers the expression and single-file layers. It does not cover J3, for the reason the next section gives. +Two limits on that. The rewrite's author had read chant's implementation closely while writing the specification from it, so this establishes that the specification is complete enough to implement from, not that a reader who had never seen chant would arrive at the same place. The other is that the agreement covers the expression and single-file layers and not J3, for the reason the next section gives. **What the whole-build fixtures establish, and against how many implementations.** The reference implements J2's per-file verdict, J3's fixpoint and revival from the specification (#21, #22, #61). Thirty whole-build fixtures assert the verdicts of an entire build rather than the value of one expression, and four fire a taint edge on purpose: @@ -127,17 +127,17 @@ The control is the one with teeth. An implementation that falls back on every fi Until `chant-v0.70.1` chant had no entry that took a set of files, so none of these were answerable there: a taint edge does not exist inside a single file. chant#2408 added one, and the nine fixtures that need no host now run against both implementations. They agree on every file's final verdict and its tentative verdict, and for every taint casualty they agree on the file the edge came from and on which rule it was. Since `chant-v0.72.0` the fixtures that name a host reach chant too (chant#2438), and a skip fails the suite. -Two agreements to name. chant classifies the capturing sibling as reached by a capture rather than an import, the distinction chant#2406 was filed for. And a file whose only tie to another is a call returning computed plain data folds in both, which is `F-Identity`'s entity test holding in an implementation that has never read it. +Two agreements to name. chant classifies the capturing sibling as reached by a capture rather than an import, the distinction chant#2406 was filed for. The other is a file whose only tie to another is a call returning computed plain data, which folds in both; that is `F-Identity`'s entity test holding in an implementation that has never read it. -Writing J2 and J3 from the specification found one more gap in it, which that test is the resolution of. `F-Import` and `F-Val-Live` stated two identity predicates and nothing said they answer different questions, so either choice for both uses is wrong, in one direction unsoundly. `F-Identity` makes the recursive test normative and `F-Import`'s broader one an over-approximation whose cost is coverage (#59). +Writing J2 and J3 from the specification found one more gap in it, which that test is the resolution of. The texts of `F-Import` and `F-Val-Live` stated two identity predicates and nothing said they answer different questions, so either choice for both uses is wrong, in one direction unsoundly. `F-Identity` makes the recursive test normative and `F-Import`'s broader one an over-approximation whose cost is coverage (#59). The port's own failure mode: chant-v0.69.0 extended an envelope check from three kinds to five while the port still had three, and because no fixture covered the shape, the suite stayed green against a stale port until the drift was found by reading the release diff. Two fixtures now cover it, and the port that made the drift possible is gone. ## Field provenance -`packages/conformance/provenance-report.md` counts every field chant's corpus emits by where its value came from (#237). F-Obs-Provenance names four kinds. A field is declared directly or comes from a composite, and a composite's field is either one of its parameters or a literal it fixes. The fourth kind is unknown, with the reason chant records. A field is one of chant's emitted property paths through plain objects; an array counts whole. Files that fold are counted from the record `foldProject` returns. A file that runs has no fold record. For those the harness builds the entry the way `chant build` does and counts the record that build keeps. +`packages/conformance/provenance-report.md` counts every field chant's corpus emits by where its value came from (#237). F-Obs-Provenance names four kinds. A field is declared directly or comes from a composite, and a composite's field is either one of its parameters or a literal it fixes. The fourth kind is unknown, with the reason chant records. Here a field means one of chant's emitted property paths through plain objects; an array counts whole. Files that fold are counted from the record `foldProject` returns. A file that runs has no fold record. For those the harness builds the entry the way `chant build` does and counts the record that build keeps. -This run is at the pin, `chant-v0.109.0` at `a2d3c66aa`, the first chant release that reports provenance. An earlier run on a build of chant's main branch ahead of the release counted more than twice as many direct fields in files that fold. The release reports a member destructured from a lexicon composite's result as unknown rather than direct (chant#3608), and those fields moved from direct to unknown. +This run is at the pin, `chant-v0.109.0` at `a2d3c66aa`, the first chant release that reports provenance. On a build of chant's main branch ahead of the release, an earlier run counted more than twice as many direct fields in files that fold. The release reports a member destructured from a lexicon composite's result as unknown rather than direct (chant#3608), and those fields moved from direct to unknown. | Files | Count | Entities | Fields | Direct | Composite parameter | Composite literal | Unknown | Known share | Known among composite fields | |---|---|---|---|---|---|---|---|---|---| @@ -146,7 +146,7 @@ This run is at the pin, `chant-v0.109.0` at `a2d3c66aa`, the first chant release | all | 467 | 1513 | 8887 | 2658 | 14 | 4 | 6211 | 30.1% | 0.3% | | `jhgaylor/infisical-chant`, run | 23 | 10 | 158 | 0 | 0 | 0 | 158 | 0.0% | 0.0% | -The known share counts every field whose kind is not unknown, over all fields. A direct field is known by construction, and the third claim is about composites. So the last column leaves direct fields out of both sides: it is the attributed composite fields over every field a composite expanded. The external project's eight files that fold emit no field. +The known share counts every field whose kind is not unknown, over all fields. A direct field is known by construction, and the third claim is about composites. The last column therefore leaves direct fields out of both sides: it is the attributed composite fields over every field a composite expanded. The external project's eight files that fold emit no field. Every unknown carries the reason `composite-not-interpreted`. The other reason, `no-provenance`, needs a build in a sandboxed child. Nothing here builds that way. The unknowns come from two places: @@ -159,7 +159,7 @@ A lexicon's composite is host code. chant invokes its factory and interprets onl **What this establishes.** chant's record reaches every file in the corpus, and no field falls through to `direct` without a record behind it. Where the fold interprets a composite's body, the attribution is complete on this corpus. That is two composite calls. -**What it does not.** It counts fields, not drift; how often each kind of field drifts in a running estate is not measured here. chant's examples mostly call composites a lexicon ships. A project that writes its own composites would score differently in either direction. The one external project emits all of its fields from files that run. A whole array counts as one field. The package and project split is decided from syntax: a composite is the project's when the declaring file or a project file it imports passes its name to `Composite`. The run row comes from executing those files in the harness's own process. +**Limits.** It counts fields, not drift; how often each kind of field drifts in a running estate is not measured here. chant's examples mostly call composites a lexicon ships. A project that writes its own composites would score differently in either direction. The one external project emits all of its fields from files that run. A whole array counts as one field. The package and project split is decided from syntax: a composite is the project's when the declaring file or a project file it imports passes its name to `Composite`. The run row comes from executing those files in the harness's own process. ## What the specification found diff --git a/paper/mechanism.md b/paper/mechanism.md index 81349e8..df7e2a1 100644 --- a/paper/mechanism.md +++ b/paper/mechanism.md @@ -19,9 +19,7 @@ The **statement gate** (`S-Module`) examines only exported statements, and recog Six further shapes disqualify the whole file (`S-Disqualify`). A default export and a star re-export are two of them; an exported class is a third. Non-exported statements are invisible to the gate, neither admitted nor disqualifying, and they never execute. -The gate's granularity is the design decision rather than the list. It is per module, and the justification is that an unreducible export can reference, or be referenced by, a reducible one in ways only running proves safe. A per-declaration gate would have to decide whether a half-reduced namespace is coherent, and it is not (`F-Total`). - -The gate is per module rather than per declaration, and the reason is this: an unfoldable export can reference or be referenced by a foldable one in ways only running proves safe (`F-Total`). +The gate's granularity is the design decision rather than the list. Per-module gating is justified because an unreducible export can reference, or be referenced by, a reducible one in ways only running proves safe. A per-declaration gate would have to decide whether a half-reduced namespace is coherent, and it is not (`F-Total`). The **expression classifier** (`grammar.md` §2) then decides the shapes inside an admitted statement. It resolves nothing. That is deliberate, and it is the subject of the direction claim below. @@ -29,7 +27,7 @@ The **expression classifier** (`grammar.md` §2) then decides the shapes inside ## What reduction produces -The value domain and the three mechanisms by which reduction reaches a value have their own section. Two facts from it are needed here. Reduction produces envelopes that denote what the source named, of which exactly one kind survives to serialization (`F-Val-Fate`). And the guarantee is narrow: none of the reduced file's own statements execute, while revival does import and invoke the module the fallback path would have imported (`F-NoOwnExecution`). +The value domain and the three mechanisms by which reduction reaches a value have their own section. Two facts from it are needed here. Reduction produces envelopes that denote what the source named, of which exactly one kind survives to serialization (`F-Val-Fate`). The guarantee is also narrow: none of the reduced file's own statements execute, while revival does import and invoke the module the fallback path would have imported (`F-NoOwnExecution`). ## Two sub-grammars, and an asymmetry @@ -51,9 +49,9 @@ The two disagree on exactly that point, and the specification says so rather tha The subset has a single definition with two consumers. A lint pass reads it without a binding resolver or a registry; an evaluator reads it with both. They will disagree, and the specification's job is to constrain how. -The claim is one-directional and stated with its exceptions inside it. **If evaluation succeeds, classification accepts** (`F-Direction`), except in two cases. The classifier is flow-insensitive, so it requires every branch of a short-circuiting operator to be admissible where the evaluator reduces only the taken one (`F-Exc-Lazy`); `false && f()` is therefore a lint error on source that reduces cleanly. And the classifier takes the intrinsic registry as an optional parameter, so without one a call form the registry would admit is refused (`F-Exc-Registry`). +The claim is one-directional and stated with its exceptions inside it. **If evaluation succeeds, classification accepts** (`F-Direction`), except in two cases. The classifier is flow-insensitive, so it requires every branch of a short-circuiting operator to be admissible where the evaluator reduces only the taken one (`F-Exc-Lazy`); `false && f()` is therefore a lint error on source that reduces cleanly. The other exception comes from the intrinsic registry being an optional parameter of the classifier, so without one a call form the registry would admit is refused (`F-Exc-Registry`). -The direction is chosen rather than observed, and the reason is asymmetric cost. A classifier that accepts too much produces a fallback the author learns about from a per-file decision line. A classifier that rejects too much produces an error on correct source, and a lint that cries wolf gets disabled, taking the real diagnostics with it. The classifier is also the predicate a downstream tool asks *will this reduce* without running a reduction, and such a tool must get an answer safe to act on. +The direction is chosen rather than observed, and the reason is asymmetric cost. Accepting too much produces a fallback the author learns about from a per-file decision line. Rejecting too much produces an error on correct source, and a lint that cries wolf gets disabled, taking the real diagnostics with it. A downstream tool also asks the classifier *will this reduce* without running a reduction, and such a tool must get an answer safe to act on. Twelve divergences run the permitted way, and the specification enumerates all twelve rather than describing the shape of the set (`F-Div-*`). A claim that two analyses disagree only in one direction needs a list of where, because the list is what a reader checks and what a new rule has to join. @@ -80,11 +78,11 @@ The two rows that run the other way are the exceptions named above, and there is Evaluating a single file yields either a reduction with a complete export namespace, or a fallback with a located reason (`F-Total`, `F-Reason`). Three properties of that verdict matter downstream. -**It is total per file.** One unrecognised export disqualifies the whole module. There is no partial namespace, which is what lets a referring file treat another file's result as either wholly available or wholly absent. +**The verdict is total per file.** One unrecognised export disqualifies the whole module. There is no partial namespace, which is what lets a referring file treat another file's result as either wholly available or wholly absent. -**It is reported.** A fallback is a normal outcome rather than an error, and that is exactly why it must appear: an unreported fallback is indistinguishable from a reduction, and the no-execution guarantee becomes unauditable (`F-Obs-Report`). The reason is located, naming the construct and its position; a failure inside a called function is re-anchored at the call site, with the callee's own position carried in the message (`F-Reason`). +**Nothing falls back silently.** A fallback is a normal outcome rather than an error, and that is exactly why it must appear: an unreported fallback is indistinguishable from a reduction, and the no-execution guarantee becomes unauditable (`F-Obs-Report`). The reason is located, naming the construct and its position; a failure inside a called function is re-anchored at the call site, with the callee's own position carried in the message (`F-Reason`). -**It is parameterized by isolation.** Under an isolated mode, a reduction that would have to invoke project-owned code falls back instead (`F-IsolatedRefusal`). The verdict is therefore not a pure function of the source, and a specification that omitted the parameter would describe a judgment that behaves differently in any real deployment. +**Isolation parameterizes it.** Under an isolated mode, a reduction that would have to invoke project-owned code falls back instead (`F-IsolatedRefusal`). The verdict is therefore not a pure function of the source, and a specification that omitted the parameter would describe a judgment that behaves differently in any real deployment. All of this is still a proposal. What makes a verdict final is the fixpoint. @@ -100,8 +98,8 @@ Every comparable system avoids the problem by not having it. Compile-time functi The fixpoint (`F-Taint`) closes the tentative verdicts under two edges: -- **forward**, along imports: a running file taints what it imports, because its real import would construct what a folded copy already holds (`F-Succ`); -- **backward**, along captures: a file whose objects were captured taints the capturer, because the instance the capturer holds is no longer the one the build collects (`F-Succ`, `F-Capture`). +- **forward** along imports, where a running file taints what it imports because its real import would construct what a folded copy already holds (`F-Succ`); +- **backward** along captures, where a file whose objects were captured taints the capturer because the instance the capturer holds is no longer the one the build collects (`F-Succ`, `F-Capture`). A third edge runs through calls rather than imports: a project-local function whose call returns a live object the body produced records the same capture (`F-CallLeak`). Invocation propagates identity the same way import does. @@ -111,7 +109,7 @@ The property this buys is stated and argued in `theorem.md`: exactly one object Two consequences look like defects: -**A leaf fix buys nothing while an importer still falls back.** Making a leaf reducible changes no verdict until every file in the closure above it also reduces. This was observed as coverage *falling* after a migration that made a widely imported file reducible, which read as a regression and was the rule working. An implementation that optimised it away would reintroduce the two-objects problem directly. +**A leaf fix buys nothing while an importer still falls back**. Making a leaf reducible changes no verdict until every file in the closure above it also reduces. This was observed as coverage *falling* after a migration that made a widely imported file reducible, which read as a regression and was the rule working. An implementation that optimised it away would reintroduce the two-objects problem directly. **A file's verdict is not a property of its own source.** Through the backward edge, a file that reduces cleanly can be forced back because something else captured one of its objects and then fell back. Nothing in the first file predicts that, which places a real obligation on reporting: the reason must be able to say that a file fell back because another did and captured from it. @@ -140,10 +138,10 @@ Tentative verdicts first, each file judged alone (J2). `run-only-importer.ts` fa Now the fixpoint (`F-Taint`): -1. Seed: `{ run-only-importer.ts }`, the one file that failed on its own (`F-Seed`). -2. Forward edge: the seed imports `shared-config.ts`, so that file is tainted (`F-Succ`). Nothing about it resists reduction, and it runs anyway. Reduced independently, its objects would be rebuilt by the importer's real import, leaving two objects claiming to be one entity. -3. Backward edge: `capturing-sibling.ts` reduced cleanly and captured `sharedLabels` from a file that now runs, so the object it holds is not the object the build will collect, and the reverse edge taints it (`F-Succ`, via `F-Capture`). -4. Closure: nothing reaches `independent.ts`. It imports no sibling and captures nothing; its labels are the same *value* as the shared ones and deliberately not the same *object*, because the edge is identity and not equality. +1. The seed is `{ run-only-importer.ts }`, the one file that failed on its own (`F-Seed`). +2. `shared-config.ts` is imported by the seed, so the forward edge taints it (`F-Succ`). Nothing about it resists reduction, and it runs anyway. If it reduced independently, the importer's real import would rebuild its objects, leaving two objects claiming to be one entity. +3. `capturing-sibling.ts` reduced cleanly and captured `sharedLabels` from a file that now runs, so the object it holds is not the object the build will collect, and the backward edge taints it (`F-Succ`, via `F-Capture`). +4. At closure nothing reaches `independent.ts`. It imports no sibling and captures nothing; its labels are the same *value* as the shared ones and deliberately not the same *object*, because the edge is identity and not equality. Three files run and one folds. Note which edge does the third step. `capturing-sibling.ts` also imports `shared-config.ts`, and that forward edge points from importer to imported, so it cannot carry taint back. Only the capture edge can, and without it the file would reduce while its source runs. @@ -155,9 +153,9 @@ The control file is what makes the example an example. Without it, "taint forced The subset is parameterized. A host provides six things (`F-Host-Interface`). Two concern entities, being the constructors that build them and how they expose attributes. Three are lists the host installs, an intrinsic registry and an authoring-helper allowlist and a trust set. The sixth is the form a composite registration takes. A registered call is admitted only if it is a pure function of its arguments and invoking it at fold time is indistinguishable from invoking it during a real run (`F-Host-Admission`), and revival always invokes the function the file imported rather than a reimplementation (`F-Host-NoSubstitution`). -One rule is an asymmetry between two kinds of callee. Into a **package**, reduction goes only through a closed allowlist, checked by name *and* by the provenance of the binding, so a helper of the author's own that happens to share a registered name is not the host's and the file falls back (`F-Div-Provenance`). Into a **project file**, reduction proceeds whenever the callee's body is itself in the subset, with no allowlist at all. +One rule is an asymmetry between two kinds of callee. Into a **package**, reduction goes only through a closed allowlist, checked by name *and* by the provenance of the binding, so a helper of the author's own that happens to share a registered name is not the host's and the file falls back (`F-Div-Provenance`). For a callee in a **project file**, reduction proceeds whenever the callee's body is itself in the subset, with no allowlist at all. -That looks backwards until the trust boundary is stated. Package code is already loaded and executed by the build before reduction begins, to obtain the serializers and lint rules the build cannot run without; admitting a call into it costs no execution the process was not already performing, so it is admitted by declaration and verified by registration. Project code is the untrusted input, and it is admitted only when it can be *evaluated without being executed*, which a syntactic check of the callee's body decides and an allowlist could not. +That looks backwards until the trust boundary is stated. Package code is already loaded and executed by the build before reduction begins, to obtain the serializers and lint rules the build cannot run without; admitting a call into it costs no execution the process was not already performing, so it is admitted by declaration and verified by registration. The untrusted input is project code, and it is admitted only when it can be *evaluated without being executed*, which a syntactic check of the callee's body decides and an allowlist could not. Admission to the allowlist has its own bar. A registered call must be a pure function of its arguments, and calling it during reduction must be indistinguishable from calling it during a real run (`F-Host-Admission`). Revival then uses the function the file imported rather than a reimplementation (`F-Host-NoSubstitution`), which is the principle compile-time function execution states: context decides where a function runs and never what it means. diff --git a/paper/related-work.md b/paper/related-work.md index c882862..4ea5984 100644 --- a/paper/related-work.md +++ b/paper/related-work.md @@ -6,7 +6,7 @@ Draft for #27. Rule identifiers refer to `spec/`. The order follows #31: the nea D, Zig, Rust and C++ evaluate a function at compile time when its inputs are static and at run time otherwise. D's specification states the principle this work relies on: a function's semantics cannot depend on compile-time values, so the calling context alone decides where it runs. `F-Host-NoSubstitution` is the same principle as a rule. The function revival invokes is the one the file imported, never a reimplementation. -Two differences. CTFE decides per call site; this work decides per file (`F-Total`). A CTFE'd value is copied into the compiled program, so nothing at run time shares identity with a compile-time object. Here a folded entity is the object other files hold references to, which is why J3 exists. The D compiler also treats an unevaluable required context as an error; `F-Depth` and `F-Total` require a fallback. +Two differences. CTFE decides per call site; this work decides per file (`F-Total`). A value computed by CTFE is copied into the compiled program, so nothing at run time shares identity with a compile-time object. Here a folded entity is the object other files hold references to, which is why J3 exists. The D compiler also treats an unevaluable required context as an error; under `F-Depth` and `F-Total` the same case falls back. ## Separate partial evaluation @@ -14,7 +14,7 @@ Heldal and Hughes treat a program as modules that can be specialized independent ## Partial evaluation and binding-time analysis -The shape classifier of `grammar.md` is a binding-time analysis and `fold` is the specializer, in the sense of Jones, Gomard and Sestoft. The static and dynamic split is theirs. The per-file verdict with taint (J2, J3) is closer to an online decision over a coarse unit than to an offline BTA. Forcing a folded file back to run is a coarse form of the lift operation. Multi-stage programming makes staging explicit in the language instead of inferring it (Taha and Sheard, MetaML). +In Jones, Gomard and Sestoft's terms the shape classifier of `grammar.md` is a binding-time analysis and `fold` is the specializer. The static and dynamic split is theirs. The per-file verdict with taint (J2, J3) is closer to an online decision over a coarse unit than to an offline BTA. Forcing a folded file back to run is a coarse form of the lift operation. Multi-stage programming makes staging explicit in the language instead of inferring it (Taha and Sheard, MetaML). ## Partial evaluation of JavaScript @@ -41,7 +41,7 @@ Nix import-from-derivation pauses evaluation, realises a store object, and resum Every row answers unsupported source with an error and so has no two-path agreement problem and no identity problem. This work's fallback (`F-Total`) is what removes that simplification. -Pkl and CUE deserve one more sentence each, because a reader will have them open in the next tab. Both give a platform typed, deterministic configuration that emits YAML or JSON, and Pkl puts value constraints in the type where this work puts them in a separate semantic pass over folded values. What neither gives is the authoring surface being the artifact's own shape: a Pkl or CUE file is a second grammar pointed at the spec, where a typed object literal is the spec with its keys unquoted. On the fourteen operational properties chant's own comparison scores, the configuration languages answer the first three and leave the rest to a second abstraction that shares no types with what was authored; this work's claim to a platform is exactly those three, with the same file carrying the rest when the platform is chant. Pkl's bindings for other languages shell out to an evaluator binary; the `data-host` profile is what lets an evaluator for this subset be a library in the platform's own language instead. +A reader will have Pkl and CUE open in the next tab, so they get one more sentence each. Both give a platform typed, deterministic configuration that emits YAML or JSON, and Pkl puts value constraints in the type where this work puts them in a separate semantic pass over folded values. What neither gives is the authoring surface being the artifact's own shape: a Pkl or CUE file is a second grammar pointed at the spec, where a typed object literal is the spec with its keys unquoted. On the fourteen operational properties chant's own comparison scores, the configuration languages answer the first three and leave the rest to a second abstraction that shares no types with what was authored; this work's claim to a platform is exactly those three, with the same file carrying the rest when the platform is chant. Pkl's bindings for other languages shell out to an evaluator binary; the `data-host` profile is what lets an evaluator for this subset be a library in the platform's own language instead. ## Infrastructure tools @@ -53,4 +53,8 @@ Per-file partial evaluation with a fallback is precedented in shape (Next.js) an ## Citations to confirm before submission -Jones, Gomard, Sestoft 1993. Taha and Sheard 1997. Heldal and Hughes 1997 and 2000, full text. The D specification's CTFE section, primary text. Siek et al. 2015 for the gradual guarantee, if the analogy is used. +- Jones, Gomard, Sestoft 1993. +- Taha and Sheard 1997. +- Heldal and Hughes 1997 and 2000, full text. +- The D specification's CTFE section, primary text. +- Siek et al. 2015 for the gradual guarantee, if the analogy is used. diff --git a/paper/theorem.md b/paper/theorem.md index 7fb3f08..4a85b21 100644 --- a/paper/theorem.md +++ b/paper/theorem.md @@ -24,9 +24,9 @@ In neither case do a folded object and a run object for `e` coexist. ∎ **What the sketch assumes.** `F-Memo` and `F-Count` hold in the implementation. The run path yields one module instance per file; under isolation this is why every run-fallback file is bundled into one module graph (`F-IsolatedRefusal`, J2). `T(B)` exists and is finite (`F-Fix`). -**Where the argument was wrong once.** The first prose statement of the forward edge had the direction reversed. Writing `Succ` as an operator caught it (#15). The paper should keep that as evidence that the formal statement earns its place. +**Where the argument was wrong once**. The first prose statement of the forward edge had the direction reversed. Writing `Succ` as an operator caught it (#15). The paper should keep that as evidence that the formal statement earns its place. -**What has been executed.** A second implementation, written from J2 and J3 rather than ported, computes `T(B)` by a worklist from `Seed`. Whole-build fixtures hold it to each edge in turn: a file that seeds with no edge at all, the forward edge into an import, the backward edge two hops out through a capture. A fourth is the control: the file nothing reaches, which must still fold. Falling back on everything satisfies the claim and is what a degraded implementation does. chant answers the same fixtures since chant-v0.70.1 (chant#2408), and the two implementations agree on every file: the final verdict, the verdict before taint, and for each casualty the file the edge came from and which rule it was. chant's own differential over every mixed corpus entry and the adversarial build remain the evidence from a real corpus rather than a designed one (`paper/measurements.md`). +**What has been executed.** A second implementation, written from J2 and J3 rather than ported, computes `T(B)` by a worklist from `Seed`. Whole-build fixtures hold it to each edge in turn: a file that seeds with no edge at all, the forward edge into an import, the backward edge two hops out through a capture. A fourth is the control: the file nothing reaches, which must still fold. Falling back on everything satisfies the claim and is what a degraded implementation does. Since chant-v0.70.1 (chant#2408) chant has answered the same fixtures, and the two implementations agree on every file: the final verdict, the verdict before taint, and for each casualty the file the edge came from and which rule it was. chant's own differential over every mixed corpus entry and the adversarial build remain the evidence from a real corpus rather than a designed one (`paper/measurements.md`). ## Theorem 2, the permitted direction of divergence @@ -36,15 +36,15 @@ Let `shape(e, ρ)` be the classifier's verdict on expression `e` with optional r **Proof sketch.** Both consumers import one classifier, so every syntactic question has one answer by construction. Every remaining disagreement is a resolution the classifier does not perform. `spec/divergence.md` enumerates them as `F-Div-*`, twelve rows, and each is a rejection by `fold` of something `shape` accepted. The two exceptions are the only sites where `fold` accepts something `shape` rejects, one from lazy evaluation and one from a missing registry, and each is stated with its reason. ∎ -**Corollary.** Every disagreement outside `F-Exc` costs coverage and never correctness: a file the classifier passes and the folder rejects falls back to run, and never produces wrong output. +**Corollary**. Every disagreement outside `F-Exc` costs coverage and never correctness: a file the classifier passes and the folder rejects falls back to run, and never produces wrong output. ## Property 3, the round trip Let `generate` be any function from the value domain to source in the subset, a generator in the sense of `enables.md`. -**Claim.** For every value `v` the domain admits, `fold(generate(v)) = v` in the `data-host` profile, and `fold(generate(v)) = revive(v)` in `full`, where `revive` is `F-Val-Fate`. +**Claim.** For every value `v` the domain admits, `fold(generate(v))` is `v` in the `data-host` profile and `revive(v)` in `full` (with `revive` being `F-Val-Fate`). -The argument has two halves. Completeness is `F-Val-Source` (`spec/values.md`, spec `1.5`), a table with one source form per case of `F-Val-Domain`; each form folds to its value by the rule the table cites, and the domain is closed, so the table is exhaustive. Fidelity is an obligation on each generator rather than a rule: its output is in the subset and folds to its input. The specification states the obligation in `spec/README.md`. The suite tests it through the `roundtrip` fixture kind, whose input is a namespace as data and whose expectation is that the fold of the generated source equals it. The profile split is forced, since in `full` the fold of a resource's form is a live instance and the value the round trip returns to is the revived one. +The argument has two halves. Completeness is `F-Val-Source` (`spec/values.md`, spec `1.5`), a table with one source form per case of `F-Val-Domain`; each form folds to its value by the rule the table cites, and the domain is closed, so the table is exhaustive. Fidelity is an obligation on each generator rather than a rule: its output is in the subset and folds to its input. The specification states the obligation in `spec/README.md`. The suite tests it through the `roundtrip` fixture kind. A fixture of that kind takes a namespace as data for its input and expects the fold of the generated source to equal it. The profile split is forced, since in `full` the fold of a resource's form is a live instance and the value the round trip returns to is the revived one. The reference carries the smallest generator that makes the property testable, one form per case with no factoring, and it passes the four `roundtrip` fixtures. One holds scalars inside containers and one a resource with attribute references to it; a third constructs a resource by spread arguments and the last carries a symbol through both intrinsic forms. Two `F-Val-Source` fixtures write the table by hand for each profile in turn. chant's three generators emit through one pipeline whose forms are the table's (inventory `L12.1` to `L12.3`). Its Kubernetes round-trip suite re-serializes generated source and compares resource count and kinds rather than bytes (`L12.4`), so the byte-level measurement over real templates is still to be taken, and chant's adapter has no `generate` hook yet. Until both exist the property is proved for the reference and stated for chant. diff --git a/paper/values-and-modes.md b/paper/values-and-modes.md index 675374e..7b293fe 100644 --- a/paper/values-and-modes.md +++ b/paper/values-and-modes.md @@ -4,7 +4,7 @@ Draft for #58, split out of the mechanism section. What reduction produces, and ## The value domain -Reduction yields a value from a closed domain (`F-Val-Domain`). Six cases are ordinary JSON, from scalars through arrays to plain objects. The other six are **envelopes**, non-array objects carrying one marker key, each denoting something the build has not yet constructed (`F-Val-Envelope`). +A reduced value comes from a closed domain (`F-Val-Domain`). Six cases are ordinary JSON, from scalars through arrays to plain objects. The other six are **envelopes**, non-array objects carrying one marker key, each denoting something the build has not yet constructed (`F-Val-Envelope`). | Envelope | Denotes | Fate under revival | |---|---|---| @@ -29,11 +29,11 @@ Revival replaces five of the six, resolving each name through the folding file's Inside the arguments of an intrinsic or an authoring helper, an `__attrRef` is refused rather than passed (`F-Val-Position`). The receiving function inspects what it is given, checking types and dereferencing weak references, and a look-alike plain object makes it produce wrong output rather than absent output. One position out, in a construction's props, the same value passes untouched, because there the serializer resolves it by name. -The same value is therefore valid in one position and a rejection in another. A definition of the domain alone does not capture that, so the rule is part of the domain rather than a note about it. +Position therefore decides whether the same value is valid or a rejection. A definition of the domain alone does not capture that, so the rule is part of the domain rather than a note about it. ### Liveness, and why it matters -A value *carries a live object* when it, or anything reachable through plain objects and arrays, has a prototype other than the plain ones, or is a function (`F-Val-Live`). Live objects reached through cross-file resolution pass through revival untouched, because the generic walk would rebuild them as plain copies and destroy the identity the fixpoint exists to preserve. +A value *carries a live object* when it is a function or has a prototype other than the plain ones, or when anything reachable from it through plain objects and arrays does (`F-Val-Live`). Live objects reached through cross-file resolution pass through revival untouched, because the generic walk would rebuild them as plain copies and destroy the identity the fixpoint exists to preserve. This predicate is what makes the identity rules statable at all. Without a definition of *this value is a live entity rather than plain data*, there is nothing for identity to be a property of, and the capture edge of the fixpoint has nothing to test. @@ -43,13 +43,13 @@ Three smaller rules complete the domain. A **callable** is in the domain and is never a value. A project-local function may be called during reduction, but `{ resolver: f }` does not reduce though `f(x)` does, because nothing can serialize a function (`F-Val-Callable`). -**Constructor arity is contractual.** The common shape is a props object, optionally followed by resource-level attributes. When the argument list is neither, the positional argument list is authoritative and the entity is built by spreading it (`F-Val-Arity`). An implementation that assumed the props object comes first would construct a real lexicon's parameter type wrongly. +**Constructor arity is contractual**. The common shape is a props object, optionally followed by resource-level attributes. When the argument list is neither, the positional argument list is authoritative and the entity is built by spreading it (`F-Val-Arity`). An implementation that assumed the props object comes first would construct a real lexicon's parameter type wrongly. -**Absence has two forms.** `undefined` in a property position is dropped at emission; in an array position it becomes `null` (R10.7). Both follow from the host's JSON semantics and both must be stated, because platforms act on the difference between an absent field and a null one. +**Absence has two forms**. A property whose value is `undefined` is dropped at emission, and an `undefined` array element becomes `null` (R10.7). Both follow from the host's JSON semantics and both must be stated, because platforms act on the difference between an absent field and a null one. ## Three evaluation modes -Reduction reaches a value by three different mechanisms. Conflating them is the easiest way to misread the design, and the second has no counterpart in the first. +There are three different mechanisms by which reduction reaches a value. Conflating them is the easiest way to misread the design, and the second has no counterpart in the first. ### Envelope, then revive diff --git a/scripts/docs-sentences-baseline.json b/scripts/docs-sentences-baseline.json index 023144c..0967ef4 100644 --- a/scripts/docs-sentences-baseline.json +++ b/scripts/docs-sentences-baseline.json @@ -1,49 +1 @@ -{ - "paper/discussion.md": { - "discourse/epistrophe": 1, - "anaphora/repeated-opening": 1 - }, - "paper/draft.md": { - "anaphora/repeated-opening": 15, - "discourse/conjunction-opener": 11, - "tricolon/comma-series": 1, - "discourse/epistrophe": 1 - }, - "paper/enables.md": { - "anaphora/repeated-opening": 2 - }, - "paper/introduction.md": { - "anaphora/repeated-opening": 3, - "discourse/conjunction-opener": 1 - }, - "paper/measurements.md": { - "anaphora/repeated-opening": 7, - "discourse/conjunction-opener": 6, - "discourse/epistrophe": 1, - "repetition/near-duplicate": 1 - }, - "paper/mechanism.md": { - "discourse/epistrophe": 1, - "discourse/conjunction-opener": 2, - "anaphora/repeated-opening": 8, - "claude/colon-reveal": 5 - }, - "paper/related-work.md": { - "anaphora/repeated-opening": 2, - "discourse/conjunction-opener": 1, - "tricolon/comma-series": 1, - "discourse/punchy-fragments": 1 - }, - "paper/theorem.md": { - "anaphora/repeated-opening": 3, - "tricolon/comma-series": 2 - }, - "paper/values-and-modes.md": { - "anaphora/repeated-opening": 4, - "tricolon/comma-series": 1 - }, - "README.md": { - "tricolon/comma-series": 1, - "anaphora/repeated-opening": 1 - } -} +{} diff --git a/scripts/lint-docs-sentences.mjs b/scripts/lint-docs-sentences.mjs index 3e21131..138327b 100644 --- a/scripts/lint-docs-sentences.mjs +++ b/scripts/lint-docs-sentences.mjs @@ -1,22 +1,13 @@ // Prose lint for spec/*.md and README.md (copied from chant's scripts/lint-docs-sentences.mjs), // -// Posture here: README.md, spec/README.md and spec/prior-art.md are prose and -// carry no real findings. Four baselined entries in them are heading-run -// artifacts: a table or bullet list between two headings blanks out, so the -// headings read as consecutive sentences opening with "##". A fifth, in -// paper/measurements.md, is a lone sentence between a table and a heading -// read as a fragment pair; it follows the position, not the words. A sixth, -// in paper/README.md, is the heading run again: the rule counts "##" lines -// whatever sits between them, so adding a sentence raised the count. Those -// six are the only tolerated findings in the prose and paper files. The rule files (grammar, judgments, values, divergence, hosts, -// inventory) are formal text: every rule opens with its identifier in bold, -// case analyses open with "If"/"with"/"otherwise", and definitions are short -// lines. The linter reads those as anaphora, fragments and colon reveals; -// they are structure, not tells. Those files are baselined and may only -// shrink, same ratchet as chant. on the `sentences` trope ruleset — the +// Posture here: the rules run on the `sentences` trope ruleset, the // AI-writing tells (em-dash density, colon reveals, tricolons, anaphora, -// bold-first bullets, …) that tropes.fyi catalogs and the package detects -// per sentence with real parse trees, not regexes. +// bold-first bullets, ...) that tropes.fyi catalogs and the package detects +// per sentence with real parse trees, not regexes. The baseline is empty: +// spec/, paper/, README.md and docs/content carry no gated finding, the rule +// files included. Their formal shapes (a bolded identifier opening each rule, +// case analyses, judgment notation) are blanked by scripts/lib/doc-prose.mjs +// before the rules see them. // // Same posture as scripts/typecheck.ts: a RATCHET, not a purity gate. The // docs corpus predates the linter; every existing finding is baselined