From d1f13d2871a815b253b151edf6d3f5d544ea10e2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Aug 2015 18:22:46 -0700 Subject: [PATCH] perf(library/module): skip checksum if trust level is very high --- src/library/module.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/library/module.cpp b/src/library/module.cpp index ee8ae55e9..4ddba048e 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -369,9 +369,11 @@ struct import_modules_fn { std::vector 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(); r->m_fname = fname;