michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

perf(library/module): skip checksum if trust level is very high

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-14 18:22:46 -07:00
parent d3d1b58fb4
commit d1f13d2871
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/module.cpp
View file

@ -369,9 +369,11 @@ struct import_modules_fn {
std::vector<char> code(code_size);
d1.read(code);
unsigned computed_hash = hash(code_size, [&](unsigned i) { return code[i]; });
if (claimed_hash != computed_hash)
throw exception(sstream() << "file '" << fname << "' has been corrupted, checksum mismatch");
if (m_senv.env().trust_lvl() <= LEAN_BELIEVER_TRUST_LEVEL) {
unsigned computed_hash = hash(code_size, [&](unsigned i) { return code[i]; });
if (claimed_hash != computed_hash)
throw exception(sstream() << "file '" << fname << "' has been corrupted, checksum mismatch");
}
module_info_ptr r = std::make_shared<module_info>();
r->m_fname = fname;