Ergonomic Level Operations

[ssoelvsten]

This might have been an issue previously but it is especially noticeable with the addition of the integrity dimension. Consider a value x at the level {secret}, then to declassify and endorse it to the level of {} one has to do the following:

val x'  = declassify(x, authority, `<; secret>`)
val x'' = endorse(x, authority, `<;>`)

This is not very ergonomic. If there are tons of labels, resp. unknown labels, then I as the programmer don't want to, resp. cannot, write it out. Hence, there is some need for using levelOf and some set operations on levels to derive the third argument in either case.

NOTE: DeclassifyUtil provide a combined Declassification and Endorsement

The declassify-then-endorse pattern might be done so often, we might want to also add helper functions in DeclassifyUtil, similar to the inputPini? Maybe, that file should be renamed to IFCUtil at that point.

[aslanix]

Adding levelOf is not as generally useful as it sounds. For soundness reasons the levelOf 𝓁 must be 𝓁. See for example https://arxiv.org/pdf/2208.13560 and their semantics of the labelOf. Some label meta-operations may come in with extra precision but they need care, there is some preliminary work in https://arxiv.org/pdf/2509.08758.

Perhaps there is some utility in combining that with an extra declassification, I can see how that can work. Declassify-then-endorse (or the other way around) are related to NMIFC, which is something that is currently being investigated/added.