diff --git a/composer/spec/assets/CVLMathAbstract.spec b/composer/spec/assets/CVLMathAbstract.spec new file mode 100644 index 0000000..8938309 --- /dev/null +++ b/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); +} diff --git a/composer/spec/assets/__init__.py b/composer/spec/assets/__init__.py new file mode 100644 index 0000000..b33217b --- /dev/null +++ b/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 diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py index 5799f16..b906626 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_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, diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index d96585c..5fb7042 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/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 + + +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. + + ## 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 537b2af..4c90ef9 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 51d1476..7598446 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 0000000..2be230a --- /dev/null +++ b/tests/test_cvlmath_asset.py @@ -0,0 +1,145 @@ +"""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 ( + CVLMATH_ABSTRACT_PROJECT_PATH, + CVLMATH_ABSTRACT_SPEC_NAME, + MATH_SPEC_NAME, + MATH_SPEC_PROJECT_PATH, + bundled_math_spec_text, + cvlmath_abstract_spec_text, + install_cvlmath_resources, +) + + +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_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 + + 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" + ) + # 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): + 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_present_ships_abstract_resource_only(tmp_path): + math_spec = tmp_path / MATH_SPEC_PROJECT_PATH + math_spec.parent.mkdir(parents=True) + 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() + # 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() + + +@pytest.mark.parametrize( + "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.""" + 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}") + 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, + text=True, + ) + assert res.returncode == 0, f"stdout:\n{res.stdout}\nstderr:\n{res.stderr}"