Module policy_limit 

Policy limits as values (crates/kernel/spec/PolicyLimit.lean §8-73): each type carries one ceiling’s legal domain and the one refusal that says no, so a caller hands over what it observed and cannot spell a second refusal.

The numbers live in consts_policy and the sentences live here. A limit has no public constructor, no getter, no Display and no serde: a caller outside this crate can neither mint a looser limit nor read the figure out to format a sentence of its own. The compile-failure counterexample is tests/ui/forge_policy_limit.rs.

Structs

ClockZonesMax

How many concern zones a clock stamp may carry, the UTC row not among them. Refused rather than dropped: a configured zone that silently stops rendering is a wrong stamp, and a wrong stamp is worse than no stamp.

ImageMaxBytes

How many bytes one picture may carry to a provider. Sized so a base64 body of it stays inside what every provider this city calls accepts (the number’s derivation is on the constant in consts_policy).

ImageQuality

The quality one lossy picture may be encoded at. The legal domain is 0..=max: the maximum is admitted and one more is refused, because a caller that asks for more has asked for something no encoder has, and a clamped answer tells it the picture is better than it is.

ImagesPerTurn

How many pictures one turn may put on a provider request. The legal domain is 0..=max: a turn carrying exactly the limit is sent, and one more picture is refused before any byte leaves for the provider.