PROOF.ud.law: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3390-3399 of bend-osdev-apparmor@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&start_line=3390&end_line=3399

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

def ud.law(+opts: O.AaOptions, +flags: PR.AaFlags, +req: P.AaPerms, +h1: {PR.AaMode.enforcing(PR.AaFlags.mode(flags)) == True{} : Bool}, +h2: {P.AaPerms.any(req) == True{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, Nil{})) == False{} : Bool}:
  match flags:
    case PR.AaFlags{m, fa}:
      match req:
        case P.AaPerms{rb}:
          match rb:
            case Nil{}:
              b.absurd(Bool, V.AaDecision.allowed(V.AaEval.decide(opts, PR.AaFlags{m, fa}, P.AaPerms{Nil{}}, Nil{})), False{}, h2)
            case Con{y, ys}:
              ud.mode(P.AaPerms.covers(P.AaPerms.minus(P.AaPerms.none(), P.AaPerms.none()), P.AaPerms{Con{y, ys}}), m, P.AaPerms.meets(P.AaPerms{Con{y, ys}}, P.AaPerms.none()), O.AaOptions.complain_deny(opts), V.AaEval.choose(Bool.or(fa, P.AaPerms.meets(P.AaPerms{Con{y, ys}}, P.AaPerms.none())), V.AaAudit{}, V.AaAllow{}), V.AaDeny{Bool.or(fa, Bool.not(P.AaPerms.covers(P.AaPerms.minus(P.AaPerms.none(), P.AaPerms.none()), P.AaPerms.minus(P.AaPerms{Con{y, ys}}, P.AaPerms.minus(P.AaPerms.none(), P.AaPerms.none())))))}, Equal.cong(Bool, Bool, x => Bool.not(x), Bool.or(y, P.AaBits.any(ys)), True{}, h2), h1, {==})

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.absurd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ud.mode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaDecision
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaDecision.allowed
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaEval.choose
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaEval.decide
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/options.bend&name=AaOptions
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/options.bend&name=AaOptions.complain_deny
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms.any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms.covers
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms.meets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms.minus
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaPerms.none
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaFlags
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaFlags.mode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaMode.enforcing