A brief update on what’s happening in the Aeneas project at large.

Charon

  • The README has been updated. It’s now a good reflection of where the project is at and where we plan to go;
  • Thanks to the welcome help of @Vague, Charon now works on Windows;
  • Thanks again to @Vague, the cli interface of Charon was modernized and cleaner up. The old options are still available but will soon be deprecated. We’ve replaced:
    • charon [OPTIONS] becomes charon cargo [OPTIONS] [– CARGO_OPTIONS];
    • charon –no-cargo [OPTIONS] becomes charon rustc [OPTIONS] [– RUSTC_OPTIONS];
    • charon –read-llbc becomes charon pretty-print .
  • The –no-cargo –crate option was removed because it behaved inconsistently; use --rustc-arg=--crate-name= instead;
  • Charon now translates the lang_item identifier for built-in definitions. This makes it easier to recognize a number of built-ins like Box, String, Copy, etc;
  • Progress is ongoing towards supporting later MIRs (https://github.com/AeneasVerif/charon/issues/543).

Aeneas

  • the progress_pure and progress_pure_def attributes allow automatically lifting theorems and generating theorems from definitions so that progress can use them
  • several new tactics: zmodify (to convert propositions so that they manipulate elements of ZMod), simp_lists (to simplify expressions like List.get (List.set …) - it uses scalar_tac to discharge the proof obligations), simp_ifs (to simplify if then else expressions by using scalar_tac)
  • thanks to the work of Fernando Leal, a new progress* tactic allows repeatedly applying split and progress, while its variant progress*? generates the corresponding proof script. progress*, progress*? and progress can now use the keyword by to use a custom discharger for the preconditions. A new syntax is also possible for progress: let* ⟨ … ⟩ ← THM_NAME (with variants: let* ⟨ b, b_post ⟩ ← * and let* ⟨ b, b_post ⟩ ← *?).
  • simp procedures for elements of ZMod (that we intend to port to Mathlib), which simplify constants ((17 : ZMod 12) ~> (5 : ZMod 12)), inverses ((12⁻¹ : ZMod 7) ~> (3 : ZMod 7)) and powers (((2 ^ 16)⁻¹ : ZMod 3329) ~> (169 : ZMod 3329)).
  • removal of inefficient scalar_tac and simp lemmas which drastically improved the proof performance
  • many bug fixes and improvements in the tactics of the Lean backend
  • minor improvements of the quality of the extracted code when it contains arrays and slices
  • better handling of multi-files Lean projects with the -split-files and -subdir options
  • following changes in Charon, default trait methods are now handled properly the extracted global constants are now marked as irreducible, as Lean would otherwise expand them when trying to unify. The constants are also all marked with the global_simps simpset attribute.

Eurydice

  • Eurydice now demands that Charon be invoked with –remove-associated-types ‘*’, which in turn enables support for a larger class of iterators, such as chunks, chunks_exact, or range-step_by iterators – these are now all supported (but some implementations may be missing from eurydice_glue.h, please send PRs)
  • expand support for generating syntactic sugar for such iterators, notably, step_by iterators are now guaranteed to be emitted as for-loops
  • support for generating code that is C++17-compatible; by default, code generated by Eurydice requires either C11 or C++21 – for users who must use older versions of C++, the new -fcxx17-compat option generates code that is incompatible with C (any version) but compatible with C++17

Scylla

Significant progress, as we are now able to extract large chunks of HACL* from C to Rust automatically, directly using concrete C syntax as opposed to relying on the Low* intermediate representation.