Tahina Ramananandro (professional account)

# Motivation Coming up with a domain-specific language for formally verified parsing and serialization at the right level of abstraction with runtime efficiency in mind is much larger a research...

#41 introduced module dependency analysis assuming that all .3d files are in the same directory. In #45, I heavily rely on this assumption when generating Makefiles by prefixing all source...

For now #45 supports GNU Make and NMAKE, but not [Ninja](https://ninja-build.org). Caveats: * Syntax for variables is different

Bring --batch closer to --makefile: make --batch sort and run GenMakefile tasks

1

# Motivation * One issue described by @aseemr and @nikswamy was that the Wrapper files produced by `--batch` make all modules on the command line share the same internal state,...

bitsum: try removing positivity constraint on `key_size`

1

https://github.com/project-everest/everparse/blob/452f1fedecf5c3413095787480ac3f1c7680e715/src/lowparse/LowParse.Spec.BitSum.fst#L21 Thank you @nikswamy for pointing this out. For now I will leave it as is, for the sake of merging your changes into master, CI permitting. Later I will...

3d: validate module names before processing

1

Suggested by @msprotz at https://github.com/project-everest/everparse/pull/15#discussion_r437675160

Suggested by @msprotz at https://github.com/project-everest/everparse/pull/15#discussion_r437039857

Missing low-level instances

2

List compiled by @ad-l Sum types: - [x] finalizers for explicit sum types - [ ] intro lemmas for implicit sum types - [x] accessors for explicit sum types -...

This issue is a follow-up to #254 . Currently, since merging that PR and project-everest/hacl-star#584, Everest upgrades have been breaking, since quic_provider was removed from HACL*. quic_provider should be replaced...

Avoid lemma duplication between `bool` and `prop` predicates

1

From @TWal in https://github.com/FStarLang/FStar/pull/3094#issuecomment-1810450113 : > The bool and prop properties are causing a lot of redundancy in ulib, but is it needed? While I agree that we need to...