Failed to create the 'latest' symlink. [WinError 1314] A required privilege is not held by the client: '.' -> 'latest'

General Discussion
,
1

Simplest test project fails in windows, when the sol or spec files are not in the current folder.
When running from the current folder, it is fine. Also tested in Mac, it’s all fine. This problem is in windows only

Files:
contracts/Math.sol
contracts/Math.spec

C:\CertoraTest\contracts>certoraRun Math.sol --verify Math:Math.spec

But when the files are in different folders:
contracts/Math.sol
certora/specs/Math.spec

It fails with the following errors:

C:\CertoraTest>certoraRun contracts/Math.sol --verify Math:certora/specs/Math.spec

Failed to create the 'latest' symlink. [WinError 1314] A required privilege is not held by the client: '.' -> 'latest'
Compiling contracts\Math.sol...
Compiling contracts\Math.sol to expose internal function information...

Connecting to server...

Job submitted to server
...
Error: Could not access content of certora/specs/Math.spec
[main] ERROR ALWAYS - Could not access content of certora/specs/Math.spec
Error: Encountered exception CertoraFileCache could not access .certora_sources/certora\specs\Math.spec; file either does not exist on disk or was not cached while running: -cache 1939143932417734230-optimisticFalse-iterNone-None--certora-cli-4.10.1 -globalTimeout 7200
[main] ERROR ALWAYS - Encountered exception CertoraFileCache could not access .certora_sources/certora\specs\Math.spec; file either does not exist on disk or was not cached while running: -cache 1939143932417734230-optimisticFalse-iterNone-None--certora-cli-4.10.1 -globalTimeout 7200        
Done 0m
2

Yeah, there is a problem with Windows. You should use WSL or any other Linux emulator on Windows.
Sorry for the inconvenience.

3

Thanks @RedLikeRoses for the reply. At least I know it’s not just me.
But this is surprising as the only thing goes wrong here is the way the path is treated. I can even see the zip files have correct paths. Also there is no mention in the docs that you might encounter some issues in windows. The documents provide instructions for installation on Windows environment as well without mentioning such problem.

Can I use WSL in a way that it just treats the path, or I have to take everything (e.g. VS Code ) into linux environment on windows?

4

I just know that the tool has issues with Windows. So I can’t provide more details here, It’s out of my depth.

Regarding documentation. We will fix it soon.

WSL. I’m using Mac, so not sure how it’s used. I will ask somebody to help.

5

Will be great if you fix the documentation. For someone who is just testing it for the first time, it’s not trivial to know if such an issue exists in the tool.
Another issue I found, which is technically has the same root, was that it couldn’t figure out the Openzeppelin library references, so I had to flatten to get it working. But when I tested on Mac, it was all smooth.

6

@0xMohandes Have you tried switching to WSL already? Did you encounter any issues? The Certora prover is fully supported on Linux.

7

No, used Mac for now.
My point is that Certora docs imply that Windows is supported, but it misleads the newcomers.
In fact it works for certain conditions, (i.e. when the solidity file and spec file are both in the current folder and they don’t reference anything from any other folder). Even without knowing what’s happening under the hood, it seems like a simple fix. I suggest either updating the docs or fixing it.

I will update if I try WSL, but that’s not why I have raised. My workaround was using Mac. I raised it because I thought you might not be aware of this issue, while it might just turn away some enthusiasts.

8

I installed WSL on Windows11, using the default Ubuntu installation and Certora Prover works fine.

9

Installed WSL, and it works. I didn’t have much understanding of how WSL works as I have been mainly a Windows users most of my career life. Good to have all steps in the docs if you require WSL to work on windows.