diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml index 5ad018806..ab9cf89c8 100644 --- a/.github/workflows/formal.yml +++ b/.github/workflows/formal.yml @@ -3,8 +3,8 @@ name: Formal on: [push, pull_request] jobs: - acl-model: - name: Build the Lean ACL model and check it tracks the code + models: + name: Build the Lean models and check they track the code runs-on: ubuntu-latest steps: - name: Install Linux packages @@ -13,21 +13,32 @@ jobs: uses: actions/checkout@v7 with: fetch-depth: 0 - # elan picks the toolchain pinned in formal/acl/lean-toolchain on first use + # elan picks the toolchain pinned in each model's lean-toolchain on first use - name: Install elan run: | curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none echo "$HOME/.elan/bin" >> "$GITHUB_PATH" - - name: Build the model + - name: Build the graph store model + working-directory: formal/http + run: lake build + # the ACL model requires the graph store's, by path + - name: Build the ACL model working-directory: formal/acl run: lake build - # lake build only warns on sorry; the README's "no sorry" claim is checked here + # 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: | - if grep -rnw --include='*.lean' sorry formal/acl; then - echo "::error::formal/acl has unproven theorems" + if grep -rnw --include='*.lean' --exclude-dir=.lake sorry formal; then + echo "::error::formal/ has unproven theorems" exit 1 fi - - name: The model tracks the code + - name: The models track the code if: github.event_name == 'pull_request' - run: formal/acl/tracks-code.sh "${{ github.event.pull_request.base.sha }}" + run: | + formal/http/tracks-code.sh "${{ github.event.pull_request.base.sha }}" + formal/acl/tracks-code.sh "${{ github.event.pull_request.base.sha }}" diff --git a/.github/workflows/http-tests.yml b/.github/workflows/http-tests.yml index 21e6bcdc3..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 model's decision (formal/acl) 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/CHANGELOG.md b/CHANGELOG.md index d04a70266..84e0f69f9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -50,6 +50,7 @@ - A write whose `Accept` names no RDF syntax is no longer refused with `406` - `405` responses list the allowed methods, a `415` to `PATCH` names the accepted type, and access requests answer `201` - An anonymous `HEAD` on a document the requester may only append to is answered `200` with its entity tag instead of `403`: the front Varnish fetched a HEAD as a GET on a cache miss, so the platform decided it as a read. `HEAD` now bypasses the cache and is decided as a HEAD, the way a conditional write by an agent without `acl:Read` needs +- A chart drawn as a Table shows every variable its query selects, or every property its graph's resources carry, instead of only its category and series ### Security - A document's types, which authorizations match on, come from its own graph only, so a write to one document cannot change another's access 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/cli/pom.xml b/cli/pom.xml index 419170fc5..ec13e1d18 100644 --- a/cli/pom.xml +++ b/cli/pom.xml @@ -4,7 +4,7 @@ com.atomgraph linkeddatahub-cli - 6.3.0 + 6.3.1-SNAPSHOT jar LinkedDataHub CLI diff --git a/formal/README.md b/formal/README.md index eb31f7238..4687db24c 100644 --- a/formal/README.md +++ b/formal/README.md @@ -5,12 +5,16 @@ model lives in its own directory with its own toolchain, README and mapping to t | Directory | Tool | Covers | |-----------|------|--------| -| [`acl/`](acl/) | Lean 4 | The authorization decision, the graph store writes that change what it reads, and the 6.0 migration of seeded authorizations | +| [`http/`](http/) | Lean 4 | The graph store: its documents, its writes and the invariants they keep, and its answer to every request | +| [`acl/`](acl/) | Lean 4 | The authorization decision over the graph store's data, the server's answer with the decision in front of the graph store, and the 6.0 migration of seeded authorizations | + +The graph store model stands alone; the ACL model requires it, by path, since the decision reads the graph store's +data and its theorems about writes are about the graph store's writes. The `Formal` workflow (`.github/workflows/formal.yml`) builds every model on each push, fails on an unproven theorem, and on a pull request fails when a transcribed source changes without the model -(`acl/tracks-code.sh`). The HTTP test suite replays the ACL model's decision against the server -(`tests/http/formal/`). +(`http/tracks-code.sh`, `acl/tracks-code.sh`). The HTTP test suite replays the models' answers against the server: +the status and the document's graph after each request (`tests/http/formal/`). ## Why @@ -28,7 +32,7 @@ about the authorization decision, which is the part already modelled. ## Roadmap Each step is independent of the ones after it. The first three are the cheapest and buy most of the -credibility; the fourth is the one that answers the agent-era question and changes the product. +credibility; the fifth is the one that answers the agent-era question and changes the product. 1. **The model is a build artifact.** Done in this directory's `Formal` workflow: `lake build`, a `sorry` check and the drift check. The README mapping stops being a promise kept by hand. @@ -40,29 +44,44 @@ credibility; the fourth is the one that answers the agent-era question and chang before every request. Verifying the Java directly is not worth the cost; this is how the proofs constrain the code. -3. **Every hypothesis of a theorem is an enforced constraint.** `AdminTyped`, `Typed`, `Site.Finite` - and `Reader.Expressive` (see `acl/README.md`, "What the proofs need of the data") are premises an - attacker can try to falsify. Each gets a server-side check and a negative HTTP test. - -4. **Delegation as non-interference.** Model `On-Behalf-Of` and `acl:delegates`, and prove that for +3. **Every hypothesis of a theorem is an enforced constraint.** Done: of the premises in `acl/README.md`, + "What the proofs need of the data", the two a request can falsify, `AdminTyped` and `Typed`, are kept by + a type rule on every write (`checkDocumentTypes`), proven preserved by `Step.adminTyped` and `Step.typed`, + and tried by negative HTTP tests. `Site.Finite` and `Reader.Expressive` are facts about URIs and the + query, with nothing to falsify. + +4. **The graph store's answer is modelled, and the server is replayed against it.** Done: the graph store + is a model of its own, `http/`, which the ACL model now requires. `http/LdhHttp/Answer.lean` gives every + status a graph store request can get and the store after it, as a program, and proves that a refused + request changes nothing and that a request that goes through is a `Write`, so the graph store keeps + 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. `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 the caller could execute alone, independently of prompt content. That reduces prompt injection to misuse within existing rights, and motivates scoping `acl:delegates`, which today delegates everything. Scoped delegation is the one design change this roadmap expects to force. -5. **Concurrency in its own model.** The lock protocol (a `PUT` holds its parent's lock and re-checks +6. **Concurrency in its own model.** The lock protocol (a `PUT` holds its parent's lock and re-checks the parent exists, a `DELETE` checks for children) is a TLA+ problem: a small model and TLC, in a sibling directory. Lean is the wrong tool for it. -6. **Chokepoints checked by structure.** The input-handling class is closed by `SecureXML` and +7. **Chokepoints checked by structure.** The input-handling class is closed by `SecureXML` and `URLValidator` being the only paths to a parser or an outbound connection. Architecture tests that forbid raw XML parser factories, URL opening and SPARQL string concatenation outside those classes turn that from a convention into a build failure. -7. **The claims are published.** A threat model page in the wiki, a `SECURITY.md` stating what is +8. **The claims are published.** A threat model page in the wiki, a `SECURITY.md` stating what is proven and under which hypotheses, and the model handed to the next penetration retest as its oracle. ## Not in scope -Authentication (WebID, OAuth, delegation until step 4), content negotiation, caching, imports, uploads, +Authentication (WebID, OAuth, delegation until step 5), content negotiation, caching, imports, uploads, XSLT and the client. Each is a candidate for its own model once the ones above hold. diff --git a/formal/acl/LdhAcl.lean b/formal/acl/LdhAcl.lean index f31bfe8d0..25180d69e 100644 --- a/formal/acl/LdhAcl.lean +++ b/formal/acl/LdhAcl.lean @@ -1,6 +1,6 @@ -import LdhAcl.Base import LdhAcl.Model import LdhAcl.Step import LdhAcl.Theorems import LdhAcl.Migration import LdhAcl.Decide +import LdhAcl.Gate diff --git a/formal/acl/LdhAcl/Decide.lean b/formal/acl/LdhAcl/Decide.lean index 601ed28b5..2a9742982 100644 --- a/formal/acl/LdhAcl/Decide.lean +++ b/formal/acl/LdhAcl/Decide.lean @@ -7,131 +7,7 @@ import LdhAcl.Theorems namespace LdhAcl -/-! ## Finite data -/ - -/-- A store as data: a document's graph as the list of its triples. A document listed more than once has the -union of its lists. -/ -abbrev FinStore := List (Node × List Triple) - -/-- The graph store's notion of existence, computed. -/ -def hasDoc (fs : FinStore) (d : Node) : Bool := fs.any (·.1 == d) - -/-- The triples of a document's own graph. -/ -def graphOf (fs : FinStore) (d : Node) : List Triple := - fs.foldr (fun p acc => if p.1 = d then p.2 ++ acc else acc) [] - -/-- The abstract store the data denotes. -/ -def FinStore.toStore (fs : FinStore) : Store := - fun d => if hasDoc fs d then some (fun t => t ∈ graphOf fs d) else none - -theorem hasDoc_iff {fs : FinStore} {d : Node} : hasDoc fs d = true ↔ ∃ ts, (d, ts) ∈ fs := by - simp only [hasDoc, List.any_eq_true, beq_iff_eq] - constructor - · rintro ⟨⟨d', ts⟩, h, rfl⟩ - exact ⟨ts, h⟩ - · rintro ⟨ts, h⟩ - exact ⟨(d, ts), h, rfl⟩ - -theorem graphOf_cons {p : Node × List Triple} {fs : FinStore} {d : Node} : - graphOf (p :: fs) d = if p.1 = d then p.2 ++ graphOf fs d else graphOf fs d := rfl - -theorem mem_graphOf {fs : FinStore} {d : Node} {t : Triple} : - t ∈ graphOf fs d ↔ ∃ ts, (d, ts) ∈ fs ∧ t ∈ ts := by - induction fs with - | nil => simp [graphOf] - | cons p fs ih => - obtain ⟨p1, p2⟩ := p - rw [graphOf_cons] - by_cases h : p1 = d - · subst h - simp only [if_true, List.mem_append, ih, List.mem_cons] - constructor - · rintro (ht | ⟨ts, hts, ht⟩) - · exact ⟨p2, Or.inl rfl, ht⟩ - · exact ⟨ts, Or.inr hts, ht⟩ - · rintro ⟨ts, hts | hts, ht⟩ - · cases hts; exact Or.inl ht - · exact Or.inr ⟨ts, hts, ht⟩ - · simp only [h, if_false, ih, List.mem_cons] - constructor - · rintro ⟨ts, hts, ht⟩ - exact ⟨ts, Or.inr hts, ht⟩ - · rintro ⟨ts, hts | hts, ht⟩ - · cases hts; exact absurd rfl h - · exact ⟨ts, hts, ht⟩ - -theorem hasDoc_of_mem_graphOf {fs : FinStore} {d : Node} {t : Triple} (h : t ∈ graphOf fs d) : - hasDoc fs d = true := by - obtain ⟨ts, hm, _⟩ := mem_graphOf.1 h - exact hasDoc_iff.2 ⟨ts, hm⟩ - -theorem toStore_of_hasDoc {fs : FinStore} {d : Node} (h : hasDoc fs d = true) : - fs.toStore d = some (fun t => t ∈ graphOf fs d) := by - simp [FinStore.toStore, h] - -theorem toStore_of_not_hasDoc {fs : FinStore} {d : Node} (h : ¬ hasDoc fs d = true) : - fs.toStore d = none := by - simp [FinStore.toStore, h] - -theorem present_iff {fs : FinStore} {d : Node} : present fs.toStore d ↔ hasDoc fs d = true := by - constructor - · rintro ⟨g, hg⟩ - unfold FinStore.toStore at hg - split at hg - · assumption - · cases hg - · intro h - exact ⟨_, toStore_of_hasDoc h⟩ - -/-- A triple of a document's own graph. -/ -theorem own_iff {fs : FinStore} {d : Node} {t : Triple} : - (∃ g, fs.toStore d = some g ∧ g t) ↔ t ∈ graphOf fs d := by - constructor - · rintro ⟨g, hg, ht⟩ - by_cases h : hasDoc fs d = true - · rw [toStore_of_hasDoc h] at hg - cases hg - exact ht - · rw [toStore_of_not_hasDoc h] at hg - cases hg - · intro ht - exact ⟨_, toStore_of_hasDoc (hasDoc_of_mem_graphOf ht), ht⟩ - -theorem ownTypes_iff {fs : FinStore} {x t : Node} : - ownTypes fs.toStore x t ↔ ⟨x, .rdfType, t⟩ ∈ graphOf fs x := own_iff - -theorem owner_iff {fs : FinStore} {x a : Node} : - owner fs.toStore x a ↔ ⟨x, .aclOwner, a⟩ ∈ graphOf fs x := own_iff - -/-- The objects of a document's own `rdf:type` triples. -/ -def typesOf (fs : FinStore) (x : Node) : List Node := - (graphOf fs x).filterMap fun t => if t.s = x ∧ t.p = .rdfType then some t.o else none - -/-- The objects of a document's own `acl:owner` triples. -/ -def ownersOf (fs : FinStore) (x : Node) : List Node := - (graphOf fs x).filterMap fun t => if t.s = x ∧ t.p = .aclOwner then some t.o else none - -theorem mem_filterMap_prop {fs : FinStore} {x p o : Node} : - o ∈ ((graphOf fs x).filterMap fun t => if t.s = x ∧ t.p = p then some t.o else none) ↔ - ⟨x, p, o⟩ ∈ graphOf fs x := by - simp only [List.mem_filterMap] - constructor - · rintro ⟨⟨s, p', o'⟩, ht, h⟩ - simp only at h - split at h - · rename_i hsp - cases h - obtain ⟨rfl, rfl⟩ := hsp - exact ht - · cases h - · intro h - exact ⟨_, h, by simp⟩ - -theorem mem_typesOf {fs : FinStore} {x t : Node} : t ∈ typesOf fs x ↔ ownTypes fs.toStore x t := - mem_filterMap_prop.trans ownTypes_iff.symm - -theorem mem_ownersOf {fs : FinStore} {x a : Node} : a ∈ ownersOf fs x ↔ owner fs.toStore x a := - mem_filterMap_prop.trans owner_iff.symm +open LdhHttp /-! ## Containment, as edges -/ @@ -277,8 +153,7 @@ def FinAdmin.reader (fa : FinAdmin) : Reader where sub_refl := fun _ => Or.inl rfl /-- The deployment constants, computed. -/ -structure FinSite where - parent : Node → Node +structure FinSite extends HSite where admin : Node → Bool def FinSite.agrees (fsite : FinSite) (site : Site) : Prop := diff --git a/formal/acl/LdhAcl/Gate.lean b/formal/acl/LdhAcl/Gate.lean new file mode 100644 index 000000000..13a92234e --- /dev/null +++ b/formal/acl/LdhAcl/Gate.lean @@ -0,0 +1,76 @@ +/- +The graph store's answer behind the authorization decision: the decision first, then `LdhHttp.answerB`. + +Three theorems hold of the two together and of neither alone: a request is answered `403` exactly when the decision +denies it (`decide_forbidden_iff`), so a denied agent learns nothing a later check would say; a request that goes +through is a `Step`, an authorized `Write` (`decide_step`); and so the server keeps the invariants, including the +typing of admin documents the decision's class grants depend on (`decide_inv`). +-/ +import LdhAcl.Decide + +namespace LdhAcl + +open LdhHttp + +/-- The server's answer: the decision first, and nothing else for a request it denies. -/ +def decideB (fsite : FinSite) (fs : FinStore) (fa : FinAdmin) (agent : Option Node) (pc : Precond) (req : HReq) : + Except Refusal (Success × FinStore) := + if allowRequestB fsite fs fa agent (req.method pc) req.target then answerB fsite.toHSite fs agent pc req + else .error .forbidden + +/-- The status and the store after the request. -/ +def serveB (fsite : FinSite) (fs : FinStore) (fa : FinAdmin) (agent : Option Node) (pc : Precond) (req : HReq) : + Nat × FinStore := + match decideB fsite fs fa agent pc req with + | .ok (s, fs') => (s.code, fs') + | .error r => (r.code, fs) + +/-- **A refused request changes nothing.** -/ +theorem serve_refused {fsite fs fa agent pc req r} (h : decideB fsite fs fa agent pc req = .error r) : + serveB fsite fs fa agent pc req = (r.code, fs) := by + simp [serveB, h] + +/-- **`403` is the decision's, and only the decision's.** A request is answered `403` exactly when the model +denies it, and a denied request learns nothing else: not whether the document exists, nor anything a later check +would have said about it. -/ +theorem decide_forbidden_iff {site : Site} {fsite : FinSite} (h : fsite.agrees site) {fs fa agent pc req} : + decideB fsite fs fa agent pc req = .error .forbidden ↔ + ¬ allowRequest site fa.reader fs.toStore agent (req.method pc) req.target := by + rw [allowRequest_iff h] + constructor + · intro hd ha + simp only [decideB, ha, if_true] at hd + exact answer_not_forbidden hd + · intro hn + simp [decideB, hn] + +/-- **A request that goes through is an authorized write, or changes nothing.** -/ +theorem decide_step {site : Site} {fsite : FinSite} (h : fsite.agrees site) (ht : fsite.toHSite.agrees site.toTree) + {fs : FinStore} {fa : FinAdmin} {agent : Option Node} {pc : Precond} {req : HReq} {s : Success} {fs' : FinStore} + (hown : OwnGraphContainment fs.toStore) (hd : decideB fsite fs fa agent pc req = .ok (s, fs')) : + fs' = fs ∨ ∃ r, Step site fa.reader agent fs.toStore r fs'.toStore := by + unfold decideB at hd + split at hd + · rename_i ha + have ha := (allowRequest_iff h _ _).2 ha + rcases answer_write ht hown hd with rfl | ⟨r, ⟨htg, hm⟩, hw⟩ + · exact Or.inl rfl + · refine Or.inr ⟨r, ⟨?_, hw⟩⟩ + rw [htg] + rcases hm with hm | ⟨hp, hm⟩ + · rw [hm]; exact ha + · rw [hm]; rw [hp] at ha; exact ha + · cases hd + +/-- **The server keeps the invariants.** Every answer leaves the containment invariants, and the typing of +documents and of admin documents, as it found them. -/ +theorem decide_inv {site : Site} {fsite : FinSite} (h : fsite.agrees site) (ht : fsite.toHSite.agrees site.toTree) + {fs : FinStore} {fa : FinAdmin} {agent : Option Node} {pc : Precond} {req : HReq} {s : Success} {fs' : FinStore} + (hinv : Inv site.toTree fs.toStore) (hd : decideB fsite fs fa agent pc req = .ok (s, fs')) : + Inv site.toTree fs'.toStore ∧ (AdminTyped site fs.toStore → AdminTyped site fs'.toStore) ∧ + (Typed fs.toStore → Typed fs'.toStore) := by + rcases decide_step h ht hinv.own hd with rfl | ⟨_, hs⟩ + · exact ⟨hinv, id, id⟩ + · exact ⟨hs.inv hinv, hs.adminTyped, hs.typed⟩ + +end LdhAcl diff --git a/formal/acl/LdhAcl/Migration.lean b/formal/acl/LdhAcl/Migration.lean index 6127a369b..cc57b3b6b 100644 --- a/formal/acl/LdhAcl/Migration.lean +++ b/formal/acl/LdhAcl/Migration.lean @@ -10,13 +10,12 @@ import LdhAcl.Theorems namespace LdhAcl +open LdhHttp + /-- URI paths are finite: every non-root document's parent chain ends at a root. -/ def Site.Finite (site : Site) : Prop := ∀ d, ¬ site.isRoot d → site.chain d site.euRoot ∨ site.chain d site.adRoot -/-- Every document the store has is typed with a hierarchy class. -/ -def Typed (st : Store) : Prop := ∀ x, present st x → ∃ t, ownTypes st x t ∧ hierClass t - /-- An authorization with its targets replaced. -/ def Auth.withTargets (au : Auth) (accessTo default accessToClass : List Node) : Auth := { au with accessTo, default, accessToClass } @@ -36,7 +35,7 @@ theorem below_adRoot {site : Site} (hf : site.Finite) {d : Node} (hd : site.admi · exact hc /-- A grant on a root and its descendants covers every document the store has in that root's tree. -/ -theorem root_grant_covers {site : Site} {st : Store} (h : Inv site st) {au : Auth} {sub} +theorem root_grant_covers {site : Site} {st : Store} (h : Inv site.toTree st) {au : Auth} {sub} {root x : Node} (hc : site.chain x root ∨ x = root) (hx : present st x) : (au.withTargets [root] [root] []).covers sub (context st x) := by rw [covers_context] @@ -49,7 +48,7 @@ theorem root_grant_covers {site : Site} {st : Store} (h : Inv site st) {au : Aut /-- **The admin role in plain WAC.** `accessTo` and `acl:default` on the admin root cover every admin document, which `ownerAclQuery` gave `acl:Control` over `def:Root` before 6.0 without looking at the target. -/ -theorem admin_role_covers {site : Site} {st : Store} (h : Inv site st) (hf : site.Finite) {au : Auth} +theorem admin_role_covers {site : Site} {st : Store} (h : Inv site.toTree st) (hf : site.Finite) {au : Auth} {sub} {x : Node} (hx : site.admin x) (hp : present st x) : (au.withTargets [site.adRoot] [site.adRoot] []).covers sub (context st x) := by by_cases hr : x = site.adRoot @@ -73,7 +72,7 @@ theorem class_grant_covers {st : Store} (ht : Typed st) {au : Auth} {sub : Node /-- **On the end-user dataspace the migration changes nothing.** A class grant on the hierarchy classes and a default grant on the end-user root cover the same documents. -/ -theorem migrate_endUser {site : Site} {rd : Reader} {st : Store} (h : Inv site st) (hf : site.Finite) +theorem migrate_endUser {site : Site} {rd : Reader} {st : Store} (h : Inv site.toTree st) (hf : site.Finite) (ht : Typed st) {au : Auth} {x : Node} (hx : ¬ site.admin x) (hp : present st x) : (au.withTargets [] [] hierClasses).covers rd.sub (context st x) ↔ (au.withTargets [site.euRoot] [site.euRoot] []).covers rd.sub (context st x) := by @@ -84,7 +83,7 @@ theorem migrate_endUser {site : Site} {rd : Reader} {st : Store} (h : Inv site s /-- **On the admin dataspace the migration takes access away.** The class grant covers every admin document; the default grant on the end-user root covers none. -/ -theorem migrate_admin {site : Site} {rd : Reader} {st : Store} (h : Inv site st) (ht : Typed st) +theorem migrate_admin {site : Site} {rd : Reader} {st : Store} (h : Inv site.toTree st) (ht : Typed st) (hat : AdminTyped site st) {au : Auth} {x : Node} (hx : site.admin x) (hp : present st x) : (au.withTargets [] [] hierClasses).covers rd.sub (context st x) ∧ ¬ (au.withTargets [site.euRoot] [site.euRoot] []).covers rd.sub (context st x) := by @@ -111,7 +110,7 @@ theorem ownerAccess_endUserOnly (site : Site) (sub : Node → Node → Prop) : /-- **Owner access is the owner grant of releases before 6.0 on the end-user dataspace.** The owner-access authorization matches an agent on an end-user document exactly when the agent owns it, which is when `createOwnerAuthorization` fired. -/ -theorem ownerAccess_endUser {site : Site} {sub : Node → Node → Prop} {st : Store} (h : Inv site st) +theorem ownerAccess_endUser {site : Site} {sub : Node → Node → Prop} {st : Store} (h : Inv site.toTree st) (hf : site.Finite) {M : Node → Node → Prop} {x a : Node} (hx : ¬ site.admin x) (hp : present st x) : ((ownerAccess site).principal M (owner st x) (some a) ∧ (ownerAccess site).covers sub (context st x)) ↔ owner st x a := by @@ -131,7 +130,7 @@ theorem ownerAccess_endUser {site : Site} {sub : Node → Node → Prop} {st : S /-- **Owner access opens nothing in the admin dataspace.** The owner grant of releases before 6.0 applied there too, so an admin kept acl:Write on every authorization it created after leaving the owners group. -/ -theorem ownerAccess_admin {site : Site} {rd : Reader} {st : Store} (h : Inv site st) +theorem ownerAccess_admin {site : Site} {rd : Reader} {st : Store} (h : Inv site.toTree st) (hat : AdminTyped site st) {x : Node} (hx : site.admin x) : ¬ (ownerAccess site).covers rd.sub (context st x) := endUserOnly_confined h hat (ownerAccess_endUserOnly site rd.sub) hx diff --git a/formal/acl/LdhAcl/Model.lean b/formal/acl/LdhAcl/Model.lean index 96a00fcbb..db74d1625 100644 --- a/formal/acl/LdhAcl/Model.lean +++ b/formal/acl/LdhAcl/Model.lean @@ -10,10 +10,22 @@ The authorization decision of `AuthorizationFilter`: plain WAC over LinkedDataHu from the document's own graph (`documentContextQuery`), authorizations and memberships from the admin document they are the primary topic of (`aclQuery`). -/ -import LdhAcl.Base +import LdhHttp namespace LdhAcl +open LdhHttp + +/-- `acl:Read`, `acl:Append`, `acl:Write`, `acl:Control`. -/ +inductive Mode where + | read | append | write | control + deriving DecidableEq, Repr + +/-- `AccessModes.covering`: a granted mode covers the required one if it is that mode or one of its +superclasses in `acl.rdf`, where the only edge between modes is `acl:Append rdfs:subClassOf acl:Write`. -/ +def Mode.covers (granted required : Mode) : Prop := + granted = required ∨ (granted = .write ∧ required = .append) + /-! ## The two dataspaces -/ /-- Deployment constants. The end-user and the admin dataspace are two URI trees: `parent` (the URI parent @@ -30,17 +42,11 @@ structure Site where def Site.isRoot (site : Site) (d : Node) : Prop := d = site.euRoot ∨ d = site.adRoot -/-- The classes of the document hierarchy, which both dataspaces type their documents with. -/ -def hierClass (c : Node) : Prop := c = .defRoot ∨ c = .dhContainer ∨ c = .dhItem +/-- The document hierarchy the graph store keeps: the URI parent, and the two roots. -/ +@[reducible] def Site.toTree (site : Site) : Tree := ⟨site.parent, site.isRoot⟩ /-! ## Containment and ancestry -/ -def isContainment (t : Triple) : Prop := t.p = .siocHasParent ∨ t.p = .siocHasContainer - -/-- `g` states that `d` is contained in `p`. -/ -def contains (g : Graph) (d p : Node) : Prop := - g ⟨d, .siocHasParent, p⟩ ∨ g ⟨d, .siocHasContainer, p⟩ - /-- A containment triple in *any* graph: what a path over `urn:x-arq:UnionGraph` sees. -/ def parentU (st : Store) (d p : Node) : Prop := ∃ y g, st y = some g ∧ contains g d p diff --git a/formal/acl/LdhAcl/Step.lean b/formal/acl/LdhAcl/Step.lean index 17393e146..9e43f388b 100644 --- a/formal/acl/LdhAcl/Step.lean +++ b/formal/acl/LdhAcl/Step.lean @@ -1,302 +1,47 @@ /- -The writes of `DocumentHierarchyGraphStoreImpl`, and the invariants they keep. - -Each write touches one graph, the request URI's, and is modelled only in the triples the decision reads: the -document's ownership and containment. A graph written for document `x` may state containment of `x` only: a payload -with `sioc:has_parent` or `sioc:has_container` of any other subject is refused (`422`, `checkForeignContainment`), -and containment of `x` itself is stripped or guarded. That rule is what makes the union graph a faithful view of -containment. +An authorized write: a request the decision allows, and the `Write` the graph store makes of it (`LdhHttp.Write`). +What the graph store's writes keep (containment, the hierarchy, the typing of documents) is theirs; what this file +adds is what follows for the authorization decision, which reads the stores they change. -/ import LdhAcl.Model namespace LdhAcl -/-- The write rule: every containment triple of `g` is about `x`. -/ -def NoForeign (x : Node) (g : Graph) : Prop := ∀ t, g t → isContainment t → t.s = x - -/-- The containment `put()` asserts for a non-root document: both `sioc:has_parent` and -`sioc:has_container` are allowed by the model, always pointing at the URI parent. -/ -def containedIn (site : Site) (x : Node) (t : Triple) : Prop := - ¬ site.isRoot x ∧ t.s = x ∧ isContainment t ∧ t.o = site.parent x +open LdhHttp /-- One authorized write by `agent`, from `st` to `st'`, on either dataspace's store. -/ -inductive Step (site : Site) (rd : Reader) (agent : Option Node) : Store → Req → Store → Prop where - | post {st x payload g} : - allowRequest site rd st agent .post x → - st x = some g → - NoForeign x payload → - Step site rd agent st (.post x payload) - (st.set x (some fun t => g t ∨ (payload t ∧ ¬ ownership x t ∧ ¬ containment x t))) - | putExisting {st x payload createOnly g} : - allowRequest site rd st agent (Req.put x payload createOnly).method x → - st x = some g → - createOnly = false → - NoForeign x payload → - Step site rd agent st (.put x payload createOnly) - (st.set x (some fun t => - (payload t ∧ ¬ ownership x t ∧ ¬ containment x t) ∨ containedIn site x t ∨ - (g t ∧ ownership x t))) - | putNew {st x payload createOnly} : - allowRequest site rd st agent (Req.put x payload createOnly).method x → - st x = none → - NoForeign x payload → - Step site rd agent st (.put x payload createOnly) - (st.set x (some fun t => - (payload t ∧ ¬ ownership x t ∧ ¬ containment x t) ∨ containedIn site x t ∨ - (∃ a, agent = some a ∧ t.s = x ∧ (t.p = .aclOwner ∨ t.p = .dctCreator) ∧ t.o = a))) - | patch {st x after g} : - allowRequest site rd st agent .patch x → - st x = some g → - NoForeign x after → - (∀ t, ownership x t ∨ containment x t → (after t ↔ g t)) → - Step site rd agent st (.patch x after) (st.set x (some after)) - | delete {st x} : - allowRequest site rd st agent .delete x → - ¬ site.isRoot x → - ¬ hasChild st x → - Step site rd agent st (.delete x) (st.set x none) +structure Step (site : Site) (rd : Reader) (agent : Option Node) (st : Store) (req : Req) (st' : Store) : Prop where + authorized : allowRequest site rd st agent req.method req.target + write : Write site.toTree agent st req st' theorem Step.frame {site rd agent st req st'} (h : Step site rd agent st req st') - {y : Node} (hy : y ≠ req.target) : st' y = st y := by - cases h <;> simp [Store.set, Req.target] at hy ⊢ <;> simp [hy] - -theorem Step.authorized {site rd agent st req st'} (h : Step site rd agent st req st') : - allowRequest site rd st agent req.method req.target := by - cases h <;> assumption - -/-! ## Invariants -/ - -/-- What the write rule maintains: every containment triple sits in its subject's own graph. -/ -def OwnGraphContainment (st : Store) : Prop := - ∀ y g t, st y = some g → g t → isContainment t → t.s = y - -/-- A document's own graph points its containment at its URI parent and nowhere else. -/ -def Exact (site : Site) (st : Store) : Prop := - ∀ d g p, st d = some g → contains g d p → ¬ site.isRoot d ∧ p = site.parent d - -/-- Every non-root document's own graph states its containment. -/ -def Contained (site : Site) (st : Store) : Prop := - ∀ d g, st d = some g → ¬ site.isRoot d → contains g d (site.parent d) - -/-- Every non-root document's URI parent is in the store. -/ -def Hier (site : Site) (st : Store) : Prop := - ∀ d, present st d → ¬ site.isRoot d → present st (site.parent d) - -def RootsPresent (site : Site) (st : Store) : Prop := - present st site.euRoot ∧ present st site.adRoot - -structure Inv (site : Site) (st : Store) : Prop where - own : OwnGraphContainment st - exact : Exact site st - contained : Contained site st - hier : Hier site st - roots : RootsPresent site st - -theorem present_set_self {st : Store} {x : Node} {g : Graph} : present (st.set x (some g)) x := - ⟨g, by simp [Store.set]⟩ - -theorem present_set_other {st : Store} {x z : Node} {v} (h : z ≠ x) : - present (st.set x v) z ↔ present st z := by - simp [present, Store.set, h] - -/-- Every write but a delete leaves a graph at its target. -/ -theorem Step.present_target {site rd agent st req st'} (h : Step site rd agent st req st') - (hd : ∀ x, req ≠ .delete x) : present st' req.target := by - cases h with - | delete => exact absurd rfl (hd _) - | _ => exact present_set_self - -/-- Every write but a delete keeps every present document present. -/ -theorem Step.present_mono {site rd agent st req st'} (h : Step site rd agent st req st') - (hd : ∀ x, req ≠ .delete x) {p : Node} (hp : present st p) : present st' p := by - by_cases hpx : p = req.target - · rw [hpx]; exact h.present_target hd - · obtain ⟨g, hg⟩ := hp; exact ⟨g, by rw [h.frame hpx]; exact hg⟩ - -theorem ownership_not_containment {x : Node} {t : Triple} (ho : ownership x t) (hc : isContainment t) : - False := by - obtain ⟨_, hp⟩ := ho - rcases hp with hp | hp <;> rcases hc with hc | hc <;> rw [hp] at hc <;> cases hc - -theorem own_preserved {site rd agent st req st'} (hs : Step site rd agent st req st') - (h : OwnGraphContainment st) : OwnGraphContainment st' := by - intro y g' t hy ht hc - by_cases hyx : y = req.target - · cases hs with - | @post x _ g _ hg hnf => - simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy; subst hy - rcases ht with ht | ⟨ht, _⟩ - · exact h _ _ _ hg ht hc - · exact hnf _ ht hc - | putExisting _ _ _ hnf => - simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy; subst hy - rcases ht with ⟨ht, _⟩ | ⟨_, hs, _⟩ | ⟨_, hs, _⟩ - · exact hnf _ ht hc - · exact hs - · exact hs - | putNew _ _ hnf => - simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy; subst hy - rcases ht with ⟨ht, _⟩ | ⟨_, hs, _⟩ | ⟨_, _, hs, _⟩ - · exact hnf _ ht hc - · exact hs - · exact hs - | patch _ _ hnf _ => - simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy; subst hy - exact hnf _ ht hc - | delete => - simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy - · rw [hs.frame hyx] at hy - exact h _ _ _ hy ht hc - -theorem exact_preserved {site rd agent st req st'} (hs : Step site rd agent st req st') - (h : Exact site st) : Exact site st' := by - intro d g' p hd hc - by_cases hdx : d = req.target - · cases hs with - | @post x _ g _ hg _ => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd - rcases hc with (hc | ⟨_, _, hn⟩) | (hc | ⟨_, _, hn⟩) - · exact h _ _ _ hg (Or.inl hc) - · exact absurd ⟨rfl, Or.inl rfl⟩ hn - · exact h _ _ _ hg (Or.inr hc) - · exact absurd ⟨rfl, Or.inr rfl⟩ hn - | putExisting => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd - rcases hc with (⟨_, _, hn⟩ | ⟨hr, _, _, ho⟩ | ⟨_, ho⟩) | (⟨_, _, hn⟩ | ⟨hr, _, _, ho⟩ | ⟨_, ho⟩) - · exact absurd ⟨rfl, Or.inl rfl⟩ hn - · exact ⟨hr, ho⟩ - · exact (ownership_not_containment ho (Or.inl rfl)).elim - · exact absurd ⟨rfl, Or.inr rfl⟩ hn - · exact ⟨hr, ho⟩ - · exact (ownership_not_containment ho (Or.inr rfl)).elim - | putNew => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd - rcases hc with (⟨_, _, hn⟩ | ⟨hr, _, _, ho⟩ | ⟨_, _, _, hp, _⟩) | - (⟨_, _, hn⟩ | ⟨hr, _, _, ho⟩ | ⟨_, _, _, hp, _⟩) - · exact absurd ⟨rfl, Or.inl rfl⟩ hn - · exact ⟨hr, ho⟩ - · rcases hp with hp | hp <;> cases hp - · exact absurd ⟨rfl, Or.inr rfl⟩ hn - · exact ⟨hr, ho⟩ - · rcases hp with hp | hp <;> cases hp - | @patch x _ g _ hg _ hkeep => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd - rcases hc with hc | hc - · exact h _ _ _ hg (Or.inl ((hkeep _ (Or.inr ⟨rfl, Or.inl rfl⟩)).1 hc)) - · exact h _ _ _ hg (Or.inr ((hkeep _ (Or.inr ⟨rfl, Or.inr rfl⟩)).1 hc)) - | delete => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd - · rw [hs.frame hdx] at hd - exact h _ _ _ hd hc - -theorem contained_preserved {site rd agent st req st'} (hs : Step site rd agent st req st') - (h : Contained site st) : Contained site st' := by - intro d g' hd hroot - by_cases hdx : d = req.target - · cases hs with - | @post x _ g _ hg _ => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd - rcases h d g hg hroot with hc | hc - · exact Or.inl (Or.inl hc) - · exact Or.inr (Or.inl hc) - | putExisting => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd - exact Or.inl (Or.inr (Or.inl ⟨hroot, rfl, Or.inl rfl, rfl⟩)) - | putNew => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd - exact Or.inl (Or.inr (Or.inl ⟨hroot, rfl, Or.inl rfl, rfl⟩)) - | @patch x _ g _ hg _ hkeep => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd - rcases h d g hg hroot with hc | hc - · exact Or.inl ((hkeep _ (Or.inr ⟨rfl, Or.inl rfl⟩)).2 hc) - · exact Or.inr ((hkeep _ (Or.inr ⟨rfl, Or.inr rfl⟩)).2 hc) - | delete => - simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd - · rw [hs.frame hdx] at hd - exact h d g' hd hroot - -theorem ownTypes_present {st : Store} {x t : Node} (h : ownTypes st x t) : present st x := by - obtain ⟨g, hg, _⟩ := h; exact ⟨g, hg⟩ - -/-- A create is authorized only below a present parent. -/ -theorem create_parent_present {site rd st agent m x} (hnew : st x = none) - (ha : allow site rd st agent True m x) : present st (site.parent x) := by - rcases ha with ⟨hp | hn, _⟩ | ⟨_, _, ht, _⟩ - · obtain ⟨g, hg⟩ := hp; simp [hnew] at hg - · exact absurd trivial hn - · rcases ht with ht | ht <;> exact ownTypes_present ht - -theorem put_allow {site rd st agent x payload createOnly} - (ha : allowRequest site rd st agent (Req.put x payload createOnly).method x) : - ∃ m, allow site rd st agent True m x := by - cases createOnly <;> exact ⟨_, ha⟩ - -theorem hier_preserved {site rd agent st req st'} (hs : Step site rd agent st req st') - (h : Hier site st) (hc : Contained site st) : Hier site st' := by - intro d hd hroot - cases hs with - | @delete x _ _ noChild => - have hdx : d ≠ x := by - rintro rfl; obtain ⟨g, hg⟩ := hd; simp [Store.set] at hg - have hd0 := (present_set_other hdx).1 hd - have hp := h d hd0 hroot - by_cases hpx : site.parent d = x - · obtain ⟨g, hg⟩ := hd0 - have hcd := hc d g hg hroot - rw [hpx] at hcd - exact absurd ⟨d, g, hdx, hg, hcd⟩ noChild - · exact (present_set_other hpx).2 hp - | @putNew x _ _ ha hn hnf => - have hs' : Step site rd agent st (.put x _ _) _ := Step.putNew ha hn hnf - apply hs'.present_mono (by intro _ h; cases h) - by_cases hdx : d = x - · subst hdx - obtain ⟨m, ham⟩ := put_allow ha - exact create_parent_present hn ham - · exact h d ((present_set_other hdx).1 hd) hroot - | @post x _ g ha hg hnf => - have hs' := Step.post (site := site) (rd := rd) (agent := agent) ha hg hnf - apply hs'.present_mono (by intro _ h; cases h) - by_cases hdx : d = x - · subst hdx; exact h d ⟨_, hg⟩ hroot - · exact h d ((present_set_other hdx).1 hd) hroot - | @putExisting x _ _ g ha hg hc' hnf => - have hs' := Step.putExisting (site := site) (rd := rd) (agent := agent) ha hg hc' hnf - apply hs'.present_mono (by intro _ h; cases h) - by_cases hdx : d = x - · subst hdx; exact h d ⟨_, hg⟩ hroot - · exact h d ((present_set_other hdx).1 hd) hroot - | @patch x _ g ha hg hnf hkeep => - have hs' := Step.patch (site := site) (rd := rd) (agent := agent) ha hg hnf hkeep - apply hs'.present_mono (by intro _ h; cases h) - by_cases hdx : d = x - · subst hdx; exact h d ⟨_, hg⟩ hroot - · exact h d ((present_set_other hdx).1 hd) hroot - -theorem roots_preserved {site rd agent st req st'} (hs : Step site rd agent st req st') - (h : RootsPresent site st) : RootsPresent site st' := by - cases hs with - | @delete x _ hr _ => - have he : site.euRoot ≠ x := fun e => hr (Or.inl e.symm) - have ha : site.adRoot ≠ x := fun e => hr (Or.inr e.symm) - exact ⟨(present_set_other he).2 h.1, (present_set_other ha).2 h.2⟩ - | post ha hg hnf => - have hs' := Step.post (site := site) (rd := rd) (agent := agent) ha hg hnf - exact ⟨hs'.present_mono (by intro _ h; cases h) h.1, hs'.present_mono (by intro _ h; cases h) h.2⟩ - | putExisting ha hg hc hnf => - have hs' := Step.putExisting (site := site) (rd := rd) (agent := agent) ha hg hc hnf - exact ⟨hs'.present_mono (by intro _ h; cases h) h.1, hs'.present_mono (by intro _ h; cases h) h.2⟩ - | putNew ha hn hnf => - have hs' := Step.putNew (site := site) (rd := rd) (agent := agent) ha hn hnf - exact ⟨hs'.present_mono (by intro _ h; cases h) h.1, hs'.present_mono (by intro _ h; cases h) h.2⟩ - | patch ha hg hnf hkeep => - have hs' := Step.patch (site := site) (rd := rd) (agent := agent) ha hg hnf hkeep - exact ⟨hs'.present_mono (by intro _ h; cases h) h.1, hs'.present_mono (by intro _ h; cases h) h.2⟩ + {y : Node} (hy : y ≠ req.target) : st' y = st y := h.write.frame hy /-- **The invariants hold after every write.** -/ -theorem Step.inv {site rd agent st req st'} (hs : Step site rd agent st req st') (h : Inv site st) : - Inv site st' := - ⟨own_preserved hs h.own, exact_preserved hs h.exact, contained_preserved hs h.contained, - hier_preserved hs h.hier h.contained, roots_preserved hs h.roots⟩ +theorem Step.inv {site rd agent st req st'} (hs : Step site rd agent st req st') (h : Inv site.toTree st) : + Inv site.toTree st' := hs.write.inv h + +/-- **Every document stays typed with a hierarchy class.** -/ +theorem Step.typed {site rd agent st req st'} (hs : Step site rd agent st req st') (h : Typed st) : + Typed st' := hs.write.typed h + +/-- Admin documents carry hierarchy classes only. -/ +def AdminTyped (site : Site) (st : Store) : Prop := + ∀ x t, site.admin x → ownTypes st x t → hierClass t + +/-- **Admin documents stay typed with hierarchy classes only.** -/ +theorem Step.adminTyped {site rd agent st req st'} (hs : Step site rd agent st req st') + (h : AdminTyped site st) : AdminTyped site st' := by + intro x c hx ht + rcases hs.write.ownTypes ht with ht | hc + · exact h x c hx ht + · exact hc + +theorem Write.adminTyped {site : Site} {agent st req st'} (hw : Write site.toTree agent st req st') + (h : AdminTyped site st) : AdminTyped site st' := by + intro x c hx ht + rcases hw.ownTypes ht with ht | hc + · exact h x c hx ht + · exact hc end LdhAcl diff --git a/formal/acl/LdhAcl/Theorems.lean b/formal/acl/LdhAcl/Theorems.lean index 84c182ba5..37787c966 100644 --- a/formal/acl/LdhAcl/Theorems.lean +++ b/formal/acl/LdhAcl/Theorems.lean @@ -5,6 +5,8 @@ import LdhAcl.Step namespace LdhAcl +open LdhHttp + /-! ## Modes -/ /-- **`acl:Control` is inert.** It covers no mode a request requires: `allowRequest` asks only for @@ -97,7 +99,7 @@ theorem parentU_iff {st : Store} (h : OwnGraphContainment st) {d p : Node} : · rintro ⟨g, hg, hc⟩; exact ⟨d, g, hg, hc⟩ /-- Ancestors found through the union graph are on the URI-parent chain. -/ -theorem ancestor_chain {site st} (h : Inv site st) {x a : Node} (ha : ancestor st x a) : +theorem ancestor_chain {site : Site} {st} (h : Inv site.toTree st) {x a : Node} (ha : ancestor st x a) : site.chain x a := by induction ha with | step hr => @@ -110,7 +112,7 @@ theorem ancestor_chain {site st} (h : Inv site st) {x a : Node} (ha : ancestor s exact .trans ⟨hn, hp⟩ ih /-- A node the store does not have has no ancestors: nothing outside its own graph can give it any. -/ -theorem ancestor_absent {site st} (h : Inv site st) {x a : Node} (hx : ¬ present st x) : +theorem ancestor_absent {site : Site} {st} (h : Inv site.toTree st) {x a : Node} (hx : ¬ present st x) : ¬ ancestor st x a := by intro ha cases ha with @@ -119,7 +121,7 @@ theorem ancestor_absent {site st} (h : Inv site st) {x a : Node} (hx : ¬ presen exact hx ⟨g, hg⟩ /-- A present document's ancestors are exactly its URI-parent chain. -/ -theorem ancestor_iff_chain {site st} (h : Inv site st) {x a : Node} (hx : present st x) : +theorem ancestor_iff_chain {site : Site} {st} (h : Inv site.toTree st) {x a : Node} (hx : present st x) : ancestor st x a ↔ site.chain x a := by refine ⟨ancestor_chain h, fun hc => ?_⟩ induction hc with @@ -134,7 +136,7 @@ theorem ancestor_iff_chain {site st} (h : Inv site st) {x a : Node} (hx : presen /-- **Ancestry is a function of presence.** Under the invariants, what the union-graph path finds for `x` depends on nothing but whether `x` is in the store. -/ -theorem ancestor_iff {site st} (h : Inv site st) {x a : Node} : +theorem ancestor_iff {site : Site} {st} (h : Inv site.toTree st) {x a : Node} : ancestor st x a ↔ present st x ∧ site.chain x a := by by_cases hx : present st x · rw [ancestor_iff_chain h hx]; exact ⟨fun hc => ⟨hx, hc⟩, fun ⟨_, hc⟩ => hc⟩ @@ -142,7 +144,7 @@ theorem ancestor_iff {site st} (h : Inv site st) {x a : Node} : /-- **Ancestry is stable.** A write leaves the ancestors of every document that is present before and after it as they were. -/ -theorem ancestor_stable {site rd agent st req st'} (hs : Step site rd agent st req st') (h : Inv site st) +theorem ancestor_stable {site rd agent st req st'} (hs : Step site rd agent st req st') (h : Inv site.toTree st) {x a : Node} (hx : present st x) (hx' : present st' x) : ancestor st' x a ↔ ancestor st x a := by rw [ancestor_iff_chain (hs.inv h) hx', ancestor_iff_chain h hx] @@ -151,7 +153,7 @@ theorem ancestor_stable {site rd agent st req st'} (hs : Step site rd agent st r /-- **The lookup is local.** Under the invariants, everything the lookup returns for `x` is read from `x`'s own graph. -/ -theorem context_local {site st st'} (h : Inv site st) (h' : Inv site st') {x : Node} +theorem context_local {site : Site} {st st'} (h : Inv site.toTree st) (h' : Inv site.toTree st') {x : Node} (hx : st' x = st x) : context st' x = context st x := by have hp : present st' x ↔ present st x := by simp [present, hx] funext r n @@ -188,7 +190,7 @@ theorem endUser_step_preserves_acl {site rd agent st req st'} (hs : Step site rd `endUser_step_preserves_acl`, every change of access to a document other than the one written goes through a write to the admin dataspace. -/ theorem endUser_step_preserves_other_grants {site rd agent st req st'} - (hs : Step site rd agent st req st') (h : Inv site st) (hx : ¬ site.admin req.target) + (hs : Step site rd agent st req st') (h : Inv site.toTree st) (hx : ¬ site.admin req.target) {y : Node} (hy : y ≠ req.target) {agent' m} : grant site rd st' agent' m y ↔ grant site rd st agent' m y := by obtain ⟨hA, hM⟩ := endUser_step_preserves_acl hs hx @@ -197,9 +199,10 @@ theorem endUser_step_preserves_other_grants {site rd agent st req st'} /-! ## The admin role is derived -/ /-- The reader can find any authorization in a graph that contains its description, and the description -states no ownership or containment, which the store would strip or refuse. -/ +states no ownership or containment, which the store would strip or refuse, and types the document with a +hierarchy class and nothing else, as the store requires. -/ def Reader.Expressive (rd : Reader) : Prop := - ∀ d au, ∃ p : Graph, (∀ t, p t → ¬ ownership d t ∧ ¬ isContainment t) ∧ + ∀ d au, ∃ p : Graph, (∀ t, p t → ¬ ownership d t ∧ ¬ isContainment t) ∧ HierTypes d p ∧ TypedBy d p ∧ ∀ g : Graph, (∀ t, p t → g t) → rd.auths d g au /-- **acl:Write on any admin document is the admin role.** An agent the decision lets `PUT` an existing @@ -208,11 +211,12 @@ marks an admin: whoever may write the admin dataspace is one. -/ theorem admin_write_grants_anything {site rd agent st d g} (hex : rd.Expressive) (hd : site.admin d) (hg : st d = some g) (ha : allowRequest site rd st agent .put d) (au : Auth) : ∃ p st', Step site rd agent st (.put d p false) st' ∧ authIn site rd st' au := by - obtain ⟨p, hp, hread⟩ := hex d au + obtain ⟨p, hp, hty, htb, hread⟩ := hex d au let g' : Graph := fun t => - (p t ∧ ¬ ownership d t ∧ ¬ containment d t) ∨ containedIn site d t ∨ (g t ∧ ownership d t) + (p t ∧ ¬ ownership d t ∧ ¬ containment d t) ∨ containedIn site.toTree d p t ∨ (g t ∧ ownership d t) ∨ + itemTyped site.toTree d p t have hstep : Step site rd agent st (.put d p false) (st.set d (some g')) := - Step.putExisting ha hg rfl fun t ht hc => absurd hc (hp t ht).2 + ⟨ha, Write.putExisting hg rfl (fun t ht hc => absurd hc (hp t ht).2) hty fun _ => htb⟩ refine ⟨p, _, hstep, d, g', hd, by simp [Store.set], hread _ fun t ht => Or.inl ⟨ht, (hp t ht).1, ?_⟩⟩ rintro ⟨_, hc⟩; exact (hp t ht).2 hc @@ -224,10 +228,6 @@ def EndUserOnly (site : Site) (sub : Node → Node → Prop) (au : Auth) : Prop (∀ t ∈ au.accessTo, ¬ site.admin t) ∧ (∀ c ∈ au.default, ¬ site.admin c) ∧ ∀ c ∈ au.accessToClass, ∀ t, hierClass t → sub t c → False -/-- Admin documents carry hierarchy classes only. -/ -def AdminTyped (site : Site) (st : Store) : Prop := - ∀ x t, site.admin x → ownTypes st x t → hierClass t - theorem chain_admin {site : Site} {d c : Node} (h : site.chain d c) : (site.admin c ↔ site.admin d) := by induction h with | step hr => @@ -239,7 +239,7 @@ theorem chain_admin {site : Site} {d c : Node} (h : site.chain d c) : (site.admi /-- **Dataspace confinement.** An authorization scoped to the end-user dataspace covers no admin document. `make-public` and the owner-access authorization are of that kind. -/ -theorem endUserOnly_confined {site : Site} {rd : Reader} {st : Store} (h : Inv site st) (ht : AdminTyped site st) {au : Auth} +theorem endUserOnly_confined {site : Site} {rd : Reader} {st : Store} (h : Inv site.toTree st) (ht : AdminTyped site st) {au : Auth} (hau : EndUserOnly site rd.sub au) {x : Node} (hx : site.admin x) : ¬ au.covers rd.sub (context st x) := by rw [covers_context] @@ -251,7 +251,7 @@ theorem endUserOnly_confined {site : Site} {rd : Reader} {st : Store} (h : Inv s /-- **Access to the admin dataspace comes only from authorizations scoped into it.** Any request the decision allows on an admin node, including a create below an admin container, is allowed by an authorization in force that is not scoped to the end-user dataspace. -/ -theorem admin_allow_needs_admin_scope {site rd st agent isPut m x} (h : Inv site st) +theorem admin_allow_needs_admin_scope {site rd st agent isPut m x} (h : Inv site.toTree st) (ht : AdminTyped site st) (hx : site.admin x) (ha : allow site rd st agent isPut m x) : ∃ au, authIn site rd st au ∧ ¬ EndUserOnly site rd.sub au := by have viaAdmin : ∀ y, site.admin y → grant site rd st agent m y → @@ -262,8 +262,8 @@ theorem admin_allow_needs_admin_scope {site rd st agent isPut m x} (h : Inv site · exact viaAdmin x hx hg · have hnr : ¬ site.isRoot x := by rintro (rfl | rfl) - · exact hn h.roots.1 - · exact hn h.roots.2 + · exact hn (h.roots _ (Or.inl rfl)) + · exact hn (h.roots _ (Or.inr rfl)) refine viaAdmin _ ?_ hg exact (site.parent_admin x (fun e => hnr (Or.inl e)) (fun e => hnr (Or.inr e))).2 hx @@ -273,43 +273,7 @@ theorem admin_allow_needs_admin_scope {site rd st agent isPut m x} (h : Inv site that write. `lacl:OwnerAgent` membership is therefore fixed for the life of a document. -/ theorem owner_confined {site rd agent st req st'} (hs : Step site rd agent st req st') {y b : Node} (ho : owner st' y b) : - owner st y b ∨ (y = req.target ∧ st y = none ∧ agent = some b) := by - by_cases hy : y = req.target - · subst hy - cases hs with - | post _ hg => - obtain ⟨g', hg', hb⟩ := ho - simp [Store.set, Req.target] at hg' - subst hg' - rcases hb with hb | ⟨_, hno, _⟩ - · exact Or.inl ⟨_, hg, hb⟩ - · exact absurd ⟨rfl, Or.inl rfl⟩ hno - | putExisting _ hg _ => - obtain ⟨g', hg', hb⟩ := ho - simp [Store.set, Req.target] at hg' - subst hg' - rcases hb with ⟨_, hno, _⟩ | ⟨_, _, hp, _⟩ | ⟨hb, _⟩ - · exact absurd ⟨rfl, Or.inl rfl⟩ hno - · rcases hp with hp | hp <;> cases hp - · exact Or.inl ⟨_, hg, hb⟩ - | putNew _ hn => - obtain ⟨g', hg', hb⟩ := ho - simp [Store.set, Req.target] at hg' - subst hg' - rcases hb with ⟨_, hno, _⟩ | ⟨_, _, hp, _⟩ | ⟨a, ha, _, _, hab⟩ - · exact absurd ⟨rfl, Or.inl rfl⟩ hno - · rcases hp with hp | hp <;> cases hp - · simp at hab; subst hab - exact Or.inr ⟨rfl, hn, ha⟩ - | patch _ hg _ hkeep => - obtain ⟨g', hg', hb⟩ := ho - simp [Store.set, Req.target] at hg' - subst hg' - exact Or.inl ⟨_, hg, (hkeep _ (Or.inl ⟨rfl, Or.inl rfl⟩)).1 hb⟩ - | delete => - obtain ⟨g', hg', _⟩ := ho - simp [Store.set, Req.target] at hg' - · obtain ⟨g, hg, hb⟩ := ho - exact Or.inl ⟨g, by rw [← hs.frame hy]; exact hg, hb⟩ + owner st y b ∨ (y = req.target ∧ st y = none ∧ agent = some b) := + hs.write.owner_confined ho end LdhAcl diff --git a/formal/acl/Main.lean b/formal/acl/Main.lean index dd796103f..ae5e1b768 100644 --- a/formal/acl/Main.lean +++ b/formal/acl/Main.lean @@ -1,101 +1,37 @@ /- -`ldh-acl`: the decision of `LdhAcl.Decide` over a live instance's datasets. +`ldh-acl`: the decision of `LdhAcl.Decide`, and the server's answer of `LdhAcl.Gate` (the decision, then the +graph store's answer of `LdhHttp.Answer`), over a live instance's datasets. ldh-acl --end-user END_USER.nq --admin ADMIN.nq --admin-base https://admin.example.org/ --probes PROBES.tsv + ldh-acl --end-user END_USER.nq --admin ADMIN.nq --admin-base https://admin.example.org/ --request REQUEST.tsv + [--payload PAYLOAD.nt | --delete DELETE.nt --insert INSERT.nt] [--fixed URI]... The datasets are N-Quads dumps of the two stores. Each probe line is `AGENTMETHODDOCUMENT`, where `AGENT` is a WebID or `-` for no agent and `METHOD` is `GET`, `HEAD`, `POST`, `PUT`, `PUT*` (a `PUT` with `If-None-Match: *`), `PATCH` or `DELETE`. For every probe, one line comes back: `allow` or `deny`, then the probe. -What this file adds to the proven decision is unproven and small: the N-Quads reader, the interning of IRIs as -nodes, the reading of authorizations, memberships and subclass axioms out of the admin dataset (transcribed from -`aclQuery` in `web.xml`), and the URI parent a `PUT` of a new document is decided on. +A request is one line, `AGENTMETHODDOCUMENTPRECONDITION`, with `METHOD` one of `GET`, `HEAD`, `POST`, +`PUT`, `PATCH` and `DELETE`, and `PRECONDITION` one of `none`, `current` (`If-Match` with the current entity tag), +`stale` (`If-Match` with another) and `absent` (`If-None-Match: *`). The body of a `POST` or `PUT` is the +`--payload` 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. + +What this file adds to the proven model is unproven and small: the reading of authorizations, memberships and +subclass axioms out of the admin dataset (transcribed from `aclQuery` in `web.xml`). Reading the dumps and the +request is `LdhHttp.IO`'s. -/ import LdhAcl +import LdhHttp.IO import Std.Data.HashMap -open LdhAcl Std - -instance : Hashable Node where - hash - | .rdfType => 1 | .aclOwner => 2 | .dctCreator => 3 | .siocHasParent => 4 | .siocHasContainer => 5 - | .nfoFileDataObject => 6 | .dhContainer => 7 | .dhItem => 8 | .defRoot => 9 - | .iri n => hash (n + 16) - -/-! ## Terms and quads -/ - -inductive Term where - | iri (s : String) - | blank (s : String) - | literal - deriving Repr, BEq - -structure Quad where - s : Term - p : Term - o : Term - g : Term - -/-- The name a node is interned under: an IRI, or a blank node label, which cannot collide with an IRI. -/ -def Term.key : Term → Option String - | .iri s => some s - | .blank s => some s - | .literal => none - -/-! ## N-Quads -/ - -/-- One term from the front of `s`; the rest after it. Literals keep nothing but their kind. -/ -partial def parseTerm (s : Substring) : Option (Term × Substring) := - let s := s.trimLeft - if s.isEmpty then none - else match s.front with - | '<' => - let body := (s.drop 1).takeWhile (· ≠ '>') - let rest := (s.drop 1).dropWhile (· ≠ '>') - if rest.isEmpty then none else some (.iri body.toString, rest.drop 1) - | '_' => - let body := s.takeWhile fun c => !c.isWhitespace - some (.blank body.toString, s.drop body.bsize) - | '"' => - -- the closing quote is the first one not escaped - let rec close (t : Substring) (escaped : Bool) : Substring := - if t.isEmpty then t - else - let c := t.front - if escaped then close (t.drop 1) false - else if c == '\\' then close (t.drop 1) true - else if c == '"' then t.drop 1 - else close (t.drop 1) false - let after := close (s.drop 1) false - -- a language tag or a datatype follows without a space - let after := after.dropWhile fun c => !c.isWhitespace - some (.literal, after) - | _ => none - -def parseQuad (line : String) : Option Quad := do - let (s, r) ← parseTerm line.toSubstring - let (p, r) ← parseTerm r - let (o, r) ← parseTerm r - let (g, _) ← parseTerm r - pure ⟨s, p, o, g⟩ +open LdhHttp LdhAcl Std -def readQuads (path : System.FilePath) : IO (Array Quad) := do - let lines ← IO.FS.lines path - let mut quads := #[] - for line in lines do - let t := line.trim - if t.isEmpty || t.startsWith "#" then continue - match parseQuad t with - | some q => quads := quads.push q - | none => throw (IO.userError s!"cannot read N-Quads line: {line}") - pure quads /-! ## Vocabulary -/ namespace V -def rdfType := "http://www.w3.org/1999/02/22-rdf-syntax-ns#type" def rdfsSubClassOf := "http://www.w3.org/2000/01/rdf-schema#subClassOf" -def aclOwner := "http://www.w3.org/ns/auth/acl#owner" def aclAgent := "http://www.w3.org/ns/auth/acl#agent" def aclAgentGroup := "http://www.w3.org/ns/auth/acl#agentGroup" def aclAgentClass := "http://www.w3.org/ns/auth/acl#agentClass" @@ -112,65 +48,8 @@ def foafAgent := "http://xmlns.com/foaf/0.1/Agent" def foafPrimaryTopic := "http://xmlns.com/foaf/0.1/primaryTopic" def foafMember := "http://xmlns.com/foaf/0.1/member" def laclOwnerAgent := "https://w3id.org/atomgraph/linkeddatahub/admin/acl#OwnerAgent" -def dctCreator := "http://purl.org/dc/terms/creator" -def siocHasParent := "http://rdfs.org/sioc/ns#has_parent" -def siocHasContainer := "http://rdfs.org/sioc/ns#has_container" -def nfoFileDataObject := "http://www.semanticdesktop.org/ontologies/2007/03/22/nfo#FileDataObject" -def dhContainer := "https://w3id.org/atomgraph/linkeddatahub/document-hierarchy#Container" -def dhItem := "https://w3id.org/atomgraph/linkeddatahub/document-hierarchy#Item" -def defRoot := "https://w3id.org/atomgraph/linkeddatahub/default#Root" end V -/-- The terms the decision reads are constructors of `Node`; every other one is interned. -/ -def vocabulary : List (String × Node) := - [(V.rdfType, .rdfType), (V.aclOwner, .aclOwner), (V.dctCreator, .dctCreator), (V.siocHasParent, .siocHasParent), - (V.siocHasContainer, .siocHasContainer), (V.nfoFileDataObject, .nfoFileDataObject), - (V.dhContainer, .dhContainer), (V.dhItem, .dhItem), (V.defRoot, .defRoot)] - -structure Interner where - nodes : HashMap String Node := vocabulary.foldl (fun m (k, n) => m.insert k n) {} - next : Nat := 0 - -def Interner.intern (i : Interner) (key : String) : Node × Interner := - match i.nodes[key]? with - | some n => (n, i) - | none => (.iri i.next, { nodes := i.nodes.insert key (.iri i.next), next := i.next + 1 }) - -/-- Interns a batch of keys, in order. -/ -def Interner.internAll (i : Interner) (keys : List String) : List Node × Interner := - keys.foldr (fun k (ns, i) => let (n, i) := i.intern k; (n :: ns, i)) ([], i) - -/-! ## Reading the stores -/ - -/-- A quad whose three positions are nodes, as a triple under its graph name; a literal object drops the quad, -since the decision reads none. -/ -def Quad.keys (q : Quad) : Option (String × String × String × String) := do - let s ← q.s.key - let p ← q.p.key - let o ← q.o.key - let g ← q.g.key - pure (s, p, o, g) - -def internQuads (i : Interner) (quads : Array Quad) : Array (Node × Triple) × Interner := Id.run do - let mut i := i - let mut out := #[] - for q in quads do - if let some (s, p, o, g) := q.keys then - let (ns, i1) := i.intern s - let (np, i2) := i1.intern p - let (no, i3) := i2.intern o - let (ng, i4) := i3.intern g - i := i4 - out := out.push (ng, ⟨ns, np, no⟩) - pure (out, i) - -/-- Groups interned quads by graph. -/ -def toFinStore (quads : Array (Node × Triple)) : FinStore := Id.run do - let mut m : HashMap Node (List Triple) := {} - for (g, t) in quads do - m := m.insert g (t :: m.getD g []) - pure (m.toList) - /-! ## Reading the admin dataset: `aclQuery` -/ /-- The quads of one graph, by subject. -/ @@ -243,26 +122,6 @@ def readAdmin (i : Interner) (quads : Array Quad) (adminBase : String) : FinAdmi sub := (ns, no) :: sub pure (⟨auths, members, sub⟩, i) -/-! ## The site -/ - -/-- The URI parent `put()` resolves: `..` against the document URI, by RFC 3986. The base's last segment goes -first, so a URI with a trailing slash (every document the graph store has) climbs one level, and one without -climbs two: `/a/b/` and `/a/b/c` both give `/a/`. The root of a tree is its own parent. -/ -def parentIri (s : String) : String := - -- no path at all: nothing to climb - if !(((s.splitOn "://").getD 1 "").contains '/') then s else - -- the directory of the URI: up to and including its last slash - let dir := match s.revPosOf '/' with - | some pos => s.extract 0 (s.next pos) - | none => s - let core := dir.dropRight 1 - match core.revPosOf '/' with - | none => s - | some pos => - let before := core.extract 0 pos - -- the slash found belongs to the scheme's `//`: the URI has no path above it - if before.endsWith "/" || before.endsWith ":" then dir else core.extract 0 (core.next pos) - /-! ## Probes -/ structure Probe where @@ -295,27 +154,60 @@ structure Args where admin : Option String := none adminBase : Option String := none probes : Option String := none + request : Option RequestFiles := none -def parseArgs : List String → Args → Except String Args +partial def parseArgs : List String → Args → Except String Args | [], a => .ok a | "--end-user" :: v :: rest, a => parseArgs rest { a with endUser := some v } | "--admin" :: v :: rest, a => parseArgs rest { a with admin := some v } | "--admin-base" :: v :: rest, a => parseArgs rest { a with adminBase := some v } | "--probes" :: v :: rest, a => parseArgs rest { a with probes := some v } - | arg :: _, _ => .error s!"unknown argument: {arg}" + | "--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 + | some (rest, f) => parseArgs rest { a with request := some f } + | none => .error s!"unknown argument: {arg}" def usage : String := - "usage: ldh-acl --end-user END_USER.nq --admin ADMIN.nq --admin-base ADMIN_BASE_URI --probes PROBES.tsv" + "usage: ldh-acl --end-user END_USER.nq --admin ADMIN.nq --admin-base ADMIN_BASE_URI " ++ + "(--probes PROBES.tsv | --request REQUEST.tsv [--payload PAYLOAD.nt | --delete DELETE.nt --insert INSERT.nt] " ++ + "[--fixed URI]...)" + +/-- The admin dataspace is the graphs under the admin base: aclQuery's FILTER, and the dataspace a URI belongs to. -/ +def adminNodes (i : Interner) (adminBase : String) : HashMap Node Unit := Id.run do + let mut m : HashMap Node Unit := {} + for (k, n) in i.nodes.toList do + if k.startsWith adminBase then m := m.insert n () + pure m + +/-- One request, decided and answered: its status, then the document's graph after it. -/ +def runRequest (files : RequestFiles) (endUserQuads adminQuads : Array Quad) (adminBase : String) : IO UInt32 := do + let i : Interner := {} + let (euTriples, i) := internQuads i endUserQuads + let (adTriples, i) := internQuads i adminQuads + let (fa, i) := readAdmin i adminQuads adminBase + let r ← match ← loadRequest i files with + | .ok r => pure r + | .error e => IO.eprintln e; return 2 + let admins := adminNodes r.interner adminBase + let fsite : FinSite := { r.hs with admin := fun d => admins.contains d } + let fs : FinStore := toFinStore (euTriples ++ adTriples) + let (status, fs') := serveB fsite fs fa r.agent r.pc r.req + printAnswer r.interner status fs' r.req.target + 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 - let (some endUserPath, some adminPath, some adminBase, some probesPath) := - (args.endUser, args.admin, args.adminBase, args.probes) + let (some endUserPath, some adminPath, some adminBase) := (args.endUser, args.admin, args.adminBase) | IO.eprintln usage; return 2 let endUserQuads ← readQuads endUserPath let adminQuads ← readQuads adminPath + if let some files := args.request then + return ← runRequest files endUserQuads adminQuads adminBase + let some probesPath := args.probes + | IO.eprintln usage; return 2 let probeLines ← IO.FS.lines probesPath let mut probes : Array Probe := #[] for line in probeLines do @@ -341,13 +233,11 @@ def main (argv : List String) : IO UInt32 := do parents := parents.insert target parent decoded := decoded.push (agent, p.method, target, p.line) let fs : FinStore := toFinStore (euTriples ++ adTriples) - -- the admin dataspace is the graphs under the admin base: aclQuery's FILTER, and the dataspace a URI belongs to - let adminNodes : HashMap Node Unit := Id.run do - let mut m : HashMap Node Unit := {} - for (k, n) in i.nodes.toList do - if k.startsWith adminBase then m := m.insert n () - pure m - let fsite : FinSite := { parent := fun d => parents.getD d d, admin := fun d => adminNodes.contains d } + let admins := adminNodes i adminBase + -- the decision reads the URI parent and the dataspace alone + let fsite : FinSite := { + parent := fun d => parents.getD d d, isRoot := fun _ => false, slashed := fun _ => true, + doubleSlash := fun _ => false, fixed := fun _ => false, admin := fun d => admins.contains d } for (agent, method, target, line) in decoded do let verdict := if allowRequestB fsite fs fa agent method target then "allow" else "deny" IO.println s!"{verdict}\t{line}" diff --git a/formal/acl/README.md b/formal/acl/README.md index 05a5979eb..293179ed7 100644 --- a/formal/acl/README.md +++ b/formal/acl/README.md @@ -1,7 +1,9 @@ # LinkedDataHub ACL model in Lean -A Lean 4 model of LinkedDataHub's authorization decision and of the graph store writes that change what -the decision reads, with proofs of the properties the access-control model is meant to have. +A Lean 4 model of LinkedDataHub's authorization decision, and of the server's answer with the decision in front of +the graph store, with proofs of the properties the access-control model is meant to have. It builds on the graph +store model in [`../http/`](../http/): the store the decision reads, the writes that change it and the graph +store's answer are that model's, which this one requires by path. The model is a specification. It is not extracted from the Java, and nothing here checks the Java against it: each definition is transcribed from the code listed in the mapping below. When that code @@ -16,10 +18,10 @@ lake build Lean `v4.15.0` (pinned in `lean-toolchain`), core library only, with no Mathlib. -The `Formal` workflow builds the model on every push, fails on a `sorry`, and on a pull request runs -`tracks-code.sh`, which fails when a source listed under "Mapping to the code" changes without a change -in this directory. `web.xml` counts only through the three queries the mapping names; the rest of the -file is free to change. Run it locally against the branch point: +`lake build` builds the graph store model first. The `Formal` workflow builds both on every push, fails on a +`sorry`, and on a pull request runs each model's `tracks-code.sh`, which fails when a source listed under "Mapping to +the code" changes without a change in that model's directory. Here `web.xml` counts only through the two queries +the mapping names; the rest of the file is free to change. Run it locally against the branch point: ```bash formal/acl/tracks-code.sh origin/develop @@ -29,13 +31,13 @@ formal/acl/tracks-code.sh origin/develop | File | Contents | |------|----------| -| `LdhAcl/Base.lean` | The store (one named graph per document), modes, own-graph lookups and requests | -| `LdhAcl/Model.lean` | The two dataspaces, ancestry, the admin dataset, the document context and the decision | -| `LdhAcl/Step.lean` | Graph store writes as a step relation, and the invariants they keep | +| `LdhAcl/Model.lean` | Modes, the two dataspaces, ancestry, the admin dataset, the document context and the decision | +| `LdhAcl/Step.lean` | An authorized write: a request the decision allows, and the graph store's `Write` of it | | `LdhAcl/Theorems.lean` | What the decision guarantees | | `LdhAcl/Migration.lean` | The seeded authorizations, and what migrating those of a release before 6.0 changes | | `LdhAcl/Decide.lean` | The decision as a program over finite data, and the proof that it agrees with `allowRequest` | -| `Main.lean` | `ldh-acl`: that program over a live instance's datasets, for `tests/http/formal/` to replay against the server | +| `LdhAcl/Gate.lean` | The server's answer: the decision, then the graph store's answer, and what holds of the two together | +| `Main.lean` | `ldh-acl`: the decision and the server's answer over a live instance's datasets, for `tests/http/formal/` to replay against the server | ## The model @@ -54,8 +56,12 @@ formal/acl/tracks-code.sh origin/develop - **Where each triple is read from:** - types, ancestry and the owner come from the document's own graph; - authorizations and memberships come from the admin document they are the primary topic of. -- **The write rule:** a graph written for `x` may state `sioc:has_parent` or `sioc:has_container` of `x` only. - Under it, a containment path over `urn:x-arq:UnionGraph` finds exactly the own-graph ancestry. +- **The graph store's rules** are the graph store model's: under its write rule, a containment path over + `urn:x-arq:UnionGraph` finds exactly the own-graph ancestry, and under its type rule a class grant reaches a + document only through a hierarchy class. +- **A step (`Step`)** is a request the decision allows, and the graph store's `Write` of it. +- **The server's answer (`Gate.lean`):** the decision, and a request it denies is answered `403` before any of the + graph store's checks; then the graph store's answer. ## Mapping to the code @@ -68,18 +74,16 @@ formal/acl/tracks-code.sh origin/develop | `Reader`, `authIn`, `memberIn` | `aclQuery`'s `?g foaf:primaryTopic ?auth` and `?groupG foaf:primaryTopic ?Group` | | `grant`, `allow` | `AuthorizationFilter.authorize`, including the `PUT` fallback to the parent | | `allowRequest` | `AuthorizationFilter.filter`, `getAccessMode` | -| `Step.post`, `Step.putExisting`, `Step.putNew`, `Step.patch`, `Step.delete` | `DocumentHierarchyGraphStoreImpl.post`, `put`, `patch`, `delete` | -| `NoForeign` | `getForeignContainment`, `checkForeignContainment` | -| `ownership`, `containment` | `removeOwnership`, `isOwnershipChanged`, `removeContainment`, `isContainmentChanged` | -| `hasChild` | `childQuery` (`web.xml`), `hasChild` | | `EndUserOnly` (class part) | the `adm:HierarchyClassAccess` constraint on `acl:Authorization` (`app/admin/adm.ttl`) | | `ownerAccess` | `acl/authorizations/owner-access/` (`platform/namespace-ontology.trig.template`) | | `Auth.withTargets` rewrites | `migrations/6.0-acl.ru.template` | +| `Site.toTree` | the hierarchy the graph store keeps for both dataspaces: the URI parent and the two roots | | `readAdmin` (`Main.lean`) | `aclQuery`'s `?g foaf:primaryTopic ?auth`, `?groupG foaf:primaryTopic ?Group . ?Group foaf:member $agent` and `rdfs:subClassOf*` branches, with its `strstarts($base)` filters | -| `parentIri` (`Main.lean`) | `IRIx.resolve("..")` in `AuthorizationFilter.authorize` | +| `parentIri` (`LdhHttp.IO`) | `IRIx.resolve("..")` in `AuthorizationFilter.authorize` | +| `decideB`, `Refusal.forbidden` | `AuthorizationFilter.filter`, and `AuthorizationExceptionMapper` (`server/mapper/auth/`), which answers every denial `403` | +| `HReq.method` (`LdhHttp.Answer`) | `getAccessMode`: a `PUT` with `If-None-Match: *` requires acl:Append | -`AuthorizationFilter` lives in `server/filter/request/` and `DocumentHierarchyGraphStoreImpl` in -`server/model/impl/`, both under `src/main/java/com/atomgraph/linkeddatahub/`. +`AuthorizationFilter` lives in `server/filter/request/`, under `src/main/java/com/atomgraph/linkeddatahub/`. ## Results @@ -92,14 +96,15 @@ Proven with no `sorry`, using only the axioms `propext`, `Quot.sound` and, throu | `grantWith_mono` | More authorizations or memberships never take access away | | `covers_context` | Matching the lookup's rows is WAC: named, below a default container, or of a granted class | | `untagged_fails_open` | An untagged `VALUES (?Type ?Ancestor)` table would match a default grant on a document not below its container | -| `Step.inv` | The containment rule, exact containment, the hierarchy and the roots hold after every write | +| `Step.inv`, `Step.typed` | The graph store's invariants hold after every authorized write, as they do after every `Write` | +| `Step.adminTyped` | After every write, admin documents are still typed with hierarchy classes only | | `parentU_iff`, `ancestor_iff` | Under the rule, union-graph ancestry is own-graph ancestry: the URI-parent chain of a present document | | `ancestor_stable` | A write never changes the ancestors of a document present before and after it | | `context_local` | The lookup for `x` reads only `x`'s own graph | | `endUser_step_preserves_acl`, `endUser_step_preserves_other_grants` | A write to an end-user document changes no authorization, no membership and no decision about any other document | | `admin_write_grants_anything` | acl:Write on an admin document can put any authorization in force: the admin role is whoever may write the admin dataspace | | `endUserOnly_confined`, `admin_allow_needs_admin_scope` | An authorization scoped to the end-user dataspace covers no admin document; every allowed request on an admin node comes from one that is not | -| `owner_confined` | `lacl:OwnerAgent` membership is fixed for the life of a document | +| `owner_confined` | `lacl:OwnerAgent` membership is fixed for the life of a document, by the graph store's `Write.owner_confined` | | `admin_role_covers` | `accessTo` and `acl:default` on the admin root cover every admin document | | `migrate_endUser` | On the end-user dataspace, a class grant on the hierarchy classes and a default grant on the root cover the same documents | | `migrate_admin` | On the admin dataspace, the class grant covers every document and the default grant on the end-user root none | @@ -107,38 +112,66 @@ Proven with no `sorry`, using only the axioms `propext`, `Quot.sound` and, throu | `ownerAccess_admin` | Owner access opens nothing in the admin dataspace, where the owner grant before 6.0 applied too | | `Anc_iff_reachB` | Reachability over an edge list with each edge used once is the transitive closure, with fuel the number of edges | | `allowRequest_iff` | `allowRequestB`, a `Bool` over a finite store and admin dataset, is `allowRequest` on the store and reader they denote | +| `decide_forbidden_iff` | The server answers `403` exactly when the decision denies the request: a denied agent learns nothing a later check would say, not even whether the document exists | +| `serve_refused` | A refused request leaves the store as it was | +| `decide_step` | A request that goes through is a `Step`, an authorized `Write`, from the store before it to the store after it, or changes nothing | +| `decide_inv` | So the server keeps `Inv`, `AdminTyped` and `Typed`, as every `Step` does | -## Replaying the decision against the server +## Replaying the model against the server `allowRequest` is a proposition; `Decide.lean` gives the same decision as a program over finite data (`FinStore`, `FinAdmin`, `FinSite`) and proves them equal (`allowRequest_iff`), for every `Site` whose `parent` and `admin` the -program's agree with. `Main.lean` runs that program on N-Quads dumps of the two stores: +program's agree with. `Gate.lean` puts it in front of the graph store's answer (`LdhHttp.answerB`), a program from +the start: `decideB` gives a request's status and the store after it, and `decide_step` proves that whatever it +writes is a `Step`. `Main.lean` runs both on N-Quads dumps of the two stores: ```bash lake build .lake/build/bin/ldh-acl --end-user end-user.nq --admin admin.nq --admin-base https://admin.localhost:4443/ --probes probes.tsv +.lake/build/bin/ldh-acl --end-user end-user.nq --admin admin.nq --admin-base https://admin.localhost:4443/ \ + --request request.tsv --payload payload.nt ``` Each probe line is `AGENTMETHODDOCUMENT` (`-` for no agent; `PUT*` is a `PUT` with `If-None-Match: *`), and -each answer `allow` or `deny`. The part outside the proof is small and transcribed from `aclQuery`: the N-Quads -reader, the interning of IRIs as nodes, the reading of authorizations (every `foaf:primaryTopic` of an admin graph -under the admin base, with its `acl:` properties from that graph), memberships (`foaf:member` of such a topic) and -`rdfs:subClassOf` from the admin dataset, and the URI parent a `PUT` of a new document is decided on. +each answer `allow` or `deny`. A request is `AGENTMETHODDOCUMENTPRECONDITION`, with the precondition +`none`, `current` or `stale` (`If-Match` with the current entity tag or another) or `absent` (`If-None-Match: *`); the +body of a `POST` or `PUT` is `--payload`, and a `PATCH` is `DELETE { --delete } INSERT { --insert } WHERE {}`. The +answer is the status, then the document's graph after the request. + +The part outside the proofs is small and transcribed: the reading of authorizations (every `foaf:primaryTopic` of an +admin graph under the admin base, with its `acl:` properties from that graph), memberships (`foaf:member` of such a +topic) and `rdfs:subClassOf` from the admin dataset. Reading the dumps and the request is `LdhHttp.IO`'s. `tests/http/formal/acl-conformance.sh` drives it: a seeded random scenario of documents, groups and authorizations -is built through the API, and before every request the stores are dumped and the server's status compared with -the verdict, 401 or 403 on `deny` and anything else on `allow`. The scenario's own writes are requests the model +is built through the API, and before every request the stores are dumped and the request handed to `ldh-acl`. The +server has to return the predicted status, and the document's graph after the request has to be the predicted one, +but for the `dct:created` and `dct:modified` the server stamps. The requests carry random preconditions, and +payloads some of which the write and type rules refuse or strip. The scenario's own writes are requests the model decides, so the agents' rights shape what gets built. `ACL_CONFORMANCE_SEED` replays a scenario, and a mismatch -leaves its dumps and probe under the results directory. +leaves its dumps, request and payloads under the results directory. ## What the proofs need of the data -These are hypotheses of the theorems, which the implementation has to enforce: +Two hypotheses of the theorems are about the stored data, which a write could falsify. The type rule enforces both, +the model proves that every write keeps them, and an HTTP test tries each write that would break them: + +- **`AdminTyped`:** admin documents carry hierarchy classes only (`Step.adminTyped`, from the graph store's + `Write.ownTypes`). Together with + `EndUserOnly`, it requires the store to refuse `acl:accessToClass` of any class a hierarchy class is a + subclass of. `adm:HierarchyClassAccess` refuses the hierarchy classes and the superclasses the platform's + vocabularies declare for them; a superclass a namespace ontology declares is admin data, written by the + admin role (see `rdfs:subClassOf*` below). Tested by `tests/http/admin/acl/class-authorization-admin-typed.sh`. +- **`Typed`:** every document is typed with a hierarchy class (`Write.typed`, in the graph store model). It is needed only for + `migrate_endUser`. Tested by `tests/http/document-hierarchy/{PUT,POST,PATCH}-foreign-type-422.sh`. + +Every seeded document satisfies both. The admin dataset also seeds graphs for two endpoints, `clear` and `sign up`, +typed `foaf:Document`, with no containment. They are not documents: `Dispatcher` routes them to their own resources, +so no graph store write reaches them, and `adm:HierarchyClassAccess` refuses a grant of `foaf:Document`. A store +written before the type rule may hold documents typed otherwise: a `PATCH` leaves the types it finds, and the first +`PUT` drops them. + +The other two are facts about the platform rather than its data, and nothing a request sends can falsify them: -- **`AdminTyped`:** admin documents carry hierarchy classes only. Together with `EndUserOnly`, it - requires the store to refuse `acl:accessToClass` of any class a hierarchy class is a subclass of, which - includes the hierarchy classes themselves and any superclass the ontology declares for them. -- **`Typed`:** every document is typed with a hierarchy class. It is needed only for `migrate_endUser`. - **`Site.Finite`:** every parent chain ends at a root, as URI paths do. - **`Reader.Expressive`:** an authorization can be described in an admin document's graph. It is needed only to show that write access to the admin dataspace is the admin role. @@ -148,9 +181,5 @@ These are hypotheses of the theorems, which the implementation has to enforce: - **`rdfs:subClassOf*`:** fixed. Class axioms are admin data, and a write to them is an admin write. - **The read-allowed dataspace shortcut:** a dataspace marked readable skips the decision for `GET` and `HEAD`. - **Authentication:** WebID, OAuth and `On-Behalf-Of` delegation. The agent is an input. -- **Concurrency:** steps are sequential. Under the locks, a `PUT` holds its parent's lock as well as its own and - re-checks that the parent exists, and a `DELETE` checks for children; the model does not prove that - serialisation. -- **Other server work:** validation, skolemization, dates, imports, uploads, content negotiation and caching. - A write refused for its body, such as one with a malformed IRI answered with `422`, changes nothing, and the - model has no step for it. +- **What the graph store model leaves out:** concurrency, validation and the rest of the server's work; see its + README. diff --git a/formal/acl/lake-manifest.json b/formal/acl/lake-manifest.json index 06eefe971..da4983def 100644 --- a/formal/acl/lake-manifest.json +++ b/formal/acl/lake-manifest.json @@ -1,5 +1,12 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", - "packages": [], + "packages": + [{"type": "path", + "scope": "", + "name": "LdhHttp", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "./../http", + "configFile": "lakefile.lean"}], "name": "LdhAcl", "lakeDir": ".lake"} diff --git a/formal/acl/lakefile.lean b/formal/acl/lakefile.lean index 73545fc85..db7c93bc5 100644 --- a/formal/acl/lakefile.lean +++ b/formal/acl/lakefile.lean @@ -6,10 +6,13 @@ package LdhAcl where -- ("missing SG_READ_ONLY flag"); not creating the segment sidesteps it. GNU ld knows no such flag moreLinkArgs := if System.Platform.isOSX then #["-Wl,-no_data_const"] else #[] +/-- The graph store: the authorization decision is modelled over its data and its writes. -/ +require LdhHttp from "../http" + @[default_target] lean_lib LdhAcl -/-- The decision over a live instance's datasets: see `Main.lean`. -/ +/-- The decision, and the server's answer behind it, over a live instance's datasets: see `Main.lean`. -/ @[default_target] lean_exe «ldh-acl» where root := `Main diff --git a/formal/acl/tracks-code.sh b/formal/acl/tracks-code.sh index a46468e7b..ef81a1863 100755 --- a/formal/acl/tracks-code.sh +++ b/formal/acl/tracks-code.sh @@ -21,13 +21,13 @@ sources=( src/main/java/com/atomgraph/linkeddatahub/server/util/DocumentContext.java src/main/java/com/atomgraph/linkeddatahub/server/util/AuthorizationParams.java src/main/java/com/atomgraph/linkeddatahub/server/filter/request/AuthorizationFilter.java - src/main/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImpl.java + src/main/java/com/atomgraph/linkeddatahub/server/mapper/auth/AuthorizationExceptionMapper.java src/main/resources/com/atomgraph/linkeddatahub/app/admin/adm.ttl platform/namespace-ontology.trig.template migrations/6.0-acl.ru.template ) # web.xml is transcribed query by query: only these context params count -queries=(documentContextQuery aclQuery childQuery) +queries=(documentContextQuery aclQuery) changed=() while IFS= read -r file; do diff --git a/formal/http/.gitignore b/formal/http/.gitignore new file mode 100644 index 000000000..01f8cdb63 --- /dev/null +++ b/formal/http/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/formal/http/LdhHttp.lean b/formal/http/LdhHttp.lean new file mode 100644 index 000000000..01eb6ba3c --- /dev/null +++ b/formal/http/LdhHttp.lean @@ -0,0 +1,7 @@ +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/Answer.lean b/formal/http/LdhHttp/Answer.lean new file mode 100644 index 000000000..bc029b499 --- /dev/null +++ b/formal/http/LdhHttp/Answer.lean @@ -0,0 +1,545 @@ +/- +The graph store's answer to a request, as a program over finite data: the status, and the store after it. + +Everything `DocumentHierarchyGraphStoreImpl` does with a request, in the order it checks it: the methods a document +allows, the URI checks, the write and type rules, the preconditions, existence, the parent and the children. Who is +asking is no part of it, beyond the agent a new document is owned by: the authorization decision comes before all of +it, and lives in the ACL model. A refused request changes nothing (`respond_refused`), no check here answers `403` +(`answer_not_forbidden`), and a request that goes through is a `Write` (`answer_write`), so the graph store keeps +every invariant a `Write` does (`answer_inv`). + +The payload is ground: no blank nodes, which the server skolemizes, and no `dct:created` or `dct:modified`, which it +replaces. Constraint validation (SPIN and SHACL, `422`), parsing (`400`, `415`) and content negotiation are not +modelled: the replay sends only valid, parseable payloads that satisfy the ontology's constraints. +-/ +import LdhHttp.Fin + +namespace LdhHttp + +/-! ## Requests and responses -/ + +/-- The precondition a request carries. -/ +inductive Precond where + /-- Neither `If-Match` nor `If-None-Match`. -/ + | none + /-- `If-Match` with the document's current entity tag. -/ + | current + /-- `If-Match` with any other entity tag. -/ + | stale + /-- `If-None-Match: *`: create, only if there is nothing. -/ + | absent + deriving DecidableEq, Repr + +/-- A graph store request. A `PATCH` is `DELETE { delete } INSERT { insert } WHERE {}` over ground triples. -/ +inductive HReq where + | get (x : Node) + | head (x : Node) + | post (x : Node) (payload : List Triple) + | put (x : Node) (payload : List Triple) + | patch (x : Node) (delete insert : List Triple) + | delete (x : Node) + +def HReq.target : HReq → Node + | .get x | .head x | .post x _ | .put x _ | .patch x _ _ | .delete x => x + +/-- The method the decision is asked about: `getAccessMode` requires acl:Append of a `PUT` with `If-None-Match: *`. -/ +def HReq.method (pc : Precond) : HReq → Method + | .get _ => .get + | .head _ => .head + | .post .. => .post + | .put .. => if pc = .absent then .putCreate else .put + | .patch .. => .patch + | .delete _ => .delete + +/-- The statuses of a request that goes through. -/ +inductive Success where + | ok | created | noContent + deriving DecidableEq, Repr + +/-- The statuses of a request that does not. -/ +inductive Refusal where + | permanentRedirect | badRequest | forbidden | notFound | methodNotAllowed | conflict + | preconditionFailed | unprocessable | preconditionRequired + deriving DecidableEq, Repr + +def Success.code : Success → Nat + | .ok => 200 | .created => 201 | .noContent => 204 + +def Refusal.code : Refusal → Nat + | .permanentRedirect => 308 | .badRequest => 400 | .forbidden => 403 | .notFound => 404 + | .methodNotAllowed => 405 | .conflict => 409 | .preconditionFailed => 412 | .unprocessable => 422 + | .preconditionRequired => 428 + +/-- The deployment constants the graph store reads. -/ +structure HSite where + /-- The URI parent `put()` resolves. -/ + parent : Node → Node + isRoot : Node → Bool + /-- The URI ends with a slash; `put()` redirects one that does not. -/ + slashed : Node → Bool + /-- The URI's path has a double slash, which `put()` refuses. -/ + doubleSlash : Node → Bool + /-- The owner's or the secretary's WebID document, which can be neither replaced nor deleted. -/ + fixed : Node → Bool + +def HSite.agrees (hs : HSite) (tr : Tree) : Prop := + (∀ d, tr.parent d = hs.parent d) ∧ ∀ d, hs.isRoot d = true ↔ tr.isRoot d + +/-! ## The rules, computed -/ + +def ownershipB (x : Node) (t : Triple) : Bool := t.s == x && (t.p == .aclOwner || t.p == .dctCreator) + +def containmentB (x : Node) (t : Triple) : Bool := t.s == x && (t.p == .siocHasParent || t.p == .siocHasContainer) + +def isContainmentB (t : Triple) : Bool := t.p == .siocHasParent || t.p == .siocHasContainer + +def hierClassB (c : Node) : Bool := c == .defRoot || c == .dhContainer || c == .dhItem + +/-- What a write keeps of a payload: `removeOwnership` and `removeContainment` strip the rest. -/ +def keepB (x : Node) (t : Triple) : Bool := !ownershipB x t && !containmentB x t + +/-- `checkForeignContainment` refuses the payload. -/ +def foreignContainmentB (x : Node) (ts : List Triple) : Bool := ts.any fun t => isContainmentB t && t.s != x + +/-- `checkDocumentTypes` refuses the payload. -/ +def foreignTypeB (x : Node) (ts : List Triple) : Bool := + ts.any fun t => t.s == x && t.p == .rdfType && !hierClassB t.o + +/-- `isHierarchyTyped`. -/ +def typedB (x : Node) (ts : List Triple) : Bool := ts.any fun t => t.s == x && t.p == .rdfType && hierClassB t.o + +/-- `childQuery`: a document whose own graph points its containment at `x`. -/ +def hasChildB (fs : FinStore) (x : Node) : Bool := + fs.any fun p => p.1 != x && p.2.any fun t => t.s == p.1 && isContainmentB t && t.o == x + +theorem ownershipB_iff {x : Node} {t : Triple} : ownershipB x t = true ↔ ownership x t := by + simp [ownershipB, ownership] + +theorem containmentB_iff {x : Node} {t : Triple} : containmentB x t = true ↔ containment x t := by + simp [containmentB, containment] + +theorem isContainmentB_iff {t : Triple} : isContainmentB t = true ↔ isContainment t := by + simp [isContainmentB, isContainment] + +theorem hierClassB_iff {c : Node} : hierClassB c = true ↔ hierClass c := by + simp [hierClassB, hierClass, or_assoc] + +theorem keepB_iff {x : Node} {t : Triple} : keepB x t = true ↔ ¬ ownership x t ∧ ¬ containment x t := by + simp [keepB, ← ownershipB_iff, ← containmentB_iff] + +theorem ff {b : Bool} (h : ¬ b = true) : b = false := by cases b <;> simp_all + +theorem any_false {α : Type} {l : List α} {p : α → Bool} (h : l.any p = false) {t : α} (ht : t ∈ l) : + p t = false := by + cases hp : p t + · rfl + · have := List.any_eq_true.2 ⟨t, ht, hp⟩; rw [h] at this; cases this + +theorem noForeign_of {x : Node} {ts : List Triple} (h : foreignContainmentB x ts = false) : + NoForeign x fun t => t ∈ ts := by + intro t ht hc + have := any_false h ht + simp only [Bool.and_eq_false_iff, bne_eq_false_iff_eq] at this + rcases this with h1 | h1 + · rw [isContainmentB_iff.2 hc] at h1; cases h1 + · exact h1 + +theorem hierTypes_of {x : Node} {ts : List Triple} (h : foreignTypeB x ts = false) : HierTypes x fun t => t ∈ ts := by + intro c hc + have := any_false h hc + simp only [beq_self_eq_true, Bool.true_and, Bool.not_eq_false', Bool.and_eq_false_iff] at this + exact hierClassB_iff.1 (by simpa using this) + +theorem typedBy_of {x : Node} {ts : List Triple} (h : typedB x ts = true) : TypedBy x fun t => t ∈ ts := by + obtain ⟨⟨s, p, o⟩, ht, h⟩ := List.any_eq_true.1 h + simp only [Bool.and_eq_true, beq_iff_eq] at h + obtain ⟨⟨rfl, rfl⟩, hh⟩ := h + exact ⟨o, ht, hierClassB_iff.1 hh⟩ + +theorem hasChild_of {fs : FinStore} {x : Node} (h : hasChildB fs x = false) : ¬ hasChild fs.toStore x := by + rintro ⟨k, g, hk, hg, hc⟩ + have hh : hasDoc fs k = true := present_iff.1 ⟨g, hg⟩ + rw [toStore_of_hasDoc hh] at hg; cases hg + have hc' : ∃ q, ⟨k, q, x⟩ ∈ graphOf fs k ∧ isContainment ⟨k, q, x⟩ := by + rcases hc with hc | hc + · exact ⟨_, hc, Or.inl rfl⟩ + · exact ⟨_, hc, Or.inr rfl⟩ + obtain ⟨q, hm, hq⟩ := hc' + obtain ⟨ts, hp, ht⟩ := mem_graphOf.1 hm + have h1 := any_false h hp + rw [show (k != x) = true from bne_iff_ne.2 hk, Bool.true_and] at h1 + have h2 := any_false h1 ht + simp [isContainmentB_iff.2 hq] at h2 + +/-! ## The graph store -/ + +/-- `evaluatePreconditions` on a document the store has: a write quotes its current entity tag, or is refused. -/ +def precondFails : Precond → Option Refusal + | .none => some .preconditionRequired + | .current => none + | .stale | .absent => some .preconditionFailed + +/-- `GET` and `HEAD`. -/ +def readB (fs : FinStore) (x : Node) : Except Refusal (Success × FinStore) := + if hasDoc fs x then .ok (.ok, fs) else .error .notFound + +/-- `post()`. Appending nothing is a no-op that needs no precondition. -/ +def postB (fs : FinStore) (x : Node) (payload : List Triple) (pc : Precond) : Except Refusal (Success × FinStore) := + if payload.isEmpty then .ok (.noContent, fs) + else if foreignContainmentB x payload then .error .unprocessable + else if foreignTypeB x payload then .error .unprocessable + else if !hasDoc fs x then .error .notFound + else match precondFails pc with + | some r => .error r + | none => .ok (.noContent, fs.set x (graphOf fs x ++ payload.filter (keepB x))) + +/-- The containment `put()` asserts: `sioc:has_parent` of a container, `sioc:has_container` of anything else. -/ +def containedB (hs : HSite) (x : Node) (payload : List Triple) : List Triple := + if hs.isRoot x then [] + else if decide (⟨x, .rdfType, .dhContainer⟩ ∈ payload) then [⟨x, .siocHasParent, hs.parent x⟩] + else [⟨x, .siocHasContainer, hs.parent x⟩] + +/-- The `dh:Item` `put()` types a document with that is neither the root nor a container. -/ +def itemB (hs : HSite) (x : Node) (payload : List Triple) : List Triple := + if hs.isRoot x || decide (⟨x, .rdfType, .dhContainer⟩ ∈ payload) then [] else [⟨x, .rdfType, .dhItem⟩] + +/-- The graph `put()` writes, with `keep` the ownership: the stored one, or the agent's for a new document. -/ +def putGraph (hs : HSite) (x : Node) (payload keep : List Triple) : List Triple := + payload.filter (keepB x) ++ (containedB hs x payload ++ (keep ++ itemB hs x payload)) + +def ownedBy (x : Node) : Option Node → List Triple + | some a => [⟨x, .aclOwner, a⟩, ⟨x, .dctCreator, a⟩] + | none => [] + +/-- `put()`. -/ +def putB (hs : HSite) (fs : FinStore) (agent : Option Node) (x : Node) (payload : List Triple) (pc : Precond) : + Except Refusal (Success × FinStore) := + if hs.fixed x then .error .methodNotAllowed + else if !hs.slashed x then .error .permanentRedirect + else if hs.doubleSlash x then .error .badRequest + else if foreignContainmentB x payload then .error .unprocessable + else if foreignTypeB x payload then .error .unprocessable + else if hs.isRoot x && !typedB x payload then .error .unprocessable + else if hasDoc fs x then + match precondFails pc with + | some r => .error r + | none => .ok (.noContent, fs.set x (putGraph hs x payload ((graphOf fs x).filter (ownershipB x)))) + -- If-Match is false when there is no current representation + else if pc = .current ∨ pc = .stale then .error .preconditionFailed + else if !hs.isRoot x && !hasDoc fs (hs.parent x) then .error .conflict + else .ok (.created, fs.set x (putGraph hs x payload (ownedBy x agent))) + +/-- `delete()` once its preconditions hold, as a `PATCH` that empties the graph reaches it. -/ +def deleteChecked (fs : FinStore) (x : Node) : Except Refusal (Success × FinStore) := + if hasChildB fs x then .error .conflict + else if !hasDoc fs x then .error .notFound + else .ok (.noContent, fs.erase x) + +/-- `delete()`. The preconditions are evaluated only on a document the store has. -/ +def deleteB (hs : HSite) (fs : FinStore) (x : Node) (pc : Precond) : Except Refusal (Success × FinStore) := + if hs.isRoot x || hs.fixed x then .error .methodNotAllowed + else if hasDoc fs x then + match precondFails pc with + | some r => .error r + | none => deleteChecked fs x + else deleteChecked fs x + +/-- `rdf:type cannot be removed`: a resource the update leaves described but untyped. -/ +def untypesB (g after : List Triple) : Bool := + g.any fun t => t.p == .rdfType && !(after.any fun u => u.s == t.s && u.p == .rdfType) && after.any fun u => u.s == t.s + +/-- `patch()`. -/ +def patchB (hs : HSite) (fs : FinStore) (x : Node) (del ins : List Triple) (pc : Precond) : + Except Refusal (Success × FinStore) := + if !hasDoc fs x then .error .notFound + else match precondFails pc with + | some r => .error r + | none => + let g := graphOf fs x + let after := g.filter (fun t => !decide (t ∈ del)) ++ ins + if after.isEmpty then + if hs.isRoot x || hs.fixed x then .error .unprocessable else deleteChecked fs x + else if (g ++ ins).any (fun t => (ownershipB x t || containmentB x t) && decide (t ∈ g) != decide (t ∈ after)) + then .error .unprocessable + else if after.any (fun t => isContainmentB t && t.s != x && !decide (t ∈ g)) then .error .unprocessable + else if after.any (fun t => t.s == x && t.p == .rdfType && !hierClassB t.o && !decide (t ∈ g)) + then .error .unprocessable + else if !typedB x after then .error .unprocessable + else if untypesB g after then .error .unprocessable + else .ok (.noContent, fs.set x after) + +/-- What the graph store does with a request: everything after the authorization decision. -/ +def answerB (hs : HSite) (fs : FinStore) (agent : Option Node) (pc : Precond) : + HReq → Except Refusal (Success × FinStore) + | .get x => readB fs x + | .head x => readB fs x + | .post x payload => postB fs x payload pc + | .put x payload => putB hs fs agent x payload pc + | .patch x del ins => patchB hs fs x del ins pc + | .delete x => deleteB hs fs x pc + +/-- The status and the store after the request. -/ +def respondB (hs : HSite) (fs : FinStore) (agent : Option Node) (pc : Precond) (req : HReq) : Nat × FinStore := + match answerB hs fs agent pc req with + | .ok (s, fs') => (s.code, fs') + | .error r => (r.code, fs) + +/-! ## What the answer guarantees -/ + +/-- **A refused request changes nothing.** -/ +theorem respond_refused {hs fs agent pc req r} (h : answerB hs fs agent pc req = .error r) : + respondB hs fs agent pc req = (r.code, fs) := by + simp [respondB, h] + +theorem deleteChecked_not_forbidden {fs x} : deleteChecked fs x ≠ .error .forbidden := by + unfold deleteChecked + split + · simp + · split <;> simp + +theorem precondFails_ne {pc : Precond} : precondFails pc ≠ some .forbidden := by + cases pc <;> simp [precondFails] + +/-- **No check of the graph store answers `403`:** that status is the authorization decision's. -/ +theorem answer_not_forbidden {hs fs agent pc req} : answerB hs fs agent pc req ≠ .error .forbidden := by + intro hd + cases req with + | get | head => simp only [answerB, readB] at hd; split at hd <;> cases hd + | post => + simp only [answerB, postB] at hd + repeat' (first | exact precondFails_ne ‹_› | split at hd | cases hd) + | put => + simp only [answerB, putB] at hd + repeat' (first | exact precondFails_ne ‹_› | split at hd | cases hd) + | patch => + simp only [answerB, patchB] at hd + repeat' (first | exact deleteChecked_not_forbidden hd | exact precondFails_ne ‹_› | split at hd | cases hd) + | delete => + simp only [answerB, deleteB] at hd + repeat' (first | exact deleteChecked_not_forbidden hd | exact precondFails_ne ‹_› | split at hd | cases hd) + +/-! ## What goes through is a `Write` -/ + +theorem toStore_hasDoc {fs : FinStore} {x : Node} (h : hasDoc fs x = true) : + fs.toStore x = some fun t => t ∈ graphOf fs x := toStore_of_hasDoc h + +theorem toStore_not_hasDoc {fs : FinStore} {x : Node} (h : hasDoc fs x = false) : fs.toStore x = none := + toStore_of_not_hasDoc (by simp [h]) + +theorem mem_containedB {tr : Tree} {hs : HSite} (h : hs.agrees tr) {x : Node} {payload : List Triple} + {t : Triple} : t ∈ containedB hs x payload ↔ containedIn tr x (fun t => t ∈ payload) t := by + unfold containedB containedIn + rw [← h.2 x, h.1 x] + by_cases hr : hs.isRoot x = true + · simp [hr] + · by_cases hc : (⟨x, .rdfType, .dhContainer⟩ : Triple) ∈ payload + · simp [hr, hc] + · simp [hr, hc] + +theorem mem_itemB {tr : Tree} {hs : HSite} (h : hs.agrees tr) {x : Node} {payload : List Triple} + {t : Triple} : t ∈ itemB hs x payload ↔ itemTyped tr x (fun t => t ∈ payload) t := by + unfold itemB itemTyped + rw [← h.2 x] + by_cases hr : hs.isRoot x = true + · simp [hr] + · by_cases hc : (⟨x, .rdfType, .dhContainer⟩ : Triple) ∈ payload + · simp [hr, hc] + · simp [hr, hc] + +theorem putGraph_existing {tr : Tree} {hs : HSite} (h : hs.agrees tr) {fs : FinStore} {x : Node} + {payload : List Triple} : + (fun t => t ∈ putGraph hs x payload ((graphOf fs x).filter (ownershipB x))) = + fun t => ((t ∈ payload) ∧ ¬ ownership x t ∧ ¬ containment x t) ∨ containedIn tr x (fun t => t ∈ payload) t ∨ + ((t ∈ graphOf fs x) ∧ ownership x t) ∨ itemTyped tr x (fun t => t ∈ payload) t := by + funext t + simp only [putGraph, List.mem_append, List.mem_filter, keepB_iff, ownershipB_iff, mem_containedB h, mem_itemB h] + +theorem mem_ownedBy {x : Node} {agent : Option Node} {t : Triple} : + t ∈ ownedBy x agent ↔ ∃ a, agent = some a ∧ t.s = x ∧ (t.p = .aclOwner ∨ t.p = .dctCreator) ∧ t.o = a := by + cases agent with + | none => simp [ownedBy] + | some a => + obtain ⟨s, p, o⟩ := t + simp only [ownedBy, List.mem_cons, List.mem_singleton, Triple.mk.injEq, List.not_mem_nil, or_false, + Option.some.injEq, exists_eq_left'] + constructor + · rintro (⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩) + · exact ⟨rfl, Or.inl rfl, rfl⟩ + · exact ⟨rfl, Or.inr rfl, rfl⟩ + · rintro ⟨rfl, hp | hp, rfl⟩ <;> subst hp + · exact Or.inl ⟨rfl, rfl, rfl⟩ + · exact Or.inr ⟨rfl, rfl, rfl⟩ + +theorem putGraph_new {tr : Tree} {hs : HSite} (h : hs.agrees tr) {x : Node} {payload : List Triple} + {agent : Option Node} : + (fun t => t ∈ putGraph hs x payload (ownedBy x agent)) = + fun t => ((t ∈ payload) ∧ ¬ ownership x t ∧ ¬ containment x t) ∨ containedIn tr x (fun t => t ∈ payload) t ∨ + (∃ a, agent = some a ∧ t.s = x ∧ (t.p = .aclOwner ∨ t.p = .dctCreator) ∧ t.o = a) ∨ + itemTyped tr x (fun t => t ∈ payload) t := by + funext t + simp only [putGraph, List.mem_append, List.mem_filter, keepB_iff, mem_ownedBy, mem_containedB h, mem_itemB h] + +theorem deleteChecked_write {tr : Tree} {hs : HSite} (h : hs.agrees tr) {fs : FinStore} {agent : Option Node} + {x : Node} {s : Success} {fs' : FinStore} (hr : hs.isRoot x = false) (hd : deleteChecked fs x = .ok (s, fs')) : + Write tr agent fs.toStore (.delete x) fs'.toStore := by + unfold deleteChecked at hd + split at hd + · cases hd + · rename_i hc + split at hd + · cases hd + · cases hd + rw [toStore_erase] + refine Write.delete (fun hroot => ?_) (hasChild_of (by simpa using hc)) + rw [← h.2 x, hr] at hroot; cases hroot + +/-- The write a request is carried out as: on its document, by its method, or by `DELETE` for a `PATCH` that +empties the graph, which `patch()` hands to `delete()`. -/ +def HReq.writes (req : HReq) (pc : Precond) (r : Req) : Prop := + r.target = req.target ∧ (r.method = req.method pc ∨ (req.method pc = .patch ∧ r.method = .delete)) + +/-- **A request that goes through is a write of the model, or changes nothing.** For a store whose containment +sits in its subjects' own graphs, as `Inv` has it, every answer with a success status is a `Write` of the request +from the store before it to the store after it, or leaves the store as it was. -/ +theorem answer_write {tr : Tree} {hs : HSite} (h : hs.agrees tr) {fs : FinStore} {agent : Option Node} + {pc : Precond} {req : HReq} {s : Success} {fs' : FinStore} + (hown : OwnGraphContainment fs.toStore) (hd : answerB hs fs agent pc req = .ok (s, fs')) : + fs' = fs ∨ ∃ r, req.writes pc r ∧ Write tr agent fs.toStore r fs'.toStore := by + cases req with + | get x | head x => + simp only [answerB, readB] at hd; split at hd + · cases hd; exact Or.inl rfl + · cases hd + | post x payload => + simp only [answerB, postB] at hd + split at hd + · cases hd; exact Or.inl rfl + split at hd; · cases hd + rename_i hfc + split at hd; · cases hd + rename_i hft + split at hd; · cases hd + rename_i hx + have hx : hasDoc fs x = true := by simpa using hx + split at hd; · cases hd + cases hd + refine Or.inr ⟨.post x fun t => t ∈ payload, ⟨rfl, Or.inl rfl⟩, ?_⟩ + have hG : (fun t => t ∈ graphOf fs x ++ payload.filter (keepB x)) = + fun t => t ∈ graphOf fs x ∨ (t ∈ payload ∧ ¬ ownership x t ∧ ¬ containment x t) := by + funext t; simp only [List.mem_append, List.mem_filter, keepB_iff] + rw [toStore_set, hG] + exact Write.post (toStore_hasDoc hx) (noForeign_of (by simpa using hfc)) (hierTypes_of (by simpa using hft)) + | put x payload => + simp only [answerB, putB] at hd + split at hd; · cases hd + split at hd; · cases hd + split at hd; · cases hd + split at hd; · cases hd + rename_i hfc + split at hd; · cases hd + rename_i hft + split at hd; · cases hd + rename_i hroot + have hnf := noForeign_of (x := x) (ts := payload) (by simpa using hfc) + have hty := hierTypes_of (x := x) (ts := payload) (by simpa using hft) + have hrt : tr.isRoot x → TypedBy x fun t => t ∈ payload := by + intro hr + have hr' := (h.2 x).2 hr + simp only [hr', Bool.true_and, Bool.not_eq_true'] at hroot + exact typedBy_of (by simpa using hroot) + split at hd + · rename_i hx + split at hd; · cases hd + rename_i hpc + cases hd + have hcf : pc ≠ .absent := by rintro rfl; simp [precondFails] at hpc + refine Or.inr ⟨.put x (fun t => t ∈ payload) false, ⟨rfl, Or.inl (by simp [HReq.method, hcf, Req.method])⟩, ?_⟩ + rw [toStore_set, putGraph_existing h] + exact Write.putExisting (toStore_hasDoc hx) rfl hnf hty hrt + · rename_i hx + split at hd; · cases hd + split at hd; · cases hd + rename_i hpar + cases hd + refine Or.inr ⟨.put x (fun t => t ∈ payload) (decide (pc = .absent)), ⟨rfl, Or.inl ?_⟩, ?_⟩ + · by_cases hcf : pc = .absent <;> simp [HReq.method, hcf, Req.method] + rw [toStore_set, putGraph_new h] + refine Write.putNew (toStore_not_hasDoc (by simpa using hx)) hnf hty hrt fun hr => ?_ + have hr' : hs.isRoot x = false := by + cases hb : hs.isRoot x + · rfl + · exact absurd ((h.2 x).1 hb) hr + rw [h.1 x] + exact present_iff.2 (by simpa [hr'] using hpar) + | patch x del ins => + simp only [answerB, patchB] at hd + split at hd; · cases hd + rename_i hx + have hx : hasDoc fs x = true := by simpa using hx + split at hd; · cases hd + split at hd + · split at hd; · cases hd + rename_i hr + have hr : hs.isRoot x = false := by simp at hr; exact hr.1 + exact Or.inr ⟨_, ⟨rfl, Or.inr ⟨rfl, rfl⟩⟩, deleteChecked_write h hr hd⟩ + split at hd; · cases hd + rename_i hoc + split at hd; · cases hd + rename_i hfc + split at hd; · cases hd + rename_i hft + split at hd; · cases hd + rename_i hty + split at hd; · cases hd + cases hd + refine Or.inr ⟨Req.patch x fun t => t ∈ (graphOf fs x).filter (fun t => !decide (t ∈ del)) ++ ins, + ⟨rfl, Or.inl rfl⟩, ?_⟩ + rw [toStore_set] + refine Write.patch (toStore_hasDoc hx) ?_ ?_ ?_ (typedBy_of (by simpa using hty)) + · -- the containment the update adds is about x, and what it keeps was, by `hown` + intro t ht hc + by_cases hg : t ∈ graphOf fs x + · exact hown x _ t (toStore_hasDoc hx) hg hc + · have := any_false (ff hfc) ht + simp [isContainmentB_iff.2 hc, hg] at this + exact this + · intro t ho + have hm : t ∈ graphOf fs x ++ ins ∨ ¬ (t ∈ graphOf fs x ++ ins) := Classical.em _ + rcases hm with hm | hm + · have := any_false (ff hoc) hm + have hoc' : (ownershipB x t || containmentB x t) = true := by + rcases ho with ho | ho + · simp [ownershipB_iff.2 ho] + · simp [containmentB_iff.2 ho] + simp only [hoc', Bool.true_and, bne_eq_false_iff_eq, decide_eq_decide] at this + exact this.symm + · simp only [List.mem_append, not_or] at hm + simp [List.mem_append, List.mem_filter, hm.1, hm.2] + · intro c hc + by_cases hg : (⟨x, .rdfType, c⟩ : Triple) ∈ graphOf fs x + · exact Or.inl hg + · have := any_false (ff hft) hc + simp only [beq_self_eq_true, Bool.true_and, hg, decide_false, Bool.not_false, Bool.and_true, + Bool.not_eq_false'] at this + exact Or.inr (hierClassB_iff.1 this) + | delete x => + simp only [answerB, deleteB] at hd + split at hd; · cases hd + rename_i hr + have hr' : hs.isRoot x = false := by simp at hr; exact hr.1 + split at hd + · split at hd; · cases hd + exact Or.inr ⟨_, ⟨rfl, Or.inl rfl⟩, deleteChecked_write h hr' hd⟩ + · exact Or.inr ⟨_, ⟨rfl, Or.inl rfl⟩, deleteChecked_write h hr' hd⟩ + +/-- **The graph store keeps the invariants.** Every answer leaves the containment invariants, and the typing of +documents, as it found them. -/ +theorem answer_inv {tr : Tree} {hs : HSite} (h : hs.agrees tr) {fs : FinStore} {agent : Option Node} + {pc : Precond} {req : HReq} {s : Success} {fs' : FinStore} + (hinv : Inv tr fs.toStore) (hd : answerB hs fs agent pc req = .ok (s, fs')) : + Inv tr fs'.toStore ∧ (Typed fs.toStore → Typed fs'.toStore) := by + rcases answer_write h hinv.own hd with rfl | ⟨_, _, hw⟩ + · exact ⟨hinv, id⟩ + · exact ⟨hw.inv hinv, hw.typed⟩ + +end LdhHttp diff --git a/formal/acl/LdhAcl/Base.lean b/formal/http/LdhHttp/Base.lean similarity index 75% rename from formal/acl/LdhAcl/Base.lean rename to formal/http/LdhHttp/Base.lean index 8181af61d..3bdf95d04 100644 --- a/formal/acl/LdhAcl/Base.lean +++ b/formal/http/LdhHttp/Base.lean @@ -1,27 +1,17 @@ /- -What the authorization decision reads and the requests that change it: the quad store of a dataspace, one named graph -per document, the access modes, and the graph store's requests. +The graph store's data and requests: the quad store of a dataspace, one named graph per document, the document +hierarchy over it, and the requests that change it. -/ -namespace LdhAcl +namespace LdhHttp -/-- RDF nodes. The vocabulary terms the decision reads are constructors of their own; every other IRI is -`iri n`. Literals play no part in the decision and are not modelled. -/ +/-- RDF nodes. The vocabulary terms the graph store and the authorization decision read are constructors of their +own; every other term, literals included, is `iri n`. -/ inductive Node where | rdfType | aclOwner | dctCreator | siocHasParent | siocHasContainer | nfoFileDataObject | dhContainer | dhItem | defRoot | iri (n : Nat) deriving DecidableEq, Repr -/-- `acl:Read`, `acl:Append`, `acl:Write`, `acl:Control`. -/ -inductive Mode where - | read | append | write | control - deriving DecidableEq, Repr - -/-- `AccessModes.covering`: a granted mode covers the required one if it is that mode or one of its -superclasses in `acl.rdf`, where the only edge between modes is `acl:Append rdfs:subClassOf acl:Write`. -/ -def Mode.covers (granted required : Mode) : Prop := - granted = required ∨ (granted = .write ∧ required = .append) - structure Triple where s : Node p : Node @@ -42,6 +32,22 @@ def present (st : Store) (x : Node) : Prop := ∃ g, st x = some g def Store.set (st : Store) (x : Node) (v : Option Graph) : Store := fun y => if y = x then v else st y +/-! ## The document hierarchy -/ + +/-- Deployment constants: the URI parent `put()` resolves, and the documents with none, the roots. -/ +structure Tree where + parent : Node → Node + isRoot : Node → Prop + +/-- The classes of the document hierarchy, which both dataspaces type their documents with. -/ +def hierClass (c : Node) : Prop := c = .defRoot ∨ c = .dhContainer ∨ c = .dhItem + +def isContainment (t : Triple) : Prop := t.p = .siocHasParent ∨ t.p = .siocHasContainer + +/-- `g` states that `d` is contained in `p`. -/ +def contains (g : Graph) (d p : Node) : Prop := + g ⟨d, .siocHasParent, p⟩ ∨ g ⟨d, .siocHasContainer, p⟩ + /-! ## Reading a document's own graph -/ /-- The `acl:accessToClass` rows of `documentContextQuery`: the types a document's own graph asserts for it. -/ @@ -93,4 +99,4 @@ asserted in any other graph does not count. -/ def hasChild (st : Store) (x : Node) : Prop := ∃ k g, k ≠ x ∧ st k = some g ∧ (g ⟨k, .siocHasParent, x⟩ ∨ g ⟨k, .siocHasContainer, x⟩) -end LdhAcl +end LdhHttp 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/Fin.lean b/formal/http/LdhHttp/Fin.lean new file mode 100644 index 000000000..72311504f --- /dev/null +++ b/formal/http/LdhHttp/Fin.lean @@ -0,0 +1,198 @@ +/- +A store as data: what the executable answer runs on, and the abstract store it denotes. +-/ +import LdhHttp.Write + +namespace LdhHttp + +/-! ## Finite data -/ + +/-- A store as data: a document's graph as the list of its triples. A document listed more than once has the +union of its lists. -/ +abbrev FinStore := List (Node × List Triple) + +/-- The graph store's notion of existence, computed. -/ +def hasDoc (fs : FinStore) (d : Node) : Bool := fs.any (·.1 == d) + +/-- The triples of a document's own graph. -/ +def graphOf (fs : FinStore) (d : Node) : List Triple := + fs.foldr (fun p acc => if p.1 = d then p.2 ++ acc else acc) [] + +/-- The abstract store the data denotes. -/ +def FinStore.toStore (fs : FinStore) : Store := + fun d => if hasDoc fs d then some (fun t => t ∈ graphOf fs d) else none + +theorem hasDoc_iff {fs : FinStore} {d : Node} : hasDoc fs d = true ↔ ∃ ts, (d, ts) ∈ fs := by + simp only [hasDoc, List.any_eq_true, beq_iff_eq] + constructor + · rintro ⟨⟨d', ts⟩, h, rfl⟩ + exact ⟨ts, h⟩ + · rintro ⟨ts, h⟩ + exact ⟨(d, ts), h, rfl⟩ + +theorem graphOf_cons {p : Node × List Triple} {fs : FinStore} {d : Node} : + graphOf (p :: fs) d = if p.1 = d then p.2 ++ graphOf fs d else graphOf fs d := rfl + +theorem mem_graphOf {fs : FinStore} {d : Node} {t : Triple} : + t ∈ graphOf fs d ↔ ∃ ts, (d, ts) ∈ fs ∧ t ∈ ts := by + induction fs with + | nil => simp [graphOf] + | cons p fs ih => + obtain ⟨p1, p2⟩ := p + rw [graphOf_cons] + by_cases h : p1 = d + · subst h + simp only [if_true, List.mem_append, ih, List.mem_cons] + constructor + · rintro (ht | ⟨ts, hts, ht⟩) + · exact ⟨p2, Or.inl rfl, ht⟩ + · exact ⟨ts, Or.inr hts, ht⟩ + · rintro ⟨ts, hts | hts, ht⟩ + · cases hts; exact Or.inl ht + · exact Or.inr ⟨ts, hts, ht⟩ + · simp only [h, if_false, ih, List.mem_cons] + constructor + · rintro ⟨ts, hts, ht⟩ + exact ⟨ts, Or.inr hts, ht⟩ + · rintro ⟨ts, hts | hts, ht⟩ + · cases hts; exact absurd rfl h + · exact ⟨ts, hts, ht⟩ + +theorem hasDoc_of_mem_graphOf {fs : FinStore} {d : Node} {t : Triple} (h : t ∈ graphOf fs d) : + hasDoc fs d = true := by + obtain ⟨ts, hm, _⟩ := mem_graphOf.1 h + exact hasDoc_iff.2 ⟨ts, hm⟩ + +theorem toStore_of_hasDoc {fs : FinStore} {d : Node} (h : hasDoc fs d = true) : + fs.toStore d = some (fun t => t ∈ graphOf fs d) := by + simp [FinStore.toStore, h] + +theorem toStore_of_not_hasDoc {fs : FinStore} {d : Node} (h : ¬ hasDoc fs d = true) : + fs.toStore d = none := by + simp [FinStore.toStore, h] + +theorem present_iff {fs : FinStore} {d : Node} : present fs.toStore d ↔ hasDoc fs d = true := by + constructor + · rintro ⟨g, hg⟩ + unfold FinStore.toStore at hg + split at hg + · assumption + · cases hg + · intro h + exact ⟨_, toStore_of_hasDoc h⟩ + +/-- A triple of a document's own graph. -/ +theorem own_iff {fs : FinStore} {d : Node} {t : Triple} : + (∃ g, fs.toStore d = some g ∧ g t) ↔ t ∈ graphOf fs d := by + constructor + · rintro ⟨g, hg, ht⟩ + by_cases h : hasDoc fs d = true + · rw [toStore_of_hasDoc h] at hg + cases hg + exact ht + · rw [toStore_of_not_hasDoc h] at hg + cases hg + · intro ht + exact ⟨_, toStore_of_hasDoc (hasDoc_of_mem_graphOf ht), ht⟩ + +theorem ownTypes_iff {fs : FinStore} {x t : Node} : + ownTypes fs.toStore x t ↔ ⟨x, .rdfType, t⟩ ∈ graphOf fs x := own_iff + +theorem owner_iff {fs : FinStore} {x a : Node} : + owner fs.toStore x a ↔ ⟨x, .aclOwner, a⟩ ∈ graphOf fs x := own_iff + +/-- The objects of a document's own `rdf:type` triples. -/ +def typesOf (fs : FinStore) (x : Node) : List Node := + (graphOf fs x).filterMap fun t => if t.s = x ∧ t.p = .rdfType then some t.o else none + +/-- The objects of a document's own `acl:owner` triples. -/ +def ownersOf (fs : FinStore) (x : Node) : List Node := + (graphOf fs x).filterMap fun t => if t.s = x ∧ t.p = .aclOwner then some t.o else none + +theorem mem_filterMap_prop {fs : FinStore} {x p o : Node} : + o ∈ ((graphOf fs x).filterMap fun t => if t.s = x ∧ t.p = p then some t.o else none) ↔ + ⟨x, p, o⟩ ∈ graphOf fs x := by + simp only [List.mem_filterMap] + constructor + · rintro ⟨⟨s, p', o'⟩, ht, h⟩ + simp only at h + split at h + · rename_i hsp + cases h + obtain ⟨rfl, rfl⟩ := hsp + exact ht + · cases h + · intro h + exact ⟨_, h, by simp⟩ + +theorem mem_typesOf {fs : FinStore} {x t : Node} : t ∈ typesOf fs x ↔ ownTypes fs.toStore x t := + mem_filterMap_prop.trans ownTypes_iff.symm + +theorem mem_ownersOf {fs : FinStore} {x a : Node} : a ∈ ownersOf fs x ↔ owner fs.toStore x a := + mem_filterMap_prop.trans owner_iff.symm + +/-! ## Writing a finite store -/ + +/-- The store with document `x`'s graph replaced by `ts`. -/ +def FinStore.set (fs : FinStore) (x : Node) (ts : List Triple) : FinStore := + (x, ts) :: fs.filter fun p => p.1 != x + +/-- The store without document `x`. -/ +def FinStore.erase (fs : FinStore) (x : Node) : FinStore := fs.filter fun p => p.1 != x + +theorem hasDoc_erase {fs : FinStore} {x y : Node} (h : y ≠ x) : hasDoc (fs.erase x) y = hasDoc fs y := by + simp only [FinStore.erase, hasDoc, List.any_filter] + congr 1; funext p + by_cases hp : p.1 = y + · subst hp; simp [h] + · simp [hp] + +theorem graphOf_erase {fs : FinStore} {x y : Node} (h : y ≠ x) : graphOf (fs.erase x) y = graphOf fs y := by + induction fs with + | nil => rfl + | cons p fs ih => + simp only [FinStore.erase, List.filter_cons] at ih ⊢ + by_cases hp : p.1 = x + · have hpy : p.1 ≠ y := fun e => h (e ▸ hp) + simp [hp, ih, graphOf_cons, Ne.symm h] + · simp only [hp, bne_iff_ne, ne_eq, not_false_eq_true, decide_true, ite_true, graphOf_cons, ih] + +theorem hasDoc_cons_other {fs : FinStore} {p : Node × List Triple} {y : Node} (h : p.1 ≠ y) : + hasDoc (p :: fs) y = hasDoc fs y := by + simp [hasDoc, h] + +theorem graphOf_cons_other {fs : FinStore} {p : Node × List Triple} {y : Node} (h : p.1 ≠ y) : + graphOf (p :: fs) y = graphOf fs y := by + rw [graphOf_cons, if_neg h] + +theorem set_eq {fs : FinStore} {x : Node} {ts : List Triple} : fs.set x ts = (x, ts) :: fs.erase x := rfl + +theorem hasDoc_erase_self {fs : FinStore} {x : Node} : hasDoc (fs.erase x) x = false := by + simp [FinStore.erase, hasDoc, List.any_filter] + +theorem toStore_erase {fs : FinStore} {x : Node} : (fs.erase x).toStore = fs.toStore.set x none := by + funext y + by_cases h : y = x + · subst h; simp [FinStore.toStore, Store.set, hasDoc_erase_self] + · simp [FinStore.toStore, Store.set, h, hasDoc_erase h, graphOf_erase h] + +theorem toStore_set {fs : FinStore} {x : Node} {ts : List Triple} : + (fs.set x ts).toStore = fs.toStore.set x (some fun t => t ∈ ts) := by + funext y + by_cases h : y = x + · subst h + have he : graphOf (fs.erase y) y = [] := by + rcases hx : graphOf (fs.erase y) y with _ | ⟨t, _⟩ + · rfl + · have : hasDoc (fs.erase y) y = true := hasDoc_of_mem_graphOf (hx ▸ List.mem_cons_self t _) + rw [hasDoc_erase_self] at this; cases this + have hh : hasDoc (fs.set y ts) y = true := by simp [FinStore.set, hasDoc] + have hg : graphOf (fs.set y ts) y = ts := by rw [set_eq, graphOf_cons, if_pos rfl, he, List.append_nil] + rw [toStore_of_hasDoc hh, hg]; simp [Store.set] + · have hh : hasDoc (fs.set x ts) y = hasDoc fs y := by + rw [set_eq, hasDoc_cons_other (Ne.symm h), hasDoc_erase h] + have hg : graphOf (fs.set x ts) y = graphOf fs y := by + rw [set_eq, graphOf_cons_other (Ne.symm h), graphOf_erase h] + simp [FinStore.toStore, Store.set, h, hh, hg] + +end LdhHttp diff --git a/formal/http/LdhHttp/IO.lean b/formal/http/LdhHttp/IO.lean new file mode 100644 index 000000000..58d159d4d --- /dev/null +++ b/formal/http/LdhHttp/IO.lean @@ -0,0 +1,295 @@ +/- +Reading a live instance's data and a request into the model's terms, and printing an answer. Unproven and small: +the N-Triples and N-Quads reader, the interning of terms as nodes (literals included, so that a payload of +literals is not empty), the URI parent `put()` resolves, and the URI checks of `put()` (a root is its own URI +parent; a trailing slash; a double slash in the path). +-/ +import LdhHttp.Answer +import Std.Data.HashMap + +namespace LdhHttp + +open Std + +instance : Hashable Node where + hash + | .rdfType => 1 | .aclOwner => 2 | .dctCreator => 3 | .siocHasParent => 4 | .siocHasContainer => 5 + | .nfoFileDataObject => 6 | .dhContainer => 7 | .dhItem => 8 | .defRoot => 9 + | .iri n => hash (n + 16) + +/-! ## Terms and quads -/ + +inductive Term where + | iri (s : String) + | blank (s : String) + /-- A literal, as written: the quoted form with its language tag or datatype. -/ + | literal (s : String) + deriving Repr, BEq + +structure Quad where + s : Term + p : Term + o : Term + g : Term + +/-- The name a node is interned under: an IRI, or a blank node label, which cannot collide with an IRI. The admin +dataset is read through these alone, as `aclQuery` matches no literal. -/ +def Term.key : Term → Option String + | .iri s => some s + | .blank s => some s + | .literal _ => none + +/-- The name a store's term is interned under: a literal as written, which cannot collide with an IRI or a blank +node label either. The graph store's answer reads literals: a payload of literals alone is not empty. -/ +def Term.storeKey : Term → String + | .iri s => s + | .blank s => s + | .literal s => s + +/-! ## N-Quads -/ + +/-- One term from the front of `s`; the rest after it. -/ +partial def parseTerm (s : Substring) : Option (Term × Substring) := + let s := s.trimLeft + if s.isEmpty then none + else match s.front with + | '<' => + let body := (s.drop 1).takeWhile (· ≠ '>') + let rest := (s.drop 1).dropWhile (· ≠ '>') + if rest.isEmpty then none else some (.iri body.toString, rest.drop 1) + | '_' => + let body := s.takeWhile fun c => !c.isWhitespace + some (.blank body.toString, s.drop body.bsize) + | '"' => + -- the closing quote is the first one not escaped + let rec close (t : Substring) (escaped : Bool) : Substring := + if t.isEmpty then t + else + let c := t.front + if escaped then close (t.drop 1) false + else if c == '\\' then close (t.drop 1) true + else if c == '"' then t.drop 1 + else close (t.drop 1) false + let after := close (s.drop 1) false + -- a language tag or a datatype follows without a space + let after := after.dropWhile fun c => !c.isWhitespace + some (.literal (Substring.mk s.str s.startPos after.startPos).toString, after) + | _ => none + +def parseQuad (line : String) : Option Quad := do + let (s, r) ← parseTerm line.toSubstring + let (p, r) ← parseTerm r + let (o, r) ← parseTerm r + let (g, _) ← parseTerm r + pure ⟨s, p, o, g⟩ + +def parseTriple (line : String) : Option (Term × Term × Term) := do + let (s, r) ← parseTerm line.toSubstring + let (p, r) ← parseTerm r + let (o, _) ← parseTerm r + pure (s, p, o) + +def readTriples (path : System.FilePath) : IO (Array (Term × Term × Term)) := do + let lines ← IO.FS.lines path + let mut triples := #[] + for line in lines do + let t := line.trim + if t.isEmpty || t.startsWith "#" then continue + match parseTriple t with + | some q => triples := triples.push q + | none => throw (IO.userError s!"cannot read N-Triples line: {line}") + pure triples + +def readQuads (path : System.FilePath) : IO (Array Quad) := do + let lines ← IO.FS.lines path + let mut quads := #[] + for line in lines do + let t := line.trim + if t.isEmpty || t.startsWith "#" then continue + match parseQuad t with + | some q => quads := quads.push q + | none => throw (IO.userError s!"cannot read N-Quads line: {line}") + pure quads + +/-! ## Vocabulary -/ + +namespace V +def rdfType := "http://www.w3.org/1999/02/22-rdf-syntax-ns#type" +def aclOwner := "http://www.w3.org/ns/auth/acl#owner" +def dctCreator := "http://purl.org/dc/terms/creator" +def siocHasParent := "http://rdfs.org/sioc/ns#has_parent" +def siocHasContainer := "http://rdfs.org/sioc/ns#has_container" +def nfoFileDataObject := "http://www.semanticdesktop.org/ontologies/2007/03/22/nfo#FileDataObject" +def dhContainer := "https://w3id.org/atomgraph/linkeddatahub/document-hierarchy#Container" +def dhItem := "https://w3id.org/atomgraph/linkeddatahub/document-hierarchy#Item" +def defRoot := "https://w3id.org/atomgraph/linkeddatahub/default#Root" +end V + + +/-- The terms the decision reads are constructors of `Node`; every other one is interned. -/ +def vocabulary : List (String × Node) := + [(V.rdfType, .rdfType), (V.aclOwner, .aclOwner), (V.dctCreator, .dctCreator), (V.siocHasParent, .siocHasParent), + (V.siocHasContainer, .siocHasContainer), (V.nfoFileDataObject, .nfoFileDataObject), + (V.dhContainer, .dhContainer), (V.dhItem, .dhItem), (V.defRoot, .defRoot)] + +structure Interner where + nodes : HashMap String Node := vocabulary.foldl (fun m (k, n) => m.insert k n) {} + next : Nat := 0 + +def Interner.intern (i : Interner) (key : String) : Node × Interner := + match i.nodes[key]? with + | some n => (n, i) + | none => (.iri i.next, { nodes := i.nodes.insert key (.iri i.next), next := i.next + 1 }) + +/-- Interns a batch of keys, in order. -/ +def Interner.internAll (i : Interner) (keys : List String) : List Node × Interner := + keys.foldr (fun k (ns, i) => let (n, i) := i.intern k; (n :: ns, i)) ([], i) + +/-! ## Reading the stores -/ + +def internTriple (i : Interner) (s p o : Term) : Triple × Interner := + let (ns, i) := i.intern s.storeKey + let (np, i) := i.intern p.storeKey + let (no, i) := i.intern o.storeKey + (⟨ns, np, no⟩, i) + +/-- Every quad, literals included, as a triple under its graph name. -/ +def internQuads (i : Interner) (quads : Array Quad) : Array (Node × Triple) × Interner := Id.run do + let mut i := i + let mut out := #[] + for q in quads do + let (t, i1) := internTriple i q.s q.p q.o + let (ng, i2) := i1.intern q.g.storeKey + i := i2 + out := out.push (ng, t) + pure (out, i) + +def internTriples (i : Interner) (ts : Array (Term × Term × Term)) : List Triple × Interner := Id.run do + let mut i := i + let mut out := #[] + for (s, p, o) in ts do + let (t, i1) := internTriple i s p o + i := i1 + out := out.push t + pure (out.toList, i) + +/-- A node as an N-Triples term, from the name it was interned under. -/ +def render (names : HashMap Node String) (n : Node) : String := + let k := names.getD n "" + if k.startsWith "\"" || k.startsWith "_:" then k else s!"<{k}>" + +/-- Groups interned quads by graph. -/ +def toFinStore (quads : Array (Node × Triple)) : FinStore := Id.run do + let mut m : HashMap Node (List Triple) := {} + for (g, t) in quads do + m := m.insert g (t :: m.getD g []) + pure (m.toList) + +/-! ## The site -/ + +/-- The URI parent `put()` resolves: `..` against the document URI, by RFC 3986. The base's last segment goes +first, so a URI with a trailing slash (every document the graph store has) climbs one level, and one without +climbs two: `/a/b/` and `/a/b/c` both give `/a/`. The root of a tree is its own parent. -/ +def parentIri (s : String) : String := + -- no path at all: nothing to climb + if !(((s.splitOn "://").getD 1 "").contains '/') then s else + -- the directory of the URI: up to and including its last slash + let dir := match s.revPosOf '/' with + | some pos => s.extract 0 (s.next pos) + | none => s + let core := dir.dropRight 1 + match core.revPosOf '/' with + | none => s + | some pos => + let before := core.extract 0 pos + -- the slash found belongs to the scheme's `//`: the URI has no path above it + if before.endsWith "/" || before.endsWith ":" then dir else core.extract 0 (core.next pos) + +/-- The URI's path has a double slash. -/ +def doubleSlash (s : String) : Bool := + decide ((((s.splitOn "://").getD 1 "").splitOn "//").length > 1) + +def parsePrecond : String → Option Precond + | "none" => some .none + | "current" => some .current + | "stale" => some .stale + | "absent" => some .absent + | _ => none + +/-! ## Requests -/ + +/-- Where a request and its body are read from. -/ +structure RequestFiles where + request : String + payload : Option String := none + delete : Option String := none + insert : Option String := none + /-- The owner's and the secretary's WebID documents. -/ + fixed : List String := [] + +/-- A request read and interned: the site constants about its document, the agent, the precondition and the +request. -/ +structure LoadedRequest where + hs : HSite + agent : Option Node + pc : Precond + req : HReq + interner : Interner + +/-- Reads `AGENTMETHODDOCUMENTPRECONDITION` and the body files, interning their terms. -/ +def loadRequest (i : Interner) (files : RequestFiles) : IO (Except String LoadedRequest) := do + let line := ((← IO.FS.lines files.request).toList.filter (!·.trim.isEmpty)).headD "" + let (agentKey, method, target, pc) ← match line.splitOn "\t" with + | [a, m, t, p] => match parsePrecond p with + | some pc => pure (if a == "-" then none else some a, m, t, pc) + | none => return .error s!"cannot read precondition: {p}" + | _ => return .error s!"cannot read request: {line}" + let readOpt (path : Option String) : IO (Array (Term × Term × Term)) := + match path with + | some p => readTriples p + | none => pure #[] + let payloadTerms ← readOpt files.payload + let deleteTerms ← readOpt files.delete + let insertTerms ← readOpt files.insert + let (x, i) := i.intern target + let (parent, i) := i.intern (parentIri target) + let (agent, i) := match agentKey with + | some a => let (n, i) := i.intern a; (some n, i) + | none => (none, i) + let (payload, i) := internTriples i payloadTerms + let (del, i) := internTriples i deleteTerms + let (ins, i) := internTriples i insertTerms + let (fixedNodes, i) := i.internAll files.fixed + let req ← match method with + | "GET" => pure (HReq.get x) + | "HEAD" => pure (HReq.head x) + | "POST" => pure (HReq.post x payload) + | "PUT" => pure (HReq.put x payload) + | "PATCH" => pure (HReq.patch x del ins) + | "DELETE" => pure (HReq.delete x) + | m => return .error s!"cannot read method: {m}" + -- the constants are computed for the request's document: a root is its own URI parent + let hs : HSite := { + parent := fun d => if d == x then parent else d + isRoot := fun d => d == x && parentIri target == target + slashed := fun d => d != x || target.endsWith "/" + doubleSlash := fun d => d == x && doubleSlash target + fixed := fun d => fixedNodes.contains d } + return .ok ⟨hs, agent, pc, req, i⟩ + +/-- The status, then the document's graph, as N-Triples: a set of triples, each printed once. -/ +def printAnswer (i : Interner) (status : Nat) (fs : FinStore) (x : Node) : IO Unit := do + IO.println s!"{status}" + let names : HashMap Node String := i.nodes.fold (fun m k n => m.insert n k) {} + for t in (graphOf fs x).eraseDups do + IO.println s!"{render names t.s} {render names t.p} {render names t.o} ." + +/-- The arguments that name a request and its body. -/ +def parseRequestArg : List String → RequestFiles → Option (List String × RequestFiles) + | "--payload" :: v :: rest, f => some (rest, { f with payload := some v }) + | "--delete" :: v :: rest, f => some (rest, { f with delete := some v }) + | "--insert" :: v :: rest, f => some (rest, { f with insert := some v }) + | "--fixed" :: v :: rest, f => some (rest, { f with fixed := v :: f.fixed }) + | _, _ => none + +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/LdhHttp/Write.lean b/formal/http/LdhHttp/Write.lean new file mode 100644 index 000000000..5a750f198 --- /dev/null +++ b/formal/http/LdhHttp/Write.lean @@ -0,0 +1,440 @@ +/- +The writes of `DocumentHierarchyGraphStoreImpl`, and the invariants they keep. + +Each write touches one graph, the request URI's. A write is what the graph store does with a request it answers +with a success status; whether the request was authorized is no part of it. A graph written for document `x` may state containment of `x` only: a +payload with `sioc:has_parent` or `sioc:has_container` of any other subject is refused (`422`, +`checkForeignContainment`), and containment of `x` itself is stripped or guarded. That rule is what makes the union +graph a faithful view of containment. A write may also type `x` with hierarchy classes only, and must leave it typed +with one (`422`, `checkDocumentTypes`). A document is created only below a parent the store has (`409`). +-/ +import LdhHttp.Base + +namespace LdhHttp + +/-- The write rule: every containment triple of `g` is about `x`. -/ +def NoForeign (x : Node) (g : Graph) : Prop := ∀ t, g t → isContainment t → t.s = x + +/-- The containment `put()` asserts for a non-root document, pointing at the URI parent: `sioc:has_parent` when +the payload types it `dh:Container`, `sioc:has_container` otherwise. -/ +def containedIn (tr : Tree) (x : Node) (payload : Graph) (t : Triple) : Prop := + ¬ tr.isRoot x ∧ + ((payload ⟨x, .rdfType, .dhContainer⟩ ∧ t = ⟨x, .siocHasParent, tr.parent x⟩) ∨ + (¬ payload ⟨x, .rdfType, .dhContainer⟩ ∧ t = ⟨x, .siocHasContainer, tr.parent x⟩)) + +theorem containedIn.props {tr : Tree} {x : Node} {payload : Graph} {t : Triple} + (h : containedIn tr x payload t) : ¬ tr.isRoot x ∧ t.s = x ∧ isContainment t ∧ t.o = tr.parent x := by + obtain ⟨hr, ⟨_, rfl⟩ | ⟨_, rfl⟩⟩ := h + · exact ⟨hr, rfl, Or.inl rfl, rfl⟩ + · exact ⟨hr, rfl, Or.inr rfl, rfl⟩ + +/-- A non-root document's `put()` graph states its containment in its URI parent. -/ +theorem containedIn_contains {tr : Tree} {x : Node} {payload : Graph} {G : Graph} (hr : ¬ tr.isRoot x) + (hG : ∀ t, containedIn tr x payload t → G t) : contains G x (tr.parent x) := by + by_cases hc : payload ⟨x, .rdfType, .dhContainer⟩ + · exact Or.inl (hG _ ⟨hr, Or.inl ⟨hc, rfl⟩⟩) + · exact Or.inr (hG _ ⟨hr, Or.inr ⟨hc, rfl⟩⟩) + +/-- The type rule: a graph written for `x` types `x` with hierarchy classes only. -/ +def HierTypes (x : Node) (g : Graph) : Prop := ∀ c, g ⟨x, .rdfType, c⟩ → hierClass c + +/-- `g` types `x` with a hierarchy class. -/ +def TypedBy (x : Node) (g : Graph) : Prop := ∃ c, g ⟨x, .rdfType, c⟩ ∧ hierClass c + +/-- The class `put()` asserts for a non-root document the payload does not type `dh:Container`. -/ +def itemTyped (tr : Tree) (x : Node) (payload : Graph) (t : Triple) : Prop := + ¬ tr.isRoot x ∧ ¬ payload ⟨x, .rdfType, .dhContainer⟩ ∧ t = ⟨x, .rdfType, .dhItem⟩ + +/-- One write by `agent`, from `st` to `st'`. A `PUT` of the root is stored as sent, so its payload has to type it; +any other `PUT` is typed `dh:Item` unless it is a container, and creates a document only below a parent the store +has. A `PATCH` may keep the types the document has and add hierarchy classes, and must not drop the last of them. -/ +inductive Write (tr : Tree) (agent : Option Node) : Store → Req → Store → Prop where + | post {st x payload g} : + st x = some g → + NoForeign x payload → + HierTypes x payload → + Write tr agent st (.post x payload) + (st.set x (some fun t => g t ∨ (payload t ∧ ¬ ownership x t ∧ ¬ containment x t))) + | putExisting {st x payload createOnly g} : + st x = some g → + createOnly = false → + NoForeign x payload → + HierTypes x payload → + (tr.isRoot x → TypedBy x payload) → + Write tr agent st (.put x payload createOnly) + (st.set x (some fun t => + (payload t ∧ ¬ ownership x t ∧ ¬ containment x t) ∨ containedIn tr x payload t ∨ + (g t ∧ ownership x t) ∨ itemTyped tr x payload t)) + | putNew {st x payload createOnly} : + st x = none → + NoForeign x payload → + HierTypes x payload → + (tr.isRoot x → TypedBy x payload) → + (¬ tr.isRoot x → present st (tr.parent x)) → + Write tr agent st (.put x payload createOnly) + (st.set x (some fun t => + (payload t ∧ ¬ ownership x t ∧ ¬ containment x t) ∨ containedIn tr x payload t ∨ + (∃ a, agent = some a ∧ t.s = x ∧ (t.p = .aclOwner ∨ t.p = .dctCreator) ∧ t.o = a) ∨ + itemTyped tr x payload t)) + | patch {st x after g} : + st x = some g → + NoForeign x after → + (∀ t, ownership x t ∨ containment x t → (after t ↔ g t)) → + (∀ c, after ⟨x, .rdfType, c⟩ → g ⟨x, .rdfType, c⟩ ∨ hierClass c) → + TypedBy x after → + Write tr agent st (.patch x after) (st.set x (some after)) + | delete {st x} : + ¬ tr.isRoot x → + ¬ hasChild st x → + Write tr agent st (.delete x) (st.set x none) + +theorem Write.frame {tr agent st req st'} (h : Write tr agent st req st') + {y : Node} (hy : y ≠ req.target) : st' y = st y := by + cases h <;> simp [Store.set, Req.target] at hy ⊢ <;> simp [hy] + +/-! ## Invariants -/ + +/-- What the write rule maintains: every containment triple sits in its subject's own graph. -/ +def OwnGraphContainment (st : Store) : Prop := + ∀ y g t, st y = some g → g t → isContainment t → t.s = y + +/-- A document's own graph points its containment at its URI parent and nowhere else. -/ +def Exact (tr : Tree) (st : Store) : Prop := + ∀ d g p, st d = some g → contains g d p → ¬ tr.isRoot d ∧ p = tr.parent d + +/-- Every non-root document's own graph states its containment. -/ +def Contained (tr : Tree) (st : Store) : Prop := + ∀ d g, st d = some g → ¬ tr.isRoot d → contains g d (tr.parent d) + +/-- Every non-root document's URI parent is in the store. -/ +def Hier (tr : Tree) (st : Store) : Prop := + ∀ d, present st d → ¬ tr.isRoot d → present st (tr.parent d) + +def RootsPresent (tr : Tree) (st : Store) : Prop := + ∀ r, tr.isRoot r → present st r + +structure Inv (tr : Tree) (st : Store) : Prop where + own : OwnGraphContainment st + exact : Exact tr st + contained : Contained tr st + hier : Hier tr st + roots : RootsPresent tr st + +theorem present_set_self {st : Store} {x : Node} {g : Graph} : present (st.set x (some g)) x := + ⟨g, by simp [Store.set]⟩ + +theorem present_set_other {st : Store} {x z : Node} {v} (h : z ≠ x) : + present (st.set x v) z ↔ present st z := by + simp [present, Store.set, h] + +/-- Every write but a delete leaves a graph at its target. -/ +theorem Write.present_target {tr agent st req st'} (h : Write tr agent st req st') + (hd : ∀ x, req ≠ .delete x) : present st' req.target := by + cases h with + | delete => exact absurd rfl (hd _) + | _ => exact present_set_self + +/-- Every write but a delete keeps every present document present. -/ +theorem Write.present_mono {tr agent st req st'} (h : Write tr agent st req st') + (hd : ∀ x, req ≠ .delete x) {p : Node} (hp : present st p) : present st' p := by + by_cases hpx : p = req.target + · rw [hpx]; exact h.present_target hd + · obtain ⟨g, hg⟩ := hp; exact ⟨g, by rw [h.frame hpx]; exact hg⟩ + +theorem ownership_not_containment {x : Node} {t : Triple} (ho : ownership x t) (hc : isContainment t) : + False := by + obtain ⟨_, hp⟩ := ho + rcases hp with hp | hp <;> rcases hc with hc | hc <;> rw [hp] at hc <;> cases hc + +theorem own_preserved {tr agent st req st'} (hs : Write tr agent st req st') + (h : OwnGraphContainment st) : OwnGraphContainment st' := by + intro y g' t hy ht hc + by_cases hyx : y = req.target + · cases hs with + | @post x _ g hg hnf => + simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy; subst hy + rcases ht with ht | ⟨ht, _⟩ + · exact h _ _ _ hg ht hc + · exact hnf _ ht hc + | putExisting _ _ hnf => + simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy; subst hy + rcases ht with ⟨ht, _⟩ | hci | ⟨_, hs, _⟩ | ⟨_, _, rfl⟩ + · exact hnf _ ht hc + · exact hci.props.2.1 + · exact hs + · rcases hc with hc | hc <;> cases hc + | putNew _ hnf => + simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy; subst hy + rcases ht with ⟨ht, _⟩ | hci | ⟨_, _, hs, _⟩ | ⟨_, _, rfl⟩ + · exact hnf _ ht hc + · exact hci.props.2.1 + · exact hs + · rcases hc with hc | hc <;> cases hc + | patch _ hnf => + simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy; subst hy + exact hnf _ ht hc + | delete => + simp [Req.target] at hyx; subst hyx; simp [Store.set] at hy + · rw [hs.frame hyx] at hy + exact h _ _ _ hy ht hc + +theorem exact_preserved {tr agent st req st'} (hs : Write tr agent st req st') + (h : Exact tr st) : Exact tr st' := by + intro d g' p hd hc + by_cases hdx : d = req.target + · cases hs with + | @post x _ g hg _ => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd + rcases hc with (hc | ⟨_, _, hn⟩) | (hc | ⟨_, _, hn⟩) + · exact h _ _ _ hg (Or.inl hc) + · exact absurd ⟨rfl, Or.inl rfl⟩ hn + · exact h _ _ _ hg (Or.inr hc) + · exact absurd ⟨rfl, Or.inr rfl⟩ hn + | putExisting => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd + rcases hc with (⟨_, _, hn⟩ | hci | ⟨_, ho⟩ | ⟨_, _, he⟩) | + (⟨_, _, hn⟩ | hci | ⟨_, ho⟩ | ⟨_, _, he⟩) + · exact absurd ⟨rfl, Or.inl rfl⟩ hn + · exact ⟨hci.props.1, hci.props.2.2.2⟩ + · exact (ownership_not_containment ho (Or.inl rfl)).elim + · cases he + · exact absurd ⟨rfl, Or.inr rfl⟩ hn + · exact ⟨hci.props.1, hci.props.2.2.2⟩ + · exact (ownership_not_containment ho (Or.inr rfl)).elim + · cases he + | putNew => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd + rcases hc with (⟨_, _, hn⟩ | hci | ⟨_, _, _, hp, _⟩ | ⟨_, _, he⟩) | + (⟨_, _, hn⟩ | hci | ⟨_, _, _, hp, _⟩ | ⟨_, _, he⟩) + · exact absurd ⟨rfl, Or.inl rfl⟩ hn + · exact ⟨hci.props.1, hci.props.2.2.2⟩ + · rcases hp with hp | hp <;> cases hp + · cases he + · exact absurd ⟨rfl, Or.inr rfl⟩ hn + · exact ⟨hci.props.1, hci.props.2.2.2⟩ + · rcases hp with hp | hp <;> cases hp + · cases he + | @patch x _ g hg _ hkeep => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd + rcases hc with hc | hc + · exact h _ _ _ hg (Or.inl ((hkeep _ (Or.inr ⟨rfl, Or.inl rfl⟩)).1 hc)) + · exact h _ _ _ hg (Or.inr ((hkeep _ (Or.inr ⟨rfl, Or.inr rfl⟩)).1 hc)) + | delete => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd + · rw [hs.frame hdx] at hd + exact h _ _ _ hd hc + +theorem contained_preserved {tr agent st req st'} (hs : Write tr agent st req st') + (h : Contained tr st) : Contained tr st' := by + intro d g' hd hroot + by_cases hdx : d = req.target + · cases hs with + | @post x _ g hg _ => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd + rcases h d g hg hroot with hc | hc + · exact Or.inl (Or.inl hc) + · exact Or.inr (Or.inl hc) + | putExisting => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd + exact containedIn_contains hroot fun _ h => Or.inr (Or.inl h) + | putNew => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd + exact containedIn_contains hroot fun _ h => Or.inr (Or.inl h) + | @patch x _ g hg _ hkeep => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd; subst hd + rcases h d g hg hroot with hc | hc + · exact Or.inl ((hkeep _ (Or.inr ⟨rfl, Or.inl rfl⟩)).2 hc) + · exact Or.inr ((hkeep _ (Or.inr ⟨rfl, Or.inr rfl⟩)).2 hc) + | delete => + simp [Req.target] at hdx; subst hdx; simp [Store.set] at hd + · rw [hs.frame hdx] at hd + exact h d g' hd hroot + +theorem ownTypes_present {st : Store} {x t : Node} (h : ownTypes st x t) : present st x := by + obtain ⟨g, hg, _⟩ := h; exact ⟨g, hg⟩ + +theorem hier_preserved {tr agent st req st'} (hs : Write tr agent st req st') + (h : Hier tr st) (hc : Contained tr st) : Hier tr st' := by + intro d hd hroot + have hm := hs.present_mono + cases hs with + | @delete x _ noChild => + have hdx : d ≠ x := by + rintro rfl; obtain ⟨g, hg⟩ := hd; simp [Store.set] at hg + have hd0 := (present_set_other hdx).1 hd + have hp := h d hd0 hroot + by_cases hpx : tr.parent d = x + · obtain ⟨g, hg⟩ := hd0 + have hcd := hc d g hg hroot + rw [hpx] at hcd + exact absurd ⟨d, g, hdx, hg, hcd⟩ noChild + · exact (present_set_other hpx).2 hp + | @putNew x _ _ _ _ _ _ hpar => + apply hm (by intro _ h; cases h) + by_cases hdx : d = x + · subst hdx; exact hpar hroot + · exact h d ((present_set_other hdx).1 hd) hroot + | @post x _ g hg => + apply hm (by intro _ h; cases h) + by_cases hdx : d = x + · subst hdx; exact h d ⟨_, hg⟩ hroot + · exact h d ((present_set_other hdx).1 hd) hroot + | @putExisting x _ _ g hg => + apply hm (by intro _ h; cases h) + by_cases hdx : d = x + · subst hdx; exact h d ⟨_, hg⟩ hroot + · exact h d ((present_set_other hdx).1 hd) hroot + | @patch x _ g hg => + apply hm (by intro _ h; cases h) + by_cases hdx : d = x + · subst hdx; exact h d ⟨_, hg⟩ hroot + · exact h d ((present_set_other hdx).1 hd) hroot + +theorem roots_preserved {tr agent st req st'} (hs : Write tr agent st req st') + (h : RootsPresent tr st) : RootsPresent tr st' := by + have hm := hs.present_mono + cases hs with + | @delete x hr _ => + intro r hrr + have hrx : r ≠ x := fun e => hr (e ▸ hrr) + exact (present_set_other hrx).2 (h r hrr) + | _ => exact fun r hrr => hm (by intro _ h; cases h) (h r hrr) + +/-- **The invariants hold after every write.** -/ +theorem Write.inv {tr agent st req st'} (hs : Write tr agent st req st') (h : Inv tr st) : + Inv tr st' := + ⟨own_preserved hs h.own, exact_preserved hs h.exact, contained_preserved hs h.contained, + hier_preserved hs h.hier h.contained, roots_preserved hs h.roots⟩ + +/-! ## Typing -/ + +/-- Every document the store has is typed with a hierarchy class. -/ +def Typed (st : Store) : Prop := ∀ x, present st x → ∃ t, ownTypes st x t ∧ hierClass t + +/-- A write types a document with nothing but the classes it had and hierarchy classes. -/ +theorem Write.ownTypes {tr agent st req st'} (hs : Write tr agent st req st') {x c : Node} + (ht : LdhHttp.ownTypes st' x c) : LdhHttp.ownTypes st x c ∨ hierClass c := by + obtain ⟨g', hg', hc⟩ := ht + by_cases hx : x = req.target + · cases hs with + | @post y _ g hg _ hty => + simp [Req.target] at hx; subst hx; simp [Store.set] at hg'; subst hg' + rcases hc with hc | ⟨hc, _⟩ + · exact Or.inl ⟨g, hg, hc⟩ + · exact Or.inr (hty c hc) + | putExisting _ _ _ hty => + simp [Req.target] at hx; subst hx; simp [Store.set] at hg'; subst hg' + rcases hc with ⟨hc, _⟩ | hci | ⟨_, _, hp⟩ | ⟨_, _, he⟩ + · exact Or.inr (hty c hc) + · rcases hci.props.2.2.1 with hp | hp <;> cases hp + · rcases hp with hp | hp <;> cases hp + · cases he; exact Or.inr (Or.inr (Or.inr rfl)) + | putNew _ _ hty => + simp [Req.target] at hx; subst hx; simp [Store.set] at hg'; subst hg' + rcases hc with ⟨hc, _⟩ | hci | ⟨_, _, _, hp, _⟩ | ⟨_, _, he⟩ + · exact Or.inr (hty c hc) + · rcases hci.props.2.2.1 with hp | hp <;> cases hp + · rcases hp with hp | hp <;> cases hp + · cases he; exact Or.inr (Or.inr (Or.inr rfl)) + | @patch y _ g hg _ _ hty => + simp [Req.target] at hx; subst hx; simp [Store.set] at hg'; subst hg' + rcases hty c hc with hc | hc + · exact Or.inl ⟨g, hg, hc⟩ + · exact Or.inr hc + | delete => + simp [Req.target] at hx; subst hx; simp [Store.set] at hg' + · exact Or.inl ⟨g', by rw [← hs.frame hx]; exact hg', hc⟩ + +theorem set_self {st : Store} {x : Node} {v : Option Graph} : st.set x v x = v := by simp [Store.set] + +/-- What a `PUT` stores types the document with a hierarchy class: the payload's, or the `dh:Item` `put()` adds. -/ +theorem put_typed {tr : Tree} {st : Store} {x : Node} {payload G : Graph} + (hroot : tr.isRoot x → TypedBy x payload) + (hG : ∀ t, (payload t ∧ ¬ ownership x t ∧ ¬ containment x t) ∨ itemTyped tr x payload t → G t) : + ∃ c, ownTypes (st.set x (some G)) x c ∧ hierClass c := by + have hno : ∀ c, ¬ ownership x ⟨x, .rdfType, c⟩ ∧ ¬ containment x ⟨x, .rdfType, c⟩ := by + intro c; constructor <;> rintro ⟨_, hp | hp⟩ <;> cases hp + by_cases hr : tr.isRoot x + · obtain ⟨c, hc, hh⟩ := hroot hr + exact ⟨c, ⟨_, set_self, hG _ (Or.inl ⟨hc, hno c⟩)⟩, hh⟩ + · by_cases hk : payload ⟨x, .rdfType, .dhContainer⟩ + · exact ⟨_, ⟨_, set_self, hG _ (Or.inl ⟨hk, hno _⟩)⟩, Or.inr (Or.inl rfl)⟩ + · exact ⟨_, ⟨_, set_self, hG _ (Or.inr ⟨hr, hk, rfl⟩)⟩, Or.inr (Or.inr rfl)⟩ + +/-- **Every document stays typed with a hierarchy class.** -/ +theorem Write.typed {tr agent st req st'} (hs : Write tr agent st req st') (h : Typed st) : + Typed st' := by + intro x hx + by_cases hxt : x = req.target + · cases hs with + | @post y _ g hg => + simp [Req.target] at hxt; subst hxt + obtain ⟨c, ⟨g0, hg0, hc⟩, hh⟩ := h x ⟨g, hg⟩ + rw [hg] at hg0; cases hg0 + exact ⟨c, ⟨_, set_self, Or.inl hc⟩, hh⟩ + | @putExisting y payload _ g _ _ _ _ hroot => + simp [Req.target] at hxt; subst hxt + exact put_typed hroot fun t ht => ht.elim Or.inl fun ht => Or.inr (Or.inr (Or.inr ht)) + | @putNew y payload _ _ _ _ hroot => + simp [Req.target] at hxt; subst hxt + exact put_typed hroot fun t ht => ht.elim Or.inl fun ht => Or.inr (Or.inr (Or.inr ht)) + | @patch y after _ _ _ _ _ htb => + simp [Req.target] at hxt; subst hxt + obtain ⟨c, hc, hh⟩ := htb + exact ⟨c, ⟨_, set_self, hc⟩, hh⟩ + | delete => + simp [Req.target] at hxt; subst hxt + obtain ⟨g, hg⟩ := hx; simp [Store.set] at hg + · obtain ⟨g, hg⟩ := hx + rw [hs.frame hxt] at hg + obtain ⟨c, ⟨g0, hg0, hc⟩, hh⟩ := h x ⟨g, hg⟩ + exact ⟨c, ⟨g0, by rw [hs.frame hxt]; exact hg0, hc⟩, hh⟩ + +/-! ## Ownership -/ + +/-- **Ownership confinement.** Whoever owns a document after a write owned it before, or created it with +that write. -/ +theorem Write.owner_confined {tr agent st req st'} (hs : Write tr agent st req st') + {y b : Node} (ho : owner st' y b) : + owner st y b ∨ (y = req.target ∧ st y = none ∧ agent = some b) := by + by_cases hy : y = req.target + · subst hy + cases hs with + | post hg => + obtain ⟨g', hg', hb⟩ := ho + simp [Store.set, Req.target] at hg' + subst hg' + rcases hb with hb | ⟨_, hno, _⟩ + · exact Or.inl ⟨_, hg, hb⟩ + · exact absurd ⟨rfl, Or.inl rfl⟩ hno + | putExisting hg _ => + obtain ⟨g', hg', hb⟩ := ho + simp [Store.set, Req.target] at hg' + subst hg' + rcases hb with ⟨_, hno, _⟩ | hci | ⟨hb, _⟩ | ⟨_, _, he⟩ + · exact absurd ⟨rfl, Or.inl rfl⟩ hno + · rcases hci.props.2.2.1 with hp | hp <;> cases hp + · exact Or.inl ⟨_, hg, hb⟩ + · cases he + | putNew hn => + obtain ⟨g', hg', hb⟩ := ho + simp [Store.set, Req.target] at hg' + subst hg' + rcases hb with ⟨_, hno, _⟩ | hci | ⟨a, ha, _, _, hab⟩ | ⟨_, _, he⟩ + · exact absurd ⟨rfl, Or.inl rfl⟩ hno + · rcases hci.props.2.2.1 with hp | hp <;> cases hp + · simp at hab; subst hab + exact Or.inr ⟨rfl, hn, ha⟩ + · cases he + | patch hg _ hkeep => + obtain ⟨g', hg', hb⟩ := ho + simp [Store.set, Req.target] at hg' + subst hg' + exact Or.inl ⟨_, hg, (hkeep _ (Or.inl ⟨rfl, Or.inl rfl⟩)).1 hb⟩ + | delete => + obtain ⟨g', hg', _⟩ := ho + simp [Store.set, Req.target] at hg' + · obtain ⟨g, hg, hb⟩ := ho + exact Or.inl ⟨g, by rw [← hs.frame hy]; exact hg, hb⟩ + +end LdhHttp diff --git a/formal/http/Main.lean b/formal/http/Main.lean new file mode 100644 index 000000000..2af81136f --- /dev/null +++ b/formal/http/Main.lean @@ -0,0 +1,132 @@ +/- +`ldh-http`: the graph store's answer of `LdhHttp.Answer` over a live instance's datasets, with no authorization in +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` +and `DELETE`, and `PRECONDITION` one of `none`, `current` (`If-Match` with the current entity tag), `stale` +(`If-Match` with another) and `absent` (`If-None-Match: *`). The body of a `POST` or `PUT` is the `--payload` +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 + +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 + | some (rest, f) => parseArgs rest { a with request := some f } + | none => .error s!"unknown argument: {arg}" + +def usage : String := + "usage: ldh-http --dataset DATASET.nq... --request REQUEST.tsv " ++ + "[--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 := {} + let mut triples : Array (Node × Triple) := #[] + for path in args.datasets do + let (ts, i') := internQuads i (← readQuads path) + i := i' + triples := triples ++ ts + let r ← match ← loadRequest i files with + | .ok r => pure r + | .error e => IO.eprintln e; return 2 + let (status, fs') := respondB r.hs (toFinStore triples) r.agent r.pc r.req + printAnswer r.interner status fs' r.req.target + return 0 diff --git a/formal/http/README.md b/formal/http/README.md new file mode 100644 index 000000000..827703094 --- /dev/null +++ b/formal/http/README.md @@ -0,0 +1,174 @@ +# 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, 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. + +The model is a specification. It is not extracted from the Java: each definition is transcribed from the code +listed in the mapping below, and when that code changes, the definition changes in the same commit. + +## Building + +```bash +cd formal/http +lake build +``` + +Lean `v4.15.0` (pinned in `lean-toolchain`), core library only, with no Mathlib. + +The `Formal` workflow builds the model on every push, fails on a `sorry`, and on a pull request runs +`tracks-code.sh`, which fails when a source listed under "Mapping to the code" changes without a change in this +directory. `web.xml` counts only through `childQuery`. Run it locally against the branch point: + +```bash +formal/http/tracks-code.sh origin/develop +``` + +## Files + +| File | Contents | +|------|----------| +| `LdhHttp/Base.lean` | The store (one named graph per document), the document hierarchy, own-graph lookups and requests | +| `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, and the TimeGate's choice over a history | + +## The model + +- **Documents:** one named graph per document, named by the document's URI. The default graph is empty and not + modelled. A document exists when its graph does. +- **The hierarchy (`Tree`):** the URI parent `put()` resolves, and the roots, the documents with none. +- **The write rule:** a graph written for `x` may state `sioc:has_parent` or `sioc:has_container` of `x` only. + `PUT` asserts the containment itself: `sioc:has_parent` of a container, `sioc:has_container` of anything else. +- **The type rule:** a graph written for `x` may type `x` with the hierarchy classes (`def:Root`, `dh:Container`, + `dh:Item`) only, and leaves it typed with one: `PUT` adds `dh:Item` to a non-root document that is not a container, + a `PUT` of the root must carry the type itself, and a `PATCH` may keep the types it finds, add hierarchy classes and + not drop the last of them. +- **Ownership:** `acl:owner` and `dct:creator` of a document are the server's: a new document gets the agent's, an + existing one keeps its own, and a `PATCH` cannot change them. +- **Creation:** a document is created only below a parent the store has (`409`, checked under the parent's lock). +- **The answer (`Answer.lean`):** each method's checks in the order the graph store makes them: the methods a + 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 + +| Lean | Code | +|------|------| +| `Write.post`, `Write.putExisting`, `Write.putNew`, `Write.patch`, `Write.delete` | `DocumentHierarchyGraphStoreImpl.post`, `put`, `patch`, `delete` | +| `NoForeign` | `getForeignContainment`, `checkForeignContainment` | +| `hierClass`, `HierTypes`, `TypedBy` | `HIERARCHY_CLASSES`, `getForeignTypes`, `isHierarchyTyped`, `checkDocumentTypes`, and their checks in `put` (the root) and `patch` | +| `containedIn`, `itemTyped` | the `sioc:has_parent` or `sioc:has_container`, and the `dh:Item`, that `put` asserts | +| `ownership`, `containment` | `removeOwnership`, `isOwnershipChanged`, `removeContainment`, `isContainmentChanged` | +| `hasChild` | `childQuery` (`web.xml`), `hasChild` | +| `Write.putNew`'s parent | `put`'s `409` for a parent that does not exist | +| `readB` | `get()`, and the store client's `404` for a graph it does not have | +| `postB`, `putB`, `patchB`, `deleteB`, `deleteChecked` | `DocumentHierarchyGraphStoreImpl.post`, `put`, `patch`, `delete`, in their order of checks; `delete`'s `404` is Core's `GraphStoreBase.delete` | +| `precondFails` | `evaluatePreconditions`: `428` without `If-Match` or `If-None-Match: *`, and Core's evaluation of either | +| `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 | +| `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 + +Proven with no `sorry`, using only the axioms `propext`, `Quot.sound` and, through case splits on presence, +`Classical.choice`: + +| Theorem | Statement | +|---------|-----------| +| `Write.inv` | The containment rule, exact containment, the hierarchy and the roots hold after every write | +| `Write.typed` | After every write, every document is still typed with a hierarchy class | +| `Write.ownTypes` | A write types a document with nothing but the classes it had and hierarchy classes | +| `Write.owner_confined` | Whoever owns a document after a write owned it before, or created it with that write | +| `respond_refused` | A refused request leaves the store as it was | +| `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 model + +`ldh-http` runs the answer on N-Quads dumps of the stores: + +```bash +lake build +.lake/build/bin/ldh-http --dataset end-user.nq --dataset admin.nq --request request.tsv --payload payload.nt +``` + +A request is `AGENTMETHODDOCUMENTPRECONDITION`, with the precondition `none`, `current` or `stale` +(`If-Match` with the current entity tag or another) or `absent` (`If-None-Match: *`); the body of a `POST` or `PUT` +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. 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 + +- **Concurrency:** writes are sequential. Under the locks, a `PUT` holds its parent's lock as well as its own and + re-checks that the parent exists, and a `DELETE` checks for children; the model does not prove that + serialisation. +- **Other server work:** constraint validation, parsing, skolemization, dates, imports, uploads, content + negotiation, conditional `GET` and caching. A write refused for its body, such as one with a malformed IRI or a + 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`. +- **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/lake-manifest.json b/formal/http/lake-manifest.json new file mode 100644 index 000000000..5315cf3a3 --- /dev/null +++ b/formal/http/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "LdhHttp", + "lakeDir": ".lake"} diff --git a/formal/http/lakefile.lean b/formal/http/lakefile.lean new file mode 100644 index 000000000..7d1d2dcbd --- /dev/null +++ b/formal/http/lakefile.lean @@ -0,0 +1,15 @@ +import Lake +open Lake DSL + +package LdhHttp where + -- ld64 in the pinned toolchain emits a __DATA_CONST segment that dyld on macOS 26 and later refuses to load + -- ("missing SG_READ_ONLY flag"); not creating the segment sidesteps it. GNU ld knows no such flag + moreLinkArgs := if System.Platform.isOSX then #["-Wl,-no_data_const"] else #[] + +@[default_target] +lean_lib LdhHttp + +/-- The graph store's answer over a live instance's datasets: see `Main.lean`. -/ +@[default_target] +lean_exe «ldh-http» where + root := `Main diff --git a/formal/http/lean-toolchain b/formal/http/lean-toolchain new file mode 100644 index 000000000..d0eb99ff6 --- /dev/null +++ b/formal/http/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.15.0 diff --git a/formal/http/tracks-code.sh b/formal/http/tracks-code.sh new file mode 100755 index 000000000..3622a8b56 --- /dev/null +++ b/formal/http/tracks-code.sh @@ -0,0 +1,51 @@ +#!/usr/bin/env bash +# The Lean model of the graph store is transcribed by hand from the code listed under "Mapping to the code" in +# README.md. +# This fails when a commit range changes one of those sources without touching the model, so the +# transcription cannot drift silently: either the definitions change in the same commit, or the README +# says why they do not. +# +# Usage: tracks-code.sh [] (head defaults to HEAD; the range starts at their merge base) +set -euo pipefail + +head=${2:-HEAD} +base=$(git merge-base "$1" "$head") +cd "$(git rev-parse --show-toplevel)" +model=formal/http +web_xml=src/main/webapp/WEB-INF/web.xml +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) + +changed=() +while IFS= read -r file; do + [ -n "$file" ] && changed+=("$file") +done < <(git diff --name-only "$base" "$head" -- "${sources[@]}") + +query_text() { # + git show "$1:$web_xml" | xmllint --xpath "string(//*[local-name()='context-param'][*[local-name()='param-name']='$config$2']/*[local-name()='param-value'])" - +} +for query in "${queries[@]}"; do + if [ "$(query_text "$base" "$query")" != "$(query_text "$head" "$query")" ]; then + changed+=("$web_xml ($query)") + fi +done + +[ ${#changed[@]} -eq 0 ] && exit 0 +[ -n "$(git diff --name-only "$base" "$head" -- "$model")" ] && exit 0 + +{ + echo "$model transcribes these sources, and $(git rev-parse --short "$base")..$(git rev-parse --short "$head") changes them without touching the model:" + printf ' %s\n' "${changed[@]}" + echo "Change the matching definitions in $model in the same commit, or record in $model/README.md why they stand." +} >&2 +exit 1 diff --git a/plugins/ldh/.claude-plugin/plugin.json b/plugins/ldh/.claude-plugin/plugin.json index f38008983..e8f025c69 100644 --- a/plugins/ldh/.claude-plugin/plugin.json +++ b/plugins/ldh/.claude-plugin/plugin.json @@ -1,7 +1,7 @@ { "name": "ldh", "displayName": "LinkedDataHub", - "version": "6.3.0", + "version": "6.3.1-SNAPSHOT", "description": "Build Linked Data dataspaces, datasets and applications on LinkedDataHub with the ldh CLI: provision a dataspace, model and import data, declare documents, views and charts, and write reusable packages", "author": { "name": "AtomGraph", diff --git a/plugins/ldh/skills/app/SKILL.md b/plugins/ldh/skills/app/SKILL.md index 5aae6a794..feb658ab5 100644 --- a/plugins/ldh/skills/app/SKILL.md +++ b/plugins/ldh/skills/app/SKILL.md @@ -205,7 +205,9 @@ Finer access control: `ldh admin create group`, `ldh admin add agent`, `ldh admi (https://docs.linkeddatahub.com/reference/administration/acl/). An authorization names documents with `--to`, and a subtree with `--default `, which covers every document below the container. `--to-all-in` takes a class, but not a document class (`dh:Item`, `dh:Container`, `def:Root` or one -above them), which the admin refuses: those classes are shared with the admin documents. +above them), which the admin refuses: those classes are shared with the admin documents. A document is +typed with those classes and no other (a write that types it otherwise gets `422`), so a class grant +reaches uploaded files (`nfo:FileDataObject`) only; grant documents with `--to` and `--default`. ## Building incrementally instead diff --git a/pom.xml b/pom.xml index d46e8951c..2482f31fa 100644 --- a/pom.xml +++ b/pom.xml @@ -3,7 +3,7 @@ com.atomgraph linkeddatahub - 6.3.0 + 6.3.1-SNAPSHOT ${packaging.type} AtomGraph LinkedDataHub @@ -46,7 +46,7 @@ https://github.com/AtomGraph/LinkedDataHub scm:git:git://github.com/AtomGraph/LinkedDataHub.git scm:git:git@github.com:AtomGraph/LinkedDataHub.git - linkeddatahub-6.3.0 + HEAD diff --git a/rdf/pom.xml b/rdf/pom.xml index 13e4c49c2..ddd51ee55 100644 --- a/rdf/pom.xml +++ b/rdf/pom.xml @@ -4,7 +4,7 @@ com.atomgraph linkeddatahub-rdf - 6.3.0 + 6.3.1-SNAPSHOT jar LinkedDataHub RDF diff --git a/src/main/java/com/atomgraph/linkeddatahub/server/factory/ApplicationFactory.java b/src/main/java/com/atomgraph/linkeddatahub/server/factory/ApplicationFactory.java index 784572993..ac4c3b592 100644 --- a/src/main/java/com/atomgraph/linkeddatahub/server/factory/ApplicationFactory.java +++ b/src/main/java/com/atomgraph/linkeddatahub/server/factory/ApplicationFactory.java @@ -58,7 +58,10 @@ public void dispose(Optional getDataspace() { - return (Optional)getContainerRequestContext().getProperty(LDS.Dataspace.getURI()); + Optional appOpt = (Optional)getContainerRequestContext().getProperty(LDS.Dataspace.getURI()); + + // the property is absent when a filter before the one setting it refused the request; never provide null, which the request scope caches and then refuses to seed again on the next lookup + return appOpt != null ? appOpt : Optional.empty(); } /** diff --git a/src/main/java/com/atomgraph/linkeddatahub/server/factory/DatasetFactory.java b/src/main/java/com/atomgraph/linkeddatahub/server/factory/DatasetFactory.java index f7f9d4375..f1881280a 100644 --- a/src/main/java/com/atomgraph/linkeddatahub/server/factory/DatasetFactory.java +++ b/src/main/java/com/atomgraph/linkeddatahub/server/factory/DatasetFactory.java @@ -59,7 +59,10 @@ public void dispose(Optional t) */ public Optional getDataset() { - return (Optional)getContainerRequestContext().getProperty(LDS.Dataset.getURI()); + Optional datasetOpt = (Optional)getContainerRequestContext().getProperty(LDS.Dataset.getURI()); + + // the property is absent when a filter before the one setting it refused the request; never provide null, which the request scope caches and then refuses to seed again on the next lookup + return datasetOpt != null ? datasetOpt : Optional.empty(); } /** diff --git a/src/main/java/com/atomgraph/linkeddatahub/server/factory/OntologyFactory.java b/src/main/java/com/atomgraph/linkeddatahub/server/factory/OntologyFactory.java index 8fc56c6a2..fed3043d0 100644 --- a/src/main/java/com/atomgraph/linkeddatahub/server/factory/OntologyFactory.java +++ b/src/main/java/com/atomgraph/linkeddatahub/server/factory/OntologyFactory.java @@ -54,7 +54,10 @@ public void dispose(Optional t) */ public Optional getOntology() { - return (Optional)getContainerRequestContext().getProperty(OWL.Ontology.getURI()); + Optional ontologyOpt = (Optional)getContainerRequestContext().getProperty(OWL.Ontology.getURI()); + + // the property is absent when a filter before the one setting it refused the request; never provide null, which the request scope caches and then refuses to seed again on the next lookup + return ontologyOpt != null ? ontologyOpt : Optional.empty(); } /** diff --git a/src/main/java/com/atomgraph/linkeddatahub/server/factory/ServiceFactory.java b/src/main/java/com/atomgraph/linkeddatahub/server/factory/ServiceFactory.java index 4326c5a4c..2706d4406 100644 --- a/src/main/java/com/atomgraph/linkeddatahub/server/factory/ServiceFactory.java +++ b/src/main/java/com/atomgraph/linkeddatahub/server/factory/ServiceFactory.java @@ -61,7 +61,7 @@ public Optional getService() { Optional appOpt = (Optional)getContainerRequestContext().getProperty(LDS.Dataspace.getURI()); - if (!appOpt.isPresent()) return Optional.empty(); + if (appOpt == null || !appOpt.isPresent()) return Optional.empty(); // absent when a filter before ApplicationFilter refused the request Service service = appOpt.get().getService(); diff --git a/src/main/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImpl.java b/src/main/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImpl.java index c9e762d9c..3158de62e 100644 --- a/src/main/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImpl.java +++ b/src/main/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImpl.java @@ -37,6 +37,7 @@ import com.atomgraph.linkeddatahub.server.util.Skolemizer; import com.atomgraph.linkeddatahub.vocabulary.ACL; import com.atomgraph.linkeddatahub.vocabulary.DH; +import com.atomgraph.linkeddatahub.vocabulary.Default; import com.atomgraph.linkeddatahub.vocabulary.LDH; import com.atomgraph.linkeddatahub.vocabulary.NFO; import com.atomgraph.linkeddatahub.vocabulary.SIOC; @@ -186,6 +187,13 @@ public class DocumentHierarchyGraphStoreImpl extends com.atomgraph.core.model.im * Name of the Graph Store Protocol query parameter that identifies the default graph indirectly. */ public static final String DEFAULT_PARAM_NAME = "default"; + + /** + * The classes of the document hierarchy, the only ones a document may be typed with: a class grant matches a + * document's types, and the documents of both dataspaces share these, so a document typed with any other class + * could be reached by a grant scoped to the other dataspace. + */ + public static final Set HIERARCHY_CLASSES = Set.of(Default.Root, DH.Container, DH.Item); private final com.atomgraph.linkeddatahub.dataspaces.model.Dataspace application; private final OntModel ontology; @@ -450,6 +458,7 @@ protected Response post(Model model, Runnable beforeWrite) if (model.isEmpty()) return Response.noContent().build(); checkForeignContainment(model); + checkDocumentTypes(model); return writeLocked(() -> { @@ -552,9 +561,13 @@ protected Response put(Model model, Runnable beforeWrite) } checkForeignContainment(model); + checkDocumentTypes(model); URI parentURI = getURI().resolve(".."); boolean root = getDataspace().getBaseURI().equals(getURI()); + // the root is stored as sent, without the dh:Item every other document is given below + if (root && !isHierarchyTyped(model, getURI().toString())) + throw new WebApplicationException("Root document <" + getURI() + "> must be typed with a document hierarchy class", UNPROCESSABLE_ENTITY.getStatusCode()); // the parent's lock as well as the document's: a DELETE of the parent holds it while it checks for children, so // the two cannot interleave return writeLocked(root ? List.of(getURI()) : List.of(parentURI, getURI()), () -> @@ -724,6 +737,12 @@ public Response patch(UpdateRequest updateRequest) if (getForeignContainment(existingModel, getURI().toString()).stream().anyMatch(stmt -> !beforeUpdateModel.contains(stmt))) throw new WebApplicationException("sioc:has_parent and sioc:has_container in document <" + getURI() + "> can only be stated of the document itself", UNPROCESSABLE_ENTITY.getStatusCode()); + // only the types the update adds are held to the rule: a graph written before it may still carry others + if (getForeignTypes(existingModel, getURI().toString()).stream().anyMatch(type -> !beforeUpdateModel.contains(beforeUpdateModel.createResource(getURI().toString()), RDF.type, type))) + throw new WebApplicationException("Document <" + getURI() + "> can only be typed with document hierarchy classes", UNPROCESSABLE_ENTITY.getStatusCode()); + if (!isHierarchyTyped(existingModel, getURI().toString())) + throw new WebApplicationException("Document <" + getURI() + "> must stay typed with a document hierarchy class", UNPROCESSABLE_ENTITY.getStatusCode()); + // SPIN constraints are class-scoped; allowing rdf:type removal would silently bypass them for (Resource resource : getChangedResources(beforeUpdateModel, existingModel)) { @@ -1057,6 +1076,54 @@ public void checkForeignContainment(Model model) throw new WebApplicationException("sioc:has_parent and sioc:has_container in document <" + getURI() + "> can only be stated of the document itself", UNPROCESSABLE_ENTITY.getStatusCode()); } + /** + * Returns the classes the model types the document with that are not document hierarchy classes. + * + * @param model RDF model + * @param documentURI document URI + * @return non-hierarchy types of the document + */ + public static Set getForeignTypes(Model model, String documentURI) + { + if (model == null) throw new IllegalArgumentException("Model cannot be null"); + if (documentURI == null) throw new IllegalArgumentException("Document URI cannot be null"); + + Set types = new HashSet<>(); + model.listObjectsOfProperty(ResourceFactory.createResource(documentURI), RDF.type). + filterDrop(HIERARCHY_CLASSES::contains). + forEach(types::add); + + return types; + } + + /** + * Returns true if the model types the document with a document hierarchy class. + * + * @param model RDF model + * @param documentURI document URI + * @return true if typed with a hierarchy class + */ + public static boolean isHierarchyTyped(Model model, String documentURI) + { + if (model == null) throw new IllegalArgumentException("Model cannot be null"); + if (documentURI == null) throw new IllegalArgumentException("Document URI cannot be null"); + + Resource document = ResourceFactory.createResource(documentURI); + return HIERARCHY_CLASSES.stream().anyMatch(type -> model.contains(document, RDF.type, type)); + } + + /** + * Refuses a payload that types the requested document with any class but the document hierarchy classes. + * + * @param model request payload + * @throws WebApplicationException with 422 Unprocessable Entity if it does + */ + public void checkDocumentTypes(Model model) + { + if (!getForeignTypes(model, getURI().toString()).isEmpty()) + throw new WebApplicationException("Document <" + getURI() + "> can only be typed with document hierarchy classes", UNPROCESSABLE_ENTITY.getStatusCode()); + } + private static boolean isChanged(Model beforeUpdateModel, Model afterUpdateModel, String documentURI, List properties) { if (beforeUpdateModel == null) throw new IllegalArgumentException("Model before update cannot be null"); diff --git a/src/main/java/com/atomgraph/linkeddatahub/writer/factory/SourceResolverFactory.java b/src/main/java/com/atomgraph/linkeddatahub/writer/factory/SourceResolverFactory.java index bc45d0a1f..2f7b248e9 100644 --- a/src/main/java/com/atomgraph/linkeddatahub/writer/factory/SourceResolverFactory.java +++ b/src/main/java/com/atomgraph/linkeddatahub/writer/factory/SourceResolverFactory.java @@ -157,7 +157,10 @@ public ContainerRequestContext getContainerRequestContext() */ public Optional getDataspace() { - return (Optional)getContainerRequestContext().getProperty(LDS.Dataspace.getURI()); + Optional appOpt = (Optional)getContainerRequestContext().getProperty(LDS.Dataspace.getURI()); + + // the property is absent when the request was refused before it was set; the error response is still written through XSLT, which needs a resolver + return appOpt != null ? appOpt : Optional.empty(); } } \ No newline at end of file diff --git a/src/main/webapp/static/com/atomgraph/linkeddatahub/xsl/client/block/chart.xsl b/src/main/webapp/static/com/atomgraph/linkeddatahub/xsl/client/block/chart.xsl index 8107a9fe5..02178b545 100644 --- a/src/main/webapp/static/com/atomgraph/linkeddatahub/xsl/client/block/chart.xsl +++ b/src/main/webapp/static/com/atomgraph/linkeddatahub/xsl/client/block/chart.xsl @@ -431,7 +431,11 @@ exclude-result-prefixes="#all" - + + + + @@ -447,7 +451,10 @@ exclude-result-prefixes="#all" - + + + + diff --git a/src/main/webapp/static/com/atomgraph/linkeddatahub/xsl/client/functions.xsl b/src/main/webapp/static/com/atomgraph/linkeddatahub/xsl/client/functions.xsl index 18bb803b9..0ce5a47db 100644 --- a/src/main/webapp/static/com/atomgraph/linkeddatahub/xsl/client/functions.xsl +++ b/src/main/webapp/static/com/atomgraph/linkeddatahub/xsl/client/functions.xsl @@ -373,33 +373,23 @@ exclude-result-prefixes="#all" + - - + + - - - - - - - - - - - - - - - - - - + + + + + + @@ -407,16 +397,17 @@ exclude-result-prefixes="#all" + - - + - + diff --git a/src/test/java/com/atomgraph/linkeddatahub/server/factory/ApplicationFactoryRequestScopeTest.java b/src/test/java/com/atomgraph/linkeddatahub/server/factory/ApplicationFactoryRequestScopeTest.java new file mode 100644 index 000000000..5c5d172dc --- /dev/null +++ b/src/test/java/com/atomgraph/linkeddatahub/server/factory/ApplicationFactoryRequestScopeTest.java @@ -0,0 +1,154 @@ +/** + * Copyright 2026 Martynas Jusevičius + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * + */ +package com.atomgraph.linkeddatahub.server.factory; + +import com.atomgraph.linkeddatahub.dataspaces.model.Dataspace; +import com.atomgraph.linkeddatahub.vocabulary.LDS; +import jakarta.annotation.Priority; +import jakarta.inject.Inject; +import jakarta.ws.rs.BadRequestException; +import jakarta.ws.rs.GET; +import jakarta.ws.rs.Path; +import jakarta.ws.rs.container.ContainerRequestContext; +import jakarta.ws.rs.container.ContainerRequestFilter; +import jakarta.ws.rs.container.ContainerResponseContext; +import jakarta.ws.rs.container.ContainerResponseFilter; +import jakarta.ws.rs.container.PreMatching; +import java.net.URI; +import java.util.List; +import java.util.Optional; +import org.glassfish.hk2.api.TypeLiteral; +import org.glassfish.hk2.utilities.binding.AbstractBinder; +import org.glassfish.jersey.internal.MapPropertiesDelegate; +import org.glassfish.jersey.process.internal.RequestScoped; +import org.glassfish.jersey.server.ApplicationHandler; +import org.glassfish.jersey.server.ContainerRequest; +import org.glassfish.jersey.server.ContainerResponse; +import org.glassfish.jersey.server.ResourceConfig; +import org.junit.jupiter.api.Test; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.mockito.Mockito.mock; + +/** + * Tests that {@link ApplicationFactory} provides an empty dataspace, not null, when a request is refused before + * ApplicationFilter sets it. The request scope caches whatever the factory provides, but takes a cached + * null for a missing instance, so the second lookup in the same request failed with IllegalStateException + * ("already seeded in this scope") and turned the refusal into a 500. Crawlers requesting + * ?accept=application%2Frdf+xml, whose unencoded + decodes to a space, hit it about 2,500 + * times a day on linkeddatahub.com. + * + * @author Martynas Jusevičius {@literal } + */ +public class ApplicationFactoryRequestScopeTest +{ + + private static final URI BASE_URI = URI.create("https://localhost:4443/"); + private static final String REFUSE_HEADER = "X-Refuse"; + private static final String DATASPACE_HEADER = "X-Dataspace"; + + @Path("/") + public static class RootResource + { + + @GET + public String get() + { + return "root"; + } + + } + + /** + * Stands in for ApplicationFilter: refuses the request before setting the dataspace when asked to, + * like its setAccept() does for a malformed accept parameter. + */ + @PreMatching + @Priority(700) + public static class DataspaceFilter implements ContainerRequestFilter + { + + @Override + public void filter(ContainerRequestContext request) + { + if (request.getHeaderString(REFUSE_HEADER) != null) throw new BadRequestException("Refused before the dataspace was set"); + + request.setProperty(LDS.Dataspace.getURI(), Optional.of(mock(Dataspace.class))); + } + + } + + /** + * Stands in for the response filters that each look the dataspace up, ResponseHeadersFilter and + * XkeyTaggingFilter: the second lookup of a request is the one that used to fail. + */ + public static class DataspaceLookupFilter implements ContainerResponseFilter + { + + @Inject jakarta.inject.Provider> app; + + @Override + public void filter(ContainerRequestContext request, ContainerResponseContext response) + { + response.getHeaders().add(DATASPACE_HEADER, app.get().isPresent() ? "present" : "empty"); + } + + } + + @Priority(100) + public static class FirstLookupFilter extends DataspaceLookupFilter {} + + @Priority(200) + public static class SecondLookupFilter extends DataspaceLookupFilter {} + + private ContainerResponse get(boolean refuse) throws Exception + { + ResourceConfig config = new ResourceConfig(RootResource.class, DataspaceFilter.class, FirstLookupFilter.class, SecondLookupFilter.class); + config.register(new AbstractBinder() + { + @Override + protected void configure() + { + bindFactory(ApplicationFactory.class).to(new TypeLiteral>() {}). + in(RequestScoped.class); + } + }); + + ContainerRequest request = new ContainerRequest(BASE_URI, BASE_URI, "GET", null, new MapPropertiesDelegate(), null); + if (refuse) request.header(REFUSE_HEADER, "true"); + + return new ApplicationHandler(config).apply(request).get(); + } + + @Test + public void refusedRequestKeepsItsStatus() throws Exception + { + ContainerResponse response = get(true); + + assertEquals(400, response.getStatus()); + assertEquals(List.of("empty", "empty"), response.getHeaders().get(DATASPACE_HEADER)); + } + + @Test + public void matchedRequestSeesTheDataspaceTwice() throws Exception + { + ContainerResponse response = get(false); + + assertEquals(200, response.getStatus()); + assertEquals(List.of("present", "present"), response.getHeaders().get(DATASPACE_HEADER)); + } + +} diff --git a/src/test/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImplTest.java b/src/test/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImplTest.java index 2b19536c6..e4c2cd9b5 100644 --- a/src/test/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImplTest.java +++ b/src/test/java/com/atomgraph/linkeddatahub/server/model/impl/DocumentHierarchyGraphStoreImplTest.java @@ -21,6 +21,8 @@ import com.atomgraph.linkeddatahub.model.impl.CSVImportImpl; import com.atomgraph.linkeddatahub.model.impl.RDFImportImpl; import com.atomgraph.linkeddatahub.vocabulary.ACL; +import com.atomgraph.linkeddatahub.vocabulary.DH; +import com.atomgraph.linkeddatahub.vocabulary.Default; import com.atomgraph.linkeddatahub.vocabulary.LDH; import com.atomgraph.linkeddatahub.vocabulary.PROV; import com.atomgraph.linkeddatahub.vocabulary.SIOC; @@ -287,6 +289,67 @@ public void testForeignContainmentNullModel() assertThrows(IllegalArgumentException.class, () -> DocumentHierarchyGraphStoreImpl.getForeignContainment(null, DOC.toString())); } + // getForeignTypes(), isHierarchyTyped() + + @Test + public void testForeignTypesIgnoresHierarchyClasses() + { + Model model = ModelFactory.createDefaultModel(); + model.createResource(DOC.toString()). + addProperty(RDF.type, Default.Root). + addProperty(RDF.type, DH.Container). + addProperty(RDF.type, DH.Item); + + assertTrue(DocumentHierarchyGraphStoreImpl.getForeignTypes(model, DOC.toString()).isEmpty()); + } + + @Test + public void testForeignTypesFindsOtherClass() + { + Model model = ModelFactory.createDefaultModel(); + Resource foo = model.createResource("http://localhost/ns#Foo"); + model.createResource(DOC.toString()). + addProperty(RDF.type, DH.Item). + addProperty(RDF.type, foo); + + assertEquals(Set.of(foo), DocumentHierarchyGraphStoreImpl.getForeignTypes(model, DOC.toString())); + } + + @Test + public void testForeignTypesIgnoresOtherSubjects() + { + Model model = ModelFactory.createDefaultModel(); + model.createResource(DOC.toString() + "#thing").addProperty(RDF.type, model.createResource("http://localhost/ns#Foo")); + model.createResource().addProperty(RDF.type, model.createResource("http://localhost/ns#Foo")); + + assertTrue(DocumentHierarchyGraphStoreImpl.getForeignTypes(model, DOC.toString()).isEmpty()); + } + + @Test + public void testForeignTypesNullModel() + { + assertThrows(IllegalArgumentException.class, () -> DocumentHierarchyGraphStoreImpl.getForeignTypes(null, DOC.toString())); + } + + @Test + public void testHierarchyTyped() + { + Model model = ModelFactory.createDefaultModel(); + model.createResource(DOC.toString()).addProperty(RDF.type, DH.Item); + + assertTrue(DocumentHierarchyGraphStoreImpl.isHierarchyTyped(model, DOC.toString())); + } + + @Test + public void testHierarchyTypedOtherClassOnly() + { + Model model = ModelFactory.createDefaultModel(); + model.createResource(DOC.toString()).addProperty(RDF.type, model.createResource("http://localhost/ns#Foo")); + model.createResource(DOC.toString() + "#thing").addProperty(RDF.type, DH.Item); + + assertFalse(DocumentHierarchyGraphStoreImpl.isHierarchyTyped(model, DOC.toString())); + } + // getLastModified(Resource) @Test 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/admin/acl/class-authorization-admin-typed.sh b/tests/http/admin/acl/class-authorization-admin-typed.sh new file mode 100755 index 000000000..75e659bba --- /dev/null +++ b/tests/http/admin/acl/class-authorization-admin-typed.sh @@ -0,0 +1,76 @@ +#!/usr/bin/env bash +set -euo pipefail + +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 + +# A class grant reaches a document through the classes the document's own graph types it with. Admin documents are +# typed with the document hierarchy classes only, which no authorization may name, so a grant of any other class - +# scoped to the end-user dataspace - reaches none of them: a write that would type an admin document with the granted +# class is refused with 422, even from the owner, and the grantee is still denied. + +class="http://xmlns.com/foaf/0.1/Person" +document="${ADMIN_BASE_URL}acl/groups/writers/" + +get_status() +{ + curl -k -w "%{http_code}" -o /dev/null -s \ + -E "$AGENT_CERT_FILE":"$AGENT_CERT_PWD" \ + -H "Accept: application/n-triples" \ + "$document" +} + +ldh admin create authorization \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --label "Read access to a class" \ + --agent "$AGENT_URI" \ + --to-all-in "$class" \ + --read \ + "$ADMIN_BASE_URL" > /dev/null + +status=$(get_status) +echo "DEBUG: <$document> before. Expected: $STATUS_FORBIDDEN Got: $status" +[ "$status" = "$STATUS_FORBIDDEN" ] || exit 1 + +# send a write as the owner and assert the status + +write() +{ + local label="$1" expected="$2" method="$3" content_type="$4" body="$5" actual + + actual=$(printf '%s\n' "$body" | curl -k -w "%{http_code}" -o /dev/null -s \ + -E "$OWNER_CERT_FILE":"$OWNER_CERT_PWD" \ + -X "$method" \ + -H "If-Match: $(etag "$document" "$OWNER_CERT_FILE" "$OWNER_CERT_PWD" "application/n-triples")" \ + -H "Accept: application/n-triples" \ + -H "Content-Type: $content_type" \ + --data-binary @- \ + "$document") + echo "DEBUG: ${label}: Expected: $expected" + echo "DEBUG: ${label}: Got: $actual" + [ "$actual" = "$expected" ] || exit 1 +} + +write "POST the granted class" "$STATUS_UNPROCESSABLE_ENTITY" POST "application/n-triples" \ + "<${document}> <${class}> ." + +write "PATCH in the granted class" "$STATUS_UNPROCESSABLE_ENTITY" PATCH "application/sparql-update" \ + "INSERT { <${document}> <${class}> } WHERE {}" + +group_ntriples=$(ldh get \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --accept 'application/n-triples' \ + "$document") +write "PUT with the granted class" "$STATUS_UNPROCESSABLE_ENTITY" PUT "application/n-triples" \ + "$(printf '%s\n<%s> <%s> .' "$group_ntriples" "$document" "$class")" + +status=$(get_status) +echo "DEBUG: <$document> after. Expected: $STATUS_FORBIDDEN Got: $status" +[ "$status" = "$STATUS_FORBIDDEN" ] || exit 1 diff --git a/tests/http/document-hierarchy/PATCH-foreign-type-422.sh b/tests/http/document-hierarchy/PATCH-foreign-type-422.sh new file mode 100755 index 000000000..e6bee5280 --- /dev/null +++ b/tests/http/document-hierarchy/PATCH-foreign-type-422.sh @@ -0,0 +1,69 @@ +#!/usr/bin/env bash +set -euo pipefail + +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 + +# A document is typed with the document hierarchy classes only, and stays typed with one: a PATCH that adds any other +# class to the document, or swaps its hierarchy class for another, is refused with 422 and changes nothing. + +item=$(ldh create item \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --title "Typed" \ + --slug "patch-foreign-type" \ + --container "$END_USER_BASE_URL") + +# send a PATCH as the owner and assert the status + +patch() +{ + local label="$1" expected="$2" update="$3" actual + + actual=$(curl -k -w "%{http_code}" -o /dev/null -s \ + -E "$OWNER_CERT_FILE":"$OWNER_CERT_PWD" \ + -X PATCH \ + -H "If-Match: $(etag "$item" "$OWNER_CERT_FILE" "$OWNER_CERT_PWD" "application/n-triples")" \ + -H "Accept: application/n-triples" \ + -H "Content-Type: application/sparql-update" \ + --data-binary "$update" \ + "$item") + echo "DEBUG: ${label}: Expected: $expected" + echo "DEBUG: ${label}: Got: $actual" + [ "$actual" = "$expected" ] || exit 1 +} + +# assert that the item is typed dh:Item and nothing else + +assert_unchanged() +{ + local types + + types=$(ldh get \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --accept 'application/n-triples' \ + "$item" \ + | grep -E "^<${item}> " || true) + echo "DEBUG: Expected types: <${item}> ." + echo "DEBUG: Got types: $types" + [ "$types" = "<${item}> ." ] || exit 1 +} + +patch "add another class" "$STATUS_UNPROCESSABLE_ENTITY" \ + "INSERT { <${item}> } WHERE {}" +assert_unchanged + +patch "swap the hierarchy class for another" "$STATUS_UNPROCESSABLE_ENTITY" \ + "DELETE { <${item}> } INSERT { <${item}> } WHERE {}" +assert_unchanged + +# another class on a resource in the document goes through + +patch "add another class to a resource in the document" "$STATUS_NO_CONTENT" \ + "INSERT { <${item}#this> } WHERE {}" diff --git a/tests/http/document-hierarchy/POST-foreign-type-422.sh b/tests/http/document-hierarchy/POST-foreign-type-422.sh new file mode 100755 index 000000000..0e17d9ef7 --- /dev/null +++ b/tests/http/document-hierarchy/POST-foreign-type-422.sh @@ -0,0 +1,61 @@ +#!/usr/bin/env bash +set -euo pipefail + +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 + +# A document is typed with the document hierarchy classes only: a POST whose payload types the document with any other +# class is refused with 422 and appends nothing. + +item=$(ldh create item \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --title "Typed" \ + --slug "post-foreign-type" \ + --container "$END_USER_BASE_URL") + +# send a POST to the item as the owner and assert the status + +post() +{ + local label="$1" expected="$2" payload="$3" actual + + actual=$(printf '%s\n' "$payload" | curl -k -w "%{http_code}" -o /dev/null -s \ + -E "$OWNER_CERT_FILE":"$OWNER_CERT_PWD" \ + -H "If-Match: $(etag "$item" "$OWNER_CERT_FILE" "$OWNER_CERT_PWD" "application/n-triples")" \ + -H "Accept: application/n-triples" \ + -H "Content-Type: application/n-triples" \ + --data-binary @- \ + "$item") + echo "DEBUG: ${label}: Expected: $expected" + echo "DEBUG: ${label}: Got: $actual" + [ "$actual" = "$expected" ] || exit 1 +} + +post "append another class" "$STATUS_UNPROCESSABLE_ENTITY" \ + "<${item}> . +<${item}> \"refused payload\" ." + +item_ntriples=$(ldh get \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --accept 'application/n-triples' \ + "$item") +types=$(echo "$item_ntriples" | grep -E "^<${item}> " || true) +echo "DEBUG: Expected types: <${item}> ." +echo "DEBUG: Got types: $types" +[ "$types" = "<${item}> ." ] || exit 1 +if echo "$item_ntriples" | grep -q "refused payload"; then + echo "DEBUG: the refused payload was appended" + exit 1 +fi + +# another class on a resource in the document goes through + +post "append another class on a resource in the document" "$STATUS_NO_CONTENT" \ + "<${item}#this> ." diff --git a/tests/http/document-hierarchy/PUT-foreign-type-422.sh b/tests/http/document-hierarchy/PUT-foreign-type-422.sh new file mode 100755 index 000000000..6ce22874c --- /dev/null +++ b/tests/http/document-hierarchy/PUT-foreign-type-422.sh @@ -0,0 +1,98 @@ +#!/usr/bin/env bash +set -euo pipefail + +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 + +# A document is typed with the document hierarchy classes only: a PUT whose payload types the document with any other +# class is refused with 422, whether it replaces a document or creates one, and writes nothing. The root, which is +# stored as sent, must be typed with one of them. A class grant matches a document's types, so this is what keeps a +# grant of any other class away from the documents. + +item=$(ldh create item \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --title "Typed" \ + --slug "put-foreign-type" \ + --container "$END_USER_BASE_URL") + +# send a PUT as the owner and assert the status: a replace quotes the document's tag, a create asks for none + +put() +{ + local label="$1" expected="$2" document="$3" payload="$4" precondition actual + + if [ "$document" = "$item" ] || [ "$document" = "$END_USER_BASE_URL" ]; then + precondition="If-Match: $(etag "$document" "$OWNER_CERT_FILE" "$OWNER_CERT_PWD" "application/n-triples")" + else + precondition="If-None-Match: *" + fi + + actual=$(printf '%s\n' "$payload" | curl -k -w "%{http_code}" -o /dev/null -s \ + -E "$OWNER_CERT_FILE":"$OWNER_CERT_PWD" \ + -X PUT \ + -H "$precondition" \ + -H "Accept: application/n-triples" \ + -H "Content-Type: application/n-triples" \ + --data-binary @- \ + "$document") + echo "DEBUG: ${label}: Expected: $expected" + echo "DEBUG: ${label}: Got: $actual" + [ "$actual" = "$expected" ] || exit 1 +} + +# replacing a document + +put "replace with another class" "$STATUS_UNPROCESSABLE_ENTITY" "$item" \ + "<${item}> . +<${item}> . +<${item}> \"Replaced\" ." + +item_ntriples=$(ldh get \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --accept 'application/n-triples' \ + "$item") +title=$(echo "$item_ntriples" | grep -E "^<${item}> " || true) +echo "DEBUG: Expected title: <${item}> \"Typed\" ." +echo "DEBUG: Got title: $title" +[ "$title" = "<${item}> \"Typed\" ." ] || exit 1 + +# creating a document + +created="${END_USER_BASE_URL}$(uuidgen | tr '[:upper:]' '[:lower:]')/" + +put "create with another class" "$STATUS_UNPROCESSABLE_ENTITY" "$created" \ + "<${created}> . +<${created}> \"Created\" ." + +status=$(curl -k -w "%{http_code}" -o /dev/null -s \ + -E "$OWNER_CERT_FILE":"$OWNER_CERT_PWD" \ + -H "Accept: application/n-triples" \ + "$created") +echo "DEBUG: the refused document. Expected: $STATUS_FORBIDDEN Got: $status" +[ "$status" = "$STATUS_FORBIDDEN" ] || exit 1 + +# the root without its hierarchy class + +root_ntriples=$(ldh get \ + -c "$OWNER_CERT_KEYSTORE" \ + -p "$OWNER_CERT_PWD" \ + --accept 'application/n-triples' \ + "$END_USER_BASE_URL") +untyped_root=$(echo "$root_ntriples" | grep -vE "^<${END_USER_BASE_URL}> ") + +put "replace the root untyped" "$STATUS_UNPROCESSABLE_ENTITY" "$END_USER_BASE_URL" "$untyped_root" +put "replace the root as it is" "$STATUS_NO_CONTENT" "$END_USER_BASE_URL" "$root_ntriples" + +# another class on a resource in the document goes through + +put "replace with another class on a resource in the document" "$STATUS_NO_CONTENT" "$item" \ + "<${item}> \"Replaced\" . +<${item}> <${item}#this> . +<${item}#this> ." diff --git a/tests/http/formal/acl-conformance.sh b/tests/http/formal/acl-conformance.sh index df24064bc..01936c62e 100755 --- a/tests/http/formal/acl-conformance.sh +++ b/tests/http/formal/acl-conformance.sh @@ -1,11 +1,14 @@ #!/usr/bin/env bash set -euo pipefail -# The Lean model of the authorization decision (formal/acl), replayed against the server. A random scenario of -# documents, groups and authorizations is built through the API, and before every request the two datasets are -# dumped and handed to ldh-acl, the executable decision proven equal to the model's allowRequest. The server has -# to agree with its verdict: 401 or 403 where it says deny, anything else where it says allow. The scenario's -# writes are themselves requests the model decides, so what the agents may do shapes what gets built. +# The Lean models of the graph store and the authorization decision (formal/http, formal/acl), replayed against the +# server. A random scenario of documents, groups and authorizations is built through the API, and before every +# request the two datasets are dumped and handed to ldh-acl, which runs the server's answer to the request +# (LdhAcl.Gate): the decision proven equal to the model's allowRequest, then the graph store's answer +# (LdhHttp.Answer), proven to write only what an authorized Write writes. The server has to +# agree with it twice: on the status, and on the document's graph after the request, but for the dates the server +# stamps. The requests carry random preconditions and payloads, some of which the write and type rules refuse. The +# scenario's writes are themselves requests the model decides, so what the agents may do shapes what gets built. # # ACL_CONFORMANCE_SEED replays a scenario; ACL_CONFORMANCE_STEPS sets how many random steps follow the setup. @@ -82,7 +85,8 @@ items=( docs=("${containers[@]}" "${items[@]}" "${END_USER_BASE_URL}${tag}/a/x") targets=("${docs[@]}" "$END_USER_BASE_URL" "$ADMIN_BASE_URL") agents=(anon agent agent2 owner) -methods=(GET HEAD POST PUT 'PUT*' PATCH DELETE) +methods=(GET HEAD POST PUT PATCH DELETE) +preconditions=(current current current none stale absent) groups=() group_docs=() @@ -96,58 +100,95 @@ dump() riot --syntax=trig --output=nquads "$work/admin.trig" > "$work/admin.nq" } -# the model's verdict on a request, over the last dump +# the model's answer to the request in $work/request.tsv, over the last dump: the status, then the document's graph predict() { - printf '%s\t%s\t%s\n' "${1:--}" "$2" "$3" > "$work/probe.tsv" - "$decider" --end-user "$work/end-user.nq" --admin "$work/admin.nq" --admin-base "$ADMIN_BASE_URL" --probes "$work/probe.tsv" \ - | cut -f1 + "$decider" --end-user "$work/end-user.nq" --admin "$work/admin.nq" --admin-base "$ADMIN_BASE_URL" \ + --request "$work/request.tsv" --payload "$work/payload.nt" --delete "$work/delete.nt" --insert "$work/insert.nt" } +# the quads of the document's graph in the last dump: its name is the term before the closing dot +quads_of() { awk -v g="<$1>" '$(NF-1) == g' "$work/end-user.nq" "$work/admin.nq"; } + # whether the last dump has a graph named by the document -exists_doc() { grep -qF -- "> <$1> ." "$work/end-user.nq" "$work/admin.nq"; } +exists_doc() { [ -n "$(quads_of "$1")" ]; } + +# the document's graph in the last dump, as N-Triples, without the dates the server stamps on every write +graph_of() { quads_of "$1" | sed 's/ <[^>]*> \.$/ ./' | without_dates "$1"; } + +without_dates() +{ + grep -vF -e "<$1> " -e "<$1> " | sort -u || true +} + +T="" +DH="https://w3id.org/atomgraph/linkeddatahub/document-hierarchy#" document_body() { - local type="https://w3id.org/atomgraph/linkeddatahub/document-hierarchy#Item" c + local type="${DH}Item" c for c in "${containers[@]}"; do - [ "$c" = "$1" ] && type="https://w3id.org/atomgraph/linkeddatahub/document-hierarchy#Container" + [ "$c" = "$1" ] && type="${DH}Container" done - printf '<%s> <%s> .\n<%s> "Conformance %s" .\n' "$1" "$type" "$1" "$RANDOM" + printf '<%s> %s <%s> .\n<%s> "Conformance %s" .\n' "$1" "$T" "$type" "$1" "$RANDOM" +} + +# a payload for the method, mostly one the rules let through, sometimes one they refuse or strip; `plain` asks for +# the one they let through +payloads() +{ + local method="$1" target="$2" variant other="${docs[$(pick ${#docs[@]})]}" + : > "$work/payload.nt"; : > "$work/delete.nt"; : > "$work/insert.nt" + if [ "${3:-}" = plain ]; then variant=plain; else variant=$(pick 8); fi + case "$method:$variant" in + POST:0) ;; # appending nothing + POST:1) printf '<%s> %s .\n' "$target" "$T" > "$work/payload.nt" ;; + POST:2) printf '<%s> <%s> .\n' "$other" "$target" > "$work/payload.nt" ;; + POST:3) printf '<%s> <%s> .\n' "$target" "$AGENT2_URI" > "$work/payload.nt" ;; + POST:*) printf '<%s#p%s> "v" .\n' "$target" "$RANDOM" > "$work/payload.nt" ;; + PUT:0) { document_body "$target"; printf '<%s> %s .\n' "$target" "$T"; } > "$work/payload.nt" ;; + PUT:1) { document_body "$target"; printf '<%s> <%s> .\n' "$other" "$target"; } > "$work/payload.nt" ;; + PUT:2) { document_body "$target"; printf '<%s> <%s> .\n' "$target" "$AGENT2_URI"; } > "$work/payload.nt" ;; + PUT:*) document_body "$target" > "$work/payload.nt" ;; + PATCH:0) printf '<%s> %s .\n' "$target" "$T" > "$work/insert.nt" ;; + PATCH:1) printf '<%s> <%s> .\n' "$target" "$END_USER_BASE_URL" > "$work/insert.nt" ;; + PATCH:2) printf '<%s> %s <%sItem> .\n' "$target" "$T" "$DH" > "$work/delete.nt" + printf '<%s> %s <%sContainer> .\n' "$target" "$T" "$DH" > "$work/insert.nt" ;; + PATCH:*) printf '<%s> "%s" .\n' "$target" "$RANDOM" > "$work/insert.nt" ;; + *) ;; + esac } -# the request, as the agent; prints the status. A write to an existing document quotes the owner's validator, so -# that only the decision stands between the request and its effect +# the request, as the agent, with the precondition and the payloads in $work; prints the status request() { - local agent="$1" method="$2" target="$3" pair ifmatch="" + local agent="$1" method="$2" target="$3" precondition="$4" pair header=(-H "X-Conformance-Step: $step") pair=$(cert_pair "$agent") - if exists_doc "$target" && [ "$method" != GET ] && [ "$method" != HEAD ] && [ "$method" != POST ] && [ "$method" != 'PUT*' ]; then - ifmatch=$(etag "$target" "$OWNER_CERT_FILE" "$OWNER_CERT_PWD" "application/n-triples" 2>/dev/null || true) - fi + case "$precondition" in + current) + # the owner's validator for the variant the request negotiates; a document with none has no current tag + if exists_doc "$target"; then + header=(-H "If-Match: $(etag "$target" "$OWNER_CERT_FILE" "$OWNER_CERT_PWD" "application/n-triples" 2>/dev/null || echo '"none"')") + else + header=(-H 'If-Match: "none"') + fi ;; + stale) header=(-H 'If-Match: "stale"') ;; + absent) header=(-H 'If-None-Match: *') ;; + esac case "$method" in GET) curl -k -s -o /dev/null -w '%{http_code}' ${pair:+-E "$pair"} -H "Accept: application/n-triples" "$target" ;; HEAD) curl -k -s -o /dev/null -w '%{http_code}' -I ${pair:+-E "$pair"} -H "Accept: application/n-triples" "$target" ;; - POST) - printf '<%s#p%s> "v" .\n' "$target" "$RANDOM" \ - | curl -k -s -o /dev/null -w '%{http_code}' ${pair:+-E "$pair"} -X POST \ - -H "Content-Type: application/n-triples" -H "Accept: application/n-triples" --data-binary @- "$target" ;; - PUT) - document_body "$target" \ - | curl -k -s -o /dev/null -w '%{http_code}' ${pair:+-E "$pair"} -X PUT ${ifmatch:+-H "If-Match: $ifmatch"} \ - -H "Content-Type: application/n-triples" -H "Accept: application/n-triples" --data-binary @- "$target" ;; - 'PUT*') - document_body "$target" \ - | curl -k -s -o /dev/null -w '%{http_code}' ${pair:+-E "$pair"} -X PUT -H "If-None-Match: *" \ - -H "Content-Type: application/n-triples" -H "Accept: application/n-triples" --data-binary @- "$target" ;; + POST|PUT) + curl -k -s -o /dev/null -w '%{http_code}' ${pair:+-E "$pair"} -X "$method" "${header[@]}" \ + -H "Content-Type: application/n-triples" -H "Accept: application/n-triples" --data-binary @"$work/payload.nt" "$target" ;; PATCH) - curl -k -s -o /dev/null -w '%{http_code}' ${pair:+-E "$pair"} -X PATCH ${ifmatch:+-H "If-Match: $ifmatch"} \ + curl -k -s -o /dev/null -w '%{http_code}' ${pair:+-E "$pair"} -X PATCH "${header[@]}" \ -H "Content-Type: application/sparql-update" -H "Accept: application/n-triples" \ - --data-binary "INSERT DATA { <$target> \"$RANDOM\" }" "$target" ;; + --data-binary "DELETE { $(cat "$work/delete.nt") } INSERT { $(cat "$work/insert.nt") } WHERE {}" "$target" ;; DELETE) - curl -k -s -o /dev/null -w '%{http_code}' ${pair:+-E "$pair"} -X DELETE ${ifmatch:+-H "If-Match: $ifmatch"} \ + curl -k -s -o /dev/null -w '%{http_code}' ${pair:+-E "$pair"} -X DELETE "${header[@]}" \ -H "Accept: application/n-triples" "$target" ;; esac } @@ -165,30 +206,39 @@ step=0 # one request: predicted, sent, compared probe() { - local agent="$1" method="$2" target="$3" verdict status outcome + local agent="$1" method="$2" target="$3" precondition="$4" expected status outcome=ok step=$((step + 1)) dump - verdict=$(predict "$(agent_uri "$agent")" "$method" "$target") - status=$(request "$agent" "$method" "$target") - case "$verdict:$status" in - deny:401|deny:403) outcome=ok ;; - deny:*) outcome=MISMATCH ;; - allow:401|allow:403) outcome=MISMATCH ;; - allow:*) outcome=ok ;; - esac - echo "DEBUG: step $step: $agent $method $target: model says $verdict, server returned $status: $outcome" + payloads "$method" "$target" "${5:-}" + printf '%s\t%s\t%s\t%s\n' "$(agent_uri "$agent" | sed 's/^$/-/')" "$method" "$target" "$precondition" > "$work/request.tsv" + predict > "$work/predicted" + expected=$(head -n 1 "$work/predicted") + tail -n +2 "$work/predicted" | without_dates "$target" > "$work/predicted.nt" + status=$(request "$agent" "$method" "$target" "$precondition") + cp "$work/end-user.nq" "$work/before.end-user.nq" + cp "$work/admin.nq" "$work/before.admin.nq" + dump + graph_of "$target" > "$work/actual.nt" + [ "$status" = "$expected" ] || outcome=MISMATCH + if ! diff -q "$work/predicted.nt" "$work/actual.nt" > /dev/null; then + outcome=MISMATCH + echo "DEBUG: the graph of <$target>, predicted (<) and stored (>):" + diff "$work/predicted.nt" "$work/actual.nt" | sed 's/^/DEBUG: /' || true + fi + echo "DEBUG: step $step: $agent $method $target ($precondition): model says $expected, server returned $status: $outcome" if [ "$outcome" = MISMATCH ]; then mismatches=$((mismatches + 1)) local keep="$TEST_RESULTS_DIR/acl-conformance-$seed-step-$step" - cp "$work/end-user.nq" "$keep.end-user.nq" - cp "$work/admin.nq" "$keep.admin.nq" - cp "$work/probe.tsv" "$keep.probe.tsv" - echo "DEBUG: datasets and probe kept as $keep.*" - fi - # anything but a refused request may have changed the stores, and with them what the caches hold - if [ "$method" != GET ] && [ "$method" != HEAD ] && [ "$status" != 401 ] && [ "$status" != 403 ]; then - purge_all + cp "$work/before.end-user.nq" "$keep.end-user.nq" + cp "$work/before.admin.nq" "$keep.admin.nq" + cp "$work/request.tsv" "$keep.request.tsv" + cp "$work/payload.nt" "$keep.payload.nt" + cp "$work/delete.nt" "$keep.delete.nt" + cp "$work/insert.nt" "$keep.insert.nt" + echo "DEBUG: datasets, request and payloads kept as $keep.*" fi + # a request that went through may have changed the stores, and with them what the caches hold + case "$status" in 2*) purge_all ;; esac } # the owner's administration between requests: what the ACL query will read next @@ -256,7 +306,7 @@ auth_count=0 # setup: the owner creates the tree, containers first; the model decides each of these too for d in "${containers[@]}" "${items[@]}"; do - probe owner 'PUT*' "$d" + probe owner PUT "$d" absent plain done new_group new_authorization @@ -267,7 +317,11 @@ for ((i = 1; i <= steps; i++)); do case "$(pick 12)" in 0) new_authorization ;; 1) if [ "$(pick 2)" = 0 ]; then new_group; else add_member; fi ;; - *) probe "${agents[$(pick ${#agents[@]})]}" "${methods[$(pick ${#methods[@]})]}" "${docs[$(pick ${#docs[@]})]}" ;; + *) + method="${methods[$(pick ${#methods[@]})]}" + precondition=none + case "$method" in GET|HEAD) ;; *) precondition="${preconditions[$(pick ${#preconditions[@]})]}" ;; esac + probe "${agents[$(pick ${#agents[@]})]}" "$method" "${docs[$(pick ${#docs[@]})]}" "$precondition" ;; esac done diff --git a/tests/http/misc/GET-accept-param-malformed-400.sh b/tests/http/misc/GET-accept-param-malformed-400.sh new file mode 100755 index 000000000..c42456adf --- /dev/null +++ b/tests/http/misc/GET-accept-param-malformed-400.sh @@ -0,0 +1,61 @@ +#!/usr/bin/env bash +set -euo pipefail + +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 + +# A malformed ?accept= value is refused with 400 before ApplicationFilter sets the dataspace. The response filters +# that look the dataspace up afterwards used to turn that refusal into a 500 ("already seeded in this scope"). +# Crawlers send the unencoded +, which decodes to a space: application/rdf xml + +for accept in "application%2Frdf+xml" "application/ld+json"; do + for rest in "" "&uri=${END_USER_BASE_URL}"; do + url="${END_USER_BASE_URL}?accept=${accept}${rest}" + + status=$(curl -k -s -o /dev/null -w "%{http_code}" \ + -H "Accept: text/html" \ + "$url") + + echo "DEBUG: anonymous GET $url Expected: $STATUS_BAD_REQUEST Got: $status" + if [ "$status" != "$STATUS_BAD_REQUEST" ]; then + exit 1 + fi + + status=$(curl -k -s -o /dev/null -w "%{http_code}" \ + -E "$OWNER_CERT_FILE":"$OWNER_CERT_PWD" \ + -H "Accept: text/html" \ + "$url") + + echo "DEBUG: owner GET $url Expected: $STATUS_BAD_REQUEST Got: $status" + if [ "$status" != "$STATUS_BAD_REQUEST" ]; then + exit 1 + fi + done +done + +# the admin dataspace answers the same + +status=$(curl -k -s -o /dev/null -w "%{http_code}" \ + -E "$OWNER_CERT_FILE":"$OWNER_CERT_PWD" \ + "${ADMIN_BASE_URL}?accept=application%2Fld+json") + +echo "DEBUG: owner GET admin ?accept=application%2Fld+json Expected: $STATUS_BAD_REQUEST Got: $status" +if [ "$status" != "$STATUS_BAD_REQUEST" ]; then + exit 1 +fi + +# a well-formed value still negotiates + +status=$(curl -k -s -o /dev/null -w "%{http_code}" \ + -E "$OWNER_CERT_FILE":"$OWNER_CERT_PWD" \ + "${END_USER_BASE_URL}?accept=application%2Fn-triples") + +echo "DEBUG: owner GET ?accept=application%2Fn-triples Expected: $STATUS_OK Got: $status" +if [ "$status" != "$STATUS_OK" ]; then + exit 1 +fi 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 diff --git a/tests/ui/lib/chart.mjs b/tests/ui/lib/chart.mjs index daab34e53..3180d802b 100644 --- a/tests/ui/lib/chart.mjs +++ b/tests/ui/lib/chart.mjs @@ -22,3 +22,10 @@ export const canvas = block => block.locator('.chart-canvas'); export const drawing = block => canvas(block).locator('svg, canvas, table').first(); export const chartType = block => block.locator('select.chart-type'); + +// The columns of the data table a chart was drawn from, as the chart keeps it on its block's cache: the order a chart +// that reads its columns by position takes them in, which bars and a legend do not show. Null until it has drawn. +export const columnLabels = (page, uri = fixtures.chart) => page.evaluate(key => { + const table = window.LinkedDataHub?.contents?.[key]?.['data-table']; + return table ? Array.from({ length: table.getNumberOfColumns() }, (_, i) => table.getColumnLabel(i)) : null; +}, uri); diff --git a/tests/ui/lib/fixtures.mjs b/tests/ui/lib/fixtures.mjs index 64071fdb1..4d856fa82 100644 --- a/tests/ui/lib/fixtures.mjs +++ b/tests/ui/lib/fixtures.mjs @@ -316,11 +316,11 @@ export async function seed() { writeFileSync(seriesQueryFile, seriesQuery); await ldh(['add', 'select', '--title', 'Fixture item measures', '--uri', fixtures.seriesQuery, '--query-file', seriesQueryFile, fixtures.seriesDocument]); - // A Table, because its header row IS the column order: a chart type draws the same columns as - // bars and legend entries, which say nothing about position. + // A bar chart, not a Table: a Table shows the whole projection in its own order whatever the + // series are, so only a chart that plots its series can show what order they are taken in. await ldh(['add', 'result-set-chart', '--title', 'Fixture measures chart', '--uri', fixtures.seriesChart, '--query', fixtures.seriesQuery, - '--chart-type', 'https://w3id.org/atomgraph/client#Table', + '--chart-type', 'https://w3id.org/atomgraph/client#BarChart', '--category-var-name', 'kind', ...seriesProjection.toReversed().flatMap(name => ['--series-var-name', name]), fixtures.seriesDocument]); diff --git a/tests/ui/specs/document/blocks/chart/series-order.spec.mjs b/tests/ui/specs/document/blocks/chart/series-order.spec.mjs index cb929cc6c..a4ca08a01 100644 --- a/tests/ui/specs/document/blocks/chart/series-order.spec.mjs +++ b/tests/ui/specs/document/blocks/chart/series-order.spec.mjs @@ -8,21 +8,20 @@ // notice, because every fixture chart had a single series. // // The fixture declares four series in the reverse of the order its query projects them, and draws -// them as a Table, whose header row is the DataTable's column order read straight off the page. +// them as bars; the order is read off the DataTable the chart was drawn from, which bars and a +// legend do not show. Not as a Table, which shows the whole projection whatever the series are. // Four, because a chart ordering by anything but the projection still matches it by chance one // time in 24; with two it would pass half the time without the fix. import { test, expect } from '../../../../lib/console.mjs'; import { goto } from '../../../../lib/settle.mjs'; import { fixtures, seriesProjection } from '../../../../lib/fixtures.mjs'; -import { canvas, chartBlock } from '../../../../lib/chart.mjs'; +import { chartBlock, columnLabels, drawing } from '../../../../lib/chart.mjs'; test('takes its series in the order the query projects them, not the order they are declared in', async ({ page }) => { await goto(page, fixtures.seriesDocument); - const block = chartBlock(page, fixtures.seriesChart); - const table = canvas(block).locator('.google-visualization-table'); - await expect(table).toBeVisible({ timeout: 30_000 }); + await expect(drawing(chartBlock(page, fixtures.seriesChart))).toBeVisible({ timeout: 30_000 }); // The category first, then the series as SELECT lists them. - await expect(table.locator('tr').first().locator('th')).toHaveText(['kind', ...seriesProjection]); + await expect.poll(() => columnLabels(page, fixtures.seriesChart)).toEqual(['kind', ...seriesProjection]); }); diff --git a/tests/ui/specs/document/blocks/chart/table-columns.spec.mjs b/tests/ui/specs/document/blocks/chart/table-columns.spec.mjs new file mode 100644 index 000000000..775b5ce11 --- /dev/null +++ b/tests/ui/specs/document/blocks/chart/table-columns.spec.mjs @@ -0,0 +1,111 @@ +// A chart drawn as a Table shows every column of its results, not only its category and series. +// +// The category and series pick what a chart plots: the axis it draws against and the values it draws. A table plots +// nothing, so it has no use for them, but the data table it was drawn from was cut down to them all the same. A +// ResultSetChart whose query selected five variables, saved with a category and one series, showed two columns, and +// nothing on the page said the other three existed. A chart of a graph lost every property but its category and +// series the same way. +// +// Each test seeds a document of its own: the shared fixtures chart one series, where a table and a chart of it would +// show the same columns and this could not fail. +import { test, expect } from '../../../../lib/console.mjs'; +import { goto } from '../../../../lib/settle.mjs'; +import { fixtures, ldh } from '../../../../lib/fixtures.mjs'; +import { endUserBase } from '../../../../lib/stack.mjs'; +import { canvas, chartBlock } from '../../../../lib/chart.mjs'; +import { mkdtempSync, writeFileSync } from 'node:fs'; +import { tmpdir } from 'node:os'; +import { join } from 'node:path'; + +const AC = 'https://w3id.org/atomgraph/client#'; +const LDH = 'https://w3id.org/atomgraph/linkeddatahub#'; +const DCT = 'http://purl.org/dc/terms/'; +const SPIN = 'http://spinrdf.org/spin#'; + +// Three variables, of which the chart plots two +const countsQuery = `PREFIX sioc: +PREFIX dct: + +SELECT ?kind (COUNT(?item) AS ?items) (MAX(STRLEN(?title)) AS ?longest) +WHERE + { GRAPH ?g + { ?item sioc:has_container <${fixtures.container}> ; + dct:title ?title ; + dct:description ?kind + } + } +GROUP BY ?kind +ORDER BY ?kind`; + +// Three properties per item, of which the chart plots two +const itemsConstruct = `PREFIX sioc: +PREFIX dct: + +CONSTRUCT { ?item dct:title ?title ; dct:description ?kind ; sioc:has_container ?container } +WHERE + { GRAPH ?g + { ?item sioc:has_container ?container ; + dct:title ?title ; + dct:description ?kind + FILTER ( ?container = <${fixtures.container}> ) + } + }`; + +const queryFile = text => { + const file = join(mkdtempSync(join(tmpdir(), 'ui-chart-table-')), 'q.rq'); + writeFileSync(file, text); + return file; +}; + +async function seedResultSetChart(slug) { + const doc = `${endUserBase}${slug}/`; + await ldh(['delete', doc], { allowFailure: true }); + await ldh(['create', 'item', '--container', endUserBase, '--title', `Table columns ${slug}`, '--slug', slug]); + await ldh(['add', 'select', '--title', 'Counts', '--uri', `${doc}#query`, '--query-file', queryFile(countsQuery), doc]); + await ldh(['add', 'result-set-chart', '--title', 'Counts table', '--uri', `${doc}#chart`, '--query', `${doc}#query`, + '--chart-type', `${AC}Table`, '--category-var-name', 'kind', '--series-var-name', 'items', doc]); + await ldh(['add', 'object-block', '--title', 'Counts table block', '--uri', `${doc}#block`, '--value', `${doc}#chart`, doc]); + return { doc, chart: `${doc}#chart` }; +} + +// No CLI command writes a graph chart, so it is written as data, the way any client could +async function seedGraphChart(slug) { + const doc = `${endUserBase}${slug}/`; + await ldh(['delete', doc], { allowFailure: true }); + await ldh(['create', 'item', '--container', endUserBase, '--title', `Table columns ${slug}`, '--slug', slug]); + await ldh(['add', 'construct', '--title', 'Items', '--uri', `${doc}#query`, '--query-file', queryFile(itemsConstruct), doc]); + await ldh(['patch', doc], { stdin: `INSERT { <${doc}#chart> a <${LDH}GraphChart> ; + <${DCT}title> "Items table" ; + <${SPIN}query> <${doc}#query> ; + <${LDH}chartType> <${AC}Table> ; + <${LDH}categoryProperty> <${DCT}title> ; + <${LDH}seriesProperty> <${DCT}description> } WHERE {}` }); + await ldh(['add', 'object-block', '--title', 'Items table block', '--uri', `${doc}#block`, '--value', `${doc}#chart`, doc]); + return { doc, chart: `${doc}#chart` }; +} + +const header = (page, chart) => canvas(chartBlock(page, chart)).locator('.google-visualization-table tr').first().locator('th'); + +// the documents are the owner's, unpublished, so only the owner can read them +test.describe('a chart drawn as a table', { tag: '@owner' }, () => { + test('a table of a result set shows every variable the query selects, in the order it selects them', async ({ page }) => { + const { doc, chart } = await seedResultSetChart('ui-chart-table-results'); + try { + await goto(page, doc); + await expect(header(page, chart)).toHaveText(['kind', 'items', 'longest'], { timeout: 30_000 }); + } finally { + await ldh(['delete', doc], { allowFailure: true }); + } + }); + + test('a table of a graph shows every property its resources carry', async ({ page }) => { + const { doc, chart } = await seedGraphChart('ui-chart-table-graph'); + try { + await goto(page, doc); + // one column per property: the title and description the chart names, and the container it does not + await expect(header(page, chart)).toHaveCount(3, { timeout: 30_000 }); + } finally { + await ldh(['delete', doc], { allowFailure: true }); + } + }); +});