law ambient_raise_rest_unchanged

bend-osdev-caps@0.1.0.0 · LAWS.bend:212

import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C
import bend-osdev-caps@0.1.0.0/adjust.bend as A

212law ambient_raise_rest_unchanged:
213  for +k: C.CapsKernel
214  for +c: C.CapCred
215  for +x: U32
216  {C.CapState.with_ambient(C.CapCred.sets(C.Caps.or(A.Caps.ambient_raise(k, c, x), c)), C.CapSet.empty()) == C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}