Spec 0019 — Lift: pure Effect → suggested effx declarations

Status: approved and frozen 2026-10-04 (decisions in §0). Implementation order: spec 0015 → S5 (monoweb-gap) → spec 0020 → spec 0024 → this spec; change this contract by editing this file explicitly. Evidence: docs/research/lift-spike.md (a throwaway recognizer over mono-web f433ea90 Profile reproduced the committed IR hash) and the mono-web corpus counts in §3. Companion reading: the "partial isomorphism" section of docs/research/2026-10-02-deep-research-report.md, specs 0001/0002/0005/0006/0009/0010/0013.

0. Operator decisions (2026-10-04)Copy Anchor Link

1. Status (amended by the operator on 2026-10-09). Lift preserves every explicit source or generated status, including HttpApiSchema.status(200). An omitted status remains omitted. S5 stays generator-owned and unchanged. Its runtime conditional preserves an unannotated or 200 schema and overrides another status when the declaration explicitly requests 200. The --status flag and the explicit/always modes remain withdrawn.

2. S1 (lifters) is delivered through spec 0020's Annotation.implement({ lift }) plus data rules; a separate Extension.lifters field is not added.

3. Order of work: spec 0015 → S5 (monoweb-gap) → spec 0020 → spec 0024 → this spec. Seams S2/S3/S4/S6/S7 are owned by this spec's implementation.

4. Dense target (spec 0024, amended 2026-10-09). Dense output retains explicit status witnesses, including 200. It omits a field only when the exact representation, wire contract, and canonical IR remain unchanged. Kind-default decisionTime, pattern-derived problem identifiers, and channels implied by input remain derivable fields. The corpus oracle (§10) is the identity-preserving dense rewrite. Binding reports target Binding.group (0024 §6). Historical status-removal measurements are evidence, not the current contract.

5. S4 (success without a body) reduces to recognition (2026-10-04). The operator's finding: success: HttpApiSchema.NoContent already declares a bodyless 204 (and, with status, other bodyless statuses) and generates WithHeaders(NoContent.pipe(status(204)), headers). Lift therefore recognises the noContentMutationResponse() family (a SuccessWrapper rule whose schema is HttpApiSchema.NoContent instead of the wrapped argument) and emits success: HttpApiSchema.NoContent with the helper's responseHeaders/status; seam S4 is withdrawn as a compiler change. The bodyless successes are the 8 noContentMutationResponse() calls and Contact's direct WithHeaders(Schema.Void.pipe(status(201)), { … }) (whose inline header object additionally needs exporting, a class-A refactor). Class C of §3.3 shrinks from 11 to 2 (documentMutationResponse, endpointProblemResponses(…, { cors: false })). The corpus counts in docs/research/lift-spike.md are the pre-decision measurement.

0.6 Director clarification (2026-10-06)Copy Anchor Link

The director approved the implementation design and these clarifications on 2026-10-06. The operator decisions of 2026-10-04 remain unchanged. These clarifications are director decisions, not new operator decisions.

