arc.bend checks

raw source on the hub · import 0x87f59fd07e5027177b8036b68fe915f8/arc.bend as Arc

1 import

import Base

Types

type NodeRole source · line 12 · raw

Data

---- vocabulary ---- UserDevice: a user's own device. Server: a machine the project runs. Overlay: the private (overlay) network between them. Outside: someone else's servers.

UserDevice
```
NodeRole
```
Server
```
NodeRole
```
Overlay
```
NodeRole
```
Outside
```
NodeRole
```

type Node source · line 18 · raw

Data

Node

@key:String -> @name:String -> @role:NodeRole -> Node

type ContainerKind source · line 26 · raw

Data

What a container is. The list is closed: something that is none of these is not a container. Client: the app, on the user's device. Network: the private network between client and server. DataApi: answers queries on records and changes them. AgentApi: runs agent threads. ModelApi: answers model calls. Worker: has no API of its own; it only moves data between data APIs, so it is the first thing to fold into a data API's own actions.

Client
```
ContainerKind
```
Network
```
ContainerKind
```
DataApi
```
ContainerKind
```
AgentApi
```
ContainerKind
```
ModelApi
```
ContainerKind
```
Worker
```
ContainerKind
```

type Owner source · line 35 · raw

Data

Whether the project builds and runs it, or uses it as it is.

Ours
```
Owner
```
Theirs
```
Owner
```

type Exposure source · line 40 · raw

Data

Who can reach it: its own machine (127.0.0.1), the local network, the private network, the device it is on, anyone.

Local
```
Exposure
```
Lan
```
Exposure
```
Tailnet
```
Exposure
```
Device
```
Exposure
```
Public
```
Exposure
```

type Cap source · line 49 · raw

Data

What a container provides. Hosting is serving the app itself (its HTML and scripts); a data API may also host the app only while it is private (shared_hosting_ok).

Hosting
```
Cap
```
PrivateAccess
```
Cap
```
PrivateHosting
```
Cap
```
Realtime
```
Cap
```
BlobStore
```
Cap
```

type Lang source · line 56 · raw

Data

Rust
```
Lang
```
TypeScript
```
Lang
```
JavaScript
```
Lang
```
Python
```
Lang
```
Opaque
```
Lang
```

type Container source · line 63 · raw

Data

Container

@key:String -> @name:String -> @kind:ContainerKind -> @owner:Owner -> @on:String -> @exposure:Exposure -> @caps:List<&2, Cap> -> Container

type Part source · line 66 · raw

Data

Part

@key:String -> @name:String -> @lang:Lang -> @in:String -> Part

type Link source · line 70 · raw

Data

A talks-to edge between two containers or parts, by key.

Link

@src:String -> @dst:String -> @label:String -> @live:Bool -> Link

type System source · line 73 · raw

Data

System

@nodes:List<&2, Node> -> @containers:List<&2, Container> -> @parts:List<&2, Part> -> @links:List<&2, Link> -> System

Definitions

def nodes source · line 77 · raw

@s:System -> List<&2, Node>

---- access ----

def containers source · line 82 · raw

@s:System -> List<&2, Container>

def parts source · line 87 · raw

@s:System -> List<&2, Part>

def links source · line 92 · raw

@s:System -> List<&2, Link>

def nkey source · line 97 · raw

@n:Node -> String

def ckey source · line 102 · raw

@c:Container -> String

def con source · line 107 · raw

@c:Container -> String

def caps source · line 112 · raw

@c:Container -> List<&2, Cap>

def pkey source · line 117 · raw

@p:Part -> String

def pin source · line 122 · raw

@p:Part -> String

def nkeys source · line 127 · raw

@xs:List<&2, Node> -> List<&2, String>

def ckeys source · line 134 · raw

@xs:List<&2, Container> -> List<&2, String>

def pkeys source · line 141 · raw

@xs:List<&2, Part> -> List<&2, String>

def keys source · line 149 · raw

@+s:System -> List<&2, String>

Keys links may name: containers and parts.

def is_server source · line 153 · raw

@r:NodeRole -> Bool

---- predicates on the vocabulary ----

def is_device source · line 160 · raw

@r:NodeRole -> Bool

def is_client source · line 167 · raw

@k:ContainerKind -> Bool

def is_data_api source · line 174 · raw

@k:ContainerKind -> Bool

def is_ours source · line 181 · raw

@o:Owner -> Bool

def is_local source · line 188 · raw

@e:Exposure -> Bool

def is_tailnet source · line 195 · raw

@e:Exposure -> Bool

def is_rust source · line 202 · raw

@l:Lang -> Bool

def str_eq source · line 210 · raw

@a:String -> @b:String -> Bool

---- keys, like foreign keys ----

def has source · line 213 · raw

