Add newsletters from march to july

Author: R1kM

_posts/2025-03-07-aeneas-newsletter.markdown

@@ -0,0 +1,44 @@
+---
+layout: post
+title:  "Aeneas-news: March 2025"
+date:   2025-03-07 01:07:29 +0100
+categories: newsletter
+---
+A brief update on what's happening in the Aeneas project at large.
+
+## Charon
+* Support defaulted trait methods: when a trait has a method with a default implementation, impl blocks for this trait that don't override the method now get a copy of the default method.
+* Better error handling: Charon no longer tries to translate code that rustc would reject.
+* More parsimonious output: we no longer translate trait methods that aren't used; this greatly reduces the output when using traits like Iterator.
+* Added a charon --read-llbc <file.llbc> option that pretty-prints the contents of that llbc file.
+
+
+## Aeneas
+We dramatically improved Aeneas' extraction:
+* several changes were made to the code generation to improve its quality and make it more fit to proofs by mean of the progress tactic
+* Aeneas now makes use of Charon's option --remove-associated-types to lift the associated types so that they become parameters. In the short term, this will unlock support for a large class of traits, such as iterators.
+
+The Lean backend underwent a massive revamp. This includes:
+* changes in the definitions of the machine scalars. There are now two separate definitions, for signed and unsigned integers, and they use bitvectors in their internal representation.
+* building on the previous change, we added support for many more operations, such as bitwise operations or wrapping operations, together with the necessary reasoning lemmas
+* several attributes such as progress_pure and progress_pure_tac were introduced to automatically lift lemmas so that progress can use them, or automatically introduce progress lemmas for pure definitions
+* natify and bvify, inspired by zify, now allow converting propositions to propositions manipulating either natural numbers (useful to convert from bit-vectors or ZMod) or bit-vectors. A zmodify tactic is planned to complement those.
+* bv_tac combines bvify and bv_decide to efficiently reason by using bit-vectors
+several bug fixes for the progress tactics and quality of life improvements. For instance, progress with ... can now be given a term rather than an identifier.
+* scalar_tac is now a lot faster than before, more reliable, and solves more goals.
+several range definitions (which can be used with the syntax for ... in ...) together with the necessary theorems have been added to the library, for the purpose of writing clean and concise specification.
+* the extract_goal now allows (optionally) minimizing a goal and extracting it as a lemma. extract_assert introduces an assertion which proves the current goal.
+
+## Eurydice
+* Overhaul the initialization of arrays -- we should now avoid emitting 1000+ assignments for arrays that are initialized with zeroes.
+* Preliminary support for raw pointers
+* Allow recursion
+* Clean up the test suite to run faster
+* Do not hide translation failures anymore, and error out cleanly if something isn't supported (rather than silently generate no code)
+
+## Scylla
+A new projet, Scylla, is now public! https://github.com/AeneasVerif/scylla
+
+Scylla aims to translate very regular, data-oriented C code to safe Rust. The ambition is that the programmer should be actively involved in rewriting their C code until it is regular and understandable enough to become eligible to a translation to Safe Rust. This approach allows running performance benchmarks, regression, integration and unit tests in the same original C build environment. Once the programmer is confident that the rewrites introduced no errors, they can invoke Scylla to get clean, idiomatic Rust code with no unsafe blocks.
+
+Naturally, this does not apply to very many pieces of C code. For now, our chief use-case in the HACL* library, where we can already translate all of the bignums, along with the chacha20 algorithm. Expect to see more and more programs supported in the near future.

_posts/2025-04-07-aeneas-newsletter.markdown

@@ -0,0 +1,47 @@
+---
+layout: post
+title:  "Aeneas-news: April 2025"
+date:   2025-04-07 19:43:29 +0100
+categories: newsletter
+---
+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. We've replaced:
+    - charon [OPTIONS] becomes charon cargo [OPTIONS] [-- CARGO_OPTIONS];
+    - charon --no-cargo [OPTIONS] becomes charon rustc [OPTIONS] [-- RUSTC_OPTIONS];
+    - charon --read-llbc <path> becomes charon pretty-print <path>.
+    The old options are still available but will soon be deprecated.
+* The --no-cargo --crate <name> option was removed because it behaved inconsistently; use --rustc-arg=--crate-name=<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.

_posts/2025-05-15-aeneas-newsletter.markdown

