schema_version = 1
law = "bounded"
variant = "Bounded"
natural_language = "For every input accepted by the operation, the result lies inside the inclusive configured bounds."
mathematical_statement = "forall args . lo <= f(args) and f(args) <= hi"
preconditions = ["f is unary or binary", "lo and hi are declared bounds", "lo <= hi"]
postcondition = "lo <= f(args) && f(args) <= hi"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "args"
type = "u32-list"
role = "input tuple"
[[parameters]]
name = "lo"
type = "u32"
source = "AlgebraicLaw::Bounded.lo"
[[parameters]]
name = "hi"
type = "u32"
source = "AlgebraicLaw::Bounded.hi"