law bset_drop_rest_unchanged

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

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

188# dropping from the bounding set changes no other set (in particular, not the
189# inheritable set)
190law bset_drop_rest_unchanged:
191  for +k: C.CapsKernel
192  for +c: C.CapCred
193  for +x: U32
194  {C.CapState.with_bounding(C.CapCred.sets(C.Caps.or(A.Caps.bset_drop(k, c, x), c)), C.CapSet.empty()) == C.CapState.with_bounding(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}