arc.bend checks

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

1 import

import Base

Types

type NodeRole source · line 15 · 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 PhysicalDevice source · line 21 · raw

Data

PhysicalDevice

@key:String -> @name:String -> @platform:String -> PhysicalDevice

type Vendor source · line 24 · raw

Data

Vendor
```
@name:String -> @cloud:String -> Vendor
```

type Org source · line 27 · raw

Data

Org

@name:String -> @vendor:Vendor -> @devices:List<&2, PhysicalDevice> -> Org

type Person source · line 33 · raw

Data

The agreement between the organization and its people: who they are (identities in the org's directory domain), what each is granted per scope (actions; none means no access), and budgets. It describes the people who work on the system, not the system; the diagram may omit it.

Person

@key:String -> @identity:String -> Person

type Grant source · line 35 · raw

Data

Grant

@person:String -> @scope:String -> @actions:List<&2, String> -> Grant

type Budget source · line 37 · raw

Data

Budget

@person:String -> @what:String -> @amount:Nat -> @unit:String -> Budget

type Agreement source · line 39 · raw

Data

Agreement

@domain:String -> @people:List<&2, Person> -> @grants:List<&2, Grant> -> @budgets:List<&2, Budget> -> Agreement

type Host source · line 41 · raw

Data

Owned
```
@device:String -> Host
```
Cloud
```
@provider:String -> Host
```
Other
```
Host
```

type Node source · line 46 · raw

Data

Node

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

type ContainerKind source · line 56 · 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. The private overlay is a node, not a container. DataApi: answers queries on records and changes them. Harness: an agent harness, the loop around a model (tools, context, threads), driven over its remote-control API. Proxy: forwards connections to another container, adding what it lacks, such as TLS or authentication. ModelApi: answers model calls. Cli: a command a person runs. 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
```
DataApi
```
ContainerKind
```
Harness
```
ContainerKind
```
Proxy
```
ContainerKind
```
ModelApi
```
ContainerKind
```
Cli
```
ContainerKind
```
Worker
```
ContainerKind
```

type Owner source · line 66 · raw

Data

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

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

type Exposure source · line 71 · raw

Data

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

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

type Cap source · line 81 · 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). Observability is receiving a running container's errors, traces and structured logs.

Hosting
```
Cap
```
PrivateHosting
```
Cap
```
Realtime
```
Cap
```
BlobStore
```
Cap
```
Observability
```
Cap
```

type Lang source · line 88 · raw

Data

Bend
```
Lang
```
C
```
Lang
```
Rust
```
Lang
```
TypeScript
```
Lang
```
JavaScript
```
Lang
```
Python
```
Lang
```
Opaque
```
Lang
```

type Container source · line 97 · raw

Data

Container

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

type Part source · line 100 · raw

Data

Part

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

type Link source · line 104 · 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 107 · raw

Data

System

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

Definitions

def org source · line 111 · raw

@s:System -> Org

---- access ----

def nodes source · line 116 · raw

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

def containers source · line 121 · raw

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

def parts source · line 126 · raw

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

def links source · line 131 · raw

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

def nkey source · line 136 · raw

@n:Node -> String

def ckey source · line 141 · raw

@c:Container -> String

def con source · line 146 · raw

@c:Container -> String

def caps source · line 151 · raw

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

def pkey source · line 156 · raw

@p:Part -> String

def pin source · line 161 · raw

@p:Part -> String

def pon source · line 166 · raw

@p:Part -> String

def nkeys source · line 171 · raw

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

def ckeys source · line 178 · raw

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

def pkeys source · line 185 · raw

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

def keys source · line 193 · raw

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

Keys links may name: containers and parts.

def is_server source · line 197 · raw

@r:NodeRole -> Bool

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

def is_outside source · line 204 · raw

@r:NodeRole -> Bool

def is_device source · line 211 · raw

@r:NodeRole -> Bool

def is_overlay source · line 218 · raw

@r:NodeRole -> Bool

def one_if source · line 225 · raw

@b:Bool -> Nat

def overlay_nodes.go source · line 232 · raw

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

def overlay_nodes source · line 242 · raw

@+s:System -> Nat

Private access is represented by exactly one Overlay node.

def is_client source · line 245 · raw

@k:ContainerKind -> Bool

def is_data_api source · line 252 · raw

@k:ContainerKind -> Bool

def is_ours source · line 259 · raw

@o:Owner -> Bool

def is_local source · line 266 · raw

@e:Exposure -> Bool

def is_tailnet source · line 273 · raw

@e:Exposure -> Bool

def is_rust source · line 280 · raw

@l:Lang -> Bool

def str_eq source · line 288 · raw

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

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

def has source · line 291 · raw

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

def owned_device source · line 298 · raw

@+key:String -> @+name:String -> @xs:List<&2, PhysicalDevice> -> Bool

def host_in_inventory source · line 305 · raw

@h:Host -> @name:String -> @o:Org -> Bool

def node_owned source · line 314 · raw

@n:Node -> @+o:Org -> Bool

def owned_nodes.go source · line 319 · raw

@xs:List<&2, Node> -> @+o:Org -> Bool

def owned_nodes source · line 327 · raw

@+s:System -> Bool

Every server and user device is in the owner's inventory or on its vendor's cloud.

def pick_str source · line 330 · raw

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

def distinct_keys source · line 338 · raw

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

No key names two things.

def all_in source · line 346 · raw

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

Every key in xs names something in ks.

def part_ins source · line 353 · raw

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

def part_ons source · line 360 · raw

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

def container_ons source · line 367 · raw

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

def link_ends source · line 374 · raw

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

def well_formed source · line 385 · 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 393 · raw

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

---- looking things up ----

def home source · line 401 · raw

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

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

def none source · line 404 · raw

Container

def pick_c source · line 407 · raw

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

def container source · line 415 · 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 422 · raw

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

def node_role source · line 429 · raw

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

def part_node source · line 438 · raw

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

def node_of source · line 446 · raw

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

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

def role_of source · line 449 · raw

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

def container_exposure source · line 452 · raw

@c:Container -> Exposure

def exposure_of source · line 457 · raw

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

def private_ok source · line 462 · 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 overlay.

def all_private source · line 467 · raw

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

def servers_private source · line 474 · raw

@+s:System -> Bool

def devices_via_network.go source · line 478 · raw

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

A device reaches a server over the overlay only when the destination is exposed to the tailnet.

def devices_via_network source · line 488 · raw

@+s:System -> Bool

def device_reaches source · line 492 · raw

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

A server container needs overlay exposure exactly when a device-origin link reaches it.

def exposure_for_reach source · line 499 · raw

@c:Container -> @reached:Bool -> Bool

def exposure_follows_reach.go source · line 504 · raw

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

def exposure_follows_reach source · line 513 · raw

@+s:System -> Bool

def is_cap source · line 517 · raw

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

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

def count_in source · line 532 · raw

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

def direct source · line 539 · raw

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

def tailnet_hosting.go source · line 546 · raw

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

def tailnet_hosting source · line 556 · raw

@+s:System -> Nat

How many containers host the app at Tailnet exposure.

def provided source · line 560 · raw

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

How many containers provide want. One tailnet host plus one overlay composes private hosting.

def cons_if source · line 568 · raw

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

---- observability: everything we run reports to the observability provider ----

def providers source · line 576 · raw

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

Keys of the containers that provide want.

def part_container source · line 584 · raw

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

The container a link end belongs to: a part's container, else the key itself.

def reports_to source · line 592 · raw

@ls:List<&2, Link> -> @+k:String -> @+ps:List<&2, Part> -> @+obs:List<&2, String> -> Bool

Some link from container k (or one of its parts) reaches one of obs.

def observed.go source · line 599 · raw

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

def observed source · line 609 · raw

@+s:System -> Bool

Every container we build (ours, with source) links to a container providing Observability.

def tailnet_data_apis.go source · line 612 · raw

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

def tailnet_data_apis source · line 622 · raw

@+s:System -> Nat

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

def own_data_apis.go source · line 625 · raw

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

def own_data_apis source · line 635 · raw

@+s:System -> Nat

The system's own data APIs: those not on someone else's servers. "Exactly one" means one store.

def shared_hosting_ok source · line 639 · raw

@c:Container -> Bool

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

def shared_hosting_private.go source · line 644 · raw

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

def shared_hosting_private source · line 651 · raw

@+s:System -> Bool

def backend source · line 655 · raw

@c:Container -> Bool

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

def rust_ok source · line 660 · raw

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

def all_rust.go source · line 665 · raw

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

def all_rust source · line 672 · raw

@+s:System -> Bool

def container_ours source · line 676 · raw

@c:Container -> Bool

Every modeled part belongs to a container we build; someone else's program is a black box.

def parts_ours.go source · line 681 · raw

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

def parts_ours source · line 688 · raw

@+s:System -> Bool

def path source · line 692 · 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 695 · raw

@n:Node -> String

def node_boxes source · line 704 · raw

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

def stack_label source · line 711 · raw

@frameworks:List<&2, String> -> @libraries:List<&2, String> -> String

def container_box source · line 726 · raw

@c:Container -> String

def container_boxes source · line 731 · raw

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

def part_box source · line 738 · raw

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

def part_boxes source · line 743 · raw

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

def style source · line 750 · raw

@live:Bool -> String

def edges source · line 757 · raw

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

def d2 source · line 766 · raw

@+s:System -> String

def ends_with_at source · line 778 · raw

@+identity:String -> @+domain:String -> Bool

---- the agreement: people, their identities and grants ----

def people_in.go source · line 781 · raw

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

def people_in_domain source · line 789 · raw

@a:Agreement -> Bool

Every person's identity is in the organization's directory domain.

def is_identity source · line 794 · raw

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

def identities_known.go source · line 801 · raw

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

def identities_known source · line 809 · raw

@ids:List<&2, String> -> @a:Agreement -> Bool

Every identity actually in use (from a snapshot) is one of the agreement's people.

def pick_list source · line 814 · raw

@c:Bool -> @a:List<&2, String> -> @b:List<&2, String> -> List<&2, String>

def granted.go source · line 821 · raw

@xs:List<&2, Grant> -> @+person:String -> @+scope:String -> List<&2, String>

def granted source · line 829 · raw

@a:Agreement -> @+person:String -> @+scope:String -> List<&2, String>

What person is granted on scope; [] when nothing is granted there.