def dw.mode

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

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

3269# a deny rule meets the request (hit), so the grants cannot cover it
3270def 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}:
3271  match hit:
3272    case False{}:
3273      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.decide.mode(m, cov, False{}, O.AaOptions.complain_deny(opts), ok, no)), False{}, h)
3274    case True{}:
3275      match cov:
3276        case True{}:
3277          b.absurd_tf(Bool, V.AaDecision.allowed(V.AaEval.decide.mode(m, True{}, True{}, O.AaOptions.complain_deny(opts), ok, no)), False{}, e)
3278        case False{}:
3279          match m:
3280            case PR.AaModeEnforce{}:
3281              hno
3282            case PR.AaModePrompt{}:
3283              hno
3284            case PR.AaModeKill{}:
3285              {==}
3286            case PR.AaModeDefaultAllow{}:
3287              hno
3288            case PR.AaModeUnconfined{}:
3289              b.absurd(Bool, True{}, False{}, h1)
3290            case PR.AaModeComplain{}:
3291              match opts:
3292                case O.AaOptions{c, d, v}:
3293                  match c:
3294                    case True{}:
3295                      hno
3296                    case False{}:
3297                      b.absurd(Bool, True{}, False{}, h1)