Skip to content

Commit fe21b69

Browse files
AmxxAmxx
committed
Update FV specs and run script
1 parent f9f7db0 commit fe21b69

29 files changed

+207
-304
lines changed

‎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}`);
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: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
{
2+
"files": [
3+
"certora/harnesses/AccessControlHarness.sol"
4+
],
5+
"process": "emv",
6+
"verify": "AccessControlHarness:certora/specs/AccessControl.spec"
7+
}

‎certora/specs/AccessControlDefaultAdminRules.conf

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

‎certora/specs/AccessManaged.conf

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
{
2+
"files": [
3+
"certora/harnesses/AccessManagedHarness.sol",
4+
"certora/harnesses/AccessManagerHarness.sol"
5+
],
6+
"link": [
7+
"AccessManagedHarness:_authority=AccessManagerHarness"
8+
],
9+
"optimistic_hashing": true,
10+
"optimistic_loop": true,
11+
"process": "emv",
12+
"verify": "AccessManagedHarness:certora/specs/AccessManaged.spec"
13+
}

‎certora/specs/AccessManager.conf

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

‎certora/specs/Account.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/AccountHarness.sol"
4+
],
5+
"optimistic_loop": true,
6+
"process": "emv",
7+
"verify": "AccountHarness:certora/specs/Account.spec"
8+
}

‎certora/specs/DoubleEndedQueue.conf

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

‎certora/specs/ERC20.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/ERC20PermitHarness.sol"
4+
],
5+
"optimistic_loop": true,
6+
"process": "emv",
7+
"verify": "ERC20PermitHarness:certora/specs/ERC20.spec"
8+
}

0 commit comments

Comments
 (0)