Ship CVLMath relational math library; prefer relational properties over formula mirroring

composer/spec/assets/CVLMathAbstract.spec

@@ -0,0 +1,128 @@
+/*
+ * CVLMathAbstract — relational abstractions of the standard Solidity
+ * mulDiv/WAD helpers, shipped into generated projects by the autoprove
+ * pipeline as certora/specs/summaries/CVLMathAbstract.spec.
+ *
+ * The `*Abstract` functions replace the nonlinear product / quotient with
+ * solver-friendly axioms (zero-preservation, exactness at the denominator,
+ * monotonicity, down/up rounding within 1). Use them as summaries when the
+ * exact formulas make the prover time out and the property only needs
+ * relational facts — do NOT weaken the property instead.
+ *
+ * This file is deliberately standalone (it defines no `*Summary` names), so
+ * it can be imported alongside the exact Math.spec summaries without any
+ * double-definition clash. The exact tier always lives at
+ * certora/specs/summaries/Math.spec — placed there by AutoSetup's summary
+ * closure or, failing that, copied from the same canonical bundled file by
+ * the pipeline.
+ */
+
+definition WAD() returns uint256 = 10^18;
+definition RAY() returns uint256 = 10^27;
+
+/*************************************************************
+ * Relational abstractions
+ *
+ * The `*Abstract` functions read their result from an uninterpreted ghost
+ * mapping instead of computing the exact quotient, so the solver never sees
+ * the nonlinear `x * y / d` term. The ghost is shared by every call, hence
+ * two calls with equal arguments agree — which is what makes cross-call
+ * reasoning (e.g. round-trip inequalities) possible. The quantified axioms
+ * carry the global monotonicity facts; everything argument-specific is
+ * `require`d at the call site.
+ *
+ * These abstractions deliberately UNDER-constrain: they are sound (every real
+ * mulDiv execution satisfies them, up to the overflow caveat noted on each
+ * function) but too weak to prove exact-value properties.
+ *************************************************************/
+
+// Uninterpreted model of floor(x * y / d), indexed as [x][y][d].
+ghost mapping(uint256 => mapping(uint256 => mapping(uint256 => uint256))) mulDivDownGhost {
+    // Weakly monotone in each numerator factor, antitone in the denominator.
+    axiom forall uint256 x1. forall uint256 x2. forall uint256 y. forall uint256 d.
+        x1 <= x2 => mulDivDownGhost[x1][y][d] <= mulDivDownGhost[x2][y][d];
+    axiom forall uint256 x. forall uint256 y1. forall uint256 y2. forall uint256 d.
+        y1 <= y2 => mulDivDownGhost[x][y1][d] <= mulDivDownGhost[x][y2][d];
+    axiom forall uint256 x. forall uint256 y. forall uint256 d1. forall uint256 d2.
+        d1 <= d2 => mulDivDownGhost[x][y][d2] <= mulDivDownGhost[x][y][d1];
+}
+
+// Uninterpreted model of ceil(x * y / d), indexed as [x][y][d]. Its coupling
+// with the floor model (down <= up <= down + 1) is required per call in
+// mulDivUpAbstract below.
+ghost mapping(uint256 => mapping(uint256 => mapping(uint256 => uint256))) mulDivUpGhost {
+    axiom forall uint256 x1. forall uint256 x2. forall uint256 y. forall uint256 d.
+        x1 <= x2 => mulDivUpGhost[x1][y][d] <= mulDivUpGhost[x2][y][d];
+    axiom forall uint256 x. forall uint256 y1. forall uint256 y2. forall uint256 d.
+        y1 <= y2 => mulDivUpGhost[x][y1][d] <= mulDivUpGhost[x][y2][d];
+    axiom forall uint256 x. forall uint256 y. forall uint256 d1. forall uint256 d2.
+        d1 <= d2 => mulDivUpGhost[x][y][d2] <= mulDivUpGhost[x][y][d1];
+}
+
+// Relational model of floor(x * y / d). The result is constrained only by the
+// ghost axioms above and the `require`-based axioms below — NOT the exact
+// quotient — so exact-value assertions will not be provable against it.
+// VACUITY WARNING: because the constraints are imposed with `require`, a rule
+// whose other assumptions contradict them is silently pruned rather than
+// reported (potential vacuity); keep rule_sanity checks on when summarizing
+// with this function. Also unlike the exact mulDivDownSummary, the overflow
+// revert is not modeled: the result is assumed to fit in uint256.
+function mulDivDownAbstract(uint256 x, uint256 y, uint256 d) returns uint256 {
+    if (d == 0) revert();
+    uint256 result = mulDivDownGhost[x][y][d];
+    // Zero-preservation: 0 * y == x * 0 == 0.
+    require (x == 0 || y == 0) => result == 0;
+    // Exactness when one factor equals the denominator: x * d / d == x.
+    require y == d => result == x;
+    require x == d => result == y;
+    // Linear relaxation of result * d <= x * y < (result + 1) * d: comparing
+    // one factor against the denominator bounds the result by the other factor.
+    require y <= d => result <= x;
+    require y >= d => result >= x;
+    require x <= d => result <= y;
+    require x >= d => result >= y;
+    return result;
+}
+
+// Relational model of ceil(x * y / d) = the mulDivUp / round-up family.
+// Same VACUITY WARNING as mulDivDownAbstract: all constraints are
+// `require`-based axioms, so contradicting assumptions prune silently, and
+// the overflow revert is not modeled.
+function mulDivUpAbstract(uint256 x, uint256 y, uint256 d) returns uint256 {
+    if (d == 0) revert();
+    uint256 result = mulDivUpGhost[x][y][d];
+    // Zero-preservation: ceil(0 / d) == 0.
+    require (x == 0 || y == 0) => result == 0;
+    // Exactness when one factor equals the denominator (no remainder to round).
+    require y == d => result == x;
+    require x == d => result == y;
+    // Linear relaxation of (result - 1) * d < x * y <= result * d (see the
+    // floor variant for the reading).
+    require y <= d => result <= x;
+    require y >= d => result >= x;
+    require x <= d => result <= y;
+    require x >= d => result >= y;
+    // Rounding-direction coupling with the floor model: down <= up <= down + 1.
+    require mulDivDownGhost[x][y][d] <= result;
+    require to_mathint(result) <= mulDivDownGhost[x][y][d] + 1;
+    return result;
+}
+
+// WAD convenience wrappers over the relational models (the abstract
+// counterparts of mulWadDownSummary etc.). They inherit the vacuity /
+// no-overflow-revert caveats of the functions they delegate to.
+function mulWadDownAbstract(uint256 x, uint256 y) returns uint256 {
+    return mulDivDownAbstract(x, y, WAD());
+}
+
+function mulWadUpAbstract(uint256 x, uint256 y) returns uint256 {
+    return mulDivUpAbstract(x, y, WAD());
+}
+
+function divWadDownAbstract(uint256 x, uint256 y) returns uint256 {
+    return mulDivDownAbstract(x, WAD(), y);
+}
+
+function divWadUpAbstract(uint256 x, uint256 y) returns uint256 {
+    return mulDivUpAbstract(x, WAD(), y);
+}

