Certora specification files - #180
Open
dominik-velan wants to merge 1 commit into
Open
Conversation
📝 WalkthroughWalkthroughThis PR introduces a complete formal verification suite for the Reserve Folio protocol using Certora. It adds harnesses exposing internal state, CVL specifications modeling dependencies, property-specific verification rules, Certora configurations for ten properties (P1–P10), and orchestration scripts to run the full verification workflow. The patch temporarily exposes internal Folio state variables to enable harness access. ChangesFolio Formal Verification Suite
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Suggested reviewers
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 15
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
certora/patches/Folio.patch (1)
1-41:⚠️ Potential issue | 🟡 MinorKeep
certora/patches/Folio.patchstrictly verification-only (and ensure it’s reverted after Certora runs).
certora/scripts/run-all.shapplies the patch (certora/scripts/apply-patch.sh→git apply certora/patches/Folio.patch) and then reverts it (certora/scripts/remove-patch.sh→git apply -R certora/patches/Folio.patch).- The patch changes
contracts/Folio.solvisibility fromprivate→internalforbasket,activeTrustedFill,rebalance, andactiveTrustedFillFloorPrice; ensure this patch never reaches production builds, and make the “verification-only” intent explicit incertora/README.md(it currently only describes the visibility change).🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@certora/patches/Folio.patch` around lines 1 - 41, The Certora patch makes storage variables basket, activeTrustedFill, rebalance, and activeTrustedFillFloorPrice internal (instead of private) for verification only; update certora/README.md to explicitly state this patch is verification-only and must never be merged into production, and ensure the existing scripts (certora/scripts/apply-patch.sh and certora/scripts/remove-patch.sh invoked by certora/scripts/run-all.sh) are referenced in the README as the mechanism that applies and then reverts certora/patches/Folio.patch so the change is always removed after Certora runs.
🧹 Nitpick comments (5)
certora/harnesses/FolioHarness.sol (1)
110-115: ⚡ Quick winAdd explicit zero-check for nextAuctionId.
If
nextAuctionIdis0, line 111 will underflow totype(uint256).max. WhileisAuctionActivewill correctly returnfalseand trigger therequire, an explicit check improves clarity and avoids the underflow.♻️ Add explicit guard
function getPrice(IERC20 sellToken, IERC20 buyToken) external view returns (uint256) { + require(nextAuctionId > 0, "No auctions exist"); uint256 auctionId = nextAuctionId-1; require(isAuctionActive(auctionId), "id provided is of an inactive auction");🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@certora/harnesses/FolioHarness.sol` around lines 110 - 115, Add an explicit guard in the getPrice function to prevent underflow when computing auctionId: check require(nextAuctionId > 0, "no auctions exist") before doing uint256 auctionId = nextAuctionId - 1; so the function (getPrice) validates nextAuctionId > 0, then uses auctionId and calls isAuctionActive(auctionId) and RebalancingLib._price(rebalance, auctions[auctionId], sellToken, buyToken).certora/specs/folio-value.spec (3)
219-219: 💤 Low valueUnused rule parameters:
method fandcalldataarg args.The rule declares
method f, calldataarg argsbut callsmint(e, args)directly at line 232, notf(e, args). Either the parameters should be removed or the rule should be generalized to callf(e, args)if the intent is to verify multiple methods.♻️ Cleanup
-rule shareRatioDoesNotDecreaseOnMintToken1(env e, method f, calldataarg args) +rule shareRatioDoesNotDecreaseOnMintToken1(env e, calldataarg args) {🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@certora/specs/folio-value.spec` at line 219, The rule shareRatioDoesNotDecreaseOnMintToken1 currently declares unused parameters method f and calldataarg args but calls mint(e, args) directly; either remove the unused parameters from the rule signature to avoid dead variables, or change the invocation to call f(e, args) instead of mint(e, args) so the rule generalizes to any provided method—update the rule signature and all references accordingly (modify the rule header and replace the direct mint(...) call with f(e, args) if you choose generalization).
242-242: ⚡ Quick winUnused rule parameters in
shareRatioDoesNotDecreaseOnMintToken2andshareRatioDoesNotDecreaseOnMintToken3.Both rules declare
method f, calldataarg argsbut callmint(e, args)directly, similar to the Token1 rule. These parameters should be removed for consistency.Additionally, consider consolidating these three nearly-identical rules using a parameterized approach to reduce duplication.
♻️ Cleanup
-rule shareRatioDoesNotDecreaseOnMintToken2(env e, method f, calldataarg args) +rule shareRatioDoesNotDecreaseOnMintToken2(env e, calldataarg args) { address token2; uint256 id; _, token2, _, id = setupAssumptionsWithAuction(e);Similar fix for Token3, and consider a parameterized helper function.
Also applies to: 264-264
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@certora/specs/folio-value.spec` at line 242, The rules shareRatioDoesNotDecreaseOnMintToken2 and shareRatioDoesNotDecreaseOnMintToken3 declare unused parameters "method f, calldataarg args" but call mint(e, args) directly (like the Token1 rule); remove the unused parameters from both rule signatures so they match the usage, update any internal references if present, and optionally refactor shareRatioDoesNotDecreaseOnMintToken1/2/3 into a single parameterized helper rule that accepts the token identifier and invokes mint(e, args) to eliminate duplication.
150-151: 💤 Low valueUnused variables:
sellBalanceBeforeandbuyBalanceBefore.These variables are declared and assigned but never used in the rule. Consider removing them for clarity.
♻️ Cleanup
require sellToken != buyToken, "the two tokens are different"; - uint256 sellBalanceBefore = balanceByToken[sellToken][currentContract]; - uint256 buyBalanceBefore = balanceByToken[buyToken][currentContract]; - // Execute bid🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@certora/specs/folio-value.spec` around lines 150 - 151, Remove the two unused local variables by deleting the declarations "uint256 sellBalanceBefore = balanceByToken[sellToken][currentContract];" and "uint256 buyBalanceBefore = balanceByToken[buyToken][currentContract];" from the spec; they are never referenced elsewhere (search for sellBalanceBefore, buyBalanceBefore, balanceByToken, currentContract) so simply remove them to clean up the rule and run the spec checks to confirm no references remain.certora/specs/folio-priceMonotonicity.spec (1)
57-57: 💤 Low valueMisleading comment: "price.low >= 100 * price.high" doesn't match the constraint.
The constraint
startPrice < 20000 * endPricelimits the price ratio to 20000x, but the comment references a different constraint pattern. SincestartPrice > endPrice(line 56), this constraint meansstartPrice / endPrice < 20000.Consider updating the comment to accurately describe the constraint:
📝 Clarification
- require startPrice < 20000 * endPrice, "price.low >= 100 * price.high"; + require startPrice < 20000 * endPrice, "price decline limited to 20000x factor";🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@certora/specs/folio-priceMonotonicity.spec` at line 57, The error string on the require is misleading: update the message on the require call that currently reads require startPrice < 20000 * endPrice, "price.low >= 100 * price.high" to accurately reflect the actual constraint that startPrice < 20000 * endPrice (i.e., startPrice / endPrice < 20000 or "startPrice < 20000 * endPrice"); ensure the require message references startPrice/endPrice or the 20000x ratio so it matches the constraint in the spec.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@certora/confs/properties/P3-2.conf`:
- Line 61: The Certora property config currently disables sanity checks by
setting the "rule_sanity" key to "none"; update the "rule_sanity" setting in
certora/confs/properties/P3-2.conf from "none" to "basic" (or "advanced") so
vacuity/triviality checks are enabled for this property run and proofs aren't
reported vacuously.
In `@certora/confs/properties/P6-2.conf`:
- Around line 41-42: The JSON in certora/confs/properties/P6-2.conf has a
trailing comma in the "files" array (after
"certora/harnesses/RebalancingLibHarness.sol"), which breaks strict JSON
parsing; open the P6-2.conf, locate the "files" array and remove the trailing
comma after the last entry so the array ends with ] instead of "...,", ensuring
valid JSON for the parser.
In `@certora/harnesses/FolioHarness.sol`:
- Around line 67-69: _isTokenInDeficit currently multiplies limitL and weightL
then divides, risking overflow and differing from _isTokenInSurplus; change the
arithmetic to use Math.mulDiv with the same rounding semantics as
_isTokenInSurplus to avoid intermediate overflow. Specifically, compute the
scaled product using Math.mulDiv(limitL, weightL, 1e18, Rounding.Down) and then
use Math.mulDiv(result, totalShares, 1e27, Rounding.Down) (or mirror the exact
rounding used in _isTokenInSurplus) and compare that final value to
currentBalance inside _isTokenInDeficit.
In `@certora/mocks/MockTrustedFiller.sol`:
- Around line 69-89: The exchange function lacks a guard for the swapActive flag
allowing swaps after closeFiller()/emergencyCloseFiller() set swapActive =
false; add an early require in exchange (e.g., require(swapActive,
"MockTrustedFiller: swap not active")) so the function reverts when swaps are
closed, placing this check near the top of exchange before any balance reads,
and ensure it uses the same error string style as other requires in the
contract.
In `@certora/README.md`:
- Line 9: Update the README folder diagram to use the actual directory names:
replace any occurrence of "conf/" with "confs/" and "spec/" with "specs" so the
listed directories match the repository; adjust the entries shown in the tree
(the "conf/" node on the top-level listing and the "spec/" node later in the
diagram) to "confs/" and "specs/" respectively and ensure any related
descriptive text reflects those corrected names.
- Line 11: Update all misspelled filenames from "prerequisities" to
"prerequisites": rename the actual files certora/confs/folio_prerequisities.conf
-> certora/confs/folio_prerequisites.conf and
certora/specs/folio-prerequisities.spec ->
certora/specs/folio-prerequisites.spec, and update their references in
certora/README.md (change folio_prerequisities.conf and
folio-prerequisities.spec to folio_prerequisites.conf and
folio-prerequisites.spec) plus any other code/docs referencing these exact names
(search for "prerequisities") so all links and imports point to the corrected
filenames.
- Line 7: The README’s fenced code block for the folder structure is missing a
language specifier; update the opening fence (the lone "```" that begins the
certora/ folder example) to include a language identifier such as "text" or
"plaintext" so the block renders/accessibility improves (look for the README
line that contains only "```" before the "certora/" listing and change it to
"```text").
In `@certora/scripts/apply-patch.sh`:
- Line 3: The script apply-patch.sh uses a CWD-dependent path; fix it by
resolving the script directory (use BASH_SOURCE and dirname to set a SCRIPT_DIR
variable) and then call git apply with the patch path constructed from that
SCRIPT_DIR pointing to ../patches/Folio.patch so the patch is applied correctly
regardless of the current working directory.
In `@certora/scripts/P1.sh`:
- Around line 3-5: The cleanup step in P1.sh (and similarly P10.sh) can mask a
failing certoraRun because remove-patch.sh runs unconditionally and its exit
code may overwrite certoraRun's; modify the script to capture the exit status of
certoraRun (e.g., STATUS=$?), set a trap to invoke
certora/scripts/remove-patch.sh on EXIT so cleanup always runs, and after the
trap-completed exit handler, exit with the captured STATUS (non-zero if
verification failed) instead of the cleanup's status; ensure you reference and
preserve the certoraRun invocation and the call to
certora/scripts/remove-patch.sh when implementing this change.
In `@certora/scripts/P2.sh`:
- Around line 3-5: The script P2.sh can mask certoraRun failures because the
final cleanup (certora/scripts/remove-patch.sh) can overwrite the exit status;
modify P2.sh to enable strict error handling (e.g., set -euo pipefail) and/or
capture certoraRun's exit code into a variable (EXIT_CODE=$?) immediately after
running certoraRun, always run cleanup (certora/scripts/remove-patch.sh), then
exit with the saved EXIT_CODE so a failing certoraRun propagates correctly;
ensure apply-patch.sh still runs before certoraRun and cleanup runs regardless
of intermediate failures.
In `@certora/scripts/run-all.sh`:
- Around line 3-13: The script certora/scripts/run-all.sh lacks strict shell
error handling and cleanup on early exit; enable strict mode (e.g., set -euo
pipefail) at the top of run-all.sh, add a trap to always run
certora/scripts/remove-patch.sh on EXIT (and optionally on INT/TERM) to
guarantee rollback, and ensure certoraRun failures are not masked by letting
errors propagate (or capturing exit codes and exiting non‑zero) while still
invoking the trap; reference the certoraRun invocations, the initial
certora/scripts/apply-patch.sh call, the for-loop over
certora/confs/properties/*.conf, and certora/scripts/remove-patch.sh so the
changes are applied around those symbols.
In `@certora/specs/folio-mockFill.spec`:
- Around line 74-76: The test calls envfree methods with an environment
parameter: replace calls to MockTrustedFiller.sellToken(e) and
MockTrustedFiller.buyToken(e) so they are invoked without the environment
argument (e.g., use filler.sellToken() and filler.buyToken()) or call them on
the direct contract reference that expects an env parameter; update the two
occurrences around variables filler and e to match the method declaration
(MockTrustedFiller.sellToken and MockTrustedFiller.buyToken are declared
envfree) so the call signatures are consistent.
In `@certora/specs/folio-priceMonotonicity.spec`:
- Line 42: The auction duration bound uses 6048000 (70 days) but comments say 7
days; update the constraint in the spec that references
currentContract.auctions[id].endTime - currentContract.auctions[id].startTime to
use 604800 (7 days in seconds) if the intended limit is 7 days, or alternatively
update the accompanying comments to match 6048000 if 70 days is intended; ensure
the change is applied consistently wherever the same expression appears in
folio-priceMonotonicity.spec.
In `@certora/specs/folio-value.spec`:
- Around line 13-46: The rule totalValueOfTokenDoesNotDecrease uses an
unconstrained local uint256 price when computing tokenValue_before/after
(balanceByToken[token][currentContract] * price), so make price explicit: either
fetch the on-chain price (e.g., call the contract pricing accessor or helper to
set price = getPrice(e, token, referenceToken) before computing
tokenValue_before) or constrain the symbolic price to be the same pre/post
(assume price_before == price_after or add an assume like price >= 0 and
price_unchanged) so the comparison between shareValue_before and
shareValue_after is meaningful; update references to price where used and ensure
balanceByToken, totalSupply, shareValue_before and shareValue_after calculations
use the initialized/constrained price.
In `@certora/specs/summaries-Folio.spec`:
- Around line 1-4: The leading comment in summaries-Folio.spec is incorrect: it
claims "No summaries needed for Folio" but the file imports
"Summaries/OpenZeppelin/OZ_Math-Folio.spec",
"Summaries/PRB/PRB_Math-Folio.spec", and "Summaries/exp-nondet.spec"; update or
remove the comment to accurately reflect that these summary specs are being
imported (e.g., change the comment to state which summaries are included or
delete the misleading line) so maintainers aren't confused by the mismatch.
---
Outside diff comments:
In `@certora/patches/Folio.patch`:
- Around line 1-41: The Certora patch makes storage variables basket,
activeTrustedFill, rebalance, and activeTrustedFillFloorPrice internal (instead
of private) for verification only; update certora/README.md to explicitly state
this patch is verification-only and must never be merged into production, and
ensure the existing scripts (certora/scripts/apply-patch.sh and
certora/scripts/remove-patch.sh invoked by certora/scripts/run-all.sh) are
referenced in the README as the mechanism that applies and then reverts
certora/patches/Folio.patch so the change is always removed after Certora runs.
---
Nitpick comments:
In `@certora/harnesses/FolioHarness.sol`:
- Around line 110-115: Add an explicit guard in the getPrice function to prevent
underflow when computing auctionId: check require(nextAuctionId > 0, "no
auctions exist") before doing uint256 auctionId = nextAuctionId - 1; so the
function (getPrice) validates nextAuctionId > 0, then uses auctionId and calls
isAuctionActive(auctionId) and RebalancingLib._price(rebalance,
auctions[auctionId], sellToken, buyToken).
In `@certora/specs/folio-priceMonotonicity.spec`:
- Line 57: The error string on the require is misleading: update the message on
the require call that currently reads require startPrice < 20000 * endPrice,
"price.low >= 100 * price.high" to accurately reflect the actual constraint that
startPrice < 20000 * endPrice (i.e., startPrice / endPrice < 20000 or
"startPrice < 20000 * endPrice"); ensure the require message references
startPrice/endPrice or the 20000x ratio so it matches the constraint in the
spec.
In `@certora/specs/folio-value.spec`:
- Line 219: The rule shareRatioDoesNotDecreaseOnMintToken1 currently declares
unused parameters method f and calldataarg args but calls mint(e, args)
directly; either remove the unused parameters from the rule signature to avoid
dead variables, or change the invocation to call f(e, args) instead of mint(e,
args) so the rule generalizes to any provided method—update the rule signature
and all references accordingly (modify the rule header and replace the direct
mint(...) call with f(e, args) if you choose generalization).
- Line 242: The rules shareRatioDoesNotDecreaseOnMintToken2 and
shareRatioDoesNotDecreaseOnMintToken3 declare unused parameters "method f,
calldataarg args" but call mint(e, args) directly (like the Token1 rule); remove
the unused parameters from both rule signatures so they match the usage, update
any internal references if present, and optionally refactor
shareRatioDoesNotDecreaseOnMintToken1/2/3 into a single parameterized helper
rule that accepts the token identifier and invokes mint(e, args) to eliminate
duplication.
- Around line 150-151: Remove the two unused local variables by deleting the
declarations "uint256 sellBalanceBefore =
balanceByToken[sellToken][currentContract];" and "uint256 buyBalanceBefore =
balanceByToken[buyToken][currentContract];" from the spec; they are never
referenced elsewhere (search for sellBalanceBefore, buyBalanceBefore,
balanceByToken, currentContract) so simply remove them to clean up the rule and
run the spec checks to confirm no references remain.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro Plus
Run ID: deb1d52f-87b1-4ed7-8325-d51fba735976
📒 Files selected for processing (48)
certora/README.mdcertora/confs/folio_prerequisities.confcertora/confs/properties/P1.confcertora/confs/properties/P10.confcertora/confs/properties/P2.confcertora/confs/properties/P3-1.confcertora/confs/properties/P3-2.confcertora/confs/properties/P4-1.confcertora/confs/properties/P4-2.confcertora/confs/properties/P4-3.confcertora/confs/properties/P5_P9.confcertora/confs/properties/P6-2.confcertora/confs/properties/P6.confcertora/confs/properties/P7.confcertora/confs/properties/P8.confcertora/harnesses/FolioHarness.solcertora/harnesses/InterpolatePriceHarness.solcertora/harnesses/RebalancingLibHarness.solcertora/mocks/MockTrustedFiller.solcertora/patches/Folio.patchcertora/scripts/P1.shcertora/scripts/P10.shcertora/scripts/P2.shcertora/scripts/P3.shcertora/scripts/P4.shcertora/scripts/P5.shcertora/scripts/P6.shcertora/scripts/P7.shcertora/scripts/P8.shcertora/scripts/apply-patch.shcertora/scripts/remove-patch.shcertora/scripts/run-all.shcertora/specs/Summaries/ERC20s_CVL.speccertora/specs/Summaries/Math.speccertora/specs/Summaries/OpenZeppelin/OZ_Math-Folio.speccertora/specs/Summaries/PRB/PRB_Math-Folio.speccertora/specs/Summaries/exp-nondet.speccertora/specs/Summaries/set.speccertora/specs/folio-assumptions.speccertora/specs/folio-methods-common.speccertora/specs/folio-mockFill.speccertora/specs/folio-prerequisities.speccertora/specs/folio-priceMonotonicity.speccertora/specs/folio-priceMonotonicity2.speccertora/specs/folio-properties.speccertora/specs/folio-splittingBids.speccertora/specs/folio-value.speccertora/specs/summaries-Folio.spec
| "fillersCannotExceedTheTradedCap", | ||
| // "fillersCannotExceedTheTradedCapSimple" | ||
| ], | ||
| "rule_sanity": "none", |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Show the exact line 61 and a bit of surrounding context
FILE="certora/confs/properties/P3-2.conf"
echo "== Context around line 61 =="
nl -ba "$FILE" | sed -n '45,80p'
echo
echo "== All occurrences of rule_sanity in repo (limited output) =="
rg -n "\"rule_sanity\"\s*:\s*\"(none|basic|advanced|off|disable)\"" -S .Repository: reserve-protocol/reserve-index-dtf
Length of output: 1990
🌐 Web query:
Certora "rule_sanity" config "none" "basic" meaning
💡 Result:
In the Certora Prover, the rule_sanity configuration option controls whether the tool performs automated sanity checks—such as vacuity and trivial invariant checks—to ensure your rules are meaningful and correctly specified [1][2]. The two values have the following meanings: "basic": This setting enables standard sanity checks, including vacuity and trivial invariant checks [1]. A rule is considered vacuous if no computation paths satisfy its requirements, which can cause a rule to pass incorrectly because the assertions are never reached [3]. Using "basic" (or "advanced") is highly recommended during rule development to prevent these misleading results [4][2]. "none": This setting disables all automated rule sanity checks [1]. When this is used, the Prover does not warn you if a rule is vacuous or trivial; consequently, a vacuous rule will simply be marked as "verified" because the Prover finds no counterexamples (since there are no reachable paths where the assertion could fail) [3]. It is generally advised to use "basic" or "advanced" at all times to ensure that your verification results are valid [2].
Citations:
- 1: https://docs.certora.com/en/latest/docs/prover/checking/sanity.html
- 2: https://docs.certora.com/projects/tutorials/en/latest/lesson2_started/config_files.html
- 3: https://docs.certora.com/projects/tutorials/en/latest/lesson2_started/vacuity.html
- 4: https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=script
Re-enable Certora rule sanity checks for this property run.
certora/confs/properties/P3-2.conf sets "rule_sanity": "none", which disables vacuity/trivial sanity checks; this can cause vacuous or weakly justified proofs to be reported as verified. Change it to "basic" (or "advanced").
Suggested change
- "rule_sanity": "none",
+ "rule_sanity": "basic",📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| "rule_sanity": "none", | |
| "rule_sanity": "basic", |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/confs/properties/P3-2.conf` at line 61, The Certora property config
currently disables sanity checks by setting the "rule_sanity" key to "none";
update the "rule_sanity" setting in certora/confs/properties/P3-2.conf from
"none" to "basic" (or "advanced") so vacuity/triviality checks are enabled for
this property run and proofs aren't reported vacuously.
Comment on lines
+41
to
+42
| "msg": "P6 - priceMonotonicity at startTime", | ||
| } No newline at end of file |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Verify whether this file parses as strict JSON.
jq empty certora/confs/properties/P6-2.conf
# Expected: currently fails near Line 42; passes after removing trailing comma.Repository: reserve-protocol/reserve-index-dtf
Length of output: 142
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="certora/confs/properties/P6-2.conf"
echo "== file stats =="
wc -l "$FILE"
echo
echo "== lines 35-50 =="
nl -ba "$FILE" | sed -n '35,55p'
echo
echo "== jq parse attempt (strict JSON) =="
jq empty "$FILE" || true
echo
echo "== jq parse attempt after removing comma on the suspected msg line =="
# Remove a trailing comma specifically on the `"msg": "...",` line (best-effort; no other code changes)
perl -pe 's/("msg"\s*:\s*"P6 - priceMonotonicity at startTime"),\s*}/$1}/' "$FILE" | jq empty - || trueRepository: reserve-protocol/reserve-index-dtf
Length of output: 214
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="certora/confs/properties/P6-2.conf"
echo "== cat -n (full file) =="
cat -n "$FILE"
echo
echo "== jq parse attempt (strict JSON) =="
jq empty "$FILE" || true
echo
echo "== jq parse attempt after removing a suspected trailing comma near msg =="
# If the file is JSON-like and the only blocker is a trailing comma after the msg string,
# removing that comma should move/clear the jq error.
# Best-effort: remove a comma that appears right before a closing brace on a line containing "msg".
perl -0777 -pe 's/("msg"\s*:\s*"P6 - priceMonotonicity at startTime")\s*,(\s*})/$1$2/g' "$FILE" | jq empty - || trueRepository: reserve-protocol/reserve-index-dtf
Length of output: 2168
Fix strict-JSON parsing: remove the trailing comma in the files array
Strict JSON parsing fails because files has a trailing comma after the last element ("certora/harnesses/RebalancingLibHarness.sol",), which causes the parser error at line 8 (before ]).
Proposed fix
- "certora/harnesses/RebalancingLibHarness.sol",
+ "certora/harnesses/RebalancingLibHarness.sol"
],🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/confs/properties/P6-2.conf` around lines 41 - 42, The JSON in
certora/confs/properties/P6-2.conf has a trailing comma in the "files" array
(after "certora/harnesses/RebalancingLibHarness.sol"), which breaks strict JSON
parsing; open the P6-2.conf, locate the "files" array and remove the trailing
comma after the last entry so the array ends with ] instead of "...,", ensuring
valid JSON for the parser.
Comment on lines
+67
to
+69
| function _isTokenInDeficit(uint256 currentBalance, uint256 totalShares, uint256 limitL, uint256 weightL) internal pure returns (bool) { | ||
| return ((limitL * weightL / 1e18) * totalShares) / 1e27 > currentBalance; | ||
| } |
There was a problem hiding this comment.
🛠️ Refactor suggestion | 🟠 Major | ⚡ Quick win
Inconsistent calculation method and potential overflow.
Line 68 uses plain division operators while _isTokenInSurplus (line 48) uses Math.mulDiv with explicit rounding. The intermediate multiplication (limitL * weightL / 1e18) * totalShares could overflow before the final division by 1e27.
♻️ Align with _isTokenInSurplus implementation
function _isTokenInDeficit(uint256 currentBalance, uint256 totalShares, uint256 limitL, uint256 weightL) internal pure returns (bool) {
- return ((limitL * weightL / 1e18) * totalShares) / 1e27 > currentBalance;
+ return Math.mulDiv(Math.mulDiv(limitL, weightL, 1e18, Math.Rounding.Floor), totalShares, 1e27, Math.Rounding.Floor) > currentBalance;
}📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| function _isTokenInDeficit(uint256 currentBalance, uint256 totalShares, uint256 limitL, uint256 weightL) internal pure returns (bool) { | |
| return ((limitL * weightL / 1e18) * totalShares) / 1e27 > currentBalance; | |
| } | |
| function _isTokenInDeficit(uint256 currentBalance, uint256 totalShares, uint256 limitL, uint256 weightL) internal pure returns (bool) { | |
| return Math.mulDiv(Math.mulDiv(limitL, weightL, 1e18, Math.Rounding.Floor), totalShares, 1e27, Math.Rounding.Floor) > currentBalance; | |
| } |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/harnesses/FolioHarness.sol` around lines 67 - 69, _isTokenInDeficit
currently multiplies limitL and weightL then divides, risking overflow and
differing from _isTokenInSurplus; change the arithmetic to use Math.mulDiv with
the same rounding semantics as _isTokenInSurplus to avoid intermediate overflow.
Specifically, compute the scaled product using Math.mulDiv(limitL, weightL,
1e18, Rounding.Down) and then use Math.mulDiv(result, totalShares, 1e27,
Rounding.Down) (or mirror the exact rounding used in _isTokenInSurplus) and
compare that final value to currentBalance inside _isTokenInDeficit.
Comment on lines
+69
to
+89
| function exchange(uint256 sellAmountToExchange) external returns (uint256) { | ||
| require(sellAmountToExchange > 0, "MockTrustedFiller: invalid amount"); | ||
|
|
||
| uint256 availableSellTokens = sellToken.balanceOf(address(this)); | ||
| require(availableSellTokens >= sellAmountToExchange, "MockTrustedFiller: insufficient sell tokens"); | ||
|
|
||
| // Calculate required buy tokens using price: sellAmountToExchange * price / D27 | ||
| // {buyTok} = {sellTok} * D27{buyTok/sellTok} / D27 | ||
| uint256 requiredBuyTokens = Math.mulDiv(sellAmountToExchange, price, 1e27, Math.Rounding.Ceil); | ||
|
|
||
| // Check caller has enough buy tokens | ||
| require(buyToken.balanceOf(msg.sender) >= requiredBuyTokens, "MockTrustedFiller: insufficient caller buy tokens"); | ||
|
|
||
| // Transfer buy tokens from caller to this contract | ||
| buyToken.safeTransferFrom(msg.sender, address(this), requiredBuyTokens); | ||
|
|
||
| // Transfer sell tokens from this contract to caller | ||
| sellToken.safeTransfer(msg.sender, sellAmountToExchange); | ||
|
|
||
| return requiredBuyTokens; | ||
| } |
There was a problem hiding this comment.
Missing swapActive check allows exchange after closure.
The exchange function doesn't verify swapActive status. After closeFiller() or emergencyCloseFiller() sets swapActive = false (line 97), exchange should revert but currently doesn't, potentially allowing unintended token swaps.
🐛 Add swapActive guard
function exchange(uint256 sellAmountToExchange) external returns (uint256) {
require(sellAmountToExchange > 0, "MockTrustedFiller: invalid amount");
+ require(swapActive, "MockTrustedFiller: filler closed");📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| function exchange(uint256 sellAmountToExchange) external returns (uint256) { | |
| require(sellAmountToExchange > 0, "MockTrustedFiller: invalid amount"); | |
| uint256 availableSellTokens = sellToken.balanceOf(address(this)); | |
| require(availableSellTokens >= sellAmountToExchange, "MockTrustedFiller: insufficient sell tokens"); | |
| // Calculate required buy tokens using price: sellAmountToExchange * price / D27 | |
| // {buyTok} = {sellTok} * D27{buyTok/sellTok} / D27 | |
| uint256 requiredBuyTokens = Math.mulDiv(sellAmountToExchange, price, 1e27, Math.Rounding.Ceil); | |
| // Check caller has enough buy tokens | |
| require(buyToken.balanceOf(msg.sender) >= requiredBuyTokens, "MockTrustedFiller: insufficient caller buy tokens"); | |
| // Transfer buy tokens from caller to this contract | |
| buyToken.safeTransferFrom(msg.sender, address(this), requiredBuyTokens); | |
| // Transfer sell tokens from this contract to caller | |
| sellToken.safeTransfer(msg.sender, sellAmountToExchange); | |
| return requiredBuyTokens; | |
| } | |
| function exchange(uint256 sellAmountToExchange) external returns (uint256) { | |
| require(sellAmountToExchange > 0, "MockTrustedFiller: invalid amount"); | |
| require(swapActive, "MockTrustedFiller: filler closed"); | |
| uint256 availableSellTokens = sellToken.balanceOf(address(this)); | |
| require(availableSellTokens >= sellAmountToExchange, "MockTrustedFiller: insufficient sell tokens"); | |
| // Calculate required buy tokens using price: sellAmountToExchange * price / D27 | |
| // {buyTok} = {sellTok} * D27{buyTok/sellTok} / D27 | |
| uint256 requiredBuyTokens = Math.mulDiv(sellAmountToExchange, price, 1e27, Math.Rounding.Ceil); | |
| // Check caller has enough buy tokens | |
| require(buyToken.balanceOf(msg.sender) >= requiredBuyTokens, "MockTrustedFiller: insufficient caller buy tokens"); | |
| // Transfer buy tokens from caller to this contract | |
| buyToken.safeTransferFrom(msg.sender, address(this), requiredBuyTokens); | |
| // Transfer sell tokens from this contract to caller | |
| sellToken.safeTransfer(msg.sender, sellAmountToExchange); | |
| return requiredBuyTokens; | |
| } |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/mocks/MockTrustedFiller.sol` around lines 69 - 89, The exchange
function lacks a guard for the swapActive flag allowing swaps after
closeFiller()/emergencyCloseFiller() set swapActive = false; add an early
require in exchange (e.g., require(swapActive, "MockTrustedFiller: swap not
active")) so the function reverts when swaps are closed, placing this check near
the top of exchange before any balance reads, and ensure it uses the same error
string style as other requires in the contract.
|
|
||
| ## Folder Structure | ||
|
|
||
| ``` |
There was a problem hiding this comment.
Add a language specifier to the fenced code block.
The folder structure code block should specify a language for better rendering and accessibility. Consider using text or plaintext as the language identifier.
📝 Proposed fix
## Folder Structure
-```
+```text
certora/🧰 Tools
🪛 markdownlint-cli2 (0.22.1)
[warning] 7-7: Fenced code blocks should have a language specified
(MD040, fenced-code-language)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/README.md` at line 7, The README’s fenced code block for the folder
structure is missing a language specifier; update the opening fence (the lone
"```" that begins the certora/ folder example) to include a language identifier
such as "text" or "plaintext" so the block renders/accessibility improves (look
for the README line that contains only "```" before the "certora/" listing and
change it to "```text").
Source: Linters/SAST tools
Comment on lines
+3
to
+13
| certora/scripts/apply-patch.sh | ||
|
|
||
| certoraRun certora/confs/folio_prerequisities.conf | ||
|
|
||
| for FILE in certora/confs/properties/*.conf | ||
| do | ||
| echo ${FILE} | ||
| certoraRun ${FILE} | ||
| done | ||
|
|
||
| certora/scripts/remove-patch.sh No newline at end of file |
There was a problem hiding this comment.
Failing Certora runs are not enforced, and patch rollback is not guaranteed on early exit.
Without strict shell error handling, a failed certoraRun can be masked, and cleanup may be skipped on interruption. This can leave the repo patched and produce misleading run outcomes.
Suggested hardening patch
#!/bin/bash
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+ROOT_DIR="$(cd "${SCRIPT_DIR}/../.." && pwd)"
+cd "${ROOT_DIR}"
+
+cleanup() {
+ "${SCRIPT_DIR}/remove-patch.sh" || true
+}
+trap cleanup EXIT
-certora/scripts/apply-patch.sh
+"${SCRIPT_DIR}/apply-patch.sh"
certoraRun certora/confs/folio_prerequisities.conf
for FILE in certora/confs/properties/*.conf
do
- echo ${FILE}
- certoraRun ${FILE}
+ echo "${FILE}"
+ certoraRun "${FILE}"
done
-
-certora/scripts/remove-patch.sh📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| certora/scripts/apply-patch.sh | |
| certoraRun certora/confs/folio_prerequisities.conf | |
| for FILE in certora/confs/properties/*.conf | |
| do | |
| echo ${FILE} | |
| certoraRun ${FILE} | |
| done | |
| certora/scripts/remove-patch.sh | |
| #!/bin/bash | |
| set -euo pipefail | |
| SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" | |
| ROOT_DIR="$(cd "${SCRIPT_DIR}/../.." && pwd)" | |
| cd "${ROOT_DIR}" | |
| cleanup() { | |
| "${SCRIPT_DIR}/remove-patch.sh" || true | |
| } | |
| trap cleanup EXIT | |
| "${SCRIPT_DIR}/apply-patch.sh" | |
| certoraRun certora/confs/folio_prerequisities.conf | |
| for FILE in certora/confs/properties/*.conf | |
| do | |
| echo "${FILE}" | |
| certoraRun "${FILE}" | |
| done |
🧰 Tools
🪛 Shellcheck (0.11.0)
[info] 9-9: Double quote to prevent globbing and word splitting.
(SC2086)
[info] 10-10: Double quote to prevent globbing and word splitting.
(SC2086)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/scripts/run-all.sh` around lines 3 - 13, The script
certora/scripts/run-all.sh lacks strict shell error handling and cleanup on
early exit; enable strict mode (e.g., set -euo pipefail) at the top of
run-all.sh, add a trap to always run certora/scripts/remove-patch.sh on EXIT
(and optionally on INT/TERM) to guarantee rollback, and ensure certoraRun
failures are not masked by letting errors propagate (or capturing exit codes and
exiting non‑zero) while still invoking the trap; reference the certoraRun
invocations, the initial certora/scripts/apply-patch.sh call, the for-loop over
certora/confs/properties/*.conf, and certora/scripts/remove-patch.sh so the
changes are applied around those symbols.
Comment on lines
+74
to
+76
| address sellToken = filler.sellToken(e); | ||
| require ghostIndexes[to_bytes32(sellToken)] != 0; | ||
| address buyToken = filler.buyToken(e); |
There was a problem hiding this comment.
Systematic misuse of envfree methods with environment parameter.
Both locations call MockTrustedFiller.sellToken(e) and MockTrustedFiller.buyToken(e) passing an environment parameter, but these methods are declared envfree at lines 8-9. The root cause is inconsistent usage of the envfree interface - these methods should be called without parameters or via the direct contract reference.
🔧 Proposed fix
Apply at both locations:
- address sellToken = filler.sellToken(e);
+ address sellToken = MockTrustedFiller.sellToken();
require ghostIndexes[to_bytes32(sellToken)] != 0;
- address buyToken = filler.buyToken(e);
+ address buyToken = MockTrustedFiller.buyToken();📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| address sellToken = filler.sellToken(e); | |
| require ghostIndexes[to_bytes32(sellToken)] != 0; | |
| address buyToken = filler.buyToken(e); | |
| address sellToken = filler.sellToken(); | |
| require ghostIndexes[to_bytes32(sellToken)] != 0; | |
| address buyToken = filler.buyToken(); |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/specs/folio-mockFill.spec` around lines 74 - 76, The test calls
envfree methods with an environment parameter: replace calls to
MockTrustedFiller.sellToken(e) and MockTrustedFiller.buyToken(e) so they are
invoked without the environment argument (e.g., use filler.sellToken() and
filler.buyToken()) or call them on the direct contract reference that expects an
env parameter; update the two occurrences around variables filler and e to match
the method declaration (MockTrustedFiller.sellToken and
MockTrustedFiller.buyToken are declared envfree) so the call signatures are
consistent.
| require currentContract.auctions[id].prices[sellToken].low * 100 >= currentContract.auctions[id].prices[sellToken].high; | ||
| require currentContract.auctions[id].prices[sellToken].high <= 10^45; | ||
|
|
||
| require currentContract.auctions[id].endTime - currentContract.auctions[id].startTime <= 6048000; |
There was a problem hiding this comment.
Consistent time bound error: 6048000 seconds is 70 days, not 7 days.
Both lines constrain auction duration to 6048000 seconds with comments referencing "7 days". The correct value for 7 days is 604800 seconds (off by factor of 10). This systematic error suggests either:
- The intended limit is 7 days and the value should be
604800, or - The intended limit is 70 days and comments should be updated
🔧 Proposed fix for 7-day limit
- require currentContract.auctions[id].endTime - currentContract.auctions[id].startTime <= 6048000;
+ require currentContract.auctions[id].endTime - currentContract.auctions[id].startTime <= 604800, "auction duration limited to 7 days";- require auctionLength <= 6048000, "overapproximation - time limit for auction is 7 days";
+ require auctionLength <= 604800, "overapproximation - time limit for auction is 7 days";🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/specs/folio-priceMonotonicity.spec` at line 42, The auction duration
bound uses 6048000 (70 days) but comments say 7 days; update the constraint in
the spec that references currentContract.auctions[id].endTime -
currentContract.auctions[id].startTime to use 604800 (7 days in seconds) if the
intended limit is 7 days, or alternatively update the accompanying comments to
match 6048000 if 70 days is intended; ensure the change is applied consistently
wherever the same expression appears in folio-priceMonotonicity.spec.
Comment on lines
+13
to
+46
| rule totalValueOfTokenDoesNotDecrease(env e, calldataarg args, method f) | ||
| filtered { | ||
| f -> !f.isView && | ||
| f.selector != sig:removeFromBasket(address).selector && | ||
| f.selector != sig:bid(uint256,address,address,uint256,uint256,bool,bytes).selector && | ||
| f.selector != sig:createTrustedFill(uint256,address,address,address,bytes32).selector && | ||
| f.selector != sig:initialize(IFolio.FolioBasicDetails,IFolio.FolioAdditionalDetails,IFolio.FolioRegistryIndex,IFolio.FolioFlags,address).selector && | ||
| f.selector != sig:mint(uint256,address,uint256).selector | ||
| } | ||
| { | ||
| require e.msg.sender != currentContract; | ||
| setupAssumptionsWithAuction(e); | ||
| assumeNoTrustedFillers(); | ||
|
|
||
| address token; | ||
| require ghostIndexes[to_bytes32(token)] != 0, "the token is in the basket"; | ||
| uint256 price; | ||
| uint256 shares_before = totalSupply(e); | ||
| require shares_before > 0, "share value has to be defined"; | ||
|
|
||
| mathint tokenValue_before = balanceByToken[token][currentContract] * price; | ||
| mathint shareValue_before = tokenValue_before / shares_before; | ||
|
|
||
| // Execute function | ||
| f(e, args); | ||
|
|
||
| uint256 shares_after = totalSupply(e); | ||
| require shares_after > 0, "share value has to be defined"; | ||
|
|
||
| mathint tokenValue_after = balanceByToken[token][currentContract] * price; | ||
| mathint shareValue_after = tokenValue_after / shares_after; | ||
|
|
||
| assert shareValue_after >= shareValue_before; | ||
| } |
There was a problem hiding this comment.
Uninitialized price variable in value calculation.
The price variable declared at line 29 is never initialized or constrained. It's used in lines 33 and 42 to compute token value, but as an unconstrained symbolic value this could lead to vacuous verification.
Consider either:
- Retrieving price from contract state:
uint256 price = getPrice(e, token, referenceToken); - Constraining price to be constant before/after if the intent is price-independent verification
- Documenting why unconstrained price is appropriate for this property
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/specs/folio-value.spec` around lines 13 - 46, The rule
totalValueOfTokenDoesNotDecrease uses an unconstrained local uint256 price when
computing tokenValue_before/after (balanceByToken[token][currentContract] *
price), so make price explicit: either fetch the on-chain price (e.g., call the
contract pricing accessor or helper to set price = getPrice(e, token,
referenceToken) before computing tokenValue_before) or constrain the symbolic
price to be the same pre/post (assume price_before == price_after or add an
assume like price >= 0 and price_unchanged) so the comparison between
shareValue_before and shareValue_after is meaningful; update references to price
where used and ensure balanceByToken, totalSupply, shareValue_before and
shareValue_after calculations use the initialized/constrained price.
Comment on lines
+1
to
+4
| // No summaries needed for Folio - no matching function calls detected | ||
| import "Summaries/OpenZeppelin/OZ_Math-Folio.spec"; | ||
| import "Summaries/PRB/PRB_Math-Folio.spec"; | ||
| import "Summaries/exp-nondet.spec"; |
There was a problem hiding this comment.
Misleading comment contradicts actual imports.
Line 1 states "No summaries needed for Folio" but the file then imports three summary specifications (OZ_Math, PRB_Math, exp-nondet). This inconsistency could confuse maintainers about whether summaries are actually being used.
📝 Proposed fix to correct the comment
-// No summaries needed for Folio - no matching function calls detected
+// Summaries for Folio math operations
import "Summaries/OpenZeppelin/OZ_Math-Folio.spec";
import "Summaries/PRB/PRB_Math-Folio.spec";
import "Summaries/exp-nondet.spec";📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| // No summaries needed for Folio - no matching function calls detected | |
| import "Summaries/OpenZeppelin/OZ_Math-Folio.spec"; | |
| import "Summaries/PRB/PRB_Math-Folio.spec"; | |
| import "Summaries/exp-nondet.spec"; | |
| // Summaries for Folio math operations | |
| import "Summaries/OpenZeppelin/OZ_Math-Folio.spec"; | |
| import "Summaries/PRB/PRB_Math-Folio.spec"; | |
| import "Summaries/exp-nondet.spec"; |
🧰 Tools
🪛 RuboCop (1.87.0)
[fatal] 1-1: unexpected token tCONSTANT
(Using Ruby 2.7 parser; configure using TargetRubyVersion parameter, under AllCops)
(Lint/Syntax)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@certora/specs/summaries-Folio.spec` around lines 1 - 4, The leading comment
in summaries-Folio.spec is incorrect: it claims "No summaries needed for Folio"
but the file imports "Summaries/OpenZeppelin/OZ_Math-Folio.spec",
"Summaries/PRB/PRB_Math-Folio.spec", and "Summaries/exp-nondet.spec"; update or
remove the comment to accurately reflect that these summary specs are being
imported (e.g., change the comment to state which summaries are included or
delete the misleading line) so maintainers aren't confused by the mismatch.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR contains files for the Certora verification.
See the README.md file for the file structure and how to run the Certora prover.
Summary by CodeRabbit
Documentation
Tests