`RoostRelations`

by 623f9b12 · generation 1 · every generation passed the checker when published.

Relationship-based authorization over records: tuples (owner, guest, everyone) plus a row condition and one level of lookup traversal, with capability links as account-less subjects. Checks that a served read satisfies the predicate in the serving state, that a list equals the per-record check, that revoked links are never served, and that no tuple outlives its record or link.

Raw .tla Raw .cfg

RoostRelations.tla

MODULE RoostRelations

EXTENDS Naturals, FiniteSets

CONSTANTS r1, c1, u1, l1, Star, NoRecord, NoRead, NoList

Records ≜ {r1, c1}

Users ≜ {u1}

Links ≜ {l1}

Subjects ≜ Users ∪ Links ∪ {Star}

Relations ≜ {"owner", "guest"}

Roles ≜ {"member", "none"}

Parent(r) ≜ IF r = c1 THEN r1 ELSE NoRecord

VARIABLES exists, tuples, linkSt, open, role, lastRead, lastList

vars ≜ ⟨exists, tuples, linkSt, open, role, lastRead, lastList⟩

TypeOK ≜

∧ exists ⊆ Records

∧ tuples ⊆ (Records × Relations × Subjects)

∧ linkSt ∈ [Links → {"active", "revoked"}]

∧ open ∈ [Records → BOOLEAN]

∧ role ∈ [Users → Roles]

∧ lastRead ∈ ({NoRead} ∪ [s: Subjects, r: Records])

∧ lastList ∈ ({NoList} ∪ [s: Subjects, set: SUBSET Records])

Alive(s) ≜ s ∈ Links ⇒ linkSt[s] = "active"

Holds(s, r) ≜

∨ s ∈ Users ∧ role[s] = "member"

∨ ⟨r, "owner", s⟩ ∈ tuples

∨ open[r] ∧ (⟨r, "guest", s⟩ ∈ tuples ∨ ⟨r, "guest", Star⟩ ∈ tuples)

Check(s, r) ≜

∧ Alive(s)

∧ ∨ Holds(s, r)

∨ Parent(r) ≠ NoRecord ∧ Parent(r) ∈ exists ∧ Holds(s, Parent(r))

Permitted(s) ≜ {r ∈ exists : Check(s, r)}

Init ≜

∧ exists = {r1}

∧ tuples = {}

∧ linkSt = [l ∈ Links ↦ "active"]

∧ open = [r ∈ Records ↦ FALSE]

∧ role = [u ∈ Users ↦ "none"]

∧ lastRead = NoRead

∧ lastList = NoList

Clear ≜ lastRead^′ = NoRead ∧ lastList^′ = NoList

CanHold(rel, s) ≜ rel = "guest" ∨ s ∈ Links

Share(r, rel, s) ≜

∧ r ∈ exists ∧ CanHold(rel, s) ∧ Alive(s)

∧ tuples^′ = tuples ∪ {⟨r, rel, s⟩}

∧ UNCHANGED ⟨exists, linkSt, open, role⟩ ∧ Clear

Unshare(r, rel, s) ≜

∧ ⟨r, rel, s⟩ ∈ tuples

∧ tuples^′ = tuples \ {⟨r, rel, s⟩}

∧ UNCHANGED ⟨exists, linkSt, open, role⟩ ∧ Clear

Toggle(r) ≜

∧ open^′ = [open EXCEPT ![r] = ¬open[r]]

∧ UNCHANGED ⟨exists, tuples, linkSt, role⟩ ∧ Clear

SetRole(u, x) ≜

∧ role^′ = [role EXCEPT ![u] = x]

∧ UNCHANGED ⟨exists, tuples, linkSt, open⟩ ∧ Clear

CreateByLink(r, l) ≜

∧ r ∉ exists ∧ linkSt[l] = "active"

∧ exists^′ = exists ∪ {r}

∧ tuples^′ = tuples ∪ {⟨r, "owner", l⟩}

∧ UNCHANGED ⟨linkSt, open, role⟩ ∧ Clear

Delete(r) ≜

∧ r ∈ exists

∧ exists^′ = exists \ {r}

∧ tuples^′ = {t ∈ tuples : t[1] ≠ r}

∧ UNCHANGED ⟨linkSt, open, role⟩ ∧ Clear

Revoke(l) ≜

∧ linkSt[l] = "active"

