role_grant_exceeded: a role’s code reaches a capability its grant leaves out
In an @[endpoints] protocol, role R needs IO.X, ... is that role’s grant:
the body passed to run_R, and everything it calls, may use only those
capabilities, the way main’s parameters bound the whole program. This error
points at a use outside the grant and, when it can, labels each call from the
body to it.
A program that triggers it
mod Main do
needs IO
needs IO.Console
needs IO.FileWrite
needs Session.Live
@[endpoints]
protocol Stream do
role Cons needs IO.Console
Prod -> Cons : Int
end
fn main(c : Cap(IO)) do
let _ = Stream_Run.run_Cons(c, "cons", "secret", Stream_Run.addrs_from_env(),
fn (s, con, st) ->
Stream_Cons.recv_Msg_Prod_Cons_1(s, st, fn (n, st1) ->
let _ = file_write("/tmp/n", int_to_string(n))
Stream_Cons.close(s, st1)))
()
end
end
The body of role Cons writes a file, but Cons is granted only
IO.Console.
The fix
Add the capability to the grant. The body receives one Cap per granted
capability, in the order the grant lists them, between the session capability
and the state, so widening the grant also adds a parameter to the body (and to
any function the body passes its capabilities to):
mod Main do
needs IO
needs IO.Console
needs IO.FileWrite
needs Session.Live
@[endpoints]
protocol Stream do
role Cons needs IO.Console, IO.FileWrite
Prod -> Cons : Int
end
fn main(c : Cap(IO)) do
let _ = Stream_Run.run_Cons(c, "cons", "secret", Stream_Run.addrs_from_env(),
fn (s, con, fw, st) ->
Stream_Cons.recv_Msg_Prod_Cons_1(s, st, fn (n, st1) ->
let _ = file_write("/tmp/n", int_to_string(n))
Stream_Cons.close(s, st1)))
()
end
end
Or remove the use, if the role should not have that authority.
Why the rule exists
A role’s grant is what a deployment of that role is allowed to do. Reading the protocol tells an operator the most each role’s process can do, so a role that writes files must say so there, however deep the write is.
See also: the language reference.