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

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

# complain mode: allowed unless an applicable deny rule meets the request
def cd.mode(+m: PR.AaMode, +cov: Bool, +hit: Bool, +opts: O.AaOptions, +ok: V.AaDecision, +no: V.AaDecision, +h: {PR.AaMode.is_complain(m) == True{} : Bool}, +e: {Bool.and(cov, hit) == False{} : Bool}, +hok: {V.AaDecision.allowed(ok) == 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)) == Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)) : Bool}:
  match m:
    case PR.AaModeComplain{}:
      match cov:
        case True{}:
          match hit:
            case True{}:
              b.absurd_tf(Bool, V.AaDecision.allowed(ok), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), True{})), e)
            case False{}:
              match opts:
                case O.AaOptions{c, d, v}:
                  match c:
                    case True{}:
                      hok
                    case False{}:
                      hok
        case False{}:
          match hit:
            case True{}:
              match opts:
                case O.AaOptions{c, d, v}:
                  match c:
                    case True{}:
                      hno
                    case False{}:
                      {==}
            case False{}:
              match opts:
                case O.AaOptions{c, d, v}:
                  match c:
                    case True{}:
                      {==}
                    case False{}:
                      {==}
    case PR.AaModeEnforce{}:
      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(cov, ok, no)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
    case PR.AaModePrompt{}:
      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(cov, ok, no)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
    case PR.AaModeKill{}:
      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(cov, ok, V.AaKill{})), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
    case PR.AaModeDefaultAllow{}:
      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(hit, no, ok)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
    case PR.AaModeUnconfined{}:
      b.absurd(Bool, True{}, Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)

Uses (13):
  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=Base/base.bend&name=Bool.not
  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/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
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaMode.is_complain