generation.bend relies on unsafe/foreign

raw source on the hub · import 0xb6eebf6253ee268a21f3e308b12cacba/generation.bend as Generation

W3C Trace Context Level 2 propagation, with its rules proved as laws. Source: https://github.com/LucasGois1/bend-trace-context

Generation on the host's cryptographic source =============================================

The first line is the package's description on BendHub, which shows the first line of the file that a release publishes: this file.

Generated contexts on the host's cryptographic source: WebCrypto in JavaScript and the operating system's generator natively. They apply the rules of trace_context.bend: four words per trace ID candidate and two per span ID candidate, most significant first, eight candidates per identifier, no all-zero identifier, no reuse of the parent's span ID or of a received trace ID, and an immediate stop at the first source error. There is no time, counter or other fallback. TC.Context.root_with and its siblings take a caller's source instead.

The generation machine itself is pure: section 6 of LAWS.bend states its behavior over replayed tapes. This file only connects it, and the native HTTP shortcuts of native_http.bend, to the host source of entropy.bend.

Every operation here relies on entropy.bend's foreign effect, so a check of a file that imports this module reports them and answers SOME PROOFS FAIL. No law imports it: the laws state the same operations on a caller's source, which is how PROOF.bend proves them without host code.

4 imports

import Base
import ./trace_context.bend as TC
import ./native_http.bend as Adapter
import ./entropy.bend as Entropy

Definitions

def Source.host source · line 34 · raw

@state:Unit -> IO(Pair(Unit, Result<&1, &1, Pair(U32, String), U32>))

The host source as the machine reads it: each read returns one word result from Entropy.read_u32, and the state is Unit because the host keeps none.

def on_host source · line 39 · raw

@-A:Type -> @action:IO(Pair(Unit, A)) -> IO(A)

The host source has no state to hand back.

def Context.root source · line 44 · raw

IO(Result<&2, &2, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.GenerationError, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.LocalContext>)

Start a trace. The trace ID asserts random-trace-id and the root is not sampled, so it is emitted with flags 02.

def Context.child source · line 48 · raw

@parent:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Parent -> @sampling:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Sampling -> IO(Result<&2, &2, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.GenerationError, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.LocalContext>)

Continue a remote or local parent with a new operation.

def Context.restart source · line 53 · raw

@previous:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.RemoteContext -> IO(Result<&2, &2, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.GenerationError, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.LocalContext>)

Start a new trace instead of continuing a received context.

def Context.continue_or_start source · line 61 · raw

@+extraction:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Extraction -> @reception:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Reception -> @sampling:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Sampling -> @+policy:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.FailurePolicy -> IO(0xb6eebf6253ee268a21f3e308b12cacba/trace_context.FailurePolicy.result(policy, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Service))

Give a service its own operation for a received message: a child of the context that extraction keeps, the message's or the base, a root without one, or a new trace in its place at a trust boundary (TC.Context.continue_or_start_with).

def Context.send source · line 69 · raw

@+limits:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Limits -> @service:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Service -> @sampling:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Sampling -> @+policy:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.FailurePolicy -> @+carrier:List<&2, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Header> -> IO(0xb6eebf6253ee268a21f3e308b12cacba/trace_context.FailurePolicy.result(policy, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Sent))

Give one message that the service sends a new child of the service's operation, or the fallback when none can be generated (TC.Context.send_with).

def NativeHttp.continue_or_start source · line 78 · raw

@+limits:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Limits -> @headers:0xb6eebf6253ee268a21f3e308b12cacba/native_http.HeaderMap -> @base:Maybe<&2, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.BaseContext> -> @reception:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Reception -> @sampling:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Sampling -> @+policy:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.FailurePolicy -> IO(0xb6eebf6253ee268a21f3e308b12cacba/trace_context.FailurePolicy.result(policy, 0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Service))

The service's own operation for a received request, from the header map of the request, on the host's cryptographic source: native_http.bend's continue_or_start_with on Source.host. base is the context to keep when the request carries no usable traceparent.

def NativeHttp.send source · line 88 · raw

@+limits:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Limits -> @service:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Service -> @sampling:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.Sampling -> @+policy:0xb6eebf6253ee268a21f3e308b12cacba/trace_context.FailurePolicy -> @headers:0xb6eebf6253ee268a21f3e308b12cacba/native_http.HeaderMap -> IO(0xb6eebf6253ee268a21f3e308b12cacba/trace_context.FailurePolicy.result(policy, 0xb6eebf6253ee268a21f3e308b12cacba/native_http.Outbound))

Give one request that the service sends the context of a new operation, on the host's cryptographic source: native_http.bend's send_with on Source.host, which replaces the context fields of headers, the request's own header map.