PROOF.ud.mode: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3306-3324 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=3306&end_line=3324

import Base
import bend-osdev-apparmor@0.1.0.0/profile.bend as PR
import bend-osdev-apparmor@0.1.0.0/eval.bend as V

# no grant, a nonempty request, an enforcing mode: denied
def ud.mode(+cov: Bool, +m: PR.AaMode, +hit: Bool, +cd: Bool, +ok: V.AaDecision, +no: V.AaDecision, +hc: {cov == False{} : Bool}, +h1: {PR.AaMode.enforcing(m) == True{} : Bool}, +hno: {V.AaDecision.allowed(no) == False{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide.mode(m, cov, hit, cd, ok, no)) == False{} : Bool}:
  match cov:
    case True{}:
      b.absurd_tf(Bool, V.AaDecision.allowed(V.AaEval.decide.mode(m, True{}, hit, cd, ok, no)), False{}, hc)
    case False{}:
      match m:
        case PR.AaModeEnforce{}:
          hno
        case PR.AaModePrompt{}:
          hno
        case PR.AaModeKill{}:
          {==}
        case PR.AaModeDefaultAllow{}:
          b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(hit, no, ok)), False{}, h1)
        case PR.AaModeUnconfined{}:
          b.absurd(Bool, True{}, False{}, h1)
        case PR.AaModeComplain{}:
          b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(Bool.and(cd, hit), no, V.AaComplain{})), False{}, h1)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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=b.absurd_tf
  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.mode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaMode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaMode.enforcing