def cd.mode

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

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

3326# complain mode: allowed unless an applicable deny rule meets the request
3327def 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}:
3328  match m:
3329    case PR.AaModeComplain{}:
3330      match cov:
3331        case True{}:
3332          match hit:
3333            case True{}:
3334              b.absurd_tf(Bool, V.AaDecision.allowed(ok), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), True{})), e)
3335            case False{}:
3336              match opts:
3337                case O.AaOptions{c, d, v}:
3338                  match c:
3339                    case True{}:
3340                      hok
3341                    case False{}:
3342                      hok
3343        case False{}:
3344          match hit:
3345            case True{}:
3346              match opts:
3347                case O.AaOptions{c, d, v}:
3348                  match c:
3349                    case True{}:
3350                      hno
3351                    case False{}:
3352                      {==}
3353            case False{}:
3354              match opts:
3355                case O.AaOptions{c, d, v}:
3356                  match c:
3357                    case True{}:
3358                      {==}
3359                    case False{}:
3360                      {==}
3361    case PR.AaModeEnforce{}:
3362      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(cov, ok, no)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
3363    case PR.AaModePrompt{}:
3364      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(cov, ok, no)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
3365    case PR.AaModeKill{}:
3366      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(cov, ok, V.AaKill{})), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
3367    case PR.AaModeDefaultAllow{}:
3368      b.absurd(Bool, V.AaDecision.allowed(V.AaEval.choose(hit, no, ok)), Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)
3369    case PR.AaModeUnconfined{}:
3370      b.absurd(Bool, True{}, Bool.not(Bool.and(O.AaOptions.complain_deny(opts), hit)), h)