• Complete the approved 0024 remainder before lift depends on it. Items 2, 4 and 5 have separate commits and each required §8 falsifier. Preserve explicit-200/201 and verbose identity witnesses.
• S1 extends the existing definition-owned implement({ lift }) interface. The old Extension.lifters proposal in §3.1, §5 and §8 is superseded.
• Registered .annotate(Key, value) calls use the definition-owned lowering plan and lift hook. Unknown annotation keys produce EFFX3001. This resolves the old blanket .annotate rejection in §3.4.
• S5 uses the existing runtime conditional described in 0024 §3, not static proof. The 2026-10-09 operator amendment requires lift to preserve explicit 200 and non-200 status witnesses. A source 200 overrides an existing 201, NoContent status, or any other status. Omission remains omission. The generator, IR, semantic-hash normalization, status modes, and review fields do not change.
• S4 is recognition only. NoContent wrappers and the direct bodyless 201 form need no compiler behavior change. Other unsupported constructs still diagnose.
• S3 resolves the declaration input from the allowed request channels or a real configured emptyInput export. No input produces EFFX3009. IR input stays required and fully resolved. No IR-v2 shape/version change, fake Schema.Void default or unresolved placeholder is permitted.
• A name map and deterministic exported schema/tuple names must resolve to real values. Unknown references diagnose. A collision cannot produce an unresolved LIFT_RENAME_ME suggestion.
• The binding report targets Binding.group from 0024 §6. Manual adaptation stays UNVERIFIED until the real key-set and generated binding typecheck conditions pass. Reports never invent handler behavior or executable placeholder handlers.
• Unsupported endpoints retain all applicable causes. Order causes by source file, source offset and then diagnostic code. The first cause is the primary diagnostic, and the remaining causes are related diagnostics. A registered metadata call with nonliteral arguments produces EFFX3001. An unregistered metadata callee produces EFFX3006. There is no partial evaluation. No unsupported endpoint appears in a suggestion.
• Replace the historical 37-endpoint negative tally with a named immutable-source inventory. Derive expected counts from source sites and their causes under §0.5. The source-only 78/30 classification is a candidate inventory, not runtime acceptance. Actual lift and check runs must confirm every site.
• --check executes the untouched original module and the actual generated module, plus registered projection hooks. Only Δ1, Δ2 and Δ3 normalize their Reflections. Missing binding evidence cannot produce an accepted result. Semantic decisions stay explicitly unverified.
• Own execution through a narrow registered adapter with native Effect services. Application imports can perform IO. The check is not a sandbox. Acceptance environments contain only explicit nonsecret inputs and never copy ambient credentials or private payloads.

0.7 Operator status amendment (2026-10-09)Copy Anchor Link

The operator selected Preserve explicit source200 on 2026-10-09. This amendment supersedes the earlier instruction to remove explicit 200 from lift and dense output. The status clauses in §0, §0.6, §2.3, §4.2, and spec 0024 now state that rule.

The distinction is observable. An omitted Http.Contract.status compiles without a status field. Explicit 200 compiles with HttpContractData.status = 200. Headered generation emits an outer status(200), and unheadered generation uses the existing S5 conditional. Removing that witness can change wire behavior and canonical IR.

L1–L5 retain their full domains, including headered explicit-200 operations in IR_nf. No new semantic delta, generator behavior, IR shape, or hash normalizer is permitted. Earlier status-removal evidence remains historical and does not establish these laws.

0.8 Operator root clarification (2026-10-09)Copy Anchor Link

The operator selected Preserve outer root; compare isolated group on 2026-10-09. Root discovery records the unique root identity, complete composition, and group references without removing source steps. The generated contract and §2.1 check concern the unmodified exported group mounted alone on a fresh comparison root.

The original application root remains untouched. Its middleware, metadata, prefixes, errors, and other outer composition remain UNVERIFIED outside the isolated-group check. The cutover report describes a manual group-reference substitution that preserves that composition. It does not generate or replace root behavior.

Binding proof still uses the actual original root types and endpoint key sets. A fresh comparison root is never a substitute binding root. Missing or ambiguous root/group membership produces EFFX3008. Group and endpoint unsupported-construct rules remain unchanged. No new delta, global IR fact, generator behavior, or whole-application acceptance claim is permitted.

0.9 Director source-position clarification (2026-10-09)Copy Anchor Link

The director approved required SourceFileRecord.end source metadata for cross-file refactors. It records the UTF-16 end position of the exact hashed file text.

The core inserts a cross-file planned export at the target file's end. It keeps same-file exports at the original endpoint statement.

If source import facts cannot prove a safe cross-file plan, the core emits EFFX3001 and omits the affected endpoint.

This internal source fact changes no Term, IR, semantic hash, generator behavior, or wire contract.

1. Problem and non-goalsCopy Anchor Link

effx is one-way today: annotated TypeScript → IR → ordinary Effect. mono-web already holds 108 hand-written HttpApiEndpoints that humans lifted by hand into *.effx.ts (Profile, Directory, SocialEvents; Content later). The reverse tool reads pure Effect and suggests an effx declaration whose generated Effect is functionally isomorphic to what was read.

 P  pure Effect module(s)          S  suggested .effx.ts
 ──────────────────────  lift  ──▶  ───────────────────
        ▲                                   │ compile + generate (existing pipeline, unchanged)
        │ ≈  (§2, mechanical)               ▼
        └────────────────────────────  lower(S) = generated Effect

