PROOF.bits.covers_meets: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3099-3181 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=3099&end_line=3181

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

# a request that minus(a, d) covers does not meet d
def 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}:
  match a:
    case Nil{}:
      match d:
        case Nil{}:
          match r:
            case Nil{}:
              {==}
            case Con{z, zs}:
              b.and_false_r(P.AaBits.covers(Nil{}, Con{z, zs}))
        case Con{y, ys}:
          match r:
            case Nil{}:
              {==}
            case Con{z, zs}:
              match z:
                case True{}:
                  {==}
                case False{}:
                  bits.nany_meets(zs, ys)
    case Con{x, xs}:
      match x:
        case True{}:
          match d:
            case Nil{}:
              match r:
                case Nil{}:
                  {==}
                case Con{z, zs}:
                  b.and_false_r(P.AaBits.covers(Con{True{}, xs}, Con{z, zs}))
            case Con{y, ys}:
              match y:
                case True{}:
                  match r:
                    case Nil{}:
                      {==}
                    case Con{z, zs}:
                      match z:
                        case True{}:
                          {==}
                        case False{}:
                          bits.covers_meets(xs, ys, zs)
                case False{}:
                  match r:
                    case Nil{}:
                      {==}
                    case Con{z, zs}:
                      match z:
                        case True{}:
                          bits.covers_meets(xs, ys, zs)
                        case False{}:
                          bits.covers_meets(xs, ys, zs)
        case False{}:
          match d:
            case Nil{}:
              match r:
                case Nil{}:
                  {==}
                case Con{z, zs}:
                  b.and_false_r(P.AaBits.covers(Con{False{}, xs}, Con{z, zs}))
            case Con{y, ys}:
              match y:
                case True{}:
                  match r:
                    case Nil{}:
                      {==}
                    case Con{z, zs}:
                      match z:
                        case True{}:
                          {==}
                        case False{}:
                          bits.covers_meets(xs, ys, zs)
                case False{}:
                  match r:
                    case Nil{}:
                      {==}
                    case Con{z, zs}:
                      match z:
                        case True{}:
                          {==}
                        case False{}:
                          bits.covers_meets(xs, ys, zs)

Uses (8):
  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=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.and_false_r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=bits.nany_meets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.covers
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.meets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/perm.bend&name=AaBits.minus