# DA-EX-001 — Один запит, одна квитанція / One request, one receipt

## Твердження / Claim

Для валідного звернення з явним UUID v4 `requestId`, поки його запис існує та не змінений стороннім записувачем, повтор із тим самим нормалізованим вмістом повертає початкову квитанцію без додаткового запису. Інший валідний вміст під тим самим ID повертає `409 request_conflict` і не змінює запис.

For a valid inquiry with an explicit UUID v4 `requestId`, while its stored record exists and is not changed by another writer, an identical normalized replay returns the original receipt without another row. Different valid content under that ID returns `409 request_conflict` without changing the record.

## Конкретний артефакт / Concrete artifact

The `artifact/` directory contains byte-identical snapshots of the site's persistence handler, shared field validator, SQL migration and route binding. The verifier imports the snapshot of `handleInquiry`; it does not reimplement that handler. Each byte sequence is identified in `manifest.json` and `report.json`. The website build rejects source drift between these snapshots and the source it is about to publish.

No production data, credentials or user inquiries are included. Fixtures use the reserved `example.invalid` domain. Constructing a Request object does not send a network request.

## Формальні властивості / Formal properties

Let `D` be the database, `k = "RD-" + uppercase(requestId)`, and `N(p)` be the handler's validated, trimmed payload with normalized email/language. Let `R(k,D)` be the stored row, if any, and `receipt(R) = (R.id, R.created_at)`.

**U1 — uniqueness:** for every key `k` in a database enforcing the included schema,

`|{r in D.inquiries : r.id = k}| <= 1`.

**R1 — identical replay:** given a valid request, an available database, an existing unchanged `R(k,D)` and `N(p) = payload(R)`, the response is `200` with `receipt(R)`, and the handler performs no mutation of `R`.

**C1 — explicit conflict:** under the same conditions except `N(p) != payload(R)`, the response is `409 request_conflict`, and `R` is unchanged.

### Mechanism and reasoning

The migration declares `id text PRIMARY KEY NOT NULL`. Assuming SQLite enforces this constraint, a second row with the same non-null key cannot coexist with the first. The only insert in the handler uses `ON CONFLICT(id) DO NOTHING`. Starting from an empty table, successful insertion adds a previously absent key and a conflicting insertion adds no row; both preserve U1. This is a constraint-based argument under stated database assumptions, not a machine-checked proof of the JavaScript runtime.

The handler compares the stored normalized fields and consent. Its replay branch returns the existing ID and creation time only when `matches = 1`; otherwise it returns a conflict. The verification below executes this branch and the insert-race fallback. It supplies bounded execution evidence for R1/C1, not a universal proof over arbitrary HTTP streams, storage failures or distributed schedules.

## Метод / Method

`node verify.mjs` runs the actual handler against actual SQLite through a small adapter that maps D1-style `prepare/bind/first/run` calls to SQLite prepared statements. The adapter executes each SQL statement; it has no canned success responses and no in-memory JavaScript substitute for the database.

1. Five visible steps: first submission; exact replay; normalized replay; conflicting content; missing consent.
2. Every one of the 81 length-four words over `{A,B,C}` in a fresh SQLite database. A/B are distinct valid payloads sharing one ID; C lacks consent. This produces 324 handler executions. Expected status and row preservation are checked after every execution.
3. Sixteen concurrently started promises in one process and one database connection: one insert, fifteen replay receipts, one stored row.
4. A temporary on-disk database is closed cleanly and opened again. Repeating the request must return its original receipt.

Total: 347 actual handler executions. All test assertions and raw observed events are in the verifier and report. Numbers of assertions may differ on rerun because the published manifest is additionally verified before execution. The result is generated by the run, never a manually entered PASS.

## Межі гарантії / Boundaries

- One explicit request key and bounded payload classes. Without `requestId`, the handler creates a new key; this example makes no deduplication claim for that case.
- In-process Node.js and SQLite. The live endpoint and Cloudflare D1 are not called. The D1 compatibility and deployed storage configuration require separate verification.
- Concurrent promises on one connection are not distributed, multi-process or multi-host concurrency tests.
- A clean close/reopen is not a crash, power failure or disaster recovery test.
- A persisted receipt establishes neither message delivery, human review, an accepted collaboration nor a physical action.
- This evidence concerns the supplied source files and schema, not the user's research programmes or the entire website.
- The verifier was authored and executed during development of this example. It is not an independent third-party audit. The SQLite engine, Node.js runtime, operating system and SHA-256 implementation remain part of the trust assumptions.
- SHA-256 binds the checked bytes to a manifest. A manifest served by the same website is not an independent signature or external authenticity anchor.

## Primary references

- SQLite CREATE TABLE / PRIMARY KEY: https://www.sqlite.org/lang_createtable.html
- Node.js SQLite: https://nodejs.org/docs/latest-v24.x/api/sqlite.html

The code and actual report are the primary evidence for this particular example; documentation explains the underlying database mechanism.