ROMemories

Could you clarify the licenses of the various crates in the workspace? Only `stm32-metapac-gen` has a `license` key in its `Cargo.toml`, and there is no `LICENSE` file in the repository,...

Supporting the `Iterator` trait

3

hax does not currently seem to support the [`Iterator` trait](https://doc.rust-lang.org/stable/core/iter/trait.Iterator.html) in F*, when manually implementing it. For instance, the following does get extracted to F*, but does not lax check:...

F* typechecking fails when introducing an unused variable in `forall`

8

I need to use multiple variables in a [`hax_lib::forall`](https://hacspec.org/hax/frontend/hax_lib/fn.forall.html) refinement, I believe that making the predicate function take a tuple as parameter is the right way to do this, but...

Add units/unit prefixes of frequency to doc-valid-idents

1

These units/unit prefixes often come up in the embedded world. Should this PR also modify the `test_units` test? It seems only concerned with data units currently; should it also test...

Cannot access previous struct fields in `refine` attributes

7

It seems that the `refine` attribute does not allow referring to struct fields defined before the field on which the attribute is applied on. For instance, F* extraction fails on...

Extraction error with `const` generics and hax attribute on a struct field

7

I'm hitting an error during F* extraction, when having a hax attribute on a struct field using a `const` generic. Here is a reproducer (the actual attribute contents may not...

Possible unsoundness on architectures without atomics

6

My understanding is that `log` relies on atomics to implement some of its functionality, especially [`set_logger()`](https://docs.rs/log/latest/log/fn.set_logger.html) and [`set_max_level()`](https://docs.rs/log/latest/log/fn.set_max_level.html). It seems there is an internal "fake" `AtomicUsize` on platforms that do...

As mentioned in https://github.com/ariel-os/ariel-os/discussions/1449, by default laze spits out quite a few lines that might not be relevant to users, e.g.: ```sh laze: project root: [redacted]/ariel-os-hello relpath: . project_file: laze-project.yml...

Supporting module and context aliases

1

Would it be possible to add support for module and context aliases? That would be especially useful to avoid breaking changes when renaming modules or contexts. It could look like...

Would it be possible to also support the `.yaml` extension for YAML files? It has been [the recommended extension](https://yaml.org/faq) for a long time. I am not saying that every existing...