1 # bend-trace-context: the pure Trace Context core 2 # =============================================== 3 # 4 # This file is the package's public entry for everything that performs no host 5 # effect: the strict traceparent v00 codec, validated trace and span IDs and 6 # their bytes, local and remote contexts, the machine that turns source words 7 # into IDs, validated limits, the Level 2 tracestate parser, tracestate 8 # updates and emission, outgoing contexts, the extraction of a received 9 # message's context, the injection and forwarding of a context into an 10 # outgoing message's carrier, and the operations that continue or start a 11 # service's operation for a received message and give each message it sends a 12 # child of it. 13 # generation.bend adds the host's cryptographic source on top of it, and 14 # native_http.bend the header maps of bend-kit's native HTTP package. The 15 # claims this code must satisfy are stated in LAWS.bend and proved in 16 # PROOF.bend, beside this file. The tests in tests/*.bend here and the 17 # repository's consumer in tests/consumer exercise it through the same public 18 # names. 19 # 20 # The normative reference is W3C Trace Context Level 2, Candidate 21 # Recommendation Draft of 2024-03-28 ("W3C" below, with section numbers). The 22 # approved specification is issue #1 of the repository ("spec #1"), and issue 23 # #41 ("spec #41") adds the building blocks that an OpenTelemetry SDK 24 # composes. 25 # 26 # Contents 27 # 28 # Types every data type of the codec, contexts and 29 # generation, declared first 30 # Strict v00 codec Parse.*, TraceParentV00.* 31 # Identifiers and contexts TraceId, SpanId, contexts and their 32 # trace flags, children, restarts 33 # Identifiers from source words U32.to_hex, TraceId.from_words, ... 34 # Identifiers as bytes TraceId.to_bytes, TraceId.from_bytes, 35 # SpanId.to_bytes, SpanId.from_bytes 36 # Generation machine Drive.*, TraceDraw.*, SpanDraw.*, 37 # SpanPlan.*, TracePlan.*, Step.*, Draw.*, 38 # TraceId.generate_with, 39 # SpanId.generate_with, Generation.*, 40 # Context.*_with, Source.tape 41 # Error messages Error.show, ContextError.show, ... 42 # Limits Limits.new, Limits.default, accessors 43 # Tracestate keys and values, states and lookups, 44 # budgets, and the reading machine behind 45 # TraceState.parse 46 # Tracestate updates and emission TraceState.set, remove, size and 47 # truncate 48 # Outgoing contexts OutgoingContext, a local context with the 49 # state it sends, and its Emission 50 # Extraction Context.extract, TraceParent.read, 51 # incoming and base contexts, diagnostics 52 # Injection Context.inject and the Injection it 53 # writes, Context.field_names, 54 # Context.clear 55 # Forwarding Context.forward, ForwardError 56 # Continuing or starting Context.continue_or_start_with, 57 # Reception, FailurePolicy, Service, 58 # ServicePlan 59 # Sending Context.send_with, Sent, SendPlan 60 # 61 # The public names are documented in packages/trace-context/README.md. Names in 62 # the Parse, Parsed, ParsedBytes, Flags, Drive, TraceDraw, SpanDraw, 63 # TraceStep, SpanStep, SpanPlan, TracePlan, Draw, Step, Tape, Scan, Member, 64 # Value, Budget, Utf8, Entries, StateChar, Carrier, Text, Read, Extract, 65 # Forward, Policy, Serve and Send namespaces are internal: Bend lets any module 66 # import them, but they are not a compatibility contract. 67 # 68 # Notes for readers new to Bend 69 # ----------------------------- 70 # 71 # - `type T is Data:` declares a type whose values may be copied. Each indented 72 # line is a constructor with its fields, such as `Some{value}`. 73 # - A field whose type is an equation, such as 74 # `evidence: {StateKey.is_valid(text) == True{} : Bool}`, stores a proof. A 75 # value can only be built together with that proof, so the rule holds for 76 # every value a program handles, and code that receives one never checks it 77 # again. The checker verifies the proof when the program is compiled. The 78 # `.checked` helpers turn the result of a run-time check into such a proof: 79 # they receive the Bool and an equation stating what it is, and matching on 80 # the Bool refines that equation to `... == True{}` in the accepting case. 81 # - `Result<&2, &2, E, T>` is Done{value} or Fail{error}, and `Maybe<&2, T>` is 82 # Some{value} or None{}. The `&2` arguments say that the values may be copied. 83 # - A parameter may be used at most once unless it is marked `+x` (reusable). 84 # `-x` is erased: only the checker sees it. `~f` is a template: its argument 85 # is substituted at compile time, so it names top-level definitions only. 86 # - `match` may only inspect a parameter or a variable bound by a pattern, never 87 # a computed value, and definitions may not call each other in a cycle. Many 88 # helpers therefore receive a Bool computed by their caller and match on it: 89 # `Scan.read(comma, ...)` receives `Char.is_eq(char, ',')`, for example. 90 # - In every recursive call, the first argument that changes must be 91 # structurally smaller, so every function terminates. A recursion whose depth 92 # could grow with received text is written as a tail call, which compiles to 93 # a loop: the JavaScript backend overflows its stack after a few thousand 94 # nested calls, and a received value may be 32 KiB long. The other 95 # recursions are bounded: at most 32 digits, 256 characters of a key or 96 # value, 32 entries, or the characters of a field name sought. 97 # - `do Result<...>:` sequences steps that may fail: `x : T <- step` stops at 98 # the first Fail, and the block ends with `return v` or with a last step. 99 100 import Base 101 import ./src/hex.bend as Hex 102 import ./src/digits.bend as Digits 103 104 # Types 105 # ===== 106 # 107 # The types of the codec, of the identifiers and contexts, and of the 108 # generation machine. The limits, tracestate, outgoing, extraction, injection, 109 # forwarding, continue-or-start and sending types are declared in their own 110 # sections below. 111 112 # The field that a ZeroId error names: the trace ID or parent ID of a 113 # traceparent value, or a supplied span ID. 114 type Field is Data: 115 TraceIdField{} 116 ParentIdField{} 117 SpanIdField{} 118 119 # Why the strict codec, TraceId.parse, SpanId.parse or TraceParent.read 120 # refused a text, or TraceId.from_bytes or SpanId.from_bytes a list of bytes. 121 # Offsets count Bend characters (Unicode code points) from zero at the start 122 # of the text, or cells from zero at the start of the list, and the first 123 # problem in reading order is reported. 124 # UnexpectedEnd{offset} the text ends where a character is required, 125 # or the list where a byte is 126 # InvalidHex{offset} this character is not a lowercase hex digit 127 # InvalidByte{offset} this cell is above 255, so it is not a byte 128 # ExpectedSeparator{offset} this character should be "-" 129 # TrailingInput{} characters follow a complete value, or cells 130 # follow the bytes of an ID 131 # ForbiddenVersion{} the version is ff, forbidden by W3C 3.2.2.1 132 # UnsupportedVersion{version} a version other than 00, which the strict 133 # codec does not read (TraceParent.read reads 134 # versions 01 to fe by their known prefix) 135 # ZeroId{field} the named ID is all zero, forbidden by W3C 136 # 3.2.2.3 and 3.2.2.4 137 # ControlCharacter{offset} this character is a control character other 138 # than a horizontal tab, which no field value 139 # may hold (RFC 9110, section 5.5); only 140 # TraceParent.read reports it, in the fields 141 # of a later version that it does not read 142 type Error is Data: 143 UnexpectedEnd{offset: Nat} 144 InvalidHex{offset: Nat} 145 InvalidByte{offset: Nat} 146 ExpectedSeparator{offset: Nat} 147 TrailingInput{} 148 ForbiddenVersion{} 149 UnsupportedVersion{version: String} 150 ZeroId{field: Field} 151 ControlCharacter{offset: Nat} 152 153 # Why creating a context from supplied IDs was refused: a child reused its 154 # parent's span ID, or a restart reused the received trace ID. 155 type ContextError is Data: 156 ReusedSpanId{} 157 ReusedTraceId{} 158 159 # A sequence of n digits read from the front of a text, with the text that 160 # remains after it. The length n is part of the type, so a reader of 32 digits 161 # can only produce 32. 162 type Parsed<-n: Nat> is Data: 163 Parsed{digits: Digits.Digits(n), rest: String} 164 165 # The digits of n bytes read from the front of a list of cells, two digits per 166 # byte, with the cells that remain after them. 167 type ParsedBytes<-n: Nat> is Data: 168 ParsedBytes{digits: Digits.Digits(Nat.double(n)), rest: List<&2, U32>} 169 170 # A strict traceparent v00 value (W3C 3.2.2): a trace ID of 32 digits and a 171 # parent ID of 16 digits, each with a proof that it is not all zero, and a flag 172 # byte of two digits. Length and alphabet are structural: a value with a wrong 173 # length or a non-hexadecimal digit cannot be built. All eight flag bits are 174 # kept, including the reserved ones, so the codec is exact. 175 type TraceParentV00 is Data: 176 TraceParentV00{ 177 trace_id: Digits.NonZero<32n>, 178 parent_id: Digits.NonZero<16n>, 179 flags: Digits.Digits(2n) 180 } 181 182 # A validated trace ID: 32 lowercase hexadecimal digits, not all zero (W3C 183 # 3.2.2.3). `random` records whether the random-trace-id flag (W3C 3.2.2.5.2) 184 # may be emitted for it. A parsed ID makes no such assertion: only its origin 185 # can justify one. Generation sets it, and a caller who knows the ID is random 186 # sets it with TraceId.assert_random. 187 type TraceId is Data: 188 TraceId{value: Digits.NonZero<32n>, random: Bool} 189 190 # A validated span ID: 16 lowercase hexadecimal digits, not all zero, the 191 # identifier of one operation. It is sent as the parent ID of traceparent (W3C 192 # 3.2.2.4). 193 type SpanId is Data: 194 SpanId{value: Digits.NonZero<16n>} 195 196 # How a child operation obtains its sampled indication (W3C 3.2.2.5.1): 197 # InheritSampled{} keeps the parent's and SetSampled{sampled} sets it. The 198 # indication communicates a decision; it does not record anything. 199 type Sampling is Data: 200 InheritSampled{} 201 SetSampled{sampled: Bool} 202 203 # A context received from another participant. It identifies the sender's 204 # operation and keeps only the known flags: sampled and random-trace-id. It is 205 # built from a received value (RemoteContext.from_traceparent) or from its 206 # parts (RemoteContext.from_ids), and has its own type, so it cannot be sent 207 # as if it were this participant's operation. 208 type RemoteContext is Data: 209 RemoteContext{trace_id: TraceId, span_id: SpanId, sampled: Bool} 210 211 # A context that identifies an operation of this participant: the one it sends 212 # in its own headers. The Context.* operations build it. 213 type LocalContext is Data: 214 LocalContext{trace_id: TraceId, span_id: SpanId, sampled: Bool} 215 216 # The context whose trace a child operation continues: a received context or 217 # one of this participant's own operations. 218 type Parent is Data: 219 RemoteParent{context: RemoteContext} 220 LocalParent{context: LocalContext} 221 222 # Why generating identifiers failed. A source failure carries the source's own 223 # code and message; exhaustion names the identifier whose eight candidates were 224 # all rejected. 225 type GenerationError is Data: 226 SourceFailure{code: U32, message: String} 227 ExhaustedTraceId{} 228 ExhaustedSpanId{} 229 230 # The words read so far for the current trace ID candidate, in arrival order. 231 # Four words complete a candidate. 232 type TraceWords is Data: 233 NoTraceWord{} 234 OneTraceWord{first: U32} 235 TwoTraceWords{first: U32, second: U32} 236 ThreeTraceWords{first: U32, second: U32, third: U32} 237 238 # The words read so far for the current span ID candidate. Two words complete 239 # a candidate. 240 type SpanWords is Data: 241 NoSpanWord{} 242 OneSpanWord{first: U32} 243 244 # The generation machine below is shared by the IO operations and stated in 245 # the laws. Its types and its TraceDraw, SpanDraw, TraceStep, SpanStep, 246 # SpanPlan, TracePlan, Draw, Step and Drive functions are internal: callers use 247 # TraceId.generate_with, SpanId.generate_with and the `Context.*_with` 248 # operations, or generation.bend, and a host that feeds words itself uses 249 # Generation. 250 # 251 # A trace ID draw that waits for a word: `remaining` counts the further 252 # candidates allowed after the current one, so each draw gets eight 253 # candidates in all, `words` holds the words of the current candidate, and 254 # `excluded` is the trace ID that no candidate may repeat, such as the 255 # received one that a restart replaces. 256 type TraceDraw is Data: 257 TraceDraw{remaining: Nat, words: TraceWords, excluded: Maybe<&2, TraceId>} 258 259 # A span ID draw that waits for a word, as TraceDraw: `excluded` is the span 260 # ID that no candidate may repeat, such as a child's parent's. 261 type SpanDraw is Data: 262 SpanDraw{remaining: Nat, words: SpanWords, excluded: Maybe<&2, SpanId>} 263 264 # A trace ID draw after each source word, whether it generates a trace ID 265 # alone or the trace ID of a root or a restart: it waits for another word, it 266 # drew a trace ID, or it failed. 267 type TraceStep is Data: 268 NeedTraceWord{draw: TraceDraw} 269 DrawnTraceId{id: TraceId} 270 TraceFailed{error: GenerationError} 271 272 # A span ID draw after each source word, whether it generates a span ID alone 273 # or the span ID of a root, a child or a restart, as TraceStep. 274 type SpanStep is Data: 275 NeedSpanWord{draw: SpanDraw} 276 DrawnSpanId{id: SpanId} 277 SpanFailed{error: GenerationError} 278 279 # What a new local context needs besides its span ID: the span ID that it must 280 # not repeat (`excluded`), such as a child's parent's, the trace ID that it 281 # belongs to, and its sampled indication. SpanPlan.root and SpanPlan.child 282 # give the plans of a root and a child. 283 type SpanPlan is Data: 284 SpanPlan{excluded: Maybe<&2, SpanId>, trace_id: TraceId, sampled: Bool} 285 286 # What a new trace needs, a root or a restart: the trace ID that its trace 287 # ID must not repeat (`excluded`), none for a root and the received one for 288 # a restart, and the sampled indication of the context that it creates. 289 # TracePlan.root and TracePlan.restart give the plans of a root and a 290 # restart; the generation machine (TracePlan.draw), the generation that a 291 # host feeds (Generation.new_trace) and the composition on a caller's source 292 # (TracePlan.generate_with) each run one plan, so a root and a restart 293 # differ only in it. 294 type TracePlan is Data: 295 TracePlan{excluded: Maybe<&2, TraceId>, sampled: Bool} 296 297 # A generation in progress: the trace ID draw of a root or a restart, with 298 # the sampled indication of the context that it starts, or a span ID draw, 299 # with the trace ID and the sampled indication of the context that its span 300 # ID completes. 301 type Draw is Data: 302 DrawTrace{draw: TraceDraw, sampled: Bool} 303 DrawSpan{draw: SpanDraw, trace_id: TraceId, sampled: Bool} 304 305 # The state of a generation after each source word: it needs another word, it 306 # created a context, or it failed. 307 type Step is Data: 308 NeedWord{draw: Draw} 309 Created{context: LocalContext} 310 Failed{error: GenerationError} 311 312 # A generation with its word budget, for a host that feeds it one word at a 313 # time instead of passing a source as a template, such as JavaScript code 314 # calling this module: the words it may still read (`fuel`) and the 315 # machine's step. Its fields are internal, like Step: Generation.root and 316 # its siblings build one. Context.continue_or_start_with and 317 # Context.send_with drive the same values, and a host that feeds words while 318 # Generation.needs says so gets the pure driver's result (law 319 # generation_drive). Context.root_with and its siblings compose the 320 # separate generation, whose results laws root_tape and its siblings give as 321 # that driver's. 322 type Generation is Data: 323 Generation{fuel: Nat, step: Step} 324 325 # Strict v00 codec 326 # ================ 327 # 328 # TraceParentV00.parse reads exactly "00-", 32 lowercase hexadecimal digits, 329 # "-", 16 digits, "-" and two digits (W3C 3.2.2). The helpers below read one 330 # field at a time and report the first problem with the offset of the 331 # offending character. 332 333 # Put one more digit in front of a parsed sequence: n digits become 1 + n. 334 def Parsed.prepend(-n: Nat, digit: Hex.Digit, parsed: Parsed) -> Parsed<1n+n>: 335 match parsed: 336 case Parsed{digits, rest}: 337 Parsed{Digits.DCon{digit, digits}, rest} 338 339 # A decoded character, or InvalidHex at its offset when it is not a lowercase 340 # hexadecimal digit. 341 def Parse.digit_result(value: Maybe<&2, Hex.Digit>, offset: Nat) -> 342 Result<&2, &2, Error, Hex.Digit>: 343 match value: 344 case None{}: 345 Fail{InvalidHex{offset}} 346 case Some{digit}: 347 Done{digit} 348 349 # Decode one character as a lowercase hexadecimal digit. 350 def Parse.digit(char: Char, offset: Nat) -> Result<&2, &2, Error, Hex.Digit>: 351 Parse.digit_result(Hex.Digit.from_char(char), offset) 352 353 # Consume exactly n characters as digits, keeping the unconsumed rest of the 354 # text. The recursion decreases n, so no length check or unchecked conversion 355 # is needed: the result's type already has length n. 356 def Parse.digits(n: Nat, text: String, offset: Nat) -> 357 Result<&2, &2, Error, Parsed>: 358 match n: 359 case 0n: 360 Done{Parsed{Digits.DNil{}, text}} 361 case 1n+p: 362 match text: 363 case SNil{}: 364 Fail{UnexpectedEnd{offset}} 365 case SCon{char, tail}: 366 +at = offset 367 do Result<&2, &2, Error, Parsed<1n+p>>: 368 digit : Hex.Digit <- Parse.digit(char, at) 369 parsed : Parsed

