PROOF.ex.law: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3845-3849 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=3845&end_line=3849

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

def ex.law(+opts: O.AaOptions, +pol: PR.AaPolicy, +name: List<&2, U32>, +owner: Bool, +path: List<&2, U32>, +p: PR.AaProfile, +h1: {PR.AaPolicy.lookup(pol, name) == Some{p} : Maybe<&2, PR.AaProfile>}, +h2: {TR.AaTrans.is_unconfined(PR.AaFlags.mode(PR.AaProfile.flags(p))) == False{} : Bool}, +h3: {V.AaDecision.allowed(V.AaEval.file(opts, p, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)})) == False{} : Bool}) -> {TR.AaExecResult.ok(TR.AaTrans.exec(opts, pol, name, owner, path)) == False{} : Bool}:
  %Equal.sym(Maybe<&2, PR.AaProfile>, PR.AaPolicy.lookup(pol, name), Some{p}, h1) : {TR.AaExecResult.ok(TR.AaTrans.exec.of(_, opts, pol, name, owner, path)) == False{} : Bool}
  %Equal.sym(Bool, TR.AaTrans.is_unconfined(PR.AaFlags.mode(PR.AaProfile.flags(p))), False{}, h2) : {TR.AaExecResult.ok(TR.AaTrans.exec.mode(_, opts, pol, p, name, owner, path)) == False{} : Bool}
  %Equal.sym(Bool, V.AaDecision.allowed(V.AaEval.file(opts, p, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)})), False{}, h3) : {TR.AaExecResult.ok(TR.AaTrans.exec.granted(_, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)}, pol, p, name, path, V.AaEval.file(opts, p, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)}))) == False{} : Bool}
  {==}

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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.file
  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/perm.bend&name=AaPerms.bit
  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=AaPolicy
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaPolicy.lookup
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaProfile
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaProfile.flags
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/rule_file.bend&name=AaFileQuery
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/transitions.bend&name=AaExecResult.ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/transitions.bend&name=AaTrans.exec
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/transitions.bend&name=AaTrans.exec.granted
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/transitions.bend&name=AaTrans.exec.mode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/transitions.bend&name=AaTrans.exec.of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/transitions.bend&name=AaTrans.is_unconfined