trace_context.bend checks
raw source on the hub · import 0x665ae73e3f32ce98f72c7cf6844cfd3f/trace_context.bend as Trace_context
bend-trace-context: the pure Trace Context core ===============================================
This file is the package's public entry for everything that performs no host effect: the strict traceparent v00 codec, validated trace and span IDs and their bytes, local and remote contexts, the machine that turns source words into IDs, validated limits, the Level 2 tracestate parser, tracestate updates and emission, outgoing contexts, the extraction of a received message's context, the injection and forwarding of a context into an outgoing message's carrier, and the operations that continue or start a service's operation for a received message and give each message it sends a child of it. generation.bend adds the host's cryptographic source on top of it, and native_http.bend the header maps of bend-kit's native HTTP package. The claims this code must satisfy are stated in LAWS.bend and proved in PROOF.bend, beside this file. The tests in tests/*.bend here and the repository's consumer in tests/consumer exercise it through the same public names.
The normative reference is W3C Trace Context Level 2, Candidate Recommendation Draft of 2024-03-28 ("W3C" below, with section numbers). The approved specification is issue #1 of the repository ("spec #1"), and issue #41 ("spec #41") adds the building blocks that an OpenTelemetry SDK composes.
Contents
Types every data type of the codec, contexts and generation, declared first Strict v00 codec Parse.*, TraceParentV00.* Identifiers and contexts TraceId, SpanId, contexts and their trace flags, children, restarts Identifiers from source words U32.to_hex, TraceId.from_words, ... Identifiers as bytes TraceId.to_bytes, TraceId.from_bytes, SpanId.to_bytes, SpanId.from_bytes Generation machine Drive.*, TraceDraw.*, SpanDraw.*, SpanPlan.*, TracePlan.*, Step.*, Draw.*, TraceId.generate_with, SpanId.generate_with, Generation.*, Context.*_with, Source.tape Error messages Error.show, ContextError.show, ... Limits Limits.new, Limits.default, accessors Tracestate keys and values, states and lookups, budgets, and the reading machine behind TraceState.parse Tracestate updates and emission TraceState.set, remove, size and truncate Outgoing contexts OutgoingContext, a local context with the state it sends, and its Emission Extraction Context.extract, TraceParent.read, incoming and base contexts, diagnostics Injection Context.inject and the Injection it writes, Context.field_names, Context.clear Forwarding Context.forward, ForwardError Continuing or starting Context.continue_or_start_with, Reception, FailurePolicy, Service, ServicePlan Sending Context.send_with, Sent, SendPlan
The public names are documented in packages/trace-context/README.md. Names in the Parse, Parsed, ParsedBytes, Flags, Drive, TraceDraw, SpanDraw, TraceStep, SpanStep, SpanPlan, TracePlan, Draw, Step, Tape, Scan, Member, Value, Budget, Utf8, Entries, StateChar, Carrier, Text, Read, Extract, Forward, Policy, Serve and Send namespaces are internal: Bend lets any module import them, but they are not a compatibility contract.
Notes for readers new to Bend -----------------------------
- type T is Data: declares a type whose values may be copied. Each indented
line is a constructor with its fields, such as Some{value}.
- A field whose type is an equation, such as
evidence: {StateKey.is_valid(text) == True{} : Bool}, stores a proof. A
value can only be built together with that proof, so the rule holds for
every value a program handles, and code that receives one never checks it
again. The checker verifies the proof when the program is compiled. The
.checked helpers turn the result of a run-time check into such a proof:
they receive the Bool and an equation stating what it is, and matching on
the Bool refines that equation to ... == True{} in the accepting case.
- Result<&2, &2, E, T> is Done{value} or Fail{error}, and Maybe<&2, T> is
Some{value} or None{}. The &2 arguments say that the values may be copied.
- A parameter may be used at most once unless it is marked +x (reusable).
-x is erased: only the checker sees it. ~f is a template: its argument
is substituted at compile time, so it names top-level definitions only.
- match may only inspect a parameter or a variable bound by a pattern, never
a computed value, and definitions may not call each other in a cycle. Many
helpers therefore receive a Bool computed by their caller and match on it:
Scan.read(comma, ...) receives Char.is_eq(char, ','), for example.
- In every recursive call, the first argument that changes must be
structurally smaller, so every function terminates. A recursion whose depth
could grow with received text is written as a tail call, which compiles to
a loop: the JavaScript backend overflows its stack after a few thousand
nested calls, and a received value may be 32 KiB long. The other
recursions are bounded: at most 32 digits, 256 characters of a key or
value, 32 entries, or the characters of a field name sought.
- do Result<...>: sequences steps that may fail: x : T <- step stops at
the first Fail, and the block ends with return v or with a last step.
3 imports
import Base import ./src/hex.bend as Hex import ./src/digits.bend as Digits
Types
type Field source · line 114 · raw
Data
The field that a ZeroId error names: the trace ID or parent ID of a traceparent value, or a supplied span ID.
TraceIdFieldField
ParentIdFieldField
SpanIdFieldField
type Error source · line 142 · raw
Data
Why the strict codec, TraceId.parse, SpanId.parse or TraceParent.read refused a text, or TraceId.from_bytes or SpanId.from_bytes a list of bytes. Offsets count Bend characters (Unicode code points) from zero at the start of the text, or cells from zero at the start of the list, and the first problem in reading order is reported. UnexpectedEnd{offset} the text ends where a character is required, or the list where a byte is InvalidHex{offset} this character is not a lowercase hex digit InvalidByte{offset} this cell is above 255, so it is not a byte ExpectedSeparator{offset} this character should be "-" TrailingInput{} characters follow a complete value, or cells follow the bytes of an ID ForbiddenVersion{} the version is ff, forbidden by W3C 3.2.2.1 UnsupportedVersion{version} a version other than 00, which the strict codec does not read (TraceParent.read reads versions 01 to fe by their known prefix) ZeroId{field} the named ID is all zero, forbidden by W3C 3.2.2.3 and 3.2.2.4 ControlCharacter{offset} this character is a control character other than a horizontal tab, which no field value may hold (RFC 9110, section 5.5); only TraceParent.read reports it, in the fields of a later version that it does not read
UnexpectedEnd@offset:Nat -> Error
InvalidHex@offset:Nat -> Error
InvalidByte@offset:Nat -> Error
ExpectedSeparator@offset:Nat -> Error
TrailingInputError
ForbiddenVersionError
UnsupportedVersion@version:String -> Error
ZeroId@field:Field -> Error
ControlCharacter@offset:Nat -> Error
type ContextError source · line 155 · raw
Data
Why creating a context from supplied IDs was refused: a child reused its parent's span ID, or a restart reused the received trace ID.
ReusedSpanIdContextError
ReusedTraceIdContextError
type Parsed source · line 162 · raw
@-n:Nat -> Data
A sequence of n digits read from the front of a text, with the text that remains after it. The length n is part of the type, so a reader of 32 digits can only produce 32.
Parsed@-n:Nat -> @digits:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.Digits(n) -> @rest:String -> Parsed<n>
type ParsedBytes source · line 167 · raw
@-n:Nat -> Data
The digits of n bytes read from the front of a list of cells, two digits per byte, with the cells that remain after them.
ParsedBytes@-n:Nat -> @digits:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.Digits(Nat.double(n)) -> @rest:List<&2, U32> -> ParsedBytes<n>
type TraceParentV00 source · line 175 · raw
Data
A strict traceparent v00 value (W3C 3.2.2): a trace ID of 32 digits and a parent ID of 16 digits, each with a proof that it is not all zero, and a flag byte of two digits. Length and alphabet are structural: a value with a wrong length or a non-hexadecimal digit cannot be built. All eight flag bits are kept, including the reserved ones, so the codec is exact.
TraceParentV00@trace_id:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<32n> -> @parent_id:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<16n> -> @flags:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.Digits(2n) -> TraceParentV00
type TraceId source · line 187 · raw
Data
A validated trace ID: 32 lowercase hexadecimal digits, not all zero (W3C
3.2.2.3). random records whether the random-trace-id flag (W3C 3.2.2.5.2)
may be emitted for it. A parsed ID makes no such assertion: only its origin
can justify one. Generation sets it, and a caller who knows the ID is random
sets it with TraceId.assert_random.
TraceId@value:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<32n> -> @random:Bool -> TraceId
type SpanId source · line 193 · raw
Data
A validated span ID: 16 lowercase hexadecimal digits, not all zero, the identifier of one operation. It is sent as the parent ID of traceparent (W3C 3.2.2.4).
SpanId@value:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<16n> -> SpanId
type Sampling source · line 199 · raw
Data
How a child operation obtains its sampled indication (W3C 3.2.2.5.1): InheritSampled{} keeps the parent's and SetSampled{sampled} sets it. The indication communicates a decision; it does not record anything.
InheritSampledSampling
SetSampled@sampled:Bool -> Sampling
type RemoteContext source · line 208 · raw
Data
A context received from another participant. It identifies the sender's operation and keeps only the known flags: sampled and random-trace-id. It is built from a received value (RemoteContext.from_traceparent) or from its parts (RemoteContext.from_ids), and has its own type, so it cannot be sent as if it were this participant's operation.
RemoteContext@trace_id:TraceId -> @span_id:SpanId -> @sampled:Bool -> RemoteContext
type LocalContext source · line 213 · raw
Data
A context that identifies an operation of this participant: the one it sends in its own headers. The Context.* operations build it.
LocalContext@trace_id:TraceId -> @span_id:SpanId -> @sampled:Bool -> LocalContext
type Parent source · line 218 · raw
Data
The context whose trace a child operation continues: a received context or one of this participant's own operations.
RemoteParent@context:RemoteContext -> Parent
LocalParent@context:LocalContext -> Parent
type GenerationError source · line 225 · raw
Data
Why generating identifiers failed. A source failure carries the source's own code and message; exhaustion names the identifier whose eight candidates were all rejected.
SourceFailure@code:U32 -> @message:String -> GenerationError
ExhaustedTraceIdGenerationError
ExhaustedSpanIdGenerationError
type TraceWords source · line 232 · raw
Data
The words read so far for the current trace ID candidate, in arrival order. Four words complete a candidate.
NoTraceWordTraceWords
OneTraceWord@first:U32 -> TraceWords
TwoTraceWords@first:U32 -> @second:U32 -> TraceWords
ThreeTraceWords@first:U32 -> @second:U32 -> @third:U32 -> TraceWords
type SpanWords source · line 240 · raw
Data
The words read so far for the current span ID candidate. Two words complete a candidate.
NoSpanWordSpanWords
OneSpanWord@first:U32 -> SpanWords
type TraceDraw source · line 256 · raw
Data
The generation machine below is shared by the IO operations and stated in
the laws. Its types and its TraceDraw, SpanDraw, TraceStep, SpanStep,
SpanPlan, TracePlan, Draw, Step and Drive functions are internal: callers use
TraceId.generate_with, SpanId.generate_with and the Context.*_with
operations, or generation.bend, and a host that feeds words itself uses
Generation.
A trace ID draw that waits for a word: remaining counts the further
candidates allowed after the current one, so each draw gets eight
candidates in all, words holds the words of the current candidate, and
excluded is the trace ID that no candidate may repeat, such as the
received one that a restart replaces.
TraceDraw@remaining:Nat -> @words:TraceWords -> @excluded:Maybe<&2, TraceId> -> TraceDraw
type SpanDraw source · line 261 · raw
Data
A span ID draw that waits for a word, as TraceDraw: excluded is the span
ID that no candidate may repeat, such as a child's parent's.
SpanDraw@remaining:Nat -> @words:SpanWords -> @excluded:Maybe<&2, SpanId> -> SpanDraw
type TraceStep source · line 267 · raw
Data
A trace ID draw after each source word, whether it generates a trace ID alone or the trace ID of a root or a restart: it waits for another word, it drew a trace ID, or it failed.
NeedTraceWord@draw:TraceDraw -> TraceStep
DrawnTraceId@id:TraceId -> TraceStep
TraceFailed@error:GenerationError -> TraceStep
type SpanStep source · line 274 · raw
Data
A span ID draw after each source word, whether it generates a span ID alone or the span ID of a root, a child or a restart, as TraceStep.
NeedSpanWord@draw:SpanDraw -> SpanStep
DrawnSpanId@id:SpanId -> SpanStep
SpanFailed@error:GenerationError -> SpanStep
type SpanPlan source · line 283 · raw
Data
What a new local context needs besides its span ID: the span ID that it must
not repeat (excluded), such as a child's parent's, the trace ID that it
belongs to, and its sampled indication. SpanPlan.root and SpanPlan.child
give the plans of a root and a child.
SpanPlan@excluded:Maybe<&2, SpanId> -> @trace_id:TraceId -> @sampled:Bool -> SpanPlan
type TracePlan source · line 294 · raw
Data
What a new trace needs, a root or a restart: the trace ID that its trace
ID must not repeat (excluded), none for a root and the received one for
a restart, and the sampled indication of the context that it creates.
TracePlan.root and TracePlan.restart give the plans of a root and a
restart; the generation machine (TracePlan.draw), the generation that a
host feeds (Generation.new_trace) and the composition on a caller's source
(TracePlan.generate_with) each run one plan, so a root and a restart
differ only in it.
TracePlan@excluded:Maybe<&2, TraceId> -> @sampled:Bool -> TracePlan
type Draw source · line 301 · raw
Data
A generation in progress: the trace ID draw of a root or a restart, with the sampled indication of the context that it starts, or a span ID draw, with the trace ID and the sampled indication of the context that its span ID completes.
DrawTrace@draw:TraceDraw -> @sampled:Bool -> Draw
DrawSpan@draw:SpanDraw -> @trace_id:TraceId -> @sampled:Bool -> Draw
type Step source · line 307 · raw
Data
The state of a generation after each source word: it needs another word, it created a context, or it failed.
NeedWord@draw:Draw -> Step
Created@context:LocalContext -> Step
Failed@error:GenerationError -> Step
type Generation source · line 322 · raw
Data
A generation with its word budget, for a host that feeds it one word at a
time instead of passing a source as a template, such as JavaScript code
calling this module: the words it may still read (fuel) and the
machine's step. Its fields are internal, like Step: Generation.root and
its siblings build one. Context.continue_or_start_with and
Context.send_with drive the same values, and a host that feeds words while
Generation.needs says so gets the pure driver's result (law
generation_drive). Context.root_with and its siblings compose the
separate generation, whose results laws root_tape and its siblings give as
that driver's.
Generation@fuel:Nat -> @step:Step -> Generation
type LimitsError source · line 1621 · raw
Data
Why a limit configuration was refused. The first failing rule is reported: TraceParentInputTooSmall{} the traceparent input budget is below 55 TraceStateOutputTooSmall{} the tracestate output budget is below 512 TraceStateInputTooSmall{} the tracestate input budget is below the output budget
TraceParentInputTooSmallLimitsError
TraceStateOutputTooSmallLimitsError
TraceStateInputTooSmallLimitsError
type Limits source · line 1639 · raw
Data
Budgets in UTF-8 octets. The input budgets bound a received traceparent value
and a combined tracestate value; the output budget is the most an emitted
tracestate may take. evidence is the proof of Limits.is_valid, so every
Limits value follows the rules.
Limits@traceparent_input:Nat -> @tracestate_input:Nat -> @tracestate_output:Nat -> @evidence:{Limits.is_valid(traceparent_input, tracestate_input, tracestate_output) == True{} : Bool} -> Limits
type EntryError source · line 1716 · raw
Data
Why a tracestate key, value or received member was refused: MissingEquals{} a nonempty member has no "=" InvalidKey{} the text before the first "=" is not a key InvalidValue{} the text after it, without trailing optional whitespace, is not a value
MissingEqualsEntryError
InvalidKeyEntryError
InvalidValueEntryError
type StateKey source · line 1802 · raw
Data
A tracestate key, naming the vendor that owns an entry. evidence proves the
Level 2 key grammar for text, so a StateKey is always valid: build one with
StateKey.parse (the negative fixture tests/reject/invalid_state_key.bend
shows that direct construction with a wrong text does not compile).
StateKey@text:String -> @evidence:{StateKey.is_valid(text) == True{} : Bool} -> StateKey
type StateValue source · line 1807 · raw
Data
A tracestate value, opaque to every other vendor. evidence proves the
Level 2 value grammar for text. Leading spaces are part of the value.
StateValue@text:String -> @evidence:{StateValue.is_valid(text) == True{} : Bool} -> StateValue
type StateError source · line 1874 · raw
Data
Why a received tracestate value was discarded:
StateTooLarge{} the combined value exceeds its input budget
TooManyMembers{} a 33rd nonempty member was reached
InvalidEntry{member, error} a member is invalid; member numbers the
comma-separated members of the combined value
from zero, empty members included
Discarding the state never invalidates a valid traceparent (spec #1).
StateTooLargeStateError
TooManyMembersStateError
InvalidEntry@member:Nat -> @error:EntryError -> StateError
type StateEntry source · line 1880 · raw
Data
One vendor's entry: a key and its value.
StateEntry@key:StateKey -> @value:StateValue -> StateEntry
type TraceState source · line 1930 · raw
Data
Ordered vendor state: at most 32 entries with distinct keys, leftmost first.
evidence proves both properties, so every TraceState has them (law
state_valid).
TraceState@entries:List<&2, StateEntry> -> @evidence:{TraceState.is_valid(entries) == True{} : Bool} -> TraceState
type Member source · line 2072 · raw
Data
Where reading the current member stands: before its key, with only optional whitespace so far; inside its key; or inside its value. Characters read are kept most recent first, so each one costs a single step.
BlankMember
InKey@text:String -> Member
InValue@key:String -> @text:String -> Member
type Scan source · line 2081 · raw
Data
A tracestate being read: the members ended so far, empty ones included; how many more nonempty members are allowed; the current member; and the first entry of each key, in reading order. Stopped holds the first problem found. The scan and its helpers are internal.
Scanning@member:Nat -> @room:Nat -> @current:Member -> @entries:List<&2, StateEntry> -> Scan
Stopped@error:StateError -> Scan
type Truncation source · line 2412 · raw
Data
What truncation to the output budget kept, and the keys of the entries it dropped, in their original order. Reporting the keys, not the values, tells which vendors lost their state without repeating opaque data.
Truncation@kept:TraceState -> @dropped:List<&2, StateKey> -> Truncation
type OutgoingContext source · line 2513 · raw
Data
A local context and the state sent with it.
OutgoingContext@context:LocalContext -> @state:TraceState -> OutgoingContext
type Emission source · line 2520 · raw
Data
The two header values an outgoing context emits, and the keys of the entries that truncation to the output budget dropped, in their original order. A context with no state emits the tracestate "", which Context.inject does not write.
Emission@traceparent:String -> @tracestate:String -> @dropped:List<&2, StateKey> -> Emission
type Header source · line 2617 · raw
Data
One field of a message: its name and its value. A carrier is the list of a message's fields in their order; repeated fields stay separate, as the message carried them. A host that joins repeated fields into one value with commas (RFC 9110, section 5.3) gives one field with that value.
Header@name:String -> @value:String -> Header
type TraceParentError source · line 2629 · raw
Data
Why extraction refused a message's traceparent:
RepeatedTraceParent{} the message has more than one traceparent field,
or a value that joins several with a comma
TraceParentTooLarge{} the value exceeds the traceparent input budget
InvalidTraceParent{error} the value breaks the rules of its version;
error is the first problem, as the codec
reports it, with offsets counted from the
first character after optional whitespace
The received value itself is never included.
RepeatedTraceParentTraceParentError
TraceParentTooLargeTraceParentError
InvalidTraceParent@error:Error -> TraceParentError
type ReceivedPair source · line 2642 · raw
Data
The original fields of an accepted message: its traceparent value, without the optional whitespace around it, and its tracestate field values as they came, in arrival order, none when it had no tracestate field. They are what Context.forward sends. The input budgets bound the pairs that extraction keeps (law received_bounds); a pair built directly with this constructor carries no such guarantee, so forwarding checks what it sends. A pair that extraction kept is refused only when it exceeds the output budget (law forward_extracted).
ReceivedPair@traceparent:String -> @tracestate:List<&2, String> -> ReceivedPair
type IncomingContext source · line 2652 · raw
Data
The sender's operation together with the tracestate that goes with it: one extracted from a message, which also keeps the received pair when the whole pair was accepted, or one built from its parts (IncomingContext.from_remote), which keeps none. It is not this participant's operation: a service continues it with a child (Context.child_from_id with IncomingContext.parent), or forwards the received pair unchanged (Context.forward).
IncomingContext@context:RemoteContext -> @state:TraceState -> @received:Maybe<&2, ReceivedPair> -> IncomingContext
type BaseContext source · line 2658 · raw
Data
The context to continue from that extraction keeps when a message carries no usable traceparent: a context received earlier, or an operation of this participant with the state it sends.
IncomingBase@incoming:IncomingContext -> BaseContext
OutgoingBase@outgoing:OutgoingContext -> BaseContext
type TraceParentOutcome source · line 2664 · raw
Data
What extraction found in the traceparent fields of a message: an accepted value, no field, or a refusal with its reason.
TraceParentAcceptedTraceParentOutcome
TraceParentAbsentTraceParentOutcome
TraceParentRejected@error:TraceParentError -> TraceParentOutcome
type StateOutcome source · line 2678 · raw
Data
What extraction did with the tracestate fields of a message: StateAbsent{} there was no tracestate field StateAccepted{} the fields were read into the incoming state, which may be empty StateDiscarded{error} the fields were refused as a whole; the incoming context has no state and the traceparent stays accepted StateIgnored{} the fields were not read, because the message has no accepted traceparent (W3C 3.3)
StateAbsentStateOutcome
StateAcceptedStateOutcome
StateDiscarded@error:StateError -> StateOutcome
StateIgnoredStateOutcome
type Extraction source · line 2687 · raw
Data
The result of extracting a message: the context to continue from, if any,
and what happened to each field. context is the incoming context of the
message when its traceparent was accepted, and the base otherwise.
Extraction@context:Maybe<&2, BaseContext> -> @parent:TraceParentOutcome -> @state:StateOutcome -> Extraction
type Injection source · line 3212 · raw
Data
The carrier an injection writes, and the keys of the entries that truncation to the output budget dropped from the state, in their original order: diagnostics, kept apart from the carrier.
Injection@carrier:List<&2, Header> -> @dropped:List<&2, StateKey> -> Injection
type ForwardError source · line 3324 · raw
Data
Why a received context could not be forwarded unchanged: NothingToForward{} it keeps no received pair: its tracestate was discarded when it was extracted, or it was built from parts (IncomingContext.from_remote) ForwardTooLarge{} its tracestate fields, joined by commas, exceed the tracestate output budget InvalidForwardParent{error} its traceparent value is not one that TraceParent.read accepts InvalidForwardState{error} its tracestate fields are not ones that TraceState.parse_fields accepts A pair that extraction keeps always passes the last two checks (law forward_extracted); they refuse a pair built directly.
NothingToForwardForwardError
ForwardTooLargeForwardError
InvalidForwardParent@error:TraceParentError -> ForwardError
InvalidForwardState@error:StateError -> ForwardError
type Reception source · line 3443 · raw
Data
How a service takes the context that extraction keeps, the message's or the base: Continue{} continue it with a child Restart{} replace it with a new trace, as at a trust boundary: its trace ID is not reused, its state is discarded and the root defaults apply
ContinueReception
RestartReception
type FailurePolicy source · line 3451 · raw
Data
What the operations do when generating an identifier fails: Lenient{} carry on without a new operation; the result says why Strict{} fail with the GenerationError, so that the caller can refuse the operation
LenientFailurePolicy
StrictFailurePolicy
type Origin source · line 3459 · raw
Data
How a service's operation came about: Continued{} a child of the context that extraction kept Started{} a root: extraction kept no context Restarted{} a new trace in place of the kept context (Restart{})
ContinuedOrigin
StartedOrigin
RestartedOrigin
type Service source · line 3469 · raw
Data
The service's own operation for a received message, with the state it
sends, or the error that left it without one. received is the message's
incoming context when the service continues it, kept so that a message it
sends can forward the received pair if generating fails; it is None{} for
a root, a restart or a continued base.
Operating@origin:Origin -> @outgoing:OutgoingContext -> @received:Maybe<&2, IncomingContext> -> Service
Untraced@error:GenerationError -> @received:Maybe<&2, IncomingContext> -> Service
type ServicePlan source · line 3540 · raw
Data
The service's operation as Context.continue_or_start_with decides it for
a received message, before it reads any word: the generation to drive and
what the generation's result makes of the service.
ContinuePlan{generation, state, received} a child of the kept context,
sending its state
StartPlan{generation, origin} a root or a restart, whose
generation has the sampled
indication of
Serve.new_trace_sampled
A host that feeds a generation one word at a time, such as JavaScript code
calling this module, drives ServicePlan.generation and hands the result to
ServicePlan.service (law hosted_service).
ContinuePlan@generation:Generation -> @state:TraceState -> @received:Maybe<&2, IncomingContext> -> ServicePlan
StartPlan@generation:Generation -> @origin:Origin -> ServicePlan
type Unforwarded source · line 3651 · raw
Data
Why a message without a new operation does not forward a received pair:
NothingKept{} the service keeps no received context: its
operation is, or was to be, a root, a restart or
a child of a base
ForwardFailed{error} Context.forward refused the received context with
error
NothingKeptUnforwarded
ForwardFailed@error:ForwardError -> Unforwarded
type Sent source · line 3663 · raw
Data
The context fields of one message and how they came about:
Fresh{operation, injection} a new operation, injected with the
service's state
Forwarded{carrier, error} no operation could be generated (error);
the received pair is forwarded unchanged
NoContext{carrier, error, no operation could be generated, and no
reason} pair was forwarded (reason): the context
fields are cleared
Fresh@operation:LocalContext -> @injection:Injection -> Sent
Forwarded@carrier:List<&2, Header> -> @error:GenerationError -> Sent
NoContext@carrier:List<&2, Header> -> @error:GenerationError -> @reason:Unforwarded -> Sent
type SendPlan source · line 3708 · raw
Data
A message's operation as Context.send_with decides it before it reads any word, with the limits and the carrier to send it with: SendChild{generation, limits, outgoing, received, carrier} a child of the service's operation, injected with the service's state SendFallback{error, limits, received, carrier} no operation, for a service without one: the fallback, reading no word A host that feeds a generation one word at a time drives SendPlan.generation and hands the result to SendPlan.sent (law hosted_send).
SendChild@generation:Generation -> @limits:Limits -> @outgoing:OutgoingContext -> @received:Maybe<&2, IncomingContext> -> @carrier:List<&2, Header> -> SendPlan
SendFallback@error:GenerationError -> @limits:Limits -> @received:Maybe<&2, IncomingContext> -> @carrier:List<&2, Header> -> SendPlan
Definitions
def Parsed.prepend source · line 334 · raw
@-n:Nat -> @digit:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/hex.Digit -> @parsed:Parsed<n> -> Parsed<1n+n>
Put one more digit in front of a parsed sequence: n digits become 1 + n.
def Parse.digit_result source · line 341 · raw
@value:Maybe<&2, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/hex.Digit> -> @offset:Nat -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/hex.Digit>
A decoded character, or InvalidHex at its offset when it is not a lowercase hexadecimal digit.
def Parse.digit source · line 350 · raw
@char:Char -> @offset:Nat -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/hex.Digit>
Decode one character as a lowercase hexadecimal digit.
def Parse.digits source · line 356 · raw
@n:Nat -> @text:String -> @offset:Nat -> Result<&2, &2, Error, Parsed<n>>
Consume exactly n characters as digits, keeping the unconsumed rest of the text. The recursion decreases n, so no length check or unchecked conversion is needed: the result's type already has length n.
def Parse.separator_result source · line 373 · raw
@tail:String -> @ok:Bool -> @offset:Nat -> Result<&2, &2, Error, String>
The rest of the text after a "-", or ExpectedSeparator at its offset.
def Parse.separator source · line 382 · raw
@text:String -> @offset:Nat -> Result<&2, &2, Error, String>
Read the "-" expected at offset.
def Parse.end source · line 391 · raw
@text:String -> Result<&2, &2, Error, Unit>
The value must end here. Only the first character after it is inspected, so an arbitrarily long suffix is refused without being read.
def Parse.version source · line 400 · raw
@digits:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.Digits(2n) -> Result<&2, &2, Error, Unit>
The version digits: 00 is the only version the strict codec reads, ff is forbidden (W3C 3.2.2.1), and any other version is reported with its text.
def Parse.nonzero_result source · line 411 · raw
@-n:Nat -> @result:Maybe<&2, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<n>> -> @field:Field -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<n>>
Attach the proof that digits are not all zero, or fail with ZeroId naming the field.
def Parse.nonzero source · line 420 · raw
@n:Nat -> @digits:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.Digits(n) -> @field:Field -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<n>>
Check that digits are not all zero (W3C 3.2.2.3, 3.2.2.4).
def Parse.flags source · line 425 · raw
@trace_id:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<32n> -> @parent_id:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<16n> -> @parsed:Parsed<2n> -> Result<&2, &2, Error, TraceParentV00>
The last field: the two flag digits, then the end of the text.
def Parse.parent source · line 435 · raw
@trace_id:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<32n> -> @parsed:Parsed<16n> -> Result<&2, &2, Error, TraceParentV00>
After the trace ID: the parent ID, which must not be all zero, its "-" at offset 52 and the flag digits at offset 53.
def Parse.trace source · line 447 · raw
@parsed:Parsed<32n> -> Result<&2, &2, Error, TraceParentV00>
After the version: the trace ID, which must not be all zero, its "-" at offset 35 and the parent ID from offset 36.
def Parse.start source · line 458 · raw
@parsed:Parsed<2n> -> Result<&2, &2, Error, TraceParentV00>
After the two version digits: the version check, the "-" at offset 2 and the trace ID from offset 3.
def TraceParentV00.parse source · line 475 · raw
@text:String -> Result<&2, &2, Error, TraceParentV00>
Parse a strict traceparent v00 value: exactly "00-", 32 lowercase hexadecimal digits, "-", 16 digits, "-" and two digits; the IDs must not be all zero. No whitespace, case folding or suffix is accepted, and every flag byte is kept as received. This is the strict wire codec, not a complete W3C propagator: TraceParent.read and Context.extract apply the processing rules of W3C 3.2.4 and 4.1.2, such as reading later versions by their known prefix. Laws: roundtrip, inverse and formatted_length.
def TraceParentV00.format source · line 484 · raw
@context:TraceParentV00 -> String
The text of a strict v00 value: always 55 characters. It is total, because validity is carried by the argument's type, and it preserves every flag bit: it is the exact inverse of parse, not an outgoing-header policy (see LocalContext.to_traceparent for what a participant emits).
def TraceParentV00.is_sampled source · line 492 · raw
@context:TraceParentV00 -> Bool
Whether the sampled flag, bit 0 of the flag byte, is set (W3C 3.2.2.5.1).
def TraceParentV00.is_random source · line 500 · raw
@context:TraceParentV00 -> Bool
Whether the random-trace-id flag, bit 1, is set (W3C 3.2.2.5.2). It records the sender's assertion; it does not prove how the trace ID was generated.
def Parse.id.finish source · line 517 · raw
@n:Nat -> @parsed:Parsed<n> -> @field:Field -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<n>>
The digits of a supplied ID must be the whole text, and not all zero.
def Parse.id source · line 526 · raw
@+n:Nat -> @text:String -> @field:Field -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<n>>
A supplied ID is exactly n lowercase hexadecimal digits, not all zero.
def TraceId.parse source · line 535 · raw
@text:String -> Result<&2, &2, Error, TraceId>
Parse a supplied trace ID: exactly 32 lowercase hexadecimal digits, not all zero. Error offsets count from the start of the ID. The result makes no randomness assertion (laws trace_id_parse and trace_id_accepts).
def TraceId.assert_random source · line 543 · raw
@id:TraceId -> TraceId
Record the caller's assertion that these digits were generated randomly, so that the random-trace-id flag is emitted with them. The caller is responsible for the assertion; validation cannot establish it (law assert_random).
def TraceId.is_random source · line 549 · raw
@id:TraceId -> Bool
Whether the trace ID asserts that it was generated randomly.
def TraceId.to_string source · line 555 · raw
@id:TraceId -> String
The 32 lowercase hexadecimal digits of the trace ID.
def TraceId.is_eq source · line 562 · raw
@a:TraceId -> @b:TraceId -> Bool
Whether two trace IDs name the same trace. The randomness assertion is not part of the identifier, so it is ignored.
def SpanId.parse source · line 567 · raw
@text:String -> Result<&2, &2, Error, SpanId>
Parse a supplied span ID: exactly 16 lowercase hexadecimal digits, not all zero (laws span_id_parse and span_id_roundtrip).
def SpanId.to_string source · line 573 · raw
@id:SpanId -> String
The 16 lowercase hexadecimal digits of the span ID.
def SpanId.is_eq source · line 579 · raw
@a:SpanId -> @b:SpanId -> Bool
Whether two span IDs name the same operation.
def Sampling.resolve source · line 584 · raw
@sampling:Sampling -> @inherited:Bool -> Bool
The sampled indication a child receives: the inherited one, unless the caller set another (law sampling).
def RemoteContext.from_traceparent source · line 594 · raw
@value:TraceParentV00 -> RemoteContext
Interpret a received strict-v00 value as the sender's context. Bit 0 is sampled and bit 1 is random-trace-id; the reserved bits are not interpreted and do not travel with the context (law received_flags).
def RemoteContext.from_ids source · line 609 · raw
@trace_id:TraceId -> @span_id:SpanId -> @sampled:Bool -> RemoteContext
Build the sender's context from its parts, as an OpenTelemetry SDK does for a link or for a propagator of another format: its trace ID, its span ID and its sampled indication, kept as they are. It is total, since the IDs are valid by construction, and its random-trace-id bit is the trace ID's own assertion: none for a parsed ID, unless TraceId.assert_random adds it (law remote_from_ids). The result is still a received context, which a child continues: it cannot be sent as this participant's operation (tests/reject/remote_as_local.bend).
def RemoteContext.trace_id source · line 613 · raw
@context:RemoteContext -> TraceId
The trace the received context belongs to.
def RemoteContext.span_id source · line 619 · raw
@context:RemoteContext -> SpanId
The sender's operation: the parent ID of the received value.
def RemoteContext.is_sampled source · line 625 · raw
@context:RemoteContext -> Bool
The sender's sampled indication.
def Flags.known source · line 632 · raw
@sampled:Bool -> @random:Bool -> U32
The known trace flags as a number: sampled in bit 0 and random in bit 1
(W3C 3.2.2.5), with the six reserved bits zero.
def RemoteContext.flags source · line 641 · raw
@context:RemoteContext -> U32
The trace flags that the context keeps, as a number from 0 to 3: bit 0 is its sampled indication and bit 1 its trace ID's randomness assertion, the known flags that it was received or built with. Reserved bits are never among them. The Booleans stay the canonical form; the number is for an exporter, such as one that writes OTLP's Span.flags field. Laws: remote_flags and received_trace_flags.
def LocalContext.trace_id source · line 647 · raw
@context:LocalContext -> TraceId
The trace this participant's operation belongs to.
def LocalContext.span_id source · line 653 · raw
@context:LocalContext -> SpanId
This participant's operation.
def LocalContext.is_sampled source · line 659 · raw
@context:LocalContext -> Bool
The sampled indication this participant sends.
def LocalContext.to_traceparent source · line 667 · raw
@context:LocalContext -> TraceParentV00
The participating representation of a local context: version 00, and flags limited to sampled (bit 0) and random-trace-id (bit 1), with every reserved bit zero (W3C 3.2.2.5.3; laws emitted_traceparent and emitted_projection).
def LocalContext.flags source · line 679 · raw
@context:LocalContext -> U32
The trace flags of the context as a number from 0 to 3: bit 0 is its sampled indication and bit 1 its trace ID's randomness assertion. It is the flag byte of the traceparent that the context emits, 00 to 03, so an exporter that writes it, into OTLP's Span.flags field for example, agrees with what the context propagates. The Booleans stay the canonical form. Law: local_flags.
def Parent.trace_id source · line 685 · raw
@parent:Parent -> TraceId
The trace a child continues.
def Parent.span_id source · line 693 · raw
@parent:Parent -> SpanId
The parent's operation, which a child must not reuse.
def Parent.is_sampled source · line 701 · raw
@parent:Parent -> Bool
The sampled indication a child inherits by default.
def Context.from_ids source · line 711 · raw
@trace_id:TraceId -> @span_id:SpanId -> @sampled:Bool -> LocalContext
Represent an operation the caller owns, with supplied IDs and an explicit sampled indication. The IDs must belong to that operation: validating their format cannot establish where they came from (law from_ids).
def Context.root_from_ids source · line 720 · raw
@trace_id:TraceId -> @span_id:SpanId -> @sampled:Bool -> LocalContext
Start a trace with supplied IDs and the sampled indication that the caller
decided, kept as it is given (spec #41, "Sampling decision when starting a
trace"; law root). False gives an unsampled root, the default of spec #1,
"New roots default to sampled 0", which Context.continue_or_start_with
applies itself. generation.bend provides Context.root, Context.child and
Context.restart for generated IDs.
def Context.child_from_id.checked source · line 724 · raw
@trace_id:TraceId -> @span_id:SpanId -> @sampled:Bool -> @reused:Bool -> Result<&2, &2, ContextError, LocalContext>
The child, unless the span ID was found equal to the parent's.
def Context.child_from_id source · line 736 · raw
@+parent:Parent -> @+span_id:SpanId -> @sampling:Sampling -> Result<&2, &2, ContextError, LocalContext>
Continue the parent's trace with a new operation identified by a supplied span ID. The child keeps the trace ID and its randomness assertion, and its span ID must differ from the parent's (ReusedSpanId otherwise). Sampling is inherited unless set. Laws: child, child_reuse and child_accepts.
def Context.restart_from_ids.checked source · line 743 · raw
@trace_id:TraceId -> @span_id:SpanId -> @sampled:Bool -> @reused:Bool -> Result<&2, &2, ContextError, LocalContext>
The restarted root, unless the trace ID was found equal to the received one.
def Context.restart_from_ids source · line 756 · raw
@previous:RemoteContext -> @+trace_id:TraceId -> @span_id:SpanId -> @sampled:Bool -> Result<&2, &2, ContextError, LocalContext>
Start a new trace with supplied IDs instead of continuing a received context. The new trace ID must differ from the received one (ReusedTraceId otherwise), and the restart is the root of its IDs with the sampled indication that it is given: False applies the root defaults, sampled 0 included. Laws: restart, restart_reuse and restart_accepts.
def U32.to_hex source · line 770 · raw
@word:U32 -> String
The eight lowercase hexadecimal digits of a word, most significant first (laws hex_injective and word_hex).
def TraceId.from_digits source · line 774 · raw
@value:Maybe<&2, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<32n>> -> Maybe<&2, TraceId>
A trace ID from nonzero digits, with no randomness assertion.
def TraceId.from_words source · line 785 · raw
@first:U32 -> @second:U32 -> @third:U32 -> @fourth:U32 -> Maybe<&2, TraceId>
A trace ID from four words, read most significant first: the first word gives the first eight digits. Like a parsed ID it makes no randomness assertion; add one with TraceId.assert_random when the words are random. An all-zero candidate is None (laws trace_words and words_unasserted).
def SpanId.from_digits source · line 792 · raw
@value:Maybe<&2, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<16n>> -> Maybe<&2, SpanId>
A span ID from nonzero digits.
def SpanId.from_words source · line 801 · raw
@first:U32 -> @second:U32 -> Maybe<&2, SpanId>
A span ID from two words, most significant first. An all-zero candidate is None (law span_words).
def ParsedBytes.prepend source · line 815 · raw
@-n:Nat -> @digits:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.Digits(2n) -> @parsed:ParsedBytes<n> -> ParsedBytes<1n+n>
Put the two digits of one more byte in front of the bytes already read: n bytes become 1 + n.
def Parse.byte.checked source · line 822 · raw
@cell:U32 -> @above:Bool -> @offset:Nat -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.Digits(2n)>
The two digits of a cell, or InvalidByte at its offset when the check found the cell above 255.
def Parse.byte source · line 830 · raw
@+cell:U32 -> @offset:Nat -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.Digits(2n)>
Read one cell as a byte.
def Parse.bytes source · line 836 · raw
@n:Nat -> @bytes:List<&2, U32> -> @offset:Nat -> Result<&2, &2, Error, ParsedBytes<n>>
Consume exactly n cells as bytes, keeping the cells after them. As in Parse.digits, the recursion decreases n, so the result's type has the 2n digits of n bytes.
def Parse.bytes_end source · line 853 · raw
@bytes:List<&2, U32> -> Result<&2, &2, Error, Unit>
The list must end after the ID's bytes: a cell after them fails with TrailingInput, whatever it holds.
def Parse.id_bytes.finish source · line 861 · raw
@n:Nat -> @parsed:ParsedBytes<n> -> @field:Field -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<Nat.double(n)>>
The bytes of a supplied ID must be the whole list, and not all zero.
def Parse.id_bytes source · line 870 · raw
@+n:Nat -> @bytes:List<&2, U32> -> @field:Field -> Result<&2, &2, Error, 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.NonZero<Nat.double(n)>>
A supplied ID is exactly n bytes, not all zero.
def TraceId.to_bytes source · line 881 · raw
@id:TraceId -> List<&2, U32>
The 16 bytes of the trace ID, most significant first, in Base's byte convention, that of TCP.send_bytes and TCP.recv_bytes: one U32 cell from 0 to 255 per byte. The first byte holds the ID's first two digits, the first of them high. The randomness assertion is not part of the bytes (laws trace_bytes, trace_bytes_roundtrip and trace_bytes_injective).
def TraceId.from_bytes source · line 895 · raw
@bytes:List<&2, U32> -> Result<&2, &2, Error, TraceId>
Read a trace ID from exactly 16 bytes, most significant first. The cells are read in order: a missing cell fails with UnexpectedEnd and a cell above 255 with InvalidByte, at its offset counted in cells; a 17th cell fails with TrailingInput whatever it holds, and 16 zero bytes with ZeroId. Like a parsed ID, the result makes no randomness assertion, since bytes do not say how the ID was made; only a caller whose own generator, known to be random, made it adds one with TraceId.assert_random. Laws: trace_bytes_inverse, bytes_unasserted, trace_bytes_short, trace_bytes_long, trace_bytes_above, zero_bytes and trace_bytes_accepts.
def SpanId.to_bytes source · line 902 · raw
@id:SpanId -> List<&2, U32>
The 8 bytes of the span ID, most significant first (laws span_bytes, span_bytes_roundtrip and span_bytes_injective).
def SpanId.from_bytes source · line 911 · raw
@bytes:List<&2, U32> -> Result<&2, &2, Error, SpanId>
Read a span ID from exactly 8 bytes, most significant first, with the rules and errors of TraceId.from_bytes. Laws: span_bytes_inverse, span_bytes_short, span_bytes_long, span_bytes_above, zero_bytes and span_bytes_accepts.
def Draw.asserted source · line 936 · raw
@candidate:Maybe<&2, TraceId> -> Maybe<&2, TraceId>
Generation reads its words from a source trusted to be random, so each trace ID candidate asserts random-trace-id.
def Tape.next source · line 945 · raw
@tape:List<&1, Result<&1, &1, Pair(U32, String), U32>> -> Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, Result<&1, &1, Pair(U32, String), U32>)
A deterministic word source for tests and replay: each read takes the next result, and an empty tape fails with code 1, tape-exhausted.
def TraceDraw.start source · line 1025 · raw
@excluded:Maybe<&2, TraceId> -> TraceStep
A trace ID draw starts with its first candidate; seven further candidates may follow it, eight in all.
def TraceDraw.retry source · line 1029 · raw
@remaining:Nat -> @excluded:Maybe<&2, TraceId> -> TraceStep
Try another trace ID candidate, or fail once the eight are used.
def TraceDraw.reuse source · line 1037 · raw
@reused:Bool -> @id:TraceId -> @excluded:TraceId -> @remaining:Nat -> TraceStep
A trace ID candidate equal to the excluded one is retried.
def TraceDraw.check source · line 1046 · raw
@candidate:Maybe<&2, TraceId> -> @excluded:Maybe<&2, TraceId> -> @remaining:Nat -> TraceStep
Check a complete trace ID candidate: zero and the excluded trace ID are retried; anything else is the trace ID drawn.
def TraceDraw.take source · line 1059 · raw
@word:U32 -> @remaining:Nat -> @words:TraceWords -> @excluded:Maybe<&2, TraceId> -> TraceStep
Add a word to the current trace ID candidate. The fourth word completes it, most significant first, and the candidate is checked.
def TraceDraw.feed source · line 1073 · raw
@word:Result<&1, &1, Pair(U32, String), U32> -> @remaining:Nat -> @words:TraceWords -> @excluded:Maybe<&2, TraceId> -> TraceStep
Feed the next source word to a trace ID draw, given as its three fields. A source error ends the draw at once with SourceFailure (law trace_id_failure).
def TraceDraw.next source · line 1083 · raw
@word:Result<&1, &1, Pair(U32, String), U32> -> @draw:TraceDraw -> TraceStep
The step of a trace ID draw after its next source word, TraceDraw.feed of
its fields: the feed that Drive takes.
def TraceStep.waiting source · line 1090 · raw
@step:TraceStep -> Maybe<&2, TraceDraw>
The draw that a trace ID draw's step feeds its next word to, while it waits for one: the view of the step that Drive needs.
def TraceDraw.result source · line 1102 · raw
@step:TraceStep -> Result<&2, &2, GenerationError, TraceId>
The trace ID of a finished trace ID draw, or why it failed. A draw that has not finished would report exhaustion; law trace_id_ends shows that the word budget of TraceId.generate_with makes that case unreachable.
def TraceDraw.run source · line 1112 · raw
@fuel:Nat -> @current:Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, TraceStep) -> Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, TraceStep)
Drive a trace ID draw from a tape (Drive.run).
def TraceDraw.ended source · line 1120 · raw
@result:Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, TraceStep) -> Bool
Whether the trace ID draw in a driver's result has ended.
def TraceDraw.outcome source · line 1124 · raw
@-S:Type -> @done:Pair(S, TraceStep) -> Pair(S, Result<&2, &2, GenerationError, TraceId>)
The source's final state with the trace ID draw's result.
def SpanDraw.start source · line 1147 · raw
@excluded:Maybe<&2, SpanId> -> SpanStep
A span ID draw starts with its first candidate; seven further candidates may follow it, eight in all.
def SpanDraw.retry source · line 1151 · raw
@remaining:Nat -> @excluded:Maybe<&2, SpanId> -> SpanStep
Try another span ID candidate, or fail once the eight are used.
def SpanDraw.reuse source · line 1159 · raw
@reused:Bool -> @id:SpanId -> @excluded:SpanId -> @remaining:Nat -> SpanStep
A span ID candidate equal to the excluded one is retried.
def SpanDraw.check source · line 1168 · raw
@candidate:Maybe<&2, SpanId> -> @excluded:Maybe<&2, SpanId> -> @remaining:Nat -> SpanStep
Check a complete span ID candidate: zero and the excluded span ID are retried; anything else is the span ID drawn.
def SpanDraw.take source · line 1181 · raw
@word:U32 -> @remaining:Nat -> @words:SpanWords -> @excluded:Maybe<&2, SpanId> -> SpanStep
Add a word to the current span ID candidate. The second word completes it, most significant first, and the candidate is checked.
def SpanDraw.feed source · line 1191 · raw
@word:Result<&1, &1, Pair(U32, String), U32> -> @remaining:Nat -> @words:SpanWords -> @excluded:Maybe<&2, SpanId> -> SpanStep
Feed the next source word to a span ID draw, given as its three fields. A source error ends the draw at once with SourceFailure (law span_id_failure).
def SpanDraw.next source · line 1201 · raw
@word:Result<&1, &1, Pair(U32, String), U32> -> @draw:SpanDraw -> SpanStep
The step of a span ID draw after its next source word, SpanDraw.feed of its
fields: the feed that Drive takes.
def SpanStep.waiting source · line 1208 · raw
@step:SpanStep -> Maybe<&2, SpanDraw>
The draw that a span ID draw's step feeds its next word to, while it waits for one.
def SpanDraw.result source · line 1220 · raw
@step:SpanStep -> Result<&2, &2, GenerationError, SpanId>
The span ID of a finished span ID draw, or why it failed, as TraceDraw.result; law span_id_ends shows that the word budget of SpanId.generate_with makes the unfinished case unreachable.
def SpanDraw.run source · line 1230 · raw
@fuel:Nat -> @current:Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, SpanStep) -> Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, SpanStep)
Drive a span ID draw from a tape (Drive.run).
def SpanDraw.ended source · line 1238 · raw
@result:Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, SpanStep) -> Bool
Whether the span ID draw in a driver's result has ended.
def SpanDraw.outcome source · line 1242 · raw
@-S:Type -> @done:Pair(S, SpanStep) -> Pair(S, Result<&2, &2, GenerationError, SpanId>)
The source's final state with the span ID draw's result.
def Step.of_span source · line 1265 · raw
@step:SpanStep -> @trace_id:TraceId -> @sampled:Bool -> Step
The generation that a span ID draw's step gives, for a context of
trace_id with the sampled indication sampled: waiting for the draw's
next word, the context once the span ID is drawn, or the draw's failure.
def SpanPlan.root source · line 1277 · raw
@trace_id:TraceId -> @sampled:Bool -> SpanPlan
The plan of a root's span ID, once its trace ID is drawn, and of a restart's: nothing to exclude, and the sampled indication that the root or the restart was given, as it is given.
def SpanPlan.child source · line 1283 · raw
@+parent:Parent -> @sampling:Sampling -> SpanPlan
The plan of a child's span ID: the parent's span ID excluded, the parent's
trace ID, and the sampled indication that sampling resolves from the
parent's.
def SpanPlan.draw source · line 1287 · raw
@plan:SpanPlan -> Step
The generation that draws the span ID of a plan, from its first candidate.
def Step.of_trace source · line 1296 · raw
@step:TraceStep -> @sampled:Bool -> Step
The generation that a trace ID draw's step gives, for a root or a restart
with the sampled indication sampled: waiting for the draw's next word,
the root's span ID draw once the trace ID is drawn (SpanPlan.root), or the
draw's failure.
def TracePlan.root source · line 1307 · raw
@sampled:Bool -> TracePlan
The plan of a root: no trace ID to exclude, and the sampled indication
sampled, as it is given.
def TracePlan.restart source · line 1312 · raw
@previous:RemoteContext -> @sampled:Bool -> TracePlan
The plan of a restart replacing previous: the received trace ID to
exclude, and the sampled indication sampled, as it is given.
def TracePlan.draw source · line 1317 · raw
@plan:TracePlan -> Step
The generation that draws the new trace of a plan: its trace ID, from the first candidate, then the span ID of the root's span plan (Step.of_trace).
def Draw.root source · line 1323 · raw
@sampled:Bool -> Step
A root draws the new trace of its plan (TracePlan.root).
def Draw.restart source · line 1328 · raw
@previous:RemoteContext -> @sampled:Bool -> Step
A restart draws like a root but excludes the received trace ID (TracePlan.restart).
def Draw.child source · line 1332 · raw
@+parent:Parent -> @sampling:Sampling -> Step
A child draws the span ID of its plan (SpanPlan.child).
def Draw.feed source · line 1338 · raw
@word:Result<&1, &1, Pair(U32, String), U32> -> @draw:Draw -> Step
Feed the next source word, or the source's error, to the trace ID draw or the span ID draw that the generation runs. A source error ends the draw, and so the generation, at once with SourceFailure (law feed_failure).
def Step.waiting source · line 1347 · raw
@step:Step -> Maybe<&2, Draw>
The draw that a generation's step feeds its next word to, while it waits for one.
def Step.result source · line 1360 · raw
@step:Step -> Result<&2, &2, GenerationError, LocalContext>
The result of a finished generation. A generation that has not finished would report the identifier it was drawing; the root_ends, child_ends and restart_ends laws show that the word budgets of the operations below make those cases unreachable.
def Draw.run source · line 1372 · raw
@fuel:Nat -> @current:Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, Step) -> Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, Step)
Drive a generation from a tape (Drive.run).
def Draw.ended source · line 1386 · raw
@result:Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, Step) -> Bool
Whether the generation in a driver's result has ended.
def Draw.outcome source · line 1390 · raw
@-S:Type -> @done:Pair(S, Step) -> Pair(S, Result<&2, &2, GenerationError, LocalContext>)
The source's final state with the generation's result.
def TracePlan.generation source · line 1399 · raw
@plan:TracePlan -> Generation
The generation of the new trace of a plan: at most 48 words, eight trace ID candidates of four words and eight span ID candidates of two.
def Generation.root source · line 1404 · raw
@sampled:Bool -> Generation
A root with the sampled indication sampled, as it is given
(TracePlan.root).
def Generation.restart source · line 1409 · raw
@previous:RemoteContext -> @sampled:Bool -> Generation
A restart replacing previous, with the sampled indication sampled, as a
root (TracePlan.restart).
def Generation.child source · line 1413 · raw
@+parent:Parent -> @sampling:Sampling -> Generation
A child of parent: at most 16 words, eight span ID candidates.
def Generation.needs.of source · line 1417 · raw
@fuel:Nat -> @step:Step -> Bool
Whether a step needs another word within fuel more words.
def Generation.needs source · line 1430 · raw
@generation:Generation -> Bool
Whether the generation needs another word: it has not ended, and its budget allows one more.
def Generation.fed source · line 1437 · raw
@fuel:Nat -> @step:Step -> @word:Result<&1, &1, Pair(U32, String), U32> -> Generation
The generation after word: the step it gives with one word less of
budget, or, for a step that needs no word, the same step with none left.
def Generation.feed source · line 1450 · raw
@generation:Generation -> @word:Result<&1, &1, Pair(U32, String), U32> -> Generation
Feed the generation the next word of its source (see Draw.feed). A generation that needs no word ignores it.
def Generation.result source · line 1459 · raw
@generation:Generation -> Result<&2, &2, GenerationError, LocalContext>
The generation's result: the context it created, or why it failed. One that still needs a word once its budget is spent has exhausted its candidates; the root_ends, child_ends and restart_ends laws show that the budgets suffice.
def Draw.span_context source · line 1475 · raw
@-S:Type -> @+trace_id:TraceId -> @+sampled:Bool -> @done:Pair(S, Result<&2, &2, GenerationError, SpanId>) -> Pair(S, Result<&2, &2, GenerationError, LocalContext>)
The context of a span ID generated from a source for an operation of
trace_id with the sampled indication sampled, with the source's final
state: the span ID's failure is the context's.
def Source.tape source · line 1551 · raw
@tape:List<&1, Result<&1, &1, Pair(U32, String), U32>> -> IO(Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, Result<&1, &1, Pair(U32, String), U32>))
A deterministic source that replays a tape of word results.
def Error.show source · line 1565 · raw
@error:Error -> String
The name of a codec or ID error, with its offset or, for an unsupported version, its two digits. ZeroId names the field: ZeroTraceId, ZeroParentId or ZeroSpanId.
def ContextError.show source · line 1591 · raw
@error:ContextError -> String
The name of a context creation error.
def GenerationError.show source · line 1600 · raw
@error:GenerationError -> String
The name of a generation error; a source failure adds the source's code and message.
def Limits.is_valid source · line 1631 · raw
@traceparent_input:Nat -> @tracestate_input:Nat -> @+tracestate_output:Nat -> Bool
The rules of a configuration, which must accept its own emitted representation: a traceparent input budget of at least 55 octets, the length of a v00 value, and a tracestate input budget no smaller than an output budget of at least 512 octets (spec #1, "Tracestate policy and resource bounds"; the 512-octet minimum comes from #8; law limits_bounds).
def Limits.error source · line 1648 · raw
@traceparent_input:Nat -> @tracestate_output:Nat -> LimitsError
The first rule a refused configuration breaks.
def Limits.new.checked source · line 1654 · raw
@traceparent_input:Nat -> @tracestate_input:Nat -> @tracestate_output:Nat -> @valid:Bool -> @evidence:{Limits.is_valid(traceparent_input, tracestate_input, tracestate_output) == valid : Bool} -> Result<&2, &2, LimitsError, Limits>The configuration, when the check found it valid.
def Limits.new source · line 1665 · raw
@+traceparent_input:Nat -> @+tracestate_input:Nat -> @+tracestate_output:Nat -> Result<&2, &2, LimitsError, Limits>
Validate a configuration; budgets count UTF-8 octets (laws limits_new and limits_fields).
def Limits.default source · line 1673 · raw
Limits
32 KiB for each received value and 512 octets for an emitted tracestate (law default_limits). The 512-octet output budget is this package's capacity policy, not a W3C maximum.
def Limits.traceparent_input source · line 1677 · raw
@limits:Limits -> Nat
The most octets a received traceparent value may take.
def Limits.tracestate_input source · line 1684 · raw
@limits:Limits -> Nat
The most octets a combined tracestate value may take, including the commas that join repeated fields.
def Limits.tracestate_output source · line 1690 · raw
@limits:Limits -> Nat
The most octets an emitted tracestate may take.
def LimitsError.show source · line 1696 · raw
@error:LimitsError -> String
The name of a limits error.
def StateChar.in_range source · line 1722 · raw
@+code:U32 -> @low:U32 -> @high:U32 -> Bool
Whether a code point lies between two others, both included.
def StateChar.is_key_start source · line 1727 · raw
@char:Char -> Bool
lcalpha / DIGIT: a lowercase ASCII letter (%x61-7A) or a digit (%x30-39), the first character of a key.
def StateChar.is_key source · line 1733 · raw
@+char:Char -> Bool
keychar: lcalpha / DIGIT / "_" / "-" / "*" / "/" / "@".
def StateChar.is_value_end source · line 1739 · raw
@char:Char -> Bool
nblk-chr: %x21-2B / %x2D-3C / %x3E-7E, printable ASCII other than space, "," and "=". A value ends with one of these.
def StateChar.is_value source · line 1746 · raw
@+char:Char -> Bool
chr: %x20 / nblk-chr, a character of a value: nblk-chr or a space.
def StateChar.is_ows source · line 1750 · raw
@+char:Char -> Bool
OWS: a space or a horizontal tab (RFC 9110, section 5.6.3).
def StateKey.valid.rest source · line 1756 · raw
@text:String -> @room:Nat -> Bool
Every remaining character is a key character, and at most room remain.
The recursion stops once the room is used up, so a huge invalid key is not
read to its end.
def StateKey.is_valid source · line 1769 · raw
@text:String -> Bool
key = ( lcalpha / DIGIT ) 0*255( keychar ): 1 to 256 characters (W3C 3.3.2.2.1). Level 1's tenant@system restriction does not apply.
def StateValue.valid.go source · line 1778 · raw
@tail:String -> @char:Char -> @room:Nat -> Bool
char is a value character followed by tail, of which at most room
characters are allowed; the last character is not a space.
def StateValue.is_valid source · line 1791 · raw
@text:String -> Bool
value = 0*255( chr ) nblk-chr: 1 to 256 printable ASCII characters other than "," and "=", the last of which is not a space (W3C 3.3.2.2.2).
def StateKey.parse.checked source · line 1811 · raw
@text:String -> @valid:Bool -> @evidence:{StateKey.is_valid(text) == valid : Bool} -> Result<&2, &2, EntryError, StateKey>The key, when the check found the text valid.
def StateKey.parse source · line 1821 · raw
@+text:String -> Result<&2, &2, EntryError, StateKey>
Accept exactly a Level 2 key, or fail with InvalidKey. Nothing is trimmed or folded (laws key_parse, key_roundtrip and key_separators).
def StateKey.to_string source · line 1825 · raw
@key:StateKey -> String
The key's text.
def StateValue.parse.checked source · line 1831 · raw
@text:String -> @valid:Bool -> @evidence:{StateValue.is_valid(text) == valid : Bool} -> Result<&2, &2, EntryError, StateValue>The value, when the check found the text valid.
def StateValue.parse source · line 1842 · raw
@+text:String -> Result<&2, &2, EntryError, StateValue>
Accept exactly a Level 2 value, leading spaces included, or fail with InvalidValue. No whitespace is trimmed here, so a trailing space is refused (laws value_parse, value_roundtrip and value_separators).
def StateValue.to_string source · line 1846 · raw
@value:StateValue -> String
The value's text.
def EntryError.show source · line 1852 · raw
@error:EntryError -> String
The name of an entry error.
def StateEntry.key source · line 1884 · raw
@entry:StateEntry -> StateKey
The entry's key.
def StateEntry.value source · line 1890 · raw
@entry:StateEntry -> StateValue
The entry's value.
def StateEntry.key_text source · line 1896 · raw
@entry:StateEntry -> String
The text of the entry's key.
def StateEntry.format source · line 1900 · raw
@entry:StateEntry -> String
key=value, as the entry is sent.
def Entries.has_key source · line 1906 · raw
@entries:List<&2, StateEntry> -> @+key:String -> Bool
Whether one of the entries has this key.
def Entries.unique source · line 1915 · raw
@entries:List<&2, StateEntry> -> @+seen:List<&2, StateEntry> -> Bool
No entry repeats the key of an entry before it; seen holds the entries
already passed. This is the order in which the reading machine checks keys.
def TraceState.is_valid source · line 1924 · raw
@+entries:List<&2, StateEntry> -> Bool
Distinct keys and at most 32 entries (W3C 3.3.2 and 3.3.3).
def TraceState.empty source · line 1934 · raw
TraceState
The state with no entries. It formats as "".
def TraceState.entries source · line 1938 · raw
@state:TraceState -> List<&2, StateEntry>
The entries in order, leftmost first.
def TraceState.is_empty source · line 1944 · raw
@state:TraceState -> Bool
Whether the state has no entries.
def Entries.get.put source · line 1948 · raw
@entry:StateEntry -> @rest:Maybe<&2, StateValue> -> @hit:Bool -> Maybe<&2, StateValue>
The value of entry when its key matched, or the result for the rest.
def Entries.get source · line 1956 · raw
@entries:List<&2, StateEntry> -> @+key:String -> Maybe<&2, StateValue>
The value of the first entry with this key.
def TraceState.get source · line 1965 · raw
@state:TraceState -> @key:StateKey -> Maybe<&2, StateValue>
The value of the entry with this key, if there is one (laws get_entry and get_absent). The key is validated, so a lookup never needs to check it.
def Entries.format.rest source · line 1969 · raw
@entries:List<&2, StateEntry> -> String
Each entry after the first, preceded by its comma.
def Entries.format source · line 1977 · raw
@entries:List<&2, StateEntry> -> String
The entries as key=value, joined by commas.
def TraceState.format source · line 1987 · raw
@state:TraceState -> String
The normalized value: the entries in order, joined by commas, with no optional whitespace. The empty state formats as "" (laws state_roundtrip and first_wins).
def Utf8.width source · line 1999 · raw
@char:Char -> Nat
The UTF-8 octets of a character. Bend characters are Unicode code points, so this is the size of the character's UTF-8 encoding: 1 to 4.
def Utf8.length source · line 2010 · raw
@text:String -> Nat
The UTF-8 octets of a text, in which the laws state every budget. Emission measures keys and values with it, at most 256 characters each; parsing measures received text with Utf8.left instead, which stops counting past the budget.
def Budget.take source · line 2019 · raw
@need:Nat -> @budget:Nat -> Maybe<&2, Nat>
What is left of a budget after taking need octets, or None when less
remains.
def Utf8.left source · line 2031 · raw
@text:String -> @budget:Maybe<&2, Nat> -> Maybe<&2, Nat>
What is left of a budget after a text, or None once the text exceeds it. Measuring stops at the first character beyond the budget, and a None budget stays None.
def Utf8.left_more source · line 2042 · raw
@fields:List<&2, String> -> @budget:Maybe<&2, Nat> -> Maybe<&2, Nat>
Fields after the first are measured with the comma that joins them. Once the budget is exceeded, no further field is visited.
def Utf8.left_fields source · line 2053 · raw
@fields:List<&2, String> -> @budget:Maybe<&2, Nat> -> Maybe<&2, Nat>
What is left of a budget after repeated fields and the commas that join them.
def Value.restore.step source · line 2088 · raw
@kept:Bool -> @ows:Bool -> @char:Char -> @value:String -> Pair(Bool, String)
A value's characters arrive most recent first. Restoring them skips optional whitespace until the first other character, then keeps every character, so the value comes back in reading order without its trailing whitespace.
def Value.restore.go source · line 2101 · raw
@text:String -> @state:Pair(Bool, String) -> String
The restoring loop: one character at a time, with the state (whether a character was kept yet, the value so far).
def Value.restore source · line 2111 · raw
@text:String -> String
The value in reading order without its trailing optional whitespace.
def Member.start source · line 2117 · raw
@ows:Bool -> @equals:Bool -> @char:Char -> Member
A character of a member that has no key yet: optional whitespace is skipped, an "=" gives the member an empty key, which validation refuses, and anything else starts the key.
def Member.key source · line 2130 · raw
@equals:Bool -> @char:Char -> @text:String -> Member
A character inside a key: the first "=" ends the key, anything else extends it. Key characters are validated when the member ends.
def Member.push source · line 2139 · raw
@+char:Char -> @current:Member -> Member
A character other than a comma extends the current member. Inside a value every character is kept; validation refuses those the grammar excludes.
def Scan.validate source · line 2150 · raw
@key:String -> @value:String -> Result<&2, &2, EntryError, StateEntry>
Validate the key and value texts of a member that ended. An invalid key is reported before an invalid value.
def Entries.add.if source · line 2158 · raw
@entries:List<&2, StateEntry> -> @entry:StateEntry -> @present:Bool -> List<&2, StateEntry>
Keep the entries unchanged when the key was present; otherwise add the entry at the end.
def Entries.add source · line 2167 · raw
@+entries:List<&2, StateEntry> -> @+entry:StateEntry -> List<&2, StateEntry>
Keep only the first entry of each key (spec #1, "Preserve the first occurrence of a duplicate key").
def Scan.keep source · line 2172 · raw
@room:Nat -> @member:Nat -> @entry:StateEntry -> @entries:List<&2, StateEntry> -> Scan
A valid member counts toward the 32 allowed before duplicates are dropped (spec #1); with no room left, the state is discarded with TooManyMembers.
def Scan.entry source · line 2181 · raw
@parsed:Result<&2, &2, EntryError, StateEntry> -> @member:Nat -> @room:Nat -> @entries:List<&2, StateEntry> -> Scan
A member that ended: an invalid one stops reading with its number and reason; a valid one is counted and kept.
def Scan.close source · line 2193 · raw
@member:Nat -> @room:Nat -> @current:Member -> @entries:List<&2, StateEntry> -> Scan
The current member ends at a comma or with the value. An empty member, or one of optional whitespace only, is ignored but still numbered; a member without "=" is refused; otherwise its key and value are validated, trailing optional whitespace left out of the value.
def Scan.read source · line 2204 · raw
@comma:Bool -> @char:Char -> @member:Nat -> @room:Nat -> @current:Member -> @entries:List<&2, StateEntry> -> Scan
One character of a scan that is still reading: a comma ends the member, and anything else extends it.
def Scan.char source · line 2213 · raw
@+char:Char -> @scan:Scan -> Scan
Read one character, unless the scan has stopped.
def Scan.text source · line 2222 · raw
@text:String -> @scan:Scan -> Scan
Read a text one character at a time, stopping at the first problem. This is a loop (a tail call), so its depth does not grow with the text.
def Scan.more source · line 2232 · raw
@fields:List<&2, String> -> @scan:Scan -> Scan
Fields after the first are read after the comma that joins them.
def Scan.fields source · line 2240 · raw
@fields:List<&2, String> -> @scan:Scan -> Scan
Read repeated fields as their comma-joined combination.
def Scan.start source · line 2248 · raw
Scan
The scan of a new value: no member ended, 32 allowed, nothing kept.
def Scan.state source · line 2255 · raw
@entries:List<&2, StateEntry> -> @valid:Bool -> @evidence:{TraceState.is_valid(entries) == valid : Bool} -> Result<&2, &2, StateError, TraceState>The scan keeps only the first entry of each key and stops at a 33rd member, so this check is not expected to fail: the laws prove it passes for normalized values, and the corpus exercises the rest. A failure would be reported as too many members.
def Scan.result source · line 2265 · raw
@scan:Scan -> Result<&2, &2, StateError, TraceState>
The state read, once the last member has ended. TraceState.is_valid is checked here to build the state's evidence.
def Scan.finish source · line 2273 · raw
@scan:Scan -> Result<&2, &2, StateError, TraceState>
The last member ends with the value.
def Scan.within source · line 2281 · raw
@fits:Maybe<&2, Nat> -> @fields:List<&2, String> -> Result<&2, &2, StateError, TraceState>
Read the fields only when they fit the budget.
def TraceState.parse_fields source · line 2300 · raw
@limits:Limits -> @+fields:List<&2, String> -> Result<&2, &2, StateError, TraceState>
Parse repeated tracestate field values, in arrival order, as their comma-joined combination (W3C 3.3.2). The combined value, joining commas included, must fit the tracestate input budget; a larger one is refused with StateTooLarge before any member is read, without measuring the rest. Then: empty members are ignored, and so is optional whitespace before a member and after its value; every nonempty member must be a valid entry (InvalidEntry) and counts toward the 32 allowed (TooManyMembers); the first entry of each key is kept. An error discards the whole state; a valid traceparent stays valid (spec #1). W3C 3.3: parse tracestate only for a message whose traceparent was parsed. Laws: fields_join, over_budget, within_budgets, first_wins and the others of section 10 of LAWS.bend.
def TraceState.parse source · line 2304 · raw
@limits:Limits -> @text:String -> Result<&2, &2, StateError, TraceState>
Parse one combined tracestate value; see TraceState.parse_fields.
def StateError.show source · line 2309 · raw
@error:StateError -> String
The name of a tracestate error; InvalidEntry adds the member number and the reason.
def Entries.unless source · line 2328 · raw
@-A:Data -> @skip:Bool -> @item:A -> @rest:List<&2, A> -> List<&2, A>
item followed by rest, unless skip is True: one step of a filter.
Removing a key and listing the dropped keys both use it.
def Entries.without source · line 2336 · raw
@entries:List<&2, StateEntry> -> @+key:String -> List<&2, StateEntry>
The entries without the one whose key is key, in order.
def TraceState.from_entries.checked source · line 2347 · raw
@entries:List<&2, StateEntry> -> @fallback:TraceState -> @valid:Bool -> @evidence:{TraceState.is_valid(entries) == valid : Bool} -> TraceStateThe state of these entries when the check finds them valid, fallback
otherwise. Updates build their entries so that the check passes, which the
laws prove; fallback keeps the function total without an unchecked
conversion.
def TraceState.from_entries source · line 2356 · raw
@+entries:List<&2, StateEntry> -> @fallback:TraceState -> TraceState
The state of entries, checked, or fallback if the check fails.
def TraceState.set source · line 2364 · raw
@+state:TraceState -> @+key:StateKey -> @value:StateValue -> TraceState
Add or update the entry of key (W3C 3.5): it goes to the front with
value, and the other entries follow in their order. At most 31 of them
stay, so a new key in a full state removes the last entry, while updating a
key that is present evicts nothing (laws set_entries, update_keeps_all,
insert_entries and set_get).
def TraceState.remove source · line 2372 · raw
@+state:TraceState -> @key:StateKey -> TraceState
Delete the entry of key, if there is one; the other entries keep their
order (W3C 3.5; laws remove_entries and remove_get). W3C asks participants
not to delete keys other vendors generated: that breaks correlation in
their systems.
def StateEntry.size source · line 2384 · raw
@entry:StateEntry -> Nat
The octets of key=value (law entry_size).
def Entries.size.rest source · line 2390 · raw
@entries:List<&2, StateEntry> -> Nat
The octets of each entry after the first, with its comma.
def Entries.size source · line 2398 · raw
@entries:List<&2, StateEntry> -> Nat
The octets of the entries joined by commas, as Entries.format writes them.
def TraceState.size source · line 2406 · raw
@state:TraceState -> Nat
The octets of TraceState.format(state) (law state_size).
def Truncation.kept source · line 2416 · raw
@truncation:Truncation -> TraceState
The state that fits the output budget.
def Truncation.dropped source · line 2423 · raw
@truncation:Truncation -> List<&2, StateKey>
The keys of the entries removed, in their original order; none when the state already fitted.
def StateEntry.is_large source · line 2430 · raw
@entry:StateEntry -> Bool
Whether the entry is larger than 128 octets. W3C 3.3.3.1 asks to remove such entries first.
def Entries.has_large source · line 2434 · raw
@entries:List<&2, StateEntry> -> Bool
Whether one of the entries is larger than 128 octets.
def Entries.drop_last_large source · line 2443 · raw
@entries:List<&2, StateEntry> -> List<&2, StateEntry>
The entries without the rightmost one larger than 128 octets: an entry stays when a large entry follows it.
def Entries.drop_last source · line 2452 · raw
@entries:List<&2, StateEntry> -> List<&2, StateEntry>
The entries without the rightmost one.
def Entries.shrink source · line 2462 · raw
@+entries:List<&2, StateEntry> -> List<&2, StateEntry>
One removal step (spec #1): the rightmost entry larger than 128 octets, or the rightmost entry when none is.
def Entries.truncate source · line 2470 · raw
@fuel:Nat -> @+budget:Nat -> @+entries:List<&2, StateEntry> -> List<&2, StateEntry>
Remove entries one step at a time while they take more than budget
octets, and stop as soon as they fit. fuel bounds the steps. One per
entry suffices: once every entry is removed, the empty list takes 0 octets,
which fits any budget.
def Entries.dropped source · line 2479 · raw
@entries:List<&2, StateEntry> -> @+kept:List<&2, StateEntry> -> List<&2, StateKey>
The keys of the entries that kept lacks, in order.
def TraceState.truncate source · line 2493 · raw
@limits:Limits -> @state:TraceState -> Truncation
Fit a state to the output budget of limits by removing whole entries
(W3C 3.3.3.1, spec #1): while the value is over the budget, remove the
rightmost entry larger than 128 octets, or the rightmost entry when none is,
and stop as soon as it fits. The surviving entries keep their order (laws
truncate_steps, truncate_fits, truncate_whole, truncate_order and
truncate_dropped).
def OutgoingContext.new source · line 2524 · raw
@context:LocalContext -> OutgoingContext
An outgoing context with no state yet, as for a new root.
def OutgoingContext.with_state source · line 2530 · raw
@context:LocalContext -> @state:TraceState -> OutgoingContext
An outgoing context that sends state, such as the state received with the
parent of a child operation. The caller associates the state with this
operation, as with Context.from_ids.
def OutgoingContext.context source · line 2534 · raw
@outgoing:OutgoingContext -> LocalContext
The local operation.
def OutgoingContext.state source · line 2540 · raw
@outgoing:OutgoingContext -> TraceState
The state sent with the operation.
def OutgoingContext.get source · line 2546 · raw
@outgoing:OutgoingContext -> @key:StateKey -> Maybe<&2, StateValue>
The value of the entry with this key, if there is one.
def OutgoingContext.set source · line 2551 · raw
@outgoing:OutgoingContext -> @key:StateKey -> @value:StateValue -> OutgoingContext
Add or update an entry (see TraceState.set); the context is unchanged (law outgoing_set).
def OutgoingContext.remove source · line 2558 · raw
@outgoing:OutgoingContext -> @key:StateKey -> OutgoingContext
Delete an entry (see TraceState.remove); the context is unchanged (law outgoing_remove).
def Emission.of source · line 2564 · raw
@context:LocalContext -> @truncation:Truncation -> Emission
The emission of a context and a truncated state.
def OutgoingContext.emit source · line 2573 · raw
@limits:Limits -> @outgoing:OutgoingContext -> Emission
The traceparent and tracestate values to send: the participating
traceparent of the context, and the normalized value of the state
truncated to the output budget of limits (laws emit_traceparent,
emit_tracestate, emit_fits and emit_accepted).
def Emission.traceparent source · line 2579 · raw
@emission:Emission -> String
The traceparent value: always 55 characters.
def Emission.tracestate source · line 2585 · raw
@emission:Emission -> String
The tracestate value: at most the output budget in octets, "" for no state.
def Emission.dropped source · line 2591 · raw
@emission:Emission -> List<&2, StateKey>
The keys of the entries truncation dropped, in their original order.
def Header.name source · line 2697 · raw
@header:Header -> String
The field's name.
def Header.value source · line 2703 · raw
@header:Header -> String
The field's value.
def Carrier.traceparent_name source · line 2712 · raw
String
The names of the two context fields, in lowercase (W3C 3.2.1 and 3.3.1), written in this one place: extraction selects the fields by them, whatever the case of the names received; cleanup, injection and forwarding remove and write the fields under them; and Context.field_names publishes them.
def Carrier.tracestate_name source · line 2715 · raw
String
def Carrier.named source · line 2724 · raw
@name:String -> @text:String -> Bool
Whether text is name without regard to ASCII case (W3C 3.2.1 and
3.3.1): each character of text, with the letters A to Z lowered, is the
character of name at its position. Other characters are compared as they
are, so a name that differs by more than ASCII case names another field.
name is written in lowercase, and the comparison follows it, so a long
field name is not read past it.
def Carrier.keep source · line 2736 · raw
@hit:Bool -> @value:String -> @found:List<&2, String> -> List<&2, String>
value before found when hit is True: one step of Carrier.values.
def Carrier.values.go source · line 2744 · raw
@carrier:List<&2, Header> -> @+name:String -> @found:List<&2, String> -> List<&2, String>
The values of the fields named name, most recent first, before found.
def Carrier.values source · line 2754 · raw
@carrier:List<&2, Header> -> @+name:String -> List<&2, String>
The values of the fields named name without regard to ASCII case, in
their order: the loop collects them most recent first, and reversing, also
a loop, puts them back in order.
def Text.drop_ows.go source · line 2768 · raw
@tail:String -> @head:Char -> @ows:Bool -> String
head followed by tail, without the optional whitespace at its start:
ows says whether head is optional whitespace.
def Text.drop_ows source · line 2781 · raw
@text:String -> String
The text without the optional whitespace, spaces and horizontal tabs, at its start.
def Text.trim_ows source · line 2792 · raw
@text:String -> String
The text without the optional whitespace at its start and at its end (RFC 9110, section 5.5: "A field value does not include leading or trailing whitespace"). Reversing brings the end to the front, and reversing again brings it back.
def Text.has_comma.go source · line 2797 · raw
@text:String -> @found:Bool -> Bool
Whether the text contains a comma: found records whether one was seen
before.
def Text.has_comma source · line 2807 · raw
@text:String -> Bool
Whether the text contains a comma.
def Text.is_control source · line 2814 · raw
@char:Char -> Bool
Whether a character is a control character other than a horizontal tab: U+0000 to U+0008, U+000A to U+001F or U+007F. No field value may hold one (RFC 9110, section 5.5); a carriage return or a line feed would end the field.
def Text.control.go source · line 2821 · raw
@text:String -> @+offset:Nat -> @found:Maybe<&2, Nat> -> Maybe<&2, Nat>
The offset of the first control character of text, counted from
offset, unless found already holds one. This is a loop.
def Read.is_later source · line 2834 · raw
@digits:0x665ae73e3f32ce98f72c7cf6844cfd3f/src/digits.Digits(2n) -> Result<&2, &2, Error, Bool>
Whether a value's version, from its two digits, is later than 00 and so read by its known prefix (W3C 3.2.2.1 and 3.2.4): Done{False{}} for 00, which the strict codec reads, Done{True{}} for 01 to fe, and a refusal for ff.
def Read.is_later.parsed source · line 2844 · raw
@parsed:Parsed<2n> -> Result<&2, &2, Error, Bool>
Whether the version whose two digits were read is later than 00.
def Read.clean source · line 2851 · raw
@found:Maybe<&2, Nat> -> Result<&2, &2, Error, Unit>
The fields a later version does not know, once searched for a control character: none, or the offset of the first.
def Read.extension source · line 2865 · raw
@rest:String -> Result<&2, &2, Error, Unit>
What may follow the flags of a later version: the end of the value, or a dash that starts fields this version does not know. Those fields are not read (W3C 3.2.4: "Vendors MUST NOT parse or assume anything about unknown fields"), except that a control character in them is refused with ControlCharacter at its offset: no field value may hold one (RFC 9110, section 5.5), and a value forwarded unchanged must not end a message's field. Any other character than a dash at offset 55 is ExpectedSeparator.
def Read.prefix source · line 2879 · raw
@+text:String -> Result<&2, &2, Error, TraceParentV00>
A later version is read by its known prefix (W3C 3.2.4 and 4.1.2): its first 55 characters are read as version 00, which checks the trace ID, the parent ID, the flags and the dashes between them at their own offsets, and then the value must end or continue with a dash. A value that ends before its 55th character, with no invalid character before, fails with UnexpectedEnd.
def Read.by_version source · line 2886 · raw
@later:Bool -> @text:String -> Result<&2, &2, Error, TraceParentV00>
Read a value by the rules of its version: later is False for 00.
def Read.known source · line 2894 · raw
@+text:String -> Result<&2, &2, Error, TraceParentV00>
The known fields of a value, read by the rules of its version.
def Read.invalid source · line 2901 · raw
@result:Result<&2, &2, Error, TraceParentV00> -> Result<&2, &2, TraceParentError, TraceParentV00>
A refusal of the codec, as a refused traceparent.
def Read.single source · line 2911 · raw
@combined:Bool -> @text:String -> Result<&2, &2, TraceParentError, TraceParentV00>
A value that joins several with a comma is refused as repeated fields; any other value is read by the rules of its version.
def Read.trimmed source · line 2919 · raw
@+text:String -> Result<&2, &2, TraceParentError, TraceParentV00>
A value without the whitespace around it, refused when it joins several.
def Read.within source · line 2924 · raw
@fits:Maybe<&2, Nat> -> @value:String -> Result<&2, &2, TraceParentError, TraceParentV00>
A value within its budget is read without the optional whitespace around it; a value over the budget is refused without being read further.
def TraceParent.read source · line 2951 · raw
@limits:Limits -> @+value:String -> Result<&2, &2, TraceParentError, TraceParentV00>
Read one received traceparent value by the rules of a participant, and
return its known fields as a v00 value, flag byte included:
- a value over the traceparent input budget of limits, counted in UTF-8
octets with its whitespace, is refused with TraceParentTooLarge;
- optional whitespace around the value is removed (RFC 9110, section 5.5);
- a value with a comma joins repeated fields and is refused with
RepeatedTraceParent, even when the comma is in fields of a later
version: no version defines a comma, and a host that joins repeated
fields separates them with one (RFC 9110, section 5.3);
- version 00 is read exactly by TraceParentV00.parse: 55 characters and
nothing after them;
- version ff is refused with ForbiddenVersion (W3C 3.2.2.1);
- versions 01 to fe are read by their known prefix: the fields of version
00, followed by the end of the value or by a dash and fields that are
not read, whatever they hold other than a comma or a control character,
which is refused with ControlCharacter (W3C 3.2.4 and 4.1.2; RFC 9110,
section 5.5).
RemoteContext.from_traceparent then keeps the sampled and random-trace-id
flags. Laws: read_v00, read_v00_exact, read_future, read_ff, read_comma,
read_over_budget and read_within_budgets.
def Extract.ignored source · line 2963 · raw
@states:List<&2, String> -> StateOutcome
The state outcome when the tracestate fields are not read: absent without a field, ignored with one (W3C 3.3).
def Extract.kept source · line 2972 · raw
@base:Maybe<&2, BaseContext> -> @parent:TraceParentOutcome -> @states:List<&2, String> -> Extraction
The extraction of a message whose context is not read: the base is kept, with the traceparent outcome and the presence of tracestate fields.
def Extract.incoming source · line 2977 · raw
@remote:RemoteContext -> @state:TraceState -> @received:Maybe<&2, ReceivedPair> -> Maybe<&2, BaseContext>
The incoming context of an accepted message, as the context to continue from.
def Extract.parsed source · line 2985 · raw
@parsed:Result<&2, &2, StateError, TraceState> -> @remote:RemoteContext -> @text:String -> @states:List<&2, String> -> Extraction
An accepted message whose tracestate fields were parsed: an accepted state keeps the pair, which can be forwarded, and a refused one is discarded whole, keeping the traceparent (spec #1) but no pair, since the pair was not accepted whole.
def Extract.state source · line 2996 · raw
@+limits:Limits -> @+states:List<&2, String> -> @remote:RemoteContext -> @text:String -> Extraction
An accepted message with its tracestate field values, read in arrival order as their comma-joined combination (W3C 3.3.2).
def Extract.read source · line 3007 · raw
@read:Result<&2, &2, TraceParentError, TraceParentV00> -> @value:String -> @+limits:Limits -> @+states:List<&2, String> -> @base:Maybe<&2, BaseContext> -> Extraction
The extraction of a message whose only traceparent value value was read.
The value is kept without the whitespace around it only once accepted, so a
refused value is not read further.
def Extract.parents source · line 3017 · raw
@+limits:Limits -> @parents:List<&2, String> -> @+states:List<&2, String> -> @base:Maybe<&2, BaseContext> -> Extraction
The extraction of a message with these traceparent and tracestate field values.
def Context.extract source · line 3042 · raw
@+limits:Limits -> @+carrier:List<&2, Header> -> @base:Maybe<&2, BaseContext> -> Extraction
Extract the trace context of a received message from its carrier, with
base as the context to keep when the message has no usable traceparent
(spec #1, user stories 14, 15, 16, 24 and 25):
- no traceparent field keeps the base, TraceParentAbsent{};
- more than one traceparent field, whatever the case of their names, is
refused, and so is a single value that TraceParent.read refuses; the
base is kept, TraceParentRejected{error};
- an accepted value gives the incoming context and replaces the base: its
tracestate fields, whatever the case of their names, are read in
arrival order as their comma-joined combination, within the tracestate
input budget; refused fields are discarded whole, keeping the
traceparent;
- without an accepted traceparent, tracestate fields are not read.
Laws: extract_absent, extract_repeated, extract_refused, extract_read,
state_independent and received_bounds.
def Extraction.context source · line 3051 · raw
@extraction:Extraction -> Maybe<&2, BaseContext>
The context to continue from: this message's incoming context when its traceparent was accepted, the base otherwise.
def Extraction.parent source · line 3057 · raw
@extraction:Extraction -> TraceParentOutcome
What extraction found in the traceparent fields.
def Extraction.state source · line 3063 · raw
@extraction:Extraction -> StateOutcome
What extraction did with the tracestate fields.
def Extraction.incoming.base source · line 3069 · raw
@context:Maybe<&2, BaseContext> -> Maybe<&2, IncomingContext>
The incoming context an accepted message gives as its context.
def Extraction.incoming.of source · line 3078 · raw
@parent:TraceParentOutcome -> @context:Maybe<&2, BaseContext> -> Maybe<&2, IncomingContext>
This message's own context: the incoming context when its traceparent was accepted, None{} when extraction kept the base.
def Extraction.incoming source · line 3090 · raw
@extraction:Extraction -> Maybe<&2, IncomingContext>
The context this message carried, when its traceparent was accepted; None{} when extraction kept the base, even an incoming one.
def IncomingContext.context source · line 3096 · raw
@incoming:IncomingContext -> RemoteContext
The sender's operation.
def IncomingContext.state source · line 3103 · raw
@incoming:IncomingContext -> TraceState
The state received with it: empty when the message had none or when it was discarded.
def IncomingContext.received source · line 3110 · raw
@incoming:IncomingContext -> Maybe<&2, ReceivedPair>
The received pair, when the whole pair was accepted: None{} when the tracestate was discarded, and for a context built from parts.
def IncomingContext.parent source · line 3116 · raw
@incoming:IncomingContext -> Parent
The received context as the parent of a child operation.
def IncomingContext.from_remote source · line 3125 · raw
@context:RemoteContext -> @state:TraceState -> IncomingContext
An incoming context from its parts: a remote context and the tracestate that goes with it, so that an OpenTelemetry SDK's remote span contexts have one shape whatever format they came from. No message's fields were accepted, so it keeps no received pair, and Context.forward refuses it with NothingToForward (laws incoming_from_remote and forward_from_parts). A child continues it as any incoming context.
def ReceivedPair.traceparent source · line 3129 · raw
@pair:ReceivedPair -> String
The received traceparent value, without the whitespace around it.
def ReceivedPair.tracestate source · line 3135 · raw
@pair:ReceivedPair -> List<&2, String>
The received tracestate field values, in arrival order.
def BaseContext.parent source · line 3142 · raw
@base:BaseContext -> Parent
The base as the parent of a child operation: a received context or an operation of this participant.
def BaseContext.state source · line 3151 · raw
@base:BaseContext -> TraceState
The state that goes with the base: the state received with an incoming context, or the state an outgoing context sends.
def TraceParentError.show source · line 3159 · raw
@error:TraceParentError -> String
The name of a traceparent error; InvalidTraceParent adds the codec's error.
def TraceParentOutcome.show source · line 3169 · raw
@outcome:TraceParentOutcome -> String
The name of a traceparent outcome; a rejection adds its error.
def StateOutcome.show source · line 3179 · raw
@outcome:StateOutcome -> String
The name of a tracestate outcome; a discard adds its error.
def Extraction.show source · line 3193 · raw
@extraction:Extraction -> String
Both outcomes of an extraction, for a log line: "TraceParentAccepted, StateDiscarded InvalidEntry 1 MissingEquals" for example. No received value is included, so the line can be logged as it is.
def Carrier.is_context source · line 3217 · raw
@+name:String -> Bool
Whether a field name is traceparent or tracestate, without regard to ASCII case.
def Carrier.replace source · line 3241 · raw
@carrier:List<&2, Header> -> @fields:List<&2, Header> -> List<&2, Header>
The carrier's unrelated fields, followed by fields: reversing the loop's
result onto fields, also a loop, puts them back in order.
def Context.field_names source · line 3250 · raw
List<&2, String>
The names of the context fields as injection writes them: traceparent, then tracestate, in lowercase (W3C 3.2.1 and 3.3.1), the names that extraction and cleanup read too. A propagator lists them as the fields it writes, and one that writes the values of OutgoingContext.emit through a setter of its own writes them under these names, the tracestate field only when its value is not empty, as injection does. Law: inject_names.
def Carrier.context_fields source · line 3255 · raw
@traceparent:String -> @+tracestate:String -> List<&2, Header>
The context fields of a traceparent value and a tracestate value, with lowercase names; the tracestate field is left out when its value is empty.
def Context.clear source · line 3263 · raw
@carrier:List<&2, Header> -> List<&2, Header>
Remove every traceparent and tracestate field, whatever the case of its name, and keep the other fields in their order: the carrier of a message sent without context (spec #1, "Provide explicit context-field cleanup for the no-context path"). Law: clear_carrier.
def Injection.of source · line 3267 · raw
@carrier:List<&2, Header> -> @emission:Emission -> Injection
The injection of an emission into a carrier.
def Context.inject source · line 3281 · raw
@limits:Limits -> @outgoing:OutgoingContext -> @carrier:List<&2, Header> -> Injection
Write an outgoing context into a carrier as a participant: the context
fields of the carrier are replaced by the emitted traceparent, version 00
with only the sampled and random-trace-id flags, and the emitted
tracestate, truncated to the output budget of limits and left out when
empty. The other fields keep their order, and injecting the same context
into the carrier written gives that carrier again. A receiver that extracts
the carrier with the same limits continues the injected operation with the
truncated state. Laws: inject_carrier, inject_dropped, inject_idempotent and
inject_extracted.
def Injection.carrier source · line 3285 · raw
@injection:Injection -> List<&2, Header>
The carrier to send.
def Injection.dropped source · line 3292 · raw
@injection:Injection -> List<&2, StateKey>
The keys of the entries truncation dropped, in their original order; none when the state fitted.
def Text.joined.go source · line 3332 · raw
@fields:List<&2, String> -> @done:String -> String
The fields joined by commas, most recent character first, after done:
each field is reversed onto the comma before it. This is a loop.
def Text.joined source · line 3342 · raw
@fields:List<&2, String> -> String
The fields joined by commas into one value, as String.join(fields, ",") writes it. It is built by loops, so fields of any length need no deep stack.
def Forward.carrier source · line 3352 · raw
@carrier:List<&2, Header> -> @traceparent:String -> @tracestate:List<&2, String> -> List<&2, Header>
The carrier with its context fields replaced by a received pair: the traceparent value, and the tracestate fields joined into one value, left out when empty.
def Forward.state source · line 3356 · raw
@parsed:Result<&2, &2, StateError, TraceState> -> @carrier:List<&2, Header> -> @traceparent:String -> @tracestate:List<&2, String> -> Result<&2, &2, ForwardError, List<&2, Header>>
The last check of a forwarded pair: its tracestate fields parse.
def Forward.parent source · line 3365 · raw
@read:Result<&2, &2, TraceParentError, TraceParentV00> -> @+limits:Limits -> @carrier:List<&2, Header> -> @traceparent:String -> @+tracestate:List<&2, String> -> Result<&2, &2, ForwardError, List<&2, Header>>
The second check of a forwarded pair: its traceparent value reads back.
def Forward.fits source · line 3375 · raw
@fits:Maybe<&2, Nat> -> @+limits:Limits -> @carrier:List<&2, Header> -> @+traceparent:String -> @+tracestate:List<&2, String> -> Result<&2, &2, ForwardError, List<&2, Header>>
The first check of a forwarded pair: its tracestate fields, joined by commas, fit the output budget. Measuring stops past the budget.
def Forward.pair source · line 3384 · raw
@+limits:Limits -> @received:Maybe<&2, ReceivedPair> -> @carrier:List<&2, Header> -> Result<&2, &2, ForwardError, List<&2, Header>>
Forward the received pair, if there is one.
def Context.forward source · line 3406 · raw
@+limits:Limits -> @incoming:IncomingContext -> @carrier:List<&2, Header> -> Result<&2, &2, ForwardError, List<&2, Header>>
Forward a received context unchanged into a carrier: its context fields are
replaced by the traceparent value of the received pair and by its
tracestate fields joined into one field, and the other fields keep their
order. The pair must be there, its tracestate must fit the output budget of
limits whole, and both fields must read back under limits; otherwise
forwarding fails with a ForwardError and writes nothing, so a received
traceparent never travels with an edited or truncated tracestate (W3C 3.4).
The pair of a context that extraction accepted is refused only when its
tracestate exceeds the output budget, a context built from parts has no
pair to forward, and forwarding again into the carrier written gives that
carrier again.
Laws: forward_carrier, forward_nothing, forward_from_parts,
forward_too_large, forward_extracted and forward_idempotent.
def ForwardError.show source · line 3411 · raw
@error:ForwardError -> String
The name of a forwarding error; an invalid field adds its error.
def FailurePolicy.result source · line 3475 · raw
@policy:FailurePolicy -> @A:Data -> Data
The type an operation returns under policy: the value itself with
Lenient{}, and the value or the GenerationError with Strict{}.
def Policy.apply source · line 3484 · raw
@policy:FailurePolicy -> @-A:Data -> @strict:(@_:A -> Result<&2, &2, GenerationError, A>) -> @value:A -> FailurePolicy.result(policy, A)
A value under policy: itself with Lenient{}, and what strict makes of it
with Strict{}.
def Policy.apply.done source · line 3493 · raw
@-S:Type -> @policy:FailurePolicy -> @-A:Data -> @strict:(@_:A -> Result<&2, &2, GenerationError, A>) -> @done:Pair(S, A) -> Pair(S, FailurePolicy.result(policy, A))
The source's final state with a value under policy.
def Serve.new_trace_sampled source · line 3505 · raw
@sampling:Sampling -> Bool
The sampled indication of the new trace, a root or a restart, that
Context.continue_or_start_with starts: the one that sampling resolves
from the default, not sampled (spec #1, "New roots default to sampled
0"). InheritSampled{} has nothing to inherit, and SetSampled{} sets its
own. The default lives here: root and restart generation take the
indication that they are given (spec #41, "Sampling decision when starting
a trace").
def Serve.from_child source · line 3510 · raw
@state:TraceState -> @received:Maybe<&2, IncomingContext> -> @result:Result<&2, &2, GenerationError, LocalContext> -> Service
The service that a child of the kept context gives, with state, or
Untraced with the error.
def Serve.from_start source · line 3521 · raw
@origin:Origin -> @result:Result<&2, &2, GenerationError, LocalContext> -> Service
The service that a new trace gives: its generated operation, whose sampled indication Serve.new_trace_sampled gave its generation, and no state, or Untraced with the error. A new trace keeps no received pair.
def Serve.replaced source · line 3547 · raw
@base:BaseContext -> RemoteContext
The context that a restart replaces, as Generation.restart takes it: an incoming base's received context, or an outgoing base's operation as another participant receives it. The new trace ID reuses neither.
def Serve.usable source · line 3556 · raw
@+base:BaseContext -> @received:Maybe<&2, IncomingContext> -> @reception:Reception -> @sampling:Sampling -> ServicePlan
Continue the kept context with a child, with its parent and state, or
replace it with a new trace, as reception says.
def Serve.kept source · line 3565 · raw
@context:Maybe<&2, BaseContext> -> @received:Maybe<&2, IncomingContext> -> @reception:Reception -> @sampling:Sampling -> ServicePlan
Take the context that extraction keeps, or start a root without one.
def ServicePlan.new source · line 3574 · raw
@+extraction:Extraction -> @reception:Reception -> @sampling:Sampling -> ServicePlan
The plan of the service's operation for a message (see ServicePlan).
def ServicePlan.generation source · line 3578 · raw
@plan:ServicePlan -> Generation
The generation that the plan drives.
def ServicePlan.service source · line 3587 · raw
@plan:ServicePlan -> @result:Result<&2, &2, GenerationError, LocalContext> -> Service
The service that the result of the plan's generation gives, before the policy applies: its operation, or Untraced with the error.
def Serve.finish source · line 3595 · raw
@-S:Type -> @plan:ServicePlan -> @done:Pair(S, Result<&2, &2, GenerationError, LocalContext>) -> Pair(S, Service)
The source's final state with the service that the plan gives.
def Serve.strict source · line 3613 · raw
@service:Service -> Result<&2, &2, GenerationError, Service>
A service without an operation as the GenerationError that caused it.
def Send.forwarded source · line 3669 · raw
@result:Result<&2, &2, ForwardError, List<&2, Header>> -> @error:GenerationError -> @carrier:List<&2, Header> -> Sent
The fallback when a forwarding of the received pair was tried.
def Send.fallback source · line 3680 · raw
@+limits:Limits -> @received:Maybe<&2, IncomingContext> -> @error:GenerationError -> @+carrier:List<&2, Header> -> Sent
The fields a message carries when no operation could be generated: the received pair forwarded unchanged if it can be, and no context fields otherwise.
def Send.of source · line 3690 · raw
@+limits:Limits -> @+outgoing:OutgoingContext -> @received:Maybe<&2, IncomingContext> -> @+carrier:List<&2, Header> -> @result:Result<&2, &2, GenerationError, LocalContext> -> Sent
The message that a generated child gives: the child injected with the service's state, or the fallback.
def SendPlan.new source · line 3715 · raw
@limits:Limits -> @service:Service -> @sampling:Sampling -> @carrier:List<&2, Header> -> SendPlan
The plan of one message that the service sends (see SendPlan).
def SendPlan.generation source · line 3726 · raw
@plan:SendPlan -> Generation
The generation that the plan drives. A service without an operation has none to drive: its generation has already failed with the service's error, so that a host reads no word.
def SendPlan.sent source · line 3736 · raw
@plan:SendPlan -> @result:Result<&2, &2, GenerationError, LocalContext> -> Sent
The message that the result of the plan's generation gives, before the policy applies. The fallback of a service without an operation does not depend on it.
def Send.finish source · line 3744 · raw
@-S:Type -> @plan:SendPlan -> @done:Pair(S, Result<&2, &2, GenerationError, LocalContext>) -> Pair(S, Sent)
The source's final state with the message that the plan gives.
def Send.strict source · line 3756 · raw
@sent:Sent -> Result<&2, &2, GenerationError, Sent>
A message without a new operation as the GenerationError that caused it.
def Origin.show source · line 3777 · raw
@origin:Origin -> String
The name of an origin.
def Service.origin source · line 3787 · raw
@service:Service -> Maybe<&2, Origin>
How the service's operation came about; None{} without an operation.
def Service.outgoing source · line 3795 · raw
@service:Service -> Maybe<&2, OutgoingContext>
The service's operation with the state it sends; None{} without one.
def Service.error source · line 3803 · raw
@service:Service -> Maybe<&2, GenerationError>
Why the service has no operation; None{} with one.
def Service.set source · line 3813 · raw
@service:Service -> @key:StateKey -> @value:StateValue -> Service
Add or update an entry of the state that the service's operation sends, such as this participant's own (see OutgoingContext.set). A service without an operation is unchanged: it sends no state of its own.
def Service.remove source · line 3822 · raw
@service:Service -> @key:StateKey -> Service
Delete an entry of the state that the service's operation sends (see OutgoingContext.remove). A service without an operation is unchanged.
def Service.show source · line 3831 · raw
@service:Service -> String
The name of a service's origin, or Untraced with its error. It includes no received value.
def Unforwarded.show source · line 3839 · raw
@reason:Unforwarded -> String
Why no pair was forwarded: NothingKept, or the ForwardError's name.
def Sent.carrier source · line 3847 · raw
@sent:Sent -> List<&2, Header>
The fields to send with the message, in every case.
def Sent.operation source · line 3857 · raw
@sent:Sent -> Maybe<&2, LocalContext>
The new operation that the message carries; None{} for a fallback.
def Sent.error source · line 3867 · raw
@sent:Sent -> Maybe<&2, GenerationError>
Why no operation could be generated; None{} for a new operation.
def Sent.dropped source · line 3879 · raw
@sent:Sent -> List<&2, StateKey>
The keys that truncating the service's state to the output budget dropped from a new operation's message (see Injection.dropped); none for a fallback, which sends no state of its own.
def Send.fresh source · line 3890 · raw
@dropped:List<&2, StateKey> -> String
The name of a new operation's message, saying whether its state was truncated.
def Sent.show source · line 3900 · raw
@sent:Sent -> String
The name of a message's context: Fresh, saying whether its state was truncated, or for a fallback why no operation was generated and, without a forwarded pair, why none was forwarded. It includes no received value.
Templates
template Drive.fed source · line 961 · raw
@-T:Data -> @-D:Data -> @-waiting:(@_:T -> Maybe<&2, D>) -> @-feed:(@_:Result<&1, &1, Pair(U32, String), U32> -> @_:D -> T) -> @-S:Type -> @got:Pair(S, Result<&1, &1, Pair(U32, String), U32>) -> @draw:D -> Pair(S, Pair(T, Maybe<&2, D>))
The driver of the three machines: a trace ID draw, a span ID draw and a
generation. It feeds a machine one source word at a time while the
machine's step waits for one, and stops as soon as it has ended. Each
machine gives, as templates, waiting, the draw that a step feeds its next
word to, if it waits for one, and feed, the step after that word. The
driver keeps each step beside what waiting says of it.
Feed a word that a source returned, keeping the source's next state.
template Drive.run source · line 970 · raw
@-T:Data -> @-D:Data -> @-waiting:(@_:T -> Maybe<&2, D>) -> @-feed:(@_:Result<&1, &1, Pair(U32, String), U32> -> @_:D -> T) -> @fuel:Nat -> @current:Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, Pair(T, Maybe<&2, D>)) -> Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, T)
Drive a machine from a tape, stopping as soon as its step has ended; unread
words stay on the tape. fuel bounds the steps, which Bend requires for
termination; the laws show the budgets suffice.
template Drive.read source · line 988 · raw
@-T:Data -> @-D:Data -> @-waiting:(@_:T -> Maybe<&2, D>) -> @-feed:(@_:Result<&1, &1, Pair(U32, String), U32> -> @_:D -> T) -> @-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @fuel:Nat -> @current:Pair(S, Pair(T, Maybe<&2, D>)) -> IO(Pair(S, T))
Drive a machine from any source, one word at a time. read returns the
source's next state with each word, and the driver stops as soon as the
machine's step has ended; the final source state is handed back, so a
caller can see what was read. fuel bounds the words read, as in
Drive.run. Templates keep this driver free of any host effect: the effect,
if any, lives in the source.
template Drive.ended source · line 1001 · raw
@-T:Data -> @-D:Data -> @-waiting:(@_:T -> Maybe<&2, D>) -> @result:Pair(List<&1, Result<&1, &1, Pair(U32, String), U32>>, T) -> Bool
Whether the machine in a driver's result has ended.
template Drive.outcome source · line 1009 · raw
@-T:Data -> @-A:Data -> @-result:(@_:T -> Result<&2, &2, GenerationError, A>) -> @-S:Type -> @done:Pair(S, T) -> Pair(S, Result<&2, &2, GenerationError, A>)
The source's final state with the result that result gives of the
machine's final step.
template Drive.finished source · line 1015 · raw
@-T:Data -> @-A:Data -> @-result:(@_:T -> Result<&2, &2, GenerationError, A>) -> @-S:Type -> @action:IO(Pair(S, T)) -> IO(Pair(S, Result<&2, &2, GenerationError, A>))
Turn the IO driver's final step into its result.
template TraceId.generate_with source · line 1136 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @excluded:Maybe<&2, TraceId> -> IO(Pair(S, Result<&2, &2, GenerationError, TraceId>))
A trace ID alone, from a caller's source, as an OpenTelemetry SDK generates
one before its sampler decides on it. read returns the source's next state
with each word result, and the source's final state is returned. It reads
four words per candidate, most significant first, for at most eight
candidates, so at most 32 words; rejects all-zero candidates and excluded,
when there is one; and fails with SourceFailure or ExhaustedTraceId. The
source is trusted to be random: the trace ID asserts random-trace-id.
Laws: trace_id_tape, trace_id_failure, trace_id_candidate, trace_id_ends,
trace_id_exhaustion and generated_trace_id.
template SpanId.generate_with source · line 1253 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @excluded:Maybe<&2, SpanId> -> IO(Pair(S, Result<&2, &2, GenerationError, SpanId>))
A span ID alone, from a caller's source, as an OpenTelemetry SDK generates
one once its sampler has decided. The source's shape is that of
TraceId.generate_with. It reads two words per candidate, most significant
first, for at most eight candidates, so at most 16 words; rejects all-zero
candidates and excluded, when there is one, such as the span ID of a
child's parent; and fails with SourceFailure or ExhaustedSpanId.
Laws: span_id_tape, span_id_failure, span_id_candidate, span_id_ends,
span_id_exhaustion and generated_span_id.
template Draw.read source · line 1379 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @fuel:Nat -> @current:Pair(S, Step) -> IO(Pair(S, Step))
Drive a generation from any source (Drive.read).
template Draw.finished source · line 1394 · raw
@-S:Type -> @action:IO(Pair(S, Step)) -> IO(Pair(S, Result<&2, &2, GenerationError, LocalContext>))
Turn the driver's final step into the generation's result.
template Generation.run_with source · line 1466 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @generation:Generation -> IO(Pair(S, Result<&2, &2, GenerationError, LocalContext>))
Drive a generation from a caller's source, one word at a time (Draw.read), and hand back the source's final state with the result.
template SpanPlan.generate_with source · line 1486 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @plan:SpanPlan -> IO(Pair(S, Result<&2, &2, GenerationError, LocalContext>))
The local context of a span plan, from a caller's source: a span ID that excludes the plan's (SpanId.generate_with), and the context of the plan's trace ID and sampled indication with it.
template Draw.root_span_with source · line 1499 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @sampled:Bool -> @outcome:Pair(S, Result<&2, &2, GenerationError, TraceId>) -> IO(Pair(S, Result<&2, &2, GenerationError, LocalContext>))
The span ID of a root or a restart with the sampled indication sampled,
from the source's next state, once its trace ID is generated: the trace
ID's failure is the generation's, and otherwise the local context of the
root's span plan (SpanPlan.root).
template TracePlan.generate_with source · line 1511 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @plan:TracePlan -> IO(Pair(S, Result<&2, &2, GenerationError, LocalContext>))
The local context of the new trace of a plan, from a caller's source: a trace ID that excludes the plan's (TraceId.generate_with), then, from the source's next state, the span ID of the root's span plan with the plan's sampled indication (Draw.root_span_with).
template Context.root_with source · line 1528 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @sampled:Bool -> IO(Pair(S, Result<&2, &2, GenerationError, LocalContext>))
Generated contexts from a caller's source. read returns the source's next
state with each word result. The source is trusted to be random: a generated
trace ID asserts random-trace-id. A root is a trace ID, with none to
exclude, then a span ID: TraceId.generate_with, then SpanId.generate_with
from the source's next state (TracePlan.root and TracePlan.generate_with).
It reads at most 48 words and has the sampled indication sampled, as it
is given: no default applies here, and False gives an unsampled root,
emitted with flags 02, as Context.continue_or_start_with starts one by
default (spec #41, "Sampling decision when starting a trace"). Laws:
root_composed, root_tape, root_ends, root_exhaustion and generated_root.
template Context.child_with source · line 1537 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @parent:Parent -> @sampling:Sampling -> IO(Pair(S, Result<&2, &2, GenerationError, LocalContext>))
A generated child of parent from a caller's source: the local context of
its span plan (SpanPlan.child), a span ID that excludes the parent's, with
the parent's trace ID and the sampled indication that sampling resolves.
It reads at most 16 words. Laws: child_composed, child_tape, child_ends,
child_exhaustion and generated_child.
template Context.restart_with source · line 1546 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @previous:RemoteContext -> @sampled:Bool -> IO(Pair(S, Result<&2, &2, GenerationError, LocalContext>))
A generated restart replacing previous from a caller's source: a trace ID
that excludes the received one, then a span ID, as for a root, with the
sampled indication sampled (TracePlan.restart and
TracePlan.generate_with). It reads at most 48 words. Laws:
restart_composed, restart_tape, restart_ends and generated_restart.
template Serve.run source · line 3601 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @+plan:ServicePlan -> IO(Pair(S, Service))
Drive the plan's generation from a caller's source.
template Serve.operation source · line 3608 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @+extraction:Extraction -> @reception:Reception -> @sampling:Sampling -> IO(Pair(S, Service))
The service for a message, before the policy applies.
template Context.continue_or_start_with source · line 3623 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @+extraction:Extraction -> @reception:Reception -> @sampling:Sampling -> @+policy:FailurePolicy -> IO(Pair(S, FailurePolicy.result(policy, Service)))
Give a service its own operation for a received message, from a caller's source (see the section's introduction). Laws: continue_usable, restart_usable, start_unusable and restart_keeps_nothing.
template Send.run source · line 3749 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @+plan:SendPlan -> IO(Pair(S, Sent))
Drive the plan's generation from a caller's source.
template Context.send_with source · line 3769 · raw
@-S:Type -> @-read:(@_:S -> IO(Pair(S, Result<&1, &1, Pair(U32, String), U32>))) -> @source:S -> @+limits:Limits -> @service:Service -> @sampling:Sampling -> @+policy:FailurePolicy -> @+carrier:List<&2, Header> -> IO(Pair(S, FailurePolicy.result(policy, Sent)))
Give one message that the service sends the context of a new operation,
from a caller's source (see the section's introduction). carrier is the
message's own fields; its old context fields are replaced in every case.
Laws: send_operating, send_untraced and send_reports_generated.