def dw.acc

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:3299

import Base
import bend-osdev-apparmor@0.1.0.0/perm.bend as P
import bend-osdev-apparmor@0.1.0.0/options.bend as O
import bend-osdev-apparmor@0.1.0.0/profile.bend as PR
import bend-osdev-apparmor@0.1.0.0/eval.bend as V

3299def dw.acc(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +acc: V.AaAcc, +h1: {V.AaEval.deny_applies(opts, PR.AaFlags.mode(flags)) == True{} : Bool}, +h2: {P.AaPerms.meets(req, V.AaAcc.deny(acc)) == True{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide.acc(opts, flags, req, acc)) == False{} : Bool}:
3300  match flags:
3301    case PR.AaFlags{m, fa}:
3302      match acc:
3303        case V.AaAcc{al, de, au, qu}:
3304          dw.mode(P.AaPerms.meets(req, de), P.AaPerms.covers(P.AaPerms.minus(al, de), req), m, opts, V.AaEval.choose(Bool.or(fa, P.AaPerms.meets(req, au)), V.AaAudit{}, V.AaAllow{}), V.AaDeny{Bool.or(fa, Bool.not(P.AaPerms.covers(P.AaPerms.minus(qu, au), P.AaPerms.minus(req, P.AaPerms.minus(al, de)))))}, h2, pm.covers_meets(al, de, req), h1, {==})