F-Identity: name the two identity predicates and say which is normative (#59)

packages/reference/CAVEATS.md

@@ -4,24 +4,14 @@ This package is written from `spec/` and nothing else (#50). Where the
 specification is silent, ambiguous, or asks for something the package cannot
 supply, the gap is recorded here rather than papered over in the code.
 
-## Two identity predicates, never reconciled
-
-J2's **F-Import** tests a captured value for identity with "`typeof` object
-**or function**". J4's **F-Val-Live** tests for "a prototype other than
-`Object` or `Array`, or a function". A plain `{ a: 1 }` satisfies the first
-and not the second.
-
-Both appear deliberate. The broad test is right for an import capture: two
-files holding one shared plain object still disagree about which copy is the
-build's, so the capture edge has to exist. The narrow test is right for
-F-CallLeak: a helper that takes a parameter and returns computed plain data
-taints nothing, and a narrower predicate is what keeps it from doing so.
-
-The specification states both and never says they are different tests for
-different questions. This implementation uses F-Import's predicate for import
-and re-export captures and F-Val-Live's for call leaks, which reproduces the
-intent; a reader of the specification alone could implement either one twice
-and be wrong in one of two directions. Filed as #59.
+## Two identity predicates
+
+Resolved in the specification by **F-Identity** (J3), which names the entity
+test and the reference test, says the entity test is the normative one, and
+says F-Import over-approximates on purpose. This package follows it: the
+reference test for import and re-export captures, the entity test for call
+leaks. Kept here as a pointer, because the code comments cite F-Identity and
+a reader of an older revision will not find it (#59).
 
 ## No revival
 

packages/reference/src/fold.ts

@@ -77,9 +77,9 @@ const isChain = (v: unknown): boolean => v === CHAIN;
 /**
  * F-Val-Live: 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. Distinct from J2's F-Import identity test, which is the broader
- * `typeof object or function`. The specification states both predicates and
- * does not reconcile them; see packages/reference/CAVEATS.md.
+ * a function. This is F-Identity's entity test, the normative one, and the
+ * test F-CallLeak uses. F-Import uses the broader reference test instead, on
+ * purpose; F-Identity in J3 says why.
  */
 export function carriesLiveObject(v: unknown, seen = new Set<unknown>()): boolean {
   if (v === null || typeof v !== "object") return typeof v === "function";

packages/reference/src/project.ts

@@ -23,7 +23,7 @@ export type Verdict =
   | { kind: "fold"; exports: Map<string, unknown>; captures: Set<string> }
   | { kind: "run"; rule: string; reason: string };
 
-/** F-Import's identity test: `typeof` object or function. Broader than F-Val-Live; see CAVEATS.md. */
+/** F-Identity's reference test, which F-Import uses: `typeof` object or function, not recursive. */
 const hasIdentity = (v: unknown): boolean => v !== null && (typeof v === "object" || typeof v === "function");
 
 const parse = (path: string, source: string) => ts.createSourceFile(path, source, ts.ScriptTarget.Latest, true);

paper/measurements.md

@@ -73,7 +73,7 @@ The control is the one with teeth. An implementation that falls back on every fi
 
 chant cannot answer any of them. Its public entry folds one expression or one file's resource exports; nothing in it takes a set of files, and a taint edge does not exist inside a single file. The whole-build fixtures therefore run against one implementation. The suite asserts that chant reports no project entry, so it fails the day one lands rather than letting the comparison lapse (chant#2408). What supports Theorem 1 across two implementations is the differential, not these fixtures.
 
-Writing J2 and J3 from the specification alone found one more gap in it. `F-Import` and `F-Val-Live` state two different identity predicates — a value with `typeof` object or function, against one with a prototype other than `Object` or `Array` — and the specification never says they answer different questions (#59). Using either predicate for both uses is wrong, in one direction unsoundly.
+Writing J2 and J3 from the specification alone found one more gap in it. `F-Import` and `F-Val-Live` stated two different identity predicates — a value with `typeof` object or function, against one with a prototype other than `Object` or `Array` — and nothing said they answer different questions. Using either for both uses is wrong, in one direction unsoundly. `F-Identity` now settles it: the recursive test is normative, because the proposition is about entities the build names, and `F-Import`'s broader test is an over-approximation whose cost is coverage (#59).
 
 The port's own failure mode is worth recording because it is the one this section should not paper over: 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.
 
@@ -90,7 +90,7 @@ Writing the specification against the implementation found defects the implement
 | three stale documentation claims, one in a shape the parity gate could not see | docs | chant#2306, #2348 |
 | the forward taint edge stated backwards in the spec's own prose | `spec/requirements.md` | caught by writing `Succ` as an operator (#15) |
 | four normative sentences used an *unclaimed* callee and none defined it | `spec/grammar.md` | found by writing the reference from the spec text; S-Unclaimed added (#51) |
-| two identity predicates stated for captures and never reconciled | `spec/judgments.md`, `spec/values.md` | found by writing J2 and J3 from the spec text (#59) |
+| two identity predicates stated for captures and never reconciled | `spec/judgments.md`, `spec/values.md` | found by writing J2 and J3 from the spec text; F-Identity added (#59) |
 | no public entry folds a whole project, so J3 is not testable from outside | `@intentius/chant` | chant#2408, open |
 | a backward-tainted file's fallback reason claims a file imports it, and none does | `discovery/fold-import.ts` | found by walking the adversarial build for the paper's worked example; `F-Obs-Report` requires naming the backward edge |
 | a module that threw at import was cached as evaluated, so a second build in one process reported no error | `discovery/import.ts` | chant#2368, fixed in v0.69.1; found by the adversarial corpus entry this specification's inventory shaped |

scripts/docs-sentences-baseline.json

@@ -32,7 +32,7 @@
   "formatting/em-dash-density": 2
  },
  "spec/judgments.md": {
-  "discourse/punchy-fragments": 46,
+  "discourse/punchy-fragments": 45,
   "claude/colon-reveal": 21,
   "repetition/near-duplicate": 20,
   "anaphora/repeated-opening": 11,

spec/fixtures/F-Succ/backward-along-captures/expect.json

@@ -1,8 +1,24 @@
 {
-  "rules": ["F-Succ", "F-Capture", "F-Taint"],
+  "rules": [
+    "F-Succ",
+    "F-Capture",
+    "F-Identity",
+    "F-Taint"
+  ],
   "project": true,
-  "verdicts": { "breaker.ts": "run", "shared.ts": "run", "sibling.ts": "run" },
-  "tentative": { "breaker.ts": "run", "shared.ts": "fold", "sibling.ts": "fold" },
-  "taintedBy": { "shared.ts": "breaker.ts", "sibling.ts": "shared.ts" },
-  "note": "The backward edge, two hops. breaker.ts is in the seed and taints shared.ts forward; shared.ts then taints sibling.ts backward because sibling.ts captured its registry object. Nothing in sibling.ts predicts its own verdict, which is why a fallback report has to be able to name the capture."
+  "verdicts": {
+    "breaker.ts": "run",
+    "shared.ts": "run",
+    "sibling.ts": "run"
+  },
+  "tentative": {
+    "breaker.ts": "run",
+    "shared.ts": "fold",
+    "sibling.ts": "fold"
+  },
+  "taintedBy": {
+    "shared.ts": "breaker.ts",
+    "sibling.ts": "shared.ts"
+  },
+  "note": "The backward edge, two hops. breaker.ts is in the seed and taints shared.ts forward; shared.ts then taints sibling.ts backward because sibling.ts captured its registry object. Nothing in sibling.ts predicts its own verdict, which is why a fallback report has to be able to name the capture. The captured value is a plain object, which F-Identity's reference test admits and its entity test would not: the edge exists here because F-Capture over-approximates on purpose."
 }

spec/judgments.md

@@ -357,18 +357,46 @@ J2 gives each `f` a tentative verdict `w(f) ∈ {fold, run}`; when
 
 ### Definitions
 
+**F-Identity.** Two identity predicates appear in this specification and they
+are not interchangeable.
+
+- The **entity test** (F-Val-Live) recurses through plain objects and arrays.
+- The **reference test** (F-Import) is `typeof` object **or** function. It does
+  not recurse and it admits a plain `{ a: 1 }` that the entity test rejects.
+
+The proposition below is about *entities* — the values a build names and
+serializes — and the entity test is the normative one for it. Two structurally
+equal plain objects that no `AttrRef` points at cannot be told apart in the
+output, so
+duplicating one breaks nothing claimed here. Recursion is what makes that test
+usable, a plain object *holding* an entity being itself live.
+
+F-Import uses the reference test anyway, as a deliberate over-approximation.
+An imported binding is nearly always an entity, and one `typeof` is cheaper
+than a recursive walk of every resolved import. The cost is coverage rather
+than correctness (F-Direction): a file capturing only plain data from an
+import falls back where it need not. Whether to narrow F-Import to the entity
+test is a question for measurement, since it changes which files fold.
+
+F-CallLeak uses the entity test, and has to. A parameter helper returning
+computed plain data must taint nothing, and under the reference test every
+one of them would be a taint source.
+
 **F-Capture.** `f` *captures* `g`, written `f ⇝ g`, iff `w(f) = fold` and some
 value in `X(f)` is a **non-primitive** obtained from `X(g)`, a `Declarable`, a
 `CompositeInstance`, or any other object reached through `f`'s resolved
 imports of `g`. Recorded as `g ∈ L(f)`. A primitive is never a capture: it
-has no identity to disagree about (L8.5).
+has no identity to disagree about (L8.5). The test here is F-Identity's
+reference test, so the relation is an over-approximation of the entity
+relation the proposition needs.
 
 **F-CallLeak.** Let `φ` be a project-local function defined in `g` and called
 from `f` during `f`'s fold. If the call **returns** a value that carries a live
 object (R1.4) *which was not already carried in by the arguments*, then the
 call leaked `g`'s identity into `f`: `leakedIdentity(φ)` is set and `g ∈ L(f)`
-(L5.9). A function returning only plain data never leaks, which is what keeps
-a parameter helper from tainting anything. F-CallLeak is F-Capture through
+(L5.9). The test here is F-Identity's entity test. A function returning only
+plain data never leaks, which is what keeps a parameter helper from tainting
+anything. F-CallLeak is F-Capture through
 invocation rather than through import; the edge it records is the same edge.
 
 **F-Memo.** Within one build, `w`, `X` and `L` are computed **at most once per

spec/values.md

@@ -82,7 +82,9 @@ unchanged** (L6.1): the generic walk would rebuild a plain copy and destroy
 the identity J3 exists to preserve. `isIntrinsic` is keyed on a global
 `Symbol.for`, so this holds across separately loaded copies of the core.
 
-Liveness is what F-Capture (J3) and F-CallLeak test.
+Liveness is the *entity test* of F-Identity (J3), and is what F-CallLeak
+tests. F-Capture and F-Import test something broader; F-Identity says which
+is normative and what the difference costs.
 
 ## F-Val-Callable (functions are callable, never values)