def CapBits.subset

bend-osdev-caps@0.1.0.0 · caps.bend:206

import Base

206# every capability in a is in b
207def CapBits.subset(n: Nat, a: Word(n), b: Word(n)) -> Bool:
208  match n:
209    case 0n:
210      True{}
211    case 1n+p:
212      match a b:
213        case WCon{ah, at} WCon{bh, bt}:
214          CapBits.sub.bit(ah, bh, CapBits.subset(p, at, bt))