composer/spec/assets/__init__.py

@@ -0,0 +1,109 @@
+"""Static CVL assets shipped into generated projects.
+
+The ``.spec`` files in this directory are packaged data (declared under
+``[tool.setuptools.package-data]`` in pyproject.toml) resolved through
+``importlib.resources``, so they work both from a source checkout and from an
+installed wheel. The pipeline copies them into the project's ``certora/specs``
+tree so generated specs can import them like any other summary file.
+
+The CVL math library material comes in two tiers with exactly one source each:
+
+* ``CVLMathAbstract.spec`` (packaged here) — the relational ``*Abstract`` tier
+  plus WAD/RAY definitions. Standalone; always installed.
+* ``Math.spec`` (packaged by certora_autosetup, NOT here) — the exact
+  ``*Summary`` tier. AutoSetup's curated summary closure copies it into
+  ``certora/specs/summaries/`` when a matched summary needs it; when it did
+  not, the install helper copies the same canonical file to the same path.
+  Either way the exact tier exists under one name at one path, so a generated
+  spec's ``import "summaries/Math.spec"`` keeps typechecking across runs
+  (same-path diamond imports dedupe) and there is no second copy to drift.
+"""
+
+from importlib.resources import files
+from pathlib import Path
+
+from certora_autosetup.utils.constants import SUMMARIES_SUBDIR
+
+from composer.spec.gen_types import CVLResource, SUMMARIES_DIR, under_project
+from composer.spec.util import ensure_dir
+
+CVLMATH_ABSTRACT_SPEC_NAME = "CVLMathAbstract.spec"
+MATH_SPEC_NAME = "Math.spec"
+#: Canonical (project-root-relative) install locations, next to the AutoSetup /
+#: custom summaries so imports look uniform to the spec author. The Math.spec
+#: path is the SAME one AutoSetup's copy_summaries_folder uses (it preserves
+#: the bundled layout), which is what makes the single-name scheme work: its
+#: presence signals "the exact tier is already installed".
+MATH_SPEC_PROJECT_PATH = SUMMARIES_DIR / MATH_SPEC_NAME
+CVLMATH_ABSTRACT_PROJECT_PATH = SUMMARIES_DIR / CVLMATH_ABSTRACT_SPEC_NAME
+
+
+def cvlmath_abstract_spec_text() -> str:
+    """The packaged standalone relational-abstraction library source."""
+    return (files(__package__) / CVLMATH_ABSTRACT_SPEC_NAME).read_text()
+
+
+def bundled_math_spec_text() -> str:
+    """The canonical exact-tier ``Math.spec`` source, read from the
+    certora_autosetup package (the single source of the ``*Summary``
+    functions; composer deliberately ships no copy of its own).
+
+    Raises if the bundled file is missing/renamed — loud failure is wanted:
+    the install helper and AutoSetup's summary closure must agree on this
+    file's location for the single-name scheme to hold.
+    """
+    return (
+        files("certora_autosetup")
+        .joinpath("certora", *SUMMARIES_SUBDIR.parts, MATH_SPEC_NAME)
+        .read_text()
+    )
+
+
+def install_cvlmath_resources(project_root: str | Path) -> list[CVLResource]:
+    """Copy the CVL math library into *project_root*'s summaries dir
+    (mirroring how ``setup_summaries`` writes ``custom_summaries.spec``) and
+    return the :class:`CVLResource` entries advertising it to the spec author.
+
+    Must run after the AutoSetup phase: the exact tier (``Math.spec``) is only
+    written — and only advertised as a separate resource — when AutoSetup's
+    summary closure did not already place it in the project. When it did, the
+    ``*Summary`` functions are already reachable through the required
+    AutoSetup summaries import, so a separate advertisement would be
+    redundant. The abstract tier defines no ``*Summary`` names, so it always
+    coexists with whatever summaries AutoSetup emitted and is always
+    installed and advertised.
+    """
+    abstract_dest = under_project(project_root, CVLMATH_ABSTRACT_PROJECT_PATH)
+    ensure_dir(abstract_dest.parent)
+    abstract_dest.write_text(cvlmath_abstract_spec_text())
+    resources = [
+        CVLResource(
+            path=CVLMATH_ABSTRACT_PROJECT_PATH,
+            required=False,
+            sort="import",
+            description=(
+                "Relational math abstractions (mulDiv/WAD *Abstract variants) "
+                "for taming nonlinear arithmetic; constrained via require-based "
+                "axioms (no overflow revert modeled), so contradicting "
+                "assumptions prune paths silently — prefer for relational "
+                "properties, avoid under satisfy"
+            ),
+        ),
+    ]
+
+    math_dest = under_project(project_root, MATH_SPEC_PROJECT_PATH)
+    if not math_dest.exists():
+        math_dest.write_text(bundled_math_spec_text())
+        resources.append(
+            CVLResource(
+                path=MATH_SPEC_PROJECT_PATH,
+                required=False,
+                sort="import",
+                description=(
+                    "Exact math summaries (mulDiv/WAD/sqrt *Summary functions) "
+                    "preserving exact rounding and revert behavior — the same "
+                    "Math.spec AutoSetup ships with its curated summaries"
+                ),
+            )
+        )
+    return resources