∧ linkSt^′ = [linkSt EXCEPT ![l] = "revoked"]

∧ tuples^′ = {t ∈ tuples : t[3] ≠ l}

∧ UNCHANGED ⟨exists, open, role⟩ ∧ Clear

Read(s, r) ≜

∧ r ∈ exists ∧ Check(s, r)

∧ lastRead^′ = [s ↦ s, r ↦ r]

∧ lastList^′ = NoList

∧ UNCHANGED ⟨exists, tuples, linkSt, open, role⟩

List(s) ≜

∧ lastList^′ = [s ↦ s, set ↦ Permitted(s)]

∧ lastRead^′ = NoRead

∧ UNCHANGED ⟨exists, tuples, linkSt, open, role⟩

Next ≜

∨ ∃ r ∈ Records, rel ∈ Relations, s ∈ Subjects : Share(r, rel, s) ∨ Unshare(r, rel, s)

∨ ∃ r ∈ Records : Toggle(r) ∨ Delete(r)

∨ ∃ u ∈ Users, x ∈ Roles : SetRole(u, x)

∨ ∃ r ∈ Records, l ∈ Links : CreateByLink(r, l)

∨ ∃ l ∈ Links : Revoke(l)

∨ ∃ s ∈ Subjects, r ∈ Records : Read(s, r)

∨ ∃ s ∈ Subjects : List(s)

Spec ≜ Init ∧ □[Next]_vars

DecisionFromCurrentState ≜

lastRead ≠ NoRead ⇒ lastRead.r ∈ exists ∧ Check(lastRead.s, lastRead.r)

ListIsCheck ≜

lastList ≠ NoList ⇒ lastList.set = Permitted(lastList.s)

RevokedLinkNeverServes ≜

∧ (lastRead ≠ NoRead ∧ lastRead.s ∈ Links) ⇒ linkSt[lastRead.s] = "active"

∧ (lastList ≠ NoList ∧ lastList.s ∈ Links ∧ linkSt[lastList.s] = "revoked") ⇒ lastList.set = {}

NoOrphanTuples ≜

∀ t ∈ tuples : t[1] ∈ exists ∧ (t[3] ∈ Links ⇒ linkSt[t[3]] = "active")

VisitorOnlyThroughStar ≜

(lastRead ≠ NoRead ∧ lastRead.s = Star) ⇒

∃ r ∈ {lastRead.r} ∪ ({Parent(lastRead.r)} \ {NoRecord}) : open[r] ∧ ⟨r, "guest", Star⟩ ∈ tuples

RoostRelations.cfg

SPECIFICATION Spec

CONSTANTS

r1 = r1

c1 = c1

u1 = u1

l1 = l1

Star = Star

NoRecord = NoRecord

NoRead = NoRead

NoList = NoList

INVARIANTS

TypeOK

DecisionFromCurrentState

ListIsCheck

RevokedLinkNeverServes

NoOrphanTuples

VisitorOnlyThroughStar

