def ex.bound_v

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

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

762def ex.bound_v(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} -> {C.CapSet.subset(C.CapState.permitted(E.CapExec.sets(fl, s)), C.CapSet.union(C.CapState.bounding(s), C.CapState.inheritable(s))) == True{} : Bool}:
763  match fl s:
764    case E.CapExecFlags{True{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
765      h => set.bound_vz(i, fi, fp, b)
766    case E.CapExecFlags{False{}, feff, +fp, +fi} C.CapState{+p, +i, +e, +b, +a}:
767      h => set.bound_va(i, fi, fp, b, a)(h)