def ex.eff

bend-osdev-caps@0.1.0.0 · PROOF.bend:720

import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C
import bend-osdev-caps@0.1.0.0/exec.bend as E

720def ex.eff(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.effective(E.CapExec.sets(fl, s)), C.CapState.permitted(E.CapExec.sets(fl, s))) == True{} : Bool}:
721  match fl s:
722    case E.CapExecFlags{True{}, True{}, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
723      set.sub_refl(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), C.CapSet.empty()))
724    case E.CapExecFlags{True{}, False{}, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
725      set.sub_or_r(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), C.CapSet.empty())
726    case E.CapExecFlags{False{}, True{}, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
727      set.sub_refl(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a))
728    case E.CapExecFlags{False{}, False{}, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
729      set.sub_or_r(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a)