@+s:String -> @xs:List<&2, String> -> Bool

def pick_str source · line 220 · raw

@c:Bool -> @a:String -> @b:String -> String

def distinct_keys source · line 228 · raw

@xs:List<&2, String> -> Bool

No key names two things.

def all_in source · line 236 · raw

@xs:List<&2, String> -> @+ks:List<&2, String> -> Bool

Every key in xs names something in ks.

def part_ins source · line 243 · raw

@xs:List<&2, Part> -> List<&2, String>

def container_ons source · line 250 · raw

@xs:List<&2, Container> -> List<&2, String>

def link_ends source · line 257 · raw

@xs:List<&2, Link> -> List<&2, String>

def well_formed source · line 268 · raw

@+s:System -> Bool

The system is well formed: node keys and container/part keys are unique, every container is on a node, every part in a container, and every link joins two things that exist.

def part_home source · line 275 · raw

@+k:String -> @xs:List<&2, Part> -> String

---- looking things up ----

def home source · line 283 · raw

@+k:String -> @+s:System -> String

The container a key belongs to: itself, or the one its part sits in.

def none source · line 286 · raw

Container

def pick_c source · line 289 · raw

@hit:Bool -> @c:Container -> @other:Container -> Container

def container source · line 297 · raw

@+k:String -> @xs:List<&2, Container> -> Container

The container with key k (an empty one when k is unknown; well_formed rules that out).

def pick_r source · line 304 · raw

@hit:Bool -> @r:NodeRole -> @other:NodeRole -> NodeRole

def node_role source · line 311 · raw

@+k:String -> @xs:List<&2, Node> -> NodeRole

def node_of source · line 321 · raw

@+k:String -> @+s:System -> String

The node a container or part runs on, and its role.

def role_of source · line 324 · raw

@+k:String -> @+s:System -> NodeRole

def private_ok source · line 329 · raw

@c:Container -> @+ns:List<&2, Node> -> Bool

---- where it runs ---- On a server, everything is reachable only from the server itself or over the private network.

def all_private source · line 334 · raw

@xs:List<&2, Container> -> @+ns:List<&2, Node> -> Bool

def servers_private source · line 341 · raw

@+s:System -> Bool

def devices_via_network.go source · line 345 · raw

@xs:List<&2, Link> -> @+s:System -> Bool

A device reaches a server only through the private network: no link goes straight from one to the other.

def devices_via_network source · line 354 · raw

@+s:System -> Bool

def is_cap source · line 358 · raw

@want:Cap -> @c:Cap -> Bool

---- what it is: minimality, every capability provided exactly once ----

def one_if source · line 373 · raw

@b:Bool -> Nat

def count_in source · line 380 · raw

@+want:Cap -> @cs:List<&2, Cap> -> Nat

def direct source · line 387 · raw

@+want:Cap -> @xs:List<&2, Container> -> Nat

def provided source · line 395 · raw

@want:Cap -> @+s:System -> Nat

How many containers provide want. Hosting plus private access compose into private hosting.

def tailnet_data_apis.go source · line 402 · raw

@xs:List<&2, Container> -> Nat

def tailnet_data_apis source · line 412 · raw

@+s:System -> Nat

The data APIs the private network reaches: the client's data API. Local and outside ones are its sources.

def shared_hosting_ok source · line 416 · raw

@c:Container -> Bool

A data API may also host the app only while it is private.

def shared_hosting_private.go source · line 421 · raw

@xs:List<&2, Container> -> Bool

def shared_hosting_private source · line 428 · raw

@+s:System -> Bool

def backend source · line 432 · raw

@c:Container -> Bool

---- a goal: every part of our own non-client containers is Rust ----

def rust_ok source · line 437 · raw

@p:Part -> @+s:System -> Bool

def all_rust.go source · line 442 · raw

@xs:List<&2, Part> -> @+s:System -> Bool

def all_rust source · line 449 · raw

@+s:System -> Bool

def path source · line 453 · raw

@+k:String -> @+s:System -> String

---- the diagram (D2): nodes as boxes, containers inside their node, parts inside their container ----

def node_box source · line 456 · raw

@n:Node -> String

def node_boxes source · line 465 · raw

@xs:List<&2, Node> -> String

def container_box source · line 472 · raw

@c:Container -> String

def container_boxes source · line 477 · raw

@xs:List<&2, Container> -> String

def part_box source · line 484 · raw

@p:Part -> @+s:System -> String

def part_boxes source · line 489 · raw

@xs:List<&2, Part> -> @+s:System -> String

def style source · line 496 · raw

@live:Bool -> String

def edges source · line 503 · raw

@xs:List<&2, Link> -> @+s:System -> String

def d2 source · line 512 · raw

@+s:System -> String