law ambient_lower_rest_unchanged

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

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

218law ambient_lower_rest_unchanged:
219  for +k: C.CapsKernel
220  for +c: C.CapCred
221  for +x: U32
222  {C.CapState.with_ambient(C.CapCred.sets(C.Caps.or(A.Caps.ambient_lower(k, c, x), c)), C.CapSet.empty()) == C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}