def set.lub

bend-osdev-caps@0.1.0.0 · PROOF.bend:682

import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C

682def set.lub(+a: C.CapSet(), +s: C.CapSet(), +p: C.CapSet()) -> {C.CapSet.subset(a, p) == True{} : Bool} -> {C.CapSet.subset(s, p) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.union(a, s), p) == True{} : Bool}:
683  match a s p:
684    case C.CapSetW{U32{+al}, +ah} C.CapSetW{U32{+sl}, +sh} C.CapSetW{U32{+pl}, +ph}:
685      +h0 => +h1 => set.sub_intro(Word.or(32n, al, sl), pl, Word.or(9n, ah, sh), ph)(bits.lub(32n, al, sl, pl)(set.sub_lo(al, pl, ah, ph)(h0))(set.sub_lo(sl, pl, sh, ph)(h1)))(bits.lub(9n, ah, sh, ph)(set.sub_hi(al, pl, ah, ph)(h0))(set.sub_hi(sl, pl, sh, ph)(h1)))