vacp2p
/
rln-contract
mirror of https://github.com/vacp2p/rln-contract.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

incl: certora spec

This commit is contained in:
rymnc 2023-12-05 14:37:05 +05:30
parent 46a7dc5d64
commit 443cbfc9c4
No known key found for this signature in database
GPG Key ID: AAA088D5C68ECD34
3 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
certora/certora.conf
View File

@ -1,8 +1,8 @@
{ {
"files": ["src/Foo.sol"], "files": ["src/Rln.sol"],
"msg": "Verifying Foo.sol", "msg": "Verifying Rln.sol",
"rule_sanity": "basic", "rule_sanity": "basic",
"verify": "Foo:certora/specs/Foo.spec", "verify": "Rln:certora/specs/Rln.spec",
"wait_for_results": "all", "wait_for_results": "all",
} }

9
certora/specs/Foo.spec
View File

@ -1,9 +0,0 @@
methods {
function id(uint256) external returns (uint256) envfree;
}
rule checkIdOutputIsAlwaysEqualToInput {
uint256 input;
assert id(input) == input;
}

9
certora/specs/Rln.spec Normal file
View File

@ -0,0 +1,9 @@
methods {
function root() external returns (uint256) envfree;
}
rule checkDefaultRootIsCorrect {
uint256 defaultRoot = 15019797232609675441998260052101280400536945603062888308240081994073687793470;
assert root() == input;
}