Non-goals: lifting arbitrary Effect programs; rewriting user files in place by default; inventing handlers; proving handler behaviour; changing the forward semantics of any extension; RPC/CLI lift beyond the architecture in §9.

Invariants that bind this spec: ADR 0001 (decorator = contribution to IR), invariant 5/10 (no ts.* in IR; schemas are SchemaRef), invariant 11 (diagnostics are data). Lift never lowers fidelity silently: a site it cannot represent exactly is a diagnostic, never a guess.

2. Correctness definitionCopy Anchor Link

2.1 Reflection and congruenceCopy Anchor Link

Let reflect(G) be the Reflection of an HttpApiGroup G mounted alone on a fresh root HttpApi.make(rootId).add(G):

Reflection = {
  openapi: OpenApi.fromApi(root), // the wire contract
  endpoints: Array<{
    group;
    identifier;
    method;
    path; // HttpApi.reflect onEndpoint
    middleware: string[]; // sorted middleware keys
    successStatuses: number[];
    errorStatuses: number[];
    annotationKeys: string[]; // merged Context keys, sorted
    projections: Record<string, Json>;
  }>, // app hooks (§5.4): e.g. AccessSpec JSON
};

≈ is equality of Reflections after the closed set of delta normalizers Δ (§2.2) and nothing else. Key order of JSON objects is never significant; array order is.

2.2 Accepted iffCopy Anchor Link

A suggestion S for source P (group G, root id r) is accepted iff

1. S compiles with zero error diagnostics (strictAccess as the project sets it);
2. reflect(G_P) ≈ reflect(G_S), where G_S is the group exported by generate(compile(S)) (--emit=contract) built against the refactor overlay of §2.4; and
3. handler bindings agree (§7).

Δ is the complete list of tolerated differences. Each has a mechanical normalizer, a cause in Effect behaviour, and an observed instance; anything outside it fails.

A Δ is only applied when its premise holds in the data (Δ1's deep-equality, Δ2's equality); a Δ that would hide a real difference does not fire. Δ2 and Δ3 are exact; Δ1 is the only one that renames anything. A new Δ is an edit to this table with a cited Effect mechanism, never a CLI flag.

