charon
charon copied to clipboard
AeneasVerif
Support foreign constants
This is with the following:
libcrux/dev@2914abfeae3a38e5cf689d3d0959e5a8845da6ea
charon/main@298c9c42410603569dfc8f57fa12ebd90cecb8ea
this did not happen with libcrux@eddefae (same charon rev)
Running charon ...
warning: xcrun: error: unable to lookup item 'PlatformVersion' from command line tools installation
warning: xcrun: error: unable to lookup item 'PlatformVersion' in SDK '/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk'
warning: xcrun: error: unable to lookup item 'PlatformVersion' from command line tools installation
warning: xcrun: error: unable to lookup item 'PlatformVersion' in SDK '/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk'
warning: xcrun: error: unable to lookup item 'PlatformVersion' from command line tools installation
warning: xcrun: error: unable to lookup item 'PlatformVersion' in SDK '/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk'
Compiling libcrux-ml-kem v0.0.2-pre.2 (/Users/jonathan/Code/libcrux-2/libcrux-ml-kem)
thread 'rustc' panicked at 'libcrux_traits does not have a "explicit_predicates_of"', compiler/rustc_metadata/src/rmeta/decoder/cstore_impl.rs:205:1
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
then
stack backtrace:
0: 0x1053fcca4 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h5792bb1ec1b25381
1: 0x10544cd3c - core::fmt::write::he890c84243ba59b9
2: 0x1053f2d9c - std::io::Write::write_fmt::h1b5ef1cd3b11e53a
3: 0x1053fcaf8 - std::sys_common::backtrace::print::h4bb2e42f5381e3d6
4: 0x1053ff558 - std::panicking::default_hook::{{closure}}::ha05e40ed1a991c17
5: 0x1053ff360 - std::panicking::default_hook::h6ee258d9f2d00125
6: 0x1053ffae0 - std::panicking::rust_panic_with_hook::h6bbb3eaa0d6db565
7: 0x1053ff9ec - std::panicking::begin_panic_handler::{{closure}}::h807422798d307ab3
8: 0x1053fd084 - std::sys_common::backtrace::__rust_end_short_backtrace::hc910f1116ecb7527
9: 0x1053ff760 - _rust_begin_unwind
10: 0x105477ecc - core::panicking::panic_fmt::hb411a23424cd6c26
11: 0x110ebc2a8 - rustc_metadata[47357657ea2cecea]::rmeta::decoder::cstore_impl::provide_extern::explicit_predicates_of::{closure#2}
12: 0x110ebc0bc - rustc_metadata[47357657ea2cecea]::rmeta::decoder::cstore_impl::provide_extern::explicit_predicates_of
13: 0x110ba2f3c - rustc_query_impl[e3bd751713a1fc2a]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[e3bd751713a1fc2a]::query_impl::explicit_predicates_of::dynamic_query::{closure#2}::{closure#0}, rustc_middle[eadec4d34c049b6b]::query::erase::Erased<[u8; 24usize]>>
14: 0x110ac0238 - <rustc_query_impl[e3bd751713a1fc2a]::query_impl::explicit_predicates_of::dynamic_query::{closure#2} as core[2ea8d1c0976e098]::ops::function::FnOnce<(rustc_middle[eadec4d34c049b6b]::ty::context::TyCtxt, rustc_span[7c36f2217e98b708]::def_id::DefId)>>::call_once
15: 0x110a05b0c - rustc_query_system[8007b8eb5be70c8b]::query::plumbing::try_execute_query::<rustc_query_impl[e3bd751713a1fc2a]::DynamicConfig<rustc_query_system[8007b8eb5be70c8b]::query::caches::DefaultCache<rustc_span[7c36f2217e98b708]::def_id::DefId, rustc_middle[eadec4d34c049b6b]::query::erase::Erased<[u8; 24usize]>>, false, false, false>, rustc_query_impl[e3bd751713a1fc2a]::plumbing::QueryCtxt, true>
16: 0x110a689d4 - rustc_query_impl[e3bd751713a1fc2a]::query_impl::explicit_predicates_of::get_query_incr::__rust_end_short_backtrace
17: 0x10ff1d320 - rustc_middle[eadec4d34c049b6b]::query::plumbing::query_get_at::<rustc_query_system[8007b8eb5be70c8b]::query::caches::DefaultCache<rustc_span[7c36f2217e98b708]::def_id::DefId, rustc_middle[eadec4d34c049b6b]::query::erase::Erased<[u8; 24usize]>>>
18: 0x10ff2e51c - rustc_hir_analysis[8acf04c84aca6fd8]::collect::predicates_defined_on
19: 0x110ba2c78 - rustc_query_impl[e3bd751713a1fc2a]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[e3bd751713a1fc2a]::query_impl::predicates_defined_on::dynamic_query::{closure#2}::{closure#0}, rustc_middle[eadec4d34c049b6b]::query::erase::Erased<[u8; 24usize]>>
20: 0x110b0d198 - <rustc_query_impl[e3bd751713a1fc2a]::query_impl::predicates_defined_on::dynamic_query::{closure#2} as core[2ea8d1c0976e098]::ops::function::FnOnce<(rustc_middle[eadec4d34c049b6b]::ty::context::TyCtxt, rustc_span[7c36f2217e98b708]::def_id::DefId)>>::call_once
21: 0x110a05b0c - rustc_query_system[8007b8eb5be70c8b]::query::plumbing::try_execute_query::<rustc_query_impl[e3bd751713a1fc2a]::DynamicConfig<rustc_query_system[8007b8eb5be70c8b]::query::caches::DefaultCache<rustc_span[7c36f2217e98b708]::def_id::DefId, rustc_middle[eadec4d34c049b6b]::query::erase::Erased<[u8; 24usize]>>, false, false, false>, rustc_query_impl[e3bd751713a1fc2a]::plumbing::QueryCtxt, true>
22: 0x110c0ec68 - rustc_query_impl[e3bd751713a1fc2a]::query_impl::predicates_defined_on::get_query_incr::__rust_end_short_backtrace
23: 0x10439c4d4 - rustc_middle::query::plumbing::query_get_at::h500a455c110299bd
24: 0x10439dec4 - hax_frontend_exporter::types::mir_traits::solve_item_traits::h09b2e3498bb1bb62
25: 0x1043bd938 - hax_frontend_exporter::constant_utils::ConstantExt::translate_uneval::h9943dd4a502686a7
26: 0x1043c2d18 - hax_frontend_exporter::types::copied::<impl hax_frontend_exporter::sinto::SInto<S,hax_frontend_exporter::types::copied::Decorated<hax_frontend_exporter::constant_utils::ConstantExprKind>> for rustc_middle::mir::ConstantKind>::sinto::h7909a56652be56a8
27: 0x1043c129c - hax_frontend_exporter::types::mir::_::<impl hax_frontend_exporter::sinto::SInto<S,hax_frontend_exporter::types::mir::Constant> for rustc_middle::mir::Constant>::sinto::h9628faf1d7d37903
28: 0x1043e1768 - <(L,R) as hax_frontend_exporter::sinto::SInto<S,(LL,RR)>>::sinto::h10e0367826ce8e90
29: 0x1043d7224 - hax_frontend_exporter::types::mir::_::<impl hax_frontend_exporter::sinto::SInto<S,hax_frontend_exporter::types::mir::StatementKind> for rustc_middle::mir::syntax::StatementKind>::sinto::h1b46e88ab914610b
30: 0x1043c1584 - hax_frontend_exporter::types::mir::_::<impl hax_frontend_exporter::sinto::SInto<S,hax_frontend_exporter::types::mir::Statement> for rustc_middle::mir::Statement>::sinto::h845296ad7e58a3ae
31: 0x10440e238 - <alloc::vec::Vec<T> as hax_frontend_exporter::sinto::SInto<S,alloc::vec::Vec<D>>>::sinto::hcaaa90dba5154ebd
32: 0x1043e7688 - <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold::he4989e786f62e024
33: 0x104438ba8 - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::h8730751333dc3821
34: 0x1043c1698 - hax_frontend_exporter::types::mir::_::<impl hax_frontend_exporter::sinto::SInto<S,hax_frontend_exporter::types::mir::MirBody<KIND>> for rustc_middle::mir::Body>::sinto::h6ce8a93377fc8991
35: 0x104365814 - charon_lib::translate::translate_functions_to_ullbc::<impl charon_lib::translate::translate_ctx::BodyTransCtx>::translate_body_aux::h7dfe0be02651b06d
36: 0x1043652cc - charon_lib::translate::translate_functions_to_ullbc::<impl charon_lib::translate::translate_ctx::BodyTransCtx>::translate_body::he8adf4e85f0d92e6
37: 0x10436b9b0 - charon_lib::translate::translate_functions_to_ullbc::<impl charon_lib::translate::translate_ctx::TransCtx>::translate_global_aux::h02bb276f2485d838
38: 0x10436ae98 - charon_lib::translate::translate_functions_to_ullbc::<impl charon_lib::translate::translate_ctx::TransCtx>::translate_global::ha46f9ffca051f7dc
39: 0x1044f515c - charon_lib::translate::translate_crate_to_ullbc::translate::he6012132977aface
40: 0x1043d3604 - charon_lib::driver::translate::h450c19b6c84efce4
41: 0x1043ead78 - rustc_middle::ty::context::GlobalCtxt::enter::hf22a0e0f8ee56443
42: 0x1043d2e94 - <charon_lib::driver::CharonCallbacks as rustc_driver_impl::Callbacks>::after_parsing::hcd1340144eb5791e
43: 0x10d89d680 - <rustc_interface[c2a60cc96fc6f6d5]::interface::Compiler>::enter::<rustc_driver_impl[9e4f896e7075b60a]::run_compiler::{closure#1}::{closure#2}, core[2ea8d1c0976e098]::result::Result<core[2ea8d1c0976e098]::option::Option<rustc_interface[c2a60cc96fc6f6d5]::queries::Linker>, rustc_span[7c36f2217e98b708]::ErrorGuaranteed>>
44: 0x10d86b844 - rustc_span[7c36f2217e98b708]::set_source_map::<core[2ea8d1c0976e098]::result::Result<(), rustc_span[7c36f2217e98b708]::ErrorGuaranteed>, rustc_interface[c2a60cc96fc6f6d5]::interface::run_compiler<core[2ea8d1c0976e098]::result::Result<(), rustc_span[7c36f2217e98b708]::ErrorGuaranteed>, rustc_driver_impl[9e4f896e7075b60a]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
45: 0x10d865674 - std[c1662b6246061252]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[c2a60cc96fc6f6d5]::util::run_in_thread_pool_with_globals<rustc_interface[c2a60cc96fc6f6d5]::interface::run_compiler<core[2ea8d1c0976e098]::result::Result<(), rustc_span[7c36f2217e98b708]::ErrorGuaranteed>, rustc_driver_impl[9e4f896e7075b60a]::run_compiler::{closure#1}>::{closure#0}, core[2ea8d1c0976e098]::result::Result<(), rustc_span[7c36f2217e98b708]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2ea8d1c0976e098]::result::Result<(), rustc_span[7c36f2217e98b708]::ErrorGuaranteed>>
46: 0x10d85e2c4 - <<std[c1662b6246061252]::thread::Builder>::spawn_unchecked_<rustc_interface[c2a60cc96fc6f6d5]::util::run_in_thread_pool_with_globals<rustc_interface[c2a60cc96fc6f6d5]::interface::run_compiler<core[2ea8d1c0976e098]::result::Result<(), rustc_span[7c36f2217e98b708]::ErrorGuaranteed>, rustc_driver_impl[9e4f896e7075b60a]::run_compiler::{closure#1}>::{closure#0}, core[2ea8d1c0976e098]::result::Result<(), rustc_span[7c36f2217e98b708]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2ea8d1c0976e098]::result::Result<(), rustc_span[7c36f2217e98b708]::ErrorGuaranteed>>::{closure#1} as core[2ea8d1c0976e098]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
47: 0x10540860c - std::sys::unix::thread::Thread::new::thread_start::hf73630d59e230b3e
48: 0x192e22f94 - __pthread_joiner_wake
I can't seem to check out libcrux/dev@2914abfeae3a38e5cf689d3d0959e5a8845da6ea locally, did you force-push your branch since?
Turns out charon doesn't support constants in foreign crates at all:
fn foo() -> u8 {
other_crate::CONSTANT
}
This is a simple oversight on the hax side. I've got a fix, this is only blocked on charon catching up on recent hax changes.