Progress (particularly on protocol spec)
This commit is contained in:
parent
e06748dac0
commit
79134ee6aa
|
|
@ -86,7 +86,7 @@
|
|||
|
||||
# Specifications and Theory
|
||||
|
||||
- [Protocol specification](./protocol.md)
|
||||
- [Overview](./theory/index.md)
|
||||
|
||||
- [Syndicated Actor Model]()
|
||||
- [Actors, Entities, Assertions and Messages]()
|
||||
|
|
@ -96,4 +96,6 @@
|
|||
- [Attenuation of authority for security]()
|
||||
- [Attenuation of authority for privacy]()
|
||||
|
||||
- [Protocol specification](./protocol.md)
|
||||
|
||||
- [System layer analysis]()
|
||||
|
|
|
|||
|
|
@ -1,27 +1,100 @@
|
|||
# Glossary
|
||||
|
||||
## Action
|
||||
## Actor
|
||||
## Assertion
|
||||
## Attenuation
|
||||
## Capability
|
||||
|
||||
a.k.a. Cap
|
||||
|
||||
Pointer or handle denoting a live, stateful [entity](#entity) running within an
|
||||
[actor](#actor). The entity accepts [Preserves](#preserves)-format [messages](#message) and/or
|
||||
[assertions](#assertion). The capability may be [attenuated](#attenuation) to restrict the
|
||||
messages and assertions that may be delivered to the denoted entity by way of this particular
|
||||
handle.
|
||||
|
||||
## Compositional
|
||||
## Configuration Scripting Language
|
||||
## Conversational State
|
||||
## Dataspace
|
||||
## E
|
||||
## Embedded References
|
||||
## Entity
|
||||
## Event
|
||||
## Facet
|
||||
## Initial OID
|
||||
## Initial Ref
|
||||
## Macaroon
|
||||
|
||||
[*“Macaroons: Cookies with Contextual Caveats for Decentralized Authorization in the
|
||||
Cloud.”*](https://research.google/pubs/pub41892/), by Arnar Birgisson, Joe Gibbs Politz, Úlfar
|
||||
Erlingsson, Ankur Taly, Michael Vrable, and Mark Lentczner. In Proc. Network and Distributed
|
||||
System Security Symposium (NDSS), 2014. [[PDF]](https://research.google/pubs/pub41892.pdf)
|
||||
|
||||
## Membrane
|
||||
## Message
|
||||
## Network
|
||||
|
||||
A network is a group of peers, plus a medium of communication, an addressing model, and an
|
||||
associated [scope](#scope).
|
||||
|
||||
## Object Capability Model
|
||||
## Observe
|
||||
## OID
|
||||
## Preserves
|
||||
## Record
|
||||
a Preserves record
|
||||
## Reference
|
||||
a.k.a. Ref
|
||||
## Relay
|
||||
## Relay Entity
|
||||
## S6
|
||||
## Schema
|
||||
## Scope
|
||||
|
||||
A *scope* maps [refs](#reference) to the [entities](#entity) they denote. Scopes exist in
|
||||
one-to-one relationship to [networks](#network). Because [message bodies](#message) and
|
||||
[asserted values](#assertion) contain [embedded references](#embedded-references), each message
|
||||
and assertion transmitted via some network is also inseparable from its scope.
|
||||
|
||||
Most [actors](#actor) will participate in a single scope. However, [relay](#relay) actors
|
||||
participate in two or more scopes, translating refs back and forth as messages and assertions
|
||||
traverse the relay.
|
||||
|
||||
**Examples.**
|
||||
|
||||
1. A process is a scope for in-memory values: in-memory refs contain direct pointers to
|
||||
entities, which cannot be interpreted outside the context of the process's address space.
|
||||
The "network" associated with the process's scope is the intra-process graph of object
|
||||
references.
|
||||
|
||||
2. A TCP/IP socket (or serial link, or WebSocket, or Unix socket, etc.) is a scope for values
|
||||
travelling between two connected processes: [refs on the wire](#wire-symbol) denote
|
||||
entities owned by one or the other of the two participants. The "network" for a socket's
|
||||
scope is exactly the two connected peers (NB. and is *not* the underlying TCP/IP network,
|
||||
HTTP network, or Unix kernel that supports the point-to-point link).
|
||||
|
||||
3. An ethernet segment is a scope for values broadcast among stations: the embedded refs are
|
||||
(MAC address, [OID](#oid)) pairs. The network is the set of participating peers.
|
||||
|
||||
4. A running web page is a scope for the JavaScript objects it contains: both local and remote
|
||||
entities are represented by JavaScript objects. The "network" is the JavaScript heap.
|
||||
|
||||
## Supervision tree
|
||||
## Supervisor
|
||||
## Sync Peer Entity
|
||||
## Synchronization
|
||||
(`sync` action)
|
||||
## Syndicated Actor Model
|
||||
|
||||
Often abbreviated **SAM**.
|
||||
|
||||
Source [entities](#entity) running within an [actor](#actor) publish [assertions](#assertion)
|
||||
and send [messages](#message) to target entities, possibly in other actors.
|
||||
|
||||
## System Layer
|
||||
## System dataspace
|
||||
## System Dataspace
|
||||
## Transport
|
||||
## Turn
|
||||
## Wire Symbol
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
# Synit: an Alternative System Layer
|
||||
# Synit: a Reactive Operating System
|
||||
|
||||
## Welcome!
|
||||
|
||||
Synit is an experiment in applying the [Syndicated Actor
|
||||
Model](./glossary.md#syndicated-actor-model) to the [System
|
||||
Layer](./glossary.md#system-layer) of an operating system for personal
|
||||
computers, including laptops, desktops, and mobile phones.
|
||||
Synit is an experiment in applying **pervasive reactivity** and **object capabilities** to the
|
||||
[System Layer](./glossary.md#system-layer) of an operating system for personal computers,
|
||||
including laptops, desktops, and mobile phones. Its [architecture](./architecture.md) follows
|
||||
the principles of the [Syndicated Actor Model](./glossary.md#syndicated-actor-model).
|
||||
|
||||
Synit builds upon the Linux kernel, but replaces many pieces of
|
||||
familiar Linux software, including `systemd`, `NetworkManager`,
|
||||
|
|
|
|||
670
src/protocol.md
670
src/protocol.md
|
|
@ -1 +1,669 @@
|
|||
# Protocol
|
||||
# Syndicate Protocol
|
||||
|
||||
Actors in the same local [scope](./glossary#scope) communicate directly. To communicate further
|
||||
afield, scopes may be *connected* using [relay actors](./glossary.md#relay). Relays allow
|
||||
*indirect* communication: distant entities can be addressed as if they were local.
|
||||
|
||||
Relays exchange *Syndicate Protocol* messages across a [transport](./glossary.md#transport). A
|
||||
*transport* is the underlying medium connecting one relay to its counterparts on a given
|
||||
network. For example, a TLS-on-TCP/IP socket may connect a pair of relays to one another, or a
|
||||
UDP multicast socket may connect an entire group of relays across an ethernet.
|
||||
|
||||
```ditaa protocol-transport
|
||||
+-------------+ +-------------+
|
||||
| | transport | |
|
||||
| +-----+ +------------------------+ +-----+ |
|
||||
|. . . |Relay|<-->| TLS/TCP/IP socket |<-->|Relay| . . . |
|
||||
| +-----+ +------------------------+ +-----+ |
|
||||
| | | |
|
||||
+-------------+ +-------------+
|
||||
```
|
||||
|
||||
## Transport requirements
|
||||
|
||||
Transports must
|
||||
|
||||
- be able to carry [Preserves](./glossary.md#preserves) values back and forth,
|
||||
- be reliable and in-order,
|
||||
- have a well-defined lifecycle (created → connected → disconnected), and
|
||||
- assure confidentiality, integrity and replay-resistance.
|
||||
|
||||
This document focuses primarily on point-to-point transports, discussing multicast and
|
||||
in-memory variations briefly toward the end.
|
||||
|
||||
## Roles and session establishment
|
||||
|
||||
The protocol is completely symmetric, aside from [certain conventions detailed
|
||||
below](#well-known-oids) about the entities available for use immediately upon connection
|
||||
establishment. It is *not* a client/server protocol.
|
||||
|
||||
To begin a session on a newly-established point-to-point link, a relay simply starts sending
|
||||
packets. Each peer starts the session with an empty entity reference map ([see
|
||||
below](#membranes)) and making no assertions in either the outbound (on behalf of local
|
||||
entities) or inbound (on behalf of the remote peer) directions.
|
||||
|
||||
## Packet definitions
|
||||
|
||||
```preserves-schema
|
||||
Packet = Turn / Error / Extension .
|
||||
```
|
||||
|
||||
Packets exchanged by relays are [Preserves](./glossary.md#preserves) values defined using
|
||||
Preserves [schema](./glossary.md#schema).
|
||||
|
||||
A packet may be a *turn*, an *error*, or an *extension*.
|
||||
|
||||
Packets are neither commands nor responses; they are *events*.
|
||||
|
||||
### Extension packets
|
||||
|
||||
```preserves-schema
|
||||
Extension = <<rec> @label any @fields [any ...]> .
|
||||
```
|
||||
|
||||
An extension packet must be a Preserves [record](./glossary.md#record), but is otherwise
|
||||
unconstrained.
|
||||
|
||||
**Handling.**
|
||||
Peers MUST ignore extensions that they do not understand.[^no-extensions-yet]
|
||||
|
||||
### Error packets
|
||||
|
||||
```preserves-schema
|
||||
Error = <error @message string @detail any>.
|
||||
```
|
||||
|
||||
**Handling.**
|
||||
An error packet describes something that went wrong on the other end of the connection. Error
|
||||
packets are primarily intended for debugging.
|
||||
|
||||
Receipt of an error packet denotes that the sender has terminated (crashed) and will not
|
||||
respond further; the connection will usually be closed shortly thereafter.
|
||||
|
||||
Error packets are *optional*: connections may simply be closed without comment.
|
||||
|
||||
### Turn packets
|
||||
|
||||
```preserves-schema
|
||||
Turn = [TurnEvent ...].
|
||||
TurnEvent = [@oid Oid @event Event].
|
||||
Event = Assert / Retract / Message / Sync .
|
||||
|
||||
Assert = <assert @assertion Assertion @handle Handle>.
|
||||
Retract = <retract @handle Handle>.
|
||||
Message = <message @body Assertion>.
|
||||
Sync = <sync @peer #!#t>.
|
||||
|
||||
Assertion = any .
|
||||
Handle = int .
|
||||
Oid = int .
|
||||
```
|
||||
|
||||
A `Turn` is the most important packet variant. It directly reflects the
|
||||
[SAM](./glossary.md#syndicated-actor-model) notion of a [turn](./glossary.md#turn).
|
||||
|
||||
**Handling.** Each `Turn` carries [events](./glossary.md#event) to be delivered to
|
||||
[entities](./glossary.md#entity) residing at the receiving end of the transport.
|
||||
|
||||
The `assertion` fields of `Assert` events and the `body` fields of `Message` events may contain
|
||||
any Preserves value, including embedded entity references. On the wire, these will always be
|
||||
formatted [as described below](#capabilities-on-the-wire). Upon receipt of a `Turn`, embedded
|
||||
references are first mapped to internal references. Prior to transmission, internal references
|
||||
are mapped to their external form. [The mapping procedure to follow is detailed
|
||||
below.](#membranes)
|
||||
|
||||
After reference rewriting is complete, the sequence of `TurnEvent`s is examined. The
|
||||
[OID](./glossary.md#oid) in each `TurnEvent` selects an entity known to the recipient. Each
|
||||
`Event` is either publication of an assertion, retraction of a previously-published assertion,
|
||||
delivery of a single message, or a [synchronization](./glossary.md#synchronization) event.
|
||||
|
||||
In the case that the receiving party is structured internally using the SAM, it is important to
|
||||
preserve turn boundaries. Since turn boundaries are a per-[actor](./glossary.md#actor) concept,
|
||||
but a `Turn` mentions only entities, the receiver must map entities to actors, group
|
||||
`TurnEvent`s into per-actor queues, and deliver those queues to each actor in a single SAM turn
|
||||
for each actor.
|
||||
|
||||
The `Handle`s used to refer to published assertions MUST be unique within the scope of the
|
||||
transport connection.
|
||||
|
||||
## Capabilities on the wire
|
||||
|
||||
Packets sent and received on a point-to-point transport frequently include embedded references.
|
||||
These references denote *capabilities* for interacting with some entity.
|
||||
|
||||
For example, assertion of a capability-bearing record could appear as the following `Event`:
|
||||
|
||||
```preserves
|
||||
<assert <please-reply-to #![0 555]>>
|
||||
```
|
||||
|
||||
The `#![0 555]` is [concrete Preserves text syntax](./guide/preserves.md#concrete-syntax) for
|
||||
an embedded (`#!`) value (`[0 555]`).
|
||||
|
||||
In the Syndicate Protocol, these embedded values MUST conform to the `WireRef`
|
||||
schema:[^slightly-silly-wireref]
|
||||
|
||||
```preserves-schema
|
||||
WireRef = @mine [0 @oid Oid] / @yours [1 @oid Oid @attenuation Caveat ...].
|
||||
Oid = int .
|
||||
```
|
||||
|
||||
The `mine` variant denotes capability references managed by the *sender* of a given packet; the
|
||||
`yours` variant, the *receiver* of the packet. Accordingly, if a relay receives a packet
|
||||
mentioning `#![0 555]`, it will later use `#![1 555]` if it needs to send a packet to refer to
|
||||
that same entity.
|
||||
|
||||
### Attenuation of authority
|
||||
|
||||
A `yours`-variant capability may include a request[^attenuation-is-not-enforceable] to impose
|
||||
additional conditions on the receiver's use of its own capability, known as an
|
||||
[attenuation](./glossary.md#attenuation) of the capability's authority.
|
||||
|
||||
An attenuation is a chain of `Caveat`s.[^caveat-terminology-macaroon] A `Caveat` acts as a
|
||||
function that, given a Preserves value representing an assertion or message body, yields either
|
||||
a possibly-rewritten value, or no value at all. In the latter case, the value has been
|
||||
*rejected*. In the former case, the rewritten value is used as input to the next `Caveat` in
|
||||
the chain, or as the final assertion or message body for delivery to the entity backing the
|
||||
capability.
|
||||
|
||||
The chain of `Caveats` in an attenuation is written down in *reverse* order: newer `Caveat`s
|
||||
are appended to the sequence, and each `Caveat`'s output is fed into the input of the next
|
||||
leftward `Caveat` in the sequence. If no `Caveat`s are present, the capability is unattenuated,
|
||||
and inputs are passed through to the backing capability unmodified.
|
||||
|
||||
```preserves-schema
|
||||
Caveat = Rewrite / Alts .
|
||||
|
||||
Rewrite = <rewrite @pattern Pattern @template Template>.
|
||||
Alts = <or @alternatives [Rewrite ...]>.
|
||||
```
|
||||
|
||||
A `Caveat` can be either a single `Rewrite` or a sequence of alternative possible rewrites,
|
||||
tried in left-to-right order until one of them accepts the input or there are none left to try.
|
||||
(A single `Rewrite` *R* is equivalent to `<or [`*R*`]>`.)
|
||||
|
||||
A `Rewrite` applies its `Pattern` to the input to the `Caveat`. If it matches, the bindings
|
||||
captured by the pattern are gathered together and used in instantiation of the `Rewrite`'s
|
||||
`Template`, yielding the output from the `Caveat`. If the pattern does not match, the `Rewrite`
|
||||
has rejected the input, and other `alternatives` are tried until none remain, at which point
|
||||
the whole `Caveat` has rejected the input and processing of the triggering event stops.
|
||||
|
||||
#### Patterns
|
||||
|
||||
A `Pattern` within a rewrite can be any of the following variants:
|
||||
|
||||
```preserves-schema
|
||||
Pattern = PDiscard / PAtom / PEmbedded / PBind / PAnd / PNot / Lit / PCompound .
|
||||
```
|
||||
|
||||
`PDiscard` matches any value:
|
||||
|
||||
```preserves-schema
|
||||
PDiscard = <_>.
|
||||
```
|
||||
|
||||
`PAtom` requires that a matched value be a boolean, a single- or double-precision float, an
|
||||
integer, a string, a binary blob, or a symbol, respectively:
|
||||
|
||||
```preserves-schema
|
||||
PAtom = =Boolean / =Float / =Double / =SignedInteger / =String / =ByteString / =Symbol .
|
||||
```
|
||||
|
||||
`PEmbedded` requires that a matched value be an embedded capability:
|
||||
|
||||
```preserves-schema
|
||||
PEmbedded = =Embedded .
|
||||
```
|
||||
|
||||
`PBind` first *captures* the matched value, adding it to the bindings vector, and then applies
|
||||
the nested `pattern`. If the subpattern matches, the `PBind` succeeds; otherwise, it fails:
|
||||
|
||||
```preserves-schema
|
||||
PBind = <bind @pattern Pattern>.
|
||||
```
|
||||
|
||||
`PAnd` is a conjunction of patterns; every pattern in `patterns` must match for the `PAnd` to
|
||||
match:
|
||||
|
||||
```preserves-schema
|
||||
PAnd = <and @patterns [Pattern ...]>.
|
||||
```
|
||||
|
||||
`PNot` is a pattern negation: if `pattern` matches, the `PNot` fails to match, and *vice
|
||||
versa*. It is an error for `pattern` to include any `PBind` subpatterns.
|
||||
|
||||
```preserves-schema
|
||||
PNot = <not @pattern Pattern>.
|
||||
```
|
||||
|
||||
`Lit` is an exact match pattern. If the matched value is exactly equal to `value` (according to
|
||||
Preserves' own built-in equivalence relation), the match succeeds; otherwise, it fails:
|
||||
|
||||
```preserves-schema
|
||||
Lit = <lit @value any>.
|
||||
```
|
||||
|
||||
Finally, `PCompound` patterns match compound data structures. The `rec` variant demands that a
|
||||
matched value be a record, with label exactly equal to `label` and fields one-for-one matching
|
||||
the `Pattern`s in `fields`; the `arr` variant demands a sequence, with each element matching
|
||||
the corresponding element of `items`; and `dict` demands a dictionary having *at least* entries
|
||||
named by the keys of the `entries` dictionary, each matching the corresponding `Pattern`.
|
||||
|
||||
```preserves-schema
|
||||
PCompound =
|
||||
/ @rec <rec @label any @fields [Pattern ...]>
|
||||
/ @arr <arr @items [Pattern ...]>
|
||||
/ @dict <dict @entries { any: Pattern ...:... }> .
|
||||
```
|
||||
|
||||
#### Bindings
|
||||
|
||||
Bindings resulting from matching are stored as a sequence of values.
|
||||
|
||||
During matching, when a `PBind` pattern is seen, the matcher *first* appends the matched value
|
||||
to the binding sequence and *then* recurses on the nested subpattern. This makes binding
|
||||
*indexes* appear in left-to-right order as a `Pattern` is read.
|
||||
|
||||
For example, given the pattern `<bind <arr [<bind <_>>, <bind <_>>]>>` and the matched value
|
||||
`[1 2]`, the resulting captured values will be, in order, `[1 2]`, `1`, and `2`.
|
||||
|
||||
#### Templates
|
||||
|
||||
A `Template` within a rewrite produces a concrete Preserves value when instantiated with a
|
||||
vector of captured binding values. Template instantiation may fail, yielding no value.
|
||||
|
||||
A given `Template` may be any of the following variants:
|
||||
|
||||
```preserves-schema
|
||||
Template = TAttenuate / TRef / Lit / TCompound .
|
||||
```
|
||||
|
||||
`TAttenuate` first instantiates the sub-`template`. If it yields a value, and if that value is
|
||||
an embedded reference (i.e. a capability), the `Caveat`s in `attenuation` are appended to the
|
||||
(possibly-empty) sequence of `Caveat`s already present in the embedded capability. The
|
||||
resulting possibly-attenuated capability is the final result of instantiation of the
|
||||
`TAttenuate`.
|
||||
|
||||
```preserves-schema
|
||||
TAttenuate = <attenuate @template Template @attenuation [Caveat ...]>.
|
||||
```
|
||||
|
||||
`TRef` retrieves the `binding`th (0-based) index into the bindings vector, yielding the
|
||||
associated captured value as the result of instantiation. It is an error if `binding` is less
|
||||
than zero, or greater than or equal to the number of bindings in the bindings vector.
|
||||
|
||||
```preserves-schema
|
||||
TRef = <ref @binding int>.
|
||||
```
|
||||
|
||||
`Lit` (the same definition as used in the grammar for `Pattern` above) instantiates to exactly
|
||||
its `value` argument:
|
||||
|
||||
```preserves-schema
|
||||
Lit = <lit @value any>.
|
||||
```
|
||||
|
||||
Finally, `TCompound` instantiates to compound data. The `rec` variant produces a record with
|
||||
the given `label` and `fields`; `arr` produces an array; and `dict` a dictionary:
|
||||
|
||||
```preserves-schema
|
||||
TCompound =
|
||||
/ @rec <rec @label any @fields [Template ...]>
|
||||
/ @arr <arr @items [Template ...]>
|
||||
/ @dict <dict @entries { any: Template ...:... }> .
|
||||
```
|
||||
|
||||
#### Validity of Caveats
|
||||
|
||||
The above definitions imply some *validity constraints* on `Caveat`s.
|
||||
|
||||
- All `TRef`s must be bound: the index referred to must relate to the index associated with
|
||||
some `PBind` in the pattern corresponding to the template.
|
||||
|
||||
- Binding under negation is forbidden: a `pattern` within a `PNot` may not include any `PBind`
|
||||
constructors.
|
||||
|
||||
- The value produced by instantiation of `template` within a `TAttenuate` must be an embedded
|
||||
reference (a capability).
|
||||
|
||||
Implementations MUST enforce these constraints (either statically or dynamically).
|
||||
|
||||
#### Pseudocode for attenuation, pattern matching, and template instantiation
|
||||
|
||||
##### Attenuation
|
||||
```python
|
||||
def attenuate(attenuation, value):
|
||||
for caveat in reversed(attenuation):
|
||||
value = applyCaveat(caveat, value)
|
||||
if value is None:
|
||||
return None
|
||||
return value
|
||||
|
||||
def applyCaveat(caveat, value):
|
||||
if caveat is 'Alts' variant:
|
||||
for rewrite in caveat.alternatives:
|
||||
possibleResult = tryRewrite(rewrite, value);
|
||||
if possibleResult is not None:
|
||||
return possibleResult
|
||||
return None
|
||||
if caveat is 'Rewrite' variant:
|
||||
return tryRewrite(caveat, value)
|
||||
|
||||
def tryRewrite(rewrite, value):
|
||||
bindings = applyPattern(rewrite.pattern, value)
|
||||
if bindings is None:
|
||||
return None
|
||||
else:
|
||||
return instantiateTemplate(rewrite.template, bindings)
|
||||
```
|
||||
|
||||
##### Pattern matching
|
||||
```python
|
||||
def match(pattern, value, bindings):
|
||||
if pattern is 'PDiscard' variant:
|
||||
return True
|
||||
if pattern is 'PAtom' variant:
|
||||
return True if value is of the appropriate atomic class else False
|
||||
if pattern is 'PEmbedded' variant:
|
||||
return True if value is a capability else False
|
||||
if pattern is 'PBind' variant:
|
||||
append value to bindings
|
||||
return match(pattern.pattern, value, bindings)
|
||||
if pattern is 'PAnd' variant:
|
||||
for p in pattern.patterns:
|
||||
if not match(p, value, bindings):
|
||||
return False
|
||||
return True
|
||||
if pattern is 'PNot' variant:
|
||||
return False if match(pattern.pattern, value, bindings) else True
|
||||
if pattern is 'Lit' variant:
|
||||
return (pattern.value == value)
|
||||
if pattern is 'PCompound' variant:
|
||||
if pattern is 'rec' variant:
|
||||
if value is not a record: return False
|
||||
if value.label is not equal to pattern.label: return False
|
||||
if value.fields.length is not equal to pattern.fields.length: return False
|
||||
for i in [0 .. pattern.fields.length):
|
||||
if not match(pattern.fields[i], value.fields[i], bindings):
|
||||
return False
|
||||
return True
|
||||
if pattern is 'arr' variant:
|
||||
if value is not a sequence: return False
|
||||
if value.length is not equal to pattern.items.length: return False
|
||||
for i in [0 .. pattern.items.length):
|
||||
if not match(pattern.items[i], value[i], bindings):
|
||||
return False
|
||||
return True
|
||||
if pattern is 'dict' variant:
|
||||
if value is not a dictionary: return False
|
||||
for k in keys of pattern.entries:
|
||||
if k not in keys of value: return False
|
||||
if not match(pattern.entries[k], value[k], bindings):
|
||||
return False
|
||||
return True
|
||||
```
|
||||
|
||||
##### Template instantiation
|
||||
```python
|
||||
def instantiate(template, bindings):
|
||||
if template is 'TAttenuate' variant:
|
||||
c = instantiate(template.template, bindings)
|
||||
if c is not a capability: raise an exception
|
||||
c′ = c with the caveats in template.attenuation appended to the existing
|
||||
attenuation in c
|
||||
return c′
|
||||
if template is 'TRef' variant:
|
||||
if 0 ≤ template.binding < bindings.length:
|
||||
return bindings[template.binding]
|
||||
else:
|
||||
raise an exception
|
||||
if template is 'Lit' variant:
|
||||
return template.value
|
||||
if template is 'TCompound' variant:
|
||||
if template is 'rec' variant:
|
||||
return Record(label=template.label,
|
||||
fields=[instantiate(t, bindings) for t in template.fields])
|
||||
if template is 'arr' variant:
|
||||
return [instantiate(t, bindings) for t in template.items]
|
||||
if template is 'dict' variant:
|
||||
result = {}
|
||||
for k in keys of template.entries:
|
||||
result[k] = instantiate(template.entries[k], bindings)
|
||||
return result
|
||||
```
|
||||
|
||||
## Membranes
|
||||
|
||||
In order to correctly map between embedded references on the wire and entity references local
|
||||
to the relay, the relay maintains two stateful objects called *membranes*. A membrane is a
|
||||
bidirectional mapping between [OID](./glossary.md#oid) and relay-internal entity pointer.
|
||||
|
||||
- The *import membrane* connects OIDs managed by the *remote* peer to local *relay entities*
|
||||
which proxy access to an "imported" remote entity.
|
||||
|
||||
- The *export membrane* connects OIDs managed by the *local* peer to any local "exported"
|
||||
entities accessible to the peer.
|
||||
|
||||
```ditaa membranes
|
||||
|
|
||||
|
|
||||
Export Membrane | Import Membrane
|
||||
|
|
||||
+-+ | +-+
|
||||
Pointer | | ID | ID | |
|
||||
0x1234 <-+-+-> "my 7" | "your 7"<-+-+-> 0x9abc
|
||||
| | | | |
|
||||
^ | | ^ | ^ | | ^
|
||||
| | | | -+- | | | |
|
||||
V | | | | | | V
|
||||
/------\ | | \-------------/ | | /------\
|
||||
|Entity| | | | | |Relay |<-- ...
|
||||
\------/ | | | | |Entity|
|
||||
0x1234 | | --------> | | \------/
|
||||
=-------------+-+---= packets | | 0x9abc
|
||||
0x462e | | <-------- =---+-+-------------=
|
||||
/------\ | | | | 0xa043
|
||||
|Relay | | | | | /------\
|
||||
... -->|Entity| | | /-------------\ | | |Entity|
|
||||
\------/ | | | | | | \------/
|
||||
^ | | | -+- | | | ^
|
||||
| | | | | | | | |
|
||||
V | | V | V | | V
|
||||
| | | | |
|
||||
0x462e <-+-+->"your 3" | "my 3" <-+-+-> 0xa043
|
||||
Pointer | | ID | ID | | Pointer
|
||||
+-+ | +-+
|
||||
|
|
||||
Import Membrane | Export Membrane
|
||||
|
|
||||
|
|
||||
```
|
||||
|
||||
|
||||
```ditaa one-sided-membrane
|
||||
---------------------------------------+
|
||||
|
|
||||
Membrane |
|
||||
----+---- |
|
||||
/--\ | | |
|
||||
|A1|<----+ Pointer | ID +-+-------------transport---
|
||||
\--/ | |
|
||||
+---0x7f1065218700<-+-> 7
|
||||
| <---- from remote
|
||||
/--\ | peer
|
||||
|A2|<-----0x7f1065229780<-+-> 11
|
||||
\--/ |
|
||||
| ----> to remote
|
||||
+--0x7f10652fe7c0<-+-> 13 peer
|
||||
/--\ | |
|
||||
|A3|<----+ | +-+-------------------------
|
||||
\--/ | |
|
||||
|
|
||||
|
|
||||
----------------------------------------+
|
||||
```
|
||||
|
||||
|
||||
<!--
|
||||
Each relay rewrites the embedded references in the messages it sends and receives. It maps back
|
||||
and forth between one scope's name for an entity and the other scope's name for the same
|
||||
entity.
|
||||
|
||||
|
||||
```ditaa protocol-scope-chains
|
||||
(Illustrative Example)
|
||||
|
||||
Browser syndicate–server
|
||||
+----------------+ WebSocket +-------+-----------------------+
|
||||
|In–browser scope|<----------->| Relay |<-\ |
|
||||
+----------------+ (2) +-------+ | +---------+ |
|
||||
| ^ \->|Dataspace| |
|
||||
| | +---------+ |
|
||||
| V ^ ^ ^ (1) |
|
||||
+----------------+ TCP/IP +-------+ | | | |
|
||||
|Remote Syndicate|<----------->| Relay |<----+-/ | | |
|
||||
|server/dataspace| (3) +-------+ | | | |
|
||||
+----------------+ | V V V |
|
||||
| +-------+ +-------+ |
|
||||
| | Relay | | Relay | |
|
||||
+----------+-------+-+-------+--+
|
||||
^ ^
|
||||
LAN multicast (4) | | UNIX
|
||||
... <-------/---------/---------/---------/ | socket
|
||||
| | | | (5)
|
||||
v v v v
|
||||
+-------+ +-------+ +-------+ +-------+
|
||||
|. . . | |. . . | |. . . | |. . . |
|
||||
+-------+ +-------+ +-------+ +-------+
|
||||
```
|
||||
|
||||
In the diagram above, networks (scopes) 1 and 4 are *multicast*, while networks 2, 3 and 5 are
|
||||
*point-to-point*. Four relays bridge scope 1 to scopes 2 through 5. Within each scope, peers
|
||||
are able to interact with each other directly. Each point-to-point scope contains exactly two
|
||||
peers.
|
||||
|
||||
-->
|
||||
|
||||
## Client and server roles
|
||||
|
||||
## Well-known OIDs
|
||||
|
||||
OID 0, initial ref, initial oid
|
||||
|
||||
## Security considerations
|
||||
|
||||
### Secrecy
|
||||
|
||||
### Privacy
|
||||
|
||||
## Specific transport mappings
|
||||
|
||||
TCP/IP
|
||||
|
||||
TLS TCP/IP
|
||||
|
||||
WebSockets
|
||||
|
||||
|
||||
## Other kinds of medium
|
||||
|
||||
Multicast/broadcast, in-memory
|
||||
|
||||
## Reference: Complete schema of the protocol
|
||||
|
||||
The following is a consolidated form of the definitions from the text above.
|
||||
|
||||
### Protocol packets
|
||||
|
||||
The authoritative
|
||||
version of this schema is
|
||||
[`[syndicate-protocols]/schemas/protocol.prs`](https://git.syndicate-lang.org/syndicate-lang/syndicate-protocols/src/branch/main/schemas/protocol.prs).
|
||||
|
||||
```preserves-schema
|
||||
version 1 .
|
||||
|
||||
Packet = Turn / Error / Extension .
|
||||
|
||||
Extension = <<rec> @label any @fields [any ...]> .
|
||||
|
||||
Error = <error @message string @detail any>.
|
||||
|
||||
Assertion = any .
|
||||
Handle = int .
|
||||
Event = Assert / Retract / Message / Sync .
|
||||
Oid = int .
|
||||
Turn = [TurnEvent ...].
|
||||
TurnEvent = [@oid Oid @event Event].
|
||||
|
||||
Assert = <assert @assertion Assertion @handle Handle>.
|
||||
Retract = <retract @handle Handle>.
|
||||
Message = <message @body Assertion>.
|
||||
Sync = <sync @peer #!#t>.
|
||||
```
|
||||
|
||||
### Capabilities, WireRefs, and attenuations
|
||||
|
||||
The authoritative version of this schema is
|
||||
[`[syndicate-protocols]/schemas/sturdy.prs`](https://git.syndicate-lang.org/syndicate-lang/syndicate-protocols/src/branch/main/schemas/sturdy.prs).
|
||||
|
||||
```preserves-schema
|
||||
version 1 .
|
||||
|
||||
Attenuation = [Caveat ...].
|
||||
|
||||
Caveat = Rewrite / Alts .
|
||||
Rewrite = <rewrite @pattern Pattern @template Template>.
|
||||
Alts = <or @alternatives [Rewrite ...]>.
|
||||
|
||||
Oid = int .
|
||||
WireRef = @mine [0 @oid Oid] / @yours [1 @oid Oid @attenuation Caveat ...].
|
||||
|
||||
Lit = <lit @value any>.
|
||||
|
||||
Pattern = PDiscard / PAtom / PEmbedded / PBind / PAnd / PNot / Lit / PCompound .
|
||||
PDiscard = <_>.
|
||||
PAtom = =Boolean / =Float / =Double / =SignedInteger / =String / =ByteString / =Symbol .
|
||||
PEmbedded = =Embedded .
|
||||
PBind = <bind @pattern Pattern>.
|
||||
PAnd = <and @patterns [Pattern ...]>.
|
||||
PNot = <not @pattern Pattern>.
|
||||
PCompound =
|
||||
/ @rec <rec @label any @fields [Pattern ...]>
|
||||
/ @arr <arr @items [Pattern ...]>
|
||||
/ @dict <dict @entries { any: Pattern ...:... }> .
|
||||
|
||||
Template = TAttenuate / TRef / Lit / TCompound .
|
||||
TAttenuate = <attenuate @template Template @attenuation Attenuation>.
|
||||
TRef = <ref @binding int>.
|
||||
TCompound =
|
||||
/ @rec <rec @label any @fields [Template ...]>
|
||||
/ @arr <arr @items [Template ...]>
|
||||
/ @dict <dict @entries { any: Template ...:... }> .
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
#### Notes
|
||||
|
||||
[^no-extensions-yet]: This specification does not define any extensions, but future revisions
|
||||
could, for example, use extensions to perform version-negotiation. Another potential future
|
||||
use could be to propagate provenance information for tracing/debugging.
|
||||
|
||||
[^slightly-silly-wireref]: The syntax for `WireRef`s is slightly silly, using tuples as
|
||||
quasi-records with `0` and `1` acting as quasi-labels. It would probably be better to use
|
||||
real records, like `<my @oid Oid>` and `<yours @oid Oid @attenuation [Caveat ...]>`. Pros:
|
||||
less cryptic. Cons: slightly more verbose on the wire. TODO: should we revise the spec in
|
||||
this regard?
|
||||
|
||||
[^attenuation-is-not-enforceable]: Such conditions can only ever be requests: after all, every
|
||||
`yours`-capability is already completely accessible to the recipient of the packet.
|
||||
Similarly, it does not make sense to include an attenuation description on a
|
||||
`my`-capability. However, in every case, if a party wishes to *enforce* an attenuation on a
|
||||
`my`- or `yours`-capability, it may record the attenuation against the underlying
|
||||
capability internally, issuing to its peers a fresh `my`-capability denoting the attenuated
|
||||
capability.
|
||||
|
||||
[^caveat-terminology-macaroon]: This terminology, "caveat", is lifted from the excellent paper
|
||||
on [Macaroons](./glossary.md#macaroon), where it is used to describe a more general
|
||||
mechanism. Future versions of this specification may opt to include some of this
|
||||
generality.
|
||||
|
|
|
|||
|
|
@ -0,0 +1,5 @@
|
|||
# Specifications and Theory
|
||||
|
||||
TODO: links
|
||||
|
||||
[Protocol](../protocol.md)
|
||||
Loading…
Reference in New Issue