Skip to content

Commit 0950257

Browse files
renovate[bot]Amxxernestognwjames-toussaint
authored
Update dependency certora-cli to v8 (#5844)
Co-authored-by: Hadrien Croubois <[email protected]> Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com> Co-authored-by: ernestognw <[email protected]> Co-authored-by: James Toussaint <[email protected]>
1 parent 3d479dc commit 0950257

36 files changed

+604
-488
lines changed

‎.github/workflows/formal-verification.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ on:
1212
env:
1313
PIP_VERSION: '3.11'
1414
JAVA_VERSION: '11'
15-
SOLC_VERSION: '0.8.20'
15+
SOLC_VERSION: '0.8.27'
1616

1717
concurrency: ${{ github.workflow }}-${{ github.ref }}
1818

@@ -64,7 +64,7 @@ jobs:
6464
- name: Verify specification
6565
run: |
6666
make -C certora apply
67-
node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY"
67+
node certora/run.js ${{ steps.arguments.outputs.result }} -p 1 -v >> "$GITHUB_STEP_SUMMARY"
6868
env:
6969
CERTORAKEY: ${{ secrets.CERTORAKEY }}
7070

‎certora/diff/token_ERC721_ERC721.sol.patch‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
--- token/ERC721/ERC721.sol 2025-08-19 17:23:33.436823903 +0200
2+
+++ token/ERC721/ERC721.sol 2025-08-19 17:23:07.328925282 +0200
3+
@@ -27,7 +27,7 @@
4+
5+
mapping(uint256 tokenId => address) private _owners;
6+
7+
- mapping(address owner => uint256) private _balances;
8+
+ mapping(address owner => uint256) internal _balances; // private → internal for FV
9+
10+
mapping(uint256 tokenId => address) private _tokenApprovals;
11+

‎certora/harnesses/ERC20WrapperHarness.sol‎

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,18 +12,6 @@ contract ERC20WrapperHarness is ERC20Permit, ERC20Wrapper {
1212
string memory _symbol
1313
) ERC20(_name, _symbol) ERC20Permit(_name) ERC20Wrapper(_underlying) {}
1414

15-
function underlyingTotalSupply() public view returns (uint256) {
16-
return underlying().totalSupply();
17-
}
18-
19-
function underlyingBalanceOf(address account) public view returns (uint256) {
20-
return underlying().balanceOf(account);
21-
}
22-
23-
function underlyingAllowanceToThis(address account) public view returns (uint256) {
24-
return underlying().allowance(account, address(this));
25-
}
26-
2715
function recover(address account) public returns (uint256) {
2816
return _recover(account);
2917
}

‎certora/harnesses/ERC721Harness.sol‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,10 @@ contract ERC721Harness is ERC721 {
2323
_burn(tokenId);
2424
}
2525

26+
function unsafeBalanceOf(address owner) public view returns (uint256) {
27+
return _balances[owner];
28+
}
29+
2630
function unsafeOwnerOf(uint256 tokenId) external view returns (address) {
2731
return _ownerOf(tokenId);
2832
}

‎certora/run.js‎

Lines changed: 38 additions & 138 deletions
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,25 @@
11
#!/usr/bin/env node
22

33
// USAGE:
4-
// node certora/run.js [[CONTRACT_NAME:]SPEC_NAME]* [--all] [--options OPTIONS...] [--specs PATH]
4+
// node certora/run.js [CONFIG]* [--all]
55
// EXAMPLES:
66
// node certora/run.js --all
7-
// node certora/run.js AccessControl
8-
// node certora/run.js AccessControlHarness:AccessControl
7+
// node certora/run.js ERC721
8+
// node certora/run.js certora/specs/ERC721.conf
99

10-
import { spawn } from 'child_process';
11-
import { PassThrough } from 'stream';
12-
import { once } from 'events';
13-
import path from 'path';
14-
import yargs from 'yargs';
15-
import { hideBin } from 'yargs/helpers';
16-
import pLimit from 'p-limit';
17-
import fs from 'fs/promises';
10+
const glob = require('glob');
11+
const fs = require('fs');
12+
const pLimit = require('p-limit').default;
13+
const { hideBin } = require('yargs/helpers');
14+
const yargs = require('yargs/yargs');
15+
const { exec } = require('child_process');
1816

19-
const argv = yargs(hideBin(process.argv))
17+
const { argv } = yargs(hideBin(process.argv))
2018
.env('')
2119
.options({
2220
all: {
23-
alias: 'a',
2421
type: 'boolean',
2522
},
26-
spec: {
27-
alias: 's',
28-
type: 'string',
29-
default: path.resolve(import.meta.dirname, 'specs.json'),
30-
},
3123
parallel: {
3224
alias: 'p',
3325
type: 'number',
@@ -38,131 +30,39 @@ const argv = yargs(hideBin(process.argv))
3830
type: 'count',
3931
default: 0,
4032
},
41-
options: {
42-
alias: 'o',
43-
type: 'array',
44-
default: [],
45-
},
46-
})
47-
.parse();
48-
49-
function match(entry, request) {
50-
const [reqSpec, reqContract] = request.split(':').reverse();
51-
return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract);
52-
}
53-
54-
const specs = JSON.parse(fs.readFileSync(argv.spec, 'utf8')).filter(s => argv.all || argv._.some(r => match(s, r)));
33+
});
5534

35+
const pattern = 'certora/specs/*.conf';
5636
const limit = pLimit(argv.parallel);
5737

