paper: what the fold enables, the profile split, the round trip as a property, Pkl and CUE by name (#87)

justfile

@@ -0,0 +1,30 @@
+# Local entry points. CI runs the same commands from package.json; these are
+# the ones a person types.
+
+# Typecheck, the suite, and the prose ratchet: what CI's check job runs.
+check:
+    npm run typecheck
+    npm test
+    npm run lint:prose
+
+# The docs site, built to docs/dist/ (syncs spec/ and the figures first).
+site:
+    npm run --prefix docs build
+
+# The docs site with live reload at http://localhost:4321/typescript-as-data/
+site-dev:
+    npm run --prefix docs dev
+
+# Serve the last build of the site, the way it will be published.
+site-preview: site
+    npm run --prefix docs preview
+
+# The corpus cross-check and the citation gate, against a chant checkout.
+# Pass the checkout: `just corpus ../chant`. The paper's number is taken with
+# the checkout at the pinned tag, seeded per the memory notes.
+corpus repo:
+    TSAD_CHANT_REPO={{repo}} npm run corpus
+
+# Pack both packages, install them into a fresh directory, run the suite there.
+smoke:
+    npm run smoke:published

paper/README.md

@@ -33,6 +33,7 @@ Each draft feeds one section of the paper.
 | `theorem.md` | #28 | the two claims and their proof sketches |
 | `measurements.md` | #29 | evaluation |
 | `discussion.md` | #54 | discussion |
+| `enables.md` | #87 | what the fold enables, placed after the mechanism and before the evaluation |
 | `figures/` | #57 | two SVGs: the taint boundary, and the two-phase shape |
 | `../spec/prior-art.md` | #31 | the novelty narrowing, cited from related work |
 
@@ -42,7 +43,7 @@ Every section has a draft. What remains is the pass that turns seven Markdown fi
 
 ## Artifact
 
-The paper cites one specification version, by its tag (`spec-1.0` at the time of writing; `spec/VERSION` is current), and every number that depends on the rule set says which version produced it. If the track offers artifact evaluation, the artifact is this repository at a tag. It holds:
+The paper cites one specification version, by its tag (`spec-1.1` at the time of writing; `spec/VERSION` is current), and every number that depends on the rule set says which version produced it. If the track offers artifact evaluation, the artifact is this repository at a tag, and the thing an evaluator runs is the tutorial on the docs site (typescript-as-data#84). It declares a governance policy as data and plans and applies it against a throwaway Forgejo on the evaluator's own machine, which needs no account and no credentials. The repository holds:
 
 - the specification
 - the reference implementation

paper/discussion.md

@@ -36,6 +36,6 @@ The identity theorem is the paper's centre, so it is worth saying what would bre
 
 Two things, and only two.
 
-**An independent implementation of the module layer and the fixpoint.** The reference implementation covers the expression layer, written from the specification and agreeing with the production implementation on every fixture. The identity theorem is not in that layer. Until a second implementation of the fixpoint exists, that theorem has one implementation's evidence and an argument.
+**An implementation by someone who has not read chant.** The reference implementation now covers the module layer and the fixpoint as well as the expression layer, written from the specification and agreeing with the production implementation on every fixture and on every comparable file of chant's corpus. It shares an author with chant. An evaluator of the `data-host` profile in a language with no JavaScript engine (typescript-as-data#86) would be the first implementation that could not lean on one, and it would test the coercion fixtures in a way a JavaScript implementation cannot.
 
 **A corpus nobody here maintains.** Every measurement comes from one project's examples, written by people who know the subset. The measurement that would mean the most is the one not yet taken: source written against the specification by someone who has not read the implementation.

paper/enables.md

@@ -0,0 +1,19 @@
+# What the fold enables
+
+Draft for #87. The other sections say what the fold is. This one says what it is for, because a reviewer who grants every property in `mechanism.md` can still ask why anyone would want them, and the answer is three capabilities that neither a syntax linter nor a configuration language provides.
+
+## 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.
+
+## Semantic rules over values
+
+A syntax linter sees tokens and can say a key is misspelt. A configuration language with constraints in the type can say a port is out of range. Neither can say that two fields of one resource contradict each other, or that a resource in one file makes a resource in another file incoherent, because neither has the values of every file in the build before anything is emitted. The fold does. A rule that runs over folded values is a pure function of its input, deterministic and free of I/O, which is what lets it run in an editor, and it sees the same data in the editor that it sees in CI, because the data is a function of the source. Two phases follow from this: rules over the declared values before serialization, and rules over the emitted artifact after. chant's lexicons carry the first kind and its post-synth checks the second; a governance tool built on the same evaluator carries both without naming them, in its config loader and in its plan guardrails. The contract those rules run under is not yet in the specification and is stated here as a forward reference (typescript-as-data#79).
+
+## 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.
+
+## Which profile each needs
+
+The first two need only the `data-host` profile (`F-Profile-DataHost`, `judgments.md`), and so they are available to an evaluator with no JavaScript runtime. The third needs whichever profile the generator targets. None of the three needs the `run` fallback or J3; those exist so that source outside the subset can still be built by an implementation that has a runtime, and they are the part of the specification the paper is about. The capabilities are the part a platform adopts.

paper/mechanism.md

@@ -162,3 +162,9 @@ That looks backwards until the trust boundary is stated. Package code is already
 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.
 
 The generality this buys is over host vocabularies, not over languages. The syntax is TypeScript's and the operator semantics are ECMAScript's, with two deliberate departures the specification names (`R10.2`, `R10.6` in `grammar.md`'s rationale).
+
+## Two profiles, and which half is which
+
+Everything above assumes a JavaScript runtime is available for the files the fold refuses. That assumption is a profile, not a premise. `F-Profile` names it `full`, and `F-Profile-DataHost` names the other one (`judgments.md`, spec `1.1`): the specification for an evaluator that has no runtime, embedded in a platform written in another language. `data-host` is `full` with the runtime removed. Isolation is always on and a refused file is an error rather than a demotion; J3 is absent, since nothing runs and nothing can taint; revival is serialization, since there is no constructor to call; helpers and eager intrinsics are absent; a composite is interpreted or refused, never invoked.
+
+The split places the paper's contribution precisely. The identity theorem and the taint fixpoint live in `full`, because they exist to keep a folded object and a run object from coexisting, and in `data-host` no object ever runs. What survives into `data-host` is the expression layer, the per-file verdict, the value domain and the host interface as a description, which is the portable product. Stating this as two profiles of one specification, rather than as a mechanism half of which does not transfer, is what lets the same rule identifiers govern a JavaScript tool with a fallback and a Rust crate without one.

paper/related-work.md

@@ -41,6 +41,8 @@ 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.
+
 ## Infrastructure tools
 
 CDK, Pulumi and Alchemy execute the program that builds the resource graph; the graph exists only as the output of a run. Terraform evaluates HCL with functions against state. Formae compiles Pkl to data. chant's own comparison covers these; the paper cites it and adds nothing.

paper/theorem.md

@@ -38,6 +38,12 @@ Let `shape(e, ρ)` be the classifier's verdict on expression `e` with optional r
 
 **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, stated and not yet proved
+
+Let `generate` be any function from the value domain to source in the subset, a generator in the sense of `enables.md`. The claim is that for every value `v` the domain admits, `fold(generate(v)) = v`, up to the identity of live objects.
+
+Neither part of it is in the specification yet. Completeness says every value in the domain has some source form the fold reverses. That is what the specification owes (`F-Val-Source`, typescript-as-data#80). The envelope kinds are the cases that need care. Two source forms already exist: `F-Eval-Member` step 1 reverses an attribute reference and `F-Prebuild` a same-file entity. Fidelity says a particular generator's output folds to its input. It is an obligation on the generator rather than a rule, checked by a fixture family whose input is data rather than source. chant's Kubernetes lexicon carries a round-trip suite; the AWS import path's measurement is not yet taken. The property is listed here so the paper can point at it as the reason the choice of language is a matter of correctness rather than taste, and so a reviewer sees that it is a claim in flight and not a result.
+
 ## Mechanisation
 
 Declined for the submission. The venue accepts compelling arguments, exploratory implementations and substantial examples as validation. Theorem 1 has the argument above and three executed artifacts: the differential over every corpus entry including the mixed ones (`paper/measurements.md`), an adversarial build that fires both taint edges on purpose, and a second implementation held to whole-build fixtures. Theorem 2 has the shared-classifier construction and the enumerated table; a fixture per row is still owed (#24). A mechanised proof would make the claim airtight rather than accepted; if pursued it belongs in `spec/mechanization/` on its own CI job.