> For the complete documentation index, see [llms.txt](https://docs.runtimeverification.com/kontrol/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.runtimeverification.com/kontrol/developer-docs/digest-file.md).

# 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()](https://github.com/runtimeverification/kontrol/blob/b7065f74304e7af9a43506849331fd6b73039ccb/src/kontrol/kompile.py#L124). It concatenates the hashes of [`contracts.k`](https://github.com/runtimeverification/kontrol/blob/b7065f74304e7af9a43506849331fd6b73039ccb/src/tests/integration/test-data/show/contracts.k.expected), [`foundry.k`](https://github.com/runtimeverification/kontrol/blob/b7065f74304e7af9a43506849331fd6b73039ccb/src/tests/integration/test-data/show/foundry.k.expected), and any additional `.k` file passed to kontrol build using `--requires` (such as [`lemmas.k`](https://github.com/runtimeverification/kontrol/blob/b7065f74304e7af9a43506849331fd6b73039ccb/src/tests/integration/test-data/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()](https://github.com/runtimeverification/kontrol/blob/b7065f74304e7af9a43506849331fd6b73039ccb/src/kontrol/foundry.py#L194-L201) and is generated in [Foundry.digest()](https://github.com/runtimeverification/kontrol/blob/b7065f74304e7af9a43506849331fd6b73039ccb/src/kontrol/foundry.py#L165-L168) 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()](https://github.com/runtimeverification/kontrol/blob/b7065f74304e7af9a43506849331fd6b73039ccb/src/kontrol/solc_to_k.py#L704C1-L706C101)).

`method` hashes are obtained by hashing the signature, AST, the storage digest hash, and the contract digest ([Method.digest()](https://github.com/runtimeverification/kontrol/blob/b7065f74304e7af9a43506849331fd6b73039ccb/src/kontrol/solc_to_k.py#L515-L518)).

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()](https://github.com/runtimeverification/kontrol/blob/b7065f74304e7af9a43506849331fd6b73039ccb/src/kontrol/solc_to_k.py#L359)).