From a5f3927ce87fd623e9e311e293603a98a9162426 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 20:51:17 +0300 Subject: [PATCH 1/5] Ship a CVLMath relational math library into every generated project New packaged asset composer/spec/assets/CVLMath.spec: the proven exact mulDiv/WAD summaries (copied verbatim from the AutoSetup-bundled Math.spec) plus relational mulDivDownAbstract/mulDivUpAbstract variants that model floor/ceil(x*y/d) as ghost mappings constrained by solver-friendly axioms (zero-preservation, exactness at the denominator, monotonicity, down <= up <= down+1), with vacuity-warning headers on the require-based axioms. stream_autosetup() installs it at certora/specs/summaries/CVLMath.spec and registers it as an optional import resource. Prompt guidance: property generation now steers math-heavy properties toward relational forms (monotonicity, bounds, round-trip, additivity-up-to-rounding, zero-preservation) and toward summarizing with the CVLMath abstractions on timeouts instead of weakening properties; the judge's Criteria 1 clarifies that such relational arithmetic properties are not tautologies. Co-Authored-By: Claude Fable 5 --- composer/spec/assets/CVLMath.spec | 205 ++++++++++++++++++ composer/spec/assets/__init__.py | 43 ++++ composer/spec/source/pipeline.py | 5 + .../templates/property_generation_prompt.j2 | 23 ++ composer/templates/property_judge_prompt.j2 | 4 + pyproject.toml | 3 + tests/test_cvlmath_asset.py | 63 ++++++ 7 files changed, 346 insertions(+) create mode 100644 composer/spec/assets/CVLMath.spec create mode 100644 composer/spec/assets/__init__.py create mode 100644 tests/test_cvlmath_asset.py diff --git a/composer/spec/assets/CVLMath.spec b/composer/spec/assets/CVLMath.spec new file mode 100644 index 00000000..1962fb6a --- /dev/null +++ b/composer/spec/assets/CVLMath.spec @@ -0,0 +1,205 @@ +/* + * CVLMath — reusable CVL math library, shipped into generated projects by the + * autoprove pipeline as certora/specs/summaries/CVLMath.spec. + * + * Two tiers of models for the standard Solidity mulDiv/WAD helpers: + * 1. Exact summaries (`*Summary`): faithful models preserving the exact + * rounding and revert behavior. Copied verbatim from the AutoSetup-bundled + * Math.spec library. Use these by default. + * 2. Relational abstractions (`*Abstract`): replace the nonlinear product / + * quotient with solver-friendly axioms (zero-preservation, exactness at + * the denominator, monotonicity, down/up rounding within 1). Use these as + * summaries when the exact formulas make the prover time out and the + * property only needs relational facts — do NOT weaken the property + * instead. + * + * NB: if this project's AutoSetup summaries already pulled in the bundled + * Math.spec (e.g. via an OpenZeppelin Math template), importing this file too + * would define the `*Summary` functions twice and fail typechecking. In that + * case rely on the already-imported exact summaries, and copy just the + * `*Abstract` tier below into your own spec if you need it. + */ + +definition WAD() returns uint256 = 10^18; +definition RAY() returns uint256 = 10^27; + +/************************************************************* + * Tier 1: exact summaries (verbatim from AutoSetup Math.spec) + *************************************************************/ + +function mulDivDownSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 { + mathint result; + if (denominator == 0) revert(); + result = x * y / denominator; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +function mulDivUpSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 { + mathint result; + if (denominator == 0) revert(); + result = (x * y + denominator - 1) / denominator; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +function averageSummary(uint256 a, uint256 b) returns uint256 { + return require_uint256((a+b)/2); +} + +// Exact (real) square root: the result squared equals the argument. This is the +// strongest abstraction and keeps the constraint simple for the solver (no Babylonian +// loop to unroll), but for arguments that are not perfect squares no such `result` +// exists, so the `require` prunes that path (potential vacuity). Use for invariant +// reasoning where sqrt is treated as exact (e.g. constant-product AMM invariants). +function sqrtSummaryPrecise(uint256 x) returns uint256 { + mathint result; + require result >= 0 && result * result == x; + return assert_uint256(result); +} + +// Floor (integer) square root: result == floor(sqrt(x)), matching Solidity's integer +// sqrt. Sound for every argument (always has a solution), at the cost of an extra +// multiplication / strict upper bound for the solver. +function sqrtSummaryDown(uint256 x) returns uint256 { + mathint result; + require result >= 0 && result * result <= x && x < (result + 1) * (result + 1); + return assert_uint256(result); +} + +function mulWadDownSummary(uint256 x, uint256 y) returns uint256 { + mathint result; + result = x * y / 1000000000000000000; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +function mulWadUpSummary(uint256 x, uint256 y) returns uint256 { + mathint result; + result = (x * y + 999999999999999999) / 1000000000000000000; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +function divWadDownSummary(uint256 x, uint256 y) returns uint256 { + mathint result; + if (y == 0) revert(); + result = x * 1000000000000000000 / y; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +function divWadUpSummary(uint256 x, uint256 y) returns uint256 { + mathint result; + if (y == 0) revert(); + result = (x * 1000000000000000000 + y - 1) / y; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +/************************************************************* + * Tier 2: 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 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); +} diff --git a/composer/spec/assets/__init__.py b/composer/spec/assets/__init__.py new file mode 100644 index 00000000..6abfba2f --- /dev/null +++ b/composer/spec/assets/__init__.py @@ -0,0 +1,43 @@ +"""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. +""" + +from importlib.resources import files +from pathlib import Path + +from composer.spec.gen_types import CVLResource, SUMMARIES_DIR, under_project +from composer.spec.util import ensure_dir + +CVLMATH_SPEC_NAME = "CVLMath.spec" +#: Canonical (project-root-relative) install location — next to the AutoSetup / +#: custom summaries so imports look uniform to the spec author. +CVLMATH_PROJECT_PATH = SUMMARIES_DIR / CVLMATH_SPEC_NAME + + +def cvlmath_spec_text() -> str: + """The packaged CVLMath library source.""" + return (files(__package__) / CVLMATH_SPEC_NAME).read_text() + + +def install_cvlmath_resource(project_root: str | Path) -> CVLResource: + """Copy the packaged CVLMath library into *project_root*'s summaries dir + (mirroring how ``setup_summaries`` writes ``custom_summaries.spec``) and + return the :class:`CVLResource` advertising it to the spec author. + """ + dest = under_project(project_root, CVLMATH_PROJECT_PATH) + ensure_dir(dest.parent) + dest.write_text(cvlmath_spec_text()) + return CVLResource( + path=CVLMATH_PROJECT_PATH, + required=False, + sort="import", + description=( + "Reusable math abstractions (mulDiv/WAD): exact summaries and " + "relational Abstract variants for taming nonlinear arithmetic" + ), + ) diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py index 5799f162..628f67de 100644 --- a/composer/spec/source/pipeline.py +++ b/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_resource from composer.spec.context import ( WorkflowContext, CacheKey, Properties, CVLGeneration, ) @@ -167,6 +168,10 @@ async def stream_autosetup() -> tuple[SetupSuccess, list[CVLResource]]: sort="import", ), ] + # Ship the packaged CVLMath library into the project (mirroring how + # custom_summaries.spec is written by the summaries phase) and offer it + # as an optional import for taming nonlinear arithmetic. + resources.append(install_cvlmath_resource(source_input.project_root)) if sys_desc.erc20_contracts or sys_desc.external_interfaces: summary_resource = await run_task( handler_factory, diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index d96585cc..2d1bf63f 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/composer/templates/property_generation_prompt.j2 @@ -107,6 +107,29 @@ 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 + + +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 CVLMath 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. + + ## Step 4 Once all non-skipped properties have been approved by the feedback judge, AND all rules that are not expected diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index 537b2afc..4c90ef9e 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/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. diff --git a/pyproject.toml b/pyproject.toml index 51d14766..7598446e 100644 --- a/pyproject.toml +++ b/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 = [ diff --git a/tests/test_cvlmath_asset.py b/tests/test_cvlmath_asset.py new file mode 100644 index 00000000..18631a91 --- /dev/null +++ b/tests/test_cvlmath_asset.py @@ -0,0 +1,63 @@ +"""Tests for the packaged CVLMath asset and its pipeline resource wiring. + +The asset must be resolvable through ``importlib.resources`` (so it survives +being installed as a wheel, not just run from a source checkout), the install +helper must write the project copy exactly where the pipeline advertises it, +and the shipped CVL must parse with the same syntax checker the authoring +tools use. +""" + +import shutil +import subprocess + +import pytest + +from composer.spec.assets import ( + CVLMATH_PROJECT_PATH, + CVLMATH_SPEC_NAME, + cvlmath_spec_text, + install_cvlmath_resource, +) +from composer.spec.gen_types import SUMMARIES_DIR + + +def test_asset_resolvable_with_both_tiers(): + text = cvlmath_spec_text() + # Spot-check that both tiers ship: exact summaries + relational abstractions. + assert "mulDivDownSummary" in text + assert "mulDivUpSummary" in text + assert "mulDivDownAbstract" in text + assert "mulDivUpAbstract" in text + assert "definition WAD()" in text + assert "definition RAY()" in text + + +def test_install_writes_project_copy_and_builds_resource(tmp_path): + res = install_cvlmath_resource(tmp_path) + # The resource path is canonical (project-root-relative) and optional — + # this is the CVLResource the pipeline appends in stream_autosetup(). + assert res.path == CVLMATH_PROJECT_PATH + assert res.sort == "import" + assert not res.required + written = tmp_path / SUMMARIES_DIR / CVLMATH_SPEC_NAME + assert written.read_text() == cvlmath_spec_text() + + +def test_cvlmath_spec_passes_syntax_check(tmp_path): + """Parse the shipped spec with the same emv.jar checker ``put_cvl_raw`` uses.""" + from composer.certora_env import CertoraEnvironmentError, typechecker_jar + + if shutil.which("java") is None: + pytest.skip("java not on PATH") + try: + jar = typechecker_jar() + except CertoraEnvironmentError as exc: + pytest.skip(f"Typechecker.jar unavailable: {exc}") + spec = tmp_path / CVLMATH_SPEC_NAME + spec.write_text(cvlmath_spec_text()) + res = subprocess.run( + ["java", "-classpath", str(jar), "EntryPointKt", str(spec)], + capture_output=True, + text=True, + ) + assert res.returncode == 0, f"stdout:\n{res.stdout}\nstderr:\n{res.stderr}" From bab822c0bff9d4a66907dd3fd2604132c481f198 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:23:13 +0300 Subject: [PATCH 2/5] Split CVLMath abstract tier into a standalone spec; install conditionally Projects whose AutoSetup curated-summary closure already copied Math.spec (e.g. via the OZ_Math template) would fail CVL typechecking if CVLMath.spec were imported too, since its exact *Summary tier is byte-identical to Math.spec. The relational tier now lives in its own CVLMathAbstract.spec (defining no *Summary names, so it coexists with any summaries), which CVLMath.spec imports. install_cvlmath_resource() always installs the abstract file and only adds + advertises CVLMath.spec when Math.spec is absent from the project's summaries dir; otherwise the resource points at the abstract file alone. Tests cover both install branches, the byte-identical claim against the bundled Math.spec, and emv.jar syntax checks of both files. Co-Authored-By: Claude Fable 5 --- composer/spec/assets/CVLMath.spec | 134 +++------------------- composer/spec/assets/CVLMathAbstract.spec | 127 ++++++++++++++++++++ composer/spec/assets/__init__.py | 52 ++++++++- composer/spec/source/pipeline.py | 5 +- tests/test_cvlmath_asset.py | 94 ++++++++++++--- 5 files changed, 269 insertions(+), 143 deletions(-) create mode 100644 composer/spec/assets/CVLMathAbstract.spec diff --git a/composer/spec/assets/CVLMath.spec b/composer/spec/assets/CVLMath.spec index 1962fb6a..b3526015 100644 --- a/composer/spec/assets/CVLMath.spec +++ b/composer/spec/assets/CVLMath.spec @@ -3,25 +3,26 @@ * autoprove pipeline as certora/specs/summaries/CVLMath.spec. * * Two tiers of models for the standard Solidity mulDiv/WAD helpers: - * 1. Exact summaries (`*Summary`): faithful models preserving the exact - * rounding and revert behavior. Copied verbatim from the AutoSetup-bundled - * Math.spec library. Use these by default. - * 2. Relational abstractions (`*Abstract`): replace the nonlinear product / - * quotient with solver-friendly axioms (zero-preservation, exactness at - * the denominator, monotonicity, down/up rounding within 1). Use these as + * 1. Exact summaries (`*Summary`, defined below): faithful models preserving + * the exact rounding and revert behavior. Copied verbatim from the + * AutoSetup-bundled Math.spec library. Use these by default. + * 2. Relational abstractions (`*Abstract`, pulled in from the imported + * CVLMathAbstract.spec): replace the nonlinear product / quotient with + * solver-friendly axioms (zero-preservation, exactness at the + * denominator, monotonicity, down/up rounding within 1). Use these as * summaries when the exact formulas make the prover time out and the * property only needs relational facts — do NOT weaken the property * instead. * - * NB: if this project's AutoSetup summaries already pulled in the bundled - * Math.spec (e.g. via an OpenZeppelin Math template), importing this file too - * would define the `*Summary` functions twice and fail typechecking. In that - * case rely on the already-imported exact summaries, and copy just the - * `*Abstract` tier below into your own spec if you need it. + * NB: because Tier 1 is byte-identical to the AutoSetup-bundled Math.spec, + * importing both would define the `*Summary` functions twice and fail + * typechecking. The pipeline therefore only installs this file when the + * project's AutoSetup summaries did NOT already pull in Math.spec; otherwise + * it installs CVLMathAbstract.spec alone. Keep that in mind if you copy this + * file into a project by hand. */ -definition WAD() returns uint256 = 10^18; -definition RAY() returns uint256 = 10^27; +import "CVLMathAbstract.spec"; /************************************************************* * Tier 1: exact summaries (verbatim from AutoSetup Math.spec) @@ -96,110 +97,3 @@ function divWadUpSummary(uint256 x, uint256 y) returns uint256 { if (result >= 2^256) revert(); return assert_uint256(result); } - -/************************************************************* - * Tier 2: 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 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); -} diff --git a/composer/spec/assets/CVLMathAbstract.spec b/composer/spec/assets/CVLMathAbstract.spec new file mode 100644 index 00000000..623b4d87 --- /dev/null +++ b/composer/spec/assets/CVLMathAbstract.spec @@ -0,0 +1,127 @@ +/* + * 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 AutoSetup-bundled Math.spec exact + * summaries without any double-definition clash. Projects whose AutoSetup + * summaries did NOT pull in Math.spec get the exact tier too, via the + * sibling CVLMath.spec which imports this file. + */ + +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); +} diff --git a/composer/spec/assets/__init__.py b/composer/spec/assets/__init__.py index 6abfba2f..4353932d 100644 --- a/composer/spec/assets/__init__.py +++ b/composer/spec/assets/__init__.py @@ -5,6 +5,17 @@ ``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 CVLMath library ships as two files so the exact tier can be dropped when +it would clash: + +* ``CVLMathAbstract.spec`` — the relational ``*Abstract`` tier plus WAD/RAY. + Standalone; always installed. +* ``CVLMath.spec`` — the exact ``*Summary`` tier (byte-identical to the + AutoSetup-bundled Math.spec) importing the abstract file. Installed only + when AutoSetup did NOT already copy Math.spec into the project, since + importing both would define the ``*Summary`` functions twice and fail CVL + typechecking. """ from importlib.resources import files @@ -14,23 +25,58 @@ from composer.spec.util import ensure_dir CVLMATH_SPEC_NAME = "CVLMath.spec" -#: Canonical (project-root-relative) install location — next to the AutoSetup / +CVLMATH_ABSTRACT_SPEC_NAME = "CVLMathAbstract.spec" +#: Where the AutoSetup-bundled exact Math.spec lands when the curated summary +#: closure pulls it in (copy_summaries_folder preserves the bundled layout). +#: Its presence is the "exact tier already imported" signal. +AUTOSETUP_MATH_SPEC_PATH = SUMMARIES_DIR / "Math.spec" +#: Canonical (project-root-relative) install locations — next to the AutoSetup / #: custom summaries so imports look uniform to the spec author. CVLMATH_PROJECT_PATH = SUMMARIES_DIR / CVLMATH_SPEC_NAME +CVLMATH_ABSTRACT_PROJECT_PATH = SUMMARIES_DIR / CVLMATH_ABSTRACT_SPEC_NAME def cvlmath_spec_text() -> str: - """The packaged CVLMath library source.""" + """The packaged two-tier CVLMath library source (exact + import of abstract).""" return (files(__package__) / CVLMATH_SPEC_NAME).read_text() +def cvlmath_abstract_spec_text() -> str: + """The packaged standalone relational-abstraction library source.""" + return (files(__package__) / CVLMATH_ABSTRACT_SPEC_NAME).read_text() + + def install_cvlmath_resource(project_root: str | Path) -> CVLResource: """Copy the packaged CVLMath library into *project_root*'s summaries dir (mirroring how ``setup_summaries`` writes ``custom_summaries.spec``) and return the :class:`CVLResource` advertising it to the spec author. + + Must run after the AutoSetup phase: it checks whether AutoSetup already + copied Math.spec into the project. If so, only the abstract tier is + installed (and advertised) — the exact ``*Summary`` functions are already + reachable via the AutoSetup summaries import, and installing CVLMath.spec + too would double-define them. Otherwise the full two-file library is + installed and CVLMath.spec (which imports the abstract file) is advertised. """ + # The abstract tier defines no `*Summary` names, so it can always coexist + # with whatever summaries AutoSetup emitted. + abstract_dest = under_project(project_root, CVLMATH_ABSTRACT_PROJECT_PATH) + ensure_dir(abstract_dest.parent) + abstract_dest.write_text(cvlmath_abstract_spec_text()) + + if under_project(project_root, AUTOSETUP_MATH_SPEC_PATH).exists(): + return CVLResource( + path=CVLMATH_ABSTRACT_PROJECT_PATH, + required=False, + sort="import", + description=( + "Relational math abstractions (mulDiv/WAD Abstract variants) " + "for taming nonlinear arithmetic; the exact *Summary models " + "already ship with the AutoSetup summaries (Math.spec)" + ), + ) + dest = under_project(project_root, CVLMATH_PROJECT_PATH) - ensure_dir(dest.parent) dest.write_text(cvlmath_spec_text()) return CVLResource( path=CVLMATH_PROJECT_PATH, diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py index 628f67de..b7539231 100644 --- a/composer/spec/source/pipeline.py +++ b/composer/spec/source/pipeline.py @@ -170,7 +170,10 @@ async def stream_autosetup() -> tuple[SetupSuccess, list[CVLResource]]: ] # Ship the packaged CVLMath library into the project (mirroring how # custom_summaries.spec is written by the summaries phase) and offer it - # as an optional import for taming nonlinear arithmetic. + # as an optional import for taming nonlinear arithmetic. Must stay + # after the AutoSetup await above: the helper checks whether AutoSetup + # copied Math.spec into the project and, if so, installs only the + # abstract tier to avoid double-defining the exact *Summary functions. resources.append(install_cvlmath_resource(source_input.project_root)) if sys_desc.erc20_contracts or sys_desc.external_interfaces: summary_resource = await run_task( diff --git a/tests/test_cvlmath_asset.py b/tests/test_cvlmath_asset.py index 18631a91..538efb5f 100644 --- a/tests/test_cvlmath_asset.py +++ b/tests/test_cvlmath_asset.py @@ -1,10 +1,11 @@ -"""Tests for the packaged CVLMath asset and its pipeline resource wiring. +"""Tests for the packaged CVLMath assets and their pipeline resource wiring. -The asset must be resolvable through ``importlib.resources`` (so it survives +The assets must be resolvable through ``importlib.resources`` (so they survive being installed as a wheel, not just run from a source checkout), the install -helper must write the project copy exactly where the pipeline advertises it, -and the shipped CVL must parse with the same syntax checker the authoring -tools use. +helper must write the project copies exactly where the pipeline advertises +them — dropping the exact tier when AutoSetup already copied Math.spec — and +the shipped CVL must parse with the same syntax checker the authoring tools +use. """ import shutil @@ -13,38 +14,91 @@ import pytest from composer.spec.assets import ( + AUTOSETUP_MATH_SPEC_PATH, + CVLMATH_ABSTRACT_PROJECT_PATH, + CVLMATH_ABSTRACT_SPEC_NAME, CVLMATH_PROJECT_PATH, CVLMATH_SPEC_NAME, + cvlmath_abstract_spec_text, cvlmath_spec_text, install_cvlmath_resource, ) -from composer.spec.gen_types import SUMMARIES_DIR -def test_asset_resolvable_with_both_tiers(): - text = cvlmath_spec_text() - # Spot-check that both tiers ship: exact summaries + relational abstractions. - assert "mulDivDownSummary" in text - assert "mulDivUpSummary" in text +def test_abstract_asset_is_standalone_relational_tier(): + text = cvlmath_abstract_spec_text() + # The relational tier plus the WAD/RAY definitions live here... assert "mulDivDownAbstract" in text assert "mulDivUpAbstract" in text assert "definition WAD()" in text assert "definition RAY()" in text + # ...and no `*Summary` definition, so it can coexist with Math.spec. + assert "Summary(" not in text + + +def test_cvlmath_asset_is_exact_tier_importing_abstract(): + text = cvlmath_spec_text() + # Exact tier defined here (byte-identical to the AutoSetup Math.spec)... + assert "mulDivDownSummary" in text + assert "mulDivUpSummary" in text + # ...with the relational tier pulled in by import, not redefined. + assert f'import "{CVLMATH_ABSTRACT_SPEC_NAME}";' in text + assert "function mulDivDownAbstract" not in text + assert "definition WAD()" not in text + + +def test_cvlmath_exact_tier_matches_bundled_math_spec(): + """Guards the double-definition rationale: the install helper skips + CVLMath.spec exactly because its exact tier duplicates the AutoSetup + Math.spec definitions.""" + from pathlib import Path + import certora_autosetup + from certora_autosetup.utils.constants import SUMMARIES_SUBDIR -def test_install_writes_project_copy_and_builds_resource(tmp_path): + bundled = ( + Path(certora_autosetup.__file__).parent / "certora" / SUMMARIES_SUBDIR / "Math.spec" + ) + if not bundled.exists(): + pytest.skip(f"bundled Math.spec not found at {bundled}") + assert bundled.read_text().strip() in cvlmath_spec_text() + + +def test_install_without_math_spec_ships_both_tiers(tmp_path): res = install_cvlmath_resource(tmp_path) # The resource path is canonical (project-root-relative) and optional — # this is the CVLResource the pipeline appends in stream_autosetup(). assert res.path == CVLMATH_PROJECT_PATH assert res.sort == "import" assert not res.required - written = tmp_path / SUMMARIES_DIR / CVLMATH_SPEC_NAME - assert written.read_text() == cvlmath_spec_text() + assert (tmp_path / CVLMATH_PROJECT_PATH).read_text() == cvlmath_spec_text() + # The abstract tier lands next to it so the relative import resolves. + assert ( + tmp_path / CVLMATH_ABSTRACT_PROJECT_PATH + ).read_text() == cvlmath_abstract_spec_text() -def test_cvlmath_spec_passes_syntax_check(tmp_path): - """Parse the shipped spec with the same emv.jar checker ``put_cvl_raw`` uses.""" +def test_install_with_math_spec_ships_abstract_tier_only(tmp_path): + math_spec = tmp_path / AUTOSETUP_MATH_SPEC_PATH + math_spec.parent.mkdir(parents=True) + math_spec.write_text("// AutoSetup-copied exact summaries\n") + res = install_cvlmath_resource(tmp_path) + assert res.path == CVLMATH_ABSTRACT_PROJECT_PATH + assert res.sort == "import" + assert not res.required + assert ( + tmp_path / CVLMATH_ABSTRACT_PROJECT_PATH + ).read_text() == cvlmath_abstract_spec_text() + # CVLMath.spec would double-define the *Summary functions — must not exist. + assert not (tmp_path / CVLMATH_PROJECT_PATH).exists() + + +@pytest.mark.parametrize( + "spec_name", + [CVLMATH_ABSTRACT_SPEC_NAME, CVLMATH_SPEC_NAME], +) +def test_cvlmath_specs_pass_syntax_check(tmp_path, spec_name): + """Parse the shipped specs with the same emv.jar checker ``put_cvl_raw`` uses.""" from composer.certora_env import CertoraEnvironmentError, typechecker_jar if shutil.which("java") is None: @@ -53,10 +107,12 @@ def test_cvlmath_spec_passes_syntax_check(tmp_path): jar = typechecker_jar() except CertoraEnvironmentError as exc: pytest.skip(f"Typechecker.jar unavailable: {exc}") - spec = tmp_path / CVLMATH_SPEC_NAME - spec.write_text(cvlmath_spec_text()) + # Write both files so CVLMath.spec's relative import of the abstract tier + # resolves, then check the requested entry point. + (tmp_path / CVLMATH_SPEC_NAME).write_text(cvlmath_spec_text()) + (tmp_path / CVLMATH_ABSTRACT_SPEC_NAME).write_text(cvlmath_abstract_spec_text()) res = subprocess.run( - ["java", "-classpath", str(jar), "EntryPointKt", str(spec)], + ["java", "-classpath", str(jar), "EntryPointKt", str(tmp_path / spec_name)], capture_output=True, text=True, ) From 0eb716138ffbaeaf4859d16fb6d27b3bb6b79b04 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:45:04 +0300 Subject: [PATCH 3/5] Remove stale CVLMath.spec when AutoSetup later ships Math.spec If run 1 installed the full library (Math.spec absent) and a later run's AutoSetup closure pulls Math.spec in, the leftover CVLMath.spec plus a cached generated spec importing it would double-define the *Summary functions and fail CVL typechecking. Co-Authored-By: Claude Fable 5 --- composer/spec/assets/__init__.py | 5 +++++ tests/test_cvlmath_asset.py | 18 ++++++++++++++++++ 2 files changed, 23 insertions(+) diff --git a/composer/spec/assets/__init__.py b/composer/spec/assets/__init__.py index 4353932d..4eba165d 100644 --- a/composer/spec/assets/__init__.py +++ b/composer/spec/assets/__init__.py @@ -65,6 +65,11 @@ def install_cvlmath_resource(project_root: str | Path) -> CVLResource: abstract_dest.write_text(cvlmath_abstract_spec_text()) if under_project(project_root, AUTOSETUP_MATH_SPEC_PATH).exists(): + # A previous run may have installed CVLMath.spec back when Math.spec + # was absent; a cached generated spec importing it alongside the new + # Math.spec would double-define the `*Summary` functions, so drop the + # now-stale copy. + under_project(project_root, CVLMATH_PROJECT_PATH).unlink(missing_ok=True) return CVLResource( path=CVLMATH_ABSTRACT_PROJECT_PATH, required=False, diff --git a/tests/test_cvlmath_asset.py b/tests/test_cvlmath_asset.py index 538efb5f..1e1d8039 100644 --- a/tests/test_cvlmath_asset.py +++ b/tests/test_cvlmath_asset.py @@ -93,6 +93,24 @@ def test_install_with_math_spec_ships_abstract_tier_only(tmp_path): assert not (tmp_path / CVLMATH_PROJECT_PATH).exists() +def test_install_with_math_spec_removes_stale_cvlmath(tmp_path): + """Multi-run edge: run 1 installs the full library (no Math.spec yet), + then a later run's AutoSetup closure pulls Math.spec in — the leftover + CVLMath.spec must be removed or a cached generated spec importing it + would double-define the *Summary functions.""" + first = install_cvlmath_resource(tmp_path) + assert first.path == CVLMATH_PROJECT_PATH + math_spec = tmp_path / AUTOSETUP_MATH_SPEC_PATH + math_spec.write_text("// AutoSetup-copied exact summaries\n") + res = install_cvlmath_resource(tmp_path) + assert res.path == CVLMATH_ABSTRACT_PROJECT_PATH + assert not (tmp_path / CVLMATH_PROJECT_PATH).exists() + # The abstract tier is still (re)installed for the aggregator import. + assert ( + tmp_path / CVLMATH_ABSTRACT_PROJECT_PATH + ).read_text() == cvlmath_abstract_spec_text() + + @pytest.mark.parametrize( "spec_name", [CVLMATH_ABSTRACT_SPEC_NAME, CVLMATH_SPEC_NAME], From 27fb329303c0845a0f16294c4b218d6307785993 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 02:45:49 +0300 Subject: [PATCH 4/5] Single-source the exact math tier from AutoSetup's bundled Math.spec MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The exact *Summary tier now has exactly one source and one name: certora_autosetup's bundled Math.spec, copied by the install helper to certora/specs/summaries/Math.spec only when AutoSetup's summary closure did not already place it there (and advertised as a resource only then). CVLMathAbstract.spec — the relational require-axiom tier — is always installed and advertised. This removes the composer-shipped CVLMath.spec copy and the presence-conditional install / stale-unlink apparatus: with a single path there is nothing to drift, nothing to remove, and a cached generated spec importing summaries/Math.spec keeps typechecking across runs (same-path diamond imports dedupe). Tests: the drift guard now hard-fails (no skip) if the bundled Math.spec is missing or renamed — exactly the event that would break the install helper; the emv.jar syntax checks run against the two shipped names. The generation prompt names both tiers and spells out the *Abstract require-based axioms' vacuity caveat (prefer relational properties, avoid under satisfy, SANITY_FAILURE = conflicting axioms). Co-Authored-By: Claude Fable 5 --- composer/spec/assets/CVLMath.spec | 99 ------------ composer/spec/assets/CVLMathAbstract.spec | 9 +- composer/spec/assets/__init__.py | 131 ++++++++------- composer/spec/source/pipeline.py | 15 +- .../templates/property_generation_prompt.j2 | 15 +- tests/test_cvlmath_asset.py | 150 +++++++++--------- 6 files changed, 177 insertions(+), 242 deletions(-) delete mode 100644 composer/spec/assets/CVLMath.spec diff --git a/composer/spec/assets/CVLMath.spec b/composer/spec/assets/CVLMath.spec deleted file mode 100644 index b3526015..00000000 --- a/composer/spec/assets/CVLMath.spec +++ /dev/null @@ -1,99 +0,0 @@ -/* - * CVLMath — reusable CVL math library, shipped into generated projects by the - * autoprove pipeline as certora/specs/summaries/CVLMath.spec. - * - * Two tiers of models for the standard Solidity mulDiv/WAD helpers: - * 1. Exact summaries (`*Summary`, defined below): faithful models preserving - * the exact rounding and revert behavior. Copied verbatim from the - * AutoSetup-bundled Math.spec library. Use these by default. - * 2. Relational abstractions (`*Abstract`, pulled in from the imported - * CVLMathAbstract.spec): replace the nonlinear product / quotient with - * solver-friendly axioms (zero-preservation, exactness at the - * denominator, monotonicity, down/up rounding within 1). Use these as - * summaries when the exact formulas make the prover time out and the - * property only needs relational facts — do NOT weaken the property - * instead. - * - * NB: because Tier 1 is byte-identical to the AutoSetup-bundled Math.spec, - * importing both would define the `*Summary` functions twice and fail - * typechecking. The pipeline therefore only installs this file when the - * project's AutoSetup summaries did NOT already pull in Math.spec; otherwise - * it installs CVLMathAbstract.spec alone. Keep that in mind if you copy this - * file into a project by hand. - */ - -import "CVLMathAbstract.spec"; - -/************************************************************* - * Tier 1: exact summaries (verbatim from AutoSetup Math.spec) - *************************************************************/ - -function mulDivDownSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 { - mathint result; - if (denominator == 0) revert(); - result = x * y / denominator; - if (result >= 2^256) revert(); - return assert_uint256(result); -} - -function mulDivUpSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 { - mathint result; - if (denominator == 0) revert(); - result = (x * y + denominator - 1) / denominator; - if (result >= 2^256) revert(); - return assert_uint256(result); -} - -function averageSummary(uint256 a, uint256 b) returns uint256 { - return require_uint256((a+b)/2); -} - -// Exact (real) square root: the result squared equals the argument. This is the -// strongest abstraction and keeps the constraint simple for the solver (no Babylonian -// loop to unroll), but for arguments that are not perfect squares no such `result` -// exists, so the `require` prunes that path (potential vacuity). Use for invariant -// reasoning where sqrt is treated as exact (e.g. constant-product AMM invariants). -function sqrtSummaryPrecise(uint256 x) returns uint256 { - mathint result; - require result >= 0 && result * result == x; - return assert_uint256(result); -} - -// Floor (integer) square root: result == floor(sqrt(x)), matching Solidity's integer -// sqrt. Sound for every argument (always has a solution), at the cost of an extra -// multiplication / strict upper bound for the solver. -function sqrtSummaryDown(uint256 x) returns uint256 { - mathint result; - require result >= 0 && result * result <= x && x < (result + 1) * (result + 1); - return assert_uint256(result); -} - -function mulWadDownSummary(uint256 x, uint256 y) returns uint256 { - mathint result; - result = x * y / 1000000000000000000; - if (result >= 2^256) revert(); - return assert_uint256(result); -} - -function mulWadUpSummary(uint256 x, uint256 y) returns uint256 { - mathint result; - result = (x * y + 999999999999999999) / 1000000000000000000; - if (result >= 2^256) revert(); - return assert_uint256(result); -} - -function divWadDownSummary(uint256 x, uint256 y) returns uint256 { - mathint result; - if (y == 0) revert(); - result = x * 1000000000000000000 / y; - if (result >= 2^256) revert(); - return assert_uint256(result); -} - -function divWadUpSummary(uint256 x, uint256 y) returns uint256 { - mathint result; - if (y == 0) revert(); - result = (x * 1000000000000000000 + y - 1) / y; - if (result >= 2^256) revert(); - return assert_uint256(result); -} diff --git a/composer/spec/assets/CVLMathAbstract.spec b/composer/spec/assets/CVLMathAbstract.spec index 623b4d87..8938309c 100644 --- a/composer/spec/assets/CVLMathAbstract.spec +++ b/composer/spec/assets/CVLMathAbstract.spec @@ -10,10 +10,11 @@ * 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 AutoSetup-bundled Math.spec exact - * summaries without any double-definition clash. Projects whose AutoSetup - * summaries did NOT pull in Math.spec get the exact tier too, via the - * sibling CVLMath.spec which imports this file. + * 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; diff --git a/composer/spec/assets/__init__.py b/composer/spec/assets/__init__.py index 4eba165d..ecdbf01e 100644 --- a/composer/spec/assets/__init__.py +++ b/composer/spec/assets/__init__.py @@ -6,89 +6,104 @@ 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 CVLMath library ships as two files so the exact tier can be dropped when -it would clash: - -* ``CVLMathAbstract.spec`` — the relational ``*Abstract`` tier plus WAD/RAY. - Standalone; always installed. -* ``CVLMath.spec`` — the exact ``*Summary`` tier (byte-identical to the - AutoSetup-bundled Math.spec) importing the abstract file. Installed only - when AutoSetup did NOT already copy Math.spec into the project, since - importing both would define the ``*Summary`` functions twice and fail CVL - typechecking. +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_SPEC_NAME = "CVLMath.spec" CVLMATH_ABSTRACT_SPEC_NAME = "CVLMathAbstract.spec" -#: Where the AutoSetup-bundled exact Math.spec lands when the curated summary -#: closure pulls it in (copy_summaries_folder preserves the bundled layout). -#: Its presence is the "exact tier already imported" signal. -AUTOSETUP_MATH_SPEC_PATH = SUMMARIES_DIR / "Math.spec" -#: Canonical (project-root-relative) install locations — next to the AutoSetup / -#: custom summaries so imports look uniform to the spec author. -CVLMATH_PROJECT_PATH = SUMMARIES_DIR / CVLMATH_SPEC_NAME +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. MATH_SPEC_ +#: PROJECT_PATH is the SAME path 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_spec_text() -> str: - """The packaged two-tier CVLMath library source (exact + import of abstract).""" - return (files(__package__) / CVLMATH_SPEC_NAME).read_text() - - def cvlmath_abstract_spec_text() -> str: """The packaged standalone relational-abstraction library source.""" return (files(__package__) / CVLMATH_ABSTRACT_SPEC_NAME).read_text() -def install_cvlmath_resource(project_root: str | Path) -> CVLResource: - """Copy the packaged CVLMath library into *project_root*'s summaries dir +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` advertising it to the spec author. - - Must run after the AutoSetup phase: it checks whether AutoSetup already - copied Math.spec into the project. If so, only the abstract tier is - installed (and advertised) — the exact ``*Summary`` functions are already - reachable via the AutoSetup summaries import, and installing CVLMath.spec - too would double-define them. Otherwise the full two-file library is - installed and CVLMath.spec (which imports the abstract file) is advertised. + 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. """ - # The abstract tier defines no `*Summary` names, so it can always coexist - # with whatever summaries AutoSetup emitted. abstract_dest = under_project(project_root, CVLMATH_ABSTRACT_PROJECT_PATH) ensure_dir(abstract_dest.parent) abstract_dest.write_text(cvlmath_abstract_spec_text()) - - if under_project(project_root, AUTOSETUP_MATH_SPEC_PATH).exists(): - # A previous run may have installed CVLMath.spec back when Math.spec - # was absent; a cached generated spec importing it alongside the new - # Math.spec would double-define the `*Summary` functions, so drop the - # now-stale copy. - under_project(project_root, CVLMATH_PROJECT_PATH).unlink(missing_ok=True) - return CVLResource( + resources = [ + CVLResource( path=CVLMATH_ABSTRACT_PROJECT_PATH, required=False, sort="import", description=( - "Relational math abstractions (mulDiv/WAD Abstract variants) " - "for taming nonlinear arithmetic; the exact *Summary models " - "already ship with the AutoSetup summaries (Math.spec)" + "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" ), - ) - - dest = under_project(project_root, CVLMATH_PROJECT_PATH) - dest.write_text(cvlmath_spec_text()) - return CVLResource( - path=CVLMATH_PROJECT_PATH, - required=False, - sort="import", - description=( - "Reusable math abstractions (mulDiv/WAD): exact summaries and " - "relational Abstract variants for taming nonlinear arithmetic" ), - ) + ] + + 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 diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py index b7539231..b9066264 100644 --- a/composer/spec/source/pipeline.py +++ b/composer/spec/source/pipeline.py @@ -23,7 +23,7 @@ from composer.ui.autoprove_app import AutoProvePhase from composer.input.files import Document -from composer.spec.assets import install_cvlmath_resource +from composer.spec.assets import install_cvlmath_resources from composer.spec.context import ( WorkflowContext, CacheKey, Properties, CVLGeneration, ) @@ -168,13 +168,14 @@ async def stream_autosetup() -> tuple[SetupSuccess, list[CVLResource]]: sort="import", ), ] - # Ship the packaged CVLMath library into the project (mirroring how + # Ship the CVL math library into the project (mirroring how # custom_summaries.spec is written by the summaries phase) and offer it - # as an optional import for taming nonlinear arithmetic. Must stay - # after the AutoSetup await above: the helper checks whether AutoSetup - # copied Math.spec into the project and, if so, installs only the - # abstract tier to avoid double-defining the exact *Summary functions. - resources.append(install_cvlmath_resource(source_input.project_root)) + # 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, diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index 2d1bf63f..5fb70423 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/composer/templates/property_generation_prompt.j2 @@ -125,9 +125,18 @@ 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 CVLMath 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. +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. ## Step 4 diff --git a/tests/test_cvlmath_asset.py b/tests/test_cvlmath_asset.py index 1e1d8039..2be230a4 100644 --- a/tests/test_cvlmath_asset.py +++ b/tests/test_cvlmath_asset.py @@ -1,27 +1,28 @@ -"""Tests for the packaged CVLMath assets and their pipeline resource wiring. - -The assets must be resolvable through ``importlib.resources`` (so they survive -being installed as a wheel, not just run from a source checkout), the install -helper must write the project copies exactly where the pipeline advertises -them — dropping the exact tier when AutoSetup already copied Math.spec — and -the shipped CVL must parse with the same syntax checker the authoring tools -use. +"""Tests for the packaged CVL math assets and their pipeline resource wiring. + +The abstract-tier asset must be resolvable through ``importlib.resources`` (so +it survives being installed as a wheel, not just run from a source checkout), +the exact tier must come from the ONE canonical certora_autosetup-bundled +Math.spec (composer ships no copy), the install helper must write the project +files exactly where the pipeline advertises them — adding Math.spec only when +AutoSetup did not already ship it — and the shipped CVL must parse with the +same syntax checker the authoring tools use. """ import shutil import subprocess +from pathlib import Path import pytest from composer.spec.assets import ( - AUTOSETUP_MATH_SPEC_PATH, CVLMATH_ABSTRACT_PROJECT_PATH, CVLMATH_ABSTRACT_SPEC_NAME, - CVLMATH_PROJECT_PATH, - CVLMATH_SPEC_NAME, + MATH_SPEC_NAME, + MATH_SPEC_PROJECT_PATH, + bundled_math_spec_text, cvlmath_abstract_spec_text, - cvlmath_spec_text, - install_cvlmath_resource, + install_cvlmath_resources, ) @@ -36,76 +37,83 @@ def test_abstract_asset_is_standalone_relational_tier(): assert "Summary(" not in text -def test_cvlmath_asset_is_exact_tier_importing_abstract(): - text = cvlmath_spec_text() - # Exact tier defined here (byte-identical to the AutoSetup Math.spec)... - assert "mulDivDownSummary" in text - assert "mulDivUpSummary" in text - # ...with the relational tier pulled in by import, not redefined. - assert f'import "{CVLMATH_ABSTRACT_SPEC_NAME}";' in text - assert "function mulDivDownAbstract" not in text - assert "definition WAD()" not in text - - -def test_cvlmath_exact_tier_matches_bundled_math_spec(): - """Guards the double-definition rationale: the install helper skips - CVLMath.spec exactly because its exact tier duplicates the AutoSetup - Math.spec definitions.""" - from pathlib import Path - +def test_bundled_math_spec_is_resolvable_and_is_the_exact_tier(): + """Drift guard for the single-source scheme: the canonical exact tier is + certora_autosetup's bundled Math.spec, read through importlib.resources. + If that file is ever moved or renamed this test must FAIL (not skip) — + that is precisely the event that would break the install helper and any + generated spec importing summaries/Math.spec.""" import certora_autosetup from certora_autosetup.utils.constants import SUMMARIES_SUBDIR - bundled = ( - Path(certora_autosetup.__file__).parent / "certora" / SUMMARIES_SUBDIR / "Math.spec" + fs_path = ( + Path(certora_autosetup.__file__).parent + / "certora" + / SUMMARIES_SUBDIR + / MATH_SPEC_NAME + ) + assert fs_path.exists(), ( + f"canonical bundled Math.spec missing at {fs_path}; the composer " + "install helper and generated-spec imports depend on this exact path" ) - if not bundled.exists(): - pytest.skip(f"bundled Math.spec not found at {bundled}") - assert bundled.read_text().strip() in cvlmath_spec_text() + # bundled_math_spec_text() must resolve to that same file (raises rather + # than skipping if the packaged layout diverges). + text = bundled_math_spec_text() + assert text == fs_path.read_text() + # And it is the exact `*Summary` tier the resource description promises. + assert "mulDivDownSummary" in text + assert "mulDivUpSummary" in text + assert "sqrtSummaryPrecise" in text def test_install_without_math_spec_ships_both_tiers(tmp_path): - res = install_cvlmath_resource(tmp_path) - # The resource path is canonical (project-root-relative) and optional — - # this is the CVLResource the pipeline appends in stream_autosetup(). - assert res.path == CVLMATH_PROJECT_PATH - assert res.sort == "import" - assert not res.required - assert (tmp_path / CVLMATH_PROJECT_PATH).read_text() == cvlmath_spec_text() - # The abstract tier lands next to it so the relative import resolves. + resources = install_cvlmath_resources(tmp_path) + # Resource paths are canonical (project-root-relative) and optional — + # these are the CVLResources the pipeline appends in stream_autosetup(). + by_path = {res.path: res for res in resources} + assert set(by_path) == {CVLMATH_ABSTRACT_PROJECT_PATH, MATH_SPEC_PROJECT_PATH} + for res in resources: + assert res.sort == "import" + assert not res.required + assert "require" in by_path[CVLMATH_ABSTRACT_PROJECT_PATH].description + # Both tiers land in the summaries dir, byte-identical to their sources. assert ( tmp_path / CVLMATH_ABSTRACT_PROJECT_PATH ).read_text() == cvlmath_abstract_spec_text() + assert (tmp_path / MATH_SPEC_PROJECT_PATH).read_text() == bundled_math_spec_text() -def test_install_with_math_spec_ships_abstract_tier_only(tmp_path): - math_spec = tmp_path / AUTOSETUP_MATH_SPEC_PATH +def test_install_with_math_spec_present_ships_abstract_resource_only(tmp_path): + math_spec = tmp_path / MATH_SPEC_PROJECT_PATH math_spec.parent.mkdir(parents=True) - math_spec.write_text("// AutoSetup-copied exact summaries\n") - res = install_cvlmath_resource(tmp_path) - assert res.path == CVLMATH_ABSTRACT_PROJECT_PATH - assert res.sort == "import" - assert not res.required + sentinel = "// AutoSetup-copied exact summaries\n" + math_spec.write_text(sentinel) + resources = install_cvlmath_resources(tmp_path) + # Only the abstract tier is advertised: the exact tier is already + # reachable through the required AutoSetup summaries import. + assert [res.path for res in resources] == [CVLMATH_ABSTRACT_PROJECT_PATH] assert ( tmp_path / CVLMATH_ABSTRACT_PROJECT_PATH ).read_text() == cvlmath_abstract_spec_text() - # CVLMath.spec would double-define the *Summary functions — must not exist. - assert not (tmp_path / CVLMATH_PROJECT_PATH).exists() - - -def test_install_with_math_spec_removes_stale_cvlmath(tmp_path): - """Multi-run edge: run 1 installs the full library (no Math.spec yet), - then a later run's AutoSetup closure pulls Math.spec in — the leftover - CVLMath.spec must be removed or a cached generated spec importing it - would double-define the *Summary functions.""" - first = install_cvlmath_resource(tmp_path) - assert first.path == CVLMATH_PROJECT_PATH - math_spec = tmp_path / AUTOSETUP_MATH_SPEC_PATH - math_spec.write_text("// AutoSetup-copied exact summaries\n") - res = install_cvlmath_resource(tmp_path) - assert res.path == CVLMATH_ABSTRACT_PROJECT_PATH - assert not (tmp_path / CVLMATH_PROJECT_PATH).exists() - # The abstract tier is still (re)installed for the aggregator import. + # The existing Math.spec is AutoSetup's to manage — never overwritten. + assert math_spec.read_text() == sentinel + + +def test_install_is_idempotent_across_runs(tmp_path): + """Multi-run edge: run 1 installs Math.spec (no AutoSetup copy yet); a + later run must leave the on-disk exact tier intact at the same single + path, so a cached generated spec importing summaries/Math.spec still + typechecks.""" + first = install_cvlmath_resources(tmp_path) + assert {res.path for res in first} == { + CVLMATH_ABSTRACT_PROJECT_PATH, + MATH_SPEC_PROJECT_PATH, + } + second = install_cvlmath_resources(tmp_path) + # Math.spec already exists (identical canonical bytes), so it is not + # re-advertised; the file itself must survive with the same content. + assert [res.path for res in second] == [CVLMATH_ABSTRACT_PROJECT_PATH] + assert (tmp_path / MATH_SPEC_PROJECT_PATH).read_text() == bundled_math_spec_text() assert ( tmp_path / CVLMATH_ABSTRACT_PROJECT_PATH ).read_text() == cvlmath_abstract_spec_text() @@ -113,7 +121,7 @@ def test_install_with_math_spec_removes_stale_cvlmath(tmp_path): @pytest.mark.parametrize( "spec_name", - [CVLMATH_ABSTRACT_SPEC_NAME, CVLMATH_SPEC_NAME], + [CVLMATH_ABSTRACT_SPEC_NAME, MATH_SPEC_NAME], ) def test_cvlmath_specs_pass_syntax_check(tmp_path, spec_name): """Parse the shipped specs with the same emv.jar checker ``put_cvl_raw`` uses.""" @@ -125,10 +133,10 @@ def test_cvlmath_specs_pass_syntax_check(tmp_path, spec_name): jar = typechecker_jar() except CertoraEnvironmentError as exc: pytest.skip(f"Typechecker.jar unavailable: {exc}") - # Write both files so CVLMath.spec's relative import of the abstract tier - # resolves, then check the requested entry point. - (tmp_path / CVLMATH_SPEC_NAME).write_text(cvlmath_spec_text()) + return # unreachable (skip raises); keeps `jar` provably bound below + # Both files are standalone (no imports), so each is checked on its own. (tmp_path / CVLMATH_ABSTRACT_SPEC_NAME).write_text(cvlmath_abstract_spec_text()) + (tmp_path / MATH_SPEC_NAME).write_text(bundled_math_spec_text()) res = subprocess.run( ["java", "-classpath", str(jar), "EntryPointKt", str(tmp_path / spec_name)], capture_output=True, From 912cc6ed2562aef3438cb9388742f20857f2e6ac Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 02:46:45 +0300 Subject: [PATCH 5/5] Unwrap identifier split across lines in install-location comment Co-Authored-By: Claude Fable 5 --- composer/spec/assets/__init__.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/composer/spec/assets/__init__.py b/composer/spec/assets/__init__.py index ecdbf01e..b33217b3 100644 --- a/composer/spec/assets/__init__.py +++ b/composer/spec/assets/__init__.py @@ -30,10 +30,10 @@ 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. MATH_SPEC_ -#: PROJECT_PATH is the SAME path 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". +#: 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