def bits.covers_meets

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

import Base
import bend-osdev-apparmor@0.1.0.0/perm.bend as P

3099# a request that minus(a, d) covers does not meet d
3100def bits.covers_meets(+a: List<&2, Bool>, +d: List<&2, Bool>, +r: List<&2, Bool>) -> {Bool.and(P.AaBits.covers(P.AaBits.minus(a, d), r), P.AaBits.meets(r, d)) == False{} : Bool}:
3101  match a:
3102    case Nil{}:
3103      match d:
3104        case Nil{}:
3105          match r:
3106            case Nil{}:
3107              {==}
3108            case Con{z, zs}:
3109              b.and_false_r(P.AaBits.covers(Nil{}, Con{z, zs}))
3110        case Con{y, ys}:
3111          match r:
3112            case Nil{}:
3113              {==}
3114            case Con{z, zs}:
3115              match z:
3116                case True{}:
3117                  {==}
3118                case False{}:
3119                  bits.nany_meets(zs, ys)
3120    case Con{x, xs}:
3121      match x:
3122        case True{}:
3123          match d:
3124            case Nil{}:
3125              match r:
3126                case Nil{}:
3127                  {==}
3128                case Con{z, zs}:
3129                  b.and_false_r(P.AaBits.covers(Con{True{}, xs}, Con{z, zs}))
3130            case Con{y, ys}:
3131              match y:
3132                case True{}:
3133                  match r:
3134                    case Nil{}:
3135                      {==}
3136                    case Con{z, zs}:
3137                      match z:
3138                        case True{}:
3139                          {==}
3140                        case False{}:
3141                          bits.covers_meets(xs, ys, zs)
3142                case False{}:
3143                  match r:
3144                    case Nil{}:
3145                      {==}
3146                    case Con{z, zs}:
3147                      match z:
3148                        case True{}:
3149                          bits.covers_meets(xs, ys, zs)
3150                        case False{}:
3151                          bits.covers_meets(xs, ys, zs)
3152        case False{}:
3153          match d:
3154            case Nil{}:
3155              match r:
3156                case Nil{}:
3157                  {==}
3158                case Con{z, zs}:
3159                  b.and_false_r(P.AaBits.covers(Con{False{}, xs}, Con{z, zs}))
3160            case Con{y, ys}:
3161              match y:
3162                case True{}:
3163                  match r:
3164                    case Nil{}:
3165                      {==}
3166                    case Con{z, zs}:
3167                      match z:
3168                        case True{}:
3169                          {==}
3170                        case False{}:
3171                          bits.covers_meets(xs, ys, zs)
3172                case False{}:
3173                  match r:
3174                    case Nil{}:
3175                      {==}
3176                    case Con{z, zs}:
3177                      match z:
3178                        case True{}:
3179                          {==}
3180                        case False{}:
3181                          bits.covers_meets(xs, ys, zs)