cove_schema/hosts.rs
1//! What the host modules the toolchain ships declare about themselves.
2//!
3//! Each `HostApi` implementation in `cove-runtime` answers with the table
4//! named here rather than one of its own, so the description a run enforces,
5//! the one `cove check` checks a call against, and the one `cove trace` reads
6//! out of a recorded file are the same bytes. That is what ADR 0001's
7//! "shared by the compiler, runtime, and CLI" means when it is taken
8//! literally.
9//!
10//! A host outside this workspace declares itself the same way, in its own
11//! crate: nothing here is privileged, and [`SHIPPED`] is only the list of the
12//! modules `cove run` wires up. An embedder hands its own tables to the
13//! checker through [`HostSchemas`], and the ones it does not hand over are
14//! why the boundary checks a call as well as the checker.
15
16use crate::{
17 Effect, FieldSchema, HostType, ModuleSchema, OperationSchema, ResourceSchema, TypeSchema,
18};
19
20/// Every host module `cove run` registers, in the order it registers them.
21///
22/// `cove trace` and `cove replay` read a trace without a host to ask, and
23/// both need what the schema says: which calls the trace recorded are
24/// irreversible, which capability each one needs, and whether a result was
25/// recordable. `cove-sema` needs the same table for the other end of the
26/// call, where an argument still has a span to point at.
27pub static SHIPPED: &[ModuleSchema] = &[
28 CONSOLE, ENV, DOCUMENTS, CLOCK, FILES, PROCESS, DATABASE, HTTP,
29];
30
31/// Every host module the toolchain ships.
32pub fn shipped() -> &'static [ModuleSchema] {
33 SHIPPED
34}
35
36/// The shipped module `name` describes itself with, if there is one.
37///
38/// A name that is not here is not an error: a host may register any module it
39/// likes, and the compiler says only that it cannot check what it cannot see.
40pub fn module(name: &str) -> Option<&'static ModuleSchema> {
41 SHIPPED.iter().find(|module| module.name == name)
42}
43
44/// The host modules one compilation may name: the ones the toolchain ships,
45/// plus any an embedder added.
46///
47/// The shipped tables answer for `cove check` on their own, and did so
48/// alone until this existed: a module `SHIPPED` did not name was `Unknown`
49/// to the checker and checked by the boundary and nothing else. An embedder
50/// is not a lesser kind of host, though — embedding is why `HostApi` is a
51/// trait — so a module it registers should be checked exactly as a shipped
52/// one is, and the only thing missing was a way to hand its table over.
53/// This is that way.
54///
55/// A custom module answers before a shipped one of the same name. An
56/// embedding that replaces `documents` with an implementation of its own
57/// registers a description of its own with it, and the description a run
58/// enforces is the one the checker has to read: a checker reading the
59/// shipped table there would be checking a module nothing is going to run.
60///
61/// A set built with [`HostSchemas::only`] answers for the modules it was
62/// given and no others. That is for an embedding that registers a registry of
63/// its own: a set that still fell back to [`SHIPPED`] would tell such a
64/// program that `files.write` is a checked call, when the run it is about to
65/// make has no `files` module to dispatch it to.
66///
67/// The tables are [`Copy`] and their contents are `'static`, so this owns
68/// only the list. Looking one up hands back the entry itself rather than a
69/// borrow, which is what lets a caller hold a schema while it goes on
70/// reading whatever it asked.
71#[derive(Clone, Debug, PartialEq, Eq)]
72pub struct HostSchemas {
73 /// Only the added modules. The shipped ones are read from [`SHIPPED`]
74 /// rather than copied in, so a default set and a set with one addition
75 /// describe the shipped modules with the same bytes.
76 custom: Vec<ModuleSchema>,
77 /// Whether a name this set was not given falls back to [`SHIPPED`].
78 ///
79 /// True for every set built the ordinary way, because every `cove`
80 /// command runs the shipped hosts. An embedding whose registry is its
81 /// own says otherwise through [`HostSchemas::only`], and then a shipped
82 /// name it did not register is as unknown here as any other.
83 shipped: bool,
84}
85
86impl Default for HostSchemas {
87 fn default() -> HostSchemas {
88 HostSchemas {
89 custom: Vec::new(),
90 shipped: true,
91 }
92 }
93}
94
95impl HostSchemas {
96 /// The shipped modules and nothing else, which is what every command
97 /// that is not an embedding reads.
98 pub fn new() -> HostSchemas {
99 HostSchemas::default()
100 }
101
102 /// Exactly the modules in `schemas`, with no fallback to [`SHIPPED`].
103 ///
104 /// This is what an embedding hands over when its registry is its own
105 /// rather than the shipped one plus additions. `HostRegistry` dispatches
106 /// only what was registered with it, so a checker that still read the
107 /// shipped tables would check `files.write` against a description of a
108 /// module the run has not got and report nothing, leaving the boundary's
109 /// `unknown host module` to be the first mention of it — which is the
110 /// one failure moving schemas to the checker is meant to prevent.
111 ///
112 /// A shipped module the embedding does register is described here the
113 /// same as any other: it is in `schemas` because the registry has it.
114 pub fn only(schemas: impl IntoIterator<Item = ModuleSchema>) -> HostSchemas {
115 let mut set = HostSchemas {
116 custom: Vec::new(),
117 shipped: false,
118 };
119 set.extend(schemas);
120 set
121 }
122
123 /// Whether a name this set was not given is answered from [`SHIPPED`].
124 pub fn reads_shipped(&self) -> bool {
125 self.shipped
126 }
127
128 /// Adds `schema`, taking the set by value so a pipeline can be
129 /// configured in one expression.
130 pub fn with(mut self, schema: ModuleSchema) -> HostSchemas {
131 self.insert(schema);
132 self
133 }
134
135 /// Adds `schema`, replacing any module already added under that name.
136 ///
137 /// Replacing rather than appending keeps one name to one description:
138 /// two tables under one name would make every lookup depend on which was
139 /// added first, which is the drift this crate exists to prevent.
140 pub fn insert(&mut self, schema: ModuleSchema) {
141 match self
142 .custom
143 .iter_mut()
144 .find(|existing| existing.name == schema.name)
145 {
146 Some(existing) => *existing = schema,
147 None => self.custom.push(schema),
148 }
149 }
150
151 /// The module `name` describes itself with, if this set has one.
152 ///
153 /// A name that is not here is not an error: a host may register any
154 /// module it likes, and a checker reading this says only that it cannot
155 /// check what it was not shown.
156 pub fn module(&self, name: &str) -> Option<ModuleSchema> {
157 self.custom
158 .iter()
159 .find(|module| module.name == name)
160 .copied()
161 .or_else(|| self.shipped.then(|| module(name).copied()).flatten())
162 }
163
164 /// Only the modules an embedder added.
165 pub fn custom(&self) -> &[ModuleSchema] {
166 &self.custom
167 }
168
169 /// Every module name this set answers for, added ones first.
170 ///
171 /// A custom module that takes a shipped module's name is named once: it
172 /// is one module, described by whichever table answers for it.
173 pub fn names(&self) -> impl Iterator<Item = &'static str> + '_ {
174 let custom = self.custom.iter().map(|module| module.name);
175 let shipped = SHIPPED
176 .iter()
177 .filter(|_| self.shipped)
178 .map(|module| module.name)
179 .filter(|name| !self.custom.iter().any(|module| module.name == *name));
180 custom.chain(shipped)
181 }
182}
183
184impl Extend<ModuleSchema> for HostSchemas {
185 fn extend<I: IntoIterator<Item = ModuleSchema>>(&mut self, schemas: I) {
186 for schema in schemas {
187 self.insert(schema);
188 }
189 }
190}
191
192impl FromIterator<ModuleSchema> for HostSchemas {
193 fn from_iter<I: IntoIterator<Item = ModuleSchema>>(schemas: I) -> HostSchemas {
194 let mut set = HostSchemas::new();
195 set.extend(schemas);
196 set
197 }
198}
199
200// ------------------------------------------------------------------ console
201
202/// `console`: line-oriented output on two streams.
203///
204/// `println` and `print` write what the program produces; `eprintln` and
205/// `eprint` write what it has to say *about* what it produces — a warning, a
206/// progress line, a summary. With one stream the second kind has to go inside
207/// the first, which is what puts a complaint about a malformed record in the
208/// middle of the records.
209///
210/// Every operation takes a variadic `String`, which is why
211/// `console.println("a", "b")` prints one line of two space-separated parts.
212/// Bytes already handed to the terminal cannot be taken back, so all four are
213/// irreversible writes.
214///
215/// All four are the `console` capability, and the two streams are not two
216/// authorities: a program that may write to the terminal may write to the
217/// terminal, and where a line lands is a question about the program's output
218/// rather than about what it was allowed to do. A host that means to capture
219/// what a run produces and let its complaints through says so by handing
220/// `cove_runtime::host::Console` two different writers, which is where that
221/// choice belongs. ADR 0020 says why.
222pub const CONSOLE: ModuleSchema = ModuleSchema {
223 name: "console",
224 capability: "console",
225 operations: &[
226 OperationSchema {
227 name: "println",
228 params: &[HostType::String],
229 variadic: true,
230 result: HostType::Result(&HostType::Unit, &HostType::Error),
231 capability: "console",
232 effect: Effect::IrreversibleWrite,
233 cancellable: false,
234 recordable: true,
235 result_is_task_safe: true,
236 },
237 OperationSchema {
238 name: "print",
239 params: &[HostType::String],
240 variadic: true,
241 result: HostType::Result(&HostType::Unit, &HostType::Error),
242 capability: "console",
243 effect: Effect::IrreversibleWrite,
244 cancellable: false,
245 recordable: true,
246 result_is_task_safe: true,
247 },
248 OperationSchema {
249 name: "eprintln",
250 params: &[HostType::String],
251 variadic: true,
252 result: HostType::Result(&HostType::Unit, &HostType::Error),
253 capability: "console",
254 effect: Effect::IrreversibleWrite,
255 cancellable: false,
256 recordable: true,
257 result_is_task_safe: true,
258 },
259 OperationSchema {
260 name: "eprint",
261 params: &[HostType::String],
262 variadic: true,
263 result: HostType::Result(&HostType::Unit, &HostType::Error),
264 capability: "console",
265 effect: Effect::IrreversibleWrite,
266 cancellable: false,
267 recordable: true,
268 result_is_task_safe: true,
269 },
270 ],
271 types: &[],
272 resources: &[],
273};
274
275// ---------------------------------------------------------------------- env
276
277/// `env`: read-only access to the environment the host supplies.
278pub const ENV: ModuleSchema = ModuleSchema {
279 name: "env",
280 capability: "env",
281 operations: &[OperationSchema {
282 name: "get",
283 params: &[HostType::String],
284 variadic: false,
285 result: HostType::Option(&HostType::String),
286 capability: "env",
287 effect: Effect::Read,
288 cancellable: false,
289 recordable: true,
290 result_is_task_safe: true,
291 }],
292 types: &[],
293 resources: &[],
294};
295
296// ---------------------------------------------------------------- documents
297
298/// `documents`: a filtered, read-only view over a fixed set of named text
299/// documents.
300pub const DOCUMENTS: ModuleSchema = ModuleSchema {
301 name: "documents",
302 capability: "documents",
303 operations: &[OperationSchema {
304 name: "read",
305 params: &[HostType::String],
306 variadic: false,
307 result: HostType::Result(&HostType::String, &HostType::Error),
308 capability: "documents",
309 effect: Effect::Read,
310 cancellable: false,
311 recordable: true,
312 result_is_task_safe: true,
313 }],
314 types: &[],
315 resources: &[],
316};
317
318// -------------------------------------------------------------------- clock
319
320/// `clock`: monotonic time, waiting, and work bounded or repeated in time.
321///
322/// `timeout` and `every` are both given work rather than data: the first
323/// takes the block it bounds as a trailing closure, and the second takes the
324/// body it repeats. Neither could be written before ADR 0013 added a way back
325/// into Cove, because a host call receives values and had no way to run one.
326/// Both declare that work [`HostType::Any`]: what it produces is the
327/// program's business, not the clock's.
328///
329/// Both are reads. Waiting leaves nothing outside the run different, and
330/// whatever the body does is charged where the body does it.
331pub const CLOCK: ModuleSchema = ModuleSchema {
332 name: "clock",
333 capability: "clock",
334 operations: &[
335 OperationSchema {
336 name: "now",
337 params: &[],
338 variadic: false,
339 result: HostType::Duration,
340 capability: "clock",
341 effect: Effect::Read,
342 cancellable: false,
343 recordable: true,
344 result_is_task_safe: true,
345 },
346 OperationSchema {
347 name: "sleep",
348 params: &[HostType::Duration],
349 variadic: false,
350 result: HostType::Result(&HostType::Unit, &HostType::Error),
351 capability: "clock",
352 // Waiting leaves nothing outside the run different, so it reads
353 // the clock rather than writing anything.
354 effect: Effect::Read,
355 // Nothing has happened yet while a wait is in flight, so
356 // abandoning one is safe. A cancelled task stops at its next
357 // safepoint, which is after the wait it is already inside
358 // returns.
359 cancellable: true,
360 recordable: true,
361 result_is_task_safe: true,
362 },
363 OperationSchema {
364 name: "timeout",
365 params: &[HostType::Duration, HostType::Any],
366 variadic: false,
367 result: HostType::Result(&HostType::Any, &HostType::Error),
368 capability: "clock",
369 effect: Effect::Read,
370 cancellable: true,
371 // What the body did is the body's own business and is recorded
372 // where it happened; what this call answers is whether the bound
373 // held.
374 recordable: true,
375 result_is_task_safe: true,
376 },
377 OperationSchema {
378 name: "every",
379 params: &[HostType::Duration, HostType::Any],
380 variadic: false,
381 result: HostType::Result(&HostType::Unit, &HostType::Error),
382 capability: "clock",
383 effect: Effect::Read,
384 cancellable: true,
385 recordable: true,
386 result_is_task_safe: true,
387 },
388 ],
389 types: &[],
390 resources: &[],
391};
392
393// -------------------------------------------------------------------- files
394
395/// `files`: reading and writing a rooted directory, whole and a line at a
396/// time.
397///
398/// This is the first host whose operations disagree about [`Effect`], and the
399/// disagreement is real: `read`, `exists`, and `list` leave the filesystem
400/// exactly as they found it, while `write` and `delete` destroy whatever was
401/// there before and no host can put it back. Nothing in the language consults
402/// `effect` — `cove impact` is its eventual consumer — but the runtime does:
403/// it counts the calls that changed the world, and `cove run --stats` reports
404/// the count, so a run says how much of what it did cannot be undone.
405///
406/// `read`, `exists`, and `list` are cancellable for the same reason
407/// `clock.sleep` is: abandoning one leaves nothing outside the run different.
408/// `write` and `delete` are not, because a call already in flight may already
409/// have reached the disk.
410///
411/// `open` and `create` issue the two resource kinds, so a program can move a
412/// file that it does not want to hold. Neither is task-safe, and they are the
413/// first shipped resources that are not: a reader is a position in a file and
414/// a writer is a position in another, so two tasks taking turns at one of
415/// them each receive some of the lines and neither receives the file. ADR
416/// 0018 says why that is a mistake to refuse rather than a race to serialize,
417/// and why a reader answers lines rather than bytes.
418pub const FILES: ModuleSchema = ModuleSchema {
419 name: "files",
420 capability: "files",
421 operations: &[
422 OperationSchema {
423 name: "read",
424 params: &[HostType::String],
425 variadic: false,
426 result: HostType::Result(&HostType::String, &HostType::Error),
427 capability: "files",
428 effect: Effect::Read,
429 cancellable: true,
430 recordable: true,
431 result_is_task_safe: true,
432 },
433 OperationSchema {
434 name: "write",
435 params: &[HostType::String, HostType::String],
436 variadic: false,
437 result: HostType::Result(&HostType::Unit, &HostType::Error),
438 capability: "files",
439 effect: Effect::IrreversibleWrite,
440 cancellable: false,
441 recordable: true,
442 result_is_task_safe: true,
443 },
444 OperationSchema {
445 name: "exists",
446 params: &[HostType::String],
447 variadic: false,
448 result: HostType::Bool,
449 capability: "files",
450 effect: Effect::Read,
451 cancellable: true,
452 recordable: true,
453 result_is_task_safe: true,
454 },
455 OperationSchema {
456 name: "list",
457 params: &[HostType::String],
458 variadic: false,
459 result: HostType::Result(&HostType::Array(&HostType::String), &HostType::Error),
460 capability: "files",
461 effect: Effect::Read,
462 cancellable: true,
463 recordable: true,
464 result_is_task_safe: true,
465 },
466 OperationSchema {
467 name: "delete",
468 params: &[HostType::String],
469 variadic: false,
470 result: HostType::Result(&HostType::Unit, &HostType::Error),
471 capability: "files",
472 effect: Effect::IrreversibleWrite,
473 cancellable: false,
474 recordable: true,
475 result_is_task_safe: true,
476 },
477 OperationSchema {
478 name: "open",
479 params: &[HostType::String],
480 variadic: false,
481 result: HostType::Result(&HostType::Named("files.Reader"), &HostType::Error),
482 capability: "files",
483 effect: Effect::Read,
484 cancellable: true,
485 recordable: true,
486 // The reader belongs to the task that opened it, so the handle
487 // this answers with is one no task boundary lets through.
488 result_is_task_safe: false,
489 },
490 OperationSchema {
491 name: "create",
492 params: &[HostType::String],
493 variadic: false,
494 result: HostType::Result(&HostType::Named("files.Writer"), &HostType::Error),
495 capability: "files",
496 // Creating truncates whatever was there, which is the reason
497 // `write` and `delete` are irreversible and not cancellable.
498 effect: Effect::IrreversibleWrite,
499 cancellable: false,
500 recordable: true,
501 result_is_task_safe: false,
502 },
503 ],
504 types: &[],
505 resources: &[
506 ResourceSchema {
507 name: "Reader",
508 task_safe: false,
509 operations: &[
510 OperationSchema {
511 name: "readLine",
512 params: &[],
513 variadic: false,
514 result: HostType::Result(
515 &HostType::Option(&HostType::String),
516 &HostType::Error,
517 ),
518 capability: "files",
519 effect: Effect::Read,
520 cancellable: true,
521 recordable: true,
522 result_is_task_safe: true,
523 },
524 OperationSchema {
525 name: "close",
526 params: &[],
527 variadic: false,
528 result: HostType::Result(&HostType::Unit, &HostType::Error),
529 capability: "files",
530 effect: Effect::ReversibleWrite,
531 cancellable: false,
532 recordable: true,
533 result_is_task_safe: true,
534 },
535 ],
536 },
537 ResourceSchema {
538 name: "Writer",
539 task_safe: false,
540 operations: &[
541 OperationSchema {
542 name: "write",
543 params: &[HostType::String],
544 variadic: false,
545 result: HostType::Result(&HostType::Unit, &HostType::Error),
546 capability: "files",
547 effect: Effect::IrreversibleWrite,
548 cancellable: false,
549 recordable: true,
550 result_is_task_safe: true,
551 },
552 OperationSchema {
553 name: "writeLine",
554 params: &[HostType::String],
555 variadic: false,
556 result: HostType::Result(&HostType::Unit, &HostType::Error),
557 capability: "files",
558 effect: Effect::IrreversibleWrite,
559 cancellable: false,
560 recordable: true,
561 result_is_task_safe: true,
562 },
563 OperationSchema {
564 name: "close",
565 params: &[],
566 variadic: false,
567 result: HostType::Result(&HostType::Unit, &HostType::Error),
568 capability: "files",
569 effect: Effect::ReversibleWrite,
570 cancellable: false,
571 recordable: true,
572 result_is_task_safe: true,
573 },
574 ],
575 },
576 ],
577};
578
579// ------------------------------------------------------------------ process
580
581/// `process`: the run's own arguments, its end, and subprocesses.
582///
583/// `exit` and `run` are irreversible writes: a process that has ended cannot
584/// be brought back, and a subprocess that has run has already done whatever
585/// it does. Neither is cancellable for the same reason.
586///
587/// `exit` is the one shipped operation that is not recordable. Recordability
588/// means the result can be handed back later without calling the host again,
589/// and `exit` has no result worth handing back — a replay that returned
590/// `Unit` in its place would continue running a program that had ended.
591///
592/// `run` is deliberately not a spawn: it starts the subprocess, waits for it,
593/// and answers with what it wrote to standard output.
594pub const PROCESS: ModuleSchema = ModuleSchema {
595 name: "process",
596 capability: "process",
597 operations: &[
598 OperationSchema {
599 name: "args",
600 params: &[],
601 variadic: false,
602 result: HostType::Array(&HostType::String),
603 capability: "process",
604 effect: Effect::Read,
605 cancellable: true,
606 recordable: true,
607 result_is_task_safe: true,
608 },
609 OperationSchema {
610 name: "exit",
611 params: &[HostType::Int],
612 variadic: false,
613 result: HostType::Unit,
614 capability: "process",
615 effect: Effect::IrreversibleWrite,
616 cancellable: false,
617 recordable: false,
618 result_is_task_safe: true,
619 },
620 OperationSchema {
621 name: "run",
622 params: &[HostType::String, HostType::Array(&HostType::String)],
623 variadic: false,
624 result: HostType::Result(&HostType::String, &HostType::Error),
625 capability: "process",
626 effect: Effect::IrreversibleWrite,
627 cancellable: false,
628 recordable: true,
629 result_is_task_safe: true,
630 },
631 ],
632 types: &[],
633 resources: &[],
634};
635
636// ----------------------------------------------------------------- database
637
638/// `database`: querying, and connections a host keeps.
639///
640/// A row is a `String` because the runtime has no way to describe a row's
641/// columns: a typed row would need a host type with fields the boundary
642/// checks, and it checks a declared type's name only. One `Array<String>` of
643/// rows is what a host can honestly hand back today.
644///
645/// `query` reads. A statement that changes stored data would be a separate
646/// operation with a separate [`Effect`], and this module does not ship one:
647/// an `execute` whose only implementation is a fake would be a promise that
648/// data was written somewhere.
649///
650/// The connection is task-safe. What a handle names lives behind the host's
651/// own lock, so two tasks holding the same handle take turns rather than
652/// racing — which is exactly the condition the Language Card puts on a host
653/// resource crossing a task boundary. `examples/callbacks/main.cove` depends
654/// on it: the repository is captured by handlers that run in request tasks.
655pub const DATABASE: ModuleSchema = ModuleSchema {
656 name: "database",
657 capability: "database",
658 operations: &[
659 OperationSchema {
660 name: "query",
661 params: &[HostType::String],
662 variadic: false,
663 result: HostType::Result(&HostType::Array(&HostType::String), &HostType::Error),
664 capability: "database",
665 effect: Effect::Read,
666 cancellable: true,
667 recordable: true,
668 result_is_task_safe: true,
669 },
670 OperationSchema {
671 name: "connect",
672 params: &[HostType::String],
673 variadic: false,
674 result: HostType::Result(&HostType::Named("database.Connection"), &HostType::Error),
675 capability: "database",
676 // Taking a connection is a change the same host can put back,
677 // which is what `close` does.
678 effect: Effect::ReversibleWrite,
679 cancellable: false,
680 // A handle is a name, so a trace records the name and a replay
681 // hands the same one back.
682 recordable: true,
683 result_is_task_safe: true,
684 },
685 ],
686 types: &[],
687 resources: &[ResourceSchema {
688 name: "Connection",
689 task_safe: true,
690 operations: &[
691 OperationSchema {
692 name: "query",
693 params: &[HostType::String],
694 variadic: false,
695 result: HostType::Result(&HostType::Array(&HostType::String), &HostType::Error),
696 capability: "database",
697 effect: Effect::Read,
698 cancellable: true,
699 recordable: true,
700 result_is_task_safe: true,
701 },
702 OperationSchema {
703 name: "close",
704 params: &[],
705 variadic: false,
706 result: HostType::Result(&HostType::Unit, &HostType::Error),
707 capability: "database",
708 effect: Effect::ReversibleWrite,
709 cancellable: false,
710 recordable: true,
711 result_is_task_safe: true,
712 },
713 ],
714 }],
715};
716
717// --------------------------------------------------------------------- http
718
719/// `http`: fetching over the network, and listening on a port.
720///
721/// The four declared types are all ordinary data: a request and a response
722/// are what crossed the wire, a method is one of two names, and a route pairs
723/// them with the callback that answers it. A `handler` is [`HostType::Any`]
724/// because the host never looks inside it — it stores the value and calls it.
725///
726/// `listen` is a reversible write: it takes a port from the machine, and
727/// `close` gives it back. `fetch` reads, since a `GET` is what it sends and
728/// nothing outside the run is different afterwards. `json` touches nothing at
729/// all — it is a constructor the host owns because the host owns the
730/// encoding.
731///
732/// `http.Response` is the type of both halves of this module: it is what a
733/// route's handler answers, what `json` builds, and what `fetch` hands a
734/// client. A client and a server learn the same two facts about a response —
735/// its status and its body — so declaring them twice would have been two
736/// names for one shape, and a program that proxied one to the other would
737/// have had to copy it field by field.
738///
739/// The listener lives behind a lock the host owns, so two tasks may both hold
740/// the handle and take turns accepting: the resource is task-safe, and the
741/// schema is where it says so.
742pub const HTTP: ModuleSchema = ModuleSchema {
743 name: "http",
744 capability: "http",
745 operations: &[
746 OperationSchema {
747 name: "fetch",
748 params: &[HostType::String],
749 variadic: false,
750 // A status the server sent is part of the answer rather than a
751 // reason there was none, so an `Err` here means no response
752 // arrived at all: a URL that will not parse, a connection that
753 // could not be made, or one this host would not hold.
754 result: HostType::Result(&HostType::Named("http.Response"), &HostType::Error),
755 capability: "http",
756 effect: Effect::Read,
757 cancellable: true,
758 recordable: true,
759 result_is_task_safe: true,
760 },
761 OperationSchema {
762 name: "json",
763 params: &[HostType::Int, HostType::Any],
764 variadic: false,
765 result: HostType::Named("http.Response"),
766 capability: "http",
767 effect: Effect::Read,
768 cancellable: false,
769 recordable: true,
770 result_is_task_safe: true,
771 },
772 OperationSchema {
773 name: "listen",
774 params: &[HostType::Int],
775 variadic: false,
776 result: HostType::Result(&HostType::Named("http.Server"), &HostType::Error),
777 capability: "http",
778 effect: Effect::ReversibleWrite,
779 cancellable: false,
780 // A handle is a name, so recording one records the name. A replay
781 // hands the same name back and answers the calls made on it from
782 // the trace as well.
783 recordable: true,
784 result_is_task_safe: true,
785 },
786 ],
787 types: &[
788 TypeSchema {
789 name: "Method",
790 cases: &["Get", "Post"],
791 fields: &[],
792 },
793 TypeSchema {
794 name: "Request",
795 cases: &[],
796 fields: &[
797 FieldSchema {
798 name: "method",
799 ty: HostType::Named("http.Method"),
800 },
801 FieldSchema {
802 name: "path",
803 ty: HostType::String,
804 },
805 FieldSchema {
806 name: "body",
807 ty: HostType::String,
808 },
809 ],
810 },
811 TypeSchema {
812 name: "Response",
813 cases: &[],
814 fields: &[
815 FieldSchema {
816 name: "status",
817 ty: HostType::Int,
818 },
819 FieldSchema {
820 name: "body",
821 ty: HostType::String,
822 },
823 ],
824 },
825 TypeSchema {
826 name: "Route",
827 cases: &[],
828 fields: &[
829 FieldSchema {
830 name: "method",
831 ty: HostType::Named("http.Method"),
832 },
833 FieldSchema {
834 name: "path",
835 ty: HostType::String,
836 },
837 FieldSchema {
838 name: "handler",
839 ty: HostType::Any,
840 },
841 ],
842 },
843 ],
844 resources: &[ResourceSchema {
845 name: "Server",
846 task_safe: true,
847 operations: &[
848 OperationSchema {
849 name: "port",
850 params: &[],
851 variadic: false,
852 result: HostType::Int,
853 capability: "http",
854 effect: Effect::Read,
855 cancellable: false,
856 recordable: true,
857 result_is_task_safe: true,
858 },
859 OperationSchema {
860 name: "handle",
861 params: &[HostType::Array(&HostType::Named("http.Route"))],
862 variadic: false,
863 result: HostType::Result(&HostType::Bool, &HostType::Error),
864 capability: "http",
865 // A response that has reached a client cannot be taken back.
866 effect: Effect::IrreversibleWrite,
867 cancellable: true,
868 // The answer is whether a request arrived, which is a fact
869 // about the run and not about the handler that ran inside it.
870 // Replaying it reproduces the shape of the loop; the handler
871 // runs for real either way, because it is the program's own
872 // code.
873 recordable: true,
874 result_is_task_safe: true,
875 },
876 OperationSchema {
877 name: "close",
878 params: &[],
879 variadic: false,
880 result: HostType::Result(&HostType::Unit, &HostType::Error),
881 capability: "http",
882 effect: Effect::ReversibleWrite,
883 cancellable: false,
884 recordable: true,
885 result_is_task_safe: true,
886 },
887 ],
888 }],
889};
890
891#[cfg(test)]
892mod tests {
893 use super::*;
894
895 /// The registry gates on the module's capability, and each operation
896 /// declares the capability it needs. Nothing today mixes capabilities
897 /// inside one module, and a module whose operations disagreed with it
898 /// would make the grant check and the schema tell different stories.
899 #[test]
900 fn every_operation_declares_its_module_capability() {
901 for module in SHIPPED {
902 for entry in module.operations {
903 assert_eq!(entry.capability, module.capability, "`{}`", module.name);
904 }
905 for resource in module.resources {
906 for entry in resource.operations {
907 assert_eq!(entry.capability, module.capability, "`{}`", module.name);
908 }
909 }
910 }
911 }
912
913 /// Every `Named` type a shipped operation mentions is one a shipped
914 /// module declares. A name nothing declares would be a signature naming a
915 /// type that does not exist, which neither end could check a value
916 /// against.
917 #[test]
918 fn every_declared_type_a_shipped_operation_names_exists() {
919 fn named(ty: &HostType, found: &mut Vec<&'static str>) {
920 match ty {
921 HostType::Named(name) => found.push(name),
922 HostType::Array(inner) | HostType::Set(inner) | HostType::Option(inner) => {
923 named(inner, found)
924 }
925 HostType::Map(key, value) | HostType::Result(key, value) => {
926 named(key, found);
927 named(value, found);
928 }
929 _ => {}
930 }
931 }
932
933 let mut names = Vec::new();
934 for module in SHIPPED {
935 let operations = module
936 .operations
937 .iter()
938 .chain(module.resources.iter().flat_map(|r| r.operations));
939 for entry in operations {
940 for param in entry.params {
941 named(param, &mut names);
942 }
943 named(&entry.result, &mut names);
944 }
945 for declared in module.types {
946 for field in declared.fields {
947 named(&field.ty, &mut names);
948 }
949 }
950 }
951
952 for name in names {
953 let (owner, type_name) = name
954 .split_once('.')
955 .unwrap_or_else(|| panic!("`{name}` is not written qualified"));
956 let owner = module(owner).unwrap_or_else(|| panic!("`{name}` names no shipped module"));
957 assert!(
958 owner.declares_type(type_name),
959 "`{name}` names a type `{}` does not declare",
960 owner.name
961 );
962 }
963 }
964
965 /// Every shipped module declares only types some value could be.
966 ///
967 /// One thing a `HostType` can say is unsatisfiable — a `Set` element or a
968 /// `Map` key that is not one Cove's `MapKey` restriction admits — and
969 /// `ModuleSchema::validate` is what says so. No shipped table declares a
970 /// `Set` or a `Map` today, so this asserts nothing about them yet and is
971 /// the rule the first one that does will be held to.
972 #[test]
973 fn every_shipped_module_declares_a_type_some_value_could_be() {
974 for module in SHIPPED {
975 if let Err(fault) = module.validate() {
976 panic!("`{}`: {fault}", module.name);
977 }
978 }
979 }
980
981 /// A module this workspace does not ship, described by its embedder.
982 const COMPANY: ModuleSchema = ModuleSchema {
983 name: "company",
984 capability: "company",
985 operations: &[OperationSchema {
986 name: "employee",
987 params: &[HostType::String],
988 variadic: false,
989 result: HostType::Result(&HostType::String, &HostType::Error),
990 capability: "company",
991 effect: Effect::Read,
992 cancellable: false,
993 recordable: true,
994 result_is_task_safe: true,
995 }],
996 types: &[],
997 resources: &[],
998 };
999
1000 #[test]
1001 fn a_default_set_answers_for_the_shipped_modules_only() {
1002 let schemas = HostSchemas::new();
1003 assert_eq!(schemas.module("console"), Some(CONSOLE));
1004 assert!(schemas.module("company").is_none());
1005 assert!(schemas.custom().is_empty());
1006 }
1007
1008 #[test]
1009 fn an_added_module_is_answered_for_like_a_shipped_one() {
1010 let schemas = HostSchemas::new().with(COMPANY);
1011 assert_eq!(schemas.module("company"), Some(COMPANY));
1012 assert_eq!(schemas.module("console"), Some(CONSOLE));
1013 assert_eq!(schemas.custom(), [COMPANY]);
1014 }
1015
1016 /// An embedding that replaces a shipped module's implementation replaces
1017 /// its description with it, so the checker reads the table the run will
1018 /// actually enforce rather than the one nothing is going to serve.
1019 #[test]
1020 fn an_added_module_answers_before_a_shipped_one_of_the_same_name() {
1021 const OURS: ModuleSchema = ModuleSchema {
1022 name: "documents",
1023 ..COMPANY
1024 };
1025 let schemas = HostSchemas::new().with(OURS);
1026 assert_eq!(schemas.module("documents"), Some(OURS));
1027 assert_eq!(
1028 schemas.names().filter(|name| *name == "documents").count(),
1029 1
1030 );
1031 }
1032
1033 /// One name means one description, whichever order the tables arrived
1034 /// in: two under one name would make every lookup depend on the order.
1035 #[test]
1036 fn adding_a_module_twice_keeps_the_last_description() {
1037 const LATER: ModuleSchema = ModuleSchema {
1038 capability: "payroll",
1039 ..COMPANY
1040 };
1041 let schemas = HostSchemas::new().with(COMPANY).with(LATER);
1042 assert_eq!(schemas.custom(), [LATER]);
1043 }
1044
1045 /// An embedding whose registry is its own is described by its own
1046 /// tables and nothing else. The shipped fallback is right for a set that
1047 /// adds to the shipped hosts and wrong for one that replaces them: it
1048 /// would report `files.write` as a checked call in a run that has no
1049 /// `files` module to dispatch it to.
1050 #[test]
1051 fn a_set_of_only_an_embedder_s_modules_does_not_answer_for_a_shipped_one() {
1052 let schemas = HostSchemas::only([COMPANY]);
1053 assert_eq!(schemas.module("company"), Some(COMPANY));
1054 assert_eq!(schemas.module("files"), None);
1055 assert!(!schemas.reads_shipped());
1056 let names: Vec<&str> = schemas.names().collect();
1057 assert_eq!(names, ["company"]);
1058 }
1059
1060 /// A shipped module an embedding does register is described here like
1061 /// any other module it registered: it is in the set because the registry
1062 /// has it, not because it is shipped.
1063 #[test]
1064 fn a_shipped_module_an_embedding_registers_is_in_a_set_of_only_its_own() {
1065 let schemas = HostSchemas::only([COMPANY, CONSOLE]);
1066 assert_eq!(schemas.module("console"), Some(CONSOLE));
1067 assert_eq!(schemas.module("env"), None);
1068 }
1069
1070 #[test]
1071 fn every_module_a_set_answers_for_is_named_once() {
1072 let schemas = HostSchemas::new().with(COMPANY);
1073 let names: Vec<&str> = schemas.names().collect();
1074 assert_eq!(names.first(), Some(&"company"));
1075 assert!(names.contains(&"http"));
1076 assert_eq!(names.len(), SHIPPED.len() + 1);
1077 }
1078
1079 /// What `cove trace`, `cove replay`, and `cove check` read instead of a
1080 /// live host.
1081 #[test]
1082 fn the_shipped_schema_names_every_module_a_run_registers() {
1083 let names: Vec<&str> = SHIPPED.iter().map(|module| module.name).collect();
1084 assert_eq!(
1085 names,
1086 [
1087 "console",
1088 "env",
1089 "documents",
1090 "clock",
1091 "files",
1092 "process",
1093 "database",
1094 "http"
1095 ]
1096 );
1097 }
1098}