bend-trace-context Releases (3): 0.2.0.0 0x665ae73e3f32ce98f72c7cf6844cfd3f indexed https://jend.leeeet.dev/files.txt?path=bend-trace-context@0.2.0.0 0.1.2.0 0x67c024a0cb5f9d3903b7fec903b53e68 unindexed https://jend.leeeet.dev/files.txt?path=bend-trace-context@0.1.2.0 0.1.0.0 0xb6eebf6253ee268a21f3e308b12cacba unindexed https://jend.leeeet.dev/files.txt?path=bend-trace-context@0.1.0.0 Definitions (472, 1 to 100 shown): Entropy.read_u32 (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/entropy.bend&name=read_u32) # One word from the host's cryptographic source: WebCrypto in JavaScript and # the operating system's generator natively. Fail code 1 means unavailable and # code 2 means source-failure in JavaScript; natively the code is the host # errno with its strerror text. The pure codec never calls it implicitly. def read_u32() -> IO(Result<&1, &1, U32 & String, U32>): Generation.Source.host (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=Source.host) # The host source as the machine reads it: each read returns one word result # from Entropy.read_u32, and the state is Unit because the host keeps none. def Source.host(state: Unit) -> IO(Unit & Result<&1, &1, U32 & String, U32>): Generation.on_host (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=on_host) # The host source has no state to hand back. def on_host(-A: Type, action: IO(Unit & A)) -> IO(A): Generation.TraceId.generate (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=TraceId.generate) # A trace ID alone, as an OpenTelemetry SDK generates one before its sampler # decides on it (TC.TraceId.generate_with). It asserts random-trace-id and is # never `excluded`, when there is one. def TraceId.generate(excluded: Maybe<&2, TC.TraceId>) -> IO(Result<&2, &2, TC.GenerationError, TC.TraceId>): Generation.SpanId.generate (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=SpanId.generate) # A span ID alone, as an SDK generates one once its sampler has decided, or # for a child span with its parent's span ID excluded # (TC.SpanId.generate_with). def SpanId.generate(excluded: Maybe<&2, TC.SpanId>) -> IO(Result<&2, &2, TC.GenerationError, TC.SpanId>): Generation.Context.root (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=Context.root) # Start a trace: a trace ID, then a span ID, as TC.Context.root_with composes # them, with the sampled indication `sampled`, as it is given. The trace ID # asserts random-trace-id, so the root is emitted with flags 03 when it is # sampled and 02 when it is not: False gives an unsampled root, as # Context.continue_or_start starts one by default. def Context.root(sampled: Bool) -> IO(Result<&2, &2, TC.GenerationError, TC.LocalContext>): Generation.Context.child (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=Context.child) # Continue a remote or local parent with a new operation. def Context.child(parent: TC.Parent, sampling: TC.Sampling) -> IO(Result<&2, &2, TC.GenerationError, TC.LocalContext>): Generation.Context.restart (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=Context.restart) # Start a new trace instead of continuing a received context, with the # sampled indication `sampled`, as a root takes it. def Context.restart(previous: TC.RemoteContext, sampled: Bool) -> IO(Result<&2, &2, TC.GenerationError, TC.LocalContext>): Generation.Context.continue_or_start (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=Context.continue_or_start) # Give a service its own operation for a received message: a child of the # context that extraction keeps, the message's or the base, a root without # one, or a new trace in its place at a trust boundary # (TC.Context.continue_or_start_with). def Context.continue_or_start(+extraction: TC.Extraction, reception: TC.Reception, sampling: TC.Sampling, +policy: TC.FailurePolicy) -> IO(TC.FailurePolicy.result(policy, TC.Service)): Generation.Context.send (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=Context.send) # Give one message that the service sends a new child of the service's # operation, or the fallback when none can be generated # (TC.Context.send_with). def Context.send(+limits: TC.Limits, service: TC.Service, sampling: TC.Sampling, +policy: TC.FailurePolicy, +carrier: List<&2, TC.Header>) -> IO(TC.FailurePolicy.result(policy, TC.Sent)): Generation.NativeHttp.continue_or_start (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=NativeHttp.continue_or_start) # The service's own operation for a received request, from the header map of # the request, on the host's cryptographic source: native_http.bend's # continue_or_start_with on Source.host. `base` is the context to keep when # the request carries no usable traceparent. def NativeHttp.continue_or_start(+limits: TC.Limits, headers: Adapter.HeaderMap(), base: Maybe<&2, TC.BaseContext>, reception: TC.Reception, sampling: TC.Sampling, +policy: TC.FailurePolicy) -> IO(TC.FailurePolicy.result(policy, TC.Service)): Generation.NativeHttp.send (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/generation.bend&name=NativeHttp.send) # Give one request that the service sends the context of a new operation, on # the host's cryptographic source: native_http.bend's send_with on # Source.host, which replaces the context fields of `headers`, the request's # own header map. def NativeHttp.send(+limits: TC.Limits, service: TC.Service, sampling: TC.Sampling, +policy: TC.FailurePolicy, headers: Adapter.HeaderMap()) -> IO(TC.FailurePolicy.result(policy, Adapter.Outbound)): NativeHttp.HeaderMap (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=HeaderMap) # The header fields of a bend-kit request or response: each name, as bend-kit # stores it, with its values in arrival order. def HeaderMap() -> Data: NativeHttp.Outbound (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Outbound) # A request to send: the context fields the package gave it (`sent`), and # the header map to send it with, which holds those fields. type Outbound is Data: Outbound{sent: TC.Sent, headers: Map<&2, List<&2, String>>} NativeHttp.Headers.push (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Headers.push) # One field for each value of `name`, pushed onto `fields` in order, so that # the last value ends up first. A loop: a received head of 64 KiB can hold # thousands of values. def Headers.push(+name: String, values: List<&2, String>, fields: List<&2, TC.Header>) -> List<&2, TC.Header>: NativeHttp.Headers.gather (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Headers.gather) # The fields of every entry pushed onto `fields`, entry by entry. def Headers.gather(entries: List<&2, Sigma<&2, &2, String, _ => List<&2, String>>>, fields: List<&2, TC.Header>) -> List<&2, TC.Header>: NativeHttp.carrier (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=carrier) # The header fields of a map as a carrier for TC.Context.extract or # TC.Context.send: every value of every name, in arrival order within each # name (law http_carrier). The order between different names is the map's # own, which no Trace Context rule depends on. def carrier(headers: HeaderMap()) -> List<&2, TC.Header>: NativeHttp.Headers.values (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Headers.values) # The values a map holds under `name`, none when it has no entry for it. def Headers.values(+headers: HeaderMap(), name: String) -> List<&2, String>: NativeHttp.Headers.add (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Headers.add) # Put one field's value first among its name's values. def Headers.add(+headers: HeaderMap(), header: TC.Header) -> HeaderMap(): NativeHttp.Headers.write (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Headers.write) # Put every field of `fields` first among its name's values, in order. A # loop, as Headers.push is. def Headers.write(fields: List<&2, TC.Header>, +headers: HeaderMap()) -> HeaderMap(): NativeHttp.headers (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=headers) # The header map of a carrier, such as the one TC.Sent.carrier gives for a # message to send: under each name, the carrier's values of that name in # order (law http_headers), as bend-kit's Http.add would add them one by one, # with the names as the carrier spells them. The fields are put in from the # last, each value first among its name's, which leaves every name's values # in order. bend-kit writes one header line for each value. def headers(carrier: List<&2, TC.Header>) -> HeaderMap(): NativeHttp.continue_or_start_with (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=continue_or_start_with) # The service's own operation for a received message, from the header map of # its request, on a caller's source: TC.Context.continue_or_start_with over # the extraction of the map's carrier (law http_continue). `base` is the # context to keep when the request carries no usable traceparent. def continue_or_start_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, +limits: TC.Limits, headers: HeaderMap(), base: Maybe<&2, TC.BaseContext>, reception: TC.Reception, sampling: TC.Sampling, +policy: TC.FailurePolicy) -> IO(S & TC.FailurePolicy.result(policy, TC.Service)): NativeHttp.Headers.outbound (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Headers.outbound) # The request to send for a message: the message with the map of the fields # that TC.Sent.carrier gives. def Headers.outbound(+sent: TC.Sent) -> Outbound: NativeHttp.Headers.strict (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Headers.strict) # The same for a strict result: a failure stays a failure. def Headers.strict(result: Result<&2, &2, TC.GenerationError, TC.Sent>) -> Result<&2, &2, TC.GenerationError, Outbound>: NativeHttp.Headers.written (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Headers.written) # A message sent under `policy`, with its header map. def Headers.written(policy: TC.FailurePolicy, result: TC.FailurePolicy.result(policy, TC.Sent)) -> TC.FailurePolicy.result(policy, Outbound): NativeHttp.Headers.written.done (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Headers.written.done) # The source's final state with a message sent under `policy` and its map. def Headers.written.done(-S: Type, +policy: TC.FailurePolicy, done: S & TC.FailurePolicy.result(policy, TC.Sent)) -> S & TC.FailurePolicy.result(policy, Outbound): NativeHttp.send_with (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=send_with) # Give one request that the service sends the context of a new operation, on # a caller's source: TC.Context.send_with on the carrier of `headers`, the # request's own header map, and the map of the fields it gives back (law # http_send). The request's old context fields go, whatever the case of # their names, and the new ones replace them; without a new operation, the # map forwards the received pair or carries no context fields. def send_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, +limits: TC.Limits, service: TC.Service, sampling: TC.Sampling, +policy: TC.FailurePolicy, headers: HeaderMap()) -> IO(S & TC.FailurePolicy.result(policy, Outbound)): NativeHttp.Outbound.sent (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Outbound.sent) # The context fields that the package gave the request. def Outbound.sent(outbound: Outbound) -> TC.Sent: NativeHttp.Outbound.headers (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/native_http.bend&name=Outbound.headers) # The header map to send the request with. def Outbound.headers(outbound: Outbound) -> HeaderMap(): Digits.Digits.Nil (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.Nil) # The length is part of the type. A Digits(32n) cannot contain 31 or 33 digits. # This is the same type-family pattern that Base uses for Word(n). # # The empty sequence: the only value of Digits(0n). type Digits.Nil is Data: DNil{} Digits.Digits.Con (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.Con) # A first digit followed by a sequence of p digits: a value of Digits(1n+p). type Digits.Con<-p: Nat> is Data: DCon{head: Hex.Digit, tail: Digits(p)} Digits.Digits (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits) # The type of sequences of exactly n digits, computed from n: Digits(0n) is # Digits.Nil and Digits(1n+p) is Digits.Con

