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

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

# a deny rule meets the request (hit), so the grants cannot cover it
def dw.mode(+hit: Bool, +cov: Bool, +m: PR.AaMode, +opts: O.AaOptions, +ok: V.AaDecision, +no: V.AaDecision, +h: {hit == True{} : Bool}, +e: {Bool.and(cov, hit) == False{} : Bool}, +h1: {V.AaEval.deny_applies(opts, m) == True{} : Bool}, +hno: {V.AaDecision.allowed(no) == False{} : Bool}) -> {V.AaDecision.allowed(V.AaEval.decide.mode(m, cov, hit, O.AaOptions.complain_deny(opts), ok, no)) == False{} : Bool}:
  match hit:
    case False{}:
      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.decide.mode(m, cov, False{}, O.AaOptions.complain_deny(opts), ok, no)), False{}, h)
    case True{}:
      match cov:
        case True{}:
          b.absurd_tf(Bool, V.AaDecision.allowed(V.AaEval.decide.mode(m, True{}, True{}, O.AaOptions.complain_deny(opts), ok, no)), False{}, e)
        case False{}:
          match m:
            case PR.AaModeEnforce{}:
              hno
            case PR.AaModePrompt{}:
              hno
            case PR.AaModeKill{}:
              {==}
            case PR.AaModeDefaultAllow{}:
              hno
            case PR.AaModeUnconfined{}:
              b.absurd(Bool, True{}, False{}, h1)
            case PR.AaModeComplain{}:
              match opts:
                case O.AaOptions{c, d, v}:
                  match c:
                    case True{}:
                      hno
                    case False{}:
                      b.absurd(Bool, True{}, False{}, h1)

Uses (11):
  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.decide.mode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaEval.deny_applies
  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/profile.bend&name=AaMode