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