<- Parse.digits(p, tail, 1n+at) 370 return Parsed.prepend(p, digit, parsed) 371 372 # The rest of the text after a "-", or ExpectedSeparator at its offset. 373 def Parse.separator_result(tail: String, ok: Bool, offset: Nat) -> 374 Result<&2, &2, Error, String>: 375 match ok: 376 case False{}: 377 Fail{ExpectedSeparator{offset}} 378 case True{}: 379 Done{tail} 380 381 # Read the "-" expected at `offset`. 382 def Parse.separator(text: String, offset: Nat) -> Result<&2, &2, Error, String>: 383 match text: 384 case SNil{}: 385 Fail{UnexpectedEnd{offset}} 386 case SCon{char, tail}: 387 Parse.separator_result(tail, Char.is_eq(char, '-'), offset) 388 389 # The value must end here. Only the first character after it is inspected, so 390 # an arbitrarily long suffix is refused without being read. 391 def Parse.end(text: String) -> Result<&2, &2, Error, Unit>: 392 match text: 393 case SNil{}: 394 Done{Unit{}} 395 case SCon{char, tail}: 396 Fail{TrailingInput{}} 397 398 # The version digits: 00 is the only version the strict codec reads, ff is 399 # forbidden (W3C 3.2.2.1), and any other version is reported with its text. 400 def Parse.version(digits: Digits.Digits(2n)) -> Result<&2, &2, Error, Unit>: 401 match digits: 402 case Digits.DCon{Hex.H0{}, Digits.DCon{Hex.H0{}, Digits.DNil{}}}: 403 Done{Unit{}} 404 case Digits.DCon{Hex.Hf{}, Digits.DCon{Hex.Hf{}, Digits.DNil{}}}: 405 Fail{ForbiddenVersion{}} 406 case other: 407 Fail{UnsupportedVersion{Digits.Digits.to_string(2n, other)}} 408 409 # Attach the proof that digits are not all zero, or fail with ZeroId naming 410 # the field. 411 def Parse.nonzero_result(-n: Nat, result: Maybe<&2, Digits.NonZero>, field: Field) -> 412 Result<&2, &2, Error, Digits.NonZero>: 413 match result: 414 case None{}: 415 Fail{ZeroId{field}} 416 case Some{id}: 417 Done{id} 418 419 # Check that digits are not all zero (W3C 3.2.2.3, 3.2.2.4). 420 def Parse.nonzero(n: Nat, digits: Digits.Digits(n), field: Field) -> 421 Result<&2, &2, Error, Digits.NonZero>: 422 Parse.nonzero_result(n, Digits.NonZero.new(n, digits), field) 423 424 # The last field: the two flag digits, then the end of the text. 425 def Parse.flags(trace_id: Digits.NonZero<32n>, parent_id: Digits.NonZero<16n>, 426 parsed: Parsed<2n>) -> Result<&2, &2, Error, TraceParentV00>: 427 match parsed: 428 case Parsed{flags, rest}: 429 do Result<&2, &2, Error, TraceParentV00>: 430 end : Unit <- Parse.end(rest) 431 return TraceParentV00{trace_id, parent_id, flags} 432 433 # After the trace ID: the parent ID, which must not be all zero, its "-" at 434 # offset 52 and the flag digits at offset 53. 435 def Parse.parent(trace_id: Digits.NonZero<32n>, parsed: Parsed<16n>) -> 436 Result<&2, &2, Error, TraceParentV00>: 437 match parsed: 438 case Parsed{parent_digits, rest}: 439 do Result<&2, &2, Error, TraceParentV00>: 440 parent_id : Digits.NonZero<16n> <- Parse.nonzero(16n, parent_digits, ParentIdField{}) 441 after : String <- Parse.separator(rest, 52n) 442 flags : Parsed<2n> <- Parse.digits(2n, after, 53n) 443 Parse.flags(trace_id, parent_id, flags) 444 445 # After the version: the trace ID, which must not be all zero, its "-" at 446 # offset 35 and the parent ID from offset 36. 447 def Parse.trace(parsed: Parsed<32n>) -> Result<&2, &2, Error, TraceParentV00>: 448 match parsed: 449 case Parsed{trace_digits, rest}: 450 do Result<&2, &2, Error, TraceParentV00>: 451 trace_id : Digits.NonZero<32n> <- Parse.nonzero(32n, trace_digits, TraceIdField{}) 452 after : String <- Parse.separator(rest, 35n) 453 parent : Parsed<16n> <- Parse.digits(16n, after, 36n) 454 Parse.parent(trace_id, parent) 455 456 # After the two version digits: the version check, the "-" at offset 2 and the 457 # trace ID from offset 3. 458 def Parse.start(parsed: Parsed<2n>) -> Result<&2, &2, Error, TraceParentV00>: 459 match parsed: 460 case Parsed{version, rest}: 461 do Result<&2, &2, Error, TraceParentV00>: 462 version_ok : Unit <- Parse.version(version) 463 after : String <- Parse.separator(rest, 2n) 464 trace : Parsed<32n> <- Parse.digits(32n, after, 3n) 465 Parse.trace(trace) 466 467 # Parse a strict traceparent v00 value: exactly "00-", 32 lowercase 468 # hexadecimal digits, "-", 16 digits, "-" and two digits; the IDs must not be 469 # all zero. No whitespace, case folding or suffix is accepted, and every flag 470 # byte is kept as received. 471 # This is the strict wire codec, not a complete W3C propagator: 472 # TraceParent.read and Context.extract apply the processing rules of W3C 3.2.4 473 # and 4.1.2, such as reading later versions by their known prefix. 474 # Laws: roundtrip, inverse and formatted_length. 475 def TraceParentV00.parse(text: String) -> Result<&2, &2, Error, TraceParentV00>: 476 do Result<&2, &2, Error, TraceParentV00>: 477 version : Parsed<2n> <- Parse.digits(2n, text, 0n) 478 Parse.start(version) 479 480 # The text of a strict v00 value: always 55 characters. It is total, because 481 # validity is carried by the argument's type, and it preserves every flag bit: 482 # it is the exact inverse of parse, not an outgoing-header policy (see 483 # LocalContext.to_traceparent for what a participant emits). 484 def TraceParentV00.format(context: TraceParentV00) -> String: 485 match context: 486 case TraceParentV00{trace_id, parent_id, flags}: 487 "00-" ++ Digits.NonZero.to_string(32n, trace_id) ++ "-" ++ 488 Digits.NonZero.to_string(16n, parent_id) ++ "-" ++ 489 Digits.Digits.to_string(2n, flags) 490 491 # Whether the sampled flag, bit 0 of the flag byte, is set (W3C 3.2.2.5.1). 492 def TraceParentV00.is_sampled(context: TraceParentV00) -> Bool: 493 match context: 494 case TraceParentV00{trace_id, parent_id, 495 Digits.DCon{high, Digits.DCon{low, Digits.DNil{}}}}: 496 Hex.Digit.is_odd(low) 497 498 # Whether the random-trace-id flag, bit 1, is set (W3C 3.2.2.5.2). It records 499 # the sender's assertion; it does not prove how the trace ID was generated. 500 def TraceParentV00.is_random(context: TraceParentV00) -> Bool: 501 match context: 502 case TraceParentV00{trace_id, parent_id, 503 Digits.DCon{high, Digits.DCon{low, Digits.DNil{}}}}: 504 Hex.Digit.has_bit1(low) 505 506 # Identifiers and contexts 507 # ======================== 508 # 509 # Supplied IDs are parsed with the same digit reader as the codec. Contexts are 510 # created from validated IDs: a root, a child continuing a parent, a restart 511 # replacing a received trace, or the explicit construction of an operation the 512 # caller owns. A context also gives its known trace flags as a number, for an 513 # exporter; its sampled indication and its trace ID's randomness assertion 514 # stay their canonical form, and there is no trace flags type. 515 516 # The digits of a supplied ID must be the whole text, and not all zero. 517 def Parse.id.finish(n: Nat, parsed: Parsed, field: Field) -> 518 Result<&2, &2, Error, Digits.NonZero>: 519 match parsed: 520 case Parsed{digits, rest}: 521 do Result<&2, &2, Error, Digits.NonZero>: 522 end : Unit <- Parse.end(rest) 523 Parse.nonzero(n, digits, field) 524 525 # A supplied ID is exactly n lowercase hexadecimal digits, not all zero. 526 def Parse.id(+n: Nat, text: String, field: Field) -> 527 Result<&2, &2, Error, Digits.NonZero>: 528 do Result<&2, &2, Error, Digits.NonZero>: 529 parsed : Parsed <- Parse.digits(n, text, 0n) 530 Parse.id.finish(n, parsed, field) 531 532 # Parse a supplied trace ID: exactly 32 lowercase hexadecimal digits, not all 533 # zero. Error offsets count from the start of the ID. The result makes no 534 # randomness assertion (laws trace_id_parse and trace_id_accepts). 535 def TraceId.parse(text: String) -> Result<&2, &2, Error, TraceId>: 536 do Result<&2, &2, Error, TraceId>: 537 value : Digits.NonZero<32n> <- Parse.id(32n, text, TraceIdField{}) 538 return TraceId{value, False{}} 539 540 # Record the caller's assertion that these digits were generated randomly, so 541 # that the random-trace-id flag is emitted with them. The caller is responsible 542 # for the assertion; validation cannot establish it (law assert_random). 543 def TraceId.assert_random(id: TraceId) -> TraceId: 544 match id: 545 case TraceId{value, random}: 546 TraceId{value, True{}} 547 548 # Whether the trace ID asserts that it was generated randomly. 549 def TraceId.is_random(id: TraceId) -> Bool: 550 match id: 551 case TraceId{value, random}: 552 random 553 554 # The 32 lowercase hexadecimal digits of the trace ID. 555 def TraceId.to_string(id: TraceId) -> String: 556 match id: 557 case TraceId{value, random}: 558 Digits.NonZero.to_string(32n, value) 559 560 # Whether two trace IDs name the same trace. The randomness assertion is not 561 # part of the identifier, so it is ignored. 562 def TraceId.is_eq(a: TraceId, b: TraceId) -> Bool: 563 String.eq(TraceId.to_string(a), TraceId.to_string(b)) 564 565 # Parse a supplied span ID: exactly 16 lowercase hexadecimal digits, not all 566 # zero (laws span_id_parse and span_id_roundtrip). 567 def SpanId.parse(text: String) -> Result<&2, &2, Error, SpanId>: 568 do Result<&2, &2, Error, SpanId>: 569 value : Digits.NonZero<16n> <- Parse.id(16n, text, SpanIdField{}) 570 return SpanId{value} 571 572 # The 16 lowercase hexadecimal digits of the span ID. 573 def SpanId.to_string(id: SpanId) -> String: 574 match id: 575 case SpanId{value}: 576 Digits.NonZero.to_string(16n, value) 577 578 # Whether two span IDs name the same operation. 579 def SpanId.is_eq(a: SpanId, b: SpanId) -> Bool: 580 String.eq(SpanId.to_string(a), SpanId.to_string(b)) 581 582 # The sampled indication a child receives: the inherited one, unless the 583 # caller set another (law sampling). 584 def Sampling.resolve(sampling: Sampling, inherited: Bool) -> Bool: 585 match sampling: 586 case InheritSampled{}: 587 inherited 588 case SetSampled{sampled}: 589 sampled 590 591 # Interpret a received strict-v00 value as the sender's context. Bit 0 is 592 # sampled and bit 1 is random-trace-id; the reserved bits are not interpreted 593 # and do not travel with the context (law received_flags). 594 def RemoteContext.from_traceparent(value: TraceParentV00) -> RemoteContext: 595 match value: 596 case TraceParentV00{trace_id, parent_id, 597 Digits.DCon{high, Digits.DCon{+low, Digits.DNil{}}}}: 598 RemoteContext{TraceId{trace_id, Hex.Digit.has_bit1(low)}, SpanId{parent_id}, 599 Hex.Digit.is_odd(low)} 600 601 # Build the sender's context from its parts, as an OpenTelemetry SDK does for 602 # a link or for a propagator of another format: its trace ID, its span ID and 603 # its sampled indication, kept as they are. It is total, since the IDs are 604 # valid by construction, and its random-trace-id bit is the trace ID's own 605 # assertion: none for a parsed ID, unless TraceId.assert_random adds it (law 606 # remote_from_ids). The result is still a received context, which a child 607 # continues: it cannot be sent as this participant's operation 608 # (tests/reject/remote_as_local.bend). 609 def RemoteContext.from_ids(trace_id: TraceId, span_id: SpanId, sampled: Bool) -> RemoteContext: 610 RemoteContext{trace_id, span_id, sampled} 611 612 # The trace the received context belongs to. 613 def RemoteContext.trace_id(context: RemoteContext) -> TraceId: 614 match context: 615 case RemoteContext{trace_id, span_id, sampled}: 616 trace_id 617 618 # The sender's operation: the parent ID of the received value. 619 def RemoteContext.span_id(context: RemoteContext) -> SpanId: 620 match context: 621 case RemoteContext{trace_id, span_id, sampled}: 622 span_id 623 624 # The sender's sampled indication. 625 def RemoteContext.is_sampled(context: RemoteContext) -> Bool: 626 match context: 627 case RemoteContext{trace_id, span_id, sampled}: 628 sampled 629 630 # The known trace flags as a number: `sampled` in bit 0 and `random` in bit 1 631 # (W3C 3.2.2.5), with the six reserved bits zero. 632 def Flags.known(sampled: Bool, random: Bool) -> U32: 633 U32.or(Bool.to_u32(sampled), U32.shl(Bool.to_u32(random))) 634 635 # The trace flags that the context keeps, as a number from 0 to 3: bit 0 is 636 # its sampled indication and bit 1 its trace ID's randomness assertion, the 637 # known flags that it was received or built with. Reserved bits are never 638 # among them. The Booleans stay the canonical form; the number is for an 639 # exporter, such as one that writes OTLP's Span.flags field. Laws: 640 # remote_flags and received_trace_flags. 641 def RemoteContext.flags(context: RemoteContext) -> U32: 642 match context: 643 case RemoteContext{trace_id, span_id, sampled}: 644 Flags.known(sampled, TraceId.is_random(trace_id)) 645 646 # The trace this participant's operation belongs to. 647 def LocalContext.trace_id(context: LocalContext) -> TraceId: 648 match context: 649 case LocalContext{trace_id, span_id, sampled}: 650 trace_id 651 652 # This participant's operation. 653 def LocalContext.span_id(context: LocalContext) -> SpanId: 654 match context: 655 case LocalContext{trace_id, span_id, sampled}: 656 span_id 657 658 # The sampled indication this participant sends. 659 def LocalContext.is_sampled(context: LocalContext) -> Bool: 660 match context: 661 case LocalContext{trace_id, span_id, sampled}: 662 sampled 663 664 # The participating representation of a local context: version 00, and flags 665 # limited to sampled (bit 0) and random-trace-id (bit 1), with every reserved 666 # bit zero (W3C 3.2.2.5.3; laws emitted_traceparent and emitted_projection). 667 def LocalContext.to_traceparent(context: LocalContext) -> TraceParentV00: 668 match context: 669 case LocalContext{TraceId{trace_id, random}, SpanId{span_id}, sampled}: 670 TraceParentV00{trace_id, span_id, 671 Digits.DCon{Hex.H0{}, Digits.DCon{Hex.Digit.from_bits(sampled, random, False{}, False{}), Digits.DNil{}}}} 672 673 # The trace flags of the context as a number from 0 to 3: bit 0 is its sampled 674 # indication and bit 1 its trace ID's randomness assertion. It is the flag 675 # byte of the traceparent that the context emits, 00 to 03, so an exporter 676 # that writes it, into OTLP's Span.flags field for example, agrees with what 677 # the context propagates. The Booleans stay the canonical form. Law: 678 # local_flags. 679 def LocalContext.flags(context: LocalContext) -> U32: 680 match context: 681 case LocalContext{trace_id, span_id, sampled}: 682 Flags.known(sampled, TraceId.is_random(trace_id)) 683 684 # The trace a child continues. 685 def Parent.trace_id(parent: Parent) -> TraceId: 686 match parent: 687 case RemoteParent{context}: 688 RemoteContext.trace_id(context) 689 case LocalParent{context}: 690 LocalContext.trace_id(context) 691 692 # The parent's operation, which a child must not reuse. 693 def Parent.span_id(parent: Parent) -> SpanId: 694 match parent: 695 case RemoteParent{context}: 696 RemoteContext.span_id(context) 697 case LocalParent{context}: 698 LocalContext.span_id(context) 699 700 # The sampled indication a child inherits by default. 701 def Parent.is_sampled(parent: Parent) -> Bool: 702 match parent: 703 case RemoteParent{context}: 704 RemoteContext.is_sampled(context) 705 case LocalParent{context}: 706 LocalContext.is_sampled(context) 707 708 # Represent an operation the caller owns, with supplied IDs and an explicit 709 # sampled indication. The IDs must belong to that operation: validating their 710 # format cannot establish where they came from (law from_ids). 711 def Context.from_ids(trace_id: TraceId, span_id: SpanId, sampled: Bool) -> LocalContext: 712 LocalContext{trace_id, span_id, sampled} 713 714 # Start a trace with supplied IDs and the sampled indication that the caller 715 # decided, kept as it is given (spec #41, "Sampling decision when starting a 716 # trace"; law root). False gives an unsampled root, the default of spec #1, 717 # "New roots default to sampled `0`", which Context.continue_or_start_with 718 # applies itself. generation.bend provides Context.root, Context.child and 719 # Context.restart for generated IDs. 720 def Context.root_from_ids(trace_id: TraceId, span_id: SpanId, sampled: Bool) -> LocalContext: 721 Context.from_ids(trace_id, span_id, sampled) 722 723 # The child, unless the span ID was found equal to the parent's. 724 def Context.child_from_id.checked(trace_id: TraceId, span_id: SpanId, sampled: Bool, reused: Bool) -> 725 Result<&2, &2, ContextError, LocalContext>: 726 match reused: 727 case True{}: 728 Fail{ReusedSpanId{}} 729 case False{}: 730 Done{Context.from_ids(trace_id, span_id, sampled)} 731 732 # Continue the parent's trace with a new operation identified by a supplied 733 # span ID. The child keeps the trace ID and its randomness assertion, and its 734 # span ID must differ from the parent's (ReusedSpanId otherwise). Sampling is 735 # inherited unless set. Laws: child, child_reuse and child_accepts. 736 def Context.child_from_id(+parent: Parent, +span_id: SpanId, sampling: Sampling) -> 737 Result<&2, &2, ContextError, LocalContext>: 738 Context.child_from_id.checked(Parent.trace_id(parent), span_id, 739 Sampling.resolve(sampling, Parent.is_sampled(parent)), 740 SpanId.is_eq(span_id, Parent.span_id(parent))) 741 742 # The restarted root, unless the trace ID was found equal to the received one. 743 def Context.restart_from_ids.checked(trace_id: TraceId, span_id: SpanId, sampled: Bool, reused: Bool) -> 744 Result<&2, &2, ContextError, LocalContext>: 745 match reused: 746 case True{}: 747 Fail{ReusedTraceId{}} 748 case False{}: 749 Done{Context.root_from_ids(trace_id, span_id, sampled)} 750 751 # Start a new trace with supplied IDs instead of continuing a received context. 752 # The new trace ID must differ from the received one (ReusedTraceId otherwise), 753 # and the restart is the root of its IDs with the sampled indication that it 754 # is given: False applies the root defaults, sampled 0 included. Laws: 755 # restart, restart_reuse and restart_accepts. 756 def Context.restart_from_ids(previous: RemoteContext, +trace_id: TraceId, span_id: SpanId, sampled: Bool) -> 757 Result<&2, &2, ContextError, LocalContext>: 758 Context.restart_from_ids.checked(trace_id, span_id, sampled, 759 TraceId.is_eq(trace_id, RemoteContext.trace_id(previous))) 760 761 # Identifiers from source words 762 # ============================= 763 # 764 # Generated IDs are built from 32-bit words: four words for a trace ID and two 765 # for a span ID, most significant first (spec #1). These conversions make no 766 # randomness assertion; generation adds it. 767 768 # The eight lowercase hexadecimal digits of a word, most significant first 769 # (laws hex_injective and word_hex). 770 def U32.to_hex(word: U32) -> String: 771 Digits.Digits.to_string(8n, Digits.Digits.of_u32(word)) 772 773 # A trace ID from nonzero digits, with no randomness assertion. 774 def TraceId.from_digits(value: Maybe<&2, Digits.NonZero<32n>>) -> Maybe<&2, TraceId>: 775 match value: 776 case None{}: 777 None{} 778 case Some{digits}: 779 Some{TraceId{digits, False{}}} 780 781 # A trace ID from four words, read most significant first: the first word 782 # gives the first eight digits. Like a parsed ID it makes no randomness 783 # assertion; add one with TraceId.assert_random when the words are random. An 784 # all-zero candidate is None (laws trace_words and words_unasserted). 785 def TraceId.from_words(first: U32, second: U32, third: U32, fourth: U32) -> Maybe<&2, TraceId>: 786 TraceId.from_digits(Digits.NonZero.new(32n, 787 Digits.Digits.append(8n, 24n, Digits.Digits.of_u32(first), 788 Digits.Digits.append(8n, 16n, Digits.Digits.of_u32(second), 789 Digits.Digits.append(8n, 8n, Digits.Digits.of_u32(third), Digits.Digits.of_u32(fourth)))))) 790 791 # A span ID from nonzero digits. 792 def SpanId.from_digits(value: Maybe<&2, Digits.NonZero<16n>>) -> Maybe<&2, SpanId>: 793 match value: 794 case None{}: 795 None{} 796 case Some{digits}: 797 Some{SpanId{digits}} 798 799 # A span ID from two words, most significant first. An all-zero candidate is 800 # None (law span_words). 801 def SpanId.from_words(first: U32, second: U32) -> Maybe<&2, SpanId>: 802 SpanId.from_digits(Digits.NonZero.new(16n, 803 Digits.Digits.append(8n, 8n, Digits.Digits.of_u32(first), Digits.Digits.of_u32(second)))) 804 805 # Identifiers as bytes 806 # ==================== 807 # 808 # The bytes of an ID are the form of OTLP's protobuf encoding, as the text of 809 # TraceId.to_string and SpanId.to_string is that of its JSON encoding (spec 810 # #41, "Identifier forms"). TraceId.to_bytes and TraceId.from_bytes state the 811 # contract; the helpers below read bytes as Parse.id reads text. 812 813 # Put the two digits of one more byte in front of the bytes already read: n 814 # bytes become 1 + n. 815 def ParsedBytes.prepend(-n: Nat, digits: Digits.Digits(2n), parsed: ParsedBytes) -> ParsedBytes<1n+n>: 816 match digits parsed: 817 case Digits.DCon{high, Digits.DCon{low, Digits.DNil{}}} ParsedBytes{rest_digits, rest}: 818 ParsedBytes{Digits.DCon{high, Digits.DCon{low, rest_digits}}, rest} 819 820 # The two digits of a cell, or InvalidByte at its offset when the check found 821 # the cell above 255. 822 def Parse.byte.checked(cell: U32, above: Bool, offset: Nat) -> Result<&2, &2, Error, Digits.Digits(2n)>: 823 match above: 824 case True{}: 825 Fail{InvalidByte{offset}} 826 case False{}: 827 Done{Digits.Digits.of_byte(cell)} 828 829 # Read one cell as a byte. 830 def Parse.byte(+cell: U32, offset: Nat) -> Result<&2, &2, Error, Digits.Digits(2n)>: 831 Parse.byte.checked(cell, U32.is_gt(cell, 255), offset) 832 833 # Consume exactly n cells as bytes, keeping the cells after them. As in 834 # Parse.digits, the recursion decreases n, so the result's type has the 2n 835 # digits of n bytes. 836 def Parse.bytes(n: Nat, bytes: List<&2, U32>, offset: Nat) -> Result<&2, &2, Error, ParsedBytes>: 837 match n: 838 case 0n: 839 Done{ParsedBytes{Digits.DNil{}, bytes}} 840 case 1n+p: 841 match bytes: 842 case Nil{}: 843 Fail{UnexpectedEnd{offset}} 844 case Con{cell, tail}: 845 +at = offset 846 do Result<&2, &2, Error, ParsedBytes<1n+p>>: 847 digits : Digits.Digits(2n) <- Parse.byte(cell, at) 848 parsed : ParsedBytes