5838
if (argv._.length == 0 && !argv.all) {
5939
console.error(`Warning: No specs requested. Did you forget to toggle '--all'?`);
60-
}
61-
62-
for (const r of argv._) {
63-
if (!specs.some(s => match(s, r))) {
64-
console.error(`Error: Requested spec '${r}' not found in ${argv.spec}`);
65-
process.exitCode = 1;
66-
}
67-
}
68-
69-
if (process.exitCode) {
70-
process.exit(process.exitCode);
71-
}
72-
73-
for (const { spec, contract, files, options = [] } of specs) {
74-
limit(() =>
75-
runCertora(
76-
spec,
77-
contract,
78-
files,
79-
[...options, ...argv.options].flatMap(opt => opt.split(' ')),
80-
),
81-
);
82-
}
83-
84-
// Run certora, aggregate the output and print it at the end
85-
async function runCertora(spec, contract, files, options = []) {
86-
const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options];
87-
if (argv.verbose) {
88-
console.log('Running:', args.join(' '));
89-
}
90-
const child = spawn('certoraRun', args);
91-
92-
const stream = new PassThrough();
93-
const output = collect(stream);
94-
95-
child.stdout.pipe(stream, { end: false });
96-
child.stderr.pipe(stream, { end: false });
97-
98-
// as soon as we have a job id, print the output link
99-
stream.on('data', function logStatusUrl(data) {
100-
const { '-DjobId': jobId, '-DuserId': userId } = Object.fromEntries(
101-
data
102-
.toString('utf8')
103-
.match(/-D\S+=\S+/g)
104-
?.map(s => s.split('=')) || [],
105-
);
106-
107-
if (jobId && userId) {
108-
console.error(`[${spec}] https://prover.certora.com/output/${userId}/${jobId}/`);
109-
stream.off('data', logStatusUrl);
110-
}
111-
});
112-
113-
// wait for process end
114-
const [code, signal] = await once(child, 'exit');
115-
116-
// error
117-
if (code || signal) {
118-
console.error(`[${spec}] Exited with code ${code || signal}`);
119-
process.exitCode = 1;
120-
}
121-
122-
// get all output
123-
stream.end();
124-
125-
// write results in markdown format
126-
writeEntry(spec, contract, code || signal, (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]);
127-
128-
// write all details
129-
console.error(`+ certoraRun ${args.join(' ')}\n` + (await output));
130-
}
131-
132-
// Collects stream data into a string
133-
async function collect(stream) {
134-
const buffers = [];
135-
for await (const data of stream) {
136-
const buf = Buffer.isBuffer(data) ? data : Buffer.from(data);
137-
buffers.push(buf);
138-
}
139-
return Buffer.concat(buffers).toString('utf8');
140-
}
141-
142-
// Formatting
143-
let hasHeader = false;
144-
145-
function formatRow(...array) {
146-
return ['', ...array, ''].join(' | ');
147-
}
148-
149-
function writeHeader() {
150-
console.log(formatRow('spec', 'contract', 'result', 'status', 'output'));
151-
console.log(formatRow('-', '-', '-', '-', '-'));
152-
}
153-
154-
function writeEntry(spec, contract, success, url) {
155-
if (!hasHeader) {
156-
hasHeader = true;
157-
writeHeader();
158-
}
159-
console.log(
160-
formatRow(
161-
spec,
162-
contract,
163-
success ? ':heavy_check_mark:' : ':x:',
164-
url ? `[link](${url?.replace('/output/', '/jobStatus/')})` : 'error',
165-
url ? `[link](${url})` : 'error',
40+
process.exitCode = 1;
41+
} else {
42+
Promise.all(
43+
(argv.all ? glob.sync(pattern) : argv._.map(name => (fs.existsSync(name) ? name : pattern.replace('*', name)))).map(
44+
(conf, i, { length }) =>
45+
limit(
46+
() =>
47+
new Promise(resolve => {
48+
if (argv.verbose) console.log(`[${i + 1}/${length}] Running ${conf}`);
49+
exec(`certoraRun ${conf}`, (error, stdout, stderr) => {
50+
const match = stdout.match(
51+
'https://prover.certora.com/output/[a-z0-9]+/[a-z0-9]+[?]anonymousKey=[a-z0-9]+',
52+
);
53+
if (error) {
54+
console.error(`[ERR] ${conf} failed with:\n${stderr || stdout}`);
55+
process.exitCode = 1;
56+
} else if (match) {
57+
console.log(`${conf} - ${match[0]}`);
58+
} else {
59+
console.error(`[ERR] Could not parse stdout for ${conf}:\n${stdout}`);
60+
process.exitCode = 1;
61+
}
62+
resolve();
63+
});
64+
}),
65+
),
16666
),
16767
);
16868
}

‎certora/specs.json‎

Lines changed: 0 additions & 110 deletions
This file was deleted.

‎certora/specs/AccessControl.conf‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
{
2+
"files": [
3+
"certora/harnesses/AccessControlHarness.sol"
4+
],
5+
"process": "emv",
6+
"url_visibility": "public",
7+
"verify": "AccessControlHarness:certora/specs/AccessControl.spec"
8+
}

‎certora/specs/AccessControlDefaultAdminRules.conf‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
{
2+
"files": [
3+
"certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"
4+
],
5+
"process": "emv",
6+
"url_visibility": "public",
7+
"verify": "AccessControlDefaultAdminRulesHarness:certora/specs/AccessControlDefaultAdminRules.spec"
8+
}

0 commit comments

Comments
 (0)