def al.rest

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

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

966def al.rest(+v: Bool, +c: C.CapCred, +x: U32) -> {C.CapState.with_ambient(C.CapCred.sets(C.Caps.or(A.CapAdjust.ambient_lower.go(v, c, x), c)), C.CapSet.empty()) == C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}:
967  match v c:
968    case False{} c:
969      {==}
970    case True{} C.CapCred{r, eu, sv, nr, na, C.CapState{+p, +i, +e, +b, +a}}:
971      {==}