Run the Simple project with
certoraRun CounterBroken.sol:Counter --verify Counter:Counter.spec --debug
got an error as follows:
It says “Encountered an error configuring the verification environment: Expecting value: line 1 column 1 (char 0)”, but i don’t know what the error is.
hey there,
can you send some more context?
the .spec file and contract that you are trying to run on will be helpful. Also a link to your run script/run command
I do understand that it’s our example, but if you changed anything on purpose or by mistake that could lead to an error.
This is my env:
~/s/C/E/Simple > pwd
/home/jfb/source/CertoraProverSupplementary/Examples/Simple
~/s/C/E/Simple > java --version
openjdk 17.0.2 2022-01-18
OpenJDK Runtime Environment (build 17.0.2+8-Ubuntu-120.04)
OpenJDK 64-Bit Server VM (build 17.0.2+8-Ubuntu-120.04, mixed mode, sharing)
~/s/C/E/Simple > python3 --version
Python 3.8.10
~/s/C/E/Simple > solc --version
solc, the solidity compiler commandline interface
Version: 0.8.10+commit.fc410830.Linux.g++
~/s/C/E/Simple >
and then run certoraRun CounterBroken.sol:Counter --verify Counter:Counter.spec --debug in Simple project with debug log enabled.
Below is the full log
~/s/C/E/Simple > certoraRun CounterBroken.sol:Counter --verify Counter:Counter.spec --debug
DEBUG: directory .last_confs already exists
DEBUG: args.packages_path is /home/jfb/source/CertoraProverSupplementary/Examples/Simple/node_modules
WARNING: Default package file package.json not found
WARNING: Couldn't find Certora Key. Proceeding with Certora Public Key.
WARNING: If you have a private key, press ctrl+c and set the environment variable CERTORAKEY
DEBUG: parsed args successfully.
DEBUG: args= Namespace(address={}, assert_contracts=None, build_only=False, cache=None, check_args=False, cloud=None, coinbaseMode=False, contracts={'Counter'}, debug=True, delay_fetch_output_seconds=None, disableLocalTypeChecking=False, env='production', file_paths={'CounterBroken.sol'}, file_to_contract={'CounterBroken.sol': 'Counter'}, files=['CounterBroken.sol:Counter'], internal_funcs=None, jar=None, java_args=None, key='795ebbac71ae5fd6a19e7a214a524b064e33ff05', link=None, local=False, log_query_frequency_seconds=None, loop_iter=None, max_attempts_to_fetch_output=None, max_graph_depth=None, max_poll_minutes=None, method=None, mode=<Mode.VERIFY>, msg=None, no_compare=False, optimistic_loop=False, packages=None, packages_path='/home/jfb/source/CertoraProverSupplementary/Examples/Simple/node_modules', path='/home/jfb/source/CertoraProverSupplementary/Examples/Simple', process='emv', queue_wait_minutes=None, rule=None, rule_sanity=False, settings=None, short_output=False, smt_timeout=None, solc='/home/jfb/.cargo/bin/solc', solc_args=None, solc_map=None, spec_files=['Counter.spec'], staging=None, struct_link=None, tool_output=None, typecheck_only=False, verified_contract_files=['CounterBroken.sol'], verify=['Counter:Counter.spec'])
Collecting contracts and building
DEBUG: collected data:
raw_args: ['/home/jfb/.local/bin/certoraRun', 'CounterBroken.sol:Counter', '--verify', 'Counter:Counter.spec', '--debug']
conf: {'files': ['CounterBroken.sol:Counter'], 'verify': ['Counter:Counter.spec'], 'debug': True, 'process': 'emv'}
args: {'files': ['CounterBroken.sol:Counter'], 'verify': ['Counter:Counter.spec'], 'assert_contracts': None, 'msg': None, 'rule': None, 'rule_sanity': False, 'short_output': False, 'solc': '/home/jfb/.cargo/bin/solc', 'solc_args': None, 'solc_map': None, 'path': '/home/jfb/source/CertoraProverSupplementary/Examples/Simple', 'packages_path': '/home/jfb/source/CertoraProverSupplementary/Examples/Simple/node_modules', 'packages': None, 'optimistic_loop': False, 'loop_iter': None, 'method': None, 'cache': None, 'smt_timeout': None, 'link': None, 'address': {}, 'struct_link': None, 'debug': True, 'staging': None, 'cloud': None, 'jar': None, 'java_args': None, 'check_args': False, 'build_only': False, 'typecheck_only': False, 'disableLocalTypeChecking': False, 'no_compare': False, 'queue_wait_minutes': None, 'max_poll_minutes': None, 'log_query_frequency_seconds': None, 'max_attempts_to_fetch_output': None, 'delay_fetch_output_seconds': None, 'process': 'emv', 'settings': None, 'max_graph_depth': None, 'tool_output': None, 'internal_funcs': None, 'coinbaseMode': False, 'mode': <Mode.VERIFY>, 'contracts': {'Counter'}, 'file_paths': {'CounterBroken.sol'}, 'file_to_contract': {'CounterBroken.sol': 'Counter'}, 'spec_files': ['Counter.spec'], 'verified_contract_files': ['CounterBroken.sol'], 'local': False, 'env': 'production', 'key': '795ebbac71ae5fd6a19e7a214a524b064e33ff05'}
origin: git@github.com:Certora/CertoraProverSupplementary.git
revision: b4de28dfcd0e4678d8050004c6f7f2bcfee66f74
branch: master
cwd_relative: Examples/Simple
dirty: False
DEBUG: There is no TAC file. Going to script certoraBuild.py to main_with_args()
DEBUG: In /home/jfb/source/CertoraProverSupplementary/Examples/Simple/Counter.spec, found the imports: []
DEBUG: writing .certora_verify.json
Bad input to CVL typechecker
Local CVL specification syntax checking finished successfully
DEBUG:
building file CounterBroken.sol
DEBUG: relevant solc is /home/jfb/.cargo/bin/solc
DEBUG: about to run /home/jfb/.cargo/bin/solc -o /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0/ --overwrite --allow-paths /home/jfb/source/CertoraProverSupplementary/Examples/Simple,. --standard-json
DEBUG: solc input = {
"language": "Solidity",
"sources": {
"/home/jfb/source/CertoraProverSupplementary/Examples/Simple/CounterBroken.sol": {
"urls": [
"/home/jfb/source/CertoraProverSupplementary/Examples/Simple/CounterBroken.sol"
]
}
},
"settings": {
"remappings": [],
"outputSelection": {
"*": {
"*": [
"storageLayout",
"abi",
"evm.bytecode",
"evm.deployedBytecode",
"evm.methodIdentifiers",
"evm.assembly"
],
"": [
"id",
"ast"
]
}
}
}
}
DEBUG: Running cmd /home/jfb/.cargo/bin/solc -o /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0/ --overwrite --allow-paths /home/jfb/source/CertoraProverSupplementary/Examples/Simple,. --standard-json
DEBUG: stdout, stderr = /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0.standard.json.stdout, /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0.standard.json.stderr
DEBUG: Exitcode 0
DEBUG: Collecting standard json: /home/jfb/.cargo/bin/solc -o /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0/ --overwrite --allow-paths /home/jfb/source/CertoraProverSupplementary/Examples/Simple,. --standard-json
DEBUG: reading standard json data from /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0.standard.json.stdout
Encountered an error configuring the verification environment: Expecting value: line 1 column 1 (char 0)
DEBUG: Traceback (most recent call last):
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraBuild.py", line 2347, in build
certora_build_generator.build(args)
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraBuild.py", line 1727, in build
sdc_pre_finder = self.collect_for_file(build_arg_contract_file, i, debug=self.input_config.debug)
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraBuild.py", line 1251, in collect_for_file
standard_json_data = self.get_standard_json_data(sdc_name)
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraBuild.py", line 942, in get_standard_json_data
return read_json_file(json_file)
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraUtils.py", line 294, in read_json_file
json_obj = json.load(json_str)
File "/usr/lib/python3.8/json/__init__.py", line 293, in load
return loads(fp.read(),
File "/usr/lib/python3.8/json/__init__.py", line 357, in loads
return _default_decoder.decode(s)
File "/usr/lib/python3.8/json/decoder.py", line 337, in decode
obj, end = self.raw_decode(s, idx=_w(s, 0).end())
File "/usr/lib/python3.8/json/decoder.py", line 355, in raw_decode
raise JSONDecodeError("Expecting value", s, err.value) from None
json.decoder.JSONDecodeError: Expecting value: line 1 column 1 (char 0)
~/s/C/E/Simple >
Counter.spec:
methods {
counter() returns uint256 envfree
}
rule invertible {
uint256 curr = counter();
/* The `env` type represents the EVM parameters passed in every
call (msg., tx., block.* variables in Solidity)
*/
env e;
/* For non-`envfree` methods, the environment must be passed as the first argument*/
inc(e);
dec(e);
assert counter() == curr, "dec followed by inc should give the original value";
}
rule monotone {
uint256 curr = counter();
env e;
assert inc(e) > curr, "Incremented value is greater than original value";
}⏎
CounterBroken.sol
contract Counter {
address public admin;
uint public counter;
function inc() public returns (uint) {
require(msg.sender == admin);
return ++counter;
}
function dec() public returns (uint) {
require(msg.sender == admin);
return --counter;
}
}
EDIT: my git repo is clean.
Just to make sure, what to do you get when you run certoraRun --version?
~/s/C/E/Simple > certoraRun --version
certora-cli 2.7.2
This is a very old version, please run pip3 install certora-cli --upgrade or pip install certora-cli --upgrade (depending how you invoke pip)
I have upgraded it 3.0.0
~/s/C/E/Simple > certoraRun --version
certora-cli 3.0.0
And the same error occured
~/s/C/E/Simple > certoraRun CounterBroken.sol:Counter --verify Counter:Counter.spec --debug
DEBUG: setting cache key to CounterBroken.sol:Counter-optimisticFalse-iterNone
DEBUG: directory .last_confs already exists
DEBUG: args.packages_path is /home/jfb/source/CertoraProverSupplementary/Examples/Simple/node_modules
WARNING: Default package file package.json not found
WARNING: Couldn't find Certora Key. Proceeding with Certora Public Key.
WARNING: If you have a private key, press ctrl+c and set the environment variable CERTORAKEY
DEBUG: parsed args successfully.
DEBUG: args= Namespace(address={}, assert_contracts=None, build_only=False, bytecode_jsons=None, bytecode_spec=None, cache='CounterBroken.sol:Counter-optimisticFalse-iterNone', check_args=False, cloud=None, coinbaseMode=False, contracts={'Counter'}, debug='', debug_topics=False, delay_fetch_output_seconds=None, disableLocalTypeChecking=False, disable_auto_cache_key_gen=False, env='production', expected_file='expected.json', file_paths={'CounterBroken.sol'}, file_to_contract={'CounterBroken.sol': 'Counter'}, files=['CounterBroken.sol:Counter'], internal_funcs=None, jar=None, java_args=None, key='795ebbac71ae5fd6a19e7a214a524b064e33ff05', link=None, local=False, log_branch=None, log_query_frequency_seconds=None, loop_iter=None, max_attempts_to_fetch_output=None, max_graph_depth=None, max_poll_minutes=None, method=None, mode=<Mode.VERIFY>, msg=None, multi_assert_check=False, no_compare=False, optimistic_loop=False, optimize=None, packages=None, packages_path='/home/jfb/source/CertoraProverSupplementary/Examples/Simple/node_modules', path='/home/jfb/source/CertoraProverSupplementary/Examples/Simple', process='emv', queue_wait_minutes=None, rule=None, rule_sanity=False, send_only=False, settings=None, short_output=False, smt_timeout=None, solc='/home/jfb/.cargo/bin/solc', solc_args=None, solc_map=None, spec_files=['Counter.spec'], staging=None, struct_link=None, tool_output=None, typecheck_only=False, user_defined_cache=False, verified_contract_files=['CounterBroken.sol'], verify=['Counter:Counter.spec'])
Collecting contracts and building
DEBUG: collected data:
raw_args: ['/home/jfb/.local/bin/certoraRun', 'CounterBroken.sol:Counter', '--verify', 'Counter:Counter.spec', '--debug']
conf: {'files': ['CounterBroken.sol:Counter'], 'verify': ['Counter:Counter.spec'], 'cache': 'CounterBroken.sol:Counter-optimisticFalse-iterNone', 'debug': '', 'process': 'emv'}
args: {'files': ['CounterBroken.sol:Counter'], 'verify': ['Counter:Counter.spec'], 'assert_contracts': None, 'bytecode_jsons': None, 'bytecode_spec': None, 'msg': None, 'rule': None, 'multi_assert_check': False, 'rule_sanity': False, 'short_output': False, 'typecheck_only': False, 'send_only': False, 'solc': '/home/jfb/.cargo/bin/solc', 'solc_args': None, 'solc_map': None, 'path': '/home/jfb/source/CertoraProverSupplementary/Examples/Simple', 'optimize': None, 'packages_path': '/home/jfb/source/CertoraProverSupplementary/Examples/Simple/node_modules', 'packages': None, 'optimistic_loop': False, 'loop_iter': None, 'method': None, 'cache': 'CounterBroken.sol:Counter-optimisticFalse-iterNone', 'smt_timeout': None, 'link': None, 'address': {}, 'struct_link': None, 'debug': '', 'debug_topics': False, 'staging': None, 'cloud': None, 'jar': None, 'java_args': None, 'check_args': False, 'build_only': False, 'disableLocalTypeChecking': False, 'no_compare': False, 'expected_file': 'expected.json', 'queue_wait_minutes': None, 'max_poll_minutes': None, 'log_query_frequency_seconds': None, 'max_attempts_to_fetch_output': None, 'delay_fetch_output_seconds': None, 'process': 'emv', 'settings': None, 'log_branch': None, 'disable_auto_cache_key_gen': False, 'max_graph_depth': None, 'tool_output': None, 'internal_funcs': None, 'coinbaseMode': False, 'mode': <Mode.VERIFY>, 'user_defined_cache': False, 'contracts': {'Counter'}, 'file_paths': {'CounterBroken.sol'}, 'file_to_contract': {'CounterBroken.sol': 'Counter'}, 'verified_contract_files': ['CounterBroken.sol'], 'spec_files': ['Counter.spec'], 'local': False, 'env': 'production', 'key': '795ebbac71ae5fd6a19e7a214a524b064e33ff05'}
origin: git@github.com:Certora/CertoraProverSupplementary.git
revision: b4de28dfcd0e4678d8050004c6f7f2bcfee66f74
branch: master
cwd_relative: Examples/Simple
dirty: False
DEBUG: There is no TAC file. Going to script certoraBuild.py to main_with_args()
DEBUG: In /home/jfb/source/CertoraProverSupplementary/Examples/Simple/Counter.spec, found the imports: []
DEBUG: writing .certora_verify.json
Local CVL specification syntax checking finished successfully
DEBUG:
building file CounterBroken.sol
DEBUG: relevant solc is /home/jfb/.cargo/bin/solc
DEBUG: about to run /home/jfb/.cargo/bin/solc -o "/home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0/" --overwrite --allow-paths "/home/jfb/source/CertoraProverSupplementary/Examples/Simple",. --standard-json
DEBUG: solc input = {
"language": "Solidity",
"sources": {
"/home/jfb/source/CertoraProverSupplementary/Examples/Simple/CounterBroken.sol": {
"urls": [
"/home/jfb/source/CertoraProverSupplementary/Examples/Simple/CounterBroken.sol"
]
}
},
"settings": {
"remappings": [],
"outputSelection": {
"*": {
"*": [
"storageLayout",
"abi",
"evm.bytecode",
"evm.deployedBytecode",
"evm.methodIdentifiers",
"evm.assembly"
],
"": [
"id",
"ast"
]
}
}
}
}
DEBUG: Running cmd /home/jfb/.cargo/bin/solc -o "/home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0/" --overwrite --allow-paths "/home/jfb/source/CertoraProverSupplementary/Examples/Simple",. --standard-json
DEBUG: stdout, stderr = /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0.standard.json.stdout, /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0.standard.json.stderr
DEBUG: Exitcode 0
DEBUG: Collecting standard json: /home/jfb/.cargo/bin/solc -o "/home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0/" --overwrite --allow-paths "/home/jfb/source/CertoraProverSupplementary/Examples/Simple",. --standard-json
DEBUG: reading standard json data from /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0.standard.json.stdout
CRITICAL: Encountered an error running Certora Prover; consider running the script again with --debug to find out why
Traceback (most recent call last):
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraBuild.py", line 2831, in build
certora_build_generator.build(args)
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraBuild.py", line 2048, in build
sdc_pre_finder = self.collect_for_file(build_arg_contract_file, i)
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraBuild.py", line 1491, in collect_for_file
standard_json_data = self.get_standard_json_data(sdc_name)
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraBuild.py", line 1169, in get_standard_json_data
return read_json_file(json_file)
File "/home/jfb/.local/lib/python3.8/site-packages/certora_cli/certoraUtils.py", line 290, in read_json_file
json_obj = json.load(json_str)
File "/usr/lib/python3.8/json/__init__.py", line 293, in load
return loads(fp.read(),
File "/usr/lib/python3.8/json/__init__.py", line 357, in loads
return _default_decoder.decode(s)
File "/usr/lib/python3.8/json/decoder.py", line 337, in decode
obj, end = self.raw_decode(s, idx=_w(s, 0).end())
File "/usr/lib/python3.8/json/decoder.py", line 355, in raw_decode
raise JSONDecodeError("Expecting value", s, err.value) from None
json.decoder.JSONDecodeError: Expecting value: line 1 column 1 (char 0)
~/s/C/E/Simple >
Please share the file /home/jfb/source/CertoraProverSupplementary/Examples/Simple/.certora_config/CounterBroken.sol_0.standard.json.stdout?
Ideally the entire .certora_config dir, zipped.
It might be related to python version?
@jayphbee have you followed the installation guide to install cli?
make sure to have java and python upgraded to a version above the specified one in the guide, and pay special attention to step 2 - adding your python to your $PATH
I’ll double check it.
There’s no warning when i install certora-cli
~/s/C/E/Simple > pip3 install certora-cli
Requirement already satisfied: certora-cli in /home/jfb/.local/lib/python3.8/site-packages (3.0.0)
Requirement already satisfied: click in /usr/lib/python3/dist-packages (from certora-cli) (7.0)
Requirement already satisfied: tabulate in /home/jfb/.local/lib/python3.8/site-packages (from certora-cli) (0.8.9)
Requirement already satisfied: pycryptodome in /home/jfb/.local/lib/python3.8/site-packages (from certora-cli) (3.10.1)
Requirement already satisfied: requests in /home/jfb/.local/lib/python3.8/site-packages (from certora-cli) (2.25.0)
Requirement already satisfied: sly in /home/jfb/.local/lib/python3.8/site-packages (from certora-cli) (0.4)
Requirement already satisfied: tqdm in /home/jfb/.local/lib/python3.8/site-packages (from certora-cli) (4.62.3)
Requirement already satisfied: chardet<4,>=3.0.2 in /usr/lib/python3/dist-packages (from requests->certora-cli) (3.0.4)
Requirement already satisfied: idna<3,>=2.5 in /usr/lib/python3/dist-packages (from requests->certora-cli) (2.8)
Requirement already satisfied: urllib3<1.27,>=1.21.1 in /usr/lib/python3/dist-packages (from requests->certora-cli) (1.25.8)
Requirement already satisfied: certifi>=2017.4.17 in /home/jfb/.local/lib/python3.8/site-packages (from requests->certora-cli) (2021.5.30)
~/s/C/E/Simple >
@jayphbee there might not be a warning because it appears only the first time you install it.
Im not well educated on the installation process, but probably once the installation is made some meta files are staying even if you uninstall.
What i would advice you to do is adding both the certoraRun to PATH (in my mac it’s on ~/Library/Python/3.8/bin) and also your system python (i think which python should do the trick), though i doubt that the latter will help.
do that and come back to us with results. What OS do you use? looks like linux.
Follow step 2 for linux in the installation guide and make sure to add that PATH.
Do u have a docker image to play with ?
We currently do not have a container application. Please, follow the installation instructions here.
If you encountered the same error again, please uninstall the package by running the following command:
pip3 uninstall certora-cli (or pip)
Make sure it was uninstalled by running:
pip3 show certora-cli
You should see the following line:
WARNING: Package(s) not found: certora-cli
Now, try to reinstall the package