composer/spec/source/pipeline.py

@@ -23,6 +23,7 @@
 from composer.ui.autoprove_app import AutoProvePhase
 
 from composer.input.files import Document
+from composer.spec.assets import install_cvlmath_resources
 from composer.spec.context import (
     WorkflowContext, CacheKey, Properties, CVLGeneration,
 )
@@ -167,6 +168,14 @@ async def stream_autosetup() -> tuple[SetupSuccess, list[CVLResource]]:
                 sort="import",
             ),
         ]
+        # Ship the CVL math library into the project (mirroring how
+        # custom_summaries.spec is written by the summaries phase) and offer it
+        # as optional imports for taming nonlinear arithmetic. Must stay after
+        # the AutoSetup await above: the helper always installs the relational
+        # abstract tier, and copies the canonical exact-tier Math.spec (plus a
+        # resource entry for it) only when AutoSetup's summary closure did not
+        # already place it in the project.
+        resources.extend(install_cvlmath_resources(source_input.project_root))
         if sys_desc.erc20_contracts or sys_desc.external_interfaces:
             summary_resource = await run_task(
                 handler_factory,

composer/templates/property_generation_prompt.j2

@@ -107,6 +107,38 @@ within the generated summary, match the callee contract against known implemente
 For those callees, simply dispatch the call to the relevant implementation. For calls "outside" of the prover
 inputs, fall back on a sound model of the external behavior, using e.g., ghosts.
 
+### Math-Heavy Properties
+
+<math_properties>
+When formalizing properties about arithmetic-heavy code (mulDiv, WAD/RAY fixed-point math, share/asset
+conversions), prefer *relational* properties over rules that mirror the implementation's exact formula:
+
+* monotonicity (e.g., depositing more assets never mints fewer shares),
+* bounds (e.g., a fee never exceeds the amount it is charged on),
+* round-trip inequalities (e.g., `withdraw(deposit(x)) <= x`),
+* additivity up to rounding (e.g., `f(a) + f(b) <= f(a + b)` for round-down math),
+* zero-preservation (e.g., converting zero assets yields zero shares).
+
+A rule that just re-computes the implementation's formula in CVL only proves the code matches its own
+source text; the relational forms capture the *intent* (no value creation, rounding favors the protocol)
+and are far easier on the solver.
+
+If the prover *times out* on a property because of exact nonlinear formulas, do NOT weaken or skip the
+property. Instead, summarize the underlying math function (e.g., `mulDiv`) with the relational
+abstractions from the CVLMathAbstract.spec resource (see the resources list, when available): the
+`...Abstract` variants replace the nonlinear formula with solver-friendly axioms (zero-preservation,
+exactness at the denominator, monotonicity, down/up rounding within 1) that suffice to prove relational
+properties. The exact `...Summary` models (faithful rounding and revert behavior) live in the Math.spec
+summaries resource; use those by default and switch to the `...Abstract` variants only on timeout.
+
+Be aware that the `...Abstract` constraints are imposed with `require`-based axioms and do not model the
+overflow revert: a rule whose other assumptions contradict the axioms is silently pruned rather than
+reported (potential vacuity). Prefer them for relational properties, avoid relying on them under
+`satisfy` (a witness drawn from an over-constrained model proves nothing), and treat a SANITY_FAILURE
+that first appears after adopting them as a sign the axioms conflict with your rule's assumptions rather
+than a code bug.
+</math_properties>
+
 ## Step 4
 
 Once all non-skipped properties have been approved by the feedback judge, AND all rules that are not expected

composer/templates/property_judge_prompt.j2

@@ -67,6 +67,10 @@ For example, `x + 1 > x` is always true, and doesn't say anything *meaningful* a
 is *NOT* tautological even if the implementation/design of `calculateInterest` means it always returns a non-zero value. In this case, the assertion provides a valuable
 "check" on the implementation's behavior.
 
+CLARIFICATION: *Relational* properties about arithmetic — monotonicity, bounds, round-trip inequalities
+(e.g. `withdraw(deposit(x)) <= x`), additivity-up-to-rounding, zero-preservation — are meaningful checks on
+the implementation, NOT tautologies; do not reject them for failing to reproduce the implementation's exact formula.
+
 CLARIFICATION: Do **NOT** provide feedback on "brittleness" or "maintainability". Specifications are closely tied to the contract implementation they verify. Specifically:
   - A spec that directly references internal storage layouts, specific function implementations, or internal state transitions is acceptable — that's the nature of formal verification.
   - Don't suggest the spec author "abstract away" from contract internals or make specs "more general" to survive refactors — that's not a meaningful quality axis for CVL specs.

pyproject.toml

@@ -152,6 +152,9 @@ include = ["composer*", "sanity_analyzer*", "analyzer*", "certora_autosetup*"]
 
 [tool.setuptools.package-data]
 composer = ["templates/*.j2", "scripts/init-db.sql"]
+# Static CVL assets (composer/spec/assets/) the pipeline copies into generated
+# projects; resolved via importlib.resources, so they must ship with the wheel.
+"composer.spec.assets" = ["*.spec"]
 # Bundled CVL summaries, spec templates, mocks and conf templates the prover
 # reads directly off disk; ship them with the wheel.
 certora_autosetup = [