Pyrometer Enters Beta

As of today, Pyrometer enters beta. This release marks a significant increase in stability and Solidity language parity relative to the alpha version. This means it will now work on most codebases to help developers and auditors understand and find issues in their Solidity code.

This post will walk through some of the core ideas behind Pyrometer, an example of how you can use it today, and what to expect to see from the tool in the future.

What is Pyrometer?

‍
Pyrometer, in its current form, is a tool to assist in verifying Solidity functions do what the developer thinks they do. It helps developers and auditors during the review process to understand Solidity code and edge cases. It does this by showcasing how variables change throughout a function or functions.

Pyrometer "executes" Solidity code in an abstract manner, leveraging concepts from abstract interpretation, symbolic execution, and static analysis. This allows the tool to discover and show how all branches of code are reachable, and what constraints are required to execute that branch of code.

This release is primarily targeted for improved stability. Not many fancy features to announce just yet (stay tuned!), but it is a chance to highlight that Pyrometer is ready to be used by a wider group of developers and auditors.

The Analysis

As a primer, these are the basics of Pyrometer's analysis. When Pyrometer analyzes code, the user will see a few different kinds of output:
1. Concrete Values
2. Dynamic (Relational) Values
3. Expression Values
4. Range Dynamic Values

Concrete

‍
A concrete value is a `bytesX`, `address`, or number like `1` or `2`. For example:

uint256 x = 2;
──────┬──────
      ╰──────── "x" == 2 // This is output from Pyrometer

Dynamic

‍
This is a relational value, like `y`. For example:

x = y;
┬
╰── "x" == y // This is output from Pyrometer

Expression

This is a combination of other elements. For example:

x = y + 1;
┬
╰────── "x" == (y + 1) // This is output from Pyrometer

‍

Range Dynamic

A RangeDynamic consists of a length and a mapping of indices to values of elements. For example:

x[1] = y + 1;
──────┬─────
      ╰─────── Memory var "x[1]" == (y + 1)
      │
      ╰─────── Memory var "x" ∈ [ {len: 0, indices: {1: (y + 1)}}, {len: 2**256 - 1, indices: {1: (y + 1)}} ]

Each variable has a range of possible values represented by a minimum and a maximum, each being one of the element types above.

Application

‍
As an example of how to use the tool, we will look at verifying a single function from solmate's  ERC4626 implementation: convertToShares.

function convertToShares(uint256 assets) public view virtual returns (uint256) {
	uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero.

	return supply == 0 ? assets : assets.mulDivDown(supply, totalAssets());
}

Here is the function from the `FixedPointMathLib.sol` used in the calculation:

function mulDivDown(
	uint256 x,
	uint256 y,
	uint256 denominator
) internal pure returns (uint256 z) {
	/// @solidity memory-safe-assembly
	assembly {
		// Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y))
		if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT256, y)))))) {
			revert(0, 0)
		}

		// Divide x * y by the denominator.
		z := div(mul(x, y), denominator)
	}
}

Take note of this comment: `Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y))`; Pyrometer can be used to prove it*.

*manually - automatic proofs are an area of research we are exploring.

Pyrometer will output two branches, one in which it assumes `supply` is 0, and one in which it assumes it is not 0. In this example, most of the time we will examine with evaluation on. This means that all relational elements are concretized into real values. We will examine the unevaluated bounds as needed.

Here is where it assumes `totalSupply` is 0 (verbosity is set to 2 or 3 throughout this example):

Bounds: Bounds for function: function convertToShares(uint256)
Bounds: Bounds for subcontext: convertToShares(uint256).fork{ true } where:
1. (supply == 0) == true
function convertToShares(uint256 assets) public view virtual returns (uint256) {
                         ───────┬──────
                                ╰──────── "assets" ∈ [ 0, 2**256 - 1 ]
    uint256 supply = totalSupply;
    ──────────────┬───────┬─────
                  ╰───────┼── "supply" ∈ [ 0, 2**256 - 1 ]
                          │
                          ╰── Storage var "totalSupply" ∈ [ 0, 2**256 - 1 ]

    return supply == 0 ? assets : assets.mulDivDown(supply, totalAssets());
    ────────────┬──────────────────────┬──────────────────────────────────
                ╰──────────────────────┼─ "supply" == 0
                                       │
                                       ╰─ returns: "assets" ∈ [ 0, 2**256 - 1 ]
}

Here is the output where it assumes it is not 0:

Bounds: Bounds for subcontext: convertToShares(uint256).fork{ false }.totalAssets().resume{ convertToShares(uint256) }.mulDivDown(uint256, uint256, uint256).fork{ false }.resume{ convertToShares(uint256) } where:
1. ((denominator * (y * x > (MAX_UINT256 / y)) == 0) == 0 == 0 > 0) == true
2. (supply != 0) == true

function convertToShares(uint256 assets) public view virtual returns (uint256) {

    return supply == 0 ? assets : assets.mulDivDown(supply, totalAssets());
    ────────────┬──────────────────────┬──────────────────────────────────
                ╰──────────────────────┼─ "supply" == totalSupply && ∉ { == 0}
                                       │
                                       ╰─ returns: "mulDivDown(uint256, uint256, uint256).0" ∈ [ 0, 2**256 - 1 ]}


	uint256 x,
	────┬────
	    ╰────── "x" ∈ [ 0, 2**256 - 1 ]
	uint256 y,
	────┬────
	    ╰────── "y" ∈ [ 0, 2**256 - 1 ] && ∉ { == 0}
	uint256 denominator
	─────────┬─────────
	         ╰─────────── "denominator" ∈ [ 0, 2**256 - 1 ]
  ) internal pure returns (uint256 z) {
                     ────┬────
                         ╰─ returns: "z" ∈ [ 0, 2**256 - 1 ]

	if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT256, y)))))) {
	 ──────────────────────────────────┬─────────────────────────────────
	                                   ╰─ "denominator" ∈ [ 1, 2**256 - 1 ]
	                                   │
	                                   ╰─ "(y * x > (MAX_UINT256 / y))" ∈ [ 1, 2**256 - 1 ] && ∉ { == 0}
	                                   │
	                                   ╰─ "(denominator * (y * x > (MAX_UINT256 / y)) == 0)" ∈ [ 1, 2**256 - 1 ]
	                                   │
	                                   ╰─ "y" ∈ [ 1, 2**256 - 1 ] && ∉ { == 0}
	
}