What is not tolerated (each seen to fail in the spike's negative controls): path, method, parameter/body/response schema, status, response header, media type, security, operation id, summary/description/tags, x-* extensions, middleware set, access projection.

2.3 What the check cannot seeCopy Anchor Link

The IR contains facts with no Effect twin, so no wire check can validate them. They are lift decisions, printed as a reviewable list and never as "verified":

2.4 The mechanical check (--check)Copy Anchor Link

Everything in one throwaway directory, nothing written outside it:

1  overlay  = copy of the package that owns P  (cp -r, node_modules shared by symlink)
2  apply    the refactor patches of §4.3 to the overlay (they only add exports / name literals)
3  write    S into the overlay; run compile(S) --emit=contract into overlay/.effx/generated
4  write    overlay/lift-check.ts  (generated; imports G_P from the ORIGINAL package, G_S from the overlay)
5  run      `bun overlay/lift-check.ts` as a child process → Reflection×2 on stdout
6  decode   both documents with the Reflection Schema, apply Δ, diff
7  report   PASS | PASS(Δ1,Δ2,…) | FAIL(diff) ; exit code 0 | 0 | 2

Step 5 executes application modules (as mono-web's own generate-openapi.ts does). That is the one place effx evaluates user code; plain effx lift never does. The program is generated, not hand-written, so it is the same for every app: it needs only HttpApi, OpenApi and the app's optional projection hooks. Failure to build either root is EFFX3103, not a pass.

Because refactors (step 2) change the module graph, G_P is loaded from the unmodified package: the check therefore also proves the refactors wire-preserving (a refactor that changed behaviour appears as a FAIL in Δ-normalized diff).

2.5 LawsCopy Anchor Link

lower(S)  ≜ generate(compile(S))               partial; defined when compile has no errors
NF_effx   ≜ the image of lower, plus the hand-written forms of §3

IR_nf = HTTP-only operations with binding: "external", kind determined by method (GET ⇒ Query), input equal to the canonical channel, name = operationId = <group>.<key>, no Authorize/PersistentModel/Rpc/Cli exposures, no declared errors/requirements, no commandIdentity. This is the exact set of IR facts lift can recover; everything else is outside NF and L2 does not claim it.

lower∘lift ≈ id only up to ≈ (not byte equality); lift∘lower = id is at IR level. These are different strengths on purpose: the first is a wire claim, the second a syntactic claim over code effx itself wrote.

3. The recognizer (NF_effx)Copy Anchor Link

3.1 Architecture: terms, not ts.*Copy Anchor Link

TypeScript Program ──(frontend-ts "lift frontend")──▶ EffectModel  { endpoints, groups, roots, bindings }   neutral Term trees
EffectModel ──(core lifter ⊕ definition-owned implement({ lift }))──▶ LiftResult { collected: Collected, refactors, decisions, diagnostics }
collected ──(existing compileCollected)──▶ IR ──▶ semanticHash
collected ──(print)──▶ .effx.ts text (verbose), dense(collected) ──(print)──▶ dense text

Term = Lit(Json) | Ref(SchemaRef | SymbolRef)                    // resolved exactly as frontend-ts resolves refs today
     | Call{ callee: SymbolRef | { member: string }, args: Term[], chain?: Term[] }
     | Obj{ props: Record<string, Term> } | Arr(Term[]) | Opaque{ display }   // + location in the manifest, not the Term

The frontend lowers AST → Term (the only module touching ts.*; ADR 0009). Lifters are pure functions over Term. This mirrors the forward split (frontend lowers, extensions interpret) and keeps invariant 10. Reference resolution reuses exportedSymbol/schemaRefOf (packages/frontend-ts/src/resolve.ts), so SchemaRefs of lifted and hand-written declarations are identical by construction (re-exports resolve to the declaring module).

3.2 LevelsCopy Anchor Link

3.3 Shape table and mono-web countsCopy Anchor Link

Counts: mono-web main = f433ea90, packages/http-api/src (25 files, 15 containing endpoints), a syntactic AST scan with @typescript/typescript6. 108 endpoints = 107 export const X = HttpApiEndpoint.<verb>(key, path, {…}) chains + 1 wrapped as annotateAccessSpec(HttpApiEndpoint…, CONST). Verbs: GET 59, POST 41, PATCH 5, DELETE 3. Key, path and options object are literals in 108/108; no computed paths, no spread options. 16 HttpApiGroup.make(id).add(…).annotateMerge(OpenApi.annotations({title, description})) classes (one with exclude: true); none uses group prefix/middleware/addError. Root: ExternalNativeApi (15 groups) and InternalNativeApi (1).

Success wrappers over the 107 chained endpoints: privateReadResponse 39, entityMutationResponse 26, createdMutationResponse 11, noContentMutationResponse 8, privateConditionalResponses 6, noStoreReadResponse 5, publicConditionalResponses 5, dynamicAdmissionConditionalResponses 2, plain schema 2, privateEntityMutationResponse 1, direct HttpApiSchema.WithHeaders 1, documentMutationResponse 1.

Combined, by the worst construct of each endpoint (C outranks B outranks A2 outranks A1):

The preceding combined classes are the historical pre-§0.5 measurement, not the current acceptance inventory. The named immutable-source inventory derives recognizable and unsupported counts from each site and all causes (§0.6). Each unsupported endpoint diagnoses and has no suggestion. Shared schema/tuple exports remain refactors, not hidden prerequisites.

3.4 Recognition rules (core lifter)Copy Anchor Link

The core lifter is the exact inverse of packages/compiler/src/generate/http.ts:endpointExpr. Normal form emitted by effx:

HttpApiEndpoint.<verb>("<key>", "<path>", { params?, query?, headers?, payload?[.pipe(asJson)], success, error })
  .middleware(M)*                                        // declaration order
  .annotateMerge(OpenApi.annotations({identifier, summary?, description?, override?{tags}}))
  .annotateMerge(<metadataAnnotator>({…}))?
  .annotateMerge(<accessAnnotator>({…}))?

The recognizer accepts a superset: any ordering of .middleware/.annotateMerge/.pipe(e => W(e, …)) steps whose targets commute (annotation keys are disjoint, so context merge order is irrelevant; the check verifies it), the outer-wrapper form W(HttpApiEndpoint…, …), X.pipe(HttpApiSchema.status(n)), and Schema.Struct(fields) vs bare fields. Registered .annotate(Key, value) steps use their definition-owned lift. Unknown annotation keys, unknown .pipe callees, setHeaders and prefix produce EFFX3001 and omit the endpoint.

Bare-fields rule: X.fields (the query case in 15 corpus sites) is not X: X carries an identifier annotation and would add a component to OpenAPI. The refactor suggests export const XQuery = Schema.Struct(X.fields) (the human lift did exactly this: SocialEventScopeQuery).

4. OutputCopy Anchor Link

4.1 CLICopy Anchor Link

effx lift --group <id> [--project tsconfig.json] [--module <file>]
          [--form verbose|dense|both]
          [--check] [--emit-patch] [--write <file>] [--json]

--group matches the identifier in HttpApiGroup.make("<id>") (class or const). The root is the unique HttpApi.make(...) value whose .add(...) contains that group; zero or several is EFFX3008. No other flag reads or writes files.

Never rewrites a user file. The default prints to stdout. --write <file> writes only the suggested .effx.ts, and refuses to overwrite an existing file. Source refactors are printed as a unified diff with --emit-patch; nothing applies them. Cutover (re-pointing api.ts at the generated group) is listed as a required edit, never performed.

4.2 Report (stdout; --json prints the same as one Schema-encoded document)Copy Anchor Link

1  SUGGESTION (verbose)       a complete .effx.ts, builder form
2  SUGGESTION (dense)         same IR, group defaults (spec 0013)  — only when it compiles to the same hash
3  REFACTORS REQUIRED         per source symbol: file, why (EFFX3002-3004), unified diff
4  DECISIONS TO REVIEW        §2.3 table instantiated: kind, input, real export names
5  ADAPTER PREREQUISITES      symbols the lifter table names that do not resolve in the project
6  UNLIFTABLE                 endpoints omitted, one primary diagnostic plus all related causes
7  CHECK                      only with --check: PASS | PASS(Δ…) | FAIL + diff

The dense form hoists shared fields and uses .in(Group). It omits only fields whose exact representation, wire contract, and canonical IR remain recoverable. These include default success, channels implied by input, default decisionTime, pattern-derived identifiers, and derivable operation ids. Explicit status witnesses, including 200, remain. Dense output requires canonical IR equality with the verbose suggestion (L4). Historical spike sizes remain evidence, not a required layout.

4.3 Refactor suggestionsCopy Anchor Link

Every refactor is wire-preserving by construction and re-checked by §2.4. Shapes, with the human diffs they reproduce at mono-web Profile:

The name rules use the lifter's names map first, then deterministic collision-free exported names. Each suggested export contains a real schema or tuple initializer. Unknown adapter references diagnose rather than produce executable placeholders.

5. Adapter inference (definition-owned lift implementations)Copy Anchor Link

5.1 Why a plugin pointCopy Anchor Link

The IR knows nothing of personNativeAccess, privateConditionalResponses, nativeOperationAnnotations or endpointProblemResponses. Those are the application's derivations — the forward direction already routes them through user-exported functions (Http.Access.annotator, Http.Problems.registry, Http.Contract.metadata.annotator) that effx calls but never evaluates. The reverse direction needs their inverses, and they belong to the same owner. Hard-coding mono-web would repeat the mistake spec 0005 avoided in the forward direction.

5.2 ContractCopy Anchor Link

// Register each lift hook with the existing definition-owned implement({ lift }) seam.

interface Lifter {
  readonly name: string;
  readonly rules: ReadonlyArray<LiftRule>; // pure; Term → Option<Lifted>
  readonly names?: Readonly<Record<string, SymbolRef>>; // §2.3: pinned export names
  readonly emptyInput?: SchemaRef;
  readonly project?: Readonly<Record<string, ProjectionHook>>; // check-time projection of opaque Context values (§2.1)
}
type LiftRule =
  | {
      _tag: "SuccessWrapper";
      callee: SymbolRef;
      responseHeaders: SymbolRef;
      conditional?: true;
      status?: number;
    }
  | { _tag: "ProblemRegistry"; response: SymbolRef; union: SymbolRef; registry: SymbolRef } // endpointProblemResponses + problemUnion → Http.Problems
  | {
      _tag: "Metadata";
      callee: SymbolRef;
      annotator: SymbolRef;
      positional: ["summary", "description"];
    }
  | {
      _tag: "Access";
      callee: SymbolRef;
      annotator: SymbolRef;
      arguments: ArgPattern;
      emit: AccessTemplate;
    };

LiftRules are data (Schema-decoded JSON, shipped as effx.lift.json or tsconfig.effx.lift): callee/responseHeaders/annotator/registry are SymbolRefs the frontend resolves; AccessTemplate is a small closed expression language ($arg("capability"), $const, $ifPresent(arg, a, b)) — enough for the four mono-web builders; no code runs in the compiler. A code plugin (Lifter implemented in TypeScript, loaded as a build tool like an oxlint plugin) is the escape hatch for logic the data language cannot express; it lives behind the same interface and is not needed for the corpus. The trust boundary: data rules are inert; a code plugin is trusted build tooling and never evaluates the user's application program.

The mono-web "native" table the spike hard-coded (the would-be effx.lift.json):

5.3 Wrapper discovery (assist, not authority)Copy Anchor Link

effx lift --suggest-rules may propose SuccessWrapper entries by unfolding a helper's body ((s) => WithHeaders(s, H) or the 200+304 pair) and finding H. It prints a table to review; it never changes the lifter. Authority is the table plus the mechanical check: a wrong entry fails §2.4.

5.4 Opaque annotationsCopy Anchor Link

HttpApiEndpoint annotations are opaque Context keys. The check compares keys generically and a ProjectionHook JSON for keys the lifter registers (mono-web: reflectAccessSpec → AccessSpec JSON). The OpenAPI document already carries credential security through the app's transform, but the raw projection is the stronger comparison (the spike compared both).

5.5 The adapter law and the naming gapCopy Anchor Link

Forward annotator(spec) and reverse Access rule are mutually inverse by obligation of the app: ∀spec. rule(callTerm(annotator(spec))) = spec modulo the app's own registry. The check enforces it per endpoint (AccessSpec projection equal). The Profile profileAccessAnnotations/ProfileCurrentPerson adapter pair (67 lines at 188f2385 (unpublished)) is exactly this inverse, hand-written once per group; the lifter should require it or scaffold it from the same Access rule (follow-up, not v1). Because the exported names of resolvers/annotators/registries enter the IR hash as SymbolRefs but not the wire, hash equality with a human lift needs those names pinned in names (§2.3); the OpenAPI check does not care.

6. DiagnosticsCopy Anchor Link

Reserved range EFFX3xxx. Severity error unless noted; "refactor" diagnostics carry the patch and do not block printing a suggestion, they block --check unless an overlay is applied.

7. Handler bindingCopy Anchor Link

mono-web: 16 HttpApiBuilder.group(root, id, h => …) sites; 108 .handleRaw( calls, 0 .handle( (the 109th grep hit is a doc comment). The effx side is the generated <Group>ApiHandlers({ raw, guards }) factory (spec 0010), which binds exactly the same keys.

Lift recognizes the chain HttpApiBuilder.group(R, "g", h => h.handleRaw("k", fn)…) (also under Effect.succeed) as a BindingTerm { root, group, keys, kind: raw|normal } and:

1. checks key-set equality with the group's endpoints (EFFX3201) — static, no execution;
2. reports the backend-owned Binding.group declaration required by 0024 §6, with resolved handler/guard exports where available; manual adaptation stays UNVERIFIED and never becomes executable placeholder code;
3. flags every call of the app's authorization function inside the handler (EFFX3202): moving it behind the lazy authorize() callback is the one change that cannot be mechanical (the human lift adapted readOwnProfile/updateOwnProfile by hand).

"Same handler binding" in §2.2.3 is therefore: key sets equal, and the rewritten call typechecks against the generated factory (the overlay's tsc), with authorize sites listed. Handler behaviour is out of scope (spec 0009's journey owns it). .handle bindings (none in the corpus) are key-checked and reported EFFX3202; mapping {params,query,headers,payload} onto effx's merged input is deferred.

8. Compiler seams required (owner: compiler)Copy Anchor Link

No seam changes IR v2, any existing extension's semantics, or any committed hash.

9. Scope and later targetsCopy Anchor Link

This spec is HTTP-only because the corpus is HTTP-only. RPC and CLI lift require separate specs and corpora. Unsupported group and endpoint constructs produce EFFX3001: group prefix/middleware/addError, HttpApiBuilder.securityDecode, multipart or stream bodies, form-encoded payloads, and endpoint path rewriting. Outer composition of the original application root is preserved under §0.8, not rejected as group behavior. Root discovery retains full source steps and unique group references without generating root middleware, metadata, prefixes, or errors. The isolated-group check does not verify those outer behaviors.

10. Tests and falsifiersCopy Anchor Link

1. Corpus (committed fixtures, no mono-web import): vendor f433ea90's profile.ts, directory.ts, social-events.ts and their support modules as a fixture package (as rc116 does). For each group: lift with the pinned mono-web effx.lift.json and names map ⇒ the IR equals the IR of the 0024 dense rewrite of the committed .effx.ts (equal to the committed IR except HttpContractData.status, 0024 §3) (docs/research/{profile,schools,social-events}-slice-evidence.md) compared as canonical IR, plus semanticHash for the same compiler commit. Historical doc hashes (0e628ff8…, 727fcbf7…, 615feee5…) were produced by compilers 17374d6/efdc19a; the test pins the hash of the committed declaration rebuilt by the test's own compiler, so compiler evolution cannot silently rebase the oracle. (Spike: main 5de7921 and the vendored f3c6bf8 CLI produce identical Profile IR.)
2. L2 property test: generate Collected over a fixed universe of exported schemas/markers/registries/annotators for IR_nf (HTTP contract, problems, access data from the existing HttpContractData/ProblemContractData/AccessContractData Schemas via the Arbitrary adapter, filtered to NF), then decode(endpointTerm(x)) = x (pure, many runs) and parseTerm(print(t)) = t (TS, ≥25 runs, one in-memory program).
3. L1 per liftable corpus endpoint: --check PASS (or PASS with only the Δ classes of §2.2); the spike's negative controls must FAIL and name the differing path: a mutated summary and a mutated request media type did (lift-spike.md); a mutated status changes the IR hash and must additionally be added as a wire control.
4. Negative fixtures: one per EFFX3xxx. A named inventory pinned to immutable corpus source lists each unsupported endpoint and all expected causes. Counts derive from that inventory under §0.5, not the historical 37-site tally. Each site produces its deterministic primary/related diagnostics and no suggestion text. Actual lift/check runs confirm the source-only classification.
5. Totality: lifting never throws; a lifter-rule exception is EFFX3103.
6. Idempotence (L3) over the corpus; dense (L4) hash equality on all three corpus groups.
7. bun run typecheck, effect:diagnostics, lint, fmt:check, test, plus the new tests; no existing hash or generated byte changes.

Order of work (after 0015, S5, 0020 and 0024 land): S2 (pure term/printer split, byte-identical output) → S7 + core lifter + Profile corpus test → S1 via implement({ lift }) + plugin table + Directory/SocialEvents → S6 effx lift + --check → S3/S4 → binding. Each slice: own worktree, bun run check, effect:diagnostics, rc116 fixture, fast-forward, pack, cleanup.