[namedgraph]

Stacked on #499: it's based on formal/http-status, and GitHub retargets it as the stack merges. It is the follow-up to step 4 of the formal roadmap (formal/README.md).

Entity tags (formal/http/LdhHttp/ETag.lean)

• The tag: a function of the document and its graph (ETags). It is the same for the same set of triples, since toSortedNTriples sorts them. The model's one assumption is that different graphs get different tags, i.e. that the 128 bits of SHA-256 EntityTags.entityTag keeps are collision-free on the graphs that occur.
• Cond.resolve: reads If-Match against the stored graph, as evaluatePreconditions does.
• no_lost_update: a write guarded by If-Match with the tag of the graph a client read changes the store only if the document still holds that graph.
• concurrent_write_changes_nothing: once another write has changed that graph, the client's write changes nothing.

Memento (formal/http/LdhHttp/Memento.lean)

• TimeGate: selectMemento transcribed. The server picks the commit closest in time, the more recent of two equally close, and the most recent when no datetime is given. RFC 7089 leaves the choice to the server. Proven: the Memento is one of the document's commits (select_mem, select_none_iff), the newest with no datetime (select_latest), and none is closer while every more recent commit is further away (select_closest).
• TimeMap: toTimeMap transcribed. Each Memento is a prov:wasRevisionOf of exactly the one before it in the history (mem_revisions).
• Commit queue: VersioningFilter, commitAsync and reconcile. Whenever no reconcile is queued, the newest version is the document's graph (drained_is_current). Versions are snapshots taken when a reconcile runs, not one per write.
• Version file: path transcribed. It has a collision: versionFile_root_collides. The root document and a top-level document named root/ both map to graphs/root.nt, which I confirmed by calling the real GraphVersioningService.path. On a versioned dataspace they share one file, TimeMap and TimeGate. versionFile_inj proves this is the only collision. The Java is unchanged: a fix would rename the root document's file, and existing repositories' root.nt histories would need migrating.

Checked in CI

• Golden file: ldh-http --select-cases prints 500 generated histories and datetimes, 64 of them with a tie, together with the model's choice for each. They are committed as src/test/resources/.../memento-cases.tsv.
  • GraphVersioningServiceTest.testSelectMementoAgreesWithTheModel checks the Java against every case.
  • The Formal workflow regenerates the file and fails if it differs from the model.
• HTTP replay: tests/http/versioning/memento-conformance.sh writes a document four times on a versioned dataspace and reads its history from GitHub. It then checks the TimeMap's members and revision links, and the TimeGate at no datetime, at each commit, midway between two, and outside the history, against ldh-http --select. http-tests now also builds ldh-http.
• Drift check: formal/http/tracks-code.sh now also watches EntityTags, GraphVersioningService, VersioningFilter and GitHubClient.

Testing

• lake build of both packages: no sorry; the axioms are propext, Quot.sound and Classical.choice
• tracks-code.sh for both packages
• GraphVersioningServiceTest: 15 tests pass, including the 500 golden cases. Corrupting one expected index makes the new test fail on that case.
• The golden file is byte-identical to a fresh ldh-http --select-cases
• memento-conformance.sh, not yet run. It needs the versioning test repo, so it skips locally and runs in CI where VERSIONING_TEST_TOKEN is set.

🤖 Generated with Claude Code