Digest File

This documentation serves as a technical reference for understanding the structure and purpose of the digest file located in the out/ folder of a Kontrol project. The purpose of this file is to enable secure and verifiable tracking of different versions of smart contracts and their associated methods.

File Structure

The digest file consists of the following top-level fields:

• kompilation: A string representing the SHA-256 hash of the compilation artifact.

• foundry: A string representing the SHA-256 hash of the Foundry used to compile the contracts.

• methods: An object containing key-value pairs, where each key represents a function name and an object with the following fields:

• method: A string representing the SHA-256 hash of the method signature.

• contract: A string representing the SHA-256 hash of the contract that contains the method.

Kompilation

kompilation digest is computed in kompilation_digest(). It concatenates the hashes of contracts.k, foundry.k, and any additional .k file passed to kontrol build using --requires (such as lemmas.k); then hashes the concatenated string once more. The solc compiler will generate JSON files containing the ABI, AST, and other properties of the Solidity contracts, under the out/ directory. These files are processed, and the contracts.k and foundry.k files are generated. These files use mostly the bytecode and storage locations of a contract.

The hash contained in the field is changing, e.g,

• Any time a Solidity file is modified to have different bytecode, or storage locations, resulting in modified contracts.k and foundry.k files

• Any time kontrol build is called with different --requires flag values

Foundry

This hash ensures that the contracts are compiled using a specific version of Foundry. Removing Foundry and installing the same version won't trigger hash changes. Only when the Foundry version is changing, system rewrites the hash for Foundry.

Running kontrol build over a project might generate a digest file with only two fields:

{ "kompilation": "11509a7f5a670f6eae1f97ab80e7c5ce6d2e436301a87ce9df401f067135ecbb", "foundry": "e0575c929ad0874b414a52480e10609fb6a1c45cb151b0c68be04a4e7c854295" }

The foundry digest is added to the digest JSON object in Foundry.update_digest() and is generated in Foundry.digest() by concatenating each contract digest individually, and hashing the resulting string again.

Methods

The methods object contains a mapping of method signatures to their corresponding hashes and the hashes of the contracts that contain them. Each method signature is represented as a key and follows component name. Each key has object with two values:

• method: The hash of the method signature, uniquely identifying the method.

• contract: The hash of the contract that contains the method, linking the method to its parent contract.

methods digest is used by kontrol prove:

{
	"kompilation": "11509a7f5a670f6eae1f97ab80e7c5ce6d2e436301a87ce9df401f067135ecbb",
	"foundry": "e0575c929ad0874b414a52480e10609fb6a1c45cb151b0c68be04a4e7c854295",
	"methods": {
    	"test%CounterTest.testFuzz_SetNumber(uint256)": {
        	"method": "d7f5a6bd6daa1a1ee8255924820a95de17bbf6666a771e65dbdbf6f8e7f7e5c2",
        	"contract": "500a67b39157bce6d3a7f9e9a33a09d12ff2f061fbb7649bad2fcb783656a03b"
    	},
    	"test%CounterTest.test_Increment()": {
        	"method": "ef5ad1ed4ab997794356e0cd3fc946e7a67bbc6817ef4757caa9eb02cb8ac084",
        	"contract": "500a67b39157bce6d3a7f9e9a33a09d12ff2f061fbb7649bad2fcb783656a03b"
    	},
    	"test%CounterTest.setUp()": {
        	"method": "a2b1ce66eabb659b2108c5ef4aa6a18425b8c9ea12bb9247bc4aa632bfa898c8",
        	"contract": "500a67b39157bce6d3a7f9e9a33a09d12ff2f061fbb7649bad2fcb783656a03b"
    	}
	}
}

The contract digest is generated by hashing the contract name and the contents of the JSON file obtained from the solc compiler (Contract.digest()).

method hashes are obtained by hashing the signature, AST, the storage digest hash, and the contract digest (Method.digest()).

There is also a Constructor data class, which is a special case of Method used to handle a constructor() function in Solidity contracts. The hash generation implementation for it has a small variation (Constructor.digest()).