def ud.mode

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:3306

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

3306# no grant, a nonempty request, an enforcing mode: denied
3307def 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}:
3308  match cov:
3309    case True{}:
3310      b.absurd_tf(Bool, V.AaDecision.allowed(V.AaEval.decide.mode(m, True{}, hit, cd, ok, no)), False{}, hc)
3311    case False{}:
3312      match m:
3313        case PR.AaModeEnforce{}:
3314          hno
3315        case PR.AaModePrompt{}:
3316          hno
3317        case PR.AaModeKill{}:
3318          {==}
3319        case PR.AaModeDefaultAllow{}:
3320          b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(hit, no, ok)), False{}, h1)
3321        case PR.AaModeUnconfined{}:
3322          b.absurd(Bool, True{}, False{}, h1)
3323        case PR.AaModeComplain{}:
3324          b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(Bool.and(cd, hit), no, V.AaComplain{})), False{}, h1)