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/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 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