Spec 0009 — Profile proving slice

Status: spec-frozen 2026-10-03. This freezes the observable Gate 3 contract from spec 0004 §4–5. It does not claim that the compiler or mono-web integration already implements it. Change this contract explicitly if source evidence falsifies it. No production cutover, credentials, deployment, legacy writer change, or publication is authorized.

Outcome and source boundaryCopy Anchor Link

The unchanged mono-web just e2e profile journey runs against an effx-generated Profile HttpApiGroup, a generated Profile raw-handler binding, and the canonical mono-web SDK. It traverses browser → React Router proxy → Better Auth → native HTTP → existing authorization/receipt transaction → disposable PostgreSQL. The generated contract replaces only profile.readOwnProfile and profile.updateOwnProfile. Mono-web keeps its Profile domain, SQL, ProfileLive, authorization interpreter, handleRaw behavior, request/response semantics, Foldkit Model/update/view and proxy (docs/research/profile-baseline.md; mono-web packages/database/src/profile/{postgres,postgres-layer}.ts; apps/backend/src/profile/http.ts).

Dependency direction: effx compiles exported mono-web declarations as source input but never imports @vektorprogrammet/* in effx code or package dependencies. Mono-web installs a pinned effx distribution artifact, not a path into the effx workspace. The only installed Effect in mono-web's application dependency graph remains its selected/patched release. Effx's CLI runs as a separate build process and does not provide an application runtime or service Layer (effx AGENTS.md; mono-web AGENTS.md#boundary-practices).

Baseline source is mono-web f433ea906c9f9af5134c7316d54c78d8c859038f and Effect 4.0.0-rc.116, in the retained clean mono-web-effx-baseline worktree. The exact source count is 18 files / 2,355 physical lines including apps/dashboard/app/foldkit/profile/elements.ts (docs/research/profile-baseline.md). Gate 0 passed on the original hand-written code, not the generated path.

Portable dependency and generationCopy Anchor Link

Choose vendored immutable package artifacts. Build a release-grade @effx/runtime tarball and a self-contained @effx/cli tarball from a named effx commit. Commit them under mono-web tools/effx-dist/ with a source-revision/digest manifest. Install @effx/runtime from file:../../tools/effx-dist/runtime-<digest>.tgz in packages/http-api, and the CLI from a repository-relative file:tools/effx-dist/cli-<digest>.tgz root devDependency. Commit the resulting bun.lock. Update the mono-web ignore/layout declarations to admit exactly these immutable artifacts while keeping .effx/**, OpenAPI JSON and the SDK operation index ignored. The packaged runtime uses mono-web's Effect as a compatible peer and installs no second application Effect. The bundled CLI includes or portably resolves its compiler/frontend/IR/@effect/platform-bun closure in its own build process. It must not rely on workspace:* at install time (effx packages/{runtime,cli,compiler,frontend-ts}/package.json; mono-web package.json:33-50, .gitignore:11-13, tools/conventions/src/layout.ts).

This artifact does not exist yet: effx packages are private, at 0.0.0, export source, and the CLI depends on workspace packages and imports @effect/platform-bun without declaring it. Packaging and a target-compatible runtime type surface are prerequisites, not a successful install claim. A sibling file:../../../effx/packages/* path is absent on a clean hosted checkout. bun link is machine-local and not a locked distribution. Both alternatives fail the portable frozen-lockfile requirement. Neither path is accepted as a temporary passing gate (effx packages/cli/package.json:1-17, packages/cli/src/main.ts:1-6; mono-web devenv.nix:293-305, .github/workflows/checks.yml:24-47).

Create two source-project configs with the same explicit monorepo root identity and only packages/http-api/src/profile.effx.ts as a collected entry. From the mono-web worktree, inside its pinned devenv shell, run a repository recipe just effx-profile. The recipe invokes the installed effx build --project packages/http-api/tsconfig.effx.json --strict-access --emit=contract and effx build --project apps/backend/tsconfig.effx.json --strict-access --emit=handlers in that order. --emit and contract-only/handler modes are required effx CLI changes, not flags supported today. Both passes must produce the same normalized Profile IR/hash. The contract pass writes only packages/http-api/.effx/generated/profile-contract.ts; the handler pass writes only apps/backend/.effx/generated/profile-handlers.ts. They are derived, ignored files, never copies in effx. The current CLI writes four files into one <dirname(tsconfig)>/.effx/generated and has no --outDir or --emit flag, so the present CLI cannot satisfy this layout unchanged (effx packages/cli/src/{main,commands}.ts, packages/compiler/src/generate/{http,client}.ts).

The HTTP package's generate script runs the contract pass before its existing generate-openapi.ts imports ExternalNativeApi. The backend package generates its handler pass before typecheck/build. Turbo's generate outputs include both derived paths; the just effx-profile prerequisite runs before type-aware just lint, just check-types, and just check, so a fresh worktree does not lint/typecheck missing generated imports. The SDK's generate remains downstream of HTTP generation. Its own test must depend on its generate so the new index-parity test works in a fresh tree (mono-web turbo.json:7-27, justfile:44-104, packages/{http-api,sdk}/package.json). Add both generated directories to the owning TS project includes and prove devenv shell -- bun install --frozen-lockfile before any gate. Do not disable the pre-merge hook or run generation in the operator-owned main checkout.

Declaration and generated contractCopy Anchor Link

Place the only Profile effx declaration at packages/http-api/src/profile.effx.ts, beside the existing contract schemas. Use a declaration-only builder with Operation.query(...).http.get(...).http.contract(...).http.problems(...).http.access(...).declare() and the analogous command/PATCH chain. This lowers the same semantic Query/Command and Http.* annotations as the proposed decorators, but contains no fake callable handler. The suggested @Query/@Command decorators on static methods need a real implementation. Importing a backend handler into the contract package reverses the dependency. An unused stub misstates executable behavior. Effx must add an explicit declaration-only mode with a required external raw binding. Its current Operation.handler: SymbolRef, static-method collector, and generated .handleAll assume a callable handler (effx packages/compiler/src/extensions/core.ts:171-223, packages/frontend-ts/src/collect.ts, packages/compiler/src/generate/http.ts:169-239). No inferred empty E/R may masquerade as checked errors; declaration-only operations require explicit failures/requirements or a generated type check against every bound raw callback and guard. An unmapped failure must fail compilation, not pass vacuously (effx packages/compiler/src/extensions/problem-contract.ts:164-197).

One group-level annotation must preserve title Profile, description Authenticated self-service profile API. and x-displayName: Profile (profile.ts:129-143). Export distinct response-header schemas from the existing http-semantics.ts primitives for the private GET and mutation PATCH. Refactor its existing response helpers to share these definitions, not copy cache literals into the effx declaration. The generator needs group-level OpenAPI annotations and a contract-only emission mode. A validated endpoint name, distinct from the stable IR operation id, must drive the emitted endpoint key, generated binding key and SDK lookup. metadata.operationId supplies profile.<endpoint key>; reject a mismatched group prefix, empty suffix or duplicate name. Today effx uses the IR operation name for the endpoint/client key even when OpenAPI metadata gives another ID (effx packages/compiler/src/generate/{http,client}.ts).

The declaration's Http.Problems.codes are the single source of each Profile list, using exported readonly tuples rather than parallel arrays in endpoint-problems.ts. GET codes: request.malformed, header.malformed, precondition.invalid, precondition.failed, authority.denied, origin.denied, internal.error, profile.not-found, profile.unavailable. PATCH codes: request.malformed, header.malformed, authority.denied, origin.denied, idempotency-key.invalid, idempotency.in-flight, idempotency.digest-conflict, idempotency.response-expired, request.too-large, media-type.unsupported, validation.failed, validation.no-change, validation.field-not-deletable, precondition.invalid, precondition.failed, precondition.required, transaction.conflict, internal.error, profile.not-found, profile.unavailable, idempotency.unavailable (packages/http-api/src/endpoint-problems.ts:91-127). PersonSecurity contributes credential failures separately. A contract-owned nativeProblemResponses(identifier, codes) derivation composes endpointProblemResponses(problemUnion(identifier, codes)) using NativeProblemRegistry; it is the Http.Problems.registry symbol. The generator supplies exact ProfileReadOwnProfileProblem and ProfileUpdateOwnProfileProblem schema identifiers rather than its current <operationName>Problem default. Its registry signature must preserve the nonempty NativeProblemCode tuple type, not cast a plain ReadonlyArray<string> into it (effx packages/runtime/src/Annotation.ts:50-54; mono-web http-semantics.ts:1144-1158,1517-1539). Keep profileProblems and commandReceiptProblems as backend failure mappings until parity; generated problem schemas are declarations, not failure translation.

A contract-owned profileAccessAnnotations derivation converts effx's named Http.Access fields to the existing personNativeAccess and accessSpecAnnotations, preserving cookie/bearer alternatives, Person, capability, owner requirement, profile.current-person resolver and decision time. Export a symbol for that resolver; map it explicitly to the registered resolver ID rather than guessing from the export name. The generated endpoint uses the resulting Context annotation after PersonSecurity. Effx must not import mono-web AccessSpec or implement its interpreter (effx docs/specs/0006-access-contract-extension.md:28-79,122-153; mono-web packages/http-api/src/access.ts:76-104,322-378).

The generated profile-contract.ts exports endpoint constants and ProfileApi only. It imports contract-owned schemas/derivations, never a backend handler. packages/http-api/src/api.ts replaces .add(ProfileApi) from the old profile.ts with this generated group exactly once. It retains the other 14 external groups, root error middleware, root metadata and separate internal receipts root. Do not import effx's current partial root/AppRoutes into that shared package: today's http.ts combines groups, handler implementations and a new root in one file (mono-web packages/http-api/src/api.ts:25-88; effx packages/compiler/src/generate/http.ts:197-310). Migrate tests and backend uses of ReadOwnProfileEndpoint/UpdateOwnProfileEndpoint to the generated endpoint constants or ExternalNativeApi.groups.profile.endpoints. Remove obsolete Profile declarations and code-list exports; do not retain compatibility aliases (mono-web apps/backend/src/profile/http.ts:20-26,210-212,260-262, apps/backend/src/test/native-http.ts:32-34,108-110,288-295).

Generated handler and authority adapterCopy Anchor Link

Emit apps/backend/.effx/generated/profile-handlers.ts as a separate backend-owned artifact. Profile's Http.Group declaration names the exported concrete ExternalNativeApi value as its root symbol, rather than passing a generic root into the factory. The generator imports that value from packages/http-api/src/api.ts in the backend artifact and emits ProfileApiHandlers({ raw, guards }). It registers both operations through HttpApiBuilder.group(ExternalNativeApi, "profile", ...) with .handleRaw("readOwnProfile", ...) and .handleRaw("updateOwnProfile", ...). The imported full root supplies native group/endpoint types; no cast or partial root/AppRoutes is permitted. The generated contract imports neither the backend factory nor the root, so the dependency runs backend → HTTP API, never in reverse. During the one-time replacement, the existing handwritten Profile group keeps ExternalNativeApi source-resolvable until its generated contract replaces that group. Require every raw/guard record key at compile time; reject duplicates/missing handlers and callbacks with undeclared failures (effx packages/compiler/src/generate/http.ts; mono-web apps/backend/src/profile/http.ts:344-354, apps/backend/src/router.ts:209-221, packages/http-api/src/api.ts:25-88).

The raw record in apps/backend/src/profile/http.ts delegates to the existing readOwnProfile and updateOwnProfile helpers via webHandler, with a lazy authorization callback. Adapt each helper to accept and invoke that callback at its current authorizePerson site. GET resolves the actor and checks the generated endpoint's reflected AccessSpec in the read snapshot. PATCH parses Idempotency-Key, If-Match and strict merge-patch before executeNativeHttpCommandPostgres. Inside that executor's prepare transaction, the lazy guard resolves resolveRequestPersonAuthorityInTransaction and checks the generated update AccessSpec on every retry. It returns the authorized actor to the existing ETag/revision check and Profile.use(updateOwnProfile) path. Keep receipt lookup before the precondition, the two revision fences, committed response bytes, replay, strict output, stale conflict and denial behavior. Do not add a pre-transaction authorization step or reuse a prior decision (apps/backend/src/profile/http.ts:119-161,163-201,202-354; apps/backend/src/http-api/receipt-transaction.ts).

For raw mode, bind the guard to the same Web Request that webHandler obtains from HttpServerRequest, and call it lazily from the helper. Do not convert or consume a PATCH body twice. The generated raw factory passes an authorization function to the adapter; the adapter attaches the converted request after webHandler runs. This is a required raw-mode refinement of spec 0006's HttpServerRequest guard interface, not silent compliance with its current nullary signature. Preserve the security marker/type gate and require one typed guard per qualified operation ID (profile.readOwnProfile, profile.updateOwnProfile). Mono-web's transport already constructs a header-only Web Request for credential checks (apps/backend/src/http-api/transport.ts:145-153,175-183), but this slice must not clone a body stream (installed HttpServerRequest.ts:1053-1077). The factory and the backend adapter run no independent Effect runtime. The existing router, main, ProfileLive, database and identity layers remain the composition root (apps/backend/src/main.ts:94-98,153-167, packages/database/src/profile/postgres-layer.ts:13-42).

.handleRaw opts out of automatic payload decoding, not parameter/header/query decoding. Its HttpServerResponse result bypasses automatic success encoding; the existing readJsonPatch, conditionalJson and commandOutcomeResponse still own the exact bytes/status/headers. The generator's current .handleAll spreads decoded headers/payload into a handler and cannot return the existing Web Response path. This is an explicit generator change, not a cast around the type mismatch (installed mono-web HttpApiBuilder.ts:827-890, HttpApiEndpoint.ts:589-607; effx packages/compiler/src/generate/http.ts:169-195,226-238).

SDK, index and browser continuityCopy Anchor Link

packages/sdk/src/effect-client.ts keeps one HttpApiClient.make(ExternalNativeApi, { baseUrl, transformClient }). Because ExternalNativeApi now includes the generated Profile group, its client.profile.readOwnProfile and client.profile.updateOwnProfile are generated from that group while the other 105 operations remain unchanged. Keep promise.ts, its cookie/Origin/headers/fetch/credentials transform, the same-origin dashboard loader/action and proxy. Do not instantiate effx's standalone generated client.ts service: it has a second root/Fetch layer and lacks mono-web's caller-controlled credential transform. In this slice, the effx-generated Profile contract is the source consumed by Effect's single generated SDK client; client.ts is not a second runtime client (mono-web packages/sdk/src/{effect-client,promise}.ts, apps/dashboard/app/{lib/api.server.ts,routes/__foldkit.profile.ts,routes/dashboard.profile.rediger._index.tsx,foldkit/profile/browser-client.ts}; effx packages/compiler/src/generate/client.ts:47-94).

Keep one operation index: packages/sdk/scripts/generate-operations.ts projects OpenApi.fromApi(ExternalNativeApi) into the ignored native-api-operations.json. Do not invent an effx-maintained second list: effx's current CompileResult.index is an IR graph index, not this SDK catalog. Add an SDK test for exact sorted {group, method, operationId, path} equality between the canonical API projection and generated JSON. Assert unique IDs, 107 external operations (2 Profile and 105 unchanged), and no internal endpoint. Independently project the generated ProfileApi group, compare its two tuples to the Profile index subset, and compare the group endpoint keys to keys of both Effect and Promise clients. The test must run after SDK generate, including under just test on a clean tree. Keep the OpenAPI contract and browser's PUT /profile proxy to native PATCH /api/profile unchanged (mono-web packages/sdk/scripts/generate-operations.ts:24-56, apps/dashboard/app/routes/__foldkit.profile.ts:61-86).

Falsifiers and acceptance at the migration revisionCopy Anchor Link

1. Portable clean clone: in a new isolated worktree, the committed effx artifacts and bun.lock permit devenv shell -- bun install --frozen-lockfile without an effx sibling checkout, registry publication, bun link, or second application Effect. Deleting either vendored artifact must fail loudly.
2. Source/IR: declaration-only source has no callable stub, both CLI passes produce the same Profile semantic hash, and generated contract code imports no backend module. Negative fixtures reject absent binding, duplicate key, wrong method/path, mismatched operation ID, missing security marker, unsupported target Effect import and unmapped typed failure. The generated artifacts typecheck under mono-web's rc.116 exports and its patch, not only effx Effect 4.0.0.
3. Contract diff: exact generated GET/PATCH request/response schemas, 200/304 statuses, headers, media type, group OpenAPI metadata, AccessSpec (cookie/bearer, scope, decision time), endpoint problem unions and middleware match the frozen profile.ts/endpoint-problems.ts. The native contract still has 108 endpoints in total: 107 on ExternalNativeApi and one on the separate internal root. The 105 non-Profile external tuples do not change.
4. Security and transport: the generated factory binds .handleRaw for both operations on the full external root. An unauthenticated GET/PATCH yields 401 problems. A successful edit returns fresh fields and ETag; malformed/unknown fields and unsupported media are rejected. A competing write yields stale 412, same-identity replay preserves response bytes, changed digest yields 409, and another actor cannot update the profile. Axe has no serious/critical form violations (apps/dashboard/e2e/native-profile-self-edit.spec.ts, docs/research/profile-baseline.md).
5. Run actual gates serially under mono-web's machine-wide heavy lock in the integration worktree: devenv shell -- just measure --class e2e -- just e2e profile; devenv shell -- just measure --class test -- bun run --cwd apps/backend vitest run src/profile/http.test.ts --no-file-parallelism --maxWorkers=1; devenv shell -- just measure --class test -- bun run --cwd packages/database vitest run src/profile/postgres.test.ts --no-file-parallelism --maxWorkers=1; devenv shell -- just measure --class check -- just check --concurrency=1. Every command exits 0 at the same committed migration revision. Do not infer the generated path from Gate 0's original passing run. Keep unrelated processes and the operator's main checkout untouched.
6. Count maintained source: use the 18 Profile responsibilities in docs/research/profile-baseline.md (17 listed rows plus profile/elements.ts). Replace obsolete paths with their hand-written successors. Include new mono-web declarations, access/problem adapters and backend binding adapters. Exclude tests, migrations, shared infrastructure and generated output. Report (after − 2,355) physical lines with wc -l. Count the generated effx contract/handler/client artifacts and SDK/OpenAPI derivations separately. No reduction claim without both counts; Profile SQL is parked and its 727-line adapter remains hand-written (STATE.md, spec 0008).

No implementation, build, test, install, packaging or generated mono-web artifact was produced by this frozen spec. The existing mono-web worktree remains the read-only baseline for this design. Implementation must occur in its writable integration branch only after the prerequisites above are real, then use the named acceptance gates before claiming parity.