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

<- Parse.digits(p, tail, 1n+at) 304 return Parsed.prepend(p, digit, parsed) 305 306 # The rest of the text after a "-", or ExpectedSeparator at its offset. 307 def Parse.separator_result(tail: String, ok: Bool, offset: Nat) -> 308 Result<&2, &2, Error, String>: 309 match ok: 310 case False{}: 311 Fail{ExpectedSeparator{offset}} 312 case True{}: 313 Done{tail} 314 315 # Read the "-" expected at `offset`. 316 def Parse.separator(text: String, offset: Nat) -> Result<&2, &2, Error, String>: 317 match text: 318 case SNil{}: 319 Fail{UnexpectedEnd{offset}} 320 case SCon{char, tail}: 321 Parse.separator_result(tail, Char.is_eq(char, '-'), offset) 322 323 # The value must end here. Only the first character after it is inspected, so 324 # an arbitrarily long suffix is refused without being read. 325 def Parse.end(text: String) -> Result<&2, &2, Error, Unit>: 326 match text: 327 case SNil{}: 328 Done{Unit{}} 329 case SCon{char, tail}: 330 Fail{TrailingInput{}} 331 332 # The version digits: 00 is the only version the strict codec reads, ff is 333 # forbidden (W3C 3.2.2.1), and any other version is reported with its text. 334 def Parse.version(digits: Digits.Digits(2n)) -> Result<&2, &2, Error, Unit>: 335 match digits: 336 case Digits.DCon{Hex.H0{}, Digits.DCon{Hex.H0{}, Digits.DNil{}}}: 337 Done{Unit{}} 338 case Digits.DCon{Hex.Hf{}, Digits.DCon{Hex.Hf{}, Digits.DNil{}}}: 339 Fail{ForbiddenVersion{}} 340 case other: 341 Fail{UnsupportedVersion{Digits.Digits.to_string(2n, other)}} 342 343 # Attach the proof that digits are not all zero, or fail with ZeroId naming 344 # the field. 345 def Parse.nonzero_result(-n: Nat, result: Maybe<&2, Digits.NonZero>, field: Field) -> 346 Result<&2, &2, Error, Digits.NonZero>: 347 match result: 348 case None{}: 349 Fail{ZeroId{field}} 350 case Some{id}: 351 Done{id} 352 353 # Check that digits are not all zero (W3C 3.2.2.3, 3.2.2.4). 354 def Parse.nonzero(n: Nat, digits: Digits.Digits(n), field: Field) -> 355 Result<&2, &2, Error, Digits.NonZero>: 356 Parse.nonzero_result(n, Digits.NonZero.new(n, digits), field) 357 358 # The last field: the two flag digits, then the end of the text. 359 def Parse.flags(trace_id: Digits.NonZero<32n>, parent_id: Digits.NonZero<16n>, 360 parsed: Parsed<2n>) -> Result<&2, &2, Error, TraceParentV00>: 361 match parsed: 362 case Parsed{flags, rest}: 363 do Result<&2, &2, Error, TraceParentV00>: 364 end : Unit <- Parse.end(rest) 365 return TraceParentV00{trace_id, parent_id, flags} 366 367 # After the trace ID: the parent ID, which must not be all zero, its "-" at 368 # offset 52 and the flag digits at offset 53. 369 def Parse.parent(trace_id: Digits.NonZero<32n>, parsed: Parsed<16n>) -> 370 Result<&2, &2, Error, TraceParentV00>: 371 match parsed: 372 case Parsed{parent_digits, rest}: 373 do Result<&2, &2, Error, TraceParentV00>: 374 parent_id : Digits.NonZero<16n> <- Parse.nonzero(16n, parent_digits, ParentIdField{}) 375 after : String <- Parse.separator(rest, 52n) 376 flags : Parsed<2n> <- Parse.digits(2n, after, 53n) 377 Parse.flags(trace_id, parent_id, flags) 378 379 # After the version: the trace ID, which must not be all zero, its "-" at 380 # offset 35 and the parent ID from offset 36. 381 def Parse.trace(parsed: Parsed<32n>) -> Result<&2, &2, Error, TraceParentV00>: 382 match parsed: 383 case Parsed{trace_digits, rest}: 384 do Result<&2, &2, Error, TraceParentV00>: 385 trace_id : Digits.NonZero<32n> <- Parse.nonzero(32n, trace_digits, TraceIdField{}) 386 after : String <- Parse.separator(rest, 35n) 387 parent : Parsed<16n> <- Parse.digits(16n, after, 36n) 388 Parse.parent(trace_id, parent) 389 390 # After the two version digits: the version check, the "-" at offset 2 and the 391 # trace ID from offset 3. 392 def Parse.start(parsed: Parsed<2n>) -> Result<&2, &2, Error, TraceParentV00>: 393 match parsed: 394 case Parsed{version, rest}: 395 do Result<&2, &2, Error, TraceParentV00>: 396 version_ok : Unit <- Parse.version(version) 397 after : String <- Parse.separator(rest, 2n) 398 trace : Parsed<32n> <- Parse.digits(32n, after, 3n) 399 Parse.trace(trace) 400 401 # Parse a strict traceparent v00 value: exactly "00-", 32 lowercase 402 # hexadecimal digits, "-", 16 digits, "-" and two digits; the IDs must not be 403 # all zero. No whitespace, case folding or suffix is accepted, and every flag 404 # byte is kept as received. 405 # This is the strict wire codec, not a complete W3C propagator: 406 # TraceParent.read and Context.extract apply the processing rules of W3C 3.2.4 407 # and 4.1.2, such as reading later versions by their known prefix. 408 # Laws: roundtrip, inverse and formatted_length. 409 def TraceParentV00.parse(text: String) -> Result<&2, &2, Error, TraceParentV00>: 410 do Result<&2, &2, Error, TraceParentV00>: 411 version : Parsed<2n> <- Parse.digits(2n, text, 0n) 412 Parse.start(version) 413 414 # The text of a strict v00 value: always 55 characters. It is total, because 415 # validity is carried by the argument's type, and it preserves every flag bit: 416 # it is the exact inverse of parse, not an outgoing-header policy (see 417 # LocalContext.to_traceparent for what a participant emits). 418 def TraceParentV00.format(context: TraceParentV00) -> String: 419 match context: 420 case TraceParentV00{trace_id, parent_id, flags}: 421 "00-" ++ Digits.NonZero.to_string(32n, trace_id) ++ "-" ++ 422 Digits.NonZero.to_string(16n, parent_id) ++ "-" ++ 423 Digits.Digits.to_string(2n, flags) 424 425 # Whether the sampled flag, bit 0 of the flag byte, is set (W3C 3.2.2.5.1). 426 def TraceParentV00.is_sampled(context: TraceParentV00) -> Bool: 427 match context: 428 case TraceParentV00{trace_id, parent_id, 429 Digits.DCon{high, Digits.DCon{low, Digits.DNil{}}}}: 430 Hex.Digit.is_odd(low) 431 432 # Whether the random-trace-id flag, bit 1, is set (W3C 3.2.2.5.2). It records 433 # the sender's assertion; it does not prove how the trace ID was generated. 434 def TraceParentV00.is_random(context: TraceParentV00) -> Bool: 435 match context: 436 case TraceParentV00{trace_id, parent_id, 437 Digits.DCon{high, Digits.DCon{low, Digits.DNil{}}}}: 438 Hex.Digit.has_bit1(low) 439 440 # Identifiers and contexts 441 # ======================== 442 # 443 # Supplied IDs are parsed with the same digit reader as the codec. Contexts are 444 # created from validated IDs: a root, a child continuing a parent, a restart 445 # replacing a received trace, or the explicit construction of an operation the 446 # caller owns. 447 448 # The digits of a supplied ID must be the whole text, and not all zero. 449 def Parse.id.finish(n: Nat, parsed: Parsed, field: Field) -> 450 Result<&2, &2, Error, Digits.NonZero>: 451 match parsed: 452 case Parsed{digits, rest}: 453 do Result<&2, &2, Error, Digits.NonZero>: 454 end : Unit <- Parse.end(rest) 455 Parse.nonzero(n, digits, field) 456 457 # A supplied ID is exactly n lowercase hexadecimal digits, not all zero. 458 def Parse.id(+n: Nat, text: String, field: Field) -> 459 Result<&2, &2, Error, Digits.NonZero>: 460 do Result<&2, &2, Error, Digits.NonZero>: 461 parsed : Parsed <- Parse.digits(n, text, 0n) 462 Parse.id.finish(n, parsed, field) 463 464 # Parse a supplied trace ID: exactly 32 lowercase hexadecimal digits, not all 465 # zero. Error offsets count from the start of the ID. The result makes no 466 # randomness assertion (laws trace_id_parse and trace_id_accepts). 467 def TraceId.parse(text: String) -> Result<&2, &2, Error, TraceId>: 468 do Result<&2, &2, Error, TraceId>: 469 value : Digits.NonZero<32n> <- Parse.id(32n, text, TraceIdField{}) 470 return TraceId{value, False{}} 471 472 # Record the caller's assertion that these digits were generated randomly, so 473 # that the random-trace-id flag is emitted with them. The caller is responsible 474 # for the assertion; validation cannot establish it (law assert_random). 475 def TraceId.assert_random(id: TraceId) -> TraceId: 476 match id: 477 case TraceId{value, random}: 478 TraceId{value, True{}} 479 480 # Whether the trace ID asserts that it was generated randomly. 481 def TraceId.is_random(id: TraceId) -> Bool: 482 match id: 483 case TraceId{value, random}: 484 random 485 486 # The 32 lowercase hexadecimal digits of the trace ID. 487 def TraceId.to_string(id: TraceId) -> String: 488 match id: 489 case TraceId{value, random}: 490 Digits.NonZero.to_string(32n, value) 491 492 # Whether two trace IDs name the same trace. The randomness assertion is not 493 # part of the identifier, so it is ignored. 494 def TraceId.is_eq(a: TraceId, b: TraceId) -> Bool: 495 String.eq(TraceId.to_string(a), TraceId.to_string(b)) 496 497 # Parse a supplied span ID: exactly 16 lowercase hexadecimal digits, not all 498 # zero (laws span_id_parse and span_id_roundtrip). 499 def SpanId.parse(text: String) -> Result<&2, &2, Error, SpanId>: 500 do Result<&2, &2, Error, SpanId>: 501 value : Digits.NonZero<16n> <- Parse.id(16n, text, SpanIdField{}) 502 return SpanId{value} 503 504 # The 16 lowercase hexadecimal digits of the span ID. 505 def SpanId.to_string(id: SpanId) -> String: 506 match id: 507 case SpanId{value}: 508 Digits.NonZero.to_string(16n, value) 509 510 # Whether two span IDs name the same operation. 511 def SpanId.is_eq(a: SpanId, b: SpanId) -> Bool: 512 String.eq(SpanId.to_string(a), SpanId.to_string(b)) 513 514 # The sampled indication a child receives: the inherited one, unless the 515 # caller set another (law sampling). 516 def Sampling.resolve(sampling: Sampling, inherited: Bool) -> Bool: 517 match sampling: 518 case InheritSampled{}: 519 inherited 520 case SetSampled{sampled}: 521 sampled 522 523 # Interpret a received strict-v00 value as the sender's context. Bit 0 is 524 # sampled and bit 1 is random-trace-id; the reserved bits are not interpreted 525 # and do not travel with the context (law received_flags). 526 def RemoteContext.from_traceparent(value: TraceParentV00) -> RemoteContext: 527 match value: 528 case TraceParentV00{trace_id, parent_id, 529 Digits.DCon{high, Digits.DCon{+low, Digits.DNil{}}}}: 530 RemoteContext{TraceId{trace_id, Hex.Digit.has_bit1(low)}, SpanId{parent_id}, 531 Hex.Digit.is_odd(low)} 532 533 # The trace the received context belongs to. 534 def RemoteContext.trace_id(context: RemoteContext) -> TraceId: 535 match context: 536 case RemoteContext{trace_id, span_id, sampled}: 537 trace_id 538 539 # The sender's operation: the parent ID of the received value. 540 def RemoteContext.span_id(context: RemoteContext) -> SpanId: 541 match context: 542 case RemoteContext{trace_id, span_id, sampled}: 543 span_id 544 545 # The sender's sampled indication. 546 def RemoteContext.is_sampled(context: RemoteContext) -> Bool: 547 match context: 548 case RemoteContext{trace_id, span_id, sampled}: 549 sampled 550 551 # The trace this participant's operation belongs to. 552 def LocalContext.trace_id(context: LocalContext) -> TraceId: 553 match context: 554 case LocalContext{trace_id, span_id, sampled}: 555 trace_id 556 557 # This participant's operation. 558 def LocalContext.span_id(context: LocalContext) -> SpanId: 559 match context: 560 case LocalContext{trace_id, span_id, sampled}: 561 span_id 562 563 # The sampled indication this participant sends. 564 def LocalContext.is_sampled(context: LocalContext) -> Bool: 565 match context: 566 case LocalContext{trace_id, span_id, sampled}: 567 sampled 568 569 # The participating representation of a local context: version 00, and flags 570 # limited to sampled (bit 0) and random-trace-id (bit 1), with every reserved 571 # bit zero (W3C 3.2.2.5.3; laws emitted_traceparent and emitted_projection). 572 def LocalContext.to_traceparent(context: LocalContext) -> TraceParentV00: 573 match context: 574 case LocalContext{TraceId{trace_id, random}, SpanId{span_id}, sampled}: 575 TraceParentV00{trace_id, span_id, 576 Digits.DCon{Hex.H0{}, Digits.DCon{Hex.Digit.from_bits(sampled, random, False{}, False{}), Digits.DNil{}}}} 577 578 # The trace a child continues. 579 def Parent.trace_id(parent: Parent) -> TraceId: 580 match parent: 581 case RemoteParent{context}: 582 RemoteContext.trace_id(context) 583 case LocalParent{context}: 584 LocalContext.trace_id(context) 585 586 # The parent's operation, which a child must not reuse. 587 def Parent.span_id(parent: Parent) -> SpanId: 588 match parent: 589 case RemoteParent{context}: 590 RemoteContext.span_id(context) 591 case LocalParent{context}: 592 LocalContext.span_id(context) 593 594 # The sampled indication a child inherits by default. 595 def Parent.is_sampled(parent: Parent) -> Bool: 596 match parent: 597 case RemoteParent{context}: 598 RemoteContext.is_sampled(context) 599 case LocalParent{context}: 600 LocalContext.is_sampled(context) 601 602 # Represent an operation the caller owns, with supplied IDs and an explicit 603 # sampled indication. The IDs must belong to that operation: validating their 604 # format cannot establish where they came from (law from_ids). 605 def Context.from_ids(trace_id: TraceId, span_id: SpanId, sampled: Bool) -> LocalContext: 606 LocalContext{trace_id, span_id, sampled} 607 608 # Start a trace with supplied IDs. A new root is not sampled (spec #1: "New 609 # roots default to sampled `0`"; law root). generation.bend provides 610 # Context.root, Context.child and Context.restart for generated IDs. 611 def Context.root_from_ids(trace_id: TraceId, span_id: SpanId) -> LocalContext: 612 Context.from_ids(trace_id, span_id, False{}) 613 614 # The child, unless the span ID was found equal to the parent's. 615 def Context.child_from_id.checked(trace_id: TraceId, span_id: SpanId, sampled: Bool, reused: Bool) -> 616 Result<&2, &2, ContextError, LocalContext>: 617 match reused: 618 case True{}: 619 Fail{ReusedSpanId{}} 620 case False{}: 621 Done{Context.from_ids(trace_id, span_id, sampled)} 622 623 # Continue the parent's trace with a new operation identified by a supplied 624 # span ID. The child keeps the trace ID and its randomness assertion, and its 625 # span ID must differ from the parent's (ReusedSpanId otherwise). Sampling is 626 # inherited unless set. Laws: child, child_reuse and child_accepts. 627 def Context.child_from_id(+parent: Parent, +span_id: SpanId, sampling: Sampling) -> 628 Result<&2, &2, ContextError, LocalContext>: 629 Context.child_from_id.checked(Parent.trace_id(parent), span_id, 630 Sampling.resolve(sampling, Parent.is_sampled(parent)), 631 SpanId.is_eq(span_id, Parent.span_id(parent))) 632 633 # The restarted root, unless the trace ID was found equal to the received one. 634 def Context.restart_from_ids.checked(trace_id: TraceId, span_id: SpanId, reused: Bool) -> 635 Result<&2, &2, ContextError, LocalContext>: 636 match reused: 637 case True{}: 638 Fail{ReusedTraceId{}} 639 case False{}: 640 Done{Context.root_from_ids(trace_id, span_id)} 641 642 # Start a new trace with supplied IDs instead of continuing a received context. 643 # The new trace ID must differ from the received one (ReusedTraceId otherwise), 644 # and the root defaults apply, sampled 0 included. Laws: restart, 645 # restart_reuse and restart_accepts. 646 def Context.restart_from_ids(previous: RemoteContext, +trace_id: TraceId, span_id: SpanId) -> 647 Result<&2, &2, ContextError, LocalContext>: 648 Context.restart_from_ids.checked(trace_id, span_id, 649 TraceId.is_eq(trace_id, RemoteContext.trace_id(previous))) 650 651 # Identifiers from source words 652 # ============================= 653 # 654 # Generated IDs are built from 32-bit words: four words for a trace ID and two 655 # for a span ID, most significant first (spec #1). These conversions make no 656 # randomness assertion; generation adds it. 657 658 # The eight lowercase hexadecimal digits of a word, most significant first 659 # (laws hex_injective and word_hex). 660 def U32.to_hex(word: U32) -> String: 661 Digits.Digits.to_string(8n, Digits.Digits.of_u32(word)) 662 663 # A trace ID from nonzero digits, with no randomness assertion. 664 def TraceId.from_digits(value: Maybe<&2, Digits.NonZero<32n>>) -> Maybe<&2, TraceId>: 665 match value: 666 case None{}: 667 None{} 668 case Some{digits}: 669 Some{TraceId{digits, False{}}} 670 671 # A trace ID from four words, read most significant first: the first word 672 # gives the first eight digits. Like a parsed ID it makes no randomness 673 # assertion; add one with TraceId.assert_random when the words are random. An 674 # all-zero candidate is None (laws trace_words and words_unasserted). 675 def TraceId.from_words(first: U32, second: U32, third: U32, fourth: U32) -> Maybe<&2, TraceId>: 676 TraceId.from_digits(Digits.NonZero.new(32n, 677 Digits.Digits.append(8n, 24n, Digits.Digits.of_u32(first), 678 Digits.Digits.append(8n, 16n, Digits.Digits.of_u32(second), 679 Digits.Digits.append(8n, 8n, Digits.Digits.of_u32(third), Digits.Digits.of_u32(fourth)))))) 680 681 # A span ID from nonzero digits. 682 def SpanId.from_digits(value: Maybe<&2, Digits.NonZero<16n>>) -> Maybe<&2, SpanId>: 683 match value: 684 case None{}: 685 None{} 686 case Some{digits}: 687 Some{SpanId{digits}} 688 689 # A span ID from two words, most significant first. An all-zero candidate is 690 # None (law span_words). 691 def SpanId.from_words(first: U32, second: U32) -> Maybe<&2, SpanId>: 692 SpanId.from_digits(Digits.NonZero.new(16n, 693 Digits.Digits.append(8n, 8n, Digits.Digits.of_u32(first), Digits.Digits.of_u32(second)))) 694 695 # Generation machine 696 # ================== 697 # 698 # A generation is a small state machine fed one source word at a time. It 699 # draws the trace ID first (for a root or a restart), then the span ID, gives 700 # each identifier eight candidates, rejects zero and reused IDs, and stops at 701 # the first source error. The same machine runs over a replayed tape in the 702 # laws and over the host's cryptographic source in generation.bend. 703 704 # A root draws its trace ID, then its span ID, and starts unsampled. Seven 705 # further candidates follow the first, eight in all. 706 def Draw.root() -> Step: 707 NeedWord{DrawTrace{7n, NoTraceWord{}, None{}}} 708 709 # A restart draws like a root but must not reuse the received trace ID. 710 def Draw.restart(previous: RemoteContext) -> Step: 711 NeedWord{DrawTrace{7n, NoTraceWord{}, Some{RemoteContext.trace_id(previous)}}} 712 713 # A child keeps the parent's trace ID and draws a span ID other than the 714 # parent's. 715 def Draw.child(+parent: Parent, sampling: Sampling) -> Step: 716 NeedWord{DrawSpan{7n, NoSpanWord{}, 717 SpanPlan{Parent.trace_id(parent), Sampling.resolve(sampling, Parent.is_sampled(parent)), 718 Some{Parent.span_id(parent)}}}} 719 720 # Try another trace ID candidate, or fail once the eight are used. 721 def Draw.retry_trace(remaining: Nat, previous: Maybe<&2, TraceId>) -> Step: 722 match remaining: 723 case 0n: 724 Failed{ExhaustedTraceId{}} 725 case 1n+p: 726 NeedWord{DrawTrace{p, NoTraceWord{}, previous}} 727 728 # An accepted trace ID is followed by the span ID, with the root default 729 # sampled indication. 730 def Draw.accept_trace(trace_id: TraceId) -> Step: 731 NeedWord{DrawSpan{7n, NoSpanWord{}, SpanPlan{trace_id, False{}, None{}}}} 732 733 # A trace ID candidate equal to the received one is retried. 734 def Draw.reuse_trace(reused: Bool, id: TraceId, previous: TraceId, remaining: Nat) -> Step: 735 match reused: 736 case True{}: 737 Draw.retry_trace(remaining, Some{previous}) 738 case False{}: 739 Draw.accept_trace(id) 740 741 # Check a complete trace ID candidate: zero and, for a restart, the received 742 # trace ID are retried; anything else is accepted. 743 def Draw.check_trace(candidate: Maybe<&2, TraceId>, previous: Maybe<&2, TraceId>, remaining: Nat) -> Step: 744 match candidate: 745 case None{}: 746 Draw.retry_trace(remaining, previous) 747 case Some{+id}: 748 match previous: 749 case None{}: 750 Draw.accept_trace(id) 751 case Some{+old}: 752 Draw.reuse_trace(TraceId.is_eq(id, old), id, old, remaining) 753 754 # Try another span ID candidate, or fail once the eight are used. 755 def Draw.retry_span(remaining: Nat, plan: SpanPlan) -> Step: 756 match remaining: 757 case 0n: 758 Failed{ExhaustedSpanId{}} 759 case 1n+p: 760 NeedWord{DrawSpan{p, NoSpanWord{}, plan}} 761 762 # An accepted span ID completes the new local context. 763 def Draw.accept_span(id: SpanId, plan: SpanPlan) -> Step: 764 match plan: 765 case SpanPlan{trace_id, sampled, parent}: 766 Created{Context.from_ids(trace_id, id, sampled)} 767 768 # A span ID candidate equal to the parent's is retried. 769 def Draw.reuse_span(reused: Bool, id: SpanId, plan: SpanPlan, remaining: Nat) -> Step: 770 match reused: 771 case True{}: 772 Draw.retry_span(remaining, plan) 773 case False{}: 774 Draw.accept_span(id, plan) 775 776 # Check a complete span ID candidate: zero and, for a child, the parent's span 777 # ID are retried; anything else is accepted. 778 def Draw.check_span(candidate: Maybe<&2, SpanId>, plan: SpanPlan, remaining: Nat) -> Step: 779 match candidate: 780 case None{}: 781 Draw.retry_span(remaining, plan) 782 case Some{+id}: 783 match plan: 784 case SpanPlan{+trace_id, +sampled, None{}}: 785 Draw.accept_span(id, SpanPlan{trace_id, sampled, None{}}) 786 case SpanPlan{+trace_id, +sampled, Some{+old}}: 787 Draw.reuse_span(SpanId.is_eq(id, old), id, SpanPlan{trace_id, sampled, Some{old}}, remaining) 788 789 # Generation reads its words from a source trusted to be random, so each 790 # trace ID candidate asserts random-trace-id. 791 def Draw.asserted(candidate: Maybe<&2, TraceId>) -> Maybe<&2, TraceId>: 792 match candidate: 793 case None{}: 794 None{} 795 case Some{id}: 796 Some{TraceId.assert_random(id)} 797 798 # Feed the next source word to the machine. A source error ends the 799 # generation at once with SourceFailure (law feed_failure); a word completes 800 # or extends the current candidate. 801 def Draw.feed(word: Result<&1, &1, U32 & String, U32>, draw: Draw) -> Step: 802 match word: 803 case Fail{(code, message)}: 804 Failed{SourceFailure{code, message}} 805 case Done{next}: 806 match draw: 807 case DrawTrace{remaining, NoTraceWord{}, previous}: 808 NeedWord{DrawTrace{remaining, OneTraceWord{next}, previous}} 809 case DrawTrace{remaining, OneTraceWord{first}, previous}: 810 NeedWord{DrawTrace{remaining, TwoTraceWords{first, next}, previous}} 811 case DrawTrace{remaining, TwoTraceWords{first, second}, previous}: 812 NeedWord{DrawTrace{remaining, ThreeTraceWords{first, second, next}, previous}} 813 case DrawTrace{remaining, ThreeTraceWords{first, second, third}, previous}: 814 Draw.check_trace(Draw.asserted(TraceId.from_words(first, second, third, next)), previous, remaining) 815 case DrawSpan{remaining, NoSpanWord{}, plan}: 816 NeedWord{DrawSpan{remaining, OneSpanWord{next}, plan}} 817 case DrawSpan{remaining, OneSpanWord{first}, plan}: 818 Draw.check_span(SpanId.from_words(first, next), plan, remaining) 819 820 # The result of a finished generation. A generation that has not finished 821 # would report the identifier it was drawing; the root_ends, child_ends and 822 # restart_ends laws show that the word budgets of the operations below make 823 # those cases unreachable. 824 def Step.result(step: Step) -> Result<&2, &2, GenerationError, LocalContext>: 825 match step: 826 case Created{context}: 827 Done{context} 828 case Failed{error}: 829 Fail{error} 830 case NeedWord{DrawTrace{remaining, words, previous}}: 831 Fail{ExhaustedTraceId{}} 832 case NeedWord{DrawSpan{remaining, words, plan}}: 833 Fail{ExhaustedSpanId{}} 834 835 # Whether a generation has ended, with or without a context. 836 def Step.is_finished(step: Step) -> Bool: 837 match step: 838 case NeedWord{draw}: 839 False{} 840 case Created{context}: 841 True{} 842 case Failed{error}: 843 True{} 844 845 # A deterministic word source for tests and replay: each read takes the next 846 # result, and an empty tape fails with code 1, tape-exhausted. 847 def Tape.next(tape: List<&1, Result<&1, &1, U32 & String, U32>>) -> 848 List<&1, Result<&1, &1, U32 & String, U32>> & Result<&1, &1, U32 & String, U32>: 849 match tape: 850 case Nil{}: 851 (Nil{}, Fail{(1, "tape-exhausted")}) 852 case Con{word, rest}: 853 (rest, word) 854 855 # Feed a word that a source returned, keeping the source's next state. 856 def Draw.fed_by(-S: Type, got: S & Result<&1, &1, U32 & String, U32>, draw: Draw) -> S & Step: 857 (state, word) = got 858 (state, Draw.feed(word, draw)) 859 860 # Whether the generation in a driver's result has ended. 861 def Draw.ended(result: List<&1, Result<&1, &1, U32 & String, U32>> & Step) -> Bool: 862 (tape, step) = result 863 Step.is_finished(step) 864 865 # Drive a generation from a tape, reading one word at a time and stopping as 866 # soon as it ends; unread words stay on the tape. `fuel` bounds the steps, 867 # which Bend requires for termination; the laws show the budgets suffice. 868 def Draw.run(fuel: Nat, current: List<&1, Result<&1, &1, U32 & String, U32>> & Step) -> 869 List<&1, Result<&1, &1, U32 & String, U32>> & Step: 870 match fuel current: 871 case _ Tuple{tape, Created{context}}: 872 (tape, Created{context}) 873 case _ Tuple{tape, Failed{error}}: 874 (tape, Failed{error}) 875 case 0n Tuple{tape, NeedWord{draw}}: 876 (tape, NeedWord{draw}) 877 case 1n+p Tuple{tape, NeedWord{draw}}: 878 Draw.run(p, Draw.fed_by(List<&1, Result<&1, &1, U32 & String, U32>>, Tape.next(tape), draw)) 879 880 # Drive a generation from any source. `read` returns the source's next state 881 # with each word, one word at a time, and the driver stops as soon as the 882 # generation ends; the final source state is handed back, so a caller can see 883 # what was read. `fuel` bounds the words read, as in Draw.run. Templates keep 884 # this driver free of any host effect: the effect, if any, lives in the 885 # source. 886 def Draw.read(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), fuel: Nat, 887 current: S & Step) -> IO(S & Step): 888 match fuel current: 889 case _ Tuple{state, Created{context}}: 890 IO.pure(S & Step, (state, Created{context})) 891 case _ Tuple{state, Failed{error}}: 892 IO.pure(S & Step, (state, Failed{error})) 893 case 0n Tuple{state, NeedWord{draw}}: 894 IO.pure(S & Step, (state, NeedWord{draw})) 895 case 1n+p Tuple{state, NeedWord{draw}}: 896 IO.bind(S & Result<&1, &1, U32 & String, U32>, S & Step, read(state), 897 got => Draw.read(~S, ~read, p, Draw.fed_by(S, got, draw))) 898 899 # The source's final state with the generation's result. 900 def Draw.outcome(-S: Type, done: S & Step) -> S & Result<&2, &2, GenerationError, LocalContext>: 901 (state, step) = done 902 (state, Step.result(step)) 903 904 # Turn the driver's final step into the generation's result. 905 def Draw.finished(~S: Type, action: IO(S & Step)) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 906 IO.bind(S & Step, S & Result<&2, &2, GenerationError, LocalContext>, action, 907 done => IO.pure(S & Result<&2, &2, GenerationError, LocalContext>, Draw.outcome(S, done))) 908 909 # A root: at most 48 words, eight trace ID candidates of four words and eight 910 # span ID candidates of two. 911 def Generation.root() -> Generation: 912 Generation{48n, Draw.root()} 913 914 # A restart replacing `previous`: at most 48 words, as a root. 915 def Generation.restart(previous: RemoteContext) -> Generation: 916 Generation{48n, Draw.restart(previous)} 917 918 # A child of `parent`: at most 16 words, eight span ID candidates. 919 def Generation.child(+parent: Parent, sampling: Sampling) -> Generation: 920 Generation{16n, Draw.child(parent, sampling)} 921 922 # Whether a step needs another word within `fuel` more words. 923 def Generation.needs.of(fuel: Nat, step: Step) -> Bool: 924 match fuel step: 925 case 0n _: 926 False{} 927 case 1n+p NeedWord{draw}: 928 True{} 929 case 1n+p Created{context}: 930 False{} 931 case 1n+p Failed{error}: 932 False{} 933 934 # Whether the generation needs another word: it has not ended, and its 935 # budget allows one more. 936 def Generation.needs(generation: Generation) -> Bool: 937 match generation: 938 case Generation{fuel, step}: 939 Generation.needs.of(fuel, step) 940 941 # The generation after `word`: the step it gives with one word less of 942 # budget, or, for a step that needs no word, the same step with none left. 943 def Generation.fed(fuel: Nat, step: Step, word: Result<&1, &1, U32 & String, U32>) -> Generation: 944 match fuel step: 945 case 0n other: 946 Generation{0n, other} 947 case 1n+p NeedWord{draw}: 948 Generation{p, Draw.feed(word, draw)} 949 case 1n+p Created{context}: 950 Generation{0n, Created{context}} 951 case 1n+p Failed{error}: 952 Generation{0n, Failed{error}} 953 954 # Feed the generation the next word of its source (see Draw.feed). A 955 # generation that needs no word ignores it. 956 def Generation.feed(generation: Generation, word: Result<&1, &1, U32 & String, U32>) -> Generation: 957 match generation: 958 case Generation{fuel, step}: 959 Generation.fed(fuel, step, word) 960 961 # The generation's result: the context it created, or why it failed. One that 962 # still needs a word once its budget is spent has exhausted its candidates; 963 # the root_ends, child_ends and restart_ends laws show that the budgets 964 # suffice. 965 def Generation.result(generation: Generation) -> Result<&2, &2, GenerationError, LocalContext>: 966 match generation: 967 case Generation{fuel, step}: 968 Step.result(step) 969 970 # Drive a generation from a caller's source, one word at a time 971 # (Draw.read), and hand back the source's final state with the result. 972 def Generation.run_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 973 generation: Generation) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 974 match generation: 975 case Generation{fuel, step}: 976 Draw.finished(~S, Draw.read(~S, ~read, fuel, (source, step))) 977 978 # Generated contexts from a caller's source. `read` returns the source's next 979 # state with each word result. The source is trusted to be random: a generated 980 # trace ID asserts random-trace-id. A root or restart reads at most 48 words, 981 # and a child at most 16 (Generation.root and its siblings). 982 # Laws: root_tape, root_ends, root_exhaustion and generated_root. 983 def Context.root_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S) -> 984 IO(S & Result<&2, &2, GenerationError, LocalContext>): 985 Generation.run_with(~S, ~read, source, Generation.root()) 986 987 # A generated child of `parent` from a caller's source: at most 16 words. 988 # Laws: child_tape, child_ends, child_exhaustion and generated_child. 989 def Context.child_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 990 parent: Parent, sampling: Sampling) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 991 Generation.run_with(~S, ~read, source, Generation.child(parent, sampling)) 992 993 # A generated restart replacing `previous` from a caller's source: at most 48 994 # words. Laws: restart_tape, restart_ends and generated_restart. 995 def Context.restart_with(~S: Type, ~read: S -> IO(S & Result<&1, &1, U32 & String, U32>), source: S, 996 previous: RemoteContext) -> IO(S & Result<&2, &2, GenerationError, LocalContext>): 997 Generation.run_with(~S, ~read, source, Generation.restart(previous)) 998 999 # A deterministic source that replays a tape of word results. 1000 def Source.tape(tape: List<&1, Result<&1, &1, U32 & String, U32>>) -> 1001 IO(List<&1, Result<&1, &1, U32 & String, U32>> & Result<&1, &1, U32 & String, U32>): 1002 IO.pure(List<&1, Result<&1, &1, U32 & String, U32>> & Result<&1, &1, U32 & String, U32>, Tape.next(tape)) 1003 1004 # Error messages 1005 # ============== 1006 # 1007 # Readable names for the error constructors, for logs and test output. They 1008 # include no text received from another participant, except the two 1009 # hexadecimal digits of an unsupported version. 1010 1011 # The name of a codec or ID error, with its offset or, for an unsupported 1012 # version, its two digits. ZeroId names the field: ZeroTraceId, ZeroParentId or 1013 # ZeroSpanId. 1014 def Error.show(error: Error) -> String: 1015 match error: 1016 case UnexpectedEnd{offset}: 1017 "UnexpectedEnd at " ++ Nat.show(offset) 1018 case InvalidHex{offset}: 1019 "InvalidHex at " ++ Nat.show(offset) 1020 case ExpectedSeparator{offset}: 1021 "ExpectedSeparator at " ++ Nat.show(offset) 1022 case TrailingInput{}: 1023 "TrailingInput" 1024 case ForbiddenVersion{}: 1025 "ForbiddenVersion" 1026 case UnsupportedVersion{version}: 1027 "UnsupportedVersion " ++ version 1028 case ZeroId{TraceIdField{}}: 1029 "ZeroTraceId" 1030 case ZeroId{ParentIdField{}}: 1031 "ZeroParentId" 1032 case ZeroId{SpanIdField{}}: 1033 "ZeroSpanId" 1034 case ControlCharacter{offset}: 1035 "ControlCharacter at " ++ Nat.show(offset) 1036 1037 # The name of a context creation error. 1038 def ContextError.show(error: ContextError) -> String: 1039 match error: 1040 case ReusedSpanId{}: 1041 "ReusedSpanId" 1042 case ReusedTraceId{}: 1043 "ReusedTraceId" 1044 1045 # The name of a generation error; a source failure adds the source's code and 1046 # message. 1047 def GenerationError.show(error: GenerationError) -> String: 1048 match error: 1049 case SourceFailure{code, message}: 1050 "SourceFailure " ++ U32.show(code) ++ " " ++ message 1051 case ExhaustedTraceId{}: 1052 "ExhaustedTraceId" 1053 case ExhaustedSpanId{}: 1054 "ExhaustedSpanId" 1055 1056 # Limits 1057 # ====== 1058 # 1059 # Budgets, in UTF-8 octets, for the traceparent and tracestate values the 1060 # package reads and the tracestate it emits (spec #1, "Tracestate policy and 1061 # resource bounds"). 1062 1063 # Why a limit configuration was refused. The first failing rule is reported: 1064 # TraceParentInputTooSmall{} the traceparent input budget is below 55 1065 # TraceStateOutputTooSmall{} the tracestate output budget is below 512 1066 # TraceStateInputTooSmall{} the tracestate input budget is below the output 1067 # budget 1068 type LimitsError is Data: 1069 TraceParentInputTooSmall{} 1070 TraceStateOutputTooSmall{} 1071 TraceStateInputTooSmall{} 1072 1073 # The rules of a configuration, which must accept its own emitted 1074 # representation: a traceparent input budget of at least 55 octets, the length 1075 # of a v00 value, and a tracestate input budget no smaller than an output 1076 # budget of at least 512 octets (spec #1, "Tracestate policy and resource 1077 # bounds"; the 512-octet minimum comes from #8; law limits_bounds). 1078 def Limits.is_valid(traceparent_input: Nat, tracestate_input: Nat, +tracestate_output: Nat) -> Bool: 1079 Bool.and(Nat.is_ge(traceparent_input, 55n), 1080 Bool.and(Nat.is_ge(tracestate_output, 512n), Nat.is_ge(tracestate_input, tracestate_output))) 1081 1082 # Budgets in UTF-8 octets. The input budgets bound a received traceparent value 1083 # and a combined tracestate value; the output budget is the most an emitted 1084 # tracestate may take. `evidence` is the proof of Limits.is_valid, so every 1085 # Limits value follows the rules. 1086 type Limits is Data: 1087 Limits{ 1088 traceparent_input: Nat, 1089 tracestate_input: Nat, 1090 tracestate_output: Nat, 1091 evidence: {Limits.is_valid(traceparent_input, tracestate_input, tracestate_output) == True{} : Bool} 1092 } 1093 1094 # The first rule a refused configuration breaks. 1095 def Limits.error(traceparent_input: Nat, tracestate_output: Nat) -> LimitsError: 1096 Bool.pick(LimitsError, Nat.is_lt(traceparent_input, 55n), TraceParentInputTooSmall{}, 1097 Bool.pick(LimitsError, Nat.is_lt(tracestate_output, 512n), TraceStateOutputTooSmall{}, 1098 TraceStateInputTooSmall{})) 1099 1100 # The configuration, when the check found it valid. 1101 def Limits.new.checked(traceparent_input: Nat, tracestate_input: Nat, tracestate_output: Nat, valid: Bool, 1102 evidence: {Limits.is_valid(traceparent_input, tracestate_input, tracestate_output) == valid : Bool}) -> 1103 Result<&2, &2, LimitsError, Limits>: 1104 match valid: 1105 case True{}: 1106 Done{Limits{traceparent_input, tracestate_input, tracestate_output, evidence}} 1107 case False{}: 1108 Fail{Limits.error(traceparent_input, tracestate_output)} 1109 1110 # Validate a configuration; budgets count UTF-8 octets (laws limits_new and 1111 # limits_fields). 1112 def Limits.new(+traceparent_input: Nat, +tracestate_input: Nat, +tracestate_output: Nat) -> 1113 Result<&2, &2, LimitsError, Limits>: 1114 Limits.new.checked(traceparent_input, tracestate_input, tracestate_output, 1115 Limits.is_valid(traceparent_input, tracestate_input, tracestate_output), {==}) 1116 1117 # 32 KiB for each received value and 512 octets for an emitted tracestate 1118 # (law default_limits). The 512-octet output budget is this package's capacity 1119 # policy, not a W3C maximum. 1120 def Limits.default() -> Limits: 1121 Limits{32768n, 32768n, 512n, {==}} 1122 1123 # The most octets a received traceparent value may take. 1124 def Limits.traceparent_input(limits: Limits) -> Nat: 1125 match limits: 1126 case Limits{traceparent_input, tracestate_input, tracestate_output, evidence}: 1127 traceparent_input 1128 1129 # The most octets a combined tracestate value may take, including the commas 1130 # that join repeated fields. 1131 def Limits.tracestate_input(limits: Limits) -> Nat: 1132 match limits: 1133 case Limits{traceparent_input, tracestate_input, tracestate_output, evidence}: 1134 tracestate_input 1135 1136 # The most octets an emitted tracestate may take. 1137 def Limits.tracestate_output(limits: Limits) -> Nat: 1138 match limits: 1139 case Limits{traceparent_input, tracestate_input, tracestate_output, evidence}: 1140 tracestate_output 1141 1142 # The name of a limits error. 1143 def LimitsError.show(error: LimitsError) -> String: 1144 match error: 1145 case TraceParentInputTooSmall{}: 1146 "TraceParentInputTooSmall" 1147 case TraceStateOutputTooSmall{}: 1148 "TraceStateOutputTooSmall" 1149 case TraceStateInputTooSmall{}: 1150 "TraceStateInputTooSmall" 1151 1152 # Tracestate: characters, keys and values 1153 # ======================================= 1154 # 1155 # The Level 2 grammar of W3C 3.3.2.2. The character classes are written with 1156 # the code point ranges of the standard's ABNF. 1157 1158 # Why a tracestate key, value or received member was refused: 1159 # MissingEquals{} a nonempty member has no "=" 1160 # InvalidKey{} the text before the first "=" is not a key 1161 # InvalidValue{} the text after it, without trailing optional whitespace, 1162 # is not a value 1163 type EntryError is Data: 1164 MissingEquals{} 1165 InvalidKey{} 1166 InvalidValue{} 1167 1168 # Whether a code point lies between two others, both included. 1169 def StateChar.in_range(+code: U32, low: U32, high: U32) -> Bool: 1170 Bool.and(U32.is_ge(code, low), U32.is_le(code, high)) 1171 1172 # lcalpha / DIGIT: a lowercase ASCII letter (%x61-7A) or a digit (%x30-39), 1173 # the first character of a key. 1174 def StateChar.is_key_start(char: Char) -> Bool: 1175 match char: 1176 case Chr{+code}: 1177 Bool.or(StateChar.in_range(code, 97, 122), StateChar.in_range(code, 48, 57)) 1178 1179 # keychar: lcalpha / DIGIT / "_" / "-" / "*" / "/" / "@". 1180 def StateChar.is_key(+char: Char) -> Bool: 1181 Bool.or(StateChar.is_key_start(char), Bool.or(Char.is_eq(char, '_'), Bool.or(Char.is_eq(char, '-'), 1182 Bool.or(Char.is_eq(char, '*'), Bool.or(Char.is_eq(char, '/'), Char.is_eq(char, '@')))))) 1183 1184 # nblk-chr: %x21-2B / %x2D-3C / %x3E-7E, printable ASCII other than space, 1185 # "," and "=". A value ends with one of these. 1186 def StateChar.is_value_end(char: Char) -> Bool: 1187 match char: 1188 case Chr{+code}: 1189 Bool.or(StateChar.in_range(code, 33, 43), Bool.or(StateChar.in_range(code, 45, 60), 1190 StateChar.in_range(code, 62, 126))) 1191 1192 # chr: %x20 / nblk-chr, a character of a value: nblk-chr or a space. 1193 def StateChar.is_value(+char: Char) -> Bool: 1194 Bool.or(Char.is_eq(char, ' '), StateChar.is_value_end(char)) 1195 1196 # OWS: a space or a horizontal tab (RFC 9110, section 5.6.3). 1197 def StateChar.is_ows(+char: Char) -> Bool: 1198 Bool.or(Char.is_eq(char, ' '), Char.is_eq(char, '\t')) 1199 1200 # Every remaining character is a key character, and at most `room` remain. 1201 # The recursion stops once the room is used up, so a huge invalid key is not 1202 # read to its end. 1203 def StateKey.valid.rest(text: String, room: Nat) -> Bool: 1204 match text: 1205 case SNil{}: 1206 True{} 1207 case SCon{char, tail}: 1208 match room: 1209 case 0n: 1210 False{} 1211 case 1n+left: 1212 Bool.and(StateChar.is_key(char), StateKey.valid.rest(tail, left)) 1213 1214 # key = ( lcalpha / DIGIT ) 0*255( keychar ): 1 to 256 characters (W3C 1215 # 3.3.2.2.1). Level 1's tenant@system restriction does not apply. 1216 def StateKey.is_valid(text: String) -> Bool: 1217 match text: 1218 case SNil{}: 1219 False{} 1220 case SCon{char, tail}: 1221 Bool.and(StateChar.is_key_start(char), StateKey.valid.rest(tail, 255n)) 1222 1223 # `char` is a value character followed by `tail`, of which at most `room` 1224 # characters are allowed; the last character is not a space. 1225 def StateValue.valid.go(tail: String, char: Char, room: Nat) -> Bool: 1226 match tail: 1227 case SNil{}: 1228 StateChar.is_value_end(char) 1229 case SCon{next, rest}: 1230 match room: 1231 case 0n: 1232 False{} 1233 case 1n+left: 1234 Bool.and(StateChar.is_value(char), StateValue.valid.go(rest, next, left)) 1235 1236 # value = 0*255( chr ) nblk-chr: 1 to 256 printable ASCII characters other 1237 # than "," and "=", the last of which is not a space (W3C 3.3.2.2.2). 1238 def StateValue.is_valid(text: String) -> Bool: 1239 match text: 1240 case SNil{}: 1241 False{} 1242 case SCon{char, tail}: 1243 StateValue.valid.go(tail, char, 255n) 1244 1245 # A tracestate key, naming the vendor that owns an entry. `evidence` proves the 1246 # Level 2 key grammar for `text`, so a StateKey is always valid: build one with 1247 # StateKey.parse (the negative fixture tests/reject/invalid_state_key.bend 1248 # shows that direct construction with a wrong text does not compile). 1249 type StateKey is Data: 1250 StateKey{text: String, evidence: {StateKey.is_valid(text) == True{} : Bool}} 1251 1252 # A tracestate value, opaque to every other vendor. `evidence` proves the 1253 # Level 2 value grammar for `text`. Leading spaces are part of the value. 1254 type StateValue is Data: 1255 StateValue{text: String, evidence: {StateValue.is_valid(text) == True{} : Bool}} 1256 1257 # The key, when the check found the text valid. 1258 def StateKey.parse.checked(text: String, valid: Bool, evidence: {StateKey.is_valid(text) == valid : Bool}) -> 1259 Result<&2, &2, EntryError, StateKey>: 1260 match valid: 1261 case True{}: 1262 Done{StateKey{text, evidence}} 1263 case False{}: 1264 Fail{InvalidKey{}} 1265 1266 # Accept exactly a Level 2 key, or fail with InvalidKey. Nothing is trimmed 1267 # or folded (laws key_parse, key_roundtrip and key_separators). 1268 def StateKey.parse(+text: String) -> Result<&2, &2, EntryError, StateKey>: 1269 StateKey.parse.checked(text, StateKey.is_valid(text), {==}) 1270 1271 # The key's text. 1272 def StateKey.to_string(key: StateKey) -> String: 1273 match key: 1274 case StateKey{text, evidence}: 1275 text 1276 1277 # The value, when the check found the text valid. 1278 def StateValue.parse.checked(text: String, valid: Bool, evidence: {StateValue.is_valid(text) == valid : Bool}) -> 1279 Result<&2, &2, EntryError, StateValue>: 1280 match valid: 1281 case True{}: 1282 Done{StateValue{text, evidence}} 1283 case False{}: 1284 Fail{InvalidValue{}} 1285 1286 # Accept exactly a Level 2 value, leading spaces included, or fail with 1287 # InvalidValue. No whitespace is trimmed here, so a trailing space is refused 1288 # (laws value_parse, value_roundtrip and value_separators). 1289 def StateValue.parse(+text: String) -> Result<&2, &2, EntryError, StateValue>: 1290 StateValue.parse.checked(text, StateValue.is_valid(text), {==}) 1291 1292 # The value's text. 1293 def StateValue.to_string(value: StateValue) -> String: 1294 match value: 1295 case StateValue{text, evidence}: 1296 text 1297 1298 # The name of an entry error. 1299 def EntryError.show(error: EntryError) -> String: 1300 match error: 1301 case MissingEquals{}: 1302 "MissingEquals" 1303 case InvalidKey{}: 1304 "InvalidKey" 1305 case InvalidValue{}: 1306 "InvalidValue" 1307 1308 # Tracestate: entries, states and lookups 1309 # ======================================= 1310 # 1311 # A state is the ordered list of vendor entries of a tracestate, leftmost first 1312 # (W3C 3.3.3), with distinct keys and at most 32 entries. 1313 1314 # Why a received tracestate value was discarded: 1315 # StateTooLarge{} the combined value exceeds its input budget 1316 # TooManyMembers{} a 33rd nonempty member was reached 1317 # InvalidEntry{member, error} a member is invalid; `member` numbers the 1318 # comma-separated members of the combined value 1319 # from zero, empty members included 1320 # Discarding the state never invalidates a valid traceparent (spec #1). 1321 type StateError is Data: 1322 StateTooLarge{} 1323 TooManyMembers{} 1324 InvalidEntry{member: Nat, error: EntryError} 1325 1326 # One vendor's entry: a key and its value. 1327 type StateEntry is Data: 1328 StateEntry{key: StateKey, value: StateValue} 1329 1330 # The entry's key. 1331 def StateEntry.key(entry: StateEntry) -> StateKey: 1332 match entry: 1333 case StateEntry{key, value}: 1334 key 1335 1336 # The entry's value. 1337 def StateEntry.value(entry: StateEntry) -> StateValue: 1338 match entry: 1339 case StateEntry{key, value}: 1340 value 1341 1342 # The text of the entry's key. 1343 def StateEntry.key_text(entry: StateEntry) -> String: 1344 StateKey.to_string(StateEntry.key(entry)) 1345 1346 # `key=value`, as the entry is sent. 1347 def StateEntry.format(entry: StateEntry) -> String: 1348 match entry: 1349 case StateEntry{key, value}: 1350 StateKey.to_string(key) ++ "=" ++ StateValue.to_string(value) 1351 1352 # Whether one of the entries has this key. 1353 def Entries.has_key(entries: List<&2, StateEntry>, +key: String) -> Bool: 1354 match entries: 1355 case Nil{}: 1356 False{} 1357 case Con{entry, rest}: 1358 Bool.or(String.eq(StateEntry.key_text(entry), key), Entries.has_key(rest, key)) 1359 1360 # No entry repeats the key of an entry before it; `seen` holds the entries 1361 # already passed. This is the order in which the reading machine checks keys. 1362 def Entries.unique(entries: List<&2, StateEntry>, +seen: List<&2, StateEntry>) -> Bool: 1363 match entries: 1364 case Nil{}: 1365 True{} 1366 case Con{+entry, rest}: 1367 Bool.and(Bool.not(Entries.has_key(seen, StateEntry.key_text(entry))), 1368 Entries.unique(rest, List.append(&2, StateEntry, seen, Con{entry, Nil{}}))) 1369 1370 # Distinct keys and at most 32 entries (W3C 3.3.2 and 3.3.3). 1371 def TraceState.is_valid(+entries: List<&2, StateEntry>) -> Bool: 1372 Bool.and(Entries.unique(entries, Nil{}), Nat.is_le(List.length(&2, StateEntry, entries), 32n)) 1373 1374 # Ordered vendor state: at most 32 entries with distinct keys, leftmost first. 1375 # `evidence` proves both properties, so every TraceState has them (law 1376 # state_valid). 1377 type TraceState is Data: 1378 TraceState{entries: List<&2, StateEntry>, evidence: {TraceState.is_valid(entries) == True{} : Bool}} 1379 1380 # The state with no entries. It formats as "". 1381 def TraceState.empty() -> TraceState: 1382 TraceState{Nil{}, {==}} 1383 1384 # The entries in order, leftmost first. 1385 def TraceState.entries(state: TraceState) -> List<&2, StateEntry>: 1386 match state: 1387 case TraceState{entries, evidence}: 1388 entries 1389 1390 # Whether the state has no entries. 1391 def TraceState.is_empty(state: TraceState) -> Bool: 1392 List.is_empty(&2, StateEntry, TraceState.entries(state)) 1393 1394 # The value of `entry` when its key matched, or the result for the rest. 1395 def Entries.get.put(entry: StateEntry, rest: Maybe<&2, StateValue>, hit: Bool) -> Maybe<&2, StateValue>: 1396 match hit: 1397 case True{}: 1398 Some{StateEntry.value(entry)} 1399 case False{}: 1400 rest 1401 1402 # The value of the first entry with this key. 1403 def Entries.get(entries: List<&2, StateEntry>, +key: String) -> Maybe<&2, StateValue>: 1404 match entries: 1405 case Nil{}: 1406 None{} 1407 case Con{+entry, rest}: 1408 Entries.get.put(entry, Entries.get(rest, key), String.eq(StateEntry.key_text(entry), key)) 1409 1410 # The value of the entry with this key, if there is one (laws get_entry and 1411 # get_absent). The key is validated, so a lookup never needs to check it. 1412 def TraceState.get(state: TraceState, key: StateKey) -> Maybe<&2, StateValue>: 1413 Entries.get(TraceState.entries(state), StateKey.to_string(key)) 1414 1415 # Each entry after the first, preceded by its comma. 1416 def Entries.format.rest(entries: List<&2, StateEntry>) -> String: 1417 match entries: 1418 case Nil{}: 1419 "" 1420 case Con{entry, rest}: 1421 "," ++ StateEntry.format(entry) ++ Entries.format.rest(rest) 1422 1423 # The entries as `key=value`, joined by commas. 1424 def Entries.format(entries: List<&2, StateEntry>) -> String: 1425 match entries: 1426 case Nil{}: 1427 "" 1428 case Con{entry, rest}: 1429 StateEntry.format(entry) ++ Entries.format.rest(rest) 1430 1431 # The normalized value: the entries in order, joined by commas, with no 1432 # optional whitespace. The empty state formats as "" (laws state_roundtrip and 1433 # first_wins). 1434 def TraceState.format(state: TraceState) -> String: 1435 Entries.format(TraceState.entries(state)) 1436 1437 # Tracestate: budgets 1438 # =================== 1439 # 1440 # A received value is measured in UTF-8 octets before it is read. Measuring 1441 # stops at the first character past the budget, so an oversized value is never 1442 # read to its end. 1443 1444 # The UTF-8 octets of a character. Bend characters are Unicode code points, so 1445 # this is the size of the character's UTF-8 encoding: 1 to 4. 1446 def Utf8.width(char: Char) -> Nat: 1447 match char: 1448 case Chr{+code}: 1449 Bool.pick(Nat, U32.is_lt(code, 128), 1n, 1450 Bool.pick(Nat, U32.is_lt(code, 2048), 2n, 1451 Bool.pick(Nat, U32.is_lt(code, 65536), 3n, 4n))) 1452 1453 # The UTF-8 octets of a text, in which the laws state every budget. Emission 1454 # measures keys and values with it, at most 256 characters each; parsing 1455 # measures received text with Utf8.left instead, which stops counting past 1456 # the budget. 1457 def Utf8.length(text: String) -> Nat: 1458 match text: 1459 case SNil{}: 1460 0n 1461 case SCon{char, tail}: 1462 Nat.add(Utf8.width(char), Utf8.length(tail)) 1463 1464 # What is left of a budget after taking `need` octets, or None when less 1465 # remains. 1466 def Budget.take(need: Nat, budget: Nat) -> Maybe<&2, Nat>: 1467 match need budget: 1468 case 0n _: 1469 Some{budget} 1470 case 1n+more 0n: 1471 None{} 1472 case 1n+more 1n+left: 1473 Budget.take(more, left) 1474 1475 # What is left of a budget after a text, or None once the text exceeds it. 1476 # Measuring stops at the first character beyond the budget, and a None budget 1477 # stays None. 1478 def Utf8.left(text: String, budget: Maybe<&2, Nat>) -> Maybe<&2, Nat>: 1479 match text budget: 1480 case _ None{}: 1481 None{} 1482 case SNil{} Some{left}: 1483 Some{left} 1484 case SCon{char, tail} Some{left}: 1485 Utf8.left(tail, Budget.take(Utf8.width(char), left)) 1486 1487 # Fields after the first are measured with the comma that joins them. Once the 1488 # budget is exceeded, no further field is visited. 1489 def Utf8.left_more(fields: List<&2, String>, budget: Maybe<&2, Nat>) -> Maybe<&2, Nat>: 1490 match fields budget: 1491 case Nil{} _: 1492 budget 1493 case Con{field, rest} None{}: 1494 None{} 1495 case Con{field, rest} Some{left}: 1496 Utf8.left_more(rest, Utf8.left(field, Utf8.left(",", Some{left}))) 1497 1498 # What is left of a budget after repeated fields and the commas that join 1499 # them. 1500 def Utf8.left_fields(fields: List<&2, String>, budget: Maybe<&2, Nat>) -> Maybe<&2, Nat>: 1501 match fields: 1502 case Nil{}: 1503 budget 1504 case Con{field, rest}: 1505 Utf8.left_more(rest, Utf8.left(field, budget)) 1506 1507 # Tracestate: the reading machine 1508 # =============================== 1509 # 1510 # TraceState.parse measures the combined value against its budget, then reads 1511 # it once from left to right, one character at a time. A comma ends the 1512 # current member; the machine validates each nonempty member when it ends, 1513 # counts it toward the 32 allowed, and keeps it only when its key is new. 1514 # Reading stops at the first problem. 1515 1516 # Where reading the current member stands: before its key, with only optional 1517 # whitespace so far; inside its key; or inside its value. Characters read are 1518 # kept most recent first, so each one costs a single step. 1519 type Member is Data: 1520 Blank{} 1521 InKey{text: String} 1522 InValue{key: String, text: String} 1523 1524 # A tracestate being read: the members ended so far, empty ones included; how 1525 # many more nonempty members are allowed; the current member; and the first 1526 # entry of each key, in reading order. Stopped holds the first problem found. 1527 # The scan and its helpers are internal. 1528 type Scan is Data: 1529 Scanning{member: Nat, room: Nat, current: Member, entries: List<&2, StateEntry>} 1530 Stopped{error: StateError} 1531 1532 # A value's characters arrive most recent first. Restoring them skips optional 1533 # whitespace until the first other character, then keeps every character, so 1534 # the value comes back in reading order without its trailing whitespace. 1535 def Value.restore.step(kept: Bool, ows: Bool, char: Char, value: String) -> Bool & String: 1536 match kept: 1537 case True{}: 1538 (True{}, SCon{char, value}) 1539 case False{}: 1540 match ows: 1541 case True{}: 1542 (False{}, value) 1543 case False{}: 1544 (True{}, SCon{char, value}) 1545 1546 # The restoring loop: one character at a time, with the state (whether a 1547 # character was kept yet, the value so far). 1548 def Value.restore.go(text: String, state: Bool & String) -> String: 1549 match text: 1550 case SNil{}: 1551 (kept, value) = state 1552 value 1553 case SCon{+char, tail}: 1554 (kept, value) = state 1555 Value.restore.go(tail, Value.restore.step(kept, StateChar.is_ows(char), char, value)) 1556 1557 # The value in reading order without its trailing optional whitespace. 1558 def Value.restore(text: String) -> String: 1559 Value.restore.go(text, (False{}, "")) 1560 1561 # A character of a member that has no key yet: optional whitespace is 1562 # skipped, an "=" gives the member an empty key, which validation refuses, and 1563 # anything else starts the key. 1564 def Member.start(ows: Bool, equals: Bool, char: Char) -> Member: 1565 match ows: 1566 case True{}: 1567 Blank{} 1568 case False{}: 1569 match equals: 1570 case True{}: 1571 InValue{"", ""} 1572 case False{}: 1573 InKey{SCon{char, SNil{}}} 1574 1575 # A character inside a key: the first "=" ends the key, anything else extends 1576 # it. Key characters are validated when the member ends. 1577 def Member.key(equals: Bool, char: Char, text: String) -> Member: 1578 match equals: 1579 case True{}: 1580 InValue{String.reverse(text), ""} 1581 case False{}: 1582 InKey{SCon{char, text}} 1583 1584 # A character other than a comma extends the current member. Inside a value 1585 # every character is kept; validation refuses those the grammar excludes. 1586 def Member.push(+char: Char, current: Member) -> Member: 1587 match current: 1588 case Blank{}: 1589 Member.start(StateChar.is_ows(char), Char.is_eq(char, '='), char) 1590 case InKey{text}: 1591 Member.key(Char.is_eq(char, '='), char, text) 1592 case InValue{key, text}: 1593 InValue{key, SCon{char, text}} 1594 1595 # Validate the key and value texts of a member that ended. An invalid key is 1596 # reported before an invalid value. 1597 def Scan.validate(key: String, value: String) -> Result<&2, &2, EntryError, StateEntry>: 1598 do Result<&2, &2, EntryError, StateEntry>: 1599 parsed_key : StateKey <- StateKey.parse(key) 1600 parsed_value : StateValue <- StateValue.parse(value) 1601 return StateEntry{parsed_key, parsed_value} 1602 1603 # Keep the entries unchanged when the key was present; otherwise add the 1604 # entry at the end. 1605 def Entries.add.if(entries: List<&2, StateEntry>, entry: StateEntry, present: Bool) -> List<&2, StateEntry>: 1606 match present: 1607 case True{}: 1608 entries 1609 case False{}: 1610 List.append(&2, StateEntry, entries, Con{entry, Nil{}}) 1611 1612 # Keep only the first entry of each key (spec #1, "Preserve the first 1613 # occurrence of a duplicate key"). 1614 def Entries.add(+entries: List<&2, StateEntry>, +entry: StateEntry) -> List<&2, StateEntry>: 1615 Entries.add.if(entries, entry, Entries.has_key(entries, StateEntry.key_text(entry))) 1616 1617 # A valid member counts toward the 32 allowed before duplicates are dropped 1618 # (spec #1); with no room left, the state is discarded with TooManyMembers. 1619 def Scan.keep(room: Nat, member: Nat, entry: StateEntry, entries: List<&2, StateEntry>) -> Scan: 1620 match room: 1621 case 0n: 1622 Stopped{TooManyMembers{}} 1623 case 1n+left: 1624 Scanning{1n+member, left, Blank{}, Entries.add(entries, entry)} 1625 1626 # A member that ended: an invalid one stops reading with its number and 1627 # reason; a valid one is counted and kept. 1628 def Scan.entry(parsed: Result<&2, &2, EntryError, StateEntry>, member: Nat, room: Nat, 1629 entries: List<&2, StateEntry>) -> Scan: 1630 match parsed: 1631 case Fail{error}: 1632 Stopped{InvalidEntry{member, error}} 1633 case Done{entry}: 1634 Scan.keep(room, member, entry, entries) 1635 1636 # The current member ends at a comma or with the value. An empty member, or 1637 # one of optional whitespace only, is ignored but still numbered; a member 1638 # without "=" is refused; otherwise its key and value are validated, trailing 1639 # optional whitespace left out of the value. 1640 def Scan.close(member: Nat, room: Nat, current: Member, entries: List<&2, StateEntry>) -> Scan: 1641 match current: 1642 case Blank{}: 1643 Scanning{1n+member, room, Blank{}, entries} 1644 case InKey{text}: 1645 Stopped{InvalidEntry{member, MissingEquals{}}} 1646 case InValue{key, text}: 1647 Scan.entry(Scan.validate(key, Value.restore(text)), member, room, entries) 1648 1649 # One character of a scan that is still reading: a comma ends the member, and 1650 # anything else extends it. 1651 def Scan.read(comma: Bool, char: Char, member: Nat, room: Nat, current: Member, 1652 entries: List<&2, StateEntry>) -> Scan: 1653 match comma: 1654 case True{}: 1655 Scan.close(member, room, current, entries) 1656 case False{}: 1657 Scanning{member, room, Member.push(char, current), entries} 1658 1659 # Read one character, unless the scan has stopped. 1660 def Scan.char(+char: Char, scan: Scan) -> Scan: 1661 match scan: 1662 case Stopped{error}: 1663 Stopped{error} 1664 case Scanning{member, room, current, entries}: 1665 Scan.read(Char.is_eq(char, ','), char, member, room, current, entries) 1666 1667 # Read a text one character at a time, stopping at the first problem. This is 1668 # a loop (a tail call), so its depth does not grow with the text. 1669 def Scan.text(text: String, scan: Scan) -> Scan: 1670 match text scan: 1671 case _ Stopped{error}: 1672 Stopped{error} 1673 case SNil{} Scanning{member, room, current, entries}: 1674 Scanning{member, room, current, entries} 1675 case SCon{char, tail} Scanning{member, room, current, entries}: 1676 Scan.text(tail, Scan.char(char, Scanning{member, room, current, entries})) 1677 1678 # Fields after the first are read after the comma that joins them. 1679 def Scan.more(fields: List<&2, String>, scan: Scan) -> Scan: 1680 match fields: 1681 case Nil{}: 1682 scan 1683 case Con{field, rest}: 1684 Scan.more(rest, Scan.text(field, Scan.char(',', scan))) 1685 1686 # Read repeated fields as their comma-joined combination. 1687 def Scan.fields(fields: List<&2, String>, scan: Scan) -> Scan: 1688 match fields: 1689 case Nil{}: 1690 scan 1691 case Con{field, rest}: 1692 Scan.more(rest, Scan.text(field, scan)) 1693 1694 # The scan of a new value: no member ended, 32 allowed, nothing kept. 1695 def Scan.start() -> Scan: 1696 Scanning{0n, 32n, Blank{}, Nil{}} 1697 1698 # The scan keeps only the first entry of each key and stops at a 33rd member, 1699 # so this check is not expected to fail: the laws prove it passes for 1700 # normalized values, and the corpus exercises the rest. A failure would be 1701 # reported as too many members. 1702 def Scan.state(entries: List<&2, StateEntry>, valid: Bool, 1703 evidence: {TraceState.is_valid(entries) == valid : Bool}) -> Result<&2, &2, StateError, TraceState>: 1704 match valid: 1705 case True{}: 1706 Done{TraceState{entries, evidence}} 1707 case False{}: 1708 Fail{TooManyMembers{}} 1709 1710 # The state read, once the last member has ended. TraceState.is_valid is 1711 # checked here to build the state's evidence. 1712 def Scan.result(scan: Scan) -> Result<&2, &2, StateError, TraceState>: 1713 match scan: 1714 case Stopped{error}: 1715 Fail{error} 1716 case Scanning{member, room, current, +entries}: 1717 Scan.state(entries, TraceState.is_valid(entries), {==}) 1718 1719 # The last member ends with the value. 1720 def Scan.finish(scan: Scan) -> Result<&2, &2, StateError, TraceState>: 1721 match scan: 1722 case Stopped{error}: 1723 Fail{error} 1724 case Scanning{member, room, current, entries}: 1725 Scan.result(Scan.close(member, room, current, entries)) 1726 1727 # Read the fields only when they fit the budget. 1728 def Scan.within(fits: Maybe<&2, Nat>, fields: List<&2, String>) -> Result<&2, &2, StateError, TraceState>: 1729 match fits: 1730 case None{}: 1731 Fail{StateTooLarge{}} 1732 case Some{left}: 1733 Scan.finish(Scan.fields(fields, Scan.start())) 1734 1735 # Parse repeated tracestate field values, in arrival order, as their 1736 # comma-joined combination (W3C 3.3.2). The combined value, joining commas 1737 # included, must fit the tracestate input budget; a larger one is refused with 1738 # StateTooLarge before any member is read, without measuring the rest. Then: 1739 # empty members are ignored, and so is optional whitespace before a member and 1740 # after its value; every nonempty member must be a valid entry (InvalidEntry) 1741 # and counts toward the 32 allowed (TooManyMembers); the first entry of each 1742 # key is kept. An error discards the whole state; a valid traceparent stays 1743 # valid (spec #1). W3C 3.3: parse tracestate only for a message whose 1744 # traceparent was parsed. 1745 # Laws: fields_join, over_budget, within_budgets, first_wins and the others of 1746 # section 10 of LAWS.bend. 1747 def TraceState.parse_fields(limits: Limits, +fields: List<&2, String>) -> Result<&2, &2, StateError, TraceState>: 1748 Scan.within(Utf8.left_fields(fields, Some{Limits.tracestate_input(limits)}), fields) 1749 1750 # Parse one combined tracestate value; see TraceState.parse_fields. 1751 def TraceState.parse(limits: Limits, text: String) -> Result<&2, &2, StateError, TraceState>: 1752 TraceState.parse_fields(limits, Con{text, Nil{}}) 1753 1754 # The name of a tracestate error; InvalidEntry adds the member number and the 1755 # reason. 1756 def StateError.show(error: StateError) -> String: 1757 match error: 1758 case StateTooLarge{}: 1759 "StateTooLarge" 1760 case TooManyMembers{}: 1761 "TooManyMembers" 1762 case InvalidEntry{member, reason}: 1763 "InvalidEntry " ++ Nat.show(member) ++ " " ++ EntryError.show(reason) 1764 1765 # Tracestate: updates 1766 # =================== 1767 # 1768 # W3C 3.5 lets a participant add, update and delete entries of the state it 1769 # sends. A changed entry moves to the front and the other entries keep their 1770 # order. Spec #1: updating a key of a full state evicts nothing, and adding a 1771 # 33rd key removes the last entry. 1772 1773 # `item` followed by `rest`, unless `skip` is True: one step of a filter. 1774 # Removing a key and listing the dropped keys both use it. 1775 def Entries.unless(-A: Data, skip: Bool, item: A, rest: List<&2, A>) -> List<&2, A>: 1776 match skip: 1777 case True{}: 1778 rest 1779 case False{}: 1780 Con{item, rest} 1781 1782 # The entries without the one whose key is `key`, in order. 1783 def Entries.without(entries: List<&2, StateEntry>, +key: String) -> List<&2, StateEntry>: 1784 match entries: 1785 case Nil{}: 1786 Nil{} 1787 case Con{+entry, rest}: 1788 Entries.unless(StateEntry, String.eq(StateEntry.key_text(entry), key), entry, Entries.without(rest, key)) 1789 1790 # The state of these entries when the check finds them valid, `fallback` 1791 # otherwise. Updates build their entries so that the check passes, which the 1792 # laws prove; `fallback` keeps the function total without an unchecked 1793 # conversion. 1794 def TraceState.from_entries.checked(entries: List<&2, StateEntry>, fallback: TraceState, valid: Bool, 1795 evidence: {TraceState.is_valid(entries) == valid : Bool}) -> TraceState: 1796 match valid: 1797 case True{}: 1798 TraceState{entries, evidence} 1799 case False{}: 1800 fallback 1801 1802 # The state of `entries`, checked, or `fallback` if the check fails. 1803 def TraceState.from_entries(+entries: List<&2, StateEntry>, fallback: TraceState) -> TraceState: 1804 TraceState.from_entries.checked(entries, fallback, TraceState.is_valid(entries), {==}) 1805 1806 # Add or update the entry of `key` (W3C 3.5): it goes to the front with 1807 # `value`, and the other entries follow in their order. At most 31 of them 1808 # stay, so a new key in a full state removes the last entry, while updating a 1809 # key that is present evicts nothing (laws set_entries, update_keeps_all, 1810 # insert_entries and set_get). 1811 def TraceState.set(+state: TraceState, +key: StateKey, value: StateValue) -> TraceState: 1812 TraceState.from_entries(Con{StateEntry{key, value}, 1813 List.take(&2, StateEntry, Entries.without(TraceState.entries(state), StateKey.to_string(key)), 31n)}, state) 1814 1815 # Delete the entry of `key`, if there is one; the other entries keep their 1816 # order (W3C 3.5; laws remove_entries and remove_get). W3C asks participants 1817 # not to delete keys other vendors generated: that breaks correlation in 1818 # their systems. 1819 def TraceState.remove(+state: TraceState, key: StateKey) -> TraceState: 1820 TraceState.from_entries(Entries.without(TraceState.entries(state), StateKey.to_string(key)), state) 1821 1822 # Tracestate: emission 1823 # ==================== 1824 # 1825 # The emitted value is the normalized one of TraceState.format. Its size in 1826 # UTF-8 octets counts each entry's key, equals sign and value and the commas 1827 # between entries (spec #1). Keys and values are ASCII, so an octet is also a 1828 # character, the unit of W3C 3.3.3.1. 1829 1830 # The octets of `key=value` (law entry_size). 1831 def StateEntry.size(entry: StateEntry) -> Nat: 1832 match entry: 1833 case StateEntry{key, value}: 1834 Nat.add(Utf8.length(StateKey.to_string(key)), 1n+Utf8.length(StateValue.to_string(value))) 1835 1836 # The octets of each entry after the first, with its comma. 1837 def Entries.size.rest(entries: List<&2, StateEntry>) -> Nat: 1838 match entries: 1839 case Nil{}: 1840 0n 1841 case Con{entry, rest}: 1842 1n+Nat.add(StateEntry.size(entry), Entries.size.rest(rest)) 1843 1844 # The octets of the entries joined by commas, as Entries.format writes them. 1845 def Entries.size(entries: List<&2, StateEntry>) -> Nat: 1846 match entries: 1847 case Nil{}: 1848 0n 1849 case Con{entry, rest}: 1850 Nat.add(StateEntry.size(entry), Entries.size.rest(rest)) 1851 1852 # The octets of TraceState.format(state) (law state_size). 1853 def TraceState.size(state: TraceState) -> Nat: 1854 Entries.size(TraceState.entries(state)) 1855 1856 # What truncation to the output budget kept, and the keys of the entries it 1857 # dropped, in their original order. Reporting the keys, not the values, tells 1858 # which vendors lost their state without repeating opaque data. 1859 type Truncation is Data: 1860 Truncation{kept: TraceState, dropped: List<&2, StateKey>} 1861 1862 # The state that fits the output budget. 1863 def Truncation.kept(truncation: Truncation) -> TraceState: 1864 match truncation: 1865 case Truncation{kept, dropped}: 1866 kept 1867 1868 # The keys of the entries removed, in their original order; none when the 1869 # state already fitted. 1870 def Truncation.dropped(truncation: Truncation) -> List<&2, StateKey>: 1871 match truncation: 1872 case Truncation{kept, dropped}: 1873 dropped 1874 1875 # Whether the entry is larger than 128 octets. W3C 3.3.3.1 asks to remove 1876 # such entries first. 1877 def StateEntry.is_large(entry: StateEntry) -> Bool: 1878 Nat.is_gt(StateEntry.size(entry), 128n) 1879 1880 # Whether one of the entries is larger than 128 octets. 1881 def Entries.has_large(entries: List<&2, StateEntry>) -> Bool: 1882 match entries: 1883 case Nil{}: 1884 False{} 1885 case Con{entry, rest}: 1886 Bool.or(StateEntry.is_large(entry), Entries.has_large(rest)) 1887 1888 # The entries without the rightmost one larger than 128 octets: an entry 1889 # stays when a large entry follows it. 1890 def Entries.drop_last_large(entries: List<&2, StateEntry>) -> List<&2, StateEntry>: 1891 match entries: 1892 case Nil{}: 1893 Nil{} 1894 case Con{+entry, +rest}: 1895 Bool.pick(List<&2, StateEntry>, Entries.has_large(rest), Con{entry, Entries.drop_last_large(rest)}, 1896 Bool.pick(List<&2, StateEntry>, StateEntry.is_large(entry), rest, Con{entry, rest})) 1897 1898 # The entries without the rightmost one. 1899 def Entries.drop_last(entries: List<&2, StateEntry>) -> List<&2, StateEntry>: 1900 match entries: 1901 case Nil{}: 1902 Nil{} 1903 case Con{entry, +rest}: 1904 Bool.pick(List<&2, StateEntry>, List.is_empty(&2, StateEntry, rest), Nil{}, 1905 Con{entry, Entries.drop_last(rest)}) 1906 1907 # One removal step (spec #1): the rightmost entry larger than 128 octets, or 1908 # the rightmost entry when none is. 1909 def Entries.shrink(+entries: List<&2, StateEntry>) -> List<&2, StateEntry>: 1910 Bool.pick(List<&2, StateEntry>, Entries.has_large(entries), Entries.drop_last_large(entries), 1911 Entries.drop_last(entries)) 1912 1913 # Remove entries one step at a time while they take more than `budget` 1914 # octets, and stop as soon as they fit. `fuel` bounds the steps. One per 1915 # entry suffices: once every entry is removed, the empty list takes 0 octets, 1916 # which fits any budget. 1917 def Entries.truncate(fuel: Nat, +budget: Nat, +entries: List<&2, StateEntry>) -> List<&2, StateEntry>: 1918 match fuel: 1919 case 0n: 1920 entries 1921 case 1n+more: 1922 Bool.pick(List<&2, StateEntry>, Nat.is_le(Entries.size(entries), budget), entries, 1923 Entries.truncate(more, budget, Entries.shrink(entries))) 1924 1925 # The keys of the entries that `kept` lacks, in order. 1926 def Entries.dropped(entries: List<&2, StateEntry>, +kept: List<&2, StateEntry>) -> List<&2, StateKey>: 1927 match entries: 1928 case Nil{}: 1929 Nil{} 1930 case Con{+entry, rest}: 1931 Entries.unless(StateKey, Entries.has_key(kept, StateEntry.key_text(entry)), StateEntry.key(entry), 1932 Entries.dropped(rest, kept)) 1933 1934 # Fit a state to the output budget of `limits` by removing whole entries 1935 # (W3C 3.3.3.1, spec #1): while the value is over the budget, remove the 1936 # rightmost entry larger than 128 octets, or the rightmost entry when none is, 1937 # and stop as soon as it fits. The surviving entries keep their order (laws 1938 # truncate_steps, truncate_fits, truncate_whole, truncate_order and 1939 # truncate_dropped). 1940 def TraceState.truncate(limits: Limits, state: TraceState) -> Truncation: 1941 +entries = TraceState.entries(state) 1942 +kept = Entries.truncate(List.length(&2, StateEntry, entries), Limits.tracestate_output(limits), entries) 1943 Truncation{TraceState.from_entries(kept, TraceState.empty()), Entries.dropped(entries, kept)} 1944 1945 # Outgoing contexts 1946 # ================= 1947 # 1948 # An outgoing context is a local context with the tracestate its participant 1949 # sends with it: the state attached to a local operation (spec #1). Editing 1950 # that state is allowed because the traceparent of a local context 1951 # identifies an operation of this participant: a root, a child, a restart or 1952 # an operation the caller constructed with Context.from_ids. W3C 3.4 and spec 1953 # #1 forbid sending a received traceparent unchanged with an edited or 1954 # truncated tracestate. The types rule out passing a RemoteContext here, but 1955 # not a local context built with the received IDs: Context.from_ids must only 1956 # be given the IDs of the caller's own operation. A received pair is 1957 # forwarded as it came, by Context.forward. 1958 1959 # A local context and the state sent with it. 1960 type OutgoingContext is Data: 1961 OutgoingContext{context: LocalContext, state: TraceState} 1962 1963 # The two header values an outgoing context emits, and the keys of the 1964 # entries that truncation to the output budget dropped, in their original 1965 # order. A context with no state emits the tracestate "", which 1966 # Context.inject does not write. 1967 type Emission is Data: 1968 Emission{traceparent: String, tracestate: String, dropped: List<&2, StateKey>} 1969 1970 # An outgoing context with no state yet, as for a new root. 1971 def OutgoingContext.new(context: LocalContext) -> OutgoingContext: 1972 OutgoingContext{context, TraceState.empty()} 1973 1974 # An outgoing context that sends `state`, such as the state received with the 1975 # parent of a child operation. The caller associates the state with this 1976 # operation, as with Context.from_ids. 1977 def OutgoingContext.with_state(context: LocalContext, state: TraceState) -> OutgoingContext: 1978 OutgoingContext{context, state} 1979 1980 # The local operation. 1981 def OutgoingContext.context(outgoing: OutgoingContext) -> LocalContext: 1982 match outgoing: 1983 case OutgoingContext{context, state}: 1984 context 1985 1986 # The state sent with the operation. 1987 def OutgoingContext.state(outgoing: OutgoingContext) -> TraceState: 1988 match outgoing: 1989 case OutgoingContext{context, state}: 1990 state 1991 1992 # The value of the entry with this key, if there is one. 1993 def OutgoingContext.get(outgoing: OutgoingContext, key: StateKey) -> Maybe<&2, StateValue>: 1994 TraceState.get(OutgoingContext.state(outgoing), key) 1995 1996 # Add or update an entry (see TraceState.set); the context is unchanged (law 1997 # outgoing_set). 1998 def OutgoingContext.set(outgoing: OutgoingContext, key: StateKey, value: StateValue) -> OutgoingContext: 1999 match outgoing: 2000 case OutgoingContext{context, state}: Lines 1-2000 of 3312. More: https://jend.leeeet.dev/read.txt?path=bend-trace-context@0.1.2.0/trace_context.bend&start_line=2001