Aymeric Fromherz
Aymeric Fromherz
When running Charon commit 65c45918 on the crate ordnung commit e1f1e3bd, the following error related to mismatched generics appears: ``` error: Mismatched generics: expected: GenericParams { regions: [], types: [Some(TypeVar...
When running Charon on a virtual manifest, e.g., serde, Charon currently crashes with the following error message ``` error: manifest path `/Users/fromherz/Work/papers/charon-tool-paper/tools/serde/Cargo.toml` is a virtual manifest, but this command requires...
Charon commit https://github.com/AeneasVerif/charon/commit/e0b2b31542eaf8725757880ec62f27bc00a0007f aborts on the following code with error message `Compilation failed: error: Unimplemented: Alias(Alias { kind: Opaque, args: [Lifetime(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" })...
Charon commit e0b2b31 aborts on the following code with error message `Compilation failed: error: Unexpected `ShallowInitBox`` ```rust use std::vec; pub struct Error { messages: Vec, } pub struct IntoIter {...
The following code ```rust pub struct S; impl S { pub fn f Option { None } } ``` crashes on Charon version 8fe7c7311 with the following error message ```...
e.g., the process and annotations needed to use `charon::opaque` attributes
In the Lean backend, the `progress` tactic performs a lot of work to automate proofs and handle the Aeneas monadic translation. However, the current tactic also assumes particular shapes for...
E.g. ```rust trait LendingIterator { type Item Option
Consider the following minimal code snippet (done with @W95Psp and @TWal) ```fstar assume val p: int -> int -> prop assume val test: x:int -> y:int -> Lemma (p x...
Recapping here the list of Steel work items **Code Refactoring** - [x] Replace SteelAtomic unobservable and SteelAtomic observable by SteelGhost and SteelAtomic - [ ] Remove the quantification on invariant_names...