schema_version = 1
law = "zero-product"
variant = "ZeroProduct"
natural_language = "When enabled, a zero result implies at least one zero operand; when disabled, a non-zero counterexample pair must exist."
mathematical_statement = "holds -> forall a b . f(a,b)=0 implies a=0 or b=0; not holds -> exists x y . x!=0 and y!=0 and f(x,y)=0"
preconditions = ["f is binary", "holds declares whether the zero-product property is enforced"]
postcondition = "holds selects either the universal zero-product implication or the existential counterexample obligation"
citation = "SPEC.md#algebraic-laws"
[[variables]]
name = "a"
type = "u32"
role = "input"
[[variables]]
name = "b"
type = "u32"
role = "input"
[[variables]]
name = "x"
type = "u32"
role = "counterexample"
[[variables]]
name = "y"
type = "u32"
role = "counterexample"
[[parameters]]
name = "holds"
type = "bool"
source = "AlgebraicLaw::ZeroProduct.holds"