From 97f956bcd1f2aaffca20666745f4be558935017d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martynas=20Jusevi=C4=8Dius?= Date: Mon, 26 Oct 2026 23:52:47 +0100 Subject: [PATCH 1/2] Model entity tags and Memento in the graph store model ETag.lean takes the entity tag as a function of the document and its graph, collision-free by assumption, resolves If-Match against the stored graph as evaluatePreconditions does, and proves that a write guarded by the tag of the graph a client read changes the store only if the document still holds that graph. Memento.lean transcribes the TimeGate (the closest commit, the more recent of two as close, the most recent with no datetime), the TimeMap (the history, each Memento a revision of the next one down it), the commit queue (once drained, the newest version is the document's graph) and the version file, where the root document and a top-level document named root collide. The TimeGate is replayed against the Java on 500 cases ldh-http --select-cases generates, which GraphVersioningServiceTest checks and the Formal workflow regenerates, and against the server by tests/http/versioning/memento-conformance.sh on a versioned dataspace. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/formal.yml | 5 + .github/workflows/http-tests.yml | 7 +- formal/README.md | 8 +- formal/http/LdhHttp.lean | 2 + formal/http/LdhHttp/ETag.lean | 94 ++++ formal/http/LdhHttp/Memento.lean | 244 +++++++++ formal/http/Main.lean | 80 ++- formal/http/README.md | 69 ++- formal/http/tracks-code.sh | 4 + .../util/GraphVersioningServiceTest.java | 32 ++ .../server/util/memento-cases.tsv | 500 ++++++++++++++++++ tests/http/versioning/memento-conformance.sh | 121 +++++ 12 files changed, 1152 insertions(+), 14 deletions(-) create mode 100644 formal/http/LdhHttp/ETag.lean create mode 100644 formal/http/LdhHttp/Memento.lean create mode 100644 src/test/resources/com/atomgraph/linkeddatahub/server/util/memento-cases.tsv create mode 100755 tests/http/versioning/memento-conformance.sh diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml index bc88bb474..ab9cf89c8 100644 --- a/.github/workflows/formal.yml +++ b/.github/workflows/formal.yml @@ -25,6 +25,11 @@ jobs: - name: Build the ACL model working-directory: formal/acl run: lake build + # GraphVersioningServiceTest replays these cases against the Java TimeGate; here they are checked against the model + - name: The TimeGate cases are the model's + run: | + formal/http/.lake/build/bin/ldh-http --select-cases > /tmp/memento-cases.tsv + diff -u src/test/resources/com/atomgraph/linkeddatahub/server/util/memento-cases.tsv /tmp/memento-cases.tsv # lake build only warns on sorry; the READMEs' "no sorry" claim is checked here - name: Every theorem is proven run: | diff --git a/.github/workflows/http-tests.yml b/.github/workflows/http-tests.yml index f61a9fcdf..3169b3b73 100644 --- a/.github/workflows/http-tests.yml +++ b/.github/workflows/http-tests.yml @@ -51,7 +51,8 @@ jobs: working-directory: cli - name: Add the ldh launcher to PATH run: echo "$GITHUB_WORKSPACE/cli/bin" >> "$GITHUB_PATH" - # the formal suite replays the Lean models (formal/acl over formal/http) against the server through ldh-acl; + # the formal suite replays the Lean models (formal/acl over formal/http) against the server through ldh-acl, + # and the versioning suite the Memento model through ldh-http; # elan picks the toolchain pinned in formal/acl/lean-toolchain - name: Install elan run: | @@ -60,6 +61,10 @@ jobs: - name: Build ldh-acl run: lake build ldh-acl working-directory: formal/acl + # the versioning suite replays the Memento model's TimeGate and TimeMap through ldh-http + - name: Build ldh-http + run: lake build ldh-http + working-directory: formal/http - name: Generating server certificate run: | server-cert-gen.sh .env nginx ssl diff --git a/formal/README.md b/formal/README.md index ff6e0e695..4687db24c 100644 --- a/formal/README.md +++ b/formal/README.md @@ -57,9 +57,11 @@ credibility; the fifth is the one that answers the agent-era question and change every invariant a `Write` does. `acl/LdhAcl/Gate.lean` puts the decision in front of it and proves that `403` is the decision's alone (a denied agent learns nothing else, not even whether the document exists) and that what goes through is an authorized `Write`. The replay checks the server's status and - the document's graph after each request against it. Next on the graph store model: entity tags, to - prove that a write guarded by `If-Match` changes only the version it quoted, and Memento's TimeGate and - TimeMap. + the document's graph after each request against it. `ETag.lean` proves that a write guarded by + `If-Match` loses no update, on the assumption that the tag's digest is collision-free. `Memento.lean` + models the TimeGate (the closest commit, the more recent of two as close), the TimeMap and the commit + queue, and the TimeGate is replayed against the Java on generated histories and against the server on a + versioned dataspace. 5. **Delegation as non-interference.** Model `On-Behalf-Of` and `acl:delegates`, and prove that for any plan an LLM emits, the requests the secretary can execute on behalf of a caller are exactly those diff --git a/formal/http/LdhHttp.lean b/formal/http/LdhHttp.lean index ec713d978..01eb6ba3c 100644 --- a/formal/http/LdhHttp.lean +++ b/formal/http/LdhHttp.lean @@ -2,4 +2,6 @@ import LdhHttp.Base import LdhHttp.Write import LdhHttp.Fin import LdhHttp.Answer +import LdhHttp.ETag +import LdhHttp.Memento import LdhHttp.IO diff --git a/formal/http/LdhHttp/ETag.lean b/formal/http/LdhHttp/ETag.lean new file mode 100644 index 000000000..e5c34b676 --- /dev/null +++ b/formal/http/LdhHttp/ETag.lean @@ -0,0 +1,94 @@ +/- +Entity tags, and what a write guarded by one guarantees. + +`EntityTags.entityTag` digests the document's URI and its graph as sorted N-Triples with SHA-256, keeps 128 bits, +and folds in the negotiated variant. The model takes one variant, as the replay negotiates N-Triples throughout, and +the tag as a function of the document and its graph with two properties: it is the graph's, so the order and +repetition of triples do not count (`ETags.set`, the sorting), and different graphs have different tags +(`ETags.sound`). The second is the one assumption: that the digest is collision-free on the graphs that occur. + +`answerB` takes the precondition as `current` or `stale`; `Cond.resolve` computes which, as `evaluatePreconditions` +does, from the tag the request quotes and the graph the store has. Every write reads the graph, changes it in memory +and writes the whole of it back, so a write the precondition does not guard can overwrite another's work; one it +does guard cannot (`no_lost_update`). +-/ +import LdhHttp.Answer + +namespace LdhHttp + +/-- An entity tag function. -/ +structure ETags (Tag : Type) where + tag : Node → List Triple → Tag + /-- The tag is of the graph, a set of triples: `toSortedNTriples` sorts the lines. -/ + set : ∀ x ts ts', (∀ t, t ∈ ts ↔ t ∈ ts') → tag x ts = tag x ts' + /-- Collision-freeness: one tag of a document, one graph. -/ + sound : ∀ x ts ts', tag x ts = tag x ts' → ∀ t, t ∈ ts ↔ t ∈ ts' + +/-- The conditional headers of a write. -/ +inductive Cond (Tag : Type) where + /-- Neither `If-Match` nor `If-None-Match`. -/ + | none + /-- `If-Match` with an entity tag. -/ + | ifMatch (t : Tag) + /-- `If-None-Match: *`. -/ + | ifNoneMatchAny + +/-- `evaluatePreconditions`: `If-Match` holds when it quotes the tag of the graph the store has. -/ +def Cond.resolve {Tag : Type} [DecidableEq Tag] (E : ETags Tag) (fs : FinStore) (x : Node) : Cond Tag → Precond + | .none => .none + | .ifNoneMatchAny => .absent + | .ifMatch t => if hasDoc fs x = true ∧ E.tag x (graphOf fs x) = t then .current else .stale + +/-- A request whose `If-Match` quotes a tag the document does not have changes nothing. -/ +theorem stale_changes_nothing {hs : HSite} {fs : FinStore} {agent : Option Node} {req : HReq} {s : Success} + {fs' : FinStore} (hd : answerB hs fs agent .stale req = .ok (s, fs')) : fs' = fs := by + cases req with + | get x | head x => + simp only [answerB, readB] at hd; split at hd + · cases hd; rfl + · cases hd + | post x payload => + simp only [answerB, postB, precondFails] at hd + repeat' (first | (cases hd; rfl) | split at hd | cases hd) + | put x payload => + simp only [answerB, putB, precondFails] at hd + repeat' (first | split at hd | cases hd) + all_goals simp_all + | patch x del ins => + simp only [answerB, patchB, precondFails] at hd + repeat' (first | split at hd | cases hd) + | delete x => + simp only [answerB, deleteB, precondFails] at hd + split at hd; · cases hd + split at hd + · cases hd + · rename_i hx + simp only [deleteChecked] at hd + split at hd; · cases hd + split at hd + · cases hd + · simp_all + +/-- **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: whatever another write did in between, this one is not made over it. -/ +theorem no_lost_update {Tag : Type} [DecidableEq Tag] (E : ETags Tag) {hs : HSite} {fs : FinStore} + {agent : Option Node} {req : HReq} {s : Success} {fs' : FinStore} {g₀ : List Triple} + (hd : answerB hs fs agent ((Cond.ifMatch (E.tag req.target g₀)).resolve E fs req.target) req = .ok (s, fs')) + (hw : fs' ≠ fs) : + hasDoc fs req.target = true ∧ ∀ t, t ∈ graphOf fs req.target ↔ t ∈ g₀ := by + simp only [Cond.resolve] at hd + split at hd + · rename_i hc + exact ⟨hc.1, E.sound _ _ _ hc.2⟩ + · exact absurd (stale_changes_nothing hd) hw + +/-- **A write over another's is refused.** Two clients read the same graph; once one of them has changed it, the +other's write, quoting the tag it read, changes nothing. -/ +theorem concurrent_write_changes_nothing {Tag : Type} [DecidableEq Tag] (E : ETags Tag) {hs : HSite} + {fs : FinStore} {agent : Option Node} {req : HReq} {s : Success} {fs' : FinStore} {g₀ : List Triple} + (hchanged : ¬ (hasDoc fs req.target = true ∧ ∀ t, t ∈ graphOf fs req.target ↔ t ∈ g₀)) + (hd : answerB hs fs agent ((Cond.ifMatch (E.tag req.target g₀)).resolve E fs req.target) req = .ok (s, fs')) : + fs' = fs := + Classical.byContradiction fun hw => hchanged (no_lost_update E hd hw) + +end LdhHttp diff --git a/formal/http/LdhHttp/Memento.lean b/formal/http/LdhHttp/Memento.lean new file mode 100644 index 000000000..2ddd99659 --- /dev/null +++ b/formal/http/LdhHttp/Memento.lean @@ -0,0 +1,244 @@ +/- +Memento (RFC 7089): a document's versions, as `GraphVersioningService` keeps and serves them. + +A versioned dataspace commits every document's graph to a Git repository, one file per document. Its history is the +list of commits that touched the file, most recent first, as GitHub lists them (`GitHubClient.listCommits`). The +TimeGate selects one of them for a datetime, the TimeMap lists them all, and a write schedules the commit that +records it. Four things are modelled: + +* **the TimeGate's choice** (`selectMemento`): RFC 7089 leaves it to the server and asks only that it be consistent. + This one takes the commit closest in time, the more recent of two as close, and the most recent with no datetime; +* **the TimeMap** (`toTimeMap`): its members are the history, and each is `prov:wasRevisionOf` the one before it; +* **the commit queue** (`commitAsync`, `reconcile`): every write that succeeds queues a reconcile, the reconciles of a + branch run one at a time, and each records the graph the store has when it runs. Versions are snapshots taken when a + reconcile runs, not one per write: two writes close together can leave one version. Once the queue is drained, the + newest version is the document's graph (`drained_is_current`); +* **the file a document is versioned in** (`path`): the root document's is `root`, which a document named `root` at + the top of the tree shares (`versionFile_root_collides`). +-/ +import LdhHttp.Base + +namespace LdhHttp + +/-! ## The TimeGate -/ + +/-- A commit of a document's file: its SHA and its author datetime, in seconds. -/ +structure Commit where + sha : Nat + time : Int + deriving DecidableEq, Repr + +/-- `Duration.between(commit.datetime(), datetime).abs()`. -/ +def Commit.dist (d : Int) (c : Commit) : Nat := (c.time - d).natAbs + +/-- `stream().min(comparator)`: the first of the closest, as `BinaryOperator.minBy` keeps the earlier of two equal. -/ +def closer (d : Int) (best c : Commit) : Commit := if c.dist d < best.dist d then c else best + +/-- `selectMemento`, over a history most recent first. -/ +def selectMemento : List Commit → Option Int → Option Commit + | [], _ => none + | c :: _, none => some c + | c :: cs, some d => some (cs.foldl (closer d) c) + +theorem foldl_closer (d : Int) : ∀ (cs : List Commit) (b r : Commit), cs.foldl (closer d) b = r → + (r = b ∨ r ∈ cs) ∧ r.dist d ≤ b.dist d ∧ (∀ c ∈ cs, r.dist d ≤ c.dist d) ∧ + ∃ pre post, b :: cs = pre ++ r :: post ∧ ∀ c ∈ pre, r.dist d < c.dist d + | [], b, r, hr => by + simp only [List.foldl_nil] at hr; subst hr + exact ⟨Or.inl rfl, Nat.le_refl _, by simp, [], [], rfl, by simp⟩ + | c :: cs, b, r, hr => by + simp only [List.foldl_cons] at hr + obtain ⟨hm, hb, hall, pre, post, hsplit, hpre⟩ := foldl_closer d cs (closer d b c) r hr + by_cases hc : c.dist d < b.dist d + · simp only [closer, hc, if_true] at hm hb hall hsplit hpre + refine ⟨?_, by omega, ?_, b :: pre, post, by rw [List.cons_append, ← hsplit], ?_⟩ + · rcases hm with h | h + · rw [h]; exact Or.inr (List.mem_cons_self _ _) + · exact Or.inr (List.mem_cons_of_mem _ h) + · intro c' hc' + rcases List.mem_cons.1 hc' with rfl | h + · exact hb + · exact hall c' h + · intro c' hc' + rcases List.mem_cons.1 hc' with rfl | h + · omega + · exact hpre c' h + · simp only [closer, hc, if_false] at hm hb hall hsplit hpre + refine ⟨?_, hb, ?_, ?_⟩ + · rcases hm with h | h + · exact Or.inl h + · exact Or.inr (List.mem_cons_of_mem _ h) + · intro c' hc' + rcases List.mem_cons.1 hc' with rfl | h + · omega + · exact hall c' h + · cases pre with + | nil => + simp only [List.nil_append, List.cons.injEq] at hsplit + obtain ⟨hrb, rfl⟩ := hsplit + exact ⟨[], c :: cs, by rw [← hrb]; rfl, by simp⟩ + | cons p pre => + simp only [List.cons_append, List.cons.injEq] at hsplit + obtain ⟨hpb, hcs⟩ := hsplit + have hrb := hpre p (List.mem_cons_self _ _) + rw [← hpb] at hrb + refine ⟨b :: c :: pre, post, by rw [hcs]; rfl, ?_⟩ + intro c' hc' + rcases List.mem_cons.1 hc' with rfl | h + · exact hrb + rcases List.mem_cons.1 h with rfl | h + · omega + · exact hpre c' (List.mem_cons_of_mem _ h) + +/-- A history has a Memento for every datetime, and only a history: an empty one is `404`. -/ +theorem select_none_iff {cs : List Commit} {dt : Option Int} : selectMemento cs dt = none ↔ cs = [] := by + cases cs with + | nil => simp [selectMemento] + | cons c cs => cases dt <;> simp [selectMemento] + +/-- **The Memento is one of the document's.** -/ +theorem select_mem {cs : List Commit} {dt : Option Int} {m : Commit} (h : selectMemento cs dt = some m) : + m ∈ cs := by + cases cs with + | nil => simp [selectMemento] at h + | cons c cs => + cases dt with + | none => simp [selectMemento] at h; exact h ▸ List.mem_cons_self _ _ + | some d => + simp only [selectMemento, Option.some.injEq] at h + rcases (foldl_closer d cs c m h).1 with h | h + · rw [h]; exact List.mem_cons_self _ _ + · exact List.mem_cons_of_mem _ h + +/-- **With no datetime, the most recent.** -/ +theorem select_latest {c : Commit} {cs : List Commit} : selectMemento (c :: cs) none = some c := rfl + +/-- **The closest, and of the closest the most recent.** No commit of the history is closer to the datetime, and +every commit more recent than the Memento is further from it. -/ +theorem select_closest {cs : List Commit} {d : Int} {m : Commit} (h : selectMemento cs (some d) = some m) : + (∀ c ∈ cs, m.dist d ≤ c.dist d) ∧ ∃ pre post, cs = pre ++ m :: post ∧ ∀ c ∈ pre, m.dist d < c.dist d := by + cases cs with + | nil => simp [selectMemento] at h + | cons c cs => + simp only [selectMemento, Option.some.injEq] at h + obtain ⟨_, hb, hall, rest⟩ := foldl_closer d cs c m h + refine ⟨fun c' hc' => ?_, rest⟩ + rcases List.mem_cons.1 hc' with rfl | h + · exact hb + · exact hall c' h + +/-! ## The TimeMap -/ + +/-- `toTimeMap`'s `prov:hadMember`: a Memento for every commit of the history. -/ +def members (cs : List Commit) : List Nat := cs.map (·.sha) + +/-- `toTimeMap`'s `prov:wasRevisionOf`: each Memento is a revision of the next one down the history. -/ +def revisions : List Commit → List (Commit × Commit) + | c :: c' :: cs => (c, c') :: revisions (c' :: cs) + | _ => [] + +theorem mem_members {cs : List Commit} {sha : Nat} : sha ∈ members cs ↔ ∃ c ∈ cs, c.sha = sha := by + simp [members] + +/-- **Each Memento is a revision of the one before it in the history, and of nothing else.** -/ +theorem mem_revisions : ∀ {cs : List Commit} {a b : Commit}, + (a, b) ∈ revisions cs ↔ ∃ pre post, cs = pre ++ a :: b :: post + | [], a, b => by simp [revisions] + | [c], a, b => by + simp only [revisions, List.not_mem_nil, false_iff, not_exists] + intro pre post h + cases pre with + | nil => simp at h + | cons p pre => cases pre <;> simp at h + | c :: c' :: cs, a, b => by + simp only [revisions, List.mem_cons, Prod.mk.injEq] + rw [mem_revisions] + constructor + · rintro (⟨rfl, rfl⟩ | ⟨pre, post, h⟩) + · exact ⟨[], cs, rfl⟩ + · exact ⟨c :: pre, post, by rw [h]; rfl⟩ + · rintro ⟨pre, post, h⟩ + cases pre with + | nil => + simp only [List.nil_append, List.cons.injEq] at h + exact Or.inl ⟨h.1.symm, h.2.1.symm⟩ + | cons p pre => + simp only [List.cons_append, List.cons.injEq] at h + exact Or.inr ⟨pre, post, h.2⟩ + +/-! ## The commit queue -/ + +/-- One document's versioning: the graph the store has, the reconciles queued for it, and the graph its newest +version holds, `none` for no graph. -/ +structure Versioning (G : Type) where + store : Option G + queued : Nat + newest : Option G + /-- A write has been made since versioning began: the file of a document that predates it is not yet its own. -/ + written : Bool + +inductive VEvent (G : Type) where + /-- A write that succeeds, leaving the graph `g` (`none` after a `DELETE`); `VersioningFilter` queues a reconcile. -/ + | write (g : Option G) + /-- The next reconcile of the branch's chain runs: it commits the graph the store has, or deletes the file. -/ + | reconcile + +def Versioning.step {G : Type} (v : Versioning G) : VEvent G → Option (Versioning G) + | .write g => some { v with store := g, queued := v.queued + 1, written := true } + | .reconcile => if v.queued = 0 then none else some { v with queued := v.queued - 1, newest := v.store } + +/-- Once nothing is queued, the newest version of a document written since versioning began is its graph. -/ +def Versioning.Drained {G : Type} (v : Versioning G) : Prop := v.written = true → v.queued = 0 → v.newest = v.store + +/-- Every event leaves the versioning drained-current: a write queues a reconcile, and a reconcile records the +store's graph. -/ +theorem Versioning.step_drained {G : Type} {v v' : Versioning G} {e : VEvent G} + (hs : v.step e = some v') : v'.Drained := by + cases e with + | write g => + simp only [Versioning.step, Option.some.injEq] at hs; subst hs + intro _ hq; simp at hq + | reconcile => + simp only [Versioning.step] at hs + split at hs + · cases hs + · simp only [Option.some.injEq] at hs; subst hs + intro _ _; rfl + +/-- The events a document's versioning goes through. -/ +inductive Versioning.Reach {G : Type} : Versioning G → Versioning G → Prop where + | refl (v) : Reach v v + | step {v v' v''} (e : VEvent G) : v.step e = some v' → Reach v' v'' → Reach v v'' + +/-- **A drained queue is current.** From the state versioning begins in, whatever writes and reconciles follow, +whenever no reconcile is queued the newest version is the document's graph. -/ +theorem drained_is_current {G : Type} {store newest : Option G} {v : Versioning G} + (h : Versioning.Reach ⟨store, 0, newest, false⟩ v) : v.Drained := by + have : ∀ {a b : Versioning G}, Versioning.Reach a b → a.Drained → b.Drained := by + intro a b hr + induction hr with + | refl => exact id + | step e hs _ ih => exact fun _ => ih (Versioning.step_drained hs) + exact this h (by intro hw; simp at hw) + +/-! ## The version file -/ + +/-- `GraphVersioningService.path`, on the document's path below the base as segments, without the trailing slash: +the root document, which has none, is versioned as `root`. -/ +def versionFile (segments : List String) : List String := if segments = [] then ["root"] else segments + +/-- **The root document shares its file with a document named `root`.** `https://example.org/` and +`https://example.org/root/` are versioned in the same `root.nt`, so their histories, TimeMaps and TimeGates are one. -/ +theorem versionFile_root_collides : versionFile [] = versionFile ["root"] := rfl + +/-- That is the only collision: two other documents never share a file. -/ +theorem versionFile_inj {a b : List String} (ha : a ≠ ["root"]) (hb : b ≠ ["root"]) + (h : versionFile a = versionFile b) : a = b := by + unfold versionFile at h + by_cases ha' : a = [] <;> by_cases hb' : b = [] <;> simp only [ha', hb', if_true, if_false] at h + · rw [ha', hb'] + · exact absurd h.symm hb + · exact absurd h ha + · exact h + +end LdhHttp diff --git a/formal/http/Main.lean b/formal/http/Main.lean index 4fbdbcc62..2af81136f 100644 --- a/formal/http/Main.lean +++ b/formal/http/Main.lean @@ -4,6 +4,8 @@ front of it: what the graph store does with a request it is asked to answer. ldh-http --dataset END_USER.nq [--dataset ADMIN.nq]... --request REQUEST.tsv [--payload PAYLOAD.nt | --delete DELETE.nt --insert INSERT.nt] [--fixed URI]... + ldh-http --select HISTORY.tsv [--datetime SECONDS] + ldh-http --select-cases The datasets are N-Quads dumps of the stores. A request is one line, `AGENTMETHODDOCUMENTPRECONDITION`, with `AGENT` a WebID or `-` (it owns a document it creates), `METHOD` one of `GET`, `HEAD`, `POST`, `PUT`, `PATCH` @@ -12,6 +14,13 @@ and `DELETE`, and `PRECONDITION` one of `none`, `current` (`If-Match` with the c N-Triples; a `PATCH` is `DELETE { --delete } INSERT { --insert } WHERE {}`. `--fixed` names the owner's and the secretary's WebID documents. The status comes back on the first line, then the document's graph after the request, as N-Triples. + +`--select` is the TimeGate's choice (`selectMemento`) for a history, one `SHASECONDS` line per commit, most +recent first, and an `Accept-Datetime` in seconds since the epoch, or none: the selected SHA, or `none` for an empty +history. `--select-cases` prints a fixed set of generated histories and datetimes with the choice for each, one +`SECONDS,...DATETIMEINDEX` line per case (`-` for no datetime, or no Memento): the `memento-cases.tsv` of +`GraphVersioningServiceTest`'s resources, which the `Formal` workflow regenerates and the test replays against the +Java. -/ import LdhHttp @@ -20,10 +29,18 @@ open LdhHttp structure Args where datasets : List String := [] request : Option RequestFiles := none + select : Option String := none + datetime : Option Int := none + selectCases : Bool := false partial def parseArgs : List String → Args → Except String Args | [], a => .ok a | "--dataset" :: v :: rest, a => parseArgs rest { a with datasets := a.datasets ++ [v] } + | "--select" :: v :: rest, a => parseArgs rest { a with select := some v } + | "--datetime" :: v :: rest, a => match v.toInt? with + | some d => parseArgs rest { a with datetime := some d } + | none => .error s!"cannot read datetime: {v}" + | "--select-cases" :: rest, a => parseArgs rest { a with selectCases := true } | "--request" :: v :: rest, a => parseArgs rest { a with request := some { (a.request.getD { request := v }) with request := v } } | args@(arg :: _), a => match parseRequestArg args (a.request.getD { request := "" }) with @@ -32,12 +49,73 @@ partial def parseArgs : List String → Args → Except String Args def usage : String := "usage: ldh-http --dataset DATASET.nq... --request REQUEST.tsv " ++ - "[--payload PAYLOAD.nt | --delete DELETE.nt --insert INSERT.nt] [--fixed URI]..." + "[--payload PAYLOAD.nt | --delete DELETE.nt --insert INSERT.nt] [--fixed URI]...\n" ++ + " ldh-http --select HISTORY.tsv [--datetime SECONDS]\n" ++ + " ldh-http --select-cases" + +/-! ## The TimeGate -/ + +/-- A linear congruential generator: the cases are the same on every run and every machine. -/ +def lcg (x : Nat) : Nat := (1664525 * x + 1013904223) % 4294967296 + +/-- `n` cases from `seed`: histories of up to six commits, most recent first, a few seconds apart and some at the +same second, so that the datetimes fall between, on and beside them, and two commits are often as close. -/ +def selectCases (n seed : Nat) : List (List Int × Option Int) := Id.run do + let mut x := seed + let mut out := #[] + for _ in [0:n] do + x := lcg x + let len := (x / 65536) % 7 + x := lcg x + let mut t : Int := ((x / 65536) % 100 : Nat) + let mut times := #[] + for _ in [0:len] do + times := times.push t + x := lcg x + t := t - (((x / 65536) % 6 : Nat) : Int) + x := lcg x + let dt : Option Int := if (x / 65536) % 6 = 0 then none else + let lo := (times.toList.getLastD 0) - 10 + let hi := (times.toList.headD 0) + 10 + some (lo + (((x / 256) % (hi - lo + 1).toNat : Nat) : Int)) + out := out.push (times.toList, dt) + return out.toList + +def runSelectCases : IO UInt32 := do + for (times, dt) in selectCases 500 20261027 do + let history := times.enum.map fun (i, t) => ({ sha := i, time := t } : Commit) + let chosen := match selectMemento history dt with + | some c => toString c.sha + | none => "-" + let dts := match dt with + | some d => toString d + | none => "-" + IO.println s!"{",".intercalate (times.map toString)}\t{dts}\t{chosen}" + return 0 + +def runSelect (path : String) (dt : Option Int) : IO UInt32 := do + let lines := (← IO.FS.lines path).toList.filter (!·.trim.isEmpty) + let mut shas := #[] + let mut history := #[] + for line in lines do + match line.splitOn "\t" with + | [sha, t] => match t.trim.toInt? with + | some time => + history := history.push ({ sha := shas.size, time := time } : Commit) + shas := shas.push sha + | none => IO.eprintln s!"cannot read time: {line}"; return 2 + | _ => IO.eprintln s!"cannot read commit: {line}"; return 2 + match selectMemento history.toList dt with + | some c => IO.println (shas.getD c.sha "") + | none => IO.println "none" + return 0 def main (argv : List String) : IO UInt32 := do let args ← match parseArgs argv {} with | .ok a => pure a | .error e => IO.eprintln e; IO.eprintln usage; return 2 + if args.selectCases then return ← runSelectCases + if let some path := args.select then return ← runSelect path args.datetime let some files := args.request | IO.eprintln usage; return 2 let mut i : Interner := {} diff --git a/formal/http/README.md b/formal/http/README.md index 1688227b2..827703094 100644 --- a/formal/http/README.md +++ b/formal/http/README.md @@ -1,7 +1,8 @@ # LinkedDataHub graph store model in Lean -A Lean 4 model of LinkedDataHub's graph store: the documents it keeps, the writes it makes of a request, and its -answer to every request, with proofs of the invariants those writes keep. Who is asking is no part of it: the +A Lean 4 model of LinkedDataHub's graph store: the documents it keeps, the writes it makes of a request, its answer +to every request, the entity tags that guard its writes and the versions it serves (Memento), with proofs of the +invariants those writes keep. Who is asking is no part of it: the authorization decision comes before all of it, and is the ACL model's ([`../acl/`](../acl/)), which builds on this one. @@ -33,8 +34,10 @@ formal/http/tracks-code.sh origin/develop | `LdhHttp/Write.lean` | The graph store's writes as a relation, and the invariants they keep | | `LdhHttp/Fin.lean` | A store as data, and the abstract store it denotes | | `LdhHttp/Answer.lean` | The graph store's answer as a program: every status and the store after it, and the proof that what goes through is a `Write` | +| `LdhHttp/ETag.lean` | Entity tags, the precondition they resolve to, and the proof that a write guarded by one loses no update | +| `LdhHttp/Memento.lean` | The TimeGate's choice, the TimeMap, the commit queue and the version file | | `LdhHttp/IO.lean` | Reading dumps and a request into the model's terms, and printing an answer | -| `Main.lean` | `ldh-http`: the answer over a live instance's datasets | +| `Main.lean` | `ldh-http`: the answer over a live instance's datasets, and the TimeGate's choice over a history | ## The model @@ -54,6 +57,17 @@ formal/http/tracks-code.sh origin/develop document allows (`405`), the URI (`308`, `400`), the write and type rules (`422`), the preconditions (`428` without one on an existing document, `412` on a stale one or on `If-None-Match: *`), existence (`404`), the parent and the children (`409`), and the rest of `PATCH`'s guards (`422`). +- **Entity tags (`ETag.lean`):** a function of the document and its graph, the same for the same set of triples + (`toSortedNTriples` sorts them) and, the one assumption, different for different graphs: the 128 bits of + SHA-256 `EntityTags.entityTag` keeps being collision-free on the graphs that occur. `If-Match` holds when it quotes + the tag of the graph the store has. The negotiated variant the server folds into a tag is left out: the model takes + one, as the replay negotiates N-Triples throughout. +- **Memento (`Memento.lean`):** a document's history is the commits that touched its file, most recent first, as + `GitHubClient.listCommits` lists them. The TimeGate selects the commit closest in time to `Accept-Datetime`, the + more recent of two as close, and the most recent with none. The TimeMap lists the history, each Memento a + `prov:wasRevisionOf` the next one down. Every write that succeeds queues a reconcile (`VersioningFilter`), a + branch's reconciles run one at a time, and each commits the graph the store has when it runs: a version is a + snapshot then, not one per write. ## Mapping to the code @@ -72,9 +86,17 @@ formal/http/tracks-code.sh origin/develop | `HSite.fixed`, `HSite.isRoot` | `allowedMethods`: no `PUT` or `DELETE` of the owner's or the secretary's WebID document, no `DELETE` of the root | | `untypesB` | `patch`'s `rdf:type cannot be removed` | | `parentIri`, `doubleSlash`, `slashed` (`IO.lean`) | `IRIx.resolve("..")`; `put`'s redirect to a trailing slash and refusal of a double slash | - -`DocumentHierarchyGraphStoreImpl` lives in `src/main/java/com/atomgraph/linkeddatahub/server/model/impl/`. Core's -`GraphStoreBase` is a dependency, outside what `tracks-code.sh` can watch. +| `ETags` | `EntityTags.entityTag`, over `toSortedNTriples` (`server/util/`) | +| `Cond.resolve` | `evaluatePreconditions`' reading of `If-Match` and `If-None-Match: *` | +| `Commit`, the history | `GitHubClient.CommitInfo` and `listCommits` (`client/`): the file's commits, most recent first | +| `selectMemento`, `closer` | `GraphVersioningService.selectMemento`: `stream().min()` over the absolute distance | +| `members`, `revisions` | `GraphVersioningService.toTimeMap`'s `prov:hadMember` and `prov:wasRevisionOf` | +| `Versioning.step` | `VersioningFilter` (`server/filter/response/`), which queues a reconcile after a write that succeeds, and `commitAsync` and `reconcile`, which run a branch's one at a time | +| `versionFile` | `GraphVersioningService.path` | + +`DocumentHierarchyGraphStoreImpl` lives in `server/model/impl/`, all of them under +`src/main/java/com/atomgraph/linkeddatahub/`. Core's `GraphStoreBase` is a dependency, outside what `tracks-code.sh` +can watch. ## Results @@ -91,10 +113,18 @@ Proven with no `sorry`, using only the axioms `propext`, `Quot.sound` and, throu | `answer_not_forbidden` | No check of the graph store answers `403`: that status is the authorization decision's | | `answer_write` | A request that goes through is a `Write` of it from the store before to the store after, or changes nothing | | `answer_inv` | So the graph store keeps `Inv` and `Typed`, as every `Write` 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 the graph a client read, the client's write quoting its tag changes nothing | +| `select_mem`, `select_none_iff` | The TimeGate's Memento is one of the document's; there is one exactly when the history is not empty | +| `select_latest` | With no datetime, the most recent | +| `select_closest` | No commit is closer to the datetime, and every more recent one is further from it | +| `mem_revisions` | Each Memento is a revision of the one before it in the history, and of nothing else | +| `drained_is_current` | Whatever writes and reconciles follow, whenever none is queued the newest version is the document's graph | +| `versionFile_root_collides`, `versionFile_inj` | The root document and a top-level document named `root` share a version file; no two other documents do | The invariants are hypotheses the ACL model's theorems take; it proves them of its authorized writes through these. -## Replaying the answer +## Replaying the model `ldh-http` runs the answer on N-Quads dumps of the stores: @@ -108,7 +138,24 @@ A request is `AGENTMETHODDOCUMENTPRECONDITION`, with the precondi is `--payload`, and a `PATCH` is `DELETE { --delete } INSERT { --insert } WHERE {}`. The answer is the status, then the document's graph after the request. It is what the graph store does with a request it is asked to answer; the server's own answer puts the authorization decision first, which is `ldh-acl --request` in the ACL model, and what -`tests/http/formal/acl-conformance.sh` replays. +`tests/http/formal/acl-conformance.sh` replays. That replay sends the current entity tag, a stale one, none and +`If-None-Match: *`, and states which it sent: the model's tags are abstract, so the replay resolves them, which it +can, having read the tag it quotes. + +The TimeGate is replayed twice: + +```bash +.lake/build/bin/ldh-http --select history.tsv --datetime 1761523200 # SHASECONDS per commit, most recent first +.lake/build/bin/ldh-http --select-cases +``` + +- `--select-cases` prints 500 generated histories and datetimes, many with two commits as close, and the model's + choice for each. They are `GraphVersioningServiceTest`'s `memento-cases.tsv`: the test checks the Java's choice + on every case, and the `Formal` workflow regenerates the file and fails when it is not the model's. +- `tests/http/versioning/memento-conformance.sh` writes a document four times on a versioned dataspace, reads its + history from GitHub, and checks the server's TimeMap against it and its TimeGate against `--select`: with no + datetime, at each commit, midway between two, and outside the history. It runs where the versioning suite does, on + a dataspace with a test repository. ## Not modelled @@ -120,4 +167,8 @@ server's own answer puts the authorization decision first, which is `ldh-acl --r missing title answered with `422`, changes nothing, and the model has no write for it. The answer takes the payload as ground triples free of `dct:created` and `dct:modified`, and the replay sends only such payloads, valid against the ontology's constraints, with a single-operation `PATCH`. -- **Entity tags:** a precondition is `current` or `stale` as the request states it, not computed from the graph. +- **The entity tag's value:** the replay cannot compute the server's tags (Jena's N-Triples, SHA-256, the variant + folding), so it states whether the tag it quotes is current. +- **Versioning's failures and limits:** a reconcile that fails, a write whose response fails after the store has + changed (no reconcile is queued for it), and a history longer than `listCommits` pages through. The history's order + is GitHub's. diff --git a/formal/http/tracks-code.sh b/formal/http/tracks-code.sh index 947bab599..3622a8b56 100755 --- a/formal/http/tracks-code.sh +++ b/formal/http/tracks-code.sh @@ -18,6 +18,10 @@ config=https://w3id.org/atomgraph/linkeddatahub/config# # Sources transcribed whole: any change counts sources=( src/main/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImpl.java + src/main/java/com/atomgraph/linkeddatahub/server/util/EntityTags.java + src/main/java/com/atomgraph/linkeddatahub/server/util/GraphVersioningService.java + src/main/java/com/atomgraph/linkeddatahub/server/filter/response/VersioningFilter.java + src/main/java/com/atomgraph/linkeddatahub/client/GitHubClient.java ) # web.xml is transcribed query by query: only these context params count queries=(childQuery) diff --git a/src/test/java/com/atomgraph/linkeddatahub/server/util/GraphVersioningServiceTest.java b/src/test/java/com/atomgraph/linkeddatahub/server/util/GraphVersioningServiceTest.java index ae5aa69b3..8bcbe8bf5 100644 --- a/src/test/java/com/atomgraph/linkeddatahub/server/util/GraphVersioningServiceTest.java +++ b/src/test/java/com/atomgraph/linkeddatahub/server/util/GraphVersioningServiceTest.java @@ -176,6 +176,38 @@ public void testSelectMementoResolvesTiesTowardsTheMoreRecent() assertEquals("sha-2", GraphVersioningService.selectMemento(commits, Instant.parse("2026-08-17T11:00:00Z")).get().sha()); } + /** + * The TimeGate's choice agrees with the Lean model's (formal/http, selectMemento) on the + * cases ldh-http --select-cases generates: memento-cases.tsv, one line per case, the commit + * times in seconds most recent first, the datetime or -, and the index of the commit selected or + * -. The Formal workflow regenerates the file from the model and fails on a difference. + */ + @Test + public void testSelectMementoAgreesWithTheModel() throws java.io.IOException + { + try (java.io.InputStream is = getClass().getResourceAsStream("memento-cases.tsv")) + { + List lines = new String(is.readAllBytes(), StandardCharsets.UTF_8).lines().filter(line -> !line.isBlank()).toList(); + assertEquals(500, lines.size()); + + for (String line : lines) + { + String[] fields = line.split("\t", -1); + List commits = new java.util.ArrayList<>(); + if (!fields[0].isEmpty()) + { + String[] times = fields[0].split(","); + for (int i = 0; i < times.length; i++) + commits.add(new GitHubClient.CommitInfo(String.valueOf(i), Instant.ofEpochSecond(Long.parseLong(times[i])), "https://localhost/agent#this")); + } + Instant datetime = fields[1].equals("-") ? null : Instant.ofEpochSecond(Long.parseLong(fields[1])); + + Optional selected = GraphVersioningService.selectMemento(commits, datetime); + assertEquals(fields[2], selected.map(GitHubClient.CommitInfo::sha).orElse("-"), line); + } + } + } + @Test public void testSelectMementoWithoutDatetimeIsMostRecent() { diff --git a/src/test/resources/com/atomgraph/linkeddatahub/server/util/memento-cases.tsv b/src/test/resources/com/atomgraph/linkeddatahub/server/util/memento-cases.tsv new file mode 100644 index 000000000..308d09ff8 --- /dev/null +++ b/src/test/resources/com/atomgraph/linkeddatahub/server/util/memento-cases.tsv @@ -0,0 +1,500 @@ +62,60,59,55,54,53 - 0 +67,64,61 64 1 +48,46 54 0 +85 92 0 +50,49,46,44 43 3 +88,87,82,80 89 0 +58,56,55,55 49 2 +56 58 0 +10,6,2,0,-2 6 1 +9,7,4,1 7 1 +41,38,37,33,32 - 0 +19 14 0 +3,1 12 0 +37,37 39 0 +39,36,35,31 47 0 +88,85,81,79 - 0 +91,86,83,79,77 88 1 +61,56,54,50 51 3 +41,40,35,31,31 46 0 +95,94,91,87,82 104 0 +4,4,1 7 0 + - - +49,44 57 0 +47,47,42,42,40,36 46 0 +60,55 - 0 +36,36,35 - 0 +78,77,77,73,70,70 84 0 +72,69 - 0 +57,55,53 63 0 + 3 - +58,58,56,56,55 66 0 + - - +52 54 0 +33,33,29,24 39 0 + -4 - +8,4,0,-5,-8,-8 15 0 + 4 - +79,79,78 85 0 +79,75,73,68,65,62 88 0 +38,34,29,28,28,24 - 0 +13,11,8,7 19 0 +5,1,1,0 -6 3 +23,19,19 - 0 +41,36,35,34,32 40 0 +68,67,67 70 0 +22,17,13,12,8 30 0 +17,12,8 -2 2 +51 46 0 +98,93,91 88 2 +16,14 12 1 +4,3,-1 -7 2 +7,4,3 11 0 + - - +29 37 0 +14,13 5 1 +86,83,82 - 0 +95 94 0 +49 39 0 +17 25 0 +27,27,25,23,22,17 33 0 +66 57 0 +21,19,14 28 0 +77,72 86 0 +97,97,97,95 96 0 +90,89,88,86 96 0 +13,10 18 0 +59,58,58,53,53 62 0 +9,5 - 0 +94,91,89,89,88,88 - 0 + 9 - +24,22,22 20 1 +41 34 0 + 7 - +65,64 55 1 +23,18,18,17 7 3 + -7 - +79,74 66 1 +67 68 0 +51,46,42,37,33 26 4 +21,18,17 25 0 +94,93,88,83,82,81 82 4 +50,47 51 0 +84,81,79,79 77 2 +53,50 43 1 +5,4,0 -6 2 + -2 - +13,9,5,4,3,1 -4 5 +54 56 0 +56 54 0 +14,13 21 0 +3,3,-2,-7,-7,-11 -11 5 +0 -1 0 +68,68,67,66,62,58 - 0 + 2 - +16,14,13,9 - 0 + -1 - +64,64,63 72 0 +61,59,56 58 1 +12,11,11,6 - 0 +44,44,40 41 2 +38 - 0 +15,13,8 15 0 +61,61,60 54 2 +75 84 0 +3,1,0,-5 -7 3 +96,94 105 0 +19,18,18,15,14,13 - 0 +4,0,-1,-5,-5 4 0 +70,68,63,59,59,58 67 1 +88 80 0 +63,62,61,58,58 71 0 +20 21 0 +18,13,12,8 8 3 +13,8 - 0 +59,59,56,52 59 0 +24,24,22,18 16 3 +15,15,12,7 10 2 +11,8 0 1 +22,20,18 9 2 +19 23 0 +99 92 0 +77,72,71,67,67 - 0 +56,53 52 1 +67,64 73 0 +69,65,61,56,51,47 51 4 +61,59 - 0 +30,30 34 0 +27 36 0 +78 72 0 +4,4,4,0 6 0 +18 28 0 +86 76 0 +12,11,7,6,4,2 16 0 +30,25,21,20 32 0 +14,12,11,11 3 2 +74,73,69,65,65 76 0 +27,23,21 19 2 +76,73,72,69 80 0 +99,99,95,91,86,85 95 2 +53,51 - 0 +59,59,56,55,54 51 4 +94,91 99 0 +12,10 5 1 +60,60,60,60,58 48 4 + -10 - +54,54,53,53,50 53 2 +9,9 9 0 +75,74,73 77 0 + 8 - + 8 - +25 18 0 +13,11,7 14 0 +63 60 0 + -4 - + 8 - +74,69,69,69,64,62 57 5 +91,87,87,82 88 1 + -6 - +37,33,29,24,21 23 3 +54,51,48,45,44 59 0 +85,82,80,79 - 0 +21,21,19,14,9 30 0 + 4 - + -2 - +97,95,95 98 0 + - - +52,50 48 1 +45,45,42,41 37 3 +35,30,29,24,20 20 4 +58,55,53,48,44,42 58 0 +47 - 0 + -8 - +42,38 - 0 +99,96,96 - 0 + -5 - +72,70,66,65,65 62 3 + -4 - +29,25 - 0 + 2 - +10,7,6,3,3,-2 10 0 +60,60,56 67 0 +72 71 0 +6 -4 0 +83,82,80,77 71 3 +92,88,83 75 2 + -5 - +82,82 88 0 +39,34,30,28,27 - 0 +13,13,12,9,9,6 23 0 +72,67,66,63 62 3 +26,25,22 - 0 +45,40 54 0 +75,71 67 1 +83,83,82,82 92 0 +98,95,93 98 0 +61,58,54,50,48 - 0 +21,18,13,13,13,10 17 1 +73,73,70,70,70 69 2 +37,35,34 44 0 +1,1,-2,-6,-11,-11 -19 4 +12,11 14 0 +27,24 26 0 +30,28,24,21 38 0 +63,60,56,53,53 60 1 + -6 - +9 4 0 +94 100 0 +39,34,34 39 0 +21,21,17,13,8 - 0 +75,71,68,66,65,62 73 0 +32 34 0 +50,49,46,44,39 - 0 +26 - 0 + -6 - +78,77 76 1 +38,37 39 0 +54 56 0 +73,70,70 67 1 + -5 - +43,42 35 1 +15,14,10,7 9 2 +75,73,71 - 0 +33,32,31,27 - 0 +77,75,75,72,69,66 64 5 +13,8,4 - 0 +2,2 2 0 +29,26,26,26,22,19 20 5 +96,94,89,85 93 1 + 8 - + - - +40 40 0 + 8 - +46,44,42,38,37,33 23 5 +62,60 - 0 +16 - 0 +73,73 72 0 + 2 - +13 7 0 + -10 - +7,3,-1,-2 -12 3 +99,97,97,92,92,88 81 5 +98,94,90 - 0 +97,92,89,85,80,80 89 2 +76,73,70 68 2 +62,62,58 67 0 +14,13,12,11,10 7 4 +47,42,42 - 0 +26,24,19,16,11,6 3 5 +64,61,59 57 2 +9,7,6,2,0 8 0 +4,3,-1,-6 12 0 +11,8 -2 1 +24,23,22 28 0 +63,61,58,56,55,50 62 0 +73,69 - 0 +26,23,18 - 0 +21,17 27 0 + -6 - + -1 - +91,90 99 0 +95,92,88,83,78,75 105 0 +82,80,79,77 72 3 + 6 - +81,79 85 0 +62,58,57,57,57 - 0 +89,85,80,77,75 99 0 +75,70,66,62,61,61 65 2 +5,5,1,-2,-3,-8 -5 4 +69,68 77 0 +75,70,65,65,65 66 2 +46,46,46 37 0 +30,25,20,19 - 0 +65,65,64 65 0 +72,70,68 75 0 +49,47,42,41 39 3 +33,31,26,26,25,21 33 0 +89,86,84,84,82,81 90 0 +49 - 0 + -6 - +41,41,39,36,33,31 - 0 +25,20,18,17,14,13 17 3 +2,2 -7 0 +71 73 0 + - - +65,62 73 0 +27,26,22,21,16,15 26 1 +69,65,63 65 1 +2,0,-4,-8,-11 - 0 +85,82,81,76 93 0 +78,77,72 78 0 +96,91,88,85,80 80 4 +28,23 22 1 +26,21,17,13,9 3 4 +30,25,24 19 2 +86 80 0 + 7 - + 5 - +61,58,55,51,47,44 60 0 +81,81,78,77,72 87 0 +98,96,95 90 2 +19,15 20 0 +64,59 63 0 +72,70,70,65 70 1 + - - + - - + -5 - +51 41 0 +72,68,67 77 0 + -6 - +6,5,1 -3 2 +87 - 0 +39 35 0 +36,36,36,31 - 0 +24,21,17 30 0 +87,87,83,79,76 68 4 + -7 - + -6 - +62,61 51 1 +67 - 0 +33,32,28 30 1 +29,27,24,20,20,18 24 2 +41,36 29 1 + 10 - +63,62,61,57 - 0 +79 76 0 +92,92,90,87,85,82 74 5 + 5 - + 0 - +47,44,43,39,34 - 0 +3,-1 -5 1 +21,20,20,15,11 - 0 +47 54 0 +68,63,60 - 0 +25,20,18,16,11,8 - 0 + -4 - +65,64,60,59,56 56 4 +82,80,78 87 0 +78,76,76,75,72 84 0 + - - +27,22,18,14 28 0 + -6 - +24,19 29 0 +75,73 81 0 + -5 - +2,-3,-3,-4,-6,-7 - 0 + -6 - +85,82 74 1 +89,85 94 0 +38,33,31,30 - 0 +96,95,94,89,89 100 0 +36 36 0 +87,87,85 87 0 +48,44,42,41 53 0 +8,3,-2,-7,-11,-14 -20 5 +26,24 - 0 +92,88,85 87 1 +89 99 0 +57,54,53,49,46,42 67 0 +86 - 0 +23,21 20 1 +2 -3 0 +20,17,17,13,8,7 29 0 +35,32,32,27,23 - 0 +8,8,7,6,2,2 13 0 +94 96 0 +18 25 0 + 8 - +46,45,45,43,40,35 35 5 +21,16,15,15,11 14 2 +72 - 0 + 7 - + - - +4 14 0 +14,12,10,7,7,2 7 3 +35,32,32,30,29 25 4 +78,75 70 1 +53,48,48 60 0 +12 18 0 +80,75,74,74 74 2 +58,56 66 0 + 3 - +26,24,19 33 0 +87,82,81,79,78 - 0 +71,71 63 0 +5,3,2 7 0 +57 55 0 + 8 - +85,80,78,74,70,68 87 0 +26,25,22,19 12 3 +76 68 0 +98,96,91,91,86,85 - 0 +36,36 37 0 +42,41 48 0 +13,10,10,5,5 6 3 +27,26,22,18 17 3 +65,63,59,54,51 61 1 +84,83,81,81,81,79 90 0 +88,88,86,81,79,78 69 5 +3,2,1 -9 2 +94,94,91,87,84 91 2 +76,76,75,73 80 0 +66,66,66,61 57 3 +2,0,-2,-3,-7,-8 -18 5 +97 92 0 +70,68,67 73 0 +96,95 90 1 +94,91,90,89,88,84 98 0 +18,14,13,8,7 -1 4 +83,80,76 - 0 +84,83,80,78,77,74 - 0 +20,16,15,12,8 1 4 +24,23,21,21,19 13 4 +53,50,50,45,41 32 4 + 5 - +64,60,60 62 0 +48,45,44,41 37 3 +90,89,85,81,81,79 - 0 + -3 - +10,9,6,4,-1 -10 4 +81,78,73 85 0 +57,54,51,49,44 - 0 +99 102 0 + 2 - +3,3 7 0 +34,32,32,31,29 29 4 + -5 - +52 44 0 + -10 - +81,79,76,71 87 0 +12,7,2,1,-2,-7 -15 5 +64 66 0 +30 - 0 +31,30,27,26,26,24 34 0 +23,18,17,15 14 3 +83,82,82 86 0 +96,92,87,86 102 0 +17,14,10,10 5 2 +82,77,74,69,65,64 66 4 +30,25,24 30 0 +20 21 0 + - - +17,13 22 0 +10,6,1,0 -2 3 +69,66,62 - 0 +65,61,58,55,55,52 71 0 +27 32 0 +20,18,14,10,9 -1 4 +37,32,29,27 - 0 +73,71 72 0 +30,27,26,21,17 11 4 +76,73,69,66 84 0 +73,72,67 76 0 +89 97 0 +9,4,0,-4,-7,-7 - 0 +82,79,78 70 2 +17,16,11 19 0 +13,8,7,4,4 -5 3 + 6 - +74,70,69,68,67,66 72 0 +68 60 0 +49,47,45 37 2 +32,27,23,23 24 2 +68,65,63,61,59 60 3 +73,73,71,69 70 2 +77,77,75,70,68,63 - 0 +76,75,75,70,69,68 64 5 +46,45,43,41 32 3 +7,4,1,-1,-3,-6 - 0 + -8 - +30,27 - 0 +12,9,5 15 0 +53,49,44,43,39,39 51 0 +52,48 45 1 +76,72 63 1 +62,61,60 71 0 +24,19,15,10 - 0 +35,33,30,28,26,26 38 0 +69,65,63,59 - 0 +64 69 0 +94 - 0 +63,63,62,61,58,58 61 3 +58,56,56,53,49,48 40 5 +80,77,76 71 2 +93,90,86,86 87 2 +63 69 0 +57,53,49,46 - 0 +52,51,48 - 0 +15,14,13,13,9 1 4 +97 101 0 +96,96,91,87,87 86 3 +98 96 0 +67,67,62,62,61 69 0 +86 94 0 +34 37 0 +29,27,22,17,15,11 8 5 +48,43 53 0 +24 30 0 + -3 - +11 11 0 +48,44 45 1 diff --git a/tests/http/versioning/memento-conformance.sh b/tests/http/versioning/memento-conformance.sh new file mode 100755 index 000000000..370e25a4e --- /dev/null +++ b/tests/http/versioning/memento-conformance.sh @@ -0,0 +1,121 @@ +#!/usr/bin/env bash +set -euo pipefail + +# The Lean model of Memento (formal/http, LdhHttp.Memento), replayed against the server. A document is written four +# times, and once its versions are committed, the history GitHub lists for its file is handed to ldh-http. The +# server's TimeMap has to list exactly that history, each Memento a prov:wasRevisionOf the one before it, and its +# TimeGate has to select what the model's selectMemento selects: with no datetime, at each commit, midway between +# two (where both are as close), and before and after the history. + +# requires a dataspace configured with lds:versioningRepository (branch "main", path prefix "graphs") +# pointing at $VERSIONING_TEST_REPO ("owner/repo"), with the token in secrets/credentials.trig +if [ -z "${VERSIONING_TEST_REPO:-}" ] || [ -z "${GITHUB_TOKEN:-}" ] || ! command -v gh > /dev/null; then + echo "SKIPPED: VERSIONING_TEST_REPO/GITHUB_TOKEN not set or gh CLI not available" + exit 0 +fi + +initialize_dataset "$END_USER_BASE_URL" "$TMP_END_USER_DATASET" "$END_USER_ENDPOINT_URL" +initialize_dataset "$ADMIN_BASE_URL" "$TMP_ADMIN_DATASET" "$ADMIN_ENDPOINT_URL" +purge_cache "$END_USER_VARNISH_SERVICE" +purge_cache "$ADMIN_VARNISH_SERVICE" +purge_cache "$FRONTEND_VARNISH_SERVICE" +reset_packages +clear_ontology + +decider="${LDH_HTTP_DECIDER:-$HTTP_TEST_ROOT/../../formal/http/.lake/build/bin/ldh-http}" +if [ ! -x "$decider" ]; then + echo "DEBUG: ldh-http not found at $decider: run 'lake build' in formal/http, or point LDH_HTTP_DECIDER at it" >&2 + exit 1 +fi + +work=$(mktemp -d) +trap 'rm -rf "$work"' EXIT + +# add agent to the writers group + +ldh admin add agent \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --agent "$AGENT_URI" \ + "${ADMIN_BASE_URL}acl/groups/writers/" + +slug=$(uuidgen | tr '[:upper:]' '[:lower:]') +doc_url="${END_USER_BASE_URL}${slug}/" +path="${VERSIONING_PATH_PREFIX:-graphs}/${slug}.nt" + +put_document() +{ + echo "<${doc_url}> . +<${doc_url}> \"${1}\" ." | \ + ldh put \ + -c "$AGENT_CERT_KEYSTORE" \ + -p "$AGENT_CERT_PWD" \ + -t "application/n-triples" \ + "$doc_url" > /dev/null +} + +# the file's history as GitHub lists it, most recent first: SHA and author datetime in seconds, as the server reads it +history() +{ + gh api "repos/${VERSIONING_TEST_REPO}/commits?path=${path}&sha=${VERSIONING_TEST_BRANCH:-main}&per_page=100" \ + --jq '.[] | "\(.sha)\t\(.commit.author.date | fromdateiso8601)"' 2> /dev/null || true +} + +iso() { date -u -d "@$1" +%Y-%m-%dT%H:%M:%SZ 2> /dev/null || date -u -r "$1" +%Y-%m-%dT%H:%M:%SZ; } + +# four versions, each committed before the next is written +for n in 1 2 3 4; do + put_document "Version $n" + for i in $(seq 1 30); do + [ "$(history | wc -l | tr -d ' ')" -ge "$n" ] && break + sleep 1 + done + count=$(history | wc -l | tr -d ' ') + echo "DEBUG: version $n: $count commits" + [ "$count" -ge "$n" ] || exit 1 +done + +history > "$work/history.tsv" +echo "DEBUG: history (most recent first):" +sed 's/^/DEBUG: /' "$work/history.tsv" + +# the TimeMap lists the history, and each Memento is a revision of the next one down it + +timemap=$( +ldh get \ + -c "$AGENT_CERT_KEYSTORE" \ + -p "$AGENT_CERT_PWD" \ + --accept 'application/n-triples' \ + --timemap \ + "$doc_url") + +expected_members=$(cut -f1 "$work/history.tsv" | sed "s|^|${doc_url}?version=|" | sort) +actual_members=$(echo "$timemap" | grep -F "<${doc_url}?timemap> " | sed -E 's/^.* <([^>]*)> \.$/\1/' | sort) +echo "DEBUG: TimeMap members. Expected:"; echo "$expected_members" | sed 's/^/DEBUG: /' +echo "DEBUG: Got:"; echo "$actual_members" | sed 's/^/DEBUG: /' +[ "$expected_members" = "$actual_members" ] || exit 1 + +expected_revisions=$(cut -f1 "$work/history.tsv" | awk -v d="$doc_url" 'NR > 1 { print d "?version=" prev " " d "?version=" $0 } { prev = $0 }' | sort) +actual_revisions=$(echo "$timemap" | grep -F "" | sed -E 's/^<([^>]*)> <[^>]*> <([^>]*)> \.$/\1 \2/' | sort) +echo "DEBUG: TimeMap revisions. Expected:"; echo "$expected_revisions" | sed 's/^/DEBUG: /' +echo "DEBUG: Got:"; echo "$actual_revisions" | sed 's/^/DEBUG: /' +[ "$expected_revisions" = "$actual_revisions" ] || exit 1 + +# the TimeGate selects what the model selects + +times=$(cut -f2 "$work/history.tsv") +first=$(echo "$times" | tail -n 1) +last=$(echo "$times" | head -n 1) +datetimes=$( { echo "$times"; echo "$times" | awk 'NR > 1 { print int((prev + $0) / 2) } { prev = $0 }'; echo $((first - 3600)); echo $((last + 3600)); } | sort -un) + +expected=$("$decider" --select "$work/history.tsv") +actual=$(ldh get -c "$AGENT_CERT_KEYSTORE" -p "$AGENT_CERT_PWD" --timegate "$doc_url") +echo "DEBUG: TimeGate with no datetime. Expected: ${doc_url}?version=${expected} Got: $actual" +[ "$actual" = "${doc_url}?version=${expected}" ] || exit 1 + +for s in $datetimes; do + expected=$("$decider" --select "$work/history.tsv" --datetime "$s") + actual=$(ldh get -c "$AGENT_CERT_KEYSTORE" -p "$AGENT_CERT_PWD" --timegate --datetime "$(iso "$s")" "$doc_url") + echo "DEBUG: TimeGate at $(iso "$s"). Expected: ${doc_url}?version=${expected} Got: $actual" + [ "$actual" = "${doc_url}?version=${expected}" ] || exit 1 +done From ed1e6025622248654835819b88b0232b7342dcb1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martynas=20Jusevi=C4=8Dius?= Date: Tue, 27 Oct 2026 08:58:38 +0100 Subject: [PATCH 2/2] Describe the formal models in the README A section after the test suite's: what the graph store and access control models prove, how the Formal workflow and the HTTP replay keep them tied to the code, and a link to the roadmap. Co-Authored-By: Claude Opus 5.5 --- README.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/README.md b/README.md index 8a9225b4a..21804ebc1 100644 --- a/README.md +++ b/README.md @@ -368,6 +368,17 @@ LinkedDataHub includes an HTTP [test suite](https://github.com/AtomGraph/LinkedD ![HTTP-tests](https://github.com/AtomGraph/LinkedDataHub/actions/workflows/http-tests.yml/badge.svg) +## Formal verification + +The parts of LinkedDataHub whose failure is a security incident are specified in [Lean 4](https://lean-lang.org/), with machine-checked proofs of what the server guarantees: + +* [graph store](formal/http/): its answer to every request, and the invariants every write keeps, covering the document hierarchy, types limited to the hierarchy classes, and ownership. A write guarded by `If-Match` loses no update, and the Memento TimeGate selects the version closest to the requested datetime +* [access control](formal/acl/): the authorization decision in front of the graph store. A denied request answers `403` and reveals nothing else, not even whether the document exists. A write to an end-user document changes no authorization over any other document, and an authorization scoped to end-user documents opens no admin document + +The models are transcribed from the code, not extracted from it. The `Formal` workflow builds them on every push, fails on an unproven theorem, and fails a pull request that changes a transcribed source without changing the model. The HTTP test suite replays the models' answers against a running server, comparing the status and the document's graph after each request. See [`formal/README.md`](formal/README.md) for the roadmap. + +![Formal](https://github.com/AtomGraph/LinkedDataHub/actions/workflows/formal.yml/badge.svg) + ## Dependencies ### Browser