beck_core/
secure.rs

1//! §3.5's security properties, as checks rather than as intentions.
2//!
3//! [`docs/03-type-and-effect-system.md`](../../../../../docs/03-type-and-effect-system.md) §3.5:
4//! "Placement-as-type makes vulnerability classes *unrepresentable*." This module is where three of
5//! that table's rows stop being prose:
6//!
7//! | property | mechanism, here |
8//! |---|---|
9//! | secrets cannot reach the browser | [`sendable`] at every tier crossing, and `secret[T]` is not |
10//! | the log holds data, never code or views | [`storable`], checked at compile time |
11//! | authority is one chokepoint | a `cap.*` effect is discharged only inside `decide`'s validator |
12//!
13//! # Two axes, not one
14//!
15//! "Is it stored" and "does it cross" are independent questions, and conflating them is how systems
16//! end up choosing between an incomplete audit trail and a leak. Beck answers them separately:
17//!
18//! | | Sendable | Storable | |
19//! |---|---|---|---|
20//! | ordinary data | ✓ | ✓ | a `Str`, a model of them |
21//! | `Html` | ✓ | ✗ | a patch stream crosses; replay recomputes a view rather than reading it back |
22//! | **`internal[T]`** | ✗ | ✓ | why an account was suspended: recorded forever, never rendered |
23//! | `secret[T]`, a closure | ✗ | ✗ | a token must reach neither the browser nor the log (§3.7 F5) |
24//!
25//! The third row was empty until the question "what if you want a table but not a data object" was
26//! asked directly. Without it, an event that has to record a fact a client must never see forces a
27//! choice between dropping it from the log and trusting that no view renders it.
28//!
29//! The others in that table are checked elsewhere and named in the Phase 2 report: `ingress`/
30//! `durable` being undischargeable on the client is [`crate::place`]; escaping in `html""` is
31//! [`crate::html`]; effect-derived NetworkPolicy and grants are `beck-infra`; the macro phase's
32//! capability restriction is `beck-macro`; and the tamper-evident history is the replay harness.
33//!
34//! # What "crosses a boundary" means concretely
35//!
36//! Not every value in a program crosses. In Phase 2's topology exactly three do, and each is a type
37//! the splitter already names:
38//!
39//! * the **command** type — the browser's entire write surface, client → server;
40//! * the **event** type — appended to the log, and read back by replay;
41//! * the **state** type — the fold's accumulator, which the view consumes and whose rendering the
42//!   client subscribes to.
43//!
44//! So the Sendable check is not a whole-program dataflow analysis; it is three types and the
45//! transitive closure of their fields. That is a much stronger position than it sounds: a secret
46//! cannot reach the browser without being *reachable from* one of those three, and if it is, the
47//! type says so.
48
49use std::collections::{BTreeMap, BTreeSet};
50use std::sync::Arc;
51
52use beck_diag::{Diagnostic, Diagnostics, Span};
53
54use crate::check::Program;
55use crate::core::{CoreKind, Prim};
56use crate::ty::{Effect, Tier, Ty, TyDecl};
57
58/// Why a type may not cross a boundary.
59#[derive(Clone, Debug, PartialEq, Eq)]
60pub struct NotSendable {
61    /// The offending type, by name — `secret[Str]`, or the function type.
62    pub offender: String,
63    /// The field path that reaches it: `State.config.api_key`.
64    pub path: Vec<String>,
65    pub why: &'static str,
66}
67
68impl NotSendable {
69    pub fn flow(&self) -> String {
70        self.path.join(".")
71    }
72}
73
74/// May a value of this type cross a tier boundary? §3.5: "Boundary crossings require `Sendable`;
75/// `secret[T]` isn't."
76pub fn sendable(ty: &Ty, types: &BTreeMap<Arc<str>, TyDecl>) -> Result<(), NotSendable> {
77    check(ty, types, Rule::Sendable)
78}
79
80/// May a value of this type be written to the log?
81///
82/// Strictly stronger than [`sendable`]: a rendered view can cross a boundary — that is what a patch
83/// stream *is* — but it cannot be stored, because replay must reconstruct it rather than read it
84/// back. [`docs/19-phase-1-report.md`](../../../../../docs/19-phase-1-report.md) §19.9 predicted this:
85/// the runtime refusal in `value_to_repr` was "the right thing to have while the proof is missing",
86/// and this is the proof. The refusal stays, now unreachable from a program that compiles.
87pub fn storable(ty: &Ty, types: &BTreeMap<Arc<str>, TyDecl>) -> Result<(), NotSendable> {
88    check(ty, types, Rule::Storable)
89}
90
91#[derive(Clone, Copy, PartialEq, Eq)]
92enum Rule {
93    Sendable,
94    Storable,
95}
96
97fn check(ty: &Ty, types: &BTreeMap<Arc<str>, TyDecl>, rule: Rule) -> Result<(), NotSendable> {
98    fn go(
99        ty: &Ty,
100        types: &BTreeMap<Arc<str>, TyDecl>,
101        rule: Rule,
102        path: &mut Vec<String>,
103        seen: &mut BTreeSet<Arc<str>>,
104    ) -> Result<(), NotSendable> {
105        let fail = |offender: String, why: &'static str, path: &Vec<String>| {
106            Err(NotSendable {
107                offender,
108                path: path.clone(),
109                why,
110            })
111        };
112        match ty {
113            Ty::Var(_) => Ok(()),
114            Ty::Fun(..) => fail(
115                format!("{ty}"),
116                "a function is code, and code does not cross a boundary as data",
117                path,
118            ),
119            Ty::Con(name, args) => {
120                match name.as_ref() {
121                    Ty::SECRET => {
122                        return fail(
123                            format!("{ty}"),
124                            "`secret[T]` is deliberately not Sendable: that is the whole mechanism",
125                            path,
126                        )
127                    }
128                    // The other half of the pair, and the only asymmetric case: `internal[T]` is
129                    // *storable* — that is what it exists for — and never crosses.
130                    Ty::INTERNAL if rule == Rule::Sendable => {
131                        return fail(
132                            format!("{ty}"),
133                            "`internal[T]` is recorded and never shown: it may be written to the \
134                             log and may not cross a boundary",
135                            path,
136                        )
137                    }
138                    Ty::HTML | Ty::ATTR if rule == Rule::Storable => {
139                        return fail(
140                            format!("{ty}"),
141                            "a view is derived from state, so storing one would make replay read \
142                             it back rather than recompute it",
143                            path,
144                        )
145                    }
146                    _ => {}
147                }
148                for (i, a) in args.iter().enumerate() {
149                    path.push(format!("[{i}]"));
150                    go(a, types, rule, path, seen)?;
151                    path.pop();
152                }
153                let Some(decl) = types.get(name.as_ref()) else {
154                    return Ok(());
155                };
156                if !seen.insert(name.clone()) {
157                    // A recursive type: its fields have already been walked.
158                    return Ok(());
159                }
160                let out = match decl {
161                    TyDecl::Model { fields, .. } => {
162                        for (f, t) in fields {
163                            path.push(f.to_string());
164                            go(t, types, rule, path, seen)?;
165                            path.pop();
166                        }
167                        Ok(())
168                    }
169                    TyDecl::Union { variants, .. } => {
170                        for v in variants {
171                            for (f, t) in &v.fields {
172                                path.push(format!("{}.{f}", v.name));
173                                go(t, types, rule, path, seen)?;
174                                path.pop();
175                            }
176                        }
177                        Ok(())
178                    }
179                    TyDecl::Newtype { inner, .. } | TyDecl::Alias { ty: inner, .. } => {
180                        go(inner, types, rule, path, seen)
181                    }
182                };
183                seen.remove(name.as_ref());
184                out
185            }
186        }
187    }
188    let mut path = vec![format!("{ty}")];
189    let mut seen = BTreeSet::new();
190    go(ty, types, rule, &mut path, &mut seen)
191}
192
193/// One step of `beck explain flow <T>`: where a type is reachable, and whether that is allowed.
194#[derive(Clone, Debug)]
195pub struct Reach {
196    pub what: Arc<str>,
197    pub tier: Tier,
198    pub blocked: Option<&'static str>,
199}
200
201/// §4.7's `beck explain flow ApiKey`: every definition whose signature mentions a type, the tier it
202/// runs on, and whether that is a leak.
203pub fn flow(program: &Program, ty_name: &str) -> Vec<Reach> {
204    let mut out = Vec::new();
205    for name in &program.def_order {
206        let Some(d) = program.defs.get(name) else {
207            continue;
208        };
209        let mentions = std::iter::once(&d.ret)
210            .chain(d.params.iter().map(|(_, _, t)| t))
211            .any(|t| mentions_type(t, ty_name, &program.types));
212        if !mentions {
213            continue;
214        }
215        out.push(Reach {
216            what: d.name.clone(),
217            tier: d.tier,
218            blocked: (d.tier == Tier::Client).then_some("a client cannot hold a `secret[T]`"),
219        });
220    }
221    for s in &program.signals {
222        if !mentions_type(&s.ty, ty_name, &program.types) {
223            continue;
224        }
225        out.push(Reach {
226            what: s.name.clone(),
227            tier: s.tier,
228            blocked: (s.tier == Tier::Client).then_some("a client cannot hold a `secret[T]`"),
229        });
230    }
231    out
232}
233
234/// `beck explain flow <T>` — everywhere a type reaches, and everywhere it is refused.
235///
236/// A `String` for the reason [`crate::place::report`] is one: the command line and the playground
237/// ask this question, and a second renderer is a second thing to keep true.
238pub fn flow_report(program: &Program, ty_name: &str) -> Result<String, String> {
239    use std::fmt::Write;
240    let Some(decl) = program.types.get(ty_name) else {
241        return Err(format!("no type `{ty_name}` in this program"));
242    };
243    let is_secret = sendable(&Ty::con(ty_name), &program.types).err();
244    let mut out = String::new();
245    let _ = writeln!(
246        out,
247        "{ty_name} ({}) — {}",
248        match decl {
249            TyDecl::Model { .. } => "model",
250            TyDecl::Union { .. } => "union",
251            TyDecl::Newtype { .. } => "newtype",
252            TyDecl::Alias { .. } => "alias",
253        },
254        match &is_secret {
255            Some(bad) => format!("not Sendable: {} at {}", bad.offender, bad.flow()),
256            None => "Sendable".to_string(),
257        }
258    );
259
260    let reached = flow(program, ty_name);
261    if reached.is_empty() {
262        let _ = writeln!(out, "\n  reaches nothing — no signature mentions it");
263        return Ok(out);
264    }
265    let _ = writeln!(out);
266    for r in &reached {
267        match (&r.blocked, &is_secret) {
268            (Some(why), Some(_)) => {
269                let _ = writeln!(out, "  BLOCKED: {:<18} {:<8} {why}", r.what, r.tier.name());
270            }
271            _ => {
272                let _ = writeln!(out, "  reaches: {:<18} {:<8} ok", r.what, r.tier.name());
273            }
274        }
275    }
276    if is_secret.is_some() {
277        let _ = writeln!(
278            out,
279            "\na crossing requires Sendable, and `secret[T]` is deliberately not \
280             (docs/03 §3.5).\nWhat blocks the leak is the placement, so moving one of \
281             these to the client is the compile error."
282        );
283    }
284    Ok(out)
285}
286
287fn mentions_type(ty: &Ty, name: &str, types: &BTreeMap<Arc<str>, TyDecl>) -> bool {
288    fn go(
289        ty: &Ty,
290        name: &str,
291        types: &BTreeMap<Arc<str>, TyDecl>,
292        seen: &mut BTreeSet<Arc<str>>,
293    ) -> bool {
294        match ty {
295            Ty::Var(_) => false,
296            Ty::Fun(ps, r, _) => {
297                ps.iter().any(|p| go(p, name, types, seen)) || go(r, name, types, seen)
298            }
299            Ty::Con(n, args) => {
300                if n.as_ref() == name {
301                    return true;
302                }
303                if args.iter().any(|a| go(a, name, types, seen)) {
304                    return true;
305                }
306                if !seen.insert(n.clone()) {
307                    return false;
308                }
309                match types.get(n.as_ref()) {
310                    Some(TyDecl::Model { fields, .. }) => {
311                        fields.iter().any(|(_, t)| go(t, name, types, seen))
312                    }
313                    Some(TyDecl::Union { variants, .. }) => variants
314                        .iter()
315                        .any(|v| v.fields.iter().any(|(_, t)| go(t, name, types, seen))),
316                    Some(TyDecl::Newtype { inner, .. }) | Some(TyDecl::Alias { ty: inner, .. }) => {
317                        go(inner, name, types, seen)
318                    }
319                    None => false,
320                }
321            }
322        }
323    }
324    go(ty, name, types, &mut BTreeSet::new())
325}
326
327/// Run §3.5's checks over a placed program.
328///
329/// Split in two because the two halves have different *scopes*, which multi-module compilation
330/// made visible and single-file compilation could not:
331///
332/// * **Boundaries** are a property of one module's types and placements. A module that puts a
333///   secret in something the client subscribes to is wrong on its own terms, and should be told so
334///   without waiting for whatever imports it.
335/// * **Capability discharge** is a property of the *whole program*, because the chokepoint is one
336///   `decide` node and it lives wherever the wiring lives. A policy module holding `cap.session`
337///   is not an error; it is a policy module. It becomes an error only if, once linked, nothing
338///   reaches it from the validator.
339///
340/// Running the second per module reported every correctly-factored authority module as a violation
341/// — which is how this distinction was found.
342pub fn check_security(program: &Program, diags: &mut Diagnostics) {
343    check_boundaries(program, diags);
344    check_capabilities(program, diags);
345}
346
347/// The per-module half.
348pub fn check_boundaries(program: &Program, diags: &mut Diagnostics) {
349    boundaries(program, diags);
350}
351
352/// The whole-program half — run once, after linking.
353pub fn check_capabilities(program: &Program, diags: &mut Diagnostics) {
354    capabilities(program, diags);
355}
356
357/// The three types that cross, and what they are allowed to contain.
358fn boundaries(program: &Program, diags: &mut Diagnostics) {
359    for s in &program.signals {
360        // The durable accumulator, and the events that build it, are what the log holds.
361        if s.effects.contains(&Effect::Durable) {
362            let state = element(&s.ty);
363            if let Err(bad) = storable(&state, &program.types) {
364                reject(
365                    diags,
366                    "B0411",
367                    format!("`{}` is durable, so its state must be storable", s.name),
368                    s.span,
369                    &bad,
370                    "the log is the only description of this program's history; a value it cannot \
371                     read back is a state replay would not reproduce",
372                );
373            }
374        }
375        // Anything the browser subscribes to crosses to the browser.
376        if s.tier == Tier::Client {
377            let carried = element(&s.ty);
378            if let Err(bad) = sendable(&carried, &program.types) {
379                reject(
380                    diags,
381                    "B0410",
382                    format!(
383                        "`{}` runs on the client, so its value must be Sendable",
384                        s.name
385                    ),
386                    s.span,
387                    &bad,
388                    "this value crosses to the browser; §3.5's whole claim is that the compiler \
389                     proves it cannot carry a secret",
390                );
391            }
392        }
393    }
394
395    // The command union is the client's entire write surface (§3.5), so it crosses by definition.
396    if let Some(TyDecl::Union { .. }) = program.types.get("Command") {
397        if let Err(bad) = sendable(&Ty::con("Command"), &program.types) {
398            let span = program
399                .signals
400                .first()
401                .map(|s| s.span)
402                .unwrap_or(Span::NONE);
403            reject(
404                diags,
405                "B0410",
406                "`Command` is what clients send, so it must be Sendable".to_string(),
407                span,
408                &bad,
409                "a command is minted in the browser: a secret in one would be a secret the browser \
410                 already had",
411            );
412        }
413    }
414
415    // A definition placed on the client has its whole signature cross with it.
416    for name in &program.def_order {
417        let Some(d) = program.defs.get(name) else {
418            continue;
419        };
420        if d.tier != Tier::Client {
421            continue;
422        }
423        for t in std::iter::once(&d.ret).chain(d.params.iter().map(|(_, _, t)| t)) {
424            if let Err(bad) = sendable(t, &program.types) {
425                // Deliberately not "anything unsendable": a client-placed definition may perfectly
426                // well take a closure or return `Html`, and those fail `sendable` for reasons that
427                // have nothing to do with a leak. The two that are leaks are named.
428                let kind = if bad.offender.starts_with("secret[") {
429                    "a secret"
430                } else if bad.offender.starts_with("internal[") {
431                    "an internal fact"
432                } else {
433                    continue;
434                };
435                reject(
436                    diags,
437                    "B0410",
438                    format!("`{}` runs on the client and handles {kind}", d.name),
439                    d.span,
440                    &bad,
441                    "`beck explain flow` shows the whole path; the fix is to keep the \
442                     definition on a tier that can hold it",
443                );
444            }
445        }
446    }
447}
448
449fn reject(
450    diags: &mut Diagnostics,
451    code: &'static str,
452    message: String,
453    span: Span,
454    bad: &NotSendable,
455    note: &str,
456) {
457    diags.push(
458        Diagnostic::error(code, message, span)
459            .with_primary_label(format!("`{}` reaches it at `{}`", bad.offender, bad.flow()))
460            .with_note(bad.why)
461            .with_note(note.to_string()),
462    );
463}
464
465fn element(t: &Ty) -> Ty {
466    match t {
467        Ty::Con(n, args)
468            if (n.as_ref() == Ty::SIGNAL || n.as_ref() == Ty::STREAM) && args.len() == 1 =>
469        {
470            args[0].clone()
471        }
472        other => other.clone(),
473    }
474}
475
476/// §3.5: "Only `validate` — the `ingress` consumer, holding `Session` capabilities — turns commands
477/// into events; forgetting an auth check means the `cap.*` effect goes undischarged."
478///
479/// A capability is *held* at exactly one place in a Beck program: the validator `decide` is given,
480/// because that is the only function handed a `Proposal`, and a `Proposal` is the only thing
481/// carrying a `Session`. So a `cap.*` effect anywhere the validator does not reach is a capability
482/// nobody can discharge — a requirement with no holder, which is what a missing auth check looks
483/// like from the type system's side.
484fn capabilities(program: &Program, diags: &mut Diagnostics) {
485    // A program with no `decide` node has no chokepoint, so it is a library rather than an
486    // application, and "this capability has no holder" is not a statement anyone can make about it.
487    // The check runs again over the linked program, which is where the question has an answer.
488    if !has_chokepoint(program) {
489        return;
490    }
491    let authorised = reachable_from_validator(program);
492    for name in &program.def_order {
493        let Some(d) = program.defs.get(name) else {
494            continue;
495        };
496        let caps: Vec<&Effect> = d
497            .effects
498            .iter()
499            .filter(|e| matches!(e, Effect::Cap(_)))
500            .collect();
501        if caps.is_empty() || authorised.contains(name) {
502            continue;
503        }
504        let names: Vec<String> = caps.iter().map(|e| e.name()).collect();
505        diags.push(
506            Diagnostic::error(
507                "B0412",
508                format!("`{name}` requires a capability nothing can discharge"),
509                d.span,
510            )
511            .with_primary_label(format!("needs {{{}}}", names.join(", ")))
512            .with_note(
513                "a `Session` reaches exactly one place in a Beck program: the validator `decide` is \
514                 given, which is the only function handed a `Proposal`. Authority is one chokepoint \
515                 (docs/03 §3.5), so a capability required outside it has no holder",
516            )
517            .with_fix(
518                "call this from `validate` — or, if it genuinely needs no authority, drop the \
519                 `cap.*` from its `uses`",
520            ),
521        );
522    }
523}
524
525/// Does this program have an authority chokepoint at all?
526fn has_chokepoint(program: &Program) -> bool {
527    program.signals.iter().any(|s| {
528        matches!(
529            &s.expr.kind,
530            CoreKind::Prim {
531                op: Prim::Decide,
532                ..
533            }
534        )
535    })
536}
537
538/// Every definition reachable from the validator `decide` was given.
539fn reachable_from_validator(program: &Program) -> BTreeSet<Arc<str>> {
540    let mut roots: Vec<Arc<str>> = Vec::new();
541    for s in &program.signals {
542        if let CoreKind::Prim {
543            op: Prim::Decide,
544            args,
545        } = &s.expr.kind
546        {
547            if let Some(v) = args.get(2) {
548                let mut names = BTreeSet::new();
549                crate::place::mentions(v, &mut names);
550                roots.extend(names);
551            }
552        }
553    }
554    let mut out: BTreeSet<Arc<str>> = BTreeSet::new();
555    while let Some(n) = roots.pop() {
556        if !out.insert(n.clone()) {
557            continue;
558        }
559        if let Some(d) = program.defs.get(&n) {
560            let mut names = BTreeSet::new();
561            crate::place::mentions(&d.body, &mut names);
562            roots.extend(names);
563        }
564    }
565    out
566}
567
568#[cfg(test)]
569mod tests {
570    use super::*;
571    use crate::{check_str, compile_str};
572
573    fn types() -> BTreeMap<Arc<str>, TyDecl> {
574        BTreeMap::from([
575            (
576                Arc::from("Config"),
577                TyDecl::Model {
578                    name: Arc::from("Config"),
579                    params: Vec::new(),
580                    fields: vec![
581                        (Arc::from("host"), Ty::str_()),
582                        (Arc::from("key"), Ty::secret(Ty::str_())),
583                    ],
584                },
585            ),
586            (
587                Arc::from("State"),
588                TyDecl::Model {
589                    name: Arc::from("State"),
590                    params: Vec::new(),
591                    fields: vec![(Arc::from("config"), Ty::con("Config"))],
592                },
593            ),
594        ])
595    }
596
597    #[test]
598    fn a_secret_is_not_sendable_however_deeply_it_is_buried() {
599        let t = types();
600        assert!(sendable(&Ty::str_(), &t).is_ok());
601        let bad = sendable(&Ty::con("State"), &t).expect_err("State reaches a secret");
602        // The path is the diagnostic: §4.7's `beck explain flow` is this string.
603        assert_eq!(bad.flow(), "State.config.key");
604        assert_eq!(bad.offender, "secret[Str]");
605        // …and through a collection, too.
606        assert!(sendable(&Ty::list(Ty::con("Config")), &t).is_err());
607        assert!(sendable(&Ty::map(Ty::str_(), Ty::con("Config")), &t).is_err());
608    }
609
610    #[test]
611    fn a_view_may_cross_a_boundary_but_may_not_be_stored() {
612        // The distinction docs/19 §19.9 could not express: a patch stream is a view crossing a
613        // boundary, and it is fine; a view *in the log* is a state replay would read rather than
614        // recompute.
615        let t = types();
616        assert!(sendable(&Ty::html(), &t).is_ok());
617        assert!(storable(&Ty::html(), &t).is_err());
618    }
619
620    #[test]
621    fn a_recursive_type_terminates() {
622        let t = BTreeMap::from([(
623            Arc::from("Tree"),
624            TyDecl::Model {
625                name: Arc::from("Tree"),
626                params: Vec::new(),
627                fields: vec![(Arc::from("kids"), Ty::list(Ty::con("Tree")))],
628            },
629        )]);
630        assert!(sendable(&Ty::con("Tree"), &t).is_ok());
631    }
632
633    #[test]
634    fn a_state_that_caches_a_view_is_refused_at_compile_time() {
635        // The exact program docs/19 §19.9 named as compiling today and writing `unit` into the log:
636        // "`model State: cached: Html` compiles today, and the encoder would have written `unit`
637        // into a snapshot — silently". It does not compile now.
638        let src = crate::split::tests::TODO.replace(
639            "model State:\n    todos: Map[Id, Todo]",
640            "model State:\n    todos: Map[Id, Todo]\n    cached: Html",
641        );
642        let (_, d, _) = compile_str("t.beck", &src);
643        let codes: Vec<&str> = d.iter().map(|x| x.code).collect();
644        assert!(codes.contains(&"B0411"), "got {codes:?}");
645    }
646
647    #[test]
648    fn a_secret_in_the_command_union_is_refused() {
649        // "Clients can only *propose*": the command union is the browser's entire write surface, so
650        // a secret in one would be a secret the browser already held.
651        let src = crate::split::tests::TODO.replace(
652            "union Command:\n    Add(id: Id, text: Str)",
653            "union Command:\n    Add(id: Id, text: Str, token: secret[Str])",
654        );
655        let (_, d, _) = compile_str("t.beck", &src);
656        let codes: Vec<&str> = d.iter().map(|x| x.code).collect();
657        assert!(codes.contains(&"B0410"), "got {codes:?}");
658    }
659
660    #[test]
661    fn a_capability_required_outside_the_chokepoint_has_no_holder() {
662        let src = crate::split::tests::TODO.replace(
663            "def done_class(t: Todo) -> Str:",
664            "def audit(t: Todo) -> Str uses cap.admin:\n    return t.text\n\n\
665             def done_class(t: Todo) -> Str:",
666        );
667        let (_, d, _) = compile_str("t.beck", &src);
668        let codes: Vec<&str> = d.iter().map(|x| x.code).collect();
669        assert!(codes.contains(&"B0412"), "got {codes:?}");
670    }
671
672    #[test]
673    fn a_capability_required_inside_the_chokepoint_is_exactly_what_it_is_for() {
674        // The same effect, reached from `validate`, is not an error — it is the design. And it
675        // moves the whole authority path to the server, because no other tier discharges `cap.*`.
676        let src = crate::split::tests::TODO
677            .replace(
678                "def owned(s: State, p: Proposal, id: Id, evs: list[Event])",
679                "def admin(p: Proposal) -> Bool uses cap.admin:\n\
680                 \x20   return p.session.actor != \"\"\n\n\
681                 def owned(s: State, p: Proposal, id: Id, evs: list[Event])",
682            )
683            .replace(
684                "    match map_get(s.todos, id):\n        case Some(value):\n            if value.owner != p.session.actor:",
685                "    match map_get(s.todos, id):\n        case Some(value):\n            if not admin(p):",
686            );
687        let (program, d, map) = check_str("t.beck", &src);
688        assert!(!d.has_errors(), "{}", d.render(&map));
689        let mut diags = Diagnostics::new();
690        let solution = crate::place::solve(&program, None);
691        let mut program = program;
692        crate::place::apply(&mut program, &solution);
693        check_security(&program, &mut diags);
694        assert!(
695            !diags.iter().any(|x| x.code == "B0412"),
696            "{}",
697            diags.render(&map)
698        );
699        assert_eq!(
700            program.defs["admin"].tier,
701            Tier::Server,
702            "only the server holds a capability"
703        );
704    }
705
706    #[test]
707    fn explain_flow_names_the_definitions_a_type_reaches() {
708        let src = "\
709model Config:
710    key: secret[Str]
711
712def load() -> Config uses env:
713    return Config(key=secret_env(\"API_KEY\"))
714
715def host(c: Config) -> Str:
716    return \"api.example.com\"
717";
718        let (program, d, map) = check_str("t.beck", src);
719        assert!(!d.has_errors(), "{}", d.render(&map));
720        let reached: Vec<String> = flow(&program, "Config")
721            .into_iter()
722            .map(|r| r.what.to_string())
723            .collect();
724        assert_eq!(reached, ["load", "host"]);
725    }
726}
727
728#[cfg(test)]
729mod quadrants {
730    use super::*;
731
732    /// The four combinations, asserted as a table, because the point of `internal[T]` is that the
733    /// two axes are *independent* — and a table is the only way to see that they are.
734    #[test]
735    fn the_two_axes_are_independent() {
736        let types: BTreeMap<Arc<str>, TyDecl> = BTreeMap::new();
737        let quad = |t: &Ty| (sendable(t, &types).is_ok(), storable(t, &types).is_ok());
738
739        assert_eq!(quad(&Ty::str_()), (true, true), "ordinary data does both");
740        assert_eq!(
741            quad(&Ty::html()),
742            (true, false),
743            "a view crosses as patches and is never read back from the log"
744        );
745        assert_eq!(
746            quad(&Ty::internal(Ty::str_())),
747            (false, true),
748            "`internal[T]` is the quadrant `secret[T]` alone left empty"
749        );
750        assert_eq!(
751            quad(&Ty::secret(Ty::str_())),
752            (false, false),
753            "a token reaches neither the browser nor the log (§3.7 F5)"
754        );
755        assert_eq!(
756            quad(&Ty::fun(vec![Ty::int()], Ty::int())),
757            (false, false),
758            "code is not data in either direction"
759        );
760    }
761
762    #[test]
763    fn an_internal_field_is_found_however_deeply_it_is_buried() {
764        let types = BTreeMap::from([(
765            Arc::from("Suspension"),
766            TyDecl::Model {
767                name: Arc::from("Suspension"),
768                params: Vec::new(),
769                fields: vec![
770                    (Arc::from("at"), Ty::int()),
771                    (Arc::from("reason"), Ty::internal(Ty::str_())),
772                ],
773            },
774        )]);
775        let bad = sendable(&Ty::list(Ty::con("Suspension")), &types)
776            .expect_err("a list of them still cannot cross");
777        assert_eq!(bad.flow(), "list[Suspension].[0].reason");
778        // …and the same type is perfectly storable, which is the whole point.
779        assert!(storable(&Ty::list(Ty::con("Suspension")), &types).is_ok());
780    }
781}