admission.bend relies on unsafe/foreign

raw source on the hub · import bend-kit-http@0.32.0.0/admission.bend as Admission

Private bounded transport accounting. Replies contain copied data, never resources.

2 imports

import Base
import bend-kit-resources@0.1.0.0/resources.bend as Res

Types

type Counts source · line 5 · raw

Data

Counts

@connections:U32 -> @active:U32 -> @buffered:U32 -> @connection_high:U32 -> @active_high:U32 -> @buffered_high:U32 -> @connection_rejected:Nat -> @active_rejected:Nat -> @buffered_rejected:Nat -> Counts

type Caps source · line 10 · raw

Data

Caps

@connections:U32 -> @active:U32 -> @buffered:U32 -> Caps

type Command source · line 13 · raw

Data

Acquire

@kind:U32 -> @reply:Chan(Bool) -> Command

Release

@kind:U32 -> @reply:Chan(Unit) -> Command

Snapshot
```
@reply:Chan(Counts) -> Command
```
Quiesce
```
@reply:Chan(Bool) -> Command
```
Running
```
@reply:Chan(Bool) -> Command
```
Stop
```
Command
```

type Lease source · line 22 · raw

Type

One transport resource: its pool, and every lease taken from it joined in one grant.

Lease

@pool:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Pool -> @held:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Grant -> Lease

type Marks source · line 25 · raw

Data

Marks

@connection_high:U32 -> @active_high:U32 -> @buffered_high:U32 -> @connection_rejected:Nat -> @active_rejected:Nat -> @buffered_rejected:Nat -> Marks

type Ledger source · line 29 · raw

Type

Ledger

@connections:Lease -> @active:Lease -> @buffered:Lease -> @marks:Marks -> Ledger

type Booked source · line 33 · raw

Type

Broken means a lease count is wrong, such as a give with no matching take.

Booked

@ledger:Ledger -> @admitted:Bool -> Booked

Broken
```
Booked
```

type Taken source · line 37 · raw

Type

Admitted
```
@lease:Lease -> Taken
```
Full
```
@lease:Lease -> Taken
```
Lost
```
Taken
```

type Step source · line 195 · raw

Type

Waiting
```
@ledger:Ledger -> Step
```

Received

@ledger:Ledger -> @command:Maybe<&1, Command> -> Step

Acquired

@reply:Chan(Bool) -> @booked:Booked -> Step

Released

@reply:Chan(Unit) -> @booked:Booked -> Step

Counted

@reply:Chan(Counts) -> @counted:Pair(Counts, Ledger) -> Step

Finishing
```
@checked:Pair(Bool, Ledger) -> Step
```

Definitions

def lease.open source · line 42 · raw

@+owner:Nat -> @capacity:U32 -> Lease

def ledger.open source · line 45 · raw

@caps:Caps -> Ledger

def lease.joined source · line 49 · raw

@combined:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Combine -> @pool:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Pool -> Taken

def lease.took source · line 56 · raw

@reserved:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Reserve -> @held:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Grant -> Taken

def lease.take source · line 63 · raw

@lease:Lease -> Taken

def lease.released source · line 67 · raw

@released:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Release -> @rest:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Grant -> Maybe<&1, Lease>

def lease.split source · line 74 · raw

@parts:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Split -> @pool:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Pool -> Maybe<&1, Lease>

def lease.give source · line 81 · raw

@lease:Lease -> Maybe<&1, Lease>

def count source · line 85 · raw

@+pool:0x8ef64648a1ae4481382be5e5ce2a9fc8/resources.Pool -> U32

def counts source · line 88 · raw

@ledger:Ledger -> Pair(Counts, Ledger)

def final source · line 93 · raw

@ledger:Ledger -> Counts

def marked source · line 97 · raw

@ledger:Ledger -> Ledger

Raises each high-water mark to its current count.

def refused source · line 103 · raw

@kind:U32 -> @marks:Marks -> Marks

def acquire.rollback source · line 113 · raw

@connections:Maybe<&1, Lease> -> @active:Lease -> @buffered:Lease -> @marks:Marks -> Booked

A refused buffer returns the connection lease it already took.

def acquire.buffered source · line 120 · raw

@taken:Taken -> @connections:Lease -> @active:Lease -> @marks:Marks -> Booked

def acquire.connection source · line 130 · raw

@taken:Taken -> @active:Lease -> @buffered:Lease -> @marks:Marks -> Booked

A connection holds one connection unit and one buffer unit, taken together.

def acquire.active source · line 139 · raw

@taken:Taken -> @connections:Lease -> @buffered:Lease -> @marks:Marks -> Booked

def acquire source · line 148 · raw

@kind:U32 -> @ledger:Ledger -> Booked

def acquire.running source · line 157 · raw

@running:Bool -> @kind:U32 -> @ledger:Ledger -> Booked

def release.connection source · line 164 · raw

@connections:Maybe<&1, Lease> -> @buffered:Maybe<&1, Lease> -> @active:Lease -> @marks:Marks -> Booked

def release.active source · line 171 · raw

@active:Maybe<&1, Lease> -> @connections:Lease -> @buffered:Lease -> @marks:Marks -> Booked

def release source · line 178 · raw

@kind:U32 -> @ledger:Ledger -> Booked

def stopped source · line 187 · raw

@closing:Bool -> @counts:Counts -> Bool

def idle source · line 191 · raw

@closing:Bool -> @counted:Pair(Counts, Ledger) -> Pair(Bool, Ledger)

def open source · line 264 · raw

@caps:Caps -> IO(Chan(Command))

def open.owner source · line 271 · raw

@caps:Caps -> IO(Pair(Chan(Command), Chan(Counts)))

The affine server owner joins this actual actor result after closing its listener.

def boolean.sent source · line 277 · raw

@sent:Result<&1, &1, Command, Unit> -> @+reply:Chan(Bool) -> IO(Bool)

def quiesce source · line 287 · raw

@+inbox:Chan(Command) -> IO(Bool)

False also covers copied controls used after actual controller closure.

def running source · line 293 · raw

@+inbox:Chan(Command) -> IO(Bool)

def take source · line 299 · raw

@+inbox:Chan(Command) -> @kind:U32 -> IO(Bool)

def give.sent source · line 308 · raw

@sent:Result<&1, &1, Command, Unit> -> @+reply:Chan(Unit) -> IO(Unit)

Correct owners cannot retire the actor while a lease remains counted. If an internal channel is externally closed, report the violation instead of joining an unanswered reply or pretending a retained operation drained.

def give source · line 317 · raw

@+inbox:Chan(Command) -> @kind:U32 -> IO(Unit)

def snapshot.sent source · line 323 · raw

@sent:Result<&1, &1, Command, Unit> -> @+reply:Chan(Counts) -> IO(Maybe<&2, Counts>)

def snapshot source · line 336 · raw

@+inbox:Chan(Command) -> IO(Maybe<&2, Counts>)

A successful rendezvous send was received: Stop cannot erase a queued request. After controller closure a failed send returns None without waiting on its reply.

def close source · line 344 · raw

@inbox:Chan(Command) -> IO(Unit)

Retire accounting after listener closure; quiesce is the separate admission cutover. Finite internal fixtures may finish their already-accepted protocol.

Unsafe

unsafe loop source · line 205 · raw

@+inbox:Chan(Command) -> @+running:Bool -> @+closing:Bool -> @step:Step -> IO(Counts)

The private inbox is reusable: IO.join would close it after one receive.