trace_context.bend

bend-trace-context@0.2.0.0 · 3,907 lines · 415 definitions

1# bend-trace-context: the pure Trace Context core
2# ===============================================
3#
4# This file is the package's public entry for everything that performs no host
5# effect: the strict traceparent v00 codec, validated trace and span IDs and
6# their bytes, local and remote contexts, the machine that turns source words
7# into IDs, validated limits, the Level 2 tracestate parser, tracestate
8# updates and emission, outgoing contexts, the extraction of a received
9# message's context, the injection and forwarding of a context into an
10# outgoing message's carrier, and the operations that continue or start a
11# service's operation for a received message and give each message it sends a
12# child of it.
13# generation.bend adds the host's cryptographic source on top of it, and
14# native_http.bend the header maps of bend-kit's native HTTP package. The
15# claims this code must satisfy are stated in LAWS.bend and proved in
16# PROOF.bend, beside this file. The tests in tests/*.bend here and the
17# repository's consumer in tests/consumer exercise it through the same public
18# names.
19#
20# The normative reference is W3C Trace Context Level 2, Candidate
21# Recommendation Draft of 2024-03-28 ("W3C" below, with section numbers). The
22# approved specification is issue #1 of the repository ("spec #1"), and issue
23# #41 ("spec #41") adds the building blocks that an OpenTelemetry SDK
24# composes.
25#
26# Contents
27#
28#   Types                            every data type of the codec, contexts and
29#                                    generation, declared first
30#   Strict v00 codec                 Parse.*, TraceParentV00.*
31#   Identifiers and contexts         TraceId, SpanId, contexts and their
32#                                    trace flags, children, restarts
33#   Identifiers from source words    U32.to_hex, TraceId.from_words, ...
34#   Identifiers as bytes             TraceId.to_bytes, TraceId.from_bytes,
35#                                    SpanId.to_bytes, SpanId.from_bytes
36#   Generation machine               Drive.*, TraceDraw.*, SpanDraw.*,
37#                                    SpanPlan.*, TracePlan.*, Step.*, Draw.*,
38#                                    TraceId.generate_with,
39#                                    SpanId.generate_with, Generation.*,
40#                                    Context.*_with, Source.tape
41#   Error messages                   Error.show, ContextError.show, ...
42#   Limits                           Limits.new, Limits.default, accessors
43#   Tracestate                       keys and values, states and lookups,
44#                                    budgets, and the reading machine behind
45#                                    TraceState.parse
46#   Tracestate updates and emission  TraceState.set, remove, size and
47#                                    truncate
48#   Outgoing contexts                OutgoingContext, a local context with the
49#                                    state it sends, and its Emission
50#   Extraction                       Context.extract, TraceParent.read,
51#                                    incoming and base contexts, diagnostics
52#   Injection                        Context.inject and the Injection it
53#                                    writes, Context.field_names,
54#                                    Context.clear
55#   Forwarding                       Context.forward, ForwardError
56#   Continuing or starting           Context.continue_or_start_with,
57#                                    Reception, FailurePolicy, Service,
58#                                    ServicePlan
59#   Sending                          Context.send_with, Sent, SendPlan
60#
61# The public names are documented in packages/trace-context/README.md. Names in
62# the Parse, Parsed, ParsedBytes, Flags, Drive, TraceDraw, SpanDraw,
63# TraceStep, SpanStep, SpanPlan, TracePlan, Draw, Step, Tape, Scan, Member,
64# Value, Budget, Utf8, Entries, StateChar, Carrier, Text, Read, Extract,
65# Forward, Policy, Serve and Send namespaces are internal: Bend lets any module
66# import them, but they are not a compatibility contract.
67#
68# Notes for readers new to Bend
69# -----------------------------
70#
71# - `type T is Data:` declares a type whose values may be copied. Each indented
72#   line is a constructor with its fields, such as `Some{value}`.
73# - A field whose type is an equation, such as
74#   `evidence: {StateKey.is_valid(text) == True{} : Bool}`, stores a proof. A
75#   value can only be built together with that proof, so the rule holds for
76#   every value a program handles, and code that receives one never checks it
77#   again. The checker verifies the proof when the program is compiled. The
78#   `.checked` helpers turn the result of a run-time check into such a proof:
79#   they receive the Bool and an equation stating what it is, and matching on
80#   the Bool refines that equation to `... == True{}` in the accepting case.
81# - `Result<&2, &2, E, T>` is Done{value} or Fail{error}, and `Maybe<&2, T>` is
82#   Some{value} or None{}. The `&2` arguments say that the values may be copied.
83# - A parameter may be used at most once unless it is marked `+x` (reusable).
84#   `-x` is erased: only the checker sees it. `~f` is a template: its argument
85#   is substituted at compile time, so it names top-level definitions only.
86# - `match` may only inspect a parameter or a variable bound by a pattern, never
87#   a computed value, and definitions may not call each other in a cycle. Many
88#   helpers therefore receive a Bool computed by their caller and match on it:
89#   `Scan.read(comma, ...)` receives `Char.is_eq(char, ',')`, for example.
90# - In every recursive call, the first argument that changes must be
91#   structurally smaller, so every function terminates. A recursion whose depth
92#   could grow with received text is written as a tail call, which compiles to
93#   a loop: the JavaScript backend overflows its stack after a few thousand
94#   nested calls, and a received value may be 32 KiB long. The other
95#   recursions are bounded: at most 32 digits, 256 characters of a key or
96#   value, 32 entries, or the characters of a field name sought.
97# - `do Result<...>:` sequences steps that may fail: `x : T <- step` stops at
98#   the first Fail, and the block ends with `return v` or with a last step.
99
100import Base
101import bend-trace-context@0.2.0.0/src/hex.bend as Hex
102import bend-trace-context@0.2.0.0/src/digits.bend as Digits
103
104# Types
105# =====
106#
107# The types of the codec, of the identifiers and contexts, and of the
108# generation machine. The limits, tracestate, outgoing, extraction, injection,
109# forwarding, continue-or-start and sending types are declared in their own
110# sections below.
111
112# The field that a ZeroId error names: the trace ID or parent ID of a
113# traceparent value, or a supplied span ID.
114type Field is Data:
115  TraceIdField{}
116  ParentIdField{}
117  SpanIdField{}
118
119# Why the strict codec, TraceId.parse, SpanId.parse or TraceParent.read
120# refused a text, or TraceId.from_bytes or SpanId.from_bytes a list of bytes.
121# Offsets count Bend characters (Unicode code points) from zero at the start
122# of the text, or cells from zero at the start of the list, and the first
123# problem in reading order is reported.
124#   UnexpectedEnd{offset}        the text ends where a character is required,
125#                                or the list where a byte is
126#   InvalidHex{offset}           this character is not a lowercase hex digit
127#   InvalidByte{offset}          this cell is above 255, so it is not a byte
128#   ExpectedSeparator{offset}    this character should be "-"
129#   TrailingInput{}              characters follow a complete value, or cells
130#                                follow the bytes of an ID
131#   ForbiddenVersion{}           the version is ff, forbidden by W3C 3.2.2.1
132#   UnsupportedVersion{version}  a version other than 00, which the strict
133#                                codec does not read (TraceParent.read reads
134#                                versions 01 to fe by their known prefix)
135#   ZeroId{field}                the named ID is all zero, forbidden by W3C
136#                                3.2.2.3 and 3.2.2.4
137#   ControlCharacter{offset}     this character is a control character other
138#                                than a horizontal tab, which no field value
139#                                may hold (RFC 9110, section 5.5); only
140#                                TraceParent.read reports it, in the fields
141#                                of a later version that it does not read
142type Error is Data:
143  UnexpectedEnd{offset: Nat}
144  InvalidHex{offset: Nat}
145  InvalidByte{offset: Nat}
146  ExpectedSeparator{offset: Nat}
147  TrailingInput{}
148  ForbiddenVersion{}
149  UnsupportedVersion{version: String}
150  ZeroId{field: Field}
151  ControlCharacter{offset: Nat}
152
153# Why creating a context from supplied IDs was refused: a child reused its
154# parent's span ID, or a restart reused the received trace ID.
155type ContextError is Data:
156  ReusedSpanId{}
157  ReusedTraceId{}
158
159# A sequence of n digits read from the front of a text, with the text that
160# remains after it. The length n is part of the type, so a reader of 32 digits
161# can only produce 32.
162type Parsed<-n: Nat> is Data:
163  Parsed{digits: Digits.Digits(n), rest: String}
164
165# The digits of n bytes read from the front of a list of cells, two digits per
166# byte, with the cells that remain after them.
167type ParsedBytes<-n: Nat> is Data:
168  ParsedBytes{digits: Digits.Digits(Nat.double(n)), rest: List<&2, U32>}
169
170# A strict traceparent v00 value (W3C 3.2.2): a trace ID of 32 digits and a
171# parent ID of 16 digits, each with a proof that it is not all zero, and a flag
172# byte of two digits. Length and alphabet are structural: a value with a wrong
173# length or a non-hexadecimal digit cannot be built. All eight flag bits are
174# kept, including the reserved ones, so the codec is exact.
175type TraceParentV00 is Data:
176  TraceParentV00{
177    trace_id: Digits.NonZero<32n>,
178    parent_id: Digits.NonZero<16n>,
179    flags: Digits.Digits(2n)
180  }
181
182# A validated trace ID: 32 lowercase hexadecimal digits, not all zero (W3C
183# 3.2.2.3). `random` records whether the random-trace-id flag (W3C 3.2.2.5.2)
184# may be emitted for it. A parsed ID makes no such assertion: only its origin
185# can justify one. Generation sets it, and a caller who knows the ID is random
186# sets it with TraceId.assert_random.
187type TraceId is Data:
188  TraceId{value: Digits.NonZero<32n>, random: Bool}
189
190# A validated span ID: 16 lowercase hexadecimal digits, not all zero, the
191# identifier of one operation. It is sent as the parent ID of traceparent (W3C
192# 3.2.2.4).
193type SpanId is Data:
194  SpanId{value: Digits.NonZero<16n>}
195
196# How a child operation obtains its sampled indication (W3C 3.2.2.5.1):
197# InheritSampled{} keeps the parent's and SetSampled{sampled} sets it. The
198# indication communicates a decision; it does not record anything.
199type Sampling is Data:
200  InheritSampled{}
201  SetSampled{sampled: Bool}
202
203# A context received from another participant. It identifies the sender's
204# operation and keeps only the known flags: sampled and random-trace-id. It is
205# built from a received value (RemoteContext.from_traceparent) or from its
206# parts (RemoteContext.from_ids), and has its own type, so it cannot be sent
207# as if it were this participant's operation.
208type RemoteContext is Data:
209  RemoteContext{trace_id: TraceId, span_id: SpanId, sampled: Bool}
210
211# A context that identifies an operation of this participant: the one it sends
212# in its own headers. The Context.* operations build it.
213type LocalContext is Data:
214  LocalContext{trace_id: TraceId, span_id: SpanId, sampled: Bool}
215
216# The context whose trace a child operation continues: a received context or
217# one of this participant's own operations.
218type Parent is Data:
219  RemoteParent{context: RemoteContext}
220  LocalParent{context: LocalContext}
221
222# Why generating identifiers failed. A source failure carries the source's own
223# code and message; exhaustion names the identifier whose eight candidates were
224# all rejected.
225type GenerationError is Data:
226  SourceFailure{code: U32, message: String}
227  ExhaustedTraceId{}
228  ExhaustedSpanId{}
229
230# The words read so far for the current trace ID candidate, in arrival order.
231# Four words complete a candidate.
232type TraceWords is Data:
233  NoTraceWord{}
234  OneTraceWord{first: U32}
235  TwoTraceWords{first: U32, second: U32}
236  ThreeTraceWords{first: U32, second: U32, third: U32}
237
238# The words read so far for the current span ID candidate. Two words complete
239# a candidate.
240type SpanWords is Data:
241  NoSpanWord{}
242  OneSpanWord{first: U32}
243
244# The generation machine below is shared by the IO operations and stated in
245# the laws. Its types and its TraceDraw, SpanDraw, TraceStep, SpanStep,
246# SpanPlan, TracePlan, Draw, Step and Drive functions are internal: callers use
247# TraceId.generate_with, SpanId.generate_with and the `Context.*_with`
248# operations, or generation.bend, and a host that feeds words itself uses
249# Generation.
250#
251# A trace ID draw that waits for a word: `remaining` counts the further
252# candidates allowed after the current one, so each draw gets eight
253# candidates in all, `words` holds the words of the current candidate, and
254# `excluded` is the trace ID that no candidate may repeat, such as the
255# received one that a restart replaces.
256type TraceDraw is Data:
257  TraceDraw{remaining: Nat, words: TraceWords, excluded: Maybe<&2, TraceId>}
258
259# A span ID draw that waits for a word, as TraceDraw: `excluded` is the span
260# ID that no candidate may repeat, such as a child's parent's.
261type SpanDraw is Data:
262  SpanDraw{remaining: Nat, words: SpanWords, excluded: Maybe<&2, SpanId>}
263
264# A trace ID draw after each source word, whether it generates a trace ID
265# alone or the trace ID of a root or a restart: it waits for another word, it
266# drew a trace ID, or it failed.
267type TraceStep is Data:
268  NeedTraceWord{draw: TraceDraw}
269  DrawnTraceId{id: TraceId}
270  TraceFailed{error: GenerationError}
271
272# A span ID draw after each source word, whether it generates a span ID alone
273# or the span ID of a root, a child or a restart, as TraceStep.
274type SpanStep is Data:
275  NeedSpanWord{draw: SpanDraw}
276  DrawnSpanId{id: SpanId}
277  SpanFailed{error: GenerationError}
278
279# What a new local context needs besides its span ID: the span ID that it must
280# not repeat (`excluded`), such as a child's parent's, the trace ID that it
281# belongs to, and its sampled indication. SpanPlan.root and SpanPlan.child
282# give the plans of a root and a child.
283type SpanPlan is Data:
284  SpanPlan{excluded: Maybe<&2, SpanId>, trace_id: TraceId, sampled: Bool}
285
286# What a new trace needs, a root or a restart: the trace ID that its trace
287# ID must not repeat (`excluded`), none for a root and the received one for
288# a restart, and the sampled indication of the context that it creates.
289# TracePlan.root and TracePlan.restart give the plans of a root and a
290# restart; the generation machine (TracePlan.draw), the generation that a
291# host feeds (Generation.new_trace) and the composition on a caller's source
292# (TracePlan.generate_with) each run one plan, so a root and a restart
293# differ only in it.
294type TracePlan is Data:
295  TracePlan{excluded: Maybe<&2, TraceId>, sampled: Bool}
296
297# A generation in progress: the trace ID draw of a root or a restart, with
298# the sampled indication of the context that it starts, or a span ID draw,
299# with the trace ID and the sampled indication of the context that its span
300# ID completes.
301type Draw is Data:
302  DrawTrace{draw: TraceDraw, sampled: Bool}
303  DrawSpan{draw: SpanDraw, trace_id: TraceId, sampled: Bool}
304
305# The state of a generation after each source word: it needs another word, it
306# created a context, or it failed.
307type Step is Data:
308  NeedWord{draw: Draw}
309  Created{context: LocalContext}
310  Failed{error: GenerationError}
311
312# A generation with its word budget, for a host that feeds it one word at a
313# time instead of passing a source as a template, such as JavaScript code
314# calling this module: the words it may still read (`fuel`) and the
315# machine's step. Its fields are internal, like Step: Generation.root and
316# its siblings build one. Context.continue_or_start_with and
317# Context.send_with drive the same values, and a host that feeds words while
318# Generation.needs says so gets the pure driver's result (law
319# generation_drive). Context.root_with and its siblings compose the
320# separate generation, whose results laws root_tape and its siblings give as
321# that driver's.
322type Generation is Data:
323  Generation{fuel: Nat, step: Step}
324
325# Strict v00 codec
326# ================
327#
328# TraceParentV00.parse reads exactly "00-", 32 lowercase hexadecimal digits,
329# "-", 16 digits, "-" and two digits (W3C 3.2.2). The helpers below read one
330# field at a time and report the first problem with the offset of the
331# offending character.
332
333# Put one more digit in front of a parsed sequence: n digits become 1 + n.
334def Parsed.prepend(-n: Nat, digit: Hex.Digit, parsed: Parsed<n>) -> Parsed<1n+n>:
335  match parsed:
336    case Parsed{digits, rest}:
337      Parsed{Digits.DCon{digit, digits}, rest}
338
339# A decoded character, or InvalidHex at its offset when it is not a lowercase
340# hexadecimal digit.
341def Parse.digit_result(value: Maybe<&2, Hex.Digit>, offset: Nat) ->
342  Result<&2, &2, Error, Hex.Digit>:
343  match value:
344    case None{}:
345      Fail{InvalidHex{offset}}
346    case Some{digit}:
347      Done{digit}
348
349# Decode one character as a lowercase hexadecimal digit.
350def Parse.digit(char: Char, offset: Nat) -> Result<&2, &2, Error, Hex.Digit>:
351  Parse.digit_result(Hex.Digit.from_char(char), offset)
352
353# Consume exactly n characters as digits, keeping the unconsumed rest of the
354# text. The recursion decreases n, so no length check or unchecked conversion
355# is needed: the result's type already has length n.
356def Parse.digits(n: Nat, text: String, offset: Nat) ->
357  Result<&2, &2, Error, Parsed<n>>:
358  match n:
359    case 0n:
360      Done{Parsed{Digits.DNil{}, text}}
361    case 1n+p:
362      match text:
363        case SNil{}:
364          Fail{UnexpectedEnd{offset}}
365        case SCon{char, tail}:
366          +at = offset
367          do Result<&2, &2, Error, Parsed<1n+p>>:
368            digit : Hex.Digit <- Parse.digit(char, at)
369            parsed : Parsed<p> <- Parse.digits(p, tail, 1n+at)
370            return Parsed.prepend(p, digit, parsed)
371
372# The rest of the text after a "-", or ExpectedSeparator at its offset.
373def Parse.separator_result(tail: String, ok: Bool, offset: Nat) ->
374  Result<&2, &2, Error, String>:
375  match ok:
376    case False{}:
377      Fail{ExpectedSeparator{offset}}
378    case True{}:
379      Done{tail}
380
381# Read the "-" expected at `offset`.
382def Parse.separator(text: String, offset: Nat) -> Result<&2, &2, Error, String>:
383  match text:
384    case SNil{}:
385      Fail{UnexpectedEnd{offset}}
386    case SCon{char, tail}:
387      Parse.separator_result(tail, Char.is_eq(char, '-'), offset)
388
389# The value must end here. Only the first character after it is inspected, so
390# an arbitrarily long suffix is refused without being read.
391def Parse.end(text: String) -> Result<&2, &2, Error, Unit>:
392  match text:
393    case SNil{}:
394      Done{Unit{}}
395    case SCon{char, tail}:
396      Fail{TrailingInput{}}
397
398# The version digits: 00 is the only version the strict codec reads, ff is
399# forbidden (W3C 3.2.2.1), and any other version is reported with its text.
400def Parse.version(digits: Digits.Digits(2n)) -> Result<&2, &2, Error, Unit>:
401  match digits:
402    case Digits.DCon{Hex.H0{}, Digits.DCon{Hex.H0{}, Digits.DNil{}}}:
403      Done{Unit{}}
404    case Digits.DCon{Hex.Hf{}, Digits.DCon{Hex.Hf{}, Digits.DNil{}}}:
405      Fail{ForbiddenVersion{}}
406    case other:
407      Fail{UnsupportedVersion{Digits.Digits.to_string(2n, other)}}
408
409# Attach the proof that digits are not all zero, or fail with ZeroId naming
410# the field.
411def Parse.nonzero_result(-n: Nat, result: Maybe<&2, Digits.NonZero<n>>, field: Field) ->
412  Result<&2, &2, Error, Digits.NonZero<n>>:
413  match result:
414    case None{}:
415      Fail{ZeroId{field}}
416    case Some{id}:
417      Done{id}
418
419# Check that digits are not all zero (W3C 3.2.2.3, 3.2.2.4).
420def Parse.nonzero(n: Nat, digits: Digits.Digits(n), field: Field) ->
421  Result<&2, &2, Error, Digits.NonZero<n>>:
422  Parse.nonzero_result(n, Digits.NonZero.new(n, digits), field)
423
424# The last field: the two flag digits, then the end of the text.
425def Parse.flags(trace_id: Digits.NonZero<32n>, parent_id: Digits.NonZero<16n>,
426  parsed: Parsed<2n>) -> Result<&2, &2, Error, TraceParentV00>:
427  match parsed:
428    case Parsed{flags, rest}:
429      do Result<&2, &2, Error, TraceParentV00>:
430        end : Unit <- Parse.end(rest)
431        return TraceParentV00{trace_id, parent_id, flags}
432
433# After the trace ID: the parent ID, which must not be all zero, its "-" at
434# offset 52 and the flag digits at offset 53.
435def Parse.parent(trace_id: Digits.NonZero<32n>, parsed: Parsed<16n>) ->
436  Result<&2, &2, Error, TraceParentV00>:
437  match parsed:
438    case Parsed{parent_digits, rest}:
439      do Result<&2, &2, Error, TraceParentV00>:
440        parent_id : Digits.NonZero<16n> <- Parse.nonzero(16n, parent_digits, ParentIdField{})
441        after : String <- Parse.separator(rest, 52n)
442        flags : Parsed<2n> <- Parse.digits(2n, after, 53n)
443        Parse.flags(trace_id, parent_id, flags)
444
445# After the version: the trace ID, which must not be all zero, its "-" at
446# offset 35 and the parent ID from offset 36.
447def Parse.trace(parsed: Parsed<32n>) -> Result<&2, &2, Error, TraceParentV00>:
448  match parsed:
449    case Parsed{trace_digits, rest}:
450      do Result<&2, &2, Error, TraceParentV00>:
451        trace_id : Digits.NonZero<32n> <- Parse.nonzero(32n, trace_digits, TraceIdField{})
452        after : String <- Parse.separator(rest, 35n)
453        parent : Parsed<16n> <- Parse.digits(16n, after, 36n)
454        Parse.parent(trace_id, parent)
455
456# After the two version digits: the version check, the "-" at offset 2 and the
457# trace ID from offset 3.
458def Parse.start(parsed: Parsed<2n>) -> Result<&2, &2, Error, TraceParentV00>:
459  match parsed:
460    case Parsed{version, rest}:
461      do Result<&2, &2, Error, TraceParentV00>:
462        version_ok : Unit <- Parse.version(version)
463        after : String <- Parse.separator(rest, 2n)
464        trace : Parsed<32n> <- Parse.digits(32n, after, 3n)
465        Parse.trace(trace)
466
467# Parse a strict traceparent v00 value: exactly "00-", 32 lowercase
468# hexadecimal digits, "-", 16 digits, "-" and two digits; the IDs must not be
469# all zero. No whitespace, case folding or suffix is accepted, and every flag
470# byte is kept as received.
471# This is the strict wire codec, not a complete W3C propagator:
472# TraceParent.read and Context.extract apply the processing rules of W3C 3.2.4
473# and 4.1.2, such as reading later versions by their known prefix.
474# Laws: roundtrip, inverse and formatted_length.
475def TraceParentV00.parse(text: String) -> Result<&2, &2, Error, TraceParentV00>:
476  do Result<&2, &2, Error, TraceParentV00>:
477    version : Parsed<2n> <- Parse.digits(2n, text, 0n)
478    Parse.start(version)
479
480# The text of a strict v00 value: always 55 characters. It is total, because
481# validity is carried by the argument's type, and it preserves every flag bit:
482# it is the exact inverse of parse, not an outgoing-header policy (see
483# LocalContext.to_traceparent for what a participant emits).
484def TraceParentV00.format(context: TraceParentV00) -> String:
485  match context:
486    case TraceParentV00{trace_id, parent_id, flags}:
487      "00-" ++ Digits.NonZero.to_string(32n, trace_id) ++ "-" ++
488        Digits.NonZero.to_string(16n, parent_id) ++ "-" ++
489        Digits.Digits.to_string(2n, flags)
490
491# Whether the sampled flag, bit 0 of the flag byte, is set (W3C 3.2.2.5.1).
492def TraceParentV00.is_sampled(context: TraceParentV00) -> Bool:
493  match context:
494    case TraceParentV00{trace_id, parent_id,
495      Digits.DCon{high, Digits.DCon{low, Digits.DNil{}}}}:
496      Hex.Digit.is_odd(low)
497
498# Whether the random-trace-id flag, bit 1, is set (W3C 3.2.2.5.2). It records
499# the sender's assertion; it does not prove how the trace ID was generated.
500def TraceParentV00.is_random(context: TraceParentV00) -> Bool:
501  match context:
502    case TraceParentV00{trace_id, parent_id,
503      Digits.DCon{high, Digits.DCon{low, Digits.DNil{}}}}:
504      Hex.Digit.has_bit1(low)
505
506# Identifiers and contexts
507# ========================
508#
509# Supplied IDs are parsed with the same digit reader as the codec. Contexts are
510# created from validated IDs: a root, a child continuing a parent, a restart
511# replacing a received trace, or the explicit construction of an operation the
512# caller owns. A context also gives its known trace flags as a number, for an
513# exporter; its sampled indication and its trace ID's randomness assertion
514# stay their canonical form, and there is no trace flags type.
515
516# The digits of a supplied ID must be the whole text, and not all zero.
517def Parse.id.finish(n: Nat, parsed: Parsed<n>, field: Field) ->
518  Result<&2, &2, Error, Digits.NonZero<n>>:
519  match parsed:
520    case Parsed{digits, rest}:
521      do Result<&2, &2, Error, Digits.NonZero<n>>:
522        end : Unit <- Parse.end(rest)
523        Parse.nonzero(n, digits, field)
524
525# A supplied ID is exactly n lowercase hexadecimal digits, not all zero.
526def Parse.id(+n: Nat, text: String, field: Field) ->
527  Result<&2, &2, Error, Digits.NonZero<n>>:
528  do Result<&2, &2, Error, Digits.NonZero<n>>:
529    parsed : Parsed<n> <- Parse.digits(n, text, 0n)
530    Parse.id.finish(n, parsed, field)
531
532# Parse a supplied trace ID: exactly 32 lowercase hexadecimal digits, not all
533# zero. Error offsets count from the start of the ID. The result makes no
534# randomness assertion (laws trace_id_parse and trace_id_accepts).
535def TraceId.parse(text: String) -> Result<&2, &2, Error, TraceId>:
536  do Result<&2, &2, Error, TraceId>:
537    value : Digits.NonZero<32n> <- Parse.id(32n, text, TraceIdField{})
538    return TraceId{value, False{}}
539
540# Record the caller's assertion that these digits were generated randomly, so
541# that the random-trace-id flag is emitted with them. The caller is responsible
542# for the assertion; validation cannot establish it (law assert_random).
543def TraceId.assert_random(id: TraceId) -> TraceId:
544  match id:
545    case TraceId{value, random}:
546      TraceId{value, True{}}
547
548# Whether the trace ID asserts that it was generated randomly.
549def TraceId.is_random(id: TraceId) -> Bool:
550  match id:
551    case TraceId{value, random}:
552      random
553
554# The 32 lowercase hexadecimal digits of the trace ID.
555def TraceId.to_string(id: TraceId) -> String:
556  match id:
557    case TraceId{value, random}:
558      Digits.NonZero.to_string(32n, value)
559
560# Whether two trace IDs name the same trace. The randomness assertion is not
561# part of the identifier, so it is ignored.
562def TraceId.is_eq(a: TraceId, b: TraceId) -> Bool:
563  String.eq(TraceId.to_string(a), TraceId.to_string(b))
564
565# Parse a supplied span ID: exactly 16 lowercase hexadecimal digits, not all
566# zero (laws span_id_parse and span_id_roundtrip).
567def SpanId.parse(text: String) -> Result<&2, &2, Error, SpanId>:
568  do Result<&2, &2, Error, SpanId>:
569    value : Digits.NonZero<16n> <- Parse.id(16n, text, SpanIdField{})
570    return SpanId{value}
571
572# The 16 lowercase hexadecimal digits of the span ID.
573def SpanId.to_string(id: SpanId) -> String:
574  match id:
575    case SpanId{value}:
576      Digits.NonZero.to_string(16n, value)
577
578# Whether two span IDs name the same operation.
579def SpanId.is_eq(a: SpanId, b: SpanId) -> Bool:
580  String.eq(SpanId.to_string(a), SpanId.to_string(b))
581
582# The sampled indication a child receives: the inherited one, unless the
583# caller set another (law sampling).
584def Sampling.resolve(sampling: Sampling, inherited: Bool) -> Bool:
585  match sampling:
586    case InheritSampled{}:
587      inherited
588    case SetSampled{sampled}:
589      sampled
590
591# Interpret a received strict-v00 value as the sender's context. Bit 0 is
592# sampled and bit 1 is random-trace-id; the reserved bits are not interpreted
593# and do not travel with the context (law received_flags).
594def RemoteContext.from_traceparent(value: TraceParentV00) -> RemoteContext:
595  match value:
596    case TraceParentV00{trace_id, parent_id,
597      Digits.DCon{high, Digits.DCon{+low, Digits.DNil{}}}}:
598      RemoteContext{TraceId{trace_id, Hex.Digit.has_bit1(low)}, SpanId{parent_id},
599        Hex.Digit.is_odd(low)}
600
601# Build the sender's context from its parts, as an OpenTelemetry SDK does for
602# a link or for a propagator of another format: its trace ID, its span ID and
603# its sampled indication, kept as they are. It is total, since the IDs are
604# valid by construction, and its random-trace-id bit is the trace ID's own
605# assertion: none for a parsed ID, unless TraceId.assert_random adds it (law
606# remote_from_ids). The result is still a received context, which a child
607# continues: it cannot be sent as this participant's operation
608# (tests/reject/remote_as_local.bend).
609def RemoteContext.from_ids(trace_id: TraceId, span_id: SpanId, sampled: Bool) -> RemoteContext:
610  RemoteContext{trace_id, span_id, sampled}
611
612# The trace the received context belongs to.
613def RemoteContext.trace_id(context: RemoteContext) -> TraceId:
614  match context:
615    case RemoteContext{trace_id, span_id, sampled}:
616      trace_id
617
618# The sender's operation: the parent ID of the received value.
619def RemoteContext.span_id(context: RemoteContext) -> SpanId:
620  match context:
621    case RemoteContext{trace_id, span_id, sampled}:
622      span_id
623
624# The sender's sampled indication.
625def RemoteContext.is_sampled(context: RemoteContext) -> Bool:
626  match context:
627    case RemoteContext{trace_id, span_id, sampled}:
628      sampled
629
630# The known trace flags as a number: `sampled` in bit 0 and `random` in bit 1
631# (W3C 3.2.2.5), with the six reserved bits zero.
632def Flags.known(sampled: Bool, random: Bool) -> U32:
633  U32.or(Bool.to_u32(sampled), U32.shl(Bool.to_u32(random)))
634
635# The trace flags that the context keeps, as a number from 0 to 3: bit 0 is
636# its sampled indication and bit 1 its trace ID's randomness assertion, the
637# known flags that it was received or built with. Reserved bits are never
638# among them. The Booleans stay the canonical form; the number is for an
639# exporter, such as one that writes OTLP's Span.flags field. Laws:
640# remote_flags and received_trace_flags.
641def RemoteContext.flags(context: RemoteContext) -> U32:
642  match context:
643    case RemoteContext{trace_id, span_id, sampled}:
644      Flags.known(sampled, TraceId.is_random(trace_id))
645
646# The trace this participant's operation belongs to.
647def LocalContext.trace_id(context: LocalContext) -> TraceId:
648  match context:
649    case LocalContext{trace_id, span_id, sampled}:
650      trace_id
651
652# This participant's operation.
653def LocalContext.span_id(context: LocalContext) -> SpanId:
654  match context:
655    case LocalContext{trace_id, span_id, sampled}:
656      span_id
657
658# The sampled indication this participant sends.
659def LocalContext.is_sampled(context: LocalContext) -> Bool:
660  match context:
661    case LocalContext{trace_id, span_id, sampled}:
662      sampled
663
664# The participating representation of a local context: version 00, and flags
665# limited to sampled (bit 0) and random-trace-id (bit 1), with every reserved
666# bit zero (W3C 3.2.2.5.3; laws emitted_traceparent and emitted_projection).
667def LocalContext.to_traceparent(context: LocalContext) -> TraceParentV00:
668  match context:
669    case LocalContext{TraceId{trace_id, random}, SpanId{span_id}, sampled}:
670      TraceParentV00{trace_id, span_id,
671        Digits.DCon{Hex.H0{}, Digits.DCon{Hex.Digit.from_bits(sampled, random, False{}, False{}), Digits.DNil{}}}}
672
673# The trace flags of the context as a number from 0 to 3: bit 0 is its sampled
674# indication and bit 1 its trace ID's randomness assertion. It is the flag
675# byte of the traceparent that the context emits, 00 to 03, so an exporter
676# that writes it, into OTLP's Span.flags field for example, agrees with what
677# the context propagates. The Booleans stay the canonical form. Law:
678# local_flags.
679def LocalContext.flags(context: LocalContext) -> U32:
680  match context:
681    case LocalContext{trace_id, span_id, sampled}:
682      Flags.known(sampled, TraceId.is_random(trace_id))
683
684# The trace a child continues.
685def Parent.trace_id(parent: Parent) -> TraceId:
686  match parent:
687    case RemoteParent{context}:
688      RemoteContext.trace_id(context)
689    case LocalParent{context}:
690      LocalContext.trace_id(context)
691
692# The parent's operation, which a child must not reuse.
693def Parent.span_id(parent: Parent) -> SpanId:
694  match parent:
695    case RemoteParent{context}:
696      RemoteContext.span_id(context)
697    case LocalParent{context}:
698      LocalContext.span_id(context)
699
700# The sampled indication a child inherits by default.
701def Parent.is_sampled(parent: Parent) -> Bool:
702  match parent:
703    case RemoteParent{context}:
704      RemoteContext.is_sampled(context)
705    case LocalParent{context}:
706      LocalContext.is_sampled(context)
707
708# Represent an operation the caller owns, with supplied IDs and an explicit
709# sampled indication. The IDs must belong to that operation: validating their
710# format cannot establish where they came from (law from_ids).
711def Context.from_ids(trace_id: TraceId, span_id: SpanId, sampled: Bool) -> LocalContext:
712  LocalContext{trace_id, span_id, sampled}
713
714# Start a trace with supplied IDs and the sampled indication that the caller
715# decided, kept as it is given (spec #41, "Sampling decision when starting a
716# trace"; law root). False gives an unsampled root, the default of spec #1,
717# "New roots default to sampled `0`", which Context.continue_or_start_with
718# applies itself. generation.bend provides Context.root, Context.child and
719# Context.restart for generated IDs.
720def Context.root_from_ids(trace_id: TraceId, span_id: SpanId, sampled: Bool) -> LocalContext:
721  Context.from_ids(trace_id, span_id, sampled)
722
723# The child, unless the span ID was found equal to the parent's.
724def Context.child_from_id.checked(trace_id: TraceId, span_id: SpanId, sampled: Bool, reused: Bool) ->
725  Result<&2, &2, ContextError, LocalContext>:
726  match reused:
727    case True{}:
728      Fail{ReusedSpanId{}}
729    case False{}:
730      Done{Context.from_ids(trace_id, span_id, sampled)}
731
732# Continue the parent's trace with a new operation identified by a supplied
733# span ID. The child keeps the trace ID and its randomness assertion, and its
734# span ID must differ from the parent's (ReusedSpanId otherwise). Sampling is
735# inherited unless set. Laws: child, child_reuse and child_accepts.
736def Context.child_from_id(+parent: Parent, +span_id: SpanId, sampling: Sampling) ->
737  Result<&2, &2, ContextError, LocalContext>:
738  Context.child_from_id.checked(Parent.trace_id(parent), span_id,
739    Sampling.resolve(sampling, Parent.is_sampled(parent)),
740    SpanId.is_eq(span_id, Parent.span_id(parent)))
741
742# The restarted root, unless the trace ID was found equal to the received one.
743def Context.restart_from_ids.checked(trace_id: TraceId, span_id: SpanId, sampled: Bool, reused: Bool) ->
744  Result<&2, &2, ContextError, LocalContext>:
745  match reused:
746    case True{}:
747      Fail{ReusedTraceId{}}
748    case False{}:
749      Done{Context.root_from_ids(trace_id, span_id, sampled)}
750
751# Start a new trace with supplied IDs instead of continuing a received context.
752# The new trace ID must differ from the received one (ReusedTraceId otherwise),
753# and the restart is the root of its IDs with the sampled indication that it
754# is given: False applies the root defaults, sampled 0 included. Laws:
755# restart, restart_reuse and restart_accepts.
756def Context.restart_from_ids(previous: RemoteContext, +trace_id: TraceId, span_id: SpanId, sampled: Bool) ->
757  Result<&2, &2, ContextError, LocalContext>:
758  Context.restart_from_ids.checked(trace_id, span_id, sampled,
759    TraceId.is_eq(trace_id, RemoteContext.trace_id(previous)))
760
761# Identifiers from source words
762# =============================
763#
764# Generated IDs are built from 32-bit words: four words for a trace ID and two
765# for a span ID, most significant first (spec #1). These conversions make no
766# randomness assertion; generation adds it.
767
768# The eight lowercase hexadecimal digits of a word, most significant first
769# (laws hex_injective and word_hex).
770def U32.to_hex(word: U32) -> String:
771  Digits.Digits.to_string(8n, Digits.Digits.of_u32(word))
772
773# A trace ID from nonzero digits, with no randomness assertion.
774def TraceId.from_digits(value: Maybe<&2, Digits.NonZero<32n>>) -> Maybe<&2, TraceId>:
775  match value:
776    case None{}:
777      None{}
778    case Some{digits}:
779      Some{TraceId{digits, False{}}}
780
781# A trace ID from four words, read most significant first: the first word
782# gives the first eight digits. Like a parsed ID it makes no randomness
783# assertion; add one with TraceId.assert_random when the words are random. An
784# all-zero candidate is None (laws trace_words and words_unasserted).
785def TraceId.from_words(first: U32, second: U32, third: U32, fourth: U32) -> Maybe<&2, TraceId>:
786  TraceId.from_digits(Digits.NonZero.new(32n,
787    Digits.Digits.append(8n, 24n, Digits.Digits.of_u32(first),
788      Digits.Digits.append(8n, 16n, Digits.Digits.of_u32(second),
789        Digits.Digits.append(8n, 8n, Digits.Digits.of_u32(third), Digits.Digits.of_u32(fourth))))))
790
791# A span ID from nonzero digits.
792def SpanId.from_digits(value: Maybe<&2, Digits.NonZero<16n>>) -> Maybe<&2, SpanId>:
793  match value:
794    case None{}:
795      None{}
796    case Some{digits}:
797      Some{SpanId{digits}}
798
799# A span ID from two words, most significant first. An all-zero candidate is
800# None (law span_words).
801def SpanId.from_words(first: U32, second: U32) -> Maybe<&2, SpanId>:
802  SpanId.from_digits(Digits.NonZero.new(16n,
803    Digits.Digits.append(8n, 8n, Digits.Digits.of_u32(first), Digits.Digits.of_u32(second))))
804
805# Identifiers as bytes
806# ====================
807#
808# The bytes of an ID are the form of OTLP's protobuf encoding, as the text of
809# TraceId.to_string and SpanId.to_string is that of its JSON encoding (spec
810# #41, "Identifier forms"). TraceId.to_bytes and TraceId.from_bytes state the
811# contract; the helpers below read bytes as Parse.id reads text.
812
813# Put the two digits of one more byte in front of the bytes already read: n
814# bytes become 1 + n.
815def ParsedBytes.prepend(-n: Nat, digits: Digits.Digits(2n), parsed: ParsedBytes<n>) -> ParsedBytes<1n+n>:
816  match digits parsed:
817    case Digits.DCon{high, Digits.DCon{low, Digits.DNil{}}} ParsedBytes{rest_digits, rest}:
818      ParsedBytes{Digits.DCon{high, Digits.DCon{low, rest_digits}}, rest}
819
820# The two digits of a cell, or InvalidByte at its offset when the check found
821# the cell above 255.
822def Parse.byte.checked(cell: U32, above: Bool, offset: Nat) -> Result<&2, &2, Error, Digits.Digits(2n)>:
823  match above:
824    case True{}:
825      Fail{InvalidByte{offset}}
826    case False{}:
827      Done{Digits.Digits.of_byte(cell)}
828
829# Read one cell as a byte.
830def Parse.byte(+cell: U32, offset: Nat) -> Result<&2, &2, Error, Digits.Digits(2n)>:
831  Parse.byte.checked(cell, U32.is_gt(cell, 255), offset)
832
833# Consume exactly n cells as bytes, keeping the cells after them. As in
834# Parse.digits, the recursion decreases n, so the result's type has the 2n
835# digits of n bytes.
836def Parse.bytes(n: Nat, bytes: List<&2, U32>, offset: Nat) -> Result<&2, &2, Error, ParsedBytes<n>>:
837  match n:
838    case 0n:
839      Done{ParsedBytes{Digits.DNil{}, bytes}}
840    case 1n+p:
841      match bytes:
842        case Nil{}:
843          Fail{UnexpectedEnd{offset}}
844        case Con{cell, tail}:
845          +at = offset
846          do Result<&2, &2, Error, ParsedBytes<1n+p>>:
847            digits : Digits.Digits(2n) <- Parse.byte(cell, at)
848            parsed : ParsedBytes<p> <- Parse.bytes(p, tail, 1n+at)
849            return ParsedBytes.prepend(p, digits, parsed)
850
851# The list must end after the ID's bytes: a cell after them fails with
852# TrailingInput, whatever it holds.
853def Parse.bytes_end(bytes: List<&2, U32>) -> Result<&2, &2, Error, Unit>:
854  match bytes:
855    case Nil{}:
856      Done{Unit{}}
857    case Con{cell, rest}:
858      Fail{TrailingInput{}}
859
860# The bytes of a supplied ID must be the whole list, and not all zero.
861def Parse.id_bytes.finish(n: Nat, parsed: ParsedBytes<n>, field: Field) ->
862  Result<&2, &2, Error, Digits.NonZero<Nat.double(n)>>:
863  match parsed:
864    case ParsedBytes{digits, rest}:
865      do Result<&2, &2, Error, Digits.NonZero<Nat.double(n)>>:
866        end : Unit <- Parse.bytes_end(rest)
867        Parse.nonzero(Nat.double(n), digits, field)
868
869# A supplied ID is exactly n bytes, not all zero.
870def Parse.id_bytes(+n: Nat, bytes: List<&2, U32>, field: Field) ->
871  Result<&2, &2, Error, Digits.NonZero<Nat.double(n)>>:
872  do Result<&2, &2, Error, Digits.NonZero<Nat.double(n)>>:
873    parsed : ParsedBytes<n> <- Parse.bytes(n, bytes, 0n)
874    Parse.id_bytes.finish(n, parsed, field)
875
876# The 16 bytes of the trace ID, most significant first, in Base's byte
877# convention, that of TCP.send_bytes and TCP.recv_bytes: one U32 cell from 0
878# to 255 per byte. The first byte holds the ID's first two digits, the first
879# of them high. The randomness assertion is not part of the bytes (laws
880# trace_bytes, trace_bytes_roundtrip and trace_bytes_injective).
881def TraceId.to_bytes(id: TraceId) -> List<&2, U32>:
882  match id:
883    case TraceId{value, random}:
884      Digits.Digits.to_bytes(16n, Digits.NonZero.digits(32n, value))
885
886# Read a trace ID from exactly 16 bytes, most significant first. The cells
887# are read in order: a missing cell fails with UnexpectedEnd and a cell above
888# 255 with InvalidByte, at its offset counted in cells; a 17th cell fails with
889# TrailingInput whatever it holds, and 16 zero bytes with ZeroId. Like a
890# parsed ID, the result makes no randomness assertion, since bytes do not say
891# how the ID was made; only a caller whose own generator, known to be random,
892# made it adds one with TraceId.assert_random. Laws: trace_bytes_inverse,
893# bytes_unasserted, trace_bytes_short, trace_bytes_long, trace_bytes_above,
894# zero_bytes and trace_bytes_accepts.
895def TraceId.from_bytes(bytes: List<&2, U32>) -> Result<&2, &2, Error, TraceId>:
896  do Result<&2, &2, Error, TraceId>:
897    value : Digits.NonZero<32n> <- Parse.id_bytes(16n, bytes, TraceIdField{})
898    return TraceId{value, False{}}
899
900# The 8 bytes of the span ID, most significant first (laws span_bytes,
901# span_bytes_roundtrip and span_bytes_injective).
902def SpanId.to_bytes(id: SpanId) -> List<&2, U32>:
903  match id:
904    case SpanId{value}:
905      Digits.Digits.to_bytes(8n, Digits.NonZero.digits(16n, value))
906
907# Read a span ID from exactly 8 bytes, most significant first, with the rules
908# and errors of TraceId.from_bytes. Laws: span_bytes_inverse,
909# span_bytes_short, span_bytes_long, span_bytes_above, zero_bytes and
910# span_bytes_accepts.
911def SpanId.from_bytes(bytes: List<&2, U32>) -> Result<&2, &2, Error, SpanId>:
912  do Result<&2, &2, Error, SpanId>:
913    value : Digits.NonZero<16n> <- Parse.id_bytes(8n, bytes, SpanIdField{})
914    return SpanId{value}
915
916# Generation machine
917# ==================
918#
919# A generation is a small state machine fed one source word at a time. It
920# has two pieces, each of which draws one identifier: a trace ID draw
921# (TraceDraw, TraceStep) reads four words per candidate, and a span ID draw
922# (SpanDraw, SpanStep) two. Each piece gives its identifier eight
923# candidates, rejects zero and the identifier to exclude, and stops at the
924# first source error. TraceId.generate_with and SpanId.generate_with run one
925# piece alone. A generation (Draw, Step) runs the pieces in turn: a root or
926# a restart draws its trace ID, then its span ID, as its trace plan
927# (TracePlan) says, and a child only its span ID, as its span plan
928# (SpanPlan) says. A root and a restart differ only in their plan.
929# Context.root_with and its siblings compose the two operations in the same
930# order. One driver (Drive) runs the
931# three machines, over a replayed tape in the laws and over the host's
932# cryptographic source in generation.bend.
933
934# Generation reads its words from a source trusted to be random, so each
935# trace ID candidate asserts random-trace-id.
936def Draw.asserted(candidate: Maybe<&2, TraceId>) -> Maybe<&2, TraceId>:
937  match candidate:
938    case None{}:
939      None{}
940    case Some{id}:
941      Some{TraceId.assert_random(id)}
942
943# A deterministic word source for tests and replay: each read takes the next
944# result, and an empty tape fails with code 1, tape-exhausted.
945def Tape.next(tape: List<&1, Result<&1, &1, U32 & String, U32>>) ->
946  List<&1, Result<&1, &1, U32 & String, U32>> & Result<&1, &1, U32 & String, U32>:
947  match tape:
948    case Nil{}:
949      (Nil{}, Fail{(1, "tape-exhausted")})
950    case Con{word, rest}:
951      (rest, word)
952
953# The driver of the three machines: a trace ID draw, a span ID draw and a
954# generation. It feeds a machine one source word at a time while the
955# machine's step waits for one, and stops as soon as it has ended. Each
956# machine gives, as templates, `waiting`, the draw that a step feeds its next
957# word to, if it waits for one, and `feed`, the step after that word. The
958# driver keeps each step beside what `waiting` says of it.
959#
960# Feed a word that a source returned, keeping the source's next state.
961def Drive.fed(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>, ~feed: Result<&1, &1, U32 & String, U32> -> D -> T,
962  -S: Type, got: S & Result<&1, &1, U32 & String, U32>, draw: D) -> S & (T & Maybe<&2, D>):
963  (state, word) = got
964  +next = feed(word, draw)
965  (state, (next, waiting(next)))
966
967# Drive a machine from a tape, stopping as soon as its step has ended; unread
968# words stay on the tape. `fuel` bounds the steps, which Bend requires for
969# termination; the laws show the budgets suffice.
970def Drive.run(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>, ~feed: Result<&1, &1, U32 & String, U32> -> D -> T,
971  fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & (T & Maybe<&2, D>)) ->
972  List<&1, Result<&1, &1, U32 & String, U32>> & T:
973  match fuel current:
974    case _ Tuple{tape, Tuple{step, None{}}}:
975      (tape, step)
976    case 0n Tuple{tape, Tuple{step, Some{draw}}}:
977      (tape, step)
978    case 1n+p Tuple{tape, Tuple{step, Some{draw}}}:
979      Drive.run(~T, ~D, ~waiting, ~feed, p, Drive.fed(~T, ~D, ~waiting, ~feed,
980        List<&1, Result<&1, &1, U32 & String, U32>>, Tape.next(tape), draw))
981
982# Drive a machine from any source, one word at a time. `read` returns the
983# source's next state with each word, and the driver stops as soon as the
984# machine's step has ended; the final source state is handed back, so a
985# caller can see what was read. `fuel` bounds the words read, as in
986# Drive.run. Templates keep this driver free of any host effect: the effect,
987# if any, lives in the source.
988def Drive.read(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>, ~feed: Result<&1, &1, U32 & String, U32> -> D -> T,
989  ~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), fuel: Nat, current: S & (T & Maybe<&2, D>)) ->
990  IO(S & T):
991  match fuel current:
992    case _ Tuple{state, Tuple{step, None{}}}:
993      IO.pure(S & T, (state, step))
994    case 0n Tuple{state, Tuple{step, Some{draw}}}:
995      IO.pure(S & T, (state, step))
996    case 1n+p Tuple{state, Tuple{step, Some{draw}}}:
997      IO.bind(S & Result<&1, &1, U32 & String, U32>, S & T, read(state),
998        got => Drive.read(~T, ~D, ~waiting, ~feed, ~S, ~read, p, Drive.fed(~T, ~D, ~waiting, ~feed, S, got, draw)))
999
1000# Whether the machine in a driver's result has ended.
1001def Drive.ended(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>,
1002  result: List<&1, Result<&1, &1, U32 & String, U32>> & T) -> Bool:
1003  match result:
1004    case Tuple{tape, step}:
1005      Maybe.is_none(&2, D, waiting(step))
1006
1007# The source's final state with the result that `result` gives of the
1008# machine's final step.
1009def Drive.outcome(~T: Data, ~A: Data, ~result: T -> Result<&2, &2, GenerationError, A>, -S: Type, done: S & T) ->
1010  S & Result<&2, &2, GenerationError, A>:
1011  (state, step) = done
1012  (state, result(step))
1013
1014# Turn the IO driver's final step into its result.
1015def Drive.finished(~T: Data, ~A: Data, ~result: T -> Result<&2, &2, GenerationError, A>, ~S: Type,
1016  action: IO(S & T)) -> IO(S & Result<&2, &2, GenerationError, A>):
1017  IO.bind(S & T, S & Result<&2, &2, GenerationError, A>, action,
1018    done => IO.pure(S & Result<&2, &2, GenerationError, A>, Drive.outcome(~T, ~A, ~result, S, done)))
1019
1020# Trace ID draws
1021# --------------
1022
1023# A trace ID draw starts with its first candidate; seven further candidates
1024# may follow it, eight in all.
1025def TraceDraw.start(excluded: Maybe<&2, TraceId>) -> TraceStep:
1026  NeedTraceWord{TraceDraw{7n, NoTraceWord{}, excluded}}
1027
1028# Try another trace ID candidate, or fail once the eight are used.
1029def TraceDraw.retry(remaining: Nat, excluded: Maybe<&2, TraceId>) -> TraceStep:
1030  match remaining:
1031    case 0n:
1032      TraceFailed{ExhaustedTraceId{}}
1033    case 1n+p:
1034      NeedTraceWord{TraceDraw{p, NoTraceWord{}, excluded}}
1035
1036# A trace ID candidate equal to the excluded one is retried.
1037def TraceDraw.reuse(reused: Bool, id: TraceId, excluded: TraceId, remaining: Nat) -> TraceStep:
1038  match reused:
1039    case True{}:
1040      TraceDraw.retry(remaining, Some{excluded})
1041    case False{}:
1042      DrawnTraceId{id}
1043
1044# Check a complete trace ID candidate: zero and the excluded trace ID are
1045# retried; anything else is the trace ID drawn.
1046def TraceDraw.check(candidate: Maybe<&2, TraceId>, excluded: Maybe<&2, TraceId>, remaining: Nat) -> TraceStep:
1047  match candidate:
1048    case None{}:
1049      TraceDraw.retry(remaining, excluded)
1050    case Some{+id}:
1051      match excluded:
1052        case None{}:
1053          DrawnTraceId{id}
1054        case Some{+old}:
1055          TraceDraw.reuse(TraceId.is_eq(id, old), id, old, remaining)
1056
1057# Add a word to the current trace ID candidate. The fourth word completes it,
1058# most significant first, and the candidate is checked.
1059def TraceDraw.take(word: U32, remaining: Nat, words: TraceWords, excluded: Maybe<&2, TraceId>) -> TraceStep:
1060  match words:
1061    case NoTraceWord{}:
1062      NeedTraceWord{TraceDraw{remaining, OneTraceWord{word}, excluded}}
1063    case OneTraceWord{first}:
1064      NeedTraceWord{TraceDraw{remaining, TwoTraceWords{first, word}, excluded}}
1065    case TwoTraceWords{first, second}:
1066      NeedTraceWord{TraceDraw{remaining, ThreeTraceWords{first, second, word}, excluded}}
1067    case ThreeTraceWords{first, second, third}:
1068      TraceDraw.check(Draw.asserted(TraceId.from_words(first, second, third, word)), excluded, remaining)
1069
1070# Feed the next source word to a trace ID draw, given as its three fields. A
1071# source error ends the draw at once with SourceFailure (law
1072# trace_id_failure).
1073def TraceDraw.feed(word: Result<&1, &1, U32 & String, U32>, remaining: Nat, words: TraceWords,
1074  excluded: Maybe<&2, TraceId>) -> TraceStep:
1075  match word:
1076    case Fail{(code, message)}:
1077      TraceFailed{SourceFailure{code, message}}
1078    case Done{next}:
1079      TraceDraw.take(next, remaining, words, excluded)
1080
1081# The step of a trace ID draw after its next source word, TraceDraw.feed of
1082# its fields: the `feed` that Drive takes.
1083def TraceDraw.next(word: Result<&1, &1, U32 & String, U32>, draw: TraceDraw) -> TraceStep:
1084  match draw:
1085    case TraceDraw{remaining, words, excluded}:
1086      TraceDraw.feed(word, remaining, words, excluded)
1087
1088# The draw that a trace ID draw's step feeds its next word to, while it
1089# waits for one: the view of the step that Drive needs.
1090def TraceStep.waiting(step: TraceStep) -> Maybe<&2, TraceDraw>:
1091  match step:
1092    case NeedTraceWord{draw}:
1093      Some{draw}
1094    case DrawnTraceId{id}:
1095      None{}
1096    case TraceFailed{error}:
1097      None{}
1098
1099# The trace ID of a finished trace ID draw, or why it failed. A draw that has
1100# not finished would report exhaustion; law trace_id_ends shows that the word
1101# budget of TraceId.generate_with makes that case unreachable.
1102def TraceDraw.result(step: TraceStep) -> Result<&2, &2, GenerationError, TraceId>:
1103  match step:
1104    case DrawnTraceId{id}:
1105      Done{id}
1106    case TraceFailed{error}:
1107      Fail{error}
1108    case NeedTraceWord{draw}:
1109      Fail{ExhaustedTraceId{}}
1110
1111# Drive a trace ID draw from a tape (Drive.run).
1112def TraceDraw.run(fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & TraceStep) ->
1113  List<&1, Result<&1, &1, U32 & String, U32>> & TraceStep:
1114  match current:
1115    case Tuple{tape, +step}:
1116      Drive.run(~TraceStep, ~TraceDraw, ~TraceStep.waiting, ~TraceDraw.next, fuel,
1117        (tape, (step, TraceStep.waiting(step))))
1118
1119# Whether the trace ID draw in a driver's result has ended.
1120def TraceDraw.ended(result: List<&1, Result<&1, &1, U32 & String, U32>> & TraceStep) -> Bool:
1121  Drive.ended(~TraceStep, ~TraceDraw, ~TraceStep.waiting, result)
1122
1123# The source's final state with the trace ID draw's result.
1124def TraceDraw.outcome(-S: Type, done: S & TraceStep) -> S & Result<&2, &2, GenerationError, TraceId>:
1125  Drive.outcome(~TraceStep, ~TraceId, ~TraceDraw.result, S, done)
1126
1127# A trace ID alone, from a caller's source, as an OpenTelemetry SDK generates
1128# one before its sampler decides on it. `read` returns the source's next state
1129# with each word result, and the source's final state is returned. It reads
1130# four words per candidate, most significant first, for at most eight
1131# candidates, so at most 32 words; rejects all-zero candidates and `excluded`,
1132# when there is one; and fails with SourceFailure or ExhaustedTraceId. The
1133# source is trusted to be random: the trace ID asserts random-trace-id.
1134# Laws: trace_id_tape, trace_id_failure, trace_id_candidate, trace_id_ends,
1135# trace_id_exhaustion and generated_trace_id.
1136def TraceId.generate_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S,
1137  excluded: Maybe<&2, TraceId>) -> IO(S & Result<&2, &2, GenerationError, TraceId>):
1138  +start = TraceDraw.start(excluded)
1139  Drive.finished(~TraceStep, ~TraceId, ~TraceDraw.result, ~S, Drive.read(~TraceStep, ~TraceDraw, ~TraceStep.waiting,
1140    ~TraceDraw.next, ~S, ~read, 32n, (source, (start, TraceStep.waiting(start)))))
1141
1142# Span ID draws
1143# -------------
1144
1145# A span ID draw starts with its first candidate; seven further candidates
1146# may follow it, eight in all.
1147def SpanDraw.start(excluded: Maybe<&2, SpanId>) -> SpanStep:
1148  NeedSpanWord{SpanDraw{7n, NoSpanWord{}, excluded}}
1149
1150# Try another span ID candidate, or fail once the eight are used.
1151def SpanDraw.retry(remaining: Nat, excluded: Maybe<&2, SpanId>) -> SpanStep:
1152  match remaining:
1153    case 0n:
1154      SpanFailed{ExhaustedSpanId{}}
1155    case 1n+p:
1156      NeedSpanWord{SpanDraw{p, NoSpanWord{}, excluded}}
1157
1158# A span ID candidate equal to the excluded one is retried.
1159def SpanDraw.reuse(reused: Bool, id: SpanId, excluded: SpanId, remaining: Nat) -> SpanStep:
1160  match reused:
1161    case True{}:
1162      SpanDraw.retry(remaining, Some{excluded})
1163    case False{}:
1164      DrawnSpanId{id}
1165
1166# Check a complete span ID candidate: zero and the excluded span ID are
1167# retried; anything else is the span ID drawn.
1168def SpanDraw.check(candidate: Maybe<&2, SpanId>, excluded: Maybe<&2, SpanId>, remaining: Nat) -> SpanStep:
1169  match candidate:
1170    case None{}:
1171      SpanDraw.retry(remaining, excluded)
1172    case Some{+id}:
1173      match excluded:
1174        case None{}:
1175          DrawnSpanId{id}
1176        case Some{+old}:
1177          SpanDraw.reuse(SpanId.is_eq(id, old), id, old, remaining)
1178
1179# Add a word to the current span ID candidate. The second word completes it,
1180# most significant first, and the candidate is checked.
1181def SpanDraw.take(word: U32, remaining: Nat, words: SpanWords, excluded: Maybe<&2, SpanId>) -> SpanStep:
1182  match words:
1183    case NoSpanWord{}:
1184      NeedSpanWord{SpanDraw{remaining, OneSpanWord{word}, excluded}}
1185    case OneSpanWord{first}:
1186      SpanDraw.check(SpanId.from_words(first, word), excluded, remaining)
1187
1188# Feed the next source word to a span ID draw, given as its three fields. A
1189# source error ends the draw at once with SourceFailure (law
1190# span_id_failure).
1191def SpanDraw.feed(word: Result<&1, &1, U32 & String, U32>, remaining: Nat, words: SpanWords,
1192  excluded: Maybe<&2, SpanId>) -> SpanStep:
1193  match word:
1194    case Fail{(code, message)}:
1195      SpanFailed{SourceFailure{code, message}}
1196    case Done{next}:
1197      SpanDraw.take(next, remaining, words, excluded)
1198
1199# The step of a span ID draw after its next source word, SpanDraw.feed of its
1200# fields: the `feed` that Drive takes.
1201def SpanDraw.next(word: Result<&1, &1, U32 & String, U32>, draw: SpanDraw) -> SpanStep:
1202  match draw:
1203    case SpanDraw{remaining, words, excluded}:
1204      SpanDraw.feed(word, remaining, words, excluded)
1205
1206# The draw that a span ID draw's step feeds its next word to, while it waits
1207# for one.
1208def SpanStep.waiting(step: SpanStep) -> Maybe<&2, SpanDraw>:
1209  match step:
1210    case NeedSpanWord{draw}:
1211      Some{draw}
1212    case DrawnSpanId{id}:
1213      None{}
1214    case SpanFailed{error}:
1215      None{}
1216
1217# The span ID of a finished span ID draw, or why it failed, as
1218# TraceDraw.result; law span_id_ends shows that the word budget of
1219# SpanId.generate_with makes the unfinished case unreachable.
1220def SpanDraw.result(step: SpanStep) -> Result<&2, &2, GenerationError, SpanId>:
1221  match step:
1222    case DrawnSpanId{id}:
1223      Done{id}
1224    case SpanFailed{error}:
1225      Fail{error}
1226    case NeedSpanWord{draw}:
1227      Fail{ExhaustedSpanId{}}
1228
1229# Drive a span ID draw from a tape (Drive.run).
1230def SpanDraw.run(fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & SpanStep) ->
1231  List<&1, Result<&1, &1, U32 & String, U32>> & SpanStep:
1232  match current:
1233    case Tuple{tape, +step}:
1234      Drive.run(~SpanStep, ~SpanDraw, ~SpanStep.waiting, ~SpanDraw.next, fuel,
1235        (tape, (step, SpanStep.waiting(step))))
1236
1237# Whether the span ID draw in a driver's result has ended.
1238def SpanDraw.ended(result: List<&1, Result<&1, &1, U32 & String, U32>> & SpanStep) -> Bool:
1239  Drive.ended(~SpanStep, ~SpanDraw, ~SpanStep.waiting, result)
1240
1241# The source's final state with the span ID draw's result.
1242def SpanDraw.outcome(-S: Type, done: S & SpanStep) -> S & Result<&2, &2, GenerationError, SpanId>:
1243  Drive.outcome(~SpanStep, ~SpanId, ~SpanDraw.result, S, done)
1244
1245# A span ID alone, from a caller's source, as an OpenTelemetry SDK generates
1246# one once its sampler has decided. The source's shape is that of
1247# TraceId.generate_with. It reads two words per candidate, most significant
1248# first, for at most eight candidates, so at most 16 words; rejects all-zero
1249# candidates and `excluded`, when there is one, such as the span ID of a
1250# child's parent; and fails with SourceFailure or ExhaustedSpanId.
1251# Laws: span_id_tape, span_id_failure, span_id_candidate, span_id_ends,
1252# span_id_exhaustion and generated_span_id.
1253def SpanId.generate_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S,
1254  excluded: Maybe<&2, SpanId>) -> IO(S & Result<&2, &2, GenerationError, SpanId>):
1255  +start = SpanDraw.start(excluded)
1256  Drive.finished(~SpanStep, ~SpanId, ~SpanDraw.result, ~S, Drive.read(~SpanStep, ~SpanDraw, ~SpanStep.waiting,
1257    ~SpanDraw.next, ~S, ~read, 16n, (source, (start, SpanStep.waiting(start)))))
1258
1259# Generations
1260# -----------
1261
1262# The generation that a span ID draw's step gives, for a context of
1263# `trace_id` with the sampled indication `sampled`: waiting for the draw's
1264# next word, the context once the span ID is drawn, or the draw's failure.
1265def Step.of_span(step: SpanStep, trace_id: TraceId, sampled: Bool) -> Step:
1266  match step:
1267    case NeedSpanWord{draw}:
1268      NeedWord{DrawSpan{draw, trace_id, sampled}}
1269    case DrawnSpanId{id}:
1270      Created{Context.from_ids(trace_id, id, sampled)}
1271    case SpanFailed{error}:
1272      Failed{error}
1273
1274# The plan of a root's span ID, once its trace ID is drawn, and of a
1275# restart's: nothing to exclude, and the sampled indication that the root or
1276# the restart was given, as it is given.
1277def SpanPlan.root(trace_id: TraceId, sampled: Bool) -> SpanPlan:
1278  SpanPlan{None{}, trace_id, sampled}
1279
1280# The plan of a child's span ID: the parent's span ID excluded, the parent's
1281# trace ID, and the sampled indication that `sampling` resolves from the
1282# parent's.
1283def SpanPlan.child(+parent: Parent, sampling: Sampling) -> SpanPlan:
1284  SpanPlan{Some{Parent.span_id(parent)}, Parent.trace_id(parent), Sampling.resolve(sampling, Parent.is_sampled(parent))}
1285
1286# The generation that draws the span ID of a plan, from its first candidate.
1287def SpanPlan.draw(plan: SpanPlan) -> Step:
1288  match plan:
1289    case SpanPlan{excluded, trace_id, sampled}:
1290      Step.of_span(SpanDraw.start(excluded), trace_id, sampled)
1291
1292# The generation that a trace ID draw's step gives, for a root or a restart
1293# with the sampled indication `sampled`: waiting for the draw's next word,
1294# the root's span ID draw once the trace ID is drawn (SpanPlan.root), or the
1295# draw's failure.
1296def Step.of_trace(step: TraceStep, sampled: Bool) -> Step:
1297  match step:
1298    case NeedTraceWord{draw}:
1299      NeedWord{DrawTrace{draw, sampled}}
1300    case DrawnTraceId{id}:
1301      SpanPlan.draw(SpanPlan.root(id, sampled))
1302    case TraceFailed{error}:
1303      Failed{error}
1304
1305# The plan of a root: no trace ID to exclude, and the sampled indication
1306# `sampled`, as it is given.
1307def TracePlan.root(sampled: Bool) -> TracePlan:
1308  TracePlan{None{}, sampled}
1309
1310# The plan of a restart replacing `previous`: the received trace ID to
1311# exclude, and the sampled indication `sampled`, as it is given.
1312def TracePlan.restart(previous: RemoteContext, sampled: Bool) -> TracePlan:
1313  TracePlan{Some{RemoteContext.trace_id(previous)}, sampled}
1314
1315# The generation that draws the new trace of a plan: its trace ID, from the
1316# first candidate, then the span ID of the root's span plan (Step.of_trace).
1317def TracePlan.draw(plan: TracePlan) -> Step:
1318  match plan:
1319    case TracePlan{excluded, sampled}:
1320      Step.of_trace(TraceDraw.start(excluded), sampled)
1321
1322# A root draws the new trace of its plan (TracePlan.root).
1323def Draw.root(sampled: Bool) -> Step:
1324  TracePlan.draw(TracePlan.root(sampled))
1325
1326# A restart draws like a root but excludes the received trace ID
1327# (TracePlan.restart).
1328def Draw.restart(previous: RemoteContext, sampled: Bool) -> Step:
1329  TracePlan.draw(TracePlan.restart(previous, sampled))
1330
1331# A child draws the span ID of its plan (SpanPlan.child).
1332def Draw.child(+parent: Parent, sampling: Sampling) -> Step:
1333  SpanPlan.draw(SpanPlan.child(parent, sampling))
1334
1335# Feed the next source word, or the source's error, to the trace ID draw or
1336# the span ID draw that the generation runs. A source error ends the draw,
1337# and so the generation, at once with SourceFailure (law feed_failure).
1338def Draw.feed(word: Result<&1, &1, U32 & String, U32>, draw: Draw) -> Step:
1339  match draw:
1340    case DrawTrace{trace, sampled}:
1341      Step.of_trace(TraceDraw.next(word, trace), sampled)
1342    case DrawSpan{span, trace_id, sampled}:
1343      Step.of_span(SpanDraw.next(word, span), trace_id, sampled)
1344
1345# The draw that a generation's step feeds its next word to, while it waits
1346# for one.
1347def Step.waiting(step: Step) -> Maybe<&2, Draw>:
1348  match step:
1349    case NeedWord{draw}:
1350      Some{draw}
1351    case Created{context}:
1352      None{}
1353    case Failed{error}:
1354      None{}
1355
1356# The result of a finished generation. A generation that has not finished
1357# would report the identifier it was drawing; the root_ends, child_ends and
1358# restart_ends laws show that the word budgets of the operations below make
1359# those cases unreachable.
1360def Step.result(step: Step) -> Result<&2, &2, GenerationError, LocalContext>:
1361  match step:
1362    case Created{context}:
1363      Done{context}
1364    case Failed{error}:
1365      Fail{error}
1366    case NeedWord{DrawTrace{draw, sampled}}:
1367      Fail{ExhaustedTraceId{}}
1368    case NeedWord{DrawSpan{draw, trace_id, sampled}}:
1369      Fail{ExhaustedSpanId{}}
1370
1371# Drive a generation from a tape (Drive.run).
1372def Draw.run(fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & Step) ->
1373  List<&1, Result<&1, &1, U32 & String, U32>> & Step:
1374  match current:
1375    case Tuple{tape, +step}:
1376      Drive.run(~Step, ~Draw, ~Step.waiting, ~Draw.feed, fuel, (tape, (step, Step.waiting(step))))
1377
1378# Drive a generation from any source (Drive.read).
1379def Draw.read(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), fuel: Nat,
1380  current: S & Step) -> IO(S & Step):
1381  match current:
1382    case Tuple{state, +step}:
1383      Drive.read(~Step, ~Draw, ~Step.waiting, ~Draw.feed, ~S, ~read, fuel, (state, (step, Step.waiting(step))))
1384
1385# Whether the generation in a driver's result has ended.
1386def Draw.ended(result: List<&1, Result<&1, &1, U32 & String, U32>> & Step) -> Bool:
1387  Drive.ended(~Step, ~Draw, ~Step.waiting, result)
1388
1389# The source's final state with the generation's result.
1390def Draw.outcome(-S: Type, done: S & Step) -> S & Result<&2, &2, GenerationError, LocalContext>:
1391  Drive.outcome(~Step, ~LocalContext, ~Step.result, S, done)
1392
1393# Turn the driver's final step into the generation's result.
1394def Draw.finished(~S: Type, action: IO(S & Step)) -> IO(S & Result<&2, &2, GenerationError, LocalContext>):
1395  Drive.finished(~Step, ~LocalContext, ~Step.result, ~S, action)
1396
1397# The generation of the new trace of a plan: at most 48 words, eight trace ID
1398# candidates of four words and eight span ID candidates of two.
1399def TracePlan.generation(plan: TracePlan) -> Generation:
1400  Generation{48n, TracePlan.draw(plan)}
1401
1402# A root with the sampled indication `sampled`, as it is given
1403# (TracePlan.root).
1404def Generation.root(sampled: Bool) -> Generation:
1405  TracePlan.generation(TracePlan.root(sampled))
1406
1407# A restart replacing `previous`, with the sampled indication `sampled`, as a
1408# root (TracePlan.restart).
1409def Generation.restart(previous: RemoteContext, sampled: Bool) -> Generation:
1410  TracePlan.generation(TracePlan.restart(previous, sampled))
1411
1412# A child of `parent`: at most 16 words, eight span ID candidates.
1413def Generation.child(+parent: Parent, sampling: Sampling) -> Generation:
1414  Generation{16n, Draw.child(parent, sampling)}
1415
1416# Whether a step needs another word within `fuel` more words.
1417def Generation.needs.of(fuel: Nat, step: Step) -> Bool:
1418  match fuel step:
1419    case 0n _:
1420      False{}
1421    case 1n+p NeedWord{draw}:
1422      True{}
1423    case 1n+p Created{context}:
1424      False{}
1425    case 1n+p Failed{error}:
1426      False{}
1427
1428# Whether the generation needs another word: it has not ended, and its
1429# budget allows one more.
1430def Generation.needs(generation: Generation) -> Bool:
1431  match generation:
1432    case Generation{fuel, step}:
1433      Generation.needs.of(fuel, step)
1434
1435# The generation after `word`: the step it gives with one word less of
1436# budget, or, for a step that needs no word, the same step with none left.
1437def Generation.fed(fuel: Nat, step: Step, word: Result<&1, &1, U32 & String, U32>) -> Generation:
1438  match fuel step:
1439    case 0n other:
1440      Generation{0n, other}
1441    case 1n+p NeedWord{draw}:
1442      Generation{p, Draw.feed(word, draw)}
1443    case 1n+p Created{context}:
1444      Generation{0n, Created{context}}
1445    case 1n+p Failed{error}:
1446      Generation{0n, Failed{error}}
1447
1448# Feed the generation the next word of its source (see Draw.feed). A
1449# generation that needs no word ignores it.
1450def Generation.feed(generation: Generation, word: Result<&1, &1, U32 & String, U32>) -> Generation:
1451  match generation:
1452    case Generation{fuel, step}:
1453      Generation.fed(fuel, step, word)
1454
1455# The generation's result: the context it created, or why it failed. One that
1456# still needs a word once its budget is spent has exhausted its candidates;
1457# the root_ends, child_ends and restart_ends laws show that the budgets
1458# suffice.
1459def Generation.result(generation: Generation) -> Result<&2, &2, GenerationError, LocalContext>:
1460  match generation:
1461    case Generation{fuel, step}:
1462      Step.result(step)
1463
1464# Drive a generation from a caller's source, one word at a time
1465# (Draw.read), and hand back the source's final state with the result.
1466def Generation.run_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S,
1467  generation: Generation) -> IO(S & Result<&2, &2, GenerationError, LocalContext>):
1468  match generation:
1469    case Generation{fuel, step}:
1470      Draw.finished(~S, Draw.read(~S, ~read, fuel, (source, step)))
1471
1472# The context of a span ID generated from a source for an operation of
1473# `trace_id` with the sampled indication `sampled`, with the source's final
1474# state: the span ID's failure is the context's.
1475def Draw.span_context(-S: Type, +trace_id: TraceId, +sampled: Bool,
1476  done: S & Result<&2, &2, GenerationError, SpanId>) -> S & Result<&2, &2, GenerationError, LocalContext>:
1477  match done:
1478    case Tuple{state, Fail{error}}:
1479      (state, Fail{error})
1480    case Tuple{state, Done{span_id}}:
1481      (state, Done{Context.from_ids(trace_id, span_id, sampled)})
1482
1483# The local context of a span plan, from a caller's source: a span ID that
1484# excludes the plan's (SpanId.generate_with), and the context of the plan's
1485# trace ID and sampled indication with it.
1486def SpanPlan.generate_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S,
1487  plan: SpanPlan) -> IO(S & Result<&2, &2, GenerationError, LocalContext>):
1488  match plan:
1489    case SpanPlan{excluded, trace_id, sampled}:
1490      IO.bind(S & Result<&2, &2, GenerationError, SpanId>, S & Result<&2, &2, GenerationError, LocalContext>,
1491        SpanId.generate_with(~S, ~read, source, excluded),
1492        outcome => IO.pure(S & Result<&2, &2, GenerationError, LocalContext>,
1493          Draw.span_context(S, trace_id, sampled, outcome)))
1494
1495# The span ID of a root or a restart with the sampled indication `sampled`,
1496# from the source's next state, once its trace ID is generated: the trace
1497# ID's failure is the generation's, and otherwise the local context of the
1498# root's span plan (SpanPlan.root).
1499def Draw.root_span_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), sampled: Bool,
1500  outcome: S & Result<&2, &2, GenerationError, TraceId>) -> IO(S & Result<&2, &2, GenerationError, LocalContext>):
1501  match outcome:
1502    case Tuple{state, Fail{error}}:
1503      IO.pure(S & Result<&2, &2, GenerationError, LocalContext>, (state, Fail{error}))
1504    case Tuple{state, Done{trace_id}}:
1505      SpanPlan.generate_with(~S, ~read, state, SpanPlan.root(trace_id, sampled))
1506
1507# The local context of the new trace of a plan, from a caller's source: a
1508# trace ID that excludes the plan's (TraceId.generate_with), then, from the
1509# source's next state, the span ID of the root's span plan with the plan's
1510# sampled indication (Draw.root_span_with).
1511def TracePlan.generate_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S,
1512  plan: TracePlan) -> IO(S & Result<&2, &2, GenerationError, LocalContext>):
1513  match plan:
1514    case TracePlan{excluded, sampled}:
1515      IO.bind(S & Result<&2, &2, GenerationError, TraceId>, S & Result<&2, &2, GenerationError, LocalContext>,
1516        TraceId.generate_with(~S, ~read, source, excluded), outcome => Draw.root_span_with(~S, ~read, sampled, outcome))
1517
1518# Generated contexts from a caller's source. `read` returns the source's next
1519# state with each word result. The source is trusted to be random: a generated
1520# trace ID asserts random-trace-id. A root is a trace ID, with none to
1521# exclude, then a span ID: TraceId.generate_with, then SpanId.generate_with
1522# from the source's next state (TracePlan.root and TracePlan.generate_with).
1523# It reads at most 48 words and has the sampled indication `sampled`, as it
1524# is given: no default applies here, and False gives an unsampled root,
1525# emitted with flags 02, as Context.continue_or_start_with starts one by
1526# default (spec #41, "Sampling decision when starting a trace"). Laws:
1527# root_composed, root_tape, root_ends, root_exhaustion and generated_root.
1528def Context.root_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, sampled: Bool) ->
1529  IO(S & Result<&2, &2, GenerationError, LocalContext>):
1530  TracePlan.generate_with(~S, ~read, source, TracePlan.root(sampled))
1531
1532# A generated child of `parent` from a caller's source: the local context of
1533# its span plan (SpanPlan.child), a span ID that excludes the parent's, with
1534# the parent's trace ID and the sampled indication that `sampling` resolves.
1535# It reads at most 16 words. Laws: child_composed, child_tape, child_ends,
1536# child_exhaustion and generated_child.
1537def Context.child_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S,
1538  parent: Parent, sampling: Sampling) -> IO(S & Result<&2, &2, GenerationError, LocalContext>):
1539  SpanPlan.generate_with(~S, ~read, source, SpanPlan.child(parent, sampling))
1540
1541# A generated restart replacing `previous` from a caller's source: a trace ID
1542# that excludes the received one, then a span ID, as for a root, with the
1543# sampled indication `sampled` (TracePlan.restart and
1544# TracePlan.generate_with). It reads at most 48 words. Laws:
1545# restart_composed, restart_tape, restart_ends and generated_restart.
1546def Context.restart_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S,
1547  previous: RemoteContext, sampled: Bool) -> IO(S & Result<&2, &2, GenerationError, LocalContext>):
1548  TracePlan.generate_with(~S, ~read, source, TracePlan.restart(previous, sampled))
1549
1550# A deterministic source that replays a tape of word results.
1551def Source.tape(tape: List<&1, Result<&1, &1, U32 & String, U32>>) ->
1552  IO(List<&1, Result<&1, &1, U32 & String, U32>> & Result<&1, &1, U32 & String, U32>):
1553  IO.pure(List<&1, Result<&1, &1, U32 & String, U32>> & Result<&1, &1, U32 & String, U32>, Tape.next(tape))
1554
1555# Error messages
1556# ==============
1557#
1558# Readable names for the error constructors, for logs and test output. They
1559# include no text received from another participant, except the two
1560# hexadecimal digits of an unsupported version.
1561
1562# The name of a codec or ID error, with its offset or, for an unsupported
1563# version, its two digits. ZeroId names the field: ZeroTraceId, ZeroParentId or
1564# ZeroSpanId.
1565def Error.show(error: Error) -> String:
1566  match error:
1567    case UnexpectedEnd{offset}:
1568      "UnexpectedEnd at " ++ Nat.show(offset)
1569    case InvalidHex{offset}:
1570      "InvalidHex at " ++ Nat.show(offset)
1571    case InvalidByte{offset}:
1572      "InvalidByte at " ++ Nat.show(offset)
1573    case ExpectedSeparator{offset}:
1574      "ExpectedSeparator at " ++ Nat.show(offset)
1575    case TrailingInput{}:
1576      "TrailingInput"
1577    case ForbiddenVersion{}:
1578      "ForbiddenVersion"
1579    case UnsupportedVersion{version}:
1580      "UnsupportedVersion " ++ version
1581    case ZeroId{TraceIdField{}}:
1582      "ZeroTraceId"
1583    case ZeroId{ParentIdField{}}:
1584      "ZeroParentId"
1585    case ZeroId{SpanIdField{}}:
1586      "ZeroSpanId"
1587    case ControlCharacter{offset}:
1588      "ControlCharacter at " ++ Nat.show(offset)
1589
1590# The name of a context creation error.
1591def ContextError.show(error: ContextError) -> String:
1592  match error:
1593    case ReusedSpanId{}:
1594      "ReusedSpanId"
1595    case ReusedTraceId{}:
1596      "ReusedTraceId"
1597
1598# The name of a generation error; a source failure adds the source's code and
1599# message.
1600def GenerationError.show(error: GenerationError) -> String:
1601  match error:
1602    case SourceFailure{code, message}:
1603      "SourceFailure " ++ U32.show(code) ++ " " ++ message
1604    case ExhaustedTraceId{}:
1605      "ExhaustedTraceId"
1606    case ExhaustedSpanId{}:
1607      "ExhaustedSpanId"
1608
1609# Limits
1610# ======
1611#
1612# Budgets, in UTF-8 octets, for the traceparent and tracestate values the
1613# package reads and the tracestate it emits (spec #1, "Tracestate policy and
1614# resource bounds").
1615
1616# Why a limit configuration was refused. The first failing rule is reported:
1617#   TraceParentInputTooSmall{}   the traceparent input budget is below 55
1618#   TraceStateOutputTooSmall{}   the tracestate output budget is below 512
1619#   TraceStateInputTooSmall{}    the tracestate input budget is below the output
1620#                                budget
1621type LimitsError is Data:
1622  TraceParentInputTooSmall{}
1623  TraceStateOutputTooSmall{}
1624  TraceStateInputTooSmall{}
1625
1626# The rules of a configuration, which must accept its own emitted
1627# representation: a traceparent input budget of at least 55 octets, the length
1628# of a v00 value, and a tracestate input budget no smaller than an output
1629# budget of at least 512 octets (spec #1, "Tracestate policy and resource
1630# bounds"; the 512-octet minimum comes from #8; law limits_bounds).
1631def Limits.is_valid(traceparent_input: Nat, tracestate_input: Nat, +tracestate_output: Nat) -> Bool:
1632  Bool.and(Nat.is_ge(traceparent_input, 55n),
1633    Bool.and(Nat.is_ge(tracestate_output, 512n), Nat.is_ge(tracestate_input, tracestate_output)))
1634
1635# Budgets in UTF-8 octets. The input budgets bound a received traceparent value
1636# and a combined tracestate value; the output budget is the most an emitted
1637# tracestate may take. `evidence` is the proof of Limits.is_valid, so every
1638# Limits value follows the rules.
1639type Limits is Data:
1640  Limits{
1641    traceparent_input: Nat,
1642    tracestate_input: Nat,
1643    tracestate_output: Nat,
1644    evidence: {Limits.is_valid(traceparent_input, tracestate_input, tracestate_output) == True{} : Bool}
1645  }
1646
1647# The first rule a refused configuration breaks.
1648def Limits.error(traceparent_input: Nat, tracestate_output: Nat) -> LimitsError:
1649  Bool.pick(LimitsError, Nat.is_lt(traceparent_input, 55n), TraceParentInputTooSmall{},
1650    Bool.pick(LimitsError, Nat.is_lt(tracestate_output, 512n), TraceStateOutputTooSmall{},
1651      TraceStateInputTooSmall{}))
1652
1653# The configuration, when the check found it valid.
1654def Limits.new.checked(traceparent_input: Nat, tracestate_input: Nat, tracestate_output: Nat, valid: Bool,
1655  evidence: {Limits.is_valid(traceparent_input, tracestate_input, tracestate_output) == valid : Bool}) ->
1656  Result<&2, &2, LimitsError, Limits>:
1657  match valid:
1658    case True{}:
1659      Done{Limits{traceparent_input, tracestate_input, tracestate_output, evidence}}
1660    case False{}:
1661      Fail{Limits.error(traceparent_input, tracestate_output)}
1662
1663# Validate a configuration; budgets count UTF-8 octets (laws limits_new and
1664# limits_fields).
1665def Limits.new(+traceparent_input: Nat, +tracestate_input: Nat, +tracestate_output: Nat) ->
1666  Result<&2, &2, LimitsError, Limits>:
1667  Limits.new.checked(traceparent_input, tracestate_input, tracestate_output,
1668    Limits.is_valid(traceparent_input, tracestate_input, tracestate_output), {==})
1669
1670# 32 KiB for each received value and 512 octets for an emitted tracestate
1671# (law default_limits). The 512-octet output budget is this package's capacity
1672# policy, not a W3C maximum.
1673def Limits.default() -> Limits:
1674  Limits{32768n, 32768n, 512n, {==}}
1675
1676# The most octets a received traceparent value may take.
1677def Limits.traceparent_input(limits: Limits) -> Nat:
1678  match limits:
1679    case Limits{traceparent_input, tracestate_input, tracestate_output, evidence}:
1680      traceparent_input
1681
1682# The most octets a combined tracestate value may take, including the commas
1683# that join repeated fields.
1684def Limits.tracestate_input(limits: Limits) -> Nat:
1685  match limits:
1686    case Limits{traceparent_input, tracestate_input, tracestate_output, evidence}:
1687      tracestate_input
1688
1689# The most octets an emitted tracestate may take.
1690def Limits.tracestate_output(limits: Limits) -> Nat:
1691  match limits:
1692    case Limits{traceparent_input, tracestate_input, tracestate_output, evidence}:
1693      tracestate_output
1694
1695# The name of a limits error.
1696def LimitsError.show(error: LimitsError) -> String:
1697  match error:
1698    case TraceParentInputTooSmall{}:
1699      "TraceParentInputTooSmall"
1700    case TraceStateOutputTooSmall{}:
1701      "TraceStateOutputTooSmall"
1702    case TraceStateInputTooSmall{}:
1703      "TraceStateInputTooSmall"
1704
1705# Tracestate: characters, keys and values
1706# =======================================
1707#
1708# The Level 2 grammar of W3C 3.3.2.2. The character classes are written with
1709# the code point ranges of the standard's ABNF.
1710
1711# Why a tracestate key, value or received member was refused:
1712#   MissingEquals{}   a nonempty member has no "="
1713#   InvalidKey{}      the text before the first "=" is not a key
1714#   InvalidValue{}    the text after it, without trailing optional whitespace,
1715#                     is not a value
1716type EntryError is Data:
1717  MissingEquals{}
1718  InvalidKey{}
1719  InvalidValue{}
1720
1721# Whether a code point lies between two others, both included.
1722def StateChar.in_range(+code: U32, low: U32, high: U32) -> Bool:
1723  Bool.and(U32.is_ge(code, low), U32.is_le(code, high))
1724
1725# lcalpha / DIGIT: a lowercase ASCII letter (%x61-7A) or a digit (%x30-39),
1726# the first character of a key.
1727def StateChar.is_key_start(char: Char) -> Bool:
1728  match char:
1729    case Chr{+code}:
1730      Bool.or(StateChar.in_range(code, 97, 122), StateChar.in_range(code, 48, 57))
1731
1732# keychar: lcalpha / DIGIT / "_" / "-" / "*" / "/" / "@".
1733def StateChar.is_key(+char: Char) -> Bool:
1734  Bool.or(StateChar.is_key_start(char), Bool.or(Char.is_eq(char, '_'), Bool.or(Char.is_eq(char, '-'),
1735    Bool.or(Char.is_eq(char, '*'), Bool.or(Char.is_eq(char, '/'), Char.is_eq(char, '@'))))))
1736
1737# nblk-chr: %x21-2B / %x2D-3C / %x3E-7E, printable ASCII other than space,
1738# "," and "=". A value ends with one of these.
1739def StateChar.is_value_end(char: Char) -> Bool:
1740  match char:
1741    case Chr{+code}:
1742      Bool.or(StateChar.in_range(code, 33, 43), Bool.or(StateChar.in_range(code, 45, 60),
1743        StateChar.in_range(code, 62, 126)))
1744
1745# chr: %x20 / nblk-chr, a character of a value: nblk-chr or a space.
1746def StateChar.is_value(+char: Char) -> Bool:
1747  Bool.or(Char.is_eq(char, ' '), StateChar.is_value_end(char))
1748
1749# OWS: a space or a horizontal tab (RFC 9110, section 5.6.3).
1750def StateChar.is_ows(+char: Char) -> Bool:
1751  Bool.or(Char.is_eq(char, ' '), Char.is_eq(char, '\t'))
1752
1753# Every remaining character is a key character, and at most `room` remain.
1754# The recursion stops once the room is used up, so a huge invalid key is not
1755# read to its end.
1756def StateKey.valid.rest(text: String, room: Nat) -> Bool:
1757  match text:
1758    case SNil{}:
1759      True{}
1760    case SCon{char, tail}:
1761      match room:
1762        case 0n:
1763          False{}
1764        case 1n+left:
1765          Bool.and(StateChar.is_key(char), StateKey.valid.rest(tail, left))
1766
1767# key = ( lcalpha / DIGIT ) 0*255( keychar ): 1 to 256 characters (W3C
1768# 3.3.2.2.1). Level 1's tenant@system restriction does not apply.
1769def StateKey.is_valid(text: String) -> Bool:
1770  match text:
1771    case SNil{}:
1772      False{}
1773    case SCon{char, tail}:
1774      Bool.and(StateChar.is_key_start(char), StateKey.valid.rest(tail, 255n))
1775
1776# `char` is a value character followed by `tail`, of which at most `room`
1777# characters are allowed; the last character is not a space.
1778def StateValue.valid.go(tail: String, char: Char, room: Nat) -> Bool:
1779  match tail:
1780    case SNil{}:
1781      StateChar.is_value_end(char)
1782    case SCon{next, rest}:
1783      match room:
1784        case 0n:
1785          False{}
1786        case 1n+left:
1787          Bool.and(StateChar.is_value(char), StateValue.valid.go(rest, next, left))
1788
1789# value = 0*255( chr ) nblk-chr: 1 to 256 printable ASCII characters other
1790# than "," and "=", the last of which is not a space (W3C 3.3.2.2.2).
1791def StateValue.is_valid(text: String) -> Bool:
1792  match text:
1793    case SNil{}:
1794      False{}
1795    case SCon{char, tail}:
1796      StateValue.valid.go(tail, char, 255n)
1797
1798# A tracestate key, naming the vendor that owns an entry. `evidence` proves the
1799# Level 2 key grammar for `text`, so a StateKey is always valid: build one with
1800# StateKey.parse (the negative fixture tests/reject/invalid_state_key.bend
1801# shows that direct construction with a wrong text does not compile).
1802type StateKey is Data:
1803  StateKey{text: String, evidence: {StateKey.is_valid(text) == True{} : Bool}}
1804
1805# A tracestate value, opaque to every other vendor. `evidence` proves the
1806# Level 2 value grammar for `text`. Leading spaces are part of the value.
1807type StateValue is Data:
1808  StateValue{text: String, evidence: {StateValue.is_valid(text) == True{} : Bool}}
1809
1810# The key, when the check found the text valid.
1811def StateKey.parse.checked(text: String, valid: Bool, evidence: {StateKey.is_valid(text) == valid : Bool}) ->
1812  Result<&2, &2, EntryError, StateKey>:
1813  match valid:
1814    case True{}:
1815      Done{StateKey{text, evidence}}
1816    case False{}:
1817      Fail{InvalidKey{}}
1818
1819# Accept exactly a Level 2 key, or fail with InvalidKey. Nothing is trimmed
1820# or folded (laws key_parse, key_roundtrip and key_separators).
1821def StateKey.parse(+text: String) -> Result<&2, &2, EntryError, StateKey>:
1822  StateKey.parse.checked(text, StateKey.is_valid(text), {==})
1823
1824# The key's text.
1825def StateKey.to_string(key: StateKey) -> String:
1826  match key:
1827    case StateKey{text, evidence}:
1828      text
1829
1830# The value, when the check found the text valid.
1831def StateValue.parse.checked(text: String, valid: Bool, evidence: {StateValue.is_valid(text) == valid : Bool}) ->
1832  Result<&2, &2, EntryError, StateValue>:
1833  match valid:
1834    case True{}:
1835      Done{StateValue{text, evidence}}
1836    case False{}:
1837      Fail{InvalidValue{}}
1838
1839# Accept exactly a Level 2 value, leading spaces included, or fail with
1840# InvalidValue. No whitespace is trimmed here, so a trailing space is refused
1841# (laws value_parse, value_roundtrip and value_separators).
1842def StateValue.parse(+text: String) -> Result<&2, &2, EntryError, StateValue>:
1843  StateValue.parse.checked(text, StateValue.is_valid(text), {==})
1844
1845# The value's text.
1846def StateValue.to_string(value: StateValue) -> String:
1847  match value:
1848    case StateValue{text, evidence}:
1849      text
1850
1851# The name of an entry error.
1852def EntryError.show(error: EntryError) -> String:
1853  match error:
1854    case MissingEquals{}:
1855      "MissingEquals"
1856    case InvalidKey{}:
1857      "InvalidKey"
1858    case InvalidValue{}:
1859      "InvalidValue"
1860
1861# Tracestate: entries, states and lookups
1862# =======================================
1863#
1864# A state is the ordered list of vendor entries of a tracestate, leftmost first
1865# (W3C 3.3.3), with distinct keys and at most 32 entries.
1866
1867# Why a received tracestate value was discarded:
1868#   StateTooLarge{}               the combined value exceeds its input budget
1869#   TooManyMembers{}              a 33rd nonempty member was reached
1870#   InvalidEntry{member, error}   a member is invalid; `member` numbers the
1871#                                 comma-separated members of the combined value
1872#                                 from zero, empty members included
1873# Discarding the state never invalidates a valid traceparent (spec #1).
1874type StateError is Data:
1875  StateTooLarge{}
1876  TooManyMembers{}
1877  InvalidEntry{member: Nat, error: EntryError}
1878
1879# One vendor's entry: a key and its value.
1880type StateEntry is Data:
1881  StateEntry{key: StateKey, value: StateValue}
1882
1883# The entry's key.
1884def StateEntry.key(entry: StateEntry) -> StateKey:
1885  match entry:
1886    case StateEntry{key, value}:
1887      key
1888
1889# The entry's value.
1890def StateEntry.value(entry: StateEntry) -> StateValue:
1891  match entry:
1892    case StateEntry{key, value}:
1893      value
1894
1895# The text of the entry's key.
1896def StateEntry.key_text(entry: StateEntry) -> String:
1897  StateKey.to_string(StateEntry.key(entry))
1898
1899# `key=value`, as the entry is sent.
1900def StateEntry.format(entry: StateEntry) -> String:
1901  match entry:
1902    case StateEntry{key, value}:
1903      StateKey.to_string(key) ++ "=" ++ StateValue.to_string(value)
1904
1905# Whether one of the entries has this key.
1906def Entries.has_key(entries: List<&2, StateEntry>, +key: String) -> Bool:
1907  match entries:
1908    case Nil{}:
1909      False{}
1910    case Con{entry, rest}:
1911      Bool.or(String.eq(StateEntry.key_text(entry), key), Entries.has_key(rest, key))
1912
1913# No entry repeats the key of an entry before it; `seen` holds the entries
1914# already passed. This is the order in which the reading machine checks keys.
1915def Entries.unique(entries: List<&2, StateEntry>, +seen: List<&2, StateEntry>) -> Bool:
1916  match entries:
1917    case Nil{}:
1918      True{}
1919    case Con{+entry, rest}:
1920      Bool.and(Bool.not(Entries.has_key(seen, StateEntry.key_text(entry))),
1921        Entries.unique(rest, List.append(&2, StateEntry, seen, Con{entry, Nil{}})))
1922
1923# Distinct keys and at most 32 entries (W3C 3.3.2 and 3.3.3).
1924def TraceState.is_valid(+entries: List<&2, StateEntry>) -> Bool:
1925  Bool.and(Entries.unique(entries, Nil{}), Nat.is_le(List.length(&2, StateEntry, entries), 32n))
1926
1927# Ordered vendor state: at most 32 entries with distinct keys, leftmost first.
1928# `evidence` proves both properties, so every TraceState has them (law
1929# state_valid).
1930type TraceState is Data:
1931  TraceState{entries: List<&2, StateEntry>, evidence: {TraceState.is_valid(entries) == True{} : Bool}}
1932
1933# The state with no entries. It formats as "".
1934def TraceState.empty() -> TraceState:
1935  TraceState{Nil{}, {==}}
1936
1937# The entries in order, leftmost first.
1938def TraceState.entries(state: TraceState) -> List<&2, StateEntry>:
1939  match state:
1940    case TraceState{entries, evidence}:
1941      entries
1942
1943# Whether the state has no entries.
1944def TraceState.is_empty(state: TraceState) -> Bool:
1945  List.is_empty(&2, StateEntry, TraceState.entries(state))
1946
1947# The value of `entry` when its key matched, or the result for the rest.
1948def Entries.get.put(entry: StateEntry, rest: Maybe<&2, StateValue>, hit: Bool) -> Maybe<&2, StateValue>:
1949  match hit:
1950    case True{}:
1951      Some{StateEntry.value(entry)}
1952    case False{}:
1953      rest
1954
1955# The value of the first entry with this key.
1956def Entries.get(entries: List<&2, StateEntry>, +key: String) -> Maybe<&2, StateValue>:
1957  match entries:
1958    case Nil{}:
1959      None{}
1960    case Con{+entry, rest}:
1961      Entries.get.put(entry, Entries.get(rest, key), String.eq(StateEntry.key_text(entry), key))
1962
1963# The value of the entry with this key, if there is one (laws get_entry and
1964# get_absent). The key is validated, so a lookup never needs to check it.
1965def TraceState.get(state: TraceState, key: StateKey) -> Maybe<&2, StateValue>:
1966  Entries.get(TraceState.entries(state), StateKey.to_string(key))
1967
1968# Each entry after the first, preceded by its comma.
1969def Entries.format.rest(entries: List<&2, StateEntry>) -> String:
1970  match entries:
1971    case Nil{}:
1972      ""
1973    case Con{entry, rest}:
1974      "," ++ StateEntry.format(entry) ++ Entries.format.rest(rest)
1975
1976# The entries as `key=value`, joined by commas.
1977def Entries.format(entries: List<&2, StateEntry>) -> String:
1978  match entries:
1979    case Nil{}:
1980      ""
1981    case Con{entry, rest}:
1982      StateEntry.format(entry) ++ Entries.format.rest(rest)
1983
1984# The normalized value: the entries in order, joined by commas, with no
1985# optional whitespace. The empty state formats as "" (laws state_roundtrip and
1986# first_wins).
1987def TraceState.format(state: TraceState) -> String:
1988  Entries.format(TraceState.entries(state))
1989
1990# Tracestate: budgets
1991# ===================
1992#
1993# A received value is measured in UTF-8 octets before it is read. Measuring
1994# stops at the first character past the budget, so an oversized value is never
1995# read to its end.
1996
1997# The UTF-8 octets of a character. Bend characters are Unicode code points, so
1998# this is the size of the character's UTF-8 encoding: 1 to 4.
1999def Utf8.width(char: Char) -> Nat:
2000  match char:
2001    case Chr{+code}:
2002      Bool.pick(Nat, U32.is_lt(code, 128), 1n,
2003        Bool.pick(Nat, U32.is_lt(code, 2048), 2n,
2004          Bool.pick(Nat, U32.is_lt(code, 65536), 3n, 4n)))
2005
2006# The UTF-8 octets of a text, in which the laws state every budget. Emission
2007# measures keys and values with it, at most 256 characters each; parsing
2008# measures received text with Utf8.left instead, which stops counting past
2009# the budget.
2010def Utf8.length(text: String) -> Nat:
2011  match text:
2012    case SNil{}:
2013      0n
2014    case SCon{char, tail}:
2015      Nat.add(Utf8.width(char), Utf8.length(tail))
2016
2017# What is left of a budget after taking `need` octets, or None when less
2018# remains.
2019def Budget.take(need: Nat, budget: Nat) -> Maybe<&2, Nat>:
2020  match need budget:
2021    case 0n _:
2022      Some{budget}
2023    case 1n+more 0n:
2024      None{}
2025    case 1n+more 1n+left:
2026      Budget.take(more, left)
2027
2028# What is left of a budget after a text, or None once the text exceeds it.
2029# Measuring stops at the first character beyond the budget, and a None budget
2030# stays None.
2031def Utf8.left(text: String, budget: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
2032  match text budget:
2033    case _ None{}:
2034      None{}
2035    case SNil{} Some{left}:
2036      Some{left}
2037    case SCon{char, tail} Some{left}:
2038      Utf8.left(tail, Budget.take(Utf8.width(char), left))
2039
2040# Fields after the first are measured with the comma that joins them. Once the
2041# budget is exceeded, no further field is visited.
2042def Utf8.left_more(fields: List<&2, String>, budget: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
2043  match fields budget:
2044    case Nil{} _:
2045      budget
2046    case Con{field, rest} None{}:
2047      None{}
2048    case Con{field, rest} Some{left}:
2049      Utf8.left_more(rest, Utf8.left(field, Utf8.left(",", Some{left})))
2050
2051# What is left of a budget after repeated fields and the commas that join
2052# them.
2053def Utf8.left_fields(fields: List<&2, String>, budget: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
2054  match fields:
2055    case Nil{}:
2056      budget
2057    case Con{field, rest}:
2058      Utf8.left_more(rest, Utf8.left(field, budget))
2059
2060# Tracestate: the reading machine
2061# ===============================
2062#
2063# TraceState.parse measures the combined value against its budget, then reads
2064# it once from left to right, one character at a time. A comma ends the
2065# current member; the machine validates each nonempty member when it ends,
2066# counts it toward the 32 allowed, and keeps it only when its key is new.
2067# Reading stops at the first problem.
2068
2069# Where reading the current member stands: before its key, with only optional
2070# whitespace so far; inside its key; or inside its value. Characters read are
2071# kept most recent first, so each one costs a single step.
2072type Member is Data:
2073  Blank{}
2074  InKey{text: String}
2075  InValue{key: String, text: String}
2076
2077# A tracestate being read: the members ended so far, empty ones included; how
2078# many more nonempty members are allowed; the current member; and the first
2079# entry of each key, in reading order. Stopped holds the first problem found.
2080# The scan and its helpers are internal.
2081type Scan is Data:
2082  Scanning{member: Nat, room: Nat, current: Member, entries: List<&2, StateEntry>}
2083  Stopped{error: StateError}
2084
2085# A value's characters arrive most recent first. Restoring them skips optional
2086# whitespace until the first other character, then keeps every character, so
2087# the value comes back in reading order without its trailing whitespace.
2088def Value.restore.step(kept: Bool, ows: Bool, char: Char, value: String) -> Bool & String:
2089  match kept:
2090    case True{}:
2091      (True{}, SCon{char, value})
2092    case False{}:
2093      match ows:
2094        case True{}:
2095          (False{}, value)
2096        case False{}:
2097          (True{}, SCon{char, value})
2098
2099# The restoring loop: one character at a time, with the state (whether a
2100# character was kept yet, the value so far).
2101def Value.restore.go(text: String, state: Bool & String) -> String:
2102  match text:
2103    case SNil{}:
2104      (kept, value) = state
2105      value
2106    case SCon{+char, tail}:
2107      (kept, value) = state
2108      Value.restore.go(tail, Value.restore.step(kept, StateChar.is_ows(char), char, value))
2109
2110# The value in reading order without its trailing optional whitespace.
2111def Value.restore(text: String) -> String:
2112  Value.restore.go(text, (False{}, ""))
2113
2114# A character of a member that has no key yet: optional whitespace is
2115# skipped, an "=" gives the member an empty key, which validation refuses, and
2116# anything else starts the key.
2117def Member.start(ows: Bool, equals: Bool, char: Char) -> Member:
2118  match ows:
2119    case True{}:
2120      Blank{}
2121    case False{}:
2122      match equals:
2123        case True{}:
2124          InValue{"", ""}
2125        case False{}:
2126          InKey{SCon{char, SNil{}}}
2127
2128# A character inside a key: the first "=" ends the key, anything else extends
2129# it. Key characters are validated when the member ends.
2130def Member.key(equals: Bool, char: Char, text: String) -> Member:
2131  match equals:
2132    case True{}:
2133      InValue{String.reverse(text), ""}
2134    case False{}:
2135      InKey{SCon{char, text}}
2136
2137# A character other than a comma extends the current member. Inside a value
2138# every character is kept; validation refuses those the grammar excludes.
2139def Member.push(+char: Char, current: Member) -> Member:
2140  match current:
2141    case Blank{}:
2142      Member.start(StateChar.is_ows(char), Char.is_eq(char, '='), char)
2143    case InKey{text}:
2144      Member.key(Char.is_eq(char, '='), char, text)
2145    case InValue{key, text}:
2146      InValue{key, SCon{char, text}}
2147
2148# Validate the key and value texts of a member that ended. An invalid key is
2149# reported before an invalid value.
2150def Scan.validate(key: String, value: String) -> Result<&2, &2, EntryError, StateEntry>:
2151  do Result<&2, &2, EntryError, StateEntry>:
2152    parsed_key : StateKey <- StateKey.parse(key)
2153    parsed_value : StateValue <- StateValue.parse(value)
2154    return StateEntry{parsed_key, parsed_value}
2155
2156# Keep the entries unchanged when the key was present; otherwise add the
2157# entry at the end.
2158def Entries.add.if(entries: List<&2, StateEntry>, entry: StateEntry, present: Bool) -> List<&2, StateEntry>:
2159  match present:
2160    case True{}:
2161      entries
2162    case False{}:
2163      List.append(&2, StateEntry, entries, Con{entry, Nil{}})
2164
2165# Keep only the first entry of each key (spec #1, "Preserve the first
2166# occurrence of a duplicate key").
2167def Entries.add(+entries: List<&2, StateEntry>, +entry: StateEntry) -> List<&2, StateEntry>:
2168  Entries.add.if(entries, entry, Entries.has_key(entries, StateEntry.key_text(entry)))
2169
2170# A valid member counts toward the 32 allowed before duplicates are dropped
2171# (spec #1); with no room left, the state is discarded with TooManyMembers.
2172def Scan.keep(room: Nat, member: Nat, entry: StateEntry, entries: List<&2, StateEntry>) -> Scan:
2173  match room:
2174    case 0n:
2175      Stopped{TooManyMembers{}}
2176    case 1n+left:
2177      Scanning{1n+member, left, Blank{}, Entries.add(entries, entry)}
2178
2179# A member that ended: an invalid one stops reading with its number and
2180# reason; a valid one is counted and kept.
2181def Scan.entry(parsed: Result<&2, &2, EntryError, StateEntry>, member: Nat, room: Nat,
2182  entries: List<&2, StateEntry>) -> Scan:
2183  match parsed:
2184    case Fail{error}:
2185      Stopped{InvalidEntry{member, error}}
2186    case Done{entry}:
2187      Scan.keep(room, member, entry, entries)
2188
2189# The current member ends at a comma or with the value. An empty member, or
2190# one of optional whitespace only, is ignored but still numbered; a member
2191# without "=" is refused; otherwise its key and value are validated, trailing
2192# optional whitespace left out of the value.
2193def Scan.close(member: Nat, room: Nat, current: Member, entries: List<&2, StateEntry>) -> Scan:
2194  match current:
2195    case Blank{}:
2196      Scanning{1n+member, room, Blank{}, entries}
2197    case InKey{text}:
2198      Stopped{InvalidEntry{member, MissingEquals{}}}
2199    case InValue{key, text}:
2200      Scan.entry(Scan.validate(key, Value.restore(text)), member, room, entries)
2201
2202# One character of a scan that is still reading: a comma ends the member, and
2203# anything else extends it.
2204def Scan.read(comma: Bool, char: Char, member: Nat, room: Nat, current: Member,
2205  entries: List<&2, StateEntry>) -> Scan:
2206  match comma:
2207    case True{}:
2208      Scan.close(member, room, current, entries)
2209    case False{}:
2210      Scanning{member, room, Member.push(char, current), entries}
2211
2212# Read one character, unless the scan has stopped.
2213def Scan.char(+char: Char, scan: Scan) -> Scan:
2214  match scan:
2215    case Stopped{error}:
2216      Stopped{error}
2217    case Scanning{member, room, current, entries}:
2218      Scan.read(Char.is_eq(char, ','), char, member, room, current, entries)
2219
2220# Read a text one character at a time, stopping at the first problem. This is
2221# a loop (a tail call), so its depth does not grow with the text.
2222def Scan.text(text: String, scan: Scan) -> Scan:
2223  match text scan:
2224    case _ Stopped{error}:
2225      Stopped{error}
2226    case SNil{} Scanning{member, room, current, entries}:
2227      Scanning{member, room, current, entries}
2228    case SCon{char, tail} Scanning{member, room, current, entries}:
2229      Scan.text(tail, Scan.char(char, Scanning{member, room, current, entries}))
2230
2231# Fields after the first are read after the comma that joins them.
2232def Scan.more(fields: List<&2, String>, scan: Scan) -> Scan:
2233  match fields:
2234    case Nil{}:
2235      scan
2236    case Con{field, rest}:
2237      Scan.more(rest, Scan.text(field, Scan.char(',', scan)))
2238
2239# Read repeated fields as their comma-joined combination.
2240def Scan.fields(fields: List<&2, String>, scan: Scan) -> Scan:
2241  match fields:
2242    case Nil{}:
2243      scan
2244    case Con{field, rest}:
2245      Scan.more(rest, Scan.text(field, scan))
2246
2247# The scan of a new value: no member ended, 32 allowed, nothing kept.
2248def Scan.start() -> Scan:
2249  Scanning{0n, 32n, Blank{}, Nil{}}
2250
2251# The scan keeps only the first entry of each key and stops at a 33rd member,
2252# so this check is not expected to fail: the laws prove it passes for
2253# normalized values, and the corpus exercises the rest. A failure would be
2254# reported as too many members.
2255def Scan.state(entries: List<&2, StateEntry>, valid: Bool,
2256  evidence: {TraceState.is_valid(entries) == valid : Bool}) -> Result<&2, &2, StateError, TraceState>:
2257  match valid:
2258    case True{}:
2259      Done{TraceState{entries, evidence}}
2260    case False{}:
2261      Fail{TooManyMembers{}}
2262
2263# The state read, once the last member has ended. TraceState.is_valid is
2264# checked here to build the state's evidence.
2265def Scan.result(scan: Scan) -> Result<&2, &2, StateError, TraceState>:
2266  match scan:
2267    case Stopped{error}:
2268      Fail{error}
2269    case Scanning{member, room, current, +entries}:
2270      Scan.state(entries, TraceState.is_valid(entries), {==})
2271
2272# The last member ends with the value.
2273def Scan.finish(scan: Scan) -> Result<&2, &2, StateError, TraceState>:
2274  match scan:
2275    case Stopped{error}:
2276      Fail{error}
2277    case Scanning{member, room, current, entries}:
2278      Scan.result(Scan.close(member, room, current, entries))
2279
2280# Read the fields only when they fit the budget.
2281def Scan.within(fits: Maybe<&2, Nat>, fields: List<&2, String>) -> Result<&2, &2, StateError, TraceState>:
2282  match fits:
2283    case None{}:
2284      Fail{StateTooLarge{}}
2285    case Some{left}:
2286      Scan.finish(Scan.fields(fields, Scan.start()))
2287
2288# Parse repeated tracestate field values, in arrival order, as their
2289# comma-joined combination (W3C 3.3.2). The combined value, joining commas
2290# included, must fit the tracestate input budget; a larger one is refused with
2291# StateTooLarge before any member is read, without measuring the rest. Then:
2292# empty members are ignored, and so is optional whitespace before a member and
2293# after its value; every nonempty member must be a valid entry (InvalidEntry)
2294# and counts toward the 32 allowed (TooManyMembers); the first entry of each
2295# key is kept. An error discards the whole state; a valid traceparent stays
2296# valid (spec #1). W3C 3.3: parse tracestate only for a message whose
2297# traceparent was parsed.
2298# Laws: fields_join, over_budget, within_budgets, first_wins and the others of
2299# section 10 of LAWS.bend.
2300def TraceState.parse_fields(limits: Limits, +fields: List<&2, String>) -> Result<&2, &2, StateError, TraceState>:
2301  Scan.within(Utf8.left_fields(fields, Some{Limits.tracestate_input(limits)}), fields)
2302
2303# Parse one combined tracestate value; see TraceState.parse_fields.
2304def TraceState.parse(limits: Limits, text: String) -> Result<&2, &2, StateError, TraceState>:
2305  TraceState.parse_fields(limits, Con{text, Nil{}})
2306
2307# The name of a tracestate error; InvalidEntry adds the member number and the
2308# reason.
2309def StateError.show(error: StateError) -> String:
2310  match error:
2311    case StateTooLarge{}:
2312      "StateTooLarge"
2313    case TooManyMembers{}:
2314      "TooManyMembers"
2315    case InvalidEntry{member, reason}:
2316      "InvalidEntry " ++ Nat.show(member) ++ " " ++ EntryError.show(reason)
2317
2318# Tracestate: updates
2319# ===================
2320#
2321# W3C 3.5 lets a participant add, update and delete entries of the state it
2322# sends. A changed entry moves to the front and the other entries keep their
2323# order. Spec #1: updating a key of a full state evicts nothing, and adding a
2324# 33rd key removes the last entry.
2325
2326# `item` followed by `rest`, unless `skip` is True: one step of a filter.
2327# Removing a key and listing the dropped keys both use it.
2328def Entries.unless(-A: Data, skip: Bool, item: A, rest: List<&2, A>) -> List<&2, A>:
2329  match skip:
2330    case True{}:
2331      rest
2332    case False{}:
2333      Con{item, rest}
2334
2335# The entries without the one whose key is `key`, in order.
2336def Entries.without(entries: List<&2, StateEntry>, +key: String) -> List<&2, StateEntry>:
2337  match entries:
2338    case Nil{}:
2339      Nil{}
2340    case Con{+entry, rest}:
2341      Entries.unless(StateEntry, String.eq(StateEntry.key_text(entry), key), entry, Entries.without(rest, key))
2342
2343# The state of these entries when the check finds them valid, `fallback`
2344# otherwise. Updates build their entries so that the check passes, which the
2345# laws prove; `fallback` keeps the function total without an unchecked
2346# conversion.
2347def TraceState.from_entries.checked(entries: List<&2, StateEntry>, fallback: TraceState, valid: Bool,
2348  evidence: {TraceState.is_valid(entries) == valid : Bool}) -> TraceState:
2349  match valid:
2350    case True{}:
2351      TraceState{entries, evidence}
2352    case False{}:
2353      fallback
2354
2355# The state of `entries`, checked, or `fallback` if the check fails.
2356def TraceState.from_entries(+entries: List<&2, StateEntry>, fallback: TraceState) -> TraceState:
2357  TraceState.from_entries.checked(entries, fallback, TraceState.is_valid(entries), {==})
2358
2359# Add or update the entry of `key` (W3C 3.5): it goes to the front with
2360# `value`, and the other entries follow in their order. At most 31 of them
2361# stay, so a new key in a full state removes the last entry, while updating a
2362# key that is present evicts nothing (laws set_entries, update_keeps_all,
2363# insert_entries and set_get).
2364def TraceState.set(+state: TraceState, +key: StateKey, value: StateValue) -> TraceState:
2365  TraceState.from_entries(Con{StateEntry{key, value},
2366    List.take(&2, StateEntry, Entries.without(TraceState.entries(state), StateKey.to_string(key)), 31n)}, state)
2367
2368# Delete the entry of `key`, if there is one; the other entries keep their
2369# order (W3C 3.5; laws remove_entries and remove_get). W3C asks participants
2370# not to delete keys other vendors generated: that breaks correlation in
2371# their systems.
2372def TraceState.remove(+state: TraceState, key: StateKey) -> TraceState:
2373  TraceState.from_entries(Entries.without(TraceState.entries(state), StateKey.to_string(key)), state)
2374
2375# Tracestate: emission
2376# ====================
2377#
2378# The emitted value is the normalized one of TraceState.format. Its size in
2379# UTF-8 octets counts each entry's key, equals sign and value and the commas
2380# between entries (spec #1). Keys and values are ASCII, so an octet is also a
2381# character, the unit of W3C 3.3.3.1.
2382
2383# The octets of `key=value` (law entry_size).
2384def StateEntry.size(entry: StateEntry) -> Nat:
2385  match entry:
2386    case StateEntry{key, value}:
2387      Nat.add(Utf8.length(StateKey.to_string(key)), 1n+Utf8.length(StateValue.to_string(value)))
2388
2389# The octets of each entry after the first, with its comma.
2390def Entries.size.rest(entries: List<&2, StateEntry>) -> Nat:
2391  match entries:
2392    case Nil{}:
2393      0n
2394    case Con{entry, rest}:
2395      1n+Nat.add(StateEntry.size(entry), Entries.size.rest(rest))
2396
2397# The octets of the entries joined by commas, as Entries.format writes them.
2398def Entries.size(entries: List<&2, StateEntry>) -> Nat:
2399  match entries:
2400    case Nil{}:
2401      0n
2402    case Con{entry, rest}:
2403      Nat.add(StateEntry.size(entry), Entries.size.rest(rest))
2404
2405# The octets of TraceState.format(state) (law state_size).
2406def TraceState.size(state: TraceState) -> Nat:
2407  Entries.size(TraceState.entries(state))
2408
2409# What truncation to the output budget kept, and the keys of the entries it
2410# dropped, in their original order. Reporting the keys, not the values, tells
2411# which vendors lost their state without repeating opaque data.
2412type Truncation is Data:
2413  Truncation{kept: TraceState, dropped: List<&2, StateKey>}
2414
2415# The state that fits the output budget.
2416def Truncation.kept(truncation: Truncation) -> TraceState:
2417  match truncation:
2418    case Truncation{kept, dropped}:
2419      kept
2420
2421# The keys of the entries removed, in their original order; none when the
2422# state already fitted.
2423def Truncation.dropped(truncation: Truncation) -> List<&2, StateKey>:
2424  match truncation:
2425    case Truncation{kept, dropped}:
2426      dropped
2427
2428# Whether the entry is larger than 128 octets. W3C 3.3.3.1 asks to remove
2429# such entries first.
2430def StateEntry.is_large(entry: StateEntry) -> Bool:
2431  Nat.is_gt(StateEntry.size(entry), 128n)
2432
2433# Whether one of the entries is larger than 128 octets.
2434def Entries.has_large(entries: List<&2, StateEntry>) -> Bool:
2435  match entries:
2436    case Nil{}:
2437      False{}
2438    case Con{entry, rest}:
2439      Bool.or(StateEntry.is_large(entry), Entries.has_large(rest))
2440
2441# The entries without the rightmost one larger than 128 octets: an entry
2442# stays when a large entry follows it.
2443def Entries.drop_last_large(entries: List<&2, StateEntry>) -> List<&2, StateEntry>:
2444  match entries:
2445    case Nil{}:
2446      Nil{}
2447    case Con{+entry, +rest}:
2448      Bool.pick(List<&2, StateEntry>, Entries.has_large(rest), Con{entry, Entries.drop_last_large(rest)},
2449        Bool.pick(List<&2, StateEntry>, StateEntry.is_large(entry), rest, Con{entry, rest}))
2450
2451# The entries without the rightmost one.
2452def Entries.drop_last(entries: List<&2, StateEntry>) -> List<&2, StateEntry>:
2453  match entries:
2454    case Nil{}:
2455      Nil{}
2456    case Con{entry, +rest}:
2457      Bool.pick(List<&2, StateEntry>, List.is_empty(&2, StateEntry, rest), Nil{},
2458        Con{entry, Entries.drop_last(rest)})
2459
2460# One removal step (spec #1): the rightmost entry larger than 128 octets, or
2461# the rightmost entry when none is.
2462def Entries.shrink(+entries: List<&2, StateEntry>) -> List<&2, StateEntry>:
2463  Bool.pick(List<&2, StateEntry>, Entries.has_large(entries), Entries.drop_last_large(entries),
2464    Entries.drop_last(entries))
2465
2466# Remove entries one step at a time while they take more than `budget`
2467# octets, and stop as soon as they fit. `fuel` bounds the steps. One per
2468# entry suffices: once every entry is removed, the empty list takes 0 octets,
2469# which fits any budget.
2470def Entries.truncate(fuel: Nat, +budget: Nat, +entries: List<&2, StateEntry>) -> List<&2, StateEntry>:
2471  match fuel:
2472    case 0n:
2473      entries
2474    case 1n+more:
2475      Bool.pick(List<&2, StateEntry>, Nat.is_le(Entries.size(entries), budget), entries,
2476        Entries.truncate(more, budget, Entries.shrink(entries)))
2477
2478# The keys of the entries that `kept` lacks, in order.
2479def Entries.dropped(entries: List<&2, StateEntry>, +kept: List<&2, StateEntry>) -> List<&2, StateKey>:
2480  match entries:
2481    case Nil{}:
2482      Nil{}
2483    case Con{+entry, rest}:
2484      Entries.unless(StateKey, Entries.has_key(kept, StateEntry.key_text(entry)), StateEntry.key(entry),
2485        Entries.dropped(rest, kept))
2486
2487# Fit a state to the output budget of `limits` by removing whole entries
2488# (W3C 3.3.3.1, spec #1): while the value is over the budget, remove the
2489# rightmost entry larger than 128 octets, or the rightmost entry when none is,
2490# and stop as soon as it fits. The surviving entries keep their order (laws
2491# truncate_steps, truncate_fits, truncate_whole, truncate_order and
2492# truncate_dropped).
2493def TraceState.truncate(limits: Limits, state: TraceState) -> Truncation:
2494  +entries = TraceState.entries(state)
2495  +kept = Entries.truncate(List.length(&2, StateEntry, entries), Limits.tracestate_output(limits), entries)
2496  Truncation{TraceState.from_entries(kept, TraceState.empty()), Entries.dropped(entries, kept)}
2497
2498# Outgoing contexts
2499# =================
2500#
2501# An outgoing context is a local context with the tracestate its participant
2502# sends with it: the state attached to a local operation (spec #1). Editing
2503# that state is allowed because the traceparent of a local context
2504# identifies an operation of this participant: a root, a child, a restart or
2505# an operation the caller constructed with Context.from_ids. W3C 3.4 and spec
2506# #1 forbid sending a received traceparent unchanged with an edited or
2507# truncated tracestate. The types rule out passing a RemoteContext here, but
2508# not a local context built with the received IDs: Context.from_ids must only
2509# be given the IDs of the caller's own operation. A received pair is
2510# forwarded as it came, by Context.forward.
2511
2512# A local context and the state sent with it.
2513type OutgoingContext is Data:
2514  OutgoingContext{context: LocalContext, state: TraceState}
2515
2516# The two header values an outgoing context emits, and the keys of the
2517# entries that truncation to the output budget dropped, in their original
2518# order. A context with no state emits the tracestate "", which
2519# Context.inject does not write.
2520type Emission is Data:
2521  Emission{traceparent: String, tracestate: String, dropped: List<&2, StateKey>}
2522
2523# An outgoing context with no state yet, as for a new root.
2524def OutgoingContext.new(context: LocalContext) -> OutgoingContext:
2525  OutgoingContext{context, TraceState.empty()}
2526
2527# An outgoing context that sends `state`, such as the state received with the
2528# parent of a child operation. The caller associates the state with this
2529# operation, as with Context.from_ids.
2530def OutgoingContext.with_state(context: LocalContext, state: TraceState) -> OutgoingContext:
2531  OutgoingContext{context, state}
2532
2533# The local operation.
2534def OutgoingContext.context(outgoing: OutgoingContext) -> LocalContext:
2535  match outgoing:
2536    case OutgoingContext{context, state}:
2537      context
2538
2539# The state sent with the operation.
2540def OutgoingContext.state(outgoing: OutgoingContext) -> TraceState:
2541  match outgoing:
2542    case OutgoingContext{context, state}:
2543      state
2544
2545# The value of the entry with this key, if there is one.
2546def OutgoingContext.get(outgoing: OutgoingContext, key: StateKey) -> Maybe<&2, StateValue>:
2547  TraceState.get(OutgoingContext.state(outgoing), key)
2548
2549# Add or update an entry (see TraceState.set); the context is unchanged (law
2550# outgoing_set).
2551def OutgoingContext.set(outgoing: OutgoingContext, key: StateKey, value: StateValue) -> OutgoingContext:
2552  match outgoing:
2553    case OutgoingContext{context, state}:
2554      OutgoingContext{context, TraceState.set(state, key, value)}
2555
2556# Delete an entry (see TraceState.remove); the context is unchanged (law
2557# outgoing_remove).
2558def OutgoingContext.remove(outgoing: OutgoingContext, key: StateKey) -> OutgoingContext:
2559  match outgoing:
2560    case OutgoingContext{context, state}:
2561      OutgoingContext{context, TraceState.remove(state, key)}
2562
2563# The emission of a context and a truncated state.
2564def Emission.of(context: LocalContext, truncation: Truncation) -> Emission:
2565  match truncation:
2566    case Truncation{kept, dropped}:
2567      Emission{TraceParentV00.format(LocalContext.to_traceparent(context)), TraceState.format(kept), dropped}
2568
2569# The traceparent and tracestate values to send: the participating
2570# traceparent of the context, and the normalized value of the state
2571# truncated to the output budget of `limits` (laws emit_traceparent,
2572# emit_tracestate, emit_fits and emit_accepted).
2573def OutgoingContext.emit(limits: Limits, outgoing: OutgoingContext) -> Emission:
2574  match outgoing:
2575    case OutgoingContext{context, state}:
2576      Emission.of(context, TraceState.truncate(limits, state))
2577
2578# The traceparent value: always 55 characters.
2579def Emission.traceparent(emission: Emission) -> String:
2580  match emission:
2581    case Emission{traceparent, tracestate, dropped}:
2582      traceparent
2583
2584# The tracestate value: at most the output budget in octets, "" for no state.
2585def Emission.tracestate(emission: Emission) -> String:
2586  match emission:
2587    case Emission{traceparent, tracestate, dropped}:
2588      tracestate
2589
2590# The keys of the entries truncation dropped, in their original order.
2591def Emission.dropped(emission: Emission) -> List<&2, StateKey>:
2592  match emission:
2593    case Emission{traceparent, tracestate, dropped}:
2594      dropped
2595
2596# Extraction
2597# ==========
2598#
2599# Context.extract reads the trace context of a received message from its
2600# carrier: the list of the message's fields in their order, repeated fields
2601# included (spec #1, "Preserve an ordered multi-value carrier"). Field names
2602# are compared without regard to ASCII case. A single traceparent field is
2603# read by TraceParent.read: version 00 exactly as the strict codec reads it,
2604# ff never, and versions 01 to fe by their known prefix (W3C 3.2.4 and
2605# 4.1.2). A message whose traceparent is accepted gives an incoming context:
2606# the sender's operation, the state received with it, and the original pair
2607# of fields, kept so that Context.forward can send the context unchanged. A
2608# message without a usable traceparent keeps the base context the caller
2609# passes, and its tracestate is not read (W3C 3.3). Extraction reads text
2610# only: it generates no identifier, performs no effect and never includes a
2611# received value in a diagnostic.
2612
2613# One field of a message: its name and its value. A carrier is the list of a
2614# message's fields in their order; repeated fields stay separate, as the
2615# message carried them. A host that joins repeated fields into one value
2616# with commas (RFC 9110, section 5.3) gives one field with that value.
2617type Header is Data:
2618  Header{name: String, value: String}
2619
2620# Why extraction refused a message's traceparent:
2621#   RepeatedTraceParent{}       the message has more than one traceparent field,
2622#                               or a value that joins several with a comma
2623#   TraceParentTooLarge{}       the value exceeds the traceparent input budget
2624#   InvalidTraceParent{error}   the value breaks the rules of its version;
2625#                               `error` is the first problem, as the codec
2626#                               reports it, with offsets counted from the
2627#                               first character after optional whitespace
2628# The received value itself is never included.
2629type TraceParentError is Data:
2630  RepeatedTraceParent{}
2631  TraceParentTooLarge{}
2632  InvalidTraceParent{error: Error}
2633
2634# The original fields of an accepted message: its traceparent value, without
2635# the optional whitespace around it, and its tracestate field values as they
2636# came, in arrival order, none when it had no tracestate field. They are what
2637# Context.forward sends. The input budgets bound the pairs that extraction
2638# keeps (law received_bounds); a pair built directly with this constructor
2639# carries no such guarantee, so forwarding checks what it sends. A pair that
2640# extraction kept is refused only when it exceeds the output budget (law
2641# forward_extracted).
2642type ReceivedPair is Data:
2643  ReceivedPair{traceparent: String, tracestate: List<&2, String>}
2644
2645# The sender's operation together with the tracestate that goes with it: one
2646# extracted from a message, which also keeps the received pair when the whole
2647# pair was accepted, or one built from its parts (IncomingContext.from_remote),
2648# which keeps none. It is not this participant's operation: a service
2649# continues it with a child (Context.child_from_id with
2650# IncomingContext.parent), or forwards the received pair unchanged
2651# (Context.forward).
2652type IncomingContext is Data:
2653  IncomingContext{context: RemoteContext, state: TraceState, received: Maybe<&2, ReceivedPair>}
2654
2655# The context to continue from that extraction keeps when a message carries
2656# no usable traceparent: a context received earlier, or an operation of this
2657# participant with the state it sends.
2658type BaseContext is Data:
2659  IncomingBase{incoming: IncomingContext}
2660  OutgoingBase{outgoing: OutgoingContext}
2661
2662# What extraction found in the traceparent fields of a message: an accepted
2663# value, no field, or a refusal with its reason.
2664type TraceParentOutcome is Data:
2665  TraceParentAccepted{}
2666  TraceParentAbsent{}
2667  TraceParentRejected{error: TraceParentError}
2668
2669# What extraction did with the tracestate fields of a message:
2670#   StateAbsent{}            there was no tracestate field
2671#   StateAccepted{}          the fields were read into the incoming state,
2672#                            which may be empty
2673#   StateDiscarded{error}    the fields were refused as a whole; the incoming
2674#                            context has no state and the traceparent stays
2675#                            accepted
2676#   StateIgnored{}           the fields were not read, because the message has
2677#                            no accepted traceparent (W3C 3.3)
2678type StateOutcome is Data:
2679  StateAbsent{}
2680  StateAccepted{}
2681  StateDiscarded{error: StateError}
2682  StateIgnored{}
2683
2684# The result of extracting a message: the context to continue from, if any,
2685# and what happened to each field. `context` is the incoming context of the
2686# message when its traceparent was accepted, and the base otherwise.
2687type Extraction is Data:
2688  Extraction{context: Maybe<&2, BaseContext>, parent: TraceParentOutcome, state: StateOutcome}
2689
2690# Extraction: carriers
2691# ====================
2692#
2693# A message's fields are selected by name, in their order. Reading a carrier
2694# is a loop, so a message with many fields needs no deep stack.
2695
2696# The field's name.
2697def Header.name(header: Header) -> String:
2698  match header:
2699    case Header{name, value}:
2700      name
2701
2702# The field's value.
2703def Header.value(header: Header) -> String:
2704  match header:
2705    case Header{name, value}:
2706      value
2707
2708# The names of the two context fields, in lowercase (W3C 3.2.1 and 3.3.1),
2709# written in this one place: extraction selects the fields by them, whatever
2710# the case of the names received; cleanup, injection and forwarding remove
2711# and write the fields under them; and Context.field_names publishes them.
2712def Carrier.traceparent_name() -> String:
2713  "traceparent"
2714
2715def Carrier.tracestate_name() -> String:
2716  "tracestate"
2717
2718# Whether `text` is `name` without regard to ASCII case (W3C 3.2.1 and
2719# 3.3.1): each character of `text`, with the letters A to Z lowered, is the
2720# character of `name` at its position. Other characters are compared as they
2721# are, so a name that differs by more than ASCII case names another field.
2722# `name` is written in lowercase, and the comparison follows it, so a long
2723# field name is not read past it.
2724def Carrier.named(name: String, text: String) -> Bool:
2725  match name text:
2726    case SNil{} SNil{}:
2727      True{}
2728    case SNil{} SCon{char, rest}:
2729      False{}
2730    case SCon{expected, more} SNil{}:
2731      False{}
2732    case SCon{expected, more} SCon{char, rest}:
2733      Bool.and(Char.is_eq(Char.to_lower(char), expected), Carrier.named(more, rest))
2734
2735# `value` before `found` when `hit` is True: one step of Carrier.values.
2736def Carrier.keep(hit: Bool, value: String, found: List<&2, String>) -> List<&2, String>:
2737  match hit:
2738    case True{}:
2739      Con{value, found}
2740    case False{}:
2741      found
2742
2743# The values of the fields named `name`, most recent first, before `found`.
2744def Carrier.values.go(carrier: List<&2, Header>, +name: String, found: List<&2, String>) -> List<&2, String>:
2745  match carrier:
2746    case Nil{}:
2747      found
2748    case Con{+header, rest}:
2749      Carrier.values.go(rest, name, Carrier.keep(Carrier.named(name, Header.name(header)), Header.value(header), found))
2750
2751# The values of the fields named `name` without regard to ASCII case, in
2752# their order: the loop collects them most recent first, and reversing, also
2753# a loop, puts them back in order.
2754def Carrier.values(carrier: List<&2, Header>, +name: String) -> List<&2, String>:
2755  List.reverse(&2, String, Carrier.values.go(carrier, name, Nil{}))
2756
2757# Extraction: reading a traceparent
2758# =================================
2759#
2760# TraceParent.read measures a value against the traceparent input budget,
2761# removes the optional whitespace around it, refuses a comma and reads its
2762# known fields by the rules of its version. Measuring stops at the first
2763# character past the budget, and the loops below keep the stack flat for a
2764# value of any length.
2765
2766# `head` followed by `tail`, without the optional whitespace at its start:
2767# `ows` says whether `head` is optional whitespace.
2768def Text.drop_ows.go(tail: String, head: Char, ows: Bool) -> String:
2769  match tail ows:
2770    case SNil{} False{}:
2771      SCon{head, SNil{}}
2772    case SCon{next, rest} False{}:
2773      SCon{head, SCon{next, rest}}
2774    case SNil{} True{}:
2775      SNil{}
2776    case SCon{+next, rest} True{}:
2777      Text.drop_ows.go(rest, next, StateChar.is_ows(next))
2778
2779# The text without the optional whitespace, spaces and horizontal tabs, at its
2780# start.
2781def Text.drop_ows(text: String) -> String:
2782  match text:
2783    case SNil{}:
2784      SNil{}
2785    case SCon{+head, tail}:
2786      Text.drop_ows.go(tail, head, StateChar.is_ows(head))
2787
2788# The text without the optional whitespace at its start and at its end (RFC
2789# 9110, section 5.5: "A field value does not include leading or trailing
2790# whitespace"). Reversing brings the end to the front, and reversing again
2791# brings it back.
2792def Text.trim_ows(text: String) -> String:
2793  String.reverse(Text.drop_ows(String.reverse(Text.drop_ows(text))))
2794
2795# Whether the text contains a comma: `found` records whether one was seen
2796# before.
2797def Text.has_comma.go(text: String, found: Bool) -> Bool:
2798  match text found:
2799    case _ True{}:
2800      True{}
2801    case SNil{} False{}:
2802      False{}
2803    case SCon{char, rest} False{}:
2804      Text.has_comma.go(rest, Char.is_eq(char, ','))
2805
2806# Whether the text contains a comma.
2807def Text.has_comma(text: String) -> Bool:
2808  Text.has_comma.go(text, False{})
2809
2810# Whether a character is a control character other than a horizontal tab:
2811# U+0000 to U+0008, U+000A to U+001F or U+007F. No field value may hold one
2812# (RFC 9110, section 5.5); a carriage return or a line feed would end the
2813# field.
2814def Text.is_control(char: Char) -> Bool:
2815  match char:
2816    case Chr{+code}:
2817      Bool.or(Bool.and(U32.is_lt(code, 32), Bool.not(U32.is_eq(code, 9))), U32.is_eq(code, 127))
2818
2819# The offset of the first control character of `text`, counted from
2820# `offset`, unless `found` already holds one. This is a loop.
2821def Text.control.go(text: String, +offset: Nat, found: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
2822  match text found:
2823    case _ Some{at}:
2824      Some{at}
2825    case SNil{} None{}:
2826      None{}
2827    case SCon{char, rest} None{}:
2828      Text.control.go(rest, 1n+offset, Bool.pick(Maybe<&2, Nat>, Text.is_control(char), Some{offset}, None{}))
2829
2830# Whether a value's version, from its two digits, is later than 00 and so
2831# read by its known prefix (W3C 3.2.2.1 and 3.2.4): Done{False{}} for 00,
2832# which the strict codec reads, Done{True{}} for 01 to fe, and a refusal for
2833# ff.
2834def Read.is_later(digits: Digits.Digits(2n)) -> Result<&2, &2, Error, Bool>:
2835  match digits:
2836    case Digits.DCon{Hex.H0{}, Digits.DCon{Hex.H0{}, Digits.DNil{}}}:
2837      Done{False{}}
2838    case Digits.DCon{Hex.Hf{}, Digits.DCon{Hex.Hf{}, Digits.DNil{}}}:
2839      Fail{ForbiddenVersion{}}
2840    case other:
2841      Done{True{}}
2842
2843# Whether the version whose two digits were read is later than 00.
2844def Read.is_later.parsed(parsed: Parsed<2n>) -> Result<&2, &2, Error, Bool>:
2845  match parsed:
2846    case Parsed{digits, rest}:
2847      Read.is_later(digits)
2848
2849# The fields a later version does not know, once searched for a control
2850# character: none, or the offset of the first.
2851def Read.clean(found: Maybe<&2, Nat>) -> Result<&2, &2, Error, Unit>:
2852  match found:
2853    case None{}:
2854      Done{Unit{}}
2855    case Some{offset}:
2856      Fail{ControlCharacter{offset}}
2857
2858# What may follow the flags of a later version: the end of the value, or a
2859# dash that starts fields this version does not know. Those fields are not
2860# read (W3C 3.2.4: "Vendors MUST NOT parse or assume anything about unknown
2861# fields"), except that a control character in them is refused with
2862# ControlCharacter at its offset: no field value may hold one (RFC 9110,
2863# section 5.5), and a value forwarded unchanged must not end a message's
2864# field. Any other character than a dash at offset 55 is ExpectedSeparator.
2865def Read.extension(rest: String) -> Result<&2, &2, Error, Unit>:
2866  match rest:
2867    case SNil{}:
2868      Done{Unit{}}
2869    case SCon{char, tail}:
2870      do Result<&2, &2, Error, Unit>:
2871        unknown : String <- Parse.separator_result(tail, Char.is_eq(char, '-'), 55n)
2872        Read.clean(Text.control.go(unknown, 56n, None{}))
2873
2874# A later version is read by its known prefix (W3C 3.2.4 and 4.1.2): its first
2875# 55 characters are read as version 00, which checks the trace ID, the parent
2876# ID, the flags and the dashes between them at their own offsets, and then the
2877# value must end or continue with a dash. A value that ends before its 55th
2878# character, with no invalid character before, fails with UnexpectedEnd.
2879def Read.prefix(+text: String) -> Result<&2, &2, Error, TraceParentV00>:
2880  do Result<&2, &2, Error, TraceParentV00>:
2881    known : TraceParentV00 <- TraceParentV00.parse("00" ++ String.drop(String.take(text, 55n), 2n))
2882    rest : Unit <- Read.extension(String.drop(text, 55n))
2883    return known
2884
2885# Read a value by the rules of its version: `later` is False for 00.
2886def Read.by_version(later: Bool, text: String) -> Result<&2, &2, Error, TraceParentV00>:
2887  match later:
2888    case False{}:
2889      TraceParentV00.parse(text)
2890    case True{}:
2891      Read.prefix(text)
2892
2893# The known fields of a value, read by the rules of its version.
2894def Read.known(+text: String) -> Result<&2, &2, Error, TraceParentV00>:
2895  do Result<&2, &2, Error, TraceParentV00>:
2896    version : Parsed<2n> <- Parse.digits(2n, text, 0n)
2897    later : Bool <- Read.is_later.parsed(version)
2898    Read.by_version(later, text)
2899
2900# A refusal of the codec, as a refused traceparent.
2901def Read.invalid(result: Result<&2, &2, Error, TraceParentV00>) ->
2902  Result<&2, &2, TraceParentError, TraceParentV00>:
2903  match result:
2904    case Fail{error}:
2905      Fail{InvalidTraceParent{error}}
2906    case Done{value}:
2907      Done{value}
2908
2909# A value that joins several with a comma is refused as repeated fields; any
2910# other value is read by the rules of its version.
2911def Read.single(combined: Bool, text: String) -> Result<&2, &2, TraceParentError, TraceParentV00>:
2912  match combined:
2913    case True{}:
2914      Fail{RepeatedTraceParent{}}
2915    case False{}:
2916      Read.invalid(Read.known(text))
2917
2918# A value without the whitespace around it, refused when it joins several.
2919def Read.trimmed(+text: String) -> Result<&2, &2, TraceParentError, TraceParentV00>:
2920  Read.single(Text.has_comma(text), text)
2921
2922# A value within its budget is read without the optional whitespace around
2923# it; a value over the budget is refused without being read further.
2924def Read.within(fits: Maybe<&2, Nat>, value: String) -> Result<&2, &2, TraceParentError, TraceParentV00>:
2925  match fits:
2926    case None{}:
2927      Fail{TraceParentTooLarge{}}
2928    case Some{left}:
2929      Read.trimmed(Text.trim_ows(value))
2930
2931# Read one received traceparent value by the rules of a participant, and
2932# return its known fields as a v00 value, flag byte included:
2933#   - a value over the traceparent input budget of `limits`, counted in UTF-8
2934#     octets with its whitespace, is refused with TraceParentTooLarge;
2935#   - optional whitespace around the value is removed (RFC 9110, section 5.5);
2936#   - a value with a comma joins repeated fields and is refused with
2937#     RepeatedTraceParent, even when the comma is in fields of a later
2938#     version: no version defines a comma, and a host that joins repeated
2939#     fields separates them with one (RFC 9110, section 5.3);
2940#   - version 00 is read exactly by TraceParentV00.parse: 55 characters and
2941#     nothing after them;
2942#   - version ff is refused with ForbiddenVersion (W3C 3.2.2.1);
2943#   - versions 01 to fe are read by their known prefix: the fields of version
2944#     00, followed by the end of the value or by a dash and fields that are
2945#     not read, whatever they hold other than a comma or a control character,
2946#     which is refused with ControlCharacter (W3C 3.2.4 and 4.1.2; RFC 9110,
2947#     section 5.5).
2948# RemoteContext.from_traceparent then keeps the sampled and random-trace-id
2949# flags. Laws: read_v00, read_v00_exact, read_future, read_ff, read_comma,
2950# read_over_budget and read_within_budgets.
2951def TraceParent.read(limits: Limits, +value: String) -> Result<&2, &2, TraceParentError, TraceParentV00>:
2952  Read.within(Utf8.left(value, Some{Limits.traceparent_input(limits)}), value)
2953
2954# Extraction: messages
2955# ====================
2956#
2957# Extract.parents decides from the traceparent values: none keeps the base,
2958# several are refused, and a single value is read. Only an accepted value lets
2959# the tracestate values be read.
2960
2961# The state outcome when the tracestate fields are not read: absent without
2962# a field, ignored with one (W3C 3.3).
2963def Extract.ignored(states: List<&2, String>) -> StateOutcome:
2964  match states:
2965    case Nil{}:
2966      StateAbsent{}
2967    case Con{field, rest}:
2968      StateIgnored{}
2969
2970# The extraction of a message whose context is not read: the base is kept,
2971# with the traceparent outcome and the presence of tracestate fields.
2972def Extract.kept(base: Maybe<&2, BaseContext>, parent: TraceParentOutcome, states: List<&2, String>) -> Extraction:
2973  Extraction{base, parent, Extract.ignored(states)}
2974
2975# The incoming context of an accepted message, as the context to continue
2976# from.
2977def Extract.incoming(remote: RemoteContext, state: TraceState, received: Maybe<&2, ReceivedPair>) ->
2978  Maybe<&2, BaseContext>:
2979  Some{IncomingBase{IncomingContext{remote, state, received}}}
2980
2981# An accepted message whose tracestate fields were parsed: an accepted state
2982# keeps the pair, which can be forwarded, and a refused one is discarded
2983# whole, keeping the traceparent (spec #1) but no pair, since the pair was not
2984# accepted whole.
2985def Extract.parsed(parsed: Result<&2, &2, StateError, TraceState>, remote: RemoteContext, text: String,
2986  states: List<&2, String>) -> Extraction:
2987  match parsed:
2988    case Fail{error}:
2989      Extraction{Extract.incoming(remote, TraceState.empty(), None{}), TraceParentAccepted{}, StateDiscarded{error}}
2990    case Done{state}:
2991      Extraction{Extract.incoming(remote, state, Some{ReceivedPair{text, states}}), TraceParentAccepted{},
2992        StateAccepted{}}
2993
2994# An accepted message with its tracestate field values, read in arrival order
2995# as their comma-joined combination (W3C 3.3.2).
2996def Extract.state(+limits: Limits, +states: List<&2, String>, remote: RemoteContext, text: String) -> Extraction:
2997  match states:
2998    case Nil{}:
2999      Extraction{Extract.incoming(remote, TraceState.empty(), Some{ReceivedPair{text, Nil{}}}), TraceParentAccepted{},
3000        StateAbsent{}}
3001    case Con{field, rest}:
3002      Extract.parsed(TraceState.parse_fields(limits, Con{field, rest}), remote, text, Con{field, rest})
3003
3004# The extraction of a message whose only traceparent value `value` was read.
3005# The value is kept without the whitespace around it only once accepted, so a
3006# refused value is not read further.
3007def Extract.read(read: Result<&2, &2, TraceParentError, TraceParentV00>, value: String, +limits: Limits,
3008  +states: List<&2, String>, base: Maybe<&2, BaseContext>) -> Extraction:
3009  match read:
3010    case Fail{error}:
3011      Extract.kept(base, TraceParentRejected{error}, states)
3012    case Done{known}:
3013      Extract.state(limits, states, RemoteContext.from_traceparent(known), Text.trim_ows(value))
3014
3015# The extraction of a message with these traceparent and tracestate field
3016# values.
3017def Extract.parents(+limits: Limits, parents: List<&2, String>, +states: List<&2, String>,
3018  base: Maybe<&2, BaseContext>) -> Extraction:
3019  match parents:
3020    case Nil{}:
3021      Extract.kept(base, TraceParentAbsent{}, states)
3022    case Con{+value, Nil{}}:
3023      Extract.read(TraceParent.read(limits, value), value, limits, states, base)
3024    case Con{first, Con{second, more}}:
3025      Extract.kept(base, TraceParentRejected{RepeatedTraceParent{}}, states)
3026
3027# Extract the trace context of a received message from its carrier, with
3028# `base` as the context to keep when the message has no usable traceparent
3029# (spec #1, user stories 14, 15, 16, 24 and 25):
3030#   - no traceparent field keeps the base, TraceParentAbsent{};
3031#   - more than one traceparent field, whatever the case of their names, is
3032#     refused, and so is a single value that TraceParent.read refuses; the
3033#     base is kept, TraceParentRejected{error};
3034#   - an accepted value gives the incoming context and replaces the base: its
3035#     tracestate fields, whatever the case of their names, are read in
3036#     arrival order as their comma-joined combination, within the tracestate
3037#     input budget; refused fields are discarded whole, keeping the
3038#     traceparent;
3039#   - without an accepted traceparent, tracestate fields are not read.
3040# Laws: extract_absent, extract_repeated, extract_refused, extract_read,
3041# state_independent and received_bounds.
3042def Context.extract(+limits: Limits, +carrier: List<&2, Header>, base: Maybe<&2, BaseContext>) -> Extraction:
3043  Extract.parents(limits, Carrier.values(carrier, Carrier.traceparent_name()),
3044    Carrier.values(carrier, Carrier.tracestate_name()), base)
3045
3046# Extraction: results and diagnostics
3047# ===================================
3048
3049# The context to continue from: this message's incoming context when its
3050# traceparent was accepted, the base otherwise.
3051def Extraction.context(extraction: Extraction) -> Maybe<&2, BaseContext>:
3052  match extraction:
3053    case Extraction{context, parent, state}:
3054      context
3055
3056# What extraction found in the traceparent fields.
3057def Extraction.parent(extraction: Extraction) -> TraceParentOutcome:
3058  match extraction:
3059    case Extraction{context, parent, state}:
3060      parent
3061
3062# What extraction did with the tracestate fields.
3063def Extraction.state(extraction: Extraction) -> StateOutcome:
3064  match extraction:
3065    case Extraction{context, parent, state}:
3066      state
3067
3068# The incoming context an accepted message gives as its context.
3069def Extraction.incoming.base(context: Maybe<&2, BaseContext>) -> Maybe<&2, IncomingContext>:
3070  match context:
3071    case Some{IncomingBase{incoming}}:
3072      Some{incoming}
3073    case _:
3074      None{}
3075
3076# This message's own context: the incoming context when its traceparent was
3077# accepted, None{} when extraction kept the base.
3078def Extraction.incoming.of(parent: TraceParentOutcome, context: Maybe<&2, BaseContext>) ->
3079  Maybe<&2, IncomingContext>:
3080  match parent:
3081    case TraceParentAccepted{}:
3082      Extraction.incoming.base(context)
3083    case TraceParentAbsent{}:
3084      None{}
3085    case TraceParentRejected{error}:
3086      None{}
3087
3088# The context this message carried, when its traceparent was accepted; None{}
3089# when extraction kept the base, even an incoming one.
3090def Extraction.incoming(extraction: Extraction) -> Maybe<&2, IncomingContext>:
3091  match extraction:
3092    case Extraction{context, parent, state}:
3093      Extraction.incoming.of(parent, context)
3094
3095# The sender's operation.
3096def IncomingContext.context(incoming: IncomingContext) -> RemoteContext:
3097  match incoming:
3098    case IncomingContext{context, state, received}:
3099      context
3100
3101# The state received with it: empty when the message had none or when it was
3102# discarded.
3103def IncomingContext.state(incoming: IncomingContext) -> TraceState:
3104  match incoming:
3105    case IncomingContext{context, state, received}:
3106      state
3107
3108# The received pair, when the whole pair was accepted: None{} when the
3109# tracestate was discarded, and for a context built from parts.
3110def IncomingContext.received(incoming: IncomingContext) -> Maybe<&2, ReceivedPair>:
3111  match incoming:
3112    case IncomingContext{context, state, received}:
3113      received
3114
3115# The received context as the parent of a child operation.
3116def IncomingContext.parent(incoming: IncomingContext) -> Parent:
3117  RemoteParent{IncomingContext.context(incoming)}
3118
3119# An incoming context from its parts: a remote context and the tracestate
3120# that goes with it, so that an OpenTelemetry SDK's remote span contexts have
3121# one shape whatever format they came from. No message's fields were
3122# accepted, so it keeps no received pair, and Context.forward refuses it with
3123# NothingToForward (laws incoming_from_remote and forward_from_parts). A
3124# child continues it as any incoming context.
3125def IncomingContext.from_remote(context: RemoteContext, state: TraceState) -> IncomingContext:
3126  IncomingContext{context, state, None{}}
3127
3128# The received traceparent value, without the whitespace around it.
3129def ReceivedPair.traceparent(pair: ReceivedPair) -> String:
3130  match pair:
3131    case ReceivedPair{traceparent, tracestate}:
3132      traceparent
3133
3134# The received tracestate field values, in arrival order.
3135def ReceivedPair.tracestate(pair: ReceivedPair) -> List<&2, String>:
3136  match pair:
3137    case ReceivedPair{traceparent, tracestate}:
3138      tracestate
3139
3140# The base as the parent of a child operation: a received context or an
3141# operation of this participant.
3142def BaseContext.parent(base: BaseContext) -> Parent:
3143  match base:
3144    case IncomingBase{incoming}:
3145      IncomingContext.parent(incoming)
3146    case OutgoingBase{outgoing}:
3147      LocalParent{OutgoingContext.context(outgoing)}
3148
3149# The state that goes with the base: the state received with an incoming
3150# context, or the state an outgoing context sends.
3151def BaseContext.state(base: BaseContext) -> TraceState:
3152  match base:
3153    case IncomingBase{incoming}:
3154      IncomingContext.state(incoming)
3155    case OutgoingBase{outgoing}:
3156      OutgoingContext.state(outgoing)
3157
3158# The name of a traceparent error; InvalidTraceParent adds the codec's error.
3159def TraceParentError.show(error: TraceParentError) -> String:
3160  match error:
3161    case RepeatedTraceParent{}:
3162      "RepeatedTraceParent"
3163    case TraceParentTooLarge{}:
3164      "TraceParentTooLarge"
3165    case InvalidTraceParent{reason}:
3166      "InvalidTraceParent " ++ Error.show(reason)
3167
3168# The name of a traceparent outcome; a rejection adds its error.
3169def TraceParentOutcome.show(outcome: TraceParentOutcome) -> String:
3170  match outcome:
3171    case TraceParentAccepted{}:
3172      "TraceParentAccepted"
3173    case TraceParentAbsent{}:
3174      "TraceParentAbsent"
3175    case TraceParentRejected{error}:
3176      "TraceParentRejected " ++ TraceParentError.show(error)
3177
3178# The name of a tracestate outcome; a discard adds its error.
3179def StateOutcome.show(outcome: StateOutcome) -> String:
3180  match outcome:
3181    case StateAbsent{}:
3182      "StateAbsent"
3183    case StateAccepted{}:
3184      "StateAccepted"
3185    case StateDiscarded{error}:
3186      "StateDiscarded " ++ StateError.show(error)
3187    case StateIgnored{}:
3188      "StateIgnored"
3189
3190# Both outcomes of an extraction, for a log line: "TraceParentAccepted,
3191# StateDiscarded InvalidEntry 1 MissingEquals" for example. No received
3192# value is included, so the line can be logged as it is.
3193def Extraction.show(extraction: Extraction) -> String:
3194  match extraction:
3195    case Extraction{context, parent, state}:
3196      TraceParentOutcome.show(parent) ++ ", " ++ StateOutcome.show(state)
3197
3198# Injection
3199# =========
3200#
3201# Context.inject writes the context of an operation of this participant into
3202# the carrier of an outgoing message (spec #1, "Participant injection"):
3203# every old traceparent and tracestate field is removed, whatever the ASCII
3204# case of its name, the other fields keep their order, and the emitted
3205# fields are added at the end with lowercase names. An empty tracestate is
3206# not written. Context.clear removes the context fields alone, for a message
3207# sent without context. Neither generates an identifier.
3208
3209# The carrier an injection writes, and the keys of the entries that
3210# truncation to the output budget dropped from the state, in their original
3211# order: diagnostics, kept apart from the carrier.
3212type Injection is Data:
3213  Injection{carrier: List<&2, Header>, dropped: List<&2, StateKey>}
3214
3215# Whether a field name is traceparent or tracestate, without regard to ASCII
3216# case.
3217def Carrier.is_context(+name: String) -> Bool:
3218  Bool.or(Carrier.named(Carrier.traceparent_name(), name), Carrier.named(Carrier.tracestate_name(), name))
3219
3220# `header` before `kept` unless it is a context field (`context_field`): one
3221# step of Carrier.unrelated.go.
3222def Carrier.keep_unrelated(context_field: Bool, header: Header, kept: List<&2, Header>) -> List<&2, Header>:
3223  match context_field:
3224    case True{}:
3225      kept
3226    case False{}:
3227      Con{header, kept}
3228
3229# The unrelated fields, those that are not context fields, most recent first,
3230# before `kept`. This is a loop, so a message with many fields needs no deep
3231# stack.
3232def Carrier.unrelated.go(carrier: List<&2, Header>, kept: List<&2, Header>) -> List<&2, Header>:
3233  match carrier:
3234    case Nil{}:
3235      kept
3236    case Con{+header, rest}:
3237      Carrier.unrelated.go(rest, Carrier.keep_unrelated(Carrier.is_context(Header.name(header)), header, kept))
3238
3239# The carrier's unrelated fields, followed by `fields`: reversing the loop's
3240# result onto `fields`, also a loop, puts them back in order.
3241def Carrier.replace(carrier: List<&2, Header>, fields: List<&2, Header>) -> List<&2, Header>:
3242  List.reverse.go(&2, Header, Carrier.unrelated.go(carrier, Nil{}), fields)
3243
3244# The names of the context fields as injection writes them: traceparent, then
3245# tracestate, in lowercase (W3C 3.2.1 and 3.3.1), the names that extraction
3246# and cleanup read too. A propagator lists them as the fields it writes, and
3247# one that writes the values of OutgoingContext.emit through a setter of its
3248# own writes them under these names, the tracestate field only when its value
3249# is not empty, as injection does. Law: inject_names.
3250def Context.field_names() -> List<&2, String>:
3251  [Carrier.traceparent_name(), Carrier.tracestate_name()]
3252
3253# The context fields of a traceparent value and a tracestate value, with
3254# lowercase names; the tracestate field is left out when its value is empty.
3255def Carrier.context_fields(traceparent: String, +tracestate: String) -> List<&2, Header>:
3256  Con{Header{Carrier.traceparent_name(), traceparent}, Bool.pick(List<&2, Header>, String.is_empty(tracestate),
3257    Nil{}, Con{Header{Carrier.tracestate_name(), tracestate}, Nil{}})}
3258
3259# Remove every traceparent and tracestate field, whatever the case of its
3260# name, and keep the other fields in their order: the carrier of a message
3261# sent without context (spec #1, "Provide explicit context-field cleanup for
3262# the no-context path"). Law: clear_carrier.
3263def Context.clear(carrier: List<&2, Header>) -> List<&2, Header>:
3264  Carrier.replace(carrier, Nil{})
3265
3266# The injection of an emission into a carrier.
3267def Injection.of(carrier: List<&2, Header>, emission: Emission) -> Injection:
3268  match emission:
3269    case Emission{traceparent, tracestate, dropped}:
3270      Injection{Carrier.replace(carrier, Carrier.context_fields(traceparent, tracestate)), dropped}
3271
3272# Write an outgoing context into a carrier as a participant: the context
3273# fields of the carrier are replaced by the emitted traceparent, version 00
3274# with only the sampled and random-trace-id flags, and the emitted
3275# tracestate, truncated to the output budget of `limits` and left out when
3276# empty. The other fields keep their order, and injecting the same context
3277# into the carrier written gives that carrier again. A receiver that extracts
3278# the carrier with the same limits continues the injected operation with the
3279# truncated state. Laws: inject_carrier, inject_dropped, inject_idempotent and
3280# inject_extracted.
3281def Context.inject(limits: Limits, outgoing: OutgoingContext, carrier: List<&2, Header>) -> Injection:
3282  Injection.of(carrier, OutgoingContext.emit(limits, outgoing))
3283
3284# The carrier to send.
3285def Injection.carrier(injection: Injection) -> List<&2, Header>:
3286  match injection:
3287    case Injection{carrier, dropped}:
3288      carrier
3289
3290# The keys of the entries truncation dropped, in their original order; none
3291# when the state fitted.
3292def Injection.dropped(injection: Injection) -> List<&2, StateKey>:
3293  match injection:
3294    case Injection{carrier, dropped}:
3295      dropped
3296
3297# Forwarding
3298# ==========
3299#
3300# Context.forward sends a received context on unchanged, as a service that
3301# does not take part in the trace does (W3C 3.4, "Unmodified header
3302# propagation"): the traceparent value and the tracestate text of its
3303# received pair, without normalizing flags, downgrading the version, or
3304# editing or truncating the tracestate. The tracestate fields are joined into
3305# one field (W3C 3.3.2: tracestate "SHOULD be sent as a single field when
3306# possible"), and the old context fields of the carrier are replaced, as by
3307# injection. When the pair cannot be sent whole within the limits, forwarding
3308# refuses it: the caller may continue the trace with a child operation
3309# instead, whose own traceparent lets its state be truncated (spec #1). An
3310# incoming context built from parts has no pair to send (spec #41).
3311
3312# Why a received context could not be forwarded unchanged:
3313#   NothingToForward{}            it keeps no received pair: its tracestate was
3314#                                 discarded when it was extracted, or it was
3315#                                 built from parts (IncomingContext.from_remote)
3316#   ForwardTooLarge{}             its tracestate fields, joined by commas,
3317#                                 exceed the tracestate output budget
3318#   InvalidForwardParent{error}   its traceparent value is not one that
3319#                                 TraceParent.read accepts
3320#   InvalidForwardState{error}    its tracestate fields are not ones that
3321#                                 TraceState.parse_fields accepts
3322# A pair that extraction keeps always passes the last two checks (law
3323# forward_extracted); they refuse a pair built directly.
3324type ForwardError is Data:
3325  NothingToForward{}
3326  ForwardTooLarge{}
3327  InvalidForwardParent{error: TraceParentError}
3328  InvalidForwardState{error: StateError}
3329
3330# The fields joined by commas, most recent character first, after `done`:
3331# each field is reversed onto the comma before it. This is a loop.
3332def Text.joined.go(fields: List<&2, String>, done: String) -> String:
3333  match fields:
3334    case Nil{}:
3335      done
3336    case Con{field, rest}:
3337      Text.joined.go(rest, String.reverse.go(field, SCon{',', done}))
3338
3339# The fields joined by commas into one value, as String.join(fields, ",")
3340# writes it. It is built by loops, so fields of any length need no deep
3341# stack.
3342def Text.joined(fields: List<&2, String>) -> String:
3343  match fields:
3344    case Nil{}:
3345      SNil{}
3346    case Con{field, rest}:
3347      String.reverse(Text.joined.go(rest, String.reverse.go(field, SNil{})))
3348
3349# The carrier with its context fields replaced by a received pair: the
3350# traceparent value, and the tracestate fields joined into one value, left
3351# out when empty.
3352def Forward.carrier(carrier: List<&2, Header>, traceparent: String, tracestate: List<&2, String>) -> List<&2, Header>:
3353  Carrier.replace(carrier, Carrier.context_fields(traceparent, Text.joined(tracestate)))
3354
3355# The last check of a forwarded pair: its tracestate fields parse.
3356def Forward.state(parsed: Result<&2, &2, StateError, TraceState>, carrier: List<&2, Header>, traceparent: String,
3357  tracestate: List<&2, String>) -> Result<&2, &2, ForwardError, List<&2, Header>>:
3358  match parsed:
3359    case Fail{error}:
3360      Fail{InvalidForwardState{error}}
3361    case Done{state}:
3362      Done{Forward.carrier(carrier, traceparent, tracestate)}
3363
3364# The second check of a forwarded pair: its traceparent value reads back.
3365def Forward.parent(read: Result<&2, &2, TraceParentError, TraceParentV00>, +limits: Limits, carrier: List<&2, Header>,
3366  traceparent: String, +tracestate: List<&2, String>) -> Result<&2, &2, ForwardError, List<&2, Header>>:
3367  match read:
3368    case Fail{error}:
3369      Fail{InvalidForwardParent{error}}
3370    case Done{known}:
3371      Forward.state(TraceState.parse_fields(limits, tracestate), carrier, traceparent, tracestate)
3372
3373# The first check of a forwarded pair: its tracestate fields, joined by
3374# commas, fit the output budget. Measuring stops past the budget.
3375def Forward.fits(fits: Maybe<&2, Nat>, +limits: Limits, carrier: List<&2, Header>, +traceparent: String,
3376  +tracestate: List<&2, String>) -> Result<&2, &2, ForwardError, List<&2, Header>>:
3377  match fits:
3378    case None{}:
3379      Fail{ForwardTooLarge{}}
3380    case Some{left}:
3381      Forward.parent(TraceParent.read(limits, traceparent), limits, carrier, traceparent, tracestate)
3382
3383# Forward the received pair, if there is one.
3384def Forward.pair(+limits: Limits, received: Maybe<&2, ReceivedPair>, carrier: List<&2, Header>) ->
3385  Result<&2, &2, ForwardError, List<&2, Header>>:
3386  match received:
3387    case None{}:
3388      Fail{NothingToForward{}}
3389    case Some{ReceivedPair{+traceparent, +tracestate}}:
3390      Forward.fits(Utf8.left_fields(tracestate, Some{Limits.tracestate_output(limits)}), limits, carrier, traceparent,
3391        tracestate)
3392
3393# Forward a received context unchanged into a carrier: its context fields are
3394# replaced by the traceparent value of the received pair and by its
3395# tracestate fields joined into one field, and the other fields keep their
3396# order. The pair must be there, its tracestate must fit the output budget of
3397# `limits` whole, and both fields must read back under `limits`; otherwise
3398# forwarding fails with a ForwardError and writes nothing, so a received
3399# traceparent never travels with an edited or truncated tracestate (W3C 3.4).
3400# The pair of a context that extraction accepted is refused only when its
3401# tracestate exceeds the output budget, a context built from parts has no
3402# pair to forward, and forwarding again into the carrier written gives that
3403# carrier again.
3404# Laws: forward_carrier, forward_nothing, forward_from_parts,
3405# forward_too_large, forward_extracted and forward_idempotent.
3406def Context.forward(+limits: Limits, incoming: IncomingContext, carrier: List<&2, Header>) ->
3407  Result<&2, &2, ForwardError, List<&2, Header>>:
3408  Forward.pair(limits, IncomingContext.received(incoming), carrier)
3409
3410# The name of a forwarding error; an invalid field adds its error.
3411def ForwardError.show(error: ForwardError) -> String:
3412  match error:
3413    case NothingToForward{}:
3414      "NothingToForward"
3415    case ForwardTooLarge{}:
3416      "ForwardTooLarge"
3417    case InvalidForwardParent{reason}:
3418      "InvalidForwardParent " ++ TraceParentError.show(reason)
3419    case InvalidForwardState{reason}:
3420      "InvalidForwardState " ++ StateError.show(reason)
3421
3422# Continuing or starting
3423# ======================
3424#
3425# Context.continue_or_start_with gives a service its own operation for a
3426# received message (spec #1, "Continue-or-start creates a child when
3427# extraction or the retained base supplies a usable context, and creates a
3428# root otherwise"): a child of the context that extraction keeps, the
3429# message's or the base, or a root when it keeps none. At a trust boundary, a
3430# new trace replaces the kept context instead. Context.send_with then gives
3431# each message the service sends a child of that operation. When generating
3432# an identifier fails, the policy decides: Lenient{} carries on without an
3433# operation, forwarding the received pair unchanged when it can and sending
3434# no context otherwise, and Strict{} returns the error so that the caller can
3435# refuse the operation.
3436
3437# How a service takes the context that extraction keeps, the message's or
3438# the base:
3439#   Continue{}   continue it with a child
3440#   Restart{}    replace it with a new trace, as at a trust boundary: its
3441#                trace ID is not reused, its state is discarded and the root
3442#                defaults apply
3443type Reception is Data:
3444  Continue{}
3445  Restart{}
3446
3447# What the operations do when generating an identifier fails:
3448#   Lenient{}   carry on without a new operation; the result says why
3449#   Strict{}    fail with the GenerationError, so that the caller can refuse
3450#               the operation
3451type FailurePolicy is Data:
3452  Lenient{}
3453  Strict{}
3454
3455# How a service's operation came about:
3456#   Continued{}   a child of the context that extraction kept
3457#   Started{}     a root: extraction kept no context
3458#   Restarted{}   a new trace in place of the kept context (Restart{})
3459type Origin is Data:
3460  Continued{}
3461  Started{}
3462  Restarted{}
3463
3464# The service's own operation for a received message, with the state it
3465# sends, or the error that left it without one. `received` is the message's
3466# incoming context when the service continues it, kept so that a message it
3467# sends can forward the received pair if generating fails; it is None{} for
3468# a root, a restart or a continued base.
3469type Service is Data:
3470  Operating{origin: Origin, outgoing: OutgoingContext, received: Maybe<&2, IncomingContext>}
3471  Untraced{error: GenerationError, received: Maybe<&2, IncomingContext>}
3472
3473# The type an operation returns under `policy`: the value itself with
3474# Lenient{}, and the value or the GenerationError with Strict{}.
3475def FailurePolicy.result(policy: FailurePolicy, A: Data) -> Data:
3476  match policy:
3477    case Lenient{}:
3478      A
3479    case Strict{}:
3480      Result<&2, &2, GenerationError, A>
3481
3482# A value under `policy`: itself with Lenient{}, and what `strict` makes of it
3483# with Strict{}.
3484def Policy.apply(policy: FailurePolicy, -A: Data, strict: A -> Result<&2, &2, GenerationError, A>, value: A) ->
3485  FailurePolicy.result(policy, A):
3486  match policy:
3487    case Lenient{}:
3488      value
3489    case Strict{}:
3490      strict(value)
3491
3492# The source's final state with a value under `policy`.
3493def Policy.apply.done(-S: Type, policy: FailurePolicy, -A: Data, strict: A -> Result<&2, &2, GenerationError, A>,
3494  done: S & A) -> S & FailurePolicy.result(policy, A):
3495  (source, value) = done
3496  (source, Policy.apply(policy, A, strict, value))
3497
3498# The sampled indication of the new trace, a root or a restart, that
3499# Context.continue_or_start_with starts: the one that `sampling` resolves
3500# from the default, not sampled (spec #1, "New roots default to sampled
3501# `0`"). InheritSampled{} has nothing to inherit, and SetSampled{} sets its
3502# own. The default lives here: root and restart generation take the
3503# indication that they are given (spec #41, "Sampling decision when starting
3504# a trace").
3505def Serve.new_trace_sampled(sampling: Sampling) -> Bool:
3506  Sampling.resolve(sampling, False{})
3507
3508# The service that a child of the kept context gives, with `state`, or
3509# Untraced with the error.
3510def Serve.from_child(state: TraceState, received: Maybe<&2, IncomingContext>,
3511  result: Result<&2, &2, GenerationError, LocalContext>) -> Service:
3512  match result:
3513    case Fail{error}:
3514      Untraced{error, received}
3515    case Done{context}:
3516      Operating{Continued{}, OutgoingContext.with_state(context, state), received}
3517
3518# The service that a new trace gives: its generated operation, whose sampled
3519# indication Serve.new_trace_sampled gave its generation, and no state, or
3520# Untraced with the error. A new trace keeps no received pair.
3521def Serve.from_start(origin: Origin, result: Result<&2, &2, GenerationError, LocalContext>) -> Service:
3522  match result:
3523    case Fail{error}:
3524      Untraced{error, None{}}
3525    case Done{context}:
3526      Operating{origin, OutgoingContext.new(context), None{}}
3527
3528# The service's operation as Context.continue_or_start_with decides it for
3529# a received message, before it reads any word: the generation to drive and
3530# what the generation's result makes of the service.
3531#   ContinuePlan{generation, state, received}   a child of the kept context,
3532#                                               sending its `state`
3533#   StartPlan{generation, origin}               a root or a restart, whose
3534#                                               generation has the sampled
3535#                                               indication of
3536#                                               Serve.new_trace_sampled
3537# A host that feeds a generation one word at a time, such as JavaScript code
3538# calling this module, drives ServicePlan.generation and hands the result to
3539# ServicePlan.service (law hosted_service).
3540type ServicePlan is Data:
3541  ContinuePlan{generation: Generation, state: TraceState, received: Maybe<&2, IncomingContext>}
3542  StartPlan{generation: Generation, origin: Origin}
3543
3544# The context that a restart replaces, as Generation.restart takes it: an
3545# incoming base's received context, or an outgoing base's operation as
3546# another participant receives it. The new trace ID reuses neither.
3547def Serve.replaced(base: BaseContext) -> RemoteContext:
3548  match base:
3549    case IncomingBase{incoming}:
3550      IncomingContext.context(incoming)
3551    case OutgoingBase{outgoing}:
3552      RemoteContext.from_traceparent(LocalContext.to_traceparent(OutgoingContext.context(outgoing)))
3553
3554# Continue the kept context with a child, with its parent and state, or
3555# replace it with a new trace, as `reception` says.
3556def Serve.usable(+base: BaseContext, received: Maybe<&2, IncomingContext>, reception: Reception,
3557  sampling: Sampling) -> ServicePlan:
3558  match reception:
3559    case Continue{}:
3560      ContinuePlan{Generation.child(BaseContext.parent(base), sampling), BaseContext.state(base), received}
3561    case Restart{}:
3562      StartPlan{Generation.restart(Serve.replaced(base), Serve.new_trace_sampled(sampling)), Restarted{}}
3563
3564# Take the context that extraction keeps, or start a root without one.
3565def Serve.kept(context: Maybe<&2, BaseContext>, received: Maybe<&2, IncomingContext>, reception: Reception,
3566  sampling: Sampling) -> ServicePlan:
3567  match context:
3568    case None{}:
3569      StartPlan{Generation.root(Serve.new_trace_sampled(sampling)), Started{}}
3570    case Some{+base}:
3571      Serve.usable(base, received, reception, sampling)
3572
3573# The plan of the service's operation for a message (see ServicePlan).
3574def ServicePlan.new(+extraction: Extraction, reception: Reception, sampling: Sampling) -> ServicePlan:
3575  Serve.kept(Extraction.context(extraction), Extraction.incoming(extraction), reception, sampling)
3576
3577# The generation that the plan drives.
3578def ServicePlan.generation(plan: ServicePlan) -> Generation:
3579  match plan:
3580    case ContinuePlan{generation, state, received}:
3581      generation
3582    case StartPlan{generation, origin}:
3583      generation
3584
3585# The service that the result of the plan's generation gives, before the
3586# policy applies: its operation, or Untraced with the error.
3587def ServicePlan.service(plan: ServicePlan, result: Result<&2, &2, GenerationError, LocalContext>) -> Service:
3588  match plan:
3589    case ContinuePlan{generation, state, received}:
3590      Serve.from_child(state, received, result)
3591    case StartPlan{generation, origin}:
3592      Serve.from_start(origin, result)
3593
3594# The source's final state with the service that the plan gives.
3595def Serve.finish(-S: Type, plan: ServicePlan, done: S & Result<&2, &2, GenerationError, LocalContext>) ->
3596  S & Service:
3597  (source, result) = done
3598  (source, ServicePlan.service(plan, result))
3599
3600# Drive the plan's generation from a caller's source.
3601def Serve.run(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, +plan: ServicePlan) ->
3602  IO(S & Service):
3603  IO.bind(S & Result<&2, &2, GenerationError, LocalContext>, S & Service,
3604    Generation.run_with(~S, ~read, source, ServicePlan.generation(plan)),
3605    done => IO.pure(S & Service, Serve.finish(S, plan, done)))
3606
3607# The service for a message, before the policy applies.
3608def Serve.operation(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S,
3609  +extraction: Extraction, reception: Reception, sampling: Sampling) -> IO(S & Service):
3610  Serve.run(~S, ~read, source, ServicePlan.new(extraction, reception, sampling))
3611
3612# A service without an operation as the GenerationError that caused it.
3613def Serve.strict(service: Service) -> Result<&2, &2, GenerationError, Service>:
3614  match service:
3615    case Operating{origin, outgoing, received}:
3616      Done{Operating{origin, outgoing, received}}
3617    case Untraced{error, received}:
3618      Fail{error}
3619
3620# Give a service its own operation for a received message, from a caller's
3621# source (see the section's introduction). Laws: continue_usable,
3622# restart_usable, start_unusable and restart_keeps_nothing.
3623def Context.continue_or_start_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S,
3624  +extraction: Extraction, reception: Reception, sampling: Sampling, +policy: FailurePolicy) ->
3625  IO(S & FailurePolicy.result(policy, Service)):
3626  IO.bind(S & Service, S & FailurePolicy.result(policy, Service),
3627    Serve.operation(~S, ~read, source, extraction, reception, sampling),
3628    done => IO.pure(S & FailurePolicy.result(policy, Service), Policy.apply.done(S, policy, Service, Serve.strict,
3629      done)))
3630
3631# Sending
3632# =======
3633#
3634# Context.send_with gives one message that the service sends the context of
3635# a new operation: a child of the service's operation, generated anew for
3636# every message, so that each request of a fan-out is an operation of its
3637# own (spec #1, "each distinct outgoing operation obtains its own child
3638# before injection"). When the service has no operation, or when the child
3639# cannot be generated, no new operation is reported: the message forwards the
3640# received pair unchanged if it can be sent whole, and carries no context
3641# fields otherwise (spec #1, "It may forward only an entirely accepted
3642# original pair that can be sent intact within bounds; otherwise clear
3643# outgoing context fields").
3644
3645# Why a message without a new operation does not forward a received pair:
3646#   NothingKept{}          the service keeps no received context: its
3647#                          operation is, or was to be, a root, a restart or
3648#                          a child of a base
3649#   ForwardFailed{error}   Context.forward refused the received context with
3650#                          `error`
3651type Unforwarded is Data:
3652  NothingKept{}
3653  ForwardFailed{error: ForwardError}
3654
3655# The context fields of one message and how they came about:
3656#   Fresh{operation, injection}      a new operation, injected with the
3657#                                    service's state
3658#   Forwarded{carrier, error}        no operation could be generated (`error`);
3659#                                    the received pair is forwarded unchanged
3660#   NoContext{carrier, error,        no operation could be generated, and no
3661#     reason}                        pair was forwarded (`reason`): the context
3662#                                    fields are cleared
3663type Sent is Data:
3664  Fresh{operation: LocalContext, injection: Injection}
3665  Forwarded{carrier: List<&2, Header>, error: GenerationError}
3666  NoContext{carrier: List<&2, Header>, error: GenerationError, reason: Unforwarded}
3667
3668# The fallback when a forwarding of the received pair was tried.
3669def Send.forwarded(result: Result<&2, &2, ForwardError, List<&2, Header>>, error: GenerationError,
3670  carrier: List<&2, Header>) -> Sent:
3671  match result:
3672    case Done{forwarded}:
3673      Forwarded{forwarded, error}
3674    case Fail{reason}:
3675      NoContext{Context.clear(carrier), error, ForwardFailed{reason}}
3676
3677# The fields a message carries when no operation could be generated: the
3678# received pair forwarded unchanged if it can be, and no context fields
3679# otherwise.
3680def Send.fallback(+limits: Limits, received: Maybe<&2, IncomingContext>, error: GenerationError,
3681  +carrier: List<&2, Header>) -> Sent:
3682  match received:
3683    case None{}:
3684      NoContext{Context.clear(carrier), error, NothingKept{}}
3685    case Some{incoming}:
3686      Send.forwarded(Context.forward(limits, incoming, carrier), error, carrier)
3687
3688# The message that a generated child gives: the child injected with the
3689# service's state, or the fallback.
3690def Send.of(+limits: Limits, +outgoing: OutgoingContext, received: Maybe<&2, IncomingContext>,
3691  +carrier: List<&2, Header>, result: Result<&2, &2, GenerationError, LocalContext>) -> Sent:
3692  match result:
3693    case Fail{error}:
3694      Send.fallback(limits, received, error, carrier)
3695    case Done{+operation}:
3696      Fresh{operation, Context.inject(limits, OutgoingContext.with_state(operation, OutgoingContext.state(outgoing)),
3697        carrier)}
3698
3699# A message's operation as Context.send_with decides it before it reads any
3700# word, with the limits and the carrier to send it with:
3701#   SendChild{generation, limits, outgoing, received, carrier}
3702#     a child of the service's operation, injected with the service's state
3703#   SendFallback{error, limits, received, carrier}
3704#     no operation, for a service without one: the fallback, reading no word
3705# A host that feeds a generation one word at a time drives
3706# SendPlan.generation and hands the result to SendPlan.sent (law
3707# hosted_send).
3708type SendPlan is Data:
3709  SendChild{generation: Generation, limits: Limits, outgoing: OutgoingContext,
3710    received: Maybe<&2, IncomingContext>, carrier: List<&2, Header>}
3711  SendFallback{error: GenerationError, limits: Limits, received: Maybe<&2, IncomingContext>,
3712    carrier: List<&2, Header>}
3713
3714# The plan of one message that the service sends (see SendPlan).
3715def SendPlan.new(limits: Limits, service: Service, sampling: Sampling, carrier: List<&2, Header>) -> SendPlan:
3716  match service:
3717    case Operating{origin, +outgoing, received}:
3718      SendChild{Generation.child(LocalParent{OutgoingContext.context(outgoing)}, sampling), limits, outgoing, received,
3719        carrier}
3720    case Untraced{error, received}:
3721      SendFallback{error, limits, received, carrier}
3722
3723# The generation that the plan drives. A service without an operation has
3724# none to drive: its generation has already failed with the service's
3725# error, so that a host reads no word.
3726def SendPlan.generation(plan: SendPlan) -> Generation:
3727  match plan:
3728    case SendChild{generation, limits, outgoing, received, carrier}:
3729      generation
3730    case SendFallback{error, limits, received, carrier}:
3731      Generation{0n, Failed{error}}
3732
3733# The message that the result of the plan's generation gives, before the
3734# policy applies. The fallback of a service without an operation does not
3735# depend on it.
3736def SendPlan.sent(plan: SendPlan, result: Result<&2, &2, GenerationError, LocalContext>) -> Sent:
3737  match plan:
3738    case SendChild{generation, limits, outgoing, received, carrier}:
3739      Send.of(limits, outgoing, received, carrier, result)
3740    case SendFallback{error, limits, received, carrier}:
3741      Send.fallback(limits, received, error, carrier)
3742
3743# The source's final state with the message that the plan gives.
3744def Send.finish(-S: Type, plan: SendPlan, done: S & Result<&2, &2, GenerationError, LocalContext>) -> S & Sent:
3745  (source, result) = done
3746  (source, SendPlan.sent(plan, result))
3747
3748# Drive the plan's generation from a caller's source.
3749def Send.run(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, +plan: SendPlan) ->
3750  IO(S & Sent):
3751  IO.bind(S & Result<&2, &2, GenerationError, LocalContext>, S & Sent,
3752    Generation.run_with(~S, ~read, source, SendPlan.generation(plan)),
3753    done => IO.pure(S & Sent, Send.finish(S, plan, done)))
3754
3755# A message without a new operation as the GenerationError that caused it.
3756def Send.strict(sent: Sent) -> Result<&2, &2, GenerationError, Sent>:
3757  match sent:
3758    case Fresh{operation, injection}:
3759      Done{Fresh{operation, injection}}
3760    case Forwarded{carrier, error}:
3761      Fail{error}
3762    case NoContext{carrier, error, reason}:
3763      Fail{error}
3764
3765# Give one message that the service sends the context of a new operation,
3766# from a caller's source (see the section's introduction). `carrier` is the
3767# message's own fields; its old context fields are replaced in every case.
3768# Laws: send_operating, send_untraced and send_reports_generated.
3769def Context.send_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, +limits: Limits,
3770  service: Service, sampling: Sampling, +policy: FailurePolicy, +carrier: List<&2, Header>) ->
3771  IO(S & FailurePolicy.result(policy, Sent)):
3772  IO.bind(S & Sent, S & FailurePolicy.result(policy, Sent),
3773    Send.run(~S, ~read, source, SendPlan.new(limits, service, sampling, carrier)),
3774    done => IO.pure(S & FailurePolicy.result(policy, Sent), Policy.apply.done(S, policy, Sent, Send.strict, done)))
3775
3776# The name of an origin.
3777def Origin.show(origin: Origin) -> String:
3778  match origin:
3779    case Continued{}:
3780      "Continued"
3781    case Started{}:
3782      "Started"
3783    case Restarted{}:
3784      "Restarted"
3785
3786# How the service's operation came about; None{} without an operation.
3787def Service.origin(service: Service) -> Maybe<&2, Origin>:
3788  match service:
3789    case Operating{origin, outgoing, received}:
3790      Some{origin}
3791    case Untraced{error, received}:
3792      None{}
3793
3794# The service's operation with the state it sends; None{} without one.
3795def Service.outgoing(service: Service) -> Maybe<&2, OutgoingContext>:
3796  match service:
3797    case Operating{origin, outgoing, received}:
3798      Some{outgoing}
3799    case Untraced{error, received}:
3800      None{}
3801
3802# Why the service has no operation; None{} with one.
3803def Service.error(service: Service) -> Maybe<&2, GenerationError>:
3804  match service:
3805    case Operating{origin, outgoing, received}:
3806      None{}
3807    case Untraced{error, received}:
3808      Some{error}
3809
3810# Add or update an entry of the state that the service's operation sends,
3811# such as this participant's own (see OutgoingContext.set). A service
3812# without an operation is unchanged: it sends no state of its own.
3813def Service.set(service: Service, key: StateKey, value: StateValue) -> Service:
3814  match service:
3815    case Operating{origin, outgoing, received}:
3816      Operating{origin, OutgoingContext.set(outgoing, key, value), received}
3817    case Untraced{error, received}:
3818      Untraced{error, received}
3819
3820# Delete an entry of the state that the service's operation sends (see
3821# OutgoingContext.remove). A service without an operation is unchanged.
3822def Service.remove(service: Service, key: StateKey) -> Service:
3823  match service:
3824    case Operating{origin, outgoing, received}:
3825      Operating{origin, OutgoingContext.remove(outgoing, key), received}
3826    case Untraced{error, received}:
3827      Untraced{error, received}
3828
3829# The name of a service's origin, or Untraced with its error. It includes no
3830# received value.
3831def Service.show(service: Service) -> String:
3832  match service:
3833    case Operating{origin, outgoing, received}:
3834      Origin.show(origin)
3835    case Untraced{error, received}:
3836      "Untraced " ++ GenerationError.show(error)
3837
3838# Why no pair was forwarded: NothingKept, or the ForwardError's name.
3839def Unforwarded.show(reason: Unforwarded) -> String:
3840  match reason:
3841    case NothingKept{}:
3842      "NothingKept"
3843    case ForwardFailed{error}:
3844      ForwardError.show(error)
3845
3846# The fields to send with the message, in every case.
3847def Sent.carrier(sent: Sent) -> List<&2, Header>:
3848  match sent:
3849    case Fresh{operation, injection}:
3850      Injection.carrier(injection)
3851    case Forwarded{carrier, error}:
3852      carrier
3853    case NoContext{carrier, error, reason}:
3854      carrier
3855
3856# The new operation that the message carries; None{} for a fallback.
3857def Sent.operation(sent: Sent) -> Maybe<&2, LocalContext>:
3858  match sent:
3859    case Fresh{operation, injection}:
3860      Some{operation}
3861    case Forwarded{carrier, error}:
3862      None{}
3863    case NoContext{carrier, error, reason}:
3864      None{}
3865
3866# Why no operation could be generated; None{} for a new operation.
3867def Sent.error(sent: Sent) -> Maybe<&2, GenerationError>:
3868  match sent:
3869    case Fresh{operation, injection}:
3870      None{}
3871    case Forwarded{carrier, error}:
3872      Some{error}
3873    case NoContext{carrier, error, reason}:
3874      Some{error}
3875
3876# The keys that truncating the service's state to the output budget dropped
3877# from a new operation's message (see Injection.dropped); none for a
3878# fallback, which sends no state of its own.
3879def Sent.dropped(sent: Sent) -> List<&2, StateKey>:
3880  match sent:
3881    case Fresh{operation, injection}:
3882      Injection.dropped(injection)
3883    case Forwarded{carrier, error}:
3884      Nil{}
3885    case NoContext{carrier, error, reason}:
3886      Nil{}
3887
3888# The name of a new operation's message, saying whether its state was
3889# truncated.
3890def Send.fresh(dropped: List<&2, StateKey>) -> String:
3891  match dropped:
3892    case Nil{}:
3893      "Fresh"
3894    case Con{key, rest}:
3895      "Fresh, truncated"
3896
3897# The name of a message's context: Fresh, saying whether its state was
3898# truncated, or for a fallback why no operation was generated and, without a
3899# forwarded pair, why none was forwarded. It includes no received value.
3900def Sent.show(sent: Sent) -> String:
3901  match sent:
3902    case Fresh{operation, injection}:
3903      Send.fresh(Injection.dropped(injection))
3904    case Forwarded{carrier, error}:
3905      "Forwarded after " ++ GenerationError.show(error)
3906    case NoContext{carrier, error, reason}:
3907      "NoContext after " ++ GenerationError.show(error) ++ ", " ++ Unforwarded.show(reason)