Module order 

The partial order ⊑ — “permits no more than”.

This is the relation Law I is stated in, and the whole attenuation check (US-0403) reduces to it: a flow is legal when every child’s grant is ⊑ its parent’s. Getting it wrong makes the security guarantee wrong, so the order is verified as a partial order — reflexive, antisymmetric, transitive — by property tests rather than assumed.

Every comparison is three-valued. An Unknown is a refusal: the compiler rejects rather than assume (US-0206).

Functions

atom_eq

Whether two atoms denote exactly the same permission.

atom_leq

Whether inner permits no more than outer — that is, inner ⊑ outer.

set_eq

Whether two grant sets permit exactly the same thing.

set_leq

Whether inner ⊑ outer for grant sets.

set_lt

Whether inner ⊑ outer and the two are not equal — a strict narrowing.