pub fn is_auto_stubbable(e: &Effect) -> boolExpand 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 forwhenis that it “goes through the realvalidate, so authorisation is exercised rather than bypassed”. Stubbing a capability would bypass it. An explicitstub 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: aparallel: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.