generation.bend
bend-trace-context@0.1.0.0 · 91 lines · 0 definitions
1# W3C Trace Context Level 2 propagation, with its rules proved as laws. Source: https://github.com/LucasGois1/bend-trace-context
2#
3# Generation on the host's cryptographic source
4# =============================================
5#
6# The first line is the package's description on BendHub, which shows the
7# first line of the file that a release publishes: this file.
8#
9# Generated contexts on the host's cryptographic source: WebCrypto in
10# JavaScript and the operating system's generator natively. They apply the
11# rules of trace_context.bend: four words per trace ID candidate and two per
12# span ID candidate, most significant first, eight candidates per identifier,
13# no all-zero identifier, no reuse of the parent's span ID or of a received
14# trace ID, and an immediate stop at the first source error. There is no time,
15# counter or other fallback. TC.Context.root_with and its siblings take a
16# caller's source instead.
17#
18# The generation machine itself is pure: section 6 of LAWS.bend states its
19# behavior over replayed tapes. This file only connects it, and the native
20# HTTP shortcuts of native_http.bend, to the host source of entropy.bend.
21#
22# Every operation here relies on entropy.bend's foreign effect, so a check of
23# a file that imports this module reports them and answers SOME PROOFS FAIL.
24# No law imports it: the laws state the same operations on a caller's
25# source, which is how PROOF.bend proves them without host code.
26
27import Base
28import bend-trace-context@0.1.0.0/trace_context.bend as TC
29import bend-trace-context@0.1.0.0/native_http.bend as Adapter
30import bend-trace-context@0.1.0.0/entropy.bend as Entropy
31
32# The host source as the machine reads it: each read returns one word result
33# from Entropy.read_u32, and the state is Unit because the host keeps none.
34def Source.host(state: Unit) -> IO(Unit & Result<&1, &1, U32 & String, U32>):
35 IO.bind(Result<&1, &1, U32 & String, U32>, Unit & Result<&1, &1, U32 & String, U32>,
36 Entropy.read_u32(), word => IO.pure(Unit & Result<&1, &1, U32 & String, U32>, (state, word)))
37
38# The host source has no state to hand back.
39def on_host(-A: Type, action: IO(Unit & A)) -> IO(A):
40 IO.bind(Unit & A, A, action, done => IO.pure(A, Pair.snd(Unit, A, done)))
41
42# Start a trace. The trace ID asserts random-trace-id and the root is not
43# sampled, so it is emitted with flags 02.
44def Context.root() -> IO(Result<&2, &2, TC.GenerationError, TC.LocalContext>):
45 on_host(Result<&2, &2, TC.GenerationError, TC.LocalContext>, TC.Context.root_with(~Unit, ~Source.host, Unit{}))
46
47# Continue a remote or local parent with a new operation.
48def Context.child(parent: TC.Parent, sampling: TC.Sampling) -> IO(Result<&2, &2, TC.GenerationError, TC.LocalContext>):
49 on_host(Result<&2, &2, TC.GenerationError, TC.LocalContext>,
50 TC.Context.child_with(~Unit, ~Source.host, Unit{}, parent, sampling))
51
52# Start a new trace instead of continuing a received context.
53def Context.restart(previous: TC.RemoteContext) -> IO(Result<&2, &2, TC.GenerationError, TC.LocalContext>):
54 on_host(Result<&2, &2, TC.GenerationError, TC.LocalContext>,
55 TC.Context.restart_with(~Unit, ~Source.host, Unit{}, previous))
56
57# Give a service its own operation for a received message: a child of the
58# context that extraction keeps, the message's or the base, a root without
59# one, or a new trace in its place at a trust boundary
60# (TC.Context.continue_or_start_with).
61def Context.continue_or_start(+extraction: TC.Extraction, reception: TC.Reception, sampling: TC.Sampling,
62 +policy: TC.FailurePolicy) -> IO(TC.FailurePolicy.result(policy, TC.Service)):
63 on_host(TC.FailurePolicy.result(policy, TC.Service),
64 TC.Context.continue_or_start_with(~Unit, ~Source.host, Unit{}, extraction, reception, sampling, policy))
65
66# Give one message that the service sends a new child of the service's
67# operation, or the fallback when none can be generated
68# (TC.Context.send_with).
69def Context.send(+limits: TC.Limits, service: TC.Service, sampling: TC.Sampling, +policy: TC.FailurePolicy,
70 +carrier: List<&2, TC.Header>) -> IO(TC.FailurePolicy.result(policy, TC.Sent)):
71 on_host(TC.FailurePolicy.result(policy, TC.Sent),
72 TC.Context.send_with(~Unit, ~Source.host, Unit{}, limits, service, sampling, policy, carrier))
73
74# The service's own operation for a received request, from the header map of
75# the request, on the host's cryptographic source: native_http.bend's
76# continue_or_start_with on Source.host. `base` is the context to keep when
77# the request carries no usable traceparent.
78def NativeHttp.continue_or_start(+limits: TC.Limits, headers: Adapter.HeaderMap(), base: Maybe<&2, TC.BaseContext>,
79 reception: TC.Reception, sampling: TC.Sampling, +policy: TC.FailurePolicy) ->
80 IO(TC.FailurePolicy.result(policy, TC.Service)):
81 on_host(TC.FailurePolicy.result(policy, TC.Service),
82 Adapter.continue_or_start_with(~Unit, ~Source.host, Unit{}, limits, headers, base, reception, sampling, policy))
83
84# Give one request that the service sends the context of a new operation, on
85# the host's cryptographic source: native_http.bend's send_with on
86# Source.host, which replaces the context fields of `headers`, the request's
87# own header map.
88def NativeHttp.send(+limits: TC.Limits, service: TC.Service, sampling: TC.Sampling, +policy: TC.FailurePolicy,
89 headers: Adapter.HeaderMap()) -> IO(TC.FailurePolicy.result(policy, Adapter.Outbound)):
90 on_host(TC.FailurePolicy.result(policy, Adapter.Outbound),
91 Adapter.send_with(~Unit, ~Source.host, Unit{}, limits, service, sampling, policy, headers))