Now recall the comment: `Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y))`. By default it shows only non-reverting branches, and as you can see, `denominator`'s range is 1 to type(uint256).max in the only non-reverting branch! Therefore, we have verified part of this comment. We can also turn evaluation off which gives us:

  if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT256, y)))))) {
  ──────────────────────────────────┬─────────────────────────────────
                                    ╰─────────────────────────────────── "denominator" ∈ [ max((uint256(0)), ((((0 != 0) != 0) / (y * x > (MAX_UINT256 / y)) == 0) + 1)), uint256(2**256 - 1) ]

This output is a little complicated (PRs welcome! it would be great to simplify the expression), but it shows the math behind the minimum range calculation resulting in `1` being the minimum value of `denominator`.

Additionally, `y`'s unevaluated range is (keep in mind this is in assembly, so `true` and `false` are `1` and `0`, respectively):

"y" ∈ [ max((uint256(totalSupply)), ((((((0 != 0) != 0) / denominator) != 0) / x > (MAX_UINT256 / y)) + 1)), uint256(totalSupply) ] && ∉ { == 0}

The tool has told us that so far the assembly *is* equivalent to `require(denominator != 0)`, and since `y` cannot be 0 in this branch (due to `supply == 0 ? assets : ...`), we just need to verify the `x <= MAX_UINT256/ y` statement. We see this verified in the output:

"(y * x > (MAX_UINT256 / y))" ∈ [ 1, 2**256 - 1 ] && ∉ { == 0}

‍
`y` is guaranteed to be 1, so `x > (MAX_UINT256 / y)` is guaranteed to be true in this branch as well. Thus, we have successfully used Pyrometer to verify that `mulDivDown` acts as expected, reverting in the appropriate cases.

Looking back at the `convertToShares` with evaluation off, we see:

returns: "mulDivDown(uint256, uint256, uint256).0" == ((x * y) / denominator)

where `x` is `assets`, `y` is `totalSupply`, and `denominator` is `totalAssets()` (in future versions, this mapping will be inlined in the output).

We effectively just abstracted all of `mulDivDown` into a single line of easily digestible code, from a confusing set of assembly instructions!

While that was relatively complicated to explain, once familiarized with the output of the tool, things move quickly. Most of the time, a developer or auditor will be able to spot a weird output just by looking at the 0 verbosity setting.

Hopefully this gives a sense of how to intergrate Pyrometer into your development workflow today. It can be a fantastic tool in the developer and auditor toolbelt to help analyze what the code is actually doing. But where the tool is going is even more exciting.

The Future

‍
This beta release is focused on stability, and mostly consists of the codebase going from being held together by glue (the alpha version) into something with strong foundations for building world class tooling.

Automated Analyses

‍
We are exploring using Cypher, a graph query language, for writing analyses (or another graph query language, and no, GraphQL is not a graph query language). This would allow for powerful querying of the structure of the contract and its variables. For example, here is a potential taint analysis query (note: this is not actually valid `cypher`):

 MATCH (x:Variable) -[:FunctionReturn { external: true }]-> (y:Variable)
 (y:Variable) -[:(!Require || !Assert) ]-> (y:Variable)
 return (x, y)
 

‍

In English, this says "find all variables (y) that are the result of an external function call (x) that aren't proceeded by either a require or assert." This would showcase any variables that aren't validated after an external call. This is still in the design phase, so feedback is requested.

Another example is a feature that was actually removed from this release: access control queries. Recall that in the Pyrometer announcement post, we showcased an access control query. It was removed from the beta due to many structural changes and rethinking on the scalability of writing automated analyses, but may be added back in the comes days/weeks. In the future, this query could be:

 MATCH (x:Variable) -[:StorageWrite]-> (storageVar:Variable) -[:Context]-> (z:Context) -[:Constraints]-> (constraints:Variable)
 return (storageVar, constraints)
 

This would return a storage write and the corresponding constraints accumulated to perform that storage write, bringing clarity to developers as to who and how state can be written.

This is all possible thanks to the graph intermediate representation used under the hood.

Foundry Fuzzer

Building on the idea of constraints accumulating in a function context (i.e. `x < 100 && y < 500` that appear at the top of each output section), research in being done on using this information to improve the Foundry fuzzer.

Currently, the fuzzer makes some informed guesses as to interesting values by reading the bytecode of the contract, but it has no conception of relations between variables, so a code branch from a statement like `if (x < 1000 - y) { .. }` may never been reached because the fuzzer lacks sophistication. The current approach being explored leverages the constraints generated by running the tool on a contract. These constraints are then used to generate values which are fed into the fuzzer as function inputs. This should enable significantly improved code coverage.

There are other ideas we are exploring, but we also encourage you to hop in the Pyrometer Telegram and start building on top of Pyrometer as well! There are a ton of ideas and awesome tools to be built on top of this and we would love to connect, ideate, and build along with you.

Back to building...

Go try Pyrometer out on your contracts today! Installation and usage instructions are on the github. If you run into issues, open an issue!

And finally, a huge thank you to @plotchy for being a thought partner and collaborator throughout the development process - the tool would not be where it is without you.

‍