. def Digits(n: Nat) -> Data: Digits.Digits.to_string (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.to_string) # The n lowercase characters of the digits, in order. def Digits.to_string(n: Nat, digits: Digits(n)) -> String: Digits.Digits.is_zero (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.is_zero) # Whether every digit is 0. The empty sequence counts as zero. def Digits.is_zero(n: Nat, digits: Digits(n)) -> Bool: Digits.Digits.of_u32 (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.of_u32) # The eight digits of a word, most significant first: the first digit holds # bits 31 to 28 and the last digit bits 3 to 0. def Digits.of_u32(word: U32) -> Digits(8n): Digits.Digits.to_u32 (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.to_u32) # The word whose eight digits these are, most significant first. def Digits.to_u32(digits: Digits(8n)) -> U32: Digits.Digits.to_byte (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.to_byte) # The byte of two digits, the high digit first: 16 times the high digit plus # the low one, from 0 to 255. Its bits 7 to 4 are the high digit's, bits 3 to # 0 the low digit's, and the other 24 bits are zero. def Digits.to_byte(digits: Digits(2n)) -> U32: Digits.Digits.of_byte (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.of_byte) # The two digits of a byte, the high digit first: bits 7 to 4, then bits 3 to # 0. The other bits are not read, so the caller first checks that the word is # at most 255. def Digits.of_byte(byte: U32) -> Digits(2n): Digits.Digits.to_bytes (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.to_bytes) # The n bytes of 2n digits, most significant first: each byte takes the next # two digits, the first of them high. def Digits.to_bytes(n: Nat, digits: Digits(Nat.double(n))) -> List<&2, U32>: Digits.Digits.append (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.append) # The digits of `left` followed by those of `right`: m + n digits. Identifiers # are built from source words this way, eight digits per word. def Digits.append(m: Nat, -n: Nat, left: Digits(m), right: Digits(n)) -> Digits(Nat.add(m, n)): Digits.NonZero (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=NonZero) # n digits that are not all zero. `evidence` is the proof. The equality is # checked statically; compiled evidence is a null placeholder. Keeping its # binder usable lets later proofs recover and reuse this guarantee. Even direct # construction must supply a proof that these digits are not zero. type NonZero<-n: Nat> is Data: NonZero{digits: Digits(n), evidence: {Digits.is_zero(n, digits) == False{} : Bool}} Digits.NonZero.new.checked (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=NonZero.new.checked) # Carry the equation into the branch: matching status refines its right side. # The value is built only in the False case, where the equation is the proof. def NonZero.new.checked(-n: Nat, digits: Digits(n), status: Bool, evidence: {Digits.is_zero(n, digits) == status : Bool}) -> Maybe<&2, NonZero>: Digits.NonZero.new (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=NonZero.new) # Attach the proof that the digits are not all zero, or None when they are. def NonZero.new(+n: Nat, +digits: Digits(n)) -> Maybe<&2, NonZero>: Digits.NonZero.digits (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=NonZero.digits) # The digits, without their proof. def NonZero.digits(-n: Nat, value: NonZero) -> Digits(n): Digits.NonZero.to_string (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=NonZero.to_string) # The n lowercase characters of the digits. def NonZero.to_string(n: Nat, value: NonZero) -> String: Hex.Digit (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit) # A hexadecimal digit has exactly these sixteen values, H0 to Hf, in value # order. Encoding is lowercase. type Digit is Data: H0{} H1{} H2{} H3{} H4{} H5{} H6{} H7{} … Hex.Digit.to_char (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.to_char) # The lowercase character of a digit: '0' to '9', then 'a' to 'f'. def Digit.to_char(digit: Digit) -> Char: Hex.Digit.to_u32 (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.to_u32) # The value of a digit, 0 to 15. def Digit.to_u32(digit: Digit) -> U32: Hex.Digit.is_zero (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.is_zero) # Whether the digit is 0. An identifier is all zero when every digit is. def Digit.is_zero(digit: Digit) -> Bool: Hex.Digit.is_odd (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.is_odd) # Whether bit 0 (value 1) of the digit is set. In the last digit of the flags # this is the sampled flag (W3C 3.2.2.5.1). def Digit.is_odd(digit: Digit) -> Bool: Hex.Digit.has_bit1 (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.has_bit1) # Whether bit 1 (value 2) of the digit is set. In the last digit of the flags # this is the random-trace-id flag (W3C 3.2.2.5.2). def Digit.has_bit1(digit: Digit) -> Bool: Hex.Digit.has_bit2 (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.has_bit2) # Whether bit 2 (value 4) of the digit is set. def Digit.has_bit2(digit: Digit) -> Bool: Hex.Digit.has_bit3 (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.has_bit3) # Whether bit 3 (value 8) of the digit is set. def Digit.has_bit3(digit: Digit) -> Bool: Hex.Digit.from_bits (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.from_bits) # The digit whose value is bit0 + 2 * bit1 + 4 * bit2 + 8 * bit3. def Digit.from_bits(bit0: Bool, bit1: Bool, bit2: Bool, bit3: Bool) -> Digit: Hex.Digit.all (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.all) # Every digit, in encoding order. def Digit.all() -> List<&2, Digit>: Hex.Digit.from_char.find (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.from_char.find) # Search the encoder's own alphabet, so an accepted character is exactly the # encoding of the digit returned for it. def Digit.from_char.find(digits: List<&2, Digit>, +char: Char) -> Maybe<&2, Digit>: Hex.Digit.from_char (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/hex.bend&name=Digit.from_char) # The digit a character encodes. Uppercase and every non-hexadecimal character # are rejected with None. def Digit.from_char(char: Char) -> Maybe<&2, Digit>: TraceContext.Field (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Field) # The field that a ZeroId error names: the trace ID or parent ID of a # traceparent value, or a supplied span ID. type Field is Data: TraceIdField{} ParentIdField{} SpanIdField{} TraceContext.Error (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Error) # 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 … TraceContext.ContextError (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=ContextError) # 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. type ContextError is Data: ReusedSpanId{} ReusedTraceId{} TraceContext.Parsed (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parsed) # 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. type Parsed<-n: Nat> is Data: Parsed{digits: Digits.Digits(n), rest: String} TraceContext.ParsedBytes (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=ParsedBytes) # 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. type ParsedBytes<-n: Nat> is Data: ParsedBytes{digits: Digits.Digits(Nat.double(n)), rest: List<&2, U32>} TraceContext.TraceParentV00 (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TraceParentV00) # 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. type TraceParentV00 is Data: TraceParentV00{ trace_id: Digits.NonZero<32n>, parent_id: Digits.NonZero<16n>, flags: Digits.Digits(2n) } TraceContext.TraceId (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TraceId) # 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. type TraceId is Data: TraceId{value: Digits.NonZero<32n>, random: Bool} TraceContext.SpanId (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=SpanId) # 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). type SpanId is Data: SpanId{value: Digits.NonZero<16n>} TraceContext.Sampling (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Sampling) # 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. type Sampling is Data: InheritSampled{} SetSampled{sampled: Bool} TraceContext.RemoteContext (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=RemoteContext) # 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. type RemoteContext is Data: RemoteContext{trace_id: TraceId, span_id: SpanId, sampled: Bool} TraceContext.LocalContext (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=LocalContext) # A context that identifies an operation of this participant: the one it sends # in its own headers. The Context.* operations build it. type LocalContext is Data: LocalContext{trace_id: TraceId, span_id: SpanId, sampled: Bool} TraceContext.Parent (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parent) # The context whose trace a child operation continues: a received context or # one of this participant's own operations. type Parent is Data: RemoteParent{context: RemoteContext} LocalParent{context: LocalContext} TraceContext.GenerationError (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=GenerationError) # 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. type GenerationError is Data: SourceFailure{code: U32, message: String} ExhaustedTraceId{} ExhaustedSpanId{} TraceContext.TraceWords (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TraceWords) # The words read so far for the current trace ID candidate, in arrival order. # Four words complete a candidate. type TraceWords is Data: NoTraceWord{} OneTraceWord{first: U32} TwoTraceWords{first: U32, second: U32} ThreeTraceWords{first: U32, second: U32, third: U32} TraceContext.SpanWords (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=SpanWords) # The words read so far for the current span ID candidate. Two words complete # a candidate. type SpanWords is Data: NoSpanWord{} OneSpanWord{first: U32} TraceContext.TraceDraw (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TraceDraw) # 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 … TraceContext.SpanDraw (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=SpanDraw) # 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. type SpanDraw is Data: SpanDraw{remaining: Nat, words: SpanWords, excluded: Maybe<&2, SpanId>} TraceContext.TraceStep (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TraceStep) # 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. type TraceStep is Data: NeedTraceWord{draw: TraceDraw} DrawnTraceId{id: TraceId} TraceFailed{error: GenerationError} TraceContext.SpanStep (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=SpanStep) # 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. type SpanStep is Data: NeedSpanWord{draw: SpanDraw} DrawnSpanId{id: SpanId} SpanFailed{error: GenerationError} TraceContext.SpanPlan (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=SpanPlan) # 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. type SpanPlan is Data: SpanPlan{excluded: Maybe<&2, SpanId>, trace_id: TraceId, sampled: Bool} TraceContext.TracePlan (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TracePlan) # 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. type TracePlan is Data: TracePlan{excluded: Maybe<&2, TraceId>, sampled: Bool} TraceContext.Draw (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Draw) # 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. type Draw is Data: DrawTrace{draw: TraceDraw, sampled: Bool} DrawSpan{draw: SpanDraw, trace_id: TraceId, sampled: Bool} TraceContext.Step (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Step) # The state of a generation after each source word: it needs another word, it # created a context, or it failed. type Step is Data: NeedWord{draw: Draw} Created{context: LocalContext} Failed{error: GenerationError} TraceContext.Generation (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Generation) # 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. type Generation is Data: Generation{fuel: Nat, step: Step} TraceContext.Parsed.prepend (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parsed.prepend) # Put one more digit in front of a parsed sequence: n digits become 1 + n. def Parsed.prepend(-n: Nat, digit: Hex.Digit, parsed: Parsed) -> Parsed<1n+n>: TraceContext.Parse.digit_result (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.digit_result) # A decoded character, or InvalidHex at its offset when it is not a lowercase # hexadecimal digit. def Parse.digit_result(value: Maybe<&2, Hex.Digit>, offset: Nat) -> Result<&2, &2, Error, Hex.Digit>: TraceContext.Parse.digit (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.digit) # Decode one character as a lowercase hexadecimal digit. def Parse.digit(char: Char, offset: Nat) -> Result<&2, &2, Error, Hex.Digit>: TraceContext.Parse.digits (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.digits) # 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.digits(n: Nat, text: String, offset: Nat) -> Result<&2, &2, Error, Parsed>: TraceContext.Parse.separator_result (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.separator_result) # The rest of the text after a "-", or ExpectedSeparator at its offset. def Parse.separator_result(tail: String, ok: Bool, offset: Nat) -> Result<&2, &2, Error, String>: TraceContext.Parse.separator (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.separator) # Read the "-" expected at `offset`. def Parse.separator(text: String, offset: Nat) -> Result<&2, &2, Error, String>: TraceContext.Parse.end (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.end) # 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.end(text: String) -> Result<&2, &2, Error, Unit>: TraceContext.Parse.version (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.version) # 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.version(digits: Digits.Digits(2n)) -> Result<&2, &2, Error, Unit>: TraceContext.Parse.nonzero_result (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.nonzero_result) # Attach the proof that digits are not all zero, or fail with ZeroId naming # the field. def Parse.nonzero_result(-n: Nat, result: Maybe<&2, Digits.NonZero>, field: Field) -> Result<&2, &2, Error, Digits.NonZero>: TraceContext.Parse.nonzero (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.nonzero) # Check that digits are not all zero (W3C 3.2.2.3, 3.2.2.4). def Parse.nonzero(n: Nat, digits: Digits.Digits(n), field: Field) -> Result<&2, &2, Error, Digits.NonZero>: TraceContext.Parse.flags (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.flags) # The last field: the two flag digits, then the end of the text. def Parse.flags(trace_id: Digits.NonZero<32n>, parent_id: Digits.NonZero<16n>, parsed: Parsed<2n>) -> Result<&2, &2, Error, TraceParentV00>: TraceContext.Parse.parent (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.parent) # 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.parent(trace_id: Digits.NonZero<32n>, parsed: Parsed<16n>) -> Result<&2, &2, Error, TraceParentV00>: TraceContext.Parse.trace (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.trace) # 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.trace(parsed: Parsed<32n>) -> Result<&2, &2, Error, TraceParentV00>: TraceContext.Parse.start (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.start) # After the two version digits: the version check, the "-" at offset 2 and the # trace ID from offset 3. def Parse.start(parsed: Parsed<2n>) -> Result<&2, &2, Error, TraceParentV00>: TraceContext.TraceParentV00.parse (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TraceParentV00.parse) # 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.parse(text: String) -> Result<&2, &2, Error, TraceParentV00>: TraceContext.TraceParentV00.format (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TraceParentV00.format) # 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.format(context: TraceParentV00) -> String: TraceContext.TraceParentV00.is_sampled (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TraceParentV00.is_sampled) # Whether the sampled flag, bit 0 of the flag byte, is set (W3C 3.2.2.5.1). def TraceParentV00.is_sampled(context: TraceParentV00) -> Bool: TraceContext.TraceParentV00.is_random (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=TraceParentV00.is_random) # 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 TraceParentV00.is_random(context: TraceParentV00) -> Bool: TraceContext.Parse.id.finish (https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Parse.id.finish) # The digits of a supplied ID must be the whole text, and not all zero. def Parse.id.finish(n: Nat, parsed: Parsed, field: Field) -> Result<&2, &2, Error, Digits.NonZero>: More: https://jend.leeeet.dev/packages/bend-trace-context.txt?definitions_offset=100