@@ -0,0 +1,35 @@
+---
+layout: post
+title:  "Aeneas-news: May 2025"
+date:   2025-05-15 19:39:29 +0100
+categories: newsletter
+---
+## Charon
+* Significant progress on supporting later MIRs: most constant-related shanigans have been fixed;
+Added --mir elaborated which returns a MIR that includes drops. This works in common cases, open an issue if you encounter errors with this;
+* Progress towards better support for closures, thanks in particular to @Opale;
+* Added --start-from <name> to extract the given item instead of the whole current crate;
+@Opale added an experimental --monomorphize flag that monomorphizes the whole contents of the crate;
+* Upgraded the rustc used to build charon to a recent version.
+
+## Aeneas
+* make Aeneas more resilient to errors happening either when extracting the crate with Charon or during the translation (because of unsupported features in particular)
+* add support for dynamically sized types
+* add support for blanket implementations (those used to trigger name collisions)
+* add support for definitions with name clashes (in particular, functions and constants
+defined inside function bodies) by taking the Rust discriminators into account
+* general improvement of the Lean backends (more lemmas, general improvements to the tactics) and update to Lean v4.19.0
+
+## Eurydice
+* New internal library to facilitate authoring "peephole" optimizations that rewrite AST fragments; much better support for resugaring MIR loops as for-loops as a result, with more to come
+
+## Scylla
+* Considerable progress on the libclang-based frontend that now supports a much larger subset of actual C; many rewrites to make the translation more modular, and to synthesize well-typed internal krml ASTs before translation to Rust
+* Take into account C integer promotion rules
+* Take into account C assignments returning values
+* Support for nested assignments
+* General support for for-loops
+* Usability improvements with more user options
+* Handling of multifile projects
+* Support for bundling and visibility analysis
+* Handle C typedefs properly since the translation from C to krml's AST is type-driven

_posts/2025-06-03-aeneas-newsletter.markdown

@@ -0,0 +1,29 @@
+---
+layout: post
+title:  "Aeneas-news: June 2025"
+date:   2025-06-03 09:35:29 +0100
+categories: newsletter
+---
+## Charon
+* The representation of closures was reworked in depth thanks to @Opale. They are now translated as plain structs with the appropriate Fn{Mut,Once,} impls which should require no special support from users.
+* Work is in progress to reconstruct the information for which code runs in drop in a polymorphic context.
+* ULLBC now contains details about what happens when unwinding from a function call. This doesn't yet contain all unwinding data (it's missing drop unwinds and asserts). We plan to keep this ULLBC-only short term.
+* Thanks to @FireFighterDuck, Charon now emits layout information for types whose layout does not depend on generic parameters!
+
+## Aeneas
+* minor fixes and improvements of the Lean backend
+
+## Eurydice
+* Improved support for globals
+* Fix issues related to phase ordering and empty struct types
+* Broader support for DSTs, now supporting user-defined DSTs (e.g. struct T<U: ?Sized>), built-in DSTs (e.g. Box<[T]>), and proper coercions between the two (experimental, still some issues to be ironed out)
+
+## Scylla
+* Support for alignment directives
+* Properly implement integer conversion and integer promotion rules from C
+* Improved set of annotations to better control e.g. what goes to a Box type or not
+* Fixes related to post- vs pre-increment operators
+* Support for casts betwent uintN* and uint8* via scylla_lib
+* Add support for reconstructing tagged unions as ADTs
+* Add support for tuples
+* Add support for slice reconstruction

_posts/2025-07-02-aeneas-newsletter.markdown

@@ -0,0 +1,33 @@
+---
+layout: post
+title:  "Aeneas-news: July 2025"
+date:   2025-07-02 18:40:29 +0100
+categories: newsletter
+---
+## Charon
+* @FireFighterDuck added more details to the type layouts, in particular for the representation of enums;
+* @Opale added support for closure-to-fn-ptr casts;
+* Charon names no longer contain disambiguators for impls; this makes them more stable across time;
+* Work is ongoing to rework monomorphisation to be able to handle monomorphized layouts and evaluated constants;
+* @Opale added an option that translates Box sa a normal type instead of a built-in;
+* @ssyram added pointer metadata information to types (for DSTs);
+* Added support for the unstable trait_alias feature;
+* Various improvements and bug fixes, in particular around handling of generics.
+
+## Aeneas
+* the scalar_tac attribute can now be used on theorems with preconditions, such as:
+```
+@[scalar_tac x * y]
+theorem lt_mul_lt_le (x y a b : ℕ) (h0 : x < a) (h1 : y < b) :
+  x * y ≤ (a - 1) * (b - 1) := by apply Nat.le_mul_le; omega
+```
+* the tactics based on conditional rewriting with scalar_tac (simp_scalar, simp_lists, etc.) are now a lot faster
+* attributes like progress and scalar_tac are now compatible with asynchronous execution
+
+## Eurydice
+* Support for &str and &String (contribution by ssyram)
+* Support for u128 and i128 (contribution by ssyram)
+* Support for closures (multiple people, relying on upstream work in charon) via closure conversion
+* Improvements to the compilation scheme of reborrows (&*e)
+* Improvement: calls to array::from_fn may now be nested, and the closure passed to array::from_fn may now capture variables
+* Lots of improvements to handling of traits and the compilation of trait clauses -- several cases that were previously unsupported are now handled