Update FV specs and script

.github/workflows/formal-verification.yml

@@ -12,7 +12,7 @@ on:
 env:
   PIP_VERSION: '3.11'
   JAVA_VERSION: '11'
-  SOLC_VERSION: '0.8.20'
+  SOLC_VERSION: '0.8.27'
 
 concurrency: ${{ github.workflow }}-${{ github.ref }}
 
@@ -64,7 +64,7 @@ jobs:
       - name: Verify specification
         run: |
           make -C certora apply
-          node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY"
+          node certora/run.js ${{ steps.arguments.outputs.result }} -p 1 -v >> "$GITHUB_STEP_SUMMARY"
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 

certora/harnesses/ERC20WrapperHarness.sol

@@ -12,18 +12,6 @@ contract ERC20WrapperHarness is ERC20Permit, ERC20Wrapper {
         string memory _symbol
     ) ERC20(_name, _symbol) ERC20Permit(_name) ERC20Wrapper(_underlying) {}
 
-    function underlyingTotalSupply() public view returns (uint256) {
-        return underlying().totalSupply();
-    }
-
-    function underlyingBalanceOf(address account) public view returns (uint256) {
-        return underlying().balanceOf(account);
-    }
-
-    function underlyingAllowanceToThis(address account) public view returns (uint256) {
-        return underlying().allowance(account, address(this));
-    }
-
     function recover(address account) public returns (uint256) {
         return _recover(account);
     }

certora/run.js

@@ -1,33 +1,25 @@
 #!/usr/bin/env node
 
 // USAGE:
-//    node certora/run.js [[CONTRACT_NAME:]SPEC_NAME]* [--all] [--options OPTIONS...] [--specs PATH]
+//    node certora/run.js [CONFIG]* [--all]
 // EXAMPLES:
 //    node certora/run.js --all
-//    node certora/run.js AccessControl
-//    node certora/run.js AccessControlHarness:AccessControl
+//    node certora/run.js ERC721
+//    node certora/run.js certora/specs/ERC721.conf
 
-import { spawn } from 'child_process';
-import { PassThrough } from 'stream';
-import { once } from 'events';
-import path from 'path';
-import yargs from 'yargs';
-import { hideBin } from 'yargs/helpers';
-import pLimit from 'p-limit';
-import fs from 'fs/promises';
+const glob = require('glob');
+const fs = require('fs');
+const pLimit = require('p-limit').default;
+const { hideBin } = require('yargs/helpers');
+const yargs = require('yargs/yargs');
+const { exec } = require('child_process');
 
-const argv = yargs(hideBin(process.argv))
+const { argv } = yargs(hideBin(process.argv))
   .env('')
   .options({
     all: {
-      alias: 'a',
       type: 'boolean',
     },
-    spec: {
-      alias: 's',
-      type: 'string',
-      default: path.resolve(import.meta.dirname, 'specs.json'),
-    },
     parallel: {
       alias: 'p',
       type: 'number',
@@ -38,131 +30,39 @@ const argv = yargs(hideBin(process.argv))
       type: 'count',
       default: 0,
     },
-    options: {
-      alias: 'o',
-      type: 'array',
-      default: [],
-    },
-  })
-  .parse();
-
-function match(entry, request) {
-  const [reqSpec, reqContract] = request.split(':').reverse();
-  return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract);
-}
-
-const specs = JSON.parse(fs.readFileSync(argv.spec, 'utf8')).filter(s => argv.all || argv._.some(r => match(s, r)));
+  });
 
+const pattern = 'certora/specs/*.conf';
 const limit = pLimit(argv.parallel);
 
 if (argv._.length == 0 && !argv.all) {
   console.error(`Warning: No specs requested. Did you forget 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 = 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 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 ? ':heavy_check_mark:' : ':x:',
-      url ? `[link](${url?.replace('/output/', '/jobStatus/')})` : 'error',
-      url ? `[link](${url})` : 'error',
+  process.exitCode = 1;
+} else {
+  Promise.all(
+    (argv.all ? glob.sync(pattern) : argv._.map(name => (fs.existsSync(name) ? name : pattern.replace('*', name)))).map(
+      (conf, i, { length }) =>
+        limit(
+          () =>
+            new Promise(resolve => {
+              if (argv.verbose) console.log(`[${i + 1}/${length}] Running ${conf}`);
+              exec(`certoraRun ${conf}`, (error, stdout, stderr) => {
+                const match = stdout.match(
+                  'https://prover.certora.com/output/[a-z0-9]+/[a-z0-9]+[?]anonymousKey=[a-z0-9]+',
+                );
+                if (error) {
+                  console.error(`[ERR] ${conf} failed with:\n${stderr || stdout}`);
+                  process.exitCode = 1;
+                } else if (match) {
+                  console.log(`${conf} - ${match[0]}`);
+                } else {
+                  console.error(`[ERR] Could not parse stdout for ${conf}:\n${stdout}`);
+                  process.exitCode = 1;
+                }
+                resolve();
+              });
+            }),
+        ),
     ),
   );
 }

certora/specs/AccessControl.conf

@@ -0,0 +1,7 @@
+{
+    "files": [
+        "certora/harnesses/AccessControlHarness.sol"
+    ],
+    "process": "emv",
+    "verify": "AccessControlHarness:certora/specs/AccessControl.spec"
+}

certora/specs/AccessControlDefaultAdminRules.conf

@@ -0,0 +1,7 @@
+{
+    "files": [
+        "certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"
+    ],
+    "process": "emv",
+    "verify": "AccessControlDefaultAdminRulesHarness:certora/specs/AccessControlDefaultAdminRules.spec"
+}

certora/specs/AccessManaged.conf

@@ -0,0 +1,13 @@
+{
+    "files": [
+        "certora/harnesses/AccessManagedHarness.sol",
+        "certora/harnesses/AccessManagerHarness.sol"
+    ],
+    "link": [
+        "AccessManagedHarness:_authority=AccessManagerHarness"
+    ],
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "process": "emv",
+    "verify": "AccessManagedHarness:certora/specs/AccessManaged.spec"
+}

certora/specs/AccessManager.conf

@@ -0,0 +1,9 @@
+{
+    "files": [
+        "certora/harnesses/AccessManagerHarness.sol"
+    ],
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "process": "emv",
+    "verify": "AccessManagerHarness:certora/specs/AccessManager.spec"
+}