diff options
Diffstat (limited to 'docs/denial.org')
| -rw-r--r-- | docs/denial.org | 194 |
1 files changed, 194 insertions, 0 deletions
diff --git a/docs/denial.org b/docs/denial.org new file mode 100644 index 0000000..d79a394 --- /dev/null +++ b/docs/denial.org @@ -0,0 +1,194 @@ +#+TITLE: Denials + +* Purpose +A denial is a relation that must be empty. Each tuple it holds is one +breach of a rule, so a state where every denial is empty is a state +where every rule holds. RNT knows no rule language. It knows only that +denials must be empty, and it refuses to move a branch head to a state +where one is not. Constraints across relations, the assertions SQL +names but rarely implements, become relations like any other. + +The idea is the denial form of integrity constraints, from Sadri and +Kowalski ("A theorem-proving approach to database integrity", 1988), +where a rule is written as a query for its own counterexamples. + +* Where denials live +Each multigroup holds its denials beside its schemas. + +#+begin_example +\system\branch\master\multigroup\library\schema\default\relation\book +\system\branch\master\multigroup\library\denial\no-books +#+end_example + +A multigroup stores a denial the way a schema stores a relation. An +[[file:../lib/kernel/EphemeralRelation.ml][ephemeral relation]] that wraps a [[file:../lib/kernel/Program.ml][program]] becomes the program's +evaluator name and source, and any other relation becomes its tuples. A +program is the usual case, because a rule has to be computed against +the state it judges. When a branch reads the denial back, the +[[file:evaluators.org][evaluator]] registered under that name parses the source, and reading +the denial invokes the program =within= the branch state it was read +through. The same denial therefore reads one state through the head +and another through =previous=. + +* Judging a state +[[file:../lib/protocols/Admission.mli][Admission]] is the protocol that judges a state. + +#+begin_src ocaml +type violations = (string * Concepts.Tuple.t) list + +class type implementation = object + method check : (violations, Concepts.Condition.condition) result +end +#+end_src + +=check= names every denial that holds a tuple, with one such tuple as +its witness. An empty list means the state is admitted. An error means +the state could not be judged, and an unjudged state is not admitted +either. + +A multigroup judges each of its denials in two steps. + +1. It asks the denial for its [[file:modes.org][modes]]. If the denial is not + exhaustible with nothing bound, the multigroup fails with + =unjudgeable-denial= and reads nothing. +2. Otherwise it reads the denial up to its first tuple. No tuple means + the denial holds. A first tuple is the witness, and the multigroup + reads no further. + +For a denial that wraps a program, the multigroup invokes the program +once, within the branch state it judges, and asks both questions of the +relation the program returns. + +A branch state asks each of its multigroups and names every violation +by its path, =\multigroup\[m]\denial\[d]=. Judging belongs to the +multigroup, the universe its relations describe. The branch only +versions states and collects the answers. A rule may still read +relations of any multigroup, because the branch asks all of them. + +One witness is enough to refuse a state, and asking for more would cost +a read of the whole denial, which never ends for a =Countable= one. + +* Trust +The guard rests on what a denial declares. A FOL denial over stored +relations derives its modes from theirs, so its claim to be finite +holds. A denial written in another language declares whatever its +evaluator returns. A program that declares =Finite= and then never ends +still hangs the check, and RNT cannot tell. The same holds when FOL +reads a relation from another evaluator, since FOL takes that +relation's modes as given. A cycle of programs across languages also +recurses without end. + +* Moving a head +=BranchManager= asks the proposed state for its admission before it +moves a head. If the state is not admitted, it refuses the move with a +=refused= condition that names each denial and its witness, and the +head stays where it was. It asks before taking the head, since a denial +may run a program that reads storage. + +#+begin_src plantuml :file ../images/denial-admission.svg +@startuml +participant "Scope.publish" as Publish +participant BranchManager +participant "proposed\nbranch state" as Branch +participant Multigroup +participant Denial + +Publish -> BranchManager : move the head +BranchManager -> Branch : check +loop each multigroup + Branch -> Multigroup : check + loop each denial + Multigroup -> Denial : modes + alt not exhaustible with nothing bound + Multigroup --> BranchManager : unjudgeable-denial + else exhaustible + Multigroup -> Denial : enumerate, read the first tuple + Denial --> Multigroup : a witness, or nothing + end + end + Multigroup --> Branch : violations +end +Branch --> BranchManager : violations, named by path +alt none + BranchManager -> BranchManager : move the head +else some + BranchManager --> Publish : refused, one witness per denial +end +@enduml +#+end_src + +#+RESULTS: +[[file:../images/denial-admission.svg]] + +The check judges the state itself, not a change to it. Every commit +lands only if the whole state it makes is admitted, whichever subsystem +made it, so a rule written in one language guards data written from +all of them. + +* Publishing denials +[[file:../lib/kernel/Scope.mli][Scope.publish]] binds denials with its relations, in the same state. + +#+begin_src ocaml +Scope.publish root ~branch:"master" ~home:library + ~denials:["no-books", Some no_books; "audit:shelved-twice", Some twice] + ["book", Some books] +#+end_src + +A name =d= binds in the home multigroup, and =m:d= binds in multigroup +=m=. A commit can install a rule and the data it guards together, and +the rule is judged with the data. If the state it makes already breaks +the rule, the commit is refused. A denial that cannot be judged cannot +be installed either, since the state that holds it cannot be admitted. + +* Judging a state without landing it +A subsystem that wants to know whether a change would be admitted builds +the state with [[file:../lib/kernel/Path.mli][Path.assoc_all]] and asks it. + +#+begin_src ocaml +let* next = Path.assoc_all head [Scope.relations library, "book", Some books] in +let* admission = Protocols.Admission.require next in +Protocols.Admission.check admission +#+end_src + +Nothing lands. A host can use this to preview a form, a move or an +import, and show which rule would refuse it. + +* Open problems +** Incremental checking +Every commit judges every denial of every multigroup over the whole +state. Decker ("Translating Advanced Integrity Checking Technology to +SQL", 2002) shows how to check only what a change can break. Take the +denial of a book shelved twice. + +#+begin_example +{(title, s1, s2) | shelved(title, s1) ∧ shelved(title, s2) ∧ s1 ≠ s2} +#+end_example + +A commit that inserts =shelved("Codd", "A")= can only add violations +where =title = "Codd"= and one shelf is ="A"=. Asking the denial for +those tuples, with the other shelf free, is the whole incremental check. +It is the insertion-only case of [[file:maintenance.org][incremental maintenance]], which covers +the delta rules it reuses. + +RNT cannot ask that today. The question binds some attributes of the +denial and leaves others free, and no operation produces the tuples of +a relation under a partial binding. This is the gap that [[file:modes.org::*Reachable bindings][reachable +bindings]] describes. Closing it takes three pieces. + +1. A binding-aware read, which every relation implements and FOL passes + through its plans. +2. Indexes, so that a substantial relation answers such a read by + lookup rather than by filtering a scan. +3. Read sets, so that RNT knows which relations a denial reads and how + their attributes line up with the denial's, and can turn an inserted + tuple into bindings on each denial it touches. + +** Denials do not protect themselves +A commit that removes a denial and breaks its rule is judged on the +state it makes, where the denial is gone, so it lands. Guarding +=\denial= needs the access checks the [[file:../README.org][README]] plans to keep apart +from lookup. + +** Multigroups from before denials +A multigroup stored before denials existed has no =denials= field and +does not load. |