---------------------------- MODULE RoostRelations ---------------------------- EXTENDS Naturals, FiniteSets CONSTANTS r1, c1, u1, l1, Star, NoRecord, NoRead, NoList Records == {r1, c1} Users == {u1} Links == {l1} Subjects == Users \cup Links \cup {Star} Relations == {"owner", "guest"} Roles == {"member", "none"} Parent(r) == IF r = c1 THEN r1 ELSE NoRecord VARIABLES exists, tuples, linkSt, open, role, lastRead, lastList vars == <<exists, tuples, linkSt, open, role, lastRead, lastList>> TypeOK == /\ exists \subseteq Records /\ tuples \subseteq (Records \X Relations \X Subjects) /\ linkSt \in [Links -> {"active", "revoked"}] /\ open \in [Records -> BOOLEAN] /\ role \in [Users -> Roles] /\ lastRead \in ({NoRead} \cup [s: Subjects, r: Records]) /\ lastList \in ({NoList} \cup [s: Subjects, set: SUBSET Records]) Alive(s) == s \in Links => linkSt[s] = "active" Holds(s, r) == \/ s \in Users /\ role[s] = "member" \/ <<r, "owner", s>> \in tuples \/ open[r] /\ (<<r, "guest", s>> \in tuples \/ <<r, "guest", Star>> \in tuples) Check(s, r) == /\ Alive(s) /\ \/ Holds(s, r) \/ Parent(r) # NoRecord /\ Parent(r) \in exists /\ Holds(s, Parent(r)) Permitted(s) == {r \in exists : Check(s, r)} Init == /\ exists = {r1} /\ tuples = {} /\ linkSt = [l \in Links |-> "active"] /\ open = [r \in Records |-> FALSE] /\ role = [u \in Users |-> "none"] /\ lastRead = NoRead /\ lastList = NoList Clear == lastRead' = NoRead /\ lastList' = NoList CanHold(rel, s) == rel = "guest" \/ s \in Links Share(r, rel, s) == /\ r \in exists /\ CanHold(rel, s) /\ Alive(s) /\ tuples' = tuples \cup {<<r, rel, s>>} /\ UNCHANGED <<exists, linkSt, open, role>> /\ Clear Unshare(r, rel, s) == /\ <<r, rel, s>> \in tuples /\ tuples' = tuples \ {<<r, rel, s>>} /\ UNCHANGED <<exists, linkSt, open, role>> /\ Clear Toggle(r) == /\ open' = [open EXCEPT ![r] = ~open[r]] /\ UNCHANGED <<exists, tuples, linkSt, role>> /\ Clear SetRole(u, x) == /\ role' = [role EXCEPT ![u] = x] /\ UNCHANGED <<exists, tuples, linkSt, open>> /\ Clear CreateByLink(r, l) == /\ r \notin exists /\ linkSt[l] = "active" /\ exists' = exists \cup {r} /\ tuples' = tuples \cup {<<r, "owner", l>>} /\ UNCHANGED <<linkSt, open, role>> /\ Clear Delete(r) == /\ r \in exists /\ exists' = exists \ {r} /\ tuples' = {t \in tuples : t[1] # r} /\ UNCHANGED <<linkSt, open, role>> /\ Clear Revoke(l) == /\ linkSt[l] = "active" /\ linkSt' = [linkSt EXCEPT ![l] = "revoked"] /\ tuples' = {t \in tuples : t[3] # l} /\ UNCHANGED <<exists, open, role>> /\ Clear Read(s, r) == /\ r \in exists /\ Check(s, r) /\ lastRead' = [s |-> s, r |-> r] /\ lastList' = NoList /\ UNCHANGED <<exists, tuples, linkSt, open, role>> List(s) == /\ lastList' = [s |-> s, set |-> Permitted(s)] /\ lastRead' = NoRead /\ UNCHANGED <<exists, tuples, linkSt, open, role>> Next == \/ \E r \in Records, rel \in Relations, s \in Subjects : Share(r, rel, s) \/ Unshare(r, rel, s) \/ \E r \in Records : Toggle(r) \/ Delete(r) \/ \E u \in Users, x \in Roles : SetRole(u, x) \/ \E r \in Records, l \in Links : CreateByLink(r, l) \/ \E l \in Links : Revoke(l) \/ \E s \in Subjects, r \in Records : Read(s, r) \/ \E s \in Subjects : List(s) Spec == Init /\ [][Next]_vars DecisionFromCurrentState == lastRead # NoRead => lastRead.r \in exists /\ Check(lastRead.s, lastRead.r) ListIsCheck == lastList # NoList => lastList.set = Permitted(lastList.s) RevokedLinkNeverServes == /\ (lastRead # NoRead /\ lastRead.s \in Links) => linkSt[lastRead.s] = "active" /\ (lastList # NoList /\ lastList.s \in Links /\ linkSt[lastList.s] = "revoked") => lastList.set = {} NoOrphanTuples == \A t \in tuples : t[1] \in exists /\ (t[3] \in Links => linkSt[t[3]] = "active") VisitorOnlyThroughStar == (lastRead # NoRead /\ lastRead.s = Star) => \E r \in {lastRead.r} \cup ({Parent(lastRead.r)} \ {NoRecord}) : open[r] /\ <<r, "guest", Star>> \in tuples ================================================================================

Generations

gen	changes	distinct states	depth	published	raw
1 (latest)	First generation: the relations model replacing a role-by-object permission matrix.	18523	14	2026-09-17 00:16:10 UTC	.tla .cfg

Defend this spec

Ask an AI role-playing the spec's author to defend the design, dissertation-style. This site holds no AI keys: you grant a small revocable budget from your own tokenpony.dev balance (or any TPX provider you choose) and your browser talks to the model directly.

Loading…