# 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)).


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.runtimeverification.com/kontrol/developer-docs/digest-file.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.