def file.law

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

import Base
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
import bend-osdev-apparmor@0.1.0.0/rule_file.bend as F

3528def file.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: F.AaFileQuery) -> {V.AaEval.file(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.file(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
3529  match p:
3530    case PR.AaProfile{n, a, f, r0, c, h}:
3531      match r0:
3532        case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
3533          match r:
3534            case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
3535              match q:
3536                case F.AaFileQuery{path, owner, req}:
3537                  file.inc(opts, f, req, f0, f1, F.AaFileQuery{path, owner, req})