def cap.gof_app

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

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

3558def cap.gof_app(+xs: List<&2, RC.AaCapRule>, +ys: List<&2, RC.AaCapRule>) -> {RC.AaCapRule.grants.of(RC.AaCapRule.append(xs, ys)) == P.AaGrant.append(RC.AaCapRule.grants.of(xs), RC.AaCapRule.grants.of(ys)) : List<&2, P.AaGrant>}:
3559  match xs:
3560    case Nil{}:
3561      {==}
3562    case Con{r, t}:
3563      match r:
3564        case RC.AaCapRule{qu, ks}:
3565          Equal.cong(List<&2, P.AaGrant>, List<&2, P.AaGrant>, x => Con{P.AaGrant.of(qu, P.AaPerms.bit(0n)), x}, RC.AaCapRule.grants.of(RC.AaCapRule.append(t, ys)), P.AaGrant.append(RC.AaCapRule.grants.of(t), RC.AaCapRule.grants.of(ys)), cap.gof_app(t, ys))