<- Parse.bytes(p, tail, 1n+at) 849 return ParsedBytes.prepend(p, digits, parsed) 850 851 # The list must end after the ID's bytes: a cell after them fails with 852 # TrailingInput, whatever it holds. 853 def Parse.bytes_end(bytes: List<&2, U32>) -> Result<&2, &2, Error, Unit>: 854 match bytes: 855 case Nil{}: 856 Done{Unit{}} 857 case Con{cell, rest}: 858 Fail{TrailingInput{}} 859 860 # The bytes of a supplied ID must be the whole list, and not all zero. 861 def Parse.id_bytes.finish(n: Nat, parsed: ParsedBytes, field: Field) -> 862 Result<&2, &2, Error, Digits.NonZero>: 863 match parsed: 864 case ParsedBytes{digits, rest}: 865 do Result<&2, &2, Error, Digits.NonZero>: 866 end : Unit <- Parse.bytes_end(rest) 867 Parse.nonzero(Nat.double(n), digits, field) 868 869 # A supplied ID is exactly n bytes, not all zero. 870 def Parse.id_bytes(+n: Nat, bytes: List<&2, U32>, field: Field) -> 871 Result<&2, &2, Error, Digits.NonZero>: 872 do Result<&2, &2, Error, Digits.NonZero>: 873 parsed : ParsedBytes <- Parse.bytes(n, bytes, 0n) 874 Parse.id_bytes.finish(n, parsed, field) 875 876 # The 16 bytes of the trace ID, most significant first, in Base's byte 877 # convention, that of TCP.send_bytes and TCP.recv_bytes: one U32 cell from 0 878 # to 255 per byte. The first byte holds the ID's first two digits, the first 879 # of them high. The randomness assertion is not part of the bytes (laws 880 # trace_bytes, trace_bytes_roundtrip and trace_bytes_injective). 881 def TraceId.to_bytes(id: TraceId) -> List<&2, U32>: 882 match id: 883 case TraceId{value, random}: 884 Digits.Digits.to_bytes(16n, Digits.NonZero.digits(32n, value)) 885 886 # Read a trace ID from exactly 16 bytes, most significant first. The cells 887 # are read in order: a missing cell fails with UnexpectedEnd and a cell above 888 # 255 with InvalidByte, at its offset counted in cells; a 17th cell fails with 889 # TrailingInput whatever it holds, and 16 zero bytes with ZeroId. Like a 890 # parsed ID, the result makes no randomness assertion, since bytes do not say 891 # how the ID was made; only a caller whose own generator, known to be random, 892 # made it adds one with TraceId.assert_random. Laws: trace_bytes_inverse, 893 # bytes_unasserted, trace_bytes_short, trace_bytes_long, trace_bytes_above, 894 # zero_bytes and trace_bytes_accepts. 895 def TraceId.from_bytes(bytes: List<&2, U32>) -> Result<&2, &2, Error, TraceId>: 896 do Result<&2, &2, Error, TraceId>: 897 value : Digits.NonZero<32n> <- Parse.id_bytes(16n, bytes, TraceIdField{}) 898 return TraceId{value, False{}} 899 900 # The 8 bytes of the span ID, most significant first (laws span_bytes, 901 # span_bytes_roundtrip and span_bytes_injective). 902 def SpanId.to_bytes(id: SpanId) -> List<&2, U32>: 903 match id: 904 case SpanId{value}: 905 Digits.Digits.to_bytes(8n, Digits.NonZero.digits(16n, value)) 906 907 # Read a span ID from exactly 8 bytes, most significant first, with the rules 908 # and errors of TraceId.from_bytes. Laws: span_bytes_inverse, 909 # span_bytes_short, span_bytes_long, span_bytes_above, zero_bytes and 910 # span_bytes_accepts. 911 def SpanId.from_bytes(bytes: List<&2, U32>) -> Result<&2, &2, Error, SpanId>: 912 do Result<&2, &2, Error, SpanId>: 913 value : Digits.NonZero<16n> <- Parse.id_bytes(8n, bytes, SpanIdField{}) 914 return SpanId{value} 915 916 # Generation machine 917 # ================== 918 # 919 # A generation is a small state machine fed one source word at a time. It 920 # has two pieces, each of which draws one identifier: a trace ID draw 921 # (TraceDraw, TraceStep) reads four words per candidate, and a span ID draw 922 # (SpanDraw, SpanStep) two. Each piece gives its identifier eight 923 # candidates, rejects zero and the identifier to exclude, and stops at the 924 # first source error. TraceId.generate_with and SpanId.generate_with run one 925 # piece alone. A generation (Draw, Step) runs the pieces in turn: a root or 926 # a restart draws its trace ID, then its span ID, as its trace plan 927 # (TracePlan) says, and a child only its span ID, as its span plan 928 # (SpanPlan) says. A root and a restart differ only in their plan. 929 # Context.root_with and its siblings compose the two operations in the same 930 # order. One driver (Drive) runs the 931 # three machines, over a replayed tape in the laws and over the host's 932 # cryptographic source in generation.bend. 933 934 # Generation reads its words from a source trusted to be random, so each 935 # trace ID candidate asserts random-trace-id. 936 def Draw.asserted(candidate: Maybe<&2, TraceId>) -> Maybe<&2, TraceId>: 937 match candidate: 938 case None{}: 939 None{} 940 case Some{id}: 941 Some{TraceId.assert_random(id)} 942 943 # A deterministic word source for tests and replay: each read takes the next 944 # result, and an empty tape fails with code 1, tape-exhausted. 945 def Tape.next(tape: List<&1, Result<&1, &1, U32 & String, U32>>) -> 946 List<&1, Result<&1, &1, U32 & String, U32>> & Result<&1, &1, U32 & String, U32>: 947 match tape: 948 case Nil{}: 949 (Nil{}, Fail{(1, "tape-exhausted")}) 950 case Con{word, rest}: 951 (rest, word) 952 953 # The driver of the three machines: a trace ID draw, a span ID draw and a 954 # generation. It feeds a machine one source word at a time while the 955 # machine's step waits for one, and stops as soon as it has ended. Each 956 # machine gives, as templates, `waiting`, the draw that a step feeds its next 957 # word to, if it waits for one, and `feed`, the step after that word. The 958 # driver keeps each step beside what `waiting` says of it. 959 # 960 # Feed a word that a source returned, keeping the source's next state. 961 def Drive.fed(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>, ~feed: Result<&1, &1, U32 & String, U32> -> D -> T, 962 -S: Type, got: S & Result<&1, &1, U32 & String, U32>, draw: D) -> S & (T & Maybe<&2, D>): 963 (state, word) = got 964 +next = feed(word, draw) 965 (state, (next, waiting(next))) 966 967 # Drive a machine from a tape, stopping as soon as its step has ended; unread 968 # words stay on the tape. `fuel` bounds the steps, which Bend requires for 969 # termination; the laws show the budgets suffice. 970 def Drive.run(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>, ~feed: Result<&1, &1, U32 & String, U32> -> D -> T, 971 fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & (T & Maybe<&2, D>)) -> 972 List<&1, Result<&1, &1, U32 & String, U32>> & T: 973 match fuel current: 974 case _ Tuple{tape, Tuple{step, None{}}}: 975 (tape, step) 976 case 0n Tuple{tape, Tuple{step, Some{draw}}}: 977 (tape, step) 978 case 1n+p Tuple{tape, Tuple{step, Some{draw}}}: 979 Drive.run(~T, ~D, ~waiting, ~feed, p, Drive.fed(~T, ~D, ~waiting, ~feed, 980 List<&1, Result<&1, &1, U32 & String, U32>>, Tape.next(tape), draw)) 981 982 # Drive a machine from any source, one word at a time. `read` returns the 983 # source's next state with each word, and the driver stops as soon as the 984 # machine's step has ended; the final source state is handed back, so a 985 # caller can see what was read. `fuel` bounds the words read, as in 986 # Drive.run. Templates keep this driver free of any host effect: the effect, 987 # if any, lives in the source. 988 def Drive.read(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>, ~feed: Result<&1, &1, U32 & String, U32> -> D -> T, 989 ~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), fuel: Nat, current: S & (T & Maybe<&2, D>)) -> 990 IO(S & T): 991 match fuel current: 992 case _ Tuple{state, Tuple{step, None{}}}: 993 IO.pure(S & T, (state, step)) 994 case 0n Tuple{state, Tuple{step, Some{draw}}}: 995 IO.pure(S & T, (state, step)) 996 case 1n+p Tuple{state, Tuple{step, Some{draw}}}: 997 IO.bind(S & Result<&1, &1, U32 & String, U32>, S & T, read(state), 998 got => Drive.read(~T, ~D, ~waiting, ~feed, ~S, ~read, p, Drive.fed(~T, ~D, ~waiting, ~feed, S, got, draw))) 999 1000 # Whether the machine in a driver's result has ended. 1001 def Drive.ended(~T: Data, ~D: Data, ~waiting: T -> Maybe<&2, D>, 1002 result: List<&1, Result<&1, &1, U32 & String, U32>> & T) -> Bool: 1003 match result: 1004 case Tuple{tape, step}: 1005 Maybe.is_none(&2, D, waiting(step)) 1006 1007 # The source's final state with the result that `result` gives of the 1008 # machine's final step. 1009 def Drive.outcome(~T: Data, ~A: Data, ~result: T -> Result<&2, &2, GenerationError, A>, -S: Type, done: S & T) -> 1010 S & Result<&2, &2, GenerationError, A>: 1011 (state, step) = done 1012 (state, result(step)) 1013 1014 # Turn the IO driver's final step into its result. 1015 def Drive.finished(~T: Data, ~A: Data, ~result: T -> Result<&2, &2, GenerationError, A>, ~S: Type, 1016 action: IO(S & T)) -> IO(S & Result<&2, &2, GenerationError, A>): 1017 IO.bind(S & T, S & Result<&2, &2, GenerationError, A>, action, 1018 done => IO.pure(S & Result<&2, &2, GenerationError, A>, Drive.outcome(~T, ~A, ~result, S, done))) 1019 1020 # Trace ID draws 1021 # -------------- 1022 1023 # A trace ID draw starts with its first candidate; seven further candidates 1024 # may follow it, eight in all. 1025 def TraceDraw.start(excluded: Maybe<&2, TraceId>) -> TraceStep: 1026 NeedTraceWord{TraceDraw{7n, NoTraceWord{}, excluded}} 1027 1028 # Try another trace ID candidate, or fail once the eight are used. 1029 def TraceDraw.retry(remaining: Nat, excluded: Maybe<&2, TraceId>) -> TraceStep: 1030 match remaining: 1031 case 0n: 1032 TraceFailed{ExhaustedTraceId{}} 1033 case 1n+p: 1034 NeedTraceWord{TraceDraw{p, NoTraceWord{}, excluded}} 1035 1036 # A trace ID candidate equal to the excluded one is retried. 1037 def TraceDraw.reuse(reused: Bool, id: TraceId, excluded: TraceId, remaining: Nat) -> TraceStep: 1038 match reused: 1039 case True{}: 1040 TraceDraw.retry(remaining, Some{excluded}) 1041 case False{}: 1042 DrawnTraceId{id} 1043 1044 # Check a complete trace ID candidate: zero and the excluded trace ID are 1045 # retried; anything else is the trace ID drawn. 1046 def TraceDraw.check(candidate: Maybe<&2, TraceId>, excluded: Maybe<&2, TraceId>, remaining: Nat) -> TraceStep: 1047 match candidate: 1048 case None{}: 1049 TraceDraw.retry(remaining, excluded) 1050 case Some{+id}: 1051 match excluded: 1052 case None{}: 1053 DrawnTraceId{id} 1054 case Some{+old}: 1055 TraceDraw.reuse(TraceId.is_eq(id, old), id, old, remaining) 1056 1057 # Add a word to the current trace ID candidate. The fourth word completes it, 1058 # most significant first, and the candidate is checked. 1059 def TraceDraw.take(word: U32, remaining: Nat, words: TraceWords, excluded: Maybe<&2, TraceId>) -> TraceStep: 1060 match words: 1061 case NoTraceWord{}: 1062 NeedTraceWord{TraceDraw{remaining, OneTraceWord{word}, excluded}} 1063 case OneTraceWord{first}: 1064 NeedTraceWord{TraceDraw{remaining, TwoTraceWords{first, word}, excluded}} 1065 case TwoTraceWords{first, second}: 1066 NeedTraceWord{TraceDraw{remaining, ThreeTraceWords{first, second, word}, excluded}} 1067 case ThreeTraceWords{first, second, third}: 1068 TraceDraw.check(Draw.asserted(TraceId.from_words(first, second, third, word)), excluded, remaining) 1069 1070 # Feed the next source word to a trace ID draw, given as its three fields. A 1071 # source error ends the draw at once with SourceFailure (law 1072 # trace_id_failure). 1073 def TraceDraw.feed(word: Result<&1, &1, U32 & String, U32>, remaining: Nat, words: TraceWords, 1074 excluded: Maybe<&2, TraceId>) -> TraceStep: 1075 match word: 1076 case Fail{(code, message)}: 1077 TraceFailed{SourceFailure{code, message}} 1078 case Done{next}: 1079 TraceDraw.take(next, remaining, words, excluded) 1080 1081 # The step of a trace ID draw after its next source word, TraceDraw.feed of 1082 # its fields: the `feed` that Drive takes. 1083 def TraceDraw.next(word: Result<&1, &1, U32 & String, U32>, draw: TraceDraw) -> TraceStep: 1084 match draw: 1085 case TraceDraw{remaining, words, excluded}: 1086 TraceDraw.feed(word, remaining, words, excluded) 1087 1088 # The draw that a trace ID draw's step feeds its next word to, while it 1089 # waits for one: the view of the step that Drive needs. 1090 def TraceStep.waiting(step: TraceStep) -> Maybe<&2, TraceDraw>: 1091 match step: 1092 case NeedTraceWord{draw}: 1093 Some{draw} 1094 case DrawnTraceId{id}: 1095 None{} 1096 case TraceFailed{error}: 1097 None{} 1098 1099 # The trace ID of a finished trace ID draw, or why it failed. A draw that has 1100 # not finished would report exhaustion; law trace_id_ends shows that the word 1101 # budget of TraceId.generate_with makes that case unreachable. 1102 def TraceDraw.result(step: TraceStep) -> Result<&2, &2, GenerationError, TraceId>: 1103 match step: 1104 case DrawnTraceId{id}: 1105 Done{id} 1106 case TraceFailed{error}: 1107 Fail{error} 1108 case NeedTraceWord{draw}: 1109 Fail{ExhaustedTraceId{}} 1110 1111 # Drive a trace ID draw from a tape (Drive.run). 1112 def TraceDraw.run(fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & TraceStep) -> 1113 List<&1, Result<&1, &1, U32 & String, U32>> & TraceStep: 1114 match current: 1115 case Tuple{tape, +step}: 1116 Drive.run(~TraceStep, ~TraceDraw, ~TraceStep.waiting, ~TraceDraw.next, fuel, 1117 (tape, (step, TraceStep.waiting(step)))) 1118 1119 # Whether the trace ID draw in a driver's result has ended. 1120 def TraceDraw.ended(result: List<&1, Result<&1, &1, U32 & String, U32>> & TraceStep) -> Bool: 1121 Drive.ended(~TraceStep, ~TraceDraw, ~TraceStep.waiting, result) 1122 1123 # The source's final state with the trace ID draw's result. 1124 def TraceDraw.outcome(-S: Type, done: S & TraceStep) -> S & Result<&2, &2, GenerationError, TraceId>: 1125 Drive.outcome(~TraceStep, ~TraceId, ~TraceDraw.result, S, done) 1126 1127 # A trace ID alone, from a caller's source, as an OpenTelemetry SDK generates 1128 # one before its sampler decides on it. `read` returns the source's next state 1129 # with each word result, and the source's final state is returned. It reads 1130 # four words per candidate, most significant first, for at most eight 1131 # candidates, so at most 32 words; rejects all-zero candidates and `excluded`, 1132 # when there is one; and fails with SourceFailure or ExhaustedTraceId. The 1133 # source is trusted to be random: the trace ID asserts random-trace-id. 1134 # Laws: trace_id_tape, trace_id_failure, trace_id_candidate, trace_id_ends, 1135 # trace_id_exhaustion and generated_trace_id. 1136 def TraceId.generate_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 1137 excluded: Maybe<&2, TraceId>) -> IO(S & Result<&2, &2, GenerationError, TraceId>): 1138 +start = TraceDraw.start(excluded) 1139 Drive.finished(~TraceStep, ~TraceId, ~TraceDraw.result, ~S, Drive.read(~TraceStep, ~TraceDraw, ~TraceStep.waiting, 1140 ~TraceDraw.next, ~S, ~read, 32n, (source, (start, TraceStep.waiting(start))))) 1141 1142 # Span ID draws 1143 # ------------- 1144 1145 # A span ID draw starts with its first candidate; seven further candidates 1146 # may follow it, eight in all. 1147 def SpanDraw.start(excluded: Maybe<&2, SpanId>) -> SpanStep: 1148 NeedSpanWord{SpanDraw{7n, NoSpanWord{}, excluded}} 1149 1150 # Try another span ID candidate, or fail once the eight are used. 1151 def SpanDraw.retry(remaining: Nat, excluded: Maybe<&2, SpanId>) -> SpanStep: 1152 match remaining: 1153 case 0n: 1154 SpanFailed{ExhaustedSpanId{}} 1155 case 1n+p: 1156 NeedSpanWord{SpanDraw{p, NoSpanWord{}, excluded}} 1157 1158 # A span ID candidate equal to the excluded one is retried. 1159 def SpanDraw.reuse(reused: Bool, id: SpanId, excluded: SpanId, remaining: Nat) -> SpanStep: 1160 match reused: 1161 case True{}: 1162 SpanDraw.retry(remaining, Some{excluded}) 1163 case False{}: 1164 DrawnSpanId{id} 1165 1166 # Check a complete span ID candidate: zero and the excluded span ID are 1167 # retried; anything else is the span ID drawn. 1168 def SpanDraw.check(candidate: Maybe<&2, SpanId>, excluded: Maybe<&2, SpanId>, remaining: Nat) -> SpanStep: 1169 match candidate: 1170 case None{}: 1171 SpanDraw.retry(remaining, excluded) 1172 case Some{+id}: 1173 match excluded: 1174 case None{}: 1175 DrawnSpanId{id} 1176 case Some{+old}: 1177 SpanDraw.reuse(SpanId.is_eq(id, old), id, old, remaining) 1178 1179 # Add a word to the current span ID candidate. The second word completes it, 1180 # most significant first, and the candidate is checked. 1181 def SpanDraw.take(word: U32, remaining: Nat, words: SpanWords, excluded: Maybe<&2, SpanId>) -> SpanStep: 1182 match words: 1183 case NoSpanWord{}: 1184 NeedSpanWord{SpanDraw{remaining, OneSpanWord{word}, excluded}} 1185 case OneSpanWord{first}: 1186 SpanDraw.check(SpanId.from_words(first, word), excluded, remaining) 1187 1188 # Feed the next source word to a span ID draw, given as its three fields. A 1189 # source error ends the draw at once with SourceFailure (law 1190 # span_id_failure). 1191 def SpanDraw.feed(word: Result<&1, &1, U32 & String, U32>, remaining: Nat, words: SpanWords, 1192 excluded: Maybe<&2, SpanId>) -> SpanStep: 1193 match word: 1194 case Fail{(code, message)}: 1195 SpanFailed{SourceFailure{code, message}} 1196 case Done{next}: 1197 SpanDraw.take(next, remaining, words, excluded) 1198 1199 # The step of a span ID draw after its next source word, SpanDraw.feed of its 1200 # fields: the `feed` that Drive takes. 1201 def SpanDraw.next(word: Result<&1, &1, U32 & String, U32>, draw: SpanDraw) -> SpanStep: 1202 match draw: 1203 case SpanDraw{remaining, words, excluded}: 1204 SpanDraw.feed(word, remaining, words, excluded) 1205 1206 # The draw that a span ID draw's step feeds its next word to, while it waits 1207 # for one. 1208 def SpanStep.waiting(step: SpanStep) -> Maybe<&2, SpanDraw>: 1209 match step: 1210 case NeedSpanWord{draw}: 1211 Some{draw} 1212 case DrawnSpanId{id}: 1213 None{} 1214 case SpanFailed{error}: 1215 None{} 1216 1217 # The span ID of a finished span ID draw, or why it failed, as 1218 # TraceDraw.result; law span_id_ends shows that the word budget of 1219 # SpanId.generate_with makes the unfinished case unreachable. 1220 def SpanDraw.result(step: SpanStep) -> Result<&2, &2, GenerationError, SpanId>: 1221 match step: 1222 case DrawnSpanId{id}: 1223 Done{id} 1224 case SpanFailed{error}: 1225 Fail{error} 1226 case NeedSpanWord{draw}: 1227 Fail{ExhaustedSpanId{}} 1228 1229 # Drive a span ID draw from a tape (Drive.run). 1230 def SpanDraw.run(fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & SpanStep) -> 1231 List<&1, Result<&1, &1, U32 & String, U32>> & SpanStep: 1232 match current: 1233 case Tuple{tape, +step}: 1234 Drive.run(~SpanStep, ~SpanDraw, ~SpanStep.waiting, ~SpanDraw.next, fuel, 1235 (tape, (step, SpanStep.waiting(step)))) 1236 1237 # Whether the span ID draw in a driver's result has ended. 1238 def SpanDraw.ended(result: List<&1, Result<&1, &1, U32 & String, U32>> & SpanStep) -> Bool: 1239 Drive.ended(~SpanStep, ~SpanDraw, ~SpanStep.waiting, result) 1240 1241 # The source's final state with the span ID draw's result. 1242 def SpanDraw.outcome(-S: Type, done: S & SpanStep) -> S & Result<&2, &2, GenerationError, SpanId>: 1243 Drive.outcome(~SpanStep, ~SpanId, ~SpanDraw.result, S, done) 1244 1245 # A span ID alone, from a caller's source, as an OpenTelemetry SDK generates 1246 # one once its sampler has decided. The source's shape is that of 1247 # TraceId.generate_with. It reads two words per candidate, most significant 1248 # first, for at most eight candidates, so at most 16 words; rejects all-zero 1249 # candidates and `excluded`, when there is one, such as the span ID of a 1250 # child's parent; and fails with SourceFailure or ExhaustedSpanId. 1251 # Laws: span_id_tape, span_id_failure, span_id_candidate, span_id_ends, 1252 # span_id_exhaustion and generated_span_id. 1253 def SpanId.generate_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 1254 excluded: Maybe<&2, SpanId>) -> IO(S & Result<&2, &2, GenerationError, SpanId>): 1255 +start = SpanDraw.start(excluded) 1256 Drive.finished(~SpanStep, ~SpanId, ~SpanDraw.result, ~S, Drive.read(~SpanStep, ~SpanDraw, ~SpanStep.waiting, 1257 ~SpanDraw.next, ~S, ~read, 16n, (source, (start, SpanStep.waiting(start))))) 1258 1259 # Generations 1260 # ----------- 1261 1262 # The generation that a span ID draw's step gives, for a context of 1263 # `trace_id` with the sampled indication `sampled`: waiting for the draw's 1264 # next word, the context once the span ID is drawn, or the draw's failure. 1265 def Step.of_span(step: SpanStep, trace_id: TraceId, sampled: Bool) -> Step: 1266 match step: 1267 case NeedSpanWord{draw}: 1268 NeedWord{DrawSpan{draw, trace_id, sampled}} 1269 case DrawnSpanId{id}: 1270 Created{Context.from_ids(trace_id, id, sampled)} 1271 case SpanFailed{error}: 1272 Failed{error} 1273 1274 # The plan of a root's span ID, once its trace ID is drawn, and of a 1275 # restart's: nothing to exclude, and the sampled indication that the root or 1276 # the restart was given, as it is given. 1277 def SpanPlan.root(trace_id: TraceId, sampled: Bool) -> SpanPlan: 1278 SpanPlan{None{}, trace_id, sampled} 1279 1280 # The plan of a child's span ID: the parent's span ID excluded, the parent's 1281 # trace ID, and the sampled indication that `sampling` resolves from the 1282 # parent's. 1283 def SpanPlan.child(+parent: Parent, sampling: Sampling) -> SpanPlan: 1284 SpanPlan{Some{Parent.span_id(parent)}, Parent.trace_id(parent), Sampling.resolve(sampling, Parent.is_sampled(parent))} 1285 1286 # The generation that draws the span ID of a plan, from its first candidate. 1287 def SpanPlan.draw(plan: SpanPlan) -> Step: 1288 match plan: 1289 case SpanPlan{excluded, trace_id, sampled}: 1290 Step.of_span(SpanDraw.start(excluded), trace_id, sampled) 1291 1292 # The generation that a trace ID draw's step gives, for a root or a restart 1293 # with the sampled indication `sampled`: waiting for the draw's next word, 1294 # the root's span ID draw once the trace ID is drawn (SpanPlan.root), or the 1295 # draw's failure. 1296 def Step.of_trace(step: TraceStep, sampled: Bool) -> Step: 1297 match step: 1298 case NeedTraceWord{draw}: 1299 NeedWord{DrawTrace{draw, sampled}} 1300 case DrawnTraceId{id}: 1301 SpanPlan.draw(SpanPlan.root(id, sampled)) 1302 case TraceFailed{error}: 1303 Failed{error} 1304 1305 # The plan of a root: no trace ID to exclude, and the sampled indication 1306 # `sampled`, as it is given. 1307 def TracePlan.root(sampled: Bool) -> TracePlan: 1308 TracePlan{None{}, sampled} 1309 1310 # The plan of a restart replacing `previous`: the received trace ID to 1311 # exclude, and the sampled indication `sampled`, as it is given. 1312 def TracePlan.restart(previous: RemoteContext, sampled: Bool) -> TracePlan: 1313 TracePlan{Some{RemoteContext.trace_id(previous)}, sampled} 1314 1315 # The generation that draws the new trace of a plan: its trace ID, from the 1316 # first candidate, then the span ID of the root's span plan (Step.of_trace). 1317 def TracePlan.draw(plan: TracePlan) -> Step: 1318 match plan: 1319 case TracePlan{excluded, sampled}: 1320 Step.of_trace(TraceDraw.start(excluded), sampled) 1321 1322 # A root draws the new trace of its plan (TracePlan.root). 1323 def Draw.root(sampled: Bool) -> Step: 1324 TracePlan.draw(TracePlan.root(sampled)) 1325 1326 # A restart draws like a root but excludes the received trace ID 1327 # (TracePlan.restart). 1328 def Draw.restart(previous: RemoteContext, sampled: Bool) -> Step: 1329 TracePlan.draw(TracePlan.restart(previous, sampled)) 1330 1331 # A child draws the span ID of its plan (SpanPlan.child). 1332 def Draw.child(+parent: Parent, sampling: Sampling) -> Step: 1333 SpanPlan.draw(SpanPlan.child(parent, sampling)) 1334 1335 # Feed the next source word, or the source's error, to the trace ID draw or 1336 # the span ID draw that the generation runs. A source error ends the draw, 1337 # and so the generation, at once with SourceFailure (law feed_failure). 1338 def Draw.feed(word: Result<&1, &1, U32 & String, U32>, draw: Draw) -> Step: 1339 match draw: 1340 case DrawTrace{trace, sampled}: 1341 Step.of_trace(TraceDraw.next(word, trace), sampled) 1342 case DrawSpan{span, trace_id, sampled}: 1343 Step.of_span(SpanDraw.next(word, span), trace_id, sampled) 1344 1345 # The draw that a generation's step feeds its next word to, while it waits 1346 # for one. 1347 def Step.waiting(step: Step) -> Maybe<&2, Draw>: 1348 match step: 1349 case NeedWord{draw}: 1350 Some{draw} 1351 case Created{context}: 1352 None{} 1353 case Failed{error}: 1354 None{} 1355 1356 # The result of a finished generation. A generation that has not finished 1357 # would report the identifier it was drawing; the root_ends, child_ends and 1358 # restart_ends laws show that the word budgets of the operations below make 1359 # those cases unreachable. 1360 def Step.result(step: Step) -> Result<&2, &2, GenerationError, LocalContext>: 1361 match step: 1362 case Created{context}: 1363 Done{context} 1364 case Failed{error}: 1365 Fail{error} 1366 case NeedWord{DrawTrace{draw, sampled}}: 1367 Fail{ExhaustedTraceId{}} 1368 case NeedWord{DrawSpan{draw, trace_id, sampled}}: 1369 Fail{ExhaustedSpanId{}} 1370 1371 # Drive a generation from a tape (Drive.run). 1372 def Draw.run(fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & Step) -> 1373 List<&1, Result<&1, &1, U32 & String, U32>> & Step: 1374 match current: 1375 case Tuple{tape, +step}: 1376 Drive.run(~Step, ~Draw, ~Step.waiting, ~Draw.feed, fuel, (tape, (step, Step.waiting(step)))) 1377 1378 # Drive a generation from any source (Drive.read). 1379 def Draw.read(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), fuel: Nat, 1380 current: S & Step) -> IO(S & Step): 1381 match current: 1382 case Tuple{state, +step}: 1383 Drive.read(~Step, ~Draw, ~Step.waiting, ~Draw.feed, ~S, ~read, fuel, (state, (step, Step.waiting(step)))) 1384 1385 # Whether the generation in a driver's result has ended. 1386 def Draw.ended(result: List<&1, Result<&1, &1, U32 & String, U32>> & Step) -> Bool: 1387 Drive.ended(~Step, ~Draw, ~Step.waiting, result) 1388 1389 # The source's final state with the generation's result. 1390 def Draw.outcome(-S: Type, done: S & Step) -> S & Result<&2, &2, GenerationError, LocalContext>: 1391 Drive.outcome(~Step, ~LocalContext, ~Step.result, S, done) 1392 1393 # Turn the driver's final step into the generation's result. 1394 def Draw.finished(~S: Type, action: IO(S & Step)) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 1395 Drive.finished(~Step, ~LocalContext, ~Step.result, ~S, action) 1396 1397 # The generation of the new trace of a plan: at most 48 words, eight trace ID 1398 # candidates of four words and eight span ID candidates of two. 1399 def TracePlan.generation(plan: TracePlan) -> Generation: 1400 Generation{48n, TracePlan.draw(plan)} 1401 1402 # A root with the sampled indication `sampled`, as it is given 1403 # (TracePlan.root). 1404 def Generation.root(sampled: Bool) -> Generation: 1405 TracePlan.generation(TracePlan.root(sampled)) 1406 1407 # A restart replacing `previous`, with the sampled indication `sampled`, as a 1408 # root (TracePlan.restart). 1409 def Generation.restart(previous: RemoteContext, sampled: Bool) -> Generation: 1410 TracePlan.generation(TracePlan.restart(previous, sampled)) 1411 1412 # A child of `parent`: at most 16 words, eight span ID candidates. 1413 def Generation.child(+parent: Parent, sampling: Sampling) -> Generation: 1414 Generation{16n, Draw.child(parent, sampling)} 1415 1416 # Whether a step needs another word within `fuel` more words. 1417 def Generation.needs.of(fuel: Nat, step: Step) -> Bool: 1418 match fuel step: 1419 case 0n _: 1420 False{} 1421 case 1n+p NeedWord{draw}: 1422 True{} 1423 case 1n+p Created{context}: 1424 False{} 1425 case 1n+p Failed{error}: 1426 False{} 1427 1428 # Whether the generation needs another word: it has not ended, and its 1429 # budget allows one more. 1430 def Generation.needs(generation: Generation) -> Bool: 1431 match generation: 1432 case Generation{fuel, step}: 1433 Generation.needs.of(fuel, step) 1434 1435 # The generation after `word`: the step it gives with one word less of 1436 # budget, or, for a step that needs no word, the same step with none left. 1437 def Generation.fed(fuel: Nat, step: Step, word: Result<&1, &1, U32 & String, U32>) -> Generation: 1438 match fuel step: 1439 case 0n other: 1440 Generation{0n, other} 1441 case 1n+p NeedWord{draw}: 1442 Generation{p, Draw.feed(word, draw)} 1443 case 1n+p Created{context}: 1444 Generation{0n, Created{context}} 1445 case 1n+p Failed{error}: 1446 Generation{0n, Failed{error}} 1447 1448 # Feed the generation the next word of its source (see Draw.feed). A 1449 # generation that needs no word ignores it. 1450 def Generation.feed(generation: Generation, word: Result<&1, &1, U32 & String, U32>) -> Generation: 1451 match generation: 1452 case Generation{fuel, step}: 1453 Generation.fed(fuel, step, word) 1454 1455 # The generation's result: the context it created, or why it failed. One that 1456 # still needs a word once its budget is spent has exhausted its candidates; 1457 # the root_ends, child_ends and restart_ends laws show that the budgets 1458 # suffice. 1459 def Generation.result(generation: Generation) -> Result<&2, &2, GenerationError, LocalContext>: 1460 match generation: 1461 case Generation{fuel, step}: 1462 Step.result(step) 1463 1464 # Drive a generation from a caller's source, one word at a time 1465 # (Draw.read), and hand back the source's final state with the result. 1466 def Generation.run_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 1467 generation: Generation) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 1468 match generation: 1469 case Generation{fuel, step}: 1470 Draw.finished(~S, Draw.read(~S, ~read, fuel, (source, step))) 1471 1472 # The context of a span ID generated from a source for an operation of 1473 # `trace_id` with the sampled indication `sampled`, with the source's final 1474 # state: the span ID's failure is the context's. 1475 def Draw.span_context(-S: Type, +trace_id: TraceId, +sampled: Bool, 1476 done: S & Result<&2, &2, GenerationError, SpanId>) -> S & Result<&2, &2, GenerationError, LocalContext>: 1477 match done: 1478 case Tuple{state, Fail{error}}: 1479 (state, Fail{error}) 1480 case Tuple{state, Done{span_id}}: 1481 (state, Done{Context.from_ids(trace_id, span_id, sampled)}) 1482 1483 # The local context of a span plan, from a caller's source: a span ID that 1484 # excludes the plan's (SpanId.generate_with), and the context of the plan's 1485 # trace ID and sampled indication with it. 1486 def SpanPlan.generate_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 1487 plan: SpanPlan) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 1488 match plan: 1489 case SpanPlan{excluded, trace_id, sampled}: 1490 IO.bind(S & Result<&2, &2, GenerationError, SpanId>, S & Result<&2, &2, GenerationError, LocalContext>, 1491 SpanId.generate_with(~S, ~read, source, excluded), 1492 outcome => IO.pure(S & Result<&2, &2, GenerationError, LocalContext>, 1493 Draw.span_context(S, trace_id, sampled, outcome))) 1494 1495 # The span ID of a root or a restart with the sampled indication `sampled`, 1496 # from the source's next state, once its trace ID is generated: the trace 1497 # ID's failure is the generation's, and otherwise the local context of the 1498 # root's span plan (SpanPlan.root). 1499 def Draw.root_span_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), sampled: Bool, 1500 outcome: S & Result<&2, &2, GenerationError, TraceId>) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 1501 match outcome: 1502 case Tuple{state, Fail{error}}: 1503 IO.pure(S & Result<&2, &2, GenerationError, LocalContext>, (state, Fail{error})) 1504 case Tuple{state, Done{trace_id}}: 1505 SpanPlan.generate_with(~S, ~read, state, SpanPlan.root(trace_id, sampled)) 1506 1507 # The local context of the new trace of a plan, from a caller's source: a 1508 # trace ID that excludes the plan's (TraceId.generate_with), then, from the 1509 # source's next state, the span ID of the root's span plan with the plan's 1510 # sampled indication (Draw.root_span_with). 1511 def TracePlan.generate_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 1512 plan: TracePlan) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 1513 match plan: 1514 case TracePlan{excluded, sampled}: 1515 IO.bind(S & Result<&2, &2, GenerationError, TraceId>, S & Result<&2, &2, GenerationError, LocalContext>, 1516 TraceId.generate_with(~S, ~read, source, excluded), outcome => Draw.root_span_with(~S, ~read, sampled, outcome)) 1517 1518 # Generated contexts from a caller's source. `read` returns the source's next 1519 # state with each word result. The source is trusted to be random: a generated 1520 # trace ID asserts random-trace-id. A root is a trace ID, with none to 1521 # exclude, then a span ID: TraceId.generate_with, then SpanId.generate_with 1522 # from the source's next state (TracePlan.root and TracePlan.generate_with). 1523 # It reads at most 48 words and has the sampled indication `sampled`, as it 1524 # is given: no default applies here, and False gives an unsampled root, 1525 # emitted with flags 02, as Context.continue_or_start_with starts one by 1526 # default (spec #41, "Sampling decision when starting a trace"). Laws: 1527 # root_composed, root_tape, root_ends, root_exhaustion and generated_root. 1528 def Context.root_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, sampled: Bool) -> 1529 IO(S & Result<&2, &2, GenerationError, LocalContext>): 1530 TracePlan.generate_with(~S, ~read, source, TracePlan.root(sampled)) 1531 1532 # A generated child of `parent` from a caller's source: the local context of 1533 # its span plan (SpanPlan.child), a span ID that excludes the parent's, with 1534 # the parent's trace ID and the sampled indication that `sampling` resolves. 1535 # It reads at most 16 words. Laws: child_composed, child_tape, child_ends, 1536 # child_exhaustion and generated_child. 1537 def Context.child_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 1538 parent: Parent, sampling: Sampling) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 1539 SpanPlan.generate_with(~S, ~read, source, SpanPlan.child(parent, sampling)) 1540 1541 # A generated restart replacing `previous` from a caller's source: a trace ID 1542 # that excludes the received one, then a span ID, as for a root, with the 1543 # sampled indication `sampled` (TracePlan.restart and 1544 # TracePlan.generate_with). It reads at most 48 words. Laws: 1545 # restart_composed, restart_tape, restart_ends and generated_restart. 1546 def Context.restart_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 1547 previous: RemoteContext, sampled: Bool) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 1548 TracePlan.generate_with(~S, ~read, source, TracePlan.restart(previous, sampled)) 1549 1550 # A deterministic source that replays a tape of word results. 1551 def Source.tape(tape: List<&1, Result<&1, &1, U32 & String, U32>>) -> 1552 IO(List<&1, Result<&1, &1, U32 & String, U32>> & Result<&1, &1, U32 & String, U32>): 1553 IO.pure(List<&1, Result<&1, &1, U32 & String, U32>> & Result<&1, &1, U32 & String, U32>, Tape.next(tape)) 1554 1555 # Error messages 1556 # ============== 1557 # 1558 # Readable names for the error constructors, for logs and test output. They 1559 # include no text received from another participant, except the two 1560 # hexadecimal digits of an unsupported version. 1561 1562 # The name of a codec or ID error, with its offset or, for an unsupported 1563 # version, its two digits. ZeroId names the field: ZeroTraceId, ZeroParentId or 1564 # ZeroSpanId. 1565 def Error.show(error: Error) -> String: 1566 match error: 1567 case UnexpectedEnd{offset}: 1568 "UnexpectedEnd at " ++ Nat.show(offset) 1569 case InvalidHex{offset}: 1570 "InvalidHex at " ++ Nat.show(offset) 1571 case InvalidByte{offset}: 1572 "InvalidByte at " ++ Nat.show(offset) 1573 case ExpectedSeparator{offset}: 1574 "ExpectedSeparator at " ++ Nat.show(offset) 1575 case TrailingInput{}: 1576 "TrailingInput" 1577 case ForbiddenVersion{}: 1578 "ForbiddenVersion" 1579 case UnsupportedVersion{version}: 1580 "UnsupportedVersion " ++ version 1581 case ZeroId{TraceIdField{}}: 1582 "ZeroTraceId" 1583 case ZeroId{ParentIdField{}}: 1584 "ZeroParentId" 1585 case ZeroId{SpanIdField{}}: 1586 "ZeroSpanId" 1587 case ControlCharacter{offset}: 1588 "ControlCharacter at " ++ Nat.show(offset) 1589 1590 # The name of a context creation error. 1591 def ContextError.show(error: ContextError) -> String: 1592 match error: 1593 case ReusedSpanId{}: 1594 "ReusedSpanId" 1595 case ReusedTraceId{}: 1596 "ReusedTraceId" 1597 1598 # The name of a generation error; a source failure adds the source's code and 1599 # message. 1600 def GenerationError.show(error: GenerationError) -> String: 1601 match error: 1602 case SourceFailure{code, message}: 1603 "SourceFailure " ++ U32.show(code) ++ " " ++ message 1604 case ExhaustedTraceId{}: 1605 "ExhaustedTraceId" 1606 case ExhaustedSpanId{}: 1607 "ExhaustedSpanId" 1608 1609 # Limits 1610 # ====== 1611 # 1612 # Budgets, in UTF-8 octets, for the traceparent and tracestate values the 1613 # package reads and the tracestate it emits (spec #1, "Tracestate policy and 1614 # resource bounds"). 1615 1616 # Why a limit configuration was refused. The first failing rule is reported: 1617 # TraceParentInputTooSmall{} the traceparent input budget is below 55 1618 # TraceStateOutputTooSmall{} the tracestate output budget is below 512 1619 # TraceStateInputTooSmall{} the tracestate input budget is below the output 1620 # budget 1621 type LimitsError is Data: 1622 TraceParentInputTooSmall{} 1623 TraceStateOutputTooSmall{} 1624 TraceStateInputTooSmall{} 1625 1626 # The rules of a configuration, which must accept its own emitted 1627 # representation: a traceparent input budget of at least 55 octets, the length 1628 # of a v00 value, and a tracestate input budget no smaller than an output 1629 # budget of at least 512 octets (spec #1, "Tracestate policy and resource 1630 # bounds"; the 512-octet minimum comes from #8; law limits_bounds). 1631 def Limits.is_valid(traceparent_input: Nat, tracestate_input: Nat, +tracestate_output: Nat) -> Bool: 1632 Bool.and(Nat.is_ge(traceparent_input, 55n), 1633 Bool.and(Nat.is_ge(tracestate_output, 512n), Nat.is_ge(tracestate_input, tracestate_output))) 1634 1635 # Budgets in UTF-8 octets. The input budgets bound a received traceparent value 1636 # and a combined tracestate value; the output budget is the most an emitted 1637 # tracestate may take. `evidence` is the proof of Limits.is_valid, so every 1638 # Limits value follows the rules. 1639 type Limits is Data: 1640 Limits{ 1641 traceparent_input: Nat, 1642 tracestate_input: Nat, 1643 tracestate_output: Nat, 1644 evidence: {Limits.is_valid(traceparent_input, tracestate_input, tracestate_output) == True{} : Bool} 1645 } 1646 1647 # The first rule a refused configuration breaks. 1648 def Limits.error(traceparent_input: Nat, tracestate_output: Nat) -> LimitsError: 1649 Bool.pick(LimitsError, Nat.is_lt(traceparent_input, 55n), TraceParentInputTooSmall{}, 1650 Bool.pick(LimitsError, Nat.is_lt(tracestate_output, 512n), TraceStateOutputTooSmall{}, 1651 TraceStateInputTooSmall{})) 1652 1653 # The configuration, when the check found it valid. 1654 def Limits.new.checked(traceparent_input: Nat, tracestate_input: Nat, tracestate_output: Nat, valid: Bool, 1655 evidence: {Limits.is_valid(traceparent_input, tracestate_input, tracestate_output) == valid : Bool}) -> 1656 Result<&2, &2, LimitsError, Limits>: 1657 match valid: 1658 case True{}: 1659 Done{Limits{traceparent_input, tracestate_input, tracestate_output, evidence}} 1660 case False{}: 1661 Fail{Limits.error(traceparent_input, tracestate_output)} 1662 1663 # Validate a configuration; budgets count UTF-8 octets (laws limits_new and 1664 # limits_fields). 1665 def Limits.new(+traceparent_input: Nat, +tracestate_input: Nat, +tracestate_output: Nat) -> 1666 Result<&2, &2, LimitsError, Limits>: 1667 Limits.new.checked(traceparent_input, tracestate_input, tracestate_output, 1668 Limits.is_valid(traceparent_input, tracestate_input, tracestate_output), {==}) 1669 1670 # 32 KiB for each received value and 512 octets for an emitted tracestate 1671 # (law default_limits). The 512-octet output budget is this package's capacity 1672 # policy, not a W3C maximum. 1673 def Limits.default() -> Limits: 1674 Limits{32768n, 32768n, 512n, {==}} 1675 1676 # The most octets a received traceparent value may take. 1677 def Limits.traceparent_input(limits: Limits) -> Nat: 1678 match limits: 1679 case Limits{traceparent_input, tracestate_input, tracestate_output, evidence}: 1680 traceparent_input 1681 1682 # The most octets a combined tracestate value may take, including the commas 1683 # that join repeated fields. 1684 def Limits.tracestate_input(limits: Limits) -> Nat: 1685 match limits: 1686 case Limits{traceparent_input, tracestate_input, tracestate_output, evidence}: 1687 tracestate_input 1688 1689 # The most octets an emitted tracestate may take. 1690 def Limits.tracestate_output(limits: Limits) -> Nat: 1691 match limits: 1692 case Limits{traceparent_input, tracestate_input, tracestate_output, evidence}: 1693 tracestate_output 1694 1695 # The name of a limits error. 1696 def LimitsError.show(error: LimitsError) -> String: 1697 match error: 1698 case TraceParentInputTooSmall{}: 1699 "TraceParentInputTooSmall" 1700 case TraceStateOutputTooSmall{}: 1701 "TraceStateOutputTooSmall" 1702 case TraceStateInputTooSmall{}: 1703 "TraceStateInputTooSmall" 1704 1705 # Tracestate: characters, keys and values 1706 # ======================================= 1707 # 1708 # The Level 2 grammar of W3C 3.3.2.2. The character classes are written with 1709 # the code point ranges of the standard's ABNF. 1710 1711 # Why a tracestate key, value or received member was refused: 1712 # MissingEquals{} a nonempty member has no "=" 1713 # InvalidKey{} the text before the first "=" is not a key 1714 # InvalidValue{} the text after it, without trailing optional whitespace, 1715 # is not a value 1716 type EntryError is Data: 1717 MissingEquals{} 1718 InvalidKey{} 1719 InvalidValue{} 1720 1721 # Whether a code point lies between two others, both included. 1722 def StateChar.in_range(+code: U32, low: U32, high: U32) -> Bool: 1723 Bool.and(U32.is_ge(code, low), U32.is_le(code, high)) 1724 1725 # lcalpha / DIGIT: a lowercase ASCII letter (%x61-7A) or a digit (%x30-39), 1726 # the first character of a key. 1727 def StateChar.is_key_start(char: Char) -> Bool: 1728 match char: 1729 case Chr{+code}: 1730 Bool.or(StateChar.in_range(code, 97, 122), StateChar.in_range(code, 48, 57)) 1731 1732 # keychar: lcalpha / DIGIT / "_" / "-" / "*" / "/" / "@". 1733 def StateChar.is_key(+char: Char) -> Bool: 1734 Bool.or(StateChar.is_key_start(char), Bool.or(Char.is_eq(char, '_'), Bool.or(Char.is_eq(char, '-'), 1735 Bool.or(Char.is_eq(char, '*'), Bool.or(Char.is_eq(char, '/'), Char.is_eq(char, '@')))))) 1736 1737 # nblk-chr: %x21-2B / %x2D-3C / %x3E-7E, printable ASCII other than space, 1738 # "," and "=". A value ends with one of these. 1739 def StateChar.is_value_end(char: Char) -> Bool: 1740 match char: 1741 case Chr{+code}: 1742 Bool.or(StateChar.in_range(code, 33, 43), Bool.or(StateChar.in_range(code, 45, 60), 1743 StateChar.in_range(code, 62, 126))) 1744 1745 # chr: %x20 / nblk-chr, a character of a value: nblk-chr or a space. 1746 def StateChar.is_value(+char: Char) -> Bool: 1747 Bool.or(Char.is_eq(char, ' '), StateChar.is_value_end(char)) 1748 1749 # OWS: a space or a horizontal tab (RFC 9110, section 5.6.3). 1750 def StateChar.is_ows(+char: Char) -> Bool: 1751 Bool.or(Char.is_eq(char, ' '), Char.is_eq(char, '\t')) 1752 1753 # Every remaining character is a key character, and at most `room` remain. 1754 # The recursion stops once the room is used up, so a huge invalid key is not 1755 # read to its end. 1756 def StateKey.valid.rest(text: String, room: Nat) -> Bool: 1757 match text: 1758 case SNil{}: 1759 True{} 1760 case SCon{char, tail}: 1761 match room: 1762 case 0n: 1763 False{} 1764 case 1n+left: 1765 Bool.and(StateChar.is_key(char), StateKey.valid.rest(tail, left)) 1766 1767 # key = ( lcalpha / DIGIT ) 0*255( keychar ): 1 to 256 characters (W3C 1768 # 3.3.2.2.1). Level 1's tenant@system restriction does not apply. 1769 def StateKey.is_valid(text: String) -> Bool: 1770 match text: 1771 case SNil{}: 1772 False{} 1773 case SCon{char, tail}: 1774 Bool.and(StateChar.is_key_start(char), StateKey.valid.rest(tail, 255n)) 1775 1776 # `char` is a value character followed by `tail`, of which at most `room` 1777 # characters are allowed; the last character is not a space. 1778 def StateValue.valid.go(tail: String, char: Char, room: Nat) -> Bool: 1779 match tail: 1780 case SNil{}: 1781 StateChar.is_value_end(char) 1782 case SCon{next, rest}: 1783 match room: 1784 case 0n: 1785 False{} 1786 case 1n+left: 1787 Bool.and(StateChar.is_value(char), StateValue.valid.go(rest, next, left)) 1788 1789 # value = 0*255( chr ) nblk-chr: 1 to 256 printable ASCII characters other 1790 # than "," and "=", the last of which is not a space (W3C 3.3.2.2.2). 1791 def StateValue.is_valid(text: String) -> Bool: 1792 match text: 1793 case SNil{}: 1794 False{} 1795 case SCon{char, tail}: 1796 StateValue.valid.go(tail, char, 255n) 1797 1798 # A tracestate key, naming the vendor that owns an entry. `evidence` proves the 1799 # Level 2 key grammar for `text`, so a StateKey is always valid: build one with 1800 # StateKey.parse (the negative fixture tests/reject/invalid_state_key.bend 1801 # shows that direct construction with a wrong text does not compile). 1802 type StateKey is Data: 1803 StateKey{text: String, evidence: {StateKey.is_valid(text) == True{} : Bool}} 1804 1805 # A tracestate value, opaque to every other vendor. `evidence` proves the 1806 # Level 2 value grammar for `text`. Leading spaces are part of the value. 1807 type StateValue is Data: 1808 StateValue{text: String, evidence: {StateValue.is_valid(text) == True{} : Bool}} 1809 1810 # The key, when the check found the text valid. 1811 def StateKey.parse.checked(text: String, valid: Bool, evidence: {StateKey.is_valid(text) == valid : Bool}) -> 1812 Result<&2, &2, EntryError, StateKey>: 1813 match valid: 1814 case True{}: 1815 Done{StateKey{text, evidence}} 1816 case False{}: 1817 Fail{InvalidKey{}} 1818 1819 # Accept exactly a Level 2 key, or fail with InvalidKey. Nothing is trimmed 1820 # or folded (laws key_parse, key_roundtrip and key_separators). 1821 def StateKey.parse(+text: String) -> Result<&2, &2, EntryError, StateKey>: 1822 StateKey.parse.checked(text, StateKey.is_valid(text), {==}) 1823 1824 # The key's text. 1825 def StateKey.to_string(key: StateKey) -> String: 1826 match key: 1827 case StateKey{text, evidence}: 1828 text 1829 1830 # The value, when the check found the text valid. 1831 def StateValue.parse.checked(text: String, valid: Bool, evidence: {StateValue.is_valid(text) == valid : Bool}) -> 1832 Result<&2, &2, EntryError, StateValue>: 1833 match valid: 1834 case True{}: 1835 Done{StateValue{text, evidence}} 1836 case False{}: 1837 Fail{InvalidValue{}} 1838 1839 # Accept exactly a Level 2 value, leading spaces included, or fail with 1840 # InvalidValue. No whitespace is trimmed here, so a trailing space is refused 1841 # (laws value_parse, value_roundtrip and value_separators). 1842 def StateValue.parse(+text: String) -> Result<&2, &2, EntryError, StateValue>: 1843 StateValue.parse.checked(text, StateValue.is_valid(text), {==}) 1844 1845 # The value's text. 1846 def StateValue.to_string(value: StateValue) -> String: 1847 match value: 1848 case StateValue{text, evidence}: 1849 text 1850 1851 # The name of an entry error. 1852 def EntryError.show(error: EntryError) -> String: 1853 match error: 1854 case MissingEquals{}: 1855 "MissingEquals" 1856 case InvalidKey{}: 1857 "InvalidKey" 1858 case InvalidValue{}: 1859 "InvalidValue" 1860 1861 # Tracestate: entries, states and lookups 1862 # ======================================= 1863 # 1864 # A state is the ordered list of vendor entries of a tracestate, leftmost first 1865 # (W3C 3.3.3), with distinct keys and at most 32 entries. 1866 1867 # Why a received tracestate value was discarded: 1868 # StateTooLarge{} the combined value exceeds its input budget 1869 # TooManyMembers{} a 33rd nonempty member was reached 1870 # InvalidEntry{member, error} a member is invalid; `member` numbers the 1871 # comma-separated members of the combined value 1872 # from zero, empty members included 1873 # Discarding the state never invalidates a valid traceparent (spec #1). 1874 type StateError is Data: 1875 StateTooLarge{} 1876 TooManyMembers{} 1877 InvalidEntry{member: Nat, error: EntryError} 1878 1879 # One vendor's entry: a key and its value. 1880 type StateEntry is Data: 1881 StateEntry{key: StateKey, value: StateValue} 1882 1883 # The entry's key. 1884 def StateEntry.key(entry: StateEntry) -> StateKey: 1885 match entry: 1886 case StateEntry{key, value}: 1887 key 1888 1889 # The entry's value. 1890 def StateEntry.value(entry: StateEntry) -> StateValue: 1891 match entry: 1892 case StateEntry{key, value}: 1893 value 1894 1895 # The text of the entry's key. 1896 def StateEntry.key_text(entry: StateEntry) -> String: 1897 StateKey.to_string(StateEntry.key(entry)) 1898 1899 # `key=value`, as the entry is sent. 1900 def StateEntry.format(entry: StateEntry) -> String: 1901 match entry: 1902 case StateEntry{key, value}: 1903 StateKey.to_string(key) ++ "=" ++ StateValue.to_string(value) 1904 1905 # Whether one of the entries has this key. 1906 def Entries.has_key(entries: List<&2, StateEntry>, +key: String) -> Bool: 1907 match entries: 1908 case Nil{}: 1909 False{} 1910 case Con{entry, rest}: 1911 Bool.or(String.eq(StateEntry.key_text(entry), key), Entries.has_key(rest, key)) 1912 1913 # No entry repeats the key of an entry before it; `seen` holds the entries 1914 # already passed. This is the order in which the reading machine checks keys. 1915 def Entries.unique(entries: List<&2, StateEntry>, +seen: List<&2, StateEntry>) -> Bool: 1916 match entries: 1917 case Nil{}: 1918 True{} 1919 case Con{+entry, rest}: 1920 Bool.and(Bool.not(Entries.has_key(seen, StateEntry.key_text(entry))), 1921 Entries.unique(rest, List.append(&2, StateEntry, seen, Con{entry, Nil{}}))) 1922 1923 # Distinct keys and at most 32 entries (W3C 3.3.2 and 3.3.3). 1924 def TraceState.is_valid(+entries: List<&2, StateEntry>) -> Bool: 1925 Bool.and(Entries.unique(entries, Nil{}), Nat.is_le(List.length(&2, StateEntry, entries), 32n)) 1926 1927 # Ordered vendor state: at most 32 entries with distinct keys, leftmost first. 1928 # `evidence` proves both properties, so every TraceState has them (law 1929 # state_valid). 1930 type TraceState is Data: 1931 TraceState{entries: List<&2, StateEntry>, evidence: {TraceState.is_valid(entries) == True{} : Bool}} 1932 1933 # The state with no entries. It formats as "". 1934 def TraceState.empty() -> TraceState: 1935 TraceState{Nil{}, {==}} 1936 1937 # The entries in order, leftmost first. 1938 def TraceState.entries(state: TraceState) -> List<&2, StateEntry>: 1939 match state: 1940 case TraceState{entries, evidence}: 1941 entries 1942 1943 # Whether the state has no entries. 1944 def TraceState.is_empty(state: TraceState) -> Bool: 1945 List.is_empty(&2, StateEntry, TraceState.entries(state)) 1946 1947 # The value of `entry` when its key matched, or the result for the rest. 1948 def Entries.get.put(entry: StateEntry, rest: Maybe<&2, StateValue>, hit: Bool) -> Maybe<&2, StateValue>: 1949 match hit: 1950 case True{}: 1951 Some{StateEntry.value(entry)} 1952 case False{}: 1953 rest 1954 1955 # The value of the first entry with this key. 1956 def Entries.get(entries: List<&2, StateEntry>, +key: String) -> Maybe<&2, StateValue>: 1957 match entries: 1958 case Nil{}: 1959 None{} 1960 case Con{+entry, rest}: 1961 Entries.get.put(entry, Entries.get(rest, key), String.eq(StateEntry.key_text(entry), key)) 1962 1963 # The value of the entry with this key, if there is one (laws get_entry and 1964 # get_absent). The key is validated, so a lookup never needs to check it. 1965 def TraceState.get(state: TraceState, key: StateKey) -> Maybe<&2, StateValue>: 1966 Entries.get(TraceState.entries(state), StateKey.to_string(key)) 1967 1968 # Each entry after the first, preceded by its comma. 1969 def Entries.format.rest(entries: List<&2, StateEntry>) -> String: 1970 match entries: 1971 case Nil{}: 1972 "" 1973 case Con{entry, rest}: 1974 "," ++ StateEntry.format(entry) ++ Entries.format.rest(rest) 1975 1976 # The entries as `key=value`, joined by commas. 1977 def Entries.format(entries: List<&2, StateEntry>) -> String: 1978 match entries: 1979 case Nil{}: 1980 "" 1981 case Con{entry, rest}: 1982 StateEntry.format(entry) ++ Entries.format.rest(rest) 1983 1984 # The normalized value: the entries in order, joined by commas, with no 1985 # optional whitespace. The empty state formats as "" (laws state_roundtrip and 1986 # first_wins). 1987 def TraceState.format(state: TraceState) -> String: 1988 Entries.format(TraceState.entries(state)) 1989 1990 # Tracestate: budgets 1991 # =================== 1992 # 1993 # A received value is measured in UTF-8 octets before it is read. Measuring 1994 # stops at the first character past the budget, so an oversized value is never 1995 # read to its end. 1996 1997 # The UTF-8 octets of a character. Bend characters are Unicode code points, so 1998 # this is the size of the character's UTF-8 encoding: 1 to 4. 1999 def Utf8.width(char: Char) -> Nat: 2000 match char: Lines 1-2000 of 3907. More: https://jend.leeeet.dev/read.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&start_line=2001