is_auto_stubbable

Function is_auto_stubbable 

Source
pub fn is_auto_stubbable(e: &Effect) -> bool
Expand description

Which effect atoms a stub can stand in for.

§21.3: “What is left is the genuinely external: net.out(host), env, external.read/write (store), fs.read/write(path), cap.*, nondet.” Two of that list are handled by the harness rather than by a stub and are excluded here for reasons worth stating:

  • nondet — ids and the clock are supplied deterministically by the harness, because §3.7 already makes them data at the edge. A stub would be a second answer to a solved problem.
  • cap.* — a capability is discharged by the authority chokepoint, and §21.2’s whole claim for when is that it “goes through the real validate, so authorisation is exercised rather than bypassed”. Stubbing a capability would bypass it. An explicit stub cap.x: is still accepted — saying it out loud is the point — but nothing is stubbed automatically.
  • spawn — not on §21.3’s list either, and not external at all: a parallel: scope is the program’s own control flow, and standing in for it would delete the children rather than the boundary they cross. What a test wants stubbed is what a child does.