coprocessor/docs/fundamentals/fhevm/contracts.md
The FHEVM employs symbolic execution - essentially, inputs to FHE operations are symbolic values (also called handles) that refer to ciphertexts. We check constraints on these handles, but ignore their actual values.
Inside the Executor (in FHEVM-native) and inside the Coprocessor, we actually execute the FHE operations on the ciphertexts the handles refer to. If a new ciphertext is generated as a result of an FHE operation, it is inserted into the blockchain for FHEVM-native (into the ciphertext storage contract, see Storage) or into the DB and DA for Coprocessor under a handle that is deterministically generated by the FHEVMExecutor contract.
Note: All those contracts are initially deployed behind UUPS proxies, so could be upgraded by their owner at any time. Unless if the owner renounces ownership, after which the protocol could be considered imumutable.
Symbolic execution on the blockchain is implemented via the FHEVMExecutor contract. One of its main responsibilities is to deterministically generate ciphertext handles. For this, we hash the FHE operation requested and the inputs to produce the result handle H:
H = keccak256(fheOperation, input1, input2, ..., inputN)
Inputs can either be other handles or plaintext values.
The ACL contract enforces access control for ciphertexts. The model we adopt is very simple - a ciphertext is either allowed for an address or not. An address can be any address - either an EOA address or a contract address. Essentially, it is a mapping from handle to a set of addresses that are allowed to use the handle.
Access control applies to transferring ciphertexts from one contract to another, for FHE computation on ciphertexts, for decryption and for reencryption of a ciphertext to a user-provided key.
Data in the ACL contract grows indefinitely as new ciphertexts are produced. We might want to expose ways for developers to reclaim space by marking that certain ciphertexts are no longer needed and, consequently, zeroing the slot in the ACL. A future effort will look into that.
The KMSVerifier contract allows any dApp to verify a received decryption. This contract exposes a function verifyDecryptionEIP712KMSSignatures which receives the decryption result and signatures coming from the TKMS.
KMS signers addresses are stored and updated in the contract.
The InputVerifier contract is responsible for verifying signatures when a user is inputting a new ciphertext. When a user submits an encrypted input, they first send a ZKPoK (Zero-Knowledge Proof of Knowledge) to be verified by the coprocessor nodes. If the proof verifies successfully, each coprocessor signer will sign a hash of the computed handles and the signatures will be returned to the user. The user can then input new handles onchain by providing these signatures.
This is done via the verifyInput function, which checks the coprocessors accounts' signatures including the computed handles. We trust the handles computation done by the coprocessors before using them in transactions onchain.
We defined a concept named Homomorphic Complexity Units ("HCU") that represents the complexity for a FHE operation.
When using FHE, the HCULimit contract tracks the HCU consumed in each transaction, and reverts if: