charon

charon copied to clipboard

Tracking issue for not crashing on the rustc test suite

100

In https://github.com/AeneasVerif/charon/pull/136/ we added a script that runs charon on the rustc test suite and displays the results. As we'd like to support a large portion of the rust language,...

Nadrieril

Crash when using constants in arithmetic operations

2

Using constants in arithmetic leads to crashes in Charon. See these changes for reproducers. https://github.com/cryspen/libcrux/commit/5b23caf30914d9e71bb8cc29b15f1a355d4784f9 ``` 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...

franziskuskiefer

Support foreign constants

2

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'...

msprotz

Retrieve the result of drop elaboration

4

sonmarcho

Support for mutually recursive traits and functions

5

I am getting this error: ``` Compiling libcrux-ml-kem v0.0.2-pre.2 (/Users/jonathan/Code/libcrux/libcrux-ml-kem) warning: Could not find clauses for trait obligations:core::ops::function::FnMut Available clauses: [@TraitClause0]: core::iter::traits::iterator::Iterator [@TraitClause1]: core::ops::function::FnMut [@TraitClause2]: @TraitDecl21 [Self]: core::iter::traits::iterator::Iterator - context:...

msprotz

Rename Meta into SpanMeta

2

With the recent introduction of `ItemMeta`, the type `Meta` became slightly ambiguous. This PR renames it into `SpanMeta`. Fixes #116

R1kM

Support string literals

1

Thanks to https://github.com/hacspec/hax/pull/649, hax supports string literals as they show up in MIR. Fixes #72

Nadrieril

This generates an error: ``` const S: &str = "Hello"; ``` Error: ``` Unsupported constant: "ConstValue::Slice: Slice { data: ConstAllocation { .. }, start: 0, end: 98 }" ```

sonmarcho

Add support for vec macro

1

The [vec macro](https://doc.rust-lang.org/std/macro.vec.html#) is convenient for creating vectors. Currently, Charon fails to compile it, e.g.: ```rust fn foo() { let _v = vec![1]; } ``` ```bash $ charon Compiling vec_macro...

zhassan-aws

This issue tracks language features we don't support yet. - [x] `dyn Trait`: https://github.com/AeneasVerif/charon/issues/123 - [x] `for

Nadrieril