1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
#!/usr/bin/env node
// USAGE:
// node certora/run.js [[CONTRACT_NAME:]SPEC_NAME]* [--all] [--options OPTIONS...] [--specs PATH]
// EXAMPLES:
// node certora/run.js --all
// node certora/run.js AccessControl
// node certora/run.js AccessControlHarness:AccessControl
const proc = require('child_process');
const { PassThrough } = require('stream');
const events = require('events');
const argv = require('yargs')
.env('')
.options({
all: {
alias: 'a',
type: 'boolean',
},
spec: {
alias: 's',
type: 'string',
default: __dirname + '/specs.json',
},
parallel: {
alias: 'p',
type: 'number',
default: 4,
},
verbose: {
alias: 'v',
type: 'count',
default: 0,
},
options: {
alias: 'o',
type: 'array',
default: [],
},
}).argv;
function match(entry, request) {
const [reqSpec, reqContract] = request.split(':').reverse();
return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract);
}
const specs = require(argv.spec).filter(s => argv.all || argv._.some(r => match(s, r)));
const limit = require('p-limit')(argv.parallel);
if (argv._.length == 0 && !argv.all) {
console.error(`Warning: No specs requested. Did you forgot to toggle '--all'?`);
}
for (const r of argv._) {
if (!specs.some(s => match(s, r))) {
console.error(`Error: Requested spec '${r}' not found in ${argv.spec}`);
process.exitCode = 1;
}
}
if (process.exitCode) {
process.exit(process.exitCode);
}
for (const { spec, contract, files, options = [] } of specs) {
limit(
runCertora,
spec,
contract,
files,
[...options, ...argv.options].flatMap(opt => opt.split(' ')),
);
}
// Run certora, aggregate the output and print it at the end
async function runCertora(spec, contract, files, options = []) {
const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options];
if (argv.verbose) {
console.log('Running:', args.join(' '));
}
const child = proc.spawn('certoraRun', args);
const stream = new PassThrough();
const output = collect(stream);
child.stdout.pipe(stream, { end: false });
child.stderr.pipe(stream, { end: false });
// as soon as we have a job id, print the output link
stream.on('data', function logStatusUrl(data) {
const { '-DjobId': jobId, '-DuserId': userId } = Object.fromEntries(
data
.toString('utf8')
.match(/-D\S+=\S+/g)
?.map(s => s.split('=')) || [],
);
if (jobId && userId) {
console.error(`[${spec}] https://prover.certora.com/output/${userId}/${jobId}/`);
stream.off('data', logStatusUrl);
}
});
// wait for process end
const [code, signal] = await events.once(child, 'exit');
// error
if (code || signal) {
console.error(`[${spec}] Exited with code ${code || signal}`);
process.exitCode = 1;
}
// get all output
stream.end();
// write results in markdown format
writeEntry(spec, contract, code || signal, (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]);
// write all details
console.error(`+ certoraRun ${args.join(' ')}\n` + (await output));
}
// Collects stream data into a string
async function collect(stream) {
const buffers = [];
for await (const data of stream) {
const buf = Buffer.isBuffer(data) ? data : Buffer.from(data);
buffers.push(buf);
}
return Buffer.concat(buffers).toString('utf8');
}
// Formatting
let hasHeader = false;
function formatRow(...array) {
return ['', ...array, ''].join(' | ');
}
function writeHeader() {
console.log(formatRow('spec', 'contract', 'result', 'status', 'output'));
console.log(formatRow('-', '-', '-', '-', '-'));
}
function writeEntry(spec, contract, success, url) {
if (!hasHeader) {
hasHeader = true;
writeHeader();
}
console.log(
formatRow(
spec,
contract,
success ? ':x:' : ':heavy_check_mark:',
url ? `[link](${url?.replace('/output/', '/jobStatus/')})` : 'error',
url ? `[link](${url})` : 'error',
),
);
}