this is what I came up with on my own attempt, and I may well be doing something fairly silly by the standards of “real” Alloy users.

I haven’t read the whole thing yet, but I think you could simplify things by combining positiveFlags and negativeFlags into a single multirelation:

abstract sig Valence {}
one sig Pos, Neg extends Valence {}

sig Bitfield {
    flags: Valence lone -> Flag
}

To get just the positive flags, write b.flags[Pos]. If you instead do Flag -> lone Valence, you can write b.flags.Pos, which I guess is a bit nicer.

The main reason to do this is it simplifies your other predicates. For example, here’s the new bitfieldSubset:

pred bitfieldSubset[b, b": Bitfield] {
  b.flags in b".flags
}