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