2.2 SPDX & Pragmas

SPDX

One of the things that you will often see specified at the top of every Solidity file is what is known as the SPDX license identifier. SPDX stands for Software Package Data Exchange. In the case of Solidity it's a comment that indicates its license and it is specified as a best practice to be at the top of every file. An example looks like this

// SPDX-License-Identifier: AGPLv3

The specific license obviously depends on what the developer intends for the particular smart contract. This identifier (i.e. the license) is included by the compiler in the byte code metadata that is generated, so it becomes machine readable.

Pragma

The pragma keyword in Solidity is used to enable certain compiler features or compiler checks. An example looks something like this

pragma solidity ^0.8.0;

At a high level, there are two types of pragmas:

The first kind specifies the version. There are, again, two types of versions that can be specified:\
a. The version pragma, which indicates the specific Solidity compiler version that the developer expects to be used for that source file, and it looks like\
```
pragma solidity x.y.z;
```
where x, y and z are numerals that specify that compiler version.\
This does not change the version of the compiler used nor enables or disables any features of the compiler. All it does is instructing the compiler at compilation time to check whether its version matches the one specified by the developer. This could be of several formats: it could be a very simple format, a complex one or even a floating one (which has some security implications).\
The latest Solidity compiler versions as of now are in the 0.8 range with a different z in the pragma directive. If you look at x.y.z; a different z indicates bug fixes and a different y indicates breaking changes between the compiler versions.\
So if we have compiler versions in the 0.5 range, then by looking at the 0.6 range it means that the 0.6.z range has at least one or more breaking changes compared to the previous versions.\
A floating pragma is a pragma that has a caret symbol (^) prefixed to x.y.z in the directive. This indicates that the contract can be compiled with versions starting with x.y.z all the way until x.(y + 1).z. So, as an example, consider\
```
pragma solidity ^0.8.3;
```
It indicates that the source file can be compiled with any compiler version starting from 0.8.3 going to 0.8.4, 0.8.5 and whatever else has been released; but not 0.9.z, so the transition from 0.8 to 0.9 is what is prevented by this floating platform.\
This allows the developer to specify a range of compiler versions that can be used with a particular contract, and that has some security implications similar to the floating pragma.\
A range of compiler versions can be indicated with a complex practice, where you have >, >=, <, <= symbols that are used to combine multiple versions of the Solidity compiler.\
This affects the compiler version, which in turn brings in different features that are implemented by said version. Some of those could be security features, others could be security bug fixes or optimizations.\
All these aspects affect the security posture of the bytecode that is generated from a particular smart contract.\
b. The ABI coder pragma. This directive allows a developer to specify the choice between Version 1 or Version 2 ABI coder.\
The newer Version 2 was considered experimental for a while, but is now activated by default and allows the encoding/decoding of nested arrays and structs.\
You might encounter old Solidity source code using the old directive, such as shown below\
```
pragma experimental ABIEncoderV2;
```
Version 2 is a strict superset of Version 1: contracts that use Version 2 can interact with other contracts that do not use it without any concern or limitations.\
This pragma also applies to the code defined in the file where it is activated, regardless of where that code ends up eventually; what this means is that a contract whose file is using Version 1 can still contain code that uses Version 2 by inheriting it from another contract. An example of ABI Coder pragma statement is\
```
pragma abicoder v1; // or v2, which is the default from version 0.8.z onwards
```
The ABI coder affects encoding and decoding. The optimizations it does have certain security implications.
The second pragma directive helps the developer to specify features that are considered experimental as of that point in time.\
These features are not enabled by default and have to be explicitly specified as part of this pragma directive and within every file where it is required. As of now there is only one experimental feature, which is known as SMTChecker.\
```
pragma experimental SMTChecker;
```
SMT stands for Satisfiability Modulo Theory which is an approach to formal verification, and in the case of Solidity it is used to implement safety checks by what is known as querying an SMT solver.\
There are various security checks performed by the SMT checker. The first one is where it uses the require and assert statements that are included as part of the smart contract.\
The checker considers all the required statements specified as assumptions by the developer and it tries to prove that the conditions inside the assert statements are true.\
If a failure can be established, then the checker provides what is known as a counter example that shows the user how this assertion can fail.\
There are various other checks that have been added to this empty checker over time. These include the arithmetic overflow, underflow, division by zero, unreachable code and so on.\
So SMT checker is a critical security feature that comes packaged as part of Solidity. It's implemented in the compiler itself.\
Formal verification is considered as a fundamental part of programming languages' security, so we can imagine that this particular pragma directive affects the security and optimizations of the smart contracts that use them.

What needs to be kept in mind with the pragma directives is that they are local to the files where they are specified. So if you have a Solidity file that imports other files, the pragmas from the imported files do not automatically carry over to the file that is of concern.

Previous2.1 Solidity: Influence, Features & Layout Next2.3 Imports

Last updated 1 year ago

SPDX

// SPDX-License-Identifier: AGPLv3

Pragma

The pragma keyword in Solidity is used to enable certain compiler features or compiler checks. An example looks something like this

pragma solidity ^0.8.0;

At a high level, there are two types of pragmas:

The first kind specifies the version. There are, again, two types of versions that can be specified:\

a. The version pragma, which indicates the specific Solidity compiler version that the developer expects to be used for that source file, and it looks like\

pragma solidity x.y.z;

where x, y and z are numerals that specify that compiler version.\

This does not change the version of the compiler used nor enables or disables any features of the compiler. All it does is instructing the compiler at compilation time to check whether its version matches the one specified by the developer. This could be of several formats: it could be a very simple format, a complex one or even a floating one (which has some security implications).\

The latest Solidity compiler versions as of now are in the 0.8 range with a different z in the pragma directive. If you look at x.y.z; a different z indicates bug fixes and a different y indicates breaking changes between the compiler versions.\

So if we have compiler versions in the 0.5 range, then by looking at the 0.6 range it means that the 0.6.z range has at least one or more breaking changes compared to the previous versions.\

A floating pragma is a pragma that has a caret symbol (^) prefixed to x.y.z in the directive. This indicates that the contract can be compiled with versions starting with x.y.z all the way until x.(y + 1).z. So, as an example, consider\

pragma solidity ^0.8.3;

It indicates that the source file can be compiled with any compiler version starting from 0.8.3 going to 0.8.4, 0.8.5 and whatever else has been released; but not 0.9.z, so the transition from 0.8 to 0.9 is what is prevented by this floating platform.\

This allows the developer to specify a range of compiler versions that can be used with a particular contract, and that has some security implications similar to the floating pragma.\

A range of compiler versions can be indicated with a complex practice, where you have >, >=, <, <= symbols that are used to combine multiple versions of the Solidity compiler.\

This affects the compiler version, which in turn brings in different features that are implemented by said version. Some of those could be security features, others could be security bug fixes or optimizations.\

All these aspects affect the security posture of the bytecode that is generated from a particular smart contract.\

b. The ABI coder pragma. This directive allows a developer to specify the choice between Version 1 or Version 2 ABI coder.\

The newer Version 2 was considered experimental for a while, but is now activated by default and allows the encoding/decoding of nested arrays and structs.\

You might encounter old Solidity source code using the old directive, such as shown below\

pragma experimental ABIEncoderV2;

Version 2 is a strict superset of Version 1: contracts that use Version 2 can interact with other contracts that do not use it without any concern or limitations.\

This pragma also applies to the code defined in the file where it is activated, regardless of where that code ends up eventually; what this means is that a contract whose file is using Version 1 can still contain code that uses Version 2 by inheriting it from another contract. An example of ABI Coder pragma statement is\

pragma abicoder v1; // or v2, which is the default from version 0.8.z onwards

The ABI coder affects encoding and decoding. The optimizations it does have certain security implications.

The second pragma directive helps the developer to specify features that are considered experimental as of that point in time.\

These features are not enabled by default and have to be explicitly specified as part of this pragma directive and within every file where it is required. As of now there is only one experimental feature, which is known as SMTChecker.\

pragma experimental SMTChecker;

SMT stands for Satisfiability Modulo Theory which is an approach to formal verification, and in the case of Solidity it is used to implement safety checks by what is known as querying an SMT solver.\

There are various security checks performed by the SMT checker. The first one is where it uses the require and assert statements that are included as part of the smart contract.\

The checker considers all the required statements specified as assumptions by the developer and it tries to prove that the conditions inside the assert statements are true.\

If a failure can be established, then the checker provides what is known as a counter example that shows the user how this assertion can fail.\

There are various other checks that have been added to this empty checker over time. These include the arithmetic overflow, underflow, division by zero, unreachable code and so on.\

So SMT checker is a critical security feature that comes packaged as part of Solidity. It's implemented in the compiler itself.\

Formal verification is considered as a fundamental part of programming languages' security, so we can imagine that this particular pragma directive affects the security and optimizations